decision_engine_caching.cpp

Go to the documentation of this file.
00001 /*****************************************************************************/
00002 /*!
00003  * \file decision_engine_caching.cpp
00004  * \brief Decision Engine
00005  * 
00006  * <hr>
00007  *
00008  * License to use, copy, modify, sell and/or distribute this software
00009  * and its documentation for any purpose is hereby granted without
00010  * royalty, subject to the terms and conditions defined in the \ref
00011  * LICENSE file provided with this distribution.
00012  * 
00013  * <hr>
00014  * 
00015  */
00016 /*****************************************************************************/
00017 
00018 
00019 #include "decision_engine_caching.h"
00020 #include "theory_core.h"
00021 #include "search.h"
00022 
00023 
00024 using namespace std;
00025 using namespace CVC3;
00026 
00027 #define CACHE_SIZE 20
00028 #define BASE_TRUST_LEVEL 2
00029 #define TURNOVER_RATE 10
00030 
00031 bool DecisionEngineCaching::isBetter(const Expr& e1, const Expr& e2)
00032 {
00033   ExprMap<int>::iterator it1 = d_index.find(e1.getSimpFrom());
00034   ExprMap<int>::iterator it2 = d_index.find(e2.getSimpFrom());
00035 
00036   if (it1 != d_index.end() &&
00037       (d_cache[it1->second].d_trust + BASE_TRUST_LEVEL >= d_height) &&
00038       (it2 == d_index.end() ||
00039        d_cache[it1->second].d_rank < d_cache[it2->second].d_rank ||
00040        d_cache[it2->second].d_trust + BASE_TRUST_LEVEL < d_height))
00041     return true;
00042   else
00043     return false;
00044 }
00045 
00046 
00047 DecisionEngineCaching::DecisionEngineCaching(TheoryCore* core, SearchImplBase* se)
00048   : DecisionEngine(core, se),
00049     d_startLevel(core->getCM()->scopeLevel()),
00050     d_bottomLevel(0),
00051     d_topLevel(0),
00052     d_topLevelLock(false),
00053     d_height(0),
00054     d_cache(CACHE_SIZE)
00055 {
00056 }
00057 
00058 
00059 Expr DecisionEngineCaching::findSplitter(const Expr& e) {
00060   d_visited.clear();
00061   Expr splitter; // Null by default
00062   if (!e.isNull())
00063   {
00064     d_height = e.getHeight() - 1;
00065     // heights seem to be 1 greater than SVC
00066     // probably because of top-level NOT
00067 
00068     if (!d_topLevelLock)
00069     {
00070       d_topLevel = d_core->getCM()->scopeLevel();
00071       d_topLevelLock = true;
00072     }
00073 
00074     splitter = findSplitterRec(e);
00075     DebugAssert(!splitter.isNull(),
00076     "findSplitter: can't find splitter in non-literal: "
00077     + e.toString());
00078     IF_DEBUG(debugger.counter("splitters from non-literals")++);
00079   }
00080   TRACE("splitters verbose", "findSplitter() => ", splitter, "");
00081   return splitter;
00082 }
00083 
00084 
00085 void DecisionEngineCaching::goalSatisfied()
00086 {
00087   if (d_core->getCM()->scopeLevel() - d_bottomLevel != 0)
00088   {
00089     d_bottomLevel = d_core->getCM()->scopeLevel();
00090     return;
00091   }
00092 
00093   if (d_splitters.size() == 0)
00094     return;
00095 
00096   if (!d_topLevelLock)
00097     d_topLevel = d_bottomLevel - 1;
00098   d_topLevelLock = false;
00099 
00100   int numInterestingSplitters = min(d_bottomLevel - d_startLevel - 1, TURNOVER_RATE);
00101   int numSplitters = min(CACHE_SIZE, numInterestingSplitters);
00102 
00103   vector<CacheEntry> newCache(CACHE_SIZE);
00104   ExprMap<int> newIndex;
00105 
00106   int end = d_splitters.size();
00107   int start = end - numSplitters;
00108   if (start < 0)
00109     start = 0;
00110 
00111   for (int i = end - 1, j = 0; i >= start; i--, j++)
00112   {
00113     const Expr& s = d_splitters[i];
00114     Expr splitter = s.getSimpFrom();
00115     if(!splitter.isAbsAtomicFormula()) splitter = s;
00116     newCache[j].d_expr = splitter;
00117     newCache[j].d_rank = (numSplitters - j) % numSplitters;
00118     newIndex[splitter] = j;
00119 
00120     ExprMap<int>::iterator it = d_index.find(splitter);
00121     if (it != d_index.end())
00122     {
00123       if (j == 0) // the effective splitter
00124   newCache[j].d_trust = d_cache[it->second].d_trust + 1;
00125       else
00126   newCache[j].d_trust = d_cache[it->second].d_trust;
00127     }
00128   }
00129 
00130   int i = numSplitters;
00131   int rank = numSplitters;
00132   for (int j = 0; i < CACHE_SIZE && !d_cache[j].d_expr.isNull(); j++)
00133   {
00134     if (!newIndex.count(d_cache[j].d_expr))
00135     {
00136       newCache[i] = d_cache[j];
00137       newCache[i].d_rank = rank++;
00138       newIndex[newCache[i].d_expr] = i;
00139       i++;
00140     }
00141   }
00142 
00143   d_cache = newCache;
00144   d_index = newIndex;
00145   d_bestByExpr.clear();
00146 }

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