CVC3  2.4.1
theorem.cpp
Go to the documentation of this file.
1 /*****************************************************************************/
2 /*!
3  * \file theorem.cpp
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 // See theorem.h file for more information.
25 ///////////////////////////////////////////////////////////////////////////////
26 
27 #include "theorem.h"
28 #include "theorem_value.h"
29 #include "command_line_flags.h"
30 
31 namespace CVC3 {
32  using namespace std;
33 
34  //! Compare Theorems by their expressions. Return -1, 0, or 1.
35  /*!
36  * This is an arbitrary total ordering on Theorems. For
37  * simplicity, we define rewrite theorems (e1 = e2 or e1 <=> e2) to
38  * be smaller than other theorems.
39  */
40  /*
41  int compare(const Theorem& t1, const Theorem& t2) {
42  return compare(t1.getExpr(), t2.getExpr());
43  }
44  */
45  int compare(const Theorem& t1, const Theorem& t2) {
46  if(t1.d_thm == t2.d_thm) return 0;
47  if(t1.isNull()) return -1; // Null Theorem is less than other theorems
48  if(t2.isNull()) return 1;
49 
50  bool rw1(t1.isRewrite()), rw2(t2.isRewrite());
51 
52  if(!rw2) return compare(t1, t2.getExpr());
53  else if(!rw1) return -compare(t2, t1.getExpr());
54  else {
55  int res(compare(t1.getLHS(), t2.getLHS()));
56  if(res==0) res = compare(t1.getRHS(), t2.getRHS());
57  return res;
58  }
59  }
60  /*
61  int compare(const Theorem& t1, const Expr& e2) {
62  return compare(t1.getExpr(), e2);
63  }
64  */
65  int compare(const Theorem& t1, const Expr& e2) {
66  bool rw1(t1.isRewrite()), rw2(e2.isEq() || e2.isIff());
67  if(!rw1) {
68  const Expr& e1 = t1.getExpr();
69  rw1 = (e1.isEq() || e1.isIff());
70  }
71  if(rw1) {
72  if(rw2) {
73  int res(compare(t1.getLHS(), e2[0]));
74  if(res==0) res = compare(t1.getRHS(), e2[1]);
75  return res;
76  } else return -1;
77  } else {
78  if(rw2) return 1;
79  else return compare(t1.getExpr(), e2);
80  }
81  }
82 
83  int compareByPtr(const Theorem& t1, const Theorem& t2) {
84  if(t1.d_thm == t2.d_thm) return 0;
85  else if(t1.d_thm < t2.d_thm) return -1;
86  else return 1;
87  }
88 
89 
90  // Assignment operator
92  // Handle self-assignment
93  if(this == &th) return *this;
94  if(d_thm == th.d_thm) return *this;
95 
96  long tmp = th.d_thm;
97 
98  // Increase the refcount on th
99  if (tmp & 0x1) {
100  TheoremValue* tv = (TheoremValue*) (tmp & (~(0x1)));
101  DebugAssert(tv->d_refcount > 0,
102  "Theorem::operator=: invariant violated");
103  ++(tv->d_refcount);
104  }
105  else if (tmp != 0) {
106  th.exprValue()->incRefcount();
107  }
108 
109  // Decrease the refcount on this
110  if (d_thm & 0x1) {
111  TheoremValue* tv = thm();
112  DebugAssert(tv->d_refcount > 0,
113  "Theorem::operator=: invariant violated");
114  if(--(tv->d_refcount) == 0) {
115  MemoryManager* mm = tv->getMM();
116  delete tv;
117  mm->deleteData(tv);
118  }
119  }
120  else if (d_thm != 0) {
121  exprValue()->decRefcount();
122  }
123 
124  d_thm = tmp;
125 
126  return *this;
127  }
128 
129 
130  // Constructors
132  const Assumptions& assump, const Proof& pf,
133  bool isAssump, int scope) {
134  TheoremValue* tv;
135  if (thm.isEq() || thm.isIff()) {
136  if (thm[0] == thm[1]) {
137  d_expr = thm[0].d_expr;
138  d_expr->incRefcount();
139  return;
140  }
141  tv = new(tm->getRWMM()) RWTheoremValue(tm, thm, assump, pf, isAssump, scope);
142  }
143  else
144  tv = new(tm->getMM()) RegTheoremValue(tm, thm, assump, pf, isAssump, scope);
145  tv->d_refcount++;
146  d_thm = ((intptr_t)tv)|0x1;
147  // TRACE("theorem", "Theorem(e) => ", *this, "");
148  DebugAssert(!withProof() || !pf.isNull(),
149  "Null proof in theorem:\n"+toString());
150  }
151 
152  Theorem::Theorem(TheoremManager* tm, const Expr& lhs, const Expr& rhs,
153  const Assumptions& assump, const Proof& pf, bool isAssump,
154  int scope) {
155  if (lhs == rhs) {
156  d_expr = lhs.d_expr;
157  d_expr->incRefcount();
158  return;
159  }
160  TheoremValue* tv = new(tm->getRWMM())
161  RWTheoremValue(tm, lhs, rhs, assump, pf, isAssump, scope);
162  tv->d_refcount++;
163  d_thm = ((long)tv)|0x1;
164  DebugAssert(!withProof() || !pf.isNull(),
165  "Null proof in theorem:\n"+toString());
166  }
167 
168 
169  // Copy constructor
170  Theorem::Theorem(const Theorem &th) : d_thm(th.d_thm) {
171  if (d_thm & 0x1) {
172  DebugAssert(thm()->d_refcount > 0,
173  "Theorem(const Theorem&): refcount = "
174  + int2string(thm()->d_refcount));
175  thm()->d_refcount++;
176  // TRACE("theorem", "Theorem(Theorem&) => ", *this, "");
177  } else if (d_thm != 0) {
178  exprValue()->incRefcount();
179  }
180  }
181 
182  Theorem::Theorem(const Expr& e) : d_expr(e.d_expr)
183  {
184  d_expr->incRefcount();
185  }
186 
187  // Destructor
189  if (d_thm & 0x1) {
190  TheoremValue* tv = thm();
191  // TRACE("theorem", "~Theorem(", *this, ") {");
193  "~Theorem(): refcount = "
194  + int2string(tv->d_refcount));)
195  if((--tv->d_refcount) == 0) {
196  // TRACE_MSG("theorem", "~Theorem(): deleting");
197  MemoryManager* mm = tv->getMM();
198  delete tv;
199  mm->deleteData(tv);
200  }
201  }
202  else if (d_thm != 0) {
203  exprValue()->decRefcount();
204  }
205  }
206 
207  void Theorem::printx() const { getExpr().print(); }
209  void Theorem::pprintx() const { getExpr().pprint(); }
211  void Theorem::print() const { cout << toString() << endl; }
212 
213  // Test if we are running in a proof production mode and with assumptions
214  bool Theorem::withProof() const {
215  if (isRefl()) return exprValue()->d_em->getTM()->withProof();
216  return thm()->d_tm->withProof();
217  }
218 
220  if (isRefl()) return exprValue()->d_em->getTM()->withAssumptions();
221  return thm()->d_tm->withAssumptions();
222  }
223 
224  bool Theorem::isRewrite() const {
225  DebugAssert(!isNull(), "CVC3::Theorem::isRewrite(): we are Null");
226  return isRefl() || thm()->isRewrite();
227  }
228 
229  // Return the theorem value as an Expr
231  DebugAssert(!isNull(), "CVC3::Theorem::getExpr(): we are Null");
232  if (isRefl()) {
233  Expr e(exprValue());
234  if (e.isTerm()) return e.eqExpr(e);
235  else return e.iffExpr(e);
236  }
237  else return thm()->getExpr();
238  }
239 
240  const Expr& Theorem::getLHS() const {
241  DebugAssert(!isNull(), "CVC3::Theorem::getLHS: we are Null");
242  if (isRefl()) return *((Expr*)(&d_expr));
243  else return thm()->getLHS();
244  }
245 
246  const Expr& Theorem::getRHS() const {
247  DebugAssert(!isNull(), "CVC3::Theorem::getRHS: we are Null");
248  if (isRefl()) return *((Expr*)(&d_expr));
249  else return thm()->getRHS();
250  }
251 
252 // Return the assumptions.
253 // void Theorem::getAssumptions(Assumptions& a) const
254 // {
255 // a = getAssumptionsRef();
256 // }
257 
258 
259 void Theorem::getAssumptionsRec(set<Expr>& assumptions) const
260 {
261  if (isRefl() || isFlagged()) return;
262  setFlag();
263  if(isAssump()) {
264  assumptions.insert(getExpr());
265  }
266  else {
267  const Assumptions& a = getAssumptionsRef();
268  for(Assumptions::iterator i=a.begin(), iend=a.end(); i!=iend; ++i)
269  (*i).getAssumptionsRec(assumptions);
270  }
271 }
272 
273 
274 void Theorem::getLeafAssumptions(vector<Expr>& assumptions,
275  bool negate) const
276 {
277  if (isNull() || isRefl()) return;
278  set<Expr> assumpSet;
279  clearAllFlags();
280  getAssumptionsRec(assumpSet);
281  // Order assumptions by their creation time
282  for(set<Expr>::iterator i=assumpSet.begin(), iend=assumpSet.end();
283  i!=iend; ++i)
284  assumptions.push_back(negate ? (*i).negate() : *i);
285 }
286 
287 
288 void Theorem::GetSatAssumptionsRec(vector<Theorem>& assumptions) const
289 {
290  DebugAssert(!isRefl() && !isFlagged(), "Invariant violated");
291  setFlag();
292  Expr e = getExpr();
293  if (e.isAbsLiteral()) {
294  if (isAssump() ||
295  e.isRegisteredAtom() ||
296  (e.isNot() && e[0].isRegisteredAtom())) {
297  assumptions.push_back(*this);
298  return;
299  }
300  }
301  const Assumptions& a = getAssumptionsRef();
302  for (Assumptions::iterator i = a.begin(); i != a.end(); i++) {
303  if ((*i).isRefl() || (*i).isFlagged()) continue;
304  (*i).GetSatAssumptionsRec(assumptions);
305  }
306 }
307 
308 
309 void Theorem::GetSatAssumptions(vector<Theorem>& assumptions) const {
310  DebugAssert(!isRefl() && !isFlagged(), "Invariant violated");
311  setFlag();
312  const Assumptions& a = getAssumptionsRef();
313  for (Assumptions::iterator i = a.begin(); i != a.end(); i++) {
314  if ((*i).isRefl() || (*i).isFlagged()) continue;
315  (*i).GetSatAssumptionsRec(assumptions);
316  }
317 }
318 
319 
320 void Theorem::getAssumptionsAndCongRec(set<Expr>& assumptions,
321  vector<Expr>& congruences) const
322 {
323  if (isRefl() || isFlagged()) return;
324  setFlag();
325  if(isAssump()) {
326  assumptions.insert(getExpr());
327  }
328  else {
329  const Assumptions& a = getAssumptionsRef();
330  if (isSubst() && a.size() == 1) {
331  vector<Expr> hyp;
332  const Theorem& thm = *(a.begin());
333  thm.getAssumptionsAndCongRec(assumptions, congruences);
334  if (thm.isRewrite() && thm.getLHS().isTerm()
335  && thm.getLHS().isAtomic() && thm.getRHS().isAtomic() &&
336  !thm.isRefl()) {
337  hyp.push_back(!thm.getExpr());
338  }
339  else return;
340  const Expr& e = getExpr();
341  if (e.isAtomicFormula()) {
342  if (e[0] < e[1]) {
343  hyp.push_back(e[1].eqExpr(e[0]));
344  }
345  else {
346  hyp.push_back(e);
347  }
348  congruences.push_back(Expr(OR, hyp));
349  }
350  else if (e[0].isAtomicFormula() && !e[0].isEq()) {
351  hyp.push_back(!e[0]);
352  hyp.push_back(e[1]);
353  congruences.push_back(Expr(OR, hyp));
354  hyp.pop_back();
355  hyp.pop_back();
356  hyp.push_back(e[0]);
357  hyp.push_back(!e[1]);
358  congruences.push_back(Expr(OR, hyp));
359  }
360  }
361  else {
362  Assumptions::iterator i=a.begin(), iend=a.end();
363  for(; i!=iend; ++i)
364  (*i).getAssumptionsAndCongRec(assumptions, congruences);
365  }
366  }
367 }
368 
369 
370 void Theorem::getAssumptionsAndCong(vector<Expr>& assumptions,
371  vector<Expr>& congruences,
372  bool negate) const
373 {
374  if (isNull() || isRefl()) return;
375  set<Expr> assumpSet;
376  clearAllFlags();
377  getAssumptionsAndCongRec(assumpSet, congruences);
378  // Order assumptions by their creation time
379  for(set<Expr>::iterator i=assumpSet.begin(), iend=assumpSet.end();
380  i!=iend; ++i)
381  assumptions.push_back(negate ? (*i).negate() : *i);
382 }
383 
384 
386 {
387  DebugAssert(!isNull(), "CVC3::Theorem::getAssumptionsRef: we are Null");
388  if (!isRefl()) {
389  return thm()->getAssumptionsRef();
390  }
391  else return Assumptions::emptyAssump();
392 }
393 
394 
395  bool Theorem::isAssump() const {
396  DebugAssert(!isNull(), "CVC3::Theorem::isAssump: we are Null");
397  return isRefl() ? false : thm()->isAssump();
398  }
399 
400  // Return the proof of the theorem. If running without proofs,
401  // return the Null proof.
403  static Proof null;
404  DebugAssert(!isNull(), "CVC3::Theorem::getProof: we are Null");
405  if (isRefl()) {
406  return Proof(Expr(PF_APPLY,
407  exprValue()->d_em->newVarExpr("refl"),
408  Expr(exprValue())));
409  }
410  else if (withProof() == true)
411  return thm()->getProof();
412  else
413  return null;
414  }
415 
416  bool Theorem::isFlagged() const {
417  DebugAssert(!isNull(), "CVC3::Theorem::isFlagged: we are Null");
418  if (isRefl()) return exprValue()->d_em->getTM()->isFlagged((long)d_expr);
419  else return thm()->isFlagged();
420  }
421 
422  void Theorem::clearAllFlags() const {
423  DebugAssert(!isNull(), "CVC3::Theorem::clearAllFlags: we are Null");
424  if (isRefl()) {
426  } else thm()->clearAllFlags();
427  }
428 
429  void Theorem::setFlag() const {
430  DebugAssert(!isNull(), "CVC3::Theorem::setFlag: we are Null");
431  if (isRefl()) exprValue()->d_em->getTM()->setFlag((long)d_expr);
432  else thm()->setFlag();
433  }
434 
435  void Theorem::setCachedValue(int value) const {
436  DebugAssert(!isNull(), "CVC3::Theorem::setCachedValue: we are Null");
437  if (isRefl()) exprValue()->d_em->getTM()->setCachedValue((long)d_expr, value);
438  else thm()->setCachedValue(value);
439  }
440 
442  DebugAssert(!isNull(), "CVC3::Theorem::getCachedValue: we are Null");
443  if (isRefl()) return exprValue()->d_em->getTM()->getCachedValue((long)d_expr);
444  return thm()->getCachedValue();
445  }
446 
447  void Theorem::setSubst() const {
448  DebugAssert(!isNull() && !isRefl(), "CVC3::Theorem::setSubst: invalid thm");
449  thm()->setSubst();
450  }
451 
452  bool Theorem::isSubst() const {
453  DebugAssert(!isNull(), "CVC3::Theorem::isSubst: we are Null");
454  if (isRefl()) return false;
455  return thm()->isSubst();
456  }
457 
458  void Theorem::setExpandFlag(bool val) const {
459  DebugAssert(!isNull(), "CVC3::Theorem::setExpandFlag: we are Null");
460  if (isRefl()) exprValue()->d_em->getTM()->setExpandFlag((long)d_expr, val);
461  thm()->setExpandFlag(val);
462  }
463 
464  bool Theorem::getExpandFlag() const {
465  DebugAssert(!isNull(), "CVC3::Theorem::getExpandFlag: we are Null");
466  if (isRefl()) return exprValue()->d_em->getTM()->getExpandFlag((long)d_expr);
467  return thm()->getExpandFlag();
468  }
469 
470  void Theorem::setLitFlag(bool val) const {
471  DebugAssert(!isNull(), "CVC3::Theorem::setLitFlag: we are Null");
472  if (isRefl()) exprValue()->d_em->getTM()->setLitFlag((long)d_expr, val);
473  thm()->setLitFlag(val);
474  }
475 
476  bool Theorem::getLitFlag() const {
477  DebugAssert(!isNull(), "CVC3::Theorem::getLitFlag: we are Null");
478  if (isRefl()) return exprValue()->d_em->getTM()->getLitFlag((long)d_expr);
479  return thm()->getLitFlag();
480  }
481 
482  bool Theorem::isAbsLiteral() const {
483  return getExpr().isAbsLiteral();
484  }
485 
486  int Theorem::getScope() const {
487  DebugAssert(!isNull(), "CVC3::Theorem::getScope: we are Null");
488  return isRefl() ? 0 : thm()->getScope();
489  }
490 
491  unsigned Theorem::getQuantLevel() const {
492  DebugAssert(!isNull(), "CVC3::Theorem::getQuantLevel: we are Null");
493  TRACE("quant-level", "isRefl? ", isRefl(), "");
494  return isRefl() ? 0 : thm()->getQuantLevel();
495  }
496 
497  unsigned Theorem::getQuantLevelDebug() const {
498  DebugAssert(!isNull(), "CVC3::Theorem::getQuantLevel: we are Null");
499  TRACE("quant-level", "isRefl? ", isRefl(), "");
500  return isRefl() ? 0 : thm()->getQuantLevelDebug();
501  }
502 
503 
504  void Theorem::setQuantLevel(unsigned level) {
505  DebugAssert(!isNull(), "CVC3::Theorem::setQuantLevel: we are Null");
506  // DebugAssert(!isRefl(), "CVC3::Theorem::setQuantLevel: we are Refl");
507  if (isRefl()) return;
508  thm()->setQuantLevel(level);
509  }
510 
511  size_t Theorem::hash() const {
512  static std::hash<long int> h;
513  return h(d_thm);
514  }
515 
516  void Theorem::recursivePrint(int& i) const {
519  if (!isAssump()) {
520  for (; it != iend; ++it) {
521  if (it->isFlagged()) continue;
522  it->recursivePrint(i);
523  it->setFlag();
524  }
525  }
526 
527  setCachedValue(i++);
528  cout << "[" << getCachedValue()
529  << "]@" << getScope() << "\tTheorem: {";
530 
531  if (isAssump()) {
532  cout << "assump";
533  }
534  else if (getAssumptionsRef().empty()) {
535  cout << "empty";
536  }
537  else {
538  for (it = getAssumptionsRef().begin(); it != iend; ++it) {
539  if (it != getAssumptionsRef().begin()) cout << ", ";
540  cout << "[" << it->getCachedValue() << "]" ;
541  }
542  }
543  cout << "}" << endl << "\t\t|- " << getExpr();
544  if (isSubst()) cout << " [[Subst]]";
545  cout << endl;
546  }
547 
548 
549  // Return the scope level at which this theorem was created
550 // int Theorem::getScope() const {
551 // DebugAssert(!isNull(), "CVC3::Theorem::getScope: we are Null");
552 // return thm()->getScope();
553 // }
554 
555 // Assumptions Theorem::getUserAssumptions() const {
556 // ExprMap<Theorem> em;
557 // Assumptions a = getAssumptionsCopy();
558 
559 // collectAssumptions(a, em);
560 
561 // return a;
562 // }
563 
564 // void collectAssumptions(Assumptions &a, ExprMap<Theorem> em ) const {
565 // if (isAssump()) {
566 // // cache?
567 // return;
568 // }
569 
570 // const Assumptions a2 = thm()->getAssumptions();
571 // a.add(a2);
572 // Assumptions::iterator a2begin = a2.begin();
573 // const Assumptions::iterator a2end = a2.end();
574 
575 
576 // }
577 
578 
579  // Printing Theorem
580  ostream& Theorem::print(ostream& os, const string& name) const {
581  if(isNull()) return os << name << "(Null)";
582  ExprManager *em = getExpr().getEM();
583  if (isRefl()) os << getExpr();
584  else if (withAssumptions()) {
585  em->incIndent(name.size()+2);
586  os << name << "([" << thm() << "#" << thm()->d_refcount << "]@"
587  << getScope() << "\n[";
588  if(isAssump()) os << "Assump";
589  else {
590  if(thm()->d_tm->getFlags()["print-assump"].getBool()
591  && em->isActive())
592  os << getAssumptionsRef();
593  else
594  os << "<assumptions>";
595  }
596  os << "]\n |--- ";
597  em->indent(7);
598  if(em->isActive()) os << getExpr();
599  else os << "(being destructed)";
600  if(withProof())
601  os << "\n Proof = " << getProof();
602  return os << ")";
603  }
604  else {
605  em->incIndent(name.size()+1);
606  os << name << "(";
607  if(em->isActive()) os << getExpr();
608  else os << "being destructed";
609  return os << ")";
610  }
611  return os;
612  }
613 
614 
615 } // end of namespace CVC3
void setCachedValue(int value) const
Check if the flag attribute is set.
Definition: theorem.cpp:435
bool isIff() const
Definition: expr.h:424
bool getExpandFlag() const
Check the "expand" attribute.
Definition: theorem.cpp:464
bool isEq() const
Definition: expr.h:419
void setSubst() const
Set flag stating that theorem is an instance of substitution.
Definition: theorem.cpp:447
bool isAtomic() const
Test if e is atomic.
Definition: expr.cpp:550
ExprValue * d_expr
The value. This is the only data member in this class.
Definition: expr.h:197
Data structure of expressions in CVC3.
Definition: expr.h:133
ExprManager * getEM() const
Definition: expr.h:1156
void clearAllFlags() const
Clear the flag attribute in all the theorems.
Definition: theorem.cpp:422
int getCachedValue() const
virtual const Expr & getExpr() const
bool isNull() const
Definition: proof.h:47
void recursivePrint(int &i) const
Definition: theorem.cpp:516
int compare(const Expr &e1, const Expr &e2)
Definition: expr.cpp:597
unsigned size() const
Definition: assumptions.h:94
TheoremValue * thm() const
Definition: theorem.h:133
void pprintnodag() const
Pretty-print without dagifying.
Definition: expr.cpp:383
virtual const Expr & getLHS() const
bool isAssump() const
int incIndent(int n, bool permanent=false)
Increment the current transient indentation by n.
bool withAssumptions() const
Definition: theorem.cpp:219
bool isActive()
Check if the ExprManager is still active (clear() was not called)
void getLeafAssumptions(std::vector< Expr > &assumptions, bool negate=false) const
Definition: theorem.cpp:274
ExprValue * exprValue() const
Definition: theorem.h:132
void printnodag() const
Print the expression as AST without dagifying.
Definition: expr.cpp:394
Expr eqExpr(const Expr &right) const
Definition: expr.h:929
MemoryManager * getMM() const
#define DebugAssert(cond, str)
Definition: debug.h:408
bool isTerm() const
Test if e is a term (as opposed to a predicate/formula)
Definition: expr.h:1021
Theorem & operator=(const Theorem &th)
Definition: theorem.cpp:91
size_t hash() const
Definition: theorem.cpp:511
virtual const Assumptions & getAssumptionsRef() const =0
int getScope() const
Definition: theorem.cpp:486
iterator end() const
Definition: assumptions.h:152
CVC3::ExprStream & endl(CVC3::ExprStream &os)
Print the end-of-line.
void setExpandFlag(bool val) const
Set the "expand" attribute.
Definition: theorem.cpp:458
int getCachedValue() const
Check if the flag attribute is set.
Definition: theorem.cpp:441
int getCachedValue(long ptr)
void getAssumptionsAndCongRec(std::set< Expr > &assumptions, std::vector< Expr > &congruences) const
Definition: theorem.cpp:320
void printxnodag() const
Definition: theorem.cpp:208
bool isNot() const
Definition: expr.h:420
bool isFlagged(long ptr)
bool withProof() const
Definition: theorem.cpp:214
iterator begin() const
Definition: assumptions.h:151
#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()
void setQuantLevel(unsigned level)
Set the quantification level for this theorem.
Definition: theorem.cpp:504
TheoremManager * getTM() const
Fetch the TheoremManager.
Definition: expr_manager.h:331
std::string toString() const
Definition: theorem.h:404
bool isFlagged() const
intptr_t d_thm
Definition: theorem.h:91
void print(InputLanguage lang, bool dagify=true) const
Print the expression in the specified format.
Definition: expr.cpp:362
MemoryManager * getRWMM() const
void setLitFlag(bool val) const
Set the "literal" attribute.
Definition: theorem.cpp:470
int compareByPtr(const Theorem &t1, const Theorem &t2)
Definition: theorem.cpp:83
void pprintxnodag() const
Definition: theorem.cpp:210
bool isFlagged() const
Check if the flag attribute is set.
Definition: theorem.cpp:416
virtual const Expr & getRHS() const
Expr iffExpr(const Expr &right) const
Definition: expr.h:965
unsigned getQuantLevel() const
Return quantification level for this theorem.
Definition: theorem.cpp:491
void setExpandFlag(long ptr, bool value)
bool getLitFlag(long ptr)
Definition: kinds.h:68
std::string int2string(int n)
Definition: cvc_util.h:46
unsigned getQuantLevelDebug() const
Definition: theorem.cpp:497
const Expr & getRHS() const
Definition: theorem.cpp:246
bool isAbsLiteral() const
Check if the theorem is a literal.
Definition: theorem.cpp:482
void incRefcount()
Increment reference counter.
Definition: expr_value.h:142
#define IF_DEBUG(code)
Definition: debug.h:406
Proof getProof() const
Definition: theorem.cpp:402
void setCachedValue(long ptr, int value)
const Assumptions & getAssumptionsRef() const
Definition: theorem.cpp:385
Expression Manager.
Definition: expr_manager.h:58
void printx() const
Definition: theorem.cpp:207
unsigned d_refcount
How many pointers to this theorem value.
Definition: theorem_value.h:74
virtual void deleteData(void *d)=0
Expr getExpr() const
Definition: theorem.cpp:230
void getAssumptionsRec(std::set< Expr > &assumptions) const
Definition: theorem.cpp:259
bool isNull() const
Definition: theorem.h:164
ExprValue * d_expr
Definition: theorem.h:92
void setLitFlag(bool val)
void GetSatAssumptionsRec(std::vector< Theorem > &assumptions) const
Definition: theorem.cpp:288
int indent() const
Get initial indentation.
Definition: expr_manager.h:354
void decRefcount()
Decrement reference counter.
Definition: expr_value.h:145
virtual MemoryManager * getMM()=0
void getAssumptionsAndCong(std::vector< Expr > &assumptions, std::vector< Expr > &congruences, bool negate=false) const
Definition: theorem.cpp:370
ExprManager * d_em
Our expr. manager.
Definition: expr_value.h:132
bool isRegisteredAtom() const
Definition: expr.h:1378
unsigned getQuantLevel()
unsigned getQuantLevelDebug()
void setQuantLevel(unsigned level)
bool isAbsLiteral() const
Test if e is an abstract literal.
Definition: expr.h:406
bool getExpandFlag(long ptr)
void print() const
Definition: theorem.cpp:211
bool isRefl() const
Definition: theorem.h:171
const Expr & getLHS() const
Definition: theorem.cpp:240
void pprintx() const
Definition: theorem.cpp:209
Iterator for the Assumptions: points to class Theorem.
Definition: assumptions.h:118
void pprint() const
Pretty-print the expression.
Definition: expr.cpp:373
void setCachedValue(int value)
bool isAtomicFormula() const
Test if e is an atomic formula.
Definition: expr.cpp:571
bool isSubst() const
Is theorem an instance of substitution.
Definition: theorem.cpp:452
void GetSatAssumptions(std::vector< Theorem > &assumptions) const
Definition: theorem.cpp:309
Definition: kinds.h:99
bool isRewrite() const
Definition: theorem.cpp:224
bool isAssump() const
Definition: theorem.cpp:395
void setExpandFlag(bool val)
static const Assumptions & emptyAssump()
Definition: assumptions.h:83
TheoremManager * d_tm
Theorem Manager.
Definition: theorem_value.h:65
virtual bool isRewrite() const
bool getLitFlag() const
Check the "literal" attribute.
Definition: theorem.cpp:476
void setFlag(long ptr)
void setFlag() const
Set the flag attribute.
Definition: theorem.cpp:429
void setLitFlag(long ptr, bool value)