CDMap -> CDHashMap

CDSet -> CDHashSet

19 files changed, 39 insertions, 39 deletions

diff --git a/src/theory/arith/arith_prop_manager.cpp b/src/theory/arith/arith_prop_manager.cpp
index 6d2e04de1..4b52133da 100644
--- a/src/theory/arith/arith_prop_manager.cpp
+++ b/src/theory/arith/arith_prop_manager.cpp
@@ -23,7 +23,7 @@
 #include "theory/arith/arith_utilities.h"
 #include "context/context.h"
 #include "context/cdlist.h"
-#include "context/cdmap.h"
+#include "context/cdhashmap.h"
 #include "context/cdo.h"
 
 using namespace CVC4;
diff --git a/src/theory/arith/arith_prop_manager.h b/src/theory/arith/arith_prop_manager.h
index bf7564593..2bac21437 100644
--- a/src/theory/arith/arith_prop_manager.h
+++ b/src/theory/arith/arith_prop_manager.h
@@ -29,7 +29,7 @@
 #include "theory/arith/delta_rational.h"
 #include "context/context.h"
 #include "context/cdlist.h"
-#include "context/cdmap.h"
+#include "context/cdhashmap.h"
 #include "context/cdo.h"
 #include "theory/rewriter.h"
 #include "util/stats.h"
@@ -59,7 +59,7 @@ private:
    * to its corresponding PropUnit.
    * This is node is potentially both the consequent or Rewriter::rewrite(consequent).
    */
-  typedef context::CDMap<Node, size_t, NodeHashFunction> ExplainMap;
+  typedef context::CDHashMap<Node, size_t, NodeHashFunction> ExplainMap;
   ExplainMap d_explanationMap;
 
   size_t getIndex(TNode n) const {
diff --git a/src/theory/arith/arith_utilities.h b/src/theory/arith/arith_utilities.h
index 07387c977..44b55440e 100644
--- a/src/theory/arith/arith_utilities.h
+++ b/src/theory/arith/arith_utilities.h
@@ -26,7 +26,7 @@
 #include "expr/node.h"
 #include "expr/attribute.h"
 #include "theory/arith/delta_rational.h"
-#include "context/cdset.h"
+#include "context/cdhashset.h"
 #include <vector>
 #include <stdint.h>
 #include <limits>
@@ -47,9 +47,9 @@ typedef __gnu_cxx::hash_map<ArithVar, Node> ArithVarToNodeMap;
 
 //Sets of Nodes
 typedef __gnu_cxx::hash_set<Node, NodeHashFunction> NodeSet;
-typedef context::CDSet<Node, NodeHashFunction> CDNodeSet;
+typedef context::CDHashSet<Node, NodeHashFunction> CDNodeSet;
 
-typedef context::CDSet<ArithVar> CDArithVarSet;
+typedef context::CDHashSet<ArithVar> CDArithVarSet;
 
 class ArithVarCallBack {
 public:
diff --git a/src/theory/arith/arithvar_node_map.h b/src/theory/arith/arithvar_node_map.h
index df82fde91..1dc8ddf38 100644
--- a/src/theory/arith/arithvar_node_map.h
+++ b/src/theory/arith/arithvar_node_map.h
@@ -26,7 +26,7 @@
 #include "theory/arith/arith_utilities.h"
 #include "context/context.h"
 #include "context/cdlist.h"
-#include "context/cdmap.h"
+#include "context/cdhashmap.h"
 #include "context/cdo.h"
 
 namespace CVC4 {
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index fcac6f10e..bea87fdde 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -1030,8 +1030,8 @@ Node TheoryArith::roundRobinBranch(){
 bool TheoryArith::splitDisequalities(){
   bool splitSomething = false;
 
-  context::CDSet<Node, NodeHashFunction>::iterator it = d_diseq.begin();
-  context::CDSet<Node, NodeHashFunction>::iterator it_end = d_diseq.end();
+  context::CDHashSet<Node, NodeHashFunction>::iterator it = d_diseq.begin();
+  context::CDHashSet<Node, NodeHashFunction>::iterator it_end = d_diseq.end();
   for(; it != it_end; ++ it) {
     TNode eq = (*it)[0];
     Assert(eq.getKind() == kind::EQUAL);
@@ -1073,8 +1073,8 @@ void TheoryArith::debugPrintAssertions() {
       Debug("arith::print_assertions") << uConstr << endl;
     }
   }
-  context::CDSet<Node, NodeHashFunction>::iterator it = d_diseq.begin();
-  context::CDSet<Node, NodeHashFunction>::iterator it_end = d_diseq.end();
+  context::CDHashSet<Node, NodeHashFunction>::iterator it = d_diseq.begin();
+  context::CDHashSet<Node, NodeHashFunction>::iterator it_end = d_diseq.end();
   for(; it != it_end; ++ it) {
     Debug("arith::print_assertions") << *it << endl;
   }
diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index f364885c2..e6bdbfba0 100644
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -23,7 +23,7 @@
 #include "theory/theory.h"
 #include "context/context.h"
 #include "context/cdlist.h"
-#include "context/cdset.h"
+#include "context/cdhashset.h"
 #include "expr/node.h"
 
 #include "theory/arith/arith_utilities.h"
@@ -183,7 +183,7 @@ private:
   /**
    * List of all of the inequalities asserted in the current context.
    */
-  context::CDSet<Node, NodeHashFunction> d_diseq;
+  context::CDHashSet<Node, NodeHashFunction> d_diseq;
 
   /**
    * Manages information about the assignment and upper and lower bounds on
diff --git a/src/theory/arrays/array_info.h b/src/theory/arrays/array_info.h
index fcc45bbd5..d1c435b48 100644
--- a/src/theory/arrays/array_info.h
+++ b/src/theory/arrays/array_info.h
@@ -41,7 +41,7 @@
 #define __CVC4__THEORY__ARRAYS__ARRAY_INFO_H
 #include "util/backtrackable.h"
 #include "context/cdlist.h"
-#include "context/cdmap.h"
+#include "context/cdhashmap.h"
 #include "expr/node.h"
 #include "util/stats.h"
 #include "util/ntuple.h"
diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h
index d699617e2..fcb6ee382 100644
--- a/src/theory/arrays/theory_arrays.h
+++ b/src/theory/arrays/theory_arrays.h
@@ -152,8 +152,8 @@ private:
 
 
   typedef context::CDList<TNode, context::ContextMemoryAllocator<TNode> > CTNodeListAlloc;
-  typedef context::CDMap<Node, CTNodeListAlloc*, NodeHashFunction> CNodeTNodesMap;
-  typedef context::CDMap<TNode, List<TNode>*, TNodeHashFunction > EqLists;
+  typedef context::CDHashMap<Node, CTNodeListAlloc*, NodeHashFunction> CNodeTNodesMap;
+  typedef context::CDHashMap<TNode, List<TNode>*, TNodeHashFunction > EqLists;
 
 
   typedef __gnu_cxx::hash_map<TNode, CTNodeList*, TNodeHashFunction> NodeTNodesMap;
@@ -174,7 +174,7 @@ private:
   /** List of disequalities needed to construct explanations for propagated
    * row lemmas */
 
-  context::CDMap<TNode, std::pair<TNode, TNode>, TNodeHashFunction> d_explanations;
+  context::CDHashMap<TNode, std::pair<TNode, TNode>, TNodeHashFunction> d_explanations;
 
   /**
    * stores the conflicting disequality (still need to call construct
@@ -447,9 +447,9 @@ public:
 
   void propagate(Effort e) {
 
-    Trace("arrays-prop")<<"Propagating \n";
+    // Trace("arrays-prop")<<"Propagating \n";
 
-    context::CDList<TNode>::const_iterator it = d_prop_queue.begin();
+    // context::CDList<TNode>::const_iterator it = d_prop_queue.begin();
     /*
     for(; it!= d_prop_queue.end(); it++) {
       TNode eq = *it;
diff --git a/src/theory/booleans/circuit_propagator.h b/src/theory/booleans/circuit_propagator.h
index 2f9a8f928..78221a617 100644
--- a/src/theory/booleans/circuit_propagator.h
+++ b/src/theory/booleans/circuit_propagator.h
@@ -28,8 +28,8 @@
 #include "context/context.h"
 #include "util/hash.h"
 #include "expr/node.h"
-#include "context/cdset.h"
-#include "context/cdmap.h"
+#include "context/cdhashset.h"
+#include "context/cdhashmap.h"
 #include "context/cdo.h"
 
 namespace CVC4 {
@@ -113,12 +113,12 @@ private:
 
   /** Nodes that have been attached already (computed forward edges for) */
   // All the nodes we've visited so far
-  context::CDSet<TNode, TNodeHashFunction> d_seen;
+  context::CDHashSet<TNode, TNodeHashFunction> d_seen;
 
   /**
    * Assignment status of each node.
    */
-  typedef context::CDMap<TNode, AssignmentStatus, TNodeHashFunction> AssignmentMap;
+  typedef context::CDHashMap<TNode, AssignmentStatus, TNodeHashFunction> AssignmentMap;
   AssignmentMap d_state;
 
   /**
diff --git a/src/theory/bv/bitblast_strategies.cpp b/src/theory/bv/bitblast_strategies.cpp
index 6967bff98..dacd6a538 100644
--- a/src/theory/bv/bitblast_strategies.cpp
+++ b/src/theory/bv/bitblast_strategies.cpp
@@ -79,7 +79,7 @@ void inline rshift(Bits& bits, unsigned amount) {
 }
 
 void inline lshift(Bits& bits, unsigned amount) {
-  for (int i = bits.size() - 1; i >= amount ; --i) {
+  for (int i = (int)bits.size() - 1; i >= (int)amount ; --i) {
     bits[i] = bits[i-amount]; 
   }
   for(unsigned i = 0; i < amount; ++i) {
diff --git a/src/theory/bv/bv_sat.h b/src/theory/bv/bv_sat.h
index ee48dbef4..773491fd0 100644
--- a/src/theory/bv/bv_sat.h
+++ b/src/theory/bv/bv_sat.h
@@ -30,7 +30,7 @@
 #include <ext/hash_map>
 
 #include "context/cdo.h"
-#include "context/cdset.h"
+#include "context/cdhashset.h"
 #include "context/cdlist.h"
 
 #include "theory_bv_utils.h"
diff --git a/src/theory/datatypes/explanation_manager.cpp b/src/theory/datatypes/explanation_manager.cpp
index 6107e7f2c..be0bf6805 100644
--- a/src/theory/datatypes/explanation_manager.cpp
+++ b/src/theory/datatypes/explanation_manager.cpp
@@ -47,7 +47,7 @@ void ExplanationManager::process( Node n, NodeBuilder<>& nb, ProofManager* pm )
     }
   }else{
     if( !pm->hasExplained( n ) ){
-      context::CDMap< Node, Reason, NodeHashFunction >::iterator it = d_drv_map.find( n );
+      context::CDHashMap< Node, Reason, NodeHashFunction >::iterator it = d_drv_map.find( n );
       Reason r;
       Node exp;
       if( it!=d_drv_map.end() ){
diff --git a/src/theory/datatypes/explanation_manager.h b/src/theory/datatypes/explanation_manager.h
index 2232d0048..fa0d3f818 100644
--- a/src/theory/datatypes/explanation_manager.h
+++ b/src/theory/datatypes/explanation_manager.h
@@ -160,7 +160,7 @@ class ExplanationManager : public Explainer
 {
 private:
   /** map from nodes and the reason for them */
-  context::CDMap< Node, Reason, NodeHashFunction > d_drv_map;
+  context::CDHashMap< Node, Reason, NodeHashFunction > d_drv_map;
   /** has conflict */
   context::CDO< bool > d_hasConflict;
   /** process the reason for node n */
diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h
index 4d429bc54..921df028e 100644
--- a/src/theory/datatypes/theory_datatypes.h
+++ b/src/theory/datatypes/theory_datatypes.h
@@ -40,10 +40,10 @@ namespace datatypes {
 class TheoryDatatypes : public Theory {
 private:
   typedef context::CDList<TNode, context::ContextMemoryAllocator<TNode> > EqList;
-  typedef context::CDMap<Node, EqList*, NodeHashFunction> EqLists;
+  typedef context::CDHashMap<Node, EqList*, NodeHashFunction> EqLists;
   typedef context::CDList<Node, context::ContextMemoryAllocator<Node> > EqListN;
-  typedef context::CDMap<Node, EqListN*, NodeHashFunction> EqListsN;
-  typedef context::CDMap< Node, bool, NodeHashFunction > BoolMap;
+  typedef context::CDHashMap<Node, EqListN*, NodeHashFunction> EqListsN;
+  typedef context::CDHashMap< Node, bool, NodeHashFunction > BoolMap;
 
   /** for debugging */
   context::CDList<Node> d_currAsserts;
diff --git a/src/theory/shared_terms_database.h b/src/theory/shared_terms_database.h
index a5481b807..2efd121a0 100644
--- a/src/theory/shared_terms_database.h
+++ b/src/theory/shared_terms_database.h
@@ -51,11 +51,11 @@ private:
   /** Context-dependent size of the d_addedSharedTerms list */
   context::CDO<unsigned> d_addedSharedTermsSize;
   
-  typedef context::CDMap<std::pair<Node, TNode>, theory::Theory::Set, TNodePairHashFunction> SharedTermsTheoriesMap;
+  typedef context::CDHashMap<std::pair<Node, TNode>, theory::Theory::Set, TNodePairHashFunction> SharedTermsTheoriesMap;
   /** A map from atoms and subterms to the theories that use it */
   SharedTermsTheoriesMap d_termsToTheories;
 
-  typedef context::CDMap<TNode, theory::Theory::Set, TNodeHashFunction> AlreadyNotifiedMap;
+  typedef context::CDHashMap<TNode, theory::Theory::Set, TNodeHashFunction> AlreadyNotifiedMap;
   /** Map from term to theories that have already been notified about the shared term */
   AlreadyNotifiedMap d_alreadyNotifiedMap;
 
diff --git a/src/theory/substitutions.h b/src/theory/substitutions.h
index 1ade4815d..27c1a2b69 100644
--- a/src/theory/substitutions.h
+++ b/src/theory/substitutions.h
@@ -28,7 +28,7 @@
 #include "expr/node.h"
 #include "context/context.h"
 #include "context/cdo.h"
-#include "context/cdmap.h"
+#include "context/cdhashmap.h"
 #include "util/hash.h"
 
 namespace CVC4 {
@@ -46,7 +46,7 @@ class SubstitutionMap {
 
 public:
 
-  typedef context::CDMap<Node, Node, NodeHashFunction> NodeMap;
+  typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeMap;
 
   typedef NodeMap::iterator iterator;
   typedef NodeMap::const_iterator const_iterator;
diff --git a/src/theory/term_registration_visitor.h b/src/theory/term_registration_visitor.h
index edb759157..74b756a03 100644
--- a/src/theory/term_registration_visitor.h
+++ b/src/theory/term_registration_visitor.h
@@ -36,7 +36,7 @@ class PreRegisterVisitor {
   /**
    * Map from nodes to the theories that have already seen them.
    */
-  typedef context::CDMap<TNode, theory::Theory::Set, TNodeHashFunction> TNodeVisitedMap;
+  typedef context::CDHashMap<TNode, theory::Theory::Set, TNodeHashFunction> TNodeVisitedMap;
   TNodeVisitedMap d_visited;
 
   /**
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 72244a573..4c9309fb6 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -28,7 +28,7 @@
 #include "expr/node.h"
 #include "expr/command.h"
 #include "prop/prop_engine.h"
-#include "context/cdset.h"
+#include "context/cdhashset.h"
 #include "theory/theory.h"
 #include "theory/substitutions.h"
 #include "theory/rewriter.h"
@@ -121,7 +121,7 @@ class TheoryEngine {
    * context-dependent set of those theory-propagable literals that
    * have been propagated.
    */
-  context::CDSet<TNode, TNodeHashFunction> d_hasPropagated;
+  context::CDHashSet<TNode, TNodeHashFunction> d_hasPropagated;
 
   /**
    * Statistics for a particular theory.
@@ -311,7 +311,7 @@ class TheoryEngine {
   /**
    * Map from equalities asserted to a theory, to the theory that can explain them.
    */
-  typedef context::CDMap<NodeTheoryPair, NodeTheoryPair, NodeTheoryPairHashFunction> SharedAssertionsMap;
+  typedef context::CDHashMap<NodeTheoryPair, NodeTheoryPair, NodeTheoryPairHashFunction> SharedAssertionsMap;
 
   /**
    * A map from asserted facts to where they came from (for explanations).
diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h
index ab391e242..cb7674342 100644
--- a/src/theory/uf/theory_uf.h
+++ b/src/theory/uf/theory_uf.h
@@ -30,7 +30,7 @@
 #include "theory/uf/symmetry_breaker.h"
 
 #include "context/cdo.h"
-#include "context/cdset.h"
+#include "context/cdhashset.h"
 
 namespace CVC4 {
 namespace theory {