    -----------------------------------------------------------------------------
    -- |
    -- Module    : Documentation.SBV.Examples.Optimization.LinearOpt
    -- Copyright : (c) Levent Erkok
    -- License   : BSD3
    -- Maintainer: erkokl@gmail.com
    -- Stability : experimental
    --
    -- Simple linear optimization example, as found in operations research texts.
    -----------------------------------------------------------------------------

    {-# OPTIONS_GHC -Wall -Werror #-}

    module Documentation.SBV.Examples.Optimization.LinearOpt where

    import Data.SBV

    -- $setup
    -- >>> -- For doctest purposes only:
    -- >>> import Data.SBV

    -- | Taken from <http://people.brunel.ac.uk/~mastjjb/jeb/or/morelp.html>
    --
    --    *  maximize 5x1 + 6x2
    --       - subject to
    --
    --          1. x1 + x2 <= 10
    --          2. x1 - x2 >= 3
    --          3. 5x1 + 4x2 <= 35
    --          4. x1 >= 0
    --          5. x2 >= 0
    --
    -- >>> optimize Lexicographic problem
    -- Optimal model:
    --   x1   =  47 % 9 :: Real
    --   x2   =  20 % 9 :: Real
    --   goal = 355 % 9 :: Real
    problem :: ConstraintSet
    problem :: ConstraintSet
    problem = do [SReal
    x1, 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)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    mapM String -> SymbolicT IO SReal
    sReal [String
    "x1", String
    "x2"]

                 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
    x1 SReal -> SReal -> SReal
    forall a. Num a => a -> a -> a
    + SReal
    x2 SReal -> SReal -> SBool
    forall a. OrdSymbolic a => a -> a -> SBool
    .<= SReal
    10
                 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
    x1 SReal -> SReal -> SReal
    forall a. Num a => a -> a -> a
    - SReal
    x2 SReal -> SReal -> SBool
    forall a. OrdSymbolic a => a -> a -> SBool
    .>= SReal
    3
                 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
    5SReal -> SReal -> SReal
    forall a. Num a => a -> a -> a
    *SReal
    x1 SReal -> SReal -> SReal
    forall a. Num a => a -> a -> a
    + SReal
    4SReal -> SReal -> SReal
    forall a. Num a => a -> a -> a
    *SReal
    x2 SReal -> SReal -> SBool
    forall a. OrdSymbolic a => a -> a -> SBool
    .<= SReal
    35
                 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
    x1 SReal -> SReal -> SBool
    forall a. OrdSymbolic a => a -> a -> SBool
    .>= SReal
    0
                 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
    x2 SReal -> SReal -> SBool
    forall a. OrdSymbolic a => a -> a -> SBool
    .>= SReal
    0

                 String -> SReal -> ConstraintSet
    forall a. Metric a => String -> SBV a -> ConstraintSet
    maximize String
    "goal" (SReal -> ConstraintSet) -> SReal -> ConstraintSet
    forall a b. (a -> b) -> a -> b
    $ SReal
    5 SReal -> SReal -> SReal
    forall a. Num a => a -> a -> a
    * SReal
    x1 SReal -> SReal -> SReal
    forall a. Num a => a -> a -> a
    + SReal
    6 SReal -> SReal -> SReal
    forall a. Num a => a -> a -> a
    * SReal
    x2