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.

1 files changed, 3 insertions, 3 deletions

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;