CVC3  2.4.1
theorem_value.h
Go to the documentation of this file.
1 /*****************************************************************************/
2 /*!
3  * \file theorem_value.h
4  *
5  * Author: Sergey Berezin
6  *
7  * Created: Dec 10 01:03:34 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: TheoremValue
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 appropriate modes also the set of
28 // assumptions and the 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_value.h file should NOT be used by the decision
41 // procedures. Use theorem.h instead.
42 //
43 ////////////////////////////////////////////////////////////////////////
44 
45 #ifndef _cvc3__theorem_value_h_
46 #define _cvc3__theorem_value_h_
47 
48 #include "assumptions.h"
49 #include "theorem_manager.h"
50 //#include "theory_core.h"
51 //#include "vcl.h"
52 
53 namespace CVC3 {
54 
55  //extern VCL* myvcl;
57  {
58  // These are the only classes that can create new TheoremValue classes
59  friend class Theorem;
60  friend class RegTheoremValue;
61  friend class RWTheoremValue;
62 
63  protected:
64  //! Theorem Manager
66 
67  //! The expression representing a theorem
69 
70  //! Proof of the theorem
72 
73  //! How many pointers to this theorem value
74  unsigned d_refcount;
75 
76  //! Largest scope level of the assumptions
78 
79  //! Quantification level of this theorem
80  unsigned d_quantLevel;
81 
82 
83  //! debug quantlevel, this one is from proof, not from assumption list
84  // unsigned d_quantLevelDebug;
85 
86  //! Temporary flag used during traversals
87  unsigned d_flag;
88 
89  //! Temporary cache used during traversals
90  int d_cachedValue : 28;
91 
92  bool d_isSubst : 1; //!< whether this theorem was generated by substitution
93  bool d_isAssump : 1;
94  bool d_expand : 1; //!< whether it should this be expanded in graph traversal
95  bool d_clauselit : 1; //!< whether it belongs to the conflict clause
96 
97 
98  private:
99  // Constructor.
100  /*!
101  * NOTE: it is private; only friend classes can call it.
102  *
103  * If the assumptions refer to only one theorem, grab the
104  * assumptions of that theorem instead.
105  */
106 
107  //by yeting, we should do something to catch theorems created with empty assumptions.
108  //one way is to set the d_quantLevel 999 here.
109 
111  const Proof& pf, bool isAssump) :
112  d_tm(tm), d_thm(thm), d_proof(pf), d_refcount(0),
113  d_scopeLevel(0), d_quantLevel(0), d_flag(0), d_cachedValue(0),
114  d_isSubst(0), d_isAssump(isAssump), d_expand(0), d_clauselit(0) {}
115 
116  // Disable copy constructor and assignment
118  FatalAssert(false, "TheoremValue() copy constructor called");
119  }
121  FatalAssert(false, "TheoremValue assignment operator called");
122  return *this;
123  }
124 
125  bool isFlagged() const {
126  return d_flag == d_tm->getFlag();
127  }
128 
129  void clearAllFlags() {
130  d_tm->clearAllFlags();
131  }
132 
133  void setFlag() {
134  d_flag = d_tm->getFlag();
135  }
136 
137  void setCachedValue(int value) {
138  d_cachedValue = value;
139  }
140 
141  int getCachedValue() const {
142  return d_cachedValue;
143  }
144 
145  void setSubst() { d_isSubst = true; }
146  bool isSubst() { return d_isSubst; }
147 
148  void setExpandFlag(bool val) {
149  d_expand = val;
150  }
151 
152  bool getExpandFlag() {
153  return d_expand;
154  }
155 
156  void setLitFlag(bool val) {
157  d_clauselit = val;
158  }
159 
160  bool getLitFlag() {
161  return d_clauselit;
162  }
163 
164  int getScope() {
165  return d_scopeLevel;
166  }
167 
168  unsigned getQuantLevel() { return d_quantLevel; }
169 
170  unsigned getQuantLevelDebug() {
171  return 0;
172  // return d_quantLevelDebug;
173  }
174 
175  void setQuantLevel(unsigned level) { d_quantLevel = level; }
176 
177  unsigned recQuantLevel(Expr proof){
178  return d_quantLevel;
179  /*
180  if( ! proof.isNull()){
181  // std::cout << "debug level " << proof << std::endl;;
182  }
183  else {
184  // std::cout << "proof null" << proof << std::endl;;
185  }
186 
187  unsigned nch = proof.arity();
188  unsigned level(0);
189  if (proof.getKind() == PF_APPLY){
190  for (unsigned i = 1 ; i < nch ; i++){
191  if ((proof[i]).getKind() == PF_APPLY || proof[i].getKind() == LAMBDA || proof[i].isVar()) {
192  if(proof[i].isVar()){
193  // std::cout << "found var in pf # " << proof << std::endl;
194  }
195  unsigned chLevel = recQuantLevel(proof[i]);
196  level = chLevel > level ? chLevel : level ;
197  }
198  }
199  if(proof[0].getName() == "universal_elimination"){
200  level++;
201  unsigned gtermLevel = myvcl->core()->getQuantLevelForTerm(proof[4]);
202  if((gtermLevel + 1) > level ){
203  level = gtermLevel+1;
204  }
205  // std::cout << "level " << level << std::endl;
206  }
207  else {
208  // std::cout << "proof name non-inst" << proof[0].getName() << std::endl;
209  }
210  // std::cout << "get level " << d_thm << std::endl;
211  // std::cout << "get level " << level << std::endl;
212  // std::cout << "get level " << proof << std::endl;
213  return level;
214  }
215  else if (proof.getKind() == LAMBDA){
216  std::cout << "lambda " << proof << std::endl;
217  std::cout << "lambda body " << proof << std::endl;
218  return recQuantLevel(proof.getBody());
219  }
220  else if (proof.isNull() ){
221  // std::cout <<" error in get quantleveldebug " << std::endl;
222  // std::cout << proof << std::endl;
223  return 100000;
224  }
225  else if (proof.isVar()){
226  if(proof.getType().getExpr().getType().isBool()){
227  //std::cout << "var proof " << proof.getType().getExpr() << std::endl;
228  // std::cout << "found proof var # " << proof << std::endl;
229  // std::cout << proof.getType() << std::endl;
230  // std::cout << "the quant level is " << myvcl->core()->getQuantLevelForTerm(proof.getType().getExpr()) << std::endl;
231  return myvcl->core()->getQuantLevelForTerm(proof.getType().getExpr());
232  }
233  else{
234  return 0;
235  }
236  }
237  else{
238  std::cout <<" error in get quantleveldebug " << std::endl;
239  std::cout << proof << std::endl;
240  std::cout << proof.isVar() << std::endl;
241  return 200000;
242  }
243  return 0;
244  */
245  }
246 
248  return d_quantLevel;
249  /*
250  Expr p (d_proof.getExpr());
251  unsigned ret ;
252  if (isAssump()){
253  if(d_thm.inUserAssumption()){
254  ret = 0 ;
255  // return 0;
256  }
257  else {
258  // std::cout <<" why here " << std::endl;
259  // std::cout << "the quant level is " << myvcl->core()->getQuantLevelForTerm(d_thm) << std::endl;
260  // std::cout << d_thm << std::endl;
261  // std::cout <<" == end of why here " << std::endl;
262  ret = myvcl->core()->getQuantLevelForTerm(d_thm);
263  //
264  // return myvcl->core()->getQuantLevelForTerm(d_thm);
265  }
266  }
267  else if (p.isVar()){
268  unsigned level1 = myvcl->core()->getQuantLevelForTerm(p.getType().getExpr());
269  unsigned level2 = d_quantLevel;
270  if(level1 != level2){
271  std::cout <<"not rq" << std::endl;
272  }
273  else{
274  ret = level1;
275  // return level1;
276  }
277  }
278  else {
279  ret = recQuantLevel(p);
280  // return recQuantLevel(p);
281  }
282  // std::cout << " get -- begin with debug level " << ret << std::endl;
283  // std::cout << " quant level " << d_quantLevel << std::endl;
284  // std::cout << " get level thm " << d_thm << std::endl;
285  // std::cout << " get level is var " << p.isVar() << std::endl;
286  if(p.isVar()){
287  // std::cout << "var proof " << p.getType().getExpr()<< std::endl;
288  }
289  return ret;
290  */
291  }
292 
293 
294 // virtual bool isRewrite() const { return d_thm.isEq() || d_thm.isIff(); }
295  virtual bool isRewrite() const { return false; }
296 
297  virtual const Expr& getExpr() const { return d_thm; }
298  virtual const Expr& getLHS() const {
299  // TRACE("getExpr","TheoremValue::getLHS called (",d_thm,")");
301  "TheoremValue::getLHS() called on non-rewrite theorem:\n"
302  +toString());
303  return d_thm[0];
304  }
305  virtual const Expr& getRHS() const {
306  // TRACE("getExpr","TheoremValue::getRHS called (",d_thm,")");
308  "TheoremValue::getRHS() called on non-rewrite theorem:\n"
309  +toString());
310  return d_thm[1];
311  }
312 
313  virtual const Assumptions& getAssumptionsRef() const = 0;
314 
315  bool isAssump() const { return d_isAssump; }
316  const Proof& getProof() { return d_proof; }
317 
318  public:
319  // Destructor
320  virtual ~TheoremValue() {
321  IF_DEBUG(FatalAssert(d_refcount == 0,
322  "Thm::TheoremValue::~TheoremValue(): refcount != 0.");)
323  }
324 
325  std::string toString() const {
326  return getAssumptionsRef().toString() + " |- " + getExpr().toString();
327  }
328 
329  // Memory management
330  virtual MemoryManager* getMM() = 0;
331 
332  }; // end of class TheoremValue
333 
334 ///////////////////////////////////////////////////////////////////////////////
335 // //
336 // Class: RegTheoremValue //
337 // Author: Clark Barrett //
338 // Created: Fri May 2 12:51:55 2003 //
339 // Description: A special subclass for non-rewrite theorems. Assumptions are//
340 // embedded in the object for easy reference. //
341 // //
342 ///////////////////////////////////////////////////////////////////////////////
344  {
345  friend class Theorem;
346 
347  protected:
348  //! The assumptions for the theorem
350 
351 
352  private:
353  // Constructor. NOTE: it is private; only friend classes can call it.
355  const Assumptions& assump, const Proof& pf, bool isAssump,
356  int scope = -1)
357  : TheoremValue(tm, thm, pf, isAssump), d_assump(assump)
358  {
359  DebugAssert(d_tm->isActive(), "TheoremValue()");
360  if (isAssump) {
361  DebugAssert(assump.empty(), "Expected empty assumptions");
362  // refcount tricks are because a loop is created with Assumptions
363  d_refcount = 1;
364  {
365  Theorem t(this);
366  d_assump.add1(t);
367  }
368  d_refcount = 0;
369  if (scope == -1) d_scopeLevel = tm->getCM()->scopeLevel();
370  else d_scopeLevel = scope;
371  // TRACE("quantlevel", d_quantLevel, " theorem init assump", thm.toString());
372  }
373  else {
374  if (!d_assump.empty()) {
375  const Assumptions::iterator iend = d_assump.end();
376  for (Assumptions::iterator i = d_assump.begin();
377  i != iend; ++i) {
378  if (i->getScope() > d_scopeLevel)
379  d_scopeLevel = i->getScope();
380  if (i->getQuantLevel() > d_quantLevel){
381  d_quantLevel = i->getQuantLevel();
382  }
383  }
384  // TRACE("quantlevel", d_quantLevel, " theorem non-null assump", thm.toString());
385  }
386  else{
387  TRACE("quantlevel","empty assumptions found ", thm , "");
388  }
389  }
390  //yeting, let me check d_quantleveldebug here
391  // d_quantLevelDebug = findQuantLevelDebug();
392 
393  }
394 
395  public:
396  // Destructor
398  if (d_isAssump) {
399  IF_DEBUG(FatalAssert(d_assump.size() == 1, "Expected size 1");)
400  IF_DEBUG(FatalAssert(d_assump.getFirst().thm() == this, "Expected loop");)
401  d_assump.getFirst().d_thm = 0;
402  }
403  }
404 
405  const Assumptions& getAssumptionsRef() const { return d_assump; }
406 
407  // Memory management
408  MemoryManager* getMM() { return d_tm->getMM(); }
409 
410  void* operator new(size_t size, MemoryManager* mm) {
411  return mm->newData(size);
412  }
413  void operator delete(void* pMem, MemoryManager* mm) {
414  mm->deleteData(pMem);
415  }
416 
417  void operator delete(void* d) { }
418 
419  }; // end of class RegTheoremValue
420 
421 ///////////////////////////////////////////////////////////////////////////////
422 // //
423 // Class: RWTheoremValue //
424 // Author: Clark Barrett //
425 // Created: Fri May 2 12:51:55 2003 //
426 // Description: A special subclass for theorems of the form A |- t=t' or //
427 // A |- phi iff phi'. The actual Expr is only created on //
428 // demand. The idea is that getLHS and getRHS should be used //
429 // whenever possible, avoiding creating unnecessary Expr's. //
430 // //
431 ///////////////////////////////////////////////////////////////////////////////
433  {
434  friend class Theorem;
435 
436  protected:
437  // d_thm in the base class contains the full expression, which is
438  // only constructed on demand.
442 
443  private:
444  void init(const Assumptions& assump, int scope)
445  {
446  DebugAssert(d_tm->isActive(), "TheoremValue()");
447  if (d_isAssump) {
448  DebugAssert(assump.empty(), "Expected empty assumptions");
449  // refcount tricks are because a loop is created with Assumptions
450  d_refcount = 1;
451  {
452  Theorem t(this);
453  d_assump = new Assumptions(t);
454  }
455  d_refcount = 0;
456  if (scope == -1) d_scopeLevel = d_tm->getCM()->scopeLevel();
457  else d_scopeLevel = scope;
458  // TRACE("quantlevel", d_quantLevel, " RW theorem init is assump ", d_thm.toString());
459  }
460  else {
461  if (!assump.empty()) {
462  d_assump = new Assumptions(assump);
463  const Assumptions::iterator iend = assump.end();
464  for (Assumptions::iterator i = assump.begin();
465  i != iend; ++i) {
466  if (i->getScope() > d_scopeLevel)
467  d_scopeLevel = i->getScope();
468  if (i->getQuantLevel() > d_quantLevel){
469  d_quantLevel = i->getQuantLevel();
470  // TRACE("quantlevel", d_quantLevel, "=========\n RW theorem init has non-null assump ", this->toString());
471  }
472  }
473  // TRACE("quantlevel", d_quantLevel, " RW theorem init has non-null assump ", d_thm.toString());
474  }
475  else{
476  TRACE("quantlevel", "RW empty assup found lhs << " , d_lhs, "" );
477  TRACE("quantlevel", "RW empty assup found rhs >> " , d_rhs, "" );
478  }
479  // TRACE("quantlevel", d_quantLevel, " RW theorem init has null assump ", d_thm.toString());
480  }
481 
482  // d_quantLevelDebug = findQuantLevelDebug();
483 
484  }
485 
486  // Constructor. NOTE: it is private; only friend classes can call it.
487  RWTheoremValue(TheoremManager* tm, const Expr& lhs, const Expr& rhs,
488  const Assumptions& assump, const Proof& pf, bool isAssump,
489  int scope = -1)
490  : TheoremValue(tm, Expr(), pf, isAssump), d_lhs(lhs), d_rhs(rhs), d_assump(NULL)
491  { init(assump, scope); }
492 
493  // Sometimes we have the full expression already created
495  const Assumptions& assump, const Proof& pf, bool isAssump,
496  int scope = -1)
497  : TheoremValue(tm, thm, pf, isAssump), d_lhs(thm[0]), d_rhs(thm[1]), d_assump(NULL)
498  { init(assump, scope); }
499 
500  const Expr& getExpr() const {
501  if (d_thm.isNull()) {
502  bool isBool = d_lhs.getType().isBool();
503  // have to fake out the const qualifier
504  Expr* pexpr = const_cast<Expr*>(&d_thm);
505  *pexpr = isBool ? d_lhs.iffExpr(d_rhs) : d_lhs.eqExpr(d_rhs);
506  // TRACE("getExpr", "getExpr called on RWTheorem (", d_thm, ")");
507  }
508  return d_thm;
509  }
510 
511  const Expr& getLHS() const { return d_lhs; }
512  const Expr& getRHS() const { return d_rhs; }
513 
514  public:
515  // Destructor
517  if (d_isAssump) {
518  IF_DEBUG(FatalAssert(d_assump && d_assump->size() == 1, "Expected size 1");)
519  IF_DEBUG(FatalAssert(d_assump->getFirst().thm() == this, "Expected loop");)
520  d_assump->getFirst().d_thm = 0;
521  }
522  if (d_assump) delete d_assump;
523  }
524 
525  bool isRewrite() const { return true; }
527  if (d_assump) return *d_assump;
528  else return Assumptions::emptyAssump();
529  }
530 
531  // Memory management
532  MemoryManager* getMM() { return d_tm->getRWMM(); }
533 
534  void* operator new(size_t size, MemoryManager* mm) {
535  return mm->newData(size);
536  }
537  void operator delete(void* pMem, MemoryManager* mm) {
538  mm->deleteData(pMem);
539  }
540 
541  void operator delete(void* d) { }
542 
543  }; // end of class RWTheoremValue
544 
545 } // end of namespace CVC3
546 
547 #endif
bool d_expand
whether it should this be expanded in graph traversal
Definition: theorem_value.h:94
int d_cachedValue
Temporary cache used during traversals.
Definition: theorem_value.h:90
unsigned findQuantLevelDebug()
bool isNull() const
Definition: expr.h:1223
std::string toString() const
Data structure of expressions in CVC3.
Definition: expr.h:133
virtual ~TheoremValue()
int getCachedValue() const
virtual const Expr & getExpr() const
unsigned size() const
Definition: assumptions.h:94
TheoremValue * thm() const
Definition: theorem.h:133
virtual const Expr & getLHS() const
bool isAssump() const
bool d_clauselit
whether it belongs to the conflict clause
Definition: theorem_value.h:95
TheoremValue(TheoremManager *tm, const Expr &thm, const Proof &pf, bool isAssump)
MemoryManager * getMM()
Expr eqExpr(const Expr &right) const
Definition: expr.h:929
MemoryManager * getMM() const
Expr d_thm
The expression representing a theorem.
Definition: theorem_value.h:68
bool isBool() const
Definition: type.h:60
#define DebugAssert(cond, str)
Definition: debug.h:408
virtual const Assumptions & getAssumptionsRef() const =0
int getScope() const
Definition: theorem.cpp:486
bool isRewrite() const
RegTheoremValue(TheoremManager *tm, const Expr &thm, const Assumptions &assump, const Proof &pf, bool isAssump, int scope=-1)
iterator end() const
Definition: assumptions.h:152
bool d_isSubst
whether this theorem was generated by substitution
Definition: theorem_value.h:92
Assumptions * d_assump
const Expr & getExpr() const
iterator begin() const
Definition: assumptions.h:151
Proof d_proof
Proof of the theorem.
Definition: theorem_value.h:71
RWTheoremValue(TheoremManager *tm, const Expr &thm, const Assumptions &assump, const Proof &pf, bool isAssump, int scope=-1)
ContextManager * getCM() const
#define FatalAssert(cond, msg)
If something goes horribly wrong, print a message and abort immediately with exit(1).
Definition: debug.h:37
const Proof & getProof()
std::string toString() const
Print the expression to a string.
Definition: expr.cpp:344
bool isFlagged() const
intptr_t d_thm
Definition: theorem.h:91
MemoryManager * getRWMM() const
const Assumptions & getAssumptionsRef() const
virtual const Expr & getRHS() const
Expr iffExpr(const Expr &right) const
Definition: expr.h:965
RWTheoremValue(TheoremManager *tm, const Expr &lhs, const Expr &rhs, const Assumptions &assump, const Proof &pf, bool isAssump, int scope=-1)
int d_scopeLevel
Largest scope level of the assumptions.
Definition: theorem_value.h:77
void init(const Assumptions &assump, int scope)
#define IF_DEBUG(code)
Definition: debug.h:406
unsigned d_refcount
How many pointers to this theorem value.
Definition: theorem_value.h:74
MemoryManager * getMM()
void setLitFlag(bool val)
virtual MemoryManager * getMM()=0
unsigned getQuantLevel()
unsigned getQuantLevelDebug()
const Assumptions & getAssumptionsRef() const
Theorem & getFirst()
Definition: assumptions.h:98
const Expr & getRHS() const
TheoremValue(const TheoremValue &t)
void setQuantLevel(unsigned level)
virtual void * newData(size_t size)=0
unsigned d_quantLevel
Quantification level of this theorem.
Definition: theorem_value.h:80
void add1(const Theorem &t)
Definition: assumptions.h:85
unsigned getFlag() const
bool empty() const
Definition: assumptions.h:95
Assumptions d_assump
The assumptions for the theorem.
Iterator for the Assumptions: points to class Theorem.
Definition: assumptions.h:118
const Expr & getLHS() const
void setCachedValue(int value)
TheoremValue & operator=(const TheoremValue &t)
Definition: expr.cpp:35
Definition: kinds.h:99
Type getType() const
Get the type. Recursively compute if necessary.
Definition: expr.h:1259
bool isActive()
Test whether the TheoremManager is still active.
void setExpandFlag(bool val)
std::string toString() const
static const Assumptions & emptyAssump()
Definition: assumptions.h:83
TheoremManager * d_tm
Theorem Manager.
Definition: theorem_value.h:65
unsigned recQuantLevel(Expr proof)
unsigned d_flag
debug quantlevel, this one is from proof, not from assumption list
Definition: theorem_value.h:87
virtual bool isRewrite() const