00001
00002
00003
00004
00005
00006
00007
00008
00009
00010
00011
00012
00013
00014
00015
00016
00017
00018
00019 #include "decision_engine_mbtf.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 DecisionEngineMBTF::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 >= d_height) &&
00038 (it2 == d_index.end() ||
00039 d_cache[it1->second].d_rank < d_cache[it2->second].d_rank))
00040 return true;
00041 else
00042 return false;
00043 }
00044
00045
00046 DecisionEngineMBTF::DecisionEngineMBTF(TheoryCore* core, SearchImplBase* se)
00047 : DecisionEngine(core, se),
00048 d_startLevel(core->getCM()->scopeLevel()),
00049 d_bottomLevel(0),
00050 d_topLevel(0),
00051 d_topLevelLock(false),
00052 d_height(0),
00053 d_cache(CACHE_SIZE)
00054 {
00055 }
00056
00057
00058 Expr DecisionEngineMBTF::findSplitter(const Expr& e) {
00059 d_visited.clear();
00060 Expr splitter;
00061 if (!e.isNull())
00062 {
00063 d_height = e.getHeight() - 1;
00064
00065
00066
00067 if (!d_topLevelLock)
00068 {
00069 d_topLevel = d_core->getCM()->scopeLevel();
00070 d_topLevelLock = true;
00071 }
00072
00073 splitter = findSplitterRec(e);
00074 DebugAssert(!splitter.isNull(),
00075 "findSplitter: can't find splitter in non-literal: "
00076 + e.toString());
00077 IF_DEBUG(debugger.counter("splitters from non-literals")++);
00078 }
00079 TRACE("splitters verbose", "findSplitter() => ", splitter, "");
00080 return splitter;
00081 }
00082
00083
00084 void DecisionEngineMBTF::goalSatisfied()
00085 {
00086 if (d_core->getCM()->scopeLevel() - d_bottomLevel != 0)
00087 {
00088 d_bottomLevel = d_core->getCM()->scopeLevel();
00089 return;
00090 }
00091
00092 if (d_splitters.size() == 0)
00093 return;
00094
00095 if (!d_topLevelLock)
00096 d_topLevel = d_bottomLevel - 1;
00097 d_topLevelLock = false;
00098
00099 int numSplitters = d_bottomLevel - d_startLevel - 1;
00100 int numNewSplitters = d_bottomLevel - d_topLevel;
00101
00102 vector<CacheEntry> newCache(numSplitters);
00103 ExprMap<int> newIndex;
00104
00105 int end = d_splitters.size();
00106 int start = end - numSplitters;
00107 if (start < 0)
00108 start = 0;
00109
00110 const Expr& s = d_splitters[max(0, end - numNewSplitters)];
00111 Expr topSplitter = s.getSimpFrom();
00112 if(!topSplitter.isAbsAtomicFormula()) topSplitter = s;
00113
00114 ExprMap<int>::iterator it = d_index.find(topSplitter);
00115 int maxTrust = (it != d_index.end()) ? d_cache[it->second].d_trust : numSplitters;
00116
00117 for (int i = end - 1, j = 0; i >= start; i--, j++)
00118 {
00119 const Expr& s = d_splitters[i];
00120 Expr splitter = s.getSimpFrom();
00121 if(!splitter.isAbsAtomicFormula()) splitter = s;
00122 newCache[j].d_expr = splitter;
00123 newCache[j].d_rank = (numSplitters - j) % numSplitters;
00124 newIndex[splitter] = j;
00125
00126 ExprMap<int>::iterator it = d_index.find(splitter);
00127 if (j == 0)
00128 newCache[j].d_trust = maxTrust;
00129 else if (it != d_index.end())
00130 newCache[j].d_trust = max(d_cache[it->second].d_trust - 1, 0);
00131 }
00132
00133 d_cache = newCache;
00134 d_index = newIndex;
00135 d_bestByExpr.clear();
00136 }