{-# OPTIONS_GHC -Wall -Werror #-}
module Documentation.SBV.Examples.Optimization.Production where
import Data.SBV
production :: ConstraintSet
production :: ConstraintSet
production = do SInteger
x <- String -> Symbolic SInteger
sInteger String
"X"
SInteger
y <- String -> Symbolic SInteger
sInteger String
"Y"
let timeA :: SInteger
timeA = SInteger
50 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* SInteger
x SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
24 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* SInteger
y
timeB :: SInteger
timeB = SInteger
30 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* SInteger
x SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
33 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* SInteger
y
SBool -> ConstraintSet
forall a. QuantifiedBool a => a -> ConstraintSet
forall (m :: * -> *) a.
(SolverContext m, QuantifiedBool a) =>
a -> m ()
constrain (SBool -> ConstraintSet) -> SBool -> ConstraintSet
forall a b. (a -> b) -> a -> b
$ SInteger
timeA SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
40 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* SInteger
60
SBool -> ConstraintSet
forall a. QuantifiedBool a => a -> ConstraintSet
forall (m :: * -> *) a.
(SolverContext m, QuantifiedBool a) =>
a -> m ()
constrain (SBool -> ConstraintSet) -> SBool -> ConstraintSet
forall a b. (a -> b) -> a -> b
$ SInteger
timeB SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
35 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* SInteger
60
let finalX :: SInteger
finalX = SInteger
x SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
30
finalY :: SInteger
finalY = SInteger
y SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
90
SBool -> ConstraintSet
forall a. QuantifiedBool a => a -> ConstraintSet
forall (m :: * -> *) a.
(SolverContext m, QuantifiedBool a) =>
a -> m ()
constrain (SBool -> ConstraintSet) -> SBool -> ConstraintSet
forall a b. (a -> b) -> a -> b
$ SInteger
finalX SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
75
SBool -> ConstraintSet
forall a. QuantifiedBool a => a -> ConstraintSet
forall (m :: * -> *) a.
(SolverContext m, QuantifiedBool a) =>
a -> m ()
constrain (SBool -> ConstraintSet) -> SBool -> ConstraintSet
forall a b. (a -> b) -> a -> b
$ SInteger
finalY SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
95
String -> SInteger -> ConstraintSet
forall a. Metric a => String -> SBV a -> ConstraintSet
maximize String
"stock" (SInteger -> ConstraintSet) -> SInteger -> ConstraintSet
forall a b. (a -> b) -> a -> b
$ (SInteger
finalX SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- SInteger
75) SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ (SInteger
finalY SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- SInteger
95)