{-# 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 <- forall (m :: * -> *) a.
PrimMonad m =>
a -> m (MutVar (PrimState m) a)
newMutVar (forall a. Int -> a -> IntMap a
IntMap.singleton Int
objVar forall v. AdditiveGroup v => v
zeroV)
  MutVar (PrimState m) (IntMap (v, ConstrIDSet))
l <- forall (m :: * -> *) a.
PrimMonad m =>
a -> m (MutVar (PrimState m) a)
newMutVar forall a. IntMap a
IntMap.empty
  MutVar (PrimState m) (IntMap (v, ConstrIDSet))
u <- forall (m :: * -> *) a.
PrimMonad m =>
a -> m (MutVar (PrimState m) a)
newMutVar forall a. IntMap a
IntMap.empty
  MutVar (PrimState m) (IntMap v)
m <- forall (m :: * -> *) a.
PrimMonad m =>
a -> m (MutVar (PrimState m) a)
newMutVar (forall a. Int -> a -> IntMap a
IntMap.singleton Int
objVar forall v. AdditiveGroup v => v
zeroV)
  MutVar (PrimState m) (Maybe ConstrIDSet)
e <- forall (m :: * -> *) a.
PrimMonad m =>
a -> m (MutVar (PrimState m) a)
newMutVar forall a. Monoid a => a
mempty
  MutVar (PrimState m) Int
v <- forall (m :: * -> *) a.
PrimMonad m =>
a -> m (MutVar (PrimState m) a)
newMutVar Int
0
  MutVar (PrimState m) OptDir
dir <- forall (m :: * -> *) a.
PrimMonad m =>
a -> m (MutVar (PrimState m) a)
newMutVar OptDir
OptMin
  MutVar (PrimState m) (Map (Expr Rational) Int)
defs <- forall (m :: * -> *) a.
PrimMonad m =>
a -> m (MutVar (PrimState m) a)
newMutVar forall k a. Map k a
Map.empty
  MutVar (PrimState m) (Maybe (String -> m ()))
logger <- forall (m :: * -> *) a.
PrimMonad m =>
a -> m (MutVar (PrimState m) a)
newMutVar forall a. Maybe a
Nothing
  MutVar (PrimState m) (Maybe (GenericSolverM m v -> m :~> m))
rectm <- forall (m :: * -> *) a.
PrimMonad m =>
a -> m (MutVar (PrimState m) a)
newMutVar forall a. Maybe a
Nothing
  MutVar (PrimState m) Config
config <- forall (m :: * -> *) a.
PrimMonad m =>
a -> m (MutVar (PrimState m) a)
newMutVar forall a. Default a => a
def
  MutVar (PrimState m) Int
npivot <- forall (m :: * -> *) a.
PrimMonad m =>
a -> m (MutVar (PrimState m) a)
newMutVar Int
0
  MutVar (PrimState m) [BacktrackPoint m v]
bps <- forall (m :: * -> *) a.
PrimMonad m =>
a -> m (MutVar (PrimState m) a)
newMutVar []
  forall (m :: * -> *) a. Monad m => a -> m a
return 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      <- forall (m :: * -> *) a.
PrimMonad m =>
a -> m (MutVar (PrimState m) a)
newMutVar forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> m a
readMutVar (forall (m :: * -> *) v.
GenericSolverM m v -> MutVar (PrimState m) (IntMap (Expr Rational))
svTableau GenericSolverM m v
solver)
  MutVar (PrimState m) (IntMap (v, ConstrIDSet))
l      <- forall (m :: * -> *) a.
PrimMonad m =>
a -> m (MutVar (PrimState m) a)
newMutVar forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> m a
readMutVar (forall (m :: * -> *) v.
GenericSolverM m v
-> MutVar (PrimState m) (IntMap (v, ConstrIDSet))
svLB GenericSolverM m v
solver)
  MutVar (PrimState m) (IntMap (v, ConstrIDSet))
u      <- forall (m :: * -> *) a.
PrimMonad m =>
a -> m (MutVar (PrimState m) a)
newMutVar forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> m a
readMutVar (forall (m :: * -> *) v.
GenericSolverM m v
-> MutVar (PrimState m) (IntMap (v, ConstrIDSet))
svUB GenericSolverM m v
solver)
  MutVar (PrimState m) (IntMap v)
m      <- forall (m :: * -> *) a.
PrimMonad m =>
a -> m (MutVar (PrimState m) a)
newMutVar forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> m a
readMutVar (forall (m :: * -> *) v.
GenericSolverM m v -> MutVar (PrimState m) (IntMap v)
svModel GenericSolverM m v
solver)
  MutVar (PrimState m) (Maybe ConstrIDSet)
e      <- forall (m :: * -> *) a.
PrimMonad m =>
a -> m (MutVar (PrimState m) a)
newMutVar forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> m a
readMutVar (forall (m :: * -> *) v.
GenericSolverM m v -> MutVar (PrimState m) (Maybe ConstrIDSet)
svExplanation GenericSolverM m v
solver)
  MutVar (PrimState m) Int
v      <- forall (m :: * -> *) a.
PrimMonad m =>
a -> m (MutVar (PrimState m) a)
newMutVar forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> m a
readMutVar (forall (m :: * -> *) v.
GenericSolverM m v -> MutVar (PrimState m) Int
svVCnt GenericSolverM m v
solver)
  MutVar (PrimState m) OptDir
dir    <- forall (m :: * -> *) a.
PrimMonad m =>
a -> m (MutVar (PrimState m) a)
newMutVar forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> m a
readMutVar (forall (m :: * -> *) v.
GenericSolverM m v -> MutVar (PrimState m) OptDir
svOptDir GenericSolverM m v
solver)
  MutVar (PrimState m) (Map (Expr Rational) Int)
defs   <- forall (m :: * -> *) a.
PrimMonad m =>
a -> m (MutVar (PrimState m) a)
newMutVar forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> m a
readMutVar (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 <- forall (m :: * -> *) a.
PrimMonad m =>
a -> m (MutVar (PrimState m) a)
newMutVar forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> m a
readMutVar (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  <- forall (m :: * -> *) a.
PrimMonad m =>
a -> m (MutVar (PrimState m) a)
newMutVar forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> m a
readMutVar (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 <- forall (m :: * -> *) a.
PrimMonad m =>
a -> m (MutVar (PrimState m) a)
newMutVar forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> m a
readMutVar (forall (m :: * -> *) v.
GenericSolverM m v -> MutVar (PrimState m) Config
svConfig GenericSolverM m v
solver)
  MutVar (PrimState m) Int
npivot <- forall (m :: * -> *) a.
PrimMonad m =>
a -> m (MutVar (PrimState m) a)
newMutVar forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> m a
readMutVar (forall (m :: * -> *) v.
GenericSolverM m v -> MutVar (PrimState m) Int
svNPivot GenericSolverM m v
solver)
  MutVar (PrimState m) [BacktrackPoint m v]
bps    <- forall (m :: * -> *) a.
PrimMonad m =>
a -> m (MutVar (PrimState m) a)
newMutVar forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall (m :: * -> *) v.
PrimMonad m =>
BacktrackPoint m v -> m (BacktrackPoint m v)
cloneBacktrackPoint forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> m a
readMutVar (forall (m :: * -> *) v.
GenericSolverM m v -> MutVar (PrimState m) [BacktrackPoint m v]
svBacktrackPoints GenericSolverM m v
solver)
  forall (m :: * -> *) a. Monad m => a -> m a
return 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 = 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 = forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> m (RawModel v)
getRawModel

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

boundExplanation :: SolverValue v => Bound v -> ConstrIDSet
boundExplanation :: forall v. SolverValue v => Bound v -> ConstrIDSet
boundExplanation = forall b a. b -> (a -> b) -> Maybe a -> b
maybe forall a. Monoid a => a
mempty 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 forall v. AdditiveGroup v => v -> v -> v
^+^ v
a2
      cs3 :: ConstrIDSet
cs3 = ConstrIDSet -> ConstrIDSet -> ConstrIDSet
IntSet.union ConstrIDSet
cs1 ConstrIDSet
cs2
  seq :: forall a b. a -> b -> b
seq v
a3 forall a b. (a -> b) -> a -> b
$ seq :: forall a b. a -> b -> b
seq ConstrIDSet
cs3 forall a b. (a -> b) -> a -> b
$ 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 = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Scalar v
c forall v. VectorSpace v => Scalar v -> v -> v
*^) forall (a :: * -> * -> *) b c b' c'.
Arrow a =>
a b c -> a b' c' -> a (b, b') (c, c')
*** forall a. a -> a
id)

data Config
  = Config
  { Config -> PivotStrategy
configPivotStrategy :: !PivotStrategy
  , Config -> Bool
configEnableBoundTightening :: !Bool
  } deriving (Int -> Config -> ShowS
[Config] -> ShowS
Config -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Config] -> ShowS
$cshowList :: [Config] -> ShowS
show :: Config -> String
$cshow :: Config -> String
showsPrec :: Int -> Config -> ShowS
$cshowsPrec :: Int -> Config -> ShowS
Show, Config -> Config -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Config -> Config -> Bool
$c/= :: Config -> Config -> Bool
== :: Config -> Config -> Bool
$c== :: Config -> Config -> Bool
Eq, Eq 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
min :: Config -> Config -> Config
$cmin :: Config -> Config -> Config
max :: Config -> Config -> Config
$cmax :: Config -> Config -> Config
>= :: Config -> Config -> Bool
$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
compare :: Config -> Config -> Ordering
$ccompare :: Config -> Config -> Ordering
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 = forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> a -> m ()
writeMutVar (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 = forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> m a
readMutVar (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 = forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> (a -> a) -> m ()
modifyMutVar' (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
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: PivotStrategy -> PivotStrategy -> Bool
$c/= :: PivotStrategy -> PivotStrategy -> Bool
== :: PivotStrategy -> PivotStrategy -> Bool
$c== :: PivotStrategy -> PivotStrategy -> Bool
Eq, Eq 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
min :: PivotStrategy -> PivotStrategy -> PivotStrategy
$cmin :: PivotStrategy -> PivotStrategy -> PivotStrategy
max :: PivotStrategy -> PivotStrategy -> PivotStrategy
$cmax :: PivotStrategy -> PivotStrategy -> PivotStrategy
>= :: PivotStrategy -> PivotStrategy -> Bool
$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
compare :: PivotStrategy -> PivotStrategy -> Ordering
$ccompare :: PivotStrategy -> PivotStrategy -> Ordering
Ord, Int -> PivotStrategy
PivotStrategy -> Int
PivotStrategy -> [PivotStrategy]
PivotStrategy -> PivotStrategy
PivotStrategy -> PivotStrategy -> [PivotStrategy]
PivotStrategy -> PivotStrategy -> PivotStrategy -> [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
enumFromThenTo :: PivotStrategy -> PivotStrategy -> PivotStrategy -> [PivotStrategy]
$cenumFromThenTo :: PivotStrategy -> PivotStrategy -> PivotStrategy -> [PivotStrategy]
enumFromTo :: PivotStrategy -> PivotStrategy -> [PivotStrategy]
$cenumFromTo :: PivotStrategy -> PivotStrategy -> [PivotStrategy]
enumFromThen :: PivotStrategy -> PivotStrategy -> [PivotStrategy]
$cenumFromThen :: PivotStrategy -> PivotStrategy -> [PivotStrategy]
enumFrom :: PivotStrategy -> [PivotStrategy]
$cenumFrom :: PivotStrategy -> [PivotStrategy]
fromEnum :: PivotStrategy -> Int
$cfromEnum :: PivotStrategy -> Int
toEnum :: Int -> PivotStrategy
$ctoEnum :: Int -> PivotStrategy
pred :: PivotStrategy -> PivotStrategy
$cpred :: PivotStrategy -> PivotStrategy
succ :: PivotStrategy -> PivotStrategy
$csucc :: PivotStrategy -> PivotStrategy
Enum, PivotStrategy
forall a. a -> a -> Bounded a
maxBound :: PivotStrategy
$cmaxBound :: PivotStrategy
minBound :: PivotStrategy
$cminBound :: PivotStrategy
Bounded, Int -> PivotStrategy -> ShowS
[PivotStrategy] -> ShowS
PivotStrategy -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [PivotStrategy] -> ShowS
$cshowList :: [PivotStrategy] -> ShowS
show :: PivotStrategy -> String
$cshow :: PivotStrategy -> String
showsPrec :: Int -> PivotStrategy -> ShowS
$cshowsPrec :: Int -> PivotStrategy -> ShowS
Show, ReadPrec [PivotStrategy]
ReadPrec PivotStrategy
Int -> ReadS PivotStrategy
ReadS [PivotStrategy]
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [PivotStrategy]
$creadListPrec :: ReadPrec [PivotStrategy]
readPrec :: ReadPrec PivotStrategy
$creadPrec :: ReadPrec PivotStrategy
readList :: ReadS [PivotStrategy]
$creadList :: ReadS [PivotStrategy]
readsPrec :: Int -> ReadS PivotStrategy
$creadsPrec :: Int -> ReadS 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 forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
toLower String
s of
    String
"bland-rule" -> forall a. a -> Maybe a
Just PivotStrategy
PivotStrategyBlandRule
    String
"largest-coefficient" -> forall a. a -> Maybe a
Just PivotStrategy
PivotStrategyLargestCoefficient
    String
_ -> 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 = forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> (Config -> Config) -> m ()
modifyConfig GenericSolverM m v
solver forall a b. (a -> b) -> a -> b
$ \Config
config ->
  Config
config{ configPivotStrategy :: PivotStrategy
configPivotStrategy = PivotStrategy
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 <- forall (m :: * -> *) a.
PrimMonad m =>
a -> m (MutVar (PrimState m) a)
newMutVar forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> m a
readMutVar (forall (m :: * -> *) v.
BacktrackPoint m v -> MutVar (PrimState m) (IntMap (Bound v))
bpSavedLB BacktrackPoint m v
bp)
  MutVar (PrimState m) (IntMap (Bound v))
ubs <- forall (m :: * -> *) a.
PrimMonad m =>
a -> m (MutVar (PrimState m) a)
newMutVar forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> m a
readMutVar (forall (m :: * -> *) v.
BacktrackPoint m v -> MutVar (PrimState m) (IntMap (Bound v))
bpSavedUB BacktrackPoint m v
bp)
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ 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 <- forall (m :: * -> *) a.
PrimMonad m =>
a -> m (MutVar (PrimState m) a)
newMutVar forall a. IntMap a
IntMap.empty
  MutVar (PrimState m) (IntMap (Bound v))
savedUBs <- forall (m :: * -> *) a.
PrimMonad m =>
a -> m (MutVar (PrimState m) a)
newMutVar forall a. IntMap a
IntMap.empty
  IntMap (v, ConstrIDSet)
lbs <- forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> m a
readMutVar (forall (m :: * -> *) v.
GenericSolverM m v
-> MutVar (PrimState m) (IntMap (v, ConstrIDSet))
svLB GenericSolverM m v
solver)
  IntMap (v, ConstrIDSet)
ubs <- forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> m a
readMutVar (forall (m :: * -> *) v.
GenericSolverM m v
-> MutVar (PrimState m) (IntMap (v, ConstrIDSet))
svUB GenericSolverM m v
solver)
  forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> (a -> a) -> m ()
modifyMutVar (forall (m :: * -> *) v.
GenericSolverM m v -> MutVar (PrimState m) [BacktrackPoint m v]
svBacktrackPoints GenericSolverM m v
solver) (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 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 <- forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> m a
readMutVar (forall (m :: * -> *) v.
GenericSolverM m v -> MutVar (PrimState m) [BacktrackPoint m v]
svBacktrackPoints GenericSolverM m v
solver)
  case [BacktrackPoint m v]
bps of
    [] -> forall a. HasCallStack => String -> a
error String
"popBacktrackPoint: empty backtrack points"
    BacktrackPoint m v
bp : [BacktrackPoint m v]
bps' -> do
      IntMap (v, ConstrIDSet)
lbs <- forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> m a
readMutVar (forall (m :: * -> *) v.
GenericSolverM m v
-> MutVar (PrimState m) (IntMap (v, ConstrIDSet))
svLB GenericSolverM m v
solver)
      IntMap (Bound v)
savedLBs <- forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> m a
readMutVar (forall (m :: * -> *) v.
BacktrackPoint m v -> MutVar (PrimState m) (IntMap (Bound v))
bpSavedLB BacktrackPoint m v
bp)
      forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> a -> m ()
writeMutVar (forall (m :: * -> *) v.
GenericSolverM m v
-> MutVar (PrimState m) (IntMap (v, ConstrIDSet))
svLB GenericSolverM m v
solver) forall a b. (a -> b) -> a -> b
$ 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) forall a. a -> a
id (forall a b. a -> b -> a
const forall a. IntMap a
IntMap.empty) IntMap (v, ConstrIDSet)
lbs IntMap (Bound v)
savedLBs

      IntMap (v, ConstrIDSet)
ubs <- forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> m a
readMutVar (forall (m :: * -> *) v.
GenericSolverM m v
-> MutVar (PrimState m) (IntMap (v, ConstrIDSet))
svUB GenericSolverM m v
solver)
      IntMap (Bound v)
savedUBs <- forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> m a
readMutVar (forall (m :: * -> *) v.
BacktrackPoint m v -> MutVar (PrimState m) (IntMap (Bound v))
bpSavedUB BacktrackPoint m v
bp)
      forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> a -> m ()
writeMutVar (forall (m :: * -> *) v.
GenericSolverM m v
-> MutVar (PrimState m) (IntMap (v, ConstrIDSet))
svUB GenericSolverM m v
solver) forall a b. (a -> b) -> a -> b
$ 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) forall a. a -> a
id (forall a b. a -> b -> a
const forall a. IntMap a
IntMap.empty) IntMap (v, ConstrIDSet)
ubs IntMap (Bound v)
savedUBs

      forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> a -> m ()
writeMutVar (forall (m :: * -> *) v.
GenericSolverM m v -> MutVar (PrimState m) [BacktrackPoint m v]
svBacktrackPoints GenericSolverM m v
solver) [BacktrackPoint m v]
bps'
      forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> a -> m ()
writeMutVar (forall (m :: * -> *) v.
GenericSolverM m v -> MutVar (PrimState m) (Maybe ConstrIDSet)
svExplanation GenericSolverM m v
solver) 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 <- forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> m a
readMutVar (forall (m :: * -> *) v.
GenericSolverM m v -> MutVar (PrimState m) [BacktrackPoint m v]
svBacktrackPoints GenericSolverM m v
solver)
  case [BacktrackPoint m v]
bps of
    [] -> 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
  forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> (BacktrackPoint m v -> m ()) -> m ()
withBacktrackpoint GenericSolverM m v
solver forall a b. (a -> b) -> a -> b
$ \BacktrackPoint m v
bp -> do
    IntMap (Bound v)
saved <- forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> m a
readMutVar (forall (m :: * -> *) v.
BacktrackPoint m v -> MutVar (PrimState m) (IntMap (Bound v))
bpSavedLB BacktrackPoint m v
bp)
    if Int
v forall a. Int -> IntMap a -> Bool
`IntMap.member` IntMap (Bound v)
saved then
      forall (m :: * -> *) a. Monad m => a -> m a
return ()
    else do
      IntMap (v, ConstrIDSet)
lb <- forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> m a
readMutVar (forall (m :: * -> *) v.
GenericSolverM m v
-> MutVar (PrimState m) (IntMap (v, ConstrIDSet))
svLB GenericSolverM m v
solver)
      let old :: Bound v
old = forall a. Int -> IntMap a -> Maybe a
IntMap.lookup Int
v IntMap (v, ConstrIDSet)
lb
      seq :: forall a b. a -> b -> b
seq Bound v
old forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> a -> m ()
writeMutVar (forall (m :: * -> *) v.
BacktrackPoint m v -> MutVar (PrimState m) (IntMap (Bound v))
bpSavedLB BacktrackPoint m v
bp) (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
  forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> (BacktrackPoint m v -> m ()) -> m ()
withBacktrackpoint GenericSolverM m v
solver forall a b. (a -> b) -> a -> b
$ \BacktrackPoint m v
bp -> do
    IntMap (Bound v)
saved <- forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> m a
readMutVar (forall (m :: * -> *) v.
BacktrackPoint m v -> MutVar (PrimState m) (IntMap (Bound v))
bpSavedUB BacktrackPoint m v
bp)
    if Int
v forall a. Int -> IntMap a -> Bool
`IntMap.member` IntMap (Bound v)
saved then
      forall (m :: * -> *) a. Monad m => a -> m a
return ()
    else do
      IntMap (v, ConstrIDSet)
ub <- forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> m a
readMutVar (forall (m :: * -> *) v.
GenericSolverM m v
-> MutVar (PrimState m) (IntMap (v, ConstrIDSet))
svUB GenericSolverM m v
solver)
      let old :: Bound v
old = forall a. Int -> IntMap a -> Maybe a
IntMap.lookup Int
v IntMap (v, ConstrIDSet)
ub
      seq :: forall a b. a -> b -> b
seq Bound v
old forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> a -> m ()
writeMutVar (forall (m :: * -> *) v.
BacktrackPoint m v -> MutVar (PrimState m) (IntMap (Bound v))
bpSavedUB BacktrackPoint m v
bp) (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 <- forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> m a
readMutVar (forall (m :: * -> *) v.
GenericSolverM m v -> MutVar (PrimState m) Int
svVCnt GenericSolverM m v
solver)
  forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> a -> m ()
writeMutVar (forall (m :: * -> *) v.
GenericSolverM m v -> MutVar (PrimState m) Int
svVCnt GenericSolverM m v
solver) forall a b. (a -> b) -> a -> b
$! Int
vforall a. Num a => a -> a -> a
+Int
1
  forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> (a -> a) -> m ()
modifyMutVar (forall (m :: * -> *) v.
GenericSolverM m v -> MutVar (PrimState m) (IntMap v)
svModel GenericSolverM m v
solver) (forall a. Int -> a -> IntMap a -> IntMap a
IntMap.insert Int
v forall v. AdditiveGroup v => v
zeroV)
  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 = forall (m :: * -> *).
PrimMonad m =>
GenericSolverM m Rational -> Atom Rational -> Maybe Int -> m ()
assertAtom' GenericSolverM m Rational
solver Atom Rational
atom 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') <- 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  -> forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> Int -> v -> Maybe Int -> m ()
assertUpper' GenericSolverM m Rational
solver Int
v (forall v. SolverValue v => Rational -> v
toValue Rational
rhs') Maybe Int
cid
    RelOp
Ge  -> forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> Int -> v -> Maybe Int -> m ()
assertLower' GenericSolverM m Rational
solver Int
v (forall v. SolverValue v => Rational -> v
toValue Rational
rhs') Maybe Int
cid
    RelOp
Eql -> do
      forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> Int -> v -> Maybe Int -> m ()
assertLower' GenericSolverM m Rational
solver Int
v (forall v. SolverValue v => Rational -> v
toValue Rational
rhs') Maybe Int
cid
      forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> Int -> v -> Maybe Int -> m ()
assertUpper' GenericSolverM m Rational
solver Int
v (forall v. SolverValue v => Rational -> v
toValue Rational
rhs') Maybe Int
cid
    RelOp
_ -> forall a. HasCallStack => String -> a
error String
"unsupported"
  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 = forall (m :: * -> *).
PrimMonad m =>
GenericSolverM m (Delta Rational)
-> Atom Rational -> Maybe Int -> m ()
assertAtomEx' GenericSolverM m (Delta Rational)
solver Atom Rational
atom 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') <- 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  -> forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> Int -> v -> Maybe Int -> m ()
assertUpper' GenericSolverM m (Delta Rational)
solver Int
v (forall v. SolverValue v => Rational -> v
toValue Rational
rhs') Maybe Int
cid
    RelOp
Ge  -> forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> Int -> v -> Maybe Int -> m ()
assertLower' GenericSolverM m (Delta Rational)
solver Int
v (forall v. SolverValue v => Rational -> v
toValue Rational
rhs') Maybe Int
cid
    RelOp
Lt  -> forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> Int -> v -> Maybe Int -> m ()
assertUpper' GenericSolverM m (Delta Rational)
solver Int
v (forall v. SolverValue v => Rational -> v
toValue Rational
rhs' forall v. AdditiveGroup v => v -> v -> v
^-^ forall r. Num r => Delta r
delta) Maybe Int
cid
    RelOp
Gt  -> forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> Int -> v -> Maybe Int -> m ()
assertLower' GenericSolverM m (Delta Rational)
solver Int
v (forall v. SolverValue v => Rational -> v
toValue Rational
rhs' forall v. AdditiveGroup v => v -> v -> v
^+^ forall r. Num r => Delta r
delta) Maybe Int
cid
    RelOp
Eql -> do
      forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> Int -> v -> Maybe Int -> m ()
assertLower' GenericSolverM m (Delta Rational)
solver Int
v (forall v. SolverValue v => Rational -> v
toValue Rational
rhs') Maybe Int
cid
      forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> Int -> v -> Maybe Int -> m ()
assertUpper' GenericSolverM m (Delta Rational)
solver Int
v (forall v. SolverValue v => Rational -> v
toValue Rational
rhs') Maybe Int
cid
  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 forall r. Num r => Int -> Expr r -> (r, Expr r)
LA.extract Int
LA.unitVar (Expr Rational
lhs forall v. AdditiveGroup v => v -> v -> v
^-^ Expr Rational
rhs) of
          (Rational
n,Expr Rational
e) -> (Expr Rational
e, -Rational
n)
  case forall r. Expr r -> [(r, Int)]
LA.terms Expr Rational
lhs' of
    [(Rational
1,Int
v)] -> forall (m :: * -> *) a. Monad m => a -> m a
return (Int
v, RelOp
op, Rational
rhs')
    [(-1,Int
v)] -> 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 <- forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> m a
readMutVar (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
c forall v. VectorSpace v => Scalar v -> v -> v
*^ Rational
rhs'
          op'' :: RelOp
op''  = if Rational
c forall a. Ord a => a -> a -> Bool
< Rational
0 then RelOp -> RelOp
flipOp RelOp
op else RelOp
op
      case 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
          forall (m :: * -> *) a. Monad m => a -> m a
return (Int
v,RelOp
op'',Rational
rhs'')
        Maybe Int
Nothing -> do
          Int
v <- forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> m Int
newVar GenericSolverM m v
solver
          forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> Int -> Expr Rational -> m ()
setRow GenericSolverM m v
solver Int
v Expr Rational
lhs''
          forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> (a -> a) -> m ()
modifyMutVar (forall (m :: * -> *) v.
GenericSolverM m v
-> MutVar (PrimState m) (Map (Expr Rational) Int)
svDefDB GenericSolverM m v
solver) forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Expr Rational
lhs'' Int
v
          case forall r. Num r => Expr r -> Maybe r
LA.asConst Expr Rational
lhs'' of
            Just Rational
0 -> do
              forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> (a -> a) -> m ()
modifyMutVar (forall (m :: * -> *) v.
GenericSolverM m v
-> MutVar (PrimState m) (IntMap (v, ConstrIDSet))
svLB GenericSolverM m v
solver) (forall a. Int -> a -> IntMap a -> IntMap a
IntMap.insert Int
v (forall v. SolverValue v => Rational -> v
toValue Rational
0, forall a. Monoid a => a
mempty))
              forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> (a -> a) -> m ()
modifyMutVar (forall (m :: * -> *) v.
GenericSolverM m v
-> MutVar (PrimState m) (IntMap (v, ConstrIDSet))
svUB GenericSolverM m v
solver) (forall a. Int -> a -> IntMap a -> IntMap a
IntMap.insert Int
v (forall v. SolverValue v => Rational -> v
toValue Rational
0, forall a. Monoid a => a
mempty))
            Maybe Rational
_ -> do
              Config
config <- forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> m Config
getConfig GenericSolverM m v
solver
              forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Config -> Bool
configEnableBoundTightening Config
config) forall a b. (a -> b) -> a -> b
$ do
                forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> Int -> m ()
tightenBounds GenericSolverM m v
solver Int
v
          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
c forall v. VectorSpace v => Scalar v -> v -> v
*^ Expr Rational
e)
      where
        c :: Rational
c = Rational
c1 forall a. Num a => a -> a -> a
* Rational
c2
        c1 :: Rational
c1 = forall a b. (Integral a, Num b) => a -> b
fromIntegral forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' forall a. Integral a => a -> a -> a
lcm Integer
1 [forall a. Ratio a -> a
denominator Rational
c | (Rational
c, Int
_) <- forall r. Expr r -> [(r, Int)]
LA.terms Expr Rational
e]
        c2 :: Rational
c2 = forall a. Num a => a -> a
signum forall a b. (a -> b) -> a -> b
$ forall a. [a] -> a
head ([Rational
c | (Rational
c,Int
x) <- forall r. Expr r -> [(r, Int)]
LA.terms Expr Rational
e] 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 = forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> Int -> Bound v -> m ()
assertLB GenericSolverM m v
solver Int
x (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 = forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> Int -> Bound v -> m ()
assertLB GenericSolverM m v
solver Int
x (forall a. a -> Maybe a
Just (v
l, [Int] -> ConstrIDSet
IntSet.fromList (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 = 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 <- forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> Int -> m (Bound v)
getLB GenericSolverM m v
solver Int
x
  Maybe (v, ConstrIDSet)
u0 <- 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 forall a. Ord a => a -> a -> Bool
<= v
l0' -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
    (Maybe (v, ConstrIDSet)
_, Just (v
u0', ConstrIDSet
cidSet2)) | v
u0' forall a. Ord a => a -> a -> Bool
< v
l -> do
      forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> ConstrIDSet -> m ()
setExplanation GenericSolverM m v
solver forall a b. (a -> b) -> a -> b
$ ConstrIDSet
cidSet ConstrIDSet -> ConstrIDSet -> ConstrIDSet
`IntSet.union` ConstrIDSet
cidSet2
    (Maybe (v, ConstrIDSet), Maybe (v, ConstrIDSet))
_ -> do
      forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> Int -> m ()
bpSaveLB GenericSolverM m v
solver Int
x
      forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> (a -> a) -> m ()
modifyMutVar (forall (m :: * -> *) v.
GenericSolverM m v
-> MutVar (PrimState m) (IntMap (v, ConstrIDSet))
svLB GenericSolverM m v
solver) (forall a. Int -> a -> IntMap a -> IntMap a
IntMap.insert Int
x (v
l, ConstrIDSet
cidSet))
      Bool
b <- forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> Int -> m Bool
isNonBasicVariable GenericSolverM m v
solver Int
x
      v
v <- forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> Int -> m v
getValue GenericSolverM m v
solver Int
x
      forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool
b Bool -> Bool -> Bool
&& Bool -> Bool
not (v
l forall a. Ord a => a -> a -> Bool
<= v
v)) forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> Int -> v -> m ()
update GenericSolverM m v
solver Int
x v
l
      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 = forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> Int -> Bound v -> m ()
assertUB GenericSolverM m v
solver Int
x (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 = forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> Int -> Bound v -> m ()
assertUB GenericSolverM m v
solver Int
x (forall a. a -> Maybe a
Just (v
u, [Int] -> ConstrIDSet
IntSet.fromList (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 = 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 <- forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> Int -> m (Bound v)
getLB GenericSolverM m v
solver Int
x
  Maybe (v, ConstrIDSet)
u0 <- 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' forall a. Ord a => a -> a -> Bool
<= v
u -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
    (Just (v
l0', ConstrIDSet
cidSet2), Maybe (v, ConstrIDSet)
_) | v
u forall a. Ord a => a -> a -> Bool
< v
l0' -> do
      forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> ConstrIDSet -> m ()
setExplanation GenericSolverM m v
solver forall a b. (a -> b) -> a -> b
$ ConstrIDSet
cidSet ConstrIDSet -> ConstrIDSet -> ConstrIDSet
`IntSet.union` ConstrIDSet
cidSet2
    (Maybe (v, ConstrIDSet), Maybe (v, ConstrIDSet))
_ -> do
      forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> Int -> m ()
bpSaveUB GenericSolverM m v
solver Int
x
      forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> (a -> a) -> m ()
modifyMutVar (forall (m :: * -> *) v.
GenericSolverM m v
-> MutVar (PrimState m) (IntMap (v, ConstrIDSet))
svUB GenericSolverM m v
solver) (forall a. Int -> a -> IntMap a -> IntMap a
IntMap.insert Int
x (v
u, ConstrIDSet
cidSet))
      Bool
b <- forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> Int -> m Bool
isNonBasicVariable GenericSolverM m v
solver Int
x
      v
v <- forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> Int -> m v
getValue GenericSolverM m v
solver Int
x
      forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool
b Bool -> Bool -> Bool
&& Bool -> Bool
not (v
v forall a. Ord a => a -> a -> Bool
<= v
u)) forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> Int -> v -> m ()
update GenericSolverM m v
solver Int
x v
u
      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 = 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 = 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
  forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> (a -> a) -> m ()
modifyMutVar (forall (m :: * -> *) v.
GenericSolverM m v -> MutVar (PrimState m) (IntMap (Expr Rational))
svTableau GenericSolverM m v
solver) forall a b. (a -> b) -> a -> b
$ \IntMap (Expr Rational)
t ->
    forall a. Int -> a -> IntMap a -> IntMap a
IntMap.insert Int
v (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
  forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> (a -> a) -> m ()
modifyMutVar (forall (m :: * -> *) v.
GenericSolverM m v -> MutVar (PrimState m) (IntMap v)
svModel GenericSolverM m v
solver) forall a b. (a -> b) -> a -> b
$ \IntMap v
m ->
    forall a. Int -> a -> IntMap a -> IntMap a
IntMap.insert Int
v (forall a. VectorSpace a => Model a -> a -> Expr (Scalar a) -> a
LA.evalLinear IntMap v
m (forall v. SolverValue v => Rational -> v
toValue Rational
1) Expr Rational
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 = forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> a -> m ()
writeMutVar (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 = forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> m a
readMutVar (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 = forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> m a
readMutVar (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 <- forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> m a
readMutVar (forall (m :: * -> *) v.
GenericSolverM m v -> MutVar (PrimState m) (IntMap (Expr Rational))
svTableau GenericSolverM m v
solver)
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Int
v 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 = forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM Bool -> Bool
not (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 <- forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> m [Int]
variables GenericSolverM m v
solver
  forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM forall (t :: * -> *). Foldable t => t Bool -> Bool
and forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [Int]
xs forall a b. (a -> b) -> a -> b
$ \Int
x -> do
    v
v <- forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> Int -> m v
getValue GenericSolverM m v
solver Int
x
    Bound v
l <- forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> Int -> m (Bound v)
getLB GenericSolverM m v
solver Int
x
    Bound v
u <- forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> Int -> m (Bound v)
getUB GenericSolverM m v
solver Int
x
    forall (m :: * -> *) a. Monad m => a -> m a
return (forall v. SolverValue v => Bound v -> v -> Bool
testLB Bound v
l v
v Bool -> Bool -> 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 <- forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> Int -> m (Expr Rational)
getRow GenericSolverM m v
solver Int
objVar
  Maybe (Rational, Int)
ret <- forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> m (Maybe (Rational, Int))
selectEnteringVariable GenericSolverM m v
solver
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$! 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 <- 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 -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
        Just Int
xi  -> do
          Bound v
li <- forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> Int -> m (Bound v)
getLB GenericSolverM m v
solver Int
xi
          Bound v
ui <- forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> Int -> m (Bound v)
getUB GenericSolverM m v
solver Int
xi
          Bool
isLBViolated <- do
            v
vi <- forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> Int -> m v
getValue GenericSolverM m v
solver Int
xi
            forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Bool -> Bool
not (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)
                       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)
                       forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> (Rational, Int) -> m Bool
canDecrease GenericSolverM m v
solver
          Expr Rational
xi_def <- forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> Int -> m (Expr Rational)
getRow GenericSolverM m v
solver Int
xi
          Maybe Int
r <- forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. (a, b) -> b
snd) forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a.
Monad m =>
(a -> m Bool) -> [a] -> m (Maybe a)
findM (Rational, Int) -> m Bool
q (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 <- forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (forall a. Monoid a => [a] -> a
mconcat forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map forall v. SolverValue v => Bound v -> ConstrIDSet
boundExplanation forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Bound v
c forall a. a -> [a] -> [a]
:)) forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (forall r. Expr r -> [(r, Int)]
LA.terms Expr Rational
xi_def) forall a b. (a -> b) -> a -> b
$ \(Rational
aij, Int
xj) -> do
                if Bool
isLBViolated then do
                  if Rational
aij forall a. Ord a => a -> a -> Bool
> Rational
0 then do
                    forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> Int -> m (Bound v)
getUB GenericSolverM m v
solver Int
xj
                  else do
                    forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> Int -> m (Bound v)
getLB GenericSolverM m v
solver Int
xj
                else do
                  if Rational
aij forall a. Ord a => a -> a -> Bool
> Rational
0 then do
                    forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> Int -> m (Bound v)
getLB GenericSolverM m v
solver Int
xj
                  else do
                    forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> Int -> m (Bound v)
getUB GenericSolverM m v
solver Int
xj
              forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> ConstrIDSet -> m ()
setExplanation GenericSolverM m v
solver ConstrIDSet
core
              forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
            Just Int
xj -> do
              forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> Int -> Int -> v -> m ()
pivotAndUpdate GenericSolverM m v
solver Int
xi Int
xj (forall a. HasCallStack => Maybe a -> a
fromJust forall a b. (a -> b) -> a -> b
$ forall v. SolverValue v => Bound v -> Maybe v
boundValue forall a b. (a -> b) -> a -> b
$ if Bool
isLBViolated then Bound v
li else Bound v
ui)
              Maybe ConstrIDSet
m <- forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> m a
readMutVar (forall (m :: * -> *) v.
GenericSolverM m v -> MutVar (PrimState m) (Maybe ConstrIDSet)
svExplanation GenericSolverM m v
solver)
              if forall a. Maybe a -> Bool
isJust Maybe ConstrIDSet
m then
                forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
              else
                m Bool
loop

  Maybe ConstrIDSet
m <- forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> m a
readMutVar (forall (m :: * -> *) v.
GenericSolverM m v -> MutVar (PrimState m) (Maybe ConstrIDSet)
svExplanation GenericSolverM m v
solver)
  case Maybe ConstrIDSet
m of
    Just ConstrIDSet
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
    Maybe ConstrIDSet
Nothing -> do
      forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> String -> m ()
log GenericSolverM m v
solver String
"check"
      Bool
result <- forall (m :: * -> *) v a.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> m a -> m a
recordTime GenericSolverM m v
solver m Bool
loop
      forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
result forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> m ()
checkFeasibility GenericSolverM m v
solver
      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 forall a. Eq a => a -> a -> Bool
== Int
objVar = forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
    p Int
xi = do
      Bound v
li <- forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> Int -> m (Bound v)
getLB GenericSolverM m v
solver Int
xi
      Bound v
ui <- forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> Int -> m (Bound v)
getUB GenericSolverM m v
solver Int
xi
      v
vi <- forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> Int -> m v
getValue GenericSolverM m v
solver Int
xi
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Bool -> Bool
not (forall v. SolverValue v => Bound v -> v -> Bool
testLB Bound v
li v
vi) Bool -> Bool -> Bool
|| Bool -> Bool
not (forall v. SolverValue v => Bound v -> v -> Bool
testUB Bound v
ui v
vi)
  [Int]
vs <- forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> m [Int]
basicVariables GenericSolverM m v
solver

  Config
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 ->
      forall (m :: * -> *) a.
Monad m =>
(a -> m Bool) -> [a] -> m (Maybe a)
findM Int -> m Bool
p [Int]
vs
    PivotStrategy
PivotStrategyLargestCoefficient -> do
      [Int]
xs <- forall (m :: * -> *) a.
Applicative m =>
(a -> m Bool) -> [a] -> m [a]
filterM Int -> m Bool
p [Int]
vs
      case [Int]
xs of
        [] -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
        [Int]
_ -> do
          [(Int, v)]
xs2 <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [Int]
xs forall a b. (a -> b) -> a -> b
$ \Int
xi -> do
              v
vi <- forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> Int -> m v
getValue GenericSolverM m v
solver Int
xi
              Bound v
li <- forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> Int -> m (Bound v)
getLB GenericSolverM m v
solver Int
xi
              Bound v
ui <- forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> Int -> m (Bound v)
getUB GenericSolverM m v
solver Int
xi
              if Bool -> Bool
not (forall v. SolverValue v => Bound v -> v -> Bool
testLB Bound v
li v
vi)
                then forall (m :: * -> *) a. Monad m => a -> m a
return (Int
xi, forall a. HasCallStack => Maybe a -> a
fromJust (forall v. SolverValue v => Bound v -> Maybe v
boundValue Bound v
li) forall v. AdditiveGroup v => v -> v -> v
^-^ v
vi)
                else forall (m :: * -> *) a. Monad m => a -> m a
return (Int
xi, v
vi forall v. AdditiveGroup v => v -> v -> v
^-^ forall a. HasCallStack => Maybe a -> a
fromJust (forall v. SolverValue v => Bound v -> Maybe v
boundValue Bound v
ui))
          forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a b. (a, b) -> a
fst forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a.
Foldable t =>
(a -> a -> Ordering) -> t a -> a
maximumBy (forall a b. Ord a => (b -> a) -> b -> b -> Ordering
comparing 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 <- forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> m a
readMutVar (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 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 forall a. Eq a => a -> a -> Bool
== Int
xk then do
          forall (m :: * -> *) a. Monad m => a -> m a
return (forall v. SolverValue v => Bound v -> Bound v -> Bound v
addBound Bound v
lb (forall a. a -> Maybe a
Just (forall v. SolverValue v => Rational -> v
toValue Rational
c, ConstrIDSet
IntSet.empty)), forall v. SolverValue v => Bound v -> Bound v -> Bound v
addBound Bound v
ub (forall a. a -> Maybe a
Just (forall v. SolverValue v => Rational -> v
toValue Rational
c, ConstrIDSet
IntSet.empty)))
        else do
          Bound v
lb_k <- forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> Int -> m (Bound v)
getLB GenericSolverM m v
solver Int
xk
          Bound v
ub_k <- forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> Int -> m (Bound v)
getUB GenericSolverM m v
solver Int
xk
          if Rational
c forall a. Ord a => a -> a -> Bool
> Rational
0 then do
            forall (m :: * -> *) a. Monad m => a -> m a
return (forall v. SolverValue v => Bound v -> Bound v -> Bound v
addBound Bound v
lb (forall v. SolverValue v => Scalar v -> Bound v -> Bound v
scaleBound Rational
c Bound v
lb_k), forall v. SolverValue v => Bound v -> Bound v -> Bound v
addBound Bound v
ub (forall v. SolverValue v => Scalar v -> Bound v -> Bound v
scaleBound Rational
c Bound v
ub_k))
          else do
            forall (m :: * -> *) a. Monad m => a -> m a
return (forall v. SolverValue v => Bound v -> Bound v -> Bound v
addBound Bound v
lb (forall v. SolverValue v => Scalar v -> Bound v -> Bound v
scaleBound Rational
c Bound v
ub_k), forall v. SolverValue v => Bound v -> Bound v -> Bound v
addBound Bound v
ub (forall v. SolverValue v => Scalar v -> Bound v -> Bound v
scaleBound Rational
c Bound v
lb_k))
  (Bound v
lb,Bound v
ub) <- 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 (forall a. a -> Maybe a
Just (forall v. AdditiveGroup v => v
zeroV, ConstrIDSet
IntSet.empty), forall a. a -> Maybe a
Just (forall v. AdditiveGroup v => v
zeroV, ConstrIDSet
IntSet.empty)) (forall r. Expr r -> [(r, Int)]
LA.terms Expr Rational
x_def)
  forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> Int -> Bound v -> m ()
assertLB GenericSolverM m v
solver Int
x Bound v
lb
  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
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [OptResult] -> ShowS
$cshowList :: [OptResult] -> ShowS
show :: OptResult -> String
$cshow :: OptResult -> String
showsPrec :: Int -> OptResult -> ShowS
$cshowsPrec :: Int -> OptResult -> ShowS
Show, OptResult -> OptResult -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: OptResult -> OptResult -> Bool
$c/= :: OptResult -> OptResult -> Bool
== :: OptResult -> OptResult -> Bool
$c== :: OptResult -> OptResult -> Bool
Eq, Eq OptResult
OptResult -> OptResult -> Bool
OptResult -> OptResult -> Ordering
OptResult -> OptResult -> OptResult
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: OptResult -> OptResult -> OptResult
$cmin :: OptResult -> OptResult -> OptResult
max :: OptResult -> OptResult -> OptResult
$cmax :: OptResult -> OptResult -> OptResult
>= :: OptResult -> OptResult -> Bool
$c>= :: OptResult -> OptResult -> Bool
> :: OptResult -> OptResult -> Bool
$c> :: OptResult -> OptResult -> Bool
<= :: OptResult -> OptResult -> Bool
$c<= :: OptResult -> OptResult -> Bool
< :: OptResult -> OptResult -> Bool
$c< :: OptResult -> OptResult -> Bool
compare :: OptResult -> OptResult -> Ordering
$ccompare :: OptResult -> OptResult -> Ordering
Ord)

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

instance Default Options where
  def :: Options
def =
    Options
    { objLimit :: Maybe Rational
objLimit = 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 <- forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> m Bool
isFeasible GenericSolverM m Rational
solver
    if Bool
is_fea then forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True else forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> m Bool
check GenericSolverM m Rational
solver
  if Bool -> Bool
not Bool
ret
    then forall (m :: * -> *) a. Monad m => a -> m a
return OptResult
Unsat -- unsat
    else do
      forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> String -> m ()
log GenericSolverM m Rational
solver String
"optimize"
      OptResult
result <- forall (m :: * -> *) v a.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> m a -> m a
recordTime GenericSolverM m Rational
solver m OptResult
loop
      forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (OptResult
result forall a. Eq a => a -> a -> Bool
== OptResult
Optimum) forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> m ()
checkOptimality GenericSolverM m Rational
solver
      forall (m :: * -> *) a. Monad m => a -> m a
return OptResult
result
  where
    loop :: m OptResult
    loop :: m OptResult
loop = do
      forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> m ()
checkFeasibility GenericSolverM m Rational
solver
      Maybe (Rational, Int)
ret <- 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 -> forall (m :: * -> *) a. Monad m => a -> m a
return OptResult
Optimum
       Just (Rational
c,Int
xj) -> do
         OptDir
dir <- forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> m OptDir
getOptDir GenericSolverM m Rational
solver
         Bool
r <- if OptDir
dirforall a. Eq a => a -> a -> Bool
==OptDir
OptMin
              then if Rational
c forall a. Ord a => a -> a -> Bool
> Rational
0
                then forall (m :: * -> *).
PrimMonad m =>
GenericSolverM m Rational -> Int -> m Bool
decreaseNB GenericSolverM m Rational
solver Int
xj -- xj を小さくして目的関数を小さくする
                else forall (m :: * -> *).
PrimMonad m =>
GenericSolverM m Rational -> Int -> m Bool
increaseNB GenericSolverM m Rational
solver Int
xj -- xj を大きくして目的関数を小さくする
              else if Rational
c forall a. Ord a => a -> a -> Bool
> Rational
0
                then forall (m :: * -> *).
PrimMonad m =>
GenericSolverM m Rational -> Int -> m Bool
increaseNB GenericSolverM m Rational
solver Int
xj -- xj を大きくして目的関数を大きくする
                else 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 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 <- forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> m Config
getConfig GenericSolverM m v
solver
  Expr Rational
obj_def <- 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 ->
      forall (m :: * -> *) a.
Monad m =>
(a -> m Bool) -> [a] -> m (Maybe a)
findM (Rational, Int) -> m Bool
canEnter (forall r. Expr r -> [(r, Int)]
LA.terms Expr Rational
obj_def)
    PivotStrategy
PivotStrategyLargestCoefficient -> do
      [(Rational, Int)]
ts <- forall (m :: * -> *) a.
Applicative m =>
(a -> m Bool) -> [a] -> m [a]
filterM (Rational, Int) -> m Bool
canEnter (forall r. Expr r -> [(r, Int)]
LA.terms Expr Rational
obj_def)
      case [(Rational, Int)]
ts of
        [] -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
        [(Rational, Int)]
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a b. (a, b) -> b
snd forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a.
Foldable t =>
(a -> a -> Ordering) -> t a -> a
maximumBy (forall a b. Ord a => (b -> a) -> b -> b -> Ordering
comparing forall a b. (a, b) -> a
fst) [(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 forall a. Eq a => a -> a -> Bool
== Int
LA.unitVar = forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
    canEnter (Rational
c,Int
xj) = do
      OptDir
dir <- forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> m OptDir
getOptDir GenericSolverM m v
solver
      if OptDir
dirforall a. Eq a => a -> a -> Bool
==OptDir
OptMin
       then forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> (Rational, Int) -> m Bool
canDecrease GenericSolverM m v
solver (Rational
c,Int
xj)
       else 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 forall a. Ord a => a -> a -> Ordering
compare Rational
a Rational
0 of
    Ordering
EQ -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
    Ordering
GT -> forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> Int -> m Bool
canIncrease1 GenericSolverM m v
solver Int
x
    Ordering
LT -> 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 forall a. Ord a => a -> a -> Ordering
compare Rational
a Rational
0 of
    Ordering
EQ -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
    Ordering
GT -> forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> Int -> m Bool
canDecrease1 GenericSolverM m v
solver Int
x
    Ordering
LT -> 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 <- forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> Int -> m (Bound v)
getUB GenericSolverM m v
solver Int
x
  v
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 -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
    Just (v
uv, ConstrIDSet
_) -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$! (v
v 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 <- forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> Int -> m (Bound v)
getLB GenericSolverM m v
solver Int
x
  v
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 -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
    Just (v
lv, ConstrIDSet
_) -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$! (v
lv 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 <- 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 <- forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM ((Int
xj,Rational
1) forall a. a -> [a] -> [a]
: forall a. IntMap a -> [(Int, a)]
IntMap.toList Model
col) forall a b. (a -> b) -> a -> b
$ \(Int
xi,Rational
aij) -> do
    Rational
v1 <- forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> Int -> m v
getValue GenericSolverM m Rational
solver Int
xi
    Bound Rational
li <- forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> Int -> m (Bound v)
getLB GenericSolverM m Rational
solver Int
xi
    Bound Rational
ui <- forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> Int -> m (Bound v)
getUB GenericSolverM m Rational
solver Int
xi
    forall (m :: * -> *) a. Monad m => a -> m a
return [ forall a. HasCallStack => Bool -> a -> a
assert (Rational
theta forall a. Ord a => a -> a -> Bool
>= forall v. AdditiveGroup v => v
zeroV) ((Int
xi,Rational
v2), Rational
theta)
           | Just Rational
v2 <- [forall v. SolverValue v => Bound v -> Maybe v
boundValue Bound Rational
ui | Rational
aij forall a. Ord a => a -> a -> Bool
> Rational
0] forall a. [a] -> [a] -> [a]
++ [forall v. SolverValue v => Bound v -> Maybe v
boundValue Bound Rational
li | Rational
aij forall a. Ord a => a -> a -> Bool
< Rational
0]
           , let theta :: Rational
theta = (Rational
v2 forall v. AdditiveGroup v => v -> v -> v
^-^ Rational
v1) forall v s.
(VectorSpace v, s ~ Scalar v, Fractional s) =>
v -> s -> v
^/ Rational
aij ]

  -- β(xj) := β(xj) + θ なので θ を大きく
  case [((Int, Rational), Rational)]
ubs of
    [] -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False -- unbounded
    [((Int, Rational), Rational)]
_ -> do
      let (Int
xi, Rational
v) = forall a b. (a, b) -> a
fst forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a.
Foldable t =>
(a -> a -> Ordering) -> t a -> a
minimumBy (forall a b. Ord a => (b -> a) -> b -> b -> Ordering
comparing forall a b. (a, b) -> b
snd) [((Int, Rational), Rational)]
ubs
      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
      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 <- 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 <- forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM ((Int
xj,Rational
1) forall a. a -> [a] -> [a]
: forall a. IntMap a -> [(Int, a)]
IntMap.toList Model
col) forall a b. (a -> b) -> a -> b
$ \(Int
xi,Rational
aij) -> do
    Rational
v1 <- forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> Int -> m v
getValue GenericSolverM m Rational
solver Int
xi
    Bound Rational
li <- forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> Int -> m (Bound v)
getLB GenericSolverM m Rational
solver Int
xi
    Bound Rational
ui <- forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> Int -> m (Bound v)
getUB GenericSolverM m Rational
solver Int
xi
    forall (m :: * -> *) a. Monad m => a -> m a
return [ forall a. HasCallStack => Bool -> a -> a
assert (Rational
theta forall a. Ord a => a -> a -> Bool
<= forall v. AdditiveGroup v => v
zeroV) ((Int
xi,Rational
v2), Rational
theta)
           | Just Rational
v2 <- [forall v. SolverValue v => Bound v -> Maybe v
boundValue Bound Rational
li | Rational
aij forall a. Ord a => a -> a -> Bool
> Rational
0] forall a. [a] -> [a] -> [a]
++ [forall v. SolverValue v => Bound v -> Maybe v
boundValue Bound Rational
ui | Rational
aij forall a. Ord a => a -> a -> Bool
< Rational
0]
           , let theta :: Rational
theta = (Rational
v2 forall v. AdditiveGroup v => v -> v -> v
^-^ Rational
v1) forall v s.
(VectorSpace v, s ~ Scalar v, Fractional s) =>
v -> s -> v
^/ Rational
aij ]

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

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

  Maybe ConstrIDSet
m <- forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> m a
readMutVar (forall (m :: * -> *) v.
GenericSolverM m v -> MutVar (PrimState m) (Maybe ConstrIDSet)
svExplanation GenericSolverM m Rational
solver)
  case Maybe ConstrIDSet
m of
    Just ConstrIDSet
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return OptResult
Unsat
    Maybe ConstrIDSet
Nothing -> do
      forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> String -> m ()
log GenericSolverM m Rational
solver String
"dual simplex"
      OptResult
result <- forall (m :: * -> *) v a.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> m a -> m a
recordTime GenericSolverM m Rational
solver m OptResult
loop
      forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (OptResult
result forall a. Eq a => a -> a -> Bool
== OptResult
Optimum) forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> m ()
checkFeasibility GenericSolverM m Rational
solver
      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 <- forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> Int -> m (Expr Rational)
getRow GenericSolverM m Rational
solver Int
objVar
    OptDir
dir <- forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> m OptDir
getOptDir GenericSolverM m Rational
solver
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$
      case OptDir
dir of
        OptDir
OptMin -> Expr Rational
def
        OptDir
OptMax -> 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 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)
    forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (forall r. Expr r -> [(r, Int)]
LA.terms Expr Rational
xi_def) forall a b. (a -> b) -> a -> b
$ \(Rational
aij, Int
xj) -> do
      Bool
b <- 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 = forall r. Num r => Int -> Expr r -> r
LA.coeff Int
xj Expr Rational
obj_def
        let ratio :: Rational
ratio = Rational
cj forall a. Fractional a => a -> a -> a
/ Rational
aij
        forall (m :: * -> *) a. Monad m => a -> m a
return [(Int
xj, Rational
ratio) | Rational
ratio forall a. Ord a => a -> a -> Bool
>= Rational
0]
      else
        forall (m :: * -> *) a. Monad m => a -> m a
return []
  case [(Int, Rational)]
ws of
    [] -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
    [(Int, Rational)]
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a b. (a, b) -> a
fst forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a.
Foldable t =>
(a -> a -> Ordering) -> t a -> a
minimumBy (forall a b. Ord a => (b -> a) -> b -> b -> Ordering
comparing 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 -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
    Just Rational
lim -> do
      Rational
o <- forall (m :: * -> *) v. PrimMonad m => GenericSolverM m v -> m v
getObjValue GenericSolverM m Rational
solver
      OptDir
dir <- forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> m OptDir
getOptDir GenericSolverM m Rational
solver
      case OptDir
dir of
        OptDir
OptMin -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$! (Rational
lim forall a. Ord a => a -> a -> Bool
<= Rational
o)
        OptDir
OptMax -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$! (Rational
lim 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 <- forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> m [Int]
variables GenericSolverM m v
solver
  forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM forall a. [(Int, a)] -> IntMap a
IntMap.fromList forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [Int]
xs forall a b. (a -> b) -> a -> b
$ \Int
x -> do
    v
val <- forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> Int -> m v
getValue GenericSolverM m v
solver Int
x
    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 = 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 <- forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> m a
readMutVar (forall (m :: * -> *) v.
GenericSolverM m v -> MutVar (PrimState m) (Maybe ConstrIDSet)
svExplanation GenericSolverM m v
solver)
  case Maybe ConstrIDSet
m of
    Maybe ConstrIDSet
Nothing -> forall a. HasCallStack => String -> a
error String
"no explanation is available"
    Just ConstrIDSet
cs -> 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 <- forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> Int -> m v
getValue GenericSolverM m v
solver Int
xj
  let diff :: v
diff = v
v forall v. AdditiveGroup v => v -> v -> v
^-^ v
v0

  Model
aj <- forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> Int -> m Model
getCol GenericSolverM m v
solver Int
xj
  forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> (a -> a) -> m ()
modifyMutVar (forall (m :: * -> *) v.
GenericSolverM m v -> MutVar (PrimState m) (IntMap v)
svModel GenericSolverM m v
solver) forall a b. (a -> b) -> a -> b
$ \IntMap v
m ->
    let m2 :: IntMap v
m2 = forall a b. (a -> b) -> IntMap a -> IntMap b
IntMap.map (\Rational
aij -> Rational
aij forall v. VectorSpace v => Scalar v -> v -> v
*^ v
diff) Model
aj
    in forall a. Int -> a -> IntMap a -> IntMap a
IntMap.insert Int
xj v
v forall a b. (a -> b) -> a -> b
$ forall a. (a -> a -> a) -> IntMap a -> IntMap a -> IntMap a
IntMap.unionWith 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
  forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> (a -> a) -> m ()
modifyMutVar' (forall (m :: * -> *) v.
GenericSolverM m v -> MutVar (PrimState m) Int
svNPivot GenericSolverM m v
solver) (forall a. Num a => a -> a -> a
+Int
1)
  forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> (a -> a) -> m ()
modifyMutVar' (forall (m :: * -> *) v.
GenericSolverM m v -> MutVar (PrimState m) (IntMap (Expr Rational))
svTableau GenericSolverM m v
solver) forall a b. (a -> b) -> a -> b
$ \IntMap (Expr Rational)
defs ->
    case forall r.
(Real r, Fractional r) =>
Atom r -> Int -> Maybe (RelOp, Expr r)
LA.solveFor (forall r. Num r => Int -> Expr r
LA.var Int
xi forall e r. IsEqRel e r => e -> e -> r
.==. (IntMap (Expr Rational)
defs forall a. IntMap a -> Int -> a
IntMap.! Int
xi)) Int
xj of
      Just (RelOp
Eql, Expr Rational
xj_def) ->
        forall a. Int -> a -> IntMap a -> IntMap a
IntMap.insert Int
xj Expr Rational
xj_def forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> IntMap a -> IntMap b
IntMap.map (forall r. (Num r, Eq r) => Int -> Expr r -> Expr r -> Expr r
LA.applySubst1 Int
xj Expr Rational
xj_def) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Int -> IntMap a -> IntMap a
IntMap.delete Int
xi forall a b. (a -> b) -> a -> b
$ IntMap (Expr Rational)
defs
      Maybe (RelOp, 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 forall a. Eq a => a -> a -> Bool
== Int
xj = 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 <- forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> m a
readMutVar (forall (m :: * -> *) v.
GenericSolverM m v -> MutVar (PrimState m) (IntMap v)
svModel GenericSolverM m v
solver)

  Model
aj <- 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 forall a. IntMap a -> Int -> a
IntMap.! Int
xi
  let theta :: v
theta = (v
v forall v. AdditiveGroup v => v -> v -> v
^-^ (IntMap v
m forall a. IntMap a -> Int -> a
IntMap.! Int
xi)) forall v s.
(VectorSpace v, s ~ Scalar v, Fractional s) =>
v -> s -> v
^/ Rational
aij

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

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

  Config
config <- forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> m Config
getConfig GenericSolverM m v
solver
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Config -> Bool
configEnableBoundTightening Config
config) forall a b. (a -> b) -> a -> b
$ do
    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 <- forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> m a
readMutVar (forall (m :: * -> *) v.
GenericSolverM m v
-> MutVar (PrimState m) (IntMap (v, ConstrIDSet))
svLB GenericSolverM m v
solver)
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ 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 <- forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> m a
readMutVar (forall (m :: * -> *) v.
GenericSolverM m v
-> MutVar (PrimState m) (IntMap (v, ConstrIDSet))
svUB GenericSolverM m v
solver)
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ 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 <- forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> m a
readMutVar (forall (m :: * -> *) v.
GenericSolverM m v -> MutVar (PrimState m) (IntMap (Expr Rational))
svTableau GenericSolverM m v
solver)
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ 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 <- forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> m a
readMutVar (forall (m :: * -> *) v.
GenericSolverM m v -> MutVar (PrimState m) (IntMap v)
svModel GenericSolverM m v
solver)
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ IntMap v
m 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 <- forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> m a
readMutVar (forall (m :: * -> *) v.
GenericSolverM m v -> MutVar (PrimState m) (IntMap (Expr Rational))
svTableau GenericSolverM m v
solver)
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$! (IntMap (Expr Rational)
t 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 <- forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> m a
readMutVar (forall (m :: * -> *) v.
GenericSolverM m v -> MutVar (PrimState m) (IntMap (Expr Rational))
svTableau GenericSolverM m v
solver)
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a b. (a -> Maybe b) -> IntMap a -> IntMap b
IntMap.mapMaybe (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 <- forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> Int -> m (Expr Rational)
getRow GenericSolverM m v
solver Int
xi
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$! 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 <- forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> m a
readMutVar (forall (m :: * -> *) v.
GenericSolverM m v -> MutVar (PrimState m) (Maybe ConstrIDSet)
svExplanation GenericSolverM m v
solver)
  case Maybe ConstrIDSet
m of
    Just ConstrIDSet
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
    Maybe ConstrIDSet
Nothing -> forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> a -> m ()
writeMutVar (forall (m :: * -> *) v.
GenericSolverM m v -> MutVar (PrimState m) (Maybe ConstrIDSet)
svExplanation GenericSolverM m v
solver) (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
_ [] = forall (m :: * -> *) a. Monad m => a -> m a
return 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 forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. a -> Maybe a
Just a
x)
  else 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 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 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 <- forall (m :: * -> *) v. PrimMonad m => GenericSolverM m v -> m Int
nVars GenericSolverM m v
solver
  forall (m :: * -> *) a. Monad m => a -> m a
return [Int
0..Int
vcntforall 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 <- forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> m a
readMutVar (forall (m :: * -> *) v.
GenericSolverM m v -> MutVar (PrimState m) (IntMap (Expr Rational))
svTableau GenericSolverM m v
solver)
  forall (m :: * -> *) a. Monad m => a -> m a
return (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
  forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> m ()
dumpSize GenericSolverM m v
solver
  forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> a -> m ()
writeMutVar (forall (m :: * -> *) v.
GenericSolverM m v -> MutVar (PrimState m) Int
svNPivot GenericSolverM m v
solver) Int
0
  Maybe (GenericSolverM m v -> m :~> m)
rectm <- forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> m a
readMutVar (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 forall (f :: * -> *) (g :: * -> *). (f :~> g) -> f ~> g
$$ m a
act
  (forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> String -> m ()
log GenericSolverM m v
solver forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall r. PrintfType r => String -> r
printf String
"#pivot = %d") forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> m a
readMutVar (forall (m :: * -> *) v.
GenericSolverM m v -> MutVar (PrimState m) Int
svNPivot GenericSolverM m v
solver)
  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 forall a. [a] -> [a] -> [a]
++
        case forall a. Ord a => a -> a -> Ordering
compare Rational
k Rational
0 of
          Ordering
EQ -> String
""
          Ordering
GT -> String
" + " forall a. [a] -> [a] -> [a]
++ Rational -> String
f Rational
k forall a. [a] -> [a] -> [a]
++ String
" delta"
          Ordering
LT -> String
" - " forall a. [a] -> [a] -> [a]
++ Rational -> String
f (forall a. Num a => a -> a
abs Rational
k) 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
  forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> a -> m ()
writeMutVar (forall (m :: * -> *) v.
GenericSolverM m v -> MutVar (PrimState m) (Maybe (String -> m ()))
svLogger GenericSolverM m v
solver) (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 = forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> a -> m ()
writeMutVar (forall (m :: * -> *) v.
GenericSolverM m v -> MutVar (PrimState m) (Maybe (String -> m ()))
svLogger GenericSolverM m v
solver) 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 = forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> m String -> m ()
logM GenericSolverM m v
solver (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 <- forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> m a
readMutVar (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 -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
    Just String -> m ()
logger -> m String
action 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
  forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> a -> m ()
writeMutVar (forall (m :: * -> *) v.
GenericSolverM m v
-> MutVar (PrimState m) (Maybe (GenericSolverM m v -> m :~> m))
svRecTime GenericSolverM IO v
solver) (forall a. a -> Maybe a
Just forall {v}. GenericSolverM IO v -> IO :~> IO
f)
  where
    f :: GenericSolverM IO v -> IO :~> IO
f GenericSolverM IO v
solver = forall (f :: * -> *) (g :: * -> *). (f ~> g) -> f :~> g
Nat 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 = forall a b. (Integral a, Num b) => a -> b
fromIntegral (TimeSpec -> Integer
toNanoSecs (TimeSpec
end TimeSpec -> TimeSpec -> TimeSpec
`diffTimeSpec` TimeSpec
start)) forall a. Fractional a => a -> a -> a
/ Double
10forall a b. (Num a, Integral b) => a -> b -> a
^(Int
9::Int)
        (forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> String -> m ()
log GenericSolverM IO v
solver forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall r. PrintfType r => String -> r
printf String
"cpu time = %.3fs") (TimeSpec -> TimeSpec -> Double
durationSecs TimeSpec
startCPU TimeSpec
endCPU)
        (forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> String -> m ()
log GenericSolverM IO v
solver forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall r. PrintfType r => String -> r
printf String
"wall clock time = %.3fs") (TimeSpec -> TimeSpec -> Double
durationSecs TimeSpec
startWC TimeSpec
endWC)
        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 = forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> a -> m ()
writeMutVar (forall (m :: * -> *) v.
GenericSolverM m v
-> MutVar (PrimState m) (Maybe (GenericSolverM m v -> m :~> m))
svRecTime GenericSolverM m v
solver) forall a. Maybe a
Nothing

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

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

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

  OptResult
ret <- forall (m :: * -> *).
PrimMonad m =>
GenericSolverM m Rational -> Options -> m OptResult
optimize GenericSolverM IO Rational
solver forall a. Default a => a
def
  forall a. Show a => a -> IO ()
print OptResult
ret
  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 <- forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
m (GenericSolverM m v)
newSolver
  forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> (String -> m ()) -> m ()
setLogger GenericSolverM IO Rational
solver String -> IO ()
putStrLn
  Int
x0 <- forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> m Int
newVar GenericSolverM IO Rational
solver
  Int
x1 <- forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> m Int
newVar GenericSolverM IO Rational
solver

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

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

  OptResult
ret <- forall (m :: * -> *).
PrimMonad m =>
GenericSolverM m Rational -> Options -> m OptResult
optimize GenericSolverM IO Rational
solver forall a. Default a => a
def
  forall a. Show a => a -> IO ()
print OptResult
ret
  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 <- forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
m (GenericSolverM m v)
newSolver
  forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> (String -> m ()) -> m ()
setLogger GenericSolverM IO Rational
solver String -> IO ()
putStrLn
  Int
x0 <- forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> m Int
newVar GenericSolverM IO Rational
solver

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

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

  Model
m <- forall v (m :: * -> *).
(SolverValue v, PrimMonad m) =>
GenericSolverM m v -> m Model
getModel GenericSolverM IO Rational
solver
  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 <- forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> m a
readMutVar (forall (m :: * -> *) v.
GenericSolverM m v -> MutVar (PrimState m) (IntMap (Expr Rational))
svTableau GenericSolverM m v
solver)
  let nrows :: Int
nrows = forall a. IntMap a -> Int
IntMap.size IntMap (Expr Rational)
t forall a. Num a => a -> a -> a
- Int
1 -- -1 is objVar
  [Int]
xs <- forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> m [Int]
variables GenericSolverM m v
solver
  let ncols :: Int
ncols = forall (t :: * -> *) a. Foldable t => t a -> Int
length [Int]
xs forall a. Num a => a -> a -> a
- Int
nrows
  let nnz :: Int
nnz = forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum [forall a. IntMap a -> Int
IntMap.size forall a b. (a -> b) -> a -> b
$ forall r. Expr r -> IntMap r
LA.coeffMap Expr Rational
xi_def | (Int
xi,Expr Rational
xi_def) <- forall a. IntMap a -> [(Int, a)]
IntMap.toList IntMap (Expr Rational)
t, Int
xi forall a. Eq a => a -> a -> Bool
/= Int
objVar]
  forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> String -> m ()
log GenericSolverM m v
solver forall a b. (a -> b) -> a -> b
$ 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
  forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> String -> m ()
log GenericSolverM m v
solver String
"============="

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

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

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

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

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