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

Copyright(c) Masahiro Sakai 2011-2013
LicenseBSD-style
Maintainermasahiro.sakai@gmail.com
Stabilityprovisional
Portabilityportable
Safe HaskellNone
LanguageHaskell2010

ToySolver.FourierMotzkin

Description

Naïve implementation of Fourier-Motzkin Variable Elimination

Reference:

Synopsis

Documentation

data Lit Source

Literal

Constructors

Nonneg ExprZ 
Pos ExprZ 

Instances

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