CVC3

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 "assumptions.h"
00049 #include "theorem_manager.h"
00050 //#include "theory_core.h"
00051 //#include "vcl.h"
00052 
00053 namespace CVC3 {
00054 
00055   //extern VCL* myvcl; 
00056   class TheoremValue
00057   {
00058     // These are the only classes that can create new TheoremValue classes
00059     friend class Theorem;
00060     friend class RegTheoremValue;
00061     friend class RWTheoremValue;
00062 
00063   protected:
00064     //! Theorem Manager
00065     TheoremManager* d_tm;
00066 
00067     //! The expression representing a theorem
00068     Expr d_thm;
00069 
00070     //! Proof of the theorem
00071     Proof d_proof;
00072 
00073     //! How many pointers to this theorem value
00074     unsigned d_refcount;
00075 
00076     //! Largest scope level of the assumptions
00077     int d_scopeLevel;
00078 
00079     //! Quantification level of this theorem
00080     unsigned d_quantLevel;
00081     
00082 
00083     //! debug quantlevel, this one is from proof, not from assumption list
00084     //    unsigned d_quantLevelDebug;
00085 
00086     //! Temporary flag used during traversals
00087     unsigned d_flag;
00088 
00089     //! Temporary cache used during traversals
00090     int d_cachedValue : 28;
00091 
00092     bool d_isSubst : 1; //!< whether this theorem was generated by substitution
00093     bool d_isAssump : 1;
00094     bool d_expand : 1; //!< whether it should this be expanded in graph traversal
00095     bool d_clauselit : 1;  //!< whether it belongs to the conflict clause
00096 
00097 
00098   private:
00099     // Constructor.   
00100     /*!
00101      * NOTE: it is private; only friend classes can call it.
00102      *
00103      * If the assumptions refer to only one theorem, grab the
00104      * assumptions of that theorem instead.
00105      */
00106 
00107     //by yeting, we should do something to catch theorems created with empty assumptions.
00108     //one way is to set the d_quantLevel 999 here. 
00109 
00110     TheoremValue(TheoremManager* tm, const Expr &thm,
00111      const Proof& pf, bool isAssump) :
00112       d_tm(tm), d_thm(thm), d_proof(pf), d_refcount(0),
00113       d_scopeLevel(0), d_quantLevel(0), d_flag(0), d_cachedValue(0),
00114       d_isSubst(0), d_isAssump(isAssump), d_expand(0), d_clauselit(0) {}
00115 
00116     // Disable copy constructor and assignment
00117     TheoremValue(const TheoremValue& t) {
00118       FatalAssert(false, "TheoremValue() copy constructor called");
00119     }
00120     TheoremValue& operator=(const TheoremValue& t) {
00121       FatalAssert(false, "TheoremValue assignment operator called");
00122       return *this;
00123     }
00124 
00125     bool isFlagged() const {
00126       return d_flag == d_tm->getFlag();
00127     }
00128 
00129     void clearAllFlags() {
00130       d_tm->clearAllFlags();
00131     }
00132     
00133     void setFlag() {
00134       d_flag = d_tm->getFlag();
00135     }
00136 
00137     void setCachedValue(int value) {
00138       d_cachedValue = value;
00139     }
00140 
00141     int getCachedValue() const {
00142       return d_cachedValue;
00143     }
00144 
00145     void setSubst() { d_isSubst = true; }
00146     bool isSubst() { return d_isSubst; }
00147 
00148     void setExpandFlag(bool val) {
00149       d_expand = val;
00150     }
00151 
00152     bool getExpandFlag() {
00153       return d_expand;
00154     }
00155     
00156     void setLitFlag(bool val) {
00157       d_clauselit = val;
00158     }
00159 
00160     bool getLitFlag() {
00161       return d_clauselit;
00162     }
00163 
00164     int getScope() {
00165       return d_scopeLevel;
00166     }
00167 
00168     unsigned getQuantLevel() { return d_quantLevel; }
00169 
00170     unsigned getQuantLevelDebug() { 
00171       return 0;
00172       //  return d_quantLevelDebug; 
00173     }
00174 
00175     void setQuantLevel(unsigned level) { d_quantLevel = level; }
00176 
00177     unsigned recQuantLevel(Expr proof){
00178       return d_quantLevel;
00179       /*
00180       if( ! proof.isNull()){
00181   //  std::cout << "debug level " << proof << std::endl;;
00182       }
00183       else {
00184   //  std::cout << "proof null" << proof << std::endl;;
00185       }
00186       
00187       unsigned nch = proof.arity();
00188       unsigned level(0);
00189       if (proof.getKind() == PF_APPLY){
00190   for (unsigned i = 1 ; i < nch ; i++){
00191     if ((proof[i]).getKind() == PF_APPLY || proof[i].getKind() == LAMBDA || proof[i].isVar()) {
00192       if(proof[i].isVar()){
00193         //        std::cout << "found var in pf # " << proof << std::endl;
00194       }
00195       unsigned chLevel = recQuantLevel(proof[i]);
00196       level =  chLevel > level ? chLevel : level ;
00197     }
00198   }
00199   if(proof[0].getName() == "universal_elimination"){
00200     level++;
00201     unsigned gtermLevel = myvcl->core()->getQuantLevelForTerm(proof[4]);
00202     if((gtermLevel + 1) > level ){
00203       level = gtermLevel+1;
00204     }
00205     //    std::cout << "level " << level << std::endl;
00206   }
00207   else {
00208     //    std::cout << "proof name non-inst" << proof[0].getName() << std::endl;
00209   }
00210   //  std::cout << "get level " << d_thm << std::endl;
00211   //  std::cout << "get level " << level << std::endl;
00212   //  std::cout << "get level " << proof << std::endl;
00213   return level;      
00214       }
00215       else if (proof.getKind() ==  LAMBDA){
00216   std::cout << "lambda " << proof << std::endl;
00217   std::cout << "lambda body " << proof << std::endl;
00218   return recQuantLevel(proof.getBody());
00219       }
00220       else if (proof.isNull() ){
00221   //  std::cout <<" error in get quantleveldebug " << std::endl;
00222   //  std::cout << proof << std::endl;
00223   return 100000;
00224       } 
00225       else if (proof.isVar()){
00226   if(proof.getType().getExpr().getType().isBool()){
00227     //std::cout << "var proof " << proof.getType().getExpr() << std::endl;
00228   //  std::cout << "found proof var # " << proof << std::endl;
00229   //  std::cout << proof.getType() << std::endl;
00230   //  std::cout << "the quant level is " <<   myvcl->core()->getQuantLevelForTerm(proof.getType().getExpr()) << std::endl;
00231     return myvcl->core()->getQuantLevelForTerm(proof.getType().getExpr());
00232   }
00233   else{
00234     return 0;
00235   }
00236       }
00237       else{
00238   std::cout <<" error in get quantleveldebug " << std::endl;
00239   std::cout << proof << std::endl;
00240   std::cout << proof.isVar() << std::endl;
00241   return 200000;
00242       }
00243       return 0;
00244       */
00245     }
00246 
00247     unsigned findQuantLevelDebug(){
00248       return d_quantLevel;
00249       /*
00250       Expr p (d_proof.getExpr());
00251       unsigned ret ; 
00252       if (isAssump()){  
00253   if(d_thm.inUserAssumption()){
00254     ret = 0 ;
00255     //    return 0;
00256   }
00257   else {
00258     //    std::cout <<" why here " << std::endl;
00259     //    std::cout << "the quant level is " <<   myvcl->core()->getQuantLevelForTerm(d_thm) << std::endl;
00260     //    std::cout << d_thm << std::endl;
00261     //    std::cout <<" == end of  why here " << std::endl;
00262     ret =  myvcl->core()->getQuantLevelForTerm(d_thm);
00263     //    
00264     //    return myvcl->core()->getQuantLevelForTerm(d_thm);
00265   }
00266       }
00267       else if (p.isVar()){
00268   unsigned level1 =  myvcl->core()->getQuantLevelForTerm(p.getType().getExpr());
00269   unsigned level2 = d_quantLevel;
00270   if(level1 != level2){
00271     std::cout <<"not rq" << std::endl;
00272   }
00273   else{
00274     ret = level1;
00275     //    return level1;
00276   }
00277       }
00278       else {
00279   ret = recQuantLevel(p);
00280   //  return recQuantLevel(p);
00281       }
00282       //      std::cout << " get -- begin with debug level " << ret << std::endl;
00283       //      std::cout << " quant level " << d_quantLevel << std::endl;
00284       //      std::cout << " get level thm " << d_thm << std::endl;
00285       //      std::cout << " get level is var " << p.isVar() << std::endl;
00286       if(p.isVar()){
00287   //  std::cout << "var proof " << p.getType().getExpr()<< std::endl;
00288       }
00289       return ret;
00290       */
00291     }
00292     
00293 
00294 //     virtual bool isRewrite() const { return d_thm.isEq() || d_thm.isIff(); }
00295     virtual bool isRewrite() const { return false; }
00296 
00297     virtual const Expr& getExpr() const { return d_thm; }
00298     virtual const Expr& getLHS() const {
00299       //      TRACE("getExpr","TheoremValue::getLHS called (",d_thm,")");
00300       DebugAssert(isRewrite(),
00301       "TheoremValue::getLHS() called on non-rewrite theorem:\n"
00302       +toString());
00303       return d_thm[0];
00304     }
00305     virtual const Expr& getRHS() const {
00306       //      TRACE("getExpr","TheoremValue::getRHS called (",d_thm,")");
00307       DebugAssert(isRewrite(),
00308       "TheoremValue::getRHS() called on non-rewrite theorem:\n"
00309       +toString());
00310       return d_thm[1];
00311     }
00312 
00313     virtual const Assumptions& getAssumptionsRef() const = 0;
00314 
00315     bool isAssump() const { return d_isAssump; }
00316     const Proof& getProof() { return d_proof; }
00317 
00318   public:
00319     // Destructor
00320     virtual ~TheoremValue() { 
00321       IF_DEBUG(FatalAssert(d_refcount == 0,
00322                            "Thm::TheoremValue::~TheoremValue(): refcount != 0.");)
00323     }
00324 
00325     std::string toString() const {
00326       return getAssumptionsRef().toString() + " |- " + getExpr().toString();
00327     }
00328 
00329     // Memory management
00330     virtual MemoryManager* getMM() = 0;
00331 
00332   }; // end of class TheoremValue
00333 
00334 ///////////////////////////////////////////////////////////////////////////////
00335 //                                                                           //
00336 // Class: RegTheoremValue                                                    //
00337 // Author: Clark Barrett                                                     //
00338 // Created: Fri May  2 12:51:55 2003                                         //
00339 // Description: A special subclass for non-rewrite theorems.  Assumptions are//
00340 //              embedded in the object for easy reference.                   //
00341 //                                                                           //
00342 ///////////////////////////////////////////////////////////////////////////////
00343   class RegTheoremValue :public TheoremValue
00344   {
00345     friend class Theorem;
00346 
00347   protected:
00348     //! The assumptions for the theorem
00349     Assumptions d_assump;
00350 
00351 
00352   private:
00353     // Constructor.   NOTE: it is private; only friend classes can call it.
00354     RegTheoremValue(TheoremManager* tm, const Expr& thm,
00355                     const Assumptions& assump, const Proof& pf, bool isAssump,
00356                     int scope = -1)
00357       : TheoremValue(tm, thm, pf, isAssump), d_assump(assump)
00358     {
00359       DebugAssert(d_tm->isActive(), "TheoremValue()");
00360       if (isAssump) {
00361         DebugAssert(assump.empty(), "Expected empty assumptions");
00362         // refcount tricks are because a loop is created with Assumptions
00363         d_refcount = 1;
00364         {
00365           Theorem t(this);
00366           d_assump.add1(t);
00367         }
00368         d_refcount = 0;
00369         if (scope == -1) d_scopeLevel = tm->getCM()->scopeLevel();
00370         else d_scopeLevel = scope;
00371   //  TRACE("quantlevel", d_quantLevel, " theorem init assump", thm.toString()); 
00372       }
00373       else {
00374         if (!d_assump.empty()) {
00375           const Assumptions::iterator iend = d_assump.end();
00376           for (Assumptions::iterator i = d_assump.begin(); 
00377                i != iend; ++i) {
00378             if (i->getScope() > d_scopeLevel)
00379               d_scopeLevel = i->getScope();
00380             if (i->getQuantLevel() > d_quantLevel){
00381               d_quantLevel = i->getQuantLevel();
00382       }
00383           }
00384     //    TRACE("quantlevel", d_quantLevel, " theorem non-null assump", thm.toString()); 
00385         }
00386   else{
00387     TRACE("quantlevel","empty assumptions found ", thm , "");
00388   }
00389       }
00390       //yeting, let me check d_quantleveldebug here
00391       //      d_quantLevelDebug = findQuantLevelDebug();
00392       
00393     }
00394 
00395   public:
00396     // Destructor
00397     ~RegTheoremValue() {
00398       if (d_isAssump) {
00399         IF_DEBUG(FatalAssert(d_assump.size() == 1, "Expected size 1");)
00400         IF_DEBUG(FatalAssert(d_assump.getFirst().thm() == this, "Expected loop");)
00401         d_assump.getFirst().d_thm = 0;
00402       }
00403     }
00404 
00405     const Assumptions& getAssumptionsRef() const { return d_assump; }
00406 
00407     // Memory management
00408     MemoryManager* getMM() { return d_tm->getMM(); }
00409 
00410     void* operator new(size_t size, MemoryManager* mm) {
00411       return mm->newData(size);
00412     }
00413     void operator delete(void* pMem, MemoryManager* mm) {
00414       mm->deleteData(pMem);
00415     }
00416 
00417     void operator delete(void* d) { }
00418 
00419   }; // end of class RegTheoremValue
00420 
00421 ///////////////////////////////////////////////////////////////////////////////
00422 //                                                                           //
00423 // Class: RWTheoremValue                                                     //
00424 // Author: Clark Barrett                                                     //
00425 // Created: Fri May  2 12:51:55 2003                                         //
00426 // Description: A special subclass for theorems of the form A |- t=t' or     //
00427 //              A |- phi iff phi'.  The actual Expr is only created on       //
00428 //              demand.  The idea is that getLHS and getRHS should be used   //
00429 //              whenever possible, avoiding creating unnecessary Expr's.     //
00430 //                                                                           //
00431 ///////////////////////////////////////////////////////////////////////////////
00432   class RWTheoremValue :public TheoremValue
00433   {
00434     friend class Theorem;
00435 
00436   protected:
00437     // d_thm in the base class contains the full expression, which is
00438     // only constructed on demand.
00439     Expr d_lhs;
00440     Expr d_rhs;
00441     Assumptions* d_assump;
00442 
00443   private:
00444     void init(const Assumptions& assump, int scope)
00445     {
00446       DebugAssert(d_tm->isActive(), "TheoremValue()");
00447       if (d_isAssump) {
00448         DebugAssert(assump.empty(), "Expected empty assumptions");
00449         // refcount tricks are because a loop is created with Assumptions
00450         d_refcount = 1;
00451         {
00452           Theorem t(this);
00453           d_assump = new Assumptions(t);
00454         }
00455         d_refcount = 0;
00456         if (scope == -1) d_scopeLevel = d_tm->getCM()->scopeLevel();
00457         else d_scopeLevel = scope;
00458   //  TRACE("quantlevel", d_quantLevel, " RW theorem init is assump ", d_thm.toString());      
00459       }
00460       else {
00461         if (!assump.empty()) {
00462           d_assump = new Assumptions(assump);
00463           const Assumptions::iterator iend = assump.end();
00464           for (Assumptions::iterator i = assump.begin(); 
00465                i != iend; ++i) {
00466             if (i->getScope() > d_scopeLevel)
00467               d_scopeLevel = i->getScope();
00468             if (i->getQuantLevel() > d_quantLevel){
00469               d_quantLevel = i->getQuantLevel();
00470         //        TRACE("quantlevel", d_quantLevel, "=========\n RW theorem init has non-null assump ", this->toString());                
00471       }
00472           }
00473     //    TRACE("quantlevel", d_quantLevel, " RW theorem init has non-null assump ", d_thm.toString());         
00474         }
00475   else{
00476     TRACE("quantlevel", "RW empty assup found lhs  << " , d_lhs, "" );  
00477     TRACE("quantlevel", "RW empty assup found rhs  >> " , d_rhs, "" );  
00478   }
00479   //  TRACE("quantlevel", d_quantLevel, " RW theorem init has null assump ", d_thm.toString());         
00480       }
00481 
00482       //      d_quantLevelDebug = findQuantLevelDebug();
00483 
00484     }
00485     
00486     // Constructor.   NOTE: it is private; only friend classes can call it.
00487     RWTheoremValue(TheoremManager* tm, const Expr& lhs, const Expr& rhs,
00488        const Assumptions& assump, const Proof& pf, bool isAssump,
00489                    int scope = -1)
00490       : TheoremValue(tm, Expr(), pf, isAssump), d_lhs(lhs), d_rhs(rhs), d_assump(NULL)
00491     { init(assump, scope); }
00492 
00493     // Sometimes we have the full expression already created
00494     RWTheoremValue(TheoremManager* tm, const Expr& thm,
00495                    const Assumptions& assump, const Proof& pf, bool isAssump,
00496                    int scope = -1)
00497       : TheoremValue(tm, thm, pf, isAssump), d_lhs(thm[0]), d_rhs(thm[1]), d_assump(NULL)
00498     { init(assump, scope); }
00499 
00500     const Expr& getExpr() const {
00501       if (d_thm.isNull()) {
00502   bool isBool = d_lhs.getType().isBool();
00503   // have to fake out the const qualifier
00504   Expr* pexpr = const_cast<Expr*>(&d_thm);
00505   *pexpr = isBool ? d_lhs.iffExpr(d_rhs) : d_lhs.eqExpr(d_rhs);
00506   //  TRACE("getExpr", "getExpr called on RWTheorem (", d_thm, ")");
00507       }
00508       return d_thm;
00509     }
00510 
00511     const Expr& getLHS() const { return d_lhs; }
00512     const Expr& getRHS() const { return d_rhs; }
00513 
00514   public:
00515     // Destructor
00516     ~RWTheoremValue() {
00517       if (d_isAssump) {
00518         IF_DEBUG(FatalAssert(d_assump && d_assump->size() == 1, "Expected size 1");)
00519         IF_DEBUG(FatalAssert(d_assump->getFirst().thm() == this, "Expected loop");)
00520         d_assump->getFirst().d_thm = 0;
00521       }
00522       if (d_assump) delete d_assump;
00523     }
00524 
00525     bool isRewrite() const { return true; }
00526     const Assumptions& getAssumptionsRef() const {
00527       if (d_assump) return *d_assump;
00528       else return Assumptions::emptyAssump();
00529     }
00530 
00531     // Memory management
00532     MemoryManager* getMM() { return d_tm->getRWMM(); }
00533 
00534     void* operator new(size_t size, MemoryManager* mm) {
00535       return mm->newData(size);
00536     }
00537     void operator delete(void* pMem, MemoryManager* mm) {
00538       mm->deleteData(pMem);
00539     }
00540 
00541     void operator delete(void* d) { }
00542 
00543   }; // end of class RWTheoremValue
00544 
00545 } // end of namespace CVC3
00546 
00547 #endif