Copyright	(c) Masahiro Sakai 2012
License	BSD-style
Maintainer	masahiro.sakai@gmail.com
Stability	provisional
Portability	non-portable
Safe Haskell	Safe-Inferred
Language	Haskell2010
Extensions	MonoLocalBinds ScopedTypeVariables BangPatterns TypeFamilies TypeSynonymInstances FlexibleInstances KindSignatures RankNTypes TypeOperators ExplicitNamespaces ExplicitForAll

ToySolver.Arith.Simplex

Contents

The Solver type
Problem specification
Solving
Extract results
Reading status
Configulation
Debug
Misc

Description

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

Synopsis

type Solver = GenericSolver Rational
type GenericSolver v = GenericSolverM IO v
data GenericSolverM m v
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
newSolver :: (PrimMonad m, SolverValue v) => m (GenericSolverM m v)
cloneSolver :: PrimMonad m => GenericSolverM m v -> m (GenericSolverM m v)
type Var = Int
newVar :: (PrimMonad m, SolverValue v) => GenericSolverM m v -> m Var
data RelOp
- = Lt
- | Le
- | Ge
- | Gt
- | Eql
- | NEq
(.<.), (.<=.), (.>.), (.>=.) :: IsOrdRel e r => e -> e -> r
(.<.), (.<=.), (.>.), (.>=.) :: IsOrdRel e r => e -> e -> r
(.==.) :: IsEqRel e r => e -> e -> r
(.<.), (.<=.), (.>.), (.>=.) :: IsOrdRel e r => e -> e -> r
(.<.), (.<=.), (.>.), (.>=.) :: IsOrdRel e r => e -> e -> r
type Atom r = OrdRel (Expr r)
type ConstrID = Int
type ConstrIDSet = IntSet
assertAtom :: PrimMonad m => GenericSolverM m Rational -> Atom Rational -> m ()
assertAtom' :: PrimMonad m => GenericSolverM m Rational -> Atom Rational -> Maybe ConstrID -> m ()
assertAtomEx :: PrimMonad m => GenericSolverM m (Delta Rational) -> Atom Rational -> m ()
assertAtomEx' :: PrimMonad m => GenericSolverM m (Delta Rational) -> Atom Rational -> Maybe ConstrID -> m ()
assertLower :: (PrimMonad m, SolverValue v) => GenericSolverM m v -> Var -> v -> m ()
assertLower' :: (PrimMonad m, SolverValue v) => GenericSolverM m v -> Var -> v -> Maybe ConstrID -> m ()
assertUpper :: (PrimMonad m, SolverValue v) => GenericSolverM m v -> Var -> v -> m ()
assertUpper' :: (PrimMonad m, SolverValue v) => GenericSolverM m v -> Var -> v -> Maybe ConstrID -> m ()
setObj :: (PrimMonad m, SolverValue v) => GenericSolverM m v -> Expr Rational -> m ()
getObj :: (PrimMonad m, SolverValue v) => GenericSolverM m v -> m (Expr Rational)
data OptDir
- = OptMin
- | OptMax
setOptDir :: PrimMonad m => GenericSolverM m v -> OptDir -> m ()
getOptDir :: PrimMonad m => GenericSolverM m v -> m OptDir
check :: forall m v. (PrimMonad m, SolverValue v) => GenericSolverM m v -> m Bool
pushBacktrackPoint :: PrimMonad m => GenericSolverM m v -> m ()
popBacktrackPoint :: PrimMonad m => GenericSolverM m v -> m ()
data Options = Options {
- objLimit :: Maybe Rational
}
data OptResult
- = Optimum
- | Unsat
- | Unbounded
- | ObjLimit
optimize :: forall m. PrimMonad m => GenericSolverM m Rational -> Options -> m OptResult
dualSimplex :: forall m. PrimMonad m => GenericSolverM m Rational -> Options -> m OptResult
type Model = IntMap Rational
getModel :: (SolverValue v, PrimMonad m) => GenericSolverM m v -> m Model
type RawModel v = IntMap v
getRawModel :: PrimMonad m => GenericSolverM m v -> m (RawModel v)
getValue :: PrimMonad m => GenericSolverM m v -> Var -> m v
getObjValue :: PrimMonad m => GenericSolverM m v -> m v
explain :: PrimMonad m => GenericSolverM m v -> m ConstrIDSet
getTableau :: PrimMonad m => GenericSolverM m v -> m (IntMap (Expr Rational))
getRow :: PrimMonad m => GenericSolverM m v -> Var -> m (Expr Rational)
getCol :: (PrimMonad m, SolverValue v) => GenericSolverM m v -> Var -> m (IntMap Rational)
getCoeff :: PrimMonad m => GenericSolverM m v -> Var -> Var -> m Rational
nVars :: PrimMonad m => GenericSolverM m v -> m Int
isBasicVariable :: PrimMonad m => GenericSolverM m v -> Var -> m Bool
isNonBasicVariable :: PrimMonad m => GenericSolverM m v -> Var -> m Bool
isFeasible :: (PrimMonad m, SolverValue v) => GenericSolverM m v -> m Bool
isOptimal :: (PrimMonad m, SolverValue v) => GenericSolverM m v -> m Bool
getLB :: PrimMonad m => GenericSolverM m v -> Var -> m (Bound v)
getUB :: PrimMonad m => GenericSolverM m v -> Var -> m (Bound v)
type Bound v = Maybe (v, ConstrIDSet)
boundValue :: SolverValue v => Bound v -> Maybe v
boundExplanation :: SolverValue v => Bound v -> ConstrIDSet
setLogger :: PrimMonad m => GenericSolverM m v -> (String -> m ()) -> m ()
clearLogger :: PrimMonad m => GenericSolverM m v -> m ()
enableTimeRecording :: GenericSolverM IO v -> IO ()
disableTimeRecording :: PrimMonad m => GenericSolverM m v -> m ()
data Config = Config {
- configPivotStrategy :: !PivotStrategy
- configEnableBoundTightening :: !Bool
}
setConfig :: PrimMonad m => GenericSolverM m v -> Config -> m ()
getConfig :: PrimMonad m => GenericSolverM m v -> m Config
modifyConfig :: PrimMonad m => GenericSolverM m v -> (Config -> Config) -> m ()
data PivotStrategy
- = PivotStrategyBlandRule
- | PivotStrategyLargestCoefficient
showPivotStrategy :: PivotStrategy -> String
parsePivotStrategy :: String -> Maybe PivotStrategy
setPivotStrategy :: PrimMonad m => GenericSolverM m v -> PivotStrategy -> m ()
dump :: PrimMonad m => SolverValue v => GenericSolverM m v -> m ()
simplifyAtom :: (PrimMonad m, SolverValue v) => GenericSolverM m v -> Atom Rational -> m (Var, RelOp, Rational)

The `Solver` type

type Solver = GenericSolver Rational Source #

type GenericSolver v = GenericSolverM IO v Source #

data GenericSolverM m v Source #

class (VectorSpace v, Scalar v ~ Rational, Ord v) => SolverValue v where Source #

Methods

toValue :: Rational -> v Source #

showValue :: Bool -> v -> String Source #

getModel :: PrimMonad m => GenericSolverM m v -> m Model Source #

Instances

Instances details

SolverValue Rational Source #
Instance details Defined in ToySolver.Arith.Simplex Methods toValue :: Rational -> Rational Source # showValue :: Bool -> Rational -> String Source # getModel :: PrimMonad m => GenericSolverM m Rational -> m Model Source #
SolverValue (Delta Rational) Source #
Instance details Defined in ToySolver.Arith.Simplex Methods toValue :: Rational -> Delta Rational Source # showValue :: Bool -> Delta Rational -> String Source # getModel :: PrimMonad m => GenericSolverM m (Delta Rational) -> m Model Source #

newSolver :: (PrimMonad m, SolverValue v) => m (GenericSolverM m v) Source #

cloneSolver :: PrimMonad m => GenericSolverM m v -> m (GenericSolverM m v) Source #

Problem specification

type Var = Int Source #

newVar :: (PrimMonad m, SolverValue v) => GenericSolverM m v -> m Var Source #

data RelOp Source #

relational operators

Constructors

Lt
Le
Ge
Gt
Eql
NEq

Instances

Instances details

Show RelOp Source #
Instance details Defined in ToySolver.Data.OrdRel Methods showsPrec :: Int -> RelOp -> ShowS # show :: RelOp -> String # showList :: [RelOp] -> ShowS #
Eq RelOp Source #
Instance details Defined in ToySolver.Data.OrdRel Methods (==) :: RelOp -> RelOp -> Bool # (/=) :: RelOp -> RelOp -> Bool #
Ord RelOp Source #
Instance details Defined in ToySolver.Data.OrdRel Methods compare :: RelOp -> RelOp -> Ordering # (<) :: RelOp -> RelOp -> Bool # (<=) :: RelOp -> RelOp -> Bool # (>) :: RelOp -> RelOp -> Bool # (>=) :: RelOp -> RelOp -> Bool # max :: RelOp -> RelOp -> RelOp # min :: RelOp -> RelOp -> RelOp #

(.<.), (.<=.), (.>.), (.>=.) :: IsOrdRel e r => e -> e -> r infix 4 .<., .<=., .>., .>=. Source #

(.==.) :: IsEqRel e r => e -> e -> r infix 4 Source #

(.<.), (.<=.), (.>.), (.>=.) :: IsOrdRel e r => e -> e -> r infix 4 .<., .<=., .>., .>=. Source #

type Atom r = OrdRel (Expr r) Source #

Atomic Formula of Linear Arithmetics

type ConstrID = Int Source #

type ConstrIDSet = IntSet Source #

assertAtom :: PrimMonad m => GenericSolverM m Rational -> Atom Rational -> m () Source #

assertAtom' :: PrimMonad m => GenericSolverM m Rational -> Atom Rational -> Maybe ConstrID -> m () Source #

assertAtomEx :: PrimMonad m => GenericSolverM m (Delta Rational) -> Atom Rational -> m () Source #

assertAtomEx' :: PrimMonad m => GenericSolverM m (Delta Rational) -> Atom Rational -> Maybe ConstrID -> m () Source #

assertLower :: (PrimMonad m, SolverValue v) => GenericSolverM m v -> Var -> v -> m () Source #

assertLower' :: (PrimMonad m, SolverValue v) => GenericSolverM m v -> Var -> v -> Maybe ConstrID -> m () Source #

assertUpper :: (PrimMonad m, SolverValue v) => GenericSolverM m v -> Var -> v -> m () Source #

assertUpper' :: (PrimMonad m, SolverValue v) => GenericSolverM m v -> Var -> v -> Maybe ConstrID -> m () Source #

setObj :: (PrimMonad m, SolverValue v) => GenericSolverM m v -> Expr Rational -> m () Source #

getObj :: (PrimMonad m, SolverValue v) => GenericSolverM m v -> m (Expr Rational) Source #

data OptDir #

The OptDir type represents optimization directions.

Constructors

OptMin	minimization
OptMax	maximization

Instances

Instances details

Data OptDir
Instance details Defined in Data.OptDir Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> OptDir -> c OptDir # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c OptDir # toConstr :: OptDir -> Constr # dataTypeOf :: OptDir -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c OptDir) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c OptDir) # gmapT :: (forall b. Data b => b -> b) -> OptDir -> OptDir # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> OptDir -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> OptDir -> r # gmapQ :: (forall d. Data d => d -> u) -> OptDir -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> OptDir -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> OptDir -> m OptDir # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> OptDir -> m OptDir # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> OptDir -> m OptDir #
Bounded OptDir
Instance details Defined in Data.OptDir Methods minBound :: OptDir # maxBound :: OptDir #
Enum OptDir
Instance details Defined in Data.OptDir Methods succ :: OptDir -> OptDir # pred :: OptDir -> OptDir # toEnum :: Int -> OptDir # fromEnum :: OptDir -> Int # enumFrom :: OptDir -> [OptDir] # enumFromThen :: OptDir -> OptDir -> [OptDir] # enumFromTo :: OptDir -> OptDir -> [OptDir] # enumFromThenTo :: OptDir -> OptDir -> OptDir -> [OptDir] #
Generic OptDir
Instance details Defined in Data.OptDir Associated Types type Rep OptDir :: Type -> Type # Methods from :: OptDir -> Rep OptDir x # to :: Rep OptDir x -> OptDir #
Ix OptDir
Instance details Defined in Data.OptDir Methods range :: (OptDir, OptDir) -> [OptDir] # index :: (OptDir, OptDir) -> OptDir -> Int # unsafeIndex :: (OptDir, OptDir) -> OptDir -> Int # inRange :: (OptDir, OptDir) -> OptDir -> Bool # rangeSize :: (OptDir, OptDir) -> Int # unsafeRangeSize :: (OptDir, OptDir) -> Int #
Read OptDir
Instance details Defined in Data.OptDir Methods readsPrec :: Int -> ReadS OptDir # readList :: ReadS [OptDir] # readPrec :: ReadPrec OptDir # readListPrec :: ReadPrec [OptDir] #
Show OptDir
Instance details Defined in Data.OptDir Methods showsPrec :: Int -> OptDir -> ShowS # show :: OptDir -> String # showList :: [OptDir] -> ShowS #
Eq OptDir
Instance details Defined in Data.OptDir Methods (==) :: OptDir -> OptDir -> Bool # (/=) :: OptDir -> OptDir -> Bool #
Ord OptDir
Instance details Defined in Data.OptDir Methods compare :: OptDir -> OptDir -> Ordering # (<) :: OptDir -> OptDir -> Bool # (<=) :: OptDir -> OptDir -> Bool # (>) :: OptDir -> OptDir -> Bool # (>=) :: OptDir -> OptDir -> Bool # max :: OptDir -> OptDir -> OptDir # min :: OptDir -> OptDir -> OptDir #
Hashable OptDir
Instance details Defined in Data.OptDir Methods hashWithSalt :: Int -> OptDir -> Int # hash :: OptDir -> Int #
type Rep OptDir
Instance details Defined in Data.OptDir type Rep OptDir = D1 ('MetaData "OptDir" "Data.OptDir" "OptDir-0.0.4-DFbjZiVPna85b8377JvIx4" 'False) (C1 ('MetaCons "OptMin" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "OptMax" 'PrefixI 'False) (U1 :: Type -> Type))

setOptDir :: PrimMonad m => GenericSolverM m v -> OptDir -> m () Source #

getOptDir :: PrimMonad m => GenericSolverM m v -> m OptDir Source #

Solving

check :: forall m v. (PrimMonad m, SolverValue v) => GenericSolverM m v -> m Bool Source #

pushBacktrackPoint :: PrimMonad m => GenericSolverM m v -> m () Source #

popBacktrackPoint :: PrimMonad m => GenericSolverM m v -> m () Source #

data Options Source #

Options for solving.

The default option can be obtained by def.

Constructors

Options
Fields objLimit :: Maybe Rational

Instances

Instances details

Show Options Source #
Instance details Defined in ToySolver.Arith.Simplex Methods showsPrec :: Int -> Options -> ShowS # show :: Options -> String # showList :: [Options] -> ShowS #
Default Options Source #
Instance details Defined in ToySolver.Arith.Simplex Methods def :: Options #
Eq Options Source #
Instance details Defined in ToySolver.Arith.Simplex Methods (==) :: Options -> Options -> Bool # (/=) :: Options -> Options -> Bool #
Ord Options Source #
Instance details Defined in ToySolver.Arith.Simplex Methods compare :: Options -> Options -> Ordering # (<) :: Options -> Options -> Bool # (<=) :: Options -> Options -> Bool # (>) :: Options -> Options -> Bool # (>=) :: Options -> Options -> Bool # max :: Options -> Options -> Options # min :: Options -> Options -> Options #

data OptResult Source #

results of optimization

Constructors

Optimum
Unsat
Unbounded
ObjLimit

Instances

Instances details

Show OptResult Source #
Instance details Defined in ToySolver.Arith.Simplex Methods showsPrec :: Int -> OptResult -> ShowS # show :: OptResult -> String # showList :: [OptResult] -> ShowS #
Eq OptResult Source #
Instance details Defined in ToySolver.Arith.Simplex Methods (==) :: OptResult -> OptResult -> Bool # (/=) :: OptResult -> OptResult -> Bool #
Ord OptResult Source #
Instance details Defined in ToySolver.Arith.Simplex Methods compare :: OptResult -> OptResult -> Ordering # (<) :: OptResult -> OptResult -> Bool # (<=) :: OptResult -> OptResult -> Bool # (>) :: OptResult -> OptResult -> Bool # (>=) :: OptResult -> OptResult -> Bool # max :: OptResult -> OptResult -> OptResult # min :: OptResult -> OptResult -> OptResult #

optimize :: forall m. PrimMonad m => GenericSolverM m Rational -> Options -> m OptResult Source #

dualSimplex :: forall m. PrimMonad m => GenericSolverM m Rational -> Options -> m OptResult Source #

Extract results

type Model = IntMap Rational Source #

getModel :: (SolverValue v, PrimMonad m) => GenericSolverM m v -> m Model Source #

type RawModel v = IntMap v Source #

getRawModel :: PrimMonad m => GenericSolverM m v -> m (RawModel v) Source #

getValue :: PrimMonad m => GenericSolverM m v -> Var -> m v Source #

getObjValue :: PrimMonad m => GenericSolverM m v -> m v Source #

explain :: PrimMonad m => GenericSolverM m v -> m ConstrIDSet Source #

Reading status

getTableau :: PrimMonad m => GenericSolverM m v -> m (IntMap (Expr Rational)) Source #

getRow :: PrimMonad m => GenericSolverM m v -> Var -> m (Expr Rational) Source #

getCol :: (PrimMonad m, SolverValue v) => GenericSolverM m v -> Var -> m (IntMap Rational) Source #

getCoeff :: PrimMonad m => GenericSolverM m v -> Var -> Var -> m Rational Source #

nVars :: PrimMonad m => GenericSolverM m v -> m Int Source #

isBasicVariable :: PrimMonad m => GenericSolverM m v -> Var -> m Bool Source #

isNonBasicVariable :: PrimMonad m => GenericSolverM m v -> Var -> m Bool Source #

isFeasible :: (PrimMonad m, SolverValue v) => GenericSolverM m v -> m Bool Source #

isOptimal :: (PrimMonad m, SolverValue v) => GenericSolverM m v -> m Bool Source #

getLB :: PrimMonad m => GenericSolverM m v -> Var -> m (Bound v) Source #

getUB :: PrimMonad m => GenericSolverM m v -> Var -> m (Bound v) Source #

type Bound v = Maybe (v, ConstrIDSet) Source #

boundValue :: SolverValue v => Bound v -> Maybe v Source #

boundExplanation :: SolverValue v => Bound v -> ConstrIDSet Source #

Configulation

setLogger :: PrimMonad m => GenericSolverM m v -> (String -> m ()) -> m () Source #

set callback function for receiving messages.

clearLogger :: PrimMonad m => GenericSolverM m v -> m () Source #

enableTimeRecording :: GenericSolverM IO v -> IO () Source #

disableTimeRecording :: PrimMonad m => GenericSolverM m v -> m () Source #

data Config Source #

Constructors

Config
Fields configPivotStrategy :: !PivotStrategy configEnableBoundTightening :: !Bool

Instances

Instances details

Show Config Source #
Instance details Defined in ToySolver.Arith.Simplex Methods showsPrec :: Int -> Config -> ShowS # show :: Config -> String # showList :: [Config] -> ShowS #
Default Config Source #
Instance details Defined in ToySolver.Arith.Simplex Methods def :: Config #
Eq Config Source #
Instance details Defined in ToySolver.Arith.Simplex Methods (==) :: Config -> Config -> Bool # (/=) :: Config -> Config -> Bool #
Ord Config Source #
Instance details Defined in ToySolver.Arith.Simplex Methods compare :: Config -> Config -> Ordering # (<) :: Config -> Config -> Bool # (<=) :: Config -> Config -> Bool # (>) :: Config -> Config -> Bool # (>=) :: Config -> Config -> Bool # max :: Config -> Config -> Config # min :: Config -> Config -> Config #

setConfig :: PrimMonad m => GenericSolverM m v -> Config -> m () Source #

getConfig :: PrimMonad m => GenericSolverM m v -> m Config Source #

modifyConfig :: PrimMonad m => GenericSolverM m v -> (Config -> Config) -> m () Source #

data PivotStrategy Source #

Constructors

PivotStrategyBlandRule
PivotStrategyLargestCoefficient

Instances

Instances details

Bounded PivotStrategy Source #
Instance details Defined in ToySolver.Arith.Simplex Methods minBound :: PivotStrategy # maxBound :: PivotStrategy #
Enum PivotStrategy Source #
Instance details Defined in ToySolver.Arith.Simplex Methods succ :: PivotStrategy -> PivotStrategy # pred :: PivotStrategy -> PivotStrategy # toEnum :: Int -> PivotStrategy # fromEnum :: PivotStrategy -> Int # enumFrom :: PivotStrategy -> [PivotStrategy] # enumFromThen :: PivotStrategy -> PivotStrategy -> [PivotStrategy] # enumFromTo :: PivotStrategy -> PivotStrategy -> [PivotStrategy] # enumFromThenTo :: PivotStrategy -> PivotStrategy -> PivotStrategy -> [PivotStrategy] #
Read PivotStrategy Source #
Instance details Defined in ToySolver.Arith.Simplex Methods readsPrec :: Int -> ReadS PivotStrategy # readList :: ReadS [PivotStrategy] # readPrec :: ReadPrec PivotStrategy # readListPrec :: ReadPrec [PivotStrategy] #
Show PivotStrategy Source #
Instance details Defined in ToySolver.Arith.Simplex Methods showsPrec :: Int -> PivotStrategy -> ShowS # show :: PivotStrategy -> String # showList :: [PivotStrategy] -> ShowS #
Eq PivotStrategy Source #
Instance details Defined in ToySolver.Arith.Simplex Methods (==) :: PivotStrategy -> PivotStrategy -> Bool # (/=) :: PivotStrategy -> PivotStrategy -> Bool #
Ord PivotStrategy Source #
Instance details Defined in ToySolver.Arith.Simplex Methods compare :: PivotStrategy -> PivotStrategy -> Ordering # (<) :: PivotStrategy -> PivotStrategy -> Bool # (<=) :: PivotStrategy -> PivotStrategy -> Bool # (>) :: PivotStrategy -> PivotStrategy -> Bool # (>=) :: PivotStrategy -> PivotStrategy -> Bool # max :: PivotStrategy -> PivotStrategy -> PivotStrategy # min :: PivotStrategy -> PivotStrategy -> PivotStrategy #