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:
Children can be added to any subclass of formula using the following member functions. They all return pointers to the newly created child node.
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.