-----------------------------------------------------------------------------
-- |
-- 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 [SReal
x1, 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 [String
"x1", String
"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
.<= SReal
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
.>= SReal
3
             SBool -> Goal
forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain (SBool -> Goal) -> SBool -> Goal
forall a b. (a -> b) -> a -> b
$ SReal
5SReal -> SReal -> SReal
forall a. Num a => a -> a -> a
*SReal
x1 SReal -> SReal -> SReal
forall a. Num a => a -> a -> a
+ SReal
4SReal -> SReal -> SReal
forall a. Num a => a -> a -> a
*SReal
x2 SReal -> SReal -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SReal
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
.>= SReal
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
.>= SReal
0

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