From 7f52115ab0dcba4c8ba9403a5f25b8e8c588911a Mon Sep 17 00:00:00 2001
From: Tim King <taking@cs.nyu.edu>
Date: Wed, 5 Dec 2012 19:06:21 +0000
Subject: This commit merges in CDTrailHashMap and CDInsertHashMap. CDHashSet
 now uses CDInsertHashMap. CDHashSet<TNode> have been changed to
 CDHashSet<Node>.  Switching CnfStream to use CDInsertSet. Switches a few
 CDHashMaps in arithmetic to use CDTrailHashMap. Documentation changes to
 CDHashMap.

---
 src/decision/justification_heuristic.h | 6 +++---
 src/decision/relevancy.h               | 2 +-
 2 files changed, 4 insertions(+), 4 deletions(-)

(limited to 'src/decision')

diff --git a/src/decision/justification_heuristic.h b/src/decision/justification_heuristic.h
index adccc0d55..a1b29ed47 100644
--- a/src/decision/justification_heuristic.h
+++ b/src/decision/justification_heuristic.h
@@ -49,7 +49,7 @@ class JustificationHeuristic : public ITEDecisionStrategy {
   typedef context::CDHashMap<TNode,TNode,TNodeHashFunction> SkolemMap;
 
   // being 'justified' is monotonic with respect to decisions
-  typedef context::CDHashSet<TNode,TNodeHashFunction> JustifiedSet;
+  typedef context::CDHashSet<Node,NodeHashFunction> JustifiedSet;
   JustifiedSet d_justified;
   context::CDO<unsigned>  d_prvsIndex;
 
@@ -107,8 +107,8 @@ public:
     d_visited.clear();
 
     if(Trace.isOn("justified")) {
-      for(JustifiedSet::iterator i = d_justified.begin();
-          i != d_justified.end(); ++i) {
+      for(JustifiedSet::key_iterator i = d_justified.key_begin();
+          i != d_justified.key_end(); ++i) {
         TNode n = *i;
         SatLiteral l = d_decisionEngine->hasSatLiteral(n) ?
           d_decisionEngine->getSatLiteral(n) : -1;
diff --git a/src/decision/relevancy.h b/src/decision/relevancy.h
index 8a6eb54ef..bfd30ddde 100644
--- a/src/decision/relevancy.h
+++ b/src/decision/relevancy.h
@@ -60,7 +60,7 @@ class Relevancy : public RelevancyStrategy {
   typedef hash_map<TNode,SatValue,TNodeHashFunction> PolarityCache;
 
   // being 'justified' is monotonic with respect to decisions
-  context::CDHashSet<TNode,TNodeHashFunction> d_justified;
+  context::CDHashSet<Node, NodeHashFunction> d_justified;
   context::CDO<unsigned>  d_prvsIndex;
 
   IntStat d_helfulness;
-- 
cgit v1.2.3