CVC3  2.4.1
theorem.h
Go to the documentation of this file.
1 /*****************************************************************************/
2 /*!
3  * \file theorem.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
21 //
22 // AUTHOR: Sergey Berezin, 07/05/02
23 //
24 // Abstract:
25 //
26 // A class representing a proven fact in CVC. It stores the theorem
27 // as a CVC expression, and in the proof prodicing mode also its
28 // proof.
29 //
30 // The idea is to allow only a few trusted classes to create values of
31 // this class. If all the critical computations in the decision
32 // procedures are done through the use of Theorems, then soundness of
33 // these decision procedures will rely only on the soundness of the
34 // methods in the trusted classes (the inference rules).
35 //
36 // Thus, proof checking can effectively be done at run-time on the
37 // fly. Or the soundness may be potentially proven by static analysis
38 // and many run-time checks can then be optimized away.
39 //
40 // This theorem.h file should be used by the decision procedures that
41 // use Theorem.
42 //
43 ////////////////////////////////////////////////////////////////////////
44 
45 // expr.h Has to be included outside of #ifndef, since it sources us
46 // recursively (read comments in expr_value.h).
47 #ifndef _cvc3__expr_h_
48 #include "expr.h"
49 #endif
50 
51 #ifndef _cvc3__theorem_h_
52 #define _cvc3__theorem_h_
53 
54 #include "os.h"
55 #include "proof.h"
56 
57 namespace CVC3 {
58 
59  // Declare the data holding classes but hide the definitions
60  class TheoremManager;
61  class TheoremValue;
62  class Assumptions;
63 
64  // Theorem is basically a wrapper around a pointer to a
65  // TheoremValue, so that we can pass this class around by value.
66  // All the constructors of this class are private, so do not inherit
67  // from it and do not try to create a value directly. Only
68  // TheoremProducer can create new Theorem instances.
69  //
70  // Theorems, unlike expressions, are NOT made unique, and it is
71  // possible to have the same theorem in different scopes with
72  // different assumptions and proofs. It is a deliberate feature,
73  // since natural deduction sometimes requires proving the same
74  // conclusion from different assumptions independently, e.g. in
75  // disjunction elimination rule.
76  class CVC_DLL Theorem {
77  private:
78  // Make a theorem producing class our friend. No definition is
79  // exposed here.
80  friend class TheoremProducer;
81  // Also allow our 3-valued cousin to create us
82  friend class Theorem3;
83  // Also TheoremValue classes for assumptions
84  friend class RegTheoremValue;
85  friend class RWTheoremValue;
86 
87  // Optimization: reflexivity theorems just store the exprValue pointer
88  // directly. Also, the lowest bit is set to 1 to indicate that its
89  // a reflexivity theorem. This really helps performance!
90  union {
91  intptr_t d_thm;
93  };
94 
95  //! Compare Theorems by their expressions. Return -1, 0, or 1.
96  friend int compare(const Theorem& t1, const Theorem& t2);
97  //! Compare a Theorem with an Expr (as if Expr is a Theorem)
98  friend int compare(const Theorem& t1, const Expr& e2);
99  //! Compare Theorems by TheoremValue pointers. Return -1, 0, or 1.
100  friend int compareByPtr(const Theorem& t1, const Theorem& t2);
101  //! Equality is w.r.t. compare()
102  friend bool operator==(const Theorem& t1, const Theorem& t2)
103  { return (compare(t1, t2)==0); }
104  //! Disequality is w.r.t. compare()
105  friend bool operator!=(const Theorem& t1, const Theorem& t2)
106  { return (compare(t1, t2) != 0); }
107 
108  //! Constructor only used by TheoremValue for assumptions
109  Theorem(TheoremValue* thm) :d_thm(((intptr_t)thm) | 0x1) {}
110 
111  //! Constructor for a new theorem
112  Theorem(TheoremManager* tm, const Expr &thm, const Assumptions& assump,
113  const Proof& pf, bool isAssump = false, int scope = -1);
114 
115  //! Constructor for rewrite theorems.
116  /*! These use a special efficient subclass of TheoremValue for
117  * theorems which represent rewrites: A |- t = t' or A |- phi<=>phi'
118  */
119  Theorem(TheoremManager* tm, const Expr& lhs, const Expr& rhs,
120  const Assumptions& assump, const Proof& pf, bool isAssump = false,
121  int scope = -1);
122 
123  //! Constructor for a reflexivity theorem: |-t=t or |-phi<=>phi
124  Theorem(const Expr& e);
125 
126  void recursivePrint(int& i) const;
127  void getAssumptionsRec(std::set<Expr>& assumptions) const;
128  void getAssumptionsAndCongRec(std::set<Expr>& assumptions,
129  std::vector<Expr>& congruences) const;
130  void GetSatAssumptionsRec(std::vector<Theorem>& assumptions) const;
131 
132  ExprValue* exprValue() const { return d_expr; }
133  TheoremValue* thm() const { return (TheoremValue*)(d_thm & (~(0x1))); }
134 
135  public:
136  // recusive function to print theorems and all assumptions recursively
137  // important: this function will corrupt all flags!! so exercise
138  // caution when using in any graph traversals
139  // (probably more useful to call it only before a crash)
140  void printDebug() const {
141  clearAllFlags();
142  setCachedValue(0);
143  setFlag();
144  int i = 1;
145  recursivePrint(i);
146  }
147 
148  // Default constructor creates Null theorem to allow untrusted
149  // code declare local vars without initialization (vector<Theorem>
150  // may need that, for instance).
151  Theorem(): d_thm(0) { }
152  // Copy constructor
153  Theorem(const Theorem &th);
154  // Assignment operator
155  Theorem& operator=(const Theorem &th);
156 
157  // Destructor
158  ~Theorem();
159 
160  // Test if we are running in a proof production mode and with assumptions
161  bool withProof() const;
162  bool withAssumptions() const;
163 
164  bool isNull() const { return d_thm == 0; }
165 
166  // True if theorem is of the form t=t' or phi iff phi'
167  bool isRewrite() const;
168  // True if theorem was created using assumpRule
169  bool isAssump() const;
170  // True if reflexivity theorem
171  bool isRefl() const { return d_thm && !(d_thm & 0x1); }
172 
173  // Return the theorem value as an Expr
174  Expr getExpr() const;
175  const Expr& getLHS() const;
176  const Expr& getRHS() const;
177 
178  void GetSatAssumptions(std::vector<Theorem>& assumptions) const;
179 
180 
181  // Return the assumptions. a should be empty and uninitialized
182  // void getAssumptions(Assumptions& a) const;
183  // Recurse to get actual assumptions
184 
185  void getLeafAssumptions(std::vector<Expr>& assumptions,
186  bool negate = false) const;
187  // Same as above but also collects congruences in the proof tree
188  void getAssumptionsAndCong(std::vector<Expr>& assumptions,
189  std::vector<Expr>& congruences,
190  bool negate = false) const;
191  const Assumptions& getAssumptionsRef() const;
192  // Return the proof of the theorem. If running without proofs,
193  // return the Null proof.
194  Proof getProof() const;
195  // Return the lowest scope level at which this theorem is valid.
196  // Value -1 means no information is available.
197  int getScope() const;
198  //! Return quantification level for this theorem
199  unsigned getQuantLevel() const;
200 
201  unsigned getQuantLevelDebug() const;
202 
203  //! Set the quantification level for this theorem
204  void setQuantLevel(unsigned level);
205 
206  // hash
207  size_t hash() const;
208 
209  // Printing
210  std::string toString() const;
211 
212  // For debugging
213  void printx() const;
214  void printxnodag() const;
215  void pprintx() const;
216  void pprintxnodag() const;
217 
218  void print() const;
219 
220  /*! \name Methods for Theorem Attributes
221  *
222  * Several attributes used in conflict analysis and assumptions
223  * graph traversals.
224  * @{
225  */
226  //! Check if the flag attribute is set
227  bool isFlagged() const;
228  //! Clear the flag attribute in all the theorems
229  void clearAllFlags() const;
230  //! Set the flag attribute
231  void setFlag() const;
232 
233  //! Set flag stating that theorem is an instance of substitution
234  void setSubst() const;
235  //! Is theorem an instance of substitution
236  bool isSubst() const;
237  //! Set the "expand" attribute
238  void setExpandFlag(bool val) const;
239  //! Check the "expand" attribute
240  bool getExpandFlag() const;
241  //! Set the "literal" attribute
242  /*! The expression of this theorem will be added as a conflict
243  * clause literal */
244  void setLitFlag(bool val) const;
245  //! Check the "literal" attribute
246  /*! The expression of this theorem will be added as a conflict
247  * clause literal */
248  bool getLitFlag() const;
249  //! Check if the theorem is a literal
250  bool isAbsLiteral() const;
251 
252  bool refutes(const Expr& e) const
253  {
254  return
255  (e.isNot() && e[0] == getExpr()) ||
256  (getExpr().isNot() && getExpr()[0] == e);
257  }
258 
259  bool proves(const Expr& e) const
260  {
261  return getExpr() == e;
262  }
263 
264  bool matches(const Expr& e) const
265  {
266  return proves(e) || refutes(e);
267  }
268 
269  void setCachedValue(int value) const;
270  int getCachedValue() const;
271 
272  /*!@}*/ // End of Attribute methods
273 
274  //! Printing a theorem to a stream, calling it "name".
275  std::ostream& print(std::ostream& os, const std::string& name) const;
276 
277  friend std::ostream& operator<<(std::ostream& os, const Theorem& t) {
278  return t.print(os, "Theorem");
279  }
280 
281  static bool TheoremEq(const Theorem& t1, const Theorem& t2)
282  {
283  DebugAssert(!t1.isNull() && !t2.isNull(),
284  "AssumptionsValue() Null Theorem passed to constructor");
285  return t1 == t2;
286  }
287  }; // End of Theorem
288 
289 /*****************************************************************************/
290 /*!
291  *\class Theorem3
292  *\brief Theorem3
293  *
294  * Author: Sergey Berezin
295  *
296  * Created: Tue Nov 4 17:57:07 2003
297  *
298  * Implements the 3-valued theorem used for the user assertions and
299  * the result of query. It is simply a wrapper around class Theorem,
300  * but has a different semantic meaning: the formula may have partial
301  * functions and has the Kleene's 3-valued interpretation. The fact
302  * that a Theorem3 value is derived means that the TCCs for the
303  * formula and all of its assumptions are valid in the current
304  * context, and the proofs of TCCs contribute to the set of
305  * assumptions.
306  */
307 /*****************************************************************************/
308  class Theorem3 {
309  private:
310  // Make a theorem producing class our friend. No definition is
311  // exposed here.
312  friend class TheoremProducer;
313 
315 
316  friend bool operator==(const Theorem3& t1, const Theorem3& t2) {
317  return t1.d_thm == t2.d_thm;
318  }
319  friend bool operator!=(const Theorem3& t1, const Theorem3& t2) {
320  return t1.d_thm != t2.d_thm;
321  }
322 
323 
324  // Private constructors for a new theorem
325  Theorem3(TheoremManager* tm, const Expr &thm, const Assumptions& assump,
326  const Proof& pf, bool isAssump = false, int scope = -1)
327  : d_thm(tm, thm, assump, pf, isAssump, scope) { }
328 
329  // Constructors for rewrite theorems. These use a special efficient
330  // subclass of TheoremValue for theorems which represent rewrites:
331  // A |- t = t' or A |- phi iff phi'
332  Theorem3(TheoremManager* tm, const Expr& lhs, const Expr& rhs,
333  const Assumptions& assump, const Proof& pf)
334  : d_thm(tm, lhs, rhs, assump, pf) { }
335 
336  public:
337  // recusive function to print theorems and all assumptions recursively
338  // important: this function will corrupt all flags!! so exercise
339  // caution when using in any graph traversals
340  // (probably more useful to call it only before a crash)
341  void printDebug() const { d_thm.printDebug(); }
342 
343  // Default constructor creates Null theorem to allow untrusted
344  // code declare local vars without initialization (vector<Theorem>
345  // may need that, for instance).
346  Theorem3() { }
347 
348  // Destructor
349  virtual ~Theorem3() { }
350 
351  bool isNull() const { return d_thm.isNull(); }
352 
353  // True if theorem is of the form t=t' or phi iff phi'
354  bool isRewrite() const { return d_thm.isRewrite(); }
355  bool isAssump() const { return d_thm.isAssump(); }
356 
357  // Return the theorem value as an Expr
358  Expr getExpr() const { return d_thm.getExpr(); }
359  const Expr& getLHS() const { return d_thm.getLHS(); }
360  const Expr& getRHS() const { return d_thm.getRHS(); }
361 
362  // Return the assumptions.
363  // It's an error if called while running without assumptions.
364  // void getAssumptions(Assumptions& a) const { d_thm.getAssumptions(a); }
366  return d_thm.getAssumptionsRef();
367  }
368  // Return the proof of the theorem. If running without proofs,
369  // return the Null proof.
370  Proof getProof() const { return d_thm.getProof(); }
371 
372  // Return the lowest scope level at which this theorem is valid.
373  // Value -1 means no information is available.
374  int getScope() const { return d_thm.getScope(); }
375 
376  // Test if we are running in a proof production mode and with assumptions
377  bool withProof() const { return d_thm.withProof(); }
378  bool withAssumptions() const { return d_thm.withAssumptions(); }
379 
380  // Printing
381  std::string toString() const;
382 
383  // For debugging
384  void printx() const { d_thm.printx(); }
385  void print() const { d_thm.print(); }
386 
387  //! Check if the theorem is a literal
388  bool isAbsLiteral() const { return d_thm.isAbsLiteral(); }
389 
390  friend std::ostream& operator<<(std::ostream& os, const Theorem3& t) {
391  return t.d_thm.print(os, "Theorem3");
392  }
393  }; // End of Theorem3
394 
395  //! "Less" comparator for theorems by TheoremValue pointers
396  class TheoremLess {
397  public:
398  bool operator()(const Theorem& t1, const Theorem& t2) const {
399  return (compareByPtr(t1, t2) < 0);
400  }
401  };
402  typedef std::map<Theorem,bool, TheoremLess> TheoremMap;
403 
404  inline std::string Theorem::toString() const {
405  std::ostringstream ss;
406  ss << (*this);
407  return ss.str();
408  }
409 
410  inline std::string Theorem3::toString() const {
411  std::ostringstream ss;
412  ss << (*this);
413  return ss.str();
414  }
415 
416  // Merge assumptions from different theorems
417 // inline Assumptions merge(const Theorem& t1, const Theorem& t2) {
418 // return Assumptions(t1, t2);
419 // }
420 // inline void merge(Assumptions& a, const Theorem& t) {
421 // a.add(t);
422 // }
423 // inline Assumptions merge(const std::vector<Theorem>& t) {
424 // return Assumptions(t);
425 // }
426 
427  inline bool operator<(const Theorem& t1, const Theorem& t2)
428  { return compare(t1, t2) < 0; }
429  inline bool operator<=(const Theorem& t1, const Theorem& t2)
430  { return compare(t1, t2) <= 0; }
431  inline bool operator>(const Theorem& t1, const Theorem& t2)
432  { return compare(t1, t2) > 0; }
433  inline bool operator>=(const Theorem& t1, const Theorem& t2)
434  { return compare(t1, t2) >= 0; }
435 
436 } // end of namespace CVC3
437 
438 #include "hash_fun.h"
439 namespace Hash
440 {
441 
442 template<> struct hash<CVC3::Theorem>
443 {
444  size_t operator()(const CVC3::Theorem& e) const { return e.hash(); }
445 };
446 
447 }
448 
449 #endif
void printx() const
Definition: theorem.h:384
Data structure of expressions in CVC3.
Definition: expr.h:133
#define CVC_DLL
Definition: type.h:43
Proof getProof() const
Definition: theorem.h:370
bool withAssumptions() const
Definition: theorem.h:378
std::map< Theorem, bool, TheoremLess > TheoremMap
Definition: theorem.h:402
friend std::ostream & operator<<(std::ostream &os, const Theorem3 &t)
Definition: theorem.h:390
bool operator<=(const Expr &e1, const Expr &e2)
Definition: expr.h:1612
int compare(const Expr &e1, const Expr &e2)
Definition: expr.cpp:597
TheoremValue * thm() const
Definition: theorem.h:133
static bool TheoremEq(const Theorem &t1, const Theorem &t2)
Definition: theorem.h:281
bool withAssumptions() const
Definition: theorem.cpp:219
ExprValue * exprValue() const
Definition: theorem.h:132
int getScope() const
Definition: theorem.h:374
Theorem(TheoremValue *thm)
Constructor only used by TheoremValue for assumptions.
Definition: theorem.h:109
bool proves(const Expr &e) const
Check if the flag attribute is set.
Definition: theorem.h:259
void printDebug() const
Definition: theorem.h:140
Theorem d_thm
Definition: theorem.h:314
#define DebugAssert(cond, str)
Definition: debug.h:408
size_t hash() const
Definition: theorem.cpp:511
bool operator>(const Expr &e1, const Expr &e2)
Definition: expr.h:1614
int getScope() const
Definition: theorem.cpp:486
bool matches(const Expr &e) const
Check if the flag attribute is set.
Definition: theorem.h:264
bool isRewrite() const
Definition: theorem.h:354
bool refutes(const Expr &e) const
Check if the flag attribute is set.
Definition: theorem.h:252
bool withProof() const
Definition: theorem.h:377
void print() const
Definition: theorem.h:385
Theorem3.
Definition: theorem.h:308
bool isNot() const
Definition: expr.h:420
bool withProof() const
Definition: theorem.cpp:214
friend bool operator==(const Theorem3 &t1, const Theorem3 &t2)
Definition: theorem.h:316
std::string toString() const
Definition: theorem.h:410
friend bool operator!=(const Theorem &t1, const Theorem &t2)
Disequality is w.r.t. compare()
Definition: theorem.h:105
friend bool operator==(const Theorem &t1, const Theorem &t2)
Equality is w.r.t. compare()
Definition: theorem.h:102
virtual ~Theorem3()
Definition: theorem.h:349
std::string toString() const
Definition: theorem.h:404
intptr_t d_thm
Definition: theorem.h:91
int compareByPtr(const Theorem &t1, const Theorem &t2)
Definition: theorem.cpp:83
Abstraction over different operating systems.
const Expr & getRHS() const
Definition: theorem.cpp:246
bool isAbsLiteral() const
Check if the theorem is a literal.
Definition: theorem.cpp:482
Proof getProof() const
Definition: theorem.cpp:402
Theorem3(TheoremManager *tm, const Expr &lhs, const Expr &rhs, const Assumptions &assump, const Proof &pf)
Definition: theorem.h:332
const Assumptions & getAssumptionsRef() const
Definition: theorem.cpp:385
void printx() const
Definition: theorem.cpp:207
bool operator<(const Expr &e1, const Expr &e2)
Definition: expr.h:1610
Expr getExpr() const
Definition: theorem.cpp:230
bool isNull() const
Definition: theorem.h:164
ExprValue * d_expr
Definition: theorem.h:92
hash functions
bool isNull() const
Definition: theorem.h:351
size_t operator()(const CVC3::Theorem &e) const
Definition: theorem.h:444
bool operator>=(const Expr &e1, const Expr &e2)
Definition: expr.h:1616
bool operator()(const Theorem &t1, const Theorem &t2) const
Definition: theorem.h:398
"Less" comparator for theorems by TheoremValue pointers
Definition: theorem.h:396
void printDebug() const
Definition: theorem.h:341
const Expr & getRHS() const
Definition: theorem.h:360
Theorem3(TheoremManager *tm, const Expr &thm, const Assumptions &assump, const Proof &pf, bool isAssump=false, int scope=-1)
Definition: theorem.h:325
bool isAbsLiteral() const
Check if the theorem is a literal.
Definition: theorem.h:388
void print() const
Definition: theorem.cpp:211
Definition of the API to expression package. See class Expr for details.
bool isRefl() const
Definition: theorem.h:171
const Expr & getLHS() const
Definition: theorem.cpp:240
const Expr & getLHS() const
Definition: theorem.h:359
bool isAssump() const
Definition: theorem.h:355
The base class for holding the actual data in expressions.
Definition: expr_value.h:69
friend bool operator!=(const Theorem3 &t1, const Theorem3 &t2)
Definition: theorem.h:319
friend std::ostream & operator<<(std::ostream &os, const Theorem &t)
Definition: theorem.h:277
bool isRewrite() const
Definition: theorem.cpp:224
Expr getExpr() const
Definition: theorem.h:358
bool isAssump() const
Definition: theorem.cpp:395
const Assumptions & getAssumptionsRef() const
Definition: theorem.h:365