buy

Editor GitHub daydemirlibraries urban_space specs models thingsbuy
Editor
Visualization
	`mcdp { provides trees [Nat] provides sidewalks [Nat] provides benches [Nat] requires initial_budget [$] requires community_approval [dimensionless] budget_flex = 1 + required community_approval required initial_budget * budget_flex >= (provided trees * 1000 $) + (provided sidewalks * 400 $) + (provided benches * 2000 $) }`
Diagramremove
Other informationremove
Internal representation details
CompositeNDP                                                                                                                             
│    provides   trees       SB(≥0::1) │ requires   initial_budget       SB(≥0) $                                                         
│    provides   sidewalks   SB(≥0::1) │ requires   community_approval   SB(≥0)                                                           
│    provides   benches     SB(≥0::1) │                                                                                                  
│  11 nodes, 10 edges                                                                                                                    
│   connected rec: ✓                                                                                                                     
│  provided benches                    ≤ _op provided by _mult2          equiv id                                                        
│  provided sidewalks                  ≤ _op provided by _mult1          equiv id                                                        
│  provided trees                      ≤ _op provided by _mult           equiv id                                                        
│  budget_flex required by _invmult    ≤ _res provided by _invplusop     equiv id                                                        
│  initial_budget required by _invmult ≤ required initial_budget         equiv id                                                        
│  _op required by _invplusop          ≤ required community_approval     equiv id                                                        
│  _res required by _mult              ≤ _res provided by _sum           equiv id                                                        
│  _res2 required by _mult1            ≤ _res2 provided by _sum          equiv id                                                        
│  _res3 required by _mult2            ≤ _res3 provided by _sum          equiv id                                                        
│  _result required by _sum            ≤ _result2 provided by _invmult   diff  AmbientConversion SB(≥0::200) USD  ⇸  SB(≥0) USD  > D USD 
│                                                                               𝒇 ≤ 𝒓                                                    
├   _invmult: SimpleWrap                                                                                                                 
│             │  provides   _result2   SB(≥0) USD │ requires   initial_budget   SB(≥0) $                                                 
│             │                                   │ requires   budget_flex      SB(≥1)                                                   
│             └ M_Fun_MultiplyMany_DP SB(≥0) USD  ⇸  SB(≥0)×SB(≥1) ⟨$,dimensionless⟩                                                     
│                𝒇 ≤ 𝒓₁⋅𝒓₂                                                                                                               
│               ├   Rs: ├ SB(≥0) $                                                                                                       
│               │       └ SB(≥1)                                                                                                         
│               └ algo: ApproximationAlgorithms - ApproximationAlgorithms.VAN_DER_CORPUT                                                 
├ _invplusop: SimpleWrap                                                                                                                 
│             │  provides   _res   SB(≥1) │ requires   _op   SB(≥0)                                                                      
│             └ DP_L_LME SB(≥1)  ⇸  SB(≥0)                                                                                               
│                𝒇 ≤ 𝒓 + 1                                                                                                               
│               M_C_WrapUnits   dimensionless → dimensionless > M_A_Add1_Lower   SB(≥0)  →  SB(≥1) x ⟼ x + 1                             
├      _mult: SimpleWrap                                                                                                                 
│             │  provides   _op   SB(≥0::1) │ requires   _res   SB(≥0::1000) USD                                                         
│             └ DP_L_UME SB(≥0::1)  ⇸  SB(≥0::1000) USD                                                                                  
│                𝒇 ⋅ 1000 ≤ 𝒓                                                                                                            
│               M_C_WrapUnits   dimensionless → USD > M_A_Mult1_Upper   SB(≥0::1)  →  SB(≥0::1000) x ⟼ x ⋅ 1000                          
├     _mult1: SimpleWrap                                                                                                                 
│             │  provides   _op   SB(≥0::1) │ requires   _res2   SB(≥0::400) USD                                                         
│             └ DP_L_UME SB(≥0::1)  ⇸  SB(≥0::400) USD                                                                                   
│                𝒇 ⋅ 400 ≤ 𝒓                                                                                                             
│               M_C_WrapUnits   dimensionless → USD > M_A_Mult1_Upper   SB(≥0::1)  →  SB(≥0::400) x ⟼ x ⋅ 400                            
├     _mult2: SimpleWrap                                                                                                                 
│             │  provides   _op   SB(≥0::1) │ requires   _res3   SB(≥0::2000) USD                                                        
│             └ DP_L_UME SB(≥0::1)  ⇸  SB(≥0::2000) USD                                                                                  
│                𝒇 ⋅ 2000 ≤ 𝒓                                                                                                            
│               M_C_WrapUnits   dimensionless → USD > M_A_Mult1_Upper   SB(≥0::1)  →  SB(≥0::2000) x ⟼ x ⋅ 2000                          
└       _sum: SimpleWrap                                                                                                                 
              │  provides   _res    SB(≥0::1000) USD │ requires   _result   SB(≥0::200) USD                                              
              │  provides   _res2   SB(≥0::400) USD  │                                                                                   
              │  provides   _res3   SB(≥0::2000) USD │                                                                                   
              └ M_Res_AddMany_DP WU ⟨USD,USD,USD⟩   ⇸  SB(≥0::200) USD                                                                   
                                 └ Π<3>                                                                                                  
                                   ├ SB(≥0::1000)                                                                                        
                                   ├ SB(≥0::400)                                                                                         
                                   └ SB(≥0::2000)                                                                                        
                 𝒇₁ + 𝒇₂ + 𝒇₃ ≤ 𝒓                                                                                                        
                ├      Fs: ├ SB(≥0::1000) USD                                                                                            
                │          ├ SB(≥0::400) USD                                                                                             
                │          └ SB(≥0::2000) USD                                                                                            
                ├ opspace: SB(≥0::200) USD                                                                                               
                └    algo: ApproximationAlgorithms - ApproximationAlgorithms.VAN_DER_CORPUT