| Portability | non-portable (TypeSynonymInstances, FlexibleInstances, TypeFamilies, CPP) |
|---|---|
| Stability | provisional |
| Maintainer | masahiro.sakai@gmail.com |
| Safe Haskell | None |
Algorithm.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
- (.<=.) :: IsRel e r => e -> e -> r
- (.>=.) :: IsRel e r => e -> e -> r
- (.==.) :: IsRel e r => e -> e -> r
- (.<.) :: IsRel e r => e -> e -> r
- (.>.) :: IsRel e r => e -> e -> r
- type Atom r = Rel (Expr r)
- 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
- setOptDir :: GenericSolver v -> OptDir -> IO ()
- getOptDir :: GenericSolver v -> IO OptDir
- check :: SolverValue v => GenericSolver v -> IO Bool
- data Options = Options {}
- defaultOptions :: Options
- data OptResult
- optimize :: Solver -> Options -> IO OptResult
- dualSimplex :: Solver -> Options -> IO OptResult
- type Model = IntMap Rational
- type RawModel v = IntMap v
- rawModel :: GenericSolver v -> IO (RawModel v)
- getValue :: GenericSolver v -> Var -> IO v
- getObjValue :: GenericSolver v -> IO v
- 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)
- setLogger :: GenericSolver v -> (String -> IO ()) -> IO ()
- clearLogger :: GenericSolver v -> IO ()
- data PivotStrategy
- setPivotStrategy :: GenericSolver v -> PivotStrategy -> IO ()
- dump :: SolverValue v => GenericSolver v -> IO ()
The Solver type
type Solver = GenericSolver RationalSource
data GenericSolver v Source
class (VectorSpace v, Scalar v ~ Rational, Ord v) => SolverValue v whereSource
Methods
toValue :: Rational -> vSource
showValue :: Bool -> v -> StringSource
model :: GenericSolver v -> IO ModelSource
Instances
newSolver :: SolverValue v => IO (GenericSolver v)Source
cloneSolver :: GenericSolver v -> IO (GenericSolver v)Source
Problem specification
newVar :: SolverValue v => GenericSolver v -> IO VarSource
relational operators
assertAtomEx :: GenericSolver (Delta Rational) -> Atom Rational -> IO ()Source
assertLower :: SolverValue v => GenericSolver v -> Var -> v -> IO ()Source
assertUpper :: SolverValue v => GenericSolver v -> Var -> v -> IO ()Source
setObj :: SolverValue v => GenericSolver v -> Expr Rational -> IO ()Source
getObj :: SolverValue v => GenericSolver v -> IO (Expr Rational)Source
setOptDir :: GenericSolver v -> OptDir -> IO ()Source
getOptDir :: GenericSolver v -> IO OptDirSource
Solving
check :: SolverValue v => GenericSolver v -> IO BoolSource
results of optimization
Extract results
rawModel :: GenericSolver v -> IO (RawModel v)Source
getValue :: GenericSolver v -> Var -> IO vSource
getObjValue :: GenericSolver v -> IO vSource
Reading status
getTableau :: GenericSolver v -> IO (IntMap (Expr Rational))Source
getCol :: SolverValue v => GenericSolver v -> Var -> IO (IntMap Rational)Source
nVars :: GenericSolver v -> IO IntSource
isBasicVariable :: GenericSolver v -> Var -> IO BoolSource
isNonBasicVariable :: GenericSolver v -> Var -> IO BoolSource
isFeasible :: SolverValue v => GenericSolver v -> IO BoolSource
isOptimal :: SolverValue v => GenericSolver v -> IO BoolSource
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