-----------------------------------------------------------------------------
-- |
-- 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 :: Goal
problem :: Goal
problem = do [SReal
x1, SReal
x2] <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM String -> Symbolic SReal
sReal [String
"x1", String
"x2"]

             forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain forall a b. (a -> b) -> a -> b
$ SReal
x1 forall a. Num a => a -> a -> a
+ SReal
x2 forall a. OrdSymbolic a => a -> a -> SBool
.<= SReal
10
             forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain forall a b. (a -> b) -> a -> b
$ SReal
x1 forall a. Num a => a -> a -> a
- SReal
x2 forall a. OrdSymbolic a => a -> a -> SBool
.>= SReal
3
             forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain forall a b. (a -> b) -> a -> b
$ SReal
5forall a. Num a => a -> a -> a
*SReal
x1 forall a. Num a => a -> a -> a
+ SReal
4forall a. Num a => a -> a -> a
*SReal
x2 forall a. OrdSymbolic a => a -> a -> SBool
.<= SReal
35
             forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain forall a b. (a -> b) -> a -> b
$ SReal
x1 forall a. OrdSymbolic a => a -> a -> SBool
.>= SReal
0
             forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain forall a b. (a -> b) -> a -> b
$ SReal
x2 forall a. OrdSymbolic a => a -> a -> SBool
.>= SReal
0

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