{-# OPTIONS_GHC -Wall -Werror #-}
module Documentation.SBV.Examples.Optimization.VM where
import Data.SBV
allocate :: Goal
allocate :: Goal
allocate = do
x1 :: [SBool]
x1@[x11 :: SBool
x11, x12 :: SBool
x12, x13 :: SBool
x13] <- [String] -> Symbolic [SBool]
sBools ["x11", "x12", "x13"]
x2 :: [SBool]
x2@[x21 :: SBool
x21, x22 :: SBool
x22, x23 :: SBool
x23] <- [String] -> Symbolic [SBool]
sBools ["x21", "x22", "x23"]
x3 :: [SBool]
x3@[x31 :: SBool
x31, x32 :: SBool
x32, x33 :: SBool
x33] <- [String] -> Symbolic [SBool]
sBools ["x31", "x32", "x33"]
SBool -> Goal
forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain (SBool -> Goal) -> SBool -> Goal
forall a b. (a -> b) -> a -> b
$ [SBool] -> SBool
pbStronglyMutexed [SBool]
x1
SBool -> Goal
forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain (SBool -> Goal) -> SBool -> Goal
forall a b. (a -> b) -> a -> b
$ [SBool] -> SBool
pbStronglyMutexed [SBool]
x2
SBool -> Goal
forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain (SBool -> Goal) -> SBool -> Goal
forall a b. (a -> b) -> a -> b
$ [SBool] -> SBool
pbStronglyMutexed [SBool]
x3
let need :: [SBool] -> SInteger
need :: [SBool] -> SInteger
need rs :: [SBool]
rs = [SInteger] -> SInteger
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum ([SInteger] -> SInteger) -> [SInteger] -> SInteger
forall a b. (a -> b) -> a -> b
$ (SBool -> SInteger -> SInteger)
-> [SBool] -> [SInteger] -> [SInteger]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\r :: SBool
r c :: SInteger
c -> SBool -> SInteger -> SInteger -> SInteger
forall a. Mergeable a => SBool -> a -> a -> a
ite SBool
r SInteger
c 0) [SBool]
rs [100, 50, 15]
let capacity1 :: SInteger
capacity1 = [SBool] -> SInteger
need [SBool
x11, SBool
x21, SBool
x31]
capacity2 :: SInteger
capacity2 = [SBool] -> SInteger
need [SBool
x12, SBool
x22, SBool
x32]
capacity3 :: SInteger
capacity3 = [SBool] -> SInteger
need [SBool
x13, SBool
x23, SBool
x33]
SBool -> Goal
forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain (SBool -> Goal) -> SBool -> Goal
forall a b. (a -> b) -> a -> b
$ SInteger
capacity1 SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= 100
SBool -> Goal
forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain (SBool -> Goal) -> SBool -> Goal
forall a b. (a -> b) -> a -> b
$ SInteger
capacity2 SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= 75
SBool -> Goal
forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain (SBool -> Goal) -> SBool -> Goal
forall a b. (a -> b) -> a -> b
$ SInteger
capacity3 SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= 200
let y1 :: SBool
y1 = [SBool] -> SBool
sOr [SBool
x11, SBool
x21, SBool
x31]
y2 :: SBool
y2 = [SBool] -> SBool
sOr [SBool
x12, SBool
x22, SBool
x32]
y3 :: SBool
y3 = [SBool] -> SBool
sOr [SBool
x13, SBool
x23, SBool
x33]
b2n :: SBool -> a
b2n b :: SBool
b = SBool -> a -> a -> a
forall a. Mergeable a => SBool -> a -> a -> a
ite SBool
b 1 0
let noOfServers :: SInteger
noOfServers = [SInteger] -> SInteger
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum ([SInteger] -> SInteger) -> [SInteger] -> SInteger
forall a b. (a -> b) -> a -> b
$ (SBool -> SInteger) -> [SBool] -> [SInteger]
forall a b. (a -> b) -> [a] -> [b]
map SBool -> SInteger
forall a. (Mergeable a, Num a) => SBool -> a
b2n [SBool
y1, SBool
y2, SBool
y3]
String -> SInteger -> Goal
forall a. Metric a => String -> SBV a -> Goal
minimize "noOfServers" (SInteger
noOfServers :: SInteger)
let cost1 :: SInteger
cost1 = SBool -> SInteger -> SInteger -> SInteger
forall a. Mergeable a => SBool -> a -> a -> a
ite SBool
y1 10 0
cost2 :: SInteger
cost2 = SBool -> SInteger -> SInteger -> SInteger
forall a. Mergeable a => SBool -> a -> a -> a
ite SBool
y2 5 0
cost3 :: SInteger
cost3 = SBool -> SInteger -> SInteger -> SInteger
forall a. Mergeable a => SBool -> a -> a -> a
ite SBool
y3 20 0
String -> SInteger -> Goal
forall a. Metric a => String -> SBV a -> Goal
minimize "cost" (SInteger
cost1 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
cost2 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
cost3 :: SInteger)