CVC3::ExprManager Class Reference

#include <expr_manager.h>

Collaboration diagram for CVC3::ExprManager:

Collaboration graph
[legend]
List of all members.

Public Member Functions

Private Types

Private Member Functions

Private Attributes

Friends

Classes


Detailed Description

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

typedef std::hash_set<ExprValue*, HashEV, EqEV> CVC3::ExprManager::ExprValueSet [private]

Hash set type for uniquifying expressions.

Definition at line 129 of file expr_manager.h.


Member Function Documentation

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

Definition at line 290 of file expr_manager.cpp.

References d_exprSet, DebugAssert, Hash::hash_set< _Key, _HashFcn, _EqualKey >::insert(), and isActive().


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

ContextManager* CVC3::ExprManager::d_cm [private]

For backtracking attributes.

Definition at line 65 of file expr_manager.h.

Referenced by ExprManager().

TheoremManager* CVC3::ExprManager::d_tm [private]

Needed for Refl Theorems.

Definition at line 66 of file expr_manager.h.

ExprManagerNotifyObj* CVC3::ExprManager::d_notifyObj [private]

Notification on pop().

Definition at line 67 of file expr_manager.h.

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

ExprIndex CVC3::ExprManager::d_index [private]

Index counter for Expr compare().

Definition at line 68 of file expr_manager.h.

unsigned CVC3::ExprManager::d_flagCounter [private]

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().

std::hash_set<int> CVC3::ExprManager::d_typeKinds [private]

The set of kinds representing a type.

Definition at line 74 of file expr_manager.h.

Referenced by newKind().

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

The reverse map of names to kinds.

Definition at line 84 of file expr_manager.h.

Referenced by getKind(), and newKind().

PrettyPrinter* CVC3::ExprManager::d_prettyPrinter [private]

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.

int CVC3::ExprManager::d_indent [private]

Permanent indentation.

Definition at line 99 of file expr_manager.h.

Referenced by incIndent(), and indent().

int CVC3::ExprManager::d_indentTransient [private]

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(), and registerSubclass().

ExprValueSet CVC3::ExprManager::d_exprSet [private]

Hash set for uniquifying expressions.

Definition at line 131 of file expr_manager.h.

Referenced by clear(), gc(), installExprValue(), 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().

std::hash<void*> CVC3::ExprManager::d_pointerHash [private]

A hash function for hashing pointers.

Definition at line 136 of file expr_manager.h.

Expr CVC3::ExprManager::d_bool [private]

Expr constants cached for fast access.

Definition at line 139 of file expr_manager.h.

Referenced by clear(), and ExprManager().

Expr CVC3::ExprManager::d_false [private]

Definition at line 140 of file expr_manager.h.

Referenced by clear(), and ExprManager().

Expr CVC3::ExprManager::d_true [private]

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().

Expr CVC3::ExprManager::d_nullExpr [private]

Null Expr to return by reference, for efficiency.

Definition at line 145 of file expr_manager.h.

Referenced by clear().

unsigned CVC3::ExprManager::d_simpCacheTagCurrent [private]

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.

bool CVC3::ExprManager::d_disableGC [private]

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().

bool CVC3::ExprManager::d_postponeGC [private]

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().

ExprHashMap<Expr> CVC3::ExprManager::d_rebuildCache [private]

Rebuild cache.

Definition at line 172 of file expr_manager.h.

Referenced by rebuild(), and rebuildRec().

bool CVC3::ExprManager::d_inRebuild [private]

Definition at line 173 of file expr_manager.h.

Referenced by ExprManager(), rebuild(), and rebuildRec().

TypeComputer* CVC3::ExprManager::d_typeComputer [private]

Instance of TypeComputer: must be registered.

Definition at line 188 of file expr_manager.h.

Referenced by checkType(), and computeType().


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