00001
00002
00003
00004
00005
00006
00007
00008
00009
00010
00011
00012
00013
00014
00015
00016
00017
00018
00019
00020
00021
00022
00023
00024 #ifndef _cvc3__expr_h_
00025 #include "expr.h"
00026 #endif
00027
00028 #ifndef _cvc3__include__expr_manager_h_
00029 #define _cvc3__include__expr_manager_h_
00030
00031 #include "os.h"
00032 #include "expr_map.h"
00033
00034 namespace CVC3 {
00035
00036 class CLFlags;
00037 class PrettyPrinter;
00038 class MemoryManager;
00039 class ExprManagerNotifyObj;
00040 class TheoremManager;
00041
00042
00043
00044
00045
00046
00047
00048
00049
00050
00051
00052
00053
00054
00055
00056
00057
00058 class CVC_DLL ExprManager {
00059 friend class Expr;
00060 friend class ExprValue;
00061 friend class Op;
00062 friend class HashEV;
00063 friend class Type;
00064
00065 ContextManager* d_cm;
00066 TheoremManager* d_tm;
00067 ExprManagerNotifyObj* d_notifyObj;
00068 ExprIndex d_index;
00069 unsigned d_flagCounter;
00070
00071
00072 std::hash_map<int, std::string> d_kindMap;
00073
00074 std::hash_set<int> d_typeKinds;
00075
00076 class HashString {
00077 std::hash<char*> h;
00078 public:
00079 size_t operator()(const std::string& s) const {
00080 return h(const_cast<char*>(s.c_str()));
00081 }
00082 };
00083
00084 std::hash_map<std::string, int, HashString> d_kindMapByName;
00085
00086
00087 PrettyPrinter *d_prettyPrinter;
00088
00089 size_t hash(const ExprValue* ev) const;
00090
00091
00092
00093
00094
00095 const int* d_printDepth;
00096
00097 const bool* d_withIndentation;
00098
00099 int d_indent;
00100
00101
00102
00103 int d_indentTransient;
00104
00105 const int* d_lineWidth;
00106
00107 const std::string* d_inputLang;
00108
00109 const std::string* d_outputLang;
00110
00111 const bool* d_dagPrinting;
00112
00113 const std::string d_mmFlag;
00114
00115
00116 class HashEV {
00117 ExprManager* d_em;
00118 public:
00119 HashEV(ExprManager* em): d_em(em) { }
00120 size_t operator()(ExprValue* ev) const { return d_em->hash(ev); }
00121 };
00122
00123 class EqEV {
00124 public:
00125 bool operator()(const ExprValue* ev1, const ExprValue* ev2) const;
00126 };
00127
00128
00129 typedef std::hash_set<ExprValue*, HashEV, EqEV> ExprValueSet;
00130
00131 ExprValueSet d_exprSet;
00132
00133 std::vector<MemoryManager*> d_mm;
00134
00135
00136 std::hash<void*> d_pointerHash;
00137
00138
00139 Expr d_bool;
00140 Expr d_false;
00141 Expr d_true;
00142
00143 std::vector<Expr> d_emptyVec;
00144
00145 Expr d_nullExpr;
00146
00147 void installExprValue(ExprValue* ev);
00148
00149
00150
00151
00152
00153 unsigned d_simpCacheTagCurrent;
00154
00155
00156
00157
00158
00159 bool d_disableGC;
00160
00161
00162
00163
00164
00165
00166
00167
00168 bool d_postponeGC;
00169
00170 std::vector<ExprValue*> d_postponed;
00171
00172 ExprHashMap<Expr> d_rebuildCache;
00173 IF_DEBUG(bool d_inRebuild);
00174
00175 public:
00176
00177 class TypeComputer {
00178 public:
00179 TypeComputer() {}
00180 virtual ~TypeComputer() {}
00181
00182 virtual void computeType(const Expr& e) = 0;
00183
00184 virtual void checkType(const Expr& e) = 0;
00185 };
00186 private:
00187
00188 TypeComputer* d_typeComputer;
00189
00190
00191
00192
00193
00194
00195
00196
00197
00198 Expr rebuildRec(const Expr& e);
00199
00200
00201 ExprValue* newExprValue(ExprValue* ev);
00202
00203
00204 unsigned getFlag() { return d_flagCounter; }
00205
00206 unsigned nextFlag()
00207 { FatalAssert(++d_flagCounter, "flag overflow"); return d_flagCounter; }
00208
00209
00210 void computeType(const Expr& e);
00211
00212 void checkType(const Expr& e);
00213
00214 public:
00215
00216 ExprManager(ContextManager* cm, const CLFlags& flags);
00217
00218 ~ExprManager();
00219
00220
00221
00222
00223
00224
00225
00226
00227
00228
00229 void clear();
00230
00231 bool isActive();
00232
00233
00234
00235 void gc(ExprValue* ev);
00236
00237
00238 void postponeGC() { d_postponeGC = true; }
00239
00240
00241 void resumeGC();
00242
00243
00244
00245 Expr rebuild(const Expr& e);
00246
00247
00248
00249 ExprIndex nextIndex() { return d_index++; }
00250 ExprIndex lastIndex() { return d_index - 1; }
00251
00252
00253 void clearFlags() { nextFlag(); }
00254
00255
00256
00257 const Expr& boolExpr() { return d_bool; }
00258
00259 const Expr& falseExpr() { return d_false; }
00260
00261 const Expr& trueExpr() { return d_true; }
00262
00263 const std::vector<Expr>& getEmptyVector() { return d_emptyVec; }
00264
00265 const Expr& getNullExpr() { return d_nullExpr; }
00266
00267
00268
00269
00270 Expr newExpr(ExprValue* ev) { return Expr(newExprValue(ev)); }
00271
00272 Expr newLeafExpr(const Op& op);
00273 Expr newStringExpr(const std::string &s);
00274 Expr newRatExpr(const Rational& r);
00275 Expr newSkolemExpr(const Expr& e, int i);
00276 Expr newVarExpr(const std::string &s);
00277 Expr newSymbolExpr(const std::string &s, int kind);
00278 Expr newBoundVarExpr(const std::string &name, const std::string& uid);
00279 Expr newBoundVarExpr(const std::string &name, const std::string& uid,
00280 const Type& type);
00281 Expr newBoundVarExpr(const Type& type);
00282 Expr newClosureExpr(int kind, const std::vector<Expr>& vars,
00283 const Expr& body);
00284 Expr newTheoremExpr(const Theorem& thm);
00285
00286
00287 Expr andExpr(const std::vector <Expr>& children)
00288 { return Expr(AND, children, this); }
00289 Expr orExpr(const std::vector <Expr>& children)
00290 { return Expr(OR, children, this); }
00291
00292
00293
00294
00295 size_t hash(const Expr& e) const;
00296
00297 ContextManager* getCM() const { return d_cm; }
00298
00299 Context* getCurrentContext() const { return d_cm->getCurrentContext(); }
00300
00301 int scopelevel() { return d_cm->scopeLevel(); }
00302
00303
00304 void setTM(TheoremManager* tm) { d_tm = tm; }
00305
00306 TheoremManager* getTM() const { return d_tm; }
00307
00308
00309 MemoryManager* getMM(size_t MMIndex) {
00310 DebugAssert(MMIndex < d_mm.size(), "ExprManager::getMM()");
00311 return d_mm[MMIndex];
00312 }
00313
00314 unsigned getSimpCacheTag() const { return d_simpCacheTagCurrent; }
00315
00316 void invalidateSimpCache() { d_simpCacheTagCurrent++; }
00317
00318
00319 void registerTypeComputer(TypeComputer* typeComputer)
00320 { d_typeComputer = typeComputer; }
00321
00322
00323 int printDepth() const { return *d_printDepth; }
00324
00325 bool withIndentation() const { return *d_withIndentation; }
00326
00327 int lineWidth() const { return *d_lineWidth; }
00328
00329 int indent() const { return d_indentTransient; }
00330
00331 int indent(int n, bool permanent = false);
00332
00333
00334
00335 int incIndent(int n, bool permanent = false);
00336
00337 void restoreIndent() { d_indentTransient = d_indent; }
00338
00339 InputLanguage getInputLang() const;
00340
00341 InputLanguage getOutputLang() const;
00342
00343 bool dagPrinting() const { return *d_dagPrinting; }
00344
00345
00346 PrettyPrinter* getPrinter() const { return d_prettyPrinter; }
00347
00348
00349
00350
00351
00352
00353
00354
00355
00356
00357
00358 void newKind(int kind, const std::string &name, bool isType = false);
00359
00360
00361
00362 void registerPrettyPrinter(PrettyPrinter& printer);
00363
00364 void unregisterPrettyPrinter();
00365
00366
00367 bool isKindRegistered(int kind) { return d_kindMap.count(kind) > 0; }
00368
00369 bool isTypeKind(int kind) { return d_typeKinds.count(kind) > 0; }
00370
00371
00372
00373 const std::string& getKindName(int kind);
00374
00375 int getKind(const std::string& name);
00376
00377
00378
00379
00380
00381
00382 size_t registerSubclass(size_t sizeOfSubclass);
00383
00384 };
00385
00386
00387
00388
00389
00390
00391
00392
00393
00394
00395
00396
00397
00398
00399
00400
00401 class ExprManagerNotifyObj: public ContextNotifyObj {
00402 ExprManager* d_em;
00403 public:
00404
00405 ExprManagerNotifyObj(ExprManager* em, Context* cxt)
00406 : ContextNotifyObj(cxt), d_em(em) { }
00407
00408 void notifyPre(void);
00409 void notify(void);
00410 };
00411
00412
00413 }
00414
00415
00416 #include "expr_value.h"
00417
00418 namespace CVC3 {
00419
00420 inline Expr ExprManager::newLeafExpr(const Op& op)
00421 {
00422 if (op.getExpr().isNull()) {
00423 ExprValue ev(this, op.getKind());
00424 return newExpr(&ev);
00425 }
00426 else {
00427 DebugAssert(op.getExpr().getEM() == this, "ExprManager mismatch");
00428 std::vector<Expr> kids;
00429 ExprApply ev(this, op, kids);
00430 return newExpr(&ev);
00431 }
00432 }
00433
00434 inline Expr ExprManager::newStringExpr(const std::string &s)
00435 { ExprString ev(this, s); return newExpr(&ev); }
00436
00437 inline Expr ExprManager::newRatExpr(const Rational& r)
00438 { ExprRational ev(this, r); return newExpr(&ev); }
00439
00440 inline Expr ExprManager::newSkolemExpr(const Expr& e, int i)
00441 { DebugAssert(e.getEM() == this, "ExprManager mismatch");
00442 ExprSkolem ev(this, i, e); return newExpr(&ev); }
00443
00444 inline Expr ExprManager::newVarExpr(const std::string &s)
00445 { ExprVar ev(this, s); return newExpr(&ev); }
00446
00447 inline Expr ExprManager::newSymbolExpr(const std::string &s, int kind)
00448 { ExprSymbol ev(this, kind, s); return newExpr(&ev); }
00449
00450 inline Expr ExprManager::newBoundVarExpr(const std::string &name,
00451 const std::string& uid)
00452 { ExprBoundVar ev(this, name, uid); return newExpr(&ev); }
00453
00454 inline Expr ExprManager::newBoundVarExpr(const std::string& name,
00455 const std::string& uid,
00456 const Type& type) {
00457 Expr res = newBoundVarExpr(name, uid);
00458 DebugAssert(type.getExpr().getKind() != ARROW,"");
00459 DebugAssert(res.lookupType().isNull(),
00460 "newBoundVarExpr: redefining a variable " + name);
00461 res.setType(type);
00462 return res;
00463 }
00464
00465 inline Expr ExprManager::newBoundVarExpr(const Type& type) {
00466 static int nextNum = 0;
00467 std::string name("_cvc3_");
00468 std::string uid = int2string(nextNum++);
00469 return newBoundVarExpr(name, uid, type);
00470 }
00471
00472 inline Expr ExprManager::newClosureExpr(int kind,
00473 const std::vector<Expr>& vars,
00474 const Expr& body)
00475 { ExprClosure ev(this, kind, vars, body); return newExpr(&ev); }
00476
00477 inline Expr ExprManager::newTheoremExpr(const Theorem& thm)
00478 { ExprTheorem ev(this, thm); return newExpr(&ev); }
00479
00480 inline size_t ExprManager::hash(const ExprValue* ev) const {
00481 DebugAssert(ev!=NULL, "ExprManager::hash() called on a NULL ExprValue");
00482 return ev->hash();
00483 }
00484
00485 inline bool ExprManager::EqEV::operator()(const ExprValue* ev1,
00486 const ExprValue* ev2) const {
00487 return (*ev1) == (*ev2);
00488 }
00489
00490 inline size_t ExprManager::hash(const Expr& e) const {
00491 DebugAssert(!e.isNull(), "ExprManager::hash() called on a Null Expr");
00492 return e.d_expr->hash();
00493 }
00494
00495 }
00496
00497 #endif
00498