diff options
| author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-03-12 19:41:28 -0400 |
|---|---|---|
| committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-03-20 20:00:55 -0400 |
| commit | b480438b3d39000cfac88eac12922a23f9fccbea (patch) | |
| tree | ab310d8512298a733f8e2d8f4805d06ee126208e /src/decision/justification_heuristic.h | |
| parent | 6106f021745ffc7ebc068f762a196140deb9d48d (diff) | |
Fix to bug 497: make justification heuristic's ITE cache context-dependent.
Diffstat (limited to 'src/decision/justification_heuristic.h')
| -rw-r--r-- | src/decision/justification_heuristic.h | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/src/decision/justification_heuristic.h b/src/decision/justification_heuristic.h index 91c21d981..d8f9a15a8 100644 --- a/src/decision/justification_heuristic.h +++ b/src/decision/justification_heuristic.h @@ -38,7 +38,7 @@ namespace decision { class JustificationHeuristic : public ITEDecisionStrategy { typedef std::vector<pair<TNode,TNode> > IteList; - typedef hash_map<TNode,IteList,TNodeHashFunction> IteCache; + typedef context::CDHashMap<TNode,IteList,TNodeHashFunction> IteCache; typedef context::CDHashMap<TNode,TNode,TNodeHashFunction> SkolemMap; // being 'justified' is monotonic with respect to decisions @@ -82,7 +82,7 @@ class JustificationHeuristic : public ITEDecisionStrategy { SatLiteral d_curDecision; public: JustificationHeuristic(CVC4::DecisionEngine* de, - context::Context *uc, + context::UserContext *uc, context::Context *c); ~JustificationHeuristic(); @@ -110,7 +110,7 @@ private: SatValue tryGetSatValue(Node n); /* Get list of all term-ITEs for the atomic formula v */ - const JustificationHeuristic::IteList& getITEs(TNode n); + JustificationHeuristic::IteList getITEs(TNode n); /* Compute all term-ITEs in a node recursively */ void computeITEs(TNode n, IteList &l); |