toysolver-0.0.5: Assorted decision procedures for SAT, Max-SAT, PB, MIP, etc

Portability	portable
Stability	provisional
Maintainer	masahiro.sakai@gmail.com
Safe Haskell	None

Algorithm.FourierMotzkin

Description

Naïve implementation of Fourier-Motzkin Variable Elimination

Reference:

http://users.cecs.anu.edu.au/~michaeln/pubs/arithmetic-dps.pdf

Synopsis

Documentation

data Lit Source

Literal

Constructors

Nonneg ExprZ
Pos ExprZ

Instances

Eq Lit
Ord Lit
Show Lit
Variables Lit
Complement Lit

project :: Var -> [Atom Rational] -> [([Atom Rational], Model Rational -> Model Rational)]Source

projectN :: VarSet -> [Atom Rational] -> [([Atom Rational], Model Rational -> Model Rational)]Source

eliminateQuantifiers :: Formula (Atom Rational) -> Maybe (Formula (Atom Rational))Source

solveFormula :: [Var] -> Formula (Atom Rational) -> SatResult Rational Source

solve :: VarSet -> [Atom Rational] -> Maybe (Model Rational)Source