diff options
author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2012-12-06 16:31:56 -0500 |
---|---|---|
committer | François Bobot <francois@bobot.eu> | 2012-12-07 09:27:57 +0100 |
commit | bd28a94095d8aebe4eb70fedcbe0f511edd38b0b (patch) | |
tree | 76dab80e926e8fc2dd909bed476fee2681da82e3 /src | |
parent | e90877c392971112636cf28d521d1fd525824009 (diff) |
Fix performance issue in a DFS search (bug 474)
(cherry picked from commit f056522a587d1b080224992355be070b73d97a3b)
Diffstat (limited to 'src')
-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), |