toysolver-0.0.6: Assorted decision procedures for SAT, Max-SAT, PB, MIP, etc
Algorithm.Cooper.FOL
Description
Synopsis
eliminateQuantifiers :: Formula (Atom Rational) -> Maybe QFFormulaSource
eliminate quantifiers and returns equivalent quantifier-free formula.
solveFormula :: VarSet -> Formula (Atom Rational) -> SatResult IntegerSource