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