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

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);