theorem_value.h

Go to the documentation of this file.
00001 /*****************************************************************************/
00002 /*!
00003  * \file theorem_value.h
00004  * 
00005  * Author: Sergey Berezin
00006  * 
00007  * Created: Dec 10 01:03:34 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: TheoremValue
00021 //
00022 // AUTHOR: Sergey Berezin, 07/05/02
00023 //
00024 // Abstract:
00025 //
00026 // A class representing a proven fact in CVC.  It stores the theorem
00027 // as a CVC expression, and in the appropriate modes also the set of
00028 // assumptions and the proof.
00029 //
00030 // The idea is to allow only a few trusted classes to create values of
00031 // this class.  If all the critical computations in the decision
00032 // procedures are done through the use of Theorems, then soundness of
00033 // these decision procedures will rely only on the soundness of the
00034 // methods in the trusted classes (the inference rules).
00035 //
00036 // Thus, proof checking can effectively be done at run-time on the
00037 // fly.  Or the soundness may be potentially proven by static analysis
00038 // and many run-time checks can then be optimized away.
00039 //
00040 // This theorem_value.h file should NOT be used by the decision
00041 // procedures.  Use theorem.h instead.
00042 //
00043 ////////////////////////////////////////////////////////////////////////
00044 
00045 #ifndef _cvc3__theorem_value_h_
00046 #define _cvc3__theorem_value_h_
00047 
00048 #include "theorem.h"
00049 #include "theorem_manager.h"
00050 //#include "vcl.h"
00051 
00052 //#include "theory_core.h"
00053 
00054 
00055 namespace CVC3 {
00056 
00057   //  extern VCL* myvcl;
00058 
00059   class TheoremValue
00060   {
00061     // These are the only classes that can create new TheoremValue classes
00062     friend class Theorem;
00063     friend class RegTheoremValue;
00064     friend class RWTheoremValue;
00065 
00066   protected:
00067     //! Theorem Manager
00068     TheoremManager* d_tm;
00069 
00070     //! The expression representing a theorem
00071     Expr d_thm;
00072 
00073     //! Proof of the theorem
00074     Proof d_proof;
00075 
00076     //! How many pointers to this theorem value
00077     unsigned d_refcount;
00078 
00079     //! Largest scope level of the assumptions
00080     int d_scopeLevel;
00081 
00082     //! Quantification level of this theorem
00083     unsigned d_quantLevel;
00084 
00085     //! Temporary flag used during traversals
00086     unsigned d_flag;
00087 
00088     //! Temporary cache used during traversals
00089     int d_cachedValue : 29;
00090 
00091     bool d_isAssump : 1;
00092     bool d_expand : 1; //!< whether it should this be expanded in graph traversal
00093     bool d_clauselit : 1;  //!< whether it belongs to the conflict clause
00094 
00095 
00096   private:
00097     // Constructor.   
00098     /*!
00099      * NOTE: it is private; only friend classes can call it.
00100      *
00101      * If the assumptions refer to only one theorem, grab the
00102      * assumptions of that theorem instead.
00103      */
00104     TheoremValue(TheoremManager* tm, const Expr &thm,
00105      const Proof& pf, bool isAssump) :
00106       d_tm(tm), d_thm(thm), d_proof(pf), d_refcount(0),
00107       d_scopeLevel(0), d_quantLevel(0), d_flag(0), d_isAssump(isAssump) {}
00108 
00109     // Disable copy constructor and assignment
00110     TheoremValue(const TheoremValue& t) {
00111       FatalAssert(false, "TheoremValue() copy constructor called");
00112     }
00113     TheoremValue& operator=(const TheoremValue& t) {
00114       FatalAssert(false, "TheoremValue assignment operator called");
00115       return *this;
00116     }
00117 
00118     bool isFlagged() const {
00119       return d_flag == d_tm->getFlag();
00120     }
00121 
00122     void clearAllFlags() {
00123       d_tm->clearAllFlags();
00124     }
00125     
00126     void setFlag() {
00127       d_flag = d_tm->getFlag();
00128     }
00129 
00130     void setCachedValue(int value) {
00131       d_cachedValue = value;
00132     }
00133 
00134     int getCachedValue() const {
00135       return d_cachedValue;
00136     }
00137 
00138     void setExpandFlag(bool val) {
00139       d_expand = val;
00140     }
00141 
00142     bool getExpandFlag() {
00143       return d_expand;
00144     }
00145     
00146     void setLitFlag(bool val) {
00147       d_clauselit = val;
00148     }
00149 
00150     bool getLitFlag() {
00151       return d_clauselit;
00152     }
00153 
00154     int getScope() {
00155       return d_scopeLevel;
00156     }
00157 
00158     unsigned getQuantLevel() { return d_quantLevel; }
00159     void setQuantLevel(unsigned level) { d_quantLevel = level; }
00160 
00161 //     virtual bool isRewrite() const { return d_thm.isEq() || d_thm.isIff(); }
00162     virtual bool isRewrite() const { return false; }
00163 
00164     virtual const Expr& getExpr() const { return d_thm; }
00165     virtual const Expr& getLHS() const {
00166       //      TRACE("getExpr","TheoremValue::getLHS called (",d_thm,")");
00167       DebugAssert(isRewrite(),
00168       "TheoremValue::getLHS() called on non-rewrite theorem:\n"
00169       +toString());
00170       return d_thm[0];
00171     }
00172     virtual const Expr& getRHS() const {
00173       //      TRACE("getExpr","TheoremValue::getRHS called (",d_thm,")");
00174       DebugAssert(isRewrite(),
00175       "TheoremValue::getRHS() called on non-rewrite theorem:\n"
00176       +toString());
00177       return d_thm[1];
00178     }
00179 
00180     virtual const Assumptions& getAssumptionsRef() const = 0;
00181 
00182     bool isAssump() const { return d_isAssump; }
00183     const Proof& getProof() { return d_proof; }
00184 
00185   public:
00186     // Destructor
00187     virtual ~TheoremValue() { 
00188       IF_DEBUG(FatalAssert(d_refcount == 0,
00189                            "Thm::TheoremValue::~TheoremValue(): refcount != 0."));
00190     }
00191 
00192     std::string toString() const {
00193       return getAssumptionsRef().toString() + " |- " + getExpr().toString();
00194     }
00195 
00196     // Memory management
00197     virtual MemoryManager* getMM() = 0;
00198 
00199   }; // end of class TheoremValue
00200 
00201 ///////////////////////////////////////////////////////////////////////////////
00202 //                                                                           //
00203 // Class: RegTheoremValue                                                    //
00204 // Author: Clark Barrett                                                     //
00205 // Created: Fri May  2 12:51:55 2003                                         //
00206 // Description: A special subclass for non-rewrite theorems.  Assumptions are//
00207 //              embedded in the object for easy reference.                   //
00208 //                                                                           //
00209 ///////////////////////////////////////////////////////////////////////////////
00210   class RegTheoremValue :public TheoremValue
00211   {
00212     friend class Theorem;
00213 
00214   protected:
00215     //! The assumptions for the theorem
00216     Assumptions d_assump;
00217 
00218   private:
00219     // Constructor.   NOTE: it is private; only friend classes can call it.
00220     RegTheoremValue(TheoremManager* tm, const Expr& thm,
00221                     const Assumptions& assump, const Proof& pf, bool isAssump,
00222                     int scope = -1)
00223       : TheoremValue(tm, thm, pf, isAssump), d_assump(assump)
00224     {
00225       DebugAssert(d_tm->isActive(), "TheoremValue()");
00226       if (isAssump) {
00227         DebugAssert(assump.empty(), "Expected empty assumptions");
00228         // refcount tricks are because a loop is created with Assumptions
00229         d_refcount = 1;
00230         {
00231           Theorem t(this);
00232           d_assump.add1(t);
00233         }
00234         d_refcount = 0;
00235         if (scope == -1) d_scopeLevel = tm->getCM()->scopeLevel();
00236         else d_scopeLevel = scope;
00237       }
00238       else {
00239         if (!d_assump.empty()) {
00240           const Assumptions::iterator iend = d_assump.end();
00241           for (Assumptions::iterator i = d_assump.begin(); 
00242                i != iend; ++i) {
00243             if (i->getScope() > d_scopeLevel)
00244               d_scopeLevel = i->getScope();
00245             if (i->getQuantLevel() > d_quantLevel)
00246               d_quantLevel = i->getQuantLevel();
00247           }
00248         }
00249       }
00250       TRACE("quantlevel", d_quantLevel, " theorem get_1 ", thm.toString()); 
00251       TRACE("quantlevel", d_quantLevel, " theorem get_1 ", thm.getIndex()); 
00252     }
00253 
00254   public:
00255     // Destructor
00256     ~RegTheoremValue() {
00257       if (d_isAssump) {
00258         IF_DEBUG(FatalAssert(d_assump.size() == 1, "Expected size 1"));
00259         IF_DEBUG(FatalAssert(d_assump.getFirst().thm() == this, "Expected loop"));
00260         d_assump.getFirst().d_thm = 0;
00261       }
00262     }
00263 
00264     const Assumptions& getAssumptionsRef() const { return d_assump; }
00265 
00266     // Memory management
00267     MemoryManager* getMM() { return d_tm->getMM(); }
00268 
00269     void* operator new(size_t size, MemoryManager* mm) {
00270       return mm->newData(size);
00271     }
00272     void operator delete(void* pMem, MemoryManager* mm) {
00273       mm->deleteData(pMem);
00274     }
00275 
00276     void operator delete(void* d) { }
00277 
00278   }; // end of class RegTheoremValue
00279 
00280 ///////////////////////////////////////////////////////////////////////////////
00281 //                                                                           //
00282 // Class: RWTheoremValue                                                     //
00283 // Author: Clark Barrett                                                     //
00284 // Created: Fri May  2 12:51:55 2003                                         //
00285 // Description: A special subclass for theorems of the form A |- t=t' or     //
00286 //              A |- phi iff phi'.  The actual Expr is only created on       //
00287 //              demand.  The idea is that getLHS and getRHS should be used   //
00288 //              whenever possible, avoiding creating unnecessary Expr's.     //
00289 //                                                                           //
00290 ///////////////////////////////////////////////////////////////////////////////
00291   class RWTheoremValue :public TheoremValue
00292   {
00293     friend class Theorem;
00294 
00295   protected:
00296     // d_thm in the base class contains the full expression, which is
00297     // only constructed on demand.
00298     Expr d_lhs;
00299     Expr d_rhs;
00300     Assumptions* d_assump;
00301 
00302   private:
00303     void init(const Assumptions& assump, int scope)
00304     {
00305       DebugAssert(d_tm->isActive(), "TheoremValue()");
00306       if (d_isAssump) {
00307         DebugAssert(assump.empty(), "Expected empty assumptions");
00308         // refcount tricks are because a loop is created with Assumptions
00309         d_refcount = 1;
00310         {
00311           Theorem t(this);
00312           d_assump = new Assumptions(t);
00313         }
00314         d_refcount = 0;
00315         if (scope == -1) d_scopeLevel = d_tm->getCM()->scopeLevel();
00316         else d_scopeLevel = scope;
00317       }
00318       else {
00319         if (!assump.empty()) {
00320           d_assump = new Assumptions(assump);
00321           const Assumptions::iterator iend = assump.end();
00322           for (Assumptions::iterator i = assump.begin(); 
00323                i != iend; ++i) {
00324             if (i->getScope() > d_scopeLevel)
00325               d_scopeLevel = i->getScope();
00326             if (i->getQuantLevel() > d_quantLevel)
00327               d_quantLevel = i->getQuantLevel();
00328           }
00329         }
00330       }
00331       TRACE("quantlevel", d_quantLevel, " theorem get ", d_thm.toString());
00332     }
00333 
00334     // Constructor.   NOTE: it is private; only friend classes can call it.
00335     RWTheoremValue(TheoremManager* tm, const Expr& lhs, const Expr& rhs,
00336        const Assumptions& assump, const Proof& pf, bool isAssump,
00337                    int scope = -1)
00338       : TheoremValue(tm, Expr(), pf, isAssump), d_lhs(lhs), d_rhs(rhs), d_assump(NULL)
00339     { init(assump, scope); }
00340 
00341     // Sometimes we have the full expression already created
00342     RWTheoremValue(TheoremManager* tm, const Expr& thm,
00343                    const Assumptions& assump, const Proof& pf, bool isAssump,
00344                    int scope = -1)
00345       : TheoremValue(tm, thm, pf, isAssump), d_lhs(thm[0]), d_rhs(thm[1]), d_assump(NULL)
00346     { init(assump, scope); }
00347 
00348     const Expr& getExpr() const {
00349       if (d_thm.isNull()) {
00350   bool isBool = d_lhs.getType().isBool();
00351   // have to fake out the const qualifier
00352   Expr* pexpr = const_cast<Expr*>(&d_thm);
00353   *pexpr = isBool ? d_lhs.iffExpr(d_rhs) : d_lhs.eqExpr(d_rhs);
00354   //  TRACE("getExpr", "getExpr called on RWTheorem (", d_thm, ")");
00355       }
00356       return d_thm;
00357     }
00358 
00359     const Expr& getLHS() const { return d_lhs; }
00360     const Expr& getRHS() const { return d_rhs; }
00361 
00362   public:
00363     // Destructor
00364     ~RWTheoremValue() {
00365       if (d_isAssump) {
00366         IF_DEBUG(FatalAssert(d_assump && d_assump->size() == 1, "Expected size 1"));
00367         IF_DEBUG(FatalAssert(d_assump->getFirst().thm() == this, "Expected loop"));
00368         d_assump->getFirst().d_thm = 0;
00369       }
00370       if (d_assump) delete d_assump;
00371     }
00372 
00373     bool isRewrite() const { return true; }
00374     const Assumptions& getAssumptionsRef() const {
00375       if (d_assump) return *d_assump;
00376       else return Assumptions::emptyAssump();
00377     }
00378 
00379     // Memory management
00380     MemoryManager* getMM() { return d_tm->getRWMM(); }
00381 
00382     void* operator new(size_t size, MemoryManager* mm) {
00383       return mm->newData(size);
00384     }
00385     void operator delete(void* pMem, MemoryManager* mm) {
00386       mm->deleteData(pMem);
00387     }
00388 
00389     void operator delete(void* d) { }
00390 
00391   }; // end of class RWTheoremValue
00392 
00393 }; // end of namespace CVC3
00394 
00395 #endif

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