CVC3  2.4.1
common_theorem_producer.cpp
Go to the documentation of this file.
1 /*****************************************************************************/
2 /*!
3  *\file common_theorem_producer.cpp
4  *\brief Implementation of common proof rules
5  *
6  * Author: Clark Barrett
7  *
8  * Created: Wed Jan 11 16:10:15 2006
9  *
10  * <hr>
11  *
12  * License to use, copy, modify, sell and/or distribute this software
13  * and its documentation for any purpose is hereby granted without
14  * royalty, subject to the terms and conditions defined in the \ref
15  * LICENSE file provided with this distribution.
16  *
17  * <hr>
18  *
19  */
20 /*****************************************************************************/
21 
22 
23 // This code is trusted
24 #define _CVC3_TRUSTED_
25 
26 
28 
29 
30 using namespace CVC3;
31 using namespace std;
32 
33 
34 // The trusted method of TheoremManager which creates this theorem producer
36  return new CommonTheoremProducer(this);
37 }
38 
39 
41  : TheoremProducer(tm),
42  d_skolemized_thms(tm->getCM()->getCurrentContext()),
43  d_skolemVars(tm->getCM()->getCurrentContext())
44 {}
45 
46 
47 ////////////////////////////////////////////////////////////////////////
48 // TCC rules (3-valued logic)
49 ////////////////////////////////////////////////////////////////////////
50 
51 // G1 |- phi G2 |- D_phi
52 // -------------------------
53 // G1,G2 |-_3 phi
55 CommonTheoremProducer::queryTCC(const Theorem& phi, const Theorem& D_phi) {
56  Proof pf;
57 // if(CHECK_PROOFS)
58 // CHECK_SOUND(D_phi.getExpr() == d_core->getTCC(phi.getExpr()),
59 // "CoreTheoremProducer::queryTCC: "
60 // "bad TCC for a formula:\n\n "
61 // +phi.getExpr().toString()
62 // +"\n\n TCC must be the following:\n\n "
63 // +d_core->getTCC(phi.getExpr()).toString()
64 // +"\n\nBut given this as a TCC:\n\n "
65 // +D_phi.getExpr().toString());
67  a.add(D_phi);
68  if(withProof()) {
69  vector<Expr> args;
70  vector<Proof> pfs;
71  args.push_back(phi.getExpr());
72  args.push_back(D_phi.getExpr());
73  pfs.push_back(phi.getProof());
74  pfs.push_back(D_phi.getProof());
75  pf = newPf("queryTCC", args, pfs);
76  }
77  return newTheorem3(phi.getExpr(), a, pf);
78 }
79 
80 
81 // G0,a1,...,an |-_3 phi G1 |- D_a1 ... Gn |- D_an
82 // -------------------------------------------------
83 // G0,G1,...,Gn |-_3 (a1 & ... & an) -> phi
86  const std::vector<Expr>& assump,
87  const vector<Theorem>& tccs) {
88  bool checkProofs(CHECK_PROOFS);
89  // This rule only makes sense when runnnig with assumptions
90  if(checkProofs) {
92  "implIntro3: called while running without assumptions");
93  }
94 
95  const Assumptions& phiAssump = phi.getAssumptionsRef();
96 
97  if(checkProofs) {
98  CHECK_SOUND(assump.size() == tccs.size(),
99  "implIntro3: number of assumptions ("
100  +int2string(assump.size())+") and number of TCCs ("
101  +int2string(tccs.size())
102  +") does not match");
103  for(size_t i=0; i<assump.size(); i++) {
104  const Theorem& thm = phiAssump[assump[i]];
105  CHECK_SOUND(!thm.isNull() && thm.isAssump(),
106  "implIntro3: this is not an assumption of phi:\n\n"
107  " a["+int2string(i)+"] = "+assump[i].toString()
108  +"\n\n phi = "+phi.getExpr().toString());
109 // CHECK_SOUND(tccs[i].getExpr() == d_core->getTCC(assump[i]),
110 // "implIntro3: Assumption does not match its TCC:\n\n"
111 // " a["+int2string(i)+"] = "+assump[i].toString()
112 // +" TCC(a["+int2string(i)+"]) = "
113 // +d_core->getTCC(assump[i]).toString()
114 // +"\n\n tccs["+int2string(i)+"] = "
115 // +tccs[i].getExpr().toString());
116  }
117  }
118 
119  // Proof compaction: trivial derivation
120  if(assump.size() == 0) return phi;
121 
122  Assumptions a(phiAssump - assump);
123  Assumptions b(tccs);
124  a.add(b);
125  Proof pf;
126  if(withProof()) {
127  vector<Proof> u; // Proof labels for assumptions
128  for(vector<Expr>::const_iterator i=assump.begin(), iend=assump.end();
129  i!=iend; ++i) {
130  const Theorem& t = phiAssump[*i];
131  u.push_back(t.getProof());
132  }
133  // Arguments to the proof rule:
134  // impl_intro_3(phi, a1,...,an,tcc1,...tccn,pf_tcc1,...pf_tccn,
135  // [lambda(a1,...,an): pf_phi])
136  vector<Expr> args;
137  vector<Proof> pfs;
138  args.push_back(phi.getExpr());
139  args.insert(args.end(), assump.begin(), assump.end());
140  for(vector<Theorem>::const_iterator i=tccs.begin(), iend=tccs.end();
141  i!=iend; ++i) {
142  args.push_back(i->getExpr());
143  pfs.push_back(i->getProof());
144  }
145  // Lambda-abstraction of pf_phi
146  pfs.push_back(newPf(u, assump, phi.getProof()));
147  pf = newPf("impl_intro_3", args, pfs);
148  }
149  Expr conj(andExpr(assump));
150  return newTheorem3(conj.impExpr(phi.getExpr()), a, pf);
151 }
152 
153 
155  // TRACE("assump", "assumpRule(", e, ")");
156  Proof pf;
157  if(withProof()) pf = newLabel(e);
158  return newAssumption(e, pf, scope);
159 }
160 
161 
163  return newReflTheorem(a);
164 }
165 
166 
167 // ==> (a == a) IFF TRUE
169  if(CHECK_PROOFS)
170  CHECK_SOUND((t.isEq() || t.isIff()) && t[0] == t[1],
171  "rewriteReflexivity: wrong expression: "
172  + t.toString());
173  Proof pf;
174  if(withProof()) {
175  if(t.isEq()) {
176  DebugAssert(!t[0].getType().isNull(),
177  "rewriteReflexivity: t[0] has no type: "
178  + t[0].toString());
179  pf = newPf("rewrite_eq_refl", t[0].getType().getExpr(), t[0]);
180  } else
181  pf = newPf("rewrite_iff_refl", t[0]);
182  }
183  return newRWTheorem(t, d_em->trueExpr(), Assumptions::emptyAssump(), pf);
184 }
185 
186 
188  if(CHECK_PROOFS)
189  CHECK_SOUND(a1_eq_a2.isRewrite(),
190  ("CVC3::CommonTheoremProducer: "
191  "theorem is not an equality or iff:\n "
192  + a1_eq_a2.getExpr().toString()).c_str());
193  const Expr& a1 = a1_eq_a2.getLHS();
194  const Expr& a2 = a1_eq_a2.getRHS();
195 
196  Proof pf;
197  /////////////////////////////////////////////////////////////////////////
198  //// Proof compaction
199  /////////////////////////////////////////////////////////////////////////
200  // If a1 == a2, use reflexivity
201  if(a1 == a2) return reflexivityRule(a1);
202  // Otherwise, do the work
203  if(withProof()) {
204  Type t = a1.getType();
205  // Check the types
206  IF_DEBUG(a1_eq_a2.getExpr().getType();)
207  bool isEquality = !t.isBool();
208  if(isEquality) {
209  vector<Expr> args;
210  args.push_back(t.getExpr());
211  args.push_back(a1);
212  args.push_back(a2);
213  pf = newPf("eq_symm", args, a1_eq_a2.getProof());
214  } else
215  pf = newPf("iff_symm", a1, a2, a1_eq_a2.getProof());
216  }
217  return newRWTheorem(a2, a1, Assumptions(a1_eq_a2), pf);
218 }
219 
220 
222  bool isIff = a1_eq_a2.isIff();
223  if(CHECK_PROOFS)
224  CHECK_SOUND(a1_eq_a2.isEq() || isIff, "rewriteUsingSymmetry precondition violated");
225  const Expr& a1 = a1_eq_a2[0];
226  const Expr& a2 = a1_eq_a2[1];
227  // Proof compaction: if a1 == a2, use reflexivity
228  if(a1 == a2) return reflexivityRule(a1_eq_a2);
229  // Otherwise, do the work
230  Proof pf;
231  if(withProof()) {
232  Type t = a1.getType();
233  DebugAssert(!t.isNull(),
234  "rewriteUsingSymmetry: a1 has no type: " + a1.toString());
235  if(isIff)
236  pf = newPf("rewrite_iff_symm", a1, a2);
237  else {
238  pf = newPf("rewrite_eq_symm", t.getExpr(), a1, a2);
239  }
240  }
241  return newRWTheorem(a1_eq_a2, isIff ? a2.iffExpr(a1) : a2.eqExpr(a1), Assumptions::emptyAssump(), pf);
242 }
243 
244 
246  const Theorem& a2_eq_a3) {
247  DebugAssert(!a1_eq_a2.isNull(), "transitivityRule()");
248  DebugAssert(!a2_eq_a3.isNull(), "transitivityRule()");
249  if(CHECK_PROOFS) {
250  CHECK_SOUND(a1_eq_a2.isRewrite() && a2_eq_a3.isRewrite(),
251  "CVC3::CommonTheoremProducer::transitivityRule:\n "
252  "Wrong premises: first = "
253  + a1_eq_a2.getExpr().toString() + ", second = "
254  + a2_eq_a3.getExpr().toString());
255  CHECK_SOUND(a1_eq_a2.getRHS() == a2_eq_a3.getLHS(),
256  "CVC3::CommonTheoremProducer::transitivityRule:\n "
257  "Wrong premises: first = "
258  + a1_eq_a2.getExpr().toString() + ", second = "
259  + a2_eq_a3.getExpr().toString());
260  }
261  const Expr& a1 = a1_eq_a2.getLHS();
262  const Expr& a2 = a1_eq_a2.getRHS();
263  const Expr& a3 = a2_eq_a3.getRHS();
264 
265  /////////////////////////////////////////////////////////////////////////
266  //// Proof compaction
267  /////////////////////////////////////////////////////////////////////////
268  // if a1 == a3, use reflexivity (and lose all assumptions)
269  if(a1 == a3) return reflexivityRule(a1);
270  // if a1 == a2, or if a2 == a3, use only the non-trivial part
271  if(a1 == a2) return a2_eq_a3;
272  if(a2 == a3) return a1_eq_a2;
273 
274  ////////////////////////////////////////////////////////////////////////
275  //// No shortcuts. Do the work.
276  ////////////////////////////////////////////////////////////////////////
277 
278  Proof pf;
279  Assumptions a(a1_eq_a2, a2_eq_a3);
280  // Build the proof
281  if(withProof()) {
282  Type t = a1.getType();
283  bool isEquality = (!t.isBool());
284  string name((isEquality)? "eq_trans" : "iff_trans");
285  vector<Expr> args;
286  vector<Proof> pfs;
287  DebugAssert(!t.isNull(), "transitivityRule: "
288  "Type is not computed for a1: " + a1.toString());
289  // Type argument is needed only for equality
290  if(isEquality) args.push_back(t.getExpr());
291  args.push_back(a1);
292  args.push_back(a2);
293  args.push_back(a3);
294  pfs.push_back(a1_eq_a2.getProof());
295  pfs.push_back(a2_eq_a3.getProof());
296  pf = newPf(name, args, pfs);
297  }
298  return newRWTheorem(a1, a3, a, pf);
299 }
300 
301 
303  const Theorem& thm) {
304  IF_DEBUG
305  (static DebugTimer
306  accum0(debugger.timer("substitutivityRule0 time"));
307  static DebugTimer tmpTimer(debugger.newTimer());
308  static DebugCounter count(debugger.counter("substitutivityRule0 calls"));
309  debugger.setCurrentTime(tmpTimer);
310  count++;)
311 
312  // Check that t is c == d or c IFF d
313  if(CHECK_PROOFS) {
314  CHECK_SOUND(e.arity() == 1 && e[0] == thm.getLHS(),
315  "Unexpected use of substitutivityRule0");
316  CHECK_SOUND(thm.isRewrite(),
317  "CVC3::CommonTheoremProducer::substitutivityRule0:\n "
318  "premis is not an equality or IFF: "
319  + thm.getExpr().toString()
320  + "\n expr = " + e.toString());
321  }
322  Expr e2(e.getOp(), thm.getRHS());
323  Proof pf;
324  if(withProof())
325  pf = newPf("basic_subst_op0",e, e2,thm.getProof());
326  Theorem res = newRWTheorem(e, e2, Assumptions(thm), pf);
327  if (!res.isRefl()) res.setSubst();
328  return res;
329 }
330 
331 
333  const Theorem& thm1,
334  const Theorem& thm2) {
335  IF_DEBUG
336  (static DebugTimer
337  accum0(debugger.timer("substitutivityRule1 time"));
338  static DebugTimer tmpTimer(debugger.newTimer());
339  static DebugCounter count(debugger.counter("substitutivityRule1 calls"));
340  debugger.setCurrentTime(tmpTimer);
341  count++;)
342 
343  // Check that t is c == d or c IFF d
344  if(CHECK_PROOFS) {
345  CHECK_SOUND(e.arity() == 2 && e[0] == thm1.getLHS() &&
346  e[1] == thm2.getLHS(),
347  "Unexpected use of substitutivityRule1");
348  CHECK_SOUND(thm1.isRewrite(),
349  "CVC3::CommonTheoremProducer::substitutivityRule1:\n "
350  "premis is not an equality or IFF: "
351  + thm1.getExpr().toString()
352  + "\n expr = " + e.toString());
353  CHECK_SOUND(thm2.isRewrite(),
354  "CVC3::CommonTheoremProducer::substitutivityRule1:\n "
355  "premis is not an equality or IFF: "
356  + thm2.getExpr().toString()
357  + "\n expr = " + e.toString());
358  }
359  Expr e2(e.getOp(), thm1.getRHS(), thm2.getRHS());
360  Proof pf;
361  if(withProof()) {
362  vector<Proof> pfs;
363  pfs.push_back(thm1.getProof());
364  pfs.push_back(thm2.getProof());
365  pf = newPf("basic_subst_op1", e, e2, pfs);
366  }
367  Theorem res = newRWTheorem(e, e2, Assumptions(thm1, thm2), pf);
368  if (!res.isRefl()) res.setSubst();
369  return res;
370 }
371 
372 
374  const vector<Theorem>& thms) {
375  IF_DEBUG
376  (static DebugTimer
377  accum0(debugger.timer("substitutivityRule time"));
378  static DebugTimer tmpTimer(debugger.newTimer());
379  static DebugCounter count(debugger.counter("substitutivityRule calls"));
380  debugger.setCurrentTime(tmpTimer);
381  count++;)
382  // Check for trivial case: no theorems, return (op == op)
383  unsigned size(thms.size());
384  if(size == 0)
385  return reflexivityRule(d_tm->getEM()->newLeafExpr(op));
386  // Check that theorems are of the form c_i == d_i and collect
387  // vectors of c_i's and d_i's and the vector of proofs
388  vector<Expr> c, d;
389  vector<Proof> pfs;
390  // Reserve memory for argument vectors. Do not reserve memory for
391  // pfs, they are rarely used and slow anyway.
392  c.reserve(size); d.reserve(size);
393  for(vector<Theorem>::const_iterator i = thms.begin(), iend = thms.end();
394  i != iend; ++i) {
395  // Check that t is c == d or c IFF d
396  if(CHECK_PROOFS)
397  CHECK_SOUND(i->isRewrite(),
398  "CVC3::CommonTheoremProducer::substitutivityRule:\n "
399  "premis is not an equality or IFF: "
400  + i->getExpr().toString()
401  + "\n op = " + op.toString());
402  // Collect the pieces
403  c.push_back(i->getLHS());
404  d.push_back(i->getRHS());
405  if(withProof()) pfs.push_back(i->getProof());
406  }
407  Expr e1(op, c), e2(op, d);
408  // Proof compaction: if e1 == e2, use reflexivity
409  if(e1 == e2) return reflexivityRule(e1);
410  // Otherwise, do the work
411  Assumptions a(thms);
412  Proof pf;
413  if(withProof())
414  // FIXME: this rule is not directly expressible in flea
415  pf = newPf("basic_subst_op",e1,e2,pfs);
416  Theorem res = newRWTheorem(e1, e2, a, pf);
417  IF_DEBUG(debugger.setElapsed(tmpTimer);
418  accum0 += tmpTimer;)
419  res.setSubst();
420  return res;
421 }
422 
423 
425  const vector<unsigned>& changed,
426  const vector<Theorem>& thms) {
427  IF_DEBUG
428  (static DebugTimer
429  accum0(debugger.timer("substitutivityRule2 time"));
430  static DebugTimer tmpTimer(debugger.newTimer());
431  static DebugCounter count(debugger.counter("substitutivityRule2 calls"));
432  debugger.setCurrentTime(tmpTimer);
433  count++;)
434  DebugAssert(changed.size() > 0, "substitutivityRule2 should not be called");
435  DebugAssert(changed.size() == thms.size(), "substitutivityRule2: wrong args");
436 
437  // Check that theorems are of the form c_i == d_i and collect
438  // vectors of c_i's and d_i's and the vector of proofs
439  unsigned size = e.arity();
440  if (size == 1) return substitutivityRule(e, thms.back());
441  unsigned csize = changed.size();
442  if (size == 2) {
443  if (csize == 2) return substitutivityRule(e, thms[0], thms[1]);
444  if (changed[0] == 0) {
445  return substitutivityRule(e, thms[0], reflexivityRule(e[1]));
446  }
447  else {
448  return substitutivityRule(e, reflexivityRule(e[0]), thms[0]);
449  }
450  }
451  DebugAssert(size >= csize, "Bad call to substitutivityRule2");
452 
453  vector<Expr> c;
454  bool checkProofs(CHECK_PROOFS);
455  for(unsigned j = 0, k = 0; k < size; ++k) {
456  if (j == csize || changed[j] != k) {
457  c.push_back(e[k]);
458  continue;
459  }
460  // Check that t is c == d or c IFF d
461  if(checkProofs)
462  CHECK_SOUND(thms[j].isRewrite() && thms[j].getLHS() == e[k],
463  "CVC3::CommonTheoremProducer::substitutivityRule:\n "
464  "premis is not an equality or IFF: "
465  + thms[j].getExpr().toString()
466  + "\n e = " + e.toString());
467  // Collect the pieces
468  c.push_back(thms[j].getRHS());
469  ++j;
470  }
471  Expr e2(e.getOp(), c);
472  IF_DEBUG(if(e == e2) {
473  ostream& os = debugger.getOS();
474  os << "substitutivityRule2: e = " << e << "\n e2 = " << e2
475  << "\n changed kids: [\n";
476  for(unsigned j=0; j<changed.size(); j++)
477  os << " (" << changed[j] << ") " << thms[j] << "\n";
478  os << "]\n";
479  })
480  DebugAssert(e != e2,
481  "substitutivityRule2 should not be called in this case:\n"
482  "e = "+e.toString());
483 
484  Proof pf;
485  Assumptions a(thms);
486  if(withProof()) {
487  vector<Proof> pfs;
488  for(vector<Theorem>::const_iterator i = thms.begin(), iend = thms.end();
489  i != iend; ++i) {
490  // Check that t is c == d or c IFF d
491  if(CHECK_PROOFS)
492  CHECK_SOUND(i->isRewrite(),
493  "CVC3::CommonTheoremProducer::substitutivityRule:\n "
494  "premis is not an equality or IFF: "
495  + i->getExpr().toString());
496  // + "\n op = " + ((Op) e.getOp).toString());
497  pfs.push_back(i->getProof());
498  }
499  pf = newPf("optimized_subst_op",e,e2,pfs);
500  }
501  Theorem res = newRWTheorem(e, e2, a, pf);
502  IF_DEBUG(debugger.setElapsed(tmpTimer);
503  accum0 += tmpTimer;)
504  if (!res.isRefl()) res.setSubst();
505  return res;
506 }
507 
508 
510  const int changed,
511  const Theorem& thm)
512 {
513  // Get the arity of the expression
514  int size = e.arity();
515 
516  // The changed must be within the arity
517  DebugAssert(size >= changed, "Bad call to substitutivityRule");
518 
519  // Check that t is c == d or c IFF d
520  if(CHECK_PROOFS)
521  CHECK_SOUND(thm.isRewrite() && thm.getLHS() == e[changed], "CVC3::CommonTheoremProducer::substitutivityRule:\n "
522  "premise is not an equality or IFF: " + thm.getExpr().toString() + "\n" +
523  "e = " + e.toString());
524 
525  // Collect the new sub-expressions
526  vector<Expr> c;
527  for(int k = 0; k < size; ++ k)
528  if (k != changed) c.push_back(e[k]);
529  else c.push_back(thm.getRHS());
530 
531  // Construct the new expression
532  Expr e2(e.getOp(), c);
533 
534  // Check if they are the same
535  IF_DEBUG(if(e == e2) {
536  ostream& os = debugger.getOS();
537  os << "substitutivityRule: e = " << e << "\n e2 = " << e2 << endl;
538  })
539 
540  // The new expressions must not be equal
541  DebugAssert(e != e2, "substitutivityRule should not be called in this case:\ne = "+e.toString());
542 
543  // Construct the proof object
544  Proof pf;
545  Assumptions a(thm);
546  if(withProof()) {
547  // Check that t is c == d or c IFF d
548  if(CHECK_PROOFS)
549  CHECK_SOUND(thm.isRewrite(), "CVC3::CommonTheoremProducer::substitutivityRule:\npremise is not an equality or IFF: " + thm.getExpr().toString());
550  pf = newPf("optimized_subst_op2",e,e2,thm.getProof());
551  }
552 
553  // Return the resulting theorem
554  Theorem res = newRWTheorem(e, e2, a, pf);;
555  res.setSubst();
556  return res;
557 }
558 
559 
560 // |- e, |- !e ==> |- FALSE
562  const Theorem& not_e) {
563  Proof pf;
564  if(CHECK_PROOFS)
565  CHECK_SOUND(!e.getExpr() == not_e.getExpr(),
566  "CommonTheoremProducer::contraditionRule: "
567  "theorems don't match:\n e = "+e.toString()
568  +"\n not_e = "+not_e.toString());
569  Assumptions a(e, not_e);
570  if(withProof()) {
571  vector<Proof> pfs;
572  pfs.push_back(e.getProof());
573  pfs.push_back(not_e.getProof());
574  pf = newPf("contradition", e.getExpr(), pfs);
575  }
576  return newTheorem(d_em->falseExpr(), a, pf);
577 }
578 
579 
581 {
582  Proof pf;
583  if (withProof()) {
584  pf = newPf("excludedMiddle", e);
585  }
586  return newTheorem(e.orExpr(!e), Assumptions::emptyAssump(), pf);
587 }
588 
589 
590 // e ==> e IFF TRUE
592 {
593  Proof pf;
594  if(withProof()) {
595  pf = newPf("iff_true", e.getExpr(), e.getProof());
596  }
597  return newRWTheorem(e.getExpr(), d_em->trueExpr(), Assumptions(e), pf);
598 }
599 
600 
601 // e ==> !e IFF FALSE
603  Proof pf;
604  if(withProof()) {
605  pf = newPf("iff_not_false", e.getExpr(), e.getProof());
606  }
607  return newRWTheorem(!e.getExpr(), d_em->falseExpr(), Assumptions(e), pf);
608 }
609 
610 
611 // e IFF TRUE ==> e
613  if(CHECK_PROOFS)
614  CHECK_SOUND(e.isRewrite() && e.getRHS().isTrue(),
615  "CommonTheoremProducer::iffTrueElim: "
616  "theorem is not e<=>TRUE: "+ e.toString());
617  Proof pf;
618  if(withProof()) {
619  pf = newPf("iff_true_elim", e.getLHS(), e.getProof());
620  }
621  return newTheorem(e.getLHS(), Assumptions(e), pf);
622 }
623 
624 
625 // e IFF FALSE ==> !e
627  if(CHECK_PROOFS)
628  CHECK_SOUND(e.isRewrite() && e.getRHS().isFalse(),
629  "CommonTheoremProducer::iffFalseElim: "
630  "theorem is not e<=>FALSE: "+ e.toString());
631  const Expr& lhs = e.getLHS();
632  Proof pf;
633  if(withProof()) {
634  pf = newPf("iff_false_elim", lhs, e.getProof());
635  }
636  return newTheorem(!lhs, Assumptions(e), pf);
637 }
638 
639 
640 // e1 <=> e2 ==> ~e1 <=> ~e2
642  if(CHECK_PROOFS)
643  CHECK_SOUND(e.isRewrite() && e.getRHS().getType().isBool(),
644  "CommonTheoremProducer::iffContrapositive: "
645  "theorem is not e1<=>e2: "+ e.toString());
646  Proof pf;
647  if(withProof()) {
648  pf = newPf("iff_contrapositive", e.getExpr(), e.getProof());
649  }
650  return newRWTheorem(e.getLHS().negate(),e.getRHS().negate(), Assumptions(e), pf);
651 }
652 
653 
654 // !!e ==> e
656  if(CHECK_PROOFS)
657  CHECK_SOUND(not_not_e.getExpr().isNot() && not_not_e.getExpr()[0].isNot(),
658  "CommonTheoremProducer::notNotElim: bad theorem: !!e = "
659  + not_not_e.toString());
660  Proof pf;
661  if(withProof())
662  pf = newPf("not_not_elim", not_not_e.getExpr(), not_not_e.getProof());
663  return newTheorem(not_not_e.getExpr()[0][0], Assumptions(not_not_e), pf);
664 }
665 
666 
668 {
669  if(CHECK_PROOFS) {
670  CHECK_SOUND(e1_iff_e2.isRewrite(),
671  "iffMP: not IFF: "+e1_iff_e2.toString());
672  CHECK_SOUND(e1.getExpr() == (e1_iff_e2.getLHS()),
673  "iffMP: theorems don't match:\n e1 = " + e1.toString()
674  + ", e1_iff_e2 = " + e1_iff_e2.toString());
675  }
676  const Expr& e2(e1_iff_e2.getRHS());
677  // Avoid e1.getExpr(), it may cause unneeded Expr creation
678  if (e1_iff_e2.getLHS() == e2) return e1;
679  Proof pf;
680  Assumptions a(e1, e1_iff_e2);
681  if(withProof()) {
682  vector<Proof> pfs;
683  pfs.push_back(e1.getProof());
684  pfs.push_back(e1_iff_e2.getProof());
685  pf = newPf("iff_mp", e1.getExpr(), e2, pfs);
686  }
687  return newTheorem(e2, a, pf);
688 }
689 
690 
691 // e1 AND (e1 IMPLIES e2) ==> e2
693  const Theorem& e1_impl_e2) {
694  const Expr& impl = e1_impl_e2.getExpr();
695  if(CHECK_PROOFS) {
696  CHECK_SOUND(impl.isImpl() && impl.arity()==2,
697  "implMP: not IMPLIES: "+impl.toString());
698  CHECK_SOUND(e1.getExpr() == impl[0],
699  "implMP: theorems don't match:\n e1 = " + e1.toString()
700  + ", e1_impl_e2 = " + impl.toString());
701  }
702  const Expr& e2 = impl[1];
703  // Avoid e1.getExpr(), it may cause unneeded Expr creation
704  // if (impl[0] == e2) return e1; // this line commented by yeting because of proof translation
705  Proof pf;
706  Assumptions a(e1, e1_impl_e2);
707  if(withProof()) {
708  vector<Proof> pfs;
709  pfs.push_back(e1.getProof());
710  pfs.push_back(e1_impl_e2.getProof());
711  pf = newPf("impl_mp", e1.getExpr(), e2, pfs);
712  }
713  return newTheorem(e2, a, pf);
714 }
715 
716 
717 // AND(e_0,...e_{n-1}) ==> e_i
719  if(CHECK_PROOFS) {
720  CHECK_SOUND(e.getExpr().isAnd(), "andElim: not an AND: " + e.toString());
721  CHECK_SOUND(i < e.getExpr().arity(), "andElim: i = " + int2string(i)
722  + " >= arity = " + int2string(e.getExpr().arity())
723  + " in " + e.toString());
724  }
725  Proof pf;
726  if(withProof())
727  pf = newPf("andE", d_em->newRatExpr(i), e.getExpr(), e.getProof());
728  return newTheorem(e.getExpr()[i], Assumptions(e), pf);
729 }
730 
731 
732 //! e1, e2 ==> AND(e1, e2)
734  vector<Theorem> thms;
735  thms.push_back(e1);
736  thms.push_back(e2);
737  return andIntro(thms);
738 }
739 
740 
741 Theorem CommonTheoremProducer::andIntro(const vector<Theorem>& es) {
742  Proof pf;
743  if(CHECK_PROOFS)
744  CHECK_SOUND(es.size() > 1,
745  "andIntro(vector<Theorem>): vector must have more than 1 element");
746  Assumptions a(es);
747  /*
748  if(withProof()) {
749  vector<Proof> pfs;
750  for(vector<Theorem>::const_iterator i=es.begin(), iend=es.end();
751  i!=iend; ++i)
752  pfs.push_back(i->getProof());
753  // pf = newPf("andI", andExpr(kids), pfs);
754  }
755  */
756  vector<Expr> kids;
757  for(vector<Theorem>::const_iterator i=es.begin(), iend=es.end();
758  i!=iend; ++i)
759  kids.push_back(i->getExpr());
760 
761  if(withProof()) {
762  vector<Proof> pfs;
763  for(vector<Theorem>::const_iterator i=es.begin(), iend=es.end();
764  i!=iend; ++i)
765  pfs.push_back(i->getProof());
766  pf = newPf("andI", andExpr(kids), pfs);
767  }
768  return newTheorem(andExpr(kids), a, pf);
769 }
770 
771 
772 // G,a1,...,an |- phi
773 // -------------------------------------------------
774 // G |- (a1 & ... & an) -> phi
776  const std::vector<Expr>& assump) {
777  bool checkProofs(CHECK_PROOFS);
778  // This rule only makes sense when runnnig with assumptions
779  if(checkProofs) {
781  "implIntro: called while running without assumptions");
782  }
783 
784  const Assumptions& phiAssump = phi.getAssumptionsRef();
785 
786  if(checkProofs) {
787  for(size_t i=0; i<assump.size(); i++) {
788  const Theorem& thm = phiAssump[assump[i]];
789  CHECK_SOUND(!thm.isNull() && thm.isAssump(),
790  "implIntro: this is not an assumption of phi:\n\n"
791  " a["+int2string(i)+"] = "+assump[i].toString()
792  +"\n\n phi = "+phi.getExpr().toString());
793  }
794  }
795 
796  // Proof compaction: trivial derivation
797  if(assump.size() == 0) return phi;
798 
799  Assumptions a(phiAssump - assump);
800  Proof pf;
801  if(withProof()) {
802  vector<Proof> u; // Proof labels for assumptions
803  for(vector<Expr>::const_iterator i=assump.begin(), iend=assump.end();
804  i!=iend; ++i) {
805  const Theorem& t = phiAssump[*i];
806  u.push_back(t.getProof());
807  }
808  // Arguments to the proof rule:
809  // impl_intro_3(phi, a1,...,an,tcc1,...tccn,pf_tcc1,...pf_tccn,
810  // [lambda(a1,...,an): pf_phi])
811  vector<Expr> args;
812  vector<Proof> pfs;
813  args.push_back(phi.getExpr());
814  args.insert(args.end(), assump.begin(), assump.end());
815  // Lambda-abstraction of pf_phi
816  pfs.push_back(newPf(u, assump, phi.getProof()));
817  pf = newPf("impl_intro", args, pfs);
818  }
819  Expr conj(andExpr(assump));
820  return newTheorem(conj.impExpr(phi.getExpr()), a, pf);
821 }
822 
823 
824 // e1 => e2 ==> ~e2 => ~e1
826  const Expr& impl = thm.getExpr();
827  if(CHECK_PROOFS) {
828  CHECK_SOUND(impl.isImpl() && impl.arity()==2,
829  "CommonTheoremProducer::implContrapositive: thm="
830  +impl.toString());
831  }
832  Proof pf;
833  if(withProof())
834  pf = newPf("impl_contrapositive", impl, thm.getProof());
835  return newTheorem(impl[1].negate().impExpr(impl[0].negate()), Assumptions(thm), pf);
836 }
837 
838 
839 // ==> ITE(TRUE, e1, e2) == e1
840 Theorem
842  Proof pf;
843  if(CHECK_PROOFS)
844  CHECK_SOUND(e.isITE() && e[0].isTrue(),
845  "rewriteIteTrue precondition violated");
846  if(withProof()) {
847  Type t = e[1].getType();
848  DebugAssert(!t.isNull(), "rewriteIteTrue: e1 has no type: "
849  + e[1].toString());
850  bool useIff = t.isBool();
851  if(useIff)
852  pf = newPf("rewrite_ite_true_iff", e[1], e[2]);
853  else {
854  pf = newPf("rewrite_ite_true", t.getExpr(), e[1], e[2]);
855  }
856  }
857  return newRWTheorem(e, e[1], Assumptions::emptyAssump(), pf);
858 }
859 
860 
861 // ==> ITE(FALSE, e1, e2) == e2
862 Theorem
864  Proof pf;
865  if(CHECK_PROOFS)
866  CHECK_SOUND(e.isITE() && e[0].isFalse(),
867  "rewriteIteFalse precondition violated");
868  if(withProof()) {
869  Type t = e[1].getType();
870  DebugAssert(!t.isNull(), "rewriteIteFalse: e1 has no type: "
871  + e[1].toString());
872  bool useIff = t.isBool();
873  if(useIff)
874  pf = newPf("rewrite_ite_false_iff", e[1], e[2]);
875  else {
876  pf = newPf("rewrite_ite_false", t.getExpr(), e[1], e[2]);
877  }
878  }
879  return newRWTheorem(e, e[2], Assumptions::emptyAssump(), pf);
880 }
881 
882 
883 // ==> ITE(c, e, e) == e
884 Theorem
886  Proof pf;
887  if(CHECK_PROOFS)
888  CHECK_SOUND(e.isITE() && e[1] == e[2],
889  "rewriteIteSame precondition violated");
890  if(withProof()) {
891  Type t = e[1].getType();
892  DebugAssert(!t.isNull(), "rewriteIteSame: e[1] has no type: "
893  + e[1].toString());
894  bool useIff = t.isBool();
895  if(useIff)
896  pf = newPf("rewrite_ite_same_iff", e[0], e[1]);
897  else {
898  pf = newPf("rewrite_ite_same", t.getExpr(), e[0], e[1]);
899  }
900  }
901  return newRWTheorem(e, e[1], Assumptions::emptyAssump(), pf);
902 }
903 
904 
905 // NOT e ==> e IFF FALSE
907 {
908  if(CHECK_PROOFS)
909  CHECK_SOUND(not_e.getExpr().isNot(),
910  "notToIff: not NOT: "+not_e.toString());
911 
912  // Make it an atomic rule (more efficient)
913  Expr e(not_e.getExpr()[0]);
914  Proof pf;
915  if(withProof())
916  pf=newPf("not_to_iff", e, not_e.getProof());
917  return newRWTheorem(e, d_em->falseExpr(), Assumptions(not_e), pf);
918 }
919 
920 
921 // e1 XOR e2 ==> e1 IFF (NOT e2)
923 {
924  if(CHECK_PROOFS) {
925  CHECK_SOUND(e.isXor(), "xorToIff precondition violated");
926  CHECK_SOUND(e.arity() >= 2, "Expected XOR of arity >= 2");
927  }
928  Expr res = e[e.arity()-1];
929  for (int i = e.arity()-2; i >=0; --i) {
930  res = (!e[i]).iffExpr(res);
931  }
932  Proof pf;
933  if(withProof()) {
934  pf = newPf("xorToIff");
935  }
936  return newRWTheorem(e, res, Assumptions::emptyAssump(), pf);
937 }
938 
939 
940 // ==> IFF(e1,e2) IFF <simplified expr>
942  Proof pf;
943  if(CHECK_PROOFS)
944  CHECK_SOUND(e.isIff(), "rewriteIff precondition violated");
945  if(withProof()) {
946  pf = newPf("rewrite_iff", e[0], e[1]);
947  }
948 
949  if(e[0] == e[1]) return rewriteReflexivity(e);
950 
951  switch(e[0].getKind()) {
952  case TRUE_EXPR:
953  return newRWTheorem(e, e[1], Assumptions::emptyAssump(), pf);
954  case FALSE_EXPR:
955  return newRWTheorem(e, !e[1], Assumptions::emptyAssump() ,pf);
956  case NOT:
957  if(e[0][0]==e[1])
959  break;
960  default: break;
961  }
962 
963  switch(e[1].getKind()) {
964  case TRUE_EXPR:
965  return newRWTheorem(e, e[0], Assumptions::emptyAssump(), pf);
966  case FALSE_EXPR:
967  return newRWTheorem(e, !e[0], Assumptions::emptyAssump(), pf);
968  case NOT:
969  if(e[0]==e[1][0])
971  break;
972  default:
973  break;
974  }
975 
976  if(e[0] < e[1])
977  return rewriteUsingSymmetry(e);
978  else
979  return reflexivityRule(e);
980 }
981 
982 
983 // ==> AND(e_1,...,e_n) IFF <simplified expr>
984 // 1) if e_i = FALSE then return FALSE
985 // 2) if e_i = TRUE, remove it from children
986 // 3) if e_i = AND(f_1,...,f_m) then AND(e_1,...,e_{i-1},f_1,...,f_m,e_{i+1},...,e_n)
987 // 4) if n=0 return TRUE
988 // 5) if n=1 return e_1
990  if(CHECK_PROOFS)
991  CHECK_SOUND(e.isAnd(), "rewriteAnd: bad Expr: " + e.toString());
992  Proof pf;
993  ExprMap<bool> newKids;
994  bool isFalse (false);
995  for (Expr::iterator k=e.begin(), kend=e.end(); !isFalse && k != kend; ++k) {
996  const Expr& ek = *k;
997  if (ek.isFalse()) { isFalse=true; break; }
998  if (ek.isAnd() && ek.arity() < 10) {
999  for(Expr::iterator j=ek.begin(), jend=ek.end(); j!=jend; ++j) {
1000  if(newKids.count(j->negate()) > 0) { isFalse=true; break; }
1001  newKids[*j]=true;
1002  }
1003  } else if(!ek.isTrue()) {
1004  if(newKids.count(ek.negate()) > 0) { isFalse=true; break; }
1005  newKids[ek]=true;
1006  }
1007  }
1008  Expr res;
1009  if (isFalse) res = d_em->falseExpr();
1010  else if (newKids.size() == 0) res = d_em->trueExpr(); // All newKids were TRUE
1011  else if (newKids.size() == 1)
1012  res = newKids.begin()->first; // The only child
1013  else {
1014  vector<Expr> v;
1015  for(ExprMap<bool>::iterator i=newKids.begin(), iend=newKids.end();
1016  i!=iend; ++i)
1017  v.push_back(i->first);
1018  res = andExpr(v);
1019  }
1020  if(withProof()) {
1021  pf = newPf("rewrite_and", e,res);
1022  }
1023  return newRWTheorem(e, res, Assumptions::emptyAssump(), pf);
1024 }
1025 
1026 
1027 // ==> OR(e1,e2) IFF <simplified expr>
1029  if(CHECK_PROOFS)
1030  CHECK_SOUND(e.isOr(), "rewriteOr: bad Expr: " + e.toString());
1031  Proof pf;
1032  ExprMap<bool> newKids;
1033  bool isTrue (false);
1034  for (Expr::iterator k=e.begin(), kend=e.end(); !isTrue && k != kend; ++k) {
1035  const Expr& ek = *k;
1036  if (ek.isTrue()) { isTrue=true; break; }
1037  else if (ek.isOr() && ek.arity() < 10) {
1038  for(Expr::iterator j=ek.begin(), jend=ek.end(); j!=jend; ++j) {
1039  if(newKids.count(j->negate()) > 0) { isTrue=true; break; }
1040  newKids[*j]=true;
1041  }
1042  } else if(!ek.isFalse()) {
1043  if(newKids.count(ek.negate()) > 0) { isTrue=true; break; }
1044  newKids[ek]=true;
1045  }
1046  }
1047  Expr res;
1048  if (isTrue) res = d_em->trueExpr();
1049  else if (newKids.size() == 0) res = d_em->falseExpr(); // All kids were FALSE
1050  else if (newKids.size() == 1) res = newKids.begin()->first; // The only child
1051  else {
1052  vector<Expr> v;
1053  for(ExprMap<bool>::iterator i=newKids.begin(), iend=newKids.end();
1054  i!=iend; ++i)
1055  v.push_back(i->first);
1056  res = orExpr(v);
1057  }
1058  if(withProof()) {
1059  pf = newPf("rewrite_or", e, res);
1060  }
1061  return newRWTheorem(e, res, Assumptions::emptyAssump(), pf);
1062 }
1063 
1064 
1065 // ==> NOT TRUE IFF FALSE
1067  Proof pf;
1068  if(CHECK_PROOFS)
1069  CHECK_SOUND(e.isNot() && e[0].isTrue(),
1070  "rewriteNotTrue precondition violated");
1071  if(withProof())
1072  pf = newPf("rewrite_not_true");
1073  return newRWTheorem(e, d_em->falseExpr(), Assumptions::emptyAssump(), pf);
1074 }
1075 
1076 
1077 // ==> NOT FALSE IFF TRUE
1079  Proof pf;
1080  if(CHECK_PROOFS)
1081  CHECK_SOUND(e.isNot() && e[0].isFalse(),
1082  "rewriteNotFalse precondition violated");
1083  if(withProof())
1084  pf = newPf("rewrite_not_false");
1085  return newRWTheorem(e, d_em->trueExpr(), Assumptions::emptyAssump(), pf);
1086 }
1087 
1088 
1089 // ==> (NOT NOT e) IFF e, takes !!e
1091  Proof pf;
1092  if(CHECK_PROOFS)
1093  CHECK_SOUND(e.isNot() && e[0].isNot(),
1094  "rewriteNotNot precondition violated");
1095  if(withProof())
1096  pf = newPf("rewrite_not_not", e[0][0]);
1097  return newRWTheorem(e, e[0][0], Assumptions::emptyAssump(), pf);
1098 }
1099 
1100 
1101 //! ==> NOT FORALL (vars): e IFF EXISTS (vars) NOT e
1103  if(CHECK_PROOFS) {
1104  CHECK_SOUND(e.isNot() && e[0].isForall(),
1105  "rewriteNotForall: expr must be NOT FORALL:\n"
1106  +e.toString());
1107  }
1108  Proof pf;
1109  if(withProof())
1110  pf = newPf("rewrite_not_forall", e);
1111  return newRWTheorem(e, d_em->newClosureExpr(EXISTS, e[0].getVars(),
1112  !e[0].getBody()), Assumptions::emptyAssump(), pf);
1113 }
1114 
1115 
1116 //! ==> NOT EXISTS (vars): e IFF FORALL (vars) NOT e
1118  if(CHECK_PROOFS) {
1119  CHECK_SOUND(e.isNot() && e[0].isExists(),
1120  "rewriteNotExists: expr must be NOT FORALL:\n"
1121  +e.toString());
1122  }
1123  Proof pf;
1124  if(withProof())
1125  pf = newPf("rewrite_not_exists", e);
1126  return newRWTheorem(e, d_em->newClosureExpr(FORALL, e[0].getVars(),
1127  !e[0].getBody()), Assumptions::emptyAssump(), pf);
1128 }
1129 
1130 
1132 {
1133  vector<Expr> vars;
1134  const vector<Expr>& boundVars = e.getVars();
1135  for(unsigned int i=0; i<boundVars.size(); i++) {
1136  Expr skolV(e.skolemExpr(i));
1137  Type tp(e.getVars()[i].getType());
1138  skolV.setType(tp);
1139  vars.push_back(skolV);
1140  }
1141  return(e.getBody().substExpr(boundVars, vars));
1142 }
1143 
1144 
1146 {
1147  Proof pf;
1148  if(CHECK_PROOFS) {
1149  CHECK_SOUND(e.isExists(), "skolemize rewrite called on non-existential: "
1150  + e.toString());
1151  }
1152  Expr skol = skolemize(e);
1153  if(withProof()) {
1154  Expr rw(e.iffExpr(skol));
1155  pf = newLabel(rw);
1156  }
1157  TRACE("quantlevel", "skolemize ", skol, "");
1158  TRACE("quantlevel sko", "skolemize ", skol, "");
1159  TRACE("quantlevel sko", "skolemize from org ", e, "");
1160  return newRWTheorem(e, skol, Assumptions::emptyAssump(), pf);
1161 
1162 }
1163 
1164 
1166 {
1167  Proof pf;
1168  if(CHECK_PROOFS) {
1169  CHECK_SOUND(e.isExists(), "skolemizeRewriteVar("
1170  +e.toString()+")");
1171  }
1172 
1173  const vector<Expr>& boundVars = e.getVars();
1174  const Expr& body = e.getBody();
1175 
1176  if(CHECK_PROOFS) {
1177  CHECK_SOUND(boundVars.size()==1, "skolemizeRewriteVar("
1178  +e.toString()+")");
1179  CHECK_SOUND(body.isEq() || body.isIff(), "skolemizeRewriteVar("
1180  +e.toString()+")");
1181  const Expr& v = boundVars[0];
1182  CHECK_SOUND(body[1] == v, "skolemizeRewriteVar("
1183  +e.toString()+")");
1184  CHECK_SOUND(!(v.subExprOf(body[0])), "skolemizeRewriteVar("
1185  +e.toString()+")");
1186  }
1187  // Create the Skolem constant appropriately
1188  Expr skolV(e.skolemExpr(0));
1189  Type tp(e.getVars()[0].getType());
1190  skolV.setType(tp);
1191  // Skolemized expression
1192  Expr skol = Expr(body.getOp(), body[0], skolV);
1193 
1194  if(withProof()) {
1195  Expr rw(e.iffExpr(skol));
1196  pf = newLabel(rw);
1197  }
1198  return newRWTheorem(e, skol, Assumptions::emptyAssump(), pf);
1199 }
1200 
1201 
1203  // This rule is sound for all expressions phi
1204  Proof pf;
1205  const Expr boundVar = d_em->newBoundVarExpr(phi.getType());
1206 
1207  Expr body;
1208  if(phi.getType().isBool())
1209  body = phi.iffExpr(boundVar);
1210  else
1211  body = phi.eqExpr(boundVar);
1212 
1213  std::vector<Expr> v;
1214  v.push_back(boundVar);
1215  const Expr result = d_em->newClosureExpr(EXISTS, v, body);
1216 
1217  if(withProof())
1218  pf = newPf("var_intro", phi, boundVar);
1219  return newTheorem(result, Assumptions::emptyAssump(), pf);
1220 }
1221 
1222 
1224  const Expr& e = thm.getExpr();
1225  if(e.isExists()) {
1226  TRACE("skolem", "Skolemizing existential:", "", "{");
1228  iend=d_skolemized_thms.end();
1229  if(i!=iend) {
1230  TRACE("skolem", "Skolemized theorem found in map: ", (*i).second, "}");
1231  return iffMP(thm, (*i).second);
1232  }
1233  Theorem skol = skolemizeRewrite(e);
1234  for(unsigned int i=0; i<e.getVars().size(); i++) {
1235  Expr skolV(e.skolemExpr(i));
1236  Type tp(e.getVars()[i].getType());
1237  skolV.setType(tp);
1238  }
1239  d_skolem_axioms.push_back(skol);
1240  d_skolemized_thms.insert(e, skol, 0);//d_coreSatAPI->getBottomScope());
1241  skol = iffMP(thm, skol);
1242 
1243  TRACE("skolem", "skolemized new theorem: ", skol, "}");
1244  return skol;
1245  }
1246  return thm;
1247 }
1248 
1249 
1251  // First, look up the cache
1253  iend=d_skolemVars.end();
1254  if(i!=iend) return (*i).second;
1255  // Not in cache; create a new one
1256  Theorem thm = varIntroRule(e);
1257  const Expr& e2 = thm.getExpr();
1258  DebugAssert(e2.isExists() && e2.getVars().size()==1, "varIntroSkolem: e2 = "
1259  +e2.toString());
1260  Theorem skolThm;
1261  // Check if we have a corresponding skolemized version already
1263  jend=d_skolemized_thms.end();
1264  if(j!=jend) {
1265  skolThm = (*i).second;
1266  } else {
1267  skolThm = skolemizeRewriteVar(e2);
1268  d_skolem_axioms.push_back(skolThm);
1269  d_skolemized_thms.insert(e2, skolThm, 0); //d_coreSatAPI->getBottomScope());
1270  }
1271  thm = iffMP(thm, skolThm);
1272  d_skolemVars.insert(e, thm, 0); //d_coreSatAPI->getBottomScope());
1273  return thm;
1274 }
1275 
1276 
1277 // Derived Rules
1278 
1279 
1281 {
1283 }
1284 
1285 
1287 {
1288  return iffMP(e, rewriteAnd(e.getExpr()));
1289 }
1290 
1291 
1293 {
1294  return iffMP(e, rewriteOr(e.getExpr()));
1295 }
1296 
1297 
1299 {
1300  Proof pf;
1301  if(CHECK_PROOFS)
1302  CHECK_SOUND(e1.isApply() && e2.isApply() && e1.getOp() == e2.getOp(),
1303  "ackermann precondition violated");
1304  Expr hyp;
1305  int ar = e1.arity();
1306  if (ar == 1) {
1307  hyp = Expr(e1[0].eqExpr(e2[0]));
1308  }
1309  else {
1310  vector<Expr> vec;
1311  for (int i = 0; i != ar; ++i) {
1312  vec.push_back(e1[i].eqExpr(e2[i]));
1313  }
1314  hyp = Expr(AND, vec);
1315  }
1316  if(withProof())
1317  pf = newPf("ackermann", e1, e2);
1318  return newTheorem(hyp.impExpr(e1.eqExpr(e2)), Assumptions::emptyAssump(), pf);
1319 }
1320 
1321 
1322 void CommonTheoremProducer::findITE(const Expr& e, Expr& condition, Expr& thenpart, Expr& elsepart)
1323 {
1324  if (!e.getType().isBool() && e.isITE()) {
1325  condition = e[0];
1326  if (!condition.containsTermITE()) {
1327  thenpart = e[1];
1328  elsepart = e[2];
1329  return;
1330  }
1331  }
1332 
1333  vector<Expr> kids;
1334  int i = 0;
1335  for (; i < e.arity(); ++i) {
1336  if (e[i].containsTermITE()) break;
1337  kids.push_back(e[i]);
1338  }
1339 
1340  if(CHECK_PROOFS) {
1341  CHECK_SOUND(i < e.arity(), "could not find ITE");
1342  }
1343 
1344  Expr t2, e2;
1345  findITE(e[i], condition, t2, e2);
1346 
1347  kids.push_back(t2);
1348  for(int k = i+1; k < e.arity(); ++k) {
1349  kids.push_back(e[k]);
1350  }
1351 
1352  thenpart = Expr(e.getOp(), kids);
1353 
1354  kids[i] = e2;
1355  elsepart = Expr(e.getOp(), kids);
1356 }
1357 
1358 
1360 
1361  if(CHECK_PROOFS) {
1362  CHECK_SOUND(e.containsTermITE(), "CommonTheoremProducer::liftOneITE: bad input" + e.toString());
1363  }
1364 
1365  Expr cond, thenpart, elsepart;
1366 
1367  findITE(e, cond, thenpart, elsepart);
1368 
1369  Proof pf;
1370  if(withProof())
1371  pf = newPf("lift_one_ite", e);
1372 
1373  return newRWTheorem(e, cond.iteExpr(thenpart, elsepart), Assumptions::emptyAssump(), pf);
1374 }
int arity() const
Definition: expr.h:1201
bool isIff() const
Definition: expr.h:424
Theorem notNotElim(const Theorem &e)
iterator begin() const
Begin iterator.
Definition: expr.h:1211
bool isEq() const
Definition: expr.h:419
void setSubst() const
Set flag stating that theorem is an instance of substitution.
Definition: theorem.cpp:447
Theorem newAssumption(const Expr &thm, const Proof &pf, int scope=-1)
Theorem iffTrue(const Theorem &e)
Data structure of expressions in CVC3.
Definition: expr.h:133
Theorem rewriteOr(const Expr &e)
==> OR(e1,...,en) IFF [simplified expr]
Theorem rewriteIteSame(const Expr &e)
==> ITE(c, e, e) == e
Proof getProof() const
Definition: theorem.h:370
Expr iteExpr(const Expr &thenpart, const Expr &elsepart) const
Definition: expr.h:961
Theorem rewriteIteTrue(const Expr &e)
==> ITE(TRUE, e1, e2) == e1
Theorem newTheorem(const Expr &thm, const Assumptions &assump, const Proof &pf)
Create a new theorem. See also newRWTheorem() and newReflTheorem()
void findITE(const Expr &e, Expr &condition, Expr &thenpart, Expr &elsepart)
Helper function for liftOneITE.
bool isTrue() const
Definition: expr.h:356
bool isImpl() const
Definition: expr.h:425
Theorem3 implIntro3(const Theorem3 &phi, const std::vector< Expr > &assump, const std::vector< Theorem > &tccs)
3-valued implication introduction rule:
bool isITE() const
Definition: expr.h:423
void add(const std::vector< Theorem > &thms)
ExprManager * getEM() const
Theorem rewriteNotExists(const Expr &existsExpr)
==> NOT EXISTS (vars): e IFF FORALL (vars) NOT e
Definition: kinds.h:84
Theorem rewriteNotTrue(const Expr &e)
==> NOT TRUE IFF FALSE
Theorem newReflTheorem(const Expr &e)
Create a reflexivity theorem.
bool isFalse() const
Definition: expr.h:355
Theorem reflexivityRule(const Expr &a)
MS C++ specific settings.
Definition: type.h:42
STL namespace.
Definition: kinds.h:85
iterator begin()
Definition: expr_map.h:190
bool containsTermITE() const
Return whether Expr contains a non-bool type ITE as a sub-term.
Definition: expr.cpp:525
Definition: kinds.h:66
bool withProof()
Testing whether to generate proofs.
Expr eqExpr(const Expr &right) const
Definition: expr.h:929
bool isBool() const
Definition: type.h:60
Theorem ackermann(const Expr &e1, const Expr &e2)
Theorem varIntroRule(const Expr &e)
|- EXISTS x. e = x
#define DebugAssert(cond, str)
Definition: debug.h:408
Theorem rewriteReflexivity(const Expr &t)
==> (a == a) IFF TRUE
Theorem iffNotFalse(const Theorem &e)
#define CHECK_SOUND(cond, msg)
Expr newClosureExpr(int kind, const Expr &var, const Expr &body)
Definition: expr_manager.h:506
size_t size() const
Definition: expr_map.h:171
Theorem contradictionRule(const Theorem &e, const Theorem &not_e)
#define CHECK_PROOFS
Theorem iffTrueElim(const Theorem &e)
bool isOr() const
Definition: expr.h:422
bool withAssumptions()
Testing whether to generate assumptions.
CVC3::ExprStream & endl(CVC3::ExprStream &os)
Print the end-of-line.
std::vector< Theorem > d_skolem_axioms
Expr orExpr(const std::vector< Expr > &children)
Definition: expr.h:955
Expr impExpr(const Expr &right) const
Definition: expr.h:969
Expr newBoundVarExpr(const std::string &name, const std::string &uid)
Definition: expr_manager.h:484
Theorem3.
Definition: theorem.h:308
Theorem3 queryTCC(const Theorem &phi, const Theorem &D_phi)
Convert 2-valued formula to 3-valued by discharging its TCC ( ): .
Op getOp() const
Get operator from expression.
Definition: expr.h:1183
CommonProofRules * createProofRules()
const Expr & getExpr() const
Definition: type.h:52
Theorem rewriteAnd(const Expr &e)
==> AND(e1,e2) IFF [simplified expr]
bool isNot() const
Definition: expr.h:420
size_t count(const Expr &e) const
Definition: expr_map.h:173
bool isExists() const
Definition: expr.h:429
Theorem varIntroSkolem(const Expr &e)
Retrun a theorem "|- e = v" for a new Skolem constant v.
bool isXor() const
Definition: expr.h:426
Theorem andIntro(const Theorem &e1, const Theorem &e2)
e1, e2 ==> AND(e1, e2)
std::string toString() const
Definition: theorem.h:404
Theorem rewriteNotFalse(const Expr &e)
==> NOT FALSE IFF TRUE
Theorem andElim(const Theorem &e, int i)
Theorem rewriteIteFalse(const Expr &e)
==> ITE(FALSE, e1, e2) == e2
std::string toString() const
Print the expression to a string.
Definition: expr.cpp:344
Theorem implMP(const Theorem &e1, const Theorem &e1_impl_e2)
Expr skolemExpr(int i) const
Create a Skolem constant for the i'th variable of an existential (*this)
Definition: expr.h:977
TheoremManager * d_tm
Theorem substitutivityRule(const Expr &e, const Theorem &thm)
Optimized case for expr with one child.
Expr iffExpr(const Expr &right) const
Definition: expr.h:965
const Expr & falseExpr()
FALSE Expr.
Definition: expr_manager.h:278
Expr newLeafExpr(const Op &op)
Definition: expr_manager.h:454
Expr negate() const
Definition: expr.h:937
const Expr & getBody() const
Get the body of the closure Expr.
Definition: expr.h:1069
std::string int2string(int n)
Definition: cvc_util.h:46
Theorem rewriteNotForall(const Expr &forallExpr)
==> NOT FORALL (vars): e IFF EXISTS (vars) NOT e
Proof newLabel(const Expr &e)
Create a new proof label (bound variable) for an assumption (formula)
const Expr & getRHS() const
Definition: theorem.cpp:246
bool isNull() const
Definition: type.h:59
const Expr & trueExpr()
TRUE Expr.
Definition: expr_manager.h:280
#define IF_DEBUG(code)
Definition: debug.h:406
std::string toString() const
Definition: expr_op.cpp:38
Proof getProof() const
Definition: theorem.cpp:402
const Assumptions & getAssumptionsRef() const
Definition: theorem.cpp:385
Expr getExpr() const
Definition: theorem.cpp:230
Expr newRatExpr(const Rational &r)
Definition: expr_manager.h:471
bool isNull() const
Definition: theorem.h:164
bool isForall() const
Definition: expr.h:428
bool isApply() const
Definition: expr.h:1014
Theorem3 newTheorem3(const Expr &thm, const Assumptions &assump, const Proof &pf)
CDMap< Expr, Theorem > d_skolemized_thms
Theorem skolemizeRewriteVar(const Expr &e)
Special version of skolemizeRewrite for "EXISTS x. t = x".
Expr orExpr(const Expr &right) const
Definition: expr.h:951
CDMap< Expr, Theorem > d_skolemVars
Mapping of e to "|- e = v" for fresh Skolem vars v.
Theorem iffFalseElim(const Theorem &e)
Theorem newRWTheorem(const Expr &lhs, const Expr &rhs, const Assumptions &assump, const Proof &pf)
Create a rewrite theorem: lhs = rhs.
Theorem symmetryRule(const Theorem &a1_eq_a2)
(same for IFF)
Theorem assumpRule(const Expr &a, int scope=-1)
const std::vector< Expr > & getVars() const
Get bound variables from a closure Expr.
Definition: expr.h:1062
Theorem rewriteUsingSymmetry(const Expr &a1_eq_a2)
Theorem transitivityRule(const Theorem &a1_eq_a2, const Theorem &a2_eq_a3)
(same for IFF)
bool isRefl() const
Definition: theorem.h:171
const Expr & getLHS() const
Definition: theorem.cpp:240
Theorem implIntro(const Theorem &phi, const std::vector< Expr > &assump)
Implication introduction rule: .
Theorem rewriteIff(const Expr &e)
==> (e1 <=> e2) <=> [simplified expr]
Theorem implContrapositive(const Theorem &thm)
e1 => e2 ==> ~e2 => ~e1
Proof newPf(const std::string &name)
Theorem notToIff(const Theorem &not_e)
Expr substExpr(const std::vector< Expr > &oldTerms, const std::vector< Expr > &newTerms) const
Definition: expr.cpp:178
Definition: expr.cpp:35
Definition: kinds.h:99
Type getType() const
Get the type. Recursively compute if necessary.
Definition: expr.h:1259
bool isRewrite() const
Definition: theorem.cpp:224
Expr getExpr() const
Definition: theorem.h:358
bool isAssump() const
Definition: theorem.cpp:395
static const Assumptions & emptyAssump()
Definition: assumptions.h:83
Expr andExpr(const std::vector< Expr > &children)
Definition: expr.h:945
iterator end()
Definition: expr_map.h:191
Definition: kinds.h:67
Theorem rewriteNotNot(const Expr &e)
==> NOT NOT e IFF e, takes !!e
Theorem iffMP(const Theorem &e1, const Theorem &e1_iff_e2)
Theorem iffContrapositive(const Theorem &thm)
e1 <=> e2 ==> ~e1 <=> ~e2
const Assumptions & getAssumptionsRef() const
Definition: theorem.h:365
iterator end() const
End iterator.
Definition: expr.h:1217
bool isAnd() const
Definition: expr.h:421