{-# OPTIONS_HADDOCK show-extensions #-}
{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
-----------------------------------------------------------------------------
-- |
-- Module      :  ToySolver.Arith.Simplex
-- Copyright   :  (c) Masahiro Sakai 2012
-- 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>
--
-- * Bruno Dutertre and Leonardo de Moura.
--   A Fast Linear-Arithmetic Solver for DPLL(T).
--   Computer Aided Verification In Computer Aided Verification, Vol. 4144 (2006), pp. 81-94.
--   <http://yices.csl.sri.com/cav06.pdf>
--
-- * Bruno Dutertre and Leonardo de Moura.
--   Integrating Simplex with DPLL(T).
--   CSL Technical Report SRI-CSL-06-01. 2006.
--   <http://yices.csl.sri.com/sri-csl-06-01.pdf>
--
-----------------------------------------------------------------------------
module ToySolver.Arith.Simplex
  (
  -- * The @Solver@ type
    Solver
  , GenericSolver
  , GenericSolverM
  , SolverValue (..)
  , newSolver
  , cloneSolver

  -- * Problem specification
  , Var
  , newVar
  , RelOp (..)
  , (.<=.), (.>=.), (.==.), (.<.), (.>.)
  , Atom (..)
  , ConstrID
  , ConstrIDSet
  , assertAtom
  , assertAtom'
  , assertAtomEx
  , assertAtomEx'
  , assertLower
  , assertLower'
  , assertUpper
  , assertUpper'
  , setObj
  , getObj
  , OptDir (..)
  , setOptDir
  , getOptDir

  -- * Solving
  , check
  , pushBacktrackPoint
  , popBacktrackPoint
  , Options (..)
  , OptResult (..)
  , optimize
  , dualSimplex

  -- * Extract results
  , Model
  , getModel
  , RawModel
  , getRawModel
  , getValue
  , getObjValue
  , explain

  -- * Reading status
  , getTableau
  , getRow
  , getCol
  , getCoeff
  , nVars
  , isBasicVariable
  , isNonBasicVariable
  , isFeasible
  , isOptimal
  , getLB
  , getUB
  , Bound
  , boundValue
  , boundExplanation

  -- * Configulation
  , setLogger
  , clearLogger
  , enableTimeRecording
  , disableTimeRecording
  , Config (..)
  , setConfig
  , getConfig
  , modifyConfig
  , PivotStrategy (..)
  , showPivotStrategy
  , parsePivotStrategy
  , setPivotStrategy

  -- * Debug
  , dump

  -- * Misc
  , simplifyAtom
  ) where

import Prelude hiding (log)
import Control.Arrow ((***))
import Control.Exception
import Control.Monad
import Control.Monad.Primitive
import Data.Char
import Data.Default.Class
import Data.Ord
import Data.List
import Data.Maybe
import Data.Monoid
import Data.Primitive.MutVar
import Data.Ratio
import Data.Map (Map)
import qualified Data.Map as Map
import Data.IntMap (IntMap)
import qualified Data.IntMap as IntMap
import Data.IntSet (IntSet)
import qualified Data.IntSet as IntSet
import Text.Printf
import Data.OptDir
import Data.VectorSpace
import System.Clock

import qualified ToySolver.Data.LA as LA
import ToySolver.Data.LA (Atom (..))
import ToySolver.Data.OrdRel
import ToySolver.Data.Delta
import ToySolver.Internal.Util (showRational)

infixr 0 ~>
-- | A natural transformation from @f@ to @g@.
type f ~> g = forall x. f x -> g x

infixr 0 :~>, $$
-- | A natural transformation suitable for storing in a container.
newtype f :~> g = Nat { forall (f :: * -> *) (g :: * -> *). (f :~> g) -> f ~> g
($$) :: f ~> g }

{--------------------------------------------------------------------
  The @Solver@ type
--------------------------------------------------------------------}

type Var = Int

data GenericSolverM m v
  = GenericSolverM
  { forall (m :: * -> *) v.
GenericSolverM m v -> MutVar (PrimState m) (IntMap (Expr Rational))
svTableau :: !(MutVar (PrimState m) (IntMap (LA.Expr Rational)))
  , forall (m :: * -> *) v.
GenericSolverM m v
-> MutVar (PrimState m) (IntMap (v, ConstrIDSet))
svLB      :: !(MutVar (PrimState m) (IntMap (v, ConstrIDSet)))
  , forall (m :: * -> *) v.
GenericSolverM m v
-> MutVar (PrimState m) (IntMap (v, ConstrIDSet))
svUB      :: !(MutVar (PrimState m) (IntMap (v, ConstrIDSet)))
  , forall (m :: * -> *) v.
GenericSolverM m v -> MutVar (PrimState m) (IntMap v)
svModel   :: !(MutVar (PrimState m) (IntMap v))
  , forall (m :: * -> *) v.
GenericSolverM m v -> MutVar (PrimState m) (Maybe ConstrIDSet)
svExplanation :: !(MutVar (PrimState m) (Maybe ConstrIDSet))
  , forall (m :: * -> *) v.
GenericSolverM m v -> MutVar (PrimState m) Int
svVCnt    :: !(MutVar (PrimState m) Int)
  , forall (m :: * -> *) v.
GenericSolverM m v -> MutVar (PrimState m) OptDir
svOptDir  :: !(MutVar (PrimState m) OptDir)

  , forall (m :: * -> *) v.
GenericSolverM m v
-> MutVar (PrimState m) (Map (Expr Rational) Int)
svDefDB  :: !(MutVar (PrimState m) (Map (LA.Expr Rational) Var))

  , forall (m :: * -> *) v.
GenericSolverM m v -> MutVar (PrimState m) (Maybe (String -> m ()))
svLogger :: !(MutVar (PrimState m) (Maybe (String -> m ())))
  , forall (m :: * -> *) v.
GenericSolverM m v
-> MutVar (PrimState m) (Maybe (GenericSolverM m v -> m :~> m))
svRecTime :: !(MutVar (PrimState m) (Maybe (GenericSolverM m v -> (m :~> m))))
  , forall (m :: * -> *) v.
GenericSolverM m v -> MutVar (PrimState m) Config
svConfig  :: !(MutVar (PrimState m) Config)
  , forall (m :: * -> *) v.
GenericSolverM m v -> MutVar (PrimState m) Int
svNPivot  :: !(MutVar (PrimState m) Int)

  , forall (m :: * -> *) v.
GenericSolverM m v -> MutVar (PrimState m) [BacktrackPoint m v]
svBacktrackPoints :: !(MutVar (PrimState m) [BacktrackPoint m v])
  }

type GenericSolver v = GenericSolverM IO v

type Solver = GenericSolver Rational

-- special basic variable
objVar :: Int
objVar :: Int
objVar = -Int
1

newSolver :: (PrimMonad m, SolverValue v) => m (GenericSolverM m v)
newSolver :: forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
m (GenericSolverM m v)
newSolver = do
  MutVar (PrimState m) (IntMap (Expr Rational))
t <- IntMap (Expr Rational)
-> m (MutVar (PrimState m) (IntMap (Expr Rational)))
forall (m :: * -> *) a.
PrimMonad m =>
a -> m (MutVar (PrimState m) a)
newMutVar (Int -> Expr Rational -> IntMap (Expr Rational)
forall a. Int -> a -> IntMap a
IntMap.singleton Int
objVar Expr Rational
forall v. AdditiveGroup v => v
zeroV)
  MutVar (PrimState m) (IntMap (v, ConstrIDSet))
l <- IntMap (v, ConstrIDSet)
-> m (MutVar (PrimState m) (IntMap (v, ConstrIDSet)))
forall (m :: * -> *) a.
PrimMonad m =>
a -> m (MutVar (PrimState m) a)
newMutVar IntMap (v, ConstrIDSet)
forall a. IntMap a
IntMap.empty
  MutVar (PrimState m) (IntMap (v, ConstrIDSet))
u <- IntMap (v, ConstrIDSet)
-> m (MutVar (PrimState m) (IntMap (v, ConstrIDSet)))
forall (m :: * -> *) a.
PrimMonad m =>
a -> m (MutVar (PrimState m) a)
newMutVar IntMap (v, ConstrIDSet)
forall a. IntMap a
IntMap.empty
  MutVar (PrimState m) (IntMap v)
m <- IntMap v -> m (MutVar (PrimState m) (IntMap v))
forall (m :: * -> *) a.
PrimMonad m =>
a -> m (MutVar (PrimState m) a)
newMutVar (Int -> v -> IntMap v
forall a. Int -> a -> IntMap a
IntMap.singleton Int
objVar v
forall v. AdditiveGroup v => v
zeroV)
  MutVar (PrimState m) (Maybe ConstrIDSet)
e <- Maybe ConstrIDSet -> m (MutVar (PrimState m) (Maybe ConstrIDSet))
forall (m :: * -> *) a.
PrimMonad m =>
a -> m (MutVar (PrimState m) a)
newMutVar Maybe ConstrIDSet
forall a. Monoid a => a
mempty
  MutVar (PrimState m) Int
v <- Int -> m (MutVar (PrimState m) Int)
forall (m :: * -> *) a.
PrimMonad m =>
a -> m (MutVar (PrimState m) a)
newMutVar Int
0
  MutVar (PrimState m) OptDir
dir <- OptDir -> m (MutVar (PrimState m) OptDir)
forall (m :: * -> *) a.
PrimMonad m =>
a -> m (MutVar (PrimState m) a)
newMutVar OptDir
OptMin
  MutVar (PrimState m) (Map (Expr Rational) Int)
defs <- Map (Expr Rational) Int
-> m (MutVar (PrimState m) (Map (Expr Rational) Int))
forall (m :: * -> *) a.
PrimMonad m =>
a -> m (MutVar (PrimState m) a)
newMutVar Map (Expr Rational) Int
forall k a. Map k a
Map.empty
  MutVar (PrimState m) (Maybe (String -> m ()))
logger <- Maybe (String -> m ())
-> m (MutVar (PrimState m) (Maybe (String -> m ())))
forall (m :: * -> *) a.
PrimMonad m =>
a -> m (MutVar (PrimState m) a)
newMutVar Maybe (String -> m ())
forall a. Maybe a
Nothing
  MutVar (PrimState m) (Maybe (GenericSolverM m v -> m :~> m))
rectm <- Maybe (GenericSolverM m v -> m :~> m)
-> m (MutVar (PrimState m) (Maybe (GenericSolverM m v -> m :~> m)))
forall (m :: * -> *) a.
PrimMonad m =>
a -> m (MutVar (PrimState m) a)
newMutVar Maybe (GenericSolverM m v -> m :~> m)
forall a. Maybe a
Nothing
  MutVar (PrimState m) Config
config <- Config -> m (MutVar (PrimState m) Config)
forall (m :: * -> *) a.
PrimMonad m =>
a -> m (MutVar (PrimState m) a)
newMutVar Config
forall a. Default a => a
def
  MutVar (PrimState m) Int
npivot <- Int -> m (MutVar (PrimState m) Int)
forall (m :: * -> *) a.
PrimMonad m =>
a -> m (MutVar (PrimState m) a)
newMutVar Int
0
  MutVar (PrimState m) [BacktrackPoint m v]
bps <- [BacktrackPoint m v]
-> m (MutVar (PrimState m) [BacktrackPoint m v])
forall (m :: * -> *) a.
PrimMonad m =>
a -> m (MutVar (PrimState m) a)
newMutVar []
  GenericSolverM m v -> m (GenericSolverM m v)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (GenericSolverM m v -> m (GenericSolverM m v))
-> GenericSolverM m v -> m (GenericSolverM m v)
forall a b. (a -> b) -> a -> b
$
    GenericSolverM
    { svTableau :: MutVar (PrimState m) (IntMap (Expr Rational))
svTableau = MutVar (PrimState m) (IntMap (Expr Rational))
t
    , svLB :: MutVar (PrimState m) (IntMap (v, ConstrIDSet))
svLB      = MutVar (PrimState m) (IntMap (v, ConstrIDSet))
l
    , svUB :: MutVar (PrimState m) (IntMap (v, ConstrIDSet))
svUB      = MutVar (PrimState m) (IntMap (v, ConstrIDSet))
u
    , svModel :: MutVar (PrimState m) (IntMap v)
svModel   = MutVar (PrimState m) (IntMap v)
m
    , svExplanation :: MutVar (PrimState m) (Maybe ConstrIDSet)
svExplanation = MutVar (PrimState m) (Maybe ConstrIDSet)
e
    , svVCnt :: MutVar (PrimState m) Int
svVCnt    = MutVar (PrimState m) Int
v
    , svOptDir :: MutVar (PrimState m) OptDir
svOptDir  = MutVar (PrimState m) OptDir
dir
    , svDefDB :: MutVar (PrimState m) (Map (Expr Rational) Int)
svDefDB   = MutVar (PrimState m) (Map (Expr Rational) Int)
defs
    , svLogger :: MutVar (PrimState m) (Maybe (String -> m ()))
svLogger  = MutVar (PrimState m) (Maybe (String -> m ()))
logger
    , svRecTime :: MutVar (PrimState m) (Maybe (GenericSolverM m v -> m :~> m))
svRecTime = MutVar (PrimState m) (Maybe (GenericSolverM m v -> m :~> m))
rectm
    , svNPivot :: MutVar (PrimState m) Int
svNPivot  = MutVar (PrimState m) Int
npivot
    , svConfig :: MutVar (PrimState m) Config
svConfig  = MutVar (PrimState m) Config
config
    , svBacktrackPoints :: MutVar (PrimState m) [BacktrackPoint m v]
svBacktrackPoints = MutVar (PrimState m) [BacktrackPoint m v]
bps
    }

cloneSolver :: PrimMonad m => GenericSolverM m v -> m (GenericSolverM m v)
cloneSolver :: forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> m (GenericSolverM m v)
cloneSolver GenericSolverM m v
solver = do
  MutVar (PrimState m) (IntMap (Expr Rational))
t      <- IntMap (Expr Rational)
-> m (MutVar (PrimState m) (IntMap (Expr Rational)))
forall (m :: * -> *) a.
PrimMonad m =>
a -> m (MutVar (PrimState m) a)
newMutVar (IntMap (Expr Rational)
 -> m (MutVar (PrimState m) (IntMap (Expr Rational))))
-> m (IntMap (Expr Rational))
-> m (MutVar (PrimState m) (IntMap (Expr Rational)))
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< MutVar (PrimState m) (IntMap (Expr Rational))
-> m (IntMap (Expr Rational))
forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> m a
readMutVar (GenericSolverM m v -> MutVar (PrimState m) (IntMap (Expr Rational))
forall (m :: * -> *) v.
GenericSolverM m v -> MutVar (PrimState m) (IntMap (Expr Rational))
svTableau GenericSolverM m v
solver)
  MutVar (PrimState m) (IntMap (v, ConstrIDSet))
l      <- IntMap (v, ConstrIDSet)
-> m (MutVar (PrimState m) (IntMap (v, ConstrIDSet)))
forall (m :: * -> *) a.
PrimMonad m =>
a -> m (MutVar (PrimState m) a)
newMutVar (IntMap (v, ConstrIDSet)
 -> m (MutVar (PrimState m) (IntMap (v, ConstrIDSet))))
-> m (IntMap (v, ConstrIDSet))
-> m (MutVar (PrimState m) (IntMap (v, ConstrIDSet)))
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< MutVar (PrimState m) (IntMap (v, ConstrIDSet))
-> m (IntMap (v, ConstrIDSet))
forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> m a
readMutVar (GenericSolverM m v
-> MutVar (PrimState m) (IntMap (v, ConstrIDSet))
forall (m :: * -> *) v.
GenericSolverM m v
-> MutVar (PrimState m) (IntMap (v, ConstrIDSet))
svLB GenericSolverM m v
solver)
  MutVar (PrimState m) (IntMap (v, ConstrIDSet))
u      <- IntMap (v, ConstrIDSet)
-> m (MutVar (PrimState m) (IntMap (v, ConstrIDSet)))
forall (m :: * -> *) a.
PrimMonad m =>
a -> m (MutVar (PrimState m) a)
newMutVar (IntMap (v, ConstrIDSet)
 -> m (MutVar (PrimState m) (IntMap (v, ConstrIDSet))))
-> m (IntMap (v, ConstrIDSet))
-> m (MutVar (PrimState m) (IntMap (v, ConstrIDSet)))
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< MutVar (PrimState m) (IntMap (v, ConstrIDSet))
-> m (IntMap (v, ConstrIDSet))
forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> m a
readMutVar (GenericSolverM m v
-> MutVar (PrimState m) (IntMap (v, ConstrIDSet))
forall (m :: * -> *) v.
GenericSolverM m v
-> MutVar (PrimState m) (IntMap (v, ConstrIDSet))
svUB GenericSolverM m v
solver)
  MutVar (PrimState m) (IntMap v)
m      <- IntMap v -> m (MutVar (PrimState m) (IntMap v))
forall (m :: * -> *) a.
PrimMonad m =>
a -> m (MutVar (PrimState m) a)
newMutVar (IntMap v -> m (MutVar (PrimState m) (IntMap v)))
-> m (IntMap v) -> m (MutVar (PrimState m) (IntMap v))
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< MutVar (PrimState m) (IntMap v) -> m (IntMap v)
forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> m a
readMutVar (GenericSolverM m v -> MutVar (PrimState m) (IntMap v)
forall (m :: * -> *) v.
GenericSolverM m v -> MutVar (PrimState m) (IntMap v)
svModel GenericSolverM m v
solver)
  MutVar (PrimState m) (Maybe ConstrIDSet)
e      <- Maybe ConstrIDSet -> m (MutVar (PrimState m) (Maybe ConstrIDSet))
forall (m :: * -> *) a.
PrimMonad m =>
a -> m (MutVar (PrimState m) a)
newMutVar (Maybe ConstrIDSet -> m (MutVar (PrimState m) (Maybe ConstrIDSet)))
-> m (Maybe ConstrIDSet)
-> m (MutVar (PrimState m) (Maybe ConstrIDSet))
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< MutVar (PrimState m) (Maybe ConstrIDSet) -> m (Maybe ConstrIDSet)
forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> m a
readMutVar (GenericSolverM m v -> MutVar (PrimState m) (Maybe ConstrIDSet)
forall (m :: * -> *) v.
GenericSolverM m v -> MutVar (PrimState m) (Maybe ConstrIDSet)
svExplanation GenericSolverM m v
solver)
  MutVar (PrimState m) Int
v      <- Int -> m (MutVar (PrimState m) Int)
forall (m :: * -> *) a.
PrimMonad m =>
a -> m (MutVar (PrimState m) a)
newMutVar (Int -> m (MutVar (PrimState m) Int))
-> m Int -> m (MutVar (PrimState m) Int)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< MutVar (PrimState m) Int -> m Int
forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> m a
readMutVar (GenericSolverM m v -> MutVar (PrimState m) Int
forall (m :: * -> *) v.
GenericSolverM m v -> MutVar (PrimState m) Int
svVCnt GenericSolverM m v
solver)
  MutVar (PrimState m) OptDir
dir    <- OptDir -> m (MutVar (PrimState m) OptDir)
forall (m :: * -> *) a.
PrimMonad m =>
a -> m (MutVar (PrimState m) a)
newMutVar (OptDir -> m (MutVar (PrimState m) OptDir))
-> m OptDir -> m (MutVar (PrimState m) OptDir)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< MutVar (PrimState m) OptDir -> m OptDir
forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> m a
readMutVar (GenericSolverM m v -> MutVar (PrimState m) OptDir
forall (m :: * -> *) v.
GenericSolverM m v -> MutVar (PrimState m) OptDir
svOptDir GenericSolverM m v
solver)
  MutVar (PrimState m) (Map (Expr Rational) Int)
defs   <- Map (Expr Rational) Int
-> m (MutVar (PrimState m) (Map (Expr Rational) Int))
forall (m :: * -> *) a.
PrimMonad m =>
a -> m (MutVar (PrimState m) a)
newMutVar (Map (Expr Rational) Int
 -> m (MutVar (PrimState m) (Map (Expr Rational) Int)))
-> m (Map (Expr Rational) Int)
-> m (MutVar (PrimState m) (Map (Expr Rational) Int))
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< MutVar (PrimState m) (Map (Expr Rational) Int)
-> m (Map (Expr Rational) Int)
forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> m a
readMutVar (GenericSolverM m v
-> MutVar (PrimState m) (Map (Expr Rational) Int)
forall (m :: * -> *) v.
GenericSolverM m v
-> MutVar (PrimState m) (Map (Expr Rational) Int)
svDefDB GenericSolverM m v
solver)
  MutVar (PrimState m) (Maybe (String -> m ()))
logger <- Maybe (String -> m ())
-> m (MutVar (PrimState m) (Maybe (String -> m ())))
forall (m :: * -> *) a.
PrimMonad m =>
a -> m (MutVar (PrimState m) a)
newMutVar (Maybe (String -> m ())
 -> m (MutVar (PrimState m) (Maybe (String -> m ()))))
-> m (Maybe (String -> m ()))
-> m (MutVar (PrimState m) (Maybe (String -> m ())))
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< MutVar (PrimState m) (Maybe (String -> m ()))
-> m (Maybe (String -> m ()))
forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> m a
readMutVar (GenericSolverM m v -> MutVar (PrimState m) (Maybe (String -> m ()))
forall (m :: * -> *) v.
GenericSolverM m v -> MutVar (PrimState m) (Maybe (String -> m ()))
svLogger GenericSolverM m v
solver)
  MutVar (PrimState m) (Maybe (GenericSolverM m v -> m :~> m))
rectm  <- Maybe (GenericSolverM m v -> m :~> m)
-> m (MutVar (PrimState m) (Maybe (GenericSolverM m v -> m :~> m)))
forall (m :: * -> *) a.
PrimMonad m =>
a -> m (MutVar (PrimState m) a)
newMutVar (Maybe (GenericSolverM m v -> m :~> m)
 -> m (MutVar
         (PrimState m) (Maybe (GenericSolverM m v -> m :~> m))))
-> m (Maybe (GenericSolverM m v -> m :~> m))
-> m (MutVar (PrimState m) (Maybe (GenericSolverM m v -> m :~> m)))
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< MutVar (PrimState m) (Maybe (GenericSolverM m v -> m :~> m))
-> m (Maybe (GenericSolverM m v -> m :~> m))
forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> m a
readMutVar (GenericSolverM m v
-> MutVar (PrimState m) (Maybe (GenericSolverM m v -> m :~> m))
forall (m :: * -> *) v.
GenericSolverM m v
-> MutVar (PrimState m) (Maybe (GenericSolverM m v -> m :~> m))
svRecTime GenericSolverM m v
solver)
  MutVar (PrimState m) Config
config <- Config -> m (MutVar (PrimState m) Config)
forall (m :: * -> *) a.
PrimMonad m =>
a -> m (MutVar (PrimState m) a)
newMutVar (Config -> m (MutVar (PrimState m) Config))
-> m Config -> m (MutVar (PrimState m) Config)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< MutVar (PrimState m) Config -> m Config
forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> m a
readMutVar (GenericSolverM m v -> MutVar (PrimState m) Config
forall (m :: * -> *) v.
GenericSolverM m v -> MutVar (PrimState m) Config
svConfig GenericSolverM m v
solver)
  MutVar (PrimState m) Int
npivot <- Int -> m (MutVar (PrimState m) Int)
forall (m :: * -> *) a.
PrimMonad m =>
a -> m (MutVar (PrimState m) a)
newMutVar (Int -> m (MutVar (PrimState m) Int))
-> m Int -> m (MutVar (PrimState m) Int)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< MutVar (PrimState m) Int -> m Int
forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> m a
readMutVar (GenericSolverM m v -> MutVar (PrimState m) Int
forall (m :: * -> *) v.
GenericSolverM m v -> MutVar (PrimState m) Int
svNPivot GenericSolverM m v
solver)
  MutVar (PrimState m) [BacktrackPoint m v]
bps    <- [BacktrackPoint m v]
-> m (MutVar (PrimState m) [BacktrackPoint m v])
forall (m :: * -> *) a.
PrimMonad m =>
a -> m (MutVar (PrimState m) a)
newMutVar ([BacktrackPoint m v]
 -> m (MutVar (PrimState m) [BacktrackPoint m v]))
-> m [BacktrackPoint m v]
-> m (MutVar (PrimState m) [BacktrackPoint m v])
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (BacktrackPoint m v -> m (BacktrackPoint m v))
-> [BacktrackPoint m v] -> m [BacktrackPoint m v]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM BacktrackPoint m v -> m (BacktrackPoint m v)
forall (m :: * -> *) v.
PrimMonad m =>
BacktrackPoint m v -> m (BacktrackPoint m v)
cloneBacktrackPoint ([BacktrackPoint m v] -> m [BacktrackPoint m v])
-> m [BacktrackPoint m v] -> m [BacktrackPoint m v]
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< MutVar (PrimState m) [BacktrackPoint m v] -> m [BacktrackPoint m v]
forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> m a
readMutVar (GenericSolverM m v -> MutVar (PrimState m) [BacktrackPoint m v]
forall (m :: * -> *) v.
GenericSolverM m v -> MutVar (PrimState m) [BacktrackPoint m v]
svBacktrackPoints GenericSolverM m v
solver)
  GenericSolverM m v -> m (GenericSolverM m v)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (GenericSolverM m v -> m (GenericSolverM m v))
-> GenericSolverM m v -> m (GenericSolverM m v)
forall a b. (a -> b) -> a -> b
$
    GenericSolverM
    { svTableau :: MutVar (PrimState m) (IntMap (Expr Rational))
svTableau = MutVar (PrimState m) (IntMap (Expr Rational))
t
    , svLB :: MutVar (PrimState m) (IntMap (v, ConstrIDSet))
svLB      = MutVar (PrimState m) (IntMap (v, ConstrIDSet))
l
    , svUB :: MutVar (PrimState m) (IntMap (v, ConstrIDSet))
svUB      = MutVar (PrimState m) (IntMap (v, ConstrIDSet))
u
    , svModel :: MutVar (PrimState m) (IntMap v)
svModel   = MutVar (PrimState m) (IntMap v)
m
    , svExplanation :: MutVar (PrimState m) (Maybe ConstrIDSet)
svExplanation = MutVar (PrimState m) (Maybe ConstrIDSet)
e
    , svVCnt :: MutVar (PrimState m) Int
svVCnt    = MutVar (PrimState m) Int
v
    , svOptDir :: MutVar (PrimState m) OptDir
svOptDir  = MutVar (PrimState m) OptDir
dir
    , svDefDB :: MutVar (PrimState m) (Map (Expr Rational) Int)
svDefDB   = MutVar (PrimState m) (Map (Expr Rational) Int)
defs
    , svLogger :: MutVar (PrimState m) (Maybe (String -> m ()))
svLogger  = MutVar (PrimState m) (Maybe (String -> m ()))
logger
    , svRecTime :: MutVar (PrimState m) (Maybe (GenericSolverM m v -> m :~> m))
svRecTime = MutVar (PrimState m) (Maybe (GenericSolverM m v -> m :~> m))
rectm
    , svNPivot :: MutVar (PrimState m) Int
svNPivot  = MutVar (PrimState m) Int
npivot
    , svConfig :: MutVar (PrimState m) Config
svConfig  = MutVar (PrimState m) Config
config
    , svBacktrackPoints :: MutVar (PrimState m) [BacktrackPoint m v]
svBacktrackPoints = MutVar (PrimState m) [BacktrackPoint m v]
bps
    }

class (VectorSpace v, Scalar v ~ Rational, Ord v) => SolverValue v where
  toValue :: Rational -> v
  showValue :: Bool -> v -> String
  getModel :: PrimMonad m => GenericSolverM m v -> m Model

instance SolverValue Rational where
  toValue :: Rational -> Rational
toValue = Rational -> Rational
forall a. a -> a
id
  showValue :: Bool -> Rational -> String
showValue = Bool -> Rational -> String
showRational
  getModel :: forall (m :: * -> *).
PrimMonad m =>
GenericSolverM m Rational -> m Model
getModel = GenericSolverM m Rational -> m Model
forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> m (RawModel v)
getRawModel

instance SolverValue (Delta Rational) where
  toValue :: Rational -> Delta Rational
toValue = Rational -> Delta Rational
forall r. Num r => r -> Delta r
fromReal
  showValue :: Bool -> Delta Rational -> String
showValue = Bool -> Delta Rational -> String
showDelta
  getModel :: forall (m :: * -> *).
PrimMonad m =>
GenericSolverM m (Delta Rational) -> m Model
getModel GenericSolverM m (Delta Rational)
solver = do
    [Int]
xs <- GenericSolverM m (Delta Rational) -> m [Int]
forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> m [Int]
variables GenericSolverM m (Delta Rational)
solver
    [Rational]
ys <- ([[Rational]] -> [Rational]) -> m [[Rational]] -> m [Rational]
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM [[Rational]] -> [Rational]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (m [[Rational]] -> m [Rational]) -> m [[Rational]] -> m [Rational]
forall a b. (a -> b) -> a -> b
$ [Int] -> (Int -> m [Rational]) -> m [[Rational]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [Int]
xs ((Int -> m [Rational]) -> m [[Rational]])
-> (Int -> m [Rational]) -> m [[Rational]]
forall a b. (a -> b) -> a -> b
$ \Int
x -> do
      Delta Rational
p Rational
q  <- GenericSolverM m (Delta Rational) -> Int -> m (Delta Rational)
forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> Int -> m v
getValue GenericSolverM m (Delta Rational)
solver Int
x
      Bound (Delta Rational)
lb <- GenericSolverM m (Delta Rational)
-> Int -> m (Bound (Delta Rational))
forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> Int -> m (Bound v)
getLB GenericSolverM m (Delta Rational)
solver Int
x
      Bound (Delta Rational)
ub <- GenericSolverM m (Delta Rational)
-> Int -> m (Bound (Delta Rational))
forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> Int -> m (Bound v)
getUB GenericSolverM m (Delta Rational)
solver Int
x
      [Rational] -> m [Rational]
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Rational] -> m [Rational]) -> [Rational] -> m [Rational]
forall a b. (a -> b) -> a -> b
$
        [(Rational
p Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
- Rational
c) Rational -> Rational -> Rational
forall a. Fractional a => a -> a -> a
/ (Rational
k Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
- Rational
q) | Just (Delta Rational
c Rational
k, ConstrIDSet
_) <- Bound (Delta Rational) -> [Bound (Delta Rational)]
forall a. a -> [a]
forall (m :: * -> *) a. Monad m => a -> m a
return Bound (Delta Rational)
lb, Rational
c Rational -> Rational -> Bool
forall a. Ord a => a -> a -> Bool
< Rational
p, Rational
k Rational -> Rational -> Bool
forall a. Ord a => a -> a -> Bool
> Rational
q] [Rational] -> [Rational] -> [Rational]
forall a. [a] -> [a] -> [a]
++
        [(Rational
d Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
- Rational
p) Rational -> Rational -> Rational
forall a. Fractional a => a -> a -> a
/ (Rational
q Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
- Rational
h) | Just (Delta Rational
d Rational
h, ConstrIDSet
_) <- Bound (Delta Rational) -> [Bound (Delta Rational)]
forall a. a -> [a]
forall (m :: * -> *) a. Monad m => a -> m a
return Bound (Delta Rational)
ub, Rational
p Rational -> Rational -> Bool
forall a. Ord a => a -> a -> Bool
< Rational
d, Rational
q Rational -> Rational -> Bool
forall a. Ord a => a -> a -> Bool
> Rational
h]
    let delta0 :: Rational
        delta0 :: Rational
delta0 = if [Rational] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Rational]
ys then Rational
0.1 else [Rational] -> Rational
forall a. Ord a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
minimum [Rational]
ys
        f :: Delta Rational -> Rational
        f :: Delta Rational -> Rational
f (Delta Rational
r Rational
k) = Rational
r Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
+ Rational
k Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
* Rational
delta0
    (IntMap (Delta Rational) -> Model)
-> m (IntMap (Delta Rational)) -> m Model
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM ((Delta Rational -> Rational) -> IntMap (Delta Rational) -> Model
forall a b. (a -> b) -> IntMap a -> IntMap b
IntMap.map Delta Rational -> Rational
f) (m (IntMap (Delta Rational)) -> m Model)
-> m (IntMap (Delta Rational)) -> m Model
forall a b. (a -> b) -> a -> b
$ MutVar (PrimState m) (IntMap (Delta Rational))
-> m (IntMap (Delta Rational))
forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> m a
readMutVar (GenericSolverM m (Delta Rational)
-> MutVar (PrimState m) (IntMap (Delta Rational))
forall (m :: * -> *) v.
GenericSolverM m v -> MutVar (PrimState m) (IntMap v)
svModel GenericSolverM m (Delta Rational)
solver)

type ConstrID = Int
type ConstrIDSet = IntSet

type Bound v = Maybe (v, ConstrIDSet)

boundValue :: SolverValue v => Bound v -> Maybe v
boundValue :: forall v. SolverValue v => Bound v -> Maybe v
boundValue = ((v, ConstrIDSet) -> v) -> Maybe (v, ConstrIDSet) -> Maybe v
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (v, ConstrIDSet) -> v
forall a b. (a, b) -> a
fst

boundExplanation :: SolverValue v => Bound v -> ConstrIDSet
boundExplanation :: forall v. SolverValue v => Bound v -> ConstrIDSet
boundExplanation = ConstrIDSet
-> ((v, ConstrIDSet) -> ConstrIDSet)
-> Maybe (v, ConstrIDSet)
-> ConstrIDSet
forall b a. b -> (a -> b) -> Maybe a -> b
maybe ConstrIDSet
forall a. Monoid a => a
mempty (v, ConstrIDSet) -> ConstrIDSet
forall a b. (a, b) -> b
snd

addBound :: SolverValue v => Bound v -> Bound v -> Bound v
addBound :: forall v. SolverValue v => Bound v -> Bound v -> Bound v
addBound Bound v
b1 Bound v
b2 = do
  (v
a1,ConstrIDSet
cs1) <- Bound v
b1
  (v
a2,ConstrIDSet
cs2) <- Bound v
b2
  let a3 :: v
a3 = v
a1 v -> v -> v
forall v. AdditiveGroup v => v -> v -> v
^+^ v
a2
      cs3 :: ConstrIDSet
cs3 = ConstrIDSet -> ConstrIDSet -> ConstrIDSet
IntSet.union ConstrIDSet
cs1 ConstrIDSet
cs2
  v -> Bound v -> Bound v
forall a b. a -> b -> b
seq v
a3 (Bound v -> Bound v) -> Bound v -> Bound v
forall a b. (a -> b) -> a -> b
$ ConstrIDSet -> Bound v -> Bound v
forall a b. a -> b -> b
seq ConstrIDSet
cs3 (Bound v -> Bound v) -> Bound v -> Bound v
forall a b. (a -> b) -> a -> b
$ (v, ConstrIDSet) -> Bound v
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (v
a3,ConstrIDSet
cs3)

scaleBound :: SolverValue v => Scalar v -> Bound v -> Bound v
scaleBound :: forall v. SolverValue v => Scalar v -> Bound v -> Bound v
scaleBound Scalar v
c = ((v, ConstrIDSet) -> (v, ConstrIDSet))
-> Maybe (v, ConstrIDSet) -> Maybe (v, ConstrIDSet)
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Scalar v
c Scalar v -> v -> v
forall v. VectorSpace v => Scalar v -> v -> v
*^) (v -> v)
-> (ConstrIDSet -> ConstrIDSet)
-> (v, ConstrIDSet)
-> (v, ConstrIDSet)
forall b c b' c'. (b -> c) -> (b' -> c') -> (b, b') -> (c, c')
forall (a :: * -> * -> *) b c b' c'.
Arrow a =>
a b c -> a b' c' -> a (b, b') (c, c')
*** ConstrIDSet -> ConstrIDSet
forall a. a -> a
id)

data Config
  = Config
  { Config -> PivotStrategy
configPivotStrategy :: !PivotStrategy
  , Config -> Bool
configEnableBoundTightening :: !Bool
  } deriving (Int -> Config -> ShowS
[Config] -> ShowS
Config -> String
(Int -> Config -> ShowS)
-> (Config -> String) -> ([Config] -> ShowS) -> Show Config
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Config -> ShowS
showsPrec :: Int -> Config -> ShowS
$cshow :: Config -> String
show :: Config -> String
$cshowList :: [Config] -> ShowS
showList :: [Config] -> ShowS
Show, Config -> Config -> Bool
(Config -> Config -> Bool)
-> (Config -> Config -> Bool) -> Eq Config
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Config -> Config -> Bool
== :: Config -> Config -> Bool
$c/= :: Config -> Config -> Bool
/= :: Config -> Config -> Bool
Eq, Eq Config
Eq Config =>
(Config -> Config -> Ordering)
-> (Config -> Config -> Bool)
-> (Config -> Config -> Bool)
-> (Config -> Config -> Bool)
-> (Config -> Config -> Bool)
-> (Config -> Config -> Config)
-> (Config -> Config -> Config)
-> Ord Config
Config -> Config -> Bool
Config -> Config -> Ordering
Config -> Config -> Config
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
$ccompare :: Config -> Config -> Ordering
compare :: Config -> Config -> Ordering
$c< :: Config -> Config -> Bool
< :: Config -> Config -> Bool
$c<= :: Config -> Config -> Bool
<= :: Config -> Config -> Bool
$c> :: Config -> Config -> Bool
> :: Config -> Config -> Bool
$c>= :: Config -> Config -> Bool
>= :: Config -> Config -> Bool
$cmax :: Config -> Config -> Config
max :: Config -> Config -> Config
$cmin :: Config -> Config -> Config
min :: Config -> Config -> Config
Ord)

instance Default Config where
  def :: Config
def =
    Config
    { configPivotStrategy :: PivotStrategy
configPivotStrategy = PivotStrategy
PivotStrategyBlandRule
    , configEnableBoundTightening :: Bool
configEnableBoundTightening = Bool
False
    }

setConfig :: PrimMonad m => GenericSolverM m v -> Config -> m ()
setConfig :: forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> Config -> m ()
setConfig GenericSolverM m v
solver Config
config = MutVar (PrimState m) Config -> Config -> m ()
forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> a -> m ()
writeMutVar (GenericSolverM m v -> MutVar (PrimState m) Config
forall (m :: * -> *) v.
GenericSolverM m v -> MutVar (PrimState m) Config
svConfig GenericSolverM m v
solver) Config
config

getConfig :: PrimMonad m => GenericSolverM m v -> m Config
getConfig :: forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> m Config
getConfig GenericSolverM m v
solver = MutVar (PrimState m) Config -> m Config
forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> m a
readMutVar (GenericSolverM m v -> MutVar (PrimState m) Config
forall (m :: * -> *) v.
GenericSolverM m v -> MutVar (PrimState m) Config
svConfig GenericSolverM m v
solver)

modifyConfig :: PrimMonad m => GenericSolverM m v -> (Config -> Config) -> m ()
modifyConfig :: forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> (Config -> Config) -> m ()
modifyConfig GenericSolverM m v
solver = MutVar (PrimState m) Config -> (Config -> Config) -> m ()
forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> (a -> a) -> m ()
modifyMutVar' (GenericSolverM m v -> MutVar (PrimState m) Config
forall (m :: * -> *) v.
GenericSolverM m v -> MutVar (PrimState m) Config
svConfig GenericSolverM m v
solver)

{-
Largest coefficient rule: original rule suggested by G. Dantzig.
Largest increase rule: computationally more expensive in comparison with Largest coefficient, but locally maximizes the progress.
Steepest edge rule: best pivot rule in practice, an efficient approximate implementation is "Devex".
Bland’s rule: avoids cycling but one of the slowest rules.
Random edge rule: Randomized have lead to the current best provable bounds for the number of pivot steps of the simplex method.
Lexicographic rule: used for avoiding cyclying.
-}
data PivotStrategy
  = PivotStrategyBlandRule
  | PivotStrategyLargestCoefficient
--  | PivotStrategySteepestEdge
  deriving (PivotStrategy -> PivotStrategy -> Bool
(PivotStrategy -> PivotStrategy -> Bool)
-> (PivotStrategy -> PivotStrategy -> Bool) -> Eq PivotStrategy
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: PivotStrategy -> PivotStrategy -> Bool
== :: PivotStrategy -> PivotStrategy -> Bool
$c/= :: PivotStrategy -> PivotStrategy -> Bool
/= :: PivotStrategy -> PivotStrategy -> Bool
Eq, Eq PivotStrategy
Eq PivotStrategy =>
(PivotStrategy -> PivotStrategy -> Ordering)
-> (PivotStrategy -> PivotStrategy -> Bool)
-> (PivotStrategy -> PivotStrategy -> Bool)
-> (PivotStrategy -> PivotStrategy -> Bool)
-> (PivotStrategy -> PivotStrategy -> Bool)
-> (PivotStrategy -> PivotStrategy -> PivotStrategy)
-> (PivotStrategy -> PivotStrategy -> PivotStrategy)
-> Ord PivotStrategy
PivotStrategy -> PivotStrategy -> Bool
PivotStrategy -> PivotStrategy -> Ordering
PivotStrategy -> PivotStrategy -> PivotStrategy
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
$ccompare :: PivotStrategy -> PivotStrategy -> Ordering
compare :: PivotStrategy -> PivotStrategy -> Ordering
$c< :: PivotStrategy -> PivotStrategy -> Bool
< :: PivotStrategy -> PivotStrategy -> Bool
$c<= :: PivotStrategy -> PivotStrategy -> Bool
<= :: PivotStrategy -> PivotStrategy -> Bool
$c> :: PivotStrategy -> PivotStrategy -> Bool
> :: PivotStrategy -> PivotStrategy -> Bool
$c>= :: PivotStrategy -> PivotStrategy -> Bool
>= :: PivotStrategy -> PivotStrategy -> Bool
$cmax :: PivotStrategy -> PivotStrategy -> PivotStrategy
max :: PivotStrategy -> PivotStrategy -> PivotStrategy
$cmin :: PivotStrategy -> PivotStrategy -> PivotStrategy
min :: PivotStrategy -> PivotStrategy -> PivotStrategy
Ord, Int -> PivotStrategy
PivotStrategy -> Int
PivotStrategy -> [PivotStrategy]
PivotStrategy -> PivotStrategy
PivotStrategy -> PivotStrategy -> [PivotStrategy]
PivotStrategy -> PivotStrategy -> PivotStrategy -> [PivotStrategy]
(PivotStrategy -> PivotStrategy)
-> (PivotStrategy -> PivotStrategy)
-> (Int -> PivotStrategy)
-> (PivotStrategy -> Int)
-> (PivotStrategy -> [PivotStrategy])
-> (PivotStrategy -> PivotStrategy -> [PivotStrategy])
-> (PivotStrategy -> PivotStrategy -> [PivotStrategy])
-> (PivotStrategy
    -> PivotStrategy -> PivotStrategy -> [PivotStrategy])
-> Enum PivotStrategy
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
$csucc :: PivotStrategy -> PivotStrategy
succ :: PivotStrategy -> PivotStrategy
$cpred :: PivotStrategy -> PivotStrategy
pred :: PivotStrategy -> PivotStrategy
$ctoEnum :: Int -> PivotStrategy
toEnum :: Int -> PivotStrategy
$cfromEnum :: PivotStrategy -> Int
fromEnum :: PivotStrategy -> Int
$cenumFrom :: PivotStrategy -> [PivotStrategy]
enumFrom :: PivotStrategy -> [PivotStrategy]
$cenumFromThen :: PivotStrategy -> PivotStrategy -> [PivotStrategy]
enumFromThen :: PivotStrategy -> PivotStrategy -> [PivotStrategy]
$cenumFromTo :: PivotStrategy -> PivotStrategy -> [PivotStrategy]
enumFromTo :: PivotStrategy -> PivotStrategy -> [PivotStrategy]
$cenumFromThenTo :: PivotStrategy -> PivotStrategy -> PivotStrategy -> [PivotStrategy]
enumFromThenTo :: PivotStrategy -> PivotStrategy -> PivotStrategy -> [PivotStrategy]
Enum, PivotStrategy
PivotStrategy -> PivotStrategy -> Bounded PivotStrategy
forall a. a -> a -> Bounded a
$cminBound :: PivotStrategy
minBound :: PivotStrategy
$cmaxBound :: PivotStrategy
maxBound :: PivotStrategy
Bounded, Int -> PivotStrategy -> ShowS
[PivotStrategy] -> ShowS
PivotStrategy -> String
(Int -> PivotStrategy -> ShowS)
-> (PivotStrategy -> String)
-> ([PivotStrategy] -> ShowS)
-> Show PivotStrategy
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> PivotStrategy -> ShowS
showsPrec :: Int -> PivotStrategy -> ShowS
$cshow :: PivotStrategy -> String
show :: PivotStrategy -> String
$cshowList :: [PivotStrategy] -> ShowS
showList :: [PivotStrategy] -> ShowS
Show, ReadPrec [PivotStrategy]
ReadPrec PivotStrategy
Int -> ReadS PivotStrategy
ReadS [PivotStrategy]
(Int -> ReadS PivotStrategy)
-> ReadS [PivotStrategy]
-> ReadPrec PivotStrategy
-> ReadPrec [PivotStrategy]
-> Read PivotStrategy
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
$creadsPrec :: Int -> ReadS PivotStrategy
readsPrec :: Int -> ReadS PivotStrategy
$creadList :: ReadS [PivotStrategy]
readList :: ReadS [PivotStrategy]
$creadPrec :: ReadPrec PivotStrategy
readPrec :: ReadPrec PivotStrategy
$creadListPrec :: ReadPrec [PivotStrategy]
readListPrec :: ReadPrec [PivotStrategy]
Read)

showPivotStrategy :: PivotStrategy -> String
showPivotStrategy :: PivotStrategy -> String
showPivotStrategy PivotStrategy
PivotStrategyBlandRule = String
"bland-rule"
showPivotStrategy PivotStrategy
PivotStrategyLargestCoefficient = String
"largest-coefficient"

parsePivotStrategy :: String -> Maybe PivotStrategy
parsePivotStrategy :: String -> Maybe PivotStrategy
parsePivotStrategy String
s =
  case (Char -> Char) -> ShowS
forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
toLower String
s of
    String
"bland-rule" -> PivotStrategy -> Maybe PivotStrategy
forall a. a -> Maybe a
Just PivotStrategy
PivotStrategyBlandRule
    String
"largest-coefficient" -> PivotStrategy -> Maybe PivotStrategy
forall a. a -> Maybe a
Just PivotStrategy
PivotStrategyLargestCoefficient
    String
_ -> Maybe PivotStrategy
forall a. Maybe a
Nothing

{-# DEPRECATED setPivotStrategy "Use setConfig instead" #-}
setPivotStrategy :: PrimMonad m => GenericSolverM m v -> PivotStrategy -> m ()
setPivotStrategy :: forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> PivotStrategy -> m ()
setPivotStrategy GenericSolverM m v
solver PivotStrategy
ps = GenericSolverM m v -> (Config -> Config) -> m ()
forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> (Config -> Config) -> m ()
modifyConfig GenericSolverM m v
solver ((Config -> Config) -> m ()) -> (Config -> Config) -> m ()
forall a b. (a -> b) -> a -> b
$ \Config
config ->
  Config
config{ configPivotStrategy = ps }

{--------------------------------------------------------------------
  problem description
--------------------------------------------------------------------}

data BacktrackPoint m v
  = BacktrackPoint
  { forall (m :: * -> *) v.
BacktrackPoint m v -> MutVar (PrimState m) (IntMap (Bound v))
bpSavedLB :: !(MutVar (PrimState m) (IntMap (Bound v)))
  , forall (m :: * -> *) v.
BacktrackPoint m v -> MutVar (PrimState m) (IntMap (Bound v))
bpSavedUB :: !(MutVar (PrimState m) (IntMap (Bound v)))
  }

cloneBacktrackPoint :: PrimMonad m => BacktrackPoint m v -> m (BacktrackPoint m v)
cloneBacktrackPoint :: forall (m :: * -> *) v.
PrimMonad m =>
BacktrackPoint m v -> m (BacktrackPoint m v)
cloneBacktrackPoint BacktrackPoint m v
bp = do
  MutVar (PrimState m) (IntMap (Bound v))
lbs <- IntMap (Bound v) -> m (MutVar (PrimState m) (IntMap (Bound v)))
forall (m :: * -> *) a.
PrimMonad m =>
a -> m (MutVar (PrimState m) a)
newMutVar (IntMap (Bound v) -> m (MutVar (PrimState m) (IntMap (Bound v))))
-> m (IntMap (Bound v))
-> m (MutVar (PrimState m) (IntMap (Bound v)))
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< MutVar (PrimState m) (IntMap (Bound v)) -> m (IntMap (Bound v))
forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> m a
readMutVar (BacktrackPoint m v -> MutVar (PrimState m) (IntMap (Bound v))
forall (m :: * -> *) v.
BacktrackPoint m v -> MutVar (PrimState m) (IntMap (Bound v))
bpSavedLB BacktrackPoint m v
bp)
  MutVar (PrimState m) (IntMap (Bound v))
ubs <- IntMap (Bound v) -> m (MutVar (PrimState m) (IntMap (Bound v)))
forall (m :: * -> *) a.
PrimMonad m =>
a -> m (MutVar (PrimState m) a)
newMutVar (IntMap (Bound v) -> m (MutVar (PrimState m) (IntMap (Bound v))))
-> m (IntMap (Bound v))
-> m (MutVar (PrimState m) (IntMap (Bound v)))
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< MutVar (PrimState m) (IntMap (Bound v)) -> m (IntMap (Bound v))
forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> m a
readMutVar (BacktrackPoint m v -> MutVar (PrimState m) (IntMap (Bound v))
forall (m :: * -> *) v.
BacktrackPoint m v -> MutVar (PrimState m) (IntMap (Bound v))
bpSavedUB BacktrackPoint m v
bp)
  BacktrackPoint m v -> m (BacktrackPoint m v)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (BacktrackPoint m v -> m (BacktrackPoint m v))
-> BacktrackPoint m v -> m (BacktrackPoint m v)
forall a b. (a -> b) -> a -> b
$ MutVar (PrimState m) (IntMap (Bound v))
-> MutVar (PrimState m) (IntMap (Bound v)) -> BacktrackPoint m v
forall (m :: * -> *) v.
MutVar (PrimState m) (IntMap (Bound v))
-> MutVar (PrimState m) (IntMap (Bound v)) -> BacktrackPoint m v
BacktrackPoint MutVar (PrimState m) (IntMap (Bound v))
lbs MutVar (PrimState m) (IntMap (Bound v))
ubs

pushBacktrackPoint :: PrimMonad m => GenericSolverM m v -> m ()
pushBacktrackPoint :: forall (m :: * -> *) v. PrimMonad m => GenericSolverM m v -> m ()
pushBacktrackPoint GenericSolverM m v
solver = do
  MutVar (PrimState m) (IntMap (Bound v))
savedLBs <- IntMap (Bound v) -> m (MutVar (PrimState m) (IntMap (Bound v)))
forall (m :: * -> *) a.
PrimMonad m =>
a -> m (MutVar (PrimState m) a)
newMutVar IntMap (Bound v)
forall a. IntMap a
IntMap.empty
  MutVar (PrimState m) (IntMap (Bound v))
savedUBs <- IntMap (Bound v) -> m (MutVar (PrimState m) (IntMap (Bound v)))
forall (m :: * -> *) a.
PrimMonad m =>
a -> m (MutVar (PrimState m) a)
newMutVar IntMap (Bound v)
forall a. IntMap a
IntMap.empty
  IntMap (v, ConstrIDSet)
lbs <- MutVar (PrimState m) (IntMap (v, ConstrIDSet))
-> m (IntMap (v, ConstrIDSet))
forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> m a
readMutVar (GenericSolverM m v
-> MutVar (PrimState m) (IntMap (v, ConstrIDSet))
forall (m :: * -> *) v.
GenericSolverM m v
-> MutVar (PrimState m) (IntMap (v, ConstrIDSet))
svLB GenericSolverM m v
solver)
  IntMap (v, ConstrIDSet)
ubs <- MutVar (PrimState m) (IntMap (v, ConstrIDSet))
-> m (IntMap (v, ConstrIDSet))
forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> m a
readMutVar (GenericSolverM m v
-> MutVar (PrimState m) (IntMap (v, ConstrIDSet))
forall (m :: * -> *) v.
GenericSolverM m v
-> MutVar (PrimState m) (IntMap (v, ConstrIDSet))
svUB GenericSolverM m v
solver)
  MutVar (PrimState m) [BacktrackPoint m v]
-> ([BacktrackPoint m v] -> [BacktrackPoint m v]) -> m ()
forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> (a -> a) -> m ()
modifyMutVar (GenericSolverM m v -> MutVar (PrimState m) [BacktrackPoint m v]
forall (m :: * -> *) v.
GenericSolverM m v -> MutVar (PrimState m) [BacktrackPoint m v]
svBacktrackPoints GenericSolverM m v
solver) (MutVar (PrimState m) (IntMap (Bound v))
-> MutVar (PrimState m) (IntMap (Bound v)) -> BacktrackPoint m v
forall (m :: * -> *) v.
MutVar (PrimState m) (IntMap (Bound v))
-> MutVar (PrimState m) (IntMap (Bound v)) -> BacktrackPoint m v
BacktrackPoint MutVar (PrimState m) (IntMap (Bound v))
savedLBs MutVar (PrimState m) (IntMap (Bound v))
savedUBs BacktrackPoint m v -> [BacktrackPoint m v] -> [BacktrackPoint m v]
forall a. a -> [a] -> [a]
:)

popBacktrackPoint :: PrimMonad m => GenericSolverM m v -> m ()
popBacktrackPoint :: forall (m :: * -> *) v. PrimMonad m => GenericSolverM m v -> m ()
popBacktrackPoint GenericSolverM m v
solver = do
  [BacktrackPoint m v]
bps <- MutVar (PrimState m) [BacktrackPoint m v] -> m [BacktrackPoint m v]
forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> m a
readMutVar (GenericSolverM m v -> MutVar (PrimState m) [BacktrackPoint m v]
forall (m :: * -> *) v.
GenericSolverM m v -> MutVar (PrimState m) [BacktrackPoint m v]
svBacktrackPoints GenericSolverM m v
solver)
  case [BacktrackPoint m v]
bps of
    [] -> String -> m ()
forall a. HasCallStack => String -> a
error String
"popBacktrackPoint: empty backtrack points"
    BacktrackPoint m v
bp : [BacktrackPoint m v]
bps' -> do
      IntMap (v, ConstrIDSet)
lbs <- MutVar (PrimState m) (IntMap (v, ConstrIDSet))
-> m (IntMap (v, ConstrIDSet))
forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> m a
readMutVar (GenericSolverM m v
-> MutVar (PrimState m) (IntMap (v, ConstrIDSet))
forall (m :: * -> *) v.
GenericSolverM m v
-> MutVar (PrimState m) (IntMap (v, ConstrIDSet))
svLB GenericSolverM m v
solver)
      IntMap (Bound v)
savedLBs <- MutVar (PrimState m) (IntMap (Bound v)) -> m (IntMap (Bound v))
forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> m a
readMutVar (BacktrackPoint m v -> MutVar (PrimState m) (IntMap (Bound v))
forall (m :: * -> *) v.
BacktrackPoint m v -> MutVar (PrimState m) (IntMap (Bound v))
bpSavedLB BacktrackPoint m v
bp)
      MutVar (PrimState m) (IntMap (v, ConstrIDSet))
-> IntMap (v, ConstrIDSet) -> m ()
forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> a -> m ()
writeMutVar (GenericSolverM m v
-> MutVar (PrimState m) (IntMap (v, ConstrIDSet))
forall (m :: * -> *) v.
GenericSolverM m v
-> MutVar (PrimState m) (IntMap (v, ConstrIDSet))
svLB GenericSolverM m v
solver) (IntMap (v, ConstrIDSet) -> m ())
-> IntMap (v, ConstrIDSet) -> m ()
forall a b. (a -> b) -> a -> b
$ (Int -> (v, ConstrIDSet) -> Bound v -> Bound v)
-> (IntMap (v, ConstrIDSet) -> IntMap (v, ConstrIDSet))
-> (IntMap (Bound v) -> IntMap (v, ConstrIDSet))
-> IntMap (v, ConstrIDSet)
-> IntMap (Bound v)
-> IntMap (v, ConstrIDSet)
forall a b c.
(Int -> a -> b -> Maybe c)
-> (IntMap a -> IntMap c)
-> (IntMap b -> IntMap c)
-> IntMap a
-> IntMap b
-> IntMap c
IntMap.mergeWithKey (\Int
_ (v, ConstrIDSet)
_curr Bound v
saved -> Bound v
saved) IntMap (v, ConstrIDSet) -> IntMap (v, ConstrIDSet)
forall a. a -> a
id (IntMap (v, ConstrIDSet)
-> IntMap (Bound v) -> IntMap (v, ConstrIDSet)
forall a b. a -> b -> a
const IntMap (v, ConstrIDSet)
forall a. IntMap a
IntMap.empty) IntMap (v, ConstrIDSet)
lbs IntMap (Bound v)
savedLBs

      IntMap (v, ConstrIDSet)
ubs <- MutVar (PrimState m) (IntMap (v, ConstrIDSet))
-> m (IntMap (v, ConstrIDSet))
forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> m a
readMutVar (GenericSolverM m v
-> MutVar (PrimState m) (IntMap (v, ConstrIDSet))
forall (m :: * -> *) v.
GenericSolverM m v
-> MutVar (PrimState m) (IntMap (v, ConstrIDSet))
svUB GenericSolverM m v
solver)
      IntMap (Bound v)
savedUBs <- MutVar (PrimState m) (IntMap (Bound v)) -> m (IntMap (Bound v))
forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> m a
readMutVar (BacktrackPoint m v -> MutVar (PrimState m) (IntMap (Bound v))
forall (m :: * -> *) v.
BacktrackPoint m v -> MutVar (PrimState m) (IntMap (Bound v))
bpSavedUB BacktrackPoint m v
bp)
      MutVar (PrimState m) (IntMap (v, ConstrIDSet))
-> IntMap (v, ConstrIDSet) -> m ()
forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> a -> m ()
writeMutVar (GenericSolverM m v
-> MutVar (PrimState m) (IntMap (v, ConstrIDSet))
forall (m :: * -> *) v.
GenericSolverM m v
-> MutVar (PrimState m) (IntMap (v, ConstrIDSet))
svUB GenericSolverM m v
solver) (IntMap (v, ConstrIDSet) -> m ())
-> IntMap (v, ConstrIDSet) -> m ()
forall a b. (a -> b) -> a -> b
$ (Int -> (v, ConstrIDSet) -> Bound v -> Bound v)
-> (IntMap (v, ConstrIDSet) -> IntMap (v, ConstrIDSet))
-> (IntMap (Bound v) -> IntMap (v, ConstrIDSet))
-> IntMap (v, ConstrIDSet)
-> IntMap (Bound v)
-> IntMap (v, ConstrIDSet)
forall a b c.
(Int -> a -> b -> Maybe c)
-> (IntMap a -> IntMap c)
-> (IntMap b -> IntMap c)
-> IntMap a
-> IntMap b
-> IntMap c
IntMap.mergeWithKey (\Int
_ (v, ConstrIDSet)
_curr Bound v
saved -> Bound v
saved) IntMap (v, ConstrIDSet) -> IntMap (v, ConstrIDSet)
forall a. a -> a
id (IntMap (v, ConstrIDSet)
-> IntMap (Bound v) -> IntMap (v, ConstrIDSet)
forall a b. a -> b -> a
const IntMap (v, ConstrIDSet)
forall a. IntMap a
IntMap.empty) IntMap (v, ConstrIDSet)
ubs IntMap (Bound v)
savedUBs

      MutVar (PrimState m) [BacktrackPoint m v]
-> [BacktrackPoint m v] -> m ()
forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> a -> m ()
writeMutVar (GenericSolverM m v -> MutVar (PrimState m) [BacktrackPoint m v]
forall (m :: * -> *) v.
GenericSolverM m v -> MutVar (PrimState m) [BacktrackPoint m v]
svBacktrackPoints GenericSolverM m v
solver) [BacktrackPoint m v]
bps'
      MutVar (PrimState m) (Maybe ConstrIDSet)
-> Maybe ConstrIDSet -> m ()
forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> a -> m ()
writeMutVar (GenericSolverM m v -> MutVar (PrimState m) (Maybe ConstrIDSet)
forall (m :: * -> *) v.
GenericSolverM m v -> MutVar (PrimState m) (Maybe ConstrIDSet)
svExplanation GenericSolverM m v
solver) Maybe ConstrIDSet
forall a. Maybe a
Nothing

withBacktrackpoint :: PrimMonad m => GenericSolverM m v -> (BacktrackPoint m v -> m ()) -> m ()
withBacktrackpoint :: forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> (BacktrackPoint m v -> m ()) -> m ()
withBacktrackpoint GenericSolverM m v
solver BacktrackPoint m v -> m ()
f = do
  [BacktrackPoint m v]
bps <- MutVar (PrimState m) [BacktrackPoint m v] -> m [BacktrackPoint m v]
forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> m a
readMutVar (GenericSolverM m v -> MutVar (PrimState m) [BacktrackPoint m v]
forall (m :: * -> *) v.
GenericSolverM m v -> MutVar (PrimState m) [BacktrackPoint m v]
svBacktrackPoints GenericSolverM m v
solver)
  case [BacktrackPoint m v]
bps of
    [] -> () -> m ()
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    BacktrackPoint m v
bp : [BacktrackPoint m v]
_ -> BacktrackPoint m v -> m ()
f BacktrackPoint m v
bp

bpSaveLB :: PrimMonad m => GenericSolverM m v -> Var -> m ()
bpSaveLB :: forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> Int -> m ()
bpSaveLB GenericSolverM m v
solver Int
v = do
  GenericSolverM m v -> (BacktrackPoint m v -> m ()) -> m ()
forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> (BacktrackPoint m v -> m ()) -> m ()
withBacktrackpoint GenericSolverM m v
solver ((BacktrackPoint m v -> m ()) -> m ())
-> (BacktrackPoint m v -> m ()) -> m ()
forall a b. (a -> b) -> a -> b
$ \BacktrackPoint m v
bp -> do
    IntMap (Bound v)
saved <- MutVar (PrimState m) (IntMap (Bound v)) -> m (IntMap (Bound v))
forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> m a
readMutVar (BacktrackPoint m v -> MutVar (PrimState m) (IntMap (Bound v))
forall (m :: * -> *) v.
BacktrackPoint m v -> MutVar (PrimState m) (IntMap (Bound v))
bpSavedLB BacktrackPoint m v
bp)
    if Int
v Int -> IntMap (Bound v) -> Bool
forall a. Int -> IntMap a -> Bool
`IntMap.member` IntMap (Bound v)
saved then
      () -> m ()
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    else do
      IntMap (v, ConstrIDSet)
lb <- MutVar (PrimState m) (IntMap (v, ConstrIDSet))
-> m (IntMap (v, ConstrIDSet))
forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> m a
readMutVar (GenericSolverM m v
-> MutVar (PrimState m) (IntMap (v, ConstrIDSet))
forall (m :: * -> *) v.
GenericSolverM m v
-> MutVar (PrimState m) (IntMap (v, ConstrIDSet))
svLB GenericSolverM m v
solver)
      let old :: Bound v
old = Int -> IntMap (v, ConstrIDSet) -> Bound v
forall a. Int -> IntMap a -> Maybe a
IntMap.lookup Int
v IntMap (v, ConstrIDSet)
lb
      Bound v -> m () -> m ()
forall a b. a -> b -> b
seq Bound v
old (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ MutVar (PrimState m) (IntMap (Bound v)) -> IntMap (Bound v) -> m ()
forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> a -> m ()
writeMutVar (BacktrackPoint m v -> MutVar (PrimState m) (IntMap (Bound v))
forall (m :: * -> *) v.
BacktrackPoint m v -> MutVar (PrimState m) (IntMap (Bound v))
bpSavedLB BacktrackPoint m v
bp) (Int -> Bound v -> IntMap (Bound v) -> IntMap (Bound v)
forall a. Int -> a -> IntMap a -> IntMap a
IntMap.insert Int
v Bound v
old IntMap (Bound v)
saved)

bpSaveUB :: PrimMonad m => GenericSolverM m v -> Var -> m ()
bpSaveUB :: forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> Int -> m ()
bpSaveUB GenericSolverM m v
solver Int
v = do
  GenericSolverM m v -> (BacktrackPoint m v -> m ()) -> m ()
forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> (BacktrackPoint m v -> m ()) -> m ()
withBacktrackpoint GenericSolverM m v
solver ((BacktrackPoint m v -> m ()) -> m ())
-> (BacktrackPoint m v -> m ()) -> m ()
forall a b. (a -> b) -> a -> b
$ \BacktrackPoint m v
bp -> do
    IntMap (Bound v)
saved <- MutVar (PrimState m) (IntMap (Bound v)) -> m (IntMap (Bound v))
forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> m a
readMutVar (BacktrackPoint m v -> MutVar (PrimState m) (IntMap (Bound v))
forall (m :: * -> *) v.
BacktrackPoint m v -> MutVar (PrimState m) (IntMap (Bound v))
bpSavedUB BacktrackPoint m v
bp)
    if Int
v Int -> IntMap (Bound v) -> Bool
forall a. Int -> IntMap a -> Bool
`IntMap.member` IntMap (Bound v)
saved then
      () -> m ()
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    else do
      IntMap (v, ConstrIDSet)
ub <- MutVar (PrimState m) (IntMap (v, ConstrIDSet))
-> m (IntMap (v, ConstrIDSet))
forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> m a
readMutVar (GenericSolverM m v
-> MutVar (PrimState m) (IntMap (v, ConstrIDSet))
forall (m :: * -> *) v.
GenericSolverM m v
-> MutVar (PrimState m) (IntMap (v, ConstrIDSet))
svUB GenericSolverM m v
solver)
      let old :: Bound v
old = Int -> IntMap (v, ConstrIDSet) -> Bound v
forall a. Int -> IntMap a -> Maybe a
IntMap.lookup Int
v IntMap (v, ConstrIDSet)
ub
      Bound v -> m () -> m ()
forall a b. a -> b -> b
seq Bound v
old (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ MutVar (PrimState m) (IntMap (Bound v)) -> IntMap (Bound v) -> m ()
forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> a -> m ()
writeMutVar (BacktrackPoint m v -> MutVar (PrimState m) (IntMap (Bound v))
forall (m :: * -> *) v.
BacktrackPoint m v -> MutVar (PrimState m) (IntMap (Bound v))
bpSavedUB BacktrackPoint m v
bp) (Int -> Bound v -> IntMap (Bound v) -> IntMap (Bound v)
forall a. Int -> a -> IntMap a -> IntMap a
IntMap.insert Int
v Bound v
old IntMap (Bound v)
saved)

{--------------------------------------------------------------------
  problem description
--------------------------------------------------------------------}

newVar :: (PrimMonad m, SolverValue v) => GenericSolverM m v -> m Var
newVar :: forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> m Int
newVar GenericSolverM m v
solver = do
  Int
v <- MutVar (PrimState m) Int -> m Int
forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> m a
readMutVar (GenericSolverM m v -> MutVar (PrimState m) Int
forall (m :: * -> *) v.
GenericSolverM m v -> MutVar (PrimState m) Int
svVCnt GenericSolverM m v
solver)
  MutVar (PrimState m) Int -> Int -> m ()
forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> a -> m ()
writeMutVar (GenericSolverM m v -> MutVar (PrimState m) Int
forall (m :: * -> *) v.
GenericSolverM m v -> MutVar (PrimState m) Int
svVCnt GenericSolverM m v
solver) (Int -> m ()) -> Int -> m ()
forall a b. (a -> b) -> a -> b
$! Int
vInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1
  MutVar (PrimState m) (IntMap v) -> (IntMap v -> IntMap v) -> m ()
forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> (a -> a) -> m ()
modifyMutVar (GenericSolverM m v -> MutVar (PrimState m) (IntMap v)
forall (m :: * -> *) v.
GenericSolverM m v -> MutVar (PrimState m) (IntMap v)
svModel GenericSolverM m v
solver) (Int -> v -> IntMap v -> IntMap v
forall a. Int -> a -> IntMap a -> IntMap a
IntMap.insert Int
v v
forall v. AdditiveGroup v => v
zeroV)
  Int -> m Int
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Int
v

assertAtom :: PrimMonad m => GenericSolverM m Rational -> LA.Atom Rational -> m ()
assertAtom :: forall (m :: * -> *).
PrimMonad m =>
GenericSolverM m Rational -> Atom Rational -> m ()
assertAtom GenericSolverM m Rational
solver Atom Rational
atom = GenericSolverM m Rational -> Atom Rational -> Maybe Int -> m ()
forall (m :: * -> *).
PrimMonad m =>
GenericSolverM m Rational -> Atom Rational -> Maybe Int -> m ()
assertAtom' GenericSolverM m Rational
solver Atom Rational
atom Maybe Int
forall a. Maybe a
Nothing

assertAtom' :: PrimMonad m => GenericSolverM m Rational -> LA.Atom Rational -> Maybe ConstrID -> m ()
assertAtom' :: forall (m :: * -> *).
PrimMonad m =>
GenericSolverM m Rational -> Atom Rational -> Maybe Int -> m ()
assertAtom' GenericSolverM m Rational
solver Atom Rational
atom Maybe Int
cid = do
  (Int
v,RelOp
op,Rational
rhs') <- GenericSolverM m Rational
-> Atom Rational -> m (Int, RelOp, Rational)
forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> Atom Rational -> m (Int, RelOp, Rational)
simplifyAtom GenericSolverM m Rational
solver Atom Rational
atom
  case RelOp
op of
    RelOp
Le  -> GenericSolverM m Rational -> Int -> Rational -> Maybe Int -> m ()
forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> Int -> v -> Maybe Int -> m ()
assertUpper' GenericSolverM m Rational
solver Int
v (Rational -> Rational
forall v. SolverValue v => Rational -> v
toValue Rational
rhs') Maybe Int
cid
    RelOp
Ge  -> GenericSolverM m Rational -> Int -> Rational -> Maybe Int -> m ()
forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> Int -> v -> Maybe Int -> m ()
assertLower' GenericSolverM m Rational
solver Int
v (Rational -> Rational
forall v. SolverValue v => Rational -> v
toValue Rational
rhs') Maybe Int
cid
    RelOp
Eql -> do
      GenericSolverM m Rational -> Int -> Rational -> Maybe Int -> m ()
forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> Int -> v -> Maybe Int -> m ()
assertLower' GenericSolverM m Rational
solver Int
v (Rational -> Rational
forall v. SolverValue v => Rational -> v
toValue Rational
rhs') Maybe Int
cid
      GenericSolverM m Rational -> Int -> Rational -> Maybe Int -> m ()
forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> Int -> v -> Maybe Int -> m ()
assertUpper' GenericSolverM m Rational
solver Int
v (Rational -> Rational
forall v. SolverValue v => Rational -> v
toValue Rational
rhs') Maybe Int
cid
    RelOp
_ -> String -> m ()
forall a. HasCallStack => String -> a
error String
"unsupported"
  () -> m ()
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ()

assertAtomEx :: PrimMonad m => GenericSolverM m (Delta Rational) -> LA.Atom Rational -> m ()
assertAtomEx :: forall (m :: * -> *).
PrimMonad m =>
GenericSolverM m (Delta Rational) -> Atom Rational -> m ()
assertAtomEx GenericSolverM m (Delta Rational)
solver Atom Rational
atom = GenericSolverM m (Delta Rational)
-> Atom Rational -> Maybe Int -> m ()
forall (m :: * -> *).
PrimMonad m =>
GenericSolverM m (Delta Rational)
-> Atom Rational -> Maybe Int -> m ()
assertAtomEx' GenericSolverM m (Delta Rational)
solver Atom Rational
atom Maybe Int
forall a. Maybe a
Nothing

assertAtomEx' :: PrimMonad m => GenericSolverM m (Delta Rational) -> LA.Atom Rational -> Maybe ConstrID -> m ()
assertAtomEx' :: forall (m :: * -> *).
PrimMonad m =>
GenericSolverM m (Delta Rational)
-> Atom Rational -> Maybe Int -> m ()
assertAtomEx' GenericSolverM m (Delta Rational)
solver Atom Rational
atom Maybe Int
cid = do
  (Int
v,RelOp
op,Rational
rhs') <- GenericSolverM m (Delta Rational)
-> Atom Rational -> m (Int, RelOp, Rational)
forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> Atom Rational -> m (Int, RelOp, Rational)
simplifyAtom GenericSolverM m (Delta Rational)
solver Atom Rational
atom
  case RelOp
op of
    RelOp
Le  -> GenericSolverM m (Delta Rational)
-> Int -> Delta Rational -> Maybe Int -> m ()
forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> Int -> v -> Maybe Int -> m ()
assertUpper' GenericSolverM m (Delta Rational)
solver Int
v (Rational -> Delta Rational
forall v. SolverValue v => Rational -> v
toValue Rational
rhs') Maybe Int
cid
    RelOp
Ge  -> GenericSolverM m (Delta Rational)
-> Int -> Delta Rational -> Maybe Int -> m ()
forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> Int -> v -> Maybe Int -> m ()
assertLower' GenericSolverM m (Delta Rational)
solver Int
v (Rational -> Delta Rational
forall v. SolverValue v => Rational -> v
toValue Rational
rhs') Maybe Int
cid
    RelOp
Lt  -> GenericSolverM m (Delta Rational)
-> Int -> Delta Rational -> Maybe Int -> m ()
forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> Int -> v -> Maybe Int -> m ()
assertUpper' GenericSolverM m (Delta Rational)
solver Int
v (Rational -> Delta Rational
forall v. SolverValue v => Rational -> v
toValue Rational
rhs' Delta Rational -> Delta Rational -> Delta Rational
forall v. AdditiveGroup v => v -> v -> v
^-^ Delta Rational
forall r. Num r => Delta r
delta) Maybe Int
cid
    RelOp
Gt  -> GenericSolverM m (Delta Rational)
-> Int -> Delta Rational -> Maybe Int -> m ()
forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> Int -> v -> Maybe Int -> m ()
assertLower' GenericSolverM m (Delta Rational)
solver Int
v (Rational -> Delta Rational
forall v. SolverValue v => Rational -> v
toValue Rational
rhs' Delta Rational -> Delta Rational -> Delta Rational
forall v. AdditiveGroup v => v -> v -> v
^+^ Delta Rational
forall r. Num r => Delta r
delta) Maybe Int
cid
    RelOp
Eql -> do
      GenericSolverM m (Delta Rational)
-> Int -> Delta Rational -> Maybe Int -> m ()
forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> Int -> v -> Maybe Int -> m ()
assertLower' GenericSolverM m (Delta Rational)
solver Int
v (Rational -> Delta Rational
forall v. SolverValue v => Rational -> v
toValue Rational
rhs') Maybe Int
cid
      GenericSolverM m (Delta Rational)
-> Int -> Delta Rational -> Maybe Int -> m ()
forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> Int -> v -> Maybe Int -> m ()
assertUpper' GenericSolverM m (Delta Rational)
solver Int
v (Rational -> Delta Rational
forall v. SolverValue v => Rational -> v
toValue Rational
rhs') Maybe Int
cid
  () -> m ()
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ()

simplifyAtom :: (PrimMonad m, SolverValue v) => GenericSolverM m v -> LA.Atom Rational -> m (Var, RelOp, Rational)
simplifyAtom :: forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> Atom Rational -> m (Int, RelOp, Rational)
simplifyAtom GenericSolverM m v
solver (OrdRel Expr Rational
lhs RelOp
op Expr Rational
rhs) = do
  let (Expr Rational
lhs',Rational
rhs') =
        case Int -> Expr Rational -> (Rational, Expr Rational)
forall r. Num r => Int -> Expr r -> (r, Expr r)
LA.extract Int
LA.unitVar (Expr Rational
lhs Expr Rational -> Expr Rational -> Expr Rational
forall v. AdditiveGroup v => v -> v -> v
^-^ Expr Rational
rhs) of
          (Rational
n,Expr Rational
e) -> (Expr Rational
e, -Rational
n)
  case Expr Rational -> [(Rational, Int)]
forall r. Expr r -> [(r, Int)]
LA.terms Expr Rational
lhs' of
    [(Rational
1,Int
v)] -> (Int, RelOp, Rational) -> m (Int, RelOp, Rational)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Int
v, RelOp
op, Rational
rhs')
    [(-1,Int
v)] -> (Int, RelOp, Rational) -> m (Int, RelOp, Rational)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Int
v, RelOp -> RelOp
flipOp RelOp
op, -Rational
rhs')
    [(Rational, Int)]
_ -> do
      Map (Expr Rational) Int
defs <- MutVar (PrimState m) (Map (Expr Rational) Int)
-> m (Map (Expr Rational) Int)
forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> m a
readMutVar (GenericSolverM m v
-> MutVar (PrimState m) (Map (Expr Rational) Int)
forall (m :: * -> *) v.
GenericSolverM m v
-> MutVar (PrimState m) (Map (Expr Rational) Int)
svDefDB GenericSolverM m v
solver)
      let (Rational
c,Expr Rational
lhs'') = Expr Rational -> (Rational, Expr Rational)
scale Expr Rational
lhs' -- lhs' = lhs'' / c = rhs'
          rhs'' :: Rational
rhs'' = Rational
Scalar Rational
c Scalar Rational -> Rational -> Rational
forall v. VectorSpace v => Scalar v -> v -> v
*^ Rational
rhs'
          op'' :: RelOp
op''  = if Rational
c Rational -> Rational -> Bool
forall a. Ord a => a -> a -> Bool
< Rational
0 then RelOp -> RelOp
flipOp RelOp
op else RelOp
op
      case Expr Rational -> Map (Expr Rational) Int -> Maybe Int
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Expr Rational
lhs'' Map (Expr Rational) Int
defs of
        Just Int
v -> do
          (Int, RelOp, Rational) -> m (Int, RelOp, Rational)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Int
v,RelOp
op'',Rational
rhs'')
        Maybe Int
Nothing -> do
          Int
v <- GenericSolverM m v -> m Int
forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> m Int
newVar GenericSolverM m v
solver
          GenericSolverM m v -> Int -> Expr Rational -> m ()
forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> Int -> Expr Rational -> m ()
setRow GenericSolverM m v
solver Int
v Expr Rational
lhs''
          MutVar (PrimState m) (Map (Expr Rational) Int)
-> (Map (Expr Rational) Int -> Map (Expr Rational) Int) -> m ()
forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> (a -> a) -> m ()
modifyMutVar (GenericSolverM m v
-> MutVar (PrimState m) (Map (Expr Rational) Int)
forall (m :: * -> *) v.
GenericSolverM m v
-> MutVar (PrimState m) (Map (Expr Rational) Int)
svDefDB GenericSolverM m v
solver) ((Map (Expr Rational) Int -> Map (Expr Rational) Int) -> m ())
-> (Map (Expr Rational) Int -> Map (Expr Rational) Int) -> m ()
forall a b. (a -> b) -> a -> b
$ Expr Rational
-> Int -> Map (Expr Rational) Int -> Map (Expr Rational) Int
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Expr Rational
lhs'' Int
v
          case Expr Rational -> Maybe Rational
forall r. Num r => Expr r -> Maybe r
LA.asConst Expr Rational
lhs'' of
            Just Rational
0 -> do
              MutVar (PrimState m) (IntMap (v, ConstrIDSet))
-> (IntMap (v, ConstrIDSet) -> IntMap (v, ConstrIDSet)) -> m ()
forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> (a -> a) -> m ()
modifyMutVar (GenericSolverM m v
-> MutVar (PrimState m) (IntMap (v, ConstrIDSet))
forall (m :: * -> *) v.
GenericSolverM m v
-> MutVar (PrimState m) (IntMap (v, ConstrIDSet))
svLB GenericSolverM m v
solver) (Int
-> (v, ConstrIDSet)
-> IntMap (v, ConstrIDSet)
-> IntMap (v, ConstrIDSet)
forall a. Int -> a -> IntMap a -> IntMap a
IntMap.insert Int
v (Rational -> v
forall v. SolverValue v => Rational -> v
toValue Rational
0, ConstrIDSet
forall a. Monoid a => a
mempty))
              MutVar (PrimState m) (IntMap (v, ConstrIDSet))
-> (IntMap (v, ConstrIDSet) -> IntMap (v, ConstrIDSet)) -> m ()
forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> (a -> a) -> m ()
modifyMutVar (GenericSolverM m v
-> MutVar (PrimState m) (IntMap (v, ConstrIDSet))
forall (m :: * -> *) v.
GenericSolverM m v
-> MutVar (PrimState m) (IntMap (v, ConstrIDSet))
svUB GenericSolverM m v
solver) (Int
-> (v, ConstrIDSet)
-> IntMap (v, ConstrIDSet)
-> IntMap (v, ConstrIDSet)
forall a. Int -> a -> IntMap a -> IntMap a
IntMap.insert Int
v (Rational -> v
forall v. SolverValue v => Rational -> v
toValue Rational
0, ConstrIDSet
forall a. Monoid a => a
mempty))
            Maybe Rational
_ -> do
              Config
config <- GenericSolverM m v -> m Config
forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> m Config
getConfig GenericSolverM m v
solver
              Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Config -> Bool
configEnableBoundTightening Config
config) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ do
                GenericSolverM m v -> Int -> m ()
forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> Int -> m ()
tightenBounds GenericSolverM m v
solver Int
v
          (Int, RelOp, Rational) -> m (Int, RelOp, Rational)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Int
v,RelOp
op'',Rational
rhs'')
  where
    scale :: LA.Expr Rational -> (Rational, LA.Expr Rational)
    scale :: Expr Rational -> (Rational, Expr Rational)
scale Expr Rational
e = (Rational
c, Rational
Scalar (Expr Rational)
c Scalar (Expr Rational) -> Expr Rational -> Expr Rational
forall v. VectorSpace v => Scalar v -> v -> v
*^ Expr Rational
e)
      where
        c :: Rational
c = Rational
c1 Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
* Rational
c2
        c1 :: Rational
c1 = Integer -> Rational
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Integer -> Rational) -> Integer -> Rational
forall a b. (a -> b) -> a -> b
$ (Integer -> Integer -> Integer) -> Integer -> [Integer] -> Integer
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
lcm Integer
1 [Rational -> Integer
forall a. Ratio a -> a
denominator Rational
c | (Rational
c, Int
_) <- Expr Rational -> [(Rational, Int)]
forall r. Expr r -> [(r, Int)]
LA.terms Expr Rational
e]
        c2 :: Rational
c2 = Rational -> Rational
forall a. Num a => a -> a
signum (Rational -> Rational) -> Rational -> Rational
forall a b. (a -> b) -> a -> b
$ [Rational] -> Rational
forall a. HasCallStack => [a] -> a
head ([Rational
c | (Rational
c,Int
x) <- Expr Rational -> [(Rational, Int)]
forall r. Expr r -> [(r, Int)]
LA.terms Expr Rational
e] [Rational] -> [Rational] -> [Rational]
forall a. [a] -> [a] -> [a]
++ [Rational
1])

assertLower :: (PrimMonad m, SolverValue v) => GenericSolverM m v -> Var -> v -> m ()
assertLower :: forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> Int -> v -> m ()
assertLower GenericSolverM m v
solver Int
x v
l = GenericSolverM m v -> Int -> Bound v -> m ()
forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> Int -> Bound v -> m ()
assertLB GenericSolverM m v
solver Int
x ((v, ConstrIDSet) -> Bound v
forall a. a -> Maybe a
Just (v
l, ConstrIDSet
IntSet.empty))

assertLower' :: (PrimMonad m, SolverValue v) => GenericSolverM m v -> Var -> v -> Maybe ConstrID -> m ()
assertLower' :: forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> Int -> v -> Maybe Int -> m ()
assertLower' GenericSolverM m v
solver Int
x v
l Maybe Int
cid = GenericSolverM m v -> Int -> Bound v -> m ()
forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> Int -> Bound v -> m ()
assertLB GenericSolverM m v
solver Int
x ((v, ConstrIDSet) -> Bound v
forall a. a -> Maybe a
Just (v
l, [Int] -> ConstrIDSet
IntSet.fromList (Maybe Int -> [Int]
forall a. Maybe a -> [a]
maybeToList Maybe Int
cid)))

assertLB :: (PrimMonad m, SolverValue v) => GenericSolverM m v -> Var -> Bound v -> m ()
assertLB :: forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> Int -> Bound v -> m ()
assertLB GenericSolverM m v
solver Int
x Maybe (v, ConstrIDSet)
Nothing = () -> m ()
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
assertLB GenericSolverM m v
solver Int
x (Just (v
l, ConstrIDSet
cidSet)) = do
  Maybe (v, ConstrIDSet)
l0 <- GenericSolverM m v -> Int -> m (Maybe (v, ConstrIDSet))
forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> Int -> m (Bound v)
getLB GenericSolverM m v
solver Int
x
  Maybe (v, ConstrIDSet)
u0 <- GenericSolverM m v -> Int -> m (Maybe (v, ConstrIDSet))
forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> Int -> m (Bound v)
getUB GenericSolverM m v
solver Int
x
  case (Maybe (v, ConstrIDSet)
l0,Maybe (v, ConstrIDSet)
u0) of
    (Just (v
l0', ConstrIDSet
_), Maybe (v, ConstrIDSet)
_) | v
l v -> v -> Bool
forall a. Ord a => a -> a -> Bool
<= v
l0' -> () -> m ()
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    (Maybe (v, ConstrIDSet)
_, Just (v
u0', ConstrIDSet
cidSet2)) | v
u0' v -> v -> Bool
forall a. Ord a => a -> a -> Bool
< v
l -> do
      GenericSolverM m v -> ConstrIDSet -> m ()
forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> ConstrIDSet -> m ()
setExplanation GenericSolverM m v
solver (ConstrIDSet -> m ()) -> ConstrIDSet -> m ()
forall a b. (a -> b) -> a -> b
$ ConstrIDSet
cidSet ConstrIDSet -> ConstrIDSet -> ConstrIDSet
`IntSet.union` ConstrIDSet
cidSet2
    (Maybe (v, ConstrIDSet), Maybe (v, ConstrIDSet))
_ -> do
      GenericSolverM m v -> Int -> m ()
forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> Int -> m ()
bpSaveLB GenericSolverM m v
solver Int
x
      MutVar (PrimState m) (IntMap (v, ConstrIDSet))
-> (IntMap (v, ConstrIDSet) -> IntMap (v, ConstrIDSet)) -> m ()
forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> (a -> a) -> m ()
modifyMutVar (GenericSolverM m v
-> MutVar (PrimState m) (IntMap (v, ConstrIDSet))
forall (m :: * -> *) v.
GenericSolverM m v
-> MutVar (PrimState m) (IntMap (v, ConstrIDSet))
svLB GenericSolverM m v
solver) (Int
-> (v, ConstrIDSet)
-> IntMap (v, ConstrIDSet)
-> IntMap (v, ConstrIDSet)
forall a. Int -> a -> IntMap a -> IntMap a
IntMap.insert Int
x (v
l, ConstrIDSet
cidSet))
      Bool
b <- GenericSolverM m v -> Int -> m Bool
forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> Int -> m Bool
isNonBasicVariable GenericSolverM m v
solver Int
x
      v
v <- GenericSolverM m v -> Int -> m v
forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> Int -> m v
getValue GenericSolverM m v
solver Int
x
      Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool
b Bool -> Bool -> Bool
&& Bool -> Bool
not (v
l v -> v -> Bool
forall a. Ord a => a -> a -> Bool
<= v
v)) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ GenericSolverM m v -> Int -> v -> m ()
forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> Int -> v -> m ()
update GenericSolverM m v
solver Int
x v
l
      GenericSolverM m v -> m ()
forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> m ()
checkNBFeasibility GenericSolverM m v
solver

assertUpper :: (PrimMonad m, SolverValue v) => GenericSolverM m v -> Var -> v -> m ()
assertUpper :: forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> Int -> v -> m ()
assertUpper GenericSolverM m v
solver Int
x v
u = GenericSolverM m v -> Int -> Bound v -> m ()
forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> Int -> Bound v -> m ()
assertUB GenericSolverM m v
solver Int
x ((v, ConstrIDSet) -> Bound v
forall a. a -> Maybe a
Just (v
u, ConstrIDSet
IntSet.empty))

assertUpper' :: (PrimMonad m, SolverValue v) => GenericSolverM m v -> Var -> v -> Maybe ConstrID -> m ()
assertUpper' :: forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> Int -> v -> Maybe Int -> m ()
assertUpper' GenericSolverM m v
solver Int
x v
u Maybe Int
cid = GenericSolverM m v -> Int -> Bound v -> m ()
forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> Int -> Bound v -> m ()
assertUB GenericSolverM m v
solver Int
x ((v, ConstrIDSet) -> Bound v
forall a. a -> Maybe a
Just (v
u, [Int] -> ConstrIDSet
IntSet.fromList (Maybe Int -> [Int]
forall a. Maybe a -> [a]
maybeToList Maybe Int
cid)))

assertUB :: (PrimMonad m, SolverValue v) => GenericSolverM m v -> Var -> Bound v -> m ()
assertUB :: forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> Int -> Bound v -> m ()
assertUB GenericSolverM m v
solver Int
x Maybe (v, ConstrIDSet)
Nothing = () -> m ()
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
assertUB GenericSolverM m v
solver Int
x (Just (v
u, ConstrIDSet
cidSet)) = do
  Maybe (v, ConstrIDSet)
l0 <- GenericSolverM m v -> Int -> m (Maybe (v, ConstrIDSet))
forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> Int -> m (Bound v)
getLB GenericSolverM m v
solver Int
x
  Maybe (v, ConstrIDSet)
u0 <- GenericSolverM m v -> Int -> m (Maybe (v, ConstrIDSet))
forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> Int -> m (Bound v)
getUB GenericSolverM m v
solver Int
x
  case (Maybe (v, ConstrIDSet)
l0,Maybe (v, ConstrIDSet)
u0) of
    (Maybe (v, ConstrIDSet)
_, Just (v
u0', ConstrIDSet
_)) | v
u0' v -> v -> Bool
forall a. Ord a => a -> a -> Bool
<= v
u -> () -> m ()
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    (Just (v
l0', ConstrIDSet
cidSet2), Maybe (v, ConstrIDSet)
_) | v
u v -> v -> Bool
forall a. Ord a => a -> a -> Bool
< v
l0' -> do
      GenericSolverM m v -> ConstrIDSet -> m ()
forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> ConstrIDSet -> m ()
setExplanation GenericSolverM m v
solver (ConstrIDSet -> m ()) -> ConstrIDSet -> m ()
forall a b. (a -> b) -> a -> b
$ ConstrIDSet
cidSet ConstrIDSet -> ConstrIDSet -> ConstrIDSet
`IntSet.union` ConstrIDSet
cidSet2
    (Maybe (v, ConstrIDSet), Maybe (v, ConstrIDSet))
_ -> do
      GenericSolverM m v -> Int -> m ()
forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> Int -> m ()
bpSaveUB GenericSolverM m v
solver Int
x
      MutVar (PrimState m) (IntMap (v, ConstrIDSet))
-> (IntMap (v, ConstrIDSet) -> IntMap (v, ConstrIDSet)) -> m ()
forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> (a -> a) -> m ()
modifyMutVar (GenericSolverM m v
-> MutVar (PrimState m) (IntMap (v, ConstrIDSet))
forall (m :: * -> *) v.
GenericSolverM m v
-> MutVar (PrimState m) (IntMap (v, ConstrIDSet))
svUB GenericSolverM m v
solver) (Int
-> (v, ConstrIDSet)
-> IntMap (v, ConstrIDSet)
-> IntMap (v, ConstrIDSet)
forall a. Int -> a -> IntMap a -> IntMap a
IntMap.insert Int
x (v
u, ConstrIDSet
cidSet))
      Bool
b <- GenericSolverM m v -> Int -> m Bool
forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> Int -> m Bool
isNonBasicVariable GenericSolverM m v
solver Int
x
      v
v <- GenericSolverM m v -> Int -> m v
forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> Int -> m v
getValue GenericSolverM m v
solver Int
x
      Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool
b Bool -> Bool -> Bool
&& Bool -> Bool
not (v
v v -> v -> Bool
forall a. Ord a => a -> a -> Bool
<= v
u)) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ GenericSolverM m v -> Int -> v -> m ()
forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> Int -> v -> m ()
update GenericSolverM m v
solver Int
x v
u
      GenericSolverM m v -> m ()
forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> m ()
checkNBFeasibility GenericSolverM m v
solver

-- FIXME: 式に定数項が含まれる可能性を考えるとこれじゃまずい?
setObj :: (PrimMonad m, SolverValue v) => GenericSolverM m v -> LA.Expr Rational -> m ()
setObj :: forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> Expr Rational -> m ()
setObj GenericSolverM m v
solver Expr Rational
e = GenericSolverM m v -> Int -> Expr Rational -> m ()
forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> Int -> Expr Rational -> m ()
setRow GenericSolverM m v
solver Int
objVar Expr Rational
e

getObj :: (PrimMonad m, SolverValue v) => GenericSolverM m v -> m (LA.Expr Rational)
getObj :: forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> m (Expr Rational)
getObj GenericSolverM m v
solver = GenericSolverM m v -> Int -> m (Expr Rational)
forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> Int -> m (Expr Rational)
getRow GenericSolverM m v
solver Int
objVar

setRow :: (PrimMonad m, SolverValue v) => GenericSolverM m v -> Var -> LA.Expr Rational -> m ()
setRow :: forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> Int -> Expr Rational -> m ()
setRow GenericSolverM m v
solver Int
v Expr Rational
e = do
  MutVar (PrimState m) (IntMap (Expr Rational))
-> (IntMap (Expr Rational) -> IntMap (Expr Rational)) -> m ()
forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> (a -> a) -> m ()
modifyMutVar (GenericSolverM m v -> MutVar (PrimState m) (IntMap (Expr Rational))
forall (m :: * -> *) v.
GenericSolverM m v -> MutVar (PrimState m) (IntMap (Expr Rational))
svTableau GenericSolverM m v
solver) ((IntMap (Expr Rational) -> IntMap (Expr Rational)) -> m ())
-> (IntMap (Expr Rational) -> IntMap (Expr Rational)) -> m ()
forall a b. (a -> b) -> a -> b
$ \IntMap (Expr Rational)
t ->
    Int
-> Expr Rational
-> IntMap (Expr Rational)
-> IntMap (Expr Rational)
forall a. Int -> a -> IntMap a -> IntMap a
IntMap.insert Int
v (IntMap (Expr Rational) -> Expr Rational -> Expr Rational
forall r. (Num r, Eq r) => VarMap (Expr r) -> Expr r -> Expr r
LA.applySubst IntMap (Expr Rational)
t Expr Rational
e) IntMap (Expr Rational)
t
  MutVar (PrimState m) (IntMap v) -> (IntMap v -> IntMap v) -> m ()
forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> (a -> a) -> m ()
modifyMutVar (GenericSolverM m v -> MutVar (PrimState m) (IntMap v)
forall (m :: * -> *) v.
GenericSolverM m v -> MutVar (PrimState m) (IntMap v)
svModel GenericSolverM m v
solver) ((IntMap v -> IntMap v) -> m ()) -> (IntMap v -> IntMap v) -> m ()
forall a b. (a -> b) -> a -> b
$ \IntMap v
m ->
    Int -> v -> IntMap v -> IntMap v
forall a. Int -> a -> IntMap a -> IntMap a
IntMap.insert Int
v (IntMap v -> v -> Expr (Scalar v) -> v
forall a. VectorSpace a => Model a -> a -> Expr (Scalar a) -> a
LA.evalLinear IntMap v
m (Rational -> v
forall v. SolverValue v => Rational -> v
toValue Rational
1) Expr Rational
Expr (Scalar v)
e) IntMap v
m

setOptDir :: PrimMonad m => GenericSolverM m v -> OptDir -> m ()
setOptDir :: forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> OptDir -> m ()
setOptDir GenericSolverM m v
solver OptDir
dir = MutVar (PrimState m) OptDir -> OptDir -> m ()
forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> a -> m ()
writeMutVar (GenericSolverM m v -> MutVar (PrimState m) OptDir
forall (m :: * -> *) v.
GenericSolverM m v -> MutVar (PrimState m) OptDir
svOptDir GenericSolverM m v
solver) OptDir
dir

getOptDir :: PrimMonad m => GenericSolverM m v -> m OptDir
getOptDir :: forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> m OptDir
getOptDir GenericSolverM m v
solver = MutVar (PrimState m) OptDir -> m OptDir
forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> m a
readMutVar (GenericSolverM m v -> MutVar (PrimState m) OptDir
forall (m :: * -> *) v.
GenericSolverM m v -> MutVar (PrimState m) OptDir
svOptDir GenericSolverM m v
solver)

{--------------------------------------------------------------------
  Status
--------------------------------------------------------------------}

nVars :: PrimMonad m => GenericSolverM m v -> m Int
nVars :: forall (m :: * -> *) v. PrimMonad m => GenericSolverM m v -> m Int
nVars GenericSolverM m v
solver = MutVar (PrimState m) Int -> m Int
forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> m a
readMutVar (GenericSolverM m v -> MutVar (PrimState m) Int
forall (m :: * -> *) v.
GenericSolverM m v -> MutVar (PrimState m) Int
svVCnt GenericSolverM m v
solver)

isBasicVariable :: PrimMonad m => GenericSolverM m v -> Var -> m Bool
isBasicVariable :: forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> Int -> m Bool
isBasicVariable GenericSolverM m v
solver Int
v = do
  IntMap (Expr Rational)
t <- MutVar (PrimState m) (IntMap (Expr Rational))
-> m (IntMap (Expr Rational))
forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> m a
readMutVar (GenericSolverM m v -> MutVar (PrimState m) (IntMap (Expr Rational))
forall (m :: * -> *) v.
GenericSolverM m v -> MutVar (PrimState m) (IntMap (Expr Rational))
svTableau GenericSolverM m v
solver)
  Bool -> m Bool
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> m Bool) -> Bool -> m Bool
forall a b. (a -> b) -> a -> b
$ Int
v Int -> IntMap (Expr Rational) -> Bool
forall a. Int -> IntMap a -> Bool
`IntMap.member` IntMap (Expr Rational)
t

isNonBasicVariable  :: PrimMonad m => GenericSolverM m v -> Var -> m Bool
isNonBasicVariable :: forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> Int -> m Bool
isNonBasicVariable GenericSolverM m v
solver Int
x = (Bool -> Bool) -> m Bool -> m Bool
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM Bool -> Bool
not (GenericSolverM m v -> Int -> m Bool
forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> Int -> m Bool
isBasicVariable GenericSolverM m v
solver Int
x)

isFeasible :: (PrimMonad m, SolverValue v) => GenericSolverM m v -> m Bool
isFeasible :: forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> m Bool
isFeasible GenericSolverM m v
solver = do
  [Int]
xs <- GenericSolverM m v -> m [Int]
forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> m [Int]
variables GenericSolverM m v
solver
  ([Bool] -> Bool) -> m [Bool] -> m Bool
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and (m [Bool] -> m Bool) -> m [Bool] -> m Bool
forall a b. (a -> b) -> a -> b
$ [Int] -> (Int -> m Bool) -> m [Bool]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [Int]
xs ((Int -> m Bool) -> m [Bool]) -> (Int -> m Bool) -> m [Bool]
forall a b. (a -> b) -> a -> b
$ \Int
x -> do
    v
v <- GenericSolverM m v -> Int -> m v
forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> Int -> m v
getValue GenericSolverM m v
solver Int
x
    Bound v
l <- GenericSolverM m v -> Int -> m (Bound v)
forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> Int -> m (Bound v)
getLB GenericSolverM m v
solver Int
x
    Bound v
u <- GenericSolverM m v -> Int -> m (Bound v)
forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> Int -> m (Bound v)
getUB GenericSolverM m v
solver Int
x
    Bool -> m Bool
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bound v -> v -> Bool
forall v. SolverValue v => Bound v -> v -> Bool
testLB Bound v
l v
v Bool -> Bool -> Bool
&& Bound v -> v -> Bool
forall v. SolverValue v => Bound v -> v -> Bool
testUB Bound v
u v
v)

isOptimal :: (PrimMonad m, SolverValue v) => GenericSolverM m v -> m Bool
isOptimal :: forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> m Bool
isOptimal GenericSolverM m v
solver = do
  Expr Rational
obj <- GenericSolverM m v -> Int -> m (Expr Rational)
forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> Int -> m (Expr Rational)
getRow GenericSolverM m v
solver Int
objVar
  Maybe (Rational, Int)
ret <- GenericSolverM m v -> m (Maybe (Rational, Int))
forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> m (Maybe (Rational, Int))
selectEnteringVariable GenericSolverM m v
solver
  Bool -> m Bool
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> m Bool) -> Bool -> m Bool
forall a b. (a -> b) -> a -> b
$! Maybe (Rational, Int) -> Bool
forall a. Maybe a -> Bool
isNothing Maybe (Rational, Int)
ret

{--------------------------------------------------------------------
  Satisfiability solving
--------------------------------------------------------------------}

check :: forall m v. (PrimMonad m, SolverValue v) => GenericSolverM m v -> m Bool
check :: forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> m Bool
check GenericSolverM m v
solver = do
  let
    loop :: m Bool
    loop :: m Bool
loop = do
      Maybe Int
m <- GenericSolverM m v -> m (Maybe Int)
forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> m (Maybe Int)
selectViolatingBasicVariable GenericSolverM m v
solver

      case Maybe Int
m of
        Maybe Int
Nothing -> Bool -> m Bool
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
        Just Int
xi  -> do
          Bound v
li <- GenericSolverM m v -> Int -> m (Bound v)
forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> Int -> m (Bound v)
getLB GenericSolverM m v
solver Int
xi
          Bound v
ui <- GenericSolverM m v -> Int -> m (Bound v)
forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> Int -> m (Bound v)
getUB GenericSolverM m v
solver Int
xi
          Bool
isLBViolated <- do
            v
vi <- GenericSolverM m v -> Int -> m v
forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> Int -> m v
getValue GenericSolverM m v
solver Int
xi
            Bool -> m Bool
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> m Bool) -> Bool -> m Bool
forall a b. (a -> b) -> a -> b
$ Bool -> Bool
not (Bound v -> v -> Bool
forall v. SolverValue v => Bound v -> v -> Bool
testLB Bound v
li v
vi)
          let q :: (Rational, Int) -> m Bool
q = if Bool
isLBViolated
                  then -- select the smallest non-basic variable xj such that
                       -- (aij > 0 and β(xj) < uj) or (aij < 0 and β(xj) > lj)
                       GenericSolverM m v -> (Rational, Int) -> m Bool
forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> (Rational, Int) -> m Bool
canIncrease GenericSolverM m v
solver
                  else -- select the smallest non-basic variable xj such that
                       -- (aij < 0 and β(xj) < uj) or (aij > 0 and β(xj) > lj)
                       GenericSolverM m v -> (Rational, Int) -> m Bool
forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> (Rational, Int) -> m Bool
canDecrease GenericSolverM m v
solver
          Expr Rational
xi_def <- GenericSolverM m v -> Int -> m (Expr Rational)
forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> Int -> m (Expr Rational)
getRow GenericSolverM m v
solver Int
xi
          Maybe Int
r <- (Maybe (Rational, Int) -> Maybe Int)
-> m (Maybe (Rational, Int)) -> m (Maybe Int)
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (((Rational, Int) -> Int) -> Maybe (Rational, Int) -> Maybe Int
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Rational, Int) -> Int
forall a b. (a, b) -> b
snd) (m (Maybe (Rational, Int)) -> m (Maybe Int))
-> m (Maybe (Rational, Int)) -> m (Maybe Int)
forall a b. (a -> b) -> a -> b
$ ((Rational, Int) -> m Bool)
-> [(Rational, Int)] -> m (Maybe (Rational, Int))
forall (m :: * -> *) a.
Monad m =>
(a -> m Bool) -> [a] -> m (Maybe a)
findM (Rational, Int) -> m Bool
q (Expr Rational -> [(Rational, Int)]
forall r. Expr r -> [(r, Int)]
LA.terms Expr Rational
xi_def)
          case Maybe Int
r of
            Maybe Int
Nothing -> do
              let c :: Bound v
c = if Bool
isLBViolated then Bound v
li else Bound v
ui
              ConstrIDSet
core <- ([Bound v] -> ConstrIDSet) -> m [Bound v] -> m ConstrIDSet
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM ([ConstrIDSet] -> ConstrIDSet
forall a. Monoid a => [a] -> a
mconcat ([ConstrIDSet] -> ConstrIDSet)
-> ([Bound v] -> [ConstrIDSet]) -> [Bound v] -> ConstrIDSet
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Bound v -> ConstrIDSet) -> [Bound v] -> [ConstrIDSet]
forall a b. (a -> b) -> [a] -> [b]
map Bound v -> ConstrIDSet
forall v. SolverValue v => Bound v -> ConstrIDSet
boundExplanation ([Bound v] -> [ConstrIDSet])
-> ([Bound v] -> [Bound v]) -> [Bound v] -> [ConstrIDSet]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Bound v
c Bound v -> [Bound v] -> [Bound v]
forall a. a -> [a] -> [a]
:)) (m [Bound v] -> m ConstrIDSet) -> m [Bound v] -> m ConstrIDSet
forall a b. (a -> b) -> a -> b
$ [(Rational, Int)]
-> ((Rational, Int) -> m (Bound v)) -> m [Bound v]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (Expr Rational -> [(Rational, Int)]
forall r. Expr r -> [(r, Int)]
LA.terms Expr Rational
xi_def) (((Rational, Int) -> m (Bound v)) -> m [Bound v])
-> ((Rational, Int) -> m (Bound v)) -> m [Bound v]
forall a b. (a -> b) -> a -> b
$ \(Rational
aij, Int
xj) -> do
                if Bool
isLBViolated then do
                  if Rational
aij Rational -> Rational -> Bool
forall a. Ord a => a -> a -> Bool
> Rational
0 then do
                    GenericSolverM m v -> Int -> m (Bound v)
forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> Int -> m (Bound v)
getUB GenericSolverM m v
solver Int
xj
                  else do
                    GenericSolverM m v -> Int -> m (Bound v)
forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> Int -> m (Bound v)
getLB GenericSolverM m v
solver Int
xj
                else do
                  if Rational
aij Rational -> Rational -> Bool
forall a. Ord a => a -> a -> Bool
> Rational
0 then do
                    GenericSolverM m v -> Int -> m (Bound v)
forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> Int -> m (Bound v)
getLB GenericSolverM m v
solver Int
xj
                  else do
                    GenericSolverM m v -> Int -> m (Bound v)
forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> Int -> m (Bound v)
getUB GenericSolverM m v
solver Int
xj
              GenericSolverM m v -> ConstrIDSet -> m ()
forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> ConstrIDSet -> m ()
setExplanation GenericSolverM m v
solver ConstrIDSet
core
              Bool -> m Bool
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
            Just Int
xj -> do
              GenericSolverM m v -> Int -> Int -> v -> m ()
forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> Int -> Int -> v -> m ()
pivotAndUpdate GenericSolverM m v
solver Int
xi Int
xj (Maybe v -> v
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe v -> v) -> Maybe v -> v
forall a b. (a -> b) -> a -> b
$ Bound v -> Maybe v
forall v. SolverValue v => Bound v -> Maybe v
boundValue (Bound v -> Maybe v) -> Bound v -> Maybe v
forall a b. (a -> b) -> a -> b
$ if Bool
isLBViolated then Bound v
li else Bound v
ui)
              Maybe ConstrIDSet
m <- MutVar (PrimState m) (Maybe ConstrIDSet) -> m (Maybe ConstrIDSet)
forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> m a
readMutVar (GenericSolverM m v -> MutVar (PrimState m) (Maybe ConstrIDSet)
forall (m :: * -> *) v.
GenericSolverM m v -> MutVar (PrimState m) (Maybe ConstrIDSet)
svExplanation GenericSolverM m v
solver)
              if Maybe ConstrIDSet -> Bool
forall a. Maybe a -> Bool
isJust Maybe ConstrIDSet
m then
                Bool -> m Bool
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
              else
                m Bool
loop

  Maybe ConstrIDSet
m <- MutVar (PrimState m) (Maybe ConstrIDSet) -> m (Maybe ConstrIDSet)
forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> m a
readMutVar (GenericSolverM m v -> MutVar (PrimState m) (Maybe ConstrIDSet)
forall (m :: * -> *) v.
GenericSolverM m v -> MutVar (PrimState m) (Maybe ConstrIDSet)
svExplanation GenericSolverM m v
solver)
  case Maybe ConstrIDSet
m of
    Just ConstrIDSet
_ -> Bool -> m Bool
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
    Maybe ConstrIDSet
Nothing -> do
      GenericSolverM m v -> String -> m ()
forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> String -> m ()
log GenericSolverM m v
solver String
"check"
      Bool
result <- GenericSolverM m v -> m Bool -> m Bool
forall (m :: * -> *) v a.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> m a -> m a
recordTime GenericSolverM m v
solver m Bool
loop
      Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
result (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ GenericSolverM m v -> m ()
forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> m ()
checkFeasibility GenericSolverM m v
solver
      Bool -> m Bool
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
result

selectViolatingBasicVariable :: forall m v. (PrimMonad m, SolverValue v) => GenericSolverM m v -> m (Maybe Var)
selectViolatingBasicVariable :: forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> m (Maybe Int)
selectViolatingBasicVariable GenericSolverM m v
solver = do
  let
    p :: Var -> m Bool
    p :: Int -> m Bool
p Int
x | Int
x Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
objVar = Bool -> m Bool
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
    p Int
xi = do
      Bound v
li <- GenericSolverM m v -> Int -> m (Bound v)
forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> Int -> m (Bound v)
getLB GenericSolverM m v
solver Int
xi
      Bound v
ui <- GenericSolverM m v -> Int -> m (Bound v)
forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> Int -> m (Bound v)
getUB GenericSolverM m v
solver Int
xi
      v
vi <- GenericSolverM m v -> Int -> m v
forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> Int -> m v
getValue GenericSolverM m v
solver Int
xi
      Bool -> m Bool
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> m Bool) -> Bool -> m Bool
forall a b. (a -> b) -> a -> b
$ Bool -> Bool
not (Bound v -> v -> Bool
forall v. SolverValue v => Bound v -> v -> Bool
testLB Bound v
li v
vi) Bool -> Bool -> Bool
|| Bool -> Bool
not (Bound v -> v -> Bool
forall v. SolverValue v => Bound v -> v -> Bool
testUB Bound v
ui v
vi)
  [Int]
vs <- GenericSolverM m v -> m [Int]
forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> m [Int]
basicVariables GenericSolverM m v
solver

  Config
config <- GenericSolverM m v -> m Config
forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> m Config
getConfig GenericSolverM m v
solver
  case Config -> PivotStrategy
configPivotStrategy Config
config of
    PivotStrategy
PivotStrategyBlandRule ->
      (Int -> m Bool) -> [Int] -> m (Maybe Int)
forall (m :: * -> *) a.
Monad m =>
(a -> m Bool) -> [a] -> m (Maybe a)
findM Int -> m Bool
p [Int]
vs
    PivotStrategy
PivotStrategyLargestCoefficient -> do
      [Int]
xs <- (Int -> m Bool) -> [Int] -> m [Int]
forall (m :: * -> *) a.
Applicative m =>
(a -> m Bool) -> [a] -> m [a]
filterM Int -> m Bool
p [Int]
vs
      case [Int]
xs of
        [] -> Maybe Int -> m (Maybe Int)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Int
forall a. Maybe a
Nothing
        [Int]
_ -> do
          [(Int, v)]
xs2 <- [Int] -> (Int -> m (Int, v)) -> m [(Int, v)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [Int]
xs ((Int -> m (Int, v)) -> m [(Int, v)])
-> (Int -> m (Int, v)) -> m [(Int, v)]
forall a b. (a -> b) -> a -> b
$ \Int
xi -> do
              v
vi <- GenericSolverM m v -> Int -> m v
forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> Int -> m v
getValue GenericSolverM m v
solver Int
xi
              Bound v
li <- GenericSolverM m v -> Int -> m (Bound v)
forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> Int -> m (Bound v)
getLB GenericSolverM m v
solver Int
xi
              Bound v
ui <- GenericSolverM m v -> Int -> m (Bound v)
forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> Int -> m (Bound v)
getUB GenericSolverM m v
solver Int
xi
              if Bool -> Bool
not (Bound v -> v -> Bool
forall v. SolverValue v => Bound v -> v -> Bool
testLB Bound v
li v
vi)
                then (Int, v) -> m (Int, v)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Int
xi, Maybe v -> v
forall a. HasCallStack => Maybe a -> a
fromJust (Bound v -> Maybe v
forall v. SolverValue v => Bound v -> Maybe v
boundValue Bound v
li) v -> v -> v
forall v. AdditiveGroup v => v -> v -> v
^-^ v
vi)
                else (Int, v) -> m (Int, v)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Int
xi, v
vi v -> v -> v
forall v. AdditiveGroup v => v -> v -> v
^-^ Maybe v -> v
forall a. HasCallStack => Maybe a -> a
fromJust (Bound v -> Maybe v
forall v. SolverValue v => Bound v -> Maybe v
boundValue Bound v
ui))
          Maybe Int -> m (Maybe Int)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Int -> m (Maybe Int)) -> Maybe Int -> m (Maybe Int)
forall a b. (a -> b) -> a -> b
$ Int -> Maybe Int
forall a. a -> Maybe a
Just (Int -> Maybe Int) -> Int -> Maybe Int
forall a b. (a -> b) -> a -> b
$ (Int, v) -> Int
forall a b. (a, b) -> a
fst ((Int, v) -> Int) -> (Int, v) -> Int
forall a b. (a -> b) -> a -> b
$ ((Int, v) -> (Int, v) -> Ordering) -> [(Int, v)] -> (Int, v)
forall (t :: * -> *) a.
Foldable t =>
(a -> a -> Ordering) -> t a -> a
maximumBy (((Int, v) -> v) -> (Int, v) -> (Int, v) -> Ordering
forall a b. Ord a => (b -> a) -> b -> b -> Ordering
comparing (Int, v) -> v
forall a b. (a, b) -> b
snd) [(Int, v)]
xs2

tightenBounds :: (PrimMonad m, SolverValue v) => GenericSolverM m v -> Var -> m ()
tightenBounds :: forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> Int -> m ()
tightenBounds GenericSolverM m v
solver Int
x = do
  -- x must be basic variable
  IntMap (Expr Rational)
defs <- MutVar (PrimState m) (IntMap (Expr Rational))
-> m (IntMap (Expr Rational))
forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> m a
readMutVar (GenericSolverM m v -> MutVar (PrimState m) (IntMap (Expr Rational))
forall (m :: * -> *) v.
GenericSolverM m v -> MutVar (PrimState m) (IntMap (Expr Rational))
svTableau GenericSolverM m v
solver)
  let x_def :: Expr Rational
x_def = IntMap (Expr Rational)
defs IntMap (Expr Rational) -> Int -> Expr Rational
forall a. IntMap a -> Int -> a
IntMap.! Int
x
      f :: (Bound v, Bound v) -> (Rational, Int) -> m (Bound v, Bound v)
f (!Bound v
lb,!Bound v
ub) (Rational
c,Int
xk) = do
        if Int
LA.unitVar Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
xk then do
          (Bound v, Bound v) -> m (Bound v, Bound v)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bound v -> Bound v -> Bound v
forall v. SolverValue v => Bound v -> Bound v -> Bound v
addBound Bound v
lb ((v, ConstrIDSet) -> Bound v
forall a. a -> Maybe a
Just (Rational -> v
forall v. SolverValue v => Rational -> v
toValue Rational
c, ConstrIDSet
IntSet.empty)), Bound v -> Bound v -> Bound v
forall v. SolverValue v => Bound v -> Bound v -> Bound v
addBound Bound v
ub ((v, ConstrIDSet) -> Bound v
forall a. a -> Maybe a
Just (Rational -> v
forall v. SolverValue v => Rational -> v
toValue Rational
c, ConstrIDSet
IntSet.empty)))
        else do
          Bound v
lb_k <- GenericSolverM m v -> Int -> m (Bound v)
forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> Int -> m (Bound v)
getLB GenericSolverM m v
solver Int
xk
          Bound v
ub_k <- GenericSolverM m v -> Int -> m (Bound v)
forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> Int -> m (Bound v)
getUB GenericSolverM m v
solver Int
xk
          if Rational
c Rational -> Rational -> Bool
forall a. Ord a => a -> a -> Bool
> Rational
0 then do
            (Bound v, Bound v) -> m (Bound v, Bound v)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bound v -> Bound v -> Bound v
forall v. SolverValue v => Bound v -> Bound v -> Bound v
addBound Bound v
lb (Scalar v -> Bound v -> Bound v
forall v. SolverValue v => Scalar v -> Bound v -> Bound v
scaleBound Rational
Scalar v
c Bound v
lb_k), Bound v -> Bound v -> Bound v
forall v. SolverValue v => Bound v -> Bound v -> Bound v
addBound Bound v
ub (Scalar v -> Bound v -> Bound v
forall v. SolverValue v => Scalar v -> Bound v -> Bound v
scaleBound Rational
Scalar v
c Bound v
ub_k))
          else do
            (Bound v, Bound v) -> m (Bound v, Bound v)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bound v -> Bound v -> Bound v
forall v. SolverValue v => Bound v -> Bound v -> Bound v
addBound Bound v
lb (Scalar v -> Bound v -> Bound v
forall v. SolverValue v => Scalar v -> Bound v -> Bound v
scaleBound Rational
Scalar v
c Bound v
ub_k), Bound v -> Bound v -> Bound v
forall v. SolverValue v => Bound v -> Bound v -> Bound v
addBound Bound v
ub (Scalar v -> Bound v -> Bound v
forall v. SolverValue v => Scalar v -> Bound v -> Bound v
scaleBound Rational
Scalar v
c Bound v
lb_k))
  (Bound v
lb,Bound v
ub) <- ((Bound v, Bound v) -> (Rational, Int) -> m (Bound v, Bound v))
-> (Bound v, Bound v) -> [(Rational, Int)] -> m (Bound v, Bound v)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (Bound v, Bound v) -> (Rational, Int) -> m (Bound v, Bound v)
f ((v, ConstrIDSet) -> Bound v
forall a. a -> Maybe a
Just (v
forall v. AdditiveGroup v => v
zeroV, ConstrIDSet
IntSet.empty), (v, ConstrIDSet) -> Bound v
forall a. a -> Maybe a
Just (v
forall v. AdditiveGroup v => v
zeroV, ConstrIDSet
IntSet.empty)) (Expr Rational -> [(Rational, Int)]
forall r. Expr r -> [(r, Int)]
LA.terms Expr Rational
x_def)
  GenericSolverM m v -> Int -> Bound v -> m ()
forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> Int -> Bound v -> m ()
assertLB GenericSolverM m v
solver Int
x Bound v
lb
  GenericSolverM m v -> Int -> Bound v -> m ()
forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> Int -> Bound v -> m ()
assertUB GenericSolverM m v
solver Int
x Bound v
ub

{--------------------------------------------------------------------
  Optimization
--------------------------------------------------------------------}

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

-- | Options for solving.
--
-- The default option can be obtained by 'def'.
data Options
  = Options
  { Options -> Maybe Rational
objLimit :: Maybe Rational
  }
  deriving (Int -> Options -> ShowS
[Options] -> ShowS
Options -> String
(Int -> Options -> ShowS)
-> (Options -> String) -> ([Options] -> ShowS) -> Show Options
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Options -> ShowS
showsPrec :: Int -> Options -> ShowS
$cshow :: Options -> String
show :: Options -> String
$cshowList :: [Options] -> ShowS
showList :: [Options] -> ShowS
Show, Options -> Options -> Bool
(Options -> Options -> Bool)
-> (Options -> Options -> Bool) -> Eq Options
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Options -> Options -> Bool
== :: Options -> Options -> Bool
$c/= :: Options -> Options -> Bool
/= :: Options -> Options -> Bool
Eq, Eq Options
Eq Options =>
(Options -> Options -> Ordering)
-> (Options -> Options -> Bool)
-> (Options -> Options -> Bool)
-> (Options -> Options -> Bool)
-> (Options -> Options -> Bool)
-> (Options -> Options -> Options)
-> (Options -> Options -> Options)
-> Ord Options
Options -> Options -> Bool
Options -> Options -> Ordering
Options -> Options -> Options
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
$ccompare :: Options -> Options -> Ordering
compare :: Options -> Options -> Ordering
$c< :: Options -> Options -> Bool
< :: Options -> Options -> Bool
$c<= :: Options -> Options -> Bool
<= :: Options -> Options -> Bool
$c> :: Options -> Options -> Bool
> :: Options -> Options -> Bool
$c>= :: Options -> Options -> Bool
>= :: Options -> Options -> Bool
$cmax :: Options -> Options -> Options
max :: Options -> Options -> Options
$cmin :: Options -> Options -> Options
min :: Options -> Options -> Options
Ord)

instance Default Options where
  def :: Options
def =
    Options
    { objLimit :: Maybe Rational
objLimit = Maybe Rational
forall a. Maybe a
Nothing
    }

optimize :: forall m. PrimMonad m => GenericSolverM m Rational -> Options -> m OptResult
optimize :: forall (m :: * -> *).
PrimMonad m =>
GenericSolverM m Rational -> Options -> m OptResult
optimize GenericSolverM m Rational
solver Options
opt = do
  Bool
ret <- do
    Bool
is_fea <- GenericSolverM m Rational -> m Bool
forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> m Bool
isFeasible GenericSolverM m Rational
solver
    if Bool
is_fea then Bool -> m Bool
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True else GenericSolverM m Rational -> m Bool
forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> m Bool
check GenericSolverM m Rational
solver
  if Bool -> Bool
not Bool
ret
    then OptResult -> m OptResult
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return OptResult
Unsat -- unsat
    else do
      GenericSolverM m Rational -> String -> m ()
forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> String -> m ()
log GenericSolverM m Rational
solver String
"optimize"
      OptResult
result <- GenericSolverM m Rational -> m OptResult -> m OptResult
forall (m :: * -> *) v a.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> m a -> m a
recordTime GenericSolverM m Rational
solver m OptResult
loop
      Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (OptResult
result OptResult -> OptResult -> Bool
forall a. Eq a => a -> a -> Bool
== OptResult
Optimum) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ GenericSolverM m Rational -> m ()
forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> m ()
checkOptimality GenericSolverM m Rational
solver
      OptResult -> m OptResult
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return OptResult
result
  where
    loop :: m OptResult
    loop :: m OptResult
loop = do
      GenericSolverM m Rational -> m ()
forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> m ()
checkFeasibility GenericSolverM m Rational
solver
      Maybe (Rational, Int)
ret <- GenericSolverM m Rational -> m (Maybe (Rational, Int))
forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> m (Maybe (Rational, Int))
selectEnteringVariable GenericSolverM m Rational
solver
      case Maybe (Rational, Int)
ret of
       Maybe (Rational, Int)
Nothing -> OptResult -> m OptResult
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return OptResult
Optimum
       Just (Rational
c,Int
xj) -> do
         OptDir
dir <- GenericSolverM m Rational -> m OptDir
forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> m OptDir
getOptDir GenericSolverM m Rational
solver
         Bool
r <- if OptDir
dirOptDir -> OptDir -> Bool
forall a. Eq a => a -> a -> Bool
==OptDir
OptMin
              then if Rational
c Rational -> Rational -> Bool
forall a. Ord a => a -> a -> Bool
> Rational
0
                then GenericSolverM m Rational -> Int -> m Bool
forall (m :: * -> *).
PrimMonad m =>
GenericSolverM m Rational -> Int -> m Bool
decreaseNB GenericSolverM m Rational
solver Int
xj -- xj を小さくして目的関数を小さくする
                else GenericSolverM m Rational -> Int -> m Bool
forall (m :: * -> *).
PrimMonad m =>
GenericSolverM m Rational -> Int -> m Bool
increaseNB GenericSolverM m Rational
solver Int
xj -- xj を大きくして目的関数を小さくする
              else if Rational
c Rational -> Rational -> Bool
forall a. Ord a => a -> a -> Bool
> Rational
0
                then GenericSolverM m Rational -> Int -> m Bool
forall (m :: * -> *).
PrimMonad m =>
GenericSolverM m Rational -> Int -> m Bool
increaseNB GenericSolverM m Rational
solver Int
xj -- xj を大きくして目的関数を大きくする
                else GenericSolverM m Rational -> Int -> m Bool
forall (m :: * -> *).
PrimMonad m =>
GenericSolverM m Rational -> Int -> m Bool
decreaseNB GenericSolverM m Rational
solver Int
xj -- xj を小さくして目的関数を大きくする
         if Bool
r
           then m OptResult
loop
           else OptResult -> m OptResult
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return OptResult
Unbounded

selectEnteringVariable :: forall m v. (PrimMonad m, SolverValue v) => GenericSolverM m v -> m (Maybe (Rational, Var))
selectEnteringVariable :: forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> m (Maybe (Rational, Int))
selectEnteringVariable GenericSolverM m v
solver = do
  Config
config <- GenericSolverM m v -> m Config
forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> m Config
getConfig GenericSolverM m v
solver
  Expr Rational
obj_def <- GenericSolverM m v -> Int -> m (Expr Rational)
forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> Int -> m (Expr Rational)
getRow GenericSolverM m v
solver Int
objVar
  case Config -> PivotStrategy
configPivotStrategy Config
config of
    PivotStrategy
PivotStrategyBlandRule ->
      ((Rational, Int) -> m Bool)
-> [(Rational, Int)] -> m (Maybe (Rational, Int))
forall (m :: * -> *) a.
Monad m =>
(a -> m Bool) -> [a] -> m (Maybe a)
findM (Rational, Int) -> m Bool
canEnter (Expr Rational -> [(Rational, Int)]
forall r. Expr r -> [(r, Int)]
LA.terms Expr Rational
obj_def)
    PivotStrategy
PivotStrategyLargestCoefficient -> do
      [(Rational, Int)]
ts <- ((Rational, Int) -> m Bool)
-> [(Rational, Int)] -> m [(Rational, Int)]
forall (m :: * -> *) a.
Applicative m =>
(a -> m Bool) -> [a] -> m [a]
filterM (Rational, Int) -> m Bool
canEnter (Expr Rational -> [(Rational, Int)]
forall r. Expr r -> [(r, Int)]
LA.terms Expr Rational
obj_def)
      case [(Rational, Int)]
ts of
        [] -> Maybe (Rational, Int) -> m (Maybe (Rational, Int))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (Rational, Int)
forall a. Maybe a
Nothing
        [(Rational, Int)]
_ -> Maybe (Rational, Int) -> m (Maybe (Rational, Int))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (Rational, Int) -> m (Maybe (Rational, Int)))
-> Maybe (Rational, Int) -> m (Maybe (Rational, Int))
forall a b. (a -> b) -> a -> b
$ (Rational, Int) -> Maybe (Rational, Int)
forall a. a -> Maybe a
Just ((Rational, Int) -> Maybe (Rational, Int))
-> (Rational, Int) -> Maybe (Rational, Int)
forall a b. (a -> b) -> a -> b
$ (Rational, (Rational, Int)) -> (Rational, Int)
forall a b. (a, b) -> b
snd ((Rational, (Rational, Int)) -> (Rational, Int))
-> (Rational, (Rational, Int)) -> (Rational, Int)
forall a b. (a -> b) -> a -> b
$ ((Rational, (Rational, Int))
 -> (Rational, (Rational, Int)) -> Ordering)
-> [(Rational, (Rational, Int))] -> (Rational, (Rational, Int))
forall (t :: * -> *) a.
Foldable t =>
(a -> a -> Ordering) -> t a -> a
maximumBy (((Rational, (Rational, Int)) -> Rational)
-> (Rational, (Rational, Int))
-> (Rational, (Rational, Int))
-> Ordering
forall a b. Ord a => (b -> a) -> b -> b -> Ordering
comparing (Rational, (Rational, Int)) -> Rational
forall a b. (a, b) -> a
fst) [(Rational -> Rational
forall a. Num a => a -> a
abs Rational
c, (Rational
c,Int
xj)) | (Rational
c,Int
xj) <- [(Rational, Int)]
ts]
  where
    canEnter :: (Rational, Var) -> m Bool
    canEnter :: (Rational, Int) -> m Bool
canEnter (Rational
_,Int
xj) | Int
xj Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
LA.unitVar = Bool -> m Bool
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
    canEnter (Rational
c,Int
xj) = do
      OptDir
dir <- GenericSolverM m v -> m OptDir
forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> m OptDir
getOptDir GenericSolverM m v
solver
      if OptDir
dirOptDir -> OptDir -> Bool
forall a. Eq a => a -> a -> Bool
==OptDir
OptMin
       then GenericSolverM m v -> (Rational, Int) -> m Bool
forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> (Rational, Int) -> m Bool
canDecrease GenericSolverM m v
solver (Rational
c,Int
xj)
       else GenericSolverM m v -> (Rational, Int) -> m Bool
forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> (Rational, Int) -> m Bool
canIncrease GenericSolverM m v
solver (Rational
c,Int
xj)

canIncrease :: (PrimMonad m, SolverValue v) => GenericSolverM m v -> (Rational,Var) -> m Bool
canIncrease :: forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> (Rational, Int) -> m Bool
canIncrease GenericSolverM m v
solver (Rational
a,Int
x) =
  case Rational -> Rational -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Rational
a Rational
0 of
    Ordering
EQ -> Bool -> m Bool
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
    Ordering
GT -> GenericSolverM m v -> Int -> m Bool
forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> Int -> m Bool
canIncrease1 GenericSolverM m v
solver Int
x
    Ordering
LT -> GenericSolverM m v -> Int -> m Bool
forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> Int -> m Bool
canDecrease1 GenericSolverM m v
solver Int
x

canDecrease :: (PrimMonad m, SolverValue v) => GenericSolverM m v -> (Rational,Var) -> m Bool
canDecrease :: forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> (Rational, Int) -> m Bool
canDecrease GenericSolverM m v
solver (Rational
a,Int
x) =
  case Rational -> Rational -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Rational
a Rational
0 of
    Ordering
EQ -> Bool -> m Bool
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
    Ordering
GT -> GenericSolverM m v -> Int -> m Bool
forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> Int -> m Bool
canDecrease1 GenericSolverM m v
solver Int
x
    Ordering
LT -> GenericSolverM m v -> Int -> m Bool
forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> Int -> m Bool
canIncrease1 GenericSolverM m v
solver Int
x

canIncrease1 :: (PrimMonad m, SolverValue v) => GenericSolverM m v -> Var -> m Bool
canIncrease1 :: forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> Int -> m Bool
canIncrease1 GenericSolverM m v
solver Int
x = do
  Bound v
u <- GenericSolverM m v -> Int -> m (Bound v)
forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> Int -> m (Bound v)
getUB GenericSolverM m v
solver Int
x
  v
v <- GenericSolverM m v -> Int -> m v
forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> Int -> m v
getValue GenericSolverM m v
solver Int
x
  case Bound v
u of
    Bound v
Nothing -> Bool -> m Bool
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
    Just (v
uv, ConstrIDSet
_) -> Bool -> m Bool
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> m Bool) -> Bool -> m Bool
forall a b. (a -> b) -> a -> b
$! (v
v v -> v -> Bool
forall a. Ord a => a -> a -> Bool
< v
uv)

canDecrease1 :: (PrimMonad m, SolverValue v) => GenericSolverM m v -> Var -> m Bool
canDecrease1 :: forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> Int -> m Bool
canDecrease1 GenericSolverM m v
solver Int
x = do
  Bound v
l <- GenericSolverM m v -> Int -> m (Bound v)
forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> Int -> m (Bound v)
getLB GenericSolverM m v
solver Int
x
  v
v <- GenericSolverM m v -> Int -> m v
forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> Int -> m v
getValue GenericSolverM m v
solver Int
x
  case Bound v
l of
    Bound v
Nothing -> Bool -> m Bool
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
    Just (v
lv, ConstrIDSet
_) -> Bool -> m Bool
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> m Bool) -> Bool -> m Bool
forall a b. (a -> b) -> a -> b
$! (v
lv v -> v -> Bool
forall a. Ord a => a -> a -> Bool
< v
v)

-- | feasibility を保ちつつ non-basic variable xj の値を大きくする
increaseNB :: PrimMonad m => GenericSolverM m Rational -> Var -> m Bool
increaseNB :: forall (m :: * -> *).
PrimMonad m =>
GenericSolverM m Rational -> Int -> m Bool
increaseNB GenericSolverM m Rational
solver Int
xj = do
  Model
col <- GenericSolverM m Rational -> Int -> m Model
forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> Int -> m Model
getCol GenericSolverM m Rational
solver Int
xj

  -- Upper bounds of θ
  -- NOTE: xj 自体の上限も考慮するのに注意
  [((Int, Rational), Rational)]
ubs <- ([[((Int, Rational), Rational)]] -> [((Int, Rational), Rational)])
-> m [[((Int, Rational), Rational)]]
-> m [((Int, Rational), Rational)]
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM [[((Int, Rational), Rational)]] -> [((Int, Rational), Rational)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (m [[((Int, Rational), Rational)]]
 -> m [((Int, Rational), Rational)])
-> m [[((Int, Rational), Rational)]]
-> m [((Int, Rational), Rational)]
forall a b. (a -> b) -> a -> b
$ [(Int, Rational)]
-> ((Int, Rational) -> m [((Int, Rational), Rational)])
-> m [[((Int, Rational), Rational)]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM ((Int
xj,Rational
1) (Int, Rational) -> [(Int, Rational)] -> [(Int, Rational)]
forall a. a -> [a] -> [a]
: Model -> [(Int, Rational)]
forall a. IntMap a -> [(Int, a)]
IntMap.toList Model
col) (((Int, Rational) -> m [((Int, Rational), Rational)])
 -> m [[((Int, Rational), Rational)]])
-> ((Int, Rational) -> m [((Int, Rational), Rational)])
-> m [[((Int, Rational), Rational)]]
forall a b. (a -> b) -> a -> b
$ \(Int
xi,Rational
aij) -> do
    Rational
v1 <- GenericSolverM m Rational -> Int -> m Rational
forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> Int -> m v
getValue GenericSolverM m Rational
solver Int
xi
    Bound Rational
li <- GenericSolverM m Rational -> Int -> m (Bound Rational)
forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> Int -> m (Bound v)
getLB GenericSolverM m Rational
solver Int
xi
    Bound Rational
ui <- GenericSolverM m Rational -> Int -> m (Bound Rational)
forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> Int -> m (Bound v)
getUB GenericSolverM m Rational
solver Int
xi
    [((Int, Rational), Rational)] -> m [((Int, Rational), Rational)]
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return [ Bool -> ((Int, Rational), Rational) -> ((Int, Rational), Rational)
forall a. HasCallStack => Bool -> a -> a
assert (Rational
theta Rational -> Rational -> Bool
forall a. Ord a => a -> a -> Bool
>= Rational
forall v. AdditiveGroup v => v
zeroV) ((Int
xi,Rational
v2), Rational
theta)
           | Just Rational
v2 <- [Bound Rational -> Maybe Rational
forall v. SolverValue v => Bound v -> Maybe v
boundValue Bound Rational
ui | Rational
aij Rational -> Rational -> Bool
forall a. Ord a => a -> a -> Bool
> Rational
0] [Maybe Rational] -> [Maybe Rational] -> [Maybe Rational]
forall a. [a] -> [a] -> [a]
++ [Bound Rational -> Maybe Rational
forall v. SolverValue v => Bound v -> Maybe v
boundValue Bound Rational
li | Rational
aij Rational -> Rational -> Bool
forall a. Ord a => a -> a -> Bool
< Rational
0]
           , let theta :: Rational
theta = (Rational
v2 Rational -> Rational -> Rational
forall v. AdditiveGroup v => v -> v -> v
^-^ Rational
v1) Rational -> Rational -> Rational
forall v s.
(VectorSpace v, s ~ Scalar v, Fractional s) =>
v -> s -> v
^/ Rational
aij ]

  -- β(xj) := β(xj) + θ なので θ を大きく
  case [((Int, Rational), Rational)]
ubs of
    [] -> Bool -> m Bool
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False -- unbounded
    [((Int, Rational), Rational)]
_ -> do
      let (Int
xi, Rational
v) = ((Int, Rational), Rational) -> (Int, Rational)
forall a b. (a, b) -> a
fst (((Int, Rational), Rational) -> (Int, Rational))
-> ((Int, Rational), Rational) -> (Int, Rational)
forall a b. (a -> b) -> a -> b
$ (((Int, Rational), Rational)
 -> ((Int, Rational), Rational) -> Ordering)
-> [((Int, Rational), Rational)] -> ((Int, Rational), Rational)
forall (t :: * -> *) a.
Foldable t =>
(a -> a -> Ordering) -> t a -> a
minimumBy ((((Int, Rational), Rational) -> Rational)
-> ((Int, Rational), Rational)
-> ((Int, Rational), Rational)
-> Ordering
forall a b. Ord a => (b -> a) -> b -> b -> Ordering
comparing ((Int, Rational), Rational) -> Rational
forall a b. (a, b) -> b
snd) [((Int, Rational), Rational)]
ubs
      GenericSolverM m Rational -> Int -> Int -> Rational -> m ()
forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> Int -> Int -> v -> m ()
pivotAndUpdate GenericSolverM m Rational
solver Int
xi Int
xj Rational
v
      Bool -> m Bool
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True

-- | feasibility を保ちつつ non-basic variable xj の値を小さくする
decreaseNB :: PrimMonad m => GenericSolverM m Rational -> Var -> m Bool
decreaseNB :: forall (m :: * -> *).
PrimMonad m =>
GenericSolverM m Rational -> Int -> m Bool
decreaseNB GenericSolverM m Rational
solver Int
xj = do
  Model
col <- GenericSolverM m Rational -> Int -> m Model
forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> Int -> m Model
getCol GenericSolverM m Rational
solver Int
xj

  -- Lower bounds of θ
  -- NOTE: xj 自体の下限も考慮するのに注意
  [((Int, Rational), Rational)]
lbs <- ([[((Int, Rational), Rational)]] -> [((Int, Rational), Rational)])
-> m [[((Int, Rational), Rational)]]
-> m [((Int, Rational), Rational)]
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM [[((Int, Rational), Rational)]] -> [((Int, Rational), Rational)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (m [[((Int, Rational), Rational)]]
 -> m [((Int, Rational), Rational)])
-> m [[((Int, Rational), Rational)]]
-> m [((Int, Rational), Rational)]
forall a b. (a -> b) -> a -> b
$ [(Int, Rational)]
-> ((Int, Rational) -> m [((Int, Rational), Rational)])
-> m [[((Int, Rational), Rational)]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM ((Int
xj,Rational
1) (Int, Rational) -> [(Int, Rational)] -> [(Int, Rational)]
forall a. a -> [a] -> [a]
: Model -> [(Int, Rational)]
forall a. IntMap a -> [(Int, a)]
IntMap.toList Model
col) (((Int, Rational) -> m [((Int, Rational), Rational)])
 -> m [[((Int, Rational), Rational)]])
-> ((Int, Rational) -> m [((Int, Rational), Rational)])
-> m [[((Int, Rational), Rational)]]
forall a b. (a -> b) -> a -> b
$ \(Int
xi,Rational
aij) -> do
    Rational
v1 <- GenericSolverM m Rational -> Int -> m Rational
forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> Int -> m v
getValue GenericSolverM m Rational
solver Int
xi
    Bound Rational
li <- GenericSolverM m Rational -> Int -> m (Bound Rational)
forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> Int -> m (Bound v)
getLB GenericSolverM m Rational
solver Int
xi
    Bound Rational
ui <- GenericSolverM m Rational -> Int -> m (Bound Rational)
forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> Int -> m (Bound v)
getUB GenericSolverM m Rational
solver Int
xi
    [((Int, Rational), Rational)] -> m [((Int, Rational), Rational)]
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return [ Bool -> ((Int, Rational), Rational) -> ((Int, Rational), Rational)
forall a. HasCallStack => Bool -> a -> a
assert (Rational
theta Rational -> Rational -> Bool
forall a. Ord a => a -> a -> Bool
<= Rational
forall v. AdditiveGroup v => v
zeroV) ((Int
xi,Rational
v2), Rational
theta)
           | Just Rational
v2 <- [Bound Rational -> Maybe Rational
forall v. SolverValue v => Bound v -> Maybe v
boundValue Bound Rational
li | Rational
aij Rational -> Rational -> Bool
forall a. Ord a => a -> a -> Bool
> Rational
0] [Maybe Rational] -> [Maybe Rational] -> [Maybe Rational]
forall a. [a] -> [a] -> [a]
++ [Bound Rational -> Maybe Rational
forall v. SolverValue v => Bound v -> Maybe v
boundValue Bound Rational
ui | Rational
aij Rational -> Rational -> Bool
forall a. Ord a => a -> a -> Bool
< Rational
0]
           , let theta :: Rational
theta = (Rational
v2 Rational -> Rational -> Rational
forall v. AdditiveGroup v => v -> v -> v
^-^ Rational
v1) Rational -> Rational -> Rational
forall v s.
(VectorSpace v, s ~ Scalar v, Fractional s) =>
v -> s -> v
^/ Rational
aij ]

  -- β(xj) := β(xj) + θ なので θ を小さく
  case [((Int, Rational), Rational)]
lbs of
    [] -> Bool -> m Bool
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False -- unbounded
    [((Int, Rational), Rational)]
_ -> do
      let (Int
xi, Rational
v) = ((Int, Rational), Rational) -> (Int, Rational)
forall a b. (a, b) -> a
fst (((Int, Rational), Rational) -> (Int, Rational))
-> ((Int, Rational), Rational) -> (Int, Rational)
forall a b. (a -> b) -> a -> b
$ (((Int, Rational), Rational)
 -> ((Int, Rational), Rational) -> Ordering)
-> [((Int, Rational), Rational)] -> ((Int, Rational), Rational)
forall (t :: * -> *) a.
Foldable t =>
(a -> a -> Ordering) -> t a -> a
maximumBy ((((Int, Rational), Rational) -> Rational)
-> ((Int, Rational), Rational)
-> ((Int, Rational), Rational)
-> Ordering
forall a b. Ord a => (b -> a) -> b -> b -> Ordering
comparing ((Int, Rational), Rational) -> Rational
forall a b. (a, b) -> b
snd) [((Int, Rational), Rational)]
lbs
      GenericSolverM m Rational -> Int -> Int -> Rational -> m ()
forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> Int -> Int -> v -> m ()
pivotAndUpdate GenericSolverM m Rational
solver Int
xi Int
xj Rational
v
      Bool -> m Bool
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True

dualSimplex :: forall m. PrimMonad m => GenericSolverM m Rational -> Options -> m OptResult
dualSimplex :: forall (m :: * -> *).
PrimMonad m =>
GenericSolverM m Rational -> Options -> m OptResult
dualSimplex GenericSolverM m Rational
solver Options
opt = do
  let
    loop :: m OptResult
    loop :: m OptResult
loop = do
      GenericSolverM m Rational -> m ()
forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> m ()
checkOptimality GenericSolverM m Rational
solver

      Bool
p <- GenericSolverM m Rational -> Options -> m Bool
forall (m :: * -> *).
PrimMonad m =>
GenericSolverM m Rational -> Options -> m Bool
prune GenericSolverM m Rational
solver Options
opt
      if Bool
p
        then OptResult -> m OptResult
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return OptResult
ObjLimit
        else do
          Maybe Int
m <- GenericSolverM m Rational -> m (Maybe Int)
forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> m (Maybe Int)
selectViolatingBasicVariable GenericSolverM m Rational
solver
          case Maybe Int
m of
            Maybe Int
Nothing -> OptResult -> m OptResult
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return OptResult
Optimum
            Just Int
xi  -> do
              Expr Rational
xi_def  <- GenericSolverM m Rational -> Int -> m (Expr Rational)
forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> Int -> m (Expr Rational)
getRow GenericSolverM m Rational
solver Int
xi
              Bound Rational
li <- GenericSolverM m Rational -> Int -> m (Bound Rational)
forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> Int -> m (Bound v)
getLB GenericSolverM m Rational
solver Int
xi
              Bound Rational
ui <- GenericSolverM m Rational -> Int -> m (Bound Rational)
forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> Int -> m (Bound v)
getUB GenericSolverM m Rational
solver Int
xi
              Bool
isLBViolated <- do
                Rational
vi <- GenericSolverM m Rational -> Int -> m Rational
forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> Int -> m v
getValue GenericSolverM m Rational
solver Int
xi
                Bool -> m Bool
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> m Bool) -> Bool -> m Bool
forall a b. (a -> b) -> a -> b
$ Bool -> Bool
not (Bound Rational -> Rational -> Bool
forall v. SolverValue v => Bound v -> v -> Bool
testLB Bound Rational
li Rational
vi)
              Maybe Int
r <- GenericSolverM m Rational -> Expr Rational -> Bool -> m (Maybe Int)
forall (m :: * -> *).
PrimMonad m =>
GenericSolverM m Rational -> Expr Rational -> Bool -> m (Maybe Int)
dualRTest GenericSolverM m Rational
solver Expr Rational
xi_def Bool
isLBViolated
              case Maybe Int
r of
                Maybe Int
Nothing -> do
                  -- dual unbounded
                  let c :: Bound Rational
c = if Bool
isLBViolated then Bound Rational
li else Bound Rational
ui
                  ConstrIDSet
core <- ([Bound Rational] -> ConstrIDSet)
-> m [Bound Rational] -> m ConstrIDSet
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM ([ConstrIDSet] -> ConstrIDSet
forall a. Monoid a => [a] -> a
mconcat ([ConstrIDSet] -> ConstrIDSet)
-> ([Bound Rational] -> [ConstrIDSet])
-> [Bound Rational]
-> ConstrIDSet
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Bound Rational -> ConstrIDSet)
-> [Bound Rational] -> [ConstrIDSet]
forall a b. (a -> b) -> [a] -> [b]
map Bound Rational -> ConstrIDSet
forall v. SolverValue v => Bound v -> ConstrIDSet
boundExplanation ([Bound Rational] -> [ConstrIDSet])
-> ([Bound Rational] -> [Bound Rational])
-> [Bound Rational]
-> [ConstrIDSet]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Bound Rational
c Bound Rational -> [Bound Rational] -> [Bound Rational]
forall a. a -> [a] -> [a]
:)) (m [Bound Rational] -> m ConstrIDSet)
-> m [Bound Rational] -> m ConstrIDSet
forall a b. (a -> b) -> a -> b
$ [(Rational, Int)]
-> ((Rational, Int) -> m (Bound Rational)) -> m [Bound Rational]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (Expr Rational -> [(Rational, Int)]
forall r. Expr r -> [(r, Int)]
LA.terms Expr Rational
xi_def) (((Rational, Int) -> m (Bound Rational)) -> m [Bound Rational])
-> ((Rational, Int) -> m (Bound Rational)) -> m [Bound Rational]
forall a b. (a -> b) -> a -> b
$ \(Rational
aij, Int
xj) -> do
                    if Bool
isLBViolated then do
                      if Rational
aij Rational -> Rational -> Bool
forall a. Ord a => a -> a -> Bool
> Rational
0 then do
                        GenericSolverM m Rational -> Int -> m (Bound Rational)
forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> Int -> m (Bound v)
getUB GenericSolverM m Rational
solver Int
xj
                      else do
                        GenericSolverM m Rational -> Int -> m (Bound Rational)
forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> Int -> m (Bound v)
getLB GenericSolverM m Rational
solver Int
xj
                    else do
                      if Rational
aij Rational -> Rational -> Bool
forall a. Ord a => a -> a -> Bool
> Rational
0 then do
                        GenericSolverM m Rational -> Int -> m (Bound Rational)
forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> Int -> m (Bound v)
getLB GenericSolverM m Rational
solver Int
xj
                      else do
                        GenericSolverM m Rational -> Int -> m (Bound Rational)
forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> Int -> m (Bound v)
getUB GenericSolverM m Rational
solver Int
xj
                  GenericSolverM m Rational -> ConstrIDSet -> m ()
forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> ConstrIDSet -> m ()
setExplanation GenericSolverM m Rational
solver ConstrIDSet
core
                  OptResult -> m OptResult
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return OptResult
Unsat
                Just Int
xj -> do
                  GenericSolverM m Rational -> Int -> Int -> Rational -> m ()
forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> Int -> Int -> v -> m ()
pivotAndUpdate GenericSolverM m Rational
solver Int
xi Int
xj (Maybe Rational -> Rational
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe Rational -> Rational) -> Maybe Rational -> Rational
forall a b. (a -> b) -> a -> b
$ Bound Rational -> Maybe Rational
forall v. SolverValue v => Bound v -> Maybe v
boundValue (Bound Rational -> Maybe Rational)
-> Bound Rational -> Maybe Rational
forall a b. (a -> b) -> a -> b
$ if Bool
isLBViolated then Bound Rational
li else Bound Rational
ui)
                  Maybe ConstrIDSet
m <- MutVar (PrimState m) (Maybe ConstrIDSet) -> m (Maybe ConstrIDSet)
forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> m a
readMutVar (GenericSolverM m Rational
-> MutVar (PrimState m) (Maybe ConstrIDSet)
forall (m :: * -> *) v.
GenericSolverM m v -> MutVar (PrimState m) (Maybe ConstrIDSet)
svExplanation GenericSolverM m Rational
solver)
                  if Maybe ConstrIDSet -> Bool
forall a. Maybe a -> Bool
isJust Maybe ConstrIDSet
m then
                    OptResult -> m OptResult
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return OptResult
Unsat
                  else
                    m OptResult
loop

  Maybe ConstrIDSet
m <- MutVar (PrimState m) (Maybe ConstrIDSet) -> m (Maybe ConstrIDSet)
forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> m a
readMutVar (GenericSolverM m Rational
-> MutVar (PrimState m) (Maybe ConstrIDSet)
forall (m :: * -> *) v.
GenericSolverM m v -> MutVar (PrimState m) (Maybe ConstrIDSet)
svExplanation GenericSolverM m Rational
solver)
  case Maybe ConstrIDSet
m of
    Just ConstrIDSet
_ -> OptResult -> m OptResult
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return OptResult
Unsat
    Maybe ConstrIDSet
Nothing -> do
      GenericSolverM m Rational -> String -> m ()
forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> String -> m ()
log GenericSolverM m Rational
solver String
"dual simplex"
      OptResult
result <- GenericSolverM m Rational -> m OptResult -> m OptResult
forall (m :: * -> *) v a.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> m a -> m a
recordTime GenericSolverM m Rational
solver m OptResult
loop
      Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (OptResult
result OptResult -> OptResult -> Bool
forall a. Eq a => a -> a -> Bool
== OptResult
Optimum) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ GenericSolverM m Rational -> m ()
forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> m ()
checkFeasibility GenericSolverM m Rational
solver
      OptResult -> m OptResult
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return OptResult
result

dualRTest :: PrimMonad m => GenericSolverM m Rational -> LA.Expr Rational -> Bool -> m (Maybe Var)
dualRTest :: forall (m :: * -> *).
PrimMonad m =>
GenericSolverM m Rational -> Expr Rational -> Bool -> m (Maybe Int)
dualRTest GenericSolverM m Rational
solver Expr Rational
row Bool
isLBViolated = do
  -- normalize to the cases of minimization
  Expr Rational
obj_def <- do
    Expr Rational
def <- GenericSolverM m Rational -> Int -> m (Expr Rational)
forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> Int -> m (Expr Rational)
getRow GenericSolverM m Rational
solver Int
objVar
    OptDir
dir <- GenericSolverM m Rational -> m OptDir
forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> m OptDir
getOptDir GenericSolverM m Rational
solver
    Expr Rational -> m (Expr Rational)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr Rational -> m (Expr Rational))
-> Expr Rational -> m (Expr Rational)
forall a b. (a -> b) -> a -> b
$
      case OptDir
dir of
        OptDir
OptMin -> Expr Rational
def
        OptDir
OptMax -> Expr Rational -> Expr Rational
forall v. AdditiveGroup v => v -> v
negateV Expr Rational
def
  -- normalize to the cases of lower bound violation
  let xi_def :: Expr Rational
xi_def =
       if Bool
isLBViolated
       then Expr Rational
row
       else Expr Rational -> Expr Rational
forall v. AdditiveGroup v => v -> v
negateV Expr Rational
row
  [(Int, Rational)]
ws <- do
    -- select non-basic variable xj such that
    -- (aij > 0 and β(xj) < uj) or (aij < 0 and β(xj) > lj)
    ([[(Int, Rational)]] -> [(Int, Rational)])
-> m [[(Int, Rational)]] -> m [(Int, Rational)]
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM [[(Int, Rational)]] -> [(Int, Rational)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (m [[(Int, Rational)]] -> m [(Int, Rational)])
-> m [[(Int, Rational)]] -> m [(Int, Rational)]
forall a b. (a -> b) -> a -> b
$ [(Rational, Int)]
-> ((Rational, Int) -> m [(Int, Rational)])
-> m [[(Int, Rational)]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (Expr Rational -> [(Rational, Int)]
forall r. Expr r -> [(r, Int)]
LA.terms Expr Rational
xi_def) (((Rational, Int) -> m [(Int, Rational)]) -> m [[(Int, Rational)]])
-> ((Rational, Int) -> m [(Int, Rational)])
-> m [[(Int, Rational)]]
forall a b. (a -> b) -> a -> b
$ \(Rational
aij, Int
xj) -> do
      Bool
b <- GenericSolverM m Rational -> (Rational, Int) -> m Bool
forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> (Rational, Int) -> m Bool
canIncrease GenericSolverM m Rational
solver (Rational
aij, Int
xj)
      if Bool
b
      then do
        let cj :: Rational
cj = Int -> Expr Rational -> Rational
forall r. Num r => Int -> Expr r -> r
LA.coeff Int
xj Expr Rational
obj_def
        let ratio :: Rational
ratio = Rational
cj Rational -> Rational -> Rational
forall a. Fractional a => a -> a -> a
/ Rational
aij
        [(Int, Rational)] -> m [(Int, Rational)]
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return [(Int
xj, Rational
ratio) | Rational
ratio Rational -> Rational -> Bool
forall a. Ord a => a -> a -> Bool
>= Rational
0]
      else
        [(Int, Rational)] -> m [(Int, Rational)]
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return []
  case [(Int, Rational)]
ws of
    [] -> Maybe Int -> m (Maybe Int)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Int
forall a. Maybe a
Nothing
    [(Int, Rational)]
_ -> Maybe Int -> m (Maybe Int)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Int -> m (Maybe Int)) -> Maybe Int -> m (Maybe Int)
forall a b. (a -> b) -> a -> b
$ Int -> Maybe Int
forall a. a -> Maybe a
Just (Int -> Maybe Int) -> Int -> Maybe Int
forall a b. (a -> b) -> a -> b
$ (Int, Rational) -> Int
forall a b. (a, b) -> a
fst ((Int, Rational) -> Int) -> (Int, Rational) -> Int
forall a b. (a -> b) -> a -> b
$ ((Int, Rational) -> (Int, Rational) -> Ordering)
-> [(Int, Rational)] -> (Int, Rational)
forall (t :: * -> *) a.
Foldable t =>
(a -> a -> Ordering) -> t a -> a
minimumBy (((Int, Rational) -> Rational)
-> (Int, Rational) -> (Int, Rational) -> Ordering
forall a b. Ord a => (b -> a) -> b -> b -> Ordering
comparing (Int, Rational) -> Rational
forall a b. (a, b) -> b
snd) [(Int, Rational)]
ws

prune :: PrimMonad m => GenericSolverM m Rational -> Options -> m Bool
prune :: forall (m :: * -> *).
PrimMonad m =>
GenericSolverM m Rational -> Options -> m Bool
prune GenericSolverM m Rational
solver Options
opt =
  case Options -> Maybe Rational
objLimit Options
opt of
    Maybe Rational
Nothing -> Bool -> m Bool
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
    Just Rational
lim -> do
      Rational
o <- GenericSolverM m Rational -> m Rational
forall (m :: * -> *) v. PrimMonad m => GenericSolverM m v -> m v
getObjValue GenericSolverM m Rational
solver
      OptDir
dir <- GenericSolverM m Rational -> m OptDir
forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> m OptDir
getOptDir GenericSolverM m Rational
solver
      case OptDir
dir of
        OptDir
OptMin -> Bool -> m Bool
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> m Bool) -> Bool -> m Bool
forall a b. (a -> b) -> a -> b
$! (Rational
lim Rational -> Rational -> Bool
forall a. Ord a => a -> a -> Bool
<= Rational
o)
        OptDir
OptMax -> Bool -> m Bool
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> m Bool) -> Bool -> m Bool
forall a b. (a -> b) -> a -> b
$! (Rational
lim Rational -> Rational -> Bool
forall a. Ord a => a -> a -> Bool
>= Rational
o)

{--------------------------------------------------------------------
  Extract results
--------------------------------------------------------------------}

type RawModel v = IntMap v

getRawModel :: PrimMonad m => GenericSolverM m v -> m (RawModel v)
getRawModel :: forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> m (RawModel v)
getRawModel GenericSolverM m v
solver = do
  [Int]
xs <- GenericSolverM m v -> m [Int]
forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> m [Int]
variables GenericSolverM m v
solver
  ([(Int, v)] -> RawModel v) -> m [(Int, v)] -> m (RawModel v)
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM [(Int, v)] -> RawModel v
forall a. [(Int, a)] -> IntMap a
IntMap.fromList (m [(Int, v)] -> m (RawModel v)) -> m [(Int, v)] -> m (RawModel v)
forall a b. (a -> b) -> a -> b
$ [Int] -> (Int -> m (Int, v)) -> m [(Int, v)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [Int]
xs ((Int -> m (Int, v)) -> m [(Int, v)])
-> (Int -> m (Int, v)) -> m [(Int, v)]
forall a b. (a -> b) -> a -> b
$ \Int
x -> do
    v
val <- GenericSolverM m v -> Int -> m v
forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> Int -> m v
getValue GenericSolverM m v
solver Int
x
    (Int, v) -> m (Int, v)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Int
x,v
val)

getObjValue :: PrimMonad m => GenericSolverM m v -> m v
getObjValue :: forall (m :: * -> *) v. PrimMonad m => GenericSolverM m v -> m v
getObjValue GenericSolverM m v
solver = GenericSolverM m v -> Int -> m v
forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> Int -> m v
getValue GenericSolverM m v
solver Int
objVar

type Model = IntMap Rational

explain :: PrimMonad m => GenericSolverM m v -> m ConstrIDSet
explain :: forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> m ConstrIDSet
explain GenericSolverM m v
solver = do
  Maybe ConstrIDSet
m <- MutVar (PrimState m) (Maybe ConstrIDSet) -> m (Maybe ConstrIDSet)
forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> m a
readMutVar (GenericSolverM m v -> MutVar (PrimState m) (Maybe ConstrIDSet)
forall (m :: * -> *) v.
GenericSolverM m v -> MutVar (PrimState m) (Maybe ConstrIDSet)
svExplanation GenericSolverM m v
solver)
  case Maybe ConstrIDSet
m of
    Maybe ConstrIDSet
Nothing -> String -> m ConstrIDSet
forall a. HasCallStack => String -> a
error String
"no explanation is available"
    Just ConstrIDSet
cs -> ConstrIDSet -> m ConstrIDSet
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ConstrIDSet
cs

{--------------------------------------------------------------------
  major function
--------------------------------------------------------------------}

update :: (PrimMonad m, SolverValue v) => GenericSolverM m v -> Var -> v -> m ()
update :: forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> Int -> v -> m ()
update GenericSolverM m v
solver Int
xj v
v = do
  -- log solver $ printf "before update x%d (%s)" xj (show v)
  -- dump solver

  v
v0 <- GenericSolverM m v -> Int -> m v
forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> Int -> m v
getValue GenericSolverM m v
solver Int
xj
  let diff :: v
diff = v
v v -> v -> v
forall v. AdditiveGroup v => v -> v -> v
^-^ v
v0

  Model
aj <- GenericSolverM m v -> Int -> m Model
forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> Int -> m Model
getCol GenericSolverM m v
solver Int
xj
  MutVar (PrimState m) (IntMap v) -> (IntMap v -> IntMap v) -> m ()
forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> (a -> a) -> m ()
modifyMutVar (GenericSolverM m v -> MutVar (PrimState m) (IntMap v)
forall (m :: * -> *) v.
GenericSolverM m v -> MutVar (PrimState m) (IntMap v)
svModel GenericSolverM m v
solver) ((IntMap v -> IntMap v) -> m ()) -> (IntMap v -> IntMap v) -> m ()
forall a b. (a -> b) -> a -> b
$ \IntMap v
m ->
    let m2 :: IntMap v
m2 = (Rational -> v) -> Model -> IntMap v
forall a b. (a -> b) -> IntMap a -> IntMap b
IntMap.map (\Rational
aij -> Rational
Scalar v
aij Scalar v -> v -> v
forall v. VectorSpace v => Scalar v -> v -> v
*^ v
diff) Model
aj
    in Int -> v -> IntMap v -> IntMap v
forall a. Int -> a -> IntMap a -> IntMap a
IntMap.insert Int
xj v
v (IntMap v -> IntMap v) -> IntMap v -> IntMap v
forall a b. (a -> b) -> a -> b
$ (v -> v -> v) -> IntMap v -> IntMap v -> IntMap v
forall a. (a -> a -> a) -> IntMap a -> IntMap a -> IntMap a
IntMap.unionWith v -> v -> v
forall v. AdditiveGroup v => v -> v -> v
(^+^) IntMap v
m2 IntMap v
m

  -- log solver $ printf "after update x%d (%s)" xj (show v)
  -- dump solver

pivot :: (PrimMonad m, SolverValue v) => GenericSolverM m v -> Var -> Var -> m ()
pivot :: forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> Int -> Int -> m ()
pivot GenericSolverM m v
solver Int
xi Int
xj = do
  MutVar (PrimState m) Int -> (Int -> Int) -> m ()
forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> (a -> a) -> m ()
modifyMutVar' (GenericSolverM m v -> MutVar (PrimState m) Int
forall (m :: * -> *) v.
GenericSolverM m v -> MutVar (PrimState m) Int
svNPivot GenericSolverM m v
solver) (Int -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1)
  MutVar (PrimState m) (IntMap (Expr Rational))
-> (IntMap (Expr Rational) -> IntMap (Expr Rational)) -> m ()
forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> (a -> a) -> m ()
modifyMutVar' (GenericSolverM m v -> MutVar (PrimState m) (IntMap (Expr Rational))
forall (m :: * -> *) v.
GenericSolverM m v -> MutVar (PrimState m) (IntMap (Expr Rational))
svTableau GenericSolverM m v
solver) ((IntMap (Expr Rational) -> IntMap (Expr Rational)) -> m ())
-> (IntMap (Expr Rational) -> IntMap (Expr Rational)) -> m ()
forall a b. (a -> b) -> a -> b
$ \IntMap (Expr Rational)
defs ->
    case Atom Rational -> Int -> Maybe (RelOp, Expr Rational)
forall r.
(Real r, Fractional r) =>
Atom r -> Int -> Maybe (RelOp, Expr r)
LA.solveFor (Int -> Expr Rational
forall r. Num r => Int -> Expr r
LA.var Int
xi Expr Rational -> Expr Rational -> Atom Rational
forall e r. IsEqRel e r => e -> e -> r
.==. (IntMap (Expr Rational)
defs IntMap (Expr Rational) -> Int -> Expr Rational
forall a. IntMap a -> Int -> a
IntMap.! Int
xi)) Int
xj of
      Just (RelOp
Eql, Expr Rational
xj_def) ->
        Int
-> Expr Rational
-> IntMap (Expr Rational)
-> IntMap (Expr Rational)
forall a. Int -> a -> IntMap a -> IntMap a
IntMap.insert Int
xj Expr Rational
xj_def (IntMap (Expr Rational) -> IntMap (Expr Rational))
-> (IntMap (Expr Rational) -> IntMap (Expr Rational))
-> IntMap (Expr Rational)
-> IntMap (Expr Rational)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr Rational -> Expr Rational)
-> IntMap (Expr Rational) -> IntMap (Expr Rational)
forall a b. (a -> b) -> IntMap a -> IntMap b
IntMap.map (Int -> Expr Rational -> Expr Rational -> Expr Rational
forall r. (Num r, Eq r) => Int -> Expr r -> Expr r -> Expr r
LA.applySubst1 Int
xj Expr Rational
xj_def) (IntMap (Expr Rational) -> IntMap (Expr Rational))
-> (IntMap (Expr Rational) -> IntMap (Expr Rational))
-> IntMap (Expr Rational)
-> IntMap (Expr Rational)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> IntMap (Expr Rational) -> IntMap (Expr Rational)
forall a. Int -> IntMap a -> IntMap a
IntMap.delete Int
xi (IntMap (Expr Rational) -> IntMap (Expr Rational))
-> IntMap (Expr Rational) -> IntMap (Expr Rational)
forall a b. (a -> b) -> a -> b
$ IntMap (Expr Rational)
defs
      Maybe (RelOp, Expr Rational)
_ -> String -> IntMap (Expr Rational)
forall a. HasCallStack => String -> a
error String
"pivot: should not happen"

pivotAndUpdate :: (PrimMonad m, SolverValue v) => GenericSolverM m v -> Var -> Var -> v -> m ()
pivotAndUpdate :: forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> Int -> Int -> v -> m ()
pivotAndUpdate GenericSolverM m v
solver Int
xi Int
xj v
v | Int
xi Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
xj = GenericSolverM m v -> Int -> v -> m ()
forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> Int -> v -> m ()
update GenericSolverM m v
solver Int
xi v
v -- xi = xj is non-basic variable
pivotAndUpdate GenericSolverM m v
solver Int
xi Int
xj v
v = do
  -- xi is basic variable
  -- xj is non-basic varaible

  -- log solver $ printf "before pivotAndUpdate x%d x%d (%s)" xi xj (show v)
  -- dump solver

  IntMap v
m <- MutVar (PrimState m) (IntMap v) -> m (IntMap v)
forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> m a
readMutVar (GenericSolverM m v -> MutVar (PrimState m) (IntMap v)
forall (m :: * -> *) v.
GenericSolverM m v -> MutVar (PrimState m) (IntMap v)
svModel GenericSolverM m v
solver)

  Model
aj <- GenericSolverM m v -> Int -> m Model
forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> Int -> m Model
getCol GenericSolverM m v
solver Int
xj
  let aij :: Rational
aij = Model
aj Model -> Int -> Rational
forall a. IntMap a -> Int -> a
IntMap.! Int
xi
  let theta :: v
theta = (v
v v -> v -> v
forall v. AdditiveGroup v => v -> v -> v
^-^ (IntMap v
m IntMap v -> Int -> v
forall a. IntMap a -> Int -> a
IntMap.! Int
xi)) v -> Rational -> v
forall v s.
(VectorSpace v, s ~ Scalar v, Fractional s) =>
v -> s -> v
^/ Rational
aij

  let m' :: IntMap v
m' = [(Int, v)] -> IntMap v
forall a. [(Int, a)] -> IntMap a
IntMap.fromList ([(Int, v)] -> IntMap v) -> [(Int, v)] -> IntMap v
forall a b. (a -> b) -> a -> b
$
           [(Int
xi, v
v), (Int
xj, (IntMap v
m IntMap v -> Int -> v
forall a. IntMap a -> Int -> a
IntMap.! Int
xj) v -> v -> v
forall v. AdditiveGroup v => v -> v -> v
^+^ v
theta)] [(Int, v)] -> [(Int, v)] -> [(Int, v)]
forall a. [a] -> [a] -> [a]
++
           [(Int
xk, (IntMap v
m IntMap v -> Int -> v
forall a. IntMap a -> Int -> a
IntMap.! Int
xk) v -> v -> v
forall v. AdditiveGroup v => v -> v -> v
^+^ (Rational
Scalar v
akj Scalar v -> v -> v
forall v. VectorSpace v => Scalar v -> v -> v
*^ v
theta)) | (Int
xk, Rational
akj) <- Model -> [(Int, Rational)]
forall a. IntMap a -> [(Int, a)]
IntMap.toList Model
aj, Int
xk Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Int
xi]
  MutVar (PrimState m) (IntMap v) -> IntMap v -> m ()
forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> a -> m ()
writeMutVar (GenericSolverM m v -> MutVar (PrimState m) (IntMap v)
forall (m :: * -> *) v.
GenericSolverM m v -> MutVar (PrimState m) (IntMap v)
svModel GenericSolverM m v
solver) (IntMap v -> IntMap v -> IntMap v
forall a. IntMap a -> IntMap a -> IntMap a
IntMap.union IntMap v
m' IntMap v
m) -- note that 'IntMap.union' is left biased.

  GenericSolverM m v -> Int -> Int -> m ()
forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> Int -> Int -> m ()
pivot GenericSolverM m v
solver Int
xi Int
xj

  Config
config <- GenericSolverM m v -> m Config
forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> m Config
getConfig GenericSolverM m v
solver
  Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Config -> Bool
configEnableBoundTightening Config
config) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ do
    GenericSolverM m v -> Int -> m ()
forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> Int -> m ()
tightenBounds GenericSolverM m v
solver Int
xj

  -- log solver $ printf "after pivotAndUpdate x%d x%d (%s)" xi xj (show v)
  -- dump solver

getLB :: PrimMonad m => GenericSolverM m v -> Var -> m (Bound v)
getLB :: forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> Int -> m (Bound v)
getLB GenericSolverM m v
solver Int
x = do
  IntMap (v, ConstrIDSet)
lb <- MutVar (PrimState m) (IntMap (v, ConstrIDSet))
-> m (IntMap (v, ConstrIDSet))
forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> m a
readMutVar (GenericSolverM m v
-> MutVar (PrimState m) (IntMap (v, ConstrIDSet))
forall (m :: * -> *) v.
GenericSolverM m v
-> MutVar (PrimState m) (IntMap (v, ConstrIDSet))
svLB GenericSolverM m v
solver)
  Bound v -> m (Bound v)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bound v -> m (Bound v)) -> Bound v -> m (Bound v)
forall a b. (a -> b) -> a -> b
$ Int -> IntMap (v, ConstrIDSet) -> Bound v
forall a. Int -> IntMap a -> Maybe a
IntMap.lookup Int
x IntMap (v, ConstrIDSet)
lb

getUB :: PrimMonad m => GenericSolverM m v -> Var -> m (Bound v)
getUB :: forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> Int -> m (Bound v)
getUB GenericSolverM m v
solver Int
x = do
  IntMap (v, ConstrIDSet)
ub <- MutVar (PrimState m) (IntMap (v, ConstrIDSet))
-> m (IntMap (v, ConstrIDSet))
forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> m a
readMutVar (GenericSolverM m v
-> MutVar (PrimState m) (IntMap (v, ConstrIDSet))
forall (m :: * -> *) v.
GenericSolverM m v
-> MutVar (PrimState m) (IntMap (v, ConstrIDSet))
svUB GenericSolverM m v
solver)
  Bound v -> m (Bound v)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bound v -> m (Bound v)) -> Bound v -> m (Bound v)
forall a b. (a -> b) -> a -> b
$ Int -> IntMap (v, ConstrIDSet) -> Bound v
forall a. Int -> IntMap a -> Maybe a
IntMap.lookup Int
x IntMap (v, ConstrIDSet)
ub

getTableau :: PrimMonad m => GenericSolverM m v -> m (IntMap (LA.Expr Rational))
getTableau :: forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> m (IntMap (Expr Rational))
getTableau GenericSolverM m v
solver = do
  IntMap (Expr Rational)
t <- MutVar (PrimState m) (IntMap (Expr Rational))
-> m (IntMap (Expr Rational))
forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> m a
readMutVar (GenericSolverM m v -> MutVar (PrimState m) (IntMap (Expr Rational))
forall (m :: * -> *) v.
GenericSolverM m v -> MutVar (PrimState m) (IntMap (Expr Rational))
svTableau GenericSolverM m v
solver)
  IntMap (Expr Rational) -> m (IntMap (Expr Rational))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (IntMap (Expr Rational) -> m (IntMap (Expr Rational)))
-> IntMap (Expr Rational) -> m (IntMap (Expr Rational))
forall a b. (a -> b) -> a -> b
$ Int -> IntMap (Expr Rational) -> IntMap (Expr Rational)
forall a. Int -> IntMap a -> IntMap a
IntMap.delete Int
objVar IntMap (Expr Rational)
t

getValue :: PrimMonad m => GenericSolverM m v -> Var -> m v
getValue :: forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> Int -> m v
getValue GenericSolverM m v
solver Int
x = do
  IntMap v
m <- MutVar (PrimState m) (IntMap v) -> m (IntMap v)
forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> m a
readMutVar (GenericSolverM m v -> MutVar (PrimState m) (IntMap v)
forall (m :: * -> *) v.
GenericSolverM m v -> MutVar (PrimState m) (IntMap v)
svModel GenericSolverM m v
solver)
  v -> m v
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (v -> m v) -> v -> m v
forall a b. (a -> b) -> a -> b
$ IntMap v
m IntMap v -> Int -> v
forall a. IntMap a -> Int -> a
IntMap.! Int
x

getRow :: PrimMonad m => GenericSolverM m v -> Var -> m (LA.Expr Rational)
getRow :: forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> Int -> m (Expr Rational)
getRow GenericSolverM m v
solver Int
x = do
  -- x should be basic variable or 'objVar'
  IntMap (Expr Rational)
t <- MutVar (PrimState m) (IntMap (Expr Rational))
-> m (IntMap (Expr Rational))
forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> m a
readMutVar (GenericSolverM m v -> MutVar (PrimState m) (IntMap (Expr Rational))
forall (m :: * -> *) v.
GenericSolverM m v -> MutVar (PrimState m) (IntMap (Expr Rational))
svTableau GenericSolverM m v
solver)
  Expr Rational -> m (Expr Rational)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr Rational -> m (Expr Rational))
-> Expr Rational -> m (Expr Rational)
forall a b. (a -> b) -> a -> b
$! (IntMap (Expr Rational)
t IntMap (Expr Rational) -> Int -> Expr Rational
forall a. IntMap a -> Int -> a
IntMap.! Int
x)

-- aijが非ゼロの列も全部探しているのは効率が悪い
getCol :: (PrimMonad m, SolverValue v) => GenericSolverM m v -> Var -> m (IntMap Rational)
getCol :: forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> Int -> m Model
getCol GenericSolverM m v
solver Int
xj = do
  IntMap (Expr Rational)
t <- MutVar (PrimState m) (IntMap (Expr Rational))
-> m (IntMap (Expr Rational))
forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> m a
readMutVar (GenericSolverM m v -> MutVar (PrimState m) (IntMap (Expr Rational))
forall (m :: * -> *) v.
GenericSolverM m v -> MutVar (PrimState m) (IntMap (Expr Rational))
svTableau GenericSolverM m v
solver)
  Model -> m Model
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Model -> m Model) -> Model -> m Model
forall a b. (a -> b) -> a -> b
$ (Expr Rational -> Maybe Rational)
-> IntMap (Expr Rational) -> Model
forall a b. (a -> Maybe b) -> IntMap a -> IntMap b
IntMap.mapMaybe (Int -> Expr Rational -> Maybe Rational
forall r. Num r => Int -> Expr r -> Maybe r
LA.lookupCoeff Int
xj) IntMap (Expr Rational)
t

getCoeff :: PrimMonad m => GenericSolverM m v -> Var -> Var -> m Rational
getCoeff :: forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> Int -> Int -> m Rational
getCoeff GenericSolverM m v
solver Int
xi Int
xj = do
  Expr Rational
xi_def <- GenericSolverM m v -> Int -> m (Expr Rational)
forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> Int -> m (Expr Rational)
getRow GenericSolverM m v
solver Int
xi
  Rational -> m Rational
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Rational -> m Rational) -> Rational -> m Rational
forall a b. (a -> b) -> a -> b
$! Int -> Expr Rational -> Rational
forall r. Num r => Int -> Expr r -> r
LA.coeff Int
xj Expr Rational
xi_def

setExplanation :: PrimMonad m => GenericSolverM m v -> ConstrIDSet -> m ()
setExplanation :: forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> ConstrIDSet -> m ()
setExplanation GenericSolverM m v
solver !ConstrIDSet
cs = do
  Maybe ConstrIDSet
m <- MutVar (PrimState m) (Maybe ConstrIDSet) -> m (Maybe ConstrIDSet)
forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> m a
readMutVar (GenericSolverM m v -> MutVar (PrimState m) (Maybe ConstrIDSet)
forall (m :: * -> *) v.
GenericSolverM m v -> MutVar (PrimState m) (Maybe ConstrIDSet)
svExplanation GenericSolverM m v
solver)
  case Maybe ConstrIDSet
m of
    Just ConstrIDSet
_ -> () -> m ()
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    Maybe ConstrIDSet
Nothing -> MutVar (PrimState m) (Maybe ConstrIDSet)
-> Maybe ConstrIDSet -> m ()
forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> a -> m ()
writeMutVar (GenericSolverM m v -> MutVar (PrimState m) (Maybe ConstrIDSet)
forall (m :: * -> *) v.
GenericSolverM m v -> MutVar (PrimState m) (Maybe ConstrIDSet)
svExplanation GenericSolverM m v
solver) (ConstrIDSet -> Maybe ConstrIDSet
forall a. a -> Maybe a
Just ConstrIDSet
cs)

{--------------------------------------------------------------------
  utility
--------------------------------------------------------------------}

findM :: Monad m => (a -> m Bool) -> [a] -> m (Maybe a)
findM :: forall (m :: * -> *) a.
Monad m =>
(a -> m Bool) -> [a] -> m (Maybe a)
findM a -> m Bool
_ [] = Maybe a -> m (Maybe a)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe a
forall a. Maybe a
Nothing
findM a -> m Bool
p (a
x:[a]
xs) = do
  Bool
r <- a -> m Bool
p a
x
  if Bool
r
  then Maybe a -> m (Maybe a)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (a -> Maybe a
forall a. a -> Maybe a
Just a
x)
  else (a -> m Bool) -> [a] -> m (Maybe a)
forall (m :: * -> *) a.
Monad m =>
(a -> m Bool) -> [a] -> m (Maybe a)
findM a -> m Bool
p [a]
xs

testLB :: SolverValue v => Bound v -> v -> Bool
testLB :: forall v. SolverValue v => Bound v -> v -> Bool
testLB Maybe (v, ConstrIDSet)
Nothing v
_  = Bool
True
testLB (Just (v
l,ConstrIDSet
_)) v
x = v
l v -> v -> Bool
forall a. Ord a => a -> a -> Bool
<= v
x

testUB :: SolverValue v => Bound v -> v -> Bool
testUB :: forall v. SolverValue v => Bound v -> v -> Bool
testUB Maybe (v, ConstrIDSet)
Nothing v
_  = Bool
True
testUB (Just (v
u,ConstrIDSet
_)) v
x = v
x v -> v -> Bool
forall a. Ord a => a -> a -> Bool
<= v
u

variables :: PrimMonad m => GenericSolverM m v -> m [Var]
variables :: forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> m [Int]
variables GenericSolverM m v
solver = do
  Int
vcnt <- GenericSolverM m v -> m Int
forall (m :: * -> *) v. PrimMonad m => GenericSolverM m v -> m Int
nVars GenericSolverM m v
solver
  [Int] -> m [Int]
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return [Int
0..Int
vcntInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1]

basicVariables :: PrimMonad m => GenericSolverM m v -> m [Var]
basicVariables :: forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> m [Int]
basicVariables GenericSolverM m v
solver = do
  IntMap (Expr Rational)
t <- MutVar (PrimState m) (IntMap (Expr Rational))
-> m (IntMap (Expr Rational))
forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> m a
readMutVar (GenericSolverM m v -> MutVar (PrimState m) (IntMap (Expr Rational))
forall (m :: * -> *) v.
GenericSolverM m v -> MutVar (PrimState m) (IntMap (Expr Rational))
svTableau GenericSolverM m v
solver)
  [Int] -> m [Int]
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (IntMap (Expr Rational) -> [Int]
forall a. IntMap a -> [Int]
IntMap.keys IntMap (Expr Rational)
t)

recordTime :: (PrimMonad m, SolverValue v) => GenericSolverM m v -> m a -> m a
recordTime :: forall (m :: * -> *) v a.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> m a -> m a
recordTime GenericSolverM m v
solver m a
act = do
  GenericSolverM m v -> m ()
forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> m ()
dumpSize GenericSolverM m v
solver
  MutVar (PrimState m) Int -> Int -> m ()
forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> a -> m ()
writeMutVar (GenericSolverM m v -> MutVar (PrimState m) Int
forall (m :: * -> *) v.
GenericSolverM m v -> MutVar (PrimState m) Int
svNPivot GenericSolverM m v
solver) Int
0
  Maybe (GenericSolverM m v -> m :~> m)
rectm <- MutVar (PrimState m) (Maybe (GenericSolverM m v -> m :~> m))
-> m (Maybe (GenericSolverM m v -> m :~> m))
forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> m a
readMutVar (GenericSolverM m v
-> MutVar (PrimState m) (Maybe (GenericSolverM m v -> m :~> m))
forall (m :: * -> *) v.
GenericSolverM m v
-> MutVar (PrimState m) (Maybe (GenericSolverM m v -> m :~> m))
svRecTime GenericSolverM m v
solver)
  a
result <-
    case Maybe (GenericSolverM m v -> m :~> m)
rectm of
      Maybe (GenericSolverM m v -> m :~> m)
Nothing -> m a
act
      Just GenericSolverM m v -> m :~> m
f -> GenericSolverM m v -> m :~> m
f GenericSolverM m v
solver (m :~> m) -> m ~> m
forall (f :: * -> *) (g :: * -> *). (f :~> g) -> f ~> g
$$ m a
act
  (GenericSolverM m v -> String -> m ()
forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> String -> m ()
log GenericSolverM m v
solver (String -> m ()) -> (Int -> String) -> Int -> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Int -> String
forall r. PrintfType r => String -> r
printf String
"#pivot = %d") (Int -> m ()) -> m Int -> m ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< MutVar (PrimState m) Int -> m Int
forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> m a
readMutVar (GenericSolverM m v -> MutVar (PrimState m) Int
forall (m :: * -> *) v.
GenericSolverM m v -> MutVar (PrimState m) Int
svNPivot GenericSolverM m v
solver)
  a -> m a
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return a
result

showDelta :: Bool -> Delta Rational -> String
showDelta :: Bool -> Delta Rational -> String
showDelta Bool
asRatio Delta Rational
v =
  case Delta Rational
v of
    (Delta Rational
r Rational
k) ->
      Rational -> String
f Rational
r String -> ShowS
forall a. [a] -> [a] -> [a]
++
        case Rational -> Rational -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Rational
k Rational
0 of
          Ordering
EQ -> String
""
          Ordering
GT -> String
" + " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Rational -> String
f Rational
k String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" delta"
          Ordering
LT -> String
" - " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Rational -> String
f (Rational -> Rational
forall a. Num a => a -> a
abs Rational
k) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" delta"
  where
    f :: Rational -> String
f = Bool -> Rational -> String
showRational Bool
asRatio

{--------------------------------------------------------------------
  Logging
--------------------------------------------------------------------}

-- | set callback function for receiving messages.
setLogger :: PrimMonad m => GenericSolverM m v -> (String -> m ()) -> m ()
setLogger :: forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> (String -> m ()) -> m ()
setLogger GenericSolverM m v
solver String -> m ()
logger = do
  MutVar (PrimState m) (Maybe (String -> m ()))
-> Maybe (String -> m ()) -> m ()
forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> a -> m ()
writeMutVar (GenericSolverM m v -> MutVar (PrimState m) (Maybe (String -> m ()))
forall (m :: * -> *) v.
GenericSolverM m v -> MutVar (PrimState m) (Maybe (String -> m ()))
svLogger GenericSolverM m v
solver) ((String -> m ()) -> Maybe (String -> m ())
forall a. a -> Maybe a
Just String -> m ()
logger)

clearLogger :: PrimMonad m => GenericSolverM m v -> m ()
clearLogger :: forall (m :: * -> *) v. PrimMonad m => GenericSolverM m v -> m ()
clearLogger GenericSolverM m v
solver = MutVar (PrimState m) (Maybe (String -> m ()))
-> Maybe (String -> m ()) -> m ()
forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> a -> m ()
writeMutVar (GenericSolverM m v -> MutVar (PrimState m) (Maybe (String -> m ()))
forall (m :: * -> *) v.
GenericSolverM m v -> MutVar (PrimState m) (Maybe (String -> m ()))
svLogger GenericSolverM m v
solver) Maybe (String -> m ())
forall a. Maybe a
Nothing

log :: PrimMonad m => GenericSolverM m v -> String -> m ()
log :: forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> String -> m ()
log GenericSolverM m v
solver String
msg = GenericSolverM m v -> m String -> m ()
forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> m String -> m ()
logM GenericSolverM m v
solver (String -> m String
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return String
msg)

logM :: PrimMonad m => GenericSolverM m v -> m String -> m ()
logM :: forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> m String -> m ()
logM GenericSolverM m v
solver m String
action = do
  Maybe (String -> m ())
m <- MutVar (PrimState m) (Maybe (String -> m ()))
-> m (Maybe (String -> m ()))
forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> m a
readMutVar (GenericSolverM m v -> MutVar (PrimState m) (Maybe (String -> m ()))
forall (m :: * -> *) v.
GenericSolverM m v -> MutVar (PrimState m) (Maybe (String -> m ()))
svLogger GenericSolverM m v
solver)
  case Maybe (String -> m ())
m of
    Maybe (String -> m ())
Nothing -> () -> m ()
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    Just String -> m ()
logger -> m String
action m String -> (String -> m ()) -> m ()
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= String -> m ()
logger

enableTimeRecording :: GenericSolverM IO v -> IO ()
enableTimeRecording :: forall v. GenericSolverM IO v -> IO ()
enableTimeRecording GenericSolverM IO v
solver = do
  MutVar (PrimState IO) (Maybe (GenericSolverM IO v -> IO :~> IO))
-> Maybe (GenericSolverM IO v -> IO :~> IO) -> IO ()
forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> a -> m ()
writeMutVar (GenericSolverM IO v
-> MutVar (PrimState IO) (Maybe (GenericSolverM IO v -> IO :~> IO))
forall (m :: * -> *) v.
GenericSolverM m v
-> MutVar (PrimState m) (Maybe (GenericSolverM m v -> m :~> m))
svRecTime GenericSolverM IO v
solver) ((GenericSolverM IO v -> IO :~> IO)
-> Maybe (GenericSolverM IO v -> IO :~> IO)
forall a. a -> Maybe a
Just GenericSolverM IO v -> IO :~> IO
forall {v}. GenericSolverM IO v -> IO :~> IO
f)
  where
    f :: GenericSolverM IO v -> IO :~> IO
f GenericSolverM IO v
solver = (IO ~> IO) -> IO :~> IO
forall (f :: * -> *) (g :: * -> *). (f ~> g) -> f :~> g
Nat ((IO ~> IO) -> IO :~> IO) -> (IO ~> IO) -> IO :~> IO
forall a b. (a -> b) -> a -> b
$ \IO x
act -> do
        TimeSpec
startCPU <- Clock -> IO TimeSpec
getTime Clock
ProcessCPUTime
        TimeSpec
startWC  <- Clock -> IO TimeSpec
getTime Clock
Monotonic
        x
result <- IO x
act
        TimeSpec
endCPU <- Clock -> IO TimeSpec
getTime Clock
ProcessCPUTime
        TimeSpec
endWC  <- Clock -> IO TimeSpec
getTime Clock
Monotonic
        let durationSecs :: TimeSpec -> TimeSpec -> Double
            durationSecs :: TimeSpec -> TimeSpec -> Double
durationSecs TimeSpec
start TimeSpec
end = Integer -> Double
forall a b. (Integral a, Num b) => a -> b
fromIntegral (TimeSpec -> Integer
toNanoSecs (TimeSpec
end TimeSpec -> TimeSpec -> TimeSpec
`diffTimeSpec` TimeSpec
start)) Double -> Double -> Double
forall a. Fractional a => a -> a -> a
/ Double
10Double -> Int -> Double
forall a b. (Num a, Integral b) => a -> b -> a
^(Int
9::Int)
        (GenericSolverM IO v -> String -> IO ()
forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> String -> m ()
log GenericSolverM IO v
solver (String -> IO ()) -> (Double -> String) -> Double -> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Double -> String
forall r. PrintfType r => String -> r
printf String
"cpu time = %.3fs") (TimeSpec -> TimeSpec -> Double
durationSecs TimeSpec
startCPU TimeSpec
endCPU)
        (GenericSolverM IO v -> String -> IO ()
forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> String -> m ()
log GenericSolverM IO v
solver (String -> IO ()) -> (Double -> String) -> Double -> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Double -> String
forall r. PrintfType r => String -> r
printf String
"wall clock time = %.3fs") (TimeSpec -> TimeSpec -> Double
durationSecs TimeSpec
startWC TimeSpec
endWC)
        x -> IO x
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return x
result

disableTimeRecording :: PrimMonad m => GenericSolverM m v -> m ()
disableTimeRecording :: forall (m :: * -> *) v. PrimMonad m => GenericSolverM m v -> m ()
disableTimeRecording GenericSolverM m v
solver = MutVar (PrimState m) (Maybe (GenericSolverM m v -> m :~> m))
-> Maybe (GenericSolverM m v -> m :~> m) -> m ()
forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> a -> m ()
writeMutVar (GenericSolverM m v
-> MutVar (PrimState m) (Maybe (GenericSolverM m v -> m :~> m))
forall (m :: * -> *) v.
GenericSolverM m v
-> MutVar (PrimState m) (Maybe (GenericSolverM m v -> m :~> m))
svRecTime GenericSolverM m v
solver) Maybe (GenericSolverM m v -> m :~> m)
forall a. Maybe a
Nothing

{--------------------------------------------------------------------
  debug and tests
--------------------------------------------------------------------}

test4 :: IO ()
test4 :: IO ()
test4 = do
  GenericSolverM IO Rational
solver <- IO (GenericSolverM IO Rational)
forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
m (GenericSolverM m v)
newSolver
  GenericSolverM IO Rational -> (String -> IO ()) -> IO ()
forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> (String -> m ()) -> m ()
setLogger GenericSolverM IO Rational
solver String -> IO ()
putStrLn
  Int
x0 <- GenericSolverM IO Rational -> IO Int
forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> m Int
newVar GenericSolverM IO Rational
solver
  Int
x1 <- GenericSolverM IO Rational -> IO Int
forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> m Int
newVar GenericSolverM IO Rational
solver

  MutVar (PrimState IO) (IntMap (Expr Rational))
-> IntMap (Expr Rational) -> IO ()
forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> a -> m ()
writeMutVar (GenericSolverM IO Rational
-> MutVar (PrimState IO) (IntMap (Expr Rational))
forall (m :: * -> *) v.
GenericSolverM m v -> MutVar (PrimState m) (IntMap (Expr Rational))
svTableau GenericSolverM IO Rational
solver) ([(Int, Expr Rational)] -> IntMap (Expr Rational)
forall a. [(Int, a)] -> IntMap a
IntMap.fromList [(Int
x1, Int -> Expr Rational
forall r. Num r => Int -> Expr r
LA.var Int
x0)])
  MutVar (PrimState IO) (IntMap (Rational, ConstrIDSet))
-> IntMap (Rational, ConstrIDSet) -> IO ()
forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> a -> m ()
writeMutVar (GenericSolverM IO Rational
-> MutVar (PrimState IO) (IntMap (Rational, ConstrIDSet))
forall (m :: * -> *) v.
GenericSolverM m v
-> MutVar (PrimState m) (IntMap (v, ConstrIDSet))
svLB GenericSolverM IO Rational
solver) (IntMap (Rational, ConstrIDSet) -> IO ())
-> IntMap (Rational, ConstrIDSet) -> IO ()
forall a b. (a -> b) -> a -> b
$ (Rational -> (Rational, ConstrIDSet))
-> Model -> IntMap (Rational, ConstrIDSet)
forall a b. (a -> b) -> IntMap a -> IntMap b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\Rational
v -> (Rational
v, ConstrIDSet
forall a. Monoid a => a
mempty)) (Model -> IntMap (Rational, ConstrIDSet))
-> Model -> IntMap (Rational, ConstrIDSet)
forall a b. (a -> b) -> a -> b
$ [(Int, Rational)] -> Model
forall a. [(Int, a)] -> IntMap a
IntMap.fromList [(Int
x0, Rational
0), (Int
x1, Rational
0)]
  MutVar (PrimState IO) (IntMap (Rational, ConstrIDSet))
-> IntMap (Rational, ConstrIDSet) -> IO ()
forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> a -> m ()
writeMutVar (GenericSolverM IO Rational
-> MutVar (PrimState IO) (IntMap (Rational, ConstrIDSet))
forall (m :: * -> *) v.
GenericSolverM m v
-> MutVar (PrimState m) (IntMap (v, ConstrIDSet))
svUB GenericSolverM IO Rational
solver) (IntMap (Rational, ConstrIDSet) -> IO ())
-> IntMap (Rational, ConstrIDSet) -> IO ()
forall a b. (a -> b) -> a -> b
$ (Rational -> (Rational, ConstrIDSet))
-> Model -> IntMap (Rational, ConstrIDSet)
forall a b. (a -> b) -> IntMap a -> IntMap b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\Rational
v -> (Rational
v, ConstrIDSet
forall a. Monoid a => a
mempty)) (Model -> IntMap (Rational, ConstrIDSet))
-> Model -> IntMap (Rational, ConstrIDSet)
forall a b. (a -> b) -> a -> b
$ [(Int, Rational)] -> Model
forall a. [(Int, a)] -> IntMap a
IntMap.fromList [(Int
x0, Rational
2), (Int
x1, Rational
3)]
  GenericSolverM IO Rational -> Expr Rational -> IO ()
forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> Expr Rational -> m ()
setObj GenericSolverM IO Rational
solver ([(Rational, Int)] -> Expr Rational
forall r. (Num r, Eq r) => [(r, Int)] -> Expr r
LA.fromTerms [(-Rational
1, Int
x0)])

  OptResult
ret <- GenericSolverM IO Rational -> Options -> IO OptResult
forall (m :: * -> *).
PrimMonad m =>
GenericSolverM m Rational -> Options -> m OptResult
optimize GenericSolverM IO Rational
solver Options
forall a. Default a => a
def
  OptResult -> IO ()
forall a. Show a => a -> IO ()
print OptResult
ret
  GenericSolverM IO Rational -> IO ()
forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> m ()
dump GenericSolverM IO Rational
solver

test5 :: IO ()
test5 :: IO ()
test5 = do
  GenericSolverM IO Rational
solver <- IO (GenericSolverM IO Rational)
forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
m (GenericSolverM m v)
newSolver
  GenericSolverM IO Rational -> (String -> IO ()) -> IO ()
forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> (String -> m ()) -> m ()
setLogger GenericSolverM IO Rational
solver String -> IO ()
putStrLn
  Int
x0 <- GenericSolverM IO Rational -> IO Int
forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> m Int
newVar GenericSolverM IO Rational
solver
  Int
x1 <- GenericSolverM IO Rational -> IO Int
forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> m Int
newVar GenericSolverM IO Rational
solver

  MutVar (PrimState IO) (IntMap (Expr Rational))
-> IntMap (Expr Rational) -> IO ()
forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> a -> m ()
writeMutVar (GenericSolverM IO Rational
-> MutVar (PrimState IO) (IntMap (Expr Rational))
forall (m :: * -> *) v.
GenericSolverM m v -> MutVar (PrimState m) (IntMap (Expr Rational))
svTableau GenericSolverM IO Rational
solver) ([(Int, Expr Rational)] -> IntMap (Expr Rational)
forall a. [(Int, a)] -> IntMap a
IntMap.fromList [(Int
x1, Int -> Expr Rational
forall r. Num r => Int -> Expr r
LA.var Int
x0)])
  MutVar (PrimState IO) (IntMap (Rational, ConstrIDSet))
-> IntMap (Rational, ConstrIDSet) -> IO ()
forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> a -> m ()
writeMutVar (GenericSolverM IO Rational
-> MutVar (PrimState IO) (IntMap (Rational, ConstrIDSet))
forall (m :: * -> *) v.
GenericSolverM m v
-> MutVar (PrimState m) (IntMap (v, ConstrIDSet))
svLB GenericSolverM IO Rational
solver) (IntMap (Rational, ConstrIDSet) -> IO ())
-> IntMap (Rational, ConstrIDSet) -> IO ()
forall a b. (a -> b) -> a -> b
$ (Rational -> (Rational, ConstrIDSet))
-> Model -> IntMap (Rational, ConstrIDSet)
forall a b. (a -> b) -> IntMap a -> IntMap b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\Rational
v -> (Rational
v, ConstrIDSet
forall a. Monoid a => a
mempty)) (Model -> IntMap (Rational, ConstrIDSet))
-> Model -> IntMap (Rational, ConstrIDSet)
forall a b. (a -> b) -> a -> b
$ [(Int, Rational)] -> Model
forall a. [(Int, a)] -> IntMap a
IntMap.fromList [(Int
x0, Rational
0), (Int
x1, Rational
0)]
  MutVar (PrimState IO) (IntMap (Rational, ConstrIDSet))
-> IntMap (Rational, ConstrIDSet) -> IO ()
forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> a -> m ()
writeMutVar (GenericSolverM IO Rational
-> MutVar (PrimState IO) (IntMap (Rational, ConstrIDSet))
forall (m :: * -> *) v.
GenericSolverM m v
-> MutVar (PrimState m) (IntMap (v, ConstrIDSet))
svUB GenericSolverM IO Rational
solver) (IntMap (Rational, ConstrIDSet) -> IO ())
-> IntMap (Rational, ConstrIDSet) -> IO ()
forall a b. (a -> b) -> a -> b
$ (Rational -> (Rational, ConstrIDSet))
-> Model -> IntMap (Rational, ConstrIDSet)
forall a b. (a -> b) -> IntMap a -> IntMap b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\Rational
v -> (Rational
v, ConstrIDSet
forall a. Monoid a => a
mempty)) (Model -> IntMap (Rational, ConstrIDSet))
-> Model -> IntMap (Rational, ConstrIDSet)
forall a b. (a -> b) -> a -> b
$ [(Int, Rational)] -> Model
forall a. [(Int, a)] -> IntMap a
IntMap.fromList [(Int
x0, Rational
2), (Int
x1, Rational
0)]
  GenericSolverM IO Rational -> Expr Rational -> IO ()
forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> Expr Rational -> m ()
setObj GenericSolverM IO Rational
solver ([(Rational, Int)] -> Expr Rational
forall r. (Num r, Eq r) => [(r, Int)] -> Expr r
LA.fromTerms [(-Rational
1, Int
x0)])

  GenericSolverM IO Rational -> IO ()
forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> m ()
checkFeasibility GenericSolverM IO Rational
solver

  OptResult
ret <- GenericSolverM IO Rational -> Options -> IO OptResult
forall (m :: * -> *).
PrimMonad m =>
GenericSolverM m Rational -> Options -> m OptResult
optimize GenericSolverM IO Rational
solver Options
forall a. Default a => a
def
  OptResult -> IO ()
forall a. Show a => a -> IO ()
print OptResult
ret
  GenericSolverM IO Rational -> IO ()
forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> m ()
dump GenericSolverM IO Rational
solver

test6 :: IO ()
test6 :: IO ()
test6 = do
  GenericSolverM IO Rational
solver <- IO (GenericSolverM IO Rational)
forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
m (GenericSolverM m v)
newSolver
  GenericSolverM IO Rational -> (String -> IO ()) -> IO ()
forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> (String -> m ()) -> m ()
setLogger GenericSolverM IO Rational
solver String -> IO ()
putStrLn
  Int
x0 <- GenericSolverM IO Rational -> IO Int
forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> m Int
newVar GenericSolverM IO Rational
solver

  GenericSolverM IO Rational -> Atom Rational -> IO ()
forall (m :: * -> *).
PrimMonad m =>
GenericSolverM m Rational -> Atom Rational -> m ()
assertAtom GenericSolverM IO Rational
solver (Rational -> Expr Rational
forall r. (Num r, Eq r) => r -> Expr r
LA.constant Rational
1 Expr Rational -> Expr Rational -> Atom Rational
forall e r. IsOrdRel e r => e -> e -> r
.<. Int -> Expr Rational
forall r. Num r => Int -> Expr r
LA.var Int
x0)
  GenericSolverM IO Rational -> Atom Rational -> IO ()
forall (m :: * -> *).
PrimMonad m =>
GenericSolverM m Rational -> Atom Rational -> m ()
assertAtom GenericSolverM IO Rational
solver (Rational -> Expr Rational
forall r. (Num r, Eq r) => r -> Expr r
LA.constant Rational
2 Expr Rational -> Expr Rational -> Atom Rational
forall e r. IsOrdRel e r => e -> e -> r
.>. Int -> Expr Rational
forall r. Num r => Int -> Expr r
LA.var Int
x0)

  Bool
ret <- GenericSolverM IO Rational -> IO Bool
forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> m Bool
check GenericSolverM IO Rational
solver
  Bool -> IO ()
forall a. Show a => a -> IO ()
print Bool
ret
  GenericSolverM IO Rational -> IO ()
forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> m ()
dump GenericSolverM IO Rational
solver

  Model
m <- GenericSolverM IO Rational -> IO Model
forall v (m :: * -> *).
(SolverValue v, PrimMonad m) =>
GenericSolverM m v -> m Model
forall (m :: * -> *).
PrimMonad m =>
GenericSolverM m Rational -> m Model
getModel GenericSolverM IO Rational
solver
  Model -> IO ()
forall a. Show a => a -> IO ()
print Model
m

dumpSize :: forall m v. PrimMonad m => SolverValue v => GenericSolverM m v -> m ()
dumpSize :: forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> m ()
dumpSize GenericSolverM m v
solver = do
  IntMap (Expr Rational)
t <- MutVar (PrimState m) (IntMap (Expr Rational))
-> m (IntMap (Expr Rational))
forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> m a
readMutVar (GenericSolverM m v -> MutVar (PrimState m) (IntMap (Expr Rational))
forall (m :: * -> *) v.
GenericSolverM m v -> MutVar (PrimState m) (IntMap (Expr Rational))
svTableau GenericSolverM m v
solver)
  let nrows :: Int
nrows = IntMap (Expr Rational) -> Int
forall a. IntMap a -> Int
IntMap.size IntMap (Expr Rational)
t Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1 -- -1 is objVar
  [Int]
xs <- GenericSolverM m v -> m [Int]
forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> m [Int]
variables GenericSolverM m v
solver
  let ncols :: Int
ncols = [Int] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Int]
xs Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
nrows
  let nnz :: Int
nnz = [Int] -> Int
forall a. Num a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum [Model -> Int
forall a. IntMap a -> Int
IntMap.size (Model -> Int) -> Model -> Int
forall a b. (a -> b) -> a -> b
$ Expr Rational -> Model
forall r. Expr r -> IntMap r
LA.coeffMap Expr Rational
xi_def | (Int
xi,Expr Rational
xi_def) <- IntMap (Expr Rational) -> [(Int, Expr Rational)]
forall a. IntMap a -> [(Int, a)]
IntMap.toList IntMap (Expr Rational)
t, Int
xi Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Int
objVar]
  GenericSolverM m v -> String -> m ()
forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> String -> m ()
log GenericSolverM m v
solver (String -> m ()) -> String -> m ()
forall a b. (a -> b) -> a -> b
$ String -> Int -> Int -> Int -> String
forall r. PrintfType r => String -> r
printf String
"%d rows, %d columns, %d non-zeros" Int
nrows Int
ncols Int
nnz

dump :: PrimMonad m => SolverValue v => GenericSolverM m v -> m ()
dump :: forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> m ()
dump GenericSolverM m v
solver = do
  GenericSolverM m v -> String -> m ()
forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> String -> m ()
log GenericSolverM m v
solver String
"============="

  GenericSolverM m v -> String -> m ()
forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> String -> m ()
log GenericSolverM m v
solver String
"Tableau:"
  IntMap (Expr Rational)
t <- MutVar (PrimState m) (IntMap (Expr Rational))
-> m (IntMap (Expr Rational))
forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> m a
readMutVar (GenericSolverM m v -> MutVar (PrimState m) (IntMap (Expr Rational))
forall (m :: * -> *) v.
GenericSolverM m v -> MutVar (PrimState m) (IntMap (Expr Rational))
svTableau GenericSolverM m v
solver)
  GenericSolverM m v -> String -> m ()
forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> String -> m ()
log GenericSolverM m v
solver (String -> m ()) -> String -> m ()
forall a b. (a -> b) -> a -> b
$ String -> ShowS
forall r. PrintfType r => String -> r
printf String
"obj = %s" (Expr Rational -> String
forall a. Show a => a -> String
show (IntMap (Expr Rational)
t IntMap (Expr Rational) -> Int -> Expr Rational
forall a. IntMap a -> Int -> a
IntMap.! Int
objVar))
  [(Int, Expr Rational)] -> ((Int, Expr Rational) -> m ()) -> m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (IntMap (Expr Rational) -> [(Int, Expr Rational)]
forall a. IntMap a -> [(Int, a)]
IntMap.toList IntMap (Expr Rational)
t) (((Int, Expr Rational) -> m ()) -> m ())
-> ((Int, Expr Rational) -> m ()) -> m ()
forall a b. (a -> b) -> a -> b
$ \(Int
xi, Expr Rational
e) -> do
    Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Int
xi Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Int
objVar) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ GenericSolverM m v -> String -> m ()
forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> String -> m ()
log GenericSolverM m v
solver (String -> m ()) -> String -> m ()
forall a b. (a -> b) -> a -> b
$ String -> Int -> ShowS
forall r. PrintfType r => String -> r
printf String
"x%d = %s" Int
xi (Expr Rational -> String
forall a. Show a => a -> String
show Expr Rational
e)

  GenericSolverM m v -> String -> m ()
forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> String -> m ()
log GenericSolverM m v
solver String
""

  GenericSolverM m v -> String -> m ()
forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> String -> m ()
log GenericSolverM m v
solver String
"Assignments and Bounds:"
  v
objVal <- GenericSolverM m v -> Int -> m v
forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> Int -> m v
getValue GenericSolverM m v
solver Int
objVar
  GenericSolverM m v -> String -> m ()
forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> String -> m ()
log GenericSolverM m v
solver (String -> m ()) -> String -> m ()
forall a b. (a -> b) -> a -> b
$ String -> ShowS
forall r. PrintfType r => String -> r
printf String
"beta(obj) = %s" (Bool -> v -> String
forall v. SolverValue v => Bool -> v -> String
showValue Bool
True v
objVal)
  [Int]
xs <- GenericSolverM m v -> m [Int]
forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> m [Int]
variables GenericSolverM m v
solver
  [Int] -> (Int -> m ()) -> m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [Int]
xs ((Int -> m ()) -> m ()) -> (Int -> m ()) -> m ()
forall a b. (a -> b) -> a -> b
$ \Int
x -> do
    Bound v
l <- GenericSolverM m v -> Int -> m (Bound v)
forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> Int -> m (Bound v)
getLB GenericSolverM m v
solver Int
x
    Bound v
u <- GenericSolverM m v -> Int -> m (Bound v)
forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> Int -> m (Bound v)
getUB GenericSolverM m v
solver Int
x
    v
v <- GenericSolverM m v -> Int -> m v
forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> Int -> m v
getValue GenericSolverM m v
solver Int
x
    let f :: Maybe (v, b) -> String
f Maybe (v, b)
Nothing = String
"Nothing"
        f (Just (v
x,b
_)) = Bool -> v -> String
forall v. SolverValue v => Bool -> v -> String
showValue Bool
True v
x
    GenericSolverM m v -> String -> m ()
forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> String -> m ()
log GenericSolverM m v
solver (String -> m ()) -> String -> m ()
forall a b. (a -> b) -> a -> b
$ String -> Int -> String -> String -> Int -> ShowS
forall r. PrintfType r => String -> r
printf String
"beta(x%d) = %s; %s <= x%d <= %s" Int
x (Bool -> v -> String
forall v. SolverValue v => Bool -> v -> String
showValue Bool
True v
v) (Bound v -> String
forall {v} {b}. SolverValue v => Maybe (v, b) -> String
f Bound v
l) Int
x (Bound v -> String
forall {v} {b}. SolverValue v => Maybe (v, b) -> String
f Bound v
u)

  GenericSolverM m v -> String -> m ()
forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> String -> m ()
log GenericSolverM m v
solver String
""
  GenericSolverM m v -> String -> m ()
forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> String -> m ()
log GenericSolverM m v
solver String
"Status:"
  Bool
is_fea <- GenericSolverM m v -> m Bool
forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> m Bool
isFeasible GenericSolverM m v
solver
  Bool
is_opt <- GenericSolverM m v -> m Bool
forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> m Bool
isOptimal GenericSolverM m v
solver
  GenericSolverM m v -> String -> m ()
forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> String -> m ()
log GenericSolverM m v
solver (String -> m ()) -> String -> m ()
forall a b. (a -> b) -> a -> b
$ String -> ShowS
forall r. PrintfType r => String -> r
printf String
"Feasible: %s" (Bool -> String
forall a. Show a => a -> String
show Bool
is_fea)
  GenericSolverM m v -> String -> m ()
forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> String -> m ()
log GenericSolverM m v
solver (String -> m ()) -> String -> m ()
forall a b. (a -> b) -> a -> b
$ String -> ShowS
forall r. PrintfType r => String -> r
printf String
"Optimal: %s" (Bool -> String
forall a. Show a => a -> String
show Bool
is_opt)

  GenericSolverM m v -> String -> m ()
forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> String -> m ()
log GenericSolverM m v
solver String
"============="

checkFeasibility :: (PrimMonad m, SolverValue v) => GenericSolverM m v -> m ()
checkFeasibility :: forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> m ()
checkFeasibility GenericSolverM m v
_ | Bool
True = () -> m ()
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
checkFeasibility GenericSolverM m v
solver = do
  [Int]
xs <- GenericSolverM m v -> m [Int]
forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> m [Int]
variables GenericSolverM m v
solver
  [Int] -> (Int -> m ()) -> m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [Int]
xs ((Int -> m ()) -> m ()) -> (Int -> m ()) -> m ()
forall a b. (a -> b) -> a -> b
$ \Int
x -> do
    v
v <- GenericSolverM m v -> Int -> m v
forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> Int -> m v
getValue GenericSolverM m v
solver Int
x
    Bound v
l <- GenericSolverM m v -> Int -> m (Bound v)
forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> Int -> m (Bound v)
getLB GenericSolverM m v
solver Int
x
    Bound v
u <- GenericSolverM m v -> Int -> m (Bound v)
forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> Int -> m (Bound v)
getUB GenericSolverM m v
solver Int
x
    let f :: Maybe (v, b) -> String
f Maybe (v, b)
Nothing = String
"Nothing"
        f (Just (v
x,b
_)) = Bool -> v -> String
forall v. SolverValue v => Bool -> v -> String
showValue Bool
True v
x
    Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Bound v -> v -> Bool
forall v. SolverValue v => Bound v -> v -> Bool
testLB Bound v
l v
v) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$
      String -> m ()
forall a. HasCallStack => String -> a
error (String -> String -> Int -> Int -> ShowS
forall r. PrintfType r => String -> r
printf String
"(%s) <= x%d is violated; x%d = (%s)" (Bound v -> String
forall {v} {b}. SolverValue v => Maybe (v, b) -> String
f Bound v
l) Int
x Int
x (Bool -> v -> String
forall v. SolverValue v => Bool -> v -> String
showValue Bool
True v
v))
    Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Bound v -> v -> Bool
forall v. SolverValue v => Bound v -> v -> Bool
testUB Bound v
u v
v) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$
      String -> m ()
forall a. HasCallStack => String -> a
error (String -> Int -> String -> Int -> ShowS
forall r. PrintfType r => String -> r
printf String
"x%d <= (%s) is violated; x%d = (%s)" Int
x (Bound v -> String
forall {v} {b}. SolverValue v => Maybe (v, b) -> String
f Bound v
u) Int
x (Bool -> v -> String
forall v. SolverValue v => Bool -> v -> String
showValue Bool
True v
v))
    () -> m ()
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ()

checkNBFeasibility :: (PrimMonad m, SolverValue v) => GenericSolverM m v -> m ()
checkNBFeasibility :: forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> m ()
checkNBFeasibility GenericSolverM m v
_ | Bool
True = () -> m ()
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
checkNBFeasibility GenericSolverM m v
solver = do
  [Int]
xs <- GenericSolverM m v -> m [Int]
forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> m [Int]
variables GenericSolverM m v
solver
  [Int] -> (Int -> m ()) -> m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [Int]
xs ((Int -> m ()) -> m ()) -> (Int -> m ()) -> m ()
forall a b. (a -> b) -> a -> b
$ \Int
x -> do
    Bool
b <- GenericSolverM m v -> Int -> m Bool
forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> Int -> m Bool
isNonBasicVariable GenericSolverM m v
solver Int
x
    Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
b (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ do
      v
v <- GenericSolverM m v -> Int -> m v
forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> Int -> m v
getValue GenericSolverM m v
solver Int
x
      Bound v
l <- GenericSolverM m v -> Int -> m (Bound v)
forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> Int -> m (Bound v)
getLB GenericSolverM m v
solver Int
x
      Bound v
u <- GenericSolverM m v -> Int -> m (Bound v)
forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> Int -> m (Bound v)
getUB GenericSolverM m v
solver Int
x
      let f :: Maybe (v, b) -> String
f Maybe (v, b)
Nothing = String
"Nothing"
          f (Just (v
x,b
_)) = Bool -> v -> String
forall v. SolverValue v => Bool -> v -> String
showValue Bool
True v
x
      Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Bound v -> v -> Bool
forall v. SolverValue v => Bound v -> v -> Bool
testLB Bound v
l v
v) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$
        String -> m ()
forall a. HasCallStack => String -> a
error (String -> String -> Int -> Int -> ShowS
forall r. PrintfType r => String -> r
printf String
"checkNBFeasibility: (%s) <= x%d is violated; x%d = (%s)" (Bound v -> String
forall {v} {b}. SolverValue v => Maybe (v, b) -> String
f Bound v
l) Int
x Int
x (Bool -> v -> String
forall v. SolverValue v => Bool -> v -> String
showValue Bool
True v
v))
      Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Bound v -> v -> Bool
forall v. SolverValue v => Bound v -> v -> Bool
testUB Bound v
u v
v) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$
        String -> m ()
forall a. HasCallStack => String -> a
error (String -> Int -> String -> Int -> ShowS
forall r. PrintfType r => String -> r
printf String
"checkNBFeasibility: x%d <= (%s) is violated; x%d = (%s)" Int
x (Bound v -> String
forall {v} {b}. SolverValue v => Maybe (v, b) -> String
f Bound v
u) Int
x (Bool -> v -> String
forall v. SolverValue v => Bool -> v -> String
showValue Bool
True v
v))

checkOptimality :: (PrimMonad m, SolverValue v) => GenericSolverM m v -> m ()
checkOptimality :: forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> m ()
checkOptimality GenericSolverM m v
_ | Bool
True = () -> m ()
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
checkOptimality GenericSolverM m v
solver = do
  Maybe (Rational, Int)
ret <- GenericSolverM m v -> m (Maybe (Rational, Int))
forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> m (Maybe (Rational, Int))
selectEnteringVariable GenericSolverM m v
solver
  case Maybe (Rational, Int)
ret of
    Maybe (Rational, Int)
Nothing -> () -> m ()
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return () -- optimal
    Just (Rational
_,Int
x) -> String -> m ()
forall a. HasCallStack => String -> a
error (String -> Int -> String
forall r. PrintfType r => String -> r
printf String
"checkOptimality: not optimal (x%d can be changed)" Int
x)