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

Generated on Tue Jul 3 14:33:36 2007 for CVC3 by  doxygen 1.5.1