search_theorem_producer.cpp

Go to the documentation of this file.
00001 /*****************************************************************************/
00002 /*!
00003  * \file search_theorem_producer.cpp
00004  * \brief Implementation of the proof rules for the simple search engine
00005  * 
00006  * Author: Sergey Berezin
00007  * 
00008  * Created: Mon Feb 24 14:51:51 2003
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 #include "search.h"
00023 #include "theory_core.h"
00024 #include "theorem_manager.h"
00025 #include "common_proof_rules.h"
00026 
00027 
00028 #define _CVC3_TRUSTED_
00029 #include "search_theorem_producer.h"
00030 
00031 
00032 using namespace std;
00033 using namespace CVC3;
00034 
00035 
00036 /////////////////////////////////////////////////////////////////////////////
00037 // class SearchEngine trusted methods
00038 /////////////////////////////////////////////////////////////////////////////
00039 
00040 SearchEngineRules*
00041 SearchEngine::createRules() {
00042   return new SearchEngineTheoremProducer(d_core->getTM());
00043 }
00044 
00045 
00046 SearchEngineTheoremProducer::SearchEngineTheoremProducer(TheoremManager* tm)
00047   : TheoremProducer(tm), d_commonRules(tm->getRules())
00048 { }
00049 
00050 
00051 /////////////////////////////////////////////////////////////////////////////
00052 // Proof rules
00053 /////////////////////////////////////////////////////////////////////////////
00054 
00055 // Proof by contradiction: !A |- FALSE ==> |- A.  "!A" doesn't
00056 // have to be present in the assumptions.
00057 Theorem
00058 SearchEngineTheoremProducer::proofByContradiction(const Expr& a,
00059               const Theorem& pfFalse) {
00060   if(CHECK_PROOFS)
00061     CHECK_SOUND(pfFalse.getExpr().isFalse(),
00062     "proofByContradiction: pfFalse = : " + pfFalse.toString());
00063   Expr not_a(!a);
00064   Assumptions assump(pfFalse.getAssumptionsRef() - not_a);
00065   Proof pf;
00066   if(withProof()) {
00067     // TODO: optimize with 1 traversal?
00068     Theorem thm(pfFalse.getAssumptionsRef()[not_a]);
00069     Proof u; // proof label for !a
00070     if(!thm.isNull()) u = thm.getProof();
00071     // Proof compaction: if u is Null, use "FALSE => A" rule
00072     if(u.isNull())
00073       pf = newPf("false_implies_anything", a, pfFalse.getProof());
00074     else
00075       pf = newPf("pf_by_contradiction", a,
00076      // LAMBDA-abstraction (LAMBDA (u: !a): pfFalse)
00077      newPf(u, not_a, pfFalse.getProof()));
00078   }
00079   return newTheorem(a, assump, pf);
00080 }
00081     
00082 // Similar rule, only negation introduction:
00083 // A |- FALSE ==> !A
00084 Theorem
00085 SearchEngineTheoremProducer::negIntro(const Expr& not_a,
00086               const Theorem& pfFalse) {
00087   if(CHECK_PROOFS) {
00088     CHECK_SOUND(pfFalse.getExpr().isFalse(),
00089     "negIntro: pfFalse = : " + pfFalse.toString());
00090     CHECK_SOUND(not_a.isNot(), "negIntro: not_a = "+not_a.toString());
00091   }
00092 
00093   Expr a(not_a[0]);
00094   Assumptions assump(pfFalse.getAssumptionsRef() - a);
00095   Proof pf;
00096   if(withProof()) {
00097     Theorem thm(pfFalse.getAssumptionsRef()[a]);
00098     Proof u; // proof label for 'a'
00099     if(!thm.isNull()) u = thm.getProof();
00100     // Proof compaction: if u is Null, use "FALSE => !A" rule
00101     if(u.isNull())
00102       pf = newPf("false_implies_anything", not_a, pfFalse.getProof());
00103     else
00104       pf = newPf("neg_intro", not_a,
00105      // LAMBDA-abstraction (LAMBDA (u: a): pfFalse)
00106      newPf(u, a, pfFalse.getProof()));
00107   }
00108   return newTheorem(not_a, assump, pf);
00109 }
00110     
00111 
00112 // Case split: u1:A |- C, u2:!A |- C  ==>  |- C
00113 Theorem
00114 SearchEngineTheoremProducer::caseSplit(const Expr& a,
00115                const Theorem& a_proves_c,
00116                const Theorem& not_a_proves_c) {
00117   Expr c(a_proves_c.getExpr());
00118 
00119   if(CHECK_PROOFS) {
00120     CHECK_SOUND(c == not_a_proves_c.getExpr(), 
00121     "caseSplit: conclusions differ:\n  positive case C = "
00122     + c.toString() + "\n  negative case C = "
00123     + not_a_proves_c.getExpr().toString());
00124     // The opposite assumption should not appear in the theorems
00125     // Actually, this doesn't violate soundness, no reason to check
00126 //     CHECK_SOUND(a_proves_c.getAssumptions()[!a].isNull(), 
00127 //    "caseSplit: wrong assumption: " + (!a).toString()
00128 //    +"\n in "+a_proves_c.toString());
00129 //     CHECK_SOUND(not_a_proves_c.getAssumptions()[a].isNull(), 
00130 //    "caseSplit: wrong assumption: " + a.toString()
00131 //    +"\n in "+not_a_proves_c.toString());
00132   }
00133 
00134   const Assumptions& a1(a_proves_c.getAssumptionsRef());
00135   const Assumptions& a2(not_a_proves_c.getAssumptionsRef());
00136   Assumptions a3 = a1 - a;
00137   Assumptions a4 = a2 - !a;
00138 
00139   // Proof compaction: if either theorem proves C without a or !a,
00140   // then just use that theorem.  This only works if assumptions are
00141   // active.
00142 
00143   if (a1 == a3) return a_proves_c;
00144   if (a2 == a4) return not_a_proves_c;
00145 
00146   // No easy way out.  Do the work.
00147   Proof pf;
00148   a3.add(a4);
00149 
00150   if(withProof()) {
00151     // Create lambda-abstractions
00152     vector<Proof> pfs;
00153     pfs.push_back(newPf(a1[a].getProof(), 
00154       a, a_proves_c.getProof()));
00155     pfs.push_back(newPf(a2[!a].getProof(), 
00156       !a, not_a_proves_c.getProof()));
00157     pf = newPf("case_split", a, c, pfs);
00158   }
00159   return newTheorem(c, a3, pf);
00160 }
00161 
00162 // Conflict clause rule: 
00163 // Gamma, A_1,...,A_n |- B ==> Gamma |- (OR B A_1 ... A_n)
00164 // The assumptions A_i are given by the vector 'lits'.
00165 // If B==FALSE, it is omitted from the result.
00166 
00167 // NOTE: here "!A_i" means an inverse of A_i, not just a negation.
00168 // That is, if A_i is NOT C, then !A_i is C.
00169 
00170 // verification function used by conflictClause
00171 void SearchEngineTheoremProducer::verifyConflict(const Theorem& thm, 
00172              TheoremMap& m) {
00173   const Assumptions& a(thm.getAssumptionsRef());
00174   const Assumptions::iterator iend = a.end();
00175   for (Assumptions::iterator i = a.begin(); 
00176        i != iend; ++i) {
00177     CHECK_SOUND(!i->isNull(),
00178     "SearchEngineTheoremProducer::conflictClause: "
00179     "Found null theorem");
00180     if (!i->isRefl() && !i->isFlagged()) {
00181       i->setFlag();
00182       if (m.count(*i) == 0) {
00183   CHECK_SOUND(!i->isAssump(), 
00184         "SearchEngineTheoremProducer::conflictClause: "
00185         "literal and gamma sets do not form a complete "
00186         "cut of Theorem assumptions. Stray theorem: \n"
00187                     +i->toString());
00188   verifyConflict(*i, m);
00189       }
00190       else {
00191   m[*i] = true;
00192       }
00193     }
00194   }
00195 }
00196 
00197 
00198 Theorem
00199 SearchEngineTheoremProducer::
00200 conflictClause(const Theorem& thm, const vector<Theorem>& lits, 
00201          const vector<Theorem>& gamma) {
00202   //  TRACE("search proofs", "conflictClause(", thm.getExpr(), ") {");
00203   IF_DEBUG(if(debugger.trace("search proofs")) {
00204     ostream& os = debugger.getOS();
00205     os << "lits = [";
00206     for(vector<Theorem>::const_iterator i=lits.begin(), iend=lits.end();
00207   i!=iend; ++i)
00208       os << i->getExpr() << ",\n";
00209     os << "]\n\ngamma = [";
00210     for(vector<Theorem>::const_iterator i=gamma.begin(), iend=gamma.end();
00211   i!=iend; ++i)
00212       os << i->getExpr() << ",\n";
00213     os << "]" << endl;
00214   });
00215   bool checkProofs(CHECK_PROOFS);
00216   // This rule only makes sense when runnnig with assumptions
00217   if(checkProofs) {
00218     CHECK_SOUND(withAssumptions(),
00219     "conflictClause: called while running without assumptions");
00220   }
00221 
00222   // Assumptions aOrig(thm.getAssumptions());
00223 
00224   vector<Expr> literals;
00225   vector<Proof> u; // Vector of proof labels
00226   literals.reserve(lits.size() + 1);
00227   u.reserve(lits.size());
00228   const vector<Theorem>::const_iterator iend = lits.end();
00229   for(vector<Theorem>::const_iterator i=lits.begin(); i!=iend; ++i) {
00230     Expr neg(i->getExpr().negate());
00231 
00232     literals.push_back(neg);
00233     if(withProof()) u.push_back(i->getProof());
00234   }
00235 
00236   if(checkProofs) {
00237     TheoremMap m;
00238     //    TRACE_MSG("search proofs", "adding gamma to m: {");
00239     for(vector<Theorem>::const_iterator i = gamma.begin();
00240   i != gamma.end(); ++i) {
00241       //      TRACE("search proofs", "m[", *i, "]");
00242       m[*i] = false;
00243     }
00244     //    TRACE_MSG("search proofs", "}");
00245 
00246     for(vector<Theorem>::const_iterator i = lits.begin(); i!=iend; ++i) {
00247       //      TRACE("search proofs", "check lit: ", *i, "");
00248       CHECK_SOUND(m.count(*i) == 0, 
00249       "SearchEngineTheoremProducer::conflictClause: "
00250       "literal and gamma sets are not disjoint: lit = "
00251       +i->toString());
00252       m[*i] = false;
00253     }
00254     thm.clearAllFlags();
00255     verifyConflict(thm, m);
00256     TheoremMap::iterator t = m.begin(), tend = m.end();
00257     for (; t != tend; ++t) {
00258       CHECK_SOUND(t->second == true,
00259       "SearchEngineTheoremProducer::conflictClause: "
00260       "literal or gamma set contains extra element : "
00261       + t->first.toString());
00262     }
00263   }
00264  
00265   Assumptions a(gamma);
00266 
00267   if(!thm.getExpr().isFalse())
00268     literals.push_back(thm.getExpr());
00269 
00270   Proof pf;
00271   if(withProof()) {
00272     if(lits.size()>0) {
00273       vector<Expr> assump;
00274       // If assumptions are not leaves, we need to create new
00275       // variables for them and substitute them for their proofs in
00276       // the proof term
00277       ExprHashMap<Expr> subst;
00278       DebugAssert(u.size() == lits.size(), "");
00279       for(size_t i=0, iend=lits.size(); i<iend; ++i) {
00280   const Expr& e(lits[i].getExpr());
00281   assump.push_back(e);
00282   Proof& v = u[i];
00283   if(!v.getExpr().isVar()) {
00284     Proof label = newLabel(e);
00285     subst[v.getExpr()] = label.getExpr();
00286     v = label;
00287   }
00288       }
00289       Proof body(thm.getProof());
00290       if(!subst.empty())
00291   body = Proof(body.getExpr().substExpr(subst));
00292       pf = newPf("conflict_clause", newPf(u, assump, body));
00293     }
00294     else
00295       pf = newPf("false_to_empty_or", thm.getProof());
00296   }
00297   Theorem res(newTheorem(Expr(OR, literals, d_em), a, pf));
00298   //  TRACE("search proofs", "conflictClause => ", res.getExpr(), " }");
00299   return res;
00300 }
00301 
00302 
00303 // Theorem
00304 // SearchEngineTheoremProducer::
00305 // conflictClause(const Theorem& thm, const vector<Expr>& lits) {
00306 //   bool checkProofs(CHECK_PROOFS);
00307 //   // This rule only makes sense when runnnig with assumptions
00308 //   if(checkProofs) {
00309 //     CHECK_SOUND(withAssumptions(),
00310 //    "conflictClause: called while running without assumptions");
00311 //   }
00312 
00313 //   Assumptions aOrig(thm.getAssumptions());
00314 
00315 //   vector<Expr> literals;
00316 //   vector<Expr> negations;
00317 //   vector<Proof> u; // Vector of proof labels
00318 //   literals.reserve(lits.size() + 1);
00319 //   negations.reserve(lits.size());
00320 //   u.reserve(lits.size());
00321 //   for(vector<Expr>::const_iterator i=lits.begin(), iend=lits.end();
00322 //       i!=iend; ++i) {
00323 //     Expr neg(i->isNot()? (*i)[0] : !(*i));
00324 //     if(checkProofs)
00325 //       CHECK_SOUND(!aOrig[neg].isNull(), 
00326 //      "SearchEngineTheoremProducer::conflictClause: "
00327 //      "literal is not in the set of assumptions: neg = "
00328 //      +neg.toString() + "\n Theorem = " + thm.toString());
00329 //     literals.push_back(*i);
00330 //     negations.push_back(neg);
00331 //     if(withProof()) u.push_back(aOrig[neg].getProof());
00332 //   }
00333 
00334 //   Assumptions a = aOrig - negations;
00335 
00336 //   if(!thm.getExpr().isFalse())
00337 //     literals.push_back(thm.getExpr());
00338 
00339 //   Proof pf;
00340 //   if(withProof()) {
00341 //     if(lits.size()>0)
00342 //       pf = newPf("conflict_clause", newPf(u, literals, thm.getProof()));
00343 //     else
00344 //       pf = newPf("false_to_empty_or", thm.getProof());
00345 //   }
00346 //  // Use ExprManager in newExpr, since literals may be empty
00347 //   return newTheorem(Expr(d_em, OR, literals), a, pf);
00348 // }
00349 
00350 
00351 // "Cut" rule: { G_i |- A_i };  G', { A_i } |- B ==> union(G_i)+G' |- B.
00352 Theorem
00353 SearchEngineTheoremProducer::
00354 cutRule(const vector<Theorem>& thmsA,
00355   const Theorem& as_prove_b) {
00356   if(CHECK_PROOFS)
00357     CHECK_SOUND(withAssumptions(),
00358     "cutRule called without assumptions activated");
00359   // Optimization: use only those theorems that occur in B's assumptions.
00360   // *** No, take it back, it's a mis-optimization.  Most of the time,
00361   // cutRule is applied when we *know* thmsA are present in the
00362   // assumptions of 'as_proof_b'.
00363 
00364   Proof pf;
00365   vector<Expr> exprs;
00366   exprs.reserve(thmsA.size() + 1);
00367   const vector<Theorem>::const_iterator iend = thmsA.end();
00368   for(vector<Theorem>::const_iterator i=thmsA.begin(); i!=iend; ++i) {
00369     exprs.push_back(i->getExpr());
00370   }
00371 
00372   Assumptions a(thmsA); // add the As
00373   a.add(as_prove_b.getAssumptionsRef() - exprs); // Add G'
00374   
00375   if(withProof()) {
00376     vector<Proof> pfs;
00377     pfs.reserve(thmsA.size() + 1);
00378     for(vector<Theorem>::const_iterator i = thmsA.begin(); i != iend; ++i) {
00379       pfs.push_back(i->getProof());
00380     }
00381     exprs.push_back(as_prove_b.getExpr());
00382     pfs.push_back(as_prove_b.getProof());
00383     pf = newPf("cut_rule",exprs,pfs);
00384   }
00385   return newTheorem(as_prove_b.getExpr(), a, pf);
00386 }
00387 
00388 
00389 void 
00390 SearchEngineTheoremProducer::checkSoundNoSkolems(const Expr& e, 
00391              ExprMap<bool>& visited, 
00392              const ExprMap<bool>& skolems)
00393 {
00394   if(visited.count(e)>0)
00395     return;
00396   else
00397     visited[e] = true;
00398   CHECK_SOUND(skolems.count(e) == 0, 
00399         "skolem constant found in axioms of false theorem: "
00400         + e.toString());
00401   for(Expr::iterator it = e.begin(), end = e.end(); it!= end; ++it)
00402     checkSoundNoSkolems(*it, visited, skolems);
00403   if(e.getKind() == FORALL || e.getKind() == EXISTS)
00404     checkSoundNoSkolems(e.getBody(), visited, skolems);       
00405 }
00406 
00407 void 
00408 SearchEngineTheoremProducer::checkSoundNoSkolems(const Theorem& t, 
00409              ExprMap<bool>& visited, 
00410              const ExprMap<bool>& skolems)
00411 {
00412   if(t.isRefl() || t.isFlagged())
00413     return;
00414   t.setFlag();
00415   if(t.isAssump())
00416     checkSoundNoSkolems(t.getExpr(), visited, skolems);
00417   else
00418   {
00419     const Assumptions& a(t.getAssumptionsRef());
00420     Assumptions::iterator it = a.begin(), end = a.end();
00421     for(; it!=end; ++it)
00422       checkSoundNoSkolems(*it, visited, skolems);
00423    }
00424 }
00425 
00426 /*! Eliminate skolem axioms: 
00427  * Gamma, Delta |- false => Gamma|- false 
00428  * where Delta is a set of skolem axioms {|-Exists(x) phi (x) => phi(c)}
00429  * and gamma does not contain any of the skolem constants c.
00430  */
00431 
00432 Theorem 
00433 SearchEngineTheoremProducer::eliminateSkolemAxioms(const Theorem& tFalse, 
00434               const std::vector<Theorem>& delta)
00435 {
00436   TRACE("skolem", "=>eliminateSkolemAxioms ", delta.size(), "{");
00437   if(delta.empty())
00438   {
00439     TRACE("skolem",  "eliminateSkolemAxioms","" , "}");
00440     return tFalse;
00441   }
00442   const Expr& falseExpr = tFalse.getExpr();
00443   if(CHECK_PROOFS) {
00444     CHECK_SOUND(falseExpr.isFalse(),
00445     "eliminateSkolemAxiom called on non-false theorem");
00446     ExprMap<bool> visited;
00447     ExprMap<bool> skolems;
00448     vector<Theorem>::const_iterator it = delta.begin(), end = delta.end();
00449     for(; it!=end; ++it) {
00450       CHECK_SOUND(it->isRewrite(),
00451       "eliminateSkolemAxioms(): Skolem axiom is not "
00452       "an IFF: "+it->toString());
00453       const Expr& ex = it->getLHS();
00454       CHECK_SOUND(ex.isExists(), 
00455       "Did not receive skolem axioms in Delta"
00456       " of eliminateSkolemAxioms" + it->toString());
00457       // Collect the Skolem constants for further soundness checks
00458       for(unsigned int j=0; j<ex.getVars().size(); j++) {
00459   Expr sk_var(ex.skolemExpr(j));
00460   if(sk_var.getType().isBool()) {
00461           sk_var = d_em->newLeafExpr(sk_var.mkOp());
00462   }
00463   skolems[sk_var] = true;
00464   TRACE("skolem", ">> Eliminating variable: ", sk_var, "<<");
00465       }
00466     }
00467     tFalse.clearAllFlags();
00468     checkSoundNoSkolems(tFalse, visited, skolems);
00469   }
00470   Proof pf;
00471   if(!withProof()) return tFalse;
00472   else 
00473     {
00474       Proof origFalse = tFalse.getProof();
00475       std::vector<Proof>skolemizeLabels;
00476       std::vector<Expr> exprs;
00477       for(unsigned int i=0; i<delta.size(); i++)
00478   {
00479     exprs.push_back(delta[i].getExpr());
00480     skolemizeLabels.push_back(delta[i].getProof());
00481   }
00482       pf = newPf(skolemizeLabels, exprs, origFalse);
00483     }
00484   TRACE("skolem",  "eliminateSkolemAxioms","" , "}");
00485   return newTheorem(tFalse.getExpr(), tFalse.getAssumptionsRef(), pf);
00486 }
00487 
00488 
00489 Theorem
00490 SearchEngineTheoremProducer::unitProp(const std::vector<Theorem>& thms,
00491               const Theorem& clause,
00492               unsigned i) {
00493   Expr e(clause.getExpr());
00494   if(CHECK_PROOFS) {
00495     // Soundness check: first, check the form of the 'clause' theorem
00496     CHECK_SOUND(e.isOr() && e.arity() > (int)i,
00497     "SearchEngineTheoremProducer::unitProp: bad theorem or i="
00498     +int2string(i)+" > arity="+int2string(e.arity())
00499     +" in clause = " + clause.toString());
00500     // Now, check correspondence of thms to the disjunction
00501     CHECK_SOUND(((int)thms.size()) == e.arity() - 1,
00502     "SearchEngineTheoremProducer::unitProp: "
00503     "wrong number of theorems"
00504     "\n  thms.size = " + int2string(thms.size())
00505     +"\n  clause.arity = " + int2string(e.arity()));
00506 
00507     for(unsigned j=0,k=0; j<thms.size(); j++) {
00508       if(j!=i) {
00509   Expr ej(e[j]), ek(thms[k].getExpr());
00510   CHECK_SOUND((ej.isNot() && ej[0] == ek) || (ek.isNot() && ej == ek[0]),
00511         "SearchEngineTheoremProducer::unitProp: "
00512         "wrong theorem["+int2string(k)+"]"
00513         "\n  thm = " + thms[k].toString() +
00514         "\n  literal = " + e[j].toString() +
00515         "\n  clause = " + clause.toString());
00516   k++;
00517       }
00518     }
00519   }
00520 
00521   Assumptions a(thms);
00522   a.add(clause);
00523   Proof pf;
00524 
00525   if(withProof()) {
00526     vector<Proof> pfs;
00527     vector<Expr> exprs;
00528     exprs.reserve(thms.size() + 1);
00529     pfs.reserve(thms.size()+1);
00530     const vector<Theorem>::const_iterator iend = thms.end();
00531     for(vector<Theorem>::const_iterator i=thms.begin(); i!=iend; ++i) {
00532       exprs.push_back(i->getExpr());
00533       pfs.push_back(i->getProof());
00534     }
00535     exprs.push_back(clause.getExpr());
00536     pfs.push_back(clause.getProof());
00537     pf = newPf("unit_prop", exprs, pfs);
00538   }
00539   return newTheorem(e[i], a, pf);
00540 }
00541 
00542 Theorem
00543 SearchEngineTheoremProducer::propAndrAF(const Theorem& andr_th,
00544           bool left,
00545           const Theorem& b_th) {
00546   const Expr& andr_e(andr_th.getExpr());
00547   if(CHECK_PROOFS) {
00548     CHECK_SOUND(andr_e.getKind() == AND_R &&
00549     ((left && b_th.refutes(andr_e[1])) ||
00550      (!left && b_th.refutes(andr_e[2]))),
00551     "SearchEngineTheoremProducer::propAndrAF");
00552   }
00553 
00554   Assumptions a(andr_th, b_th);
00555   Proof pf;
00556 
00557   if(withProof()) {
00558     vector<Proof> pfs;
00559     vector<Expr> exprs;
00560     exprs.push_back(andr_th.getExpr());
00561     exprs.push_back(b_th.getExpr());
00562     pfs.push_back(andr_th.getProof());
00563     pfs.push_back(b_th.getProof());
00564     // can we note which branch to take?
00565     pf = newPf("prop_andr_af", exprs, pfs);
00566   }
00567 
00568   return newTheorem(andr_e[0].negate(), a, pf);
00569 }
00570 
00571 Theorem
00572 SearchEngineTheoremProducer::propAndrAT(const Theorem& andr_th,
00573           const Theorem& l_th,
00574           const Theorem& r_th) {
00575   const Expr& andr_e(andr_th.getExpr());
00576   if(CHECK_PROOFS) {
00577     CHECK_SOUND(andr_e.getKind() == AND_R &&
00578     l_th.proves(andr_e[1]) && r_th.proves(andr_e[2]),
00579     "SearchEngineTheoremProducer::propAndrAT");
00580   }
00581 
00582   Assumptions a(andr_th, l_th);
00583   a.add(r_th);
00584   Proof pf;
00585 
00586   if(withProof()) {
00587     vector<Proof> pfs;
00588     vector<Expr> exprs;
00589     exprs.push_back(andr_th.getExpr());
00590     exprs.push_back(l_th.getExpr());
00591     exprs.push_back(r_th.getExpr());
00592     pfs.push_back(andr_th.getProof());
00593     pfs.push_back(l_th.getProof());
00594     pfs.push_back(r_th.getProof());
00595     pf = newPf("prop_andr_at", exprs, pfs);
00596   }
00597 
00598   return newTheorem(andr_e[0], a, pf);
00599 }
00600 
00601 void
00602 SearchEngineTheoremProducer::propAndrLRT(const Theorem& andr_th,
00603            const Theorem& a_th,
00604            Theorem* l_th,
00605            Theorem* r_th) {
00606   const Expr& andr_e(andr_th.getExpr());
00607   if(CHECK_PROOFS) {
00608     CHECK_SOUND(andr_e.getKind() == AND_R && a_th.proves(andr_e[0]),
00609     "SearchEngineTheoremProducer::propAndrLRT");
00610   }
00611 
00612   Assumptions a(andr_th, a_th);
00613   Proof pf;
00614 
00615   if(withProof()) {
00616     vector<Proof> pfs;
00617     vector<Expr> exprs;
00618     exprs.push_back(andr_th.getExpr());
00619     exprs.push_back(a_th.getExpr());
00620     pfs.push_back(andr_th.getProof());
00621     pfs.push_back(a_th.getProof());
00622     pf = newPf("prop_andr_lrt", exprs, pfs);
00623   }
00624 
00625   if (l_th) *l_th = newTheorem(andr_e[1], a, pf);
00626   if (r_th) *r_th = newTheorem(andr_e[2], a, pf);
00627 }
00628 
00629 Theorem
00630 SearchEngineTheoremProducer::propAndrLF(const Theorem& andr_th,
00631           const Theorem& a_th,
00632           const Theorem& r_th) {
00633   const Expr& andr_e(andr_th.getExpr());
00634   if(CHECK_PROOFS) {
00635     CHECK_SOUND(andr_e.getKind() == AND_R &&
00636     a_th.refutes(andr_e[0]) && r_th.proves(andr_e[2]),
00637     "SearchEngineTheoremProducer::propAndrLF");
00638   }
00639 
00640   Assumptions a(andr_th, a_th);
00641   a.add(r_th);
00642   Proof pf;
00643 
00644   if(withProof()) {
00645     vector<Proof> pfs;
00646     vector<Expr> exprs;
00647     exprs.push_back(andr_th.getExpr());
00648     exprs.push_back(a_th.getExpr());
00649     exprs.push_back(r_th.getExpr());
00650     pfs.push_back(andr_th.getProof());
00651     pfs.push_back(a_th.getProof());
00652     pfs.push_back(r_th.getProof());
00653     pf = newPf("prop_andr_lf", exprs, pfs);
00654   }
00655 
00656   return newTheorem(andr_e[1].negate(), a, pf);
00657 }
00658 
00659 Theorem
00660 SearchEngineTheoremProducer::propAndrRF(const Theorem& andr_th,
00661           const Theorem& a_th,
00662           const Theorem& l_th) {
00663   const Expr& andr_e(andr_th.getExpr());
00664   if(CHECK_PROOFS) {
00665     CHECK_SOUND(andr_e.getKind() == AND_R &&
00666     a_th.refutes(andr_e[0]) && l_th.proves(andr_e[1]),
00667     "SearchEngineTheoremProducer::propAndrRF");
00668   }
00669 
00670   Assumptions a(andr_th, a_th);
00671   a.add(l_th);
00672   Proof pf;
00673 
00674   if(withProof()) {
00675     vector<Proof> pfs;
00676     vector<Expr> exprs;
00677     exprs.push_back(andr_th.getExpr());
00678     exprs.push_back(a_th.getExpr());
00679     exprs.push_back(l_th.getExpr());
00680     pfs.push_back(andr_th.getProof());
00681     pfs.push_back(a_th.getProof());
00682     pfs.push_back(l_th.getProof());
00683     pf = newPf("prop_andr_rf", exprs, pfs);
00684   }
00685 
00686   return newTheorem(andr_e[2].negate(), a, pf);
00687 }
00688 
00689 Theorem
00690 SearchEngineTheoremProducer::confAndrAT(const Theorem& andr_th,
00691           const Theorem& a_th,
00692           bool left,
00693           const Theorem& b_th) {
00694   const Expr& andr_e(andr_th.getExpr());
00695   if(CHECK_PROOFS) {
00696     CHECK_SOUND(andr_e.getKind() == AND_R && a_th.proves(andr_e[0]) &&
00697     ((left && b_th.refutes(andr_e[1])) ||
00698      (!left && b_th.refutes(andr_e[2]))),
00699     "SearchEngineTheoremProducer::confAndrAT");
00700   }
00701 
00702   Assumptions a(andr_th, a_th);
00703   a.add(b_th);
00704   Proof pf;
00705 
00706   if(withProof()) {
00707     vector<Proof> pfs;
00708     vector<Expr> exprs;
00709     exprs.push_back(andr_th.getExpr());
00710     exprs.push_back(a_th.getExpr());
00711     exprs.push_back(b_th.getExpr());
00712     pfs.push_back(andr_th.getProof());
00713     pfs.push_back(a_th.getProof());
00714     pfs.push_back(b_th.getProof());
00715     // can we note which branch to take?
00716     pf = newPf("conf_andr_at", exprs, pfs);
00717   }
00718 
00719   return newTheorem(d_em->falseExpr(), a, pf);
00720 }
00721 
00722 Theorem
00723 SearchEngineTheoremProducer::confAndrAF(const Theorem& andr_th,
00724           const Theorem& a_th,
00725           const Theorem& l_th,
00726           const Theorem& r_th) {
00727   const Expr& andr_e(andr_th.getExpr());
00728   if(CHECK_PROOFS) {
00729     CHECK_SOUND(andr_e.getKind() == AND_R && a_th.refutes(andr_e[0]) &&
00730     l_th.proves(andr_e[1]) && r_th.proves(andr_e[2]),
00731     "SearchEngineTheoremProducer::confAndrAF");
00732   }
00733 
00734   Assumptions a;
00735   Proof pf;
00736   if(withAssumptions()) {
00737     a.add(andr_th);
00738     a.add(a_th);
00739     a.add(l_th);
00740     a.add(r_th);
00741   }
00742 
00743   if(withProof()) {
00744     vector<Proof> pfs;
00745     vector<Expr> exprs;
00746     exprs.push_back(andr_th.getExpr());
00747     exprs.push_back(a_th.getExpr());
00748     exprs.push_back(l_th.getExpr());
00749     exprs.push_back(r_th.getExpr());
00750     pfs.push_back(andr_th.getProof());
00751     pfs.push_back(a_th.getProof());
00752     pfs.push_back(l_th.getProof());
00753     pfs.push_back(r_th.getProof());
00754     pf = newPf("conf_andr_af", exprs, pfs);
00755   }
00756 
00757   return newTheorem(d_em->falseExpr(), a, pf);
00758 }
00759 
00760 Theorem
00761 SearchEngineTheoremProducer::propIffr(const Theorem& iffr_th,
00762               int p,
00763               const Theorem& a_th,
00764               const Theorem& b_th)
00765 {
00766   int a(-1), b(-1);
00767   if(CHECK_PROOFS)
00768     CHECK_SOUND(p == 0 || p == 1 || p == 2,
00769     "SearchEngineTheoremProducer::propIffr: p="
00770     +int2string(p));
00771   switch (p) {
00772   case 0: a = 1; b = 2; break;
00773   case 1: a = 0; b = 2; break;
00774   case 2: a = 0; b = 1; break;
00775   }
00776 
00777   const Expr& iffr_e(iffr_th.getExpr());
00778 
00779   bool v0 = a_th.proves(iffr_e[a]);
00780   bool v1 = b_th.proves(iffr_e[b]);
00781 
00782   if (CHECK_PROOFS) {
00783     CHECK_SOUND(iffr_e.getKind() == IFF_R &&
00784     (v0 || a_th.refutes(iffr_e[a])) &&
00785     (v1 || b_th.refutes(iffr_e[b])),
00786     "SearchEngineTheoremProducer::propIffr");
00787   }
00788 
00789   Assumptions aa;
00790   Proof pf;
00791   if (withAssumptions()) {
00792     aa.add(iffr_th);
00793     aa.add(a_th);
00794     aa.add(b_th);
00795   }
00796 
00797   if (withProof()) {
00798     vector<Proof> pfs;
00799     vector<Expr> exprs;
00800     exprs.push_back(iffr_th.getExpr());
00801     exprs.push_back(a_th.getExpr());
00802     exprs.push_back(b_th.getExpr());
00803     pfs.push_back(iffr_th.getProof());
00804     pfs.push_back(a_th.getProof());
00805     pfs.push_back(b_th.getProof());
00806     pf = newPf("prop_iffr", exprs, pfs);
00807   }
00808 
00809   return newTheorem(v0 == v1 ? iffr_e[p] : iffr_e[p].negate(), aa, pf);
00810 }
00811 
00812 Theorem
00813 SearchEngineTheoremProducer::confIffr(const Theorem& iffr_th,
00814               const Theorem& i_th,
00815               const Theorem& l_th,
00816               const Theorem& r_th)
00817 {
00818   const Expr& iffr_e(iffr_th.getExpr());
00819 
00820   bool v0 = i_th.proves(iffr_e[0]);
00821   bool v1 = l_th.proves(iffr_e[1]);
00822   bool v2 = r_th.proves(iffr_e[2]);
00823 
00824   if (CHECK_PROOFS) {
00825     CHECK_SOUND(iffr_e.getKind() == IFF_R &&
00826     (v0 || i_th.refutes(iffr_e[0])) &&
00827     (v1 || l_th.refutes(iffr_e[1])) &&
00828     (v2 || r_th.refutes(iffr_e[2])) &&
00829     ((v0 && v1 != v2) || (!v0 && v1 == v2)),
00830     "SearchEngineTheoremProducer::confIffr");
00831   }
00832 
00833   Assumptions a;
00834   Proof pf;
00835   if (withAssumptions()) {
00836     a.add(iffr_th);
00837     a.add(i_th);
00838     a.add(l_th);
00839     a.add(r_th);
00840   }
00841 
00842   if (withProof()) {
00843     vector<Proof> pfs;
00844     vector<Expr> exprs;
00845     exprs.push_back(iffr_th.getExpr());
00846     exprs.push_back(i_th.getExpr());
00847     exprs.push_back(l_th.getExpr());
00848     exprs.push_back(r_th.getExpr());
00849     pfs.push_back(iffr_th.getProof());
00850     pfs.push_back(i_th.getProof());
00851     pfs.push_back(l_th.getProof());
00852     pfs.push_back(r_th.getProof());
00853     pf = newPf("conf_iffr", exprs, pfs);
00854   }
00855 
00856   return newTheorem(d_em->falseExpr(), a, pf);
00857 }
00858 
00859 Theorem
00860 SearchEngineTheoremProducer::propIterIte(const Theorem& iter_th,
00861            bool left,
00862            const Theorem& if_th,
00863            const Theorem& then_th)
00864 {
00865   const Expr& iter_e(iter_th.getExpr());
00866 
00867   bool v0 = if_th.proves(iter_e[1]);
00868   bool v1 = then_th.proves(iter_e[left ? 2 : 3]);
00869 
00870   if (CHECK_PROOFS) {
00871     CHECK_SOUND(iter_e.getKind() == ITE_R &&
00872     (v0 || if_th.refutes(iter_e[1])) &&
00873     (v1 || then_th.refutes(iter_e[left ? 2 : 3])) &&
00874     v0 == left,
00875     "SearchEngineTheoremProducer::propIterIte");
00876   }
00877 
00878   Assumptions a;
00879   Proof pf;
00880   if (withAssumptions()) {
00881     a.add(iter_th);
00882     a.add(if_th);
00883     a.add(then_th);
00884   }
00885 
00886   if (withProof()) {
00887     vector<Proof> pfs;
00888     vector<Expr> exprs;
00889     exprs.push_back(iter_th.getExpr());
00890     exprs.push_back(if_th.getExpr());
00891     exprs.push_back(then_th.getExpr());
00892     pfs.push_back(iter_th.getProof());
00893     pfs.push_back(if_th.getProof());
00894     pfs.push_back(then_th.getProof());
00895     pf = newPf("prop_iter_ite", exprs, pfs);
00896   }
00897 
00898   return newTheorem(v1 ? iter_e[0] : iter_e[0].negate(), a, pf);
00899 }
00900 
00901 void
00902 SearchEngineTheoremProducer::propIterIfThen(const Theorem& iter_th,
00903               bool left,
00904               const Theorem& ite_th,
00905               const Theorem& then_th,
00906               Theorem* if_th,
00907               Theorem* else_th)
00908 {
00909   const Expr& iter_e(iter_th.getExpr());
00910 
00911   bool v0 = ite_th.proves(iter_e[0]);
00912   bool v1 = then_th.proves(iter_e[left ? 2 : 3]);
00913 
00914   if (CHECK_PROOFS) {
00915     CHECK_SOUND(iter_e.getKind() == ITE_R &&
00916     (v0 || ite_th.refutes(iter_e[0])) &&
00917     (v1 || then_th.refutes(iter_e[left ? 2 : 3])) &&
00918     v0 != v1,
00919     "SearchEngineTheoremProducer::propIterIfThen");
00920   }
00921 
00922   Assumptions a;
00923   Proof pf;
00924   if (withAssumptions()) {
00925     a.add(iter_th);
00926     a.add(ite_th);
00927     a.add(then_th);
00928   }
00929 
00930   if (withProof()) {
00931     vector<Proof> pfs;
00932     vector<Expr> exprs;
00933     exprs.push_back(iter_th.getExpr());
00934     exprs.push_back(ite_th.getExpr());
00935     exprs.push_back(then_th.getExpr());
00936     pfs.push_back(iter_th.getProof());
00937     pfs.push_back(ite_th.getProof());
00938     pfs.push_back(then_th.getExpr());
00939     pf = newPf("prop_iter_if_then", exprs, pfs);
00940   }
00941 
00942   if (if_th)
00943     *if_th = newTheorem(left ? iter_e[1].negate() : iter_e[1], a, pf);
00944   if (else_th)
00945     *else_th = newTheorem(v0 ? iter_e[left ? 3 : 2] : iter_e[left ? 3 : 2].negate(), a, pf);
00946 }
00947 
00948 Theorem
00949 SearchEngineTheoremProducer::propIterThen(const Theorem& iter_th,
00950             const Theorem& ite_th,
00951             const Theorem& if_th)
00952 {
00953   const Expr& iter_e(iter_th.getExpr());
00954 
00955   bool v0 = ite_th.proves(iter_e[0]);
00956   bool v1 = if_th.proves(iter_e[1]);
00957 
00958   if (CHECK_PROOFS) {
00959     CHECK_SOUND(iter_e.getKind() == ITE_R &&
00960     (v0 || ite_th.refutes(iter_e[0])) &&
00961     (v1 || if_th.refutes(iter_e[1])),
00962     "SearchEngineTheoremProducer::propIterThen");
00963   }
00964 
00965   Assumptions a;
00966   Proof pf;
00967   if (withAssumptions()) {
00968     a.add(iter_th);
00969     a.add(ite_th);
00970     a.add(if_th);
00971   }
00972 
00973   if (withProof()) {
00974     vector<Proof> pfs;
00975     vector<Expr> exprs;
00976     exprs.push_back(iter_th.getExpr());
00977     exprs.push_back(ite_th.getExpr());
00978     exprs.push_back(if_th.getExpr());
00979     pfs.push_back(iter_th.getProof());
00980     pfs.push_back(ite_th.getProof());
00981     pfs.push_back(if_th.getExpr());
00982     pf = newPf("prop_iter_then", exprs, pfs);
00983   }
00984 
00985   return newTheorem(v1 ?
00986         (v0 ? iter_e[2] : iter_e[2].negate()) :
00987         (v0 ? iter_e[3] : iter_e[3].negate()), a, pf);
00988 }
00989 
00990 Theorem
00991 SearchEngineTheoremProducer::confIterThenElse(const Theorem& iter_th,
00992                 const Theorem& ite_th,
00993                 const Theorem& then_th,
00994                 const Theorem& else_th)
00995 {
00996   const Expr& iter_e(iter_th.getExpr());
00997 
00998   bool v0 = ite_th.proves(iter_e[0]);
00999   bool v1 = then_th.proves(iter_e[2]);
01000   bool v2 = else_th.proves(iter_e[3]);
01001 
01002   if (CHECK_PROOFS) {
01003     CHECK_SOUND(iter_e.getKind() == ITE_R &&
01004     (v0 || ite_th.refutes(iter_e[0])) &&
01005     (v1 || then_th.refutes(iter_e[2])) &&
01006     (v2 || else_th.refutes(iter_e[3])) &&
01007     ((v0 && !v1 && !v2) || (!v0 && v1 && v2)),
01008     "SearchEngineTheoremProducer::confIterThenElse");
01009   }
01010 
01011   Assumptions a;
01012   Proof pf;
01013   if (withAssumptions()) {
01014     a.add(iter_th);
01015     a.add(ite_th);
01016     a.add(then_th);
01017     a.add(else_th);
01018   }
01019 
01020   if (withProof()) {
01021     vector<Proof> pfs;
01022     vector<Expr> exprs;
01023     exprs.push_back(iter_th.getExpr());
01024     exprs.push_back(ite_th.getExpr());
01025     exprs.push_back(then_th.getExpr());
01026     exprs.push_back(else_th.getExpr());
01027     pfs.push_back(iter_th.getProof());
01028     pfs.push_back(ite_th.getProof());
01029     pfs.push_back(then_th.getExpr());
01030     pfs.push_back(else_th.getExpr());
01031     pf = newPf("conf_iter_then_else", exprs, pfs);
01032   }
01033 
01034   return newTheorem(d_em->falseExpr(), a, pf);
01035 }
01036 
01037 Theorem
01038 SearchEngineTheoremProducer::confIterIfThen(const Theorem& iter_th,
01039               bool left,
01040               const Theorem& ite_th,
01041               const Theorem& if_th,
01042               const Theorem& then_th)
01043 {
01044   const Expr& iter_e(iter_th.getExpr());
01045 
01046   bool v0 = ite_th.proves(iter_e[0]);
01047   bool v1 = if_th.proves(iter_e[1]);
01048   bool v2 = then_th.proves(iter_e[left ? 2 : 3]);
01049 
01050   if (CHECK_PROOFS) {
01051     CHECK_SOUND(iter_e.getKind() == ITE_R &&
01052     (v0 || ite_th.refutes(iter_e[0])) &&
01053     (v1 || if_th.refutes(iter_e[1])) &&
01054     (v2 || then_th.refutes(iter_e[left ? 2 : 3])) &&
01055     v1 == left && v0 != v2,
01056     "SearchEngineTheoremProducer::confIterThenElse");
01057   }
01058 
01059   Assumptions a;
01060   Proof pf;
01061   if (withAssumptions()) {
01062     a.add(iter_th);
01063     a.add(ite_th);
01064     a.add(if_th);
01065     a.add(then_th);
01066   }
01067 
01068   if (withProof()) {
01069     vector<Proof> pfs;
01070     vector<Expr> exprs;
01071     exprs.push_back(iter_th.getExpr());
01072     exprs.push_back(ite_th.getExpr());
01073     exprs.push_back(if_th.getExpr());
01074     exprs.push_back(then_th.getExpr());
01075     pfs.push_back(iter_th.getProof());
01076     pfs.push_back(ite_th.getProof());
01077     pfs.push_back(if_th.getExpr());
01078     pfs.push_back(then_th.getExpr());
01079     pf = newPf("conf_iter_then_else", exprs, pfs);
01080   }
01081 
01082   return newTheorem(d_em->falseExpr(), a, pf);
01083 }
01084 
01085 // "Conflict" rule (all literals in a clause become FALSE)
01086 // { G_j |- !l_j, j in [1..n] } , G |- (OR l_1 ... l_n) ==> FALSE
01087 Theorem
01088 SearchEngineTheoremProducer::conflictRule(const std::vector<Theorem>& thms,
01089             const Theorem& clause) {
01090   Expr e(clause.getExpr());
01091   if(CHECK_PROOFS) {
01092     // Soundness check: first, check the form of the 'clause' theorem
01093     CHECK_SOUND(e.isOr(),
01094     "SearchEngineTheoremProducer::unitProp: "
01095     "bad theorem in clause = "+clause.toString());
01096     // Now, check correspondence of thms to the disjunction
01097     CHECK_SOUND(((int)thms.size()) == e.arity(),
01098     "SearchEngineTheoremProducer::conflictRule: "
01099     "wrong number of theorems"
01100     "\n  thms.size = " + int2string(thms.size())
01101     +"\n  clause.arity = " + int2string(e.arity()));
01102 
01103     for(unsigned j=0; j<thms.size(); j++) {
01104       Expr ej(e[j]), ek(thms[j].getExpr());
01105       CHECK_SOUND((ej.isNot() && ej[0] == ek) || (ek.isNot() && ej == ek[0]),
01106       "SearchEngineTheoremProducer::conflictRule: "
01107       "wrong theorem["+int2string(j)+"]"
01108       "\n  thm = " + thms[j].toString() +
01109       "\n  literal = " + e[j].toString() +
01110       "\n  clause = " + clause.toString());
01111     }
01112   }
01113 
01114   Assumptions a(thms);
01115   a.add(clause);
01116   Proof pf;
01117   if(withProof()) {
01118     vector<Proof> pfs;
01119     vector<Expr> exprs;
01120     exprs.reserve(thms.size() + 1);
01121     pfs.reserve(thms.size()+1);
01122     const vector<Theorem>::const_iterator iend = thms.end();
01123     for(vector<Theorem>::const_iterator i=thms.begin(); i!=iend; ++i) {
01124       exprs.push_back(i->getExpr());
01125       pfs.push_back(i->getProof());
01126     }
01127     exprs.push_back(clause.getExpr());
01128     pfs.push_back(clause.getProof());
01129     pf = newPf("conflict", exprs, pfs);
01130   }
01131   return newTheorem(d_em->falseExpr(), a, pf);
01132 }
01133 
01134 
01135 ///////////////////////////////////////////////////////////////////////
01136 //// Conjunctive Normal Form (CNF) proof rules
01137 ///////////////////////////////////////////////////////////////////////
01138 Theorem
01139 SearchEngineTheoremProducer::andCNFRule(const Theorem& thm) {
01140   return opCNFRule(thm, AND, "and_cnf_rule");
01141 }
01142 
01143 Theorem
01144 SearchEngineTheoremProducer::orCNFRule(const Theorem& thm) {
01145   return opCNFRule(thm, OR, "or_cnf_rule");
01146 }
01147 
01148 Theorem
01149 SearchEngineTheoremProducer::impCNFRule(const Theorem& thm) {
01150   return opCNFRule(thm, IMPLIES, "implies_cnf_rule");
01151 }
01152 
01153 Theorem
01154 SearchEngineTheoremProducer::iffCNFRule(const Theorem& thm) {
01155   return opCNFRule(thm, IFF, "iff_cnf_rule");
01156 }
01157 
01158 Theorem
01159 SearchEngineTheoremProducer::iteCNFRule(const Theorem& thm) {
01160   return opCNFRule(thm, ITE, "ite_cnf_rule");
01161 }
01162 
01163 
01164 Theorem
01165 SearchEngineTheoremProducer::iteToClauses(const Theorem& ite) {
01166   const Expr& iteExpr = ite.getExpr();
01167 
01168   if(CHECK_PROOFS) {
01169     CHECK_SOUND(iteExpr.isITE() && iteExpr.getType().isBool(),
01170     "SearchEngineTheoremProducer::iteToClauses("+iteExpr.toString()
01171     +")\n Argument must be a Boolean ITE");
01172   }
01173   const Expr& cond = iteExpr[0];
01174   const Expr& t1 = iteExpr[1];
01175   const Expr& t2 = iteExpr[2];
01176 
01177   Proof pf;
01178   if(withProof())
01179     pf = newPf("ite_to_clauses", iteExpr, ite.getProof());
01180   return newTheorem((cond.negate() || t1) && (cond || t2), ite.getAssumptionsRef(), pf);
01181 }
01182 
01183 
01184 Theorem
01185 SearchEngineTheoremProducer::iffToClauses(const Theorem& iff) {
01186   if(CHECK_PROOFS) {
01187     CHECK_SOUND(iff.isRewrite() && iff.getLHS().getType().isBool(),
01188     "SearchEngineTheoremProducer::iffToClauses("+iff.getExpr().toString()
01189     +")\n Argument must be a Boolean IFF");
01190   }
01191   const Expr& t1 = iff.getLHS();
01192   const Expr& t2 = iff.getRHS();
01193 
01194   Proof pf;
01195   if(withProof())
01196     pf = newPf("iff_to_clauses", iff.getExpr(), iff.getProof());
01197   return newTheorem((t1.negate() || t2) && (t1 || t2.negate()), iff.getAssumptionsRef(), pf);
01198 }
01199 
01200 
01201 /////////////////////////////////////////////////////////////////////////
01202 //// helper functions for CNF (Conjunctive Normal Form) conversion
01203 /////////////////////////////////////////////////////////////////////////
01204 Theorem
01205 SearchEngineTheoremProducer::opCNFRule(const Theorem& thm, 
01206                                        int kind,
01207                                        const string& ruleName) {
01208   TRACE("mycnf", "opCNFRule["+d_em->getKindName(kind)+"](",
01209   thm.getExpr(), ") {");
01210   ExprMap<Expr> localCache;
01211   if(CHECK_PROOFS) {
01212     Expr phiIffVar = thm.getExpr();
01213     CHECK_SOUND(phiIffVar.isIff(),
01214     "SearchEngineTheoremProducer::opCNFRule("
01215     +d_em->getKindName(kind)+"): "
01216     "input must be an IFF: thm = " + phiIffVar.toString());
01217     CHECK_SOUND(phiIffVar[0].getKind() == kind,
01218     "SearchEngineTheoremProducer::opCNFRule("
01219     +d_em->getKindName(kind)+"): "
01220     "input phi has wrong kind: thm = " + phiIffVar.toString());
01221     CHECK_SOUND(phiIffVar[0] != phiIffVar[1],
01222     "SearchEngineTheoremProducer::opCNFRule("
01223     +d_em->getKindName(kind)+"): "
01224     "wrong input thm = " + phiIffVar.toString());   
01225     for(Expr::iterator it=phiIffVar[0].begin(), itend=phiIffVar[0].end();
01226   it!=itend;++it){
01227       CHECK_SOUND(phiIffVar[1] != *it,
01228       "SearchEngineTheoremProducer::opCNFRule("
01229       +d_em->getKindName(kind)+"): "
01230       "wrong input thm = " + phiIffVar.toString());
01231     }
01232   }
01233   const Expr& phi = thm.getExpr()[0];
01234   const Expr& phiVar = thm.getExpr()[1];
01235 
01236   std::vector<Expr> boundVars;
01237   std::vector<Expr> boundVarsAndLiterals;
01238   std::vector<Expr> equivs;
01239   for(Expr::iterator i=phi.begin(), iend=phi.end(); i != iend; i++) {
01240     // First, strip the negation and check if the formula is atomic
01241     Expr tmp(*i);
01242     while(tmp.isNot())
01243       tmp = tmp[0];
01244 
01245     if(tmp.isPropAtom())
01246       boundVarsAndLiterals.push_back(*i); 
01247     else
01248       boundVarsAndLiterals.push_back(findInLocalCache(*i, localCache,
01249                   boundVars));
01250   }
01251   
01252   for(ExprMap<Expr>::iterator it=localCache.begin(), itend=localCache.end(); 
01253       it != itend; it++) {
01254     DebugAssert((*it).second.isIff(),
01255     "SearchEngineTheoremProducer::opCNFRule: " +
01256     (*it).second.toString());
01257     DebugAssert(!(*it).second[0].isPropLiteral() && 
01258     (*it).second[1].isAbsLiteral(),
01259     "SearchEngineTheoremProducer::opCNFRule: " +
01260     (*it).second.toString());
01261     equivs.push_back((*it).second);
01262   }
01263   
01264   DebugAssert(boundVarsAndLiterals.size() == (unsigned)phi.arity(),
01265         "SearchEngineTheoremProducer::opCNFRule: "
01266         "wrong size of boundvars: phi = " + phi.toString());
01267   
01268   DebugAssert(boundVars.size() == equivs.size(),
01269         "SearchEngineTheoremProducer::opCNFRule: "
01270         "wrong size of boundvars: phi = " + phi.toString());
01271         
01272   Expr cnfInput = phi.arity() > 0 ? Expr(phi.getOp(), boundVarsAndLiterals) : phi;
01273   Expr  result = convertToCNF(phiVar, cnfInput);
01274   if(boundVars.size() > 0)
01275     result =
01276       d_em->newClosureExpr(EXISTS, boundVars, result.andExpr(andExpr(equivs)));
01277   
01278   Proof pf;
01279   if(withProof())
01280     pf = newPf(ruleName, thm.getExpr(), thm.getProof());
01281   Theorem res(newTheorem(result, thm.getAssumptionsRef(), pf));
01282   TRACE("mycnf", "opCNFRule["+d_em->getKindName(kind)+"] => ", res.getExpr(),
01283   " }");
01284   return res;
01285 }
01286 
01287 //! produces the CNF for the formula  v <==> phi 
01288 Expr SearchEngineTheoremProducer::convertToCNF(const Expr& v, const Expr & phi) {
01289   //we assume that v \iff phi. v is the newVar corresponding to phi
01290   
01291   Expr::iterator i = phi.begin(), iend = phi.end();
01292   std::vector<Expr> clauses;
01293   std::vector<Expr> lastClause;
01294   switch(phi.getKind()) {
01295   case AND: {
01296     const Expr& negV = v.negate();
01297     lastClause.push_back(v);
01298     for(;i!=iend; ++i) {
01299       clauses.push_back(negV.orExpr(*i));
01300       lastClause.push_back(i->negate());
01301     }
01302     clauses.push_back(orExpr(lastClause));
01303   }
01304     break;
01305   case OR:{
01306     lastClause.push_back(v.negate());
01307     for(;i!=iend; ++i) {
01308       clauses.push_back(v.orExpr(i->negate()));
01309       lastClause.push_back(*i);
01310     }
01311     clauses.push_back(orExpr(lastClause));
01312   }
01313     break;
01314   case IFF: {
01315     const Expr& v1 = phi[0];
01316     const Expr& v2 = phi[1];
01317     Expr negV = v.negate();    
01318     Expr negv1 = v1.negate();
01319     Expr negv2 = v2.negate();
01320     clauses.push_back(Expr(OR, negV, negv1, v2));
01321     clauses.push_back(Expr(OR, negV, v1, negv2));
01322     clauses.push_back(Expr(OR, v, v1, v2));
01323     clauses.push_back(Expr(OR, v, negv1, negv2));
01324   } break;
01325   case IMPLIES:{
01326     const Expr& v1 = phi[0];
01327     const Expr& v2 = phi[1];
01328     Expr negV = v.negate();    
01329     Expr negv1 = v1.negate();
01330     Expr negv2 = v2.negate();
01331     clauses.push_back(Expr(OR, negV, negv1, v2));
01332     clauses.push_back(v.orExpr(v1));
01333     clauses.push_back(v.orExpr(negv2));
01334   }
01335     break;
01336   case ITE: {
01337     const Expr& v1 = phi[0];
01338     const Expr& v2 = phi[1];
01339     const Expr& v3 = phi[2];
01340     const Expr& negV = v.negate();
01341     const Expr& negv1 = v1.negate();
01342     const Expr& negv2 = v2.negate();
01343     const Expr& negv3 = v3.negate();
01344     clauses.push_back(Expr(OR, negV, negv1, v2));
01345     clauses.push_back(Expr(OR, negV, v1, v3));
01346     clauses.push_back(Expr(OR, v, negv1, negv2));
01347     clauses.push_back(Expr(OR, v, v1, negv3));
01348   }
01349     break;
01350   default:
01351     DebugAssert(false, "SearchEngineTheoremProducer::convertToCNF: "
01352     "bad operator in phi = "+phi.toString());
01353     break;
01354   }
01355   return andExpr(clauses);
01356 }
01357 
01358 ///////////////////////////////////////////////////////////////////////
01359 // helper functions for CNF converters
01360 ///////////////////////////////////////////////////////////////////////
01361 
01362 Expr SearchEngineTheoremProducer::findInLocalCache(const Expr& i, 
01363                                                    ExprMap<Expr>& localCache,
01364                                                    vector<Expr>& boundVars) {
01365   TRACE("mycnf", "findInLocalCache(", i.toString(), ") { ");
01366   Expr boundVar;
01367   unsigned int negationDepth = 0;
01368   ExprMap<Expr>::iterator it;
01369  
01370   Expr phi = i;
01371   while(phi.isNot()) {
01372     phi = phi[0];
01373     negationDepth++;
01374   }
01375   
01376   it = localCache.find(phi);
01377   Expr v;
01378   if(it != localCache.end()) {
01379     v = ((*it).second)[1];
01380     IF_DEBUG(debugger.counter("CNF Local Cache Hits")++;)
01381   }
01382   else {
01383     v = d_em->newBoundVarExpr(i.getType());
01384     boundVars.push_back(v);
01385     localCache[phi] = phi.iffExpr(v);
01386   }
01387   if(negationDepth % 2 != 0)
01388     v = !v;
01389   TRACE("mycnf", "findInLocalCache => ", v, " }");
01390   return v;
01391 }
01392 
01393 class LFSCPrinter{
01394   const Expr d_bool_res_str;
01395   const Expr d_assump_str;
01396   ExprMap<string> d_assump_map; 
01397   ExprMap<string> d_let_map; 
01398   ExprMap<bool> d_visited;
01399   void collect_assumps(const Expr& pf, ExprMap<bool>&);
01400   string new_name();
01401   void print_helper(const Expr& pf, bool definition = false);
01402   void print_clause(const Expr& );
01403  public:
01404   LFSCPrinter(const Expr, const Expr);
01405   void print(const Expr& pf);
01406 };
01407 
01408 string LFSCPrinter::new_name(){
01409   static int count = 1;
01410   ostringstream name;
01411   name << "c" << count++;
01412   return name.str();
01413 }
01414 
01415 bool is_leaf(const Expr & e){
01416   if (0 == e.arity()) return true;
01417   if ( 1 == e.arity() && e.isNot() ) return true;
01418   return false;
01419 }
01420 
01421 void LFSCPrinter::collect_assumps(const Expr& pf, ExprMap<bool>& visited){
01422   // If seen before, and it's not something trivial, add to d_dagMap
01423   if( visited.count(pf) > 0 && ( ! is_leaf(pf))) {
01424     if (pf.arity() > 0 && pf[0] == d_assump_str){ 
01425       return; // this is a assumption, we will deal this later
01426     }
01427     d_let_map[pf] = new_name();
01428     return;
01429   }
01430 
01431   visited[pf] = true;
01432   
01433   if (pf.arity() > 0 && pf[0] == d_assump_str){ 
01434     d_assump_map[pf[1]] = new_name();
01435     return;
01436   }
01437 
01438   for(Expr::iterator i = pf.begin(), iend = pf.end(); i!=iend; ++i)
01439     collect_assumps(*i, visited);
01440 }
01441 
01442 
01443 LFSCPrinter::LFSCPrinter(const Expr b_str, const Expr a_str):
01444   d_bool_res_str(b_str), d_assump_str(a_str){}
01445 
01446 
01447 void LFSCPrinter::print_clause(const Expr& clause){
01448   if ( ! clause.isOr()){
01449     cout << "ERROR2 " << endl;
01450   }
01451   
01452   int num_lit = clause.arity();
01453   
01454   cout << "(holds ";
01455   
01456   for (int i = 0; i < num_lit; i++){
01457     cout <<"(clc " ; 
01458     if (clause[i].isNot()){
01459       cout << "(neg " << clause[i][0] << ") "; 
01460     }
01461     else {
01462       cout << "(pos " << clause[i] << ") " ;
01463     }
01464   }
01465   cout << "cln";
01466   for (int i = 0; i < num_lit; i++){
01467     cout <<")";
01468   }
01469   cout << ")\n";
01470 }
01471 
01472 void LFSCPrinter::print(const Expr& pf){
01473   ExprMap<bool> visited;
01474   collect_assumps(pf, visited);
01475   ExprMap<string>::iterator i = d_assump_map.begin(), iend = d_assump_map.end();
01476   int num_clause = 0; 
01477   while( i != iend){
01478     num_clause++;
01479     cout << "(% " << (*i).second << " "  ; 
01480     print_clause((*i).first);
01481     i++;
01482   }
01483   
01484   cout << "(: (holds cln) \n";
01485   
01486   ExprMap<string>::iterator j = d_let_map.begin(), jend = d_let_map.end();
01487   int num_lets = 0; 
01488   while( j != jend){
01489     num_lets++;
01490     cout << "(satlem _ _ " ;
01491     print_helper((*j).first, true);
01492     cout << "(\\ "<< (*j).second << " "  ; 
01493     cout << endl;
01494     j++;
01495   }
01496 
01497   print_helper(pf);
01498   for ( int i = 0; i < num_clause; i++){
01499     cout <<")";
01500   }
01501   for ( int i = 0; i < num_lets; i++){
01502     cout <<"))";
01503   }
01504 
01505 }
01506 
01507 void LFSCPrinter::print_helper(const Expr& pf, bool is_definition){
01508   if (d_let_map.count(pf) > 0 && (! is_definition)){
01509     cout << d_let_map[pf] << " " ;
01510     return;
01511   }
01512   if (pf.arity() > 0 &&  pf[0] == d_bool_res_str){
01513     cout << "(R _ _ _ " ;
01514 
01515     Expr v = pf[1];
01516     if (v.isNot()){
01517       print_helper(pf[3]);
01518       print_helper(pf[2]);
01519       cout << v[0] ;
01520     }
01521     else{
01522       print_helper(pf[2]);
01523       print_helper(pf[3]);
01524       cout << v;
01525     }
01526     cout <<")";
01527   }
01528   else if (pf.arity() > 0 && pf[0] == d_assump_str){
01529     Expr clause = pf[1];
01530     cout << d_assump_map[clause] << " " ;
01531   }
01532   else {
01533     cout << "ERROR1" << endl;
01534     cout << pf << endl;
01535   }
01536 }
01537 
01538 
01539 
01540 // for LFSC proof style, by yeting 
01541 void collectVars(const Expr& e, ExprMap<bool>& varCache, ExprMap<bool>& visited) {
01542   // If seen before, and it's not something trivial, add to d_dagMap
01543   if( visited.count(e) > 0) {
01544     return;
01545   }
01546 
01547   visited[e] = true;
01548 
01549   if (e.getKind() == UCONST){ //this is for bool vars
01550     //    cout << "var is " << e << endl;
01551     //    cout << "kind string" << e.getEM()->getKindName(e.getKind()) << endl;
01552     varCache[e] = true;
01553   }
01554   for(Expr::iterator i=e.begin(), iend=e.end(); i!=iend; ++i)
01555     collectVars(*i, varCache,visited);
01556 }
01557 
01558 // theorem for minisat generated proofs,  by yeting
01559 Theorem SearchEngineTheoremProducer::satProof(const Expr& queryExpr, const Proof& satProof) {
01560   Proof pf;
01561   if(withProof())
01562     pf = newPf("minisat_proof", queryExpr, satProof);
01563   {
01564     Expr pf_expr =  pf.getExpr()[2] ;
01565     //     cout << pf_expr << endl;
01566     ExprMap<bool> vars,visited;
01567     collectVars(pf_expr,vars,visited);
01568 
01569     cout << "(check \n" ; 
01570     
01571     vector<Expr> vars_vec ;
01572     ExprMap<bool>::iterator i = vars.begin(), iend = vars.end();
01573     while (i != iend){
01574       vars_vec.push_back((*i).first);
01575       //      cout << "var " << (*i).first << endl;
01576       i++;
01577     }
01578     int num_vars = vars_vec.size();
01579     for (int i = 0; i < num_vars; i++){
01580       cout << "(% " << vars_vec[i] << " var " << endl;
01581     }
01582 
01583 
01584 
01585     const Expr bool_res_string = pf_expr.getEM()->newStringExpr("bool_resolution");
01586     const Expr assump_string = pf_expr.getEM()->newStringExpr("assumptions");
01587     LFSCPrinter lfsc_printer(bool_res_string, assump_string);
01588     lfsc_printer.print(pf_expr);
01589     
01590     for (int i = 0; i < num_vars; i++){
01591       cout << ")";
01592     }
01593     cout << ")" << endl;
01594     cout << ")" << endl;
01595   }
01596   return newTheorem(queryExpr, Assumptions::emptyAssump() , pf);
01597 }
01598 
01599 
01600 //  LocalWords:  clc

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