diff options
author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2012-12-06 16:31:56 -0500 |
---|---|---|
committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2012-12-06 16:31:56 -0500 |
commit | f056522a587d1b080224992355be070b73d97a3b (patch) | |
tree | 96a0000435020e9a77a8b2ec0e9e435c48c42a80 /src/decision/justification_heuristic.cpp | |
parent | 323d5faa1fcd6657899dabfed2e4ad455c92f5c4 (diff) |
Fix performance issue in a DFS search (bug 474)
Diffstat (limited to 'src/decision/justification_heuristic.cpp')
-rw-r--r-- | src/decision/justification_heuristic.cpp | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/src/decision/justification_heuristic.cpp b/src/decision/justification_heuristic.cpp index 494da72bf..46ec6f09f 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]; } |