{-# LANGUAGE ScopedTypeVariables #-}
{-# OPTIONS_GHC -Wall #-}
{-# OPTIONS_HADDOCK show-extensions #-}
-----------------------------------------------------------------------------
-- |
-- Module      :  ToySolver.Arith.Simplex.Textbook.LPSolver
-- Copyright   :  (c) Masahiro Sakai 2011
-- License     :  BSD-style
--
-- Maintainer  :  masahiro.sakai@gmail.com
-- Stability   :  provisional
-- Portability :  non-portable
--
-- Naïve implementation of Simplex method
--
-- Reference:
--
-- * <http://www.math.cuhk.edu.hk/~wei/lpch3.pdf>
--
-----------------------------------------------------------------------------

module ToySolver.Arith.Simplex.Textbook.LPSolver
  (
  -- * Solver type
    Solver
  , emptySolver

  -- * LP monad
  , LP
  , getTableau
  , putTableau

  -- * Problem specification
  , newVar
  , addConstraint
  , addConstraintWithArtificialVariable
  , tableau
  , define

  -- * Solving
  , phaseI
  , simplex
  , dualSimplex
  , OptResult (..)
  , twoPhaseSimplex
  , primalDualSimplex

  -- * Extract results
  , getModel

  -- * Utilities
  , collectNonnegVars
  ) where

import Control.Exception (assert)
import Control.Monad
import Control.Monad.State
import qualified Data.IntMap as IM
import qualified Data.IntSet as IS
import Data.OptDir
import Data.VectorSpace

import Data.Interval ((<=!), (>=!), (==!), (<!), (>!), (/=!))
import qualified Data.Interval as Interval

import ToySolver.Data.OrdRel
import qualified ToySolver.Data.LA as LA
import ToySolver.Data.IntVar
import qualified ToySolver.Arith.Simplex.Textbook as Simplex
import qualified ToySolver.Arith.BoundsInference as BI

-- ---------------------------------------------------------------------------
-- Solver type

type Solver r = (Var, Simplex.Tableau r, VarSet, VarMap (LA.Expr r))

emptySolver :: VarSet -> Solver r
emptySolver :: forall r. VarSet -> Solver r
emptySolver VarSet
vs = (Var
1 forall a. Num a => a -> a -> a
+ forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum ((-Var
1) forall a. a -> [a] -> [a]
: VarSet -> [Var]
IS.toList VarSet
vs), forall r. Tableau r
Simplex.emptyTableau, VarSet
IS.empty, forall a. IntMap a
IM.empty)

-- ---------------------------------------------------------------------------
-- LP Monad

type LP r = State (Solver r)

-- | Allocate a new /non-negative/ variable.
newVar :: LP r Var
newVar :: forall r. LP r Var
newVar = do
  (Var
x,Tableau r
tbl,VarSet
avs,VarMap (Expr r)
defs) <- forall s (m :: * -> *). MonadState s m => m s
get
  forall s (m :: * -> *). MonadState s m => s -> m ()
put (Var
xforall a. Num a => a -> a -> a
+Var
1,Tableau r
tbl,VarSet
avs,VarMap (Expr r)
defs)
  forall (m :: * -> *) a. Monad m => a -> m a
return Var
x

getTableau :: LP r (Simplex.Tableau r)
getTableau :: forall r. LP r (Tableau r)
getTableau = do
  (Var
_,Tableau r
tbl,VarSet
_,VarMap (Expr r)
_) <- forall s (m :: * -> *). MonadState s m => m s
get
  forall (m :: * -> *) a. Monad m => a -> m a
return Tableau r
tbl

putTableau :: Simplex.Tableau r -> LP r ()
putTableau :: forall r. Tableau r -> LP r ()
putTableau Tableau r
tbl = do
  (Var
x,Tableau r
_,VarSet
avs,VarMap (Expr r)
defs) <- forall s (m :: * -> *). MonadState s m => m s
get
  forall s (m :: * -> *). MonadState s m => s -> m ()
put (Var
x,Tableau r
tbl,VarSet
avs,VarMap (Expr r)
defs)

addArtificialVariable :: Var -> LP r ()
addArtificialVariable :: forall r. Var -> LP r ()
addArtificialVariable Var
v = do
  (Var
x,Tableau r
tbl,VarSet
avs,VarMap (Expr r)
defs) <- forall s (m :: * -> *). MonadState s m => m s
get
  forall s (m :: * -> *). MonadState s m => s -> m ()
put (Var
x, Tableau r
tbl, Var -> VarSet -> VarSet
IS.insert Var
v VarSet
avs, VarMap (Expr r)
defs)

getArtificialVariables :: LP r VarSet
getArtificialVariables :: forall r. LP r VarSet
getArtificialVariables = do
  (Var
_,Tableau r
_,VarSet
avs,VarMap (Expr r)
_) <- forall s (m :: * -> *). MonadState s m => m s
get
  forall (m :: * -> *) a. Monad m => a -> m a
return VarSet
avs

clearArtificialVariables :: LP r ()
clearArtificialVariables :: forall r. LP r ()
clearArtificialVariables = do
  (Var
x,Tableau r
tbl,VarSet
_,VarMap (Expr r)
defs) <- forall s (m :: * -> *). MonadState s m => m s
get
  forall s (m :: * -> *). MonadState s m => s -> m ()
put (Var
x, Tableau r
tbl, VarSet
IS.empty, VarMap (Expr r)
defs)

define :: Var -> LA.Expr r -> LP r ()
define :: forall r. Var -> Expr r -> LP r ()
define Var
v Expr r
e = do
  (Var
x,Tableau r
tbl,VarSet
avs,IntMap (Expr r)
defs) <- forall s (m :: * -> *). MonadState s m => m s
get
  forall s (m :: * -> *). MonadState s m => s -> m ()
put (Var
x,Tableau r
tbl,VarSet
avs, forall a. Var -> a -> IntMap a -> IntMap a
IM.insert Var
v Expr r
e IntMap (Expr r)
defs)

getDefs :: LP r (VarMap (LA.Expr r))
getDefs :: forall r. LP r (VarMap (Expr r))
getDefs = do
  (Var
_,Tableau r
_,VarSet
_,VarMap (Expr r)
defs) <- forall s (m :: * -> *). MonadState s m => m s
get
  forall (m :: * -> *) a. Monad m => a -> m a
return VarMap (Expr r)
defs

-- ---------------------------------------------------------------------------

-- | Add a contraint and maintain feasibility condition by introducing artificial variable (if necessary).
--
-- * Disequality is not supported.
--
-- * Unlike 'addConstraint', an equality contstraint becomes one row with an artificial variable.
--
addConstraintWithArtificialVariable :: Real r => LA.Atom r -> LP r ()
addConstraintWithArtificialVariable :: forall r. Real r => Atom r -> LP r ()
addConstraintWithArtificialVariable Atom r
c = do
  Atom r
c2 <- forall r. (Num r, Eq r) => Atom r -> LP r (Atom r)
expandDefs' Atom r
c
  let (Expr r
e, RelOp
rop, r
b) = forall r. Real r => Atom r -> (Expr r, RelOp, r)
normalizeConstraint Atom r
c2
  forall a. (?callStack::CallStack) => Bool -> a -> a
assert (r
b forall a. Ord a => a -> a -> Bool
>= r
0) forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => a -> m a
return ()
  Tableau r
tbl <- forall r. LP r (Tableau r)
getTableau
  case RelOp
rop of
    -- x≥0 is trivially true, since x is non-negative.
    RelOp
Ge | r
bforall a. Eq a => a -> a -> Bool
==r
0 Bool -> Bool -> Bool
&& forall r. Real r => Expr r -> Bool
isSingleVar Expr r
e -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
    -- -x≤0 is trivially true, since x is non-negative.
    RelOp
Le | r
bforall a. Eq a => a -> a -> Bool
==r
0 Bool -> Bool -> Bool
&& forall r. Real r => Expr r -> Bool
isSingleNegatedVar Expr r
e -> forall (m :: * -> *) a. Monad m => a -> m a
return ()

    RelOp
Le -> do
      Var
v <- forall r. LP r Var
newVar -- slack variable
      forall r. Tableau r -> LP r ()
putTableau forall a b. (a -> b) -> a -> b
$ forall r. (Num r, Eq r) => Tableau r -> Var -> Row r -> Tableau r
Simplex.addRow Tableau r
tbl Var
v (forall r. Expr r -> IntMap r
LA.coeffMap Expr r
e, r
b)
    RelOp
Ge -> do
      Var
v1 <- forall r. LP r Var
newVar -- surplus variable
      Var
v2 <- forall r. LP r Var
newVar -- artificial variable
      forall r. Tableau r -> LP r ()
putTableau forall a b. (a -> b) -> a -> b
$ forall r. (Num r, Eq r) => Tableau r -> Var -> Row r -> Tableau r
Simplex.addRow Tableau r
tbl Var
v2 (forall r. Expr r -> IntMap r
LA.coeffMap (Expr r
e forall v. AdditiveGroup v => v -> v -> v
^-^ forall r. Num r => Var -> Expr r
LA.var Var
v1), r
b)
      forall r. Var -> LP r ()
addArtificialVariable Var
v2
    RelOp
Eql -> do
      Var
v <- forall r. LP r Var
newVar -- artificial variable
      forall r. Tableau r -> LP r ()
putTableau forall a b. (a -> b) -> a -> b
$ forall r. (Num r, Eq r) => Tableau r -> Var -> Row r -> Tableau r
Simplex.addRow Tableau r
tbl Var
v (forall r. Expr r -> IntMap r
LA.coeffMap Expr r
e, r
b)
      forall r. Var -> LP r ()
addArtificialVariable Var
v
    RelOp
_ -> forall a. (?callStack::CallStack) => [Char] -> a
error forall a b. (a -> b) -> a -> b
$ [Char]
"ToySolver.LPSolver.addConstraintWithArtificialVariable does not support " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show RelOp
rop

-- | Add a contraint, without maintaining feasibilty condition of tableaus.
--
-- * Disequality is not supported.
--
-- * Unlike 'addConstraintWithArtificialVariable', an equality constraint becomes two rows.
--
addConstraint :: Real r => LA.Atom r -> LP r ()
addConstraint :: forall r. Real r => Atom r -> LP r ()
addConstraint Atom r
c = do
  OrdRel Expr r
lhs RelOp
rop Expr r
rhs <- forall r. (Num r, Eq r) => Atom r -> LP r (Atom r)
expandDefs' Atom r
c
  let
    (r
b', Expr r
e) = forall r. Num r => Var -> Expr r -> (r, Expr r)
LA.extract Var
LA.unitVar (Expr r
lhs forall v. AdditiveGroup v => v -> v -> v
^-^ Expr r
rhs)
    b :: r
b = - r
b'
  case RelOp
rop of
    RelOp
Le -> forall {r}. Real r => Expr r -> r -> StateT (Solver r) Identity ()
f Expr r
e r
b
    RelOp
Ge -> forall {r}. Real r => Expr r -> r -> StateT (Solver r) Identity ()
f (forall v. AdditiveGroup v => v -> v
negateV Expr r
e) (forall a. Num a => a -> a
negate r
b)
    RelOp
Eql -> do
      -- Unlike addConstraintWithArtificialVariable, an equality constraint becomes two rows.
      forall {r}. Real r => Expr r -> r -> StateT (Solver r) Identity ()
f Expr r
e r
b
      forall {r}. Real r => Expr r -> r -> StateT (Solver r) Identity ()
f (forall v. AdditiveGroup v => v -> v
negateV Expr r
e) (forall a. Num a => a -> a
negate r
b)
    RelOp
_ -> forall a. (?callStack::CallStack) => [Char] -> a
error forall a b. (a -> b) -> a -> b
$ [Char]
"ToySolver.LPSolver.addConstraint does not support " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show RelOp
rop
  where
    -- -x≤b with b≥0 is trivially true.
    f :: Expr r -> r -> StateT (Solver r) Identity ()
f Expr r
e r
b | forall r. Real r => Expr r -> Bool
isSingleNegatedVar Expr r
e Bool -> Bool -> Bool
&& r
0 forall a. Ord a => a -> a -> Bool
<= r
b = forall (m :: * -> *) a. Monad m => a -> m a
return ()
    f Expr r
e r
b = do
      Tableau r
tbl <- forall r. LP r (Tableau r)
getTableau
      Var
v <- forall r. LP r Var
newVar -- slack variable
      forall r. Tableau r -> LP r ()
putTableau forall a b. (a -> b) -> a -> b
$ forall r. (Num r, Eq r) => Tableau r -> Var -> Row r -> Tableau r
Simplex.addRow Tableau r
tbl Var
v (forall r. Expr r -> IntMap r
LA.coeffMap Expr r
e, r
b)

isSingleVar :: Real r => LA.Expr r -> Bool
isSingleVar :: forall r. Real r => Expr r -> Bool
isSingleVar Expr r
e =
  case forall r. Expr r -> [(r, Var)]
LA.terms Expr r
e of
    [(r
1,Var
_)] -> Bool
True
    [(r, Var)]
_ -> Bool
False

isSingleNegatedVar :: Real r => LA.Expr r -> Bool
isSingleNegatedVar :: forall r. Real r => Expr r -> Bool
isSingleNegatedVar Expr r
e =
  case forall r. Expr r -> [(r, Var)]
LA.terms Expr r
e of
    [(-1,Var
_)] -> Bool
True
    [(r, Var)]
_ -> Bool
False

expandDefs :: (Num r, Eq r) => LA.Expr r -> LP r (LA.Expr r)
expandDefs :: forall r. (Num r, Eq r) => Expr r -> LP r (Expr r)
expandDefs Expr r
e = do
  VarMap (Expr r)
defs <- forall r. LP r (VarMap (Expr r))
getDefs
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall r. (Num r, Eq r) => VarMap (Expr r) -> Expr r -> Expr r
LA.applySubst VarMap (Expr r)
defs Expr r
e

expandDefs' :: (Num r, Eq r) => LA.Atom r -> LP r (LA.Atom r)
expandDefs' :: forall r. (Num r, Eq r) => Atom r -> LP r (Atom r)
expandDefs' (OrdRel Expr r
lhs RelOp
op Expr r
rhs) = do
  Expr r
lhs' <- forall r. (Num r, Eq r) => Expr r -> LP r (Expr r)
expandDefs Expr r
lhs
  Expr r
rhs' <- forall r. (Num r, Eq r) => Expr r -> LP r (Expr r)
expandDefs Expr r
rhs
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall e. e -> RelOp -> e -> OrdRel e
OrdRel Expr r
lhs' RelOp
op Expr r
rhs'

tableau :: (RealFrac r) => [LA.Atom r] -> LP r ()
tableau :: forall r. RealFrac r => [Atom r] -> LP r ()
tableau [Atom r]
cs = do
  let (VarSet
nonnegVars, [Atom r]
cs') = forall r. RealFrac r => [Atom r] -> VarSet -> (VarSet, [Atom r])
collectNonnegVars [Atom r]
cs VarSet
IS.empty
      fvs :: VarSet
fvs = forall a. Variables a => a -> VarSet
vars [Atom r]
cs VarSet -> VarSet -> VarSet
`IS.difference` VarSet
nonnegVars
  forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (VarSet -> [Var]
IS.toList VarSet
fvs) forall a b. (a -> b) -> a -> b
$ \Var
v -> do
    Var
v1 <- forall r. LP r Var
newVar
    Var
v2 <- forall r. LP r Var
newVar
    forall r. Var -> Expr r -> LP r ()
define Var
v (forall r. Num r => Var -> Expr r
LA.var Var
v1 forall v. AdditiveGroup v => v -> v -> v
^-^ forall r. Num r => Var -> Expr r
LA.var Var
v2)
  forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ forall r. Real r => Atom r -> LP r ()
addConstraint [Atom r]
cs'

getModel :: Fractional r => VarSet -> LP r (Model r)
getModel :: forall r. Fractional r => VarSet -> LP r (Model r)
getModel VarSet
vs = do
  Tableau r
tbl <- forall r. LP r (Tableau r)
getTableau
  VarMap (Expr r)
defs <- forall r. LP r (VarMap (Expr r))
getDefs
  let vs' :: VarSet
vs' = (VarSet
vs VarSet -> VarSet -> VarSet
`IS.difference` forall a. IntMap a -> VarSet
IM.keysSet VarMap (Expr r)
defs) VarSet -> VarSet -> VarSet
`IS.union` forall (f :: * -> *). Foldable f => f VarSet -> VarSet
IS.unions [forall a. Variables a => a -> VarSet
vars Expr r
e | Expr r
e <- forall a. IntMap a -> [a]
IM.elems VarMap (Expr r)
defs]
      m0 :: IntMap r
m0 = forall a. [(Var, a)] -> IntMap a
IM.fromAscList [(Var
v, forall r. Num r => Tableau r -> Var -> r
Simplex.currentValue Tableau r
tbl Var
v) | Var
v <- VarSet -> [Var]
IS.toAscList VarSet
vs']
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. (Var -> a -> Bool) -> IntMap a -> IntMap a
IM.filterWithKey (\Var
k r
_ -> Var
k Var -> VarSet -> Bool
`IS.member` VarSet
vs) forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> IntMap a -> IntMap b
IM.map (forall m e v. Eval m e v => m -> e -> v
LA.eval IntMap r
m0) VarMap (Expr r)
defs forall a. IntMap a -> IntMap a -> IntMap a
`IM.union` IntMap r
m0

phaseI :: (Fractional r, Real r) => LP r Bool
phaseI :: forall r. (Fractional r, Real r) => LP r Bool
phaseI = do
  forall r. Real r => LP r ()
introduceArtificialVariables
  Tableau r
tbl <- forall r. LP r (Tableau r)
getTableau
  VarSet
avs <- forall r. LP r VarSet
getArtificialVariables
  let (Bool
ret, Tableau r
tbl') = forall r.
(Real r, Fractional r) =>
Tableau r -> VarSet -> (Bool, Tableau r)
Simplex.phaseI Tableau r
tbl VarSet
avs
  forall r. Tableau r -> LP r ()
putTableau Tableau r
tbl'
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
ret forall r. LP r ()
clearArtificialVariables
  forall (m :: * -> *) a. Monad m => a -> m a
return Bool
ret

introduceArtificialVariables :: (Real r) => LP r ()
introduceArtificialVariables :: forall r. Real r => LP r ()
introduceArtificialVariables = do
  Tableau r
tbl <- forall r. LP r (Tableau r)
getTableau
  Tableau r
tbl' <- forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM forall a. [(Var, a)] -> IntMap a
IM.fromList forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (forall a. IntMap a -> [(Var, a)]
IM.toList Tableau r
tbl) forall a b. (a -> b) -> a -> b
$ \(Var
v,(VarMap r
e,r
rhs)) -> do
    if r
rhs forall a. Ord a => a -> a -> Bool
>= r
0 then do
      forall (m :: * -> *) a. Monad m => a -> m a
return (Var
v,(VarMap r
e,r
rhs)) -- v + e == rhs
    else do
      Var
a <- forall r. LP r Var
newVar
      forall r. Var -> LP r ()
addArtificialVariable Var
a
      forall (m :: * -> *) a. Monad m => a -> m a
return (Var
a, (forall a. Var -> a -> IntMap a -> IntMap a
IM.insert Var
v (-r
1) (forall a b. (a -> b) -> IntMap a -> IntMap b
IM.map forall a. Num a => a -> a
negate VarMap r
e), -r
rhs)) -- a - (v + e) == -rhs
  forall r. Tableau r -> LP r ()
putTableau Tableau r
tbl'

simplex :: (Fractional r, Real r) => OptDir -> LA.Expr r -> LP r Bool
simplex :: forall r. (Fractional r, Real r) => OptDir -> Expr r -> LP r Bool
simplex OptDir
optdir Expr r
obj = do
  Tableau r
tbl <- forall r. LP r (Tableau r)
getTableau
  VarMap (Expr r)
defs <- forall r. LP r (VarMap (Expr r))
getDefs
  let (Bool
ret, Tableau r
tbl') = forall r.
(Real r, Fractional r) =>
OptDir -> Tableau r -> (Bool, Tableau r)
Simplex.simplex OptDir
optdir (forall r. (Num r, Eq r) => Tableau r -> Expr r -> Tableau r
Simplex.setObjFun Tableau r
tbl (forall r. (Num r, Eq r) => VarMap (Expr r) -> Expr r -> Expr r
LA.applySubst VarMap (Expr r)
defs Expr r
obj))
  forall r. Tableau r -> LP r ()
putTableau Tableau r
tbl'
  forall (m :: * -> *) a. Monad m => a -> m a
return Bool
ret

dualSimplex :: (Fractional r, Real r) => OptDir -> LA.Expr r -> LP r Bool
dualSimplex :: forall r. (Fractional r, Real r) => OptDir -> Expr r -> LP r Bool
dualSimplex OptDir
optdir Expr r
obj = do
  Tableau r
tbl <- forall r. LP r (Tableau r)
getTableau
  VarMap (Expr r)
defs <- forall r. LP r (VarMap (Expr r))
getDefs
  let (Bool
ret, Tableau r
tbl') = forall r.
(Real r, Fractional r) =>
OptDir -> Tableau r -> (Bool, Tableau r)
Simplex.dualSimplex OptDir
optdir (forall r. (Num r, Eq r) => Tableau r -> Expr r -> Tableau r
Simplex.setObjFun Tableau r
tbl (forall r. (Num r, Eq r) => VarMap (Expr r) -> Expr r -> Expr r
LA.applySubst VarMap (Expr r)
defs Expr r
obj))
  forall r. Tableau r -> LP r ()
putTableau Tableau r
tbl'
  forall (m :: * -> *) a. Monad m => a -> m a
return Bool
ret

-- | results of optimization
data OptResult = Optimum | Unsat | Unbounded
  deriving (Var -> OptResult -> ShowS
[OptResult] -> ShowS
OptResult -> [Char]
forall a.
(Var -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [OptResult] -> ShowS
$cshowList :: [OptResult] -> ShowS
show :: OptResult -> [Char]
$cshow :: OptResult -> [Char]
showsPrec :: Var -> OptResult -> ShowS
$cshowsPrec :: Var -> OptResult -> ShowS
Show, OptResult -> OptResult -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: OptResult -> OptResult -> Bool
$c/= :: OptResult -> OptResult -> Bool
== :: OptResult -> OptResult -> Bool
$c== :: OptResult -> OptResult -> Bool
Eq, Eq OptResult
OptResult -> OptResult -> Bool
OptResult -> OptResult -> Ordering
OptResult -> OptResult -> OptResult
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: OptResult -> OptResult -> OptResult
$cmin :: OptResult -> OptResult -> OptResult
max :: OptResult -> OptResult -> OptResult
$cmax :: OptResult -> OptResult -> OptResult
>= :: OptResult -> OptResult -> Bool
$c>= :: OptResult -> OptResult -> Bool
> :: OptResult -> OptResult -> Bool
$c> :: OptResult -> OptResult -> Bool
<= :: OptResult -> OptResult -> Bool
$c<= :: OptResult -> OptResult -> Bool
< :: OptResult -> OptResult -> Bool
$c< :: OptResult -> OptResult -> Bool
compare :: OptResult -> OptResult -> Ordering
$ccompare :: OptResult -> OptResult -> Ordering
Ord)

twoPhaseSimplex :: (Fractional r, Real r) => OptDir -> LA.Expr r -> LP r OptResult
twoPhaseSimplex :: forall r.
(Fractional r, Real r) =>
OptDir -> Expr r -> LP r OptResult
twoPhaseSimplex OptDir
optdir Expr r
obj = do
  Bool
ret <- forall r. (Fractional r, Real r) => LP r Bool
phaseI
  if Bool -> Bool
not Bool
ret then
    forall (m :: * -> *) a. Monad m => a -> m a
return OptResult
Unsat
  else do
    Bool
ret <- forall r. (Fractional r, Real r) => OptDir -> Expr r -> LP r Bool
simplex OptDir
optdir Expr r
obj
    if Bool
ret then
      forall (m :: * -> *) a. Monad m => a -> m a
return OptResult
Optimum
    else
      forall (m :: * -> *) a. Monad m => a -> m a
return OptResult
Unbounded

primalDualSimplex :: (Fractional r, Real r) => OptDir -> LA.Expr r -> LP r OptResult
primalDualSimplex :: forall r.
(Fractional r, Real r) =>
OptDir -> Expr r -> LP r OptResult
primalDualSimplex OptDir
optdir Expr r
obj = do
  Tableau r
tbl <- forall r. LP r (Tableau r)
getTableau
  VarMap (Expr r)
defs <- forall r. LP r (VarMap (Expr r))
getDefs
  let (Bool
ret, Tableau r
tbl') = forall r.
(Real r, Fractional r) =>
OptDir -> Tableau r -> (Bool, Tableau r)
Simplex.primalDualSimplex OptDir
optdir (forall r. (Num r, Eq r) => Tableau r -> Expr r -> Tableau r
Simplex.setObjFun Tableau r
tbl (forall r. (Num r, Eq r) => VarMap (Expr r) -> Expr r -> Expr r
LA.applySubst VarMap (Expr r)
defs Expr r
obj))
  forall r. Tableau r -> LP r ()
putTableau Tableau r
tbl'
  if Bool
ret then
    forall (m :: * -> *) a. Monad m => a -> m a
return OptResult
Optimum
  else if Bool -> Bool
not (forall r. Real r => Tableau r -> Bool
Simplex.isFeasible Tableau r
tbl') then
    forall (m :: * -> *) a. Monad m => a -> m a
return OptResult
Unsat
  else
    forall (m :: * -> *) a. Monad m => a -> m a
return OptResult
Unbounded

-- ---------------------------------------------------------------------------

-- convert right hand side to be non-negative
normalizeConstraint :: forall r. Real r => LA.Atom r -> (LA.Expr r, RelOp, r)
normalizeConstraint :: forall r. Real r => Atom r -> (Expr r, RelOp, r)
normalizeConstraint (OrdRel Expr r
a RelOp
op Expr r
b)
  | r
rhs forall a. Ord a => a -> a -> Bool
< r
0   = (forall v. AdditiveGroup v => v -> v
negateV Expr r
lhs, RelOp -> RelOp
flipOp RelOp
op, forall a. Num a => a -> a
negate r
rhs)
  | Bool
otherwise = (Expr r
lhs, RelOp
op, r
rhs)
  where
    (r
c, Expr r
lhs) = forall r. Num r => Var -> Expr r -> (r, Expr r)
LA.extract Var
LA.unitVar (Expr r
a forall v. AdditiveGroup v => v -> v -> v
^-^ Expr r
b)
    rhs :: r
rhs = - r
c

collectNonnegVars :: forall r. (RealFrac r) => [LA.Atom r] -> VarSet -> (VarSet, [LA.Atom r])
collectNonnegVars :: forall r. RealFrac r => [Atom r] -> VarSet -> (VarSet, [Atom r])
collectNonnegVars [Atom r]
cs VarSet
ivs = (VarSet
nonnegVars, [Atom r]
cs)
  where
    vs :: VarSet
vs = forall a. Variables a => a -> VarSet
vars [Atom r]
cs
    bounds :: BoundsEnv r
bounds = forall r.
RealFrac r =>
BoundsEnv r -> [Atom r] -> VarSet -> Var -> BoundsEnv r
BI.inferBounds BoundsEnv r
initialBounds [Atom r]
cs VarSet
ivs Var
1000
      where
        initialBounds :: BoundsEnv r
initialBounds = forall a. [(Var, a)] -> IntMap a
IM.fromAscList [(Var
v, forall r. Ord r => Interval r
Interval.whole) | Var
v <- VarSet -> [Var]
IS.toAscList VarSet
vs]
    nonnegVars :: VarSet
nonnegVars = (Var -> Bool) -> VarSet -> VarSet
IS.filter (\Var
v -> Interval r
0 forall r. Ord r => Interval r -> Interval r -> Bool
<=! (BoundsEnv r
bounds forall a. IntMap a -> Var -> a
IM.! Var
v)) VarSet
vs

    isTriviallyTrue :: LA.Atom r -> Bool
    isTriviallyTrue :: Atom r -> Bool
isTriviallyTrue (OrdRel Expr r
a RelOp
op Expr r
b) =
      case RelOp
op of
        RelOp
Le -> Interval r
i forall r. Ord r => Interval r -> Interval r -> Bool
<=! Interval r
0
        RelOp
Ge -> Interval r
i forall r. Ord r => Interval r -> Interval r -> Bool
>=! Interval r
0
        RelOp
Lt -> Interval r
i forall r. Ord r => Interval r -> Interval r -> Bool
<! Interval r
0
        RelOp
Gt -> Interval r
i forall r. Ord r => Interval r -> Interval r -> Bool
>! Interval r
0
        RelOp
Eql -> Interval r
i forall r. Ord r => Interval r -> Interval r -> Bool
==! Interval r
0
        RelOp
NEq -> Interval r
i forall r. Ord r => Interval r -> Interval r -> Bool
/=! Interval r
0
      where
        i :: Interval r
i = forall r.
(Real r, Fractional r) =>
BoundsEnv r -> Expr r -> Interval r
LA.computeInterval BoundsEnv r
bounds (Expr r
a forall v. AdditiveGroup v => v -> v -> v
^-^ Expr r
b)

-- ---------------------------------------------------------------------------