CVC3
2.4.1
|
Expression Manager. More...
#include <expr_manager.h>
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. More... | |
~ExprManager () | |
Destructor. More... | |
void | clear () |
Free up all memory and delete all the expressions. More... | |
bool | isActive () |
Check if the ExprManager is still active (clear() was not called) More... | |
void | gc (ExprValue *ev) |
Garbage collect the ExprValue pointer. More... | |
void | postponeGC () |
Postpone deletion of garbage-collected expressions. More... | |
void | resumeGC () |
Resume deletion of garbage-collected expressions. More... | |
Expr | rebuild (const Expr &e) |
Rebuild the Expr with this ExprManager if it belongs to another ExprManager. More... | |
ExprIndex | nextIndex () |
Return the next Expr index. More... | |
ExprIndex | lastIndex () |
void | clearFlags () |
Clears the generic Expr flag in all Exprs. More... | |
const Expr & | boolExpr () |
BOOLEAN Expr. More... | |
const Expr & | falseExpr () |
FALSE Expr. More... | |
const Expr & | trueExpr () |
TRUE Expr. More... | |
const std::vector< Expr > & | getEmptyVector () |
References to empty objects (used in ExprValue) More... | |
const Expr & | getNullExpr () |
References to empty objects (used in ExprValue) More... | |
Expr | newExpr (ExprValue *ev) |
Return either an existing or a new Expr matching ev. More... | |
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 Expr &trigger) |
Expr | newClosureExpr (int kind, const std::vector< Expr > &vars, const Expr &body, const std::vector< Expr > &triggers) |
Expr | newClosureExpr (int kind, const std::vector< Expr > &vars, const Expr &body, const std::vector< std::vector< Expr > > &triggers) |
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. More... | |
ContextManager * | getCM () const |
Fetch our ContextManager. More... | |
Context * | getCurrentContext () const |
Get the current context from our ContextManager. More... | |
int | scopelevel () |
Get current scope level. More... | |
void | setTM (TheoremManager *tm) |
Set the TheoremManager. More... | |
TheoremManager * | getTM () const |
Fetch the TheoremManager. More... | |
MemoryManager * | getMM (size_t MMIndex) |
Return a MemoryManager for the given ExprValue type. More... | |
unsigned | getSimpCacheTag () const |
Get the simplifier's cache tag. More... | |
void | invalidateSimpCache () |
Invalidate the simplifier's cache tag. More... | |
void | registerTypeComputer (TypeComputer *typeComputer) |
Register type computer. More... | |
int | printDepth () const |
Get printing depth. More... | |
bool | withIndentation () const |
Whether to print with indentation. More... | |
int | lineWidth () const |
Suggested line width for printing with indentation. More... | |
int | indent () const |
Get initial indentation. More... | |
int | indent (int n, bool permanent=false) |
Set initial indentation. Returns the previous permanent value. More... | |
int | incIndent (int n, bool permanent=false) |
Increment the current transient indentation by n. More... | |
void | restoreIndent () |
Set transient indentation to permanent. More... | |
InputLanguage | getInputLang () const |
Get the input language for printing. More... | |
InputLanguage | getOutputLang () const |
Get the output language for printing. More... | |
bool | dagPrinting () const |
Whether to print Expr's as DAGs. More... | |
PrettyPrinter * | getPrinter () const |
Return the pretty-printer if there is one; otherwise return NULL. More... | |
void | newKind (int kind, const std::string &name, bool isType=false) |
Register a new kind. More... | |
void | registerPrettyPrinter (PrettyPrinter &printer) |
Register the pretty-printer (can only do it if none registered) More... | |
void | unregisterPrettyPrinter () |
Tell ExprManager that the printer is no longer valid. More... | |
bool | isKindRegistered (int kind) |
Returns true if kind is built into CVC or has been registered via newKind. More... | |
bool | isTypeKind (int kind) |
Check if a kind represents a type. More... | |
const std::string & | getKindName (int kind) |
Return the name associated with a kind. The kind must already be registered. More... | |
int | getKind (const std::string &name) |
Return a kind associated with a name. Returns NULL_KIND if not found. More... | |
size_t | registerSubclass (size_t sizeOfSubclass) |
Register a new subclass of ExprValue. More... | |
unsigned long | getMemory (int verbosity) |
Calculate memory usage. More... | |
Private Types | |
typedef std::hash_set < ExprValue *, HashEV, EqEV > | ExprValueSet |
Hash set type for uniquifying expressions. More... | |
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() More... | |
ExprValue * | newExprValue (ExprValue *ev) |
Return either an existing or a new ExprValue matching ev. More... | |
unsigned | getFlag () |
Return the current Expr flag counter. More... | |
unsigned | nextFlag () |
Increment and return the Expr flag counter (this clears all the flags) More... | |
void | computeType (const Expr &e) |
Compute the type of the Expr. More... | |
void | checkType (const Expr &e) |
Check well-formedness of a type Expr. More... | |
Cardinality | finiteTypeInfo (Expr &e, Unsigned &n, bool enumerate, bool computeSize) |
Get information related to finiteness of a type. More... | |
Private Attributes | |
ContextManager * | d_cm |
For backtracking attributes. More... | |
TheoremManager * | d_tm |
Needed for Refl Theorems. More... | |
ExprManagerNotifyObj * | d_notifyObj |
Notification on pop() More... | |
ExprIndex | d_index |
Index counter for Expr compare() More... | |
unsigned | d_flagCounter |
Counter for a generic Expr flag. More... | |
std::hash_map< int, std::string > | d_kindMap |
The database of registered kinds. More... | |
std::hash_set< int > | d_typeKinds |
The set of kinds representing a type. More... | |
std::hash_map< std::string, int, HashString > | d_kindMapByName |
The reverse map of names to kinds. More... | |
PrettyPrinter * | d_prettyPrinter |
The registered pretty-printer, a connector to theory-specific pretty-printers. More... | |
const int * | d_printDepth |
Print upto the given depth, replace the rest with "...". -1==unlimited depth. More... | |
const bool * | d_withIndentation |
Whether to print with indentation. More... | |
int | d_indent |
Permanent indentation. More... | |
int | d_indentTransient |
Transient indentation. More... | |
const int * | d_lineWidth |
Suggested line width for printing with indentation. More... | |
const std::string * | d_inputLang |
Input language (printing) More... | |
const std::string * | d_outputLang |
Output language (printing) More... | |
const bool * | d_dagPrinting |
Whether to print Expr's as DAGs. More... | |
const std::string | d_mmFlag |
Which memory manager to use (copy the flag value and keep it the same) More... | |
ExprValueSet | d_exprSet |
Hash set for uniquifying expressions. More... | |
std::vector< MemoryManager * > | d_mm |
Array of memory managers for subclasses of ExprValue. More... | |
std::hash< void * > | d_pointerHash |
A hash function for hashing pointers. More... | |
Expr | d_bool |
Expr constants cached for fast access. More... | |
Expr | d_false |
Expr | d_true |
std::vector< Expr > | d_emptyVec |
Empty vector of Expr to return by reference as empty vector of children. More... | |
Expr | d_nullExpr |
Null Expr to return by reference, for efficiency. More... | |
unsigned | d_simpCacheTagCurrent |
Current value of the simplifier cache tag. More... | |
bool | d_disableGC |
Disable garbage collection. More... | |
bool | d_postponeGC |
Postpone deleting garbage-collected expressions. More... | |
std::vector< ExprValue * > | d_postponed |
Vector of postponed garbage-collected expressions. More... | |
bool | d_inGC |
Flag for whether GC is already running. More... | |
std::deque< ExprValue * > | d_pending |
Queue of pending exprs to GC. More... | |
ExprHashMap< Expr > | d_rebuildCache |
Rebuild cache. More... | |
TypeComputer * | d_typeComputer |
Instance of TypeComputer: must be registered. More... | |
Friends | |
class | Expr |
class | ExprValue |
class | Op |
class | HashEV |
class | Type |
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.
|
private |
Hash set type for uniquifying expressions.
Definition at line 129 of file expr_manager.h.
|
private |
Definition at line 36 of file expr_manager.cpp.
References DebugAssert.
|
friend |
Definition at line 59 of file expr_manager.h.
Referenced by clear().
|
friend |
Definition at line 60 of file expr_manager.h.
|
friend |
Definition at line 61 of file expr_manager.h.
|
friend |
Definition at line 62 of file expr_manager.h.
|
friend |
Definition at line 63 of file expr_manager.h.
Referenced by rebuildRec().
|
private |
For backtracking attributes.
Definition at line 65 of file expr_manager.h.
Referenced by ExprManager().
|
private |
Needed for Refl Theorems.
Definition at line 66 of file expr_manager.h.
|
private |
Notification on pop()
Definition at line 67 of file expr_manager.h.
Referenced by ExprManager(), and ~ExprManager().
|
private |
Index counter for Expr compare()
Definition at line 68 of file expr_manager.h.
|
private |
Counter for a generic Expr flag.
Definition at line 69 of file expr_manager.h.
|
private |
The database of registered kinds.
Definition at line 72 of file expr_manager.h.
Referenced by getKindName(), and newKind().
|
private |
The set of kinds representing a type.
Definition at line 74 of file expr_manager.h.
Referenced by newKind().
|
private |
The reverse map of names to kinds.
Definition at line 84 of file expr_manager.h.
|
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().
|
private |
Print upto the given depth, replace the rest with "...". -1==unlimited depth.
Definition at line 95 of file expr_manager.h.
|
private |
Whether to print with indentation.
Definition at line 97 of file expr_manager.h.
|
private |
Permanent indentation.
Definition at line 99 of file expr_manager.h.
Referenced by incIndent(), and indent().
|
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().
|
private |
Suggested line width for printing with indentation.
Definition at line 105 of file expr_manager.h.
|
private |
Input language (printing)
Definition at line 107 of file expr_manager.h.
Referenced by getInputLang(), and getOutputLang().
|
private |
Output language (printing)
Definition at line 109 of file expr_manager.h.
Referenced by getOutputLang().
|
private |
Whether to print Expr's as DAGs.
Definition at line 111 of file expr_manager.h.
|
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().
|
private |
Hash set for uniquifying expressions.
Definition at line 131 of file expr_manager.h.
Referenced by clear(), gc(), newExprValue(), and rebuildRec().
|
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().
|
private |
A hash function for hashing pointers.
Definition at line 136 of file expr_manager.h.
|
private |
Expr constants cached for fast access.
Definition at line 139 of file expr_manager.h.
Referenced by clear(), and ExprManager().
|
private |
Definition at line 140 of file expr_manager.h.
Referenced by clear(), and ExprManager().
|
private |
Definition at line 141 of file expr_manager.h.
Referenced by clear(), and ExprManager().
|
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().
|
private |
Null Expr to return by reference, for efficiency.
Definition at line 145 of file expr_manager.h.
Referenced by clear().
|
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.
|
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().
|
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().
|
private |
Vector of postponed garbage-collected expressions.
Definition at line 170 of file expr_manager.h.
Referenced by gc(), and resumeGC().
|
private |
Flag for whether GC is already running.
Definition at line 173 of file expr_manager.h.
Referenced by gc().
|
private |
|
private |
Rebuild cache.
Definition at line 178 of file expr_manager.h.
Referenced by rebuild(), and rebuildRec().
|
private |
Instance of TypeComputer: must be registered.
Definition at line 197 of file expr_manager.h.
Referenced by checkType(), computeType(), and finiteTypeInfo().