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