CVC3 2.2
|
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