00001
00002
00003
00004
00005
00006
00007
00008
00009
00010
00011
00012
00013
00014
00015
00016
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
00033
00034 static void registerKinds(ExprManager& em);
00035
00036
00037 ExprManager::ExprManager(ContextManager* cm, const CLFlags& flags)
00038
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
00054 d_notifyObj = new ExprManagerNotifyObj(this, d_cm->getCurrentContext());
00055
00056
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
00094 ExprManager::~ExprManager() {
00095 FatalAssert(d_emptyVec.size()==0, "~ExprManager()");
00096 delete d_notifyObj;
00097
00098 d_disableGC = false;
00099 clear();
00100 d_disableGC = true;
00101
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
00113
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
00122 d_bool = Expr();
00123 d_false = Expr();
00124 d_true = Expr();
00125
00126
00127
00128
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());
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
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
00183
00184 Expr ExprManager::rebuild(const Expr& e) {
00185
00186
00187 DebugAssert(!e.isNull(), "ExprManager::rebuild called on Null Expr");
00188
00189 DebugAssert(isActive() && e.getEM()->isActive(),
00190 "ExprManager::rebuild is called on inactive ExprManager");
00191
00192 if(e.isNull() || (e.getEM() == this)) {
00193
00194 return e;
00195 }
00196
00197 DebugAssert(!d_inRebuild, "ExprManager::rebuild()");
00198 IF_DEBUG(ScopeWatcher sw(&d_inRebuild));
00199
00200 if(d_rebuildCache.size() > 0) d_rebuildCache.clear();
00201 Expr res = rebuildRec(e);
00202
00203 if(d_rebuildCache.size() > 0) d_rebuildCache.clear();
00204
00205 return res;
00206 }
00207
00208
00209 Expr ExprManager::rebuildRec(const Expr& e) {
00210 DebugAssert(d_inRebuild, "ExprManager::rebuildRec("+e.toString()+")");
00211
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
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
00229 Expr res(ev);
00230
00231 d_rebuildCache[e] = res;
00232
00233
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
00251
00252 ExprValue* p_ev = ev->copy(this, nextIndex());
00253 d_exprSet.insert(p_ev);
00254 return p_ev;
00255 }
00256
00257
00258
00259
00260
00261
00262
00263
00264
00265
00266
00267
00268
00269
00270
00271
00272
00273
00274
00275
00276
00277
00278
00279
00280
00281
00282
00283
00284
00285
00286
00287
00288
00289
00290 void ExprManager::installExprValue(ExprValue* p_ev)
00291 {
00292 DebugAssert(isActive(), "ExprManager::installExprValue(ExprValue*)");
00293
00294
00295
00296
00297
00298
00299
00300
00301
00302
00303
00304
00305
00306
00307
00308
00309
00310
00311
00312
00313
00314
00315
00316
00317
00318
00319 d_exprSet.insert(p_ev);
00320 }
00321
00322
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
00332
00333
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
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
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
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
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
00443 em.newKind(BOOLEAN, "_BOOLEAN", true);
00444
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
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
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
00541
00542
00543
00544
00545
00546
00547
00548
00549
00550
00551
00552
00553
00554
00555
00556
00557
00558
00559
00560
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
00580
00581
00582
00583
00584
00585
00586
00587
00588
00589
00590
00591
00592
00593
00594
00595
00596
00597
00598
00599 }
00600
00601
00602 void ExprManagerNotifyObj::notifyPre() {
00603 d_em->postponeGC();
00604 }
00605
00606
00607 void ExprManagerNotifyObj::notify() {
00608 d_em->resumeGC();
00609 }