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

-- $setup
-- >>> -- For doctest purposes only:
-- >>> 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 String
"X" -- Units of X produced
                SInteger
y <- String -> Symbolic SInteger
sInteger String
"Y" -- Units of X produced

                -- Amount of time on machine A and B
                let timeA :: SInteger
timeA = SInteger
50 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* SInteger
x SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
24 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* SInteger
y
                    timeB :: SInteger
timeB = SInteger
30 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* SInteger
x SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
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
.<= SInteger
40 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* SInteger
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
.<= SInteger
35 SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
* SInteger
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
+ SInteger
30
                    finalY :: SInteger
finalY = SInteger
y SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
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
.>= SInteger
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
.>= SInteger
95

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