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/decision/justification_heuristic.h | |
| parent | e90877c392971112636cf28d521d1fd525824009 (diff) | |
Fix performance issue in a DFS search (bug 474)
(cherry picked from commit f056522a587d1b080224992355be070b73d97a3b)
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 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), |