From 068107e1d1f705eb9054b4309a26236230687d80 Mon Sep 17 00:00:00 2001 From: =?utf8?q?Dejan=20Jovanovi=C4=87?= Date: Fri, 2 Mar 2012 20:38:23 +0000 Subject: [PATCH] CDMap -> CDHashMap CDSet -> CDHashSet --- .cproject | 537 +++++++++--------- src/context/Makefile.am | 8 +- src/context/{cdmap.h => cdhashmap.h} | 90 +-- .../{cdmap_forward.h => cdhashmap_forward.h} | 2 +- src/context/{cdset.h => cdhashset.h} | 10 +- .../{cdset_forward.h => cdhashset_forward.h} | 2 +- src/context/context.h | 2 +- src/expr/attribute_internals.h | 10 +- src/expr/declaration_scope.cpp | 12 +- src/expr/declaration_scope.h | 10 +- src/smt/smt_engine.cpp | 4 +- src/smt/smt_engine.h | 8 +- src/theory/arith/arith_prop_manager.cpp | 2 +- src/theory/arith/arith_prop_manager.h | 4 +- src/theory/arith/arith_utilities.h | 6 +- src/theory/arith/arithvar_node_map.h | 2 +- src/theory/arith/theory_arith.cpp | 8 +- src/theory/arith/theory_arith.h | 4 +- src/theory/arrays/array_info.h | 2 +- src/theory/arrays/theory_arrays.h | 10 +- src/theory/booleans/circuit_propagator.h | 8 +- src/theory/bv/bitblast_strategies.cpp | 2 +- src/theory/bv/bv_sat.h | 2 +- src/theory/datatypes/explanation_manager.cpp | 2 +- src/theory/datatypes/explanation_manager.h | 2 +- src/theory/datatypes/theory_datatypes.h | 6 +- src/theory/shared_terms_database.h | 4 +- src/theory/substitutions.h | 4 +- src/theory/term_registration_visitor.h | 2 +- src/theory/theory_engine.h | 6 +- src/theory/uf/theory_uf.h | 2 +- src/util/congruence_closure.h | 18 +- src/util/trans_closure.cpp | 2 +- src/util/trans_closure.h | 4 +- test/unit/context/cdmap_black.h | 22 +- test/unit/context/cdmap_white.h | 4 +- test/unit/util/congruence_closure_white.h | 10 +- 37 files changed, 417 insertions(+), 416 deletions(-) rename src/context/{cdmap.h => cdhashmap.h} (87%) rename src/context/{cdmap_forward.h => cdhashmap_forward.h} (98%) rename src/context/{cdset.h => cdhashset.h} (94%) rename src/context/{cdset_forward.h => cdhashset_forward.h} (98%) diff --git a/.cproject b/.cproject index ac930d8b9..2579ef3ae 100644 --- a/.cproject +++ b/.cproject @@ -52,277 +52,278 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - make - check - true - true - true - - - make - -j2 - - true - true - true - - - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + make + -j10 + check + true + false + true + + + make + -j2 + true + true + true + + + diff --git a/src/context/Makefile.am b/src/context/Makefile.am index e40eac099..23607373a 100644 --- a/src/context/Makefile.am +++ b/src/context/Makefile.am @@ -16,10 +16,10 @@ libcontext_la_SOURCES = \ cdlist_forward.h \ cdqueue.h \ cdtrail_queue.h \ - cdmap.h \ - cdmap_forward.h \ - cdset.h \ - cdset_forward.h \ + cdhashmap.h \ + cdhashmap_forward.h \ + cdhashset.h \ + cdhashset_forward.h \ cdcirclist.h \ cdcirclist_forward.h \ cdvector.h \ diff --git a/src/context/cdmap.h b/src/context/cdhashmap.h similarity index 87% rename from src/context/cdmap.h rename to src/context/cdhashmap.h index 2a5365082..de21515c7 100644 --- a/src/context/cdmap.h +++ b/src/context/cdhashmap.h @@ -24,53 +24,53 @@ ** CDMap<> is something of a work in progress at present (26 May ** 2010), due to some recent discoveries of problems with its ** internal state. Here are some notes on the internal use of - ** CDOmaps that may be useful in figuring out this mess: + ** CDOhash_maps that may be useful in figuring out this mess: ** ** So you have a CDMap<>. ** - ** You insert some (key,value) pairs. Each allocates a CDOmap<> + ** You insert some (key,value) pairs. Each allocates a CDOhash_map<> ** and goes on a doubly-linked list headed by map.d_first and - ** threaded via cdomap.{d_prev,d_next}. CDOmaps are constructed + ** threaded via CDOhash_map.{d_prev,d_next}. CDOhash_maps are constructed ** with a NULL d_map pointer, but then immediately call ** makeCurrent() and set the d_map pointer back to the map. At ** context level 0, this doesn't lead to anything special. In - ** higher context levels, this stores away a CDOmap with a NULL + ** higher context levels, this stores away a CDOhash_map with a NULL ** map pointer at level 0, and a non-NULL map pointer in the ** current context level. (Remember that for later.) ** ** When a key is associated to a new value in a CDMap, its - ** associated CDOmap calls makeCurrent(), then sets the new - ** value. The save object is also a CDOmap (allocated in context + ** associated CDOhash_map calls makeCurrent(), then sets the new + ** value. The save object is also a CDOhash_map (allocated in context ** memory). ** - ** Now, CDOmaps disappear in a variety of ways. + ** Now, CDOhash_maps disappear in a variety of ways. ** ** First, you might pop beyond a "modification of the value" ** scope level, requiring a re-association of the key to an old - ** value. This is easy. CDOmap::restore() does the work, and + ** value. This is easy. CDOhash_map::restore() does the work, and ** the context memory of the save object is reclaimed as usual. ** ** Second, you might pop beyond a "insert the key" scope level, ** requiring that the key be completely removed from the map and - ** its CDOmap object memory freed. Here, the CDOmap is restored + ** its CDOhash_map object memory freed. Here, the CDOhash_map is restored ** to a "NULL-map" state (see above), signaling it to remove ** itself from the map completely and put itself on a "trash ** list" for the map. ** - ** Third, you might obliterate() the key. This calls the CDOmap + ** Third, you might obliterate() the key. This calls the CDOhash_map ** destructor, which calls destroy(), which does a successive ** restore() until level 0. If the key was in the map since ** level 0, the restore() won't remove it, so in that case - ** obliterate() removes it from the map and frees the CDOmap's + ** obliterate() removes it from the map and frees the CDOhash_map's ** memory. ** - ** Fourth, you might delete the CDMap (calling CDMap::~CDMap()). + ** Fourth, you might delete the cdhashmap(calling CDMap::~CDMap()). ** This first calls destroy(), as per ContextObj contract, but - ** CDMap doesn't save/restore itself, so that does nothing at the + ** cdhashmapdoesn't save/restore itself, so that does nothing at the ** CDMap-level. Then it empties the trash. Then, for each ** element in the map, it marks it as being "part of a complete ** map destruction", which essentially short-circuits - ** CDOmap::restore() (see CDOmap::restore()), then deallocates + ** CDOhash_map::restore() (see CDOhash_map::restore()), then deallocates ** it. Finally it asserts that the trash is empty (which it ** should be, since restore() was short-circuited). ** @@ -80,8 +80,8 @@ ** ** CDMap::emptyTrash() simply goes through and calls ** ->deleteSelf() on all elements in the trash. - ** ContextObj::deleteSelf() calls the CDOmap destructor, then - ** frees the memory associated to the CDOmap. CDOmap::~CDOmap() + ** ContextObj::deleteSelf() calls the CDOhash_map destructor, then + ** frees the memory associated to the CDOhash_map. CDOhash_map::~CDOhash_map() ** calls destroy(), which restores as much as possible. (Note, ** though, that since objects placed on the trash have already ** restored to the fullest extent possible, it does nothing.) @@ -98,7 +98,7 @@ #include "context/context.h" #include "util/Assert.h" -#include "context/cdmap_forward.h" +#include "context/cdhashmap_forward.h" namespace CVC4 { namespace context { @@ -106,27 +106,27 @@ namespace context { // Auxiliary class: almost the same as CDO (see cdo.h) template > -class CDOmap : public ContextObj { - friend class CDMap; +class CDOhash_map : public ContextObj { + friend class CDHashMap; Key d_key; Data d_data; - CDMap* d_map; + CDHashMap* d_map; - /** never put this cdmap element on the trash */ + /** never put this cdhashmapelement on the trash */ bool d_noTrash; // Doubly-linked list for keeping track of elements in order of insertion - CDOmap* d_prev; - CDOmap* d_next; + CDOhash_map* d_prev; + CDOhash_map* d_next; virtual ContextObj* save(ContextMemoryManager* pCMM) { - return new(pCMM) CDOmap(*this); + return new(pCMM) CDOhash_map(*this); } virtual void restore(ContextObj* data) { if(d_map != NULL) { - CDOmap* p = static_cast(data); + CDOhash_map* p = static_cast(data); if(p->d_map == NULL) { Assert(d_map->d_map.find(d_key) != d_map->d_map.end() && (*d_map->d_map.find(d_key)).second == this); @@ -163,7 +163,7 @@ class CDOmap : public ContextObj { } /** ensure copy ctor is only called by us */ - CDOmap(const CDOmap& other) : + CDOhash_map(const CDOhash_map& other) : ContextObj(other), d_key(other.d_key), d_data(other.d_data), @@ -174,8 +174,8 @@ class CDOmap : public ContextObj { public: - CDOmap(Context* context, - CDMap* map, + CDOhash_map(Context* context, + CDHashMap* map, const Key& key, const Data& data, bool atLevelZero = false, @@ -212,7 +212,7 @@ public: } d_map = map; - CDOmap*& first = d_map->d_first; + CDOhash_map*& first = d_map->d_first; if(first == NULL) { first = d_next = d_prev = this; Debug("gc") << "add first-elem " << this << " to map " << d_map << std::endl; @@ -225,7 +225,7 @@ public: } } - ~CDOmap() throw(AssertionException) { + ~CDOhash_map() throw(AssertionException) { destroy(); } @@ -251,14 +251,14 @@ public: return data; } - CDOmap* next() const { + CDOhash_map* next() const { if(d_next == d_map->d_first) { return NULL; } else { return d_next; } } -};/* class CDOmap<> */ +};/* class CDOhash_map<> */ /** @@ -267,12 +267,12 @@ public: * defined for the data class, and operator== for the key class. */ template -class CDMap : public ContextObj { +class CDHashMap : public ContextObj { - typedef CDOmap Element; + typedef CDOhash_map Element; typedef __gnu_cxx::hash_map table_type; - friend class CDOmap; + friend class CDOhash_map; table_type d_map; @@ -304,7 +304,7 @@ class CDMap : public ContextObj { public: - CDMap(Context* context) : + CDHashMap(Context* context) : ContextObj(context), d_map(), d_first(NULL), @@ -312,14 +312,14 @@ public: d_trash() { } - ~CDMap() throw(AssertionException) { - Debug("gc") << "cdmap " << this + ~CDHashMap() throw(AssertionException) { + Debug("gc") << "cdhashmap" << this << " disappearing, destroying..." << std::endl; destroy(); - Debug("gc") << "cdmap " << this + Debug("gc") << "cdhashmap" << this << " disappearing, done destroying" << std::endl; - Debug("gc") << "cdmap " << this << " gone, emptying trash" << std::endl; + Debug("gc") << "cdhashmap" << this << " gone, emptying trash" << std::endl; emptyTrash(); Debug("gc") << "done emptying trash for " << this << std::endl; @@ -339,7 +339,7 @@ public: } void clear() throw(AssertionException) { - Debug("gc") << "clearing cdmap " << this << ", emptying trash" << std::endl; + Debug("gc") << "clearing cdhashmap" << this << ", emptying trash" << std::endl; emptyTrash(); Debug("gc") << "done emptying trash for " << this << std::endl; @@ -464,11 +464,11 @@ public: if(i != d_map.end()) { Debug("gc") << "key " << k << " obliterated" << std::endl; // We can't call ->deleteSelf() here, because it calls the - // ContextObj destructor, which calls CDOmap::destroy(), which - // restore()'s, which puts the CDOmap on the trash, which causes + // ContextObj destructor, which calls CDOhash_map::destroy(), which + // restore()'s, which puts the CDOhash_map on the trash, which causes // a double-delete. (*i).second->~Element(); - // Writing ...->~CDOmap() in the above is legal (?) but breaks + // Writing ...->~CDOhash_map() in the above is legal (?) but breaks // g++ 4.1, though later versions have no problem. typename table_type::iterator j = d_map.find(k); @@ -575,7 +575,7 @@ public: iterator find(const Key& k) { emptyTrash(); - return const_cast(this)->find(k); + return const_cast(this)->find(k); } };/* class CDMap<> */ diff --git a/src/context/cdmap_forward.h b/src/context/cdhashmap_forward.h similarity index 98% rename from src/context/cdmap_forward.h rename to src/context/cdhashmap_forward.h index 331d6a93e..f1031fec4 100644 --- a/src/context/cdmap_forward.h +++ b/src/context/cdhashmap_forward.h @@ -35,7 +35,7 @@ namespace __gnu_cxx { namespace CVC4 { namespace context { template > - class CDMap; + class CDHashMap; }/* CVC4::context namespace */ }/* CVC4 namespace */ diff --git a/src/context/cdset.h b/src/context/cdhashset.h similarity index 94% rename from src/context/cdset.h rename to src/context/cdhashset.h index 8699d9cf4..777bbc94b 100644 --- a/src/context/cdset.h +++ b/src/context/cdhashset.h @@ -22,16 +22,16 @@ #define __CVC4__CONTEXT__CDSET_H #include "context/context.h" -#include "context/cdset_forward.h" -#include "context/cdmap.h" +#include "context/cdhashset_forward.h" +#include "context/cdhashmap.h" #include "util/Assert.h" namespace CVC4 { namespace context { template -class CDSet : protected CDMap { - typedef CDMap super; +class CDHashSet : protected CDHashMap { + typedef CDHashMap super; public: @@ -52,7 +52,7 @@ public: AlwaysAssert(false, "It is not allowed to delete a ContextObj this way!"); } - CDSet(Context* context) : + CDHashSet(Context* context) : super(context) { } diff --git a/src/context/cdset_forward.h b/src/context/cdhashset_forward.h similarity index 98% rename from src/context/cdset_forward.h rename to src/context/cdhashset_forward.h index 2339552a6..dc7da22d2 100644 --- a/src/context/cdset_forward.h +++ b/src/context/cdhashset_forward.h @@ -35,7 +35,7 @@ namespace __gnu_cxx { namespace CVC4 { namespace context { template > - class CDSet; + class CDHashSet; }/* CVC4::context namespace */ }/* CVC4 namespace */ diff --git a/src/context/context.h b/src/context/context.h index 4e0832882..f0dbff72b 100644 --- a/src/context/context.h +++ b/src/context/context.h @@ -496,7 +496,7 @@ protected: * class-facing interface. This is a "forced" makeCurrent(), useful * for ContextObjs allocated in CMM that need a special "bottom" * case when they disappear out of existence (kind of a destructor). - * See CDOmap (in cdmap.h) for an example. + * See CDOhash_map (in cdhashmap.h) for an example. */ inline void makeSaveRestorePoint() throw(AssertionException); diff --git a/src/expr/attribute_internals.h b/src/expr/attribute_internals.h index b359b1666..70535cf1c 100644 --- a/src/expr/attribute_internals.h +++ b/src/expr/attribute_internals.h @@ -27,7 +27,7 @@ #include -#include "context/cdmap.h" +#include "context/cdhashmap.h" namespace CVC4 { namespace expr { @@ -365,12 +365,12 @@ public: */ template class CDAttrHash : - public context::CDMap, + public context::CDHashMap, value_type, AttrHashStrategy> { public: CDAttrHash(context::Context* ctxt) : - context::CDMap, + context::CDHashMap, value_type, AttrHashStrategy>(ctxt) { } @@ -382,12 +382,12 @@ public: */ template <> class CDAttrHash : - protected context::CDMap { /** A "super" type, like in Java, for easy reference below. */ - typedef context::CDMap super; + typedef context::CDHashMap super; /** * BitAccessor allows us to return a bit "by reference." Of course, diff --git a/src/expr/declaration_scope.cpp b/src/expr/declaration_scope.cpp index 37c709b6a..22187ad06 100644 --- a/src/expr/declaration_scope.cpp +++ b/src/expr/declaration_scope.cpp @@ -22,8 +22,8 @@ #include "expr/expr.h" #include "expr/type.h" #include "expr/expr_manager_scope.h" -#include "context/cdmap.h" -#include "context/cdset.h" +#include "context/cdhashmap.h" +#include "context/cdhashset.h" #include "context/context.h" #include @@ -37,9 +37,9 @@ namespace CVC4 { DeclarationScope::DeclarationScope() : d_context(new Context), - d_exprMap(new(true) CDMap(d_context)), - d_typeMap(new(true) CDMap, Type>, StringHashFunction>(d_context)), - d_functions(new(true) CDSet(d_context)) { + d_exprMap(new(true) CDHashMap(d_context)), + d_typeMap(new(true) CDHashMap, Type>, StringHashFunction>(d_context)), + d_functions(new(true) CDHashSet(d_context)) { } DeclarationScope::~DeclarationScope() { @@ -67,7 +67,7 @@ bool DeclarationScope::isBound(const std::string& name) const throw() { } bool DeclarationScope::isBoundDefinedFunction(const std::string& name) const throw() { - CDMap::iterator found = + CDHashMap::iterator found = d_exprMap->find(name); return found != d_exprMap->end() && d_functions->contains((*found).second); } diff --git a/src/expr/declaration_scope.h b/src/expr/declaration_scope.h index 4bce5e1be..27533cca8 100644 --- a/src/expr/declaration_scope.h +++ b/src/expr/declaration_scope.h @@ -28,8 +28,8 @@ #include "expr/expr.h" #include "util/hash.h" -#include "context/cdset_forward.h" -#include "context/cdmap_forward.h" +#include "context/cdhashset_forward.h" +#include "context/cdhashmap_forward.h" namespace CVC4 { @@ -52,13 +52,13 @@ class CVC4_PUBLIC DeclarationScope { context::Context* d_context; /** A map for expressions. */ - context::CDMap *d_exprMap; + context::CDHashMap *d_exprMap; /** A map for types. */ - context::CDMap, Type>, StringHashFunction> *d_typeMap; + context::CDHashMap, Type>, StringHashFunction> *d_typeMap; /** A set of defined functions. */ - context::CDSet *d_functions; + context::CDHashSet *d_functions; public: /** Create a declaration scope. */ diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 3c320b814..8b5a93fa9 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -25,7 +25,7 @@ #include #include "context/cdlist.h" -#include "context/cdset.h" +#include "context/cdhashset.h" #include "context/context.h" #include "expr/command.h" #include "expr/expr.h" @@ -124,7 +124,7 @@ class SmtEnginePrivate { theory::SubstitutionMap d_topLevelSubstitutions; /** - * The last substition that the SAT layer was told about. + * The last substitution that the SAT layer was told about. * In incremental settings, substitutions cannot be performed * "backward," only forward. So SAT needs to be told of all * substitutions that are going to be done. This iterator diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 84d6d1a73..5149ed2e9 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -24,8 +24,8 @@ #include #include "context/cdlist_forward.h" -#include "context/cdmap_forward.h" -#include "context/cdset_forward.h" +#include "context/cdhashmap_forward.h" +#include "context/cdhashset_forward.h" #include "expr/expr.h" #include "expr/expr_manager.h" #include "util/proof.h" @@ -89,12 +89,12 @@ namespace smt { class CVC4_PUBLIC SmtEngine { /** The type of our internal map of defined functions */ - typedef context::CDMap + typedef context::CDHashMap DefinedFunctionMap; /** The type of our internal assertion list */ typedef context::CDList AssertionList; /** The type of our internal assignment set */ - typedef context::CDSet AssignmentSet; + typedef context::CDHashSet AssignmentSet; /** Expr manager context */ context::Context* d_context; 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 ExplainMap; + typedef context::CDHashMap 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 #include #include @@ -47,9 +47,9 @@ typedef __gnu_cxx::hash_map ArithVarToNodeMap; //Sets of Nodes typedef __gnu_cxx::hash_set NodeSet; -typedef context::CDSet CDNodeSet; +typedef context::CDHashSet CDNodeSet; -typedef context::CDSet CDArithVarSet; +typedef context::CDHashSet 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::iterator it = d_diseq.begin(); - context::CDSet::iterator it_end = d_diseq.end(); + context::CDHashSet::iterator it = d_diseq.begin(); + context::CDHashSet::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::iterator it = d_diseq.begin(); - context::CDSet::iterator it_end = d_diseq.end(); + context::CDHashSet::iterator it = d_diseq.begin(); + context::CDHashSet::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 d_diseq; + context::CDHashSet 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 > CTNodeListAlloc; - typedef context::CDMap CNodeTNodesMap; - typedef context::CDMap*, TNodeHashFunction > EqLists; + typedef context::CDHashMap CNodeTNodesMap; + typedef context::CDHashMap*, TNodeHashFunction > EqLists; typedef __gnu_cxx::hash_map NodeTNodesMap; @@ -174,7 +174,7 @@ private: /** List of disequalities needed to construct explanations for propagated * row lemmas */ - context::CDMap, TNodeHashFunction> d_explanations; + context::CDHashMap, 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::const_iterator it = d_prop_queue.begin(); + // context::CDList::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 d_seen; + context::CDHashSet d_seen; /** * Assignment status of each node. */ - typedef context::CDMap AssignmentMap; + typedef context::CDHashMap 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 #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 > EqList; - typedef context::CDMap EqLists; + typedef context::CDHashMap EqLists; typedef context::CDList > EqListN; - typedef context::CDMap EqListsN; - typedef context::CDMap< Node, bool, NodeHashFunction > BoolMap; + typedef context::CDHashMap EqListsN; + typedef context::CDHashMap< Node, bool, NodeHashFunction > BoolMap; /** for debugging */ context::CDList 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 d_addedSharedTermsSize; - typedef context::CDMap, theory::Theory::Set, TNodePairHashFunction> SharedTermsTheoriesMap; + typedef context::CDHashMap, theory::Theory::Set, TNodePairHashFunction> SharedTermsTheoriesMap; /** A map from atoms and subterms to the theories that use it */ SharedTermsTheoriesMap d_termsToTheories; - typedef context::CDMap AlreadyNotifiedMap; + typedef context::CDHashMap 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 NodeMap; + typedef context::CDHashMap 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 TNodeVisitedMap; + typedef context::CDHashMap 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 d_hasPropagated; + context::CDHashSet 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 SharedAssertionsMap; + typedef context::CDHashMap 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 { diff --git a/src/util/congruence_closure.h b/src/util/congruence_closure.h index 4e690ec16..ed1cecd7b 100644 --- a/src/util/congruence_closure.h +++ b/src/util/congruence_closure.h @@ -30,8 +30,8 @@ #include "expr/node.h" #include "context/context_mm.h" #include "context/cdo.h" -#include "context/cdmap.h" -#include "context/cdset.h" +#include "context/cdhashmap.h" +#include "context/cdhashset.h" #include "context/cdlist_context_memory.h" #include "util/exception.h" #include "context/stacking_map.h" @@ -141,15 +141,15 @@ class CongruenceClosure { // typedef all of these so that iterators are easy to define typedef context::StackingMap RepresentativeMap; typedef context::CDList > ClassList; - typedef context::CDMap ClassLists; + typedef context::CDHashMap ClassLists; typedef context::CDList > UseList; - typedef context::CDMap UseLists; - typedef context::CDMap LookupMap; + typedef context::CDHashMap UseLists; + typedef context::CDHashMap LookupMap; typedef __gnu_cxx::hash_map EqMap; - typedef context::CDMap ProofMap; - typedef context::CDMap ProofLabel; + typedef context::CDHashMap ProofMap; + typedef context::CDHashMap ProofLabel; // Simple, NON-context-dependent pending list, union find and "seen // set" types for constructing explanations and @@ -164,7 +164,7 @@ class CongruenceClosure { LookupMap d_lookup; EqMap d_eqMap; - context::CDSet d_added; + context::CDHashSet d_added; ProofMap d_proof; ProofLabel d_proofLabel; @@ -175,7 +175,7 @@ class CongruenceClosure { * The set of terms we care about (i.e. those that have been given * us with addTerm() and their representatives). */ - typedef context::CDSet CareSet; + typedef context::CDHashSet CareSet; CareSet d_careSet; // === STATISTICS === diff --git a/src/util/trans_closure.cpp b/src/util/trans_closure.cpp index 5d772b576..ba289080c 100644 --- a/src/util/trans_closure.cpp +++ b/src/util/trans_closure.cpp @@ -98,7 +98,7 @@ void TransitiveClosure::debugPrintMatrix() } unsigned TransitiveClosureNode::getId( Node i ){ - context::CDMap< Node, unsigned, NodeHashFunction >::iterator it = nodeMap.find( i ); + context::CDHashMap< Node, unsigned, NodeHashFunction >::iterator it = nodeMap.find( i ); if( it==nodeMap.end() ){ unsigned c = d_counter.get(); nodeMap[i] = c; diff --git a/src/util/trans_closure.h b/src/util/trans_closure.h index a551d4a31..3cb3385dd 100644 --- a/src/util/trans_closure.h +++ b/src/util/trans_closure.h @@ -26,7 +26,7 @@ #include #include "context/cdlist.h" -#include "context/cdmap.h" +#include "context/cdhashmap.h" #include "context/cdo.h" namespace CVC4 { @@ -128,7 +128,7 @@ public: */ class TransitiveClosureNode : public TransitiveClosure{ context::CDO< unsigned > d_counter; - context::CDMap< Node, unsigned, NodeHashFunction > nodeMap; + context::CDHashMap< Node, unsigned, NodeHashFunction > nodeMap; //for debugging context::CDList< std::pair< Node, Node > > currEdges; public: diff --git a/test/unit/context/cdmap_black.h b/test/unit/context/cdmap_black.h index eb2caa98f..0358d1edd 100644 --- a/test/unit/context/cdmap_black.h +++ b/test/unit/context/cdmap_black.h @@ -18,7 +18,7 @@ #include -#include "context/cdmap.h" +#include "context/cdhashmap.h" #include "context/cdlist.h" using namespace std; @@ -43,7 +43,7 @@ public: } void testSimpleSequence() { - CDMap map(d_context); + CDHashMap map(d_context); TS_ASSERT(map.find(3) == map.end()); TS_ASSERT(map.find(5) == map.end()); @@ -188,7 +188,7 @@ public: // no intervening find() in this one // (under the theory that this could trigger a bug) void testSimpleSequenceFewerFinds() { - CDMap map(d_context); + CDHashMap map(d_context); map.insert(3, 4); @@ -226,7 +226,7 @@ public: } void testObliterate() { - CDMap map(d_context); + CDHashMap map(d_context); map.insert(3, 4); @@ -357,7 +357,7 @@ public: } void testObliteratePrimordial() { - CDMap map(d_context); + CDHashMap map(d_context); map.insert(3, 4); @@ -460,7 +460,7 @@ public: } void testObliterateCurrent() { - CDMap map(d_context); + CDHashMap map(d_context); map.insert(3, 4); @@ -566,7 +566,7 @@ public: } void testInsertAtContextLevelZero() { - CDMap map(d_context); + CDHashMap map(d_context); map.insert(3, 4); @@ -739,7 +739,7 @@ public: } void testObliterateInsertedAtContextLevelZero() { - CDMap map(d_context); + CDHashMap map(d_context); map.insert(3, 4); @@ -933,7 +933,7 @@ public: //Debug.on("gc"); //Debug.on("context"); - CDMap*, int_hasher> map(d_context); + CDHashMap*, int_hasher> map(d_context); CDList *list1, *list2, *list3, *list4; @@ -1026,7 +1026,7 @@ public: d_context->push(); // This re-uses context memory used above. the map.clear() - // triggers an emptyTrash() which fails if the CDOmaps are put + // triggers an emptyTrash() which fails if the CDOhash_maps are put // in the trash. (We use insertDataFromContextMemory() above to // keep them out of the trash.) cout << "allocating\n"; @@ -1059,7 +1059,7 @@ public: void testCmmElementsAtLevel0() { // this was crashing - CDMap map(d_context); + CDHashMap map(d_context); int* a = (int*)d_context->getCMM()->newData(sizeof(int)); map.insertDataFromContextMemory(1, a); } diff --git a/test/unit/context/cdmap_white.h b/test/unit/context/cdmap_white.h index 42f9b8563..db940f3ea 100644 --- a/test/unit/context/cdmap_white.h +++ b/test/unit/context/cdmap_white.h @@ -18,7 +18,7 @@ #include -#include "context/cdmap.h" +#include "context/cdhashmap.h" #include "util/Assert.h" using namespace std; @@ -40,7 +40,7 @@ public: } void testUnreachableSaveAndRestore() { - CDMap map(d_context); + CDHashMap map(d_context); TS_ASSERT_THROWS_NOTHING(map.makeCurrent()); diff --git a/test/unit/util/congruence_closure_white.h b/test/unit/util/congruence_closure_white.h index 187b7dc08..0c14160f7 100644 --- a/test/unit/util/congruence_closure_white.h +++ b/test/unit/util/congruence_closure_white.h @@ -20,8 +20,8 @@ #include #include "context/context.h" -#include "context/cdset.h" -#include "context/cdmap.h" +#include "context/cdhashset.h" +#include "context/cdhashmap.h" #include "expr/node.h" #include "expr/kind.h" #include "expr/node_manager.h" @@ -34,8 +34,8 @@ using namespace std; struct MyOutputChannel { - CDSet d_notifications; - CDMap d_equivalences; + CDHashSet d_notifications; + CDHashMap d_equivalences; NodeManager* d_nm; MyOutputChannel(Context* ctxt, NodeManager* nm) : @@ -50,7 +50,7 @@ struct MyOutputChannel { } TNode find(TNode n) { - CDMap::iterator i = d_equivalences.find(n); + CDHashMap::iterator i = d_equivalences.find(n); if(i == d_equivalences.end()) { return n; } else { -- 2.30.2