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 |
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
- (.<=.) :: IsArithRel e r => e -> e -> r
- (.>=.) :: IsArithRel e r => e -> e -> r
- (.==.) :: IsArithRel e r => e -> e -> r
- (.<.) :: IsArithRel e r => e -> e -> r
- (.>.) :: IsArithRel e r => e -> e -> r
- type Atom r = ArithRel (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
- pushBacktrackPoint :: GenericSolver v -> IO ()
- popBacktrackPoint :: GenericSolver v -> IO ()
- 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
- getRawModel :: 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 Rational Source
data GenericSolver v Source
class (VectorSpace v, Scalar v ~ Rational, Ord v) => SolverValue v where Source
newSolver :: SolverValue v => IO (GenericSolver v) Source
cloneSolver :: GenericSolver v -> IO (GenericSolver v) Source
Problem specification
newVar :: SolverValue v => GenericSolver v -> IO Var Source
(.<=.) :: IsArithRel e r => e -> e -> r infix 4 Source
constructing relational formula
(.>=.) :: IsArithRel e r => e -> e -> r infix 4 Source
constructing relational formula
(.==.) :: IsArithRel e r => e -> e -> r infix 4 Source
constructing relational formula
(.<.) :: IsArithRel e r => e -> e -> r infix 4 Source
constructing relational formula
(.>.) :: IsArithRel e r => e -> e -> r infix 4 Source
constructing relational formula
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 OptDir Source
Solving
check :: SolverValue v => GenericSolver v -> IO Bool Source
pushBacktrackPoint :: GenericSolver v -> IO () Source
popBacktrackPoint :: GenericSolver v -> IO () Source
results of optimization
Extract results
getRawModel :: GenericSolver v -> IO (RawModel v) Source
getValue :: GenericSolver v -> Var -> IO v Source
getObjValue :: GenericSolver v -> IO v Source
Reading status
getTableau :: GenericSolver v -> IO (IntMap (Expr Rational)) Source
getCol :: SolverValue v => GenericSolver v -> Var -> IO (IntMap Rational) Source
nVars :: GenericSolver v -> IO Int 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
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