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)