# 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  * Copyright (C) 2003 by the Board of Trustees of Leland Stanford
00011  * Junior University and by New York University.
00012  *
00013  * License to use, copy, modify, sell and/or distribute this software
00014  * and its documentation for any purpose is hereby granted without
00015  * royalty, subject to the terms and conditions defined in the \ref
00016  * LICENSE file provided with this distribution.  In particular:
00017  *
00018  * - The above copyright notice and this permission notice must appear
00019  * in all copies of the software and related documentation.
00020  *
00021  * - THE SOFTWARE IS PROVIDED "AS-IS", WITHOUT ANY WARRANTIES,
00022  * EXPRESSED OR IMPLIED.  USE IT AT YOUR OWN RISK.
00023  *
00024  * <hr>
00025  *
00026  */
00027 /*****************************************************************************/
00028 // CLASS: Theorem
00029 //
00030 // AUTHOR: Sergey Berezin, 07/05/02
00031 //
00032 // See theorem.h file for more information.
00033 ///////////////////////////////////////////////////////////////////////////////
00034
00035 #include "theorem.h"
00036 #include "theorem_value.h"
00037 #include "command_line_flags.h"
00038
00039 namespace CVCL {
00040   using namespace std;
00041
00042   //! Compare Theorems by their expressions.  Return -1, 0, or 1.
00043   /*!
00044    *  This is an arbitrary total ordering on Theorems.  For
00045    *  simplicity, we define rewrite theorems (e1 = e2 or e1 <=> e2) to
00046    *  be smaller than other theorems.
00047    */
00048   /*
00049   int compare(const Theorem& t1, const Theorem& t2) {
00050     return compare(t1.getExpr(), t2.getExpr());
00051   }
00052   */
00053   int compare(const Theorem& t1, const Theorem& t2) {
00054     if(t1.d_thm == t2.d_thm) return 0;
00055     if(t1.isNull()) return -1; // Null Theorem is less than other theorems
00056     if(t2.isNull()) return 1;
00057
00058     bool rw1(t1.isRewrite()), rw2(t2.isRewrite());
00059
00060     if(!rw2) return compare(t1, t2.getExpr());
00061     else if(!rw1) return -compare(t2, t1.getExpr());
00062     else {
00063       int res(compare(t1.getLHS(), t2.getLHS()));
00064       if(res==0) res = compare(t1.getRHS(), t2.getRHS());
00065       return res;
00066     }
00067   }
00068   /*
00069   int compare(const Theorem& t1, const Expr& e2) {
00070     return compare(t1.getExpr(), e2);
00071   }
00072   */
00073   int compare(const Theorem& t1, const Expr& e2) {
00074     bool rw1(t1.isRewrite()), rw2(e2.isEq() || e2.isIff());
00075     if(!rw1) {
00076       const Expr& e1 = t1.getExpr();
00077       rw1 = (e1.isEq() || e1.isIff());
00078     }
00079     if(rw1) {
00080       if(rw2) {
00081         int res(compare(t1.getLHS(), e2[0]));
00082         if(res==0) res = compare(t1.getRHS(), e2[1]);
00083         return res;
00084       } else return -1;
00085     } else {
00086       if(rw2) return 1;
00087       else return compare(t1.getExpr(), e2);
00088     }
00089   }
00090
00091   int compareByPtr(const Theorem& t1, const Theorem& t2) {
00092     if(t1.d_thm == t2.d_thm) return 0;
00093     else if(t1.d_thm < t2.d_thm) return -1;
00094     else return 1;
00095   }
00096
00097   // Assignment operator
00098   Theorem& Theorem::operator=(const Theorem& th) {
00099     // Handle self-assignment
00100     if(this == &th) return *this;
00101     IF_DEBUG(bool notNull(!isNull() || !th.isNull());
00102              if(notNull)
00103              TRACE("theorem", "Theorem::operator=(",
00104                    *this, " := "+th.toString()+") {"));
00105     DebugAssert(isNull() || d_thm->d_refcount > 0,
00106                 "Theorem::operator=: OLD refcount = "
00107                 + int2string(d_thm->d_refcount));
00108
00109     IF_DEBUG(if((!isNull()) && d_thm->d_refcount == 1)
00110              TRACE("theorem", "Delete ", *this, ""));
00111     if((!isNull()) && --(d_thm->d_refcount) == 0) {
00112       MemoryManager* mm = d_thm->getMM();
00113       delete d_thm;
00114       mm->deleteData(d_thm);
00115     }
00116     d_thm = th.d_thm;
00117     DebugAssert(isNull() || d_thm->d_refcount > 0,
00118                 "Theorem::operator=: NEW refcount = "
00119                  + int2string(d_thm->d_refcount)
00120                  + " in " + this->toString());
00121     if (d_thm) ++(d_thm->d_refcount);
00122     IF_DEBUG(if(notNull)
00123              TRACE("theorem", "Theorem::operator= => ", *this," }"));
00124     return *this;
00125   }
00126
00127   // Constructors
00128   Theorem::Theorem(TheoremManager* tm, const Expr &thm,
00129                    const Assumptions& assump, const Proof& pf,
00130                    bool isAssump, int scope) {
00131     if(thm.isEq() || thm.isIff())
00132       d_thm = new(tm->getRWMM()) RWTheoremValue(tm, thm, assump, pf, isAssump, scope);
00133     else
00134       d_thm = new(tm->getMM()) TheoremValue(tm, thm, assump, pf, isAssump, scope);
00135     d_thm->d_refcount++;
00136     TRACE("theorem", "Theorem(e) => ", *this, "");
00137     DebugAssert(!withProof() || !pf.isNull(),
00138                 "Null proof in theorem:\n"+toString());
00139   }
00140
00141   Theorem::Theorem(TheoremManager* tm, const Expr& lhs, const Expr& rhs,
00142                    const Assumptions& assump, const Proof& pf, bool isAssump,
00143                    int scope) {
00144     d_thm = new(tm->getRWMM())
00145       RWTheoremValue(tm, lhs, rhs, assump, pf, isAssump, scope);
00146     d_thm->d_refcount++;
00147
00148     // record that rhs was simplified from lhs, provided that both are
00149     // atomic and rhs is a fresh expression, following SVC. We try to
00150     // approximate this by seeing if the rhs was the last created
00151     // expression (i.e. it has the last index handed out by the
00152     // expression manager), but that's not reliable since the
00153     // expressions may have been created in a different order than
00154     // they are passed into Theorem().
00155
00156     if (rhs.hasLastIndex() // FIXME: is this OK to comment out?
00157         // && tm->getVCL()->theoryCore()->isAtomicFormula(rhs)
00158         // && tm->getVCL()->theoryCore()->isAtomicFormula(lhs)
00159         )
00160       ((Expr &)rhs).setSimpFrom(lhs.hasSimpFrom() ?
00161                                 lhs.getSimpFrom() :
00162                                 lhs);
00163     TRACE("theorem", "Theorem(lhs,rhs) => ", *this, "");
00164     DebugAssert(!withProof() || !pf.isNull(),
00165                 "Null proof in theorem:\n"+toString());
00166   }
00167
00168
00169   Theorem::Theorem(TheoremManager* tm, const Expr& e, const Proof& pf) {
00170     d_thm = new(tm->getReflMM()) ReflexivityTheoremValue(tm, e, pf);
00171     d_thm->d_refcount++;
00172     TRACE("theorem", "Theorem(e=e) => ", *this, "");
00173     DebugAssert(!withProof() || !pf.isNull(),
00174                 "Null proof in theorem:\n"+toString());
00175   }
00176
00177
00178   // Copy constructor
00179   Theorem::Theorem(const Theorem &th) : d_thm(th.d_thm) {
00180     if(!isNull()) {
00181       DebugAssert(d_thm->d_refcount > 0,
00182                   "Theorem(const Theorem&): refcount = "
00183                   + int2string(d_thm->d_refcount));
00184       d_thm->d_refcount++;
00185       TRACE("theorem", "Theorem(Theorem&) => ", *this, "");
00186     }
00187   }
00188
00189   // Destructor
00190   Theorem::~Theorem() {
00191     if(!isNull()) {
00192       TRACE("theorem", "~Theorem(", *this, ") {");
00193       DebugAssert(d_thm->d_refcount > 0,
00194                   "~Theorem(): refcount = "
00195                   + int2string(d_thm->d_refcount));
00196       if((--d_thm->d_refcount) == 0) {
00197         TRACE_MSG("theorem", "~Theorem(): deleting");
00198         MemoryManager* mm = d_thm->getMM();
00199         delete d_thm;
00200         mm->deleteData(d_thm);
00201       }
00202       TRACE_MSG("theorem", "~Theorem() => }");
00203     }
00204   }
00205
00206   void Theorem::printx() const { getExpr().print(); }
00207
00208   void Theorem::print() const { cout << toString() << endl; }
00209
00210   // Test if we are running in a proof production mode and with assumptions
00211   bool Theorem::withProof() const {
00212     return d_thm->d_tm->withProof();
00213   }
00214   bool Theorem::withAssumptions() const {
00215     return d_thm->d_tm->withAssumptions();
00216   }
00217
00218   bool Theorem::isRewrite() const {
00219     DebugAssert(!isNull(), "CVCL::Theorem::isRewrite(): we are Null");
00220     return d_thm->isRewrite();
00221   }
00222
00223   // Return the theorem value as an Expr
00224   const Expr& Theorem::getExpr() const {
00225     DebugAssert(!isNull(), "CVCL::Theorem::getExpr(): we are Null");
00226     return d_thm->getExpr();
00227   }
00228
00229   const Expr& Theorem::getLHS() const {
00230     DebugAssert(!isNull(), "CVCL::Theorem::getLHS: we are Null");
00231     return d_thm->getLHS();
00232   }
00233
00234   const Expr& Theorem::getRHS() const {
00235     DebugAssert(!isNull(), "CVCL::Theorem::getRHS: we are Null");
00236     return d_thm->getRHS();
00237   }
00238
00239 // Return the assumptions.
00240 const Assumptions& Theorem::getAssumptions() const
00241 {
00242   if (!d_thm->isAssump() || !withAssumptions()) return getAssumptionsRef();
00243   DebugAssert(!isNull(), "CVCL::Theorem::getAssumptions: we are Null");
00244   Assumptions& a = d_thm->d_assump;
00245   if (a.isNull()) a.init();
00246   if (a.empty()) {
00248     a.setConst();
00249   }
00250   return a;
00251 }
00252
00253
00254 void Theorem::getAssumptionsRec(set<Expr>& assumptions) const
00255 {
00256   if(isFlagged()) return;
00257   setFlag();
00258   if(isAssump()) {
00259     assumptions.insert(getExpr());
00260   }
00261   else {
00262     Assumptions a(getAssumptions());
00263     for(Assumptions::iterator i=a.begin(), iend=a.end(); i!=iend; ++i)
00264       (*i).getAssumptionsRec(assumptions);
00265   }
00266 }
00267
00268
00269 void Theorem::getLeafAssumptions(vector<Expr>& assumptions,
00270                                  bool negate) const
00271 {
00272   if (isNull()) return;
00273   set<Expr> assumpSet;
00274   clearAllFlags();
00275   getAssumptionsRec(assumpSet);
00276   // Order assumptions by their creation time
00277   for(set<Expr>::iterator i=assumpSet.begin(), iend=assumpSet.end();
00278       i!=iend; ++i)
00279     assumptions.push_back(negate ? (*i).negate() : *i);
00280 }
00281
00282
00283 const Assumptions& Theorem::getAssumptionsRef() const
00284 {
00285   static Assumptions null;
00286   DebugAssert(!isNull(), "CVCL::Theorem::getAssumptionsRef: we are Null");
00287   if(withAssumptions()) {
00288     DebugAssert(!isAssump(), "CVCL::Theorem::getAssumptionsRef: "
00289                 "should call getAssumptions() on leaf assumptions");
00290     return d_thm->getAssumptionsRef();
00291   }
00292   else return null;
00293 }
00294
00295
00296   bool Theorem::isAssump() const {
00297     DebugAssert(!isNull(), "CVCL::Theorem::isAssump: we are Null");
00298     return d_thm->isAssump();
00299   }
00300
00301   // This method returns a *clean copy* of the Assumptions.
00302   // It can be modified without any effect on the theorem.
00303   // It's an error if called while running without assumptions.
00304   Assumptions Theorem::getAssumptionsCopy() const {
00305     return getAssumptions().copy();
00306   }
00307   // Return the proof of the theorem.  If running without proofs,
00308   // return the Null proof.
00309   const Proof& Theorem::getProof() const {
00310     static Proof null;
00311     DebugAssert(!isNull(), "CVCL::Theorem::getProof: we are Null");
00312     if(withProof() == true)
00313       return d_thm->getProof();
00314     else
00315       return null;
00316   }
00317
00318   bool Theorem::isFlagged() const {
00319     DebugAssert(!isNull(), "CVCL::Theorem::isFlagged: we are Null");
00320     return d_thm->isFlagged();
00321   }
00322
00323   void Theorem::clearAllFlags() const {
00324     DebugAssert(!isNull(), "CVCL::Theorem::clearAllFlags: we are Null");
00325     d_thm->clearAllFlags();
00326   }
00327
00328   void Theorem::setFlag() const {
00329     DebugAssert(!isNull(), "CVCL::Theorem::setFlag: we are Null");
00330     d_thm->setFlag();
00331   }
00332
00333   void Theorem::setCachedValue(int value) const {
00334     DebugAssert(!isNull(), "CVCL::Theorem::setCachedValue: we are Null");
00335     d_thm->setCachedValue(value);
00336   }
00337
00338   int Theorem::getCachedValue() const {
00339     DebugAssert(!isNull(), "CVCL::Theorem::getCachedValue: we are Null");
00340     return d_thm->getCachedValue();
00341   }
00342
00343   void Theorem::setExpandFlag(bool val) const {
00344     DebugAssert(!isNull(), "CVCL::Theorem::setExpandFlag: we are Null");
00345     d_thm->setExpandFlag(val);
00346   }
00347
00348   bool Theorem::getExpandFlag() const {
00349     DebugAssert(!isNull(), "CVCL::Theorem::getExpandFlag: we are Null");
00350     return d_thm->getExpandFlag();
00351   }
00352
00353   void Theorem::setLitFlag(bool val) const {
00354     DebugAssert(!isNull(), "CVCL::Theorem::setLitFlag: we are Null");
00355     d_thm->setLitFlag(val);
00356   }
00357
00358   bool Theorem::getLitFlag() const {
00359     DebugAssert(!isNull(), "CVCL::Theorem::getLitFlag: we are Null");
00360     return d_thm->getLitFlag();
00361   }
00362
00363   bool Theorem::isAbsLiteral() const {
00364     return getExpr().isAbsLiteral();
00365   }
00366
00367   int Theorem::getScope() const {
00368     DebugAssert(!isNull(), "CVCL::Theorem::getScope: we are Null");
00369     return d_thm->getScope();
00370   }
00371
00372   void Theorem::recursivePrint(int& i) const {
00373     cout << "[" << getCachedValue()
00374          << "]@" << getScope() << "\tTheorem: {";
00375
00376     if (isAssump()) {
00377       cout << "assump";
00378     }
00379     else if (getAssumptions().empty()) {
00380       cout << "empty";
00381     }
00382     else {
00383       const Assumptions::iterator iend = getAssumptions().end();
00384       for (Assumptions::iterator it = getAssumptions().begin();
00385            it != iend; ++it) {
00386         if (!it->isFlagged()) it->setCachedValue(i++);
00387         cout << "[" << it->getCachedValue() << "], " ;
00388       }
00389       cout << "}" << endl << "\t\t|- " << getExpr() << endl;
00390       for (Assumptions::iterator it = getAssumptions().begin();
00391            it != iend; ++it) {
00392         if (it->isFlagged()) continue;
00393         it->recursivePrint(i);
00394         it->setFlag();
00395       }
00396       return;
00397     }
00398     cout << "}" << endl << "\t\t|- " << getExpr() << endl;
00399   }
00400
00401
00402   // Return the scope level at which this theorem was created
00403 //   int Theorem::getScope() const {
00404 //     DebugAssert(!isNull(), "CVCL::Theorem::getScope: we are Null");
00405 //     return d_thm->getScope();
00406 //   }
00407
00408 //   Assumptions Theorem::getUserAssumptions() const {
00409 //     ExprMap<Theorem> em;
00410 //     Assumptions a = getAssumptionsCopy();
00411
00412 //     collectAssumptions(a, em);
00413
00414 //     return a;
00415 //   }
00416
00417 //   void collectAssumptions(Assumptions &a, ExprMap<Theorem> em ) const {
00418 //     if (isAssump()) {
00419 //       // cache?
00420 //       return;
00421 //     }
00422
00423 //     const Assumptions a2 = d_thm->getAssumptions();
00425 //     Assumptions::iterator a2begin = a2.begin();
00426 //     const Assumptions::iterator a2end = a2.end();
00427
00428
00429 //   }
00430
00431
00432   // Printing Theorem
00433   ostream& Theorem::print(ostream& os, const string& name) const {
00434     if(isNull()) return os << name << "(Null)";
00435     ExprManager *em = getExpr().getEM();
00436     if(withAssumptions()) {
00437       em->incIndent(name.size()+2);
00438       os << name << "([" << d_thm << "#" << d_thm->d_refcount << "]@"
00439          << getScope() << "\n[";
00440       if(isAssump()) os << "Assump";
00441       else {
00442         if(d_thm->d_tm->getFlags()["print-assump"].getBool()
00443            && em->isActive())
00444           os << getAssumptions();
00445         else
00446           os << "<assumptions>";
00447       }
00448       os << "]\n  |--- ";
00449       em->indent(7);
00450       if(em->isActive()) os << getExpr();
00451       else os << "(being destructed)";
00452       if(withProof())
00453         os << "\n Proof = " << getProof();
00454       return os << ")";
00455     }
00456     else {
00457       em->incIndent(name.size()+1);
00458       os << name << "(";
00459       if(em->isActive()) os << getExpr();
00460       else os << "being destructed";
00461       return os << ")";
00462     }
00463   }
00464
00465 } // end of namespace CVCL

Generated on Thu Apr 13 16:57:33 2006 for CVC Lite by  1.4.4