CVC3  2.4.1
core_theorem_producer.cpp
Go to the documentation of this file.
1 /*****************************************************************************/
2 /*!
3  * \file core_theorem_producer.cpp
4  *
5  * Author: Sergey Berezin
6  *
7  * Created: Feb 05 03:40:36 GMT 2003
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: CoreTheoremProducer
21 //
22 // AUTHOR: Sergey Berezin, 12/09/2002
23 // Vijay Ganesh, september 15th, 2004 (CNF Converter rules)
24 //
25 // Description: Implementation of the proof rules for ground
26 // equational logic (reflexivity, symmetry, transitivity, and
27 // substitutivity).
28 //
29 ///////////////////////////////////////////////////////////////////////////////
30 
31 
32 // This code is trusted
33 #define _CVC3_TRUSTED_
34 
35 
36 #include "core_theorem_producer.h"
37 #include "theory_core.h"
38 
39 
40 using namespace CVC3;
41 using namespace std;
42 
43 
44 // The trusted method of TheoryCore which creates this theorem producer
46  return new CoreTheoremProducer(tm, this);
47 }
48 
49 
50 // e: T ==> |- typePred_T(e) [asserting the type predicate of e]
51 Theorem
53  Type tp(e.getType());
54  Expr pred(d_core->getTypePred(tp, e));
55  Proof pf;
56  if(withProof()) {
57  pf = newPf("type_pred", e, tp.getExpr());
58  }
59  return newTheorem(pred, Assumptions::emptyAssump(), pf);
60 }
61 
62 
63 Theorem
65  if(CHECK_PROOFS)
67  "rewriteLetDecl: wrong expression: " + e.toString());
68  Proof pf;
69  if(withProof()) // FIXME: implement this in flea
70  pf = newPf("rewrite_letdecl", e[1]);
71  return newRWTheorem(e, e[1], Assumptions::emptyAssump(), pf);
72 }
73 
74 // ==> NOT (AND e1 ... en) IFF (OR !e1 ... !en), takes (AND ...)
76  if(CHECK_PROOFS)
77  CHECK_SOUND(e.isNot() && e[0].isAnd(),
78  "rewriteNotAnd: precondition violated: " + e.toString());
79 
80 
81  vector<Expr> kids; // vector of <!e1,...,!en>
82  for(Expr::iterator i=e[0].begin(), iend=e[0].end(); i!=iend; ++i)
83  // Collapse double negations
84  kids.push_back(i->negate());
85  Proof pf;
86  if(withProof())
87  pf = newPf("rewrite_not_and", e);
88  return newRWTheorem(e, orExpr(kids), Assumptions::emptyAssump(), pf);
89 }
90 
91 // ==> NOT (OR e1 ... en) IFF (AND !e1 ... !en), takes (OR ...)
92 Theorem
94  if(CHECK_PROOFS)
95  CHECK_SOUND(e.isNot() && e[0].isOr(),
96  "rewriteNotOr: precondition violated: " + e.toString());
97  vector<Expr> kids; // vector of <!e1,...,!en>
98  for(Expr::iterator i=e[0].begin(), iend=e[0].end(); i!=iend; ++i)
99  // Collapse double negations
100  kids.push_back(i->negate());
101  Proof pf;
102  if(withProof())
103  pf = newPf("rewrite_not_or", e);
104  return newRWTheorem(e, andExpr(kids), Assumptions::emptyAssump(), pf);
105 }
106 
107 
108 // ==> NOT IFF(e1,e2) IFF IFF(e1,NOT e2)
109 Theorem
111  Proof pf;
112  if(CHECK_PROOFS)
113  CHECK_SOUND(e.isNot() && e[0].isIff(), "rewriteNotIff precondition violated");
114  if(withProof()) {
115  pf = newPf("rewrite_not_iff", e);
116  }
117  return newRWTheorem(e, e[0][0].iffExpr(!e[0][1]), Assumptions::emptyAssump(), pf);
118 }
119 
120 
121 // ==> NOT ITE(a,b,c) IFF ITE(a,NOT b,NOT c)
122 Theorem
124  Proof pf;
125  if(CHECK_PROOFS)
126  CHECK_SOUND(e.isNot() && e[0].isITE(), "rewriteNotIte precondition violated");
127  if(withProof()) {
128  pf = newPf("rewrite_not_ite", e);
129  }
130  return newRWTheorem(e, e[0][0].iteExpr(!e[0][1], !e[0][2]), Assumptions::emptyAssump(), pf);
131 }
132 
133 
134 // a |- b == d ==> ITE(a, b, c) == ITE(a, d, c)
135 Theorem
137  Proof pf;
138  if(CHECK_PROOFS) {
139  CHECK_SOUND(withAssumptions(), "Cannot check proof without assumptions");
140  CHECK_SOUND(e.isITE() && thenThm.isRewrite() && e[1] == thenThm.getLHS(),
141  "rewriteIteThen precondition violated \n then expression: "
142  + thenThm.getExpr().toString() + "\n e = " + e.toString());
143  }
144  Assumptions a = thenThm.getAssumptionsRef() - e[0];
145  if(withProof()) {
146  Type t = e.getType();
147  DebugAssert(!t.isNull(), "rewriteIteThen: e has no type: "
148  + e.toString());
149  bool useIff = t.isBool();
150  if(useIff)
151  pf = newPf("rewrite_ite_then_iff", e, thenThm.getProof());
152  else {
153  pf = newPf("rewrite_ite_then", e, thenThm.getProof());
154  }
155  }
156  return newRWTheorem(e, e[0].iteExpr(thenThm.getRHS(), e[2]), a, pf);
157 }
158 
159 // !a |- c == d ==> ITE(a, b, c) == ITE(a, b, d)
160 Theorem
162  Proof pf;
163  if(CHECK_PROOFS) {
164  CHECK_SOUND(withAssumptions(), "Cannot check proof without assumptions");
165  CHECK_SOUND(e.isITE() && elseThm.isRewrite() && e[2] == elseThm.getLHS(),
166  "rewriteIteElse precondition violated \n else expression: "
167  + elseThm.getExpr().toString() + "\n e = " + e.toString());
168  }
169  Assumptions a = elseThm.getAssumptionsRef() - !e[0];
170  if(withProof()) {
171  Type t = e.getType();
172  DebugAssert(!t.isNull(), "rewriteIteElse: e has no type: "
173  + e.toString());
174  bool useIff = t.isBool();
175  if(useIff)
176  pf = newPf("rewrite_ite_else_iff", e, elseThm.getProof());
177  else {
178  pf = newPf("rewrite_ite_else", e, elseThm.getProof());
179  }
180  }
181  return newRWTheorem(e, e[0].iteExpr(e[1], elseThm.getRHS()), a, pf);
182 }
183 
184 // ==> ITE(c, e1, e2) <=> (!c OR e1) AND (c OR e2)
185 Theorem
187  const Expr& e1, const Expr& e2) {
188  if(CHECK_PROOFS)
189  CHECK_SOUND(e1.getType().isBool() && e2.getType().isBool(),
190  "rewriteIteBool: Not a boolean ITE: "
191  + c.iteExpr(e1, e2).toString());
192  Proof pf;
193  if(withProof())
194  pf = newPf("rewrite_ite_bool", c, e1, e2);
195  return newRWTheorem(c.iteExpr(e1,e2),
196  (e1.orExpr(!c).andExpr(c.orExpr(e2))), Assumptions::emptyAssump(), pf);
197 }
198 
199 
200 //! |= (A & B1) | (A & B2) | ... | (A & bn) <=> A & (B1 | B2 | ...| Bn)
201 Theorem
203  if(CHECK_PROOFS) {
204  CHECK_SOUND(e.isOr() && e.arity() >= 2,
205  "CoreTheoremProducer::orDistributivityRule: "
206  "input must be an OR expr: \n" + e.toString());
207  const Expr& e0 = e[0];
208 
209  CHECK_SOUND(e0.isAnd() && e0.arity() == 2,
210  "CoreTheoremProducer::orDistributivityRule: "
211  "input must be an OR of binary ANDs: \n" + e.toString());
212  }
213 
214  const Expr& A = e[0][0];
215 
216  if(CHECK_PROOFS) {
217  for(Expr::iterator i=e.begin(),iend=e.end();i!=iend;++i) {
218  const Expr& ei = *i;
219  CHECK_SOUND(ei.isAnd() && ei.arity() == 2,
220  "CoreTheoremProducer::orDistributivityRule: "
221  "input must be an OR of binary ANDs: \n" + e.toString());
222  CHECK_SOUND(A == ei[0],
223  "CoreTheoremProducer::orDistributivityRule: "
224  "input must have a common factor: \n" + e.toString());
225  }
226  }
227  vector<Expr> output;
228  for(Expr::iterator i=e.begin(),iend=e.end();i!=iend;++i) {
229  Expr ei = *i;
230  output.push_back(ei[1]);
231  }
232  Expr out = A.andExpr(orExpr(output));
233 
234  Proof pf;
235  if(withProof())
236  pf = newPf("or_distribuitivity_rule", e);
237 
238  return newRWTheorem(e, out, Assumptions::emptyAssump(), pf);
239 }
240 
241 
242 
243 //! |= (A | B1) & (A | B2) & ... & (A | bn) <=> A | (B1 & B2 & ...& Bn)
244 Theorem
246  if(CHECK_PROOFS) {
247  CHECK_SOUND(e.isAnd() && e.arity() >= 2,
248  "CoreTheoremProducer::andDistributivityRule: "
249  "input must be an AND expr: \n" + e.toString());
250  const Expr& e0 = e[0];
251 
252  CHECK_SOUND(e0.isOr() && e0.arity() == 2,
253  "CoreTheoremProducer::orDistributivityRule: "
254  "input must be an AND of binary ORs: \n" + e.toString());
255  }
256 
257  const Expr& A = e[0][0];
258 
259  if(CHECK_PROOFS) {
260  for(Expr::iterator i=e.begin(),iend=e.end();i!=iend;++i) {
261  const Expr& ei = *i;
262  CHECK_SOUND(ei.isOr() && ei.arity() == 2,
263  "CoreTheoremProducer::andDistributivityRule: "
264  "input must be an AND of binary ORs: \n" + e.toString());
265  CHECK_SOUND(A == ei[0],
266  "CoreTheoremProducer::andDistributivityRule: "
267  "input must have a common factor: \n" + e.toString());
268  }
269  }
270  vector<Expr> output;
271  for(Expr::iterator i=e.begin(),iend=e.end();i!=iend;++i) {
272  output.push_back((*i)[1]);
273  }
274  Expr out = A.orExpr(andExpr(output));
275 
276  Proof pf;
277  if(withProof())
278  pf = newPf("and_distribuitivity_rule", e);
279 
280  return newRWTheorem(e, out, Assumptions::emptyAssump(), pf);
281 }
282 
283 // ==> IMPLIES(e1,e2) IFF OR(!e1, e2)
284 Theorem
286  Proof pf;
287  if(CHECK_PROOFS)
288  CHECK_SOUND(e.isImpl(), "rewriteImplies precondition violated");
289  if(withProof()) {
290  pf = newPf("rewrite_implies", e[0], e[1]);
291  }
292  return newRWTheorem(e, !e[0] || e[1], Assumptions::emptyAssump(), pf);
293 }
294 
295 // ==> DISTINCT(e1,...,en) IFF AND 1 <= i < j <= n (e[i] /= e[j])
296 Theorem
298  Proof pf;
299  if(CHECK_PROOFS) {
300  CHECK_SOUND(e.getKind() == DISTINCT, "rewriteDistinct precondition violated");
301  CHECK_SOUND(e.arity() > 0, "rewriteDistinct precondition violated");
302  }
303  Expr res;
304  if (e.arity() == 1) {
305  res = e.getEM()->trueExpr();
306  }
307  else if (e.arity() == 2) {
308  res = !(e[0].eqExpr(e[1]));
309  }
310  else {
311  vector<Expr> tmp;
312  for (int i = 0; i < e.arity(); ++i) {
313  for (int j = i+1; j < e.arity(); ++j) {
314  tmp.push_back(!(e[i].eqExpr(e[j])));
315  }
316  }
317  res = Expr(AND, tmp);
318  }
319  if(withProof()) {
320  pf = newPf("rewrite_distinct", e , res);
321  }
322 
323  return newRWTheorem(e, res, Assumptions::emptyAssump(), pf);
324 }
325 
326 // ==> NOT(e) == ITE(e, FALSE, TRUE)
327 Theorem
329  Proof pf;
330  if(CHECK_PROOFS)
331  CHECK_SOUND(not_e.isNot() && not_e[0].getType().isBool(),
332  "NotToIte precondition violated");
333  if(withProof())
334  pf = newPf("NotToIte", not_e[0]);
335  if(not_e[0].isTrue())
336  return d_core->getCommonRules()->rewriteNotTrue(not_e);
337  else if(not_e[0].isFalse())
338  return d_core->getCommonRules()->rewriteNotFalse(not_e);
339  Expr ite(not_e[0].iteExpr(d_em->falseExpr(), d_em->trueExpr()));
340  return newRWTheorem(not_e, ite, Assumptions::emptyAssump(), pf);
341 }
342 
343 // ==> Or(e) == ITE(e[1], TRUE, e[0])
344 Theorem
346  if(CHECK_PROOFS)
347  CHECK_SOUND(e.isOr(),
348  "OrToIte: precondition violated: " + e.toString());
349  Proof pf;
350  if(withProof()) {
351  pf = newPf("OrToIte", e);
352  }
353  const vector<Expr>& kids = e.getKids();
354  unsigned k(kids.size());
355  if(k==0)
356  return newRWTheorem(e, d_em->falseExpr(), Assumptions::emptyAssump(), pf);
357  if(k==1)
358  return newRWTheorem(e, e[0], Assumptions::emptyAssump(), pf);
359  Expr ite(kids[k-1]);
360  if(CHECK_PROOFS)
361  CHECK_SOUND(!ite.getType().isNull(),
362  "OrToIte: kid " + int2string(k-1) + " has no type: "
363  + (ite).toString());
364  for (; k > 1; k--) {
365  if (kids[k-2].isTrue()) {
366  ite = d_em->trueExpr();
367  break;
368  }
369  else if(kids[k-2].isFalse()) continue;
370  else{
371  if(CHECK_PROOFS)
372  CHECK_SOUND(!kids[k-2].getType().isNull(),
373  "OrToIte: kid " + int2string(k-2) + " has no type: "
374  + (kids[k-2]).toString());
375  ite = ite.iteExpr(d_em->trueExpr(), kids[k-2]);
376  }
377  }
378  return newRWTheorem(e, ite, Assumptions::emptyAssump(), pf);
379 }
380 
381 // ==> And(e) == ITE(e[1], e[0], FALSE)
382 Theorem
384  if(CHECK_PROOFS)
385  CHECK_SOUND(e.isAnd(),
386  "AndToIte: precondition violated: " + e.toString());
387  Proof pf;
388  if(withProof()) {
389  pf = newPf("AndToIte", e);
390  }
391  const vector<Expr>& kids = e.getKids();
392  unsigned k(kids.size());
393  if(k==0)
394  return newRWTheorem(e, d_em->trueExpr(), Assumptions::emptyAssump(), pf);
395  if(k==1)
396  return newRWTheorem(e, e[0], Assumptions::emptyAssump(), pf);
397  Expr ite(kids[k-1]);
398  if(CHECK_PROOFS)
399  CHECK_SOUND(!ite.getType().isNull(),
400  "AndToIte: kid " + int2string(k-1) + " has no type: "
401  + (ite).toString());
402  for (; k > 1; k--) {
403  if (kids[k-2].isFalse()) {
404  ite = d_em->falseExpr();
405  break;
406  }
407  else if(kids[k-2].isTrue()) {
408  continue;
409  }
410  else{
411  if(CHECK_PROOFS)
412  CHECK_SOUND(!kids[k-2].getType().isNull(),
413  "AndToIte: kid " + int2string(k-2) + " has no type: "
414  + (kids[k-2]).toString());
415  ite = ite.iteExpr(kids[k-2], d_em->falseExpr());
416  }
417  }
418  return newRWTheorem(e, ite, Assumptions::emptyAssump(), pf);
419 }
420 
421 // ==> IFF(a,b) == ITE(a, b, !b)
422 Theorem
424  if(CHECK_PROOFS)
425  CHECK_SOUND(e.isIff() && e[0].getType().isBool() && e[1].getType().isBool(),
426  "IffToIte: precondition violated: " + e.toString());
427  Proof pf;
428  if(e[0] == e[1]) return d_core->getCommonRules()->reflexivityRule(e);
429  Expr ite(e[0].iteExpr(e[1], e[1].iteExpr(d_em->falseExpr(),
430  d_em->trueExpr())));
431  if(withProof()) {
432  pf = newPf("iff_to_ite", e);
433  }
434  return newRWTheorem(e, ite, Assumptions::emptyAssump(), pf);
435 }
436 
437 // ==> IMPLIES(a,b) == ITE(a, b, TRUE)
438 Theorem
440  if(CHECK_PROOFS)
441  CHECK_SOUND(e.isImpl() && e[0].getType().isBool() && e[1].getType().isBool(),
442  "ImpToIte: precondition violated: " + e.toString());
443  Proof pf;
444  if(e[0] == e[1]) return d_core->getCommonRules()->reflexivityRule(e);
445  Expr ite(e[0].iteExpr(e[1], d_em->trueExpr()));
446  if(withProof()) {
447  pf = newPf("imp_to_ite", e);
448  }
449  return newRWTheorem(e, ite, Assumptions::emptyAssump(), pf);
450 }
451 
452 
453 // ==> ITE(e, FALSE, TRUE) IFF NOT(e)
454 Theorem
456 {
457  if (CHECK_PROOFS)
458  CHECK_SOUND(e.isITE() && e[1].isFalse() && e[2].isTrue(),
459  "rewriteIteToNot: " + e.toString());
460  Proof pf;
461  if (withProof()) pf = newPf("rewrite_ite_to_not", e);
462  return newRWTheorem(e, e[0].negate(), Assumptions::emptyAssump(), pf);
463 }
464 
465 // ==> ITE(a, TRUE, b) IFF OR(a, b)
466 Theorem
468 {
469  if (CHECK_PROOFS)
470  CHECK_SOUND(e.isITE() && e[1].isTrue(),
471  "rewriteIteToOr: " + e.toString());
472  Proof pf;
473  if (withProof()) pf = newPf("rewrite_ite_to_or", e);
474  return newRWTheorem(e, e[0] || e[2], Assumptions::emptyAssump(), pf);
475 }
476 
477 // ==> ITE(a, b, FALSE) IFF AND(a, b)
478 Theorem
480 {
481  if (CHECK_PROOFS)
482  CHECK_SOUND(e.isITE() && e[2].isFalse(),
483  "rewriteIteToAnd: " + e.toString());
484  Proof pf;
485  if (withProof()) pf = newPf("rewrite_ite_to_and", e);
486  return newRWTheorem(e, e[0] && e[1], Assumptions::emptyAssump(), pf);
487 }
488 
489 // ==> ITE(a, b, !b) IFF IFF(a, b)
490 Theorem
492 {
493  if (CHECK_PROOFS)
494  CHECK_SOUND(e.isITE() && e[1] == e[2].negate(),
495  "rewriteIteToIff: " + e.toString());
496  Proof pf;
497  if (withProof()) pf = newPf("rewrite_ite_to_iff", e);
498  return newRWTheorem(e, e[0].iffExpr(e[1]), Assumptions::emptyAssump(), pf);
499 }
500 
501 // ==> ITE(a, b, TRUE) IFF IMPLIES(a, b)
502 Theorem
504 {
505  if (CHECK_PROOFS)
506  CHECK_SOUND(e.isITE() && e[2].isTrue(),
507  "rewriteIteToImp: " + e.toString());
508  Proof pf;
509  if (withProof()) pf = newPf("rewrite_ite_to_imp", e);
510  return newRWTheorem(e, e[0].impExpr(e[1]), Assumptions::emptyAssump(), pf);
511 }
512 
513 
514 // ==> ITE(a, b(a), c(a)) IFF ITE(a, b(TRUE), c(FALSE))
515 // ==> ITE(x = y, b, c) IFF ITE(x = y b[x/y], c[x = y/FALSE])
517 {
518  if (CHECK_PROOFS)
519  CHECK_SOUND(e.isITE() && e.arity()==3, "rewriteIteCond: " + e.toString());
520 
521  vector<Expr> oldTerms, newTerms;
522 // // if (e[0].isEq()) {
523 // // oldTerms.push_back(e[0][0]);
524 // // newTerms.push_back(e[0][1]);
525 // // }
526 // // else {
527  oldTerms.push_back(e[0]);
528  newTerms.push_back(d_em->trueExpr());
529 // }
530 
531  Expr e1(e[1].substExpr(oldTerms, newTerms));
532  oldTerms[0] = e[0];
533  newTerms[0] = d_em->falseExpr();
534  Expr e2(e[2].substExpr(oldTerms, newTerms));
535 
536  Proof pf;
537  if (withProof()) pf = newPf("rewrite_ite_cond", e);
538  return newRWTheorem(e, e[0].iteExpr(e1, e2), Assumptions::emptyAssump(), pf);
539 }
540 
541 
542 Theorem
544  if(CHECK_PROOFS) {
545  CHECK_SOUND(iff.isIff() && iff.arity()==2, "iffOrDistrib("
546  +iff.toString()+")");
547  CHECK_SOUND(iff[0].isOr() && iff[0].arity()==2, "iffOrDistrib("
548  +iff.toString()+")");
549  CHECK_SOUND(iff[1].isOr() && iff[1].arity()==2, "iffOrDistrib("
550  +iff.toString()+")");
551  CHECK_SOUND(iff[0][0]==iff[1][0], "iffOrDistrib("
552  +iff.toString()+")");
553  }
554  const Expr& a = iff[0][0];
555  const Expr& b = iff[0][1];
556  const Expr& c = iff[1][1];
557  Proof pf;
558  if(withProof())
559  pf = newPf("iff_or_distrib", iff);
560  return newRWTheorem(iff, (a || (b.iffExpr(c))), Assumptions::emptyAssump(), pf);
561 }
562 
563 
564 Theorem
566  if(CHECK_PROOFS) {
567  CHECK_SOUND(iff.isIff() && iff.arity()==2, "iffAndDistrib("
568  +iff.toString()+")");
569  CHECK_SOUND(iff[0].isAnd() && iff[0].arity()==2, "iffAndDistrib("
570  +iff.toString()+")");
571  CHECK_SOUND(iff[1].isAnd() && iff[1].arity()==2, "iffAndDistrib("
572  +iff.toString()+")");
573  CHECK_SOUND(iff[0][0]==iff[1][0], "iffOrDistrib("
574  +iff.toString()+")");
575  }
576  const Expr& a = iff[0][0];
577  const Expr& b = iff[0][1];
578  const Expr& c = iff[1][1];
579  Proof pf;
580  if(withProof())
581  pf = newPf("iff_and_distrib", iff);
582  return newRWTheorem(iff, (!a || (b.iffExpr(c))), Assumptions::emptyAssump(), pf);
583 }
584 
585 
586 // |- op(ITE(cond,a,b)) =/<=> ITE(cond,op(a),op(b))
587 Theorem
589  if(CHECK_PROOFS) {
590  CHECK_SOUND(e.arity()==1 && e[0].isITE(),
591  "CoreTheoremProducer::ifLiftUnaryRule("
592  "e = " + e.toString() + ")");
593  }
594  Op op(e.getOp());
595  const Expr& ite = e[0];
596  const Expr& cond = ite[0];
597  const Expr& t1 = ite[1];
598  const Expr& t2 = ite[2];
599 
600  if(CHECK_PROOFS) {
601  CHECK_SOUND(cond.getType().isBool(),
602  "CoreTheoremProducer::ifLiftUnaryRule("
603  "e = " + e.toString()+")");
604  }
605 
606  Expr e1 = Expr(op, t1);
607  Expr e2 = Expr(op, t2);
608 
609  Expr resultITE = cond.iteExpr(e1, e2);
610 
611  Proof pf;
612  if (withProof())
613  pf = newPf("if_lift_unary_rule", e);
614  return newRWTheorem(e, resultITE, Assumptions::emptyAssump(), pf);
615 }
616 
617 
618 // (a & b) <=> a & b[a/true]; takes the index of a and rewrites all
619 // the other conjuncts.
620 Theorem
622  if(CHECK_PROOFS) {
623  CHECK_SOUND(e.isAnd() && 0 <= idx && idx < e.arity(),
624  "rewriteAndSubterms("+e.toString()
625  +", idx="+int2string(idx)
626  +"):\n Expected an AND and a valid index of a child");
627  }
628  vector<Expr> kids;
629  ExprHashMap<Expr> subst;
630  subst.insert(e[idx], d_em->trueExpr());
631  for(int i=0, iend=e.arity(); i<iend; ++i) {
632  if(i==idx)
633  kids.push_back(e[i]);
634  else
635  kids.push_back(e[i].substExpr(subst));
636  }
637  Proof pf;
638  if(withProof())
639  pf = newPf("rewrite_and_subterms", e, d_em->newRatExpr(idx));
640  return newRWTheorem(e, Expr(e.getOp(), kids), Assumptions::emptyAssump(), pf);
641 }
642 
643 
644 // (a | b) <=> a | b[a/false]; takes the index of a and rewrites all
645 // the other disjuncts.
646 Theorem
648  if(CHECK_PROOFS) {
649  CHECK_SOUND(e.isOr() && 0 <= idx && idx < e.arity(),
650  "rewriteOrSubterms("+e.toString()
651  +", idx="+int2string(idx)
652  +"):\n Expected an OR and a valid index of a child");
653  }
654  vector<Expr> kids;
655  ExprHashMap<Expr> subst;
656  subst.insert(e[idx], d_em->falseExpr());
657  for(int i=0, iend=e.arity(); i<iend; ++i) {
658  if(i==idx)
659  kids.push_back(e[i]);
660  else
661  kids.push_back(e[i].substExpr(subst));
662  }
663  Proof pf;
664  if(withProof())
665  pf = newPf("rewrite_or_subterms", e, d_em->newRatExpr(idx));
666  return newRWTheorem(e, Expr(e.getOp(), kids), Assumptions::emptyAssump(), pf);
667 }
668 
669 
671 {
672  Proof pf;
673  return newTheorem(e, Assumptions::emptyAssump(), pf);
674 }
Theorem IffToIte(const Expr &e)
==> IFF(a,b) == ITE(a, b, !b)
int arity() const
Definition: expr.h:1201
bool isIff() const
Definition: expr.h:424
iterator begin() const
Begin iterator.
Definition: expr.h:1211
Data structure of expressions in CVC3.
Definition: expr.h:133
Theorem rewriteIteToOr(const Expr &e)
==> ITE(a, TRUE, b) IFF OR(a, b)
ExprManager * getEM() const
Definition: expr.h:1156
Expr iteExpr(const Expr &thenpart, const Expr &elsepart) const
Definition: expr.h:961
CoreProofRules * createProofRules(TheoremManager *tm)
Private method to get a new theorem producer.
Theorem rewriteNotIte(const Expr &e)
==> NOT ITE(a,b,c) IFF ITE(a,NOT b,NOT c)
bool isTrue() const
Definition: expr.h:356
Theorem iffOrDistrib(const Expr &iff)
((a|b)<=>(a|c))<=>(a|(b<=>c)); takes ((a|b)<=>(a|c)) as 'iff'
bool isImpl() const
Definition: expr.h:425
Theorem OrToIte(const Expr &e)
==> Or(e) == ITE(e[1], TRUE, e[0])
bool isITE() const
Definition: expr.h:423
Theorem rewriteIteCond(const Expr &e)
==> ITE(a, b(a), c(a)) IFF ITE(a, b(TRUE), c(FALSE))
Definition: kinds.h:227
Theorem rewriteIteToAnd(const Expr &e)
==> ITE(a, b, FALSE) IFF AND(a, b)
Theorem rewriteIteElse(const Expr &e, const Theorem &elseThm)
!a |- c == d ==> ITE(a, b, c) == ITE(a, b, d)
bool isFalse() const
Definition: expr.h:355
MS C++ specific settings.
Definition: type.h:42
Theorem ImpToIte(const Expr &e)
==> IMPLIES(a,b) == ITE(a, b, TRUE)
Theorem rewriteNotAnd(const Expr &e)
==> NOT (AND e1 ... en) IFF (OR !e1 ... !en), takes (AND ...)
Expr eqExpr(const Expr &right) const
Definition: expr.h:929
bool isBool() const
Definition: type.h:60
Theorem rewriteIteToImp(const Expr &e)
==> ITE(a, b, TRUE) IFF IMPLIES(a, b)
Theorem rewriteIteToNot(const Expr &e)
==> ITE(e, FALSE, TRUE) IFF NOT(e)
Theorem rewriteDistinct(const Expr &e)
==> DISTINCT(e1,...,en) IFF AND 1 <= i < j <= n (e[i] /= e[j])
#define DebugAssert(cond, str)
Definition: debug.h:408
#define CHECK_SOUND(cond, msg)
void insert(const Expr &e, const Data &d)
Definition: expr_map.h:312
#define CHECK_PROOFS
bool isOr() const
Definition: expr.h:422
const std::vector< Expr > & getKids() const
Definition: expr.h:1162
Expr andExpr(const Expr &right) const
Definition: expr.h:941
Expr orExpr(const std::vector< Expr > &children)
Definition: expr.h:955
Op getOp() const
Get operator from expression.
Definition: expr.h:1183
bool isNot() const
Definition: expr.h:420
Theorem rewriteAndSubterms(const Expr &e, int idx)
(a & b) <=> a & b[a/true]; takes the index of a
Theorem dummyTheorem(const Expr &e)
Temporary cheat for building theorems.
Theorem rewriteIteBool(const Expr &c, const Expr &e1, const Expr &e2)
==> ITE(c, e1, e2) <=> (c => e1) AND (!c => e2)
Theorem rewriteLetDecl(const Expr &e)
Replace LETDECL with its definition.
Theorem rewriteIteThen(const Expr &e, const Theorem &thenThm)
a |- b == d ==> ITE(a, b, c) == ITE(a, d, c)
std::string toString() const
Print the expression to a string.
Definition: expr.cpp:344
Expr iffExpr(const Expr &right) const
Definition: expr.h:965
Theorem rewriteIteToIff(const Expr &e)
==> ITE(a, b, !b) IFF IFF(a, b)
Expr negate() const
Definition: expr.h:937
int getKind() const
Definition: expr.h:1168
std::string int2string(int n)
Definition: cvc_util.h:46
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
Theorem rewriteImplies(const Expr &e)
==> IMPLIES(e1,e2) IFF OR(!e1, e2)
Proof getProof() const
Definition: theorem.cpp:402
const Assumptions & getAssumptionsRef() const
Definition: theorem.cpp:385
Expr getExpr() const
Definition: theorem.cpp:230
Expr orExpr(const Expr &right) const
Definition: expr.h:951
Theorem rewriteOrSubterms(const Expr &e, int idx)
(a | b) <=> a | b[a/false]; takes the index of a
Theorem NotToIte(const Expr &not_e)
==> NOT(e) == ITE(e, FALSE, TRUE)
Theorem iffAndDistrib(const Expr &iff)
((a&b)<=>(a&c))<=>(!a|(b<=>c)); takes ((a&b)<=>(a&c)) as 'iff'
Theorem andDistributivityRule(const Expr &e)
|= (A | B1) & (A | B2) & ... & (A | bn) <=> A | (B1 & B2 & ...& Bn)
Theorem rewriteNotIff(const Expr &e)
==> NOT IFF(e1,e2) IFF IFF(e1,NOT e2)
Theorem orDistributivityRule(const Expr &e)
|= (A & B1) | (A & B2) | ... | (A & bn) <=> A & (B1 | B2 | ...| Bn)
const Expr & getLHS() const
Definition: theorem.cpp:240
Definition: kinds.h:63
Type getType() const
Get the type. Recursively compute if necessary.
Definition: expr.h:1259
bool isRewrite() const
Definition: theorem.cpp:224
Theorem AndToIte(const Expr &e)
==> And(e) == ITE(e[1], e[0], FALSE)
Theorem rewriteNotOr(const Expr &e)
==> NOT (OR e1 ... en) IFF (AND !e1 ... !en), takes (OR ...)
static const Assumptions & emptyAssump()
Definition: assumptions.h:83
Expr andExpr(const std::vector< Expr > &children)
Definition: expr.h:945
Theorem ifLiftUnaryRule(const Expr &e)
|- op(ITE(cond,a,b)) =/<=> ITE(cond,op(a),op(b))
Definition: kinds.h:67
Theorem typePred(const Expr &e)
e: T ==> |- typePred_T(e) [deriving the type predicate of e]
iterator end() const
End iterator.
Definition: expr.h:1217
bool isAnd() const
Definition: expr.h:421