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 | |
parent | 53176a3d39935bd77f1c057d0b806c380b346e23 (diff) |
CDMap -> CDHashMap
CDSet -> CDHashSet
Diffstat (limited to 'src/theory')
-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 | ||||
-rw-r--r-- | src/theory/arrays/array_info.h | 2 | ||||
-rw-r--r-- | src/theory/arrays/theory_arrays.h | 10 | ||||
-rw-r--r-- | src/theory/booleans/circuit_propagator.h | 8 | ||||
-rw-r--r-- | src/theory/bv/bitblast_strategies.cpp | 2 | ||||
-rw-r--r-- | src/theory/bv/bv_sat.h | 2 | ||||
-rw-r--r-- | src/theory/datatypes/explanation_manager.cpp | 2 | ||||
-rw-r--r-- | src/theory/datatypes/explanation_manager.h | 2 | ||||
-rw-r--r-- | src/theory/datatypes/theory_datatypes.h | 6 | ||||
-rw-r--r-- | src/theory/shared_terms_database.h | 4 | ||||
-rw-r--r-- | src/theory/substitutions.h | 4 | ||||
-rw-r--r-- | src/theory/term_registration_visitor.h | 2 | ||||
-rw-r--r-- | src/theory/theory_engine.h | 6 | ||||
-rw-r--r-- | src/theory/uf/theory_uf.h | 2 |
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 { |