From: Kshitij Bansal Date: Wed, 30 Apr 2014 20:09:32 +0000 (-0400) Subject: decision engine: cache start index for and/or nodes X-Git-Tag: cvc5-1.0.0~6940 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=cb12e628b41d11376ff03e5c1a7a5e760e98e2a1;p=cvc5.git 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 --- 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 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);