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));
Theorem IffToIte(const Expr &e)
==> IFF(a,b) == ITE(a, b, !b)
iterator begin() const
Begin iterator.
Data structure of expressions in CVC3.
Theorem rewriteIteToOr(const Expr &e)
==> ITE(a, TRUE, b) IFF OR(a, b)
ExprManager * getEM() const
Expr iteExpr(const Expr &thenpart, const Expr &elsepart) const
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)
Theorem iffOrDistrib(const Expr &iff)
((a|b)<=>(a|c))<=>(a|(b<=>c)); takes ((a|b)<=>(a|c)) as 'iff'
Theorem OrToIte(const Expr &e)
==> Or(e) == ITE(e[1], TRUE, e[0])
Theorem rewriteIteCond(const Expr &e)
==> ITE(a, b(a), c(a)) IFF ITE(a, b(TRUE), c(FALSE))
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)
MS C++ specific settings.
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
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)
#define CHECK_SOUND(cond, msg)
void insert(const Expr &e, const Data &d)
const std::vector< Expr > & getKids() const
Expr andExpr(const Expr &right) const
Expr orExpr(const std::vector< Expr > &children)
Op getOp() const
Get operator from expression.
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.
Expr iffExpr(const Expr &right) const
Theorem rewriteIteToIff(const Expr &e)
==> ITE(a, b, !b) IFF IFF(a, b)
std::string int2string(int n)
const Expr & getRHS() const
const Expr & trueExpr()
TRUE Expr.
Theorem rewriteImplies(const Expr &e)
==> IMPLIES(e1,e2) IFF OR(!e1, e2)
const Assumptions & getAssumptionsRef() const
Expr orExpr(const Expr &right) const
Theorem rewriteOrSubterms(const Expr &e, int idx)
(a | b) <=> a | b[a/false]; takes the index of a
Theorem NotToIte(const Expr ¬_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
Type getType() const
Get the type. Recursively compute if necessary.
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()
Expr andExpr(const std::vector< Expr > &children)
Theorem ifLiftUnaryRule(const Expr &e)
|- op(ITE(cond,a,b)) =/<=> ITE(cond,op(a),op(b))
Theorem typePred(const Expr &e)
e: T ==> |- typePred_T(e) [deriving the type predicate of e]
iterator end() const
End iterator.