38 DebugAssert(isActive(),
"ExprManager::installExprValue(ExprValue*)");
65 d_exprSet.insert(p_ev);
72 : d_cm(cm), d_index(0), d_flagCounter(1), d_prettyPrinter(NULL),
73 d_printDepth(&(flags[
"print-depth"].getInt())),
74 d_withIndentation(&(flags[
"indent"].getBool())),
75 d_indent(0), d_indentTransient(0),
76 d_lineWidth(&(flags[
"width"].getInt())),
77 d_inputLang(&(flags[
"lang"].getString())),
78 d_outputLang(&(flags[
"output-lang"].getString())),
79 d_dagPrinting(&(flags[
"dagify-exprs"].getBool())),
80 d_mmFlag(flags[
"mm"].getString()),
83 d_simpCacheTagCurrent(1), d_disableGC(false), d_postponeGC(false),
84 d_inGC(false), d_typeComputer(NULL)
133 TRACE_MSG(
"delete",
"~ExprManager: deleting d_mm's {");
134 for(
size_t i=0; i<
d_mm.size(); ++i)
137 TRACE_MSG(
"delete",
"~ExprManager: finished deleting d_mm's }");
147 TRACE(
"delete",
"clear: number of remaining Exprs: ",
160 vector<ExprValue*> exprs;
162 TRACE_MSG(
"delete",
"clear:() collecting exprs { ");
166 TRACE(
"delete",
"expr[", n++,
"]");
169 TRACE_MSG(
"delete",
"clear(): finished collecting exprs }");
171 TRACE_MSG(
"delete",
"clear(): deleting exprs { ");
172 for(vector<ExprValue*>::iterator i=exprs.begin(), iend=exprs.end();
177 d_mm[tp]->deleteData(pExpr);
179 TRACE_MSG(
"delete",
"clear(): finished deleting exprs }");
198 d_mm[tp]->deleteData(ev);
204 d_mm[tp]->deleteData(ev);
219 d_mm[tp]->deleteData(ev);
232 "ExprManager::rebuild is called on inactive ExprManager");
239 DebugAssert(!d_inRebuild,
"ExprManager::rebuild()");
256 if(j!=jend)
return (*j).second;
279 if (ev->d_type.isNull()) ev->d_type = t;
280 if (ev->d_type != t) {
281 throw Exception(
"Types don't match in rebuildRec");
291 if(i != iend)
return (*i);
361 const std::string* langPtr
373 DebugAssert(
false,
"CVC3::ExprManager::newKind(kind = "
376 "this kind is already registered with a different name: "
382 DebugAssert(
false,
"CVC3::ExprManager::newKind(kind = "
385 "this kind name is already registered with a different index: "
393 " printer is already registered");
400 " printer is not registered");
407 (
"CVC3::ExprManager::getKindName(kind = "
408 +
int2string(kind) +
"): kind is not registered.").c_str());
417 else return (*i).second;
422 size_t idx(
d_mm.size());
436 unsigned long mem = 0;
461 return mem + memSelf;
490 #define REG(k) em.newKind(k, #k)
491 #define REG_TYPE(k) em.newKind(k, #k, true)
void computeType(const Expr &e)
Compute the type of the Expr.
std::vector< Expr > d_emptyVec
Empty vector of Expr to return by reference as empty vector of children.
Expr rebuildRec(const Expr &e)
Cached recursive descent. Must be called only during rebuild()
ExprValue * d_expr
The value. This is the only data member in this class.
std::deque< ExprValue * > d_pending
Queue of pending exprs to GC.
ExprValue * rebuild(ExprManager *em) const
Make a clean copy of itself using the given ExprManager.
size_type count(const _Key &key) const
Data structure of expressions in CVC3.
int d_indent
Permanent indentation.
TypeComputer * d_typeComputer
Instance of TypeComputer: must be registered.
ExprManager * getEM() const
PrettyPrinter * d_prettyPrinter
The registered pretty-printer, a connector to theory-specific pretty-printers.
Expr d_nullExpr
Null Expr to return by reference, for efficiency.
ExprValue * newExprValue(ExprValue *ev)
Return either an existing or a new ExprValue matching ev.
virtual size_t getMMIndex() const
Get unique memory manager ID.
void installExprValue(ExprValue *ev)
virtual void computeType(const Expr &e)=0
Compute the type of e.
void checkType(const Expr &e)
Check well-formedness of a type Expr.
int incIndent(int n, bool permanent=false)
Increment the current transient indentation by n.
std::vector< ExprValue * > d_postponed
Vector of postponed garbage-collected expressions.
bool isActive()
Check if the ExprManager is still active (clear() was not called)
Private class for d_exprSet.
_hash_table::iterator iterator
InputLanguage
Different input languages.
InputLanguage getInputLang() const
Get the input language for printing.
static unsigned long getString(int verbosity, const std::string &s)
void unregisterPrettyPrinter()
Tell ExprManager that the printer is no longer valid.
MS C++ specific settings.
const std::string * d_inputLang
Input language (printing)
size_t registerSubclass(size_t sizeOfSubclass)
Register a new subclass of ExprValue.
void clear()
Free up all memory and delete all the expressions.
Notifies ExprManager before and after each pop()
bool d_postponeGC
Postpone deleting garbage-collected expressions.
const std::string * d_outputLang
Output language (printing)
void registerPrettyPrinter(PrettyPrinter &printer)
Register the pretty-printer (can only do it if none registered)
#define DebugAssert(cond, str)
ExprHashMap< Expr > d_rebuildCache
Rebuild cache.
unsigned long getMemory(int verbosity)
Calculate memory usage.
Context * getCurrentContext()
ContextManager * d_cm
For backtracking attributes.
#define TRACE_MSG(flag, msg)
const Expr & getExpr() const
const std::string & getKindName(int kind)
Return the name associated with a kind. The kind must already be registered.
std::hash_map< std::string, int, HashString > d_kindMapByName
The reverse map of names to kinds.
MemoryManager * getMM(size_t MMIndex)
Return a MemoryManager for the given ExprValue type.
virtual ExprValue * copy(ExprManager *em, ExprIndex idx) const
Make a clean copy of itself using the given ExprManager.
std::hash_set< int > d_typeKinds
The set of kinds representing a type.
Identifier is (ID (STRING_EXPR "name"))
#define FatalAssert(cond, msg)
If something goes horribly wrong, print a message and abort immediately with exit(1).
Application of functions and predicates.
std::string toString() const
Print the expression to a string.
void resumeGC()
Resume deletion of garbage-collected expressions.
Expr newLeafExpr(const Op &op)
void newKind(int kind, const std::string &name, bool isType=false)
Register a new kind.
std::string int2string(int n)
bool d_inGC
Flag for whether GC is already running.
size_type erase(const key_type &key)
static void registerKinds(ExprManager &em)
iterator begin()
iterators
virtual void deleteData(void *d)=0
std::pair< iterator, bool > insert(const value_type &entry)
Private class for d_exprSet.
static void print(std::string name, int verbosity, unsigned long memSelf, unsigned long mem)
int indent() const
Get initial indentation.
std::hash_map< int, std::string > d_kindMap
The database of registered kinds.
A "closure" expression which binds variables used in the "body". Used by LAMBDA and quantifiers...
ExprManager(ContextManager *cm, const CLFlags &flags)
Constructor.
void setType(const Type &t) const
Set the cached type.
virtual void checkType(const Expr &e)=0
Check that e is a valid Type expr.
int getKind(const std::string &name)
Return a kind associated with a name. Returns NULL_KIND if not found.
Expr d_bool
Expr constants cached for fast access.
ExprManagerNotifyObj * d_notifyObj
Notification on pop()
const std::string d_mmFlag
Which memory manager to use (copy the flag value and keep it the same)
bool d_disableGC
Disable garbage collection.
void gc(ExprValue *ev)
Garbage collect the ExprValue pointer.
ExprIndex nextIndex()
Return the next Expr index.
Expr rebuild(const Expr &e)
Rebuild the Expr with this ExprManager if it belongs to another ExprManager.
Type d_type
The cached type of the expression (may be Null)
InputLanguage getLanguage(const std::string &lang)
The base class for holding the actual data in expressions.
Cardinality
Enum for cardinality of types.
Manager for multiple contexts. Also holds current context.
virtual Cardinality finiteTypeInfo(Expr &e, Unsigned &n, bool enumerate, bool computeSize)=0
Get information related to finiteness of a type.
Type getType() const
Get the type. Recursively compute if necessary.
int d_indentTransient
Transient indentation.
ExprValueSet d_exprSet
Hash set for uniquifying expressions.
std::vector< MemoryManager * > d_mm
Array of memory managers for subclasses of ExprValue.
Abstract API to a pretty-printer for Expr.
A class which sets a boolean value to true when created, and resets to false when deleted...
static Type typeBool(ExprManager *em)
iterator find(const key_type &key)
operations
Cardinality finiteTypeInfo(Expr &e, Unsigned &n, bool enumerate, bool computeSize)
Get information related to finiteness of a type.
InputLanguage getOutputLang() const
Get the output language for printing.