ToySolver.Arith.Simplex2

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

data GenericSolver v

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

Methods

toValue :: Rational -> v

showValue :: Bool -> v -> String

getModel :: GenericSolver v -> IO Model

Instances

SolverValue Rational

SolverValue (Delta Rational)

newSolver :: SolverValue v => IO (GenericSolver v)

cloneSolver :: GenericSolver v -> IO (GenericSolver v)

Problem specification

type Var = Int

newVar :: SolverValue v => GenericSolver v -> IO Var

data RelOp

relational operators

Constructors

Lt

Le

Ge

Gt

Eql

NEq

Instances

Eq RelOp

Ord RelOp

Show RelOp

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

constructing relational formula

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

constructing relational formula

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

constructing relational formula

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

constructing relational formula

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

constructing relational formula

type Atom r = ArithRel (Expr r)

Atomic Formula of Linear Arithmetics

assertAtom :: Solver -> Atom Rational -> IO ()

assertAtomEx :: GenericSolver (Delta Rational) -> Atom Rational -> IO ()

assertLower :: SolverValue v => GenericSolver v -> Var -> v -> IO ()

assertUpper :: SolverValue v => GenericSolver v -> Var -> v -> IO ()

setObj :: SolverValue v => GenericSolver v -> Expr Rational -> IO ()

getObj :: SolverValue v => GenericSolver v -> IO (Expr Rational)

data OptDir :: *

The OptDir type represents optimization directions.

Constructors

OptMin

minimization

OptMax

maximization

Instances

Bounded OptDir

Enum OptDir

Eq OptDir

Data OptDir

Ord OptDir

Read OptDir

Show OptDir

Ix OptDir

Hashable OptDir

Typeable * OptDir

setOptDir :: GenericSolver v -> OptDir -> IO ()

getOptDir :: GenericSolver v -> IO OptDir

Solving

check :: SolverValue v => GenericSolver v -> IO Bool

data Options

Constructors

Options

Fields

objLimit :: Maybe Rational

Instances

Eq Options

Ord Options

Show Options

Default Options

defaultOptions :: Options

data OptResult

results of optimization

Constructors

Optimum

Unsat

Unbounded

ObjLimit

Instances

Eq OptResult

Ord OptResult

Show OptResult

optimize :: Solver -> Options -> IO OptResult

dualSimplex :: Solver -> Options -> IO OptResult

Extract results

type Model = IntMap Rational

type RawModel v = IntMap v

getRawModel :: GenericSolver v -> IO (RawModel v)

getValue :: GenericSolver v -> Var -> IO v

getObjValue :: GenericSolver v -> IO v

Reading status

getTableau :: GenericSolver v -> IO (IntMap (Expr Rational))

getRow :: GenericSolver v -> Var -> IO (Expr Rational)

getCol :: SolverValue v => GenericSolver v -> Var -> IO (IntMap Rational)

getCoeff :: GenericSolver v -> Var -> Var -> IO Rational

nVars :: GenericSolver v -> IO Int

isBasicVariable :: GenericSolver v -> Var -> IO Bool

isNonBasicVariable :: GenericSolver v -> Var -> IO Bool

isFeasible :: SolverValue v => GenericSolver v -> IO Bool

isOptimal :: SolverValue v => GenericSolver v -> IO Bool

getLB :: GenericSolver v -> Var -> IO (Maybe v)

getUB :: GenericSolver v -> Var -> IO (Maybe v)

Configulation

setLogger :: GenericSolver v -> (String -> IO ()) -> IO ()

set callback function for receiving messages.

clearLogger :: GenericSolver v -> IO ()

data PivotStrategy

Constructors

PivotStrategyBlandRule

PivotStrategyLargestCoefficient

Instances

Enum PivotStrategy

Eq PivotStrategy

Ord PivotStrategy

Read PivotStrategy

Show PivotStrategy

setPivotStrategy :: GenericSolver v -> PivotStrategy -> IO ()

Debug

dump :: SolverValue v => GenericSolver v -> IO ()