common_theorem_producer.cpp

Go to the documentation of this file.
00001 /*****************************************************************************/
00002 /*!
00003  *\file common_theorem_producer.cpp
00004  *\brief Implementation of common proof rules
00005  *
00006  * Author: Clark Barrett
00007  *
00008  * Created: Wed Jan 11 16:10:15 2006
00009  *
00010  * <hr>
00011  *
00012  * License to use, copy, modify, sell and/or distribute this software
00013  * and its documentation for any purpose is hereby granted without
00014  * royalty, subject to the terms and conditions defined in the \ref
00015  * LICENSE file provided with this distribution.
00016  * 
00017  * <hr>
00018  *
00019  */
00020 /*****************************************************************************/
00021 
00022 
00023 // This code is trusted
00024 #define _CVC3_TRUSTED_
00025 
00026 
00027 #include "common_theorem_producer.h"
00028 
00029 
00030 using namespace CVC3;
00031 using namespace std;
00032 
00033 
00034 // The trusted method of TheoremManager which creates this theorem producer
00035 CommonProofRules* TheoremManager::createProofRules() {
00036   return new CommonTheoremProducer(this);
00037 }
00038 
00039 
00040 CommonTheoremProducer::CommonTheoremProducer(TheoremManager* tm)
00041   : TheoremProducer(tm),
00042     d_skolemized_thms(tm->getCM()->getCurrentContext()),
00043     d_skolemVars(tm->getCM()->getCurrentContext())
00044 {}
00045 
00046 
00047 ////////////////////////////////////////////////////////////////////////
00048 // TCC rules (3-valued logic)
00049 ////////////////////////////////////////////////////////////////////////
00050 
00051 //  G1 |- phi   G2 |- D_phi
00052 // -------------------------
00053 //       G1,G2 |-_3 phi
00054 Theorem3
00055 CommonTheoremProducer::queryTCC(const Theorem& phi, const Theorem& D_phi) {
00056   Proof pf;
00057 //   if(CHECK_PROOFS)
00058 //     CHECK_SOUND(D_phi.getExpr() == d_core->getTCC(phi.getExpr()),
00059 //    "CoreTheoremProducer::queryTCC: "
00060 //    "bad TCC for a formula:\n\n  "
00061 //    +phi.getExpr().toString()
00062 //    +"\n\n  TCC must be the following:\n\n  "
00063 //    +d_core->getTCC(phi.getExpr()).toString()
00064 //    +"\n\nBut given this as a TCC:\n\n  "
00065 //    +D_phi.getExpr().toString());
00066   Assumptions a = phi.getAssumptionsRef();
00067   a.add(D_phi);
00068   if(withProof()) {
00069     vector<Expr> args;
00070     vector<Proof> pfs;
00071     args.push_back(phi.getExpr());
00072     args.push_back(D_phi.getExpr());
00073     pfs.push_back(phi.getProof());
00074     pfs.push_back(D_phi.getProof());
00075     pf = newPf("queryTCC", args, pfs);
00076     }
00077   return newTheorem3(phi.getExpr(), a, pf);
00078 }
00079 
00080 
00081 //  G0,a1,...,an |-_3 phi  G1 |- D_a1 ... Gn |- D_an
00082 // -------------------------------------------------
00083 //    G0,G1,...,Gn |-_3 (a1 & ... & an) -> phi
00084 Theorem3
00085 CommonTheoremProducer::implIntro3(const Theorem3& phi,
00086           const std::vector<Expr>& assump,
00087           const vector<Theorem>& tccs) {
00088   bool checkProofs(CHECK_PROOFS);
00089   // This rule only makes sense when runnnig with assumptions
00090   if(checkProofs) {
00091     CHECK_SOUND(withAssumptions(),
00092     "implIntro3: called while running without assumptions");
00093   }
00094 
00095   const Assumptions& phiAssump = phi.getAssumptionsRef();
00096 
00097   if(checkProofs) {
00098     CHECK_SOUND(assump.size() == tccs.size(),
00099     "implIntro3: number of assumptions ("
00100     +int2string(assump.size())+") and number of TCCs ("
00101     +int2string(tccs.size())
00102     +") does not match");
00103     for(size_t i=0; i<assump.size(); i++) {
00104       const Theorem& thm = phiAssump[assump[i]];
00105       CHECK_SOUND(!thm.isNull() && thm.isAssump(),
00106       "implIntro3: this is not an assumption of phi:\n\n"
00107       "  a["+int2string(i)+"] = "+assump[i].toString()
00108       +"\n\n  phi = "+phi.getExpr().toString());
00109 //       CHECK_SOUND(tccs[i].getExpr() == d_core->getTCC(assump[i]),
00110 //      "implIntro3: Assumption does not match its TCC:\n\n"
00111 //      "  a["+int2string(i)+"] = "+assump[i].toString()
00112 //      +"  TCC(a["+int2string(i)+"]) = "
00113 //      +d_core->getTCC(assump[i]).toString()
00114 //      +"\n\n  tccs["+int2string(i)+"] = "
00115 //      +tccs[i].getExpr().toString());
00116     }
00117   }
00118 
00119   // Proof compaction: trivial derivation
00120   if(assump.size() == 0) return phi;
00121 
00122   Assumptions a(phiAssump - assump);
00123   Assumptions b(tccs);
00124   a.add(b);
00125   Proof pf;
00126   if(withProof()) {
00127     vector<Proof> u; // Proof labels for assumptions
00128     for(vector<Expr>::const_iterator i=assump.begin(), iend=assump.end();
00129   i!=iend; ++i) {
00130       const Theorem& t = phiAssump[*i];
00131       u.push_back(t.getProof());
00132     }
00133     // Arguments to the proof rule:
00134     // impl_intro_3(phi, a1,...,an,tcc1,...tccn,pf_tcc1,...pf_tccn,
00135     //              [lambda(a1,...,an): pf_phi])
00136     vector<Expr> args;
00137     vector<Proof> pfs;
00138     args.push_back(phi.getExpr());
00139     args.insert(args.end(), assump.begin(), assump.end());
00140     for(vector<Theorem>::const_iterator i=tccs.begin(), iend=tccs.end();
00141   i!=iend; ++i) {
00142       args.push_back(i->getExpr());
00143       pfs.push_back(i->getProof());
00144     }
00145     // Lambda-abstraction of pf_phi
00146     pfs.push_back(newPf(u, assump, phi.getProof()));
00147     pf = newPf("impl_intro_3", args, pfs);
00148   }
00149   Expr conj(andExpr(assump));
00150   return newTheorem3(conj.impExpr(phi.getExpr()), a, pf);
00151 }
00152 
00153 
00154 Theorem CommonTheoremProducer::assumpRule(const Expr& e, int scope) {
00155   //  TRACE("assump", "assumpRule(", e, ")");
00156   Proof pf;
00157   if(withProof()) pf = newLabel(e);
00158   return newAssumption(e, pf, scope);
00159 }
00160 
00161 
00162 Theorem CommonTheoremProducer::reflexivityRule(const Expr& a) {
00163   return newReflTheorem(a);
00164 }
00165 
00166 
00167 // ==> (a == a) IFF TRUE
00168 Theorem CommonTheoremProducer::rewriteReflexivity(const Expr& t) {
00169   if(CHECK_PROOFS)
00170     CHECK_SOUND((t.isEq() || t.isIff()) && t[0] == t[1],
00171     "rewriteReflexivity: wrong expression: "
00172     + t.toString());
00173   Proof pf;
00174   if(withProof()) {
00175     if(t.isEq()) {
00176       DebugAssert(!t[0].getType().isNull(),
00177       "rewriteReflexivity: t[0] has no type: "
00178       + t[0].toString());
00179       pf = newPf("rewrite_eq_refl", t[0].getType().getExpr(), t[0]);
00180     } else
00181       pf = newPf("rewrite_iff_refl", t[0]);
00182   }
00183   return newRWTheorem(t, d_em->trueExpr(), Assumptions::emptyAssump(), pf);
00184 }
00185 
00186 
00187 Theorem CommonTheoremProducer::symmetryRule(const Theorem& a1_eq_a2) {
00188   if(CHECK_PROOFS)
00189     CHECK_SOUND(a1_eq_a2.isRewrite(),
00190     ("CVC3::CommonTheoremProducer: "
00191      "theorem is not an equality or iff:\n  "
00192      + a1_eq_a2.getExpr().toString()).c_str());
00193   const Expr& a1 = a1_eq_a2.getLHS();
00194   const Expr& a2 = a1_eq_a2.getRHS();
00195 
00196   Proof pf;
00197   /////////////////////////////////////////////////////////////////////////
00198   //// Proof compaction
00199   /////////////////////////////////////////////////////////////////////////
00200   // If a1 == a2, use reflexivity
00201   if(a1 == a2) return reflexivityRule(a1);
00202   // Otherwise, do the work
00203   if(withProof()) {
00204     Type t = a1.getType();
00205     // Check the types
00206     IF_DEBUG(a1_eq_a2.getExpr().getType();)
00207     bool isEquality = !t.isBool();
00208     if(isEquality) {
00209       vector<Expr> args;
00210       args.push_back(t.getExpr());
00211       args.push_back(a1);
00212       args.push_back(a2);
00213       pf = newPf("eq_symm", args, a1_eq_a2.getProof());
00214     } else
00215       pf = newPf("iff_symm", a1, a2, a1_eq_a2.getProof());
00216   }
00217   return newRWTheorem(a2, a1, Assumptions(a1_eq_a2), pf);
00218 }
00219 
00220 
00221 Theorem CommonTheoremProducer::rewriteUsingSymmetry(const Expr& a1_eq_a2) {
00222   bool isIff = a1_eq_a2.isIff();
00223   if(CHECK_PROOFS)
00224     CHECK_SOUND(a1_eq_a2.isEq() || isIff, "rewriteUsingSymmetry precondition violated");
00225   const Expr& a1 = a1_eq_a2[0];
00226   const Expr& a2 = a1_eq_a2[1];
00227   // Proof compaction: if a1 == a2, use reflexivity
00228   if(a1 == a2) return reflexivityRule(a1_eq_a2);
00229   // Otherwise, do the work
00230   Proof pf;
00231   if(withProof()) {
00232     Type t = a1.getType();
00233     DebugAssert(!t.isNull(),
00234     "rewriteUsingSymmetry: a1 has no type: " + a1.toString());
00235     if(isIff)
00236       pf = newPf("rewrite_iff_symm", a1, a2);
00237     else {
00238       pf = newPf("rewrite_eq_symm", t.getExpr(), a1, a2);
00239     }
00240   }
00241   return newRWTheorem(a1_eq_a2, isIff ? a2.iffExpr(a1) : a2.eqExpr(a1), Assumptions::emptyAssump(), pf);
00242 }
00243 
00244 
00245 Theorem CommonTheoremProducer::transitivityRule(const Theorem& a1_eq_a2,
00246                                                 const Theorem& a2_eq_a3) {
00247   DebugAssert(!a1_eq_a2.isNull(), "transitivityRule()");
00248   DebugAssert(!a2_eq_a3.isNull(), "transitivityRule()");
00249   if(CHECK_PROOFS) {
00250     CHECK_SOUND(a1_eq_a2.isRewrite() && a2_eq_a3.isRewrite(),  
00251     "CVC3::CommonTheoremProducer::transitivityRule:\n  "
00252     "Wrong premises: first = "
00253     + a1_eq_a2.getExpr().toString() + ", second = "
00254     + a2_eq_a3.getExpr().toString());
00255     CHECK_SOUND(a1_eq_a2.getRHS() == a2_eq_a3.getLHS(),
00256     "CVC3::CommonTheoremProducer::transitivityRule:\n  "
00257     "Wrong premises: first = "
00258     + a1_eq_a2.getExpr().toString() + ", second = "
00259     + a2_eq_a3.getExpr().toString());
00260   }
00261   const Expr& a1 = a1_eq_a2.getLHS();
00262   const Expr& a2 = a1_eq_a2.getRHS();
00263   const Expr& a3 = a2_eq_a3.getRHS();
00264 
00265   /////////////////////////////////////////////////////////////////////////
00266   //// Proof compaction
00267   /////////////////////////////////////////////////////////////////////////
00268   // if a1 == a3, use reflexivity (and lose all assumptions)
00269   if(a1 == a3) return reflexivityRule(a1);
00270   // if a1 == a2, or if a2 == a3, use only the non-trivial part
00271   if(a1 == a2) return a2_eq_a3;
00272   if(a2 == a3) return a1_eq_a2;
00273 
00274   ////////////////////////////////////////////////////////////////////////
00275   //// No shortcuts.  Do the work.
00276   ////////////////////////////////////////////////////////////////////////
00277 
00278   Proof pf;
00279   Assumptions a(a1_eq_a2, a2_eq_a3);
00280   // Build the proof
00281   if(withProof()) {
00282     Type t = a1.getType();
00283     bool isEquality = (!t.isBool());
00284     string name((isEquality)? "eq_trans" : "iff_trans");
00285     vector<Expr> args;
00286     vector<Proof> pfs;
00287     DebugAssert(!t.isNull(), "transitivityRule: "
00288     "Type is not computed for a1: " + a1.toString());
00289     // Type argument is needed only for equality
00290     if(isEquality) args.push_back(t.getExpr());
00291     args.push_back(a1);
00292     args.push_back(a2);
00293     args.push_back(a3);
00294     pfs.push_back(a1_eq_a2.getProof());
00295     pfs.push_back(a2_eq_a3.getProof());
00296     pf = newPf(name, args, pfs);
00297   }
00298   return newRWTheorem(a1, a3, a, pf);
00299 }
00300 
00301 
00302 Theorem CommonTheoremProducer::substitutivityRule(const Expr& e,
00303                                                   const Theorem& thm) {
00304   IF_DEBUG
00305     (static DebugTimer
00306        accum0(debugger.timer("substitutivityRule0 time"));
00307      static DebugTimer tmpTimer(debugger.newTimer());
00308      static DebugCounter count(debugger.counter("substitutivityRule0 calls"));
00309      debugger.setCurrentTime(tmpTimer);
00310      count++;)
00311 
00312   // Check that t is c == d or c IFF d
00313   if(CHECK_PROOFS) {
00314     CHECK_SOUND(e.arity() == 1 && e[0] == thm.getLHS(),
00315                 "Unexpected use of substitutivityRule0");
00316     CHECK_SOUND(thm.isRewrite(),
00317                 "CVC3::CommonTheoremProducer::substitutivityRule0:\n  "
00318                 "premis is not an equality or IFF: "
00319                 + thm.getExpr().toString()
00320                 + "\n  expr = " + e.toString());
00321   }
00322   Expr e2(e.getOp(), thm.getRHS());
00323   Proof pf;
00324   if(withProof())
00325     pf = newPf("basic_subst_op0",e, e2,thm.getProof());
00326   Theorem res = newRWTheorem(e, e2, Assumptions(thm), pf);
00327   if (!res.isRefl()) res.setSubst();
00328   return res;
00329 }
00330 
00331 
00332 Theorem CommonTheoremProducer::substitutivityRule(const Expr& e,
00333                                                   const Theorem& thm1,
00334                                                   const Theorem& thm2) {
00335   IF_DEBUG
00336     (static DebugTimer
00337        accum0(debugger.timer("substitutivityRule1 time"));
00338      static DebugTimer tmpTimer(debugger.newTimer());
00339      static DebugCounter count(debugger.counter("substitutivityRule1 calls"));
00340      debugger.setCurrentTime(tmpTimer);
00341      count++;)
00342 
00343   // Check that t is c == d or c IFF d
00344   if(CHECK_PROOFS) {
00345     CHECK_SOUND(e.arity() == 2 && e[0] == thm1.getLHS() &&
00346                 e[1] == thm2.getLHS(),
00347                 "Unexpected use of substitutivityRule1");
00348     CHECK_SOUND(thm1.isRewrite(),
00349                 "CVC3::CommonTheoremProducer::substitutivityRule1:\n  "
00350                 "premis is not an equality or IFF: "
00351                 + thm1.getExpr().toString()
00352                 + "\n  expr = " + e.toString());
00353     CHECK_SOUND(thm2.isRewrite(),
00354                 "CVC3::CommonTheoremProducer::substitutivityRule1:\n  "
00355                 "premis is not an equality or IFF: "
00356                 + thm2.getExpr().toString()
00357                 + "\n  expr = " + e.toString());
00358   }
00359   Expr e2(e.getOp(), thm1.getRHS(), thm2.getRHS());
00360   Proof pf;
00361   if(withProof()) {
00362     vector<Proof> pfs;
00363     pfs.push_back(thm1.getProof());
00364     pfs.push_back(thm2.getProof());
00365     pf = newPf("basic_subst_op1", e, e2, pfs);
00366   }
00367   Theorem res = newRWTheorem(e, e2, Assumptions(thm1, thm2), pf);
00368   if (!res.isRefl()) res.setSubst();
00369   return res;
00370 }
00371 
00372 
00373 Theorem CommonTheoremProducer::substitutivityRule(const Op& op,
00374                                                   const vector<Theorem>& thms) {
00375   IF_DEBUG
00376     (static DebugTimer
00377        accum0(debugger.timer("substitutivityRule time"));
00378      static DebugTimer tmpTimer(debugger.newTimer());
00379      static DebugCounter count(debugger.counter("substitutivityRule calls"));
00380      debugger.setCurrentTime(tmpTimer);
00381      count++;)
00382   // Check for trivial case: no theorems, return (op == op)
00383   unsigned size(thms.size());
00384   if(size == 0)
00385     return reflexivityRule(d_tm->getEM()->newLeafExpr(op));
00386   // Check that theorems are of the form c_i == d_i and collect
00387   // vectors of c_i's and d_i's and the vector of proofs
00388   vector<Expr> c, d;
00389   vector<Proof> pfs;
00390   // Reserve memory for argument vectors.  Do not reserve memory for
00391   // pfs, they are rarely used and slow anyway.
00392   c.reserve(size); d.reserve(size);
00393   for(vector<Theorem>::const_iterator i = thms.begin(), iend = thms.end();
00394       i != iend; ++i) {
00395     // Check that t is c == d or c IFF d
00396     if(CHECK_PROOFS)
00397       CHECK_SOUND(i->isRewrite(),
00398       "CVC3::CommonTheoremProducer::substitutivityRule:\n  "
00399       "premis is not an equality or IFF: "
00400       + i->getExpr().toString()
00401       + "\n  op = " + op.toString());
00402     // Collect the pieces
00403     c.push_back(i->getLHS());
00404     d.push_back(i->getRHS());
00405     if(withProof()) pfs.push_back(i->getProof());
00406   }
00407   Expr e1(op, c), e2(op, d);
00408   // Proof compaction: if e1 == e2, use reflexivity
00409   if(e1 == e2) return reflexivityRule(e1);
00410   // Otherwise, do the work
00411   Assumptions a(thms);
00412   Proof pf;
00413   if(withProof())
00414     // FIXME: this rule is not directly expressible in flea
00415     pf = newPf("basic_subst_op",e1,e2,pfs);
00416   Theorem res = newRWTheorem(e1, e2, a, pf);
00417   IF_DEBUG(debugger.setElapsed(tmpTimer);
00418      accum0 += tmpTimer;)
00419   res.setSubst();
00420   return res;
00421 }
00422 
00423 
00424 Theorem CommonTheoremProducer::substitutivityRule(const Expr& e,
00425                                                   const vector<unsigned>& changed,
00426                                                   const vector<Theorem>& thms) {
00427   IF_DEBUG
00428     (static DebugTimer
00429        accum0(debugger.timer("substitutivityRule2 time"));
00430      static DebugTimer tmpTimer(debugger.newTimer());
00431      static DebugCounter count(debugger.counter("substitutivityRule2 calls"));
00432      debugger.setCurrentTime(tmpTimer);
00433      count++;)
00434   DebugAssert(changed.size() > 0, "substitutivityRule2 should not be called");
00435   DebugAssert(changed.size() == thms.size(), "substitutivityRule2: wrong args");
00436 
00437   // Check that theorems are of the form c_i == d_i and collect
00438   // vectors of c_i's and d_i's and the vector of proofs
00439   unsigned size = e.arity();
00440   if (size == 1) return substitutivityRule(e, thms.back());
00441   unsigned csize = changed.size();
00442   if (size == 2) {
00443     if (csize == 2) return substitutivityRule(e, thms[0], thms[1]);
00444     if (changed[0] == 0) {
00445       return substitutivityRule(e, thms[0], reflexivityRule(e[1]));
00446     }
00447     else {
00448       return substitutivityRule(e, reflexivityRule(e[0]), thms[0]);
00449     }
00450   }
00451   DebugAssert(size >= csize, "Bad call to substitutivityRule2");
00452 
00453   vector<Expr> c;
00454   bool checkProofs(CHECK_PROOFS);
00455   for(unsigned j = 0, k = 0; k < size; ++k) {
00456     if (j == csize || changed[j] != k) {
00457       c.push_back(e[k]);
00458       continue;
00459     }
00460     // Check that t is c == d or c IFF d
00461     if(checkProofs)
00462       CHECK_SOUND(thms[j].isRewrite() && thms[j].getLHS() == e[k],
00463       "CVC3::CommonTheoremProducer::substitutivityRule:\n  "
00464       "premis is not an equality or IFF: "
00465       + thms[j].getExpr().toString()
00466       + "\n  e = " + e.toString());
00467     // Collect the pieces
00468     c.push_back(thms[j].getRHS());
00469     ++j;
00470   }
00471   Expr e2(e.getOp(), c);
00472   IF_DEBUG(if(e == e2) {
00473     ostream& os = debugger.getOS();
00474     os << "substitutivityRule2: e = " << e << "\n e2 = " << e2
00475        << "\n changed kids: [\n";
00476     for(unsigned j=0; j<changed.size(); j++)
00477       os << "  (" << changed[j] << ") " << thms[j] << "\n";
00478     os << "]\n";
00479   })
00480   DebugAssert(e != e2,
00481         "substitutivityRule2 should not be called in this case:\n"
00482         "e = "+e.toString());
00483 
00484   Proof pf;
00485   Assumptions a(thms);
00486   if(withProof()) {
00487     vector<Proof> pfs;
00488     for(vector<Theorem>::const_iterator i = thms.begin(), iend = thms.end();
00489         i != iend; ++i) {
00490       // Check that t is c == d or c IFF d
00491       if(CHECK_PROOFS)
00492         CHECK_SOUND(i->isRewrite(),
00493                     "CVC3::CommonTheoremProducer::substitutivityRule:\n  "
00494                     "premis is not an equality or IFF: "
00495                     + i->getExpr().toString());
00496                     // + "\n  op = " + ((Op) e.getOp).toString());
00497       pfs.push_back(i->getProof());
00498     }
00499     pf = newPf("optimized_subst_op",e,e2,pfs);
00500   }
00501   Theorem res = newRWTheorem(e, e2, a, pf);
00502   IF_DEBUG(debugger.setElapsed(tmpTimer);
00503      accum0 += tmpTimer;)
00504   if (!res.isRefl()) res.setSubst();
00505   return res;
00506 }
00507 
00508 
00509 Theorem CommonTheoremProducer::substitutivityRule(const Expr& e,
00510                                                   const int changed,
00511                                                   const Theorem& thm)
00512 {
00513   // Get the arity of the expression
00514   int size = e.arity();
00515 
00516   // The changed must be within the arity
00517   DebugAssert(size >= changed, "Bad call to substitutivityRule");
00518 
00519   // Check that t is c == d or c IFF d
00520   if(CHECK_PROOFS)
00521     CHECK_SOUND(thm.isRewrite() && thm.getLHS() == e[changed], "CVC3::CommonTheoremProducer::substitutivityRule:\n  "
00522                 "premise is not an equality or IFF: " + thm.getExpr().toString() + "\n" +
00523                 "e = " + e.toString());
00524 
00525   // Collect the new sub-expressions
00526   vector<Expr> c;
00527   for(int k = 0; k < size; ++ k)      
00528     if (k != changed) c.push_back(e[k]);
00529     else c.push_back(thm.getRHS());
00530 
00531   // Construct the new expression
00532   Expr e2(e.getOp(), c);
00533   
00534   // Check if they are the same 
00535   IF_DEBUG(if(e == e2) {
00536     ostream& os = debugger.getOS();
00537     os << "substitutivityRule: e = " << e << "\n e2 = " << e2 << endl;
00538   })
00539 
00540   // The new expressions must not be equal
00541   DebugAssert(e != e2, "substitutivityRule should not be called in this case:\ne = "+e.toString());
00542 
00543   // Construct the proof object
00544   Proof pf;
00545   Assumptions a(thm);
00546   if(withProof()) {
00547     // Check that t is c == d or c IFF d
00548     if(CHECK_PROOFS)
00549       CHECK_SOUND(thm.isRewrite(), "CVC3::CommonTheoremProducer::substitutivityRule:\npremise is not an equality or IFF: " + thm.getExpr().toString());                 
00550     pf = newPf("optimized_subst_op2",e,e2,thm.getProof());
00551   }
00552 
00553   // Return the resulting theorem 
00554   Theorem res = newRWTheorem(e, e2, a, pf);;
00555   res.setSubst();
00556   return res;
00557 }
00558 
00559 
00560 // |- e,  |- !e ==> |- FALSE
00561 Theorem CommonTheoremProducer::contradictionRule(const Theorem& e,
00562                                                  const Theorem& not_e) {
00563   Proof pf;
00564   if(CHECK_PROOFS)
00565     CHECK_SOUND(!e.getExpr() == not_e.getExpr(),
00566     "CommonTheoremProducer::contraditionRule: "
00567     "theorems don't match:\n e = "+e.toString()
00568     +"\n not_e = "+not_e.toString());
00569   Assumptions a(e, not_e);
00570   if(withProof()) {
00571     vector<Proof> pfs;
00572     pfs.push_back(e.getProof());
00573     pfs.push_back(not_e.getProof());
00574     pf = newPf("contradition", e.getExpr(), pfs);
00575   }
00576   return newTheorem(d_em->falseExpr(), a, pf);
00577 }
00578 
00579 
00580 Theorem CommonTheoremProducer::excludedMiddle(const Expr& e)
00581 {
00582   Proof pf;
00583   if (withProof()) {
00584     pf = newPf("excludedMiddle", e);
00585   }
00586   return newTheorem(e.orExpr(!e), Assumptions::emptyAssump(), pf);
00587 }
00588 
00589 
00590 // e ==> e IFF TRUE
00591 Theorem CommonTheoremProducer::iffTrue(const Theorem& e)
00592 {
00593   Proof pf;
00594   if(withProof()) {
00595     pf = newPf("iff_true", e.getExpr(), e.getProof());
00596   }
00597   return newRWTheorem(e.getExpr(), d_em->trueExpr(), Assumptions(e), pf);
00598 }
00599 
00600 
00601 // e ==> !e IFF FALSE
00602 Theorem CommonTheoremProducer::iffNotFalse(const Theorem& e) {
00603   Proof pf;
00604   if(withProof()) {
00605     pf = newPf("iff_not_false", e.getExpr(), e.getProof());
00606   }
00607   return newRWTheorem(!e.getExpr(), d_em->falseExpr(), Assumptions(e), pf);
00608 }
00609 
00610 
00611 // e IFF TRUE ==> e
00612 Theorem CommonTheoremProducer::iffTrueElim(const Theorem& e) {
00613   if(CHECK_PROOFS)
00614     CHECK_SOUND(e.isRewrite() && e.getRHS().isTrue(),
00615     "CommonTheoremProducer::iffTrueElim: "
00616     "theorem is not e<=>TRUE: "+ e.toString());
00617   Proof pf;
00618   if(withProof()) {
00619     pf = newPf("iff_true_elim", e.getLHS(), e.getProof());
00620   }
00621   return newTheorem(e.getLHS(), Assumptions(e), pf);
00622 }
00623 
00624 
00625 // e IFF FALSE ==> !e
00626 Theorem CommonTheoremProducer::iffFalseElim(const Theorem& e) {
00627   if(CHECK_PROOFS)
00628     CHECK_SOUND(e.isRewrite() && e.getRHS().isFalse(),
00629     "CommonTheoremProducer::iffFalseElim: "
00630     "theorem is not e<=>FALSE: "+ e.toString());
00631   const Expr& lhs = e.getLHS();
00632   Proof pf;
00633   if(withProof()) {
00634     pf = newPf("iff_false_elim", lhs, e.getProof());
00635   }
00636   return newTheorem(!lhs, Assumptions(e), pf);
00637 }
00638 
00639 
00640 // e1 <=> e2  ==>  ~e1 <=> ~e2
00641 Theorem CommonTheoremProducer::iffContrapositive(const Theorem& e) {
00642   if(CHECK_PROOFS)
00643     CHECK_SOUND(e.isRewrite() && e.getRHS().getType().isBool(),
00644     "CommonTheoremProducer::iffContrapositive: "
00645     "theorem is not e1<=>e2: "+ e.toString());
00646   Proof pf;
00647   if(withProof()) {
00648     pf = newPf("iff_contrapositive", e.getExpr(), e.getProof());
00649   }
00650   return newRWTheorem(e.getLHS().negate(),e.getRHS().negate(), Assumptions(e), pf);
00651 }
00652 
00653 
00654 // !!e ==> e
00655 Theorem CommonTheoremProducer::notNotElim(const Theorem& not_not_e) {
00656   if(CHECK_PROOFS)
00657     CHECK_SOUND(not_not_e.getExpr().isNot() && not_not_e.getExpr()[0].isNot(),
00658     "CommonTheoremProducer::notNotElim: bad theorem: !!e = "
00659     + not_not_e.toString());
00660   Proof pf;
00661   if(withProof())
00662     pf = newPf("not_not_elim", not_not_e.getExpr(), not_not_e.getProof());
00663   return newTheorem(not_not_e.getExpr()[0][0], Assumptions(not_not_e), pf);
00664 }
00665 
00666 
00667 Theorem CommonTheoremProducer::iffMP(const Theorem& e1, const Theorem& e1_iff_e2)
00668 {
00669   if(CHECK_PROOFS) {
00670     CHECK_SOUND(e1_iff_e2.isRewrite(),
00671     "iffMP: not IFF: "+e1_iff_e2.toString());
00672     CHECK_SOUND(e1.getExpr() == (e1_iff_e2.getLHS()),
00673     "iffMP: theorems don't match:\n  e1 = " + e1.toString()
00674     + ", e1_iff_e2 = " + e1_iff_e2.toString());
00675   }
00676   const Expr& e2(e1_iff_e2.getRHS());
00677   // Avoid e1.getExpr(), it may cause unneeded Expr creation
00678   if (e1_iff_e2.getLHS() == e2) return e1;
00679   Proof pf;
00680   Assumptions a(e1, e1_iff_e2);
00681   if(withProof()) {
00682     vector<Proof> pfs;
00683     pfs.push_back(e1.getProof());
00684     pfs.push_back(e1_iff_e2.getProof());
00685     pf = newPf("iff_mp", e1.getExpr(), e2, pfs);
00686   }
00687   return newTheorem(e2, a, pf);
00688 }
00689 
00690 
00691 // e1 AND (e1 IMPLIES e2) ==> e2
00692 Theorem CommonTheoremProducer::implMP(const Theorem& e1,
00693                                       const Theorem& e1_impl_e2) {
00694   const Expr& impl = e1_impl_e2.getExpr();
00695   if(CHECK_PROOFS) {
00696     CHECK_SOUND(impl.isImpl() && impl.arity()==2,
00697     "implMP: not IMPLIES: "+impl.toString());
00698     CHECK_SOUND(e1.getExpr() == impl[0],
00699     "implMP: theorems don't match:\n  e1 = " + e1.toString()
00700     + ", e1_impl_e2 = " + impl.toString());
00701   }
00702   const Expr& e2 = impl[1];
00703   // Avoid e1.getExpr(), it may cause unneeded Expr creation
00704   //  if (impl[0] == e2) return e1;  // this line commented by yeting because of proof translation
00705   Proof pf;
00706   Assumptions a(e1, e1_impl_e2);
00707   if(withProof()) {
00708     vector<Proof> pfs;
00709     pfs.push_back(e1.getProof());
00710     pfs.push_back(e1_impl_e2.getProof());
00711     pf = newPf("impl_mp", e1.getExpr(), e2, pfs);
00712   }
00713   return newTheorem(e2, a, pf);
00714 }
00715 
00716 
00717 // AND(e_0,...e_{n-1}) ==> e_i
00718 Theorem CommonTheoremProducer::andElim(const Theorem& e, int i) {
00719   if(CHECK_PROOFS) {
00720     CHECK_SOUND(e.getExpr().isAnd(), "andElim: not an AND: " + e.toString());
00721     CHECK_SOUND(i < e.getExpr().arity(), "andElim: i = " + int2string(i)
00722     + " >= arity = " + int2string(e.getExpr().arity())
00723     + " in " + e.toString());
00724   }
00725   Proof pf;
00726   if(withProof())
00727     pf = newPf("andE", d_em->newRatExpr(i), e.getExpr(), e.getProof());
00728   return newTheorem(e.getExpr()[i], Assumptions(e), pf);
00729 }
00730 
00731 
00732 //! e1, e2 ==> AND(e1, e2)
00733 Theorem CommonTheoremProducer::andIntro(const Theorem& e1, const Theorem& e2) {
00734   vector<Theorem> thms;
00735   thms.push_back(e1);
00736   thms.push_back(e2);
00737   return andIntro(thms);
00738 }
00739 
00740 
00741 Theorem CommonTheoremProducer::andIntro(const vector<Theorem>& es) {
00742   Proof pf;
00743   if(CHECK_PROOFS)
00744     CHECK_SOUND(es.size() > 1,
00745     "andIntro(vector<Theorem>): vector must have more than 1 element");
00746   Assumptions a(es);
00747   /*
00748   if(withProof()) {
00749     vector<Proof> pfs;
00750     for(vector<Theorem>::const_iterator i=es.begin(), iend=es.end();
00751   i!=iend; ++i)
00752       pfs.push_back(i->getProof());
00753     //    pf = newPf("andI", andExpr(kids), pfs);
00754   }
00755   */
00756   vector<Expr> kids;
00757   for(vector<Theorem>::const_iterator i=es.begin(), iend=es.end();
00758       i!=iend; ++i)
00759     kids.push_back(i->getExpr());
00760 
00761   if(withProof()) {
00762     vector<Proof> pfs;
00763     for(vector<Theorem>::const_iterator i=es.begin(), iend=es.end();
00764   i!=iend; ++i)
00765       pfs.push_back(i->getProof());
00766     pf = newPf("andI", andExpr(kids), pfs);
00767   }
00768   return newTheorem(andExpr(kids), a, pf);
00769 }
00770 
00771 
00772 //  G,a1,...,an |- phi
00773 // -------------------------------------------------
00774 //  G |- (a1 & ... & an) -> phi
00775 Theorem CommonTheoremProducer::implIntro(const Theorem& phi,
00776                                          const std::vector<Expr>& assump) {
00777   bool checkProofs(CHECK_PROOFS);
00778   // This rule only makes sense when runnnig with assumptions
00779   if(checkProofs) {
00780     CHECK_SOUND(withAssumptions(),
00781     "implIntro: called while running without assumptions");
00782   }
00783 
00784   const Assumptions& phiAssump = phi.getAssumptionsRef();
00785 
00786   if(checkProofs) {
00787     for(size_t i=0; i<assump.size(); i++) {
00788       const Theorem& thm = phiAssump[assump[i]];
00789       CHECK_SOUND(!thm.isNull() && thm.isAssump(),
00790       "implIntro: this is not an assumption of phi:\n\n"
00791       "  a["+int2string(i)+"] = "+assump[i].toString()
00792       +"\n\n  phi = "+phi.getExpr().toString());
00793     }
00794   }
00795 
00796   // Proof compaction: trivial derivation
00797   if(assump.size() == 0) return phi;
00798 
00799   Assumptions a(phiAssump - assump);
00800   Proof pf;
00801   if(withProof()) {
00802     vector<Proof> u; // Proof labels for assumptions
00803     for(vector<Expr>::const_iterator i=assump.begin(), iend=assump.end();
00804   i!=iend; ++i) {
00805       const Theorem& t = phiAssump[*i];
00806       u.push_back(t.getProof());
00807     }
00808     // Arguments to the proof rule:
00809     // impl_intro_3(phi, a1,...,an,tcc1,...tccn,pf_tcc1,...pf_tccn,
00810     //              [lambda(a1,...,an): pf_phi])
00811     vector<Expr> args;
00812     vector<Proof> pfs;
00813     args.push_back(phi.getExpr());
00814     args.insert(args.end(), assump.begin(), assump.end());
00815     // Lambda-abstraction of pf_phi
00816     pfs.push_back(newPf(u, assump, phi.getProof()));
00817     pf = newPf("impl_intro", args, pfs);
00818   }
00819   Expr conj(andExpr(assump));
00820   return newTheorem(conj.impExpr(phi.getExpr()), a, pf);
00821 }
00822 
00823 
00824 // e1 => e2  ==>  ~e2 => ~e1
00825 Theorem CommonTheoremProducer::implContrapositive(const Theorem& thm) {
00826   const Expr& impl = thm.getExpr();
00827   if(CHECK_PROOFS) {
00828     CHECK_SOUND(impl.isImpl() && impl.arity()==2,
00829     "CommonTheoremProducer::implContrapositive: thm="
00830     +impl.toString());
00831   }
00832   Proof pf;
00833   if(withProof())
00834     pf = newPf("impl_contrapositive", impl, thm.getProof());
00835   return newTheorem(impl[1].negate().impExpr(impl[0].negate()), Assumptions(thm), pf);
00836 }
00837 
00838 
00839 // ==> ITE(TRUE, e1, e2) == e1
00840 Theorem
00841 CommonTheoremProducer::rewriteIteTrue(const Expr& e) {
00842   Proof pf;
00843   if(CHECK_PROOFS)
00844     CHECK_SOUND(e.isITE() && e[0].isTrue(),
00845     "rewriteIteTrue precondition violated");
00846   if(withProof()) {
00847     Type t = e[1].getType();
00848     DebugAssert(!t.isNull(), "rewriteIteTrue: e1 has no type: "
00849     + e[1].toString());
00850     bool useIff = t.isBool();
00851     if(useIff)
00852       pf = newPf("rewrite_ite_true_iff", e[1], e[2]);
00853     else {
00854       pf = newPf("rewrite_ite_true", t.getExpr(), e[1], e[2]);
00855     }
00856   }
00857   return newRWTheorem(e, e[1], Assumptions::emptyAssump(), pf);
00858 }
00859 
00860 
00861 // ==> ITE(FALSE, e1, e2) == e2
00862 Theorem
00863 CommonTheoremProducer::rewriteIteFalse(const Expr& e) {
00864   Proof pf;
00865   if(CHECK_PROOFS)
00866     CHECK_SOUND(e.isITE() && e[0].isFalse(),
00867     "rewriteIteFalse precondition violated");
00868   if(withProof()) {
00869     Type t = e[1].getType();
00870     DebugAssert(!t.isNull(), "rewriteIteFalse: e1 has no type: "
00871     + e[1].toString());
00872     bool useIff = t.isBool();
00873     if(useIff)
00874       pf = newPf("rewrite_ite_false_iff", e[1], e[2]);
00875     else {
00876       pf = newPf("rewrite_ite_false", t.getExpr(), e[1], e[2]);
00877     }
00878   }
00879   return newRWTheorem(e, e[2], Assumptions::emptyAssump(), pf);
00880 }
00881 
00882 
00883 // ==> ITE(c, e, e) == e
00884 Theorem
00885 CommonTheoremProducer::rewriteIteSame(const Expr& e) {
00886   Proof pf;
00887   if(CHECK_PROOFS)
00888     CHECK_SOUND(e.isITE() && e[1] == e[2],
00889     "rewriteIteSame precondition violated");
00890   if(withProof()) {
00891     Type t = e[1].getType();
00892     DebugAssert(!t.isNull(), "rewriteIteSame: e[1] has no type: "
00893     + e[1].toString());
00894     bool useIff = t.isBool();
00895     if(useIff)
00896       pf = newPf("rewrite_ite_same_iff", e[0], e[1]);
00897     else {
00898       pf = newPf("rewrite_ite_same", t.getExpr(), e[0], e[1]);
00899     }
00900   }
00901   return newRWTheorem(e, e[1], Assumptions::emptyAssump(), pf);
00902 }
00903 
00904 
00905 // NOT e ==> e IFF FALSE
00906 Theorem CommonTheoremProducer::notToIff(const Theorem& not_e)
00907 {
00908   if(CHECK_PROOFS)
00909     CHECK_SOUND(not_e.getExpr().isNot(),
00910     "notToIff: not NOT: "+not_e.toString());
00911 
00912   // Make it an atomic rule (more efficient)
00913   Expr e(not_e.getExpr()[0]);
00914   Proof pf;
00915   if(withProof())
00916     pf=newPf("not_to_iff", e, not_e.getProof());
00917   return newRWTheorem(e, d_em->falseExpr(), Assumptions(not_e), pf);
00918 }
00919 
00920 
00921 // e1 XOR e2 ==> e1 IFF (NOT e2)
00922 Theorem CommonTheoremProducer::xorToIff(const Expr& e)
00923 {
00924   if(CHECK_PROOFS) {
00925     CHECK_SOUND(e.isXor(), "xorToIff precondition violated");
00926     CHECK_SOUND(e.arity() >= 2, "Expected XOR of arity >= 2");
00927   }
00928   Expr res = e[e.arity()-1];
00929   for (int i = e.arity()-2; i >=0; --i) {
00930     res = (!e[i]).iffExpr(res);
00931   }
00932   Proof pf;
00933   if(withProof()) {
00934     pf = newPf("xorToIff");
00935   }
00936   return newRWTheorem(e, res, Assumptions::emptyAssump(), pf);
00937 }
00938 
00939 
00940 // ==> IFF(e1,e2) IFF <simplified expr>
00941 Theorem CommonTheoremProducer::rewriteIff(const Expr& e) {
00942   Proof pf;
00943   if(CHECK_PROOFS)
00944     CHECK_SOUND(e.isIff(), "rewriteIff precondition violated");
00945   if(withProof()) {
00946     pf = newPf("rewrite_iff", e[0], e[1]);
00947   }
00948 
00949   if(e[0] == e[1]) return rewriteReflexivity(e);
00950 
00951   switch(e[0].getKind()) {
00952   case TRUE_EXPR:
00953     return newRWTheorem(e, e[1], Assumptions::emptyAssump(), pf);
00954   case FALSE_EXPR:
00955     return newRWTheorem(e, !e[1], Assumptions::emptyAssump() ,pf);
00956   case NOT:
00957     if(e[0][0]==e[1]) 
00958       return newRWTheorem(e, d_em->falseExpr(), Assumptions::emptyAssump(), pf);
00959     break;
00960   default: break;
00961   }
00962   
00963   switch(e[1].getKind()) {
00964   case TRUE_EXPR:
00965     return newRWTheorem(e, e[0], Assumptions::emptyAssump(), pf);
00966   case FALSE_EXPR:
00967     return newRWTheorem(e, !e[0], Assumptions::emptyAssump(), pf);
00968   case NOT:
00969     if(e[0]==e[1][0]) 
00970       return newRWTheorem(e, d_em->falseExpr(), Assumptions::emptyAssump(), pf);
00971     break;
00972   default:
00973     break;
00974   }
00975 
00976   if(e[0] < e[1])
00977     return rewriteUsingSymmetry(e);
00978   else
00979     return reflexivityRule(e);
00980 }
00981 
00982 
00983 // ==> AND(e_1,...,e_n) IFF <simplified expr>
00984 // 1) if e_i = FALSE then return FALSE
00985 // 2) if e_i = TRUE, remove it from children
00986 // 3) if e_i = AND(f_1,...,f_m) then AND(e_1,...,e_{i-1},f_1,...,f_m,e_{i+1},...,e_n)
00987 // 4) if n=0 return TRUE
00988 // 5) if n=1 return e_1
00989 Theorem CommonTheoremProducer::rewriteAnd(const Expr& e) {
00990   if(CHECK_PROOFS)
00991     CHECK_SOUND(e.isAnd(), "rewriteAnd: bad Expr: " + e.toString());
00992   Proof pf;
00993   ExprMap<bool> newKids;
00994   bool isFalse (false);
00995   for (Expr::iterator k=e.begin(), kend=e.end(); !isFalse && k != kend; ++k) {
00996     const Expr& ek = *k;
00997     if (ek.isFalse()) { isFalse=true; break; }
00998     if (ek.isAnd() && ek.arity() < 10) {
00999       for(Expr::iterator j=ek.begin(), jend=ek.end(); j!=jend; ++j) {
01000   if(newKids.count(j->negate()) > 0) { isFalse=true; break; }
01001   newKids[*j]=true;
01002       }
01003     } else if(!ek.isTrue()) {
01004       if(newKids.count(ek.negate()) > 0) { isFalse=true; break; }
01005       newKids[ek]=true;
01006     }
01007   }
01008   Expr res;
01009   if (isFalse) res = d_em->falseExpr();
01010   else if (newKids.size() == 0) res = d_em->trueExpr(); // All newKids were TRUE
01011   else if (newKids.size() == 1)
01012     res = newKids.begin()->first; // The only child
01013   else {
01014     vector<Expr> v;
01015     for(ExprMap<bool>::iterator i=newKids.begin(), iend=newKids.end();
01016         i!=iend; ++i)
01017       v.push_back(i->first);
01018     res = andExpr(v);
01019   }
01020   if(withProof()) {
01021     pf = newPf("rewrite_and", e,res);
01022   }
01023   return newRWTheorem(e, res, Assumptions::emptyAssump(), pf);
01024 }
01025 
01026 
01027 // ==> OR(e1,e2) IFF <simplified expr>
01028 Theorem CommonTheoremProducer::rewriteOr(const Expr& e) {
01029   if(CHECK_PROOFS)
01030     CHECK_SOUND(e.isOr(), "rewriteOr: bad Expr: " + e.toString());
01031   Proof pf;
01032   ExprMap<bool> newKids;
01033   bool isTrue (false);
01034   for (Expr::iterator k=e.begin(), kend=e.end(); !isTrue && k != kend; ++k) {
01035     const Expr& ek = *k;
01036     if (ek.isTrue()) { isTrue=true; break; }
01037     else if (ek.isOr() && ek.arity() < 10) {
01038       for(Expr::iterator j=ek.begin(), jend=ek.end(); j!=jend; ++j) {
01039   if(newKids.count(j->negate()) > 0) { isTrue=true; break; }
01040   newKids[*j]=true;
01041       }
01042     } else if(!ek.isFalse()) {
01043       if(newKids.count(ek.negate()) > 0) { isTrue=true; break; }
01044       newKids[ek]=true;
01045     }
01046   }
01047   Expr res;
01048   if (isTrue) res = d_em->trueExpr();
01049   else if (newKids.size() == 0) res = d_em->falseExpr(); // All kids were FALSE
01050   else if (newKids.size() == 1) res = newKids.begin()->first; // The only child
01051   else {
01052     vector<Expr> v;
01053     for(ExprMap<bool>::iterator i=newKids.begin(), iend=newKids.end();
01054         i!=iend; ++i)
01055       v.push_back(i->first);
01056     res = orExpr(v);
01057   }
01058   if(withProof()) {
01059     pf = newPf("rewrite_or", e, res);
01060   }
01061   return newRWTheorem(e, res, Assumptions::emptyAssump(), pf);
01062 }
01063 
01064 
01065 // ==> NOT TRUE IFF FALSE
01066 Theorem CommonTheoremProducer::rewriteNotTrue(const Expr& e) {
01067   Proof pf;
01068   if(CHECK_PROOFS)
01069     CHECK_SOUND(e.isNot() && e[0].isTrue(),
01070     "rewriteNotTrue precondition violated");
01071   if(withProof())
01072     pf = newPf("rewrite_not_true");
01073   return newRWTheorem(e, d_em->falseExpr(), Assumptions::emptyAssump(), pf);
01074 }
01075 
01076 
01077 // ==> NOT FALSE IFF TRUE
01078 Theorem CommonTheoremProducer::rewriteNotFalse(const Expr& e) {
01079   Proof pf;
01080   if(CHECK_PROOFS)
01081     CHECK_SOUND(e.isNot() && e[0].isFalse(),
01082     "rewriteNotFalse precondition violated");
01083   if(withProof())
01084     pf = newPf("rewrite_not_false");
01085   return newRWTheorem(e, d_em->trueExpr(), Assumptions::emptyAssump(), pf);
01086 }
01087 
01088 
01089 // ==> (NOT NOT e) IFF e, takes !!e
01090 Theorem CommonTheoremProducer::rewriteNotNot(const Expr& e) {
01091   Proof pf;
01092   if(CHECK_PROOFS)
01093     CHECK_SOUND(e.isNot() && e[0].isNot(),
01094     "rewriteNotNot precondition violated");
01095   if(withProof())
01096     pf = newPf("rewrite_not_not", e[0][0]);
01097   return newRWTheorem(e, e[0][0], Assumptions::emptyAssump(), pf);
01098 }
01099 
01100 
01101 //! ==> NOT FORALL (vars): e  IFF EXISTS (vars) NOT e
01102 Theorem CommonTheoremProducer::rewriteNotForall(const Expr& e) {
01103   if(CHECK_PROOFS) {
01104     CHECK_SOUND(e.isNot() && e[0].isForall(),
01105     "rewriteNotForall: expr must be NOT FORALL:\n"
01106     +e.toString());
01107   }
01108   Proof pf;
01109   if(withProof())
01110     pf = newPf("rewrite_not_forall", e);
01111   return newRWTheorem(e, d_em->newClosureExpr(EXISTS, e[0].getVars(),
01112                                               !e[0].getBody()), Assumptions::emptyAssump(), pf);
01113 }
01114 
01115 
01116 //! ==> NOT EXISTS (vars): e  IFF FORALL (vars) NOT e
01117 Theorem CommonTheoremProducer::rewriteNotExists(const Expr& e) {
01118   if(CHECK_PROOFS) {
01119     CHECK_SOUND(e.isNot() && e[0].isExists(),
01120     "rewriteNotExists: expr must be NOT FORALL:\n"
01121     +e.toString());
01122   }
01123   Proof pf;
01124   if(withProof())
01125     pf = newPf("rewrite_not_exists", e);
01126   return newRWTheorem(e, d_em->newClosureExpr(FORALL, e[0].getVars(),
01127                                               !e[0].getBody()), Assumptions::emptyAssump(), pf);
01128 }
01129 
01130 
01131 Expr CommonTheoremProducer::skolemize(const Expr& e)
01132 {
01133   vector<Expr> vars;
01134   const vector<Expr>& boundVars = e.getVars(); 
01135   for(unsigned int i=0; i<boundVars.size(); i++) {
01136     Expr skolV(e.skolemExpr(i));
01137     Type tp(e.getVars()[i].getType());
01138     skolV.setType(tp);
01139     vars.push_back(skolV);
01140   }
01141   return(e.getBody().substExpr(boundVars, vars));
01142 }
01143 
01144 
01145 Theorem CommonTheoremProducer::skolemizeRewrite(const Expr& e)
01146 {
01147   Proof pf;
01148   if(CHECK_PROOFS) {
01149     CHECK_SOUND(e.isExists(), "skolemize rewrite called on non-existential: "
01150     + e.toString());
01151   }
01152   Expr skol = skolemize(e);
01153   if(withProof()) {
01154     Expr rw(e.iffExpr(skol));
01155     pf = newLabel(rw);
01156   }
01157   TRACE("quantlevel", "skolemize ", skol, "");
01158   TRACE("quantlevel sko", "skolemize ", skol, "");
01159   TRACE("quantlevel sko", "skolemize from org ", e, "");
01160   return newRWTheorem(e, skol, Assumptions::emptyAssump(), pf);
01161 
01162 }
01163 
01164 
01165 Theorem CommonTheoremProducer::skolemizeRewriteVar(const Expr& e)
01166 {
01167   Proof pf;
01168   if(CHECK_PROOFS) {
01169     CHECK_SOUND(e.isExists(), "skolemizeRewriteVar("
01170     +e.toString()+")");
01171   }
01172 
01173   const vector<Expr>& boundVars = e.getVars();
01174   const Expr& body = e.getBody();
01175 
01176   if(CHECK_PROOFS) {
01177     CHECK_SOUND(boundVars.size()==1, "skolemizeRewriteVar("
01178     +e.toString()+")");
01179     CHECK_SOUND(body.isEq() || body.isIff(), "skolemizeRewriteVar("
01180     +e.toString()+")");
01181     const Expr& v = boundVars[0];
01182     CHECK_SOUND(body[1] == v, "skolemizeRewriteVar("
01183     +e.toString()+")");
01184     CHECK_SOUND(!(v.subExprOf(body[0])), "skolemizeRewriteVar("
01185     +e.toString()+")");
01186   }
01187   // Create the Skolem constant appropriately
01188   Expr skolV(e.skolemExpr(0));
01189   Type tp(e.getVars()[0].getType());
01190   skolV.setType(tp);
01191   // Skolemized expression
01192   Expr skol = Expr(body.getOp(), body[0], skolV);
01193 
01194   if(withProof()) {
01195     Expr rw(e.iffExpr(skol));
01196     pf = newLabel(rw);
01197   }
01198   return newRWTheorem(e, skol, Assumptions::emptyAssump(), pf);
01199 }
01200 
01201 
01202 Theorem CommonTheoremProducer::varIntroRule(const Expr& phi) {
01203   // This rule is sound for all expressions phi
01204   Proof pf;
01205   const Expr boundVar = d_em->newBoundVarExpr(phi.getType());
01206 
01207   Expr body;  
01208   if(phi.getType().isBool())
01209     body = phi.iffExpr(boundVar);
01210   else
01211     body = phi.eqExpr(boundVar);
01212 
01213   std::vector<Expr> v; 
01214   v.push_back(boundVar);
01215   const Expr result = d_em->newClosureExpr(EXISTS, v, body);
01216   
01217   if(withProof()) 
01218     pf = newPf("var_intro", phi, boundVar);
01219   return newTheorem(result, Assumptions::emptyAssump(), pf);
01220 }
01221 
01222 
01223 Theorem CommonTheoremProducer::skolemize(const Theorem& thm) { 
01224   const Expr& e = thm.getExpr();
01225   if(e.isExists()) {
01226     TRACE("skolem", "Skolemizing existential:", "", "{");
01227     CDMap<Expr, Theorem>::iterator i=d_skolemized_thms.find(e),
01228       iend=d_skolemized_thms.end();
01229     if(i!=iend) {
01230       TRACE("skolem", "Skolemized theorem found in map: ", (*i).second, "}");
01231       return iffMP(thm, (*i).second);
01232     }
01233     Theorem skol = skolemizeRewrite(e);
01234     for(unsigned int i=0; i<e.getVars().size(); i++) {
01235       Expr skolV(e.skolemExpr(i));
01236       Type tp(e.getVars()[i].getType());
01237       skolV.setType(tp);
01238     }
01239     d_skolem_axioms.push_back(skol);
01240     d_skolemized_thms.insert(e, skol, 0);//d_coreSatAPI->getBottomScope());
01241     skol = iffMP(thm, skol); 
01242 
01243     TRACE("skolem", "skolemized new theorem: ", skol, "}");
01244     return skol;
01245   }
01246   return thm;
01247 }
01248 
01249 
01250 Theorem CommonTheoremProducer::varIntroSkolem(const Expr& e) {
01251   // First, look up the cache
01252   CDMap<Expr, Theorem>::iterator i=d_skolemVars.find(e),
01253     iend=d_skolemVars.end();
01254   if(i!=iend) return (*i).second;
01255   // Not in cache; create a new one
01256   Theorem thm = varIntroRule(e);
01257   const Expr& e2 = thm.getExpr();
01258   DebugAssert(e2.isExists() && e2.getVars().size()==1, "varIntroSkolem: e2 = "
01259         +e2.toString());
01260   Theorem skolThm;
01261   // Check if we have a corresponding skolemized version already
01262   CDMap<Expr, Theorem>::iterator j=d_skolemized_thms.find(e2),
01263     jend=d_skolemized_thms.end();
01264   if(j!=jend) {
01265     skolThm = (*i).second;
01266   } else {
01267     skolThm = skolemizeRewriteVar(e2);
01268     d_skolem_axioms.push_back(skolThm);
01269     d_skolemized_thms.insert(e2, skolThm, 0); //d_coreSatAPI->getBottomScope());
01270   }
01271   thm = iffMP(thm, skolThm);
01272   d_skolemVars.insert(e, thm, 0); //d_coreSatAPI->getBottomScope());
01273   return thm;
01274 }
01275 
01276 
01277 // Derived Rules
01278 
01279 
01280 Theorem CommonTheoremProducer::trueTheorem()
01281 {
01282   return iffTrueElim(reflexivityRule(d_em->trueExpr()));
01283 }
01284 
01285 
01286 Theorem CommonTheoremProducer::rewriteAnd(const Theorem& e)
01287 {
01288   return iffMP(e, rewriteAnd(e.getExpr()));
01289 }
01290 
01291 
01292 Theorem CommonTheoremProducer::rewriteOr(const Theorem& e)
01293 {
01294   return iffMP(e, rewriteOr(e.getExpr()));
01295 }
01296 
01297 
01298 Theorem CommonTheoremProducer::ackermann(const Expr& e1, const Expr& e2)
01299 {
01300   Proof pf;
01301   if(CHECK_PROOFS)
01302     CHECK_SOUND(e1.isApply() && e2.isApply() && e1.getOp() == e2.getOp(),
01303     "ackermann precondition violated");
01304   Expr hyp;
01305   int ar = e1.arity();
01306   if (ar == 1) {
01307     hyp = Expr(e1[0].eqExpr(e2[0]));
01308   }
01309   else {
01310     vector<Expr> vec;
01311     for (int i = 0; i != ar; ++i) {
01312       vec.push_back(e1[i].eqExpr(e2[i]));
01313     }
01314     hyp = Expr(AND, vec);
01315   }
01316   if(withProof())
01317     pf = newPf("ackermann", e1, e2);
01318   return newTheorem(hyp.impExpr(e1.eqExpr(e2)), Assumptions::emptyAssump(), pf);
01319 }
01320 
01321 
01322 void CommonTheoremProducer::findITE(const Expr& e, Expr& condition, Expr& thenpart, Expr& elsepart)
01323 {
01324   if (!e.getType().isBool() && e.isITE()) {
01325     condition = e[0];
01326     if (!condition.containsTermITE()) {
01327       thenpart = e[1];
01328       elsepart = e[2];
01329       return;
01330     }
01331   }
01332 
01333   vector<Expr> kids;
01334   int i = 0;
01335   for (; i < e.arity(); ++i) {
01336     if (e[i].containsTermITE()) break;
01337     kids.push_back(e[i]);
01338   }
01339 
01340   if(CHECK_PROOFS) {
01341     CHECK_SOUND(i < e.arity(), "could not find ITE");
01342   }
01343 
01344   Expr t2, e2;
01345   findITE(e[i], condition, t2, e2);
01346 
01347   kids.push_back(t2);
01348   for(int k = i+1; k < e.arity(); ++k) {
01349     kids.push_back(e[k]);
01350   }
01351 
01352   thenpart = Expr(e.getOp(), kids);
01353 
01354   kids[i] = e2;
01355   elsepart = Expr(e.getOp(), kids);
01356 }
01357 
01358 
01359 Theorem CommonTheoremProducer::liftOneITE(const Expr& e) {
01360 
01361   if(CHECK_PROOFS) {
01362     CHECK_SOUND(e.containsTermITE(), "CommonTheoremProducer::liftOneITE: bad input" + e.toString());
01363   }
01364 
01365   Expr cond, thenpart, elsepart;
01366 
01367   findITE(e, cond, thenpart, elsepart);
01368 
01369   Proof pf;
01370   if(withProof())
01371     pf = newPf("lift_one_ite", e);
01372 
01373   return newRWTheorem(e, cond.iteExpr(thenpart, elsepart), Assumptions::emptyAssump(), pf);
01374 }

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