Presburger formulas are represented as a tree of formula nodes.
` Formula`
is the base class from which all classes of formulas nodes are
derived.
Depending on their class, formula nodes can have zero or more children.
Children can be either other formula nodes or ``atomic'' constraints
(single equality, inequality, or stride constraints).
` Formula`
is an abstract base class;
a plain ` Formula`
node can never be used in a tree.

The various subclasses of formulas are:

`F_And`

Represents the logical conjunction of its children nodes. An`F_And`node with no children represents ``True''. In our current implementation, atomic constraints can only be added as children of`F_And`nodes.`F_Or`

Represents the logical disjunction of its children nodes. An`F_Or`node with no children represents ``False''.`F_Not`

Represents the logical negation of its single child node.`F_Declaration`

This subclass of`Formula`is the abstract base class for all subclasses of`Formula`that can contain variable declarations.`F_Forall`

`F_Forall`nodes have associated with them one or more variables. These variables are universally quantified in the formula represented by the`F_Forall`node's single child node.`F_Exists`

`F_Exists`nodes have associated with them one or more variables. These variables are existentially quantified in the formula represented by the`F_Exists`node's single child node.

Children can be added to any subclass of formula using the following member functions. They all return pointers to the newly created child node.

`F_And * Formula::add_and()``F_Or * Formula::add_or()``F_Not * Formula::add_not()``F_Forall * Formula::add_forall()``F_Exists * Formula::add_exists()`

The ` F_And * Formula::and_with()`
member function is also useful.
Its effect is equivalent to replacing the formula that it is called on with
an ` F_And`
node with the old formula as one of its children and another
` F_And`
node as its other child. This second ` F_And`
node is
returned as the result.

Analogous versions of these member functions exist for the Relation class.
A ` Relation`
can have only one child formula node.

In many cases, it is necessary to create a relation that contains all
pairs of tuples (its formula is ``True''),
or that contains no pairs of tuples (its formula is ``False''.)
It is possible to use the above constructors and member functions to create
such relations.
But since these relations are so common, we provide a shorthand way of
creating them.
The static member functions ` Relation Relation::True`
and
` Relation Relation::False`
return relations or sets with ``True'' and
``False'' respectively as their formulas. If one integer argument is provided
then a set is returned this arity. If two integer arguments are provided then a
relation is returned with these input and output arities respectively.

omega@cs.umd.edu