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.h | |
| parent | 323d5faa1fcd6657899dabfed2e4ad455c92f5c4 (diff) | |
Fix performance issue in a DFS search (bug 474)
Diffstat (limited to 'src/decision/justification_heuristic.h')
| -rw-r--r-- | src/decision/justification_heuristic.h | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/src/decision/justification_heuristic.h b/src/decision/justification_heuristic.h index a1b29ed47..ea67fee29 100644 --- 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, |