ToySolver.Arith.Simplex

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

The Solver type

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

Methods

toValue :: Rational -> v

showValue :: Bool -> v -> String

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

Instances

SolverValue Rational

Defined in ToySolver.Arith.Simplex

Methods

toValue :: Rational -> Rational

showValue :: Bool -> Rational -> String

getModel :: PrimMonad m => GenericSolverM m Rational -> m Model

SolverValue (Delta Rational)

Defined in ToySolver.Arith.Simplex

Methods

toValue :: Rational -> Delta Rational

showValue :: Bool -> Delta Rational -> String

getModel :: PrimMonad m => GenericSolverM m (Delta Rational) -> m Model

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

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

Problem specification

type Var = Int

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

data RelOp

relational operators

Constructors

Lt

Le

Ge

Gt

Eql

NEq

Instances

Show RelOp

Defined in ToySolver.Data.OrdRel

Methods

showsPrec :: Int -> RelOp -> ShowS

show :: RelOp -> String

showList :: [RelOp] -> ShowS

Eq RelOp

Defined in ToySolver.Data.OrdRel

Methods

(==) :: RelOp -> RelOp -> Bool

(/=) :: RelOp -> RelOp -> Bool

Ord RelOp

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 .<., .<=., .>., .>=.

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

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

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

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

type Atom r = OrdRel (Expr r)

Atomic Formula of Linear Arithmetics

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

The OptDir type represents optimization directions.

Constructors

OptMin

minimization

OptMax

maximization

Instances

Data OptDir

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

Defined in Data.OptDir

Methods

minBound :: OptDir

maxBound :: OptDir

Enum OptDir

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

Defined in Data.OptDir

Associated Types

type Rep OptDir :: Type -> Type

Methods

from :: OptDir -> Rep OptDir x

to :: Rep OptDir x -> OptDir

Ix OptDir

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

Defined in Data.OptDir

Methods

readsPrec :: Int -> ReadS OptDir

readList :: ReadS [OptDir]

readPrec :: ReadPrec OptDir

readListPrec :: ReadPrec [OptDir]

Show OptDir

Defined in Data.OptDir

Methods

showsPrec :: Int -> OptDir -> ShowS

show :: OptDir -> String

showList :: [OptDir] -> ShowS

NFData OptDir

Defined in Data.OptDir

Methods

rnf :: OptDir -> ()

Eq OptDir

Defined in Data.OptDir

Methods

(==) :: OptDir -> OptDir -> Bool

(/=) :: OptDir -> OptDir -> Bool

Ord OptDir

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

Defined in Data.OptDir

Methods

hashWithSalt :: Int -> OptDir -> Int

hash :: OptDir -> Int

type Rep OptDir

Defined in Data.OptDir

type Rep OptDir = D1 ('MetaData "OptDir" "Data.OptDir" "OptDir-0.1.0-271N2CcTVqQ2BvPQjeYc3" '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 ()

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

Solving

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 for solving.

The default option can be obtained by def.

Constructors

Options

Fields

• objLimit :: Maybe Rational

Instances

Show Options

Defined in ToySolver.Arith.Simplex

Methods

showsPrec :: Int -> Options -> ShowS

show :: Options -> String

showList :: [Options] -> ShowS

Default Options

Defined in ToySolver.Arith.Simplex

Methods

def :: Options

Eq Options

Defined in ToySolver.Arith.Simplex

Methods

(==) :: Options -> Options -> Bool

(/=) :: Options -> Options -> Bool

Ord Options

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

results of optimization

Constructors

Optimum

Unsat

Unbounded

ObjLimit

Instances

Show OptResult

Defined in ToySolver.Arith.Simplex

Methods

showsPrec :: Int -> OptResult -> ShowS

show :: OptResult -> String

showList :: [OptResult] -> ShowS

Eq OptResult

Defined in ToySolver.Arith.Simplex

Methods

(==) :: OptResult -> OptResult -> Bool

(/=) :: OptResult -> OptResult -> Bool

Ord OptResult

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

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

Extract results

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

Reading status

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

Configulation

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

set callback function for receiving messages.

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

enableTimeRecording :: GenericSolverM IO v -> IO ()

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

data Config

Constructors

Config

Fields

• configPivotStrategy :: !PivotStrategy
• configEnableBoundTightening :: !Bool

Instances

Show Config

Defined in ToySolver.Arith.Simplex

Methods

showsPrec :: Int -> Config -> ShowS

show :: Config -> String

showList :: [Config] -> ShowS

Default Config

Defined in ToySolver.Arith.Simplex

Methods

def :: Config

Eq Config

Defined in ToySolver.Arith.Simplex

Methods

(==) :: Config -> Config -> Bool

(/=) :: Config -> Config -> Bool

Ord Config

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 ()

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

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

data PivotStrategy

Constructors

PivotStrategyBlandRule

PivotStrategyLargestCoefficient

Instances

Bounded PivotStrategy

Defined in ToySolver.Arith.Simplex

Methods

minBound :: PivotStrategy

maxBound :: PivotStrategy

Enum PivotStrategy

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

Defined in ToySolver.Arith.Simplex

Methods

readsPrec :: Int -> ReadS PivotStrategy

readList :: ReadS [PivotStrategy]

readPrec :: ReadPrec PivotStrategy

readListPrec :: ReadPrec [PivotStrategy]

Show PivotStrategy

Defined in ToySolver.Arith.Simplex

Methods

showsPrec :: Int -> PivotStrategy -> ShowS

show :: PivotStrategy -> String

showList :: [PivotStrategy] -> ShowS

Eq PivotStrategy

Defined in ToySolver.Arith.Simplex

Methods

(==) :: PivotStrategy -> PivotStrategy -> Bool

(/=) :: PivotStrategy -> PivotStrategy -> Bool

Ord PivotStrategy

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

showPivotStrategy :: PivotStrategy -> String

parsePivotStrategy :: String -> Maybe PivotStrategy

setPivotStrategy :: PrimMonad m => GenericSolverM m v -> PivotStrategy -> m ()

Deprecated: Use setConfig instead

Debug

dump :: PrimMonad m => SolverValue v => GenericSolverM m v -> m ()

Misc

simplifyAtom :: (PrimMonad m, SolverValue v) => GenericSolverM m v -> Atom Rational -> m (Var, RelOp, Rational)