{-# OPTIONS_GHC -Wall -Werror #-}
module Documentation.SBV.Examples.Optimization.LinearOpt where
import Data.SBV
problem :: Goal
problem :: Goal
problem = do [x1 :: SReal
x1, x2 :: SReal
x2] <- (String -> SymbolicT IO SReal) -> [String] -> SymbolicT IO [SReal]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM String -> SymbolicT IO SReal
sReal ["x1", "x2"]
SBool -> Goal
forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain (SBool -> Goal) -> SBool -> Goal
forall a b. (a -> b) -> a -> b
$ SReal
x1 SReal -> SReal -> SReal
forall a. Num a => a -> a -> a
+ SReal
x2 SReal -> SReal -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= 10
SBool -> Goal
forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain (SBool -> Goal) -> SBool -> Goal
forall a b. (a -> b) -> a -> b
$ SReal
x1 SReal -> SReal -> SReal
forall a. Num a => a -> a -> a
- SReal
x2 SReal -> SReal -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= 3
SBool -> Goal
forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain (SBool -> Goal) -> SBool -> Goal
forall a b. (a -> b) -> a -> b
$ 5SReal -> SReal -> SReal
forall a. Num a => a -> a -> a
*SReal
x1 SReal -> SReal -> SReal
forall a. Num a => a -> a -> a
+ 4SReal -> SReal -> SReal
forall a. Num a => a -> a -> a
*SReal
x2 SReal -> SReal -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= 35
SBool -> Goal
forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain (SBool -> Goal) -> SBool -> Goal
forall a b. (a -> b) -> a -> b
$ SReal
x1 SReal -> SReal -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= 0
SBool -> Goal
forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain (SBool -> Goal) -> SBool -> Goal
forall a b. (a -> b) -> a -> b
$ SReal
x2 SReal -> SReal -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= 0
String -> SReal -> Goal
forall a. Metric a => String -> SBV a -> Goal
maximize "goal" (SReal -> Goal) -> SReal -> Goal
forall a b. (a -> b) -> a -> b
$ 5 SReal -> SReal -> SReal
forall a. Num a => a -> a -> a
* SReal
x1 SReal -> SReal -> SReal
forall a. Num a => a -> a -> a
+ 6 SReal -> SReal -> SReal
forall a. Num a => a -> a -> a
* SReal
x2