00001
00002
00003
00004
00005
00006
00007
00008
00009
00010
00011
00012
00013
00014
00015
00016
00017
00018
00019
00020
00021
00022 #include "search_impl_base.h"
00023 #include "theory.h"
00024 #include "eval_exception.h"
00025 #include "search_rules.h"
00026 #include "variable.h"
00027 #include "command_line_flags.h"
00028 #include "statistics.h"
00029 #include "theorem_manager.h"
00030 #include "expr_transform.h"
00031
00032
00033 using namespace std;
00034
00035
00036 namespace CVC3 {
00037
00038
00039 class CoreSatAPI_implBase :public TheoryCore::CoreSatAPI {
00040 SearchImplBase* d_se;
00041 public:
00042 CoreSatAPI_implBase(SearchImplBase* se) : d_se(se) {}
00043 virtual ~CoreSatAPI_implBase() {}
00044 virtual void addLemma(const Theorem& thm) { d_se->addFact(thm); }
00045 virtual Theorem addAssumption(const Expr& assump)
00046 { return d_se->newIntAssumption(assump); }
00047 virtual void addSplitter(const Expr& e, int priority)
00048 { d_se->addSplitter(e, priority); }
00049 virtual bool check(const Expr& e);
00050 };
00051
00052 bool CoreSatAPI_implBase::check(const Expr& e)
00053 {
00054 Theorem thm;
00055 int scope = d_se->theoryCore()->getCM()->scopeLevel();
00056 d_se->theoryCore()->getCM()->push();
00057 QueryResult res = d_se->checkValid(e, thm);
00058 d_se->theoryCore()->getCM()->popto(scope);
00059 return res == VALID;
00060 }
00061
00062
00063
00064 }
00065
00066
00067 using namespace CVC3;
00068
00069
00070
00071
00072
00073 SearchImplBase::Splitter::Splitter(const Literal& lit): d_lit(lit) {
00074 d_lit.count()++;
00075 TRACE("Splitter", "Splitter(", d_lit, ")");
00076 }
00077
00078
00079 SearchImplBase::Splitter::Splitter(const SearchImplBase::Splitter& s)
00080 : d_lit(s.d_lit) {
00081 d_lit.count()++;
00082 TRACE("Splitter", "Splitter[copy](", d_lit, ")");
00083 }
00084
00085
00086 SearchImplBase::Splitter&
00087 SearchImplBase::Splitter::operator=(const SearchImplBase::Splitter& s) {
00088 if(this == &s) return *this;
00089 d_lit.count()--;
00090 d_lit = s.d_lit;
00091 d_lit.count()++;
00092 TRACE("Splitter", "Splitter[assign](", d_lit, ")");
00093 return *this;
00094 }
00095
00096
00097 SearchImplBase::Splitter::~Splitter() {
00098 d_lit.count()--;
00099 TRACE("Splitter", "~Splitter(", d_lit, ")");
00100 }
00101
00102
00103
00104
00105 SearchImplBase::SearchImplBase(TheoryCore* core)
00106 : SearchEngine(core),
00107 d_bottomScope(core->getCM()->getCurrentContext()),
00108 d_dpSplitters(core->getCM()->getCurrentContext()),
00109 d_lastValid(d_commonRules->trueTheorem()),
00110 d_assumptions(core->getCM()->getCurrentContext()),
00111 d_cnfCache(core->getCM()->getCurrentContext()),
00112 d_cnfVars(core->getCM()->getCurrentContext()),
00113 d_cnfOption(&(core->getFlags()["cnf"].getBool())),
00114 d_ifLiftOption(&(core->getFlags()["iflift"].getBool())),
00115 d_ignoreCnfVarsOption(&(core->getFlags()["ignore-cnf-vars"].getBool())),
00116 d_origFormulaOption(&(core->getFlags()["orig-formula"].getBool())),
00117 d_enqueueCNFCache(core->getCM()->getCurrentContext()),
00118 d_applyCNFRulesCache(core->getCM()->getCurrentContext()),
00119 d_replaceITECache(core->getCM()->getCurrentContext())
00120 {
00121 d_vm = new VariableManager(core->getCM(), d_rules,
00122 core->getFlags()["mm"].getString());
00123 IF_DEBUG(d_assumptions.setName("CDList[SearchImplBase::d_assumptions]"));
00124 d_coreSatAPI_implBase = new CoreSatAPI_implBase(this);
00125 core->registerCoreSatAPI(d_coreSatAPI_implBase);
00126 }
00127
00128
00129
00130 SearchImplBase::~SearchImplBase()
00131 {
00132 delete d_coreSatAPI_implBase;
00133 delete d_vm;
00134 }
00135
00136
00137
00138
00139 Theorem SearchImplBase::newUserAssumption(const Expr& e) {
00140 Theorem thm;
00141 CDMap<Expr,Theorem>::iterator i(d_assumptions.find(e));
00142 IF_DEBUG(if(debugger.trace("search verbose")) {
00143 ostream& os(debugger.getOS());
00144 os << "d_assumptions = [";
00145 for(CDMap<Expr,Theorem>::iterator i=d_assumptions.begin(),
00146 iend=d_assumptions.end(); i!=iend; ++i) {
00147 debugger.getOS() << "(" << (*i).first << " => " << (*i).second << "), ";
00148 }
00149 os << "]" << endl;
00150 });
00151 if(i!=d_assumptions.end()) {
00152 TRACE("search verbose", "newUserAssumption(", e,
00153 "): assumption already exists");
00154 } else {
00155 thm = d_commonRules->assumpRule(e);
00156 d_assumptions[e] = thm;
00157 e.setUserAssumption();
00158 TRACE("search verbose", "newUserAssumption(", thm,
00159 "): created new assumption");
00160 }
00161 if (!thm.isNull()) d_core->addFact(d_core->getExprTrans()->preprocess(thm));
00162 return thm;
00163 }
00164
00165
00166
00167
00168 Theorem SearchImplBase::newIntAssumption(const Expr& e) {
00169 Theorem thm = d_commonRules->assumpRule(e);
00170 Expr atom = e.isNot() ? e[0] : e;
00171 thm.setQuantLevel(theoryCore()->getQuantLevelForTerm(atom));
00172 newIntAssumption(thm);
00173 return thm;
00174 }
00175
00176
00177 void SearchImplBase::newIntAssumption(const Theorem& thm) {
00178 DebugAssert(!d_assumptions.count(thm.getExpr()),
00179 "newIntAssumption: repeated assertion: "+thm.getExpr().toString());
00180 d_assumptions[thm.getExpr()] = thm;
00181 thm.getExpr().setIntAssumption();
00182 TRACE("search verbose", "newIntAssumption(", thm,
00183 "): new assumption");
00184 }
00185
00186
00187 void SearchImplBase::getUserAssumptions(vector<Expr>& assumptions)
00188 {
00189 for(CDMap<Expr,Theorem>::orderedIterator i=d_assumptions.orderedBegin(),
00190 iend=d_assumptions.orderedEnd(); i!=iend; ++i)
00191 if ((*i).first.isUserAssumption()) assumptions.push_back((*i).first);
00192 }
00193
00194
00195 void SearchImplBase::getInternalAssumptions(std::vector<Expr>& assumptions)
00196 {
00197 for(CDMap<Expr,Theorem>::orderedIterator i=d_assumptions.orderedBegin(),
00198 iend=d_assumptions.orderedEnd(); i!=iend; ++i)
00199 if ((*i).first.isIntAssumption()) assumptions.push_back((*i).first);
00200 }
00201
00202
00203 void SearchImplBase::getAssumptions(std::vector<Expr>& assumptions)
00204 {
00205 for(CDMap<Expr,Theorem>::orderedIterator i=d_assumptions.orderedBegin(),
00206 iend=d_assumptions.orderedEnd(); i!=iend; ++i)
00207 assumptions.push_back((*i).first);
00208 }
00209
00210
00211 bool SearchImplBase::isAssumption(const Expr& e) {
00212 return d_assumptions.count(e) > 0;
00213 }
00214
00215
00216 void SearchImplBase::addCNFFact(const Theorem& thm, bool fromCore) {
00217 TRACE("addCNFFact", "addCNFFact(", thm.getExpr(), ") {");
00218 if(thm.isAbsLiteral()) {
00219 addLiteralFact(thm);
00220
00221 if(!fromCore) d_core->enqueueFact(thm);
00222 } else {
00223 addNonLiteralFact(thm);
00224 }
00225 TRACE_MSG("addCNFFact", "addCNFFact => }");
00226 }
00227
00228
00229 void SearchImplBase::addFact(const Theorem& thm) {
00230 TRACE("search addFact", "SearchImplBase::addFact(", thm.getExpr(), ") {");
00231 if(*d_cnfOption)
00232 enqueueCNF(thm);
00233 else
00234 addCNFFact(thm, true);
00235 TRACE_MSG("search addFact", "SearchImplBase::addFact => }");
00236 }
00237
00238
00239 void SearchImplBase::addSplitter(const Expr& e, int priority) {
00240 DebugAssert(e.isAbsLiteral(), "SearchImplBase::addSplitter("+e.toString()+")");
00241 d_dpSplitters.push_back(Splitter(newLiteral(e)));
00242 }
00243
00244
00245 void SearchImplBase::getCounterExample(vector<Expr>& assertions, bool inOrder)
00246 {
00247 if(!d_core->getTM()->withAssumptions())
00248 throw EvalException
00249 ("Method getCounterExample() (or command COUNTEREXAMPLE) cannot be used\n"
00250 " without assumptions activated");
00251 if(!d_lastValid.isNull())
00252 throw EvalException
00253 ("Method getCounterExample() (or command COUNTEREXAMPLE)\n"
00254 " must be called only after failed QUERY");
00255 getInternalAssumptions(assertions);
00256
00257
00258
00259
00260
00261
00262
00263
00264
00265
00266
00267
00268
00269
00270
00271
00272
00273
00274
00275
00276 }
00277
00278
00279 Proof
00280 SearchImplBase::getProof()
00281 {
00282 if(!d_core->getTM()->withProof())
00283 throw EvalException
00284 ("DUMP_PROOF cannot be used without proofs activated");
00285 if(d_lastValid.isNull())
00286 throw EvalException
00287 ("DUMP_PROOF must be called only after successful QUERY");
00288
00289 if(d_lastValid.isNull()) return Proof();
00290 return d_lastValid.getProof();
00291 }
00292
00293
00294 const Assumptions&
00295 SearchImplBase::getAssumptionsUsed()
00296 {
00297 if(!d_core->getTM()->withAssumptions())
00298 throw EvalException
00299 ("DUMP_ASSUMPTIONS cannot be used without assumptions activated");
00300 if(d_lastValid.isNull())
00301 throw EvalException
00302 ("DUMP_ASSUMPTIONS must be called only after successful QUERY");
00303
00304 if(d_lastValid.isNull()) return Assumptions::emptyAssump();
00305 return d_lastValid.getAssumptionsRef();
00306 }
00307
00308
00309
00310
00311
00312
00313
00314
00315 void SearchImplBase::processResult(const Theorem& res, const Expr& e)
00316 {
00317
00318 DebugAssert(res.isNull() || res.getExpr().isFalse(),
00319 "processResult: bad input"
00320 + res.toString());
00321 if(res.isNull()) {
00322
00323
00324
00325 d_lastValid = Theorem();
00326
00327 d_lastCounterExample.erase(!e);
00328 if (e.isNot()) d_lastCounterExample.erase(e[0]);
00329 } else {
00330
00331 Theorem res2 =
00332 d_rules->eliminateSkolemAxioms(res, d_commonRules->getSkolemAxioms());
00333 if(e.isNot())
00334 d_lastValid = d_rules->negIntro(e, res2);
00335 else
00336 d_lastValid = d_rules->proofByContradiction(e, res2);
00337 d_lastCounterExample.clear();
00338 }
00339 }
00340
00341
00342 QueryResult SearchImplBase::checkValid(const Expr& e, Theorem& result) {
00343 d_commonRules->clearSkolemAxioms();
00344 QueryResult qres = checkValidInternal(e);
00345 result = d_lastValid;
00346 return qres;
00347 }
00348
00349
00350 QueryResult SearchImplBase::restart(const Expr& e, Theorem& result) {
00351 QueryResult qres = restartInternal(e);
00352 result = d_lastValid;
00353 return qres;
00354 }
00355
00356
00357 void
00358 SearchImplBase::enqueueCNF(const Theorem& beta) {
00359 TRACE("mycnf", "enqueueCNF(", beta, ") {");
00360 if(*d_origFormulaOption)
00361 addCNFFact(beta);
00362
00363 enqueueCNFrec(beta);
00364 TRACE_MSG("mycnf", "enqueueCNF => }");
00365 }
00366
00367
00368 void
00369 SearchImplBase::enqueueCNFrec(const Theorem& beta) {
00370 Theorem theta = beta;
00371
00372 TRACE("mycnf","enqueueCNFrec(", theta.getExpr(), ") { ");
00373 TRACE("cnf-clauses", "enqueueCNF call", theta.getExpr(), "");
00374
00375 DebugAssert(theta.getScope() <= scopeLevel(),
00376 "\n theta.getScope()="+int2string(theta.getScope())
00377 +"\n scopeLevel="+int2string(scopeLevel())
00378 +"\n e = "+theta.getExpr().toString());
00379
00380 Expr thetaExpr = theta.getExpr();
00381
00382 if(d_enqueueCNFCache.count(thetaExpr) > 0) {
00383 TRACE_MSG("mycnf", "enqueueCNFrec[cached] => }");
00384 return;
00385 }
00386
00387 d_enqueueCNFCache[thetaExpr] = true;
00388
00389
00390 while(thetaExpr.isNot() && thetaExpr[0].isNot()) {
00391 theta = d_commonRules->notNotElim(theta);
00392 thetaExpr = theta.getExpr();
00393
00394 d_enqueueCNFCache[thetaExpr] = true;
00395 }
00396
00397
00398 if(thetaExpr.isPropLiteral()) {
00399 theta = d_commonRules->iffMP(theta, replaceITE(thetaExpr));
00400 DebugAssert(!*d_ifLiftOption || theta.isAbsLiteral(),
00401 "Must be a literal: theta = "
00402 +theta.getExpr().toString());
00403 addCNFFact(theta);
00404 TRACE_MSG("mycnf", "enqueueCNFrec[literal] => }");
00405 TRACE("cnf-clauses", "literal with proofs(", theta.getExpr(), ")");
00406 return;
00407 }
00408
00409 thetaExpr = theta.getExpr();
00410
00411 switch(thetaExpr.getKind()) {
00412 case AND:
00413
00414 for(int i=0; i<thetaExpr.arity(); i++)
00415 enqueueCNFrec(d_commonRules->andElim(theta, i));
00416 TRACE_MSG("mycnf", "enqueueCNFrec[AND] => }");
00417 return;
00418 case OR: {
00419
00420
00421 bool cnf(true);
00422 TRACE("bv mycnf", "enqueueCNFrec[OR] ( ", theta.getExpr().toString(), ")");
00423 for(Expr::iterator i=thetaExpr.begin(),iend=thetaExpr.end();
00424 i!=iend && cnf; i++) {
00425 if(!(*i).isPropLiteral())
00426 cnf = false;
00427 }
00428 if(cnf) {
00429 vector<Theorem> thms;
00430 vector<unsigned int> changed;
00431 unsigned int cc=0;
00432 for(Expr::iterator i=thetaExpr.begin(),iend=thetaExpr.end();
00433 i!=iend; i++,cc++) {
00434 Theorem thm = replaceITE(*i);
00435 if(thm.getLHS() != thm.getRHS()) {
00436 thms.push_back(thm);
00437 changed.push_back(cc);
00438 }
00439 }
00440 if(changed.size() > 0) {
00441 Theorem rewrite =
00442 d_commonRules->substitutivityRule(theta.getExpr(), changed, thms);
00443 theta = d_commonRules->iffMP(theta, rewrite);
00444 }
00445 addCNFFact(theta);
00446 TRACE_MSG("mycnf", "enqueueCNFrec[cnf] => }");
00447 return;
00448 }
00449 break;
00450 }
00451 case IFF: {
00452 const Expr& t0 = thetaExpr[0];
00453 const Expr& t1 = thetaExpr[1];
00454 if(t1.isPropLiteral()) {
00455 if(!t1.isAbsLiteral())
00456 theta = d_commonRules->transitivityRule(theta, replaceITE(t1));
00457 applyCNFRules(theta);
00458 return;
00459 } else if(thetaExpr[0].isPropLiteral()) {
00460 theta = d_commonRules->symmetryRule(theta);
00461 if(!t0.isAbsLiteral())
00462 theta = d_commonRules->transitivityRule(theta, replaceITE(t0));
00463 applyCNFRules(theta);
00464 return;
00465 }
00466 break;
00467 }
00468 case ITE:
00469 if(thetaExpr[0].isPropLiteral() && thetaExpr[1].isPropLiteral()
00470 && thetaExpr[2].isPropLiteral()) {
00471
00472 vector<Theorem> thms;
00473 vector<unsigned int> changed;
00474 for(int c=0, cend=thetaExpr.arity(); c<cend; ++c) {
00475 Theorem thm = replaceITE(thetaExpr[c]);
00476 if(thm.getLHS() != thm.getRHS()) {
00477 DebugAssert(!*d_ifLiftOption || thm.getRHS().isAbsLiteral(),
00478 "thm = "+thm.getExpr().toString());
00479 thms.push_back(thm);
00480 changed.push_back(c);
00481 }
00482 }
00483 if(changed.size() > 0) {
00484 Theorem rewrite =
00485 d_commonRules->substitutivityRule(theta.getExpr(), changed, thms);
00486 theta = d_commonRules->iffMP(theta, rewrite);
00487 }
00488
00489 Theorem thm = d_rules->iteToClauses(theta);
00490 DebugAssert(thm.getExpr().isAnd() && thm.getExpr().arity()==2,
00491 "enqueueCNFrec [ITE over literals]\n thm = "
00492 +thm.getExpr().toString());
00493 addCNFFact(d_commonRules->andElim(thm, 0));
00494 addCNFFact(d_commonRules->andElim(thm, 1));
00495 return;
00496 }
00497 break;
00498 default:
00499 break;
00500 }
00501
00502
00503 Theorem res = findInCNFCache(theta.getExpr());
00504 if(!res.isNull()) {
00505 Theorem thm = d_commonRules->iffMP(theta, res);
00506 DebugAssert(thm.isAbsLiteral(), "thm = "+thm.getExpr().toString());
00507 addCNFFact(thm);
00508 TRACE("cnf-clauses", "enqueueCNFrec call[cache hit]:(",
00509 thm.getExpr(), ")");
00510 applyCNFRules(res);
00511 TRACE_MSG("mycnf", "enqueueCNFrec[cached] => }");
00512 return;
00513 }
00514
00515
00516 Theorem result;
00517
00518 result = d_commonRules->varIntroSkolem(theta.getExpr());
00519
00520 TRACE("mycnf", "enqueueCNFrec: varIntroSkolem => ", result.getExpr(),
00521 " @ "+int2string(result.getScope())
00522 +" (current="+int2string(scopeLevel())+")");
00523
00524
00525
00526 TRACE("mycnf", "enqueueCNFrec: skolemize => ", result.getExpr(),
00527 " @ "+int2string(result.getScope())
00528 +" (current="+int2string(scopeLevel())+")");
00529 DebugAssert(result.isRewrite(),
00530 "SearchImplBase::CNF(): result = "+result.toString());
00531 DebugAssert(!result.getLHS().isPropLiteral() &&
00532 result.getRHS().isPropLiteral(),
00533 "SearchImplBase::CNF(): result = "+result.toString());
00534 DebugAssert(result.getLHS() == theta.getExpr(),
00535 "SearchImplBase::CNF(): result = "+result.toString()
00536 +"\n theta = "+theta.toString());
00537
00538
00539 Theorem var(d_commonRules->iffMP(theta, result));
00540
00541 d_cnfVars[var.getExpr()] = true;
00542 TRACE("mycnf", "enqueueCNFrec: theta = ", theta.getExpr(),
00543 " @ "+int2string(theta.getScope())
00544 +" (current="+int2string(scopeLevel())+")");
00545 TRACE("mycnf", "enqueueCNFrec: var = ", var.getExpr(),
00546 " @ "+int2string(var.getScope())
00547 +" (current="+int2string(scopeLevel())+")");
00548 DebugAssert(var.isAbsLiteral(), "var = "+var.getExpr().toString());
00549 addCNFFact(var);
00550
00551 addToCNFCache(result);
00552 applyCNFRules(result);
00553 TRACE_MSG("mycnf", "enqueueCNFrec => }");
00554 }
00555
00556
00557
00558
00559
00560 void
00561 SearchImplBase::applyCNFRules(const Theorem& thm) {
00562 TRACE("mycnf", "applyCNFRules(", thm.getExpr(), ") { ");
00563
00564 Theorem result = thm;
00565 DebugAssert(result.isRewrite(),
00566 "SearchImplBase::applyCNFRules: input must be an iff: " +
00567 result.getExpr().toString());
00568 Expr lhs = result.getLHS();
00569 Expr rhs = result.getRHS();
00570 DebugAssert(rhs.isAbsLiteral(),
00571 "SearchImplBase::applyCNFRules: rhs of input must be literal: " +
00572 result.getExpr().toString());
00573
00574
00575 while(result.getLHS().isNot())
00576 result = d_commonRules->iffContrapositive(result);
00577 lhs = result.getLHS();
00578 rhs = result.getRHS();
00579
00580 CDMap<Expr,bool>::iterator it = d_applyCNFRulesCache.find(lhs);
00581 if(it == d_applyCNFRulesCache.end())
00582 d_applyCNFRulesCache[lhs] = true;
00583 else {
00584 TRACE_MSG("mycnf","applyCNFRules[temp cache] => }");
00585 return;
00586 }
00587
00588
00589 if(lhs.isPropLiteral()) {
00590 if(!lhs.isAbsLiteral()) {
00591 Theorem replaced = d_commonRules->symmetryRule(replaceITE(lhs));
00592 result = d_commonRules->transitivityRule(replaced, result);
00593 lhs = result.getLHS();
00594 DebugAssert(rhs == result.getRHS(),
00595 "applyCNFRules [literal lhs]\n result = "
00596 +result.getExpr().toString()
00597 +"\n rhs = "+rhs.toString());
00598 }
00599 Theorem thm = d_rules->iffToClauses(result);
00600 DebugAssert(thm.getExpr().isAnd() && thm.getExpr().arity()==2,
00601 "applyCNFRules [literal lhs]\n thm = "
00602 +thm.getExpr().toString());
00603 addCNFFact(d_commonRules->andElim(thm, 0));
00604 addCNFFact(d_commonRules->andElim(thm, 1));
00605 return;
00606 }
00607
00608
00609 vector<unsigned> changed;
00610 vector<Theorem> substitutions;
00611 int c=0;
00612 for(Expr::iterator j = lhs.begin(), jend = lhs.end(); j!=jend; ++c,++j) {
00613 const Expr& phi = *j;
00614 if(!phi.isPropLiteral()) {
00615 Theorem phiIffVar = findInCNFCache(phi);
00616 if(phiIffVar.isNull()) {
00617
00618 phiIffVar = d_commonRules->varIntroSkolem(phi);
00619 addToCNFCache(phiIffVar);
00620 }
00621 DebugAssert(phiIffVar.isRewrite(),
00622 "SearchImplBase::applyCNFRules: result = " +
00623 result.toString());
00624 DebugAssert(phi == phiIffVar.getLHS(),
00625 "SearchImplBase::applyCNFRules:\n phi = " +
00626 phi.toString()
00627 + "\n\n phiIffVar = " + phiIffVar.toString());
00628 DebugAssert(phiIffVar.getRHS().isAbsLiteral(),
00629 "SearchImplBase::applyCNFRules: phiIffVar = " +
00630 phiIffVar.toString());
00631 changed.push_back(c);
00632 substitutions.push_back(phiIffVar);
00633 applyCNFRules(phiIffVar);
00634 }
00635 }
00636 if(changed.size() > 0) {
00637 Theorem subst =
00638 d_commonRules->substitutivityRule(lhs, changed, substitutions);
00639 subst = d_commonRules->symmetryRule(subst);
00640 result = d_commonRules->transitivityRule(subst, result);
00641 }
00642
00643 switch(result.getLHS().getKind()) {
00644 case AND:
00645 result = d_rules->andCNFRule(result);
00646 break;
00647 case OR:
00648 result = d_rules->orCNFRule(result);
00649 break;
00650 case IFF:
00651 result = d_rules->iffCNFRule(result);
00652 break;
00653 case IMPLIES:
00654 result = d_rules->impCNFRule(result);
00655 break;
00656 case ITE:
00657 result = d_rules->iteCNFRule(result);
00658 break;
00659 default:
00660 DebugAssert(false,
00661 "SearchImplBase::applyCNFRules: "
00662 "the input operator must be and|or|iff|imp|ite\n result = " +
00663 result.getLHS().toString());
00664 break;
00665 }
00666
00667
00668 Theorem clauses(result);
00669
00670
00671 DebugAssert(!clauses.isNull(), "Oops!..");
00672 DebugAssert(clauses.getExpr().isAnd(), "clauses = "
00673 +clauses.getExpr().toString());
00674
00675
00676
00677 for(int i=0, iend=clauses.getExpr().arity(); i<iend; ++i) {
00678 Theorem clause(d_commonRules->andElim(clauses,i));
00679 addCNFFact(clause);
00680 }
00681 TRACE_MSG("mycnf","applyCNFRules => }");
00682 }
00683
00684
00685 bool SearchImplBase::isClause(const Expr& e) {
00686 if(e.isAbsLiteral()) return true;
00687 if(!e.isOr()) return false;
00688
00689 bool cnf(true);
00690 for(Expr::iterator i=e.begin(), iend=e.end(); i!=iend && cnf; ++i)
00691 cnf = (*i).isAbsLiteral();
00692 return cnf;
00693 }
00694
00695
00696 bool
00697 SearchImplBase::isPropClause(const Expr& e) {
00698 if(e.isPropLiteral()) return true;
00699 if(!e.isOr()) return false;
00700
00701 bool cnf(true);
00702 for(Expr::iterator i=e.begin(), iend=e.end(); i!=iend && cnf; ++i)
00703 cnf = (*i).isPropLiteral();
00704 return cnf;
00705 }
00706
00707
00708 bool
00709 SearchImplBase::isGoodSplitter(const Expr& e) {
00710 if(!*d_ignoreCnfVarsOption) return true;
00711 TRACE("isGoodSplitter", "isGoodSplitter(", e, ") {");
00712
00713 const Expr& var = e.isNot()? e[0] : e;
00714 bool res(!isCNFVar(var));
00715 TRACE("isGoodSplitter", "isGoodSplitter => ", res? "true" : "false", " }");
00716 return res;
00717 }
00718
00719
00720 void
00721 SearchImplBase::addToCNFCache(const Theorem& thm) {
00722 TRACE("mycnf", "addToCNFCache(", thm.getExpr(), ")");
00723
00724 d_core->getStatistics().counter("CNF New Vars")++;
00725
00726 Theorem result = thm;
00727 DebugAssert(result.isRewrite(),
00728 "SearchImplBase::addToCNFCache: input must be an iff: " +
00729 result.getExpr().toString());
00730
00731 d_cnfVars[thm.getRHS()] = true;
00732
00733 Theorem t(thm);
00734 Expr phi = thm.getLHS();
00735 while(phi.isNot()) {
00736 t = d_commonRules->iffContrapositive(thm);
00737 phi = phi[0];
00738 }
00739 DebugAssert(d_cnfCache.count(phi) == 0,
00740 "thm = "+thm.getExpr().toString() +
00741 "\n t = "+ t.getExpr().toString());
00742
00743 d_cnfCache.insert(phi, t, d_bottomScope);
00744 }
00745
00746
00747 Theorem
00748 SearchImplBase::findInCNFCache(const Expr& e) {
00749 TRACE("mycnf", "findInCNFCache(", e, ") { ");
00750 Expr phi(e);
00751
00752 int numNegs(0);
00753
00754 while(phi.isNot()) {
00755 phi = phi[0]; numNegs++;
00756 }
00757 CDMap<Expr,Theorem>::iterator it = d_cnfCache.find(phi);
00758 if(it != d_cnfCache.end()) {
00759
00760 d_core->getStatistics().counter("CNF cache hits")++;
00761 Theorem thm = (*it).second;
00762
00763 DebugAssert(thm.isRewrite() && thm.getLHS() == phi,
00764 "SearchImplBase::findInCNFCache: thm must be an iff: " +
00765 thm.getExpr().toString());
00766
00767
00768
00769
00770 if(numNegs % 2 != 0) {
00771 thm = d_commonRules->iffContrapositive(thm);
00772 numNegs--;
00773 }
00774 for(; numNegs > 0; numNegs-=2) {
00775 Theorem t = d_commonRules->rewriteNotNot(!!(thm.getLHS()));
00776 thm = d_commonRules->transitivityRule(t,thm);
00777 }
00778
00779 DebugAssert(numNegs == 0, "numNegs = "+int2string(numNegs));
00780 TRACE("mycnf", "findInCNFCache => ", thm.getExpr(), " }");
00781 return thm;
00782 }
00783 TRACE_MSG("mycnf", "findInCNFCache => null }");
00784 return Theorem();
00785 }
00786
00787
00788
00789
00790
00791
00792
00793
00794
00795
00796
00797
00798
00799
00800
00801 Theorem
00802 SearchImplBase::replaceITE(const Expr& e) {
00803 TRACE("replaceITE","replaceITE(", e, ") { ");
00804 Theorem res;
00805
00806 CDMap<Expr,Theorem>::iterator i=d_replaceITECache.find(e),
00807 iend=d_replaceITECache.end();
00808 if(i!=iend) {
00809 TRACE("replaceITE", "replaceITE[cached] => ", (*i).second, " }");
00810 return (*i).second;
00811 }
00812
00813 if(e.isAbsLiteral())
00814 res = d_core->rewriteLiteral(e);
00815 else
00816 res = d_commonRules->reflexivityRule(e);
00817
00818
00819
00820
00821
00822 if(!res.getRHS().isPropLiteral()) {
00823 Theorem varThm(findInCNFCache(res.getRHS()));
00824 if(varThm.isNull()) {
00825 varThm = d_commonRules->varIntroSkolem(res.getRHS());
00826 Theorem var;
00827 if(res.isRewrite())
00828 var = d_commonRules->transitivityRule(res,varThm);
00829 else
00830 var = d_commonRules->iffMP(res,varThm);
00831
00832
00833 addToCNFCache(varThm);
00834 }
00835 applyCNFRules(varThm);
00836
00837 res = d_commonRules->transitivityRule(res, varThm);
00838 }
00839
00840 d_replaceITECache[e] = res;
00841
00842 TRACE("replaceITE", "replaceITE => ", res, " }");
00843 return res;
00844 }