diff options
Diffstat (limited to 'src/decision')
-rw-r--r-- | src/decision/justification_heuristic.cpp | 7 | ||||
-rw-r--r-- | src/decision/justification_heuristic.h | 6 |
2 files changed, 12 insertions, 1 deletions
diff --git a/src/decision/justification_heuristic.cpp b/src/decision/justification_heuristic.cpp index ba8ab91b7..4ec4588f3 100644 --- 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 a3b05b1bb..de6bf5095 100644 --- a/src/decision/justification_heuristic.h +++ b/src/decision/justification_heuristic.h @@ -76,6 +76,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 *c): ITEDecisionStrategy(de, c), |