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 #include "theorem.h"
00028 #include "theorem_value.h"
00029 #include "command_line_flags.h"
00030
00031 namespace CVC3 {
00032 using namespace std;
00033
00034
00035
00036
00037
00038
00039
00040
00041
00042
00043
00044
00045 int compare(const Theorem& t1, const Theorem& t2) {
00046 if(t1.d_thm == t2.d_thm) return 0;
00047 if(t1.isNull()) return -1;
00048 if(t2.isNull()) return 1;
00049
00050 bool rw1(t1.isRewrite()), rw2(t2.isRewrite());
00051
00052 if(!rw2) return compare(t1, t2.getExpr());
00053 else if(!rw1) return -compare(t2, t1.getExpr());
00054 else {
00055 int res(compare(t1.getLHS(), t2.getLHS()));
00056 if(res==0) res = compare(t1.getRHS(), t2.getRHS());
00057 return res;
00058 }
00059 }
00060
00061
00062
00063
00064
00065 int compare(const Theorem& t1, const Expr& e2) {
00066 bool rw1(t1.isRewrite()), rw2(e2.isEq() || e2.isIff());
00067 if(!rw1) {
00068 const Expr& e1 = t1.getExpr();
00069 rw1 = (e1.isEq() || e1.isIff());
00070 }
00071 if(rw1) {
00072 if(rw2) {
00073 int res(compare(t1.getLHS(), e2[0]));
00074 if(res==0) res = compare(t1.getRHS(), e2[1]);
00075 return res;
00076 } else return -1;
00077 } else {
00078 if(rw2) return 1;
00079 else return compare(t1.getExpr(), e2);
00080 }
00081 }
00082
00083 int compareByPtr(const Theorem& t1, const Theorem& t2) {
00084 if(t1.d_thm == t2.d_thm) return 0;
00085 else if(t1.d_thm < t2.d_thm) return -1;
00086 else return 1;
00087 }
00088
00089
00090 Theorem& Theorem::operator=(const Theorem& th) {
00091
00092 if(this == &th) return *this;
00093 long tmp = th.d_thm;
00094
00095 if (th.isRefl()) {
00096 th.exprValue()->incRefcount();
00097 }
00098 else {
00099 TheoremValue* tv = th.thm();
00100 DebugAssert(th.isNull() || tv->d_refcount > 0,
00101 "Theorem::operator=: NEW refcount = "
00102 + int2string(tv->d_refcount)
00103 + " in " + th.toString());
00104 if (tv) ++(tv->d_refcount);
00105 }
00106
00107 if (isRefl()) {
00108 exprValue()->decRefcount();
00109 }
00110 else {
00111 TheoremValue* tv = thm();
00112 DebugAssert(isNull() || tv->d_refcount > 0,
00113 "Theorem::operator=: OLD refcount = "
00114 + int2string(tv->d_refcount));
00115
00116
00117
00118 if((!isNull()) && --(tv->d_refcount) == 0) {
00119 MemoryManager* mm = tv->getMM();
00120 delete tv;
00121 mm->deleteData(tv);
00122 }
00123 }
00124
00125 d_thm = tmp;
00126
00127 return *this;
00128 }
00129
00130
00131 Theorem::Theorem(TheoremManager* tm, const Expr &thm,
00132 const Assumptions& assump, const Proof& pf,
00133 bool isAssump, int scope) {
00134 TheoremValue* tv;
00135 if(thm.isEq() || thm.isIff())
00136 tv = new(tm->getRWMM()) RWTheoremValue(tm, thm, assump, pf, isAssump, scope);
00137 else
00138 tv = new(tm->getMM()) RegTheoremValue(tm, thm, assump, pf, isAssump, scope);
00139 tv->d_refcount++;
00140 d_thm = ((intptr_t)tv)|0x1;
00141
00142 DebugAssert(!withProof() || !pf.isNull(),
00143 "Null proof in theorem:\n"+toString());
00144 }
00145
00146 Theorem::Theorem(TheoremManager* tm, const Expr& lhs, const Expr& rhs,
00147 const Assumptions& assump, const Proof& pf, bool isAssump,
00148 int scope) {
00149 TheoremValue* tv = new(tm->getRWMM())
00150 RWTheoremValue(tm, lhs, rhs, assump, pf, isAssump, scope);
00151 tv->d_refcount++;
00152 d_thm = ((long)tv)|0x1;
00153
00154
00155
00156
00157
00158
00159
00160
00161
00162
00163
00164
00165
00166
00167
00168
00169
00170 DebugAssert(!withProof() || !pf.isNull(),
00171 "Null proof in theorem:\n"+toString());
00172 }
00173
00174
00175
00176 Theorem::Theorem(const Theorem &th) : d_thm(th.d_thm) {
00177 if (d_thm & 0x1) {
00178 DebugAssert(thm()->d_refcount > 0,
00179 "Theorem(const Theorem&): refcount = "
00180 + int2string(thm()->d_refcount));
00181 thm()->d_refcount++;
00182
00183 } else if (d_thm != 0) {
00184 exprValue()->incRefcount();
00185 }
00186 }
00187
00188 Theorem::Theorem(const Expr& e) : d_expr(e.d_expr)
00189 {
00190 d_expr->incRefcount();
00191 }
00192
00193
00194 Theorem::~Theorem() {
00195 if (d_thm & 0x1) {
00196 TheoremValue* tv = thm();
00197
00198 IF_DEBUG(FatalAssert(tv->d_refcount > 0,
00199 "~Theorem(): refcount = "
00200 + int2string(tv->d_refcount)));
00201 if((--tv->d_refcount) == 0) {
00202
00203 MemoryManager* mm = tv->getMM();
00204 delete tv;
00205 mm->deleteData(tv);
00206 }
00207 }
00208 else if (d_thm != 0) {
00209 exprValue()->decRefcount();
00210 }
00211 }
00212
00213 void Theorem::printx() const { getExpr().print(); }
00214 void Theorem::printxnodag() const { getExpr().printnodag(); }
00215 void Theorem::pprintx() const { getExpr().pprint(); }
00216 void Theorem::pprintxnodag() const { getExpr().pprintnodag(); }
00217 void Theorem::print() const { cout << toString() << endl; }
00218
00219
00220 bool Theorem::withProof() const {
00221 if (isRefl()) return exprValue()->d_em->getTM()->withProof();
00222 return thm()->d_tm->withProof();
00223 }
00224
00225 bool Theorem::withAssumptions() const {
00226 if (isRefl()) return exprValue()->d_em->getTM()->withAssumptions();
00227 return thm()->d_tm->withAssumptions();
00228 }
00229
00230 bool Theorem::isRewrite() const {
00231 DebugAssert(!isNull(), "CVC3::Theorem::isRewrite(): we are Null");
00232 return isRefl() || thm()->isRewrite();
00233 }
00234
00235
00236 Expr Theorem::getExpr() const {
00237 DebugAssert(!isNull(), "CVC3::Theorem::getExpr(): we are Null");
00238 if (isRefl()) {
00239 Expr e(exprValue());
00240 if (e.isTerm()) return e.eqExpr(e);
00241 else return e.iffExpr(e);
00242 }
00243 else return thm()->getExpr();
00244 }
00245
00246 const Expr& Theorem::getLHS() const {
00247 DebugAssert(!isNull(), "CVC3::Theorem::getLHS: we are Null");
00248 if (isRefl()) return *((Expr*)(&d_expr));
00249 else return thm()->getLHS();
00250 }
00251
00252 const Expr& Theorem::getRHS() const {
00253 DebugAssert(!isNull(), "CVC3::Theorem::getRHS: we are Null");
00254 if (isRefl()) return *((Expr*)(&d_expr));
00255 else return thm()->getRHS();
00256 }
00257
00258
00259
00260
00261
00262
00263
00264
00265 void Theorem::getAssumptionsRec(set<Expr>& assumptions) const
00266 {
00267 if (isRefl() || isFlagged()) return;
00268 setFlag();
00269 if(isAssump()) {
00270 assumptions.insert(getExpr());
00271 }
00272 else {
00273 const Assumptions& a = getAssumptionsRef();
00274 for(Assumptions::iterator i=a.begin(), iend=a.end(); i!=iend; ++i)
00275 (*i).getAssumptionsRec(assumptions);
00276 }
00277 }
00278
00279
00280 void Theorem::getLeafAssumptions(vector<Expr>& assumptions,
00281 bool negate) const
00282 {
00283 if (isNull() || isRefl()) return;
00284 set<Expr> assumpSet;
00285 clearAllFlags();
00286 getAssumptionsRec(assumpSet);
00287
00288 for(set<Expr>::iterator i=assumpSet.begin(), iend=assumpSet.end();
00289 i!=iend; ++i)
00290 assumptions.push_back(negate ? (*i).negate() : *i);
00291 }
00292
00293
00294 const Assumptions& Theorem::getAssumptionsRef() const
00295 {
00296 DebugAssert(!isNull(), "CVC3::Theorem::getAssumptionsRef: we are Null");
00297 if (!isRefl()) {
00298 return thm()->getAssumptionsRef();
00299 }
00300 else return Assumptions::emptyAssump();
00301 }
00302
00303
00304 bool Theorem::isAssump() const {
00305 DebugAssert(!isNull(), "CVC3::Theorem::isAssump: we are Null");
00306 return isRefl() ? false : thm()->isAssump();
00307 }
00308
00309
00310
00311 Proof Theorem::getProof() const {
00312 static Proof null;
00313 DebugAssert(!isNull(), "CVC3::Theorem::getProof: we are Null");
00314 if (isRefl()) {
00315 return Proof(Expr(PF_APPLY,
00316 exprValue()->d_em->newVarExpr("refl"),
00317 Expr(exprValue())));
00318 }
00319 else if (withProof() == true)
00320 return thm()->getProof();
00321 else
00322 return null;
00323 }
00324
00325 bool Theorem::isFlagged() const {
00326 DebugAssert(!isNull(), "CVC3::Theorem::isFlagged: we are Null");
00327 if (isRefl()) return exprValue()->d_em->getTM()->isFlagged((long)d_expr);
00328 else return thm()->isFlagged();
00329 }
00330
00331 void Theorem::clearAllFlags() const {
00332 DebugAssert(!isNull(), "CVC3::Theorem::clearAllFlags: we are Null");
00333 if (isRefl()) {
00334 exprValue()->d_em->getTM()->clearAllFlags();
00335 } else thm()->clearAllFlags();
00336 }
00337
00338 void Theorem::setFlag() const {
00339 DebugAssert(!isNull(), "CVC3::Theorem::setFlag: we are Null");
00340 if (isRefl()) exprValue()->d_em->getTM()->setFlag((long)d_expr);
00341 else thm()->setFlag();
00342 }
00343
00344 void Theorem::setCachedValue(int value) const {
00345 DebugAssert(!isNull(), "CVC3::Theorem::setCachedValue: we are Null");
00346 if (isRefl()) exprValue()->d_em->getTM()->setCachedValue((long)d_expr, value);
00347 else thm()->setCachedValue(value);
00348 }
00349
00350 int Theorem::getCachedValue() const {
00351 DebugAssert(!isNull(), "CVC3::Theorem::getCachedValue: we are Null");
00352 if (isRefl()) return exprValue()->d_em->getTM()->getCachedValue((long)d_expr);
00353 return thm()->getCachedValue();
00354 }
00355
00356 void Theorem::setExpandFlag(bool val) const {
00357 DebugAssert(!isNull(), "CVC3::Theorem::setExpandFlag: we are Null");
00358 if (isRefl()) exprValue()->d_em->getTM()->setExpandFlag((long)d_expr, val);
00359 thm()->setExpandFlag(val);
00360 }
00361
00362 bool Theorem::getExpandFlag() const {
00363 DebugAssert(!isNull(), "CVC3::Theorem::getExpandFlag: we are Null");
00364 if (isRefl()) return exprValue()->d_em->getTM()->getExpandFlag((long)d_expr);
00365 return thm()->getExpandFlag();
00366 }
00367
00368 void Theorem::setLitFlag(bool val) const {
00369 DebugAssert(!isNull(), "CVC3::Theorem::setLitFlag: we are Null");
00370 if (isRefl()) exprValue()->d_em->getTM()->setLitFlag((long)d_expr, val);
00371 thm()->setLitFlag(val);
00372 }
00373
00374 bool Theorem::getLitFlag() const {
00375 DebugAssert(!isNull(), "CVC3::Theorem::getLitFlag: we are Null");
00376 if (isRefl()) return exprValue()->d_em->getTM()->getLitFlag((long)d_expr);
00377 return thm()->getLitFlag();
00378 }
00379
00380 bool Theorem::isAbsLiteral() const {
00381 return getExpr().isAbsLiteral();
00382 }
00383
00384 int Theorem::getScope() const {
00385 DebugAssert(!isNull(), "CVC3::Theorem::getScope: we are Null");
00386 return isRefl() ? 0 : thm()->getScope();
00387 }
00388
00389 unsigned Theorem::getQuantLevel() const {
00390 DebugAssert(!isNull(), "CVC3::Theorem::getQuantLevel: we are Null");
00391 return isRefl() ? 0 : thm()->getQuantLevel();
00392 }
00393
00394 void Theorem::setQuantLevel(unsigned level) {
00395 DebugAssert(!isNull(), "CVC3::Theorem::setQuantLevel: we are Null");
00396 DebugAssert(!isRefl(), "CVC3::Theorem::setQuantLevel: we are Refl");
00397 thm()->setQuantLevel(level);
00398 }
00399
00400 size_t Theorem::hash() const {
00401 static std::hash<long int> h;
00402 return h(d_thm);
00403 }
00404
00405 void Theorem::recursivePrint(int& i) const {
00406 cout << "[" << getCachedValue()
00407 << "]@" << getScope() << "\tTheorem: {";
00408
00409 if (isAssump()) {
00410 cout << "assump";
00411 }
00412 else if (getAssumptionsRef().empty()) {
00413 cout << "empty";
00414 }
00415 else {
00416 const Assumptions::iterator iend = getAssumptionsRef().end();
00417 for (Assumptions::iterator it = getAssumptionsRef().begin();
00418 it != iend; ++it) {
00419 if (!it->isFlagged()) it->setCachedValue(i++);
00420 cout << "[" << it->getCachedValue() << "], " ;
00421 }
00422 cout << "}" << endl << "\t\t|- " << getExpr() << endl;
00423 for (Assumptions::iterator it = getAssumptionsRef().begin();
00424 it != iend; ++it) {
00425 if (it->isFlagged()) continue;
00426 it->recursivePrint(i);
00427 it->setFlag();
00428 }
00429 return;
00430 }
00431 cout << "}" << endl << "\t\t|- " << getExpr() << endl;
00432 }
00433
00434
00435
00436
00437
00438
00439
00440
00441
00442
00443
00444
00445
00446
00447
00448
00449
00450
00451
00452
00453
00454
00455
00456
00457
00458
00459
00460
00461
00462
00463
00464
00465
00466 ostream& Theorem::print(ostream& os, const string& name) const {
00467 if(isNull()) return os << name << "(Null)";
00468 ExprManager *em = getExpr().getEM();
00469 if (isRefl()) os << getExpr();
00470 else if (withAssumptions()) {
00471 em->incIndent(name.size()+2);
00472 os << name << "([" << thm() << "#" << thm()->d_refcount << "]@"
00473 << getScope() << "\n[";
00474 if(isAssump()) os << "Assump";
00475 else {
00476 if(thm()->d_tm->getFlags()["print-assump"].getBool()
00477 && em->isActive())
00478 os << getAssumptionsRef();
00479 else
00480 os << "<assumptions>";
00481 }
00482 os << "]\n |--- ";
00483 em->indent(7);
00484 if(em->isActive()) os << getExpr();
00485 else os << "(being destructed)";
00486 if(withProof())
00487 os << "\n Proof = " << getProof();
00488 return os << ")";
00489 }
00490 else {
00491 em->incIndent(name.size()+1);
00492 os << name << "(";
00493 if(em->isActive()) os << getExpr();
00494 else os << "being destructed";
00495 return os << ")";
00496 }
00497 return os;
00498 }
00499
00500
00501 }