theorem.h

Go to the documentation of this file.
00001 /*****************************************************************************/
00002 /*!
00003  * \file theorem.h
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 // Abstract:
00025 //
00026 // A class representing a proven fact in CVC.  It stores the theorem
00027 // as a CVC expression, and in the proof prodicing mode also its
00028 // 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.h file should be used by the decision procedures that
00041 // use Theorem.
00042 //
00043 ////////////////////////////////////////////////////////////////////////
00044 
00045 // expr.h Has to be included outside of #ifndef, since it sources us
00046 // recursively (read comments in expr_value.h).
00047 #ifndef _cvc3__expr_h_
00048 #include "expr.h"
00049 #endif
00050 
00051 #ifndef _cvc3__theorem_h_
00052 #define _cvc3__theorem_h_
00053 
00054 #include "os.h"
00055 #include "proof.h"
00056 #include "assumptions.h"
00057 
00058 namespace CVC3 {
00059 
00060   // Declare the data holding classes but hide the definitions
00061   class TheoremManager;
00062   class TheoremValue;
00063   class Assumptions;
00064 
00065   // Theorem is basically a wrapper around a pointer to a
00066   // TheoremValue, so that we can pass this class around by value.
00067   // All the constructors of this class are private, so do not inherit
00068   // from it and do not try to create a value directly.  Only
00069   // TheoremProducer can create new Theorem instances.
00070   //
00071   // Theorems, unlike expressions, are NOT made unique, and it is
00072   // possible to have the same theorem in different scopes with
00073   // different assumptions and proofs.  It is a deliberate feature,
00074   // since natural deduction sometimes requires proving the same
00075   // conclusion from different assumptions independently, e.g. in
00076   // disjunction elimination rule.
00077   class CVC_DLL Theorem {
00078   private:
00079     // Make a theorem producing class our friend.  No definition is
00080     // exposed here.
00081     friend class TheoremProducer;
00082     // Also allow our 3-valued cousin to create us
00083     friend class Theorem3;
00084     // Also TheoremValue classes for assumptions
00085     friend class RegTheoremValue;
00086     friend class RWTheoremValue;
00087 
00088     // Optimization: reflexivity theorems just store the exprValue pointer
00089     // directly.  Also, the lowest bit is set to 1 to indicate that its
00090     // a reflexivity theorem.  This really helps performance!
00091     union {
00092       intptr_t d_thm;
00093       ExprValue* d_expr;
00094     };
00095 
00096     //! Compare Theorems by their expressions.  Return -1, 0, or 1.
00097     friend int compare(const Theorem& t1, const Theorem& t2);
00098     //! Compare a Theorem with an Expr (as if Expr is a Theorem)
00099     friend int compare(const Theorem& t1, const Expr& e2);
00100     //! Compare Theorems by TheoremValue pointers.  Return -1, 0, or 1.
00101     friend int compareByPtr(const Theorem& t1, const Theorem& t2);
00102     //! Equality is w.r.t. compare()
00103     friend bool operator==(const Theorem& t1, const Theorem& t2) 
00104       { return (compare(t1, t2)==0); }
00105     //! Disequality is w.r.t. compare()
00106     friend bool operator!=(const Theorem& t1, const Theorem& t2)
00107       { return (compare(t1, t2) != 0); }
00108 
00109     //! Constructor only used by TheoremValue for assumptions
00110     Theorem(TheoremValue* thm) :d_thm(((intptr_t)thm) | 0x1) {}
00111 
00112     //! Constructor for a new theorem 
00113     Theorem(TheoremManager* tm, const Expr &thm, const Assumptions& assump,
00114             const Proof& pf, bool isAssump = false, int scope = -1);
00115 
00116     //! Constructor for rewrite theorems.
00117     /*! These use a special efficient subclass of TheoremValue for
00118      * theorems which represent rewrites: A |- t = t' or A |- phi<=>phi'
00119      */
00120     Theorem(TheoremManager* tm, const Expr& lhs, const Expr& rhs,
00121       const Assumptions& assump, const Proof& pf, bool isAssump = false,
00122             int scope = -1);
00123 
00124     //! Constructor for a reflexivity theorem: |-t=t or |-phi<=>phi
00125     Theorem(const Expr& e);
00126 
00127     void recursivePrint(int& i) const;
00128     void getAssumptionsRec(std::set<Expr>& assumptions) const;
00129 
00130     ExprValue* exprValue() const { return d_expr; }
00131     TheoremValue* thm() const { return (TheoremValue*)(d_thm & (~(0x1))); }
00132 
00133   public:
00134     // recusive function to print theorems and all assumptions recursively
00135     // important: this function will corrupt all flags!! so exercise 
00136     // caution when using in any graph traversals 
00137     // (probably more useful to call it only before a crash)
00138     void printDebug() const { 
00139       clearAllFlags();
00140       setCachedValue(0);
00141       setFlag();
00142       int i = 1; 
00143       recursivePrint(i);
00144     }
00145 
00146     // Default constructor creates Null theorem to allow untrusted
00147     // code declare local vars without initialization (vector<Theorem>
00148     // may need that, for instance).
00149     Theorem(): d_thm(0) { }
00150     // Copy constructor
00151     Theorem(const Theorem &th);
00152     // Assignment operator
00153     Theorem& operator=(const Theorem &th);
00154 
00155     // Destructor
00156     ~Theorem();
00157 
00158     // Test if we are running in a proof production mode and with assumptions
00159     bool withProof() const;
00160     bool withAssumptions() const;
00161 
00162     bool isNull() const { return d_thm == 0; }
00163 
00164     // True if theorem is of the form t=t' or phi iff phi'
00165     bool isRewrite() const;
00166     // True if theorem was created using assumpRule
00167     bool isAssump() const;
00168     // True if reflexivity theorem
00169     bool isRefl() const { return d_thm && !(d_thm & 0x1); }
00170     
00171     // Return the theorem value as an Expr
00172     Expr getExpr() const;
00173     const Expr& getLHS() const;
00174     const Expr& getRHS() const;
00175 
00176     // Return the assumptions.  a should be empty and uninitialized
00177     //    void getAssumptions(Assumptions& a) const;
00178     // Recurse to get actual assumptions
00179     void getLeafAssumptions(std::vector<Expr>& assumptions,
00180                             bool negate = false) const;
00181     const Assumptions& getAssumptionsRef() const;
00182     // Return the proof of the theorem.  If running without proofs,
00183     // return the Null proof.
00184     Proof getProof() const;
00185     // Return the lowest scope level at which this theorem is valid.
00186     // Value -1 means no information is available.
00187     int getScope() const;
00188     //! Return quantification level for this theorem
00189     unsigned getQuantLevel() const;
00190     //! Set the quantification level for this theorem
00191     void setQuantLevel(unsigned level);
00192 
00193     // hash
00194     size_t hash() const;
00195 
00196     // Printing
00197     std::string toString() const;
00198 
00199     // For debugging
00200     void printx() const;
00201     void printxnodag() const;
00202     void pprintx() const;
00203     void pprintxnodag() const;
00204     
00205     void print() const;
00206 
00207     /*! \name Methods for Theorem Attributes
00208      *
00209      * Several attributes used in conflict analysis and assumptions
00210      * graph traversals.
00211      * @{
00212      */
00213     //! Check if the flag attribute is set
00214     bool isFlagged() const;
00215     //! Clear the flag attribute in all the theorems
00216     void clearAllFlags() const;
00217     //! Set the flag attribute
00218     void setFlag() const;
00219 
00220     //! Set the "expand" attribute
00221     void setExpandFlag(bool val) const;
00222     //! Check the "expand" attribute
00223     bool getExpandFlag() const;
00224     //! Set the "literal" attribute
00225     /*! The expression of this theorem will be added as a conflict
00226      * clause literal */
00227     void setLitFlag(bool val) const;
00228     //! Check the "literal" attribute
00229     /*! The expression of this theorem will be added as a conflict
00230      * clause literal */
00231     bool getLitFlag() const;
00232     //! Check if the theorem is a literal
00233     bool isAbsLiteral() const;
00234 
00235     bool refutes(const Expr& e) const
00236     {
00237       return
00238   (e.isNot() && e[0] == getExpr()) ||
00239   (getExpr().isNot() && getExpr()[0] == e);
00240     }
00241 
00242     bool proves(const Expr& e) const
00243     {
00244       return getExpr() == e;
00245     }
00246 
00247     bool matches(const Expr& e) const
00248     {
00249       return proves(e) || refutes(e);
00250     }
00251 
00252     void setCachedValue(int value) const;
00253     int getCachedValue() const;
00254     
00255     /*!@}*/ // End of Attribute methods
00256 
00257     //! Printing a theorem to a stream, calling it "name".
00258     std::ostream& print(std::ostream& os, const std::string& name) const;
00259     
00260     friend std::ostream& operator<<(std::ostream& os, const Theorem& t) {
00261       return t.print(os, "Theorem");
00262     }
00263 
00264     static bool TheoremEq(const Theorem& t1, const Theorem& t2) 
00265     { 
00266       DebugAssert(!t1.isNull() && !t2.isNull(), 
00267                   "AssumptionsValue() Null Theorem passed to constructor");
00268       return t1 == t2;
00269     }
00270   };  // End of Theorem
00271 
00272 /*****************************************************************************/
00273 /*!
00274  *\class Theorem3
00275  *\brief Theorem3
00276  *
00277  * Author: Sergey Berezin
00278  *
00279  * Created: Tue Nov  4 17:57:07 2003
00280  *
00281  * Implements the 3-valued theorem used for the user assertions and
00282  * the result of query.  It is simply a wrapper around class Theorem,
00283  * but has a different semantic meaning: the formula may have partial
00284  * functions and has the Kleene's 3-valued interpretation.  The fact
00285  * that a Theorem3 value is derived means that the TCCs for the
00286  * formula and all of its assumptions are valid in the current
00287  * context, and the proofs of TCCs contribute to the set of
00288  * assumptions.
00289  */
00290 /*****************************************************************************/
00291   class Theorem3 {
00292   private:
00293     // Make a theorem producing class our friend.  No definition is
00294     // exposed here.
00295     friend class TheoremProducer;
00296 
00297     Theorem d_thm;
00298 
00299     friend bool operator==(const Theorem3& t1, const Theorem3& t2) {
00300       return t1.d_thm == t2.d_thm;
00301     }
00302     friend bool operator!=(const Theorem3& t1, const Theorem3& t2) {
00303       return t1.d_thm != t2.d_thm;
00304     }
00305 
00306 
00307     // Private constructors for a new theorem 
00308     Theorem3(TheoremManager* tm, const Expr &thm, const Assumptions& assump,
00309              const Proof& pf, bool isAssump = false, int scope = -1)
00310       : d_thm(tm, thm, assump, pf, isAssump, scope) { }
00311 
00312     // Constructors for rewrite theorems.  These use a special efficient
00313     // subclass of TheoremValue for theorems which represent rewrites:
00314     // A |- t = t' or A |- phi iff phi'
00315     Theorem3(TheoremManager* tm, const Expr& lhs, const Expr& rhs,
00316        const Assumptions& assump, const Proof& pf)
00317       : d_thm(tm, lhs, rhs, assump, pf) { }
00318 
00319   public:
00320     // recusive function to print theorems and all assumptions recursively
00321     // important: this function will corrupt all flags!! so exercise 
00322     // caution when using in any graph traversals 
00323     // (probably more useful to call it only before a crash)
00324     void printDebug() const { d_thm.printDebug(); }
00325 
00326     // Default constructor creates Null theorem to allow untrusted
00327     // code declare local vars without initialization (vector<Theorem>
00328     // may need that, for instance).
00329     Theorem3() { }
00330 
00331     // Destructor
00332     virtual ~Theorem3() { }
00333 
00334     bool isNull() const { return d_thm.isNull(); }
00335 
00336     // True if theorem is of the form t=t' or phi iff phi'
00337     bool isRewrite() const { return d_thm.isRewrite(); }
00338     bool isAssump() const { return d_thm.isAssump(); }
00339     
00340     // Return the theorem value as an Expr
00341     Expr getExpr() const { return d_thm.getExpr(); }
00342     const Expr& getLHS() const { return d_thm.getLHS(); }
00343     const Expr& getRHS() const { return d_thm.getRHS(); }
00344 
00345     // Return the assumptions.
00346     // It's an error if called while running without assumptions.
00347     //    void getAssumptions(Assumptions& a) const { d_thm.getAssumptions(a); }
00348     const Assumptions& getAssumptionsRef() const {
00349       return d_thm.getAssumptionsRef();
00350     }
00351     // Return the proof of the theorem.  If running without proofs,
00352     // return the Null proof.
00353     Proof getProof() const { return d_thm.getProof(); }
00354 
00355     // Return the lowest scope level at which this theorem is valid.
00356     // Value -1 means no information is available.
00357     int getScope() const { return d_thm.getScope(); }
00358 
00359     // Test if we are running in a proof production mode and with assumptions
00360     bool withProof() const { return d_thm.withProof(); }
00361     bool withAssumptions() const { return d_thm.withAssumptions(); }
00362 
00363     // Printing
00364     std::string toString() const;
00365 
00366     // For debugging
00367     void printx() const { d_thm.printx(); }
00368     void print() const { d_thm.print(); }
00369 
00370     //! Check if the theorem is a literal
00371     bool isAbsLiteral() const { return d_thm.isAbsLiteral(); }
00372 
00373     friend std::ostream& operator<<(std::ostream& os, const Theorem3& t) {
00374       return t.d_thm.print(os, "Theorem3");
00375     }
00376   };  // End of Theorem3
00377 
00378   //! "Less" comparator for theorems by TheoremValue pointers
00379   class TheoremLess {
00380   public:
00381     bool operator()(const Theorem& t1, const Theorem& t2) const {
00382       return (compareByPtr(t1, t2) < 0);
00383     }
00384   };
00385   typedef std::map<Theorem,bool, TheoremLess> TheoremMap;
00386 
00387   inline std::string Theorem::toString() const {
00388     std::ostringstream ss;
00389     ss << (*this);
00390     return ss.str();
00391   }
00392 
00393   inline std::string Theorem3::toString() const {
00394     std::ostringstream ss;
00395     ss << (*this);
00396     return ss.str();
00397   }
00398 
00399   // Merge assumptions from different theorems
00400 //   inline Assumptions merge(const Theorem& t1, const Theorem& t2) {
00401 //     return Assumptions(t1, t2);
00402 //   }
00403 //   inline void merge(Assumptions& a, const Theorem& t) {
00404 //     a.add(t);
00405 //   }
00406 //   inline Assumptions merge(const std::vector<Theorem>& t) {
00407 //     return Assumptions(t);
00408 //   }
00409 
00410   inline bool operator<(const Theorem& t1, const Theorem& t2)
00411     { return compare(t1, t2) < 0; }
00412   inline bool operator<=(const Theorem& t1, const Theorem& t2)
00413     { return compare(t1, t2) <= 0; }
00414   inline bool operator>(const Theorem& t1, const Theorem& t2)
00415     { return compare(t1, t2) > 0; }
00416   inline bool operator>=(const Theorem& t1, const Theorem& t2)
00417     { return compare(t1, t2) >= 0; }
00418 
00419 } // end of namespace CVC3
00420 
00421 #include "hash_fun.h"
00422 namespace Hash
00423 {
00424 
00425 template<> struct hash<CVC3::Theorem>
00426 {
00427   size_t operator()(const CVC3::Theorem& e) const { return e.hash(); }
00428 };
00429 
00430 }
00431 
00432 #endif

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