4.2 Building formulas

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.

Web Accessibility