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 [s] variable x, y [s] x + y ≽ ceil(sqrt(x)) + ceil(sqrt(y)) + provided z requires x, y }`
Diagramremove
Other informationremove
Internal representation details
CompositeNDP                                                                                                                   
│    provides   z   SB(≥0) s │ requires   x   SB(≥0) s                                                                         
│                            │ requires   y   SB(≥0) s                                                                         
│  9 nodes, 6 edges                                                                                                            
│   connected rec: ✓                                                                                                           
│  _res required by _RuleResSQRT_NWU   ≤ _op provided by _RuleResCeil_NWU    equiv id                                          
│  _res3 required by _RuleResSQRT_NWU1 ≤ _op provided by _RuleResCeil_NWU1   equiv id                                          
│  _x required by x                    ≤ _op provided by _RuleResSQRT_NWU    equiv id                                          
│  _x required by x                    ≤ required x                          equiv id                                          
│  _y required by y                    ≤ _op provided by _RuleResSQRT_NWU1   equiv id                                          
│  _y required by y                    ≤ required y                          equiv id                                          
│  Unconnected func:                                                                                                           
│   {CFunction(dp='y', s='_y'), CFunction(dp='x', s='_x')}                                                                     
│  Unconnected res:                                                                                                            
│   {CResource(dp='_RuleResCeil_NWU1', s='_res4'), CResource(dp='_fun_z', s='z'), CResource(dp='_RuleResCeil_NWU', s='_res2')} 
├  _RuleResCeil_NWU: SimpleWrap                                                                                                
│                    │  provides   _op   SB(≥0) s^0.5 │ requires   _res2   SB(≥0::1) s^0.5                                     
│                    └ DP_L_UME SB(≥0) s^0.5  ⇸  SB(≥0::1) s^0.5                                                               
│                       ceil(𝒇) ≤ 𝒓                                                                                            
│                      M_C_WrapUnits   s^0.5 → s^0.5 > M_A_RoundUp   SB(≥0)  →  SB(≥0::1) x ⟼ ceil(x)                          
├ _RuleResCeil_NWU1: SimpleWrap                                                                                                
│                    │  provides   _op   SB(≥0) s^0.5 │ requires   _res4   SB(≥0::1) s^0.5                                     
│                    └ DP_L_UME SB(≥0) s^0.5  ⇸  SB(≥0::1) s^0.5                                                               
│                       ceil(𝒇) ≤ 𝒓                                                                                            
│                      M_C_WrapUnits   s^0.5 → s^0.5 > M_A_RoundUp   SB(≥0)  →  SB(≥0::1) x ⟼ ceil(x)                          
├  _RuleResSQRT_NWU: SimpleWrap                                                                                                
│                    │  provides   _op   SB(≥0) s │ requires   _res   SB(≥0) s^0.5                                             
│                    └ DP_L_UME SB(≥0) s  ⇸  SB(≥0) s^0.5                                                                      
│                       𝒇^½ ≤ 𝒓                                                                                                
│                      M_C_WrapUnits   s → s^0.5 > M_A_PowerFrac_Upper   SB(≥0)  →   same x ⟼ x^½                              
├ _RuleResSQRT_NWU1: SimpleWrap                                                                                                
│                    │  provides   _op   SB(≥0) s │ requires   _res3   SB(≥0) s^0.5                                            
│                    └ DP_L_UME SB(≥0) s  ⇸  SB(≥0) s^0.5                                                                      
│                       𝒇^½ ≤ 𝒓                                                                                                
│                      M_C_WrapUnits   s → s^0.5 > M_A_PowerFrac_Upper   SB(≥0)  →   same x ⟼ x^½                              
├                 x: SimpleWrap                                                                                                
│                    │  provides   _x   SB(≥0) s │ requires   _x   SB(≥0) s                                                    
│                    └ DP_Id SB(≥0) s  ⇸  SB(≥0) s                                                                             
│                       𝒇 ≤ 𝒓                                                                                                  
└                 y: SimpleWrap                                                                                                
                     │  provides   _y   SB(≥0) s │ requires   _y   SB(≥0) s                                                    
                     └ DP_Id SB(≥0) s  ⇸  SB(≥0) s                                                                             
                        𝒇 ≤ 𝒓