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