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