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