plusinv3

Editor GitHub co-design-modelslibraries example_plusinv specs models thingsplusinv3
Editor
Visualization
	`# this has a (4,4) isolated solution: # x + y >= ceil(sqrt(x)) + ceil(sqrt(y)) + 4 mcdp { provides z [dimensionless] variable x, y [dimensionless] x + y ≽ ceil(sqrt(x)) + ceil(sqrt(y)) + provided z requires x, y }`
Diagramremove
Other informationremove
Internal representation details
CompositeNDP                                                                                        
│    provides   z   SB(≥0) │ requires   x   SB(≥0)                                                  
│                          │ requires   y   SB(≥0)                                                  
│  9 nodes, 10 edges                                                                                
│   connected rec: ✓                                                                                
│  _res2 required by _RuleResCeil_NWU  ≤ _res2 provided by _sum              equiv id               
│  _res4 required by _RuleResCeil_NWU1 ≤ _res4 provided by _sum              equiv id               
│  _res required by _RuleResSQRT_NWU   ≤ _op provided by _RuleResCeil_NWU    equiv id               
│  _res3 required by _RuleResSQRT_NWU1 ≤ _op provided by _RuleResCeil_NWU1   equiv id               
│  provided z                          ≤ z provided by _sum                  equiv id               
│  _x required by _invplus             ≤ _op provided by _RuleResSQRT_NWU    equiv id               
│  _x required by _invplus             ≤ required x                          equiv id               
│  _y required by _invplus             ≤ _op provided by _RuleResSQRT_NWU1   equiv id               
│  _y required by _invplus             ≤ required y                          equiv id               
│  _result required by _sum            ≤ _result2 provided by _invplus       equiv id               
├  _RuleResCeil_NWU: SimpleWrap                                                                     
│                    │  provides   _op   SB(≥0) │ requires   _res2   SB(≥0::1)                      
│                    └ DP_L_UME SB(≥0)  ⇸  SB(≥0::1)                                                
│                       ceil(𝒇) ≤ 𝒓                                                                 
│                      └ M_C_WrapUnits   dimensionless → dimensionless                              
│                        M_A_RoundUp   SB(≥0)  →  SB(≥0::1) x ⟼ ceil(x)                             
├ _RuleResCeil_NWU1: SimpleWrap                                                                     
│                    │  provides   _op   SB(≥0) │ requires   _res4   SB(≥0::1)                      
│                    └ DP_L_UME SB(≥0)  ⇸  SB(≥0::1)                                                
│                       ceil(𝒇) ≤ 𝒓                                                                 
│                      └ M_C_WrapUnits   dimensionless → dimensionless                              
│                        M_A_RoundUp   SB(≥0)  →  SB(≥0::1) x ⟼ ceil(x)                             
├  _RuleResSQRT_NWU: SimpleWrap                                                                     
│                    │  provides   _op   SB(≥0) │ requires   _res   SB(≥0)                          
│                    └ DP_L_UME SB(≥0)  ⇸  SB(≥0)                                                   
│                       𝒇^½ ≤ 𝒓                                                                     
│                      └ M_C_WrapUnits   dimensionless → dimensionless                              
│                        M_A_PowerFrac_Upper   SB(≥0)  →   same x ⟼ x^½                             
├ _RuleResSQRT_NWU1: SimpleWrap                                                                     
│                    │  provides   _op   SB(≥0) │ requires   _res3   SB(≥0)                         
│                    └ DP_L_UME SB(≥0)  ⇸  SB(≥0)                                                   
│                       𝒇^½ ≤ 𝒓                                                                     
│                      └ M_C_WrapUnits   dimensionless → dimensionless                              
│                        M_A_PowerFrac_Upper   SB(≥0)  →   same x ⟼ x^½                             
├          _invplus: SimpleWrap                                                                     
│                    │  provides   _result2   SB(≥0) │ requires   _x   SB(≥0)                       
│                    │                               │ requires   _y   SB(≥0)                       
│                    └ M_Fun_AddMany_DP SB(≥0)  ⇸  WU ⟨dimensionless,dimensionless⟩                 
│                                                  (_x:SB(≥0)×_y:SB(≥0))                            
│                       𝒇 ≤ 𝒓₁ + 𝒓₂                                                                 
│                      ├   opspace: SB(≥0)                                                          
│                      ├        Rs: ├ SB(≥0)                                                        
│                      │            └ SB(≥0)                                                        
│                      ├ Rs_labels: ├ _x                                                            
│                      │            └ _y                                                            
│                      └      algo: ApproximationAlgorithms - ApproximationAlgorithms.VAN_DER_CORPUT
└              _sum: SimpleWrap                                                                     
                     │  provides   _res2   SB(≥0::1) │ requires   _result   SB(≥0)                  
                     │  provides   _res4   SB(≥0::1) │                                              
                     │  provides   z       SB(≥0)    │                                              
                     └ M_Res_AddMany_DP WU ⟨dimensionless,dimensionless,dimensionless⟩  ⇸  SB(≥0)   
                                        └ Π<3>                                                      
                                          ├ SB(≥0::1)                                               
                                          ├ SB(≥0::1)                                               
                                          └ SB(≥0)                                                  
                        𝒇₁ + 𝒇₂ + 𝒇₃ ≤ 𝒓                                                            
                       ├      Fs: ├ SB(≥0::1)                                                       
                       │          ├ SB(≥0::1)                                                       
                       │          └ SB(≥0)                                                          
                       ├ opspace: SB(≥0)                                                            
                       └    algo: ApproximationAlgorithms - ApproximationAlgorithms.VAN_DER_CORPUT