Fix to bug 497: make justification heuristic's ITE cache context-dependent.

4 files changed, 19 insertions, 18 deletions

diff --git a/src/decision/decision_engine.cpp b/src/decision/decision_engine.cpp
index 08a3e49d0..98294f92b 100644
--- a/src/decision/decision_engine.cpp
+++ b/src/decision/decision_engine.cpp
@@ -29,7 +29,7 @@ using namespace std;
 namespace CVC4 {
 
 DecisionEngine::DecisionEngine(context::Context *sc,
-                                 context::Context *uc) :
+                               context::UserContext *uc) :
   d_enabledStrategies(),
   d_needIteSkolemMap(),
   d_relevancyStrategy(NULL),
diff --git a/src/decision/decision_engine.h b/src/decision/decision_engine.h
index ea16cec16..859443d00 100644
--- a/src/decision/decision_engine.h
+++ b/src/decision/decision_engine.h
@@ -50,7 +50,7 @@ class DecisionEngine {
   DPLLSatSolverInterface* d_satSolver;
 
   context::Context* d_satContext;
-  context::Context* d_userContext;
+  context::UserContext* d_userContext;
 
   // Does decision engine know the answer?
   context::CDO<SatValue> d_result;
@@ -64,7 +64,7 @@ public:
   // Necessary functions
 
   /** Constructor */
-  DecisionEngine(context::Context *sc, context::Context *uc);
+  DecisionEngine(context::Context *sc, context::UserContext *uc);
 
   /** Destructor, currently does nothing */
   ~DecisionEngine() {
diff --git a/src/decision/justification_heuristic.cpp b/src/decision/justification_heuristic.cpp
index 0b63dfbe1..b77d3ba6b 100644
--- a/src/decision/justification_heuristic.cpp
+++ b/src/decision/justification_heuristic.cpp
@@ -28,7 +28,7 @@
 using namespace CVC4;
 
 JustificationHeuristic::JustificationHeuristic(CVC4::DecisionEngine* de,
-                                               context::Context *uc,
+                                               context::UserContext *uc,
                                                context::Context *c):
   ITEDecisionStrategy(de, c),
   d_justified(c),
@@ -38,7 +38,7 @@ JustificationHeuristic::JustificationHeuristic(CVC4::DecisionEngine* de,
   d_timestat("decision::jh::time"),
   d_assertions(uc),
   d_iteAssertions(uc),
-  d_iteCache(),
+  d_iteCache(uc),
   d_visited(),
   d_visitedComputeITE(),
   d_curDecision() {
@@ -199,19 +199,20 @@ SatValue JustificationHeuristic::tryGetSatValue(Node n)
   }//end of else
 }
 
-const JustificationHeuristic::IteList&
+JustificationHeuristic::IteList
 JustificationHeuristic::getITEs(TNode n)
 {
   IteCache::iterator it = d_iteCache.find(n);
   if(it != d_iteCache.end()) {
-    return it->second;
+    return (*it).second;
   } else {
     // 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];
+    IteList ilist;
+    computeITEs(n, ilist);
+    d_iteCache.insert(n, ilist);
+    return ilist;
   }
 }
 
@@ -462,15 +463,15 @@ bool JustificationHeuristic::handleITE(TNode node, SatValue desiredVal)
 
 bool JustificationHeuristic::handleEmbeddedITEs(TNode node)
 {
-  const IteList& l = getITEs(node);
+  const IteList l = getITEs(node);
   Trace("decision::jh::ite") << " ite size = " << l.size() << std::endl;
 
   for(IteList::const_iterator i = l.begin(); i != l.end(); ++i) {
-    if(d_visited.find(i->first) == d_visited.end()) {
-      d_visited.insert(i->first);
-      if(findSplitterRec(i->second, SAT_VALUE_TRUE))
+    if(d_visited.find((*i).first) == d_visited.end()) {
+      d_visited.insert((*i).first);
+      if(findSplitterRec((*i).second, SAT_VALUE_TRUE))
         return true;
-      d_visited.erase(i->first);
+      d_visited.erase((*i).first);
     }
   }
   return false;
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);