CVC3

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