diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-03-02 20:38:23 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-03-02 20:38:23 +0000 |
commit | 068107e1d1f705eb9054b4309a26236230687d80 (patch) | |
tree | 4c422f3efd6a8319abe426c518f9d2feb7ab5a6d /src/theory/arith | |
parent | 53176a3d39935bd77f1c057d0b806c380b346e23 (diff) |
CDMap -> CDHashMap
CDSet -> CDHashSet
Diffstat (limited to 'src/theory/arith')
-rw-r--r-- | src/theory/arith/arith_prop_manager.cpp | 2 | ||||
-rw-r--r-- | src/theory/arith/arith_prop_manager.h | 4 | ||||
-rw-r--r-- | src/theory/arith/arith_utilities.h | 6 | ||||
-rw-r--r-- | src/theory/arith/arithvar_node_map.h | 2 | ||||
-rw-r--r-- | src/theory/arith/theory_arith.cpp | 8 | ||||
-rw-r--r-- | src/theory/arith/theory_arith.h | 4 |
6 files changed, 13 insertions, 13 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 |