1 /*****************************************************************************/
2 /*!
3 * \file expr_manager.cpp
4 *
5 * Author: Sergey Berezin
6 *
7 * Created: Wed Dec 4 14:20:56 2002
8 *
9 * <hr>
10 *
11 * License to use, copy, modify, sell and/or distribute this software
12 * and its documentation for any purpose is hereby granted without
13 * royalty, subject to the terms and conditions defined in the \ref
14 * LICENSE file provided with this distribution.
15 *
16 * <hr>
17 *
18 */
19 /*****************************************************************************/
20
21 #include "expr_manager.h"
22 #include "command_line_flags.h"
23 #include "expr_stream.h"
24 #include "pretty_printer.h"
25 #include "memory_manager_malloc.h"
26 #include "memory_manager_chunks.h"
27
28 using namespace CVC3;
29
30 using namespace std;
31
32 // File-local function which registers all the commonly declared
33 // kinds (defined below)
34 static void registerKinds(ExprManager& em);
35
installExprValue(ExprValue * p_ev)36 void ExprManager::installExprValue(ExprValue* p_ev)
37 {
38 DebugAssert(isActive(), "ExprManager::installExprValue(ExprValue*)");
39 // int maxHeight = 0;
40 // p_ev->d_highestKid = 0;
41 // for (unsigned i = 0; i < p_ev->arity(); i++)
42 // {
43 // int height = p_ev->getKids()[i].getHeight();
44 // if (height > maxHeight)
45 // {
46 // maxHeight = height;
47 // p_ev->d_highestKid = i;
48 // }
49 // }
50
51 // if (p_ev->d_kind == ITE && p_ev->arity() == 3)
52 // {
53 // if (p_ev->getKids()[1].getHeight() > p_ev->getKids()[2].getHeight())
54 // p_ev->d_highestKid = 1;
55 // else
56 // p_ev->d_highestKid = 2;
57 // }
58
59 // switch (p_ev->d_kind) {
60 // case NOT: case AND: case OR: case ITE: case IFF: case IMPLIES:
61 // maxHeight++;
62 // }
63 // p_ev->d_height = maxHeight;
64
65 d_exprSet.insert(p_ev);
66 }
67
68
69 // Constructor
ExprManager(ContextManager * cm,const CLFlags & flags)70 ExprManager::ExprManager(ContextManager* cm, const CLFlags& flags)
71 // Initial number of buckets is 1024 (it's kinda arbitrary)
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()),
81 d_exprSet(1024, HashEV(this), EqEV()),
82 d_mm(EXPR_VALUE_TYPE_LAST),
83 d_simpCacheTagCurrent(1), d_disableGC(false), d_postponeGC(false),
84 d_inGC(false), d_typeComputer(NULL)
85 {
86 // Initialize the notifier
87 d_notifyObj = new ExprManagerNotifyObj(this, d_cm->getCurrentContext());
88
89 // Initialize core memory managers
90 if(d_mmFlag == "chunks") {
91 d_mm[EXPR_VALUE] = new MemoryManagerChunks(sizeof(ExprValue));
92 d_mm[EXPR_NODE] = new MemoryManagerChunks(sizeof(ExprNode));
93 d_mm[EXPR_APPLY] = new MemoryManagerChunks(sizeof(ExprApply));
94 d_mm[EXPR_STRING] = new MemoryManagerChunks(sizeof(ExprString));
95 d_mm[EXPR_RATIONAL] = new MemoryManagerChunks(sizeof(ExprRational));
96 d_mm[EXPR_UCONST] = new MemoryManagerChunks(sizeof(ExprVar));
97 d_mm[EXPR_SYMBOL] = new MemoryManagerChunks(sizeof(ExprSymbol));
98 d_mm[EXPR_BOUND_VAR] = new MemoryManagerChunks(sizeof(ExprBoundVar));
99 d_mm[EXPR_CLOSURE] = new MemoryManagerChunks(sizeof(ExprClosure));
100 d_mm[EXPR_SKOLEM] = new MemoryManagerChunks(sizeof(ExprSkolem));
101 } else {
102 d_mm[EXPR_VALUE] = new MemoryManagerMalloc();
103 d_mm[EXPR_NODE] = new MemoryManagerMalloc();
104 d_mm[EXPR_APPLY] = new MemoryManagerMalloc();
105 d_mm[EXPR_STRING] = new MemoryManagerMalloc();
106 d_mm[EXPR_RATIONAL] = new MemoryManagerMalloc();
107 d_mm[EXPR_UCONST] = new MemoryManagerMalloc();
108 d_mm[EXPR_SYMBOL] = new MemoryManagerMalloc();
109 d_mm[EXPR_BOUND_VAR] = new MemoryManagerMalloc();
110 d_mm[EXPR_CLOSURE] = new MemoryManagerMalloc();
111 d_mm[EXPR_SKOLEM] = new MemoryManagerMalloc();
112 }
113 registerKinds(*this);
114
115 d_bool = newLeafExpr(BOOLEAN);
116 d_false = newLeafExpr(FALSE_EXPR);
117 d_false.setType(Type::typeBool(this));
118 d_true = newLeafExpr(TRUE_EXPR);
119 d_true.setType(Type::typeBool(this));
120
121 IF_DEBUG(d_inRebuild = false;)
122 }
123
124 // Destructor
~ExprManager()125 ExprManager::~ExprManager() {
126 FatalAssert(d_emptyVec.size()==0, "~ExprManager()");
127 delete d_notifyObj;
128 // Make sure garbage collector doesn't get in the way
129 d_disableGC = false; // clear() will assert this.
130 clear();
131 d_disableGC = true;
132 // Destroy memory managers
133 TRACE_MSG("delete", "~ExprManager: deleting d_mm's {");
134 for(size_t i=0; i<d_mm.size(); ++i)
135 delete d_mm[i];
136
137 TRACE_MSG("delete", "~ExprManager: finished deleting d_mm's }");
138 }
139
140
clear()141 void ExprManager::clear() {
142 FatalAssert(isActive(), "ExprManager::clear()");
143 // Make ExprManager inactive, but keep all the Exprs intact
144 // Remove all internal expressions.
145 d_disableGC = true;
146
147 TRACE("delete", "clear: number of remaining Exprs: ",
148 d_exprSet.size(), flush);
149
150 FatalAssert(d_nullExpr.isNull(), "ExprManager::clear()");
151
152 // Set class-local Exprs to Null
153 d_bool = Expr();
154 d_false = Expr();
155 d_true = Expr();
156
157 // Save all the pointers, clear the hash set, then free the
158 // pointers. Erasing one pointer at a time requires rehashing,
159 // which will segfault if some pointers are already deleted.
160 vector<ExprValue*> exprs;
161 exprs.reserve(d_exprSet.size());
162 TRACE_MSG("delete", "clear:() collecting exprs { ");
163 IF_DEBUG(int n(0);)
164 for(ExprValueSet::iterator i=d_exprSet.begin(), iend=d_exprSet.end();
165 i!=iend; ++i) {
166 TRACE("delete", "expr[", n++, "]");
167 exprs.push_back(*i);
168 }
169 TRACE_MSG("delete", "clear(): finished collecting exprs }");
170 d_exprSet.clear();
171 TRACE_MSG("delete", "clear(): deleting exprs { ");
172 for(vector<ExprValue*>::iterator i=exprs.begin(), iend=exprs.end();
173 i!=iend; ++i) {
174 ExprValue *pExpr= *i;
175 size_t tp(pExpr->getMMIndex()); // which memory manager to use
176 delete (pExpr);
177 d_mm[tp]->deleteData(pExpr);
178 }
179 TRACE_MSG("delete", "clear(): finished deleting exprs }");
180
181 }
182
183
isActive()184 bool ExprManager::isActive() { return !d_disableGC; }
185
186
187 // Garbage collect the ExprValue pointer
gc(ExprValue * ev)188 void ExprManager::gc(ExprValue* ev) {
189 if(!d_disableGC) {
190 d_exprSet.erase(ev);
191 if (d_inGC) d_pending.push_back(ev);
192 else if (d_postponeGC) d_postponed.push_back(ev);
193 else {
194 IF_DEBUG(FatalAssert(d_pending.size() == 0, "Expected size 1");)
195 d_inGC = true;
196 size_t tp = ev->getMMIndex();
197 delete ev;
198 d_mm[tp]->deleteData(ev);
199 while (d_pending.size() > 0) {
200 ev = d_pending.front();
201 d_pending.pop_front();
202 tp = ev->getMMIndex();
203 delete ev;
204 d_mm[tp]->deleteData(ev);
205 }
206 d_inGC = false;
207 }
208 }
209 }
210
211 void
resumeGC()212 ExprManager::resumeGC() {
213 d_postponeGC = false;
214 while(d_postponed.size()>0) {
215 ExprValue* ev = d_postponed.back();
216 size_t tp(ev->getMMIndex());
217 d_postponed.pop_back();
218 delete ev;
219 d_mm[tp]->deleteData(ev);
220 }
221 }
222
223
224 // Rebuild the Expr with this ExprManager if it belongs to another
225 // ExprManager
rebuild(const Expr & e)226 Expr ExprManager::rebuild(const Expr& e) {
227 // TRACE("expr", "rebuild(", e, ") {");
228 // Shouldn't rebuild a Null Expr (it's a bug)
229 DebugAssert(!e.isNull(), "ExprManager::rebuild called on Null Expr");
230 // Both ExprManagers must be active
231 DebugAssert(isActive() && e.getEM()->isActive(),
232 "ExprManager::rebuild is called on inactive ExprManager");
233 // If e has the same ExprManager, no rebuilding is necessary
234 if(e.isNull() || (e.getEM() == this)) {
235 // TRACE_MSG("expr", "rebuild (same EM) => }");
236 return e;
237 }
238 // Gotta rebuild
239 DebugAssert(!d_inRebuild, "ExprManager::rebuild()");
240 IF_DEBUG(ScopeWatcher sw(&d_inRebuild);)
241 // First, clear the cache
242 if(d_rebuildCache.size() > 0) d_rebuildCache.clear();
243 Expr res = rebuildRec(e);
244 // Leave no trail behind (free up Exprs)
245 if(d_rebuildCache.size() > 0) d_rebuildCache.clear();
246 // TRACE("expr", "rebuild => ", e, " }");
247 return res;
248 }
249
250
rebuildRec(const Expr & e)251 Expr ExprManager::rebuildRec(const Expr& e) {
252 DebugAssert(d_inRebuild, "ExprManager::rebuildRec("+e.toString()+")");
253 // Check cache
254 ExprHashMap<Expr>::iterator j=d_rebuildCache.find(e),
255 jend=d_rebuildCache.end();
256 if(j!=jend) return (*j).second;
257
258 ExprValue* ev = e.d_expr->rebuild(this);
259 // Uniquify the pointer
260 ExprValueSet::iterator i(d_exprSet.find(ev)), iend(d_exprSet.end());
261 if(i != iend) {
262 MemoryManager* mm = getMM(ev->getMMIndex());
263 delete ev;
264 mm->deleteData(ev);
265 ev = *i;
266 } else {
267 ev->setIndex(nextIndex());
268 d_exprSet.insert(ev);
269 }
270 // Use non-uniquifying Expr() constructor
271 Expr res(ev);
272 // Cache the result
273 d_rebuildCache[e] = res;
274
275 // Rebuild the type too
276 Type t;
277 if (!e.d_expr->d_type.isNull()) {
278 t = Type(rebuildRec(e.d_expr->d_type.getExpr()));
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");
282 }
283 }
284 return res;
285 }
286
287
newExprValue(ExprValue * ev)288 ExprValue* ExprManager::newExprValue(ExprValue* ev) {
289 DebugAssert(isActive(), "ExprManager::newExprValue(ExprValue*)");
290 ExprValueSet::iterator i(d_exprSet.find(ev)), iend(d_exprSet.end());
291 if(i != iend) return (*i);
292 // No such ExprValue. Create a clean copy, insert it into the set
293 // and return the new pointer.
294 ExprValue* p_ev = ev->copy(this, nextIndex());
295 d_exprSet.insert(p_ev);
296 return p_ev;
297 }
298
299
300 // ExprValue* ExprManager::newExprValue(const Expr& op,
301 // const vector<Expr>& kids) {
302 // // Check if op and kids have the same ExprManager
303 // DebugAssert(isActive(), "ExprManager::newExprValue(op, kids)");
304 // DebugAssert(this == op.getEM(),
305 // "ExprManager::newExprValue(op, kids): op is from a wrong "
306 // "ExprManager/ValidityChecker, call importExpr() first:\n"
307 // +op.toString());
308 // IF_DEBUG(
309 // for(vector<Expr>::const_iterator i=kids.begin(), iend=kids.end();
310 // i!=iend; ++i)
311 // DebugAssert(!i->isNull() && (i->getEM() == this),
312 // "ExprManager::newExprValue(op, kids): the child is"
313 // " from a wrong instance of ExprManager/ValidityChecker,"
314 // "call importExpr() first:\n"
315 // +i->toString());
316 // )
317 // ExprValue* res = op.d_expr->copy(this, kids);
318 // ExprValueSet::iterator i(d_exprSet.find(res)), iend(d_exprSet.end());
319 // if(i != iend) {
320 // MemoryManager* mm = getMM(res->getMMIndex());
321 // delete res;
322 // mm->deleteData(res);
323 // return (*i);
324 // } else {
325 // res->setIndex(nextIndex());
326 // installExprValue(res);
327 // return res;
328 // }
329 // }
330
331
332 //! Set initial indentation. Returns the previous permanent value.
333 int
indent(int n,bool permanent)334 ExprManager::indent(int n, bool permanent) {
335 int ret(d_indent);
336 d_indentTransient = n;
337 if(permanent) d_indent = n;
338 return ret;
339 }
340
341 //! Increment the current transient indentation by n
342 /*! If the second argument is true, sets the result as permanent.
343 \return previous permanent value. */
344 int
incIndent(int n,bool permanent)345 ExprManager::incIndent(int n, bool permanent) {
346 int ret(d_indent);
347 d_indentTransient += n;
348 if(permanent) d_indent = d_indentTransient;
349 return ret;
350 }
351
352 // Various options
353 InputLanguage
getInputLang() const354 ExprManager::getInputLang() const {
355 return getLanguage(*d_inputLang);
356 }
357
358
359 InputLanguage
getOutputLang() const360 ExprManager::getOutputLang() const {
361 const std::string* langPtr
362 = (*d_outputLang == "")? d_inputLang : d_outputLang;
363 return getLanguage(*langPtr);
364 }
365
366
newKind(int kind,const string & name,bool isType)367 void ExprManager::newKind(int kind, const string &name, bool isType) {
368 if(d_kindMap.count(kind) == 0) {
369 d_kindMap[kind] = name;
370 if(isType) d_typeKinds.insert(kind);
371 }
372 else if(d_kindMap[kind] != name) {
373 DebugAssert(false, "CVC3::ExprManager::newKind(kind = "
374 + int2string(kind) + ", name = " + name
375 + "): \n" +
376 "this kind is already registered with a different name: "
377 + d_kindMap[kind]);
378 }
379 if(d_kindMapByName.count(name) == 0)
380 d_kindMapByName[name] = kind;
381 else if(d_kindMapByName[name] != kind) {
382 DebugAssert(false, "CVC3::ExprManager::newKind(kind = "
383 + int2string(kind) + ", name = " + name
384 + "): \n" +
385 "this kind name is already registered with a different index: "
386 + int2string(d_kindMapByName[name]));
387 }
388 }
389
390 // Register a printer
registerPrettyPrinter(PrettyPrinter & printer)391 void ExprManager::registerPrettyPrinter(PrettyPrinter& printer) {
392 DebugAssert(d_prettyPrinter==NULL, "ExprManager:registerPrettyPrinter():"
393 " printer is already registered");
394 d_prettyPrinter = &printer;
395 }
396
397 // Unregister a printer
unregisterPrettyPrinter()398 void ExprManager::unregisterPrettyPrinter() {
399 FatalAssert(d_prettyPrinter!=NULL, "ExprManager:unregisterPrettyPrinter():"
400 " printer is not registered");
401 d_prettyPrinter = NULL;
402 }
403
404
getKindName(int kind)405 const string& ExprManager::getKindName(int kind) {
406 DebugAssert(d_kindMap.count(kind) > 0,
407 ("CVC3::ExprManager::getKindName(kind = "
408 + int2string(kind) + "): kind is not registered.").c_str());
409 return d_kindMap[kind];
410 }
411
getKind(const string & name)412 int ExprManager::getKind(const string& name) {
413 std::hash_map<std::string, int, HashString>::iterator
414 i=d_kindMapByName.find(name),
415 iend=d_kindMapByName.end();
416 if(i==iend) return NULL_KIND;
417 else return (*i).second;
418 }
419
420
registerSubclass(size_t sizeOfSubclass)421 size_t ExprManager::registerSubclass(size_t sizeOfSubclass) {
422 size_t idx(d_mm.size());
423 if(d_mmFlag == "chunks")
424 d_mm.push_back(new MemoryManagerChunks(sizeOfSubclass));
425 else
426 d_mm.push_back(new MemoryManagerMalloc());
427
428 FatalAssert(d_mm.back() != NULL, "Out of memory");
429 return idx;
430 }
431
432
getMemory(int verbosity)433 unsigned long ExprManager::getMemory(int verbosity)
434 {
435 unsigned long memSelf = sizeof(ExprManager);
436 unsigned long mem = 0;
437
438 // mem += MemoryTracker::getHashMap(verbosity - 1, d_kindMap);
439
440 // mem += d_typeKinds.getMemory(verbosity - 1);
441 // mem += d_kindMapByName.getMemory(verbosity - 1);
442 // mem += d_prettyPrinter->getMemory(verbosity - 1);
443 mem += MemoryTracker::getString(verbosity - 1, d_mmFlag);
444
445 // mem += d_exprSet.getMemory(verbosity - 1);
446 // mem += getMemoryVec(d_mm);
447 // for (i = 0; i < d_mm.size(); ++i) {
448 // mem += d_mm->getMemory(verbosity - 1);
449 // }
450
451 // mem += d_pointerHash.getMemory(verbosity - 1) - sizeof(hash<void*>);
452
453 // mem += getMemoryVec(d_emptyVec);
454 // mem += getMemoryVec(d_postponed);
455 // mem += d_rebuildCache.getMemory(verbosity - 1) - sizeof(ExprHashMap<Expr>);
456
457 // mem += d_typecomputer->getMemory(verbosity - 1);
458
459 MemoryTracker::print("ExprManager", verbosity, memSelf, mem);
460
461 return mem + memSelf;
462 }
463
464
computeType(const Expr & e)465 void ExprManager::computeType(const Expr& e) {
466 DebugAssert(d_typeComputer, "No type computer installed");
467 d_typeComputer->computeType(e);
468 DebugAssert(!e.getType().getExpr().isNull(), "Type not set by computeType");
469 }
470
471
checkType(const Expr & e)472 void ExprManager::checkType(const Expr& e) {
473 DebugAssert(d_typeComputer, "No type computer installed");
474 if (!e.isValidType()) d_typeComputer->checkType(e);
475 DebugAssert(e.isValidType(), "Type not checked by checkType");
476 }
477
478
finiteTypeInfo(Expr & e,Unsigned & n,bool enumerate,bool computeSize)479 Cardinality ExprManager::finiteTypeInfo(Expr& e,
480 Unsigned& n,
481 bool enumerate,
482 bool computeSize)
483 {
484 DebugAssert(d_typeComputer, "No type computer installed");
485 return d_typeComputer->finiteTypeInfo(e, n, enumerate, computeSize);
486 }
487
488
489 // Kind registration macro
490 #define REG(k) em.newKind(k, #k)
491 #define REG_TYPE(k) em.newKind(k, #k, true)
492
registerKinds(ExprManager & em)493 static void registerKinds(ExprManager& em) {
494 // Register type kinds
495 em.newKind(BOOLEAN, "_BOOLEAN", true);
496 // REG(TUPLE_TYPE);
497 em.newKind(ANY_TYPE, "_ANY_TYPE", true);
498 em.newKind(ARROW, "_ARROW", true);
499 em.newKind(TYPE, "_TYPE", true);
500 em.newKind(TYPEDECL, "_TYPEDECL", true);
501 em.newKind(TYPEDEF, "_TYPEDEF", true);
502 em.newKind(SUBTYPE, "_SUBTYPE", true);
503
504 // Register expression (non-type) kinds
505 em.newKind(NULL_KIND, "_NULL_KIND");
506
507 em.newKind(RAW_LIST, "_RAW_LIST");
508 em.newKind(STRING_EXPR, "_STRING_EXPR");
509 em.newKind(RATIONAL_EXPR, "_RATIONAL_EXPR");
510 em.newKind(TRUE_EXPR, "_TRUE_EXPR");
511 em.newKind(FALSE_EXPR, "_FALSE_EXPR");
512
513 em.newKind(EQ, "_EQ");
514 em.newKind(NEQ, "_NEQ");
515 em.newKind(DISTINCT, "_DISTINCT");
516
517 em.newKind(NOT, "_NOT");
518 em.newKind(AND, "_AND");
519 em.newKind(OR, "_OR");
520 em.newKind(XOR, "_XOR");
521 em.newKind(IFF, "_IFF");
522 em.newKind(IMPLIES, "_IMPLIES");
523
524 em.newKind(AND_R, "_AND_R");
525 em.newKind(IFF_R, "_IFF_R");
526 em.newKind(ITE_R, "_ITE_R");
527
528 em.newKind(ITE, "_ITE");
529
530 em.newKind(FORALL, "_FORALL");
531 em.newKind(EXISTS, "_EXISTS");
532
533 em.newKind(UFUNC, "_UFUNC");
534 em.newKind(APPLY, "_APPLY");
535
536 em.newKind(ASSERT, "_ASSERT");
537 em.newKind(QUERY, "_QUERY");
538 em.newKind(CHECKSAT, "_CHECKSAT");
539 em.newKind(CONTINUE, "_CONTINUE");
540 em.newKind(RESTART, "_RESTART");
541 em.newKind(DBG, "_DBG");
542 em.newKind(TRACE, "_TRACE");
543 em.newKind(UNTRACE, "_UNTRACE");
544 em.newKind(OPTION, "_OPTION");
545 em.newKind(HELP, "_HELP");
546 em.newKind(TRANSFORM, "_TRANSFORM");
547 em.newKind(PRINT, "_PRINT");
548 em.newKind(CALL, "_CALL");
549 em.newKind(ECHO, "_ECHO");
550 em.newKind(INCLUDE, "_INCLUDE");
551 em.newKind(GET_VALUE, "_GET_VALUE");
552 em.newKind(GET_ASSIGNMENT, "_GET_ASSIGNMENT");
553 em.newKind(DUMP_PROOF, "_DUMP_PROOF");
554 em.newKind(DUMP_ASSUMPTIONS, "_DUMP_ASSUMPTIONS");
555 em.newKind(DUMP_SIG, "_DUMP_SIG");
556 em.newKind(DUMP_TCC, "_DUMP_TCC");
557 em.newKind(DUMP_TCC_ASSUMPTIONS, "_DUMP_TCC_ASSUMPTIONS");
558 em.newKind(DUMP_TCC_PROOF, "_DUMP_TCC_PROOF");
559 em.newKind(DUMP_CLOSURE, "_DUMP_CLOSURE");
560 em.newKind(DUMP_CLOSURE_PROOF, "_DUMP_CLOSURE_PROOF");
561 em.newKind(WHERE, "_WHERE");
562 em.newKind(ASSERTIONS, "_ASSERTIONS");
563 em.newKind(ASSUMPTIONS, "_ASSUMPTIONS");
564 em.newKind(COUNTEREXAMPLE, "_COUNTEREXAMPLE");
565 em.newKind(COUNTERMODEL, "_COUNTERMODEL");
566 em.newKind(PUSH, "_PUSH");
567 em.newKind(POP, "_POP");
568 em.newKind(POPTO, "_POPTO");
569 em.newKind(PUSH_SCOPE, "_PUSH_SCOPE");
570 em.newKind(POP_SCOPE, "_POP_SCOPE");
571 em.newKind(POPTO_SCOPE, "_POPTO_SCOPE");
572 em.newKind(RESET, "_RESET");
573 em.newKind(CONTEXT, "_CONTEXT");
574 em.newKind(FORGET, "_FORGET");
575 em.newKind(GET_TYPE, "_GET_TYPE");
576 em.newKind(CHECK_TYPE, "_CHECK_TYPE");
577 em.newKind(GET_CHILD, "_GET_CHILD");
578 em.newKind(SUBSTITUTE, "_SUBSTITUTE");
579 em.newKind(SEQ, "_SEQ");
580 em.newKind(ARITH_VAR_ORDER, "_ARITH_VAR_ORDER");
581 em.newKind(ANNOTATION, "_ANNOTATION");
582
583 // Kinds used mostly in the parser
584
585 em.newKind(TCC, "_TCC");
586 em.newKind(ID, "_ID");
587 em.newKind(VARDECL, "_VARDECL");
588 em.newKind(VARDECLS, "_VARDECLS");
589
590
591 em.newKind(BOUND_VAR, "_BOUND_VAR");
592 em.newKind(BOUND_ID, "_BOUND_ID");
593
594 em.newKind(SKOLEM_VAR, "_SKOLEM_VAR");
595 em.newKind(THEOREM_KIND, "_THEOREM_KIND");
596
597 // em.newKind(UPDATE, "_UPDATE");
598 // em.newKind(UPDATE_SELECT, "_UPDATE_SELECT");
599
600 // em.newKind(RECORD_TYPE, "_RECORD_TYPE");
601 // em.newKind(RECORD, "_RECORD");
602 // em.newKind(RECORD_SELECT, "_RECORD_SELECT");
603 // em.newKind(RECORD_UPDATE, "_RECORD_UPDATE");
604
605 // em.newKind(TUPLE, "_TUPLE");
606 // em.newKind(TUPLE_SELECT, "_TUPLE_SELECT");
607 // em.newKind(TUPLE_UPDATE, "_TUPLE_UPDATE");
608
609 // em.newKind(SUBRANGE, "_SUBRANGE");
610
611 // em.newKind(SCALARTYPE, "_SCALARTYPE");
612 // em.newKind(DATATYPE, "_DATATYPE");
613 // em.newKind(THISTYPE, "_THISTYPE");
614 // em.newKind(CONSTRUCTOR, "_CONSTRUCTOR");
615 // em.newKind(SELECTOR, "_SELECTOR");
616 // em.newKind(TESTER, "_TESTER");
617 // em.newKind(DATATYPE_UPDATE, "_DATATYPE_UPDATE");
618
619 em.newKind(IF, "_IF");
620 em.newKind(IFTHEN, "_IFTHEN");
621 em.newKind(ELSE, "_ELSE");
622 em.newKind(COND, "_COND");
623
624 em.newKind(LET, "_LET");
625 em.newKind(LETDECLS, "_LETDECLS");
626 em.newKind(LETDECL, "_LETDECL");
627
628 em.newKind(LAMBDA, "_LAMBDA");
629 em.newKind(SIMULATE, "_SIMULATE");
630
631 em.newKind(CONST, "_CONST");
632 em.newKind(VARLIST, "_VARLIST");
633 em.newKind(UCONST, "_UCONST");
634 em.newKind(DEFUN, "_DEFUN");
635
636 // Arithmetic types and operators
637 // em.newKind(REAL, "_REAL");
638 // em.newKind(INT, "_INT");
639
640 // em.newKind(UMINUS, "_UMINUS");
641 // em.newKind(PLUS, "_PLUS");
642 // em.newKind(MINUS, "_MINUS");
643 // em.newKind(MULT, "_MULT");
644 // em.newKind(DIVIDE, "_DIVIDE");
645 // em.newKind(POW, "_POW");
646 // em.newKind(INTDIV, "_INTDIV");
647 // em.newKind(MOD, "_MOD");
648 // em.newKind(LT, "_LT");
649 // em.newKind(LE, "_LE");
650 // em.newKind(GT, "_GT");
651 // em.newKind(GE, "_GE");
652 // em.newKind(IS_INTEGER, "_IS_INTEGER");
653 // em.newKind(NEGINF, "_NEGINF");
654 // em.newKind(POSINF, "_POSINF");
655 // em.newKind(FLOOR, "_FLOOR");
656 }
657
658
notifyPre()659 void ExprManagerNotifyObj::notifyPre() {
660 d_em->postponeGC();
661 }
662
663
notify()664 void ExprManagerNotifyObj::notify() {
665 d_em->resumeGC();
666 }
667