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, a1_eq_a2.getAssumptionsRef(), 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,thm.getProof());
00326   return newRWTheorem(e, e2, thm.getAssumptionsRef(), pf);
00327 }
00328 
00329 
00330 Theorem CommonTheoremProducer::substitutivityRule(const Expr& e,
00331                                                   const Theorem& thm1,
00332                                                   const Theorem& thm2) {
00333   IF_DEBUG
00334     (static DebugTimer
00335        accum0(debugger.timer("substitutivityRule1 time"));
00336      static DebugTimer tmpTimer(debugger.newTimer());
00337      static DebugCounter count(debugger.counter("substitutivityRule1 calls"));
00338      debugger.setCurrentTime(tmpTimer);
00339      count++);
00340 
00341   // Check that t is c == d or c IFF d
00342   if(CHECK_PROOFS) {
00343     CHECK_SOUND(e.arity() == 2 && e[0] == thm1.getLHS() &&
00344                 e[1] == thm2.getLHS(),
00345                 "Unexpected use of substitutivityRule1");
00346     CHECK_SOUND(thm1.isRewrite(),
00347                 "CVC3::CommonTheoremProducer::substitutivityRule1:\n  "
00348                 "premis is not an equality or IFF: "
00349                 + thm1.getExpr().toString()
00350                 + "\n  expr = " + e.toString());
00351     CHECK_SOUND(thm2.isRewrite(),
00352                 "CVC3::CommonTheoremProducer::substitutivityRule1:\n  "
00353                 "premis is not an equality or IFF: "
00354                 + thm2.getExpr().toString()
00355                 + "\n  expr = " + e.toString());
00356   }
00357   Expr e2(e.getOp(), thm1.getRHS(), thm2.getRHS());
00358   Proof pf;
00359   if(withProof()) {
00360     vector<Proof> pfs;
00361     pfs.push_back(thm1.getProof());
00362     pfs.push_back(thm2.getProof());
00363     pf = newPf("basic_subst_op1", e, pfs);
00364   }
00365   return newRWTheorem(e, e2, Assumptions(thm1, thm2), pf);
00366 }
00367 
00368 
00369 Theorem CommonTheoremProducer::substitutivityRule(const Op& op,
00370                                                   const vector<Theorem>& thms) {
00371   IF_DEBUG
00372     (static DebugTimer
00373        accum0(debugger.timer("substitutivityRule time"));
00374      static DebugTimer tmpTimer(debugger.newTimer());
00375      static DebugCounter count(debugger.counter("substitutivityRule calls"));
00376      debugger.setCurrentTime(tmpTimer);
00377      count++);
00378   // Check for trivial case: no theorems, return (op == op)
00379   unsigned size(thms.size());
00380   if(size == 0)
00381     return reflexivityRule(d_tm->getEM()->newLeafExpr(op));
00382   // Check that theorems are of the form c_i == d_i and collect
00383   // vectors of c_i's and d_i's and the vector of proofs
00384   vector<Expr> c, d;
00385   vector<Proof> pfs;
00386   // Reserve memory for argument vectors.  Do not reserve memory for
00387   // pfs, they are rarely used and slow anyway.
00388   c.reserve(size); d.reserve(size);
00389   for(vector<Theorem>::const_iterator i = thms.begin(), iend = thms.end();
00390       i != iend; ++i) {
00391     // Check that t is c == d or c IFF d
00392     if(CHECK_PROOFS)
00393       CHECK_SOUND(i->isRewrite(),
00394       "CVC3::CommonTheoremProducer::substitutivityRule:\n  "
00395       "premis is not an equality or IFF: "
00396       + i->getExpr().toString()
00397       + "\n  op = " + op.toString());
00398     // Collect the pieces
00399     c.push_back(i->getLHS());
00400     d.push_back(i->getRHS());
00401     if(withProof()) pfs.push_back(i->getProof());
00402   }
00403   Expr e1(op, c), e2(op, d);
00404   // Proof compaction: if e1 == e2, use reflexivity
00405   if(e1 == e2) return reflexivityRule(e1);
00406   // Otherwise, do the work
00407   Assumptions a(thms);
00408   Proof pf;
00409   if(withProof())
00410     // FIXME: this rule is not directly expressible in flea
00411     pf = newPf("basic_subst_op",e1,e2,pfs);
00412   Theorem res = newRWTheorem(e1, e2, a, pf);
00413   IF_DEBUG(debugger.setElapsed(tmpTimer);
00414      accum0 += tmpTimer);
00415   return res;
00416 }
00417 
00418 
00419 Theorem CommonTheoremProducer::substitutivityRule(const Expr& e,
00420                                                   const vector<unsigned>& changed,
00421                                                   const vector<Theorem>& thms) {
00422   IF_DEBUG
00423     (static DebugTimer
00424        accum0(debugger.timer("substitutivityRule2 time"));
00425      static DebugTimer tmpTimer(debugger.newTimer());
00426      static DebugCounter count(debugger.counter("substitutivityRule2 calls"));
00427      debugger.setCurrentTime(tmpTimer);
00428      count++);
00429   DebugAssert(changed.size() > 0, "substitutivityRule2 should not be called");
00430   DebugAssert(changed.size() == thms.size(), "substitutivityRule2: wrong args");
00431 
00432   // Check that theorems are of the form c_i == d_i and collect
00433   // vectors of c_i's and d_i's and the vector of proofs
00434   unsigned size = e.arity();
00435   if (size == 1) return substitutivityRule(e, thms.back());
00436   unsigned csize = changed.size();
00437   if (size == 2) {
00438     if (csize == 2) return substitutivityRule(e, thms[0], thms[1]);
00439     if (changed[0] == 0) {
00440       return substitutivityRule(e, thms[0], reflexivityRule(e[1]));
00441     }
00442     else {
00443       return substitutivityRule(e, reflexivityRule(e[0]), thms[0]);
00444     }
00445   }
00446   DebugAssert(size >= csize, "Bad call to substitutivityRule2");
00447 
00448   vector<Expr> c;
00449   bool checkProofs(CHECK_PROOFS);
00450   for(unsigned j = 0, k = 0; k < size; ++k) {
00451     if (j == csize || changed[j] != k) {
00452       c.push_back(e[k]);
00453       continue;
00454     }
00455     // Check that t is c == d or c IFF d
00456     if(checkProofs)
00457       CHECK_SOUND(thms[j].isRewrite() && thms[j].getLHS() == e[k],
00458       "CVC3::CommonTheoremProducer::substitutivityRule:\n  "
00459       "premis is not an equality or IFF: "
00460       + thms[j].getExpr().toString()
00461       + "\n  e = " + e.toString());
00462     // Collect the pieces
00463     c.push_back(thms[j].getRHS());
00464     ++j;
00465   }
00466   Expr e2(e.getOp(), c);
00467   IF_DEBUG(if(e == e2) {
00468     ostream& os = debugger.getOS();
00469     os << "substitutivityRule2: e = " << e << "\n e2 = " << e2
00470        << "\n changed kids: [\n";
00471     for(unsigned j=0; j<changed.size(); j++)
00472       os << "  (" << changed[j] << ") " << thms[j] << "\n";
00473     os << "]\n";
00474   });
00475   DebugAssert(e != e2,
00476         "substitutivityRule2 should not be called in this case:\n"
00477         "e = "+e.toString());
00478 
00479   Proof pf;
00480   Assumptions a(thms);
00481   if(withProof()) {
00482     vector<Proof> pfs;
00483     for(vector<Theorem>::const_iterator i = thms.begin(), iend = thms.end();
00484         i != iend; ++i) {
00485       // Check that t is c == d or c IFF d
00486       if(CHECK_PROOFS)
00487         CHECK_SOUND(i->isRewrite(),
00488                     "CVC3::CommonTheoremProducer::substitutivityRule:\n  "
00489                     "premis is not an equality or IFF: "
00490                     + i->getExpr().toString());
00491                     // + "\n  op = " + ((Op) e.getOp).toString());
00492       pfs.push_back(i->getProof());
00493     }
00494     pf = newPf("optimized_subst_op",e,e2,pfs);
00495   }
00496   Theorem res = newRWTheorem(e, e2, a, pf);
00497   IF_DEBUG(debugger.setElapsed(tmpTimer);
00498      accum0 += tmpTimer);
00499   return res;
00500 }
00501 
00502 
00503 Theorem CommonTheoremProducer::substitutivityRule(const Expr& e,
00504                                                   const int changed,
00505                                                   const Theorem& thm)
00506 {
00507   // Get the arity of the expression
00508   int size = e.arity();
00509 
00510   // The changed must be within the arity
00511   DebugAssert(size >= changed, "Bad call to substitutivityRule");
00512 
00513   // Check that t is c == d or c IFF d
00514   if(CHECK_PROOFS)
00515     CHECK_SOUND(thm.isRewrite() && thm.getLHS() == e[changed], "CVC3::CommonTheoremProducer::substitutivityRule:\n  "
00516                 "premise is not an equality or IFF: " + thm.getExpr().toString() + "\n" +
00517                 "e = " + e.toString());
00518 
00519   // Collect the new sub-expressions
00520   vector<Expr> c;
00521   for(int k = 0; k < size; ++ k)      
00522     if (k != changed) c.push_back(e[k]);
00523     else c.push_back(thm.getRHS());
00524 
00525   // Construct the new expression
00526   Expr e2(e.getOp(), c);
00527   
00528   // Check if they are the same 
00529   IF_DEBUG(if(e == e2) {
00530     ostream& os = debugger.getOS();
00531     os << "substitutivityRule: e = " << e << "\n e2 = " << e2 << endl;
00532   });
00533 
00534   // The new expressions must not be equal
00535   DebugAssert(e != e2, "substitutivityRule should not be called in this case:\ne = "+e.toString());
00536 
00537   // Construct the proof object
00538   Proof pf;
00539   Assumptions a(thm);
00540   if(withProof()) {
00541     // Check that t is c == d or c IFF d
00542     if(CHECK_PROOFS)
00543       CHECK_SOUND(thm.isRewrite(), "CVC3::CommonTheoremProducer::substitutivityRule:\npremise is not an equality or IFF: " + thm.getExpr().toString());                 
00544     pf = newPf("optimized_subst_op2",e,e2,thm.getProof());
00545   }
00546 
00547   // Return the resulting theorem 
00548   return newRWTheorem(e, e2, a, pf);;
00549 }
00550 
00551 
00552 // |- e,  |- !e ==> |- FALSE
00553 Theorem CommonTheoremProducer::contradictionRule(const Theorem& e,
00554                                                  const Theorem& not_e) {
00555   Proof pf;
00556   if(CHECK_PROOFS)
00557     CHECK_SOUND(!e.getExpr() == not_e.getExpr(),
00558     "CommonTheoremProducer::contraditionRule: "
00559     "theorems don't match:\n e = "+e.toString()
00560     +"\n not_e = "+not_e.toString());
00561   Assumptions a(e, not_e);
00562   if(withProof()) {
00563     vector<Proof> pfs;
00564     pfs.push_back(e.getProof());
00565     pfs.push_back(not_e.getProof());
00566     pf = newPf("contradition", e.getExpr(), pfs);
00567   }
00568   return newTheorem(d_em->falseExpr(), a, pf);
00569 }
00570 
00571 
00572 Theorem CommonTheoremProducer::excludedMiddle(const Expr& e)
00573 {
00574   Proof pf;
00575   if (withProof()) {
00576     pf = newPf("excludedMiddle", e);
00577   }
00578   return newTheorem(e.orExpr(!e), Assumptions::emptyAssump(), pf);
00579 }
00580 
00581 
00582 // e ==> e IFF TRUE
00583 Theorem CommonTheoremProducer::iffTrue(const Theorem& e)
00584 {
00585   Proof pf;
00586   if(withProof()) {
00587     pf = newPf("iff_true", e.getExpr(), e.getProof());
00588   }
00589   return newRWTheorem(e.getExpr(), d_em->trueExpr(), e.getAssumptionsRef(), pf);
00590 }
00591 
00592 
00593 // e ==> !e IFF FALSE
00594 Theorem CommonTheoremProducer::iffNotFalse(const Theorem& e) {
00595   Proof pf;
00596   if(withProof()) {
00597     pf = newPf("iff_not_false", e.getExpr(), e.getProof());
00598   }
00599   return newRWTheorem(!e.getExpr(), d_em->falseExpr(), e.getAssumptionsRef(), pf);
00600 }
00601 
00602 
00603 // e IFF TRUE ==> e
00604 Theorem CommonTheoremProducer::iffTrueElim(const Theorem& e) {
00605   if(CHECK_PROOFS)
00606     CHECK_SOUND(e.isRewrite() && e.getRHS().isTrue(),
00607     "CommonTheoremProducer::iffTrueElim: "
00608     "theorem is not e<=>TRUE: "+ e.toString());
00609   Proof pf;
00610   if(withProof()) {
00611     pf = newPf("iff_true_elim", e.getLHS(), e.getProof());
00612   }
00613   return newTheorem(e.getLHS(), e.getAssumptionsRef(), pf);
00614 }
00615 
00616 
00617 // e IFF FALSE ==> !e
00618 Theorem CommonTheoremProducer::iffFalseElim(const Theorem& e) {
00619   if(CHECK_PROOFS)
00620     CHECK_SOUND(e.isRewrite() && e.getRHS().isFalse(),
00621     "CommonTheoremProducer::iffFalseElim: "
00622     "theorem is not e<=>FALSE: "+ e.toString());
00623   const Expr& lhs = e.getLHS();
00624   Proof pf;
00625   if(withProof()) {
00626     pf = newPf("iff_false_elim", lhs, e.getProof());
00627   }
00628   return newTheorem(!lhs, e.getAssumptionsRef(), pf);
00629 }
00630 
00631 
00632 // e1 <=> e2  ==>  ~e1 <=> ~e2
00633 Theorem CommonTheoremProducer::iffContrapositive(const Theorem& e) {
00634   if(CHECK_PROOFS)
00635     CHECK_SOUND(e.isRewrite() && e.getRHS().getType().isBool(),
00636     "CommonTheoremProducer::iffContrapositive: "
00637     "theorem is not e1<=>e2: "+ e.toString());
00638   Proof pf;
00639   if(withProof()) {
00640     pf = newPf("iff_contrapositive", e.getExpr(), e.getProof());
00641   }
00642   return newRWTheorem(e.getLHS().negate(),e.getRHS().negate(), e.getAssumptionsRef(), pf);
00643 }
00644 
00645 
00646 // !!e ==> e
00647 Theorem CommonTheoremProducer::notNotElim(const Theorem& not_not_e) {
00648   if(CHECK_PROOFS)
00649     CHECK_SOUND(not_not_e.getExpr().isNot() && not_not_e.getExpr()[0].isNot(),
00650     "CommonTheoremProducer::notNotElim: bad theorem: !!e = "
00651     + not_not_e.toString());
00652   Proof pf;
00653   if(withProof())
00654     pf = newPf("not_not_elim", not_not_e.getExpr(), not_not_e.getProof());
00655   return newTheorem(not_not_e.getExpr()[0][0], not_not_e.getAssumptionsRef(), pf);
00656 }
00657 
00658 
00659 Theorem CommonTheoremProducer::iffMP(const Theorem& e1, const Theorem& e1_iff_e2)
00660 {
00661   if(CHECK_PROOFS) {
00662     CHECK_SOUND(e1_iff_e2.isRewrite(),
00663     "iffMP: not IFF: "+e1_iff_e2.toString());
00664     CHECK_SOUND(e1.getExpr() == (e1_iff_e2.getLHS()),
00665     "iffMP: theorems don't match:\n  e1 = " + e1.toString()
00666     + ", e1_iff_e2 = " + e1_iff_e2.toString());
00667   }
00668   const Expr& e2(e1_iff_e2.getRHS());
00669   // Avoid e1.getExpr(), it may cause unneeded Expr creation
00670   if (e1_iff_e2.getLHS() == e2) return e1;
00671   Proof pf;
00672   Assumptions a(e1, e1_iff_e2);
00673   if(withProof()) {
00674     vector<Proof> pfs;
00675     pfs.push_back(e1.getProof());
00676     pfs.push_back(e1_iff_e2.getProof());
00677     pf = newPf("iff_mp", e1.getExpr(), e2, pfs);
00678   }
00679   return newTheorem(e2, a, pf);
00680 }
00681 
00682 
00683 // e1 AND (e1 IMPLIES e2) ==> e2
00684 Theorem CommonTheoremProducer::implMP(const Theorem& e1,
00685                                       const Theorem& e1_impl_e2) {
00686   const Expr& impl = e1_impl_e2.getExpr();
00687   if(CHECK_PROOFS) {
00688     CHECK_SOUND(impl.isImpl() && impl.arity()==2,
00689     "implMP: not IMPLIES: "+impl.toString());
00690     CHECK_SOUND(e1.getExpr() == impl[0],
00691     "implMP: theorems don't match:\n  e1 = " + e1.toString()
00692     + ", e1_impl_e2 = " + impl.toString());
00693   }
00694   const Expr& e2 = impl[1];
00695   // Avoid e1.getExpr(), it may cause unneeded Expr creation
00696   if (impl[0] == e2) return e1;
00697   Proof pf;
00698   Assumptions a(e1, e1_impl_e2);
00699   if(withProof()) {
00700     vector<Proof> pfs;
00701     pfs.push_back(e1.getProof());
00702     pfs.push_back(e1_impl_e2.getProof());
00703     pf = newPf("impl_mp", e1.getExpr(), e2, pfs);
00704   }
00705   return newTheorem(e2, a, pf);
00706 }
00707 
00708 
00709 // AND(e_0,...e_{n-1}) ==> e_i
00710 Theorem CommonTheoremProducer::andElim(const Theorem& e, int i) {
00711   if(CHECK_PROOFS) {
00712     CHECK_SOUND(e.getExpr().isAnd(), "andElim: not an AND: " + e.toString());
00713     CHECK_SOUND(i < e.getExpr().arity(), "andElim: i = " + int2string(i)
00714     + " >= arity = " + int2string(e.getExpr().arity())
00715     + " in " + e.toString());
00716   }
00717   Proof pf;
00718   if(withProof())
00719     pf = newPf("andE", d_em->newRatExpr(i), e.getExpr(), e.getProof());
00720   return newTheorem(e.getExpr()[i], e.getAssumptionsRef(), pf);
00721 }
00722 
00723 
00724 //! e1, e2 ==> AND(e1, e2)
00725 Theorem CommonTheoremProducer::andIntro(const Theorem& e1, const Theorem& e2) {
00726   vector<Theorem> thms;
00727   thms.push_back(e1);
00728   thms.push_back(e2);
00729   return andIntro(thms);
00730 }
00731 
00732 
00733 Theorem CommonTheoremProducer::andIntro(const vector<Theorem>& es) {
00734   Proof pf;
00735   if(CHECK_PROOFS)
00736     CHECK_SOUND(es.size() > 0,
00737     "andIntro(vector<Theorem>): vector must be non-empty");
00738   Assumptions a(es);
00739   if(withProof()) {
00740     vector<Proof> pfs;
00741     for(vector<Theorem>::const_iterator i=es.begin(), iend=es.end();
00742   i!=iend; ++i)
00743       pfs.push_back(i->getProof());
00744     pf = newPf("andI", pfs);
00745   }
00746   vector<Expr> kids;
00747   for(vector<Theorem>::const_iterator i=es.begin(), iend=es.end();
00748       i!=iend; ++i)
00749     kids.push_back(i->getExpr());
00750   return newTheorem(andExpr(kids), a, pf);
00751 }
00752 
00753 
00754 //  G,a1,...,an |- phi
00755 // -------------------------------------------------
00756 //  G |- (a1 & ... & an) -> phi
00757 Theorem CommonTheoremProducer::implIntro(const Theorem& phi,
00758                                          const std::vector<Expr>& assump) {
00759   bool checkProofs(CHECK_PROOFS);
00760   // This rule only makes sense when runnnig with assumptions
00761   if(checkProofs) {
00762     CHECK_SOUND(withAssumptions(),
00763     "implIntro: called while running without assumptions");
00764   }
00765 
00766   const Assumptions& phiAssump = phi.getAssumptionsRef();
00767 
00768   if(checkProofs) {
00769     for(size_t i=0; i<assump.size(); i++) {
00770       const Theorem& thm = phiAssump[assump[i]];
00771       CHECK_SOUND(!thm.isNull() && thm.isAssump(),
00772       "implIntro: this is not an assumption of phi:\n\n"
00773       "  a["+int2string(i)+"] = "+assump[i].toString()
00774       +"\n\n  phi = "+phi.getExpr().toString());
00775     }
00776   }
00777 
00778   // Proof compaction: trivial derivation
00779   if(assump.size() == 0) return phi;
00780 
00781   Assumptions a(phiAssump - assump);
00782   Proof pf;
00783   if(withProof()) {
00784     vector<Proof> u; // Proof labels for assumptions
00785     for(vector<Expr>::const_iterator i=assump.begin(), iend=assump.end();
00786   i!=iend; ++i) {
00787       const Theorem& t = phiAssump[*i];
00788       u.push_back(t.getProof());
00789     }
00790     // Arguments to the proof rule:
00791     // impl_intro_3(phi, a1,...,an,tcc1,...tccn,pf_tcc1,...pf_tccn,
00792     //              [lambda(a1,...,an): pf_phi])
00793     vector<Expr> args;
00794     vector<Proof> pfs;
00795     args.push_back(phi.getExpr());
00796     args.insert(args.end(), assump.begin(), assump.end());
00797     // Lambda-abstraction of pf_phi
00798     pfs.push_back(newPf(u, assump, phi.getProof()));
00799     pf = newPf("impl_intro", args, pfs);
00800   }
00801   Expr conj(andExpr(assump));
00802   return newTheorem(conj.impExpr(phi.getExpr()), a, pf);
00803 }
00804 
00805 
00806 // e1 => e2  ==>  ~e2 => ~e1
00807 Theorem CommonTheoremProducer::implContrapositive(const Theorem& thm) {
00808   const Expr& impl = thm.getExpr();
00809   if(CHECK_PROOFS) {
00810     CHECK_SOUND(impl.isImpl() && impl.arity()==2,
00811     "CommonTheoremProducer::implContrapositive: thm="
00812     +impl.toString());
00813   }
00814   Proof pf;
00815   if(withProof())
00816     pf = newPf("impl_contrapositive", impl, thm.getProof());
00817   return newTheorem(impl[1].negate().impExpr(impl[0].negate()), thm.getAssumptionsRef(), pf);
00818 }
00819 
00820 
00821 // NOT e ==> e IFF FALSE
00822 Theorem CommonTheoremProducer::notToIff(const Theorem& not_e)
00823 {
00824   if(CHECK_PROOFS)
00825     CHECK_SOUND(not_e.getExpr().isNot(),
00826     "notToIff: not NOT: "+not_e.toString());
00827 
00828   // Make it an atomic rule (more efficient)
00829   Expr e(not_e.getExpr()[0]);
00830   Proof pf;
00831   if(withProof())
00832     pf=newPf("not_to_iff", e, not_e.getProof());
00833   return newRWTheorem(e, d_em->falseExpr(), not_e.getAssumptionsRef(), pf);
00834 }
00835 
00836 
00837 // e1 XOR e2 ==> e1 IFF (NOT e2)
00838 Theorem CommonTheoremProducer::xorToIff(const Expr& e)
00839 {
00840   if(CHECK_PROOFS) {
00841     CHECK_SOUND(e.isXor(), "xorToIff precondition violated");
00842     CHECK_SOUND(e.arity() == 2, "Expected XOR of arity 2");
00843   }
00844   Proof pf;
00845   if(withProof()) {
00846     pf = newPf("xorToIff");
00847   }
00848   return newRWTheorem(e, e[0].iffExpr(!e[1]), Assumptions::emptyAssump(), pf);
00849 }
00850 
00851 
00852 // ==> IFF(e1,e2) IFF <simplified expr>
00853 Theorem CommonTheoremProducer::rewriteIff(const Expr& e) {
00854   Proof pf;
00855   if(CHECK_PROOFS)
00856     CHECK_SOUND(e.isIff(), "rewriteIff precondition violated");
00857   if(withProof()) {
00858     pf = newPf("rewrite_iff", e[0], e[1]);
00859   }
00860 
00861   if(e[0] == e[1]) return rewriteReflexivity(e);
00862 
00863   switch(e[0].getKind()) {
00864   case TRUE_EXPR:
00865     return newRWTheorem(e, e[1], Assumptions::emptyAssump(), pf);
00866   case FALSE_EXPR:
00867     return newRWTheorem(e, !e[1], Assumptions::emptyAssump() ,pf);
00868   case NOT:
00869     if(e[0][0]==e[1]) 
00870       return newRWTheorem(e, d_em->falseExpr(), Assumptions::emptyAssump(), pf);
00871     break;
00872   default: break;
00873   }
00874   
00875   switch(e[1].getKind()) {
00876   case TRUE_EXPR:
00877     return newRWTheorem(e, e[0], Assumptions::emptyAssump(), pf);
00878   case FALSE_EXPR:
00879     return newRWTheorem(e, !e[0], Assumptions::emptyAssump(), pf);
00880   case NOT:
00881     if(e[0]==e[1][0]) 
00882       return newRWTheorem(e, d_em->falseExpr(), Assumptions::emptyAssump(), pf);
00883     break;
00884   default:
00885     break;
00886   }
00887 
00888   if(e[0] < e[1])
00889     return rewriteUsingSymmetry(e);
00890   else
00891     return reflexivityRule(e);
00892 }
00893 
00894 
00895 // ==> AND(e_1,...,e_n) IFF <simplified expr>
00896 // 1) if e_i = FALSE then return FALSE
00897 // 2) if e_i = TRUE, remove it from children
00898 // 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)
00899 // 4) if n=0 return TRUE
00900 // 5) if n=1 return e_1
00901 Theorem CommonTheoremProducer::rewriteAnd(const Expr& e) {
00902   if(CHECK_PROOFS)
00903     CHECK_SOUND(e.isAnd(), "rewriteAnd: bad Expr: " + e.toString());
00904   Proof pf;
00905   ExprMap<bool> newKids;
00906   bool isFalse (false);
00907   for (Expr::iterator k=e.begin(), kend=e.end(); !isFalse && k != kend; ++k) {
00908     const Expr& ek = *k;
00909     if (ek.isFalse()) { isFalse=true; break; }
00910     if (ek.isAnd() && ek.arity() < 10) {
00911       for(Expr::iterator j=ek.begin(), jend=ek.end(); j!=jend; ++j) {
00912   if(newKids.count(j->negate()) > 0) { isFalse=true; break; }
00913   newKids[*j]=true;
00914       }
00915     } else if(!ek.isTrue()) {
00916       if(newKids.count(ek.negate()) > 0) { isFalse=true; break; }
00917       newKids[ek]=true;
00918     }
00919   }
00920   Expr res;
00921   if (isFalse) res = d_em->falseExpr();
00922   else if (newKids.size() == 0) res = d_em->trueExpr(); // All newKids were TRUE
00923   else if (newKids.size() == 1)
00924     res = newKids.begin()->first; // The only child
00925   else {
00926     vector<Expr> v;
00927     for(ExprMap<bool>::iterator i=newKids.begin(), iend=newKids.end();
00928         i!=iend; ++i)
00929       v.push_back(i->first);
00930     res = andExpr(v);
00931   }
00932   if(withProof()) {
00933     pf = newPf("rewrite_and", e,res);
00934   }
00935   return newRWTheorem(e, res, Assumptions::emptyAssump(), pf);
00936 }
00937 
00938 
00939 // ==> OR(e1,e2) IFF <simplified expr>
00940 Theorem CommonTheoremProducer::rewriteOr(const Expr& e) {
00941   if(CHECK_PROOFS)
00942     CHECK_SOUND(e.isOr(), "rewriteOr: bad Expr: " + e.toString());
00943   Proof pf;
00944   ExprMap<bool> newKids;
00945   bool isTrue (false);
00946   for (Expr::iterator k=e.begin(), kend=e.end(); !isTrue && k != kend; ++k) {
00947     const Expr& ek = *k;
00948     if (ek.isTrue()) { isTrue=true; break; }
00949     else if (ek.isOr() && ek.arity() < 10) {
00950       for(Expr::iterator j=ek.begin(), jend=ek.end(); j!=jend; ++j) {
00951   if(newKids.count(j->negate()) > 0) { isTrue=true; break; }
00952   newKids[*j]=true;
00953       }
00954     } else if(!ek.isFalse()) {
00955       if(newKids.count(ek.negate()) > 0) { isTrue=true; break; }
00956       newKids[ek]=true;
00957     }
00958   }
00959   Expr res;
00960   if (isTrue) res = d_em->trueExpr();
00961   else if (newKids.size() == 0) res = d_em->falseExpr(); // All kids were FALSE
00962   else if (newKids.size() == 1) res = newKids.begin()->first; // The only child
00963   else {
00964     vector<Expr> v;
00965     for(ExprMap<bool>::iterator i=newKids.begin(), iend=newKids.end();
00966         i!=iend; ++i)
00967       v.push_back(i->first);
00968     res = orExpr(v);
00969   }
00970   if(withProof()) {
00971     pf = newPf("rewrite_or", e, res);
00972   }
00973   return newRWTheorem(e, res, Assumptions::emptyAssump(), pf);
00974 }
00975 
00976 
00977 // ==> NOT TRUE IFF FALSE
00978 Theorem CommonTheoremProducer::rewriteNotTrue(const Expr& e) {
00979   Proof pf;
00980   if(CHECK_PROOFS)
00981     CHECK_SOUND(e.isNot() && e[0].isTrue(),
00982     "rewriteNotTrue precondition violated");
00983   if(withProof())
00984     pf = newPf("rewrite_not_true");
00985   return newRWTheorem(e, d_em->falseExpr(), Assumptions::emptyAssump(), pf);
00986 }
00987 
00988 
00989 // ==> NOT FALSE IFF TRUE
00990 Theorem CommonTheoremProducer::rewriteNotFalse(const Expr& e) {
00991   Proof pf;
00992   if(CHECK_PROOFS)
00993     CHECK_SOUND(e.isNot() && e[0].isFalse(),
00994     "rewriteNotFalse precondition violated");
00995   if(withProof())
00996     pf = newPf("rewrite_not_false");
00997   return newRWTheorem(e, d_em->trueExpr(), Assumptions::emptyAssump(), pf);
00998 }
00999 
01000 
01001 // ==> (NOT NOT e) IFF e, takes !!e
01002 Theorem CommonTheoremProducer::rewriteNotNot(const Expr& e) {
01003   Proof pf;
01004   if(CHECK_PROOFS)
01005     CHECK_SOUND(e.isNot() && e[0].isNot(),
01006     "rewriteNotNot precondition violated");
01007   if(withProof())
01008     pf = newPf("rewrite_not_not", e[0][0]);
01009   return newRWTheorem(e, e[0][0], Assumptions::emptyAssump(), pf);
01010 }
01011 
01012 
01013 //! ==> NOT FORALL (vars): e  IFF EXISTS (vars) NOT e
01014 Theorem CommonTheoremProducer::rewriteNotForall(const Expr& e) {
01015   if(CHECK_PROOFS) {
01016     CHECK_SOUND(e.isNot() && e[0].isForall(),
01017     "rewriteNotForall: expr must be NOT FORALL:\n"
01018     +e.toString());
01019   }
01020   Proof pf;
01021   if(withProof())
01022     pf = newPf("rewrite_not_forall", e);
01023   return newRWTheorem(e, d_em->newClosureExpr(EXISTS, e[0].getVars(),
01024                                               !e[0].getBody()), Assumptions::emptyAssump(), pf);
01025 }
01026 
01027 
01028 //! ==> NOT EXISTS (vars): e  IFF FORALL (vars) NOT e
01029 Theorem CommonTheoremProducer::rewriteNotExists(const Expr& e) {
01030   if(CHECK_PROOFS) {
01031     CHECK_SOUND(e.isNot() && e[0].isExists(),
01032     "rewriteNotExists: expr must be NOT FORALL:\n"
01033     +e.toString());
01034   }
01035   Proof pf;
01036   if(withProof())
01037     pf = newPf("rewrite_not_exists", e);
01038   return newRWTheorem(e, d_em->newClosureExpr(FORALL, e[0].getVars(),
01039                                               !e[0].getBody()), Assumptions::emptyAssump(), pf);
01040 }
01041 
01042 
01043 Expr CommonTheoremProducer::skolemize(const Expr& e)
01044 {
01045   vector<Expr> vars;
01046   const vector<Expr>& boundVars = e.getVars(); 
01047   for(unsigned int i=0; i<boundVars.size(); i++) {
01048     Expr skolV(e.skolemExpr(i));
01049     Type tp(e.getVars()[i].getType());
01050     skolV.setType(tp);
01051     vars.push_back(skolV);
01052   }
01053   return(e.getBody().substExpr(boundVars, vars));
01054 }
01055 
01056 
01057 Theorem CommonTheoremProducer::skolemizeRewrite(const Expr& e)
01058 {
01059   Proof pf;
01060   if(CHECK_PROOFS) {
01061     CHECK_SOUND(e.isExists(), "skolemize rewrite called on non-existential: "
01062     + e.toString());
01063   }
01064   Expr skol = skolemize(e);
01065   if(withProof()) {
01066     Expr rw(e.iffExpr(skol));
01067     pf = newLabel(rw);
01068   }
01069   TRACE("quantlevel", "skolemize ", skol, "");
01070   return newRWTheorem(e, skol, Assumptions::emptyAssump(), pf);
01071 
01072 }
01073 
01074 
01075 Theorem CommonTheoremProducer::skolemizeRewriteVar(const Expr& e)
01076 {
01077   Proof pf;
01078   if(CHECK_PROOFS) {
01079     CHECK_SOUND(e.isExists(), "skolemizeRewriteVar("
01080     +e.toString()+")");
01081   }
01082 
01083   const vector<Expr>& boundVars = e.getVars();
01084   const Expr& body = e.getBody();
01085 
01086   if(CHECK_PROOFS) {
01087     CHECK_SOUND(boundVars.size()==1, "skolemizeRewriteVar("
01088     +e.toString()+")");
01089     CHECK_SOUND(body.isEq() || body.isIff(), "skolemizeRewriteVar("
01090     +e.toString()+")");
01091     const Expr& v = boundVars[0];
01092     CHECK_SOUND(body[1] == v, "skolemizeRewriteVar("
01093     +e.toString()+")");
01094     CHECK_SOUND(!(v.subExprOf(body[0])), "skolemizeRewriteVar("
01095     +e.toString()+")");
01096   }
01097   // Create the Skolem constant appropriately
01098   Expr skolV(e.skolemExpr(0));
01099   Type tp(e.getVars()[0].getType());
01100   skolV.setType(tp);
01101   // Skolemized expression
01102   Expr skol = Expr(body.getOp(), body[0], skolV);
01103 
01104   if(withProof()) {
01105     Expr rw(e.iffExpr(skol));
01106     pf = newLabel(rw);
01107   }
01108   return newRWTheorem(e, skol, Assumptions::emptyAssump(), pf);
01109 }
01110 
01111 
01112 Theorem CommonTheoremProducer::varIntroRule(const Expr& phi) {
01113   // This rule is sound for all expressions phi
01114   Proof pf;
01115   const Expr boundVar = d_em->newBoundVarExpr(phi.getType());
01116 
01117   Expr body;  
01118   if(phi.getType().isBool())
01119     body = phi.iffExpr(boundVar);
01120   else
01121     body = phi.eqExpr(boundVar);
01122 
01123   std::vector<Expr> v; 
01124   v.push_back(boundVar);
01125   const Expr result = d_em->newClosureExpr(EXISTS, v, body);
01126   
01127   if(withProof()) 
01128     pf = newPf("var_intro", phi, boundVar);
01129   return newTheorem(result, Assumptions::emptyAssump(), pf);
01130 }
01131 
01132 
01133 Theorem CommonTheoremProducer::skolemize(const Theorem& thm) { 
01134   const Expr& e = thm.getExpr();
01135   if(e.isExists()) {
01136     TRACE("skolem", "Skolemizing existential:", "", "{");
01137     CDMap<Expr, Theorem>::iterator i=d_skolemized_thms.find(e),
01138       iend=d_skolemized_thms.end();
01139     if(i!=iend) {
01140       TRACE("skolem", "Skolemized theorem found in map: ", (*i).second, "}");
01141       return iffMP(thm, (*i).second);
01142     }
01143     Theorem skol = skolemizeRewrite(e);
01144     for(unsigned int i=0; i<e.getVars().size(); i++) {
01145       Expr skolV(e.skolemExpr(i));
01146       Type tp(e.getVars()[i].getType());
01147       skolV.setType(tp);
01148     }
01149     d_skolem_axioms.push_back(skol);
01150     d_skolemized_thms.insert(e, skol, 0);//d_coreSatAPI->getBottomScope());
01151     skol = iffMP(thm, skol);
01152     TRACE("skolem", "skolemized new theorem: ", skol, "}");
01153     return skol;
01154   }
01155   return thm;
01156 }
01157 
01158 
01159 Theorem CommonTheoremProducer::varIntroSkolem(const Expr& e) {
01160   // First, look up the cache
01161   CDMap<Expr, Theorem>::iterator i=d_skolemVars.find(e),
01162     iend=d_skolemVars.end();
01163   if(i!=iend) return (*i).second;
01164   // Not in cache; create a new one
01165   Theorem thm = varIntroRule(e);
01166   const Expr& e2 = thm.getExpr();
01167   DebugAssert(e2.isExists() && e2.getVars().size()==1, "varIntroSkolem: e2 = "
01168         +e2.toString());
01169   Theorem skolThm;
01170   // Check if we have a corresponding skolemized version already
01171   CDMap<Expr, Theorem>::iterator j=d_skolemized_thms.find(e2),
01172     jend=d_skolemized_thms.end();
01173   if(j!=jend) {
01174     skolThm = (*i).second;
01175   } else {
01176     skolThm = skolemizeRewriteVar(e2);
01177     d_skolem_axioms.push_back(skolThm);
01178     d_skolemized_thms.insert(e2, skolThm, 0); //d_coreSatAPI->getBottomScope());
01179   }
01180   thm = iffMP(thm, skolThm);
01181   d_skolemVars.insert(e, thm, 0); //d_coreSatAPI->getBottomScope());
01182   return thm;
01183 }
01184 
01185 
01186 // Derived Rules
01187 
01188 
01189 Theorem CommonTheoremProducer::trueTheorem()
01190 {
01191   return iffTrueElim(reflexivityRule(d_em->trueExpr()));
01192 }
01193 
01194 
01195 Theorem CommonTheoremProducer::rewriteAnd(const Theorem& e)
01196 {
01197   return iffMP(e, rewriteAnd(e.getExpr()));
01198 }
01199 
01200 
01201 Theorem CommonTheoremProducer::rewriteOr(const Theorem& e)
01202 {
01203   return iffMP(e, rewriteOr(e.getExpr()));
01204 }
01205 
01206 
01207 Theorem CommonTheoremProducer::ackermann(const Expr& e1, const Expr& e2)
01208 {
01209   Proof pf;
01210   if(CHECK_PROOFS)
01211     CHECK_SOUND(e1.isApply() && e2.isApply() && e1.getOp() == e2.getOp(),
01212     "ackermann precondition violated");
01213   Expr hyp;
01214   int ar = e1.arity();
01215   if (ar == 1) {
01216     hyp = Expr(e1[0].eqExpr(e2[0]));
01217   }
01218   else {
01219     vector<Expr> vec;
01220     for (int i = 0; i != ar; ++i) {
01221       vec.push_back(e1[i].eqExpr(e2[i]));
01222     }
01223     hyp = Expr(AND, vec);
01224   }
01225   if(withProof())
01226     pf = newPf("ackermann", e1, e2);
01227   return newTheorem(hyp.impExpr(e1.eqExpr(e2)), Assumptions::emptyAssump(), pf);
01228 }

Generated on Tue Jul 3 14:33:35 2007 for CVC3 by  doxygen 1.5.1