search_impl_base.cpp

Go to the documentation of this file.
00001 /*****************************************************************************/
00002 /*!
00003  * \file search_impl_base.cpp
00004  * 
00005  * Author: Clark Barrett, Vijay Ganesh (CNF Converter)
00006  * 
00007  * Created: Fri Jan 17 14:19:54 2003
00008  *
00009  * <hr>
00010  *
00011  * License to use, copy, modify, sell and/or distribute this software
00012  * and its documentation for any purpose is hereby granted without
00013  * royalty, subject to the terms and conditions defined in the \ref
00014  * LICENSE file provided with this distribution.
00015  * 
00016  * <hr>
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 // class SearchImplBase::Splitter methods
00071 
00072 // Constructor
00073 SearchImplBase::Splitter::Splitter(const Literal& lit): d_lit(lit) {
00074 d_lit.count()++;
00075   TRACE("Splitter", "Splitter(", d_lit, ")");
00076 }
00077 
00078 // Copy constructor
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 // Assignment
00086 SearchImplBase::Splitter&
00087 SearchImplBase::Splitter::operator=(const SearchImplBase::Splitter& s) {
00088   if(this == &s) return *this; // Self-assignment
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 // Destructor
00097 SearchImplBase::Splitter::~Splitter() {
00098   d_lit.count()--;
00099   TRACE("Splitter", "~Splitter(", d_lit, ")");
00100 }
00101 
00102 
00103 
00104 //! Constructor
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 //! Destructor
00130 SearchImplBase::~SearchImplBase()
00131 {
00132   delete d_coreSatAPI_implBase;
00133   delete d_vm;
00134 }
00135 
00136 
00137 // Returns a new theorem if e has not already been asserted, otherwise returns
00138 // a NULL theorem.
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 // Same as newUserAssertion, except it's an error to assert something that's
00167 // already been asserted.
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     // These literals are derived, and  should also be reported to the core.  
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   if(!d_lastCounterExample.empty()) {
00259     if (inOrder) {
00260       for(CDMap<Expr,Theorem>::orderedIterator i=d_assumptions.orderedBegin(),
00261             iend=d_assumptions.orderedEnd(); i!=iend; ++i) {
00262         if (d_lastCounterExample.find((*i).first) != d_lastCounterExample.end()) {
00263           assertions.push_back((*i).first);
00264         }
00265       }
00266       DebugAssert(assertions.size()==d_lastCounterExample.size(),
00267                   "getCounterExample: missing assertion");
00268     }
00269     else {
00270       ExprHashMap<bool>::iterator i=d_lastCounterExample.begin(),
00271         iend = d_lastCounterExample.end();
00272       for(; i!=iend; ++i) assertions.push_back((*i).first);
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   // Double-check for optimized version
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   // Double-check for optimized version
00304   if(d_lastValid.isNull()) return Assumptions::emptyAssump();
00305   return d_lastValid.getAssumptionsRef();
00306 }
00307 
00308 /*! 
00309  * Given a proof of FALSE ('res') from an assumption 'e', derive the
00310  * proof of the inverse of e.
00311  *
00312  * \param res is a proof of FALSE
00313  * \param e is the assumption used in the above proof
00314  */
00315 void SearchImplBase::processResult(const Theorem& res, const Expr& e)
00316 {
00317   // Result must be either Null (== SAT) or false (== unSAT)
00318   DebugAssert(res.isNull() || res.getExpr().isFalse(),
00319         "processResult: bad input"
00320         + res.toString());
00321   if(res.isNull()) {
00322     // Didn't prove valid (if CVC-lite is complete, it means invalid).
00323     // The assumptions for the counterexample must have been already
00324     // set by checkSAT().
00325     d_lastValid = Theorem(); // Reset last proof
00326     // Remove !e, keep just the counterexample
00327     d_lastCounterExample.erase(!e);
00328     if (e.isNot()) d_lastCounterExample.erase(e[0]);
00329   } else {
00330     // Proved valid
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(); // Reset counterexample
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   // The theorem scope shouldn't be higher than current
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   //   // Strip double negations first
00390   while(thetaExpr.isNot() && thetaExpr[0].isNot()) {
00391     theta = d_commonRules->notNotElim(theta);
00392     thetaExpr = theta.getExpr();
00393     // Cache all the derived theorems too
00394     d_enqueueCNFCache[thetaExpr] = true;
00395   }
00396 
00397   // Check for a propositional literal
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   // Obvious optimizations for AND and OR  
00411   switch(thetaExpr.getKind()) {
00412   case AND:
00413     // Split up the top-level conjunction and translate individually
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     // Check if we are already in CNF (ignoring ITEs in the terms),
00420     // and if we are, translate term ITEs on the way
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: { // Check for "var <=> phi" and "phi <=> var"
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       // Replace ITEs
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       // Convert to clauses
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   // Now do the real work
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   //  std::vector<Theorem> clauses;
00516   Theorem result;
00517   // (\phi <==> v)
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   //result = skolemize(result, false);
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   //enqueue v
00539   Theorem var(d_commonRules->iffMP(theta, result));
00540   // Add variable to the set of CNF vars
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   // phi <=> v
00551   addToCNFCache(result);
00552   applyCNFRules(result);
00553   TRACE_MSG("mycnf", "enqueueCNFrec => }");
00554 }
00555 
00556 
00557 /*!
00558  * \param thm is the input of the form phi <=> v
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   // Eliminate negation first
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   // Catch the trivial case v1 <=> v2
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   // Check the kids in e[0], replace them with cache[e[0][i]], rebuild thm
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   // Create a new variable for this child
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   // FIXME: eliminate this once debugged
00668   Theorem clauses(result);
00669 
00670   // Enqueue the clauses
00671   DebugAssert(!clauses.isNull(), "Oops!..");
00672   DebugAssert(clauses.getExpr().isAnd(), "clauses = "
00673         +clauses.getExpr().toString());
00674 
00675   // The clauses may containt term ITEs, and we need to translate those
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   // Check for var being an auxiliary CNF variable
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   // Record the CNF variable
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   //d_cnfCache.insert(phi, t);
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   // Strip all the top-level negations from e
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     // IF_DEBUG(debugger.counter("CNF cache hits")++);
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     // Now put all the negations back.  If the number of negations is
00768     // odd, first transform phi<=>v into !phi<=>!v.  Then apply
00769     // !!phi<=>phi rewrite as many times as needed.
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  * Strategy:
00789  *
00790  * For a given atomic formula phi(ite(c, t1, t2)) which depends on a
00791  * term ITE, generate an equisatisfiable formula:
00792  *
00793  * phi(x) & ite(c, t1=x, t2=x),
00794  *
00795  * where x is a new variable.
00796  *
00797  * The phi(x) part will be generated by the caller, and our job is to
00798  * assert the 'ite(c, t1=x, t2=x)', and return a rewrite theorem
00799  * phi(ite(c, t1, t2)) <=> phi(x).
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   // If 'res' is e<=>phi, and the resulting formula phi is not a
00820   // literal, introduce a new variable x, enqueue phi<=>x, and return
00821   // e<=>x.
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       //d_cnfVars[var.getExpr()] = true;
00832       //addCNFFact(var);
00833       addToCNFCache(varThm);
00834     }
00835     applyCNFRules(varThm);
00836     //enqueueCNFrec(varThm);
00837     res = d_commonRules->transitivityRule(res, varThm);
00838   }
00839   
00840   d_replaceITECache[e] = res;
00841   
00842   TRACE("replaceITE", "replaceITE => ", res, " }");
00843   return res;
00844 }

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