core_theorem_producer.cpp

Go to the documentation of this file.
00001 /*****************************************************************************/
00002 /*!
00003  * \file core_theorem_producer.cpp
00004  * 
00005  * Author: Sergey Berezin
00006  * 
00007  * Created: Feb 05 03:40:36 GMT 2003
00008  *
00009  * <hr>
00010  *
00011  * License to use, copy, modify, sell and/or distribute this software
00012  * and its documentation for any purpose is hereby granted without
00013  * royalty, subject to the terms and conditions defined in the \ref
00014  * LICENSE file provided with this distribution.
00015  * 
00016  * <hr>
00017  * 
00018  */
00019 /*****************************************************************************/
00020 // CLASS: CoreTheoremProducer
00021 //
00022 // AUTHOR: Sergey Berezin, 12/09/2002
00023 //         Vijay Ganesh, september 15th, 2004 (CNF Converter rules)
00024 //
00025 // Description: Implementation of the proof rules for ground
00026 // equational logic (reflexivity, symmetry, transitivity, and
00027 // substitutivity).
00028 //
00029 ///////////////////////////////////////////////////////////////////////////////
00030 
00031 
00032 // This code is trusted
00033 #define _CVC3_TRUSTED_
00034 
00035 
00036 #include "core_theorem_producer.h"
00037 #include "theory_core.h"
00038 
00039 
00040 using namespace CVC3;
00041 using namespace std;
00042 
00043 
00044 // The trusted method of TheoryCore which creates this theorem producer
00045 CoreProofRules* TheoryCore::createProofRules(TheoremManager* tm) {
00046   return new CoreTheoremProducer(tm, this);
00047 }
00048 
00049 
00050 // e: T ==> |- typePred_T(e)  [asserting the type predicate of e]
00051 Theorem
00052 CoreTheoremProducer::typePred(const Expr& e) {
00053   Type tp(e.getType());
00054   Expr pred(d_core->getTypePred(tp, e));
00055   Proof pf;
00056   if(withProof()) {
00057     pf = newPf("type_pred", e, tp.getExpr());
00058   }
00059   return newTheorem(pred, Assumptions::emptyAssump(), pf);
00060 }
00061 
00062 
00063 Theorem
00064 CoreTheoremProducer::rewriteLetDecl(const Expr& e) {
00065   if(CHECK_PROOFS)
00066     CHECK_SOUND(e.getKind() == LETDECL,
00067     "rewriteLetDecl: wrong expression: " + e.toString());
00068   Proof pf;
00069   if(withProof()) // FIXME: implement this in flea
00070     pf = newPf("rewrite_letdecl", e[1]);
00071   return newRWTheorem(e, e[1], Assumptions::emptyAssump(), pf);
00072 }
00073 
00074 // ==> NOT (AND e1 ... en) IFF (OR !e1 ... !en), takes (AND ...)
00075 Theorem CoreTheoremProducer::rewriteNotAnd(const Expr& e) {
00076  if(CHECK_PROOFS)
00077   CHECK_SOUND(e.isNot() && e[0].isAnd(),
00078     "rewriteNotAnd: precondition violated: " + e.toString());
00079 
00080   
00081   vector<Expr> kids; // vector of <!e1,...,!en>
00082   for(Expr::iterator i=e[0].begin(), iend=e[0].end(); i!=iend; ++i)
00083     // Collapse double negations
00084     kids.push_back(i->negate());
00085   Proof pf;
00086   if(withProof())
00087     pf = newPf("rewrite_not_and", e);
00088   return newRWTheorem(e, orExpr(kids), Assumptions::emptyAssump(), pf);
00089 }
00090 
00091 // ==> NOT (OR e1 ... en) IFF (AND !e1 ... !en), takes (OR ...)
00092 Theorem
00093 CoreTheoremProducer::rewriteNotOr(const Expr& e) {
00094   if(CHECK_PROOFS)
00095     CHECK_SOUND(e.isNot() && e[0].isOr(),
00096     "rewriteNotOr: precondition violated: " + e.toString());
00097   vector<Expr> kids; // vector of <!e1,...,!en>
00098   for(Expr::iterator i=e[0].begin(), iend=e[0].end(); i!=iend; ++i)
00099     // Collapse double negations
00100     kids.push_back(i->negate());
00101   Proof pf;
00102   if(withProof())
00103     pf = newPf("rewrite_not_or", e);
00104   return newRWTheorem(e, andExpr(kids), Assumptions::emptyAssump(), pf);
00105 }
00106 
00107 
00108 // ==> NOT IFF(e1,e2) IFF IFF(e1,NOT e2)
00109 Theorem
00110 CoreTheoremProducer::rewriteNotIff(const Expr& e) {
00111   Proof pf;
00112   if(CHECK_PROOFS)
00113     CHECK_SOUND(e.isNot() && e[0].isIff(), "rewriteNotIff precondition violated");
00114   if(withProof()) {
00115     pf = newPf("rewrite_not_iff", e);
00116   }
00117   return newRWTheorem(e, e[0][0].iffExpr(!e[0][1]), Assumptions::emptyAssump(), pf);
00118 }
00119 
00120 
00121 // ==> NOT ITE(a,b,c) IFF ITE(a,NOT b,NOT c)
00122 Theorem
00123 CoreTheoremProducer::rewriteNotIte(const Expr& e) {
00124   Proof pf;
00125   if(CHECK_PROOFS)
00126     CHECK_SOUND(e.isNot() && e[0].isITE(), "rewriteNotIte precondition violated");
00127   if(withProof()) {
00128     pf = newPf("rewrite_not_ite", e);
00129   }
00130   return newRWTheorem(e, e[0][0].iteExpr(!e[0][1], !e[0][2]), Assumptions::emptyAssump(), pf);
00131 }
00132 
00133 
00134 // a |- b == d ==> ITE(a, b, c) == ITE(a, d, c)
00135 Theorem
00136 CoreTheoremProducer::rewriteIteThen(const Expr& e, const Theorem& thenThm) {
00137   Proof pf;
00138   if(CHECK_PROOFS) {
00139     CHECK_SOUND(withAssumptions(), "Cannot check proof without assumptions");
00140     CHECK_SOUND(e.isITE() && thenThm.isRewrite() && e[1] == thenThm.getLHS(),
00141     "rewriteIteThen precondition violated \n then expression: "
00142     + thenThm.getExpr().toString() + "\n e = " + e.toString());
00143   }
00144   Assumptions a = thenThm.getAssumptionsRef() - e[0];
00145   if(withProof()) {
00146     Type t = e.getType();
00147     DebugAssert(!t.isNull(), "rewriteIteThen: e has no type: "
00148     + e.toString());
00149     bool useIff = t.isBool();
00150     if(useIff)
00151       pf = newPf("rewrite_ite_then_iff", e, thenThm.getProof());
00152     else {
00153       pf = newPf("rewrite_ite_then", e, thenThm.getProof());
00154     }
00155   }
00156   return newRWTheorem(e, e[0].iteExpr(thenThm.getRHS(), e[2]), a, pf);
00157 }
00158 
00159 // !a |- c == d ==> ITE(a, b, c) == ITE(a, b, d)
00160 Theorem
00161 CoreTheoremProducer::rewriteIteElse(const Expr& e, const Theorem& elseThm) {
00162   Proof pf;
00163   if(CHECK_PROOFS) {
00164     CHECK_SOUND(withAssumptions(), "Cannot check proof without assumptions");
00165     CHECK_SOUND(e.isITE() && elseThm.isRewrite() && e[2] == elseThm.getLHS(),
00166     "rewriteIteElse precondition violated \n else expression: "
00167     + elseThm.getExpr().toString() + "\n e = " + e.toString());
00168   }
00169   Assumptions a = elseThm.getAssumptionsRef() - !e[0];
00170   if(withProof()) {
00171     Type t = e.getType();
00172     DebugAssert(!t.isNull(), "rewriteIteElse: e has no type: "
00173     + e.toString());
00174     bool useIff = t.isBool();
00175     if(useIff)
00176       pf = newPf("rewrite_ite_else_iff", e, elseThm.getProof());
00177     else {
00178       pf = newPf("rewrite_ite_else", e, elseThm.getProof());
00179     }
00180   }
00181   return newRWTheorem(e, e[0].iteExpr(e[1], elseThm.getRHS()), a, pf);
00182 }
00183 
00184 // ==> ITE(c, e1, e2) <=> (!c OR e1) AND (c OR e2)
00185 Theorem 
00186 CoreTheoremProducer::rewriteIteBool(const Expr& c,
00187                                     const Expr& e1, const Expr& e2) {
00188   if(CHECK_PROOFS)
00189     CHECK_SOUND(e1.getType().isBool() && e2.getType().isBool(),
00190     "rewriteIteBool: Not a boolean ITE: "
00191     + c.iteExpr(e1, e2).toString());
00192   Proof pf;
00193   if(withProof())
00194     pf = newPf("rewrite_ite_bool", c, e1, e2);
00195   return newRWTheorem(c.iteExpr(e1,e2),
00196           (e1.orExpr(!c).andExpr(c.orExpr(e2))), Assumptions::emptyAssump(), pf);
00197 }
00198 
00199 
00200 //! |= (A & B1) | (A & B2) | ... | (A & bn) <=> A & (B1 | B2 | ...| Bn)
00201 Theorem
00202 CoreTheoremProducer::orDistributivityRule(const Expr& e) {
00203   if(CHECK_PROOFS) {
00204     CHECK_SOUND(e.isOr() && e.arity() >= 2,
00205     "CoreTheoremProducer::orDistributivityRule: "
00206     "input must be an OR expr: \n" + e.toString());
00207     const Expr& e0 = e[0];
00208 
00209     CHECK_SOUND(e0.isAnd() && e0.arity() == 2,
00210     "CoreTheoremProducer::orDistributivityRule: "
00211     "input must be an OR of binary ANDs: \n" + e.toString());
00212   }
00213 
00214   const Expr& A = e[0][0];
00215 
00216   if(CHECK_PROOFS) {
00217     for(Expr::iterator i=e.begin(),iend=e.end();i!=iend;++i) {
00218       const Expr& ei = *i;
00219       CHECK_SOUND(ei.isAnd() && ei.arity() == 2,
00220     "CoreTheoremProducer::orDistributivityRule: "
00221     "input must be an OR of binary ANDs: \n" + e.toString());
00222       CHECK_SOUND(A == ei[0],
00223       "CoreTheoremProducer::orDistributivityRule: "
00224       "input must have a common factor: \n" + e.toString());
00225     }
00226   }
00227   vector<Expr> output;
00228   for(Expr::iterator i=e.begin(),iend=e.end();i!=iend;++i) {
00229     Expr ei = *i;
00230     output.push_back(ei[1]);
00231   }
00232   Expr out = A.andExpr(orExpr(output));
00233 
00234   Proof pf;
00235   if(withProof())
00236     pf = newPf("or_distribuitivity_rule", e);
00237   
00238   return newRWTheorem(e, out, Assumptions::emptyAssump(), pf);
00239 } 
00240 
00241 
00242 
00243 //! |= (A | B1) & (A | B2) & ... & (A | bn) <=> A | (B1 & B2 & ...& Bn)
00244 Theorem
00245 CoreTheoremProducer::andDistributivityRule(const Expr& e) {
00246   if(CHECK_PROOFS) {
00247     CHECK_SOUND(e.isAnd() && e.arity() >= 2,
00248     "CoreTheoremProducer::andDistributivityRule: "
00249     "input must be an AND expr: \n" + e.toString());
00250     const Expr& e0 = e[0];
00251 
00252     CHECK_SOUND(e0.isOr() && e0.arity() == 2,
00253     "CoreTheoremProducer::orDistributivityRule: "
00254     "input must be an AND of binary ORs: \n" + e.toString());
00255   }
00256 
00257   const Expr& A = e[0][0];
00258 
00259   if(CHECK_PROOFS) {
00260     for(Expr::iterator i=e.begin(),iend=e.end();i!=iend;++i) {
00261       const Expr& ei = *i;
00262       CHECK_SOUND(ei.isOr() && ei.arity() == 2,
00263     "CoreTheoremProducer::andDistributivityRule: "
00264     "input must be an AND of binary ORs: \n" + e.toString());
00265       CHECK_SOUND(A == ei[0],
00266       "CoreTheoremProducer::andDistributivityRule: "
00267       "input must have a common factor: \n" + e.toString());
00268     }
00269   }
00270   vector<Expr> output;
00271   for(Expr::iterator i=e.begin(),iend=e.end();i!=iend;++i) {
00272     output.push_back((*i)[1]);
00273   }
00274   Expr out = A.orExpr(andExpr(output));
00275 
00276   Proof pf;
00277   if(withProof())
00278     pf = newPf("and_distribuitivity_rule", e);
00279   
00280   return newRWTheorem(e, out, Assumptions::emptyAssump(), pf);
00281 } 
00282 
00283 // ==> IMPLIES(e1,e2) IFF OR(!e1, e2)
00284 Theorem
00285 CoreTheoremProducer::rewriteImplies(const Expr& e) {
00286   Proof pf;
00287   if(CHECK_PROOFS)
00288     CHECK_SOUND(e.isImpl(), "rewriteImplies precondition violated");
00289   if(withProof()) {
00290     pf = newPf("rewrite_implies", e[0], e[1]);
00291   }
00292   return newRWTheorem(e, !e[0] || e[1], Assumptions::emptyAssump(), pf);
00293 }
00294 
00295 // ==> DISTINCT(e1,...,en) IFF AND 1 <= i < j <= n (e[i] /= e[j])
00296 Theorem
00297 CoreTheoremProducer::rewriteDistinct(const Expr& e) {
00298   Proof pf;
00299   if(CHECK_PROOFS) {
00300     CHECK_SOUND(e.getKind() == DISTINCT, "rewriteDistinct precondition violated");
00301     CHECK_SOUND(e.arity() > 0, "rewriteDistinct precondition violated");
00302   }
00303   Expr res;
00304   if (e.arity() == 1) {
00305     res = e.getEM()->trueExpr();
00306   }
00307   else if (e.arity() == 2) {
00308     res = !(e[0].eqExpr(e[1]));
00309   }
00310   else {
00311     vector<Expr> tmp;
00312     for (int i = 0; i < e.arity(); ++i) {
00313       for (int j = i+1; j < e.arity(); ++j) {
00314         tmp.push_back(!(e[i].eqExpr(e[j])));
00315       }
00316     }
00317     res = Expr(AND, tmp);
00318   }
00319   if(withProof()) {
00320     pf = newPf("rewrite_distinct", e , res);
00321   }
00322 
00323   return newRWTheorem(e, res, Assumptions::emptyAssump(), pf);
00324 }
00325 
00326 // ==> NOT(e) == ITE(e, FALSE, TRUE)
00327 Theorem
00328 CoreTheoremProducer::NotToIte(const Expr& not_e){
00329   Proof pf;
00330   if(CHECK_PROOFS)
00331     CHECK_SOUND(not_e.isNot() && not_e[0].getType().isBool(),
00332     "NotToIte precondition violated");
00333   if(withProof())
00334     pf = newPf("NotToIte", not_e[0]);
00335   if(not_e[0].isTrue())
00336     return d_core->getCommonRules()->rewriteNotTrue(not_e);
00337   else if(not_e[0].isFalse())
00338     return d_core->getCommonRules()->rewriteNotFalse(not_e);
00339   Expr ite(not_e[0].iteExpr(d_em->falseExpr(), d_em->trueExpr()));
00340   return newRWTheorem(not_e, ite, Assumptions::emptyAssump(), pf);  
00341 }
00342 
00343 // ==> Or(e) == ITE(e[1], TRUE, e[0])
00344 Theorem
00345 CoreTheoremProducer::OrToIte(const Expr& e){
00346   if(CHECK_PROOFS)
00347     CHECK_SOUND(e.isOr(),
00348     "OrToIte: precondition violated: " + e.toString());
00349   Proof pf;
00350   if(withProof()) {
00351     pf = newPf("OrToIte", e);
00352   }
00353   const vector<Expr>& kids = e.getKids();
00354   unsigned k(kids.size());
00355   if(k==0)
00356     return newRWTheorem(e, d_em->falseExpr(), Assumptions::emptyAssump(), pf);
00357   if(k==1)
00358     return newRWTheorem(e, e[0], Assumptions::emptyAssump(), pf);
00359   Expr ite(kids[k-1]);
00360   if(CHECK_PROOFS)
00361     CHECK_SOUND(!ite.getType().isNull(),
00362     "OrToIte: kid " + int2string(k-1) + " has no type: "
00363     + (ite).toString());
00364   for (; k > 1; k--) {
00365     if (kids[k-2].isTrue()) {
00366       ite = d_em->trueExpr();
00367       break;
00368     }
00369     else if(kids[k-2].isFalse()) continue;
00370     else{
00371       if(CHECK_PROOFS)
00372   CHECK_SOUND(!kids[k-2].getType().isNull(),
00373       "OrToIte: kid " + int2string(k-2) + " has no type: "
00374       + (kids[k-2]).toString());
00375       ite = ite.iteExpr(d_em->trueExpr(), kids[k-2]);
00376     }
00377   }
00378   return newRWTheorem(e, ite, Assumptions::emptyAssump(), pf);
00379 }
00380 
00381 // ==> And(e) == ITE(e[1], e[0], FALSE)
00382 Theorem
00383 CoreTheoremProducer::AndToIte(const Expr& e){
00384   if(CHECK_PROOFS)
00385     CHECK_SOUND(e.isAnd(),
00386     "AndToIte: precondition violated: " + e.toString());
00387   Proof pf;
00388   if(withProof()) {
00389     pf = newPf("AndToIte", e);
00390   }
00391   const vector<Expr>& kids = e.getKids();
00392   unsigned k(kids.size());
00393   if(k==0)
00394     return newRWTheorem(e, d_em->trueExpr(), Assumptions::emptyAssump(), pf);
00395   if(k==1)
00396     return newRWTheorem(e, e[0], Assumptions::emptyAssump(), pf);
00397   Expr ite(kids[k-1]);
00398   if(CHECK_PROOFS)
00399     CHECK_SOUND(!ite.getType().isNull(),
00400     "AndToIte: kid " + int2string(k-1) + " has no type: "
00401     + (ite).toString());
00402   for (; k > 1; k--) {
00403     if (kids[k-2].isFalse()) {
00404       ite = d_em->falseExpr();
00405       break;
00406     }
00407     else if(kids[k-2].isTrue()) {
00408       continue;
00409     }
00410     else{
00411       if(CHECK_PROOFS)
00412   CHECK_SOUND(!kids[k-2].getType().isNull(),
00413         "AndToIte: kid " + int2string(k-2) + " has no type: "
00414         + (kids[k-2]).toString());
00415       ite = ite.iteExpr(kids[k-2], d_em->falseExpr());
00416     }
00417   }
00418   return newRWTheorem(e, ite, Assumptions::emptyAssump(), pf);
00419 }
00420 
00421 // ==> IFF(a,b) == ITE(a, b, !b)
00422 Theorem
00423 CoreTheoremProducer::IffToIte(const Expr& e){
00424   if(CHECK_PROOFS)
00425     CHECK_SOUND(e.isIff() && e[0].getType().isBool() && e[1].getType().isBool(),
00426     "IffToIte: precondition violated: " + e.toString());
00427   Proof pf;
00428   if(e[0] == e[1]) return d_core->getCommonRules()->reflexivityRule(e);
00429   Expr ite(e[0].iteExpr(e[1], e[1].iteExpr(d_em->falseExpr(),
00430              d_em->trueExpr())));
00431   if(withProof()) {
00432     pf = newPf("iff_to_ite", e);
00433   }
00434   return newRWTheorem(e, ite, Assumptions::emptyAssump(), pf); 
00435 }
00436 
00437 // ==> IMPLIES(a,b) == ITE(a, b, TRUE)
00438 Theorem
00439 CoreTheoremProducer::ImpToIte(const Expr& e){
00440   if(CHECK_PROOFS)
00441     CHECK_SOUND(e.isImpl() && e[0].getType().isBool() && e[1].getType().isBool(),
00442     "ImpToIte: precondition violated: " + e.toString());
00443   Proof pf;
00444   if(e[0] == e[1]) return d_core->getCommonRules()->reflexivityRule(e);
00445   Expr ite(e[0].iteExpr(e[1], d_em->trueExpr()));
00446   if(withProof()) {
00447     pf = newPf("imp_to_ite", e);
00448   }
00449   return newRWTheorem(e, ite, Assumptions::emptyAssump(), pf); 
00450 }
00451 
00452 
00453 // ==> ITE(e, FALSE, TRUE) IFF NOT(e)
00454 Theorem
00455 CoreTheoremProducer::rewriteIteToNot(const Expr& e)
00456 {
00457   if (CHECK_PROOFS)
00458     CHECK_SOUND(e.isITE() && e[1].isFalse() && e[2].isTrue(),
00459     "rewriteIteToNot: " + e.toString());
00460   Proof pf;
00461   if (withProof()) pf = newPf("rewrite_ite_to_not", e);
00462   return newRWTheorem(e, e[0].negate(), Assumptions::emptyAssump(), pf);
00463 }
00464 
00465 // ==> ITE(a, TRUE, b) IFF OR(a, b)
00466 Theorem
00467 CoreTheoremProducer::rewriteIteToOr(const Expr& e)
00468 {
00469   if (CHECK_PROOFS)
00470     CHECK_SOUND(e.isITE() && e[1].isTrue(),
00471     "rewriteIteToOr: " + e.toString());
00472   Proof pf;
00473   if (withProof()) pf = newPf("rewrite_ite_to_or", e);
00474   return newRWTheorem(e, e[0] || e[2], Assumptions::emptyAssump(), pf);
00475 }
00476 
00477 // ==> ITE(a, b, FALSE) IFF AND(a, b)
00478 Theorem
00479 CoreTheoremProducer::rewriteIteToAnd(const Expr& e)
00480 {
00481   if (CHECK_PROOFS)
00482     CHECK_SOUND(e.isITE() && e[2].isFalse(),
00483     "rewriteIteToAnd: " + e.toString());
00484   Proof pf;
00485   if (withProof()) pf = newPf("rewrite_ite_to_and", e);
00486   return newRWTheorem(e, e[0] && e[1], Assumptions::emptyAssump(), pf);
00487 }
00488 
00489 // ==> ITE(a, b, !b) IFF IFF(a, b)
00490 Theorem
00491 CoreTheoremProducer::rewriteIteToIff(const Expr& e)
00492 {
00493   if (CHECK_PROOFS)
00494     CHECK_SOUND(e.isITE() && e[1] == e[2].negate(),
00495     "rewriteIteToIff: " + e.toString());
00496   Proof pf;
00497   if (withProof()) pf = newPf("rewrite_ite_to_iff", e);
00498   return newRWTheorem(e, e[0].iffExpr(e[1]), Assumptions::emptyAssump(), pf);
00499 }
00500 
00501 // ==> ITE(a, b, TRUE) IFF IMPLIES(a, b)
00502 Theorem
00503 CoreTheoremProducer::rewriteIteToImp(const Expr& e)
00504 {
00505   if (CHECK_PROOFS)
00506     CHECK_SOUND(e.isITE() && e[2].isTrue(),
00507     "rewriteIteToImp: " + e.toString());
00508   Proof pf;
00509   if (withProof()) pf = newPf("rewrite_ite_to_imp", e);
00510   return newRWTheorem(e, e[0].impExpr(e[1]), Assumptions::emptyAssump(), pf);
00511 }
00512 
00513 
00514 // ==> ITE(a, b(a), c(a)) IFF ITE(a, b(TRUE), c(FALSE))
00515 // ==> ITE(x = y, b, c) IFF ITE(x = y b[x/y], c[x = y/FALSE])
00516 Theorem CoreTheoremProducer::rewriteIteCond(const Expr& e)
00517 {
00518   if (CHECK_PROOFS)
00519     CHECK_SOUND(e.isITE() && e.arity()==3, "rewriteIteCond: " + e.toString());
00520 
00521   vector<Expr> oldTerms, newTerms;
00522 // //   if (e[0].isEq()) {
00523 // //     oldTerms.push_back(e[0][0]);
00524 // //     newTerms.push_back(e[0][1]);
00525 // //   }
00526 // //   else {
00527   oldTerms.push_back(e[0]);
00528   newTerms.push_back(d_em->trueExpr());
00529 //   }
00530   
00531   Expr e1(e[1].substExpr(oldTerms, newTerms));
00532   oldTerms[0] = e[0];
00533   newTerms[0] = d_em->falseExpr();
00534   Expr e2(e[2].substExpr(oldTerms, newTerms));
00535 
00536   Proof pf;
00537   if (withProof()) pf = newPf("rewrite_ite_cond", e);
00538   return newRWTheorem(e, e[0].iteExpr(e1, e2), Assumptions::emptyAssump(), pf);
00539 }
00540 
00541 
00542 Theorem
00543 CoreTheoremProducer::iffOrDistrib(const Expr& iff) {
00544   if(CHECK_PROOFS) {
00545     CHECK_SOUND(iff.isIff() && iff.arity()==2, "iffOrDistrib("
00546     +iff.toString()+")");
00547     CHECK_SOUND(iff[0].isOr() && iff[0].arity()==2, "iffOrDistrib("
00548     +iff.toString()+")");
00549     CHECK_SOUND(iff[1].isOr() && iff[1].arity()==2, "iffOrDistrib("
00550     +iff.toString()+")");
00551     CHECK_SOUND(iff[0][0]==iff[1][0], "iffOrDistrib("
00552     +iff.toString()+")");
00553   }
00554   const Expr& a = iff[0][0];
00555   const Expr& b = iff[0][1];
00556   const Expr& c = iff[1][1];
00557   Proof pf;
00558   if(withProof())
00559     pf = newPf("iff_or_distrib", iff);
00560   return newRWTheorem(iff, (a || (b.iffExpr(c))), Assumptions::emptyAssump(), pf);
00561 }
00562 
00563 
00564 Theorem
00565 CoreTheoremProducer::iffAndDistrib(const Expr& iff) {
00566   if(CHECK_PROOFS) {
00567     CHECK_SOUND(iff.isIff() && iff.arity()==2, "iffAndDistrib("
00568     +iff.toString()+")");
00569     CHECK_SOUND(iff[0].isAnd() && iff[0].arity()==2, "iffAndDistrib("
00570     +iff.toString()+")");
00571     CHECK_SOUND(iff[1].isAnd() && iff[1].arity()==2, "iffAndDistrib("
00572     +iff.toString()+")");
00573     CHECK_SOUND(iff[0][0]==iff[1][0], "iffOrDistrib("
00574     +iff.toString()+")");
00575   }
00576   const Expr& a = iff[0][0];
00577   const Expr& b = iff[0][1];
00578   const Expr& c = iff[1][1];
00579   Proof pf;
00580   if(withProof())
00581     pf = newPf("iff_and_distrib", iff);
00582   return newRWTheorem(iff, (!a || (b.iffExpr(c))), Assumptions::emptyAssump(), pf);
00583 }
00584 
00585 
00586 // |- op(ITE(cond,a,b)) =/<=> ITE(cond,op(a),op(b))
00587 Theorem
00588 CoreTheoremProducer::ifLiftUnaryRule(const Expr& e) {
00589   if(CHECK_PROOFS) {
00590     CHECK_SOUND(e.arity()==1 && e[0].isITE(),
00591     "CoreTheoremProducer::ifLiftUnaryRule("
00592     "e = " + e.toString() + ")");
00593   }
00594   Op op(e.getOp());
00595   const Expr& ite = e[0];
00596   const Expr& cond = ite[0];
00597   const Expr& t1 = ite[1];
00598   const Expr& t2 = ite[2];
00599 
00600   if(CHECK_PROOFS) {
00601     CHECK_SOUND(cond.getType().isBool(),
00602     "CoreTheoremProducer::ifLiftUnaryRule("
00603     "e = " + e.toString()+")");      
00604   }    
00605 
00606   Expr e1 =  Expr(op, t1);
00607   Expr e2 =  Expr(op, t2);
00608 
00609   Expr resultITE = cond.iteExpr(e1, e2);
00610 
00611   Proof pf;
00612   if (withProof())
00613     pf = newPf("if_lift_unary_rule", e);
00614   return newRWTheorem(e, resultITE, Assumptions::emptyAssump(), pf);
00615 }
00616 
00617 
00618 // (a & b) <=> a & b[a/true]; takes the index of a and rewrites all
00619 // the other conjuncts.
00620 Theorem
00621 CoreTheoremProducer::rewriteAndSubterms(const Expr& e, int idx) {
00622   if(CHECK_PROOFS) {
00623     CHECK_SOUND(e.isAnd() && 0 <= idx && idx < e.arity(),
00624     "rewriteAndSubterms("+e.toString()
00625     +", idx="+int2string(idx)
00626     +"):\n Expected an AND and a valid index of a child");
00627   }
00628   vector<Expr> kids;
00629   ExprHashMap<Expr> subst;
00630   subst.insert(e[idx], d_em->trueExpr());
00631   for(int i=0, iend=e.arity(); i<iend; ++i) {
00632     if(i==idx)
00633       kids.push_back(e[i]);
00634     else
00635       kids.push_back(e[i].substExpr(subst));
00636   }
00637   Proof pf;
00638   if(withProof())
00639     pf = newPf("rewrite_and_subterms", e, d_em->newRatExpr(idx));
00640   return newRWTheorem(e, Expr(e.getOp(), kids), Assumptions::emptyAssump(), pf);
00641 }
00642 
00643 
00644 // (a | b) <=> a | b[a/false]; takes the index of a and rewrites all
00645 // the other disjuncts.
00646 Theorem
00647 CoreTheoremProducer::rewriteOrSubterms(const Expr& e, int idx) {
00648   if(CHECK_PROOFS) {
00649     CHECK_SOUND(e.isOr() && 0 <= idx && idx < e.arity(),
00650     "rewriteOrSubterms("+e.toString()
00651     +", idx="+int2string(idx)
00652     +"):\n Expected an OR and a valid index of a child");
00653   }
00654   vector<Expr> kids;
00655   ExprHashMap<Expr> subst;
00656   subst.insert(e[idx], d_em->falseExpr());
00657   for(int i=0, iend=e.arity(); i<iend; ++i) {
00658     if(i==idx)
00659       kids.push_back(e[i]);
00660     else
00661       kids.push_back(e[i].substExpr(subst));
00662   }
00663   Proof pf;
00664   if(withProof())
00665     pf = newPf("rewrite_or_subterms", e, d_em->newRatExpr(idx));
00666   return newRWTheorem(e, Expr(e.getOp(), kids), Assumptions::emptyAssump(), pf);
00667 }
00668 
00669 
00670 Theorem CoreTheoremProducer::dummyTheorem(const Expr& e)
00671 {
00672   Proof pf; 
00673   return newTheorem(e, Assumptions::emptyAssump(), pf);
00674 }

Generated on Wed Nov 18 16:13:29 2009 for CVC3 by  doxygen 1.5.2