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 //
00024 // See theorem.h file for more information.
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   // Assignment operator
00090   Theorem& Theorem::operator=(const Theorem& th) {
00091     // Handle self-assignment
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       //      IF_DEBUG(if((!isNull()) && tv->d_refcount == 1)
00117       //               TRACE("theorem", "Delete ", *this, ""));
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   // 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       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     //    TRACE("theorem", "Theorem(e) => ", *this, "");
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     // record that rhs was simplified from lhs, provided that both are
00155     // atomic and rhs is a fresh expression, following SVC. We try to
00156     // approximate this by seeing if the rhs was the last created
00157     // expression (i.e. it has the last index handed out by the
00158     // expression manager), but that's not reliable since the
00159     // expressions may have been created in a different order than
00160     // they are passed into Theorem().
00161 
00162 //     if (rhs.hasLastIndex() // FIXME: is this OK to comment out?
00163 //  // && tm->getVCL()->theoryCore()->isAtomicFormula(rhs)
00164 //  // && tm->getVCL()->theoryCore()->isAtomicFormula(lhs)
00165 //  )
00166 //       ((Expr &)rhs).setSimpFrom(lhs.hasSimpFrom() ?
00167 //        lhs.getSimpFrom() :
00168 //        lhs);
00169 //    TRACE("theorem", "Theorem(lhs,rhs) => ", *this, "");
00170     DebugAssert(!withProof() || !pf.isNull(),
00171     "Null proof in theorem:\n"+toString());
00172   }
00173 
00174 
00175   // Copy constructor
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       //      TRACE("theorem", "Theorem(Theorem&) => ", *this, "");
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   // Destructor
00194   Theorem::~Theorem() {
00195     if (d_thm & 0x1) {
00196       TheoremValue* tv = thm();
00197       //      TRACE("theorem", "~Theorem(", *this, ") {");
00198       IF_DEBUG(FatalAssert(tv->d_refcount > 0,
00199                            "~Theorem(): refcount = "
00200                            + int2string(tv->d_refcount)));
00201       if((--tv->d_refcount) == 0) {
00202         //        TRACE_MSG("theorem", "~Theorem(): deleting");
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   // Test if we are running in a proof production mode and with assumptions
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   // Return the theorem value as an Expr
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 // Return the assumptions.
00259 // void Theorem::getAssumptions(Assumptions& a) const
00260 // {
00261 //   a = getAssumptionsRef();
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   // Order assumptions by their creation time
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   // Return the proof of the theorem.  If running without proofs,
00310   // return the Null proof.
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   // Return the scope level at which this theorem was created
00436 //   int Theorem::getScope() const {
00437 //     DebugAssert(!isNull(), "CVC3::Theorem::getScope: we are Null");
00438 //     return thm()->getScope();
00439 //   }
00440 
00441 //   Assumptions Theorem::getUserAssumptions() const {
00442 //     ExprMap<Theorem> em;
00443 //     Assumptions a = getAssumptionsCopy();
00444 
00445 //     collectAssumptions(a, em);
00446     
00447 //     return a;
00448 //   }
00449 
00450 //   void collectAssumptions(Assumptions &a, ExprMap<Theorem> em ) const {
00451 //     if (isAssump()) {
00452 //       // cache?
00453 //       return;
00454 //     }
00455     
00456 //     const Assumptions a2 = thm()->getAssumptions();
00457 //     a.add(a2);
00458 //     Assumptions::iterator a2begin = a2.begin();
00459 //     const Assumptions::iterator a2end = a2.end();
00460 
00461 
00462 //   }
00463 
00464 
00465   // Printing Theorem
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 } // end of namespace CVC3

Generated on Tue Jul 3 14:33:38 2007 for CVC3 by  doxygen 1.5.1