CVC3

decision_engine.cpp

Go to the documentation of this file.
00001 /*****************************************************************************/
00002 /*!
00003  * \file decision_engine.cpp
00004  * \brief Decision Engine
00005  * 
00006  * Author: Clark Barrett
00007  * 
00008  * Created: Sun Jul 13 22:44:55 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 
00023 #include "decision_engine.h"
00024 #include "theory_core.h"
00025 #include "search.h"
00026 
00027 
00028 using namespace std;
00029 using namespace CVC3;
00030 
00031 
00032 DecisionEngine::DecisionEngine(TheoryCore* core, SearchImplBase* se)
00033   : d_core(core), d_se(se),
00034     d_splitters(core->getCM()->getCurrentContext()),
00035     d_splitterCount(core->getStatistics().counter("splitters"))
00036 {
00037   IF_DEBUG(d_splitters.setName("CDList[SearchEngineDefault.d_splitters]");)
00038 }
00039 
00040 /*****************************************************************************/
00041 /*!
00042  * Function: DecisionEngine::findSplitterRec
00043  *
00044  * Author: Clark Barrett
00045  *
00046  * Created: Sun Jul 13 22:47:06 2003
00047  *
00048  * Search the expression e (depth-first) for an atomic formula.  Note that in
00049  * order to support the "simplify in-place" option, each sub-expression is
00050  * checked to see if it has a find pointer, and if it does, the find is
00051  * followed instead of continuing to recurse on the given expression.
00052  * \return a NULL expr if no atomic formula is found.
00053  */
00054 /*****************************************************************************/
00055 Expr DecisionEngine::findSplitterRec(const Expr& e)
00056 {
00057   Expr best;
00058 
00059   if(d_visited.count(e) > 0)
00060     return d_visited[e];
00061 
00062   if (e.isTrue() || e.isFalse() || e.isAtomic()
00063       || !d_se->isGoodSplitter(e)) {
00064     d_visited[e] = best;
00065     return best;
00066   }
00067 
00068   if (e.isAbsAtomicFormula()) {
00069     d_visited[e] = e;
00070     return e;
00071   }
00072 
00073   ExprMap<Expr>::iterator it = d_bestByExpr.find(e);
00074   if (it != d_bestByExpr.end()) {
00075     d_visited[e] = it->second;
00076     return it->second;
00077   }
00078 
00079   vector<int> order(e.arity());
00080   int i = 0;
00081 
00082   if (e.isITE())
00083   {
00084     order[i++] = 0;
00085     order[i++] = 1;//e.getHighestKid(); // always 1 or 2
00086     order[i++] = 2;//3 - e.getHighestKid();
00087   }
00088 
00089   else
00090   {
00091     if (e.arity() > 0)
00092     {
00093       order[i++] = 0;//e.getHighestKid();
00094       for (int k = 0; k < e.arity(); ++k)
00095   if (k != 0)//e.getHighestKid())
00096     order[i++] = k;
00097     }
00098   }
00099 
00100   for (int k = 0; k < e.arity(); k++)
00101   {
00102     Expr splitter =
00103       findSplitterRec(d_core->findExpr(e[order[k]]));
00104     if (!splitter.isNull() && (best.isNull() || isBetter(splitter, best)))
00105       best = splitter;
00106   }
00107 
00108   d_bestByExpr[e] = best;
00109   d_visited[e] = best;
00110   return best;
00111 }
00112 
00113 
00114 /*****************************************************************************/
00115 /*!
00116  * Function: DecisionEngine::pushDecision
00117  *
00118  * Author: Clark Barrett
00119  *
00120  * Created: Sun Jul 13 22:55:16 2003
00121  *
00122  * \param splitter 
00123  * \param whichCase If true, increment the splitter count and assert the
00124  * splitter.  If false, do NOT increment the splitter count and assert the
00125  * negation of the splitter.  Defaults to true.
00126  */
00127 /*****************************************************************************/
00128 void DecisionEngine::pushDecision(Expr splitter, bool whichCase)
00129 {
00130   string stCase = whichCase ? "TRUE" : "FALSE";
00131   if (whichCase) d_splitterCount++;
00132   d_core->getCM()->push();
00133   TRACE("search trace", "Asserting splitter("+stCase+"): ", splitter, "");
00134   TRACE("search", "Asserting splitter("+stCase+"): ", splitter, "");
00135   d_splitters.push_back(splitter);
00136   if (!whichCase)
00137     splitter = splitter.negate();
00138   Theorem thm = d_se->newIntAssumption(splitter);
00139   d_core->addFact(thm);
00140   // Search engine needs to know what original facts it derived or
00141   // split on, so that we don't split on them twice.  addFact() may
00142   // simplify these facts before calling addLiteralFact() and lose
00143   // this information.  There is no reason to add non-literals though,
00144   // as we never split on them directly.
00145   if(thm.getExpr().isAbsLiteral())
00146     d_se->addLiteralFact(thm);
00147 }
00148 
00149 
00150 void DecisionEngine::popDecision()
00151 {
00152   d_core->getCM()->pop();
00153   TRACE("search trace", "Pop: scope level =", d_core->getCM()->scopeLevel(), "");
00154 }
00155 
00156 
00157 void DecisionEngine::popTo(int dl)
00158 {
00159   d_core->getCM()->popto(dl);
00160   TRACE("search trace", "Popto: scope level =", d_core->getCM()->scopeLevel(), "");
00161 }
00162 
00163 
00164 Expr DecisionEngine::lastSplitter()
00165 {
00166   return d_splitters.back();
00167 }