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

1 files changed, 10 insertions, 0 deletions

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