Data.Presburger.Omega.Expr

Expressions

data Exp t

type IntExp

type BoolExp

data Var

Construction

nthVariable

takeFreeVariables

takeFreeVariables'

varE

nthVarE

intE

boolE

trueE

falseE

negateE

sumE

prodE

notE

conjE

disjE

(|&&|)

sumOfProductsE

(|+|)

(|-|)

(|*|)

(*|)

isZeroE

isNonnegativeE

(|==|)

(|/=|)

(|>|)

(|>=|)

(|<|)

(|<=|)

forallE

existsE

Destruction

foldIntExp

foldBoolExp

Internal data structures

data Expr t

type IntExpr

type BoolExpr

data PredOp

data Quantifier

wrapExpr

wrapSimplifiedExpr

varExpr

sumOfProductsExpr

conjExpr

disjExpr

testExpr

existsExpr

Operations on expressions

expEqual

expToFormula

Manipulating variables

rename

adjustBindings

variablesWithinRange