00001
00002
00003
00004
00005
00006
00007
00008
00009
00010
00011
00012
00013
00014
00015
00016
00017
00018
00019
00020
00021
00022
00023
00024
00025
00026
00027
00028
00029
00030
00031
00032
00033
00034
00035
00036
00037
00038
00039
00040
00041
00042
00043
00044
00045 #ifndef _cvc3__theorem_value_h_
00046 #define _cvc3__theorem_value_h_
00047
00048 #include "theorem.h"
00049 #include "theorem_manager.h"
00050
00051
00052
00053
00054
00055 namespace CVC3 {
00056
00057
00058
00059 class TheoremValue
00060 {
00061
00062 friend class Theorem;
00063 friend class RegTheoremValue;
00064 friend class RWTheoremValue;
00065
00066 protected:
00067
00068 TheoremManager* d_tm;
00069
00070
00071 Expr d_thm;
00072
00073
00074 Proof d_proof;
00075
00076
00077 unsigned d_refcount;
00078
00079
00080 int d_scopeLevel;
00081
00082
00083 unsigned d_quantLevel;
00084
00085
00086 unsigned d_flag;
00087
00088
00089 int d_cachedValue : 29;
00090
00091 bool d_isAssump : 1;
00092 bool d_expand : 1;
00093 bool d_clauselit : 1;
00094
00095
00096 private:
00097
00098
00099
00100
00101
00102
00103
00104 TheoremValue(TheoremManager* tm, const Expr &thm,
00105 const Proof& pf, bool isAssump) :
00106 d_tm(tm), d_thm(thm), d_proof(pf), d_refcount(0),
00107 d_scopeLevel(0), d_quantLevel(0), d_flag(0), d_isAssump(isAssump) {}
00108
00109
00110 TheoremValue(const TheoremValue& t) {
00111 FatalAssert(false, "TheoremValue() copy constructor called");
00112 }
00113 TheoremValue& operator=(const TheoremValue& t) {
00114 FatalAssert(false, "TheoremValue assignment operator called");
00115 return *this;
00116 }
00117
00118 bool isFlagged() const {
00119 return d_flag == d_tm->getFlag();
00120 }
00121
00122 void clearAllFlags() {
00123 d_tm->clearAllFlags();
00124 }
00125
00126 void setFlag() {
00127 d_flag = d_tm->getFlag();
00128 }
00129
00130 void setCachedValue(int value) {
00131 d_cachedValue = value;
00132 }
00133
00134 int getCachedValue() const {
00135 return d_cachedValue;
00136 }
00137
00138 void setExpandFlag(bool val) {
00139 d_expand = val;
00140 }
00141
00142 bool getExpandFlag() {
00143 return d_expand;
00144 }
00145
00146 void setLitFlag(bool val) {
00147 d_clauselit = val;
00148 }
00149
00150 bool getLitFlag() {
00151 return d_clauselit;
00152 }
00153
00154 int getScope() {
00155 return d_scopeLevel;
00156 }
00157
00158 unsigned getQuantLevel() { return d_quantLevel; }
00159 void setQuantLevel(unsigned level) { d_quantLevel = level; }
00160
00161
00162 virtual bool isRewrite() const { return false; }
00163
00164 virtual const Expr& getExpr() const { return d_thm; }
00165 virtual const Expr& getLHS() const {
00166
00167 DebugAssert(isRewrite(),
00168 "TheoremValue::getLHS() called on non-rewrite theorem:\n"
00169 +toString());
00170 return d_thm[0];
00171 }
00172 virtual const Expr& getRHS() const {
00173
00174 DebugAssert(isRewrite(),
00175 "TheoremValue::getRHS() called on non-rewrite theorem:\n"
00176 +toString());
00177 return d_thm[1];
00178 }
00179
00180 virtual const Assumptions& getAssumptionsRef() const = 0;
00181
00182 bool isAssump() const { return d_isAssump; }
00183 const Proof& getProof() { return d_proof; }
00184
00185 public:
00186
00187 virtual ~TheoremValue() {
00188 IF_DEBUG(FatalAssert(d_refcount == 0,
00189 "Thm::TheoremValue::~TheoremValue(): refcount != 0."));
00190 }
00191
00192 std::string toString() const {
00193 return getAssumptionsRef().toString() + " |- " + getExpr().toString();
00194 }
00195
00196
00197 virtual MemoryManager* getMM() = 0;
00198
00199 };
00200
00201
00202
00203
00204
00205
00206
00207
00208
00209
00210 class RegTheoremValue :public TheoremValue
00211 {
00212 friend class Theorem;
00213
00214 protected:
00215
00216 Assumptions d_assump;
00217
00218 private:
00219
00220 RegTheoremValue(TheoremManager* tm, const Expr& thm,
00221 const Assumptions& assump, const Proof& pf, bool isAssump,
00222 int scope = -1)
00223 : TheoremValue(tm, thm, pf, isAssump), d_assump(assump)
00224 {
00225 DebugAssert(d_tm->isActive(), "TheoremValue()");
00226 if (isAssump) {
00227 DebugAssert(assump.empty(), "Expected empty assumptions");
00228
00229 d_refcount = 1;
00230 {
00231 Theorem t(this);
00232 d_assump.add1(t);
00233 }
00234 d_refcount = 0;
00235 if (scope == -1) d_scopeLevel = tm->getCM()->scopeLevel();
00236 else d_scopeLevel = scope;
00237 }
00238 else {
00239 if (!d_assump.empty()) {
00240 const Assumptions::iterator iend = d_assump.end();
00241 for (Assumptions::iterator i = d_assump.begin();
00242 i != iend; ++i) {
00243 if (i->getScope() > d_scopeLevel)
00244 d_scopeLevel = i->getScope();
00245 if (i->getQuantLevel() > d_quantLevel)
00246 d_quantLevel = i->getQuantLevel();
00247 }
00248 }
00249 }
00250 TRACE("quantlevel", d_quantLevel, " theorem get_1 ", thm.toString());
00251 TRACE("quantlevel", d_quantLevel, " theorem get_1 ", thm.getIndex());
00252 }
00253
00254 public:
00255
00256 ~RegTheoremValue() {
00257 if (d_isAssump) {
00258 IF_DEBUG(FatalAssert(d_assump.size() == 1, "Expected size 1"));
00259 IF_DEBUG(FatalAssert(d_assump.getFirst().thm() == this, "Expected loop"));
00260 d_assump.getFirst().d_thm = 0;
00261 }
00262 }
00263
00264 const Assumptions& getAssumptionsRef() const { return d_assump; }
00265
00266
00267 MemoryManager* getMM() { return d_tm->getMM(); }
00268
00269 void* operator new(size_t size, MemoryManager* mm) {
00270 return mm->newData(size);
00271 }
00272 void operator delete(void* pMem, MemoryManager* mm) {
00273 mm->deleteData(pMem);
00274 }
00275
00276 void operator delete(void* d) { }
00277
00278 };
00279
00280
00281
00282
00283
00284
00285
00286
00287
00288
00289
00290
00291 class RWTheoremValue :public TheoremValue
00292 {
00293 friend class Theorem;
00294
00295 protected:
00296
00297
00298 Expr d_lhs;
00299 Expr d_rhs;
00300 Assumptions* d_assump;
00301
00302 private:
00303 void init(const Assumptions& assump, int scope)
00304 {
00305 DebugAssert(d_tm->isActive(), "TheoremValue()");
00306 if (d_isAssump) {
00307 DebugAssert(assump.empty(), "Expected empty assumptions");
00308
00309 d_refcount = 1;
00310 {
00311 Theorem t(this);
00312 d_assump = new Assumptions(t);
00313 }
00314 d_refcount = 0;
00315 if (scope == -1) d_scopeLevel = d_tm->getCM()->scopeLevel();
00316 else d_scopeLevel = scope;
00317 }
00318 else {
00319 if (!assump.empty()) {
00320 d_assump = new Assumptions(assump);
00321 const Assumptions::iterator iend = assump.end();
00322 for (Assumptions::iterator i = assump.begin();
00323 i != iend; ++i) {
00324 if (i->getScope() > d_scopeLevel)
00325 d_scopeLevel = i->getScope();
00326 if (i->getQuantLevel() > d_quantLevel)
00327 d_quantLevel = i->getQuantLevel();
00328 }
00329 }
00330 }
00331 TRACE("quantlevel", d_quantLevel, " theorem get ", d_thm.toString());
00332 }
00333
00334
00335 RWTheoremValue(TheoremManager* tm, const Expr& lhs, const Expr& rhs,
00336 const Assumptions& assump, const Proof& pf, bool isAssump,
00337 int scope = -1)
00338 : TheoremValue(tm, Expr(), pf, isAssump), d_lhs(lhs), d_rhs(rhs), d_assump(NULL)
00339 { init(assump, scope); }
00340
00341
00342 RWTheoremValue(TheoremManager* tm, const Expr& thm,
00343 const Assumptions& assump, const Proof& pf, bool isAssump,
00344 int scope = -1)
00345 : TheoremValue(tm, thm, pf, isAssump), d_lhs(thm[0]), d_rhs(thm[1]), d_assump(NULL)
00346 { init(assump, scope); }
00347
00348 const Expr& getExpr() const {
00349 if (d_thm.isNull()) {
00350 bool isBool = d_lhs.getType().isBool();
00351
00352 Expr* pexpr = const_cast<Expr*>(&d_thm);
00353 *pexpr = isBool ? d_lhs.iffExpr(d_rhs) : d_lhs.eqExpr(d_rhs);
00354
00355 }
00356 return d_thm;
00357 }
00358
00359 const Expr& getLHS() const { return d_lhs; }
00360 const Expr& getRHS() const { return d_rhs; }
00361
00362 public:
00363
00364 ~RWTheoremValue() {
00365 if (d_isAssump) {
00366 IF_DEBUG(FatalAssert(d_assump && d_assump->size() == 1, "Expected size 1"));
00367 IF_DEBUG(FatalAssert(d_assump->getFirst().thm() == this, "Expected loop"));
00368 d_assump->getFirst().d_thm = 0;
00369 }
00370 if (d_assump) delete d_assump;
00371 }
00372
00373 bool isRewrite() const { return true; }
00374 const Assumptions& getAssumptionsRef() const {
00375 if (d_assump) return *d_assump;
00376 else return Assumptions::emptyAssump();
00377 }
00378
00379
00380 MemoryManager* getMM() { return d_tm->getRWMM(); }
00381
00382 void* operator new(size_t size, MemoryManager* mm) {
00383 return mm->newData(size);
00384 }
00385 void operator delete(void* pMem, MemoryManager* mm) {
00386 mm->deleteData(pMem);
00387 }
00388
00389 void operator delete(void* d) { }
00390
00391 };
00392
00393 };
00394
00395 #endif