ToySolver.Cooper.Core

Naive implementation of Cooper's algorithm

Reference:

• http://hagi.is.s.u-tokyo.ac.jp/pub/staff/hagiya/kougiroku/ronri/5.txt
• http://www.cs.cmu.edu/~emc/spring06/home1_files/Presburger%20Arithmetic.ppt

See also:

• http://hackage.haskell.org/package/presburger

Language of presburger arithmetics

type ExprZ = Expr Integer

Linear arithmetic expression over integers.

data Lit

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

Eq Lit

Ord Lit

Show Lit

Complement Lit

Variables Lit

evalLit :: Model Integer -> Lit -> Bool

data QFFormula

quantifier-free negation normal form

Constructors

T

F

And QFFormula QFFormula

Or QFFormula QFFormula

Lit Lit

Instances

Eq QFFormula

Ord QFFormula

Show QFFormula

Boolean QFFormula

Complement QFFormula

Variables QFFormula

IsRel (Expr Integer) QFFormula

fromLAAtom :: Atom Rational -> QFFormula

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

evalQFFormula :: Model Integer -> QFFormula -> Bool

Projection

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

projectN :: VarSet -> QFFormula -> (QFFormula, Model Integer -> Model Integer)

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

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

Constraint solving

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

solve a (open) quantifier-free formula

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

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

solve a (open) quantifier-free formula