From b480438b3d39000cfac88eac12922a23f9fccbea Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Tue, 12 Mar 2013 19:41:28 -0400
Subject: Fix to bug 497: make justification heuristic's ITE cache
 context-dependent.

---
 src/decision/justification_heuristic.h | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'src/decision/justification_heuristic.h')

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);
-- 
cgit v1.2.3