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

CVC3::ExprManager Class Reference

#include <expr_manager.h>

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

List of all members.

Classes

Public Member Functions

Private Types

Private Member Functions

Private Attributes

Friends


Detailed Description

Expression Manager

Class: ExprManager

Author: Sergey Berezin

Created: Wed Dec 4 14:26:35 2002

Description: Global state of the Expr package for a particular instance of CVC3. Each instance of the CVC3 library has its own expression manager, for thread-safety.

Definition at line 58 of file expr_manager.h.


Member Typedef Documentation

Hash set type for uniquifying expressions.

Definition at line 129 of file expr_manager.h.


Member Function Documentation

sdb home mdeters cvc3 docs cvc3 src include expr_manager h size_t CVC3::ExprManager::hash ( const ExprValue ev) const [inline, private]

Definition at line 450 of file expr_manager.h.

Referenced by CVC3::Expr::hash().

void ExprManager::installExprValue ( ExprValue ev) [private]

Definition at line 36 of file expr_manager.cpp.

References DebugAssert.


Friends And Related Function Documentation

friend class Expr [friend]

Definition at line 59 of file expr_manager.h.

Referenced by clear().

friend class ExprValue [friend]

Definition at line 60 of file expr_manager.h.

friend class Op [friend]

Definition at line 61 of file expr_manager.h.

friend class HashEV [friend]

Definition at line 62 of file expr_manager.h.

friend class Type [friend]

Definition at line 63 of file expr_manager.h.

Referenced by rebuildRec().


Member Data Documentation

For backtracking attributes.

Definition at line 65 of file expr_manager.h.

Referenced by ExprManager().

Needed for Refl Theorems.

Definition at line 66 of file expr_manager.h.

Notification on pop()

Definition at line 67 of file expr_manager.h.

Referenced by ExprManager(), and ~ExprManager().

Index counter for Expr compare()

Definition at line 68 of file expr_manager.h.

Counter for a generic Expr flag.

Definition at line 69 of file expr_manager.h.

std::hash_map<int, std::string> CVC3::ExprManager::d_kindMap [private]

The database of registered kinds.

Definition at line 72 of file expr_manager.h.

Referenced by getKindName(), and newKind().

The set of kinds representing a type.

Definition at line 74 of file expr_manager.h.

Referenced by newKind().

The reverse map of names to kinds.

Definition at line 84 of file expr_manager.h.

Referenced by getKind(), and newKind().

The registered pretty-printer, a connector to theory-specific pretty-printers.

Definition at line 87 of file expr_manager.h.

Referenced by registerPrettyPrinter(), and unregisterPrettyPrinter().

const int* CVC3::ExprManager::d_printDepth [private]

Print upto the given depth, replace the rest with "...". -1==unlimited depth.

Definition at line 95 of file expr_manager.h.

const bool* CVC3::ExprManager::d_withIndentation [private]

Whether to print with indentation.

Definition at line 97 of file expr_manager.h.

Permanent indentation.

Definition at line 99 of file expr_manager.h.

Referenced by incIndent(), and indent().

Transient indentation.

Normally is the same as d_indent, but may temporarily be different for printing one single Expr

Definition at line 103 of file expr_manager.h.

Referenced by incIndent(), and indent().

const int* CVC3::ExprManager::d_lineWidth [private]

Suggested line width for printing with indentation.

Definition at line 105 of file expr_manager.h.

const std::string* CVC3::ExprManager::d_inputLang [private]

Input language (printing)

Definition at line 107 of file expr_manager.h.

Referenced by getInputLang(), and getOutputLang().

const std::string* CVC3::ExprManager::d_outputLang [private]

Output language (printing)

Definition at line 109 of file expr_manager.h.

Referenced by getOutputLang().

const bool* CVC3::ExprManager::d_dagPrinting [private]

Whether to print Expr's as DAGs.

Definition at line 111 of file expr_manager.h.

const std::string CVC3::ExprManager::d_mmFlag [private]

Which memory manager to use (copy the flag value and keep it the same)

Definition at line 113 of file expr_manager.h.

Referenced by ExprManager(), getMemory(), and registerSubclass().

Hash set for uniquifying expressions.

Definition at line 131 of file expr_manager.h.

Referenced by clear(), gc(), newExprValue(), and rebuildRec().

std::vector<MemoryManager*> CVC3::ExprManager::d_mm [private]

Array of memory managers for subclasses of ExprValue.

Definition at line 133 of file expr_manager.h.

Referenced by clear(), ExprManager(), gc(), registerSubclass(), resumeGC(), and ~ExprManager().

A hash function for hashing pointers.

Definition at line 136 of file expr_manager.h.

Expr constants cached for fast access.

Definition at line 139 of file expr_manager.h.

Referenced by clear(), and ExprManager().

Definition at line 140 of file expr_manager.h.

Referenced by clear(), and ExprManager().

Definition at line 141 of file expr_manager.h.

Referenced by clear(), and ExprManager().

std::vector<Expr> CVC3::ExprManager::d_emptyVec [private]

Empty vector of Expr to return by reference as empty vector of children.

Definition at line 143 of file expr_manager.h.

Referenced by ~ExprManager().

Null Expr to return by reference, for efficiency.

Definition at line 145 of file expr_manager.h.

Referenced by clear().

Current value of the simplifier cache tag.

The cached values of calls to Simplify are valid as long as their cache tag matches this tag. Caches can then be invalidated by incrementing this tag.

Definition at line 153 of file expr_manager.h.

Disable garbage collection.

This flag disables the garbage collection. Normally, it's set in the destructor, so that we can delete all remaining expressions without GC getting in the way.

Definition at line 159 of file expr_manager.h.

Referenced by clear(), gc(), isActive(), and ~ExprManager().

Postpone deleting garbage-collected expressions.

Useful during manipulation of context, especially at the time of backtracking, since we may have objects with circular dependencies (like find pointers).

The postponed expressions will be deleted the next time the garbage collector is called after this flag is cleared.

Definition at line 168 of file expr_manager.h.

Referenced by gc(), and resumeGC().

std::vector<ExprValue*> CVC3::ExprManager::d_postponed [private]

Vector of postponed garbage-collected expressions.

Definition at line 170 of file expr_manager.h.

Referenced by gc(), and resumeGC().

bool CVC3::ExprManager::d_inGC [private]

Flag for whether GC is already running.

Definition at line 173 of file expr_manager.h.

Referenced by gc().

std::deque<ExprValue*> CVC3::ExprManager::d_pending [private]

Queue of pending exprs to GC.

Definition at line 175 of file expr_manager.h.

Referenced by gc().

Rebuild cache.

Definition at line 178 of file expr_manager.h.

Referenced by rebuild(), and rebuildRec().

Instance of TypeComputer: must be registered.

Definition at line 197 of file expr_manager.h.

Referenced by checkType(), computeType(), and finiteTypeInfo().


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