Fix performance issue in a DFS search (bug 474)

diff --git a/src/decision/justification_heuristic.cpp b/src/decision/justification_heuristic.cpp
index 494da72bf3e38b19c20cfb09ab097be954a54e73..46ec6f09fc3f96552d5b5d8149462f76ae496a87 100644 (file)
--- a/src/decision/justification_heuristic.cpp
+++ b/src/decision/justification_heuristic.cpp
@@ -70,13 +70,17 @@ SatValue JustificationHeuristic::tryGetSatValue(Node n)
 void JustificationHeuristic::computeITEs(TNode n, IteList &l)
 {
   Trace("jh-ite") << " computeITEs( " << n << ", &l)\n";
+  d_visitedComputeITE.insert(n);
   for(unsigned i=0; i<n.getNumChildren(); ++i) {
     SkolemMap::iterator it2 = d_iteAssertions.find(n[i]);
     if(it2 != d_iteAssertions.end()) {
       l.push_back(make_pair(n[i], (*it2).second));
       Assert(n[i].getNumChildren() == 0);
     }
-    computeITEs(n[i], l);
+    if(d_visitedComputeITE.find(n[i]) ==
+         d_visitedComputeITE.end()) {
+      computeITEs(n[i], l);
+    }
   }
 }
 
@@ -89,6 +93,7 @@ const JustificationHeuristic::IteList& JustificationHeuristic::getITEs(TNode n)
     // Compute the list of ITEs
     // TODO: optimize by avoiding multiple lookup for d_iteCache[n]
     d_iteCache[n] = IteList();
+    d_visitedComputeITE.clear();
     computeITEs(n, d_iteCache[n]);
     return d_iteCache[n];
   }

diff --git a/src/decision/justification_heuristic.h b/src/decision/justification_heuristic.h
index a1b29ed47bf0b84112293a01b3cd70c383f60934..ea67fee29ffb4cf6484a513ea04328f116cd2670 100644 (file)
--- a/src/decision/justification_heuristic.h
+++ b/src/decision/justification_heuristic.h
@@ -78,6 +78,12 @@ class JustificationHeuristic : public ITEDecisionStrategy {
    * term-ITE.
    */
   hash_set<TNode,TNodeHashFunction> d_visited;
+
+  /**
+   * Set to track visited nodes in a dfs search done in computeITE
+   * function
+   */
+  hash_set<TNode,TNodeHashFunction> d_visitedComputeITE;
 public:
   JustificationHeuristic(CVC4::DecisionEngine* de,
                          context::Context *uc,