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
00091 Theorem& Theorem::operator=(const Theorem& th) {
00092
00093 if(this == &th) return *this;
00094
00095 long tmp = th.d_thm;
00096
00097
00098 if (tmp & 0x1) {
00099 TheoremValue* tv = (TheoremValue*) (tmp & (~(0x1)));
00100 DebugAssert(tv->d_refcount > 0,
00101 "Theorem::operator=: invariant violated");
00102 ++(tv->d_refcount);
00103 }
00104 else if (tmp != 0) {
00105 th.exprValue()->incRefcount();
00106 }
00107
00108
00109 if (d_thm & 0x1) {
00110 TheoremValue* tv = thm();
00111 DebugAssert(tv->d_refcount > 0,
00112 "Theorem::operator=: invariant violated");
00113 if(--(tv->d_refcount) == 0) {
00114 MemoryManager* mm = tv->getMM();
00115 delete tv;
00116 mm->deleteData(tv);
00117 }
00118 }
00119 else if (d_thm != 0) {
00120 exprValue()->decRefcount();
00121 }
00122
00123 d_thm = tmp;
00124
00125 return *this;
00126 }
00127
00128
00129
00130 Theorem::Theorem(TheoremManager* tm, const Expr &thm,
00131 const Assumptions& assump, const Proof& pf,
00132 bool isAssump, int scope) {
00133 TheoremValue* tv;
00134 if (thm.isEq() || thm.isIff()) {
00135 if (thm[0] == thm[1]) {
00136 d_expr = thm[0].d_expr;
00137 d_expr->incRefcount();
00138 return;
00139 }
00140 tv = new(tm->getRWMM()) RWTheoremValue(tm, thm, assump, pf, isAssump, scope);
00141 }
00142 else
00143 tv = new(tm->getMM()) RegTheoremValue(tm, thm, assump, pf, isAssump, scope);
00144 tv->d_refcount++;
00145 d_thm = ((intptr_t)tv)|0x1;
00146
00147 DebugAssert(!withProof() || !pf.isNull(),
00148 "Null proof in theorem:\n"+toString());
00149 }
00150
00151 Theorem::Theorem(TheoremManager* tm, const Expr& lhs, const Expr& rhs,
00152 const Assumptions& assump, const Proof& pf, bool isAssump,
00153 int scope) {
00154 if (lhs == rhs) {
00155 d_expr = lhs.d_expr;
00156 d_expr->incRefcount();
00157 return;
00158 }
00159 TheoremValue* tv = new(tm->getRWMM())
00160 RWTheoremValue(tm, lhs, rhs, assump, pf, isAssump, scope);
00161 tv->d_refcount++;
00162 d_thm = ((long)tv)|0x1;
00163 DebugAssert(!withProof() || !pf.isNull(),
00164 "Null proof in theorem:\n"+toString());
00165 }
00166
00167
00168
00169 Theorem::Theorem(const Theorem &th) : d_thm(th.d_thm) {
00170 if (d_thm & 0x1) {
00171 DebugAssert(thm()->d_refcount > 0,
00172 "Theorem(const Theorem&): refcount = "
00173 + int2string(thm()->d_refcount));
00174 thm()->d_refcount++;
00175
00176 } else if (d_thm != 0) {
00177 exprValue()->incRefcount();
00178 }
00179 }
00180
00181 Theorem::Theorem(const Expr& e) : d_expr(e.d_expr)
00182 {
00183 d_expr->incRefcount();
00184 }
00185
00186
00187 Theorem::~Theorem() {
00188 if (d_thm & 0x1) {
00189 TheoremValue* tv = thm();
00190
00191 IF_DEBUG(FatalAssert(tv->d_refcount > 0,
00192 "~Theorem(): refcount = "
00193 + int2string(tv->d_refcount));)
00194 if((--tv->d_refcount) == 0) {
00195
00196 MemoryManager* mm = tv->getMM();
00197 delete tv;
00198 mm->deleteData(tv);
00199 }
00200 }
00201 else if (d_thm != 0) {
00202 exprValue()->decRefcount();
00203 }
00204 }
00205
00206 void Theorem::printx() const { getExpr().print(); }
00207 void Theorem::printxnodag() const { getExpr().printnodag(); }
00208 void Theorem::pprintx() const { getExpr().pprint(); }
00209 void Theorem::pprintxnodag() const { getExpr().pprintnodag(); }
00210 void Theorem::print() const { cout << toString() << endl; }
00211
00212
00213 bool Theorem::withProof() const {
00214 if (isRefl()) return exprValue()->d_em->getTM()->withProof();
00215 return thm()->d_tm->withProof();
00216 }
00217
00218 bool Theorem::withAssumptions() const {
00219 if (isRefl()) return exprValue()->d_em->getTM()->withAssumptions();
00220 return thm()->d_tm->withAssumptions();
00221 }
00222
00223 bool Theorem::isRewrite() const {
00224 DebugAssert(!isNull(), "CVC3::Theorem::isRewrite(): we are Null");
00225 return isRefl() || thm()->isRewrite();
00226 }
00227
00228
00229 Expr Theorem::getExpr() const {
00230 DebugAssert(!isNull(), "CVC3::Theorem::getExpr(): we are Null");
00231 if (isRefl()) {
00232 Expr e(exprValue());
00233 if (e.isTerm()) return e.eqExpr(e);
00234 else return e.iffExpr(e);
00235 }
00236 else return thm()->getExpr();
00237 }
00238
00239 const Expr& Theorem::getLHS() const {
00240 DebugAssert(!isNull(), "CVC3::Theorem::getLHS: we are Null");
00241 if (isRefl()) return *((Expr*)(&d_expr));
00242 else return thm()->getLHS();
00243 }
00244
00245 const Expr& Theorem::getRHS() const {
00246 DebugAssert(!isNull(), "CVC3::Theorem::getRHS: we are Null");
00247 if (isRefl()) return *((Expr*)(&d_expr));
00248 else return thm()->getRHS();
00249 }
00250
00251
00252
00253
00254
00255
00256
00257
00258 void Theorem::getAssumptionsRec(set<Expr>& assumptions) const
00259 {
00260 if (isRefl() || isFlagged()) return;
00261 setFlag();
00262 if(isAssump()) {
00263 assumptions.insert(getExpr());
00264 }
00265 else {
00266 const Assumptions& a = getAssumptionsRef();
00267 for(Assumptions::iterator i=a.begin(), iend=a.end(); i!=iend; ++i)
00268 (*i).getAssumptionsRec(assumptions);
00269 }
00270 }
00271
00272
00273 void Theorem::getLeafAssumptions(vector<Expr>& assumptions,
00274 bool negate) const
00275 {
00276 if (isNull() || isRefl()) return;
00277 set<Expr> assumpSet;
00278 clearAllFlags();
00279 getAssumptionsRec(assumpSet);
00280
00281 for(set<Expr>::iterator i=assumpSet.begin(), iend=assumpSet.end();
00282 i!=iend; ++i)
00283 assumptions.push_back(negate ? (*i).negate() : *i);
00284 }
00285
00286
00287 void Theorem::GetSatAssumptionsRec(vector<Theorem>& assumptions) const
00288 {
00289 DebugAssert(!isRefl() && !isFlagged(), "Invariant violated");
00290 setFlag();
00291 Expr e = getExpr();
00292 if (e.isAbsLiteral()) {
00293 if (isAssump() ||
00294 e.isRegisteredAtom() ||
00295 (e.isNot() && e[0].isRegisteredAtom())) {
00296 assumptions.push_back(*this);
00297 return;
00298 }
00299 }
00300 const Assumptions& a = getAssumptionsRef();
00301 for (Assumptions::iterator i = a.begin(); i != a.end(); i++) {
00302 if ((*i).isRefl() || (*i).isFlagged()) continue;
00303 (*i).GetSatAssumptionsRec(assumptions);
00304 }
00305 }
00306
00307
00308 void Theorem::GetSatAssumptions(vector<Theorem>& assumptions) const {
00309 DebugAssert(!isRefl() && !isFlagged(), "Invariant violated");
00310 setFlag();
00311 const Assumptions& a = getAssumptionsRef();
00312 for (Assumptions::iterator i = a.begin(); i != a.end(); i++) {
00313 if ((*i).isRefl() || (*i).isFlagged()) continue;
00314 (*i).GetSatAssumptionsRec(assumptions);
00315 }
00316 }
00317
00318
00319 void Theorem::getAssumptionsAndCongRec(set<Expr>& assumptions,
00320 vector<Expr>& congruences) const
00321 {
00322 if (isRefl() || isFlagged()) return;
00323 setFlag();
00324 if(isAssump()) {
00325 assumptions.insert(getExpr());
00326 }
00327 else {
00328 const Assumptions& a = getAssumptionsRef();
00329 if (isSubst() && a.size() == 1) {
00330 vector<Expr> hyp;
00331 const Theorem& thm = *(a.begin());
00332 thm.getAssumptionsAndCongRec(assumptions, congruences);
00333 if (thm.isRewrite() && thm.getLHS().isTerm()
00334 && thm.getLHS().isAtomic() && thm.getRHS().isAtomic() &&
00335 !thm.isRefl()) {
00336 hyp.push_back(!thm.getExpr());
00337 }
00338 else return;
00339 const Expr& e = getExpr();
00340 if (e.isAtomicFormula()) {
00341 if (e[0] < e[1]) {
00342 hyp.push_back(e[1].eqExpr(e[0]));
00343 }
00344 else {
00345 hyp.push_back(e);
00346 }
00347 congruences.push_back(Expr(OR, hyp));
00348 }
00349 else if (e[0].isAtomicFormula() && !e[0].isEq()) {
00350 hyp.push_back(!e[0]);
00351 hyp.push_back(e[1]);
00352 congruences.push_back(Expr(OR, hyp));
00353 hyp.pop_back();
00354 hyp.pop_back();
00355 hyp.push_back(e[0]);
00356 hyp.push_back(!e[1]);
00357 congruences.push_back(Expr(OR, hyp));
00358 }
00359 }
00360 else {
00361 Assumptions::iterator i=a.begin(), iend=a.end();
00362 for(; i!=iend; ++i)
00363 (*i).getAssumptionsAndCongRec(assumptions, congruences);
00364 }
00365 }
00366 }
00367
00368
00369 void Theorem::getAssumptionsAndCong(vector<Expr>& assumptions,
00370 vector<Expr>& congruences,
00371 bool negate) const
00372 {
00373 if (isNull() || isRefl()) return;
00374 set<Expr> assumpSet;
00375 clearAllFlags();
00376 getAssumptionsAndCongRec(assumpSet, congruences);
00377
00378 for(set<Expr>::iterator i=assumpSet.begin(), iend=assumpSet.end();
00379 i!=iend; ++i)
00380 assumptions.push_back(negate ? (*i).negate() : *i);
00381 }
00382
00383
00384 const Assumptions& Theorem::getAssumptionsRef() const
00385 {
00386 DebugAssert(!isNull(), "CVC3::Theorem::getAssumptionsRef: we are Null");
00387 if (!isRefl()) {
00388 return thm()->getAssumptionsRef();
00389 }
00390 else return Assumptions::emptyAssump();
00391 }
00392
00393
00394 bool Theorem::isAssump() const {
00395 DebugAssert(!isNull(), "CVC3::Theorem::isAssump: we are Null");
00396 return isRefl() ? false : thm()->isAssump();
00397 }
00398
00399
00400
00401 Proof Theorem::getProof() const {
00402 static Proof null;
00403 DebugAssert(!isNull(), "CVC3::Theorem::getProof: we are Null");
00404 if (isRefl()) {
00405 return Proof(Expr(PF_APPLY,
00406 exprValue()->d_em->newVarExpr("refl"),
00407 Expr(exprValue())));
00408 }
00409 else if (withProof() == true)
00410 return thm()->getProof();
00411 else
00412 return null;
00413 }
00414
00415 bool Theorem::isFlagged() const {
00416 DebugAssert(!isNull(), "CVC3::Theorem::isFlagged: we are Null");
00417 if (isRefl()) return exprValue()->d_em->getTM()->isFlagged((long)d_expr);
00418 else return thm()->isFlagged();
00419 }
00420
00421 void Theorem::clearAllFlags() const {
00422 DebugAssert(!isNull(), "CVC3::Theorem::clearAllFlags: we are Null");
00423 if (isRefl()) {
00424 exprValue()->d_em->getTM()->clearAllFlags();
00425 } else thm()->clearAllFlags();
00426 }
00427
00428 void Theorem::setFlag() const {
00429 DebugAssert(!isNull(), "CVC3::Theorem::setFlag: we are Null");
00430 if (isRefl()) exprValue()->d_em->getTM()->setFlag((long)d_expr);
00431 else thm()->setFlag();
00432 }
00433
00434 void Theorem::setCachedValue(int value) const {
00435 DebugAssert(!isNull(), "CVC3::Theorem::setCachedValue: we are Null");
00436 if (isRefl()) exprValue()->d_em->getTM()->setCachedValue((long)d_expr, value);
00437 else thm()->setCachedValue(value);
00438 }
00439
00440 int Theorem::getCachedValue() const {
00441 DebugAssert(!isNull(), "CVC3::Theorem::getCachedValue: we are Null");
00442 if (isRefl()) return exprValue()->d_em->getTM()->getCachedValue((long)d_expr);
00443 return thm()->getCachedValue();
00444 }
00445
00446 void Theorem::setSubst() const {
00447 DebugAssert(!isNull() && !isRefl(), "CVC3::Theorem::setSubst: invalid thm");
00448 thm()->setSubst();
00449 }
00450
00451 bool Theorem::isSubst() const {
00452 DebugAssert(!isNull(), "CVC3::Theorem::isSubst: we are Null");
00453 if (isRefl()) return false;
00454 return thm()->isSubst();
00455 }
00456
00457 void Theorem::setExpandFlag(bool val) const {
00458 DebugAssert(!isNull(), "CVC3::Theorem::setExpandFlag: we are Null");
00459 if (isRefl()) exprValue()->d_em->getTM()->setExpandFlag((long)d_expr, val);
00460 thm()->setExpandFlag(val);
00461 }
00462
00463 bool Theorem::getExpandFlag() const {
00464 DebugAssert(!isNull(), "CVC3::Theorem::getExpandFlag: we are Null");
00465 if (isRefl()) return exprValue()->d_em->getTM()->getExpandFlag((long)d_expr);
00466 return thm()->getExpandFlag();
00467 }
00468
00469 void Theorem::setLitFlag(bool val) const {
00470 DebugAssert(!isNull(), "CVC3::Theorem::setLitFlag: we are Null");
00471 if (isRefl()) exprValue()->d_em->getTM()->setLitFlag((long)d_expr, val);
00472 thm()->setLitFlag(val);
00473 }
00474
00475 bool Theorem::getLitFlag() const {
00476 DebugAssert(!isNull(), "CVC3::Theorem::getLitFlag: we are Null");
00477 if (isRefl()) return exprValue()->d_em->getTM()->getLitFlag((long)d_expr);
00478 return thm()->getLitFlag();
00479 }
00480
00481 bool Theorem::isAbsLiteral() const {
00482 return getExpr().isAbsLiteral();
00483 }
00484
00485 int Theorem::getScope() const {
00486 DebugAssert(!isNull(), "CVC3::Theorem::getScope: we are Null");
00487 return isRefl() ? 0 : thm()->getScope();
00488 }
00489
00490 unsigned Theorem::getQuantLevel() const {
00491 DebugAssert(!isNull(), "CVC3::Theorem::getQuantLevel: we are Null");
00492 TRACE("quant-level", "isRefl? ", isRefl(), "");
00493 return isRefl() ? 0 : thm()->getQuantLevel();
00494 }
00495
00496 unsigned Theorem::getQuantLevelDebug() const {
00497 DebugAssert(!isNull(), "CVC3::Theorem::getQuantLevel: we are Null");
00498 TRACE("quant-level", "isRefl? ", isRefl(), "");
00499 return isRefl() ? 0 : thm()->getQuantLevelDebug();
00500 }
00501
00502
00503 void Theorem::setQuantLevel(unsigned level) {
00504 DebugAssert(!isNull(), "CVC3::Theorem::setQuantLevel: we are Null");
00505
00506 if (isRefl()) return;
00507 thm()->setQuantLevel(level);
00508 }
00509
00510 size_t Theorem::hash() const {
00511 static std::hash<long int> h;
00512 return h(d_thm);
00513 }
00514
00515 void Theorem::recursivePrint(int& i) const {
00516 const Assumptions::iterator iend = getAssumptionsRef().end();
00517 Assumptions::iterator it = getAssumptionsRef().begin();
00518 if (!isAssump()) {
00519 for (; it != iend; ++it) {
00520 if (it->isFlagged()) continue;
00521 it->recursivePrint(i);
00522 it->setFlag();
00523 }
00524 }
00525
00526 setCachedValue(i++);
00527 cout << "[" << getCachedValue()
00528 << "]@" << getScope() << "\tTheorem: {";
00529
00530 if (isAssump()) {
00531 cout << "assump";
00532 }
00533 else if (getAssumptionsRef().empty()) {
00534 cout << "empty";
00535 }
00536 else {
00537 for (it = getAssumptionsRef().begin(); it != iend; ++it) {
00538 if (it != getAssumptionsRef().begin()) cout << ", ";
00539 cout << "[" << it->getCachedValue() << "]" ;
00540 }
00541 }
00542 cout << "}" << endl << "\t\t|- " << getExpr();
00543 if (isSubst()) cout << " [[Subst]]";
00544 cout << endl;
00545 }
00546
00547
00548
00549
00550
00551
00552
00553
00554
00555
00556
00557
00558
00559
00560
00561
00562
00563
00564
00565
00566
00567
00568
00569
00570
00571
00572
00573
00574
00575
00576
00577
00578
00579 ostream& Theorem::print(ostream& os, const string& name) const {
00580 if(isNull()) return os << name << "(Null)";
00581 ExprManager *em = getExpr().getEM();
00582 if (isRefl()) os << getExpr();
00583 else if (withAssumptions()) {
00584 em->incIndent(name.size()+2);
00585 os << name << "([" << thm() << "#" << thm()->d_refcount << "]@"
00586 << getScope() << "\n[";
00587 if(isAssump()) os << "Assump";
00588 else {
00589 if(thm()->d_tm->getFlags()["print-assump"].getBool()
00590 && em->isActive())
00591 os << getAssumptionsRef();
00592 else
00593 os << "<assumptions>";
00594 }
00595 os << "]\n |--- ";
00596 em->indent(7);
00597 if(em->isActive()) os << getExpr();
00598 else os << "(being destructed)";
00599 if(withProof())
00600 os << "\n Proof = " << getProof();
00601 return os << ")";
00602 }
00603 else {
00604 em->incIndent(name.size()+1);
00605 os << name << "(";
00606 if(em->isActive()) os << getExpr();
00607 else os << "being destructed";
00608 return os << ")";
00609 }
00610 return os;
00611 }
00612
00613
00614 }