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

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

ToySolver.Cooper

Contents

Description

Naive implementation of Cooper's algorithm

Reference:

See also:

Synopsis

Language of presburger arithmetics

type ExprZ = Expr Integer Source

Linear arithmetic expression over integers.

data Lit Source

Literal

  • Pos e means e > 0
  • Divisible True d e means e can be divided by d (i.e. d|e)
  • Divisible False d e means e can not be divided by d (i.e. ¬(d|e))

Constructors

Pos ExprZ 
Divisible Bool Integer ExprZ 

Instances

data QFFormula Source

quantifier-free negation normal form

Constructors

T 
F 
And QFFormula QFFormula 
Or QFFormula QFFormula 
Lit Lit 

Instances

fromLAAtom :: Atom Rational -> QFFormula Source

(.|.) :: Integer -> ExprZ -> QFFormula Source

Projection

project :: Var -> QFFormula -> (QFFormula, Model Integer -> Model Integer) Source

projectCases :: Var -> QFFormula -> [(QFFormula, Model Integer -> Model Integer)] Source

projectCasesN :: VarSet -> QFFormula -> [(QFFormula, Model Integer -> Model Integer)] Source

Quantifier elimination

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

eliminate quantifiers and returns equivalent quantifier-free formula.

Constraint solving

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

solve a (open) quantifier-free formula

solveQFFormula :: VarSet -> QFFormula -> Maybe (Model Integer) Source

solveFormula :: VarSet -> Formula (Atom Rational) -> SatResult Integer Source

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

solve a (open) quantifier-free formula