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 #include <deque>
00034
00035 namespace CVC3 {
00036
00037 class CLFlags;
00038 class PrettyPrinter;
00039 class MemoryManager;
00040 class ExprManagerNotifyObj;
00041 class TheoremManager;
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
00173 bool d_inGC;
00174
00175 std::deque<ExprValue*> d_pending;
00176
00177
00178 ExprHashMap<Expr> d_rebuildCache;
00179 IF_DEBUG(bool d_inRebuild;)
00180
00181 public:
00182
00183 class TypeComputer {
00184 public:
00185 TypeComputer() {}
00186 virtual ~TypeComputer() {}
00187
00188 virtual void computeType(const Expr& e) = 0;
00189
00190 virtual void checkType(const Expr& e) = 0;
00191
00192 virtual Cardinality finiteTypeInfo(Expr& e, Unsigned& n,
00193 bool enumerate, bool computeSize) = 0;
00194 };
00195 private:
00196
00197 TypeComputer* d_typeComputer;
00198
00199
00200
00201
00202
00203
00204
00205
00206
00207 Expr rebuildRec(const Expr& e);
00208
00209
00210 ExprValue* newExprValue(ExprValue* ev);
00211
00212
00213 unsigned getFlag() { return d_flagCounter; }
00214
00215 unsigned nextFlag()
00216 { FatalAssert(++d_flagCounter, "flag overflow"); return d_flagCounter; }
00217
00218
00219 void computeType(const Expr& e);
00220
00221 void checkType(const Expr& e);
00222
00223
00224
00225
00226
00227
00228
00229
00230 Cardinality finiteTypeInfo(Expr& e, Unsigned& n,
00231 bool enumerate, bool computeSize);
00232
00233 public:
00234
00235 ExprManager(ContextManager* cm, const CLFlags& flags);
00236
00237 ~ExprManager();
00238
00239
00240
00241
00242
00243
00244
00245
00246
00247
00248 void clear();
00249
00250 bool isActive();
00251
00252
00253
00254 void gc(ExprValue* ev);
00255
00256
00257 void postponeGC() { d_postponeGC = true; }
00258
00259
00260 void resumeGC();
00261
00262
00263
00264 Expr rebuild(const Expr& e);
00265
00266
00267
00268 ExprIndex nextIndex() { return d_index++; }
00269 ExprIndex lastIndex() { return d_index - 1; }
00270
00271
00272 void clearFlags() { nextFlag(); }
00273
00274
00275
00276 const Expr& boolExpr() { return d_bool; }
00277
00278 const Expr& falseExpr() { return d_false; }
00279
00280 const Expr& trueExpr() { return d_true; }
00281
00282 const std::vector<Expr>& getEmptyVector() { return d_emptyVec; }
00283
00284 const Expr& getNullExpr() { return d_nullExpr; }
00285
00286
00287
00288
00289 Expr newExpr(ExprValue* ev) { return Expr(newExprValue(ev)); }
00290
00291 Expr newLeafExpr(const Op& op);
00292 Expr newStringExpr(const std::string &s);
00293 Expr newRatExpr(const Rational& r);
00294 Expr newSkolemExpr(const Expr& e, int i);
00295 Expr newVarExpr(const std::string &s);
00296 Expr newSymbolExpr(const std::string &s, int kind);
00297 Expr newBoundVarExpr(const std::string &name, const std::string& uid);
00298 Expr newBoundVarExpr(const std::string &name, const std::string& uid,
00299 const Type& type);
00300 Expr newBoundVarExpr(const Type& type);
00301 Expr newClosureExpr(int kind, const Expr& var, const Expr& body);
00302 Expr newClosureExpr(int kind, const std::vector<Expr>& vars,
00303 const Expr& body);
00304 Expr newClosureExpr(int kind, const std::vector<Expr>& vars,
00305 const Expr& body, const std::vector<std::vector<Expr> >& trigs);
00306
00307
00308 Expr andExpr(const std::vector <Expr>& children)
00309 { return Expr(AND, children, this); }
00310 Expr orExpr(const std::vector <Expr>& children)
00311 { return Expr(OR, children, this); }
00312
00313
00314
00315
00316 size_t hash(const Expr& e) const;
00317
00318 ContextManager* getCM() const { return d_cm; }
00319
00320 Context* getCurrentContext() const { return d_cm->getCurrentContext(); }
00321
00322 int scopelevel() { return d_cm->scopeLevel(); }
00323
00324
00325 void setTM(TheoremManager* tm) { d_tm = tm; }
00326
00327 TheoremManager* getTM() const { return d_tm; }
00328
00329
00330 MemoryManager* getMM(size_t MMIndex) {
00331 DebugAssert(MMIndex < d_mm.size(), "ExprManager::getMM()");
00332 return d_mm[MMIndex];
00333 }
00334
00335 unsigned getSimpCacheTag() const { return d_simpCacheTagCurrent; }
00336
00337 void invalidateSimpCache() { d_simpCacheTagCurrent++; }
00338
00339
00340 void registerTypeComputer(TypeComputer* typeComputer)
00341 { d_typeComputer = typeComputer; }
00342
00343
00344 int printDepth() const { return *d_printDepth; }
00345
00346 bool withIndentation() const { return *d_withIndentation; }
00347
00348 int lineWidth() const { return *d_lineWidth; }
00349
00350 int indent() const { return d_indentTransient; }
00351
00352 int indent(int n, bool permanent = false);
00353
00354
00355
00356 int incIndent(int n, bool permanent = false);
00357
00358 void restoreIndent() { d_indentTransient = d_indent; }
00359
00360 InputLanguage getInputLang() const;
00361
00362 InputLanguage getOutputLang() const;
00363
00364 bool dagPrinting() const { return *d_dagPrinting; }
00365
00366
00367 PrettyPrinter* getPrinter() const { return d_prettyPrinter; }
00368
00369
00370
00371
00372
00373
00374
00375
00376
00377
00378
00379 void newKind(int kind, const std::string &name, bool isType = false);
00380
00381
00382
00383 void registerPrettyPrinter(PrettyPrinter& printer);
00384
00385 void unregisterPrettyPrinter();
00386
00387
00388 bool isKindRegistered(int kind) { return d_kindMap.count(kind) > 0; }
00389
00390 bool isTypeKind(int kind) { return d_typeKinds.count(kind) > 0; }
00391
00392
00393
00394 const std::string& getKindName(int kind);
00395
00396 int getKind(const std::string& name);
00397
00398
00399
00400
00401
00402
00403 size_t registerSubclass(size_t sizeOfSubclass);
00404
00405
00406 unsigned long getMemory(int verbosity);
00407
00408 };
00409
00410
00411
00412
00413
00414
00415
00416
00417
00418
00419
00420
00421
00422
00423
00424
00425 class ExprManagerNotifyObj: public ContextNotifyObj {
00426 ExprManager* d_em;
00427 public:
00428
00429 ExprManagerNotifyObj(ExprManager* em, Context* cxt)
00430 : ContextNotifyObj(cxt), d_em(em) { }
00431
00432 void notifyPre(void);
00433 void notify(void);
00434 unsigned long getMemory(int verbosity) { return sizeof(ExprManagerNotifyObj); }
00435 };
00436
00437
00438 }
00439
00440
00441 #include "expr_value.h"
00442
00443 namespace CVC3 {
00444
00445 inline size_t ExprManager::hash(const ExprValue* ev) const {
00446 DebugAssert(ev!=NULL, "ExprManager::hash() called on a NULL ExprValue");
00447 return ev->hash();
00448 }
00449
00450 inline Expr ExprManager::newLeafExpr(const Op& op)
00451 {
00452 if (op.getKind() != APPLY) {
00453 ExprValue ev(this, op.getKind());
00454 return newExpr(&ev);
00455 }
00456 else {
00457 DebugAssert(op.getExpr().getEM() == this, "ExprManager mismatch");
00458 std::vector<Expr> kids;
00459 ExprApply ev(this, op, kids);
00460 return newExpr(&ev);
00461 }
00462 }
00463
00464 inline Expr ExprManager::newStringExpr(const std::string &s)
00465 { ExprString ev(this, s); return newExpr(&ev); }
00466
00467 inline Expr ExprManager::newRatExpr(const Rational& r)
00468 { ExprRational ev(this, r); return newExpr(&ev); }
00469
00470 inline Expr ExprManager::newSkolemExpr(const Expr& e, int i)
00471 { DebugAssert(e.getEM() == this, "ExprManager mismatch");
00472 ExprSkolem ev(this, i, e); return newExpr(&ev); }
00473
00474 inline Expr ExprManager::newVarExpr(const std::string &s)
00475 { ExprVar ev(this, s); return newExpr(&ev); }
00476
00477 inline Expr ExprManager::newSymbolExpr(const std::string &s, int kind)
00478 { ExprSymbol ev(this, kind, s); return newExpr(&ev); }
00479
00480 inline Expr ExprManager::newBoundVarExpr(const std::string &name,
00481 const std::string& uid)
00482 { ExprBoundVar ev(this, name, uid); return newExpr(&ev); }
00483
00484 inline Expr ExprManager::newBoundVarExpr(const std::string& name,
00485 const std::string& uid,
00486 const Type& type) {
00487 Expr res = newBoundVarExpr(name, uid);
00488 DebugAssert(type.getExpr().getKind() != ARROW,"");
00489 DebugAssert(res.lookupType().isNull(),
00490 "newBoundVarExpr: redefining a variable " + name);
00491 res.setType(type);
00492 return res;
00493 }
00494
00495 inline Expr ExprManager::newBoundVarExpr(const Type& type) {
00496 static int nextNum = 0;
00497 std::string name("_cvc3_");
00498 std::string uid = int2string(nextNum++);
00499 return newBoundVarExpr(name, uid, type);
00500 }
00501
00502 inline Expr ExprManager::newClosureExpr(int kind,
00503 const Expr& var,
00504 const Expr& body)
00505 { ExprClosure ev(this, kind, var, body); return newExpr(&ev); }
00506
00507 inline Expr ExprManager::newClosureExpr(int kind,
00508 const std::vector<Expr>& vars,
00509 const Expr& body)
00510 { ExprClosure ev(this, kind, vars, body); return newExpr(&ev); }
00511
00512 inline Expr ExprManager::newClosureExpr(int kind,
00513 const std::vector<Expr>& vars,
00514 const Expr& body,
00515 const std::vector<std::vector<Expr> >& trigs)
00516 { ExprClosure ev(this, kind, vars, body);
00517 Expr ret = newExpr(&ev); ret.setTriggers(trigs); return ret; }
00518
00519 inline bool ExprManager::EqEV::operator()(const ExprValue* ev1,
00520 const ExprValue* ev2) const {
00521 return (*ev1) == (*ev2);
00522 }
00523
00524 inline size_t ExprManager::hash(const Expr& e) const {
00525 DebugAssert(!e.isNull(), "ExprManager::hash() called on a Null Expr");
00526 return e.d_expr->hash();
00527 }
00528
00529 }
00530
00531 #endif
00532