CVC3

# theorem.cpp

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