CVC3
Classes | Public Member Functions | Static Public Member Functions | Private Types | Private Member Functions | Private Attributes | Static Private Attributes | Friends

CVC3::Expr Class Reference

Data structure of expressions in CVC3. More...

#include <expr.h>

Collaboration diagram for CVC3::Expr:
Collaboration graph
[legend]

List of all members.

Classes

Public Member Functions

Static Public Member Functions

Private Types

Private Member Functions

Private Attributes

Static Private Attributes

Friends


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 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 ExprClosure [friend]

Definition at line 139 of file expr.h.

friend class ::CInterface [friend]

Definition at line 140 of file expr.h.

friend class Theorem [friend]

Definition at line 141 of file expr.h.


The documentation for this class was generated from the following files: