1 /*****************************************************************************/ 2 /*! 3 * \file theorem_producer.h 4 * 5 * Author: Sergey Berezin 6 * 7 * Created: Dec 10 00:37:49 GMT 2002 8 * 9 * <hr> 10 * 11 * License to use, copy, modify, sell and/or distribute this software 12 * and its documentation for any purpose is hereby granted without 13 * royalty, subject to the terms and conditions defined in the \ref 14 * LICENSE file provided with this distribution. 15 * 16 * <hr> 17 * 18 */ 19 /*****************************************************************************/ 20 // CLASS: Theorem_Producer 21 // 22 // AUTHOR: Sergey Berezin, 07/05/02 23 // 24 // Abstract: 25 // 26 // This class is the only one that can create new Theorem classes. 27 // 28 // Only TRUSTED code can use it; a symbol _CVC3_TRUSTED_ must be 29 // defined in *.cpp file before including this one; otherwise you'll 30 // get a compiler warning. Custom header files (*.h) which include 31 // this file should NOT define _CVC3_TRUSTED_. This practice enforces 32 // the programmer to be aware of which part of his/her code is 33 // trusted. 34 // 35 // It defines a protected NON-virtual method newTheorem() so that any 36 // subclass can create a new Theorem. This means that no untrusted 37 // decision procedure's code should see this interface. 38 // Unfortunately, this has to be a coding policy rather than something 39 // we can enforce by C++ class structure. 40 // 41 // The intended use of this class is to make a subclass and define new 42 // methods corresponding to proof rules (they take theorems and 43 // generate new theorems). Each decision procedure should have such a 44 // subclass for its trusted core. Each new proof rule must be sound; 45 // that is, each new theorem that it generates must logically follow 46 // from the theorems in the arguments, or the new theorem must be a 47 // tautology. 48 // 49 // Each such subclass must also inherit from a decision 50 // procedure-specific abstract interface which declares the new 51 // methods (other than newTheorem). The decision procedure should only 52 // use the new abstract interface. Thus, the DP will not even see 53 // newTheorem() method. 54 // 55 // This way the untrusted part of the code will not be able to create 56 // an unsound theorem. 57 // 58 // Proof rules may expect theorems in the arguments be of a certain 59 // form; if the expectations are not met, the right thing to do is to 60 // fail in DebugAssert with the appropriate message. In other words, 61 // it is a coding bug to pass wrong theorems to the wrong rules. 62 // 63 // It is also a bug if a wrong theorem is passed but not detected by 64 // the proof rule, unless such checks are explicitly turned off 65 // globally for efficiency. 66 //////////////////////////////////////////////////////////////////////// 67 68 #ifndef _CVC3_TRUSTED_ 69 #warning "This file should be included only by TRUSTED code. Define _CVC3_TRUSTED_ before including this file." 70 #endif 71 72 #ifndef _cvc3__theorem_producer_h_ 73 #define _cvc3__theorem_producer_h_ 74 75 #include "assumptions.h" 76 #include "theorem_manager.h" 77 #include "exception.h" 78 79 // Macro to check for soundness. It should only be executed within a 80 // TheoremProducer class, and only if the -check-proofs option is set. 81 // When its 'cond' is violated, it will call a function which will 82 // eventually throw a soundness exception. 83 #define CHECK_SOUND(cond, msg) { if(!(cond)) \ 84 soundError(__FILE__, __LINE__, #cond, msg); } 85 86 // Flag whether to check soundness or not 87 #define CHECK_PROOFS *d_checkProofs 88 89 namespace CVC3 { 90 91 class TheoremProducer { 92 93 protected: 94 TheoremManager* d_tm; 95 ExprManager* d_em; 96 97 // Command-line option whether to check for soundness 98 const bool* d_checkProofs; 99 // Operator for creating proof terms 100 Op d_pfOp; 101 // Expr for filling in "condition" arguments in flea proofs 102 Expr d_hole; 103 104 // Make it possible for the subclasses to create theorems directly. 105 106 //! Create a new theorem. See also newRWTheorem() and newReflTheorem() newTheorem(const Expr & thm,const Assumptions & assump,const Proof & pf)107 Theorem newTheorem(const Expr& thm, 108 const Assumptions& assump, 109 const Proof& pf) { 110 IF_DEBUG(if(!thm.isEq() && !thm.isIff()) { 111 TRACE("newTheorem", "newTheorem(", thm, ")"); 112 debugger.counter("newTheorem() called on equality")++; 113 }) 114 return Theorem(d_tm, thm, assump, pf); 115 } 116 117 //! Create a rewrite theorem: lhs = rhs newRWTheorem(const Expr & lhs,const Expr & rhs,const Assumptions & assump,const Proof & pf)118 Theorem newRWTheorem(const Expr& lhs, const Expr& rhs, 119 const Assumptions& assump, 120 const Proof& pf) { 121 return Theorem(d_tm, lhs, rhs, assump, pf); 122 } 123 124 //! Create a reflexivity theorem newReflTheorem(const Expr & e)125 Theorem newReflTheorem(const Expr& e) { 126 return Theorem(e); 127 } 128 129 Theorem newAssumption(const Expr& thm, const Proof& pf, int scope = -1) { 130 return Theorem(d_tm, thm, Assumptions::emptyAssump(), pf, true, scope); 131 } 132 newTheorem3(const Expr & thm,const Assumptions & assump,const Proof & pf)133 Theorem3 newTheorem3(const Expr& thm, 134 const Assumptions& assump, 135 const Proof& pf) { 136 IF_DEBUG(if(!thm.isEq() && !thm.isIff()) { 137 TRACE("newTheorem", "newTheorem3(", thm, ")"); 138 debugger.counter("newTheorem3() called on equality")++; 139 }) 140 return Theorem3(d_tm, thm, assump, pf); 141 } 142 newRWTheorem3(const Expr & lhs,const Expr & rhs,const Assumptions & assump,const Proof & pf)143 Theorem3 newRWTheorem3(const Expr& lhs, const Expr& rhs, 144 const Assumptions& assump, 145 const Proof& pf) { 146 return Theorem3(d_tm, lhs, rhs, assump, pf); 147 } 148 149 void soundError(const std::string& file, int line, 150 const std::string& cond, const std::string& msg); 151 152 public: 153 // Constructor 154 TheoremProducer(TheoremManager *tm); 155 // Destructor ~TheoremProducer()156 virtual ~TheoremProducer() { } 157 158 //! Testing whether to generate proofs withProof()159 bool withProof() { return d_tm->withProof(); } 160 161 //! Testing whether to generate assumptions withAssumptions()162 bool withAssumptions() { return d_tm->withAssumptions(); } 163 164 //! Create a new proof label (bound variable) for an assumption (formula) 165 Proof newLabel(const Expr& e); 166 167 ////////////////////////////////////////////////////////////////// 168 // Functions to create proof terms 169 ////////////////////////////////////////////////////////////////// 170 171 // Apply a rule named 'name' to its arguments, Proofs or Exprs 172 Proof newPf(const std::string& name); 173 Proof newPf(const std::string& name, const Expr& e); 174 Proof newPf(const std::string& name, const Proof& pf); 175 Proof newPf(const std::string& name, const Expr& e1, const Expr& e2); 176 Proof newPf(const std::string& name, const Expr& e, const Proof& pf); 177 Proof newPf(const std::string& name, const Expr& e1, 178 const Expr& e2, const Expr& e3); 179 Proof newPf(const std::string& name, const Expr& e1, 180 const Expr& e2, const Proof& pf); 181 182 // Methods with iterators. 183 184 // Iterators are preferred to vectors, since they are often 185 // efficient 186 187 Proof newPf(const std::string& name, 188 Expr::iterator begin, const Expr::iterator &end); 189 Proof newPf(const std::string& name, const Expr& e, 190 Expr::iterator begin, const Expr::iterator &end); 191 Proof newPf(const std::string& name, 192 Expr::iterator begin, const Expr::iterator &end, 193 const std::vector<Proof>& pfs); 194 195 // Methods with vectors. 196 Proof newPf(const std::string& name, const std::vector<Expr>& args); 197 Proof newPf(const std::string& name, const Expr& e, 198 const std::vector<Expr>& args); 199 Proof newPf(const std::string& name, const Expr& e, 200 const std::vector<Proof>& pfs); 201 Proof newPf(const std::string& name, const Expr& e1, const Expr& e2, 202 const std::vector<Proof>& pfs); 203 Proof newPf(const std::string& name, const std::vector<Proof>& pfs); 204 Proof newPf(const std::string& name, const std::vector<Expr>& args, 205 const Proof& pf); 206 Proof newPf(const std::string& name, const std::vector<Expr>& args, 207 const std::vector<Proof>& pfs); 208 209 //! Creating LAMBDA-abstraction (LAMBDA label formula proof) 210 /*! The label must be a variable with a formula as a type, and 211 * matching the given "frm". */ 212 Proof newPf(const Proof& label, const Expr& frm, const Proof& pf); 213 214 //! Creating LAMBDA-abstraction (LAMBDA label proof). 215 /*! The label must be a variable with a formula as a type. */ 216 Proof newPf(const Proof& label, const Proof& pf); 217 218 /*! @brief Similarly, multi-argument lambda-abstractions: 219 * (LAMBDA (u1,...,un): (f1,...,fn). pf) */ 220 Proof newPf(const std::vector<Proof>& labels, 221 const std::vector<Expr>& frms, 222 const Proof& pf); 223 224 Proof newPf(const std::vector<Proof>& labels, 225 const Proof& pf); 226 227 }; // end of Theorem_Producer class 228 229 } // end of namespace CVC3 230 #endif 231