00001
00002
00003
00004
00005
00006
00007
00008
00009
00010
00011
00012
00013
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;
00062 if (!e.isNull())
00063 {
00064 d_height = e.getHeight() - 1;
00065
00066
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)
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 }