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
createProofRules(TheoremManager * tm)45 CoreProofRules* TheoryCore::createProofRules(TheoremManager* tm) {
46   return new CoreTheoremProducer(tm, this);
47 }
48 
49 
50 // e: T ==> |- typePred_T(e)  [asserting the type predicate of e]
51 Theorem
typePred(const Expr & e)52 CoreTheoremProducer::typePred(const Expr& e) {
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
rewriteLetDecl(const Expr & e)64 CoreTheoremProducer::rewriteLetDecl(const Expr& e) {
65   if(CHECK_PROOFS)
66     CHECK_SOUND(e.getKind() == LETDECL,
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 ...)
rewriteNotAnd(const Expr & e)75 Theorem CoreTheoremProducer::rewriteNotAnd(const Expr& e) {
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
rewriteNotOr(const Expr & e)93 CoreTheoremProducer::rewriteNotOr(const Expr& e) {
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
rewriteNotIff(const Expr & e)110 CoreTheoremProducer::rewriteNotIff(const Expr& e) {
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
rewriteNotIte(const Expr & e)123 CoreTheoremProducer::rewriteNotIte(const Expr& e) {
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
rewriteIteThen(const Expr & e,const Theorem & thenThm)136 CoreTheoremProducer::rewriteIteThen(const Expr& e, const Theorem& thenThm) {
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
rewriteIteElse(const Expr & e,const Theorem & elseThm)161 CoreTheoremProducer::rewriteIteElse(const Expr& e, const Theorem& elseThm) {
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
rewriteIteBool(const Expr & c,const Expr & e1,const Expr & e2)186 CoreTheoremProducer::rewriteIteBool(const Expr& c,
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
orDistributivityRule(const Expr & e)202 CoreTheoremProducer::orDistributivityRule(const Expr& e) {
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
andDistributivityRule(const Expr & e)245 CoreTheoremProducer::andDistributivityRule(const Expr& e) {
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
rewriteImplies(const Expr & e)285 CoreTheoremProducer::rewriteImplies(const Expr& e) {
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
rewriteDistinct(const Expr & e)297 CoreTheoremProducer::rewriteDistinct(const Expr& e) {
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
NotToIte(const Expr & not_e)328 CoreTheoremProducer::NotToIte(const Expr& not_e){
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
OrToIte(const Expr & e)345 CoreTheoremProducer::OrToIte(const Expr& e){
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
AndToIte(const Expr & e)383 CoreTheoremProducer::AndToIte(const Expr& e){
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
IffToIte(const Expr & e)423 CoreTheoremProducer::IffToIte(const Expr& e){
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
ImpToIte(const Expr & e)439 CoreTheoremProducer::ImpToIte(const Expr& e){
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
rewriteIteToNot(const Expr & e)455 CoreTheoremProducer::rewriteIteToNot(const Expr& e)
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
rewriteIteToOr(const Expr & e)467 CoreTheoremProducer::rewriteIteToOr(const Expr& e)
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
rewriteIteToAnd(const Expr & e)479 CoreTheoremProducer::rewriteIteToAnd(const Expr& e)
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
rewriteIteToIff(const Expr & e)491 CoreTheoremProducer::rewriteIteToIff(const Expr& e)
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
rewriteIteToImp(const Expr & e)503 CoreTheoremProducer::rewriteIteToImp(const Expr& e)
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])
rewriteIteCond(const Expr & e)516 Theorem CoreTheoremProducer::rewriteIteCond(const Expr& e)
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
iffOrDistrib(const Expr & iff)543 CoreTheoremProducer::iffOrDistrib(const Expr& iff) {
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
iffAndDistrib(const Expr & iff)565 CoreTheoremProducer::iffAndDistrib(const Expr& iff) {
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
ifLiftUnaryRule(const Expr & e)588 CoreTheoremProducer::ifLiftUnaryRule(const Expr& e) {
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
rewriteAndSubterms(const Expr & e,int idx)621 CoreTheoremProducer::rewriteAndSubterms(const Expr& e, int idx) {
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
rewriteOrSubterms(const Expr & e,int idx)647 CoreTheoremProducer::rewriteOrSubterms(const Expr& e, int idx) {
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 
dummyTheorem(const Expr & e)670 Theorem CoreTheoremProducer::dummyTheorem(const Expr& e)
671 {
672   Proof pf;
673   return newTheorem(e, Assumptions::emptyAssump(), pf);
674 }
675