CVC3::Expr Class Reference
[Expression Package]

Data structure of expressions in CVC3. More...

#include <expr.h>

Collaboration diagram for CVC3::Expr:

Collaboration graph
[legend]
List of all members.

Public Member Functions

Static Public Member Functions

Private Types

Private Member Functions

Private Attributes

Static Private Attributes

Friends

Classes


Detailed Description

Data structure of expressions in CVC3.

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 127 of file expr.h.


Friends And Related Function Documentation

friend class ExprHasher [friend]

Definition at line 128 of file expr.h.

friend class ExprManager [friend]

Definition at line 129 of file expr.h.

friend class Op [friend]

Definition at line 130 of file expr.h.

Referenced by getOp(), and mkOp().

friend class ExprValue [friend]

Definition at line 131 of file expr.h.

friend class ExprNode [friend]

Definition at line 132 of file expr.h.

friend class ::CInterface [friend]

Definition at line 133 of file expr.h.

friend class Theorem [friend]

Definition at line 134 of file expr.h.


The documentation for this class was generated from the following files:
Generated on Tue Jul 3 14:36:08 2007 for CVC3 by  doxygen 1.5.1