theorem_producer.h

Go to the documentation of this file.
00001 /*****************************************************************************/
00002 /*!
00003  * \file theorem_producer.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_Producer
00021 //
00022 // AUTHOR: Sergey Berezin, 07/05/02
00023 //
00024 // Abstract:
00025 //
00026 // This class is the only one that can create new Theorem classes.
00027 //
00028 // Only TRUSTED code can use it; a symbol _CVC3_TRUSTED_ must be
00029 // defined in *.cpp file before including this one; otherwise you'll
00030 // get a compiler warning.  Custom header files (*.h) which include
00031 // this file should NOT define _CVC3_TRUSTED_.  This practice enforces
00032 // the programmer to be aware of which part of his/her code is
00033 // trusted.
00034 //
00035 // It defines a protected NON-virtual method newTheorem() so that any
00036 // subclass can create a new Theorem.  This means that no untrusted
00037 // decision procedure's code should see this interface.
00038 // Unfortunately, this has to be a coding policy rather than something
00039 // we can enforce by C++ class structure.
00040 //
00041 // The intended use of this class is to make a subclass and define new
00042 // methods corresponding to proof rules (they take theorems and
00043 // generate new theorems).  Each decision procedure should have such a
00044 // subclass for its trusted core.  Each new proof rule must be sound;
00045 // that is, each new theorem that it generates must logically follow
00046 // from the theorems in the arguments, or the new theorem must be a
00047 // tautology.
00048 //
00049 // Each such subclass must also inherit from a decision
00050 // procedure-specific abstract interface which declares the new
00051 // methods (other than newTheorem). The decision procedure should only
00052 // use the new abstract interface.  Thus, the DP will not even see
00053 // newTheorem() method.
00054 //
00055 // This way the untrusted part of the code will not be able to create
00056 // an unsound theorem.
00057 //
00058 // Proof rules may expect theorems in the arguments be of a certain
00059 // form; if the expectations are not met, the right thing to do is to
00060 // fail in DebugAssert with the appropriate message.  In other words,
00061 // it is a coding bug to pass wrong theorems to the wrong rules.
00062 //
00063 // It is also a bug if a wrong theorem is passed but not detected by
00064 // the proof rule, unless such checks are explicitly turned off
00065 // globally for efficiency.
00066 ////////////////////////////////////////////////////////////////////////
00067 
00068 #ifndef _CVC3_TRUSTED_
00069 #warning "This file should be included only by TRUSTED code.  Define _CVC3_TRUSTED_ before including this file."
00070 #endif
00071 
00072 #ifndef _cvc3__theorem_producer_h_
00073 #define _cvc3__theorem_producer_h_
00074 
00075 #include "assumptions.h"
00076 #include "theorem_manager.h"
00077 #include "exception.h"
00078 
00079 // Macro to check for soundness.  It should only be executed within a
00080 // TheoremProducer class, and only if the -check-proofs option is set.
00081 // When its 'cond' is violated, it will call a function which will
00082 // eventually throw a soundness exception.
00083 #define CHECK_SOUND(cond, msg) { if(!(cond)) \
00084  soundError(__FILE__, __LINE__, #cond, msg); }
00085 
00086 // Flag whether to check soundness or not
00087 #define CHECK_PROOFS *d_checkProofs
00088 
00089 namespace CVC3 {
00090 
00091   class TheoremProducer {
00092 
00093   protected:
00094     TheoremManager* d_tm;
00095     ExprManager* d_em;
00096 
00097     // Command-line option whether to check for soundness
00098     const bool* d_checkProofs;
00099     // Operator for creating proof terms
00100     Op d_pfOp;
00101     // Expr for filling in "condition" arguments in flea proofs
00102     Expr d_hole;
00103 
00104     // Make it possible for the subclasses to create theorems directly.
00105 
00106     //! Create a new theorem.  See also newRWTheorem() and newReflTheorem()
00107     Theorem newTheorem(const Expr& thm,
00108            const Assumptions& assump,
00109            const Proof& pf) {
00110       IF_DEBUG(if(!thm.isEq() && !thm.isIff()) {
00111   TRACE("newTheorem", "newTheorem(", thm, ")");
00112   debugger.counter("newTheorem() called on equality")++;
00113       })
00114       return Theorem(d_tm, thm, assump, pf);
00115     }
00116 
00117     //! Create a rewrite theorem: lhs = rhs
00118     Theorem newRWTheorem(const Expr& lhs, const Expr& rhs,
00119        const Assumptions& assump,
00120        const Proof& pf) {
00121       return Theorem(d_tm, lhs, rhs, assump, pf);
00122     }
00123 
00124     //! Create a reflexivity theorem
00125     Theorem newReflTheorem(const Expr& e) {
00126       return Theorem(e);
00127     }
00128 
00129     Theorem newAssumption(const Expr& thm, const Proof& pf, int scope = -1) {
00130       return Theorem(d_tm, thm, Assumptions::emptyAssump(), pf, true, scope);
00131     }
00132 
00133     Theorem3 newTheorem3(const Expr& thm,
00134        const Assumptions& assump,
00135        const Proof& pf) {
00136       IF_DEBUG(if(!thm.isEq() && !thm.isIff()) {
00137   TRACE("newTheorem", "newTheorem3(", thm, ")");
00138   debugger.counter("newTheorem3() called on equality")++;
00139       })
00140       return Theorem3(d_tm, thm, assump, pf);
00141     }
00142 
00143     Theorem3 newRWTheorem3(const Expr& lhs, const Expr& rhs,
00144          const Assumptions& assump,
00145          const Proof& pf) {
00146       return Theorem3(d_tm, lhs, rhs, assump, pf);
00147     }
00148 
00149     void soundError(const std::string& file, int line,
00150         const std::string& cond, const std::string& msg);
00151 
00152   public:
00153     // Constructor
00154     TheoremProducer(TheoremManager *tm);
00155     // Destructor
00156     virtual ~TheoremProducer() { }
00157 
00158     //! Testing whether to generate proofs
00159     bool withProof() { return d_tm->withProof(); }
00160 
00161     //! Testing whether to generate assumptions
00162     bool withAssumptions() { return d_tm->withAssumptions(); }
00163 
00164     //! Create a new proof label (bound variable) for an assumption (formula)
00165     Proof newLabel(const Expr& e);
00166 
00167     //////////////////////////////////////////////////////////////////
00168     // Functions to create proof terms
00169     //////////////////////////////////////////////////////////////////
00170 
00171     // Apply a rule named 'name' to its arguments, Proofs or Exprs
00172     Proof newPf(const std::string& name);
00173     Proof newPf(const std::string& name, const Expr& e);
00174     Proof newPf(const std::string& name, const Proof& pf);
00175     Proof newPf(const std::string& name, const Expr& e1, const Expr& e2);
00176     Proof newPf(const std::string& name, const Expr& e, const Proof& pf);
00177     Proof newPf(const std::string& name, const Expr& e1,
00178     const Expr& e2, const Expr& e3);
00179     Proof newPf(const std::string& name, const Expr& e1,
00180     const Expr& e2, const Proof& pf);
00181 
00182     // Methods with iterators.
00183 
00184     // Iterators are preferred to vectors, since they are often
00185     // efficient
00186 
00187     Proof newPf(const std::string& name,
00188     Expr::iterator begin, const Expr::iterator &end);
00189     Proof newPf(const std::string& name, const Expr& e,
00190     Expr::iterator begin, const Expr::iterator &end);
00191     Proof newPf(const std::string& name,
00192     Expr::iterator begin, const Expr::iterator &end,
00193     const std::vector<Proof>& pfs);
00194 
00195     // Methods with vectors.
00196     Proof newPf(const std::string& name, const std::vector<Expr>& args);
00197     Proof newPf(const std::string& name, const Expr& e,
00198     const std::vector<Expr>& args);
00199     Proof newPf(const std::string& name, const Expr& e,
00200     const std::vector<Proof>& pfs);
00201     Proof newPf(const std::string& name, const Expr& e1, const Expr& e2,
00202     const std::vector<Proof>& pfs);
00203     Proof newPf(const std::string& name, const std::vector<Proof>& pfs);
00204     Proof newPf(const std::string& name, const std::vector<Expr>& args,
00205     const Proof& pf);
00206     Proof newPf(const std::string& name, const std::vector<Expr>& args,
00207     const std::vector<Proof>& pfs);
00208 
00209     //! Creating LAMBDA-abstraction (LAMBDA label formula proof)
00210     /*! The label must be a variable with a formula as a type, and
00211      * matching the given "frm". */
00212     Proof newPf(const Proof& label, const Expr& frm, const Proof& pf);
00213 
00214     //! Creating LAMBDA-abstraction (LAMBDA label proof).
00215     /*! The label must be a variable with a formula as a type. */
00216     Proof newPf(const Proof& label, const Proof& pf);
00217 
00218     /*! @brief Similarly, multi-argument lambda-abstractions:
00219      * (LAMBDA (u1,...,un): (f1,...,fn). pf) */
00220     Proof newPf(const std::vector<Proof>& labels,
00221     const std::vector<Expr>& frms,
00222     const Proof& pf);
00223 
00224     Proof newPf(const std::vector<Proof>& labels,
00225     const Proof& pf);
00226 
00227   }; // end of Theorem_Producer class
00228 
00229 }  // end of namespace CVC3
00230 #endif

Generated on Wed Nov 18 16:13:31 2009 for CVC3 by  doxygen 1.5.2