CVCL::Expr Class Reference
[Expression Package]

Data structure of expressions in CVC Lite. More...

#include <expr.h>

Collaboration diagram for CVCL::Expr:

Collaboration graph
List of all members.

Public Member Functions

Static Public Member Functions

Private Types

Private Member Functions

Private Attributes

Static Private Attributes



Detailed Description

Data structure of expressions in CVC Lite.

Class: Expr
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).

Definition at line 133 of file expr.h.

Friends And Related Function Documentation

friend class ExprHasher [friend]

Definition at line 134 of file expr.h.

friend class ExprManager [friend]

Definition at line 135 of file expr.h.

friend class Op [friend]

Definition at line 136 of file expr.h.

Referenced by getOp(), and mkOp().

friend class ExprValue [friend]

Definition at line 137 of file expr.h.

friend class ExprNode [friend]

Definition at line 138 of file expr.h.

friend class ::CInterface [friend]

Definition at line 139 of file expr.h.

The documentation for this class was generated from the following files:
Generated on Thu Apr 13 16:57:43 2006 for CVC Lite by  doxygen 1.4.4