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.

4 files changed, 12 insertions, 13 deletions

diff --git a/src/theory/arith/arith_static_learner.cpp b/src/theory/arith/arith_static_learner.cpp
index 5b8d3befc..9ae7cd1c2 100644
--- a/src/theory/arith/arith_static_learner.cpp
+++ b/src/theory/arith/arith_static_learner.cpp
@@ -145,8 +145,8 @@ void ArithStaticLearner::process(TNode n, NodeBuilder<>& learned, const TNodeSet
     break;
   case CONST_RATIONAL:
     // Mark constants as minmax
-    d_minMap[n] = n.getConst<Rational>();
-    d_maxMap[n] = n.getConst<Rational>();
+    d_minMap.insert(n, n.getConst<Rational>());
+    d_maxMap.insert(n, n.getConst<Rational>());
     break;
   case OR: {
     // Look for things like "x = 0 OR x = 1" (that are defTrue) and
@@ -248,7 +248,7 @@ void ArithStaticLearner::iteConstant(TNode n, NodeBuilder<>& learned){
     DeltaRational min = std::min(first, second);
     CDNodeToMinMaxMap::const_iterator minFind = d_minMap.find(n);
     if (minFind == d_minMap.end() || (*minFind).second < min) {
-      d_minMap[n] = min;
+      d_minMap.insert(n, min);
       Node nGeqMin;
       if (min.getInfinitesimalPart() == 0) {
         nGeqMin = NodeBuilder<2>(kind::GEQ) << n << mkRationalNode(min.getNoninfinitesimalPart());
@@ -267,7 +267,7 @@ void ArithStaticLearner::iteConstant(TNode n, NodeBuilder<>& learned){
     DeltaRational max = std::max(first, second);
     CDNodeToMinMaxMap::const_iterator maxFind = d_maxMap.find(n);
     if (maxFind == d_maxMap.end() || (*maxFind).second > max) {
-      d_maxMap[n] = max;
+      d_maxMap.insert(n, max);
       Node nLeqMax;
       if (max.getInfinitesimalPart() == 0) {
         nLeqMax = NodeBuilder<2>(kind::LEQ) << n << mkRationalNode(max.getNoninfinitesimalPart());
@@ -398,7 +398,7 @@ void ArithStaticLearner::addBound(TNode n) {
     /* fall through */
   case kind::LEQ:
     if (maxFind == d_maxMap.end() || (*maxFind).second > bound) {
-      d_maxMap[n[0]] = bound;
+      d_maxMap.insert(n[0], bound);
       Debug("arith::static") << "adding bound " << n << endl;
     }
     break;
@@ -407,7 +407,7 @@ void ArithStaticLearner::addBound(TNode n) {
     /* fall through */
   case kind::GEQ:
     if (minFind == d_minMap.end() || (*minFind).second < bound) {
-      d_minMap[n[0]] = bound;
+      d_minMap.insert(n[0], bound);
       Debug("arith::static") << "adding bound " << n << endl;
     }
     break;
diff --git a/src/theory/arith/arith_static_learner.h b/src/theory/arith/arith_static_learner.h
index b047018e8..0de28c5ab 100644
--- a/src/theory/arith/arith_static_learner.h
+++ b/src/theory/arith/arith_static_learner.h
@@ -27,7 +27,7 @@
 
 #include "context/context.h"
 #include "context/cdlist.h"
-#include "context/cdhashmap.h"
+#include "context/cdtrail_hashmap.h"
 #include <set>
 
 namespace CVC4 {
@@ -41,8 +41,7 @@ private:
    *  (=> _ (= x c))
    * where c is a constant.
    */
-  //typedef __gnu_cxx::hash_map<Node, std::set<Node>, NodeHashFunction> VarToNodeSetMap;
-  typedef context::CDHashMap<Node, Node, NodeHashFunction> CDNodeToNodeListMap;
+  typedef context::CDTrailHashMap<Node, Node, NodeHashFunction> CDNodeToNodeListMap;
   // The domain is an implicit list OR(x, OR(y, ..., FALSE ))
   // or FALSE
   CDNodeToNodeListMap d_miplibTrick;
@@ -50,8 +49,7 @@ private:
   /**
    * Map from a node to it's minimum and maximum.
    */
-  //typedef __gnu_cxx::hash_map<Node, DeltaRational, NodeHashFunction> NodeToMinMaxMap;
-  typedef context::CDHashMap<Node, DeltaRational, NodeHashFunction> CDNodeToMinMaxMap;
+  typedef context::CDTrailHashMap<Node, DeltaRational, NodeHashFunction> CDNodeToMinMaxMap;
   CDNodeToMinMaxMap d_minMap;
   CDNodeToMinMaxMap d_maxMap;
 
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 6ec6c7090..d2814348a 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -1369,7 +1369,7 @@ Constraint TheoryArith::constraintFromFactQueue(){
     if(assertion != reAssertion){
       Debug("arith::nf") << "getting non-nf assertion " << assertion << " |-> " <<  reAssertion << endl;
       Assert(constraint != NullConstraint);
-      d_assertionsThatDoNotMatchTheirLiterals[assertion] = constraint;
+      d_assertionsThatDoNotMatchTheirLiterals.insert(assertion, constraint);
     }
   }
 
diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index 6a83c501b..b791186cf 100644
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -22,6 +22,7 @@
 #include "context/context.h"
 #include "context/cdlist.h"
 #include "context/cdhashset.h"
+#include "context/cdinsert_hashmap.h"
 #include "context/cdqueue.h"
 #include "expr/node.h"
 
@@ -135,7 +136,7 @@ private:
    * A superset of all of the assertions that currently are not the literal for
    * their constraint do not match constraint literals. Not just the witnesses.
    */
-  context::CDHashMap<TNode, Constraint, TNodeHashFunction> d_assertionsThatDoNotMatchTheirLiterals;
+  context::CDInsertHashMap<Node, Constraint, NodeHashFunction> d_assertionsThatDoNotMatchTheirLiterals;
 
   /**
    * (For the moment) the type hierarchy goes as: