| Copyright | (c) Masahiro Sakai 2012 |
|---|---|
| License | BSD-style |
| Maintainer | masahiro.sakai@gmail.com |
| Stability | provisional |
| Portability | non-portable (TypeSynonymInstances, FlexibleInstances, TypeFamilies, CPP) |
| Safe Haskell | None |
| Language | Haskell2010 |
ToySolver.Arith.Simplex2
Contents
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
- type Solver = GenericSolver Rational
- data GenericSolver v
- class (VectorSpace v, Scalar v ~ Rational, Ord v) => SolverValue v where
- newSolver :: SolverValue v => IO (GenericSolver v)
- cloneSolver :: GenericSolver v -> IO (GenericSolver v)
- type Var = Int
- newVar :: SolverValue v => GenericSolver v -> IO Var
- data RelOp
- (.<.), (.<=.), (.>.), (.>=.) :: 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 :: Solver -> Atom Rational -> IO ()
- assertAtom' :: Solver -> Atom Rational -> Maybe ConstrID -> IO ()
- assertAtomEx :: GenericSolver (Delta Rational) -> Atom Rational -> IO ()
- assertAtomEx' :: GenericSolver (Delta Rational) -> Atom Rational -> Maybe ConstrID -> IO ()
- assertLower :: SolverValue v => GenericSolver v -> Var -> v -> IO ()
- assertLower' :: SolverValue v => GenericSolver v -> Var -> v -> Maybe ConstrID -> IO ()
- assertUpper :: SolverValue v => GenericSolver v -> Var -> v -> IO ()
- assertUpper' :: SolverValue v => GenericSolver v -> Var -> v -> Maybe ConstrID -> IO ()
- setObj :: SolverValue v => GenericSolver v -> Expr Rational -> IO ()
- getObj :: SolverValue v => GenericSolver v -> IO (Expr Rational)
- data OptDir :: *
- setOptDir :: GenericSolver v -> OptDir -> IO ()
- getOptDir :: GenericSolver v -> IO OptDir
- check :: SolverValue v => GenericSolver v -> IO Bool
- pushBacktrackPoint :: GenericSolver v -> IO ()
- popBacktrackPoint :: GenericSolver v -> IO ()
- data Options = Options {}
- data OptResult
- optimize :: Solver -> Options -> IO OptResult
- dualSimplex :: Solver -> Options -> IO OptResult
- type Model = IntMap Rational
- getModel :: SolverValue v => GenericSolver v -> IO Model
- type RawModel v = IntMap v
- getRawModel :: GenericSolver v -> IO (RawModel v)
- getValue :: GenericSolver v -> Var -> IO v
- getObjValue :: GenericSolver v -> IO v
- explain :: GenericSolver v -> IO ConstrIDSet
- 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 (Bound v)
- getUB :: GenericSolver v -> Var -> IO (Bound v)
- type Bound v = Maybe (v, ConstrIDSet)
- boundValue :: SolverValue v => Bound v -> Maybe v
- boundExplanation :: SolverValue v => Bound v -> ConstrIDSet
- setLogger :: GenericSolver v -> (String -> IO ()) -> IO ()
- clearLogger :: GenericSolver v -> IO ()
- data PivotStrategy
- setPivotStrategy :: GenericSolver v -> PivotStrategy -> IO ()
- dump :: SolverValue v => GenericSolver v -> IO ()
- simplifyAtom :: SolverValue v => GenericSolver v -> Atom Rational -> IO (Var, RelOp, Rational)
The Solver type
type Solver = GenericSolver Rational Source #
data GenericSolver v Source #
class (VectorSpace v, Scalar v ~ Rational, Ord v) => SolverValue v where Source #
Instances
newSolver :: SolverValue v => IO (GenericSolver v) Source #
cloneSolver :: GenericSolver v -> IO (GenericSolver v) Source #
Problem specification
newVar :: SolverValue v => GenericSolver v -> IO Var Source #
relational operators
type ConstrIDSet = IntSet Source #
assertAtomEx :: GenericSolver (Delta Rational) -> Atom Rational -> IO () Source #
assertAtomEx' :: GenericSolver (Delta Rational) -> Atom Rational -> Maybe ConstrID -> IO () Source #
assertLower :: SolverValue v => GenericSolver v -> Var -> v -> IO () Source #
assertLower' :: SolverValue v => GenericSolver v -> Var -> v -> Maybe ConstrID -> IO () Source #
assertUpper :: SolverValue v => GenericSolver v -> Var -> v -> IO () Source #
assertUpper' :: SolverValue v => GenericSolver v -> Var -> v -> Maybe ConstrID -> IO () Source #
setObj :: SolverValue v => GenericSolver v -> Expr Rational -> IO () Source #
getObj :: SolverValue v => GenericSolver v -> IO (Expr Rational) Source #
The OptDir type represents optimization directions.
Solving
check :: SolverValue v => GenericSolver v -> IO Bool Source #
pushBacktrackPoint :: GenericSolver v -> IO () Source #
popBacktrackPoint :: GenericSolver v -> IO () Source #
Options for solving.
The default option can be obtained by def.
results of optimization
Extract results
getModel :: SolverValue v => GenericSolver v -> IO Model Source #
getRawModel :: GenericSolver v -> IO (RawModel v) Source #
getObjValue :: GenericSolver v -> IO v Source #
explain :: GenericSolver v -> IO ConstrIDSet Source #
Reading status
getTableau :: GenericSolver v -> IO (IntMap (Expr Rational)) Source #
getCol :: SolverValue v => GenericSolver v -> Var -> IO (IntMap Rational) Source #
isBasicVariable :: GenericSolver v -> Var -> IO Bool Source #
isNonBasicVariable :: GenericSolver v -> Var -> IO Bool Source #
isFeasible :: SolverValue v => GenericSolver v -> IO Bool Source #
isOptimal :: SolverValue v => GenericSolver v -> IO Bool 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 :: GenericSolver v -> (String -> IO ()) -> IO () Source #
set callback function for receiving messages.
clearLogger :: GenericSolver v -> IO () Source #
data PivotStrategy Source #
setPivotStrategy :: GenericSolver v -> PivotStrategy -> IO () Source #
Debug
dump :: SolverValue v => GenericSolver v -> IO () Source #
Misc
simplifyAtom :: SolverValue v => GenericSolver v -> Atom Rational -> IO (Var, RelOp, Rational) Source #