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

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