bit-masks for static flagsMore...
bit-masks for dynamic flagsMore...
Data structure of expressions in CVC3.
Author: Clark Barrett
Created: Mon Nov 25 15:29:37 2002
This class is the main data structure for expressions that all other components should use. It is actually a smart pointer to the actual data holding class ExprValue and its subclasses.
Expressions are represented as DAGs with maximal sharing of subexpressions. Therefore, testing for equality is a constant time operation (simply compare the pointers).
Unused expressions are automatically garbage-collected. The use is determined by a reference counting mechanism. In particular, this means that if there is a circular dependency among expressions (e.g. an attribute points back to the expression itself), these expressions will not be garbage-collected, even if no one else is using them.
The most frequently used operations are getKind() (determining the kind of the top level node of the expression), arity() (how many children an Expr has), operator() for accessing a child, and various testers and methods for constructing new expressions.
In addition, a total ordering operator<() is provided. It is guaranteed to remain the same for the lifetime of the expressions (it may change, however, if the expression is garbage-collected and reborn).