33 #define _CVC3_TRUSTED_
54 Expr pred(d_core->getTypePred(tp, e));
57 pf = newPf(
"type_pred", e, tp.getExpr());
67 "rewriteLetDecl: wrong expression: " + e.
toString());
70 pf = newPf(
"rewrite_letdecl", e[1]);
78 "rewriteNotAnd: precondition violated: " + e.
toString());
84 kids.push_back(i->negate());
87 pf = newPf(
"rewrite_not_and", e);
96 "rewriteNotOr: precondition violated: " + e.
toString());
100 kids.push_back(i->negate());
103 pf = newPf(
"rewrite_not_or", e);
115 pf = newPf(
"rewrite_not_iff", e);
128 pf = newPf(
"rewrite_not_ite", e);
139 CHECK_SOUND(withAssumptions(),
"Cannot check proof without assumptions");
141 "rewriteIteThen precondition violated \n then expression: "
151 pf = newPf(
"rewrite_ite_then_iff", e, thenThm.
getProof());
153 pf = newPf(
"rewrite_ite_then", e, thenThm.
getProof());
156 return newRWTheorem(e, e[0].iteExpr(thenThm.
getRHS(), e[2]), a, pf);
164 CHECK_SOUND(withAssumptions(),
"Cannot check proof without assumptions");
166 "rewriteIteElse precondition violated \n else expression: "
176 pf = newPf(
"rewrite_ite_else_iff", e, elseThm.
getProof());
178 pf = newPf(
"rewrite_ite_else", e, elseThm.
getProof());
181 return newRWTheorem(e, e[0].iteExpr(e[1], elseThm.
getRHS()), a, pf);
190 "rewriteIteBool: Not a boolean ITE: "
194 pf = newPf(
"rewrite_ite_bool", c, e1, e2);
195 return newRWTheorem(c.
iteExpr(e1,e2),
205 "CoreTheoremProducer::orDistributivityRule: "
206 "input must be an OR expr: \n" + e.
toString());
207 const Expr& e0 = e[0];
210 "CoreTheoremProducer::orDistributivityRule: "
211 "input must be an OR of binary ANDs: \n" + e.
toString());
214 const Expr& A = e[0][0];
220 "CoreTheoremProducer::orDistributivityRule: "
221 "input must be an OR of binary ANDs: \n" + e.
toString());
223 "CoreTheoremProducer::orDistributivityRule: "
224 "input must have a common factor: \n" + e.
toString());
230 output.push_back(ei[1]);
236 pf = newPf(
"or_distribuitivity_rule", e);
248 "CoreTheoremProducer::andDistributivityRule: "
249 "input must be an AND expr: \n" + e.
toString());
250 const Expr& e0 = e[0];
253 "CoreTheoremProducer::orDistributivityRule: "
254 "input must be an AND of binary ORs: \n" + e.
toString());
257 const Expr& A = e[0][0];
263 "CoreTheoremProducer::andDistributivityRule: "
264 "input must be an AND of binary ORs: \n" + e.
toString());
266 "CoreTheoremProducer::andDistributivityRule: "
267 "input must have a common factor: \n" + e.
toString());
272 output.push_back((*i)[1]);
278 pf = newPf(
"and_distribuitivity_rule", e);
290 pf = newPf(
"rewrite_implies", e[0], e[1]);
304 if (e.
arity() == 1) {
307 else if (e.
arity() == 2) {
308 res = !(e[0].
eqExpr(e[1]));
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])));
320 pf = newPf(
"rewrite_distinct", e , res);
332 "NotToIte precondition violated");
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()));
348 "OrToIte: precondition violated: " + e.
toString());
351 pf = newPf(
"OrToIte", e);
353 const vector<Expr>& kids = e.
getKids();
354 unsigned k(kids.size());
362 "OrToIte: kid " +
int2string(k-1) +
" has no type: "
365 if (kids[k-2].isTrue()) {
366 ite = d_em->trueExpr();
369 else if(kids[k-2].isFalse())
continue;
373 "OrToIte: kid " +
int2string(k-2) +
" has no type: "
374 + (kids[k-2]).toString());
375 ite = ite.
iteExpr(d_em->trueExpr(), kids[k-2]);
386 "AndToIte: precondition violated: " + e.
toString());
389 pf = newPf(
"AndToIte", e);
391 const vector<Expr>& kids = e.
getKids();
392 unsigned k(kids.size());
400 "AndToIte: kid " +
int2string(k-1) +
" has no type: "
403 if (kids[k-2].isFalse()) {
404 ite = d_em->falseExpr();
407 else if(kids[k-2].isTrue()) {
413 "AndToIte: kid " +
int2string(k-2) +
" has no type: "
414 + (kids[k-2]).toString());
415 ite = ite.
iteExpr(kids[k-2], d_em->falseExpr());
426 "IffToIte: precondition violated: " + e.
toString());
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(),
432 pf = newPf(
"iff_to_ite", e);
442 "ImpToIte: precondition violated: " + e.
toString());
444 if(e[0] == e[1])
return d_core->getCommonRules()->reflexivityRule(e);
445 Expr ite(e[0].iteExpr(e[1], d_em->trueExpr()));
447 pf = newPf(
"imp_to_ite", e);
459 "rewriteIteToNot: " + e.
toString());
461 if (withProof()) pf = newPf(
"rewrite_ite_to_not", e);
473 if (withProof()) pf = newPf(
"rewrite_ite_to_or", e);
483 "rewriteIteToAnd: " + e.
toString());
485 if (withProof()) pf = newPf(
"rewrite_ite_to_and", e);
495 "rewriteIteToIff: " + e.
toString());
497 if (withProof()) pf = newPf(
"rewrite_ite_to_iff", e);
507 "rewriteIteToImp: " + e.
toString());
509 if (withProof()) pf = newPf(
"rewrite_ite_to_imp", e);
521 vector<Expr> oldTerms, newTerms;
527 oldTerms.push_back(e[0]);
528 newTerms.push_back(d_em->trueExpr());
531 Expr e1(e[1].substExpr(oldTerms, newTerms));
533 newTerms[0] = d_em->falseExpr();
534 Expr e2(e[2].substExpr(oldTerms, newTerms));
537 if (withProof()) pf = newPf(
"rewrite_ite_cond", e);
547 CHECK_SOUND(iff[0].isOr() && iff[0].arity()==2,
"iffOrDistrib("
549 CHECK_SOUND(iff[1].isOr() && iff[1].arity()==2,
"iffOrDistrib("
554 const Expr& a = iff[0][0];
555 const Expr& b = iff[0][1];
556 const Expr& c = iff[1][1];
559 pf = newPf(
"iff_or_distrib", iff);
569 CHECK_SOUND(iff[0].isAnd() && iff[0].arity()==2,
"iffAndDistrib("
571 CHECK_SOUND(iff[1].isAnd() && iff[1].arity()==2,
"iffAndDistrib("
576 const Expr& a = iff[0][0];
577 const Expr& b = iff[0][1];
578 const Expr& c = iff[1][1];
581 pf = newPf(
"iff_and_distrib", iff);
591 "CoreTheoremProducer::ifLiftUnaryRule("
595 const Expr& ite = e[0];
596 const Expr& cond = ite[0];
597 const Expr& t1 = ite[1];
598 const Expr& t2 = ite[2];
602 "CoreTheoremProducer::ifLiftUnaryRule("
613 pf = newPf(
"if_lift_unary_rule", e);
626 +
"):\n Expected an AND and a valid index of a child");
630 subst.
insert(e[idx], d_em->trueExpr());
631 for(
int i=0, iend=e.
arity(); i<iend; ++i) {
633 kids.push_back(e[i]);
635 kids.push_back(e[i].substExpr(subst));
639 pf = newPf(
"rewrite_and_subterms", e, d_em->newRatExpr(idx));
652 +
"):\n Expected an OR and a valid index of a child");
656 subst.
insert(e[idx], d_em->falseExpr());
657 for(
int i=0, iend=e.
arity(); i<iend; ++i) {
659 kids.push_back(e[i]);
661 kids.push_back(e[i].substExpr(subst));
665 pf = newPf(
"rewrite_or_subterms", e, d_em->newRatExpr(idx));