    -----------------------------------------------------------------------------
    -- |
    -- 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

    -- | 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 :: 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