ToySolver.Arith.Cooper

Language of presburger arithmetics

type ExprZ

data Lit

type QFFormula

fromLAAtom

(.|.)

evalQFFormula

type Model r

Projection

project

projectN

projectCases

projectCasesN

Quantifier elimination

eliminateQuantifiers

Constraint solving

solve

solveQFFormula

solveFormula

solveQFLIRAConj