CVC3

expr_manager.cpp

Go to the documentation of this file.
00001 /*****************************************************************************/
00002 /*!
00003  * \file expr_manager.cpp
00004  *
00005  * Author: Sergey Berezin
00006  *
00007  * Created: Wed Dec  4 14:20:56 2002
00008  *
00009  * <hr>
00010  *
00011  * License to use, copy, modify, sell and/or distribute this software
00012  * and its documentation for any purpose is hereby granted without
00013  * royalty, subject to the terms and conditions defined in the \ref
00014  * LICENSE file provided with this distribution.
00015  *
00016  * <hr>
00017  *
00018  */
00019 /*****************************************************************************/
00020 
00021 #include "expr_manager.h"
00022 #include "command_line_flags.h"
00023 #include "expr_stream.h"
00024 #include "pretty_printer.h"
00025 #include "memory_manager_malloc.h"
00026 #include "memory_manager_chunks.h"
00027 
00028 using namespace CVC3;
00029 
00030 using namespace std;
00031 
00032 // File-local function which registers all the commonly declared
00033 // kinds (defined below)
00034 static void registerKinds(ExprManager& em);
00035 
00036 void ExprManager::installExprValue(ExprValue* p_ev)
00037 {
00038   DebugAssert(isActive(), "ExprManager::installExprValue(ExprValue*)");
00039 //   int maxHeight = 0;
00040 //   p_ev->d_highestKid = 0;
00041 //   for (unsigned i = 0; i < p_ev->arity(); i++)
00042 //   {
00043 //     int height = p_ev->getKids()[i].getHeight();
00044 //     if (height > maxHeight)
00045 //     {
00046 //       maxHeight = height;
00047 //       p_ev->d_highestKid = i;
00048 //     }
00049 //   }
00050 
00051 //   if (p_ev->d_kind == ITE && p_ev->arity() == 3)
00052 //   {
00053 //     if (p_ev->getKids()[1].getHeight() > p_ev->getKids()[2].getHeight())
00054 //       p_ev->d_highestKid = 1;
00055 //     else
00056 //       p_ev->d_highestKid = 2;
00057 //   }
00058 
00059 //   switch (p_ev->d_kind) {
00060 //   case NOT: case AND: case OR: case ITE: case IFF: case IMPLIES:
00061 //     maxHeight++;
00062 //   }
00063 //   p_ev->d_height = maxHeight;
00064 
00065   d_exprSet.insert(p_ev);
00066 }
00067 
00068 
00069 // Constructor
00070 ExprManager::ExprManager(ContextManager* cm, const CLFlags& flags)
00071   // Initial number of buckets is 1024 (it's kinda arbitrary)
00072   : d_cm(cm), d_index(0), d_flagCounter(1), d_prettyPrinter(NULL),
00073     d_printDepth(&(flags["print-depth"].getInt())),
00074     d_withIndentation(&(flags["indent"].getBool())),
00075     d_indent(0), d_indentTransient(0),
00076     d_lineWidth(&(flags["width"].getInt())),
00077     d_inputLang(&(flags["lang"].getString())),
00078     d_outputLang(&(flags["output-lang"].getString())),
00079     d_dagPrinting(&(flags["dagify-exprs"].getBool())),
00080     d_mmFlag(flags["mm"].getString()),
00081     d_exprSet(1024, HashEV(this), EqEV()),
00082     d_mm(EXPR_VALUE_TYPE_LAST),
00083     d_simpCacheTagCurrent(1), d_disableGC(false), d_postponeGC(false),
00084     d_inGC(false), d_typeComputer(NULL)
00085 {
00086   // Initialize the notifier
00087   d_notifyObj = new ExprManagerNotifyObj(this, d_cm->getCurrentContext());
00088 
00089   // Initialize core memory managers
00090   if(d_mmFlag == "chunks") {
00091     d_mm[EXPR_VALUE] = new MemoryManagerChunks(sizeof(ExprValue));
00092     d_mm[EXPR_NODE] = new MemoryManagerChunks(sizeof(ExprNode));
00093     d_mm[EXPR_APPLY] = new MemoryManagerChunks(sizeof(ExprApply));
00094     d_mm[EXPR_STRING] = new MemoryManagerChunks(sizeof(ExprString));
00095     d_mm[EXPR_RATIONAL] = new MemoryManagerChunks(sizeof(ExprRational));
00096     d_mm[EXPR_UCONST] = new MemoryManagerChunks(sizeof(ExprVar));
00097     d_mm[EXPR_SYMBOL] = new MemoryManagerChunks(sizeof(ExprSymbol));
00098     d_mm[EXPR_BOUND_VAR] = new MemoryManagerChunks(sizeof(ExprBoundVar));
00099     d_mm[EXPR_CLOSURE] = new MemoryManagerChunks(sizeof(ExprClosure));
00100     d_mm[EXPR_SKOLEM] = new MemoryManagerChunks(sizeof(ExprSkolem));
00101   } else {
00102     d_mm[EXPR_VALUE] = new MemoryManagerMalloc();
00103     d_mm[EXPR_NODE] = new MemoryManagerMalloc();
00104     d_mm[EXPR_APPLY] = new MemoryManagerMalloc();
00105     d_mm[EXPR_STRING] = new MemoryManagerMalloc();
00106     d_mm[EXPR_RATIONAL] = new MemoryManagerMalloc();
00107     d_mm[EXPR_UCONST] = new MemoryManagerMalloc();
00108     d_mm[EXPR_SYMBOL] = new MemoryManagerMalloc();
00109     d_mm[EXPR_BOUND_VAR] = new MemoryManagerMalloc();
00110     d_mm[EXPR_CLOSURE] = new MemoryManagerMalloc();
00111     d_mm[EXPR_SKOLEM] = new MemoryManagerMalloc();
00112   }
00113   registerKinds(*this);
00114 
00115   d_bool = newLeafExpr(BOOLEAN);
00116   d_false = newLeafExpr(FALSE_EXPR);
00117   d_false.setType(Type::typeBool(this));
00118   d_true = newLeafExpr(TRUE_EXPR);
00119   d_true.setType(Type::typeBool(this));
00120 
00121   IF_DEBUG(d_inRebuild = false;)
00122 }
00123 
00124 // Destructor
00125 ExprManager::~ExprManager() {
00126   FatalAssert(d_emptyVec.size()==0, "~ExprManager()");
00127   delete d_notifyObj;
00128   // Make sure garbage collector doesn't get in the way
00129   d_disableGC = false;    //  clear() will assert this.
00130   clear();
00131   d_disableGC = true;
00132   // Destroy memory managers
00133   TRACE_MSG("delete", "~ExprManager: deleting d_mm's {");
00134   for(size_t i=0; i<d_mm.size(); ++i)
00135     delete d_mm[i];
00136 
00137   TRACE_MSG("delete", "~ExprManager: finished deleting d_mm's }");
00138 }
00139 
00140 
00141 void ExprManager::clear() {
00142   FatalAssert(isActive(), "ExprManager::clear()");
00143   // Make ExprManager inactive, but keep all the Exprs intact
00144   // Remove all internal expressions.
00145   d_disableGC = true;
00146 
00147   TRACE("delete", "clear: number of remaining Exprs: ",
00148   d_exprSet.size(), flush);
00149 
00150   FatalAssert(d_nullExpr.isNull(), "ExprManager::clear()");
00151 
00152   // Set class-local Exprs to Null
00153   d_bool = Expr();
00154   d_false = Expr();
00155   d_true = Expr();
00156 
00157   // Save all the pointers, clear the hash set, then free the
00158   // pointers.  Erasing one pointer at a time requires rehashing,
00159   // which will segfault if some pointers are already deleted.
00160   vector<ExprValue*> exprs;
00161   exprs.reserve(d_exprSet.size());
00162   TRACE_MSG("delete", "clear:() collecting exprs { ");
00163   IF_DEBUG(int n(0);)
00164   for(ExprValueSet::iterator i=d_exprSet.begin(), iend=d_exprSet.end();
00165       i!=iend; ++i) {
00166     TRACE("delete", "expr[", n++, "]");
00167     exprs.push_back(*i);
00168   }
00169   TRACE_MSG("delete", "clear(): finished collecting exprs }");
00170   d_exprSet.clear();
00171   TRACE_MSG("delete", "clear(): deleting exprs { ");
00172   for(vector<ExprValue*>::iterator i=exprs.begin(), iend=exprs.end();
00173       i!=iend; ++i) {
00174     ExprValue *pExpr= *i;
00175     size_t tp(pExpr->getMMIndex()); // which memory manager to use
00176     delete (pExpr);
00177     d_mm[tp]->deleteData(pExpr);
00178   }
00179   TRACE_MSG("delete", "clear(): finished deleting exprs }");
00180 
00181 }
00182 
00183 
00184 bool ExprManager::isActive() { return !d_disableGC; }
00185 
00186 
00187 // Garbage collect the ExprValue pointer
00188 void ExprManager::gc(ExprValue* ev) {
00189   if(!d_disableGC) {
00190     d_exprSet.erase(ev);
00191     if (d_inGC) d_pending.push_back(ev);
00192     else if (d_postponeGC) d_postponed.push_back(ev);
00193     else {
00194       IF_DEBUG(FatalAssert(d_pending.size() == 0, "Expected size 1");)
00195       d_inGC = true;
00196       size_t tp = ev->getMMIndex();
00197       delete ev;
00198       d_mm[tp]->deleteData(ev);
00199       while (d_pending.size() > 0) {
00200         ev = d_pending.front();
00201         d_pending.pop_front();
00202         tp = ev->getMMIndex();
00203         delete ev;
00204         d_mm[tp]->deleteData(ev);
00205       }
00206       d_inGC = false;
00207     }
00208   }
00209 }
00210 
00211 void
00212 ExprManager::resumeGC() {
00213   d_postponeGC = false;
00214   while(d_postponed.size()>0) {
00215     ExprValue* ev = d_postponed.back();
00216     size_t tp(ev->getMMIndex());
00217     d_postponed.pop_back();
00218     delete ev;
00219     d_mm[tp]->deleteData(ev);
00220   }
00221 }
00222 
00223 
00224 // Rebuild the Expr with this ExprManager if it belongs to another
00225 // ExprManager
00226 Expr ExprManager::rebuild(const Expr& e) {
00227   //  TRACE("expr", "rebuild(", e, ") {");
00228   // Shouldn't rebuild a Null Expr (it's a bug)
00229   DebugAssert(!e.isNull(), "ExprManager::rebuild called on Null Expr");
00230   // Both ExprManagers must be active
00231   DebugAssert(isActive() && e.getEM()->isActive(),
00232         "ExprManager::rebuild is called on inactive ExprManager");
00233   // If e has the same ExprManager, no rebuilding is necessary
00234   if(e.isNull() || (e.getEM() == this)) {
00235     //    TRACE_MSG("expr", "rebuild (same EM) => }");
00236     return e;
00237   }
00238   // Gotta rebuild
00239   DebugAssert(!d_inRebuild, "ExprManager::rebuild()");
00240   IF_DEBUG(ScopeWatcher sw(&d_inRebuild);)
00241   // First, clear the cache
00242   if(d_rebuildCache.size() > 0) d_rebuildCache.clear();
00243   Expr res = rebuildRec(e);
00244   // Leave no trail behind (free up Exprs)
00245   if(d_rebuildCache.size() > 0) d_rebuildCache.clear();
00246   //  TRACE("expr", "rebuild => ", e, " }");
00247   return res;
00248 }
00249 
00250 
00251 Expr ExprManager::rebuildRec(const Expr& e) {
00252   DebugAssert(d_inRebuild, "ExprManager::rebuildRec("+e.toString()+")");
00253   // Check cache
00254   ExprHashMap<Expr>::iterator j=d_rebuildCache.find(e),
00255     jend=d_rebuildCache.end();
00256   if(j!=jend) return (*j).second;
00257 
00258   ExprValue* ev = e.d_expr->rebuild(this);
00259   // Uniquify the pointer
00260   ExprValueSet::iterator i(d_exprSet.find(ev)), iend(d_exprSet.end());
00261   if(i != iend) {
00262     MemoryManager* mm = getMM(ev->getMMIndex());
00263     delete ev;
00264     mm->deleteData(ev);
00265     ev = *i;
00266   } else {
00267     ev->setIndex(nextIndex());
00268     d_exprSet.insert(ev);
00269   }
00270   // Use non-uniquifying Expr() constructor
00271   Expr res(ev);
00272   // Cache the result
00273   d_rebuildCache[e] = res;
00274 
00275   // Rebuild the type too
00276   Type t;
00277   if (!e.d_expr->d_type.isNull()) {
00278     t = Type(rebuildRec(e.d_expr->d_type.getExpr()));
00279     if (ev->d_type.isNull()) ev->d_type = t;
00280     if (ev->d_type != t) {
00281       throw Exception("Types don't match in rebuildRec");
00282     }
00283   }
00284   return res;
00285 }
00286 
00287 
00288 ExprValue* ExprManager::newExprValue(ExprValue* ev) {
00289   DebugAssert(isActive(), "ExprManager::newExprValue(ExprValue*)");
00290   ExprValueSet::iterator i(d_exprSet.find(ev)), iend(d_exprSet.end());
00291   if(i != iend) return (*i);
00292   // No such ExprValue.  Create a clean copy, insert it into the set
00293   // and return the new pointer.
00294   ExprValue* p_ev = ev->copy(this, nextIndex());
00295   d_exprSet.insert(p_ev);
00296   return p_ev;
00297 }
00298 
00299 
00300 // ExprValue* ExprManager::newExprValue(const Expr& op,
00301 //             const vector<Expr>& kids) {
00302 //   // Check if op and kids have the same ExprManager
00303 //   DebugAssert(isActive(), "ExprManager::newExprValue(op, kids)");
00304 //   DebugAssert(this == op.getEM(),
00305 //        "ExprManager::newExprValue(op, kids): op is from a wrong "
00306 //        "ExprManager/ValidityChecker, call importExpr() first:\n"
00307 //        +op.toString());
00308 //   IF_DEBUG(
00309 //     for(vector<Expr>::const_iterator i=kids.begin(), iend=kids.end();
00310 //  i!=iend; ++i)
00311 //       DebugAssert(!i->isNull() && (i->getEM() == this),
00312 //      "ExprManager::newExprValue(op, kids): the child is"
00313 //      " from a wrong instance of ExprManager/ValidityChecker,"
00314 //      "call importExpr() first:\n"
00315 //      +i->toString());
00316 //     )
00317 //   ExprValue* res = op.d_expr->copy(this, kids);
00318 //   ExprValueSet::iterator i(d_exprSet.find(res)), iend(d_exprSet.end());
00319 //   if(i != iend) {
00320 //     MemoryManager* mm = getMM(res->getMMIndex());
00321 //     delete res;
00322 //     mm->deleteData(res);
00323 //     return (*i);
00324 //   } else {
00325 //     res->setIndex(nextIndex());
00326 //     installExprValue(res);
00327 //     return res;
00328 //   }
00329 // }
00330 
00331 
00332 //! Set initial indentation.  Returns the previous permanent value.
00333 int
00334 ExprManager::indent(int n, bool permanent) {
00335   int ret(d_indent);
00336   d_indentTransient = n;
00337   if(permanent) d_indent = n;
00338   return ret;
00339 }
00340 
00341 //! Increment the current transient indentation by n
00342 /*! If the second argument is true, sets the result as permanent.
00343   \return previous permanent value. */
00344 int
00345 ExprManager::incIndent(int n, bool permanent) {
00346   int ret(d_indent);
00347   d_indentTransient += n;
00348   if(permanent) d_indent = d_indentTransient;
00349   return ret;
00350 }
00351 
00352 // Various options
00353 InputLanguage
00354 ExprManager::getInputLang() const {
00355   return getLanguage(*d_inputLang);
00356 }
00357 
00358 
00359 InputLanguage
00360 ExprManager::getOutputLang() const {
00361   const std::string* langPtr
00362     = (*d_outputLang == "")? d_inputLang : d_outputLang;
00363   return getLanguage(*langPtr);
00364 }
00365 
00366 
00367 void ExprManager::newKind(int kind, const string &name, bool isType) {
00368   if(d_kindMap.count(kind) == 0) {
00369     d_kindMap[kind] = name;
00370     if(isType) d_typeKinds.insert(kind);
00371   }
00372   else if(d_kindMap[kind] != name) {
00373     DebugAssert(false, "CVC3::ExprManager::newKind(kind = "
00374     + int2string(kind) + ", name = " + name
00375     + "): \n" +
00376     "this kind is already registered with a different name: "
00377     + d_kindMap[kind]);
00378   }
00379   if(d_kindMapByName.count(name) == 0)
00380     d_kindMapByName[name] = kind;
00381   else if(d_kindMapByName[name] != kind) {
00382     DebugAssert(false, "CVC3::ExprManager::newKind(kind = "
00383     + int2string(kind) + ", name = " + name
00384     + "): \n" +
00385     "this kind name is already registered with a different index: "
00386     + int2string(d_kindMapByName[name]));
00387   }
00388 }
00389 
00390 // Register a printer
00391 void ExprManager::registerPrettyPrinter(PrettyPrinter& printer) {
00392   DebugAssert(d_prettyPrinter==NULL, "ExprManager:registerPrettyPrinter():"
00393         " printer is already registered");
00394   d_prettyPrinter = &printer;
00395 }
00396 
00397 // Unregister a printer
00398 void ExprManager::unregisterPrettyPrinter() {
00399   FatalAssert(d_prettyPrinter!=NULL, "ExprManager:unregisterPrettyPrinter():"
00400         " printer is not registered");
00401   d_prettyPrinter = NULL;
00402 }
00403 
00404 
00405 const string& ExprManager::getKindName(int kind) {
00406   DebugAssert(d_kindMap.count(kind) > 0,
00407         ("CVC3::ExprManager::getKindName(kind = "
00408          + int2string(kind) + "): kind is not registered.").c_str());
00409   return d_kindMap[kind];
00410 }
00411 
00412 int ExprManager::getKind(const string& name) {
00413   std::hash_map<std::string, int, HashString>::iterator
00414     i=d_kindMapByName.find(name),
00415     iend=d_kindMapByName.end();
00416   if(i==iend) return NULL_KIND;
00417   else return (*i).second;
00418 }
00419 
00420 
00421 size_t ExprManager::registerSubclass(size_t sizeOfSubclass) {
00422   size_t idx(d_mm.size());
00423   if(d_mmFlag == "chunks")
00424     d_mm.push_back(new MemoryManagerChunks(sizeOfSubclass));
00425   else
00426     d_mm.push_back(new MemoryManagerMalloc());
00427 
00428   FatalAssert(d_mm.back() != NULL, "Out of memory");
00429   return idx;
00430 }
00431 
00432 
00433 unsigned long ExprManager::getMemory(int verbosity)
00434 {
00435   unsigned long memSelf = sizeof(ExprManager);
00436   unsigned long mem = 0;
00437 
00438   //  mem += MemoryTracker::getHashMap(verbosity - 1, d_kindMap);
00439 
00440 //   mem += d_typeKinds.getMemory(verbosity - 1);
00441 //   mem += d_kindMapByName.getMemory(verbosity - 1);
00442 //   mem += d_prettyPrinter->getMemory(verbosity - 1);
00443   mem += MemoryTracker::getString(verbosity - 1, d_mmFlag);
00444 
00445 //   mem += d_exprSet.getMemory(verbosity - 1);
00446 //  mem += getMemoryVec(d_mm);
00447 //   for (i = 0; i < d_mm.size(); ++i) {
00448 //     mem += d_mm->getMemory(verbosity - 1);
00449 //   }
00450 
00451 //   mem += d_pointerHash.getMemory(verbosity - 1) - sizeof(hash<void*>);
00452 
00453 //  mem += getMemoryVec(d_emptyVec);
00454   //  mem += getMemoryVec(d_postponed);
00455 //   mem += d_rebuildCache.getMemory(verbosity - 1) - sizeof(ExprHashMap<Expr>);
00456 
00457 //   mem += d_typecomputer->getMemory(verbosity - 1);
00458 
00459   MemoryTracker::print("ExprManager", verbosity, memSelf, mem);
00460 
00461   return mem + memSelf;
00462 }
00463 
00464 
00465 void ExprManager::computeType(const Expr& e) {
00466   DebugAssert(d_typeComputer, "No type computer installed");
00467   d_typeComputer->computeType(e);
00468   DebugAssert(!e.getType().getExpr().isNull(), "Type not set by computeType");
00469 }
00470 
00471 
00472 void ExprManager::checkType(const Expr& e) {
00473   DebugAssert(d_typeComputer, "No type computer installed");
00474   if (!e.isValidType()) d_typeComputer->checkType(e);
00475   DebugAssert(e.isValidType(), "Type not checked by checkType");
00476 }
00477 
00478 
00479 Cardinality ExprManager::finiteTypeInfo(Expr& e,
00480                                         Unsigned& n,
00481                                         bool enumerate,
00482                                         bool computeSize)
00483 {
00484   DebugAssert(d_typeComputer, "No type computer installed");
00485   return d_typeComputer->finiteTypeInfo(e, n, enumerate, computeSize);
00486 }
00487 
00488 
00489 // Kind registration macro
00490 #define REG(k) em.newKind(k, #k)
00491 #define REG_TYPE(k) em.newKind(k, #k, true)
00492 
00493 static void registerKinds(ExprManager& em) {
00494   // Register type kinds
00495   em.newKind(BOOLEAN, "_BOOLEAN", true);
00496   //  REG(TUPLE_TYPE);
00497   em.newKind(ANY_TYPE, "_ANY_TYPE", true);
00498   em.newKind(ARROW, "_ARROW", true);
00499   em.newKind(TYPE, "_TYPE", true);
00500   em.newKind(TYPEDECL, "_TYPEDECL", true);
00501   em.newKind(TYPEDEF, "_TYPEDEF", true);
00502   em.newKind(SUBTYPE, "_SUBTYPE", true);
00503 
00504   // Register expression (non-type) kinds
00505   em.newKind(NULL_KIND, "_NULL_KIND");
00506 
00507   em.newKind(RAW_LIST, "_RAW_LIST");
00508   em.newKind(STRING_EXPR, "_STRING_EXPR");
00509   em.newKind(RATIONAL_EXPR, "_RATIONAL_EXPR");
00510   em.newKind(TRUE_EXPR, "_TRUE_EXPR");
00511   em.newKind(FALSE_EXPR, "_FALSE_EXPR");
00512 
00513   em.newKind(EQ, "_EQ");
00514   em.newKind(NEQ, "_NEQ");
00515   em.newKind(DISTINCT, "_DISTINCT");
00516 
00517   em.newKind(NOT, "_NOT");
00518   em.newKind(AND, "_AND");
00519   em.newKind(OR, "_OR");
00520   em.newKind(XOR, "_XOR");
00521   em.newKind(IFF, "_IFF");
00522   em.newKind(IMPLIES, "_IMPLIES");
00523 
00524   em.newKind(AND_R, "_AND_R");
00525   em.newKind(IFF_R, "_IFF_R");
00526   em.newKind(ITE_R, "_ITE_R");
00527 
00528   em.newKind(ITE, "_ITE");
00529 
00530   em.newKind(FORALL, "_FORALL");
00531   em.newKind(EXISTS, "_EXISTS");
00532 
00533   em.newKind(UFUNC, "_UFUNC");
00534   em.newKind(APPLY, "_APPLY");
00535 
00536   em.newKind(ASSERT, "_ASSERT");
00537   em.newKind(QUERY, "_QUERY");
00538   em.newKind(CHECKSAT, "_CHECKSAT");
00539   em.newKind(CONTINUE, "_CONTINUE");
00540   em.newKind(RESTART, "_RESTART");
00541   em.newKind(DBG, "_DBG");
00542   em.newKind(TRACE, "_TRACE");
00543   em.newKind(UNTRACE, "_UNTRACE");
00544   em.newKind(OPTION, "_OPTION");
00545   em.newKind(HELP, "_HELP");
00546   em.newKind(TRANSFORM, "_TRANSFORM");
00547   em.newKind(PRINT, "_PRINT");
00548   em.newKind(CALL, "_CALL");
00549   em.newKind(ECHO, "_ECHO");
00550   em.newKind(INCLUDE, "_INCLUDE");
00551   em.newKind(GET_VALUE, "_GET_VALUE");
00552   em.newKind(GET_ASSIGNMENT, "_GET_ASSIGNMENT");
00553   em.newKind(DUMP_PROOF, "_DUMP_PROOF");
00554   em.newKind(DUMP_ASSUMPTIONS, "_DUMP_ASSUMPTIONS");
00555   em.newKind(DUMP_SIG, "_DUMP_SIG");
00556   em.newKind(DUMP_TCC, "_DUMP_TCC");
00557   em.newKind(DUMP_TCC_ASSUMPTIONS, "_DUMP_TCC_ASSUMPTIONS");
00558   em.newKind(DUMP_TCC_PROOF, "_DUMP_TCC_PROOF");
00559   em.newKind(DUMP_CLOSURE, "_DUMP_CLOSURE");
00560   em.newKind(DUMP_CLOSURE_PROOF, "_DUMP_CLOSURE_PROOF");
00561   em.newKind(WHERE, "_WHERE");
00562   em.newKind(ASSERTIONS, "_ASSERTIONS");
00563   em.newKind(ASSUMPTIONS, "_ASSUMPTIONS");
00564   em.newKind(COUNTEREXAMPLE, "_COUNTEREXAMPLE");
00565   em.newKind(COUNTERMODEL, "_COUNTERMODEL");
00566   em.newKind(PUSH, "_PUSH");
00567   em.newKind(POP, "_POP");
00568   em.newKind(POPTO, "_POPTO");
00569   em.newKind(PUSH_SCOPE, "_PUSH_SCOPE");
00570   em.newKind(POP_SCOPE, "_POP_SCOPE");
00571   em.newKind(POPTO_SCOPE, "_POPTO_SCOPE");
00572   em.newKind(RESET, "_RESET");
00573   em.newKind(CONTEXT, "_CONTEXT");
00574   em.newKind(FORGET, "_FORGET");
00575   em.newKind(GET_TYPE, "_GET_TYPE");
00576   em.newKind(CHECK_TYPE, "_CHECK_TYPE");
00577   em.newKind(GET_CHILD, "_GET_CHILD");
00578   em.newKind(SUBSTITUTE, "_SUBSTITUTE");
00579   em.newKind(SEQ, "_SEQ");
00580   em.newKind(ARITH_VAR_ORDER, "_ARITH_VAR_ORDER");
00581   em.newKind(ANNOTATION, "_ANNOTATION");
00582 
00583   // Kinds used mostly in the parser
00584 
00585   em.newKind(TCC, "_TCC");
00586   em.newKind(ID, "_ID");
00587   em.newKind(VARDECL, "_VARDECL");
00588   em.newKind(VARDECLS, "_VARDECLS");
00589 
00590 
00591   em.newKind(BOUND_VAR, "_BOUND_VAR");
00592   em.newKind(BOUND_ID, "_BOUND_ID");
00593 
00594   em.newKind(SKOLEM_VAR, "_SKOLEM_VAR");
00595   em.newKind(THEOREM_KIND, "_THEOREM_KIND");
00596 
00597 //   em.newKind(UPDATE, "_UPDATE");
00598 //   em.newKind(UPDATE_SELECT, "_UPDATE_SELECT");
00599 
00600 //   em.newKind(RECORD_TYPE, "_RECORD_TYPE");
00601 //   em.newKind(RECORD, "_RECORD");
00602 //   em.newKind(RECORD_SELECT, "_RECORD_SELECT");
00603 //   em.newKind(RECORD_UPDATE, "_RECORD_UPDATE");
00604 
00605 //   em.newKind(TUPLE, "_TUPLE");
00606 //   em.newKind(TUPLE_SELECT, "_TUPLE_SELECT");
00607 //   em.newKind(TUPLE_UPDATE, "_TUPLE_UPDATE");
00608 
00609 //   em.newKind(SUBRANGE, "_SUBRANGE");
00610 
00611 //   em.newKind(SCALARTYPE, "_SCALARTYPE");
00612 //   em.newKind(DATATYPE, "_DATATYPE");
00613 //   em.newKind(THISTYPE, "_THISTYPE");
00614 //   em.newKind(CONSTRUCTOR, "_CONSTRUCTOR");
00615 //   em.newKind(SELECTOR, "_SELECTOR");
00616 //   em.newKind(TESTER, "_TESTER");
00617   //  em.newKind(DATATYPE_UPDATE, "_DATATYPE_UPDATE");
00618 
00619   em.newKind(IF, "_IF");
00620   em.newKind(IFTHEN, "_IFTHEN");
00621   em.newKind(ELSE, "_ELSE");
00622   em.newKind(COND, "_COND");
00623 
00624   em.newKind(LET, "_LET");
00625   em.newKind(LETDECLS, "_LETDECLS");
00626   em.newKind(LETDECL, "_LETDECL");
00627 
00628   em.newKind(LAMBDA, "_LAMBDA");
00629   em.newKind(SIMULATE, "_SIMULATE");
00630 
00631   em.newKind(CONST, "_CONST");
00632   em.newKind(VARLIST, "_VARLIST");
00633   em.newKind(UCONST, "_UCONST");
00634   em.newKind(DEFUN, "_DEFUN");
00635 
00636   // Arithmetic types and operators
00637 //   em.newKind(REAL, "_REAL");
00638 //   em.newKind(INT, "_INT");
00639 
00640 //   em.newKind(UMINUS, "_UMINUS");
00641 //   em.newKind(PLUS, "_PLUS");
00642 //   em.newKind(MINUS, "_MINUS");
00643 //   em.newKind(MULT, "_MULT");
00644 //   em.newKind(DIVIDE, "_DIVIDE");
00645 //   em.newKind(POW, "_POW");
00646 //   em.newKind(INTDIV, "_INTDIV");
00647 //   em.newKind(MOD, "_MOD");
00648 //   em.newKind(LT, "_LT");
00649 //   em.newKind(LE, "_LE");
00650 //   em.newKind(GT, "_GT");
00651 //   em.newKind(GE, "_GE");
00652 //   em.newKind(IS_INTEGER, "_IS_INTEGER");
00653 //   em.newKind(NEGINF, "_NEGINF");
00654 //   em.newKind(POSINF, "_POSINF");
00655 //   em.newKind(FLOOR, "_FLOOR");
00656 }
00657 
00658 
00659 void ExprManagerNotifyObj::notifyPre() {
00660   d_em->postponeGC();
00661 }
00662 
00663 
00664 void ExprManagerNotifyObj::notify() {
00665   d_em->resumeGC();
00666 }