Create a constant boolean expression.

Create a constant boolean predicate.

Create a constant integer expression.

Create an expression for zero as an integer in Sally.

Create an expression for one as an integer in Sally.

Create a constant real expression.

Better constructor for adding expressions TODO maintain normal form

Subtract two SallyExpr.

Better constructor for multiplying expressions; checks that one of the operands is a constant.

Better constructor for dividing expressions; checks that the denominator is a constant.

Create the expression that is the boolean negation of the given one.

Create the expression equating two given expressions.

Create the expression representing non-equality.

a ltExpr b represents the expression a < b.

a leqExpr b represents the expression a <= b.

a gtExpr b represents the expression a > b.

a geqExpr b represents the expression a >= b.

Create an if-then-else expression: mux b x y represents the statement "if b then x else y".

Form the conjunction of the given expressions (which should be predicates, but this is not checked).

And over multiple predicates, doing some small inline simplification

Form the disjunction of the given expressions (which should be predicates, but this is not checked).

Create a variable expression.

Create a variable expression from a name.

Create the XOR of two Sally expressions.

Given a non-empty finite list of expressions, build an expression to compute their minimum. The second argument is a special value which, if present causes expressions in the list with this value to be ignored in the calculation. If the input list contains only the special value, then the special value itself is returned.

Build a Sally expression representing the number of times a particular item appears in a list of expressions.

A basic top-down recursive constant folding function.

Top-down rewriting of and terms including constant folding and constructor reduction.

Top-down rewriting of or terms including constant folding and constructor reduction.

Recursively flatten a tree of and expressions into an and sequence.

Recursively flatten a tree of or expressions into an or sequence.