    -----------------------------------------------------------------------------
    -- |
    -- Module    : Documentation.SBV.Examples.Optimization.Production
    -- Copyright : (c) Levent Erkok
    -- License   : BSD3
    -- Maintainer: erkokl@gmail.com
    -- Stability : experimental
    --
    -- Solves a simple linear optimization problem
    -----------------------------------------------------------------------------

    {-# OPTIONS_GHC -Wall -Werror #-}

    module Documentation.SBV.Examples.Optimization.Production where

    import Data.SBV

    -- | Taken from <http://people.brunel.ac.uk/~mastjjb/jeb/or/morelp.html>
    --
    -- A company makes two products (X and Y) using two machines (A and B).
    --
    --   - Each unit of X that is produced requires 50 minutes processing time on machine
    --     A and 30 minutes processing time on machine B.
    --
    --   - Each unit of Y that is produced requires 24 minutes processing time on machine
    --     A and 33 minutes processing time on machine B.
    --
    --   - At the start of the current week there are 30 units of X and 90 units of Y in stock.
    --     Available processing time on machine A is forecast to be 40 hours and on machine B is
    --     forecast to be 35 hours.
    --
    --   - The demand for X in the current week is forecast to be 75 units and for Y is forecast
    --     to be 95 units.
    --
    --   - Company policy is to maximise the combined sum of the units of X and the units of Y
    --     in stock at the end of the week.
    --
    -- How much of each product should we make in the current week?
    --
    -- We have:
    --
    -- >>> optimize Lexicographic production
    -- Optimal model:
    --   X     = 45 :: Integer
    --   Y     =  6 :: Integer
    --   stock =  1 :: Integer
    --
    -- That is, we should produce 45 X's and 6 Y's, with the final maximum stock of just 1 expected!
    production :: Goal
    production :: Goal
    production = do SInteger
    x <- String -> Symbolic SInteger
    sInteger "X" -- Units of X produced
                    SInteger
    y <- String -> Symbolic SInteger
    sInteger "Y" -- Units of X produced

                    -- Amount of time on machine A and B
                    let timeA :: SInteger
    timeA = 50 SInteger -> SInteger -> SInteger
    forall a. Num a => a -> a -> a
    * SInteger
    x SInteger -> SInteger -> SInteger
    forall a. Num a => a -> a -> a
    + 24 SInteger -> SInteger -> SInteger
    forall a. Num a => a -> a -> a
    * SInteger
    y
                        timeB :: SInteger
    timeB = 30 SInteger -> SInteger -> SInteger
    forall a. Num a => a -> a -> a
    * SInteger
    x SInteger -> SInteger -> SInteger
    forall a. Num a => a -> a -> a
    + 33 SInteger -> SInteger -> SInteger
    forall a. Num a => a -> a -> a
    * SInteger
    y

                    SBool -> Goal
    forall (m :: * -> *). SolverContext m => SBool -> m ()
    constrain (SBool -> Goal) -> SBool -> Goal
    forall a b. (a -> b) -> a -> b
    $ SInteger
    timeA SInteger -> SInteger -> SBool
    forall a. OrdSymbolic a => a -> a -> SBool
    .<= 40 SInteger -> SInteger -> SInteger
    forall a. Num a => a -> a -> a
    * 60
                    SBool -> Goal
    forall (m :: * -> *). SolverContext m => SBool -> m ()
    constrain (SBool -> Goal) -> SBool -> Goal
    forall a b. (a -> b) -> a -> b
    $ SInteger
    timeB SInteger -> SInteger -> SBool
    forall a. OrdSymbolic a => a -> a -> SBool
    .<= 35 SInteger -> SInteger -> SInteger
    forall a. Num a => a -> a -> a
    * 60

                    -- Amount of product we'll end up with
                    let finalX :: SInteger
    finalX = SInteger
    x SInteger -> SInteger -> SInteger
    forall a. Num a => a -> a -> a
    + 30
                        finalY :: SInteger
    finalY = SInteger
    y SInteger -> SInteger -> SInteger
    forall a. Num a => a -> a -> a
    + 90

                    -- Make sure the demands are met:
                    SBool -> Goal
    forall (m :: * -> *). SolverContext m => SBool -> m ()
    constrain (SBool -> Goal) -> SBool -> Goal
    forall a b. (a -> b) -> a -> b
    $ SInteger
    finalX SInteger -> SInteger -> SBool
    forall a. OrdSymbolic a => a -> a -> SBool
    .>= 75
                    SBool -> Goal
    forall (m :: * -> *). SolverContext m => SBool -> m ()
    constrain (SBool -> Goal) -> SBool -> Goal
    forall a b. (a -> b) -> a -> b
    $ SInteger
    finalY SInteger -> SInteger -> SBool
    forall a. OrdSymbolic a => a -> a -> SBool
    .>= 95

                    -- Policy: Maximize the final stock
                    String -> SInteger -> Goal
    forall a. Metric a => String -> SBV a -> Goal
    maximize "stock" (SInteger -> Goal) -> SInteger -> Goal
    forall a b. (a -> b) -> a -> b
    $ (SInteger
    finalX SInteger -> SInteger -> SInteger
    forall a. Num a => a -> a -> a
    - 75) SInteger -> SInteger -> SInteger
    forall a. Num a => a -> a -> a
    + (SInteger
    finalY SInteger -> SInteger -> SInteger
    forall a. Num a => a -> a -> a
    - 95)