diff options
author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-04-30 16:09:32 -0400 |
---|---|---|
committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-04-30 23:50:09 -0400 |
commit | cb12e628b41d11376ff03e5c1a7a5e760e98e2a1 (patch) | |
tree | cc9b80787200a7ed06ae1d11ecf5a4a1b7d1cfbf /src | |
parent | 221e509c0eb230aa549fe0107ba88514b6944ca2 (diff) |
decision engine: cache start index for and/or nodes
This is done only in "hard" case. Limited testing has not shown
improvement in the "easy" case.
This was triggerred by a benchmark sent by andy/viktor.
performance comparison notes for the change on wiki
http://church.cims.nyu.edu/wiki/User:Kshitij/decisioncacheindex
Diffstat (limited to 'src')
-rw-r--r-- | src/decision/justification_heuristic.cpp | 20 | ||||
-rw-r--r-- | src/decision/justification_heuristic.h | 10 |
2 files changed, 26 insertions, 4 deletions
diff --git a/src/decision/justification_heuristic.cpp b/src/decision/justification_heuristic.cpp index 54d2dee97..dc57fd5f9 100644 --- a/src/decision/justification_heuristic.cpp +++ b/src/decision/justification_heuristic.cpp @@ -47,7 +47,8 @@ JustificationHeuristic::JustificationHeuristic(CVC4::DecisionEngine* de, d_curDecision(), d_curThreshold(0), d_childCache(uc), - d_weightCache(uc) { + d_weightCache(uc), + d_startIndexCache(c) { StatisticsRegistry::registerStat(&d_helfulness); StatisticsRegistry::registerStat(&d_giveup); StatisticsRegistry::registerStat(&d_timestat); @@ -556,14 +557,22 @@ JustificationHeuristic::handleAndOrEasy(TNode node, SatValue desiredVal) TNode curNode = getChildByWeight(node, i, desiredVal); if ( tryGetSatValue(curNode) != desiredValInverted ) { SearchResult ret = findSplitterRec(curNode, desiredVal); - if(ret != DONT_KNOW) + if(ret != DONT_KNOW) { return ret; + } } } Assert(d_curThreshold != 0, "handleAndOrEasy: No controlling input found"); return DONT_KNOW; } +int JustificationHeuristic::getStartIndex(TNode node) { + return d_startIndexCache[node]; +} +void JustificationHeuristic::saveStartIndex(TNode node, int val) { + d_startIndexCache[node] = val; +} + JustificationHeuristic::SearchResult JustificationHeuristic::handleAndOrHard(TNode node, SatValue desiredVal) { Assert( (node.getKind() == kind::AND and desiredVal == SAT_VALUE_TRUE) or @@ -571,11 +580,14 @@ JustificationHeuristic::SearchResult JustificationHeuristic::handleAndOrHard(TNo int numChildren = node.getNumChildren(); bool noSplitter = true; - for(int i = 0; i < numChildren; ++i) { + int i_st = getStartIndex(node); + for(int i = i_st; i < numChildren; ++i) { TNode curNode = getChildByWeight(node, i, desiredVal); SearchResult ret = findSplitterRec(curNode, desiredVal); - if (ret == FOUND_SPLITTER) + if (ret == FOUND_SPLITTER) { + if(i != i_st) saveStartIndex(node, i); return FOUND_SPLITTER; + } noSplitter = noSplitter && (ret == NO_SPLITTER); } return noSplitter ? NO_SPLITTER : DONT_KNOW; diff --git a/src/decision/justification_heuristic.h b/src/decision/justification_heuristic.h index 01458d9ea..2969c4b86 100644 --- a/src/decision/justification_heuristic.h +++ b/src/decision/justification_heuristic.h @@ -154,6 +154,16 @@ private: /* Get list of all term-ITEs for the atomic formula v */ JustificationHeuristic::IteList getITEs(TNode n); + + /** + * For big and/or nodes, a cache to save starting index into children + * for efficiently. + */ + typedef context::CDHashMap<TNode, int, TNodeHashFunction> StartIndexCache; + StartIndexCache d_startIndexCache; + int getStartIndex(TNode node); + void saveStartIndex(TNode node, int val); + /* Compute all term-ITEs in a node recursively */ void computeITEs(TNode n, IteList &l); |