CVC3::ExprManager Class Reference

#include <expr_manager.h>

Collaboration diagram for CVC3::ExprManager:

[legend]

List of all members.

Classes

class EqEV
Private class for d_exprSet. More...
class HashEV
Private class for d_exprSet. More...
class HashString
Private class for hashing strings. More...
class TypeComputer
Abstract class for computing expr type. More...

Public Member Functions

ExprManager (ContextManager *cm, const CLFlags &flags)
Constructor.
~ExprManager ()
Destructor.
void clear ()
Free up all memory and delete all the expressions.
bool isActive ()
Check if the ExprManager is still active (clear() was not called).
void gc (ExprValue *ev)
Garbage collect the ExprValue pointer.
void postponeGC ()
Postpone deletion of garbage-collected expressions.
void resumeGC ()
Resume deletion of garbage-collected expressions.
Expr rebuild (const Expr &e)
Rebuild the Expr with this ExprManager if it belongs to another ExprManager.
ExprIndex nextIndex ()
Return the next Expr index.
ExprIndex lastIndex ()
void clearFlags ()
Clears the generic Expr flag in all Exprs.
const Expr & boolExpr ()
BOOLEAN Expr.
const Expr & falseExpr ()
FALSE Expr.
const Expr & trueExpr ()
TRUE Expr.
const std::vector< Expr > & getEmptyVector ()
References to empty objects (used in ExprValue).
const Expr & getNullExpr ()
References to empty objects (used in ExprValue).
Expr newExpr (ExprValue *ev)
Return either an existing or a new Expr matching ev.
Expr newLeafExpr (const Op &op)
Expr newStringExpr (const std::string &s)
Expr newRatExpr (const Rational &r)
Expr newSkolemExpr (const Expr &e, int i)
Expr newVarExpr (const std::string &s)
Expr newSymbolExpr (const std::string &s, int kind)
Expr newBoundVarExpr (const std::string &name, const std::string &uid)
Expr newBoundVarExpr (const std::string &name, const std::string &uid, const Type &type)
Expr newBoundVarExpr (const Type &type)
Expr newClosureExpr (int kind, const Expr &var, const Expr &body)
Expr newClosureExpr (int kind, const std::vector< Expr > &vars, const Expr &body)
Expr newClosureExpr (int kind, const std::vector< Expr > &vars, const Expr &body, const std::vector< std::vector< Expr > > &trigs)
Expr andExpr (const std::vector< Expr > &children)
Expr orExpr (const std::vector< Expr > &children)
size_t hash (const Expr &e) const
Hash function for a single Expr.
ContextManager * getCM () const
Fetch our ContextManager.
Context * getCurrentContext () const
Get the current context from our ContextManager.
int scopelevel ()
Get current scope level.
void setTM (TheoremManager *tm)
Set the TheoremManager.
TheoremManager * getTM () const
Fetch the TheoremManager.
MemoryManager * getMM (size_t MMIndex)
Return a MemoryManager for the given ExprValue type.
unsigned getSimpCacheTag () const
Get the simplifier's cache tag.
void invalidateSimpCache ()
Invalidate the simplifier's cache tag.
void registerTypeComputer (TypeComputer *typeComputer)
Register type computer.
int printDepth () const
Get printing depth.
bool withIndentation () const
Whether to print with indentation.
int lineWidth () const
Suggested line width for printing with indentation.
int indent () const
Get initial indentation.
int indent (int n, bool permanent=false)
Set initial indentation. Returns the previous permanent value.
int incIndent (int n, bool permanent=false)
Increment the current transient indentation by n.
void restoreIndent ()
Set transient indentation to permanent.
InputLanguage getInputLang () const
Get the input language for printing.
InputLanguage getOutputLang () const
Get the output language for printing.
bool dagPrinting () const
Whether to print Expr's as DAGs.
PrettyPrinter * getPrinter () const
Return the pretty-printer if there is one; otherwise return NULL.
void newKind (int kind, const std::string &name, bool isType=false)
Register a new kind.
void registerPrettyPrinter (PrettyPrinter &printer)
Register the pretty-printer (can only do it if none registered).
void unregisterPrettyPrinter ()
Tell ExprManager that the printer is no longer valid.
bool isKindRegistered (int kind)
Returns true if kind is built into CVC or has been registered via newKind.
bool isTypeKind (int kind)
Check if a kind represents a type.
const std::string & getKindName (int kind)
Return the name associated with a kind. The kind must already be registered.
int getKind (const std::string &name)
Return a kind associated with a name. Returns NULL_KIND if not found.
size_t registerSubclass (size_t sizeOfSubclass)
Register a new subclass of ExprValue.
unsigned long getMemory (int verbosity)
Calculate memory usage.

Private Types

typedef std::hash_set
< ExprValue *, HashEV, EqEV > ExprValueSet
Hash set type for uniquifying expressions.

Private Member Functions

size_t hash (const ExprValue *ev) const
void installExprValue (ExprValue *ev)
Expr rebuildRec (const Expr &e)
Cached recursive descent. Must be called only during rebuild().
ExprValue * newExprValue (ExprValue *ev)
Return either an existing or a new ExprValue matching ev.
unsigned getFlag ()
Return the current Expr flag counter.
unsigned nextFlag ()
Increment and return the Expr flag counter (this clears all the flags).
void computeType (const Expr &e)
Compute the type of the Expr.
void checkType (const Expr &e)
Check well-formedness of a type Expr.
Cardinality finiteTypeInfo (Expr &e, Unsigned &n, bool enumerate, bool computeSize)
Get information related to finiteness of a type.

Private Attributes

ContextManager * d_cm
For backtracking attributes.
TheoremManager * d_tm
Needed for Refl Theorems.
ExprManagerNotifyObj * d_notifyObj
Notification on pop().
ExprIndex d_index
Index counter for Expr compare().
unsigned d_flagCounter
Counter for a generic Expr flag.
std::hash_map< int, std::string > d_kindMap
The database of registered kinds.
std::hash_set< int > d_typeKinds
The set of kinds representing a type.
std::hash_map< std::string,
int, HashString > d_kindMapByName
The reverse map of names to kinds.
PrettyPrinter * d_prettyPrinter
The registered pretty-printer, a connector to theory-specific pretty-printers.
const int * d_printDepth
Print upto the given depth, replace the rest with "...". -1==unlimited depth.
const bool * d_withIndentation
Whether to print with indentation.
int d_indent
Permanent indentation.
int d_indentTransient
Transient indentation.
const int * d_lineWidth
Suggested line width for printing with indentation.
const std::string * d_inputLang
Input language (printing).
const std::string * d_outputLang
Output language (printing).
const bool * d_dagPrinting
Whether to print Expr's as DAGs.
const std::string d_mmFlag
Which memory manager to use (copy the flag value and keep it the same).
ExprValueSet d_exprSet
Hash set for uniquifying expressions.
std::vector< MemoryManager * > d_mm
Array of memory managers for subclasses of ExprValue.
std::hash< void * > d_pointerHash
A hash function for hashing pointers.
Expr d_bool
Expr constants cached for fast access.
Expr d_false
Expr d_true
std::vector< Expr > d_emptyVec
Empty vector of Expr to return by reference as empty vector of children.
Expr d_nullExpr
Null Expr to return by reference, for efficiency.
unsigned d_simpCacheTagCurrent
Current value of the simplifier cache tag.
bool d_disableGC
Disable garbage collection.
bool d_postponeGC
Postpone deleting garbage-collected expressions.
std::vector< ExprValue * > d_postponed
Vector of postponed garbage-collected expressions.
bool d_inGC
Flag for whether GC is already running.
std::deque< ExprValue * > d_pending
Queue of pending exprs to GC.
ExprHashMap< Expr > d_rebuildCache
Rebuild cache.
TypeComputer * d_typeComputer
Instance of TypeComputer: must be registered.

Friends

class Expr
class ExprValue
class Op
class HashEV
class Type

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

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

size_t CVC3::ExprManager::hash ( const ExprValue * ev ) const [inline, private]

Definition at line 445 of file expr_manager.h.

References DebugAssert, and CVC3::ExprValue::hash().

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

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

Definition at line 36 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(), getMemory(), 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().

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]