CVC3  2.4.1
theorem_producer.h
Go to the documentation of this file.
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 
92 
93  protected:
96 
97  // Command-line option whether to check for soundness
98  const bool* d_checkProofs;
99  // Operator for creating proof terms
101  // Expr for filling in "condition" arguments in flea proofs
103 
104  // Make it possible for the subclasses to create theorems directly.
105 
106  //! Create a new theorem. See also newRWTheorem() and newReflTheorem()
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
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
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 
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 
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
155  // Destructor
156  virtual ~TheoremProducer() { }
157 
158  //! Testing whether to generate proofs
159  bool withProof() { return d_tm->withProof(); }
160 
161  //! Testing whether to generate assumptions
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