{-# OPTIONS_GHC -Wall -Werror #-}
module Documentation.SBV.Examples.Optimization.ExtField where
import Data.SBV
problem :: ConstraintSet
problem :: ConstraintSet
problem = do SBV Integer
x <- String -> Symbolic (SBV Integer)
sInteger String
"x"
SReal
y <- String -> Symbolic SReal
sReal String
"y"
SReal
z <- String -> Symbolic SReal
sReal String
"z"
String -> SBV Integer -> ConstraintSet
forall a. Metric a => String -> SBV a -> ConstraintSet
maximize String
"one-x" (SBV Integer -> ConstraintSet) -> SBV Integer -> ConstraintSet
forall a b. (a -> b) -> a -> b
$ SBV Integer
1 SBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
- SBV Integer
x
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
$ SReal
y SReal -> SReal -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SReal
0 SBool -> SBool -> SBool
.&& SReal
z SReal -> SReal -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SReal
5
String -> SReal -> ConstraintSet
forall a. Metric a => String -> SBV a -> ConstraintSet
minimize String
"min_y" (SReal -> ConstraintSet) -> SReal -> ConstraintSet
forall a b. (a -> b) -> a -> b
$ SReal
2SReal -> SReal -> SReal
forall a. Num a => a -> a -> a
+SReal
ySReal -> SReal -> SReal
forall a. Num a => a -> a -> a
+SReal
z
String -> SReal -> ConstraintSet
forall a. Metric a => String -> SBV a -> ConstraintSet
minimize String
"min_z" SReal
z