diff options
132 files changed, 809 insertions, 2108 deletions
diff --git a/configure.ac b/configure.ac index c0cec382f..6efae69cb 100644 --- a/configure.ac +++ b/configure.ac @@ -826,14 +826,14 @@ AC_SUBST([CRYPTOMINISAT_LIBS]) # Check to see if this version/architecture of GNU C++ explicitly -# instantiates __gnu_cxx::hash<uint64_t> or not. Some do, some don't. +# instantiates std::hash<uint64_t> or not. Some do, some don't. # See src/util/hash.h. -AC_MSG_CHECKING([whether __gnu_cxx::hash<uint64_t> is already specialized]) +AC_MSG_CHECKING([whether std::hash<uint64_t> is already specialized]) AC_LANG_PUSH([C++]) AC_COMPILE_IFELSE([AC_LANG_SOURCE([ -#include <stdint.h> -#include <ext/hash_map> -namespace __gnu_cxx { template<> struct hash<uint64_t> {}; }])], +#include <cstdint> +#include <functional> +namespace std { template<> struct hash<uint64_t> {}; }])], [AC_MSG_RESULT([no]); CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_NEED_HASH_UINT64_T"], [AC_MSG_RESULT([yes])]) AC_LANG_POP([C++]) diff --git a/examples/sets-translate/sets_translate.cpp b/examples/sets-translate/sets_translate.cpp index 6f1de6b00..f099b017a 100644 --- a/examples/sets-translate/sets_translate.cpp +++ b/examples/sets-translate/sets_translate.cpp @@ -20,6 +20,7 @@ #include <iostream> #include <string> #include <typeinfo> +#include <unordered_map> #include <vector> #include "expr/expr.h" @@ -83,7 +84,7 @@ class Mapper { set< Type > setTypes; map< Type, Type > mapTypes; map< pair<Type, Kind>, Expr > setoperators; - hash_map< Expr, Expr, ExprHashFunction > substitutions; + unordered_map< Expr, Expr, ExprHashFunction > substitutions; ostringstream sout; ExprManager* em; int depth; diff --git a/examples/simple_vc_compat_c.c b/examples/simple_vc_compat_c.c index 5f0c183b7..46ca66e44 100644 --- a/examples/simple_vc_compat_c.c +++ b/examples/simple_vc_compat_c.c @@ -19,7 +19,8 @@ #include <stdio.h> #include <stdlib.h> -/* #include <cvc4/bindings/compat/c/c_interface.h> /* use this after CVC4 is properly installed */ +// Use this after CVC4 is properly installed. +// #include <cvc4/bindings/compat/c/c_interface.h> #include "bindings/compat/c/c_interface.h" int main() { diff --git a/src/compat/cvc3_compat.cpp b/src/compat/cvc3_compat.cpp index 2757e3dbe..ffb299394 100644 --- a/src/compat/cvc3_compat.cpp +++ b/src/compat/cvc3_compat.cpp @@ -21,7 +21,6 @@ #include <iosfwd> #include <iterator> #include <sstream> -#include <string> #include "base/exception.h" #include "base/output.h" @@ -33,9 +32,6 @@ #include "parser/parser_builder.h" #include "smt/command.h" #include "util/bitvector.h" -#include "util/hash.h" -#include "util/integer.h" -#include "util/rational.h" #include "util/sexpr.h" #include "util/subrange_bound.h" @@ -60,22 +56,22 @@ namespace CVC3 { // ExprManager-to-ExprManager import). static std::map<CVC4::ExprManager*, ValidityChecker*> s_validityCheckers; -static std::hash_map<Type, Expr, CVC4::TypeHashFunction> s_typeToExpr; -static std::hash_map<Expr, Type, CVC4::ExprHashFunction> s_exprToType; +static std::unordered_map<Type, Expr, CVC4::TypeHashFunction> s_typeToExpr; +static std::unordered_map<Expr, Type, CVC4::ExprHashFunction> s_exprToType; static bool typeHasExpr(const Type& t) { - std::hash_map<Type, Expr, CVC4::TypeHashFunction>::const_iterator i = s_typeToExpr.find(t); + std::unordered_map<Type, Expr, CVC4::TypeHashFunction>::const_iterator i = s_typeToExpr.find(t); return i != s_typeToExpr.end(); } static Expr typeToExpr(const Type& t) { - std::hash_map<Type, Expr, CVC4::TypeHashFunction>::const_iterator i = s_typeToExpr.find(t); + std::unordered_map<Type, Expr, CVC4::TypeHashFunction>::const_iterator i = s_typeToExpr.find(t); assert(i != s_typeToExpr.end()); return (*i).second; } static Type exprToType(const Expr& e) { - std::hash_map<Expr, Type, CVC4::ExprHashFunction>::const_iterator i = s_exprToType.find(e); + std::unordered_map<Expr, Type, CVC4::ExprHashFunction>::const_iterator i = s_exprToType.find(e); assert(i != s_exprToType.end()); return (*i).second; } @@ -311,8 +307,8 @@ Expr Expr::substExpr(const std::vector<Expr>& oldTerms, } Expr Expr::substExpr(const ExprHashMap<Expr>& oldToNew) const { - const hash_map<CVC4::Expr, CVC4::Expr, CVC4::ExprHashFunction>& o2n = - *reinterpret_cast<const hash_map<CVC4::Expr, CVC4::Expr, CVC4::ExprHashFunction>*>(&oldToNew); + const unordered_map<CVC4::Expr, CVC4::Expr, CVC4::ExprHashFunction>& o2n = + *reinterpret_cast<const unordered_map<CVC4::Expr, CVC4::Expr, CVC4::ExprHashFunction>*>(&oldToNew); return Expr(substitute(o2n)); } @@ -924,13 +920,16 @@ void CLFlags::setFlag(const std::string& name, } void ValidityChecker::setUpOptions(CVC4::Options& options, const CLFlags& clflags) { + // Note: SIMPLIFICATION_MODE_INCREMENTAL, which was used + // for CVC3 compatibility, is not supported by CVC4 + // anymore. + // always incremental and model-producing in CVC3 compatibility mode // also incrementally-simplifying and interactive d_smt->setOption("incremental", string("true")); // disable this option by default for now, because datatype models // are broken [MGD 10/4/2012] //d_smt->setOption("produce-models", string("true")); - d_smt->setOption("simplification-mode", string("incremental")); d_smt->setOption("interactive-mode", string("true"));// support SmtEngine::getAssertions() d_smt->setOption("statistics", string(clflags["stats"].getBool() ? "true" : "false")); diff --git a/src/compat/cvc3_compat.h b/src/compat/cvc3_compat.h index be0dc3393..25e3ae32f 100644 --- a/src/compat/cvc3_compat.h +++ b/src/compat/cvc3_compat.h @@ -49,7 +49,10 @@ #define _cvc3__include__formula_value_h_ #include <stdlib.h> + #include <map> +#include <string> +#include <unordered_map> #include <utility> #include "base/exception.h" @@ -58,7 +61,6 @@ #include "expr/type.h" #include "parser/parser.h" #include "smt/smt_engine.h" -#include "util/hash.h" #include "util/integer.h" #include "util/rational.h" @@ -267,7 +269,7 @@ class CVC4_PUBLIC ExprMap : public std::map<Expr, T> { };/* class ExprMap<T> */ template <class T> -class CVC4_PUBLIC ExprHashMap : public std::hash_map<Expr, T, CVC4::ExprHashFunction> { +class CVC4_PUBLIC ExprHashMap : public std::unordered_map<Expr, T, CVC4::ExprHashFunction> { public: void insert(Expr a, Expr b); };/* class ExprHashMap<T> */ @@ -521,8 +523,8 @@ class CVC4_PUBLIC ValidityChecker { friend class Type; // to reach in to d_exprTypeMapRemove - typedef std::hash_map<std::string, const CVC4::Datatype*, CVC4::StringHashFunction> ConstructorMap; - typedef std::hash_map<std::string, std::pair<const CVC4::Datatype*, std::string>, CVC4::StringHashFunction> SelectorMap; + typedef std::unordered_map<std::string, const CVC4::Datatype*> ConstructorMap; + typedef std::unordered_map<std::string, std::pair<const CVC4::Datatype*, std::string>> SelectorMap; ConstructorMap d_constructors; SelectorMap d_selectors; diff --git a/src/context/cdhashmap.h b/src/context/cdhashmap.h index 86a7cb141..b6024b65d 100644 --- a/src/context/cdhashmap.h +++ b/src/context/cdhashmap.h @@ -15,7 +15,7 @@ ** which must be saved and restored as contexts are pushed and ** popped. Requires that operator= be defined for the data class, ** and operator== for the key class. For key types that don't have a - ** __gnu_cxx::hash<>, you should provide an explicit HashFcn. + ** std::hash<>, you should provide an explicit HashFcn. ** ** See also: ** CDInsertHashMap : An "insert-once" CD hash map. @@ -58,36 +58,23 @@ ** 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. + ** list" for its scope. ** - ** 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 CDOhash_map's - ** memory. - ** - ** Fourth, you might delete the cdhashmap(calling CDHashMap::~CDHashMap()). + ** Third, you might delete the cdhashmap(calling CDHashMap::~CDHashMap()). ** This first calls destroy(), as per ContextObj contract, but ** cdhashmapdoesn't save/restore itself, so that does nothing at the - ** CDHashMap-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 + ** CDHashMap-level. Then, for each element in the map, it marks it as being + ** "part of a complete map destruction", which essentially short-circuits ** 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). + ** it. ** - ** Fifth, you might clear() the CDHashMap. This does exactly the + ** Fourth, you might clear() the CDHashMap. This does exactly the ** same as CDHashMap::~CDHashMap(), except that it doesn't call destroy() ** on itself. ** - ** CDHashMap::emptyTrash() simply goes through and calls - ** ->deleteSelf() on all elements in the trash. ** 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.) + ** calls destroy(), which restores as much as possible. **/ #include "cvc4_private.h" @@ -95,8 +82,9 @@ #ifndef __CVC4__CONTEXT__CDHASHMAP_H #define __CVC4__CONTEXT__CDHASHMAP_H -#include <ext/hash_map> +#include <functional> #include <iterator> +#include <unordered_map> #include <vector> #include "base/cvc4_assert.h" @@ -108,7 +96,7 @@ namespace context { // Auxiliary class: almost the same as CDO (see cdo.h) -template <class Key, class Data, class HashFcn = __gnu_cxx::hash<Key> > +template <class Key, class Data, class HashFcn = std::hash<Key> > class CDOhash_map : public ContextObj { friend class CDHashMap<Key, Data, HashFcn>; @@ -157,7 +145,7 @@ class CDOhash_map : public ContextObj { } else { Debug("gc") << "CDHashMap<> trash push_back " << this << std::endl; //this->deleteSelf(); - d_map->d_trash.push_back(this); + enqueueToGarbageCollect(); } } else { d_data = p->d_data; @@ -281,7 +269,7 @@ template <class Key, class Data, class HashFcn> class CDHashMap : public ContextObj { typedef CDOhash_map<Key, Data, HashFcn> Element; - typedef __gnu_cxx::hash_map<Key, Element*, HashFcn> table_type; + typedef std::unordered_map<Key, Element*, HashFcn> table_type; friend class CDOhash_map<Key, Data, HashFcn>; @@ -290,8 +278,6 @@ class CDHashMap : public ContextObj { Element* d_first; Context* d_context; - std::vector<Element*> d_trash; - // Nothing to save; the elements take care of themselves virtual ContextObj* save(ContextMemoryManager* pCMM) { Unreachable(); @@ -302,75 +288,38 @@ class CDHashMap : public ContextObj { Unreachable(); } - void emptyTrash() { - //FIXME multithreading - for(typename std::vector<Element*>::iterator i = d_trash.begin(); - i != d_trash.end(); - ++i) { - Debug("gc") << "emptyTrash(): " << *i << std::endl; - (*i)->deleteSelf(); - } - d_trash.clear(); - } - // no copy or assignment CDHashMap(const CDHashMap&) CVC4_UNDEFINED; CDHashMap& operator=(const CDHashMap&) CVC4_UNDEFINED; public: - - CDHashMap(Context* context) : - ContextObj(context), - d_map(), - d_first(NULL), - d_context(context), - d_trash() { - } + CDHashMap(Context* context) + : ContextObj(context), d_map(), d_first(NULL), d_context(context) {} ~CDHashMap() { - Debug("gc") << "cdhashmap" << this - << " disappearing, destroying..." << std::endl; + Debug("gc") << "cdhashmap" << this << " disappearing, destroying..." + << std::endl; destroy(); - Debug("gc") << "cdhashmap" << this - << " disappearing, done destroying" << std::endl; - - Debug("gc") << "cdhashmap" << this << " gone, emptying trash" << std::endl; - emptyTrash(); - Debug("gc") << "done emptying trash for " << this << std::endl; - - for(typename table_type::iterator i = d_map.begin(); - i != d_map.end(); - ++i) { - // mark it as being a destruction (short-circuit restore()) - (*i).second->d_map = NULL; - if(!(*i).second->d_noTrash) { - (*i).second->deleteSelf(); - } - } - d_map.clear(); - d_first = NULL; - - Assert(d_trash.empty()); + Debug("gc") << "cdhashmap" << this << " disappearing, done destroying" + << std::endl; + clear(); } - void clear() throw(AssertionException) { - Debug("gc") << "clearing cdhashmap" << this << ", emptying trash" << std::endl; - emptyTrash(); + void clear() { + Debug("gc") << "clearing cdhashmap" << this << ", emptying trash" + << std::endl; Debug("gc") << "done emptying trash for " << this << std::endl; - for(typename table_type::iterator i = d_map.begin(); - i != d_map.end(); - ++i) { + for (auto& key_element_pair : d_map) { // mark it as being a destruction (short-circuit restore()) - (*i).second->d_map = NULL; - if(!(*i).second->d_noTrash) { - (*i).second->deleteSelf(); + Element* element = key_element_pair.second; + element->d_map = nullptr; + if (!element->d_noTrash) { + element->deleteSelf(); } } d_map.clear(); - d_first = NULL; - - Assert(d_trash.empty()); + d_first = nullptr; } // The usual operators of map @@ -389,8 +338,6 @@ public: // If a key is not present, a new object is created and inserted Element& operator[](const Key& k) { - emptyTrash(); - typename table_type::iterator i = d_map.find(k); Element* obj; @@ -404,8 +351,6 @@ public: } bool insert(const Key& k, const Data& d) { - emptyTrash(); - typename table_type::iterator i = d_map.find(k); if(i == d_map.end()) {// create new object @@ -443,8 +388,6 @@ public: * insertAtContextLevelZero() a key that already is in the map. */ void insertAtContextLevelZero(const Key& k, const Data& d) { - emptyTrash(); - AlwaysAssert(d_map.find(k) == d_map.end()); Element* obj = new(true) Element(d_context, this, k, d, @@ -454,43 +397,6 @@ public: // FIXME: no erase(), too much hassle to implement efficiently... - /** - * "Obliterating" is kind of like erasing, except it's not - * backtrackable; the key is permanently removed from the map. - * (Naturally, it can be re-added as a new element.) - */ - void obliterate(const Key& k) { - typename table_type::iterator i = d_map.find(k); - if(i != d_map.end()) { - Debug("gc") << "key " << k << " obliterated" << std::endl; - // Restore this object to level 0. If it was inserted after level 0, - // nothing else to do as restore will put it in the trash. - (*i).second->destroy(); - - // Check if object was inserted at level 0: in that case, still have - // to do some work. - typename table_type::iterator j = d_map.find(k); - if(j != d_map.end()) { - Element* elt = (*j).second; - if(d_first == elt) { - if(elt->d_next == elt) { - Assert(elt->d_prev == elt); - d_first = NULL; - } else { - d_first = elt->d_next; - } - } - elt->d_prev->d_next = elt->d_next; - elt->d_next->d_prev = elt->d_prev; - d_map.erase(j);//FIXME multithreading - Debug("gc") << "key " << k << " obliterated zero-scope: " << elt << std::endl; - if(!elt->d_noTrash) { - elt->deleteSelf(); - } - } - } - } - class iterator { const Element* d_it; @@ -566,10 +472,6 @@ public: } } - iterator find(const Key& k) { - emptyTrash(); - return const_cast<const CDHashMap*>(this)->find(k); - } };/* class CDHashMap<> */ diff --git a/src/context/cdhashmap_forward.h b/src/context/cdhashmap_forward.h index e099f612e..a8fbc5ee2 100644 --- a/src/context/cdhashmap_forward.h +++ b/src/context/cdhashmap_forward.h @@ -26,15 +26,14 @@ #ifndef __CVC4__CONTEXT__CDHASHMAP_FORWARD_H #define __CVC4__CONTEXT__CDHASHMAP_FORWARD_H +#include <functional> + /// \cond internals -namespace __gnu_cxx { - template <class Key> struct hash; -}/* __gnu_cxx namespace */ namespace CVC4 { namespace context { - template <class Key, class Data, class HashFcn = __gnu_cxx::hash<Key> > + template <class Key, class Data, class HashFcn = std::hash<Key> > class CDHashMap; }/* CVC4::context namespace */ }/* CVC4 namespace */ diff --git a/src/context/cdinsert_hashmap.h b/src/context/cdinsert_hashmap.h index ef8f661fa..db679c1f7 100644 --- a/src/context/cdinsert_hashmap.h +++ b/src/context/cdinsert_hashmap.h @@ -34,7 +34,8 @@ #include "cvc4_private.h" #include <deque> -#include <ext/hash_map> +#include <functional> +#include <unordered_map> #include <utility> #include "base/cvc4_assert.h" @@ -50,14 +51,14 @@ namespace CVC4 { namespace context { -template <class Key, class Data, class HashFcn = __gnu_cxx::hash<Key> > +template <class Key, class Data, class HashFcn = std::hash<Key> > class InsertHashMap { private: typedef std::deque<Key> KeyVec; /** A list of the keys in the map maintained as a stack. */ KeyVec d_keys; - typedef __gnu_cxx::hash_map<Key, Data, HashFcn> HashMap; + typedef std::unordered_map<Key, Data, HashFcn> HashMap; /** The hash_map used for element lookup. */ HashMap d_hashMap; diff --git a/src/context/cdtrail_hashmap.h b/src/context/cdtrail_hashmap.h index 0d265271d..e64c51c65 100644 --- a/src/context/cdtrail_hashmap.h +++ b/src/context/cdtrail_hashmap.h @@ -44,8 +44,9 @@ #pragma once -#include <ext/hash_map> #include <deque> +#include <functional> +#include <unordered_map> #include <utility> #include "base/cvc4_assert.h" @@ -58,7 +59,7 @@ namespace CVC4 { namespace context { -template <class Key, class Data, class HashFcn = __gnu_cxx::hash<Key> > +template <class Key, class Data, class HashFcn = std::hash<Key> > class TrailHashMap { public: /** A pair of Key and Data that mirrors hash_map::value_type. */ @@ -92,7 +93,7 @@ private: KDTVec d_kdts; - typedef __gnu_cxx::hash_map<Key, size_t, HashFcn> PositionMap; + typedef std::unordered_map<Key, size_t, HashFcn> PositionMap; typedef typename PositionMap::iterator PM_iterator; typedef typename PositionMap::const_iterator PM_const_iterator; diff --git a/src/context/cdtrail_hashmap_forward.h b/src/context/cdtrail_hashmap_forward.h index b2beb83bc..970f2758c 100644 --- a/src/context/cdtrail_hashmap_forward.h +++ b/src/context/cdtrail_hashmap_forward.h @@ -25,14 +25,11 @@ #pragma once -namespace __gnu_cxx { - template <class Key> struct hash; -}/* __gnu_cxx namespace */ +#include <functional> namespace CVC4 { namespace context { - template <class Key, class Data, class HashFcn = __gnu_cxx::hash<Key> > + template <class Key, class Data, class HashFcn = std::hash<Key> > class CDTrailHashMap; }/* CVC4::context namespace */ }/* CVC4 namespace */ - diff --git a/src/context/context.cpp b/src/context/context.cpp index 2b781b95c..66d6a6542 100644 --- a/src/context/context.cpp +++ b/src/context/context.cpp @@ -296,6 +296,10 @@ ContextObj::ContextObj(bool allocatedInCMM, Context* pContext) : d_pScope->addToChain(this); } +void ContextObj::enqueueToGarbageCollect() { + Assert(d_pScope != NULL); + d_pScope->enqueueToGarbageCollect(this); +} ContextNotifyObj::ContextNotifyObj(Context* pContext, bool preNotify) { if(preNotify) { @@ -354,6 +358,29 @@ std::ostream& operator<<(std::ostream& out, return out << " --> NULL"; } +Scope::~Scope() { + // Call restore() method on each ContextObj object in the list. + // Note that it is the responsibility of restore() to return the + // next item in the list. + while (d_pContextObjList != NULL) { + d_pContextObjList = d_pContextObjList->restoreAndContinue(); + } + + if (d_garbage) { + while (!d_garbage->empty()) { + ContextObj* obj = d_garbage->back(); + d_garbage->pop_back(); + obj->deleteSelf(); + } + } +} + +void Scope::enqueueToGarbageCollect(ContextObj* obj) { + if (!d_garbage) { + d_garbage.reset(new std::vector<ContextObj*>); + } + d_garbage->push_back(obj); +} } /* CVC4::context namespace */ } /* CVC4 namespace */ diff --git a/src/context/context.h b/src/context/context.h index 9b3f57a5d..92eb10441 100644 --- a/src/context/context.h +++ b/src/context/context.h @@ -19,12 +19,13 @@ #ifndef __CVC4__CONTEXT__CONTEXT_H #define __CVC4__CONTEXT__CONTEXT_H -#include <iostream> #include <cstdlib> #include <cstring> -#include <vector> +#include <iostream> +#include <memory> #include <new> #include <typeinfo> +#include <vector> #include "base/cvc4_assert.h" #include "base/output.h" @@ -257,6 +258,14 @@ class Scope { */ ContextObj* d_pContextObjList; + /** + * A list of ContextObj to be garbage collected before the destruction of this + * scope. deleteSelf() will be called on each element during ~Scope(). + * + * This is either nullptr or list owned by this scope. + */ + std::unique_ptr<std::vector<ContextObj*>> d_garbage; + friend std::ostream& operator<<(std::ostream&, const Scope&) throw(AssertionException); @@ -266,54 +275,60 @@ public: * Constructor: Create a new Scope; set the level and the previous Scope * if any. */ - Scope(Context* pContext, ContextMemoryManager* pCMM, int level) throw() : - d_pContext(pContext), - d_pCMM(pCMM), - d_level(level), - d_pContextObjList(NULL) { + Scope(Context* pContext, ContextMemoryManager* pCMM, int level) throw() + : d_pContext(pContext), + d_pCMM(pCMM), + d_level(level), + d_pContextObjList(nullptr), + d_garbage() {} + + /** + * Destructor: Clears out all of the garbage and restore all of the objects + * in ContextObjList. + */ + ~Scope(); + + /** + * Get the Context for this Scope + */ + Context* getContext() const throw() { return d_pContext; } + + /** + * Get the ContextMemoryManager for this Scope + */ + ContextMemoryManager* getCMM() const throw() { return d_pCMM; } + + /** + * Get the level of the current Scope + */ + int getLevel() const throw() { return d_level; } + + /** + * Return true iff this Scope is the current top Scope + */ + bool isCurrent() const throw() { return this == d_pContext->getTopScope(); } + + /** + * When a ContextObj object is modified for the first time in this + * Scope, it should call this method to add itself to the list of + * objects that will need to be restored. Defined inline below. + */ + void addToChain(ContextObj* pContextObj) throw(AssertionException); + + /** + * Overload operator new for use with ContextMemoryManager to allow + * creation of new Scope objects in the current memory region. + */ + static void* operator new(size_t size, ContextMemoryManager* pCMM) { + Trace("context_mm") << "Scope::new " << size << " in " << pCMM << std::endl; + return pCMM->newData(size); } /** - * Destructor: Restore all of the objects in ContextObjList. Defined inline - * below. - */ - ~Scope(); - - /** - * Get the Context for this Scope - */ - Context* getContext() const throw() { return d_pContext; } - - /** - * Get the ContextMemoryManager for this Scope + * Enqueues a ContextObj to be garbage collected via a call to deleteSelf() + * during the destruction of this scope. */ - ContextMemoryManager* getCMM() const throw() { return d_pCMM; } - - /** - * Get the level of the current Scope - */ - int getLevel() const throw() { return d_level; } - - /** - * Return true iff this Scope is the current top Scope - */ - bool isCurrent() const throw() { return this == d_pContext->getTopScope(); } - - /** - * When a ContextObj object is modified for the first time in this - * Scope, it should call this method to add itself to the list of - * objects that will need to be restored. Defined inline below. - */ - void addToChain(ContextObj* pContextObj) throw(AssertionException); - - /** - * Overload operator new for use with ContextMemoryManager to allow - * creation of new Scope objects in the current memory region. - */ - static void* operator new(size_t size, ContextMemoryManager* pCMM) { - Trace("context_mm") << "Scope::new " << size << " in " << pCMM << std::endl; - return pCMM->newData(size); - } + void enqueueToGarbageCollect(ContextObj* obj); /** * Overload operator delete for Scope objects allocated using @@ -647,6 +662,12 @@ public: ::operator delete(this); } + /** + * Use this to enqueue calling deleteSelf() at the time of the destruction of + * the enclosing Scope. + */ + void enqueueToGarbageCollect(); + };/* class ContextObj */ /** @@ -725,15 +746,6 @@ inline void ContextObj::makeSaveRestorePoint() throw(AssertionException) { update(); } -inline Scope::~Scope() { - // Call restore() method on each ContextObj object in the list. - // Note that it is the responsibility of restore() to return the - // next item in the list. - while(d_pContextObjList != NULL) { - d_pContextObjList = d_pContextObjList->restoreAndContinue(); - } -} - inline void Scope::addToChain(ContextObj* pContextObj) throw(AssertionException) { if(d_pContextObjList != NULL) { diff --git a/src/cvc4.i b/src/cvc4.i index 5f90fdb7d..4768e2344 100644 --- a/src/cvc4.i +++ b/src/cvc4.i @@ -11,7 +11,7 @@ namespace std { class istream; class ostream; template <class T> class set {}; - template <class K, class V, class H> class hash_map {}; + template <class K, class V, class H> class unordered_map {}; } %{ @@ -41,7 +41,7 @@ namespace CVC4 {} using namespace CVC4; #include <cassert> -#include <ext/hash_map> +#include <unordered_map> #include <iosfwd> #include <set> #include <string> @@ -86,7 +86,7 @@ std::set<JavaInputStreamAdapter*> CVC4::JavaInputStreamAdapter::s_adapters; %template(vectorPairStringType) std::vector< std::pair< std::string, CVC4::Type > >; %template(pairStringType) std::pair< std::string, CVC4::Type >; %template(setOfType) std::set< CVC4::Type >; -%template(hashmapExpr) std::hash_map< CVC4::Expr, CVC4::Expr, CVC4::ExprHashFunction >; +%template(hashmapExpr) std::unordered_map< CVC4::Expr, CVC4::Expr, CVC4::ExprHashFunction >; // This is unfortunate, but seems to be necessary; if we leave NULL // defined, swig will expand it to "(void*) 0", and some of swig's diff --git a/src/decision/justification_heuristic.h b/src/decision/justification_heuristic.h index 4c60f94fd..70fecb871 100644 --- a/src/decision/justification_heuristic.h +++ b/src/decision/justification_heuristic.h @@ -23,6 +23,8 @@ #ifndef __CVC4__DECISION__JUSTIFICATION_HEURISTIC #define __CVC4__DECISION__JUSTIFICATION_HEURISTIC +#include <unordered_set> + #include "context/cdhashmap.h" #include "context/cdhashset.h" #include "context/cdlist.h" @@ -78,13 +80,13 @@ class JustificationHeuristic : public ITEDecisionStrategy { * splitter. Can happen when exploring assertion corresponding to a * term-ITE. */ - hash_set<TNode,TNodeHashFunction> d_visited; + std::unordered_set<TNode,TNodeHashFunction> d_visited; /** * Set to track visited nodes in a dfs search done in computeITE * function */ - hash_set<TNode,TNodeHashFunction> d_visitedComputeITE; + std::unordered_set<TNode,TNodeHashFunction> d_visitedComputeITE; /** current decision for the recursive call */ SatLiteral d_curDecision; @@ -177,7 +179,6 @@ private: };/* class JustificationHeuristic */ }/* namespace decision */ - }/* namespace CVC4 */ #endif /* __CVC4__DECISION__JUSTIFICATION_HEURISTIC */ diff --git a/src/expr/attribute.cpp b/src/expr/attribute.cpp index 2f938736e..f221c7c7e 100644 --- a/src/expr/attribute.cpp +++ b/src/expr/attribute.cpp @@ -13,12 +13,12 @@ ** ** AttributeManager implementation. **/ +#include "expr/attribute.h" + #include <utility> #include "base/output.h" -#include "expr/attribute.h" #include "expr/node_value.h" -#include "smt/smt_engine.h" using namespace std; @@ -26,15 +26,6 @@ namespace CVC4 { namespace expr { namespace attr { -SmtAttributes::SmtAttributes(context::Context* ctxt) : - d_cdbools(ctxt), - d_cdints(ctxt), - d_cdtnodes(ctxt), - d_cdnodes(ctxt), - d_cdstrings(ctxt), - d_cdptrs(ctxt) { -} - AttributeManager::AttributeManager() : d_inGarbageCollection(false) {} @@ -43,15 +34,6 @@ bool AttributeManager::inGarbageCollection() const { return d_inGarbageCollection; } -SmtAttributes& AttributeManager::getSmtAttributes(SmtEngine* smt) { - Assert(smt != NULL); - return *smt->d_smtAttributes; -} - -const SmtAttributes& AttributeManager::getSmtAttributes(SmtEngine* smt) const { - return *smt->d_smtAttributes; -} - void AttributeManager::debugHook(int debugFlag) { /* DO NOT CHECK IN ANY CODE INTO THE DEBUG HOOKS! * debugHook() is an empty function for the purpose of debugging @@ -71,17 +53,6 @@ void AttributeManager::deleteAllAttributes(NodeValue* nv) { deleteFromTable(d_ptrs, nv); } -void SmtAttributes::deleteAllAttributes(TNode n) { - NodeValue* nv = n.d_nv; - - d_cdbools.erase(nv); - deleteFromTable(d_cdints, nv); - deleteFromTable(d_cdtnodes, nv); - deleteFromTable(d_cdnodes, nv); - deleteFromTable(d_cdstrings, nv); - deleteFromTable(d_cdptrs, nv); -} - void AttributeManager::deleteAllAttributes() { d_bools.clear(); deleteAllFromTable(d_ints); diff --git a/src/expr/attribute.h b/src/expr/attribute.h index b5897ac51..5aea4a4d1 100644 --- a/src/expr/attribute.h +++ b/src/expr/attribute.h @@ -20,7 +20,6 @@ * attributes and nodes due to template use */ #include "expr/node.h" #include "expr/type_node.h" -#include "context/context.h" #ifndef __CVC4__EXPR__ATTRIBUTE_H #define __CVC4__EXPR__ATTRIBUTE_H @@ -35,45 +34,11 @@ #undef CVC4_ATTRIBUTE_H__INCLUDING__ATTRIBUTE_INTERNALS_H namespace CVC4 { - -class SmtEngine; - -namespace smt { - extern CVC4_THREADLOCAL(SmtEngine*) s_smtEngine_current; -}/* CVC4::smt namespace */ - namespace expr { namespace attr { // ATTRIBUTE MANAGER =========================================================== -struct SmtAttributes { - SmtAttributes(context::Context*); - - // IF YOU ADD ANY TABLES, don't forget to add them also to the - // implementation of deleteAllAttributes(). - - /** Underlying hash table for context-dependent boolean-valued attributes */ - CDAttrHash<bool> d_cdbools; - /** Underlying hash table for context-dependent integral-valued attributes */ - CDAttrHash<uint64_t> d_cdints; - /** Underlying hash table for context-dependent node-valued attributes */ - CDAttrHash<TNode> d_cdtnodes; - /** Underlying hash table for context-dependent node-valued attributes */ - CDAttrHash<Node> d_cdnodes; - /** Underlying hash table for context-dependent string-valued attributes */ - CDAttrHash<std::string> d_cdstrings; - /** Underlying hash table for context-dependent pointer-valued attributes */ - CDAttrHash<void*> d_cdptrs; - - /** Delete all attributes of given node */ - void deleteAllAttributes(TNode n); - - template <class T> - void deleteFromTable(CDAttrHash<T>& table, NodeValue* nv); - -};/* struct SmtAttributes */ - /** * A container for the main attribute tables of the system. There's a * one-to-one NodeManager : AttributeManager correspondence. @@ -103,9 +68,6 @@ class AttributeManager { void clearDeleteAllAttributesBuffer(); - SmtAttributes& getSmtAttributes(SmtEngine*); - const SmtAttributes& getSmtAttributes(SmtEngine*) const; - public: /** Construct an attribute manager. */ @@ -239,10 +201,10 @@ template <> struct getTable<bool, false> { static const AttrTableId id = AttrTableBool; typedef AttrHash<bool> table_type; - static inline table_type& get(AttributeManager& am, SmtEngine* smt) { + static inline table_type& get(AttributeManager& am) { return am.d_bools; } - static inline const table_type& get(const AttributeManager& am, SmtEngine* smt) { + static inline const table_type& get(const AttributeManager& am) { return am.d_bools; } }; @@ -252,10 +214,10 @@ template <> struct getTable<uint64_t, false> { static const AttrTableId id = AttrTableUInt64; typedef AttrHash<uint64_t> table_type; - static inline table_type& get(AttributeManager& am, SmtEngine* smt) { + static inline table_type& get(AttributeManager& am) { return am.d_ints; } - static inline const table_type& get(const AttributeManager& am, SmtEngine* smt) { + static inline const table_type& get(const AttributeManager& am) { return am.d_ints; } }; @@ -265,10 +227,10 @@ template <> struct getTable<TNode, false> { static const AttrTableId id = AttrTableTNode; typedef AttrHash<TNode> table_type; - static inline table_type& get(AttributeManager& am, SmtEngine* smt) { + static inline table_type& get(AttributeManager& am) { return am.d_tnodes; } - static inline const table_type& get(const AttributeManager& am, SmtEngine* smt) { + static inline const table_type& get(const AttributeManager& am) { return am.d_tnodes; } }; @@ -278,10 +240,10 @@ template <> struct getTable<Node, false> { static const AttrTableId id = AttrTableNode; typedef AttrHash<Node> table_type; - static inline table_type& get(AttributeManager& am, SmtEngine* smt) { + static inline table_type& get(AttributeManager& am) { return am.d_nodes; } - static inline const table_type& get(const AttributeManager& am, SmtEngine* smt) { + static inline const table_type& get(const AttributeManager& am) { return am.d_nodes; } }; @@ -291,10 +253,10 @@ template <> struct getTable<TypeNode, false> { static const AttrTableId id = AttrTableTypeNode; typedef AttrHash<TypeNode> table_type; - static inline table_type& get(AttributeManager& am, SmtEngine* smt) { + static inline table_type& get(AttributeManager& am) { return am.d_types; } - static inline const table_type& get(const AttributeManager& am, SmtEngine* smt) { + static inline const table_type& get(const AttributeManager& am) { return am.d_types; } }; @@ -304,10 +266,10 @@ template <> struct getTable<std::string, false> { static const AttrTableId id = AttrTableString; typedef AttrHash<std::string> table_type; - static inline table_type& get(AttributeManager& am, SmtEngine* smt) { + static inline table_type& get(AttributeManager& am) { return am.d_strings; } - static inline const table_type& get(const AttributeManager& am, SmtEngine* smt) { + static inline const table_type& get(const AttributeManager& am) { return am.d_strings; } }; @@ -317,10 +279,10 @@ template <class T> struct getTable<T*, false> { static const AttrTableId id = AttrTablePointer; typedef AttrHash<void*> table_type; - static inline table_type& get(AttributeManager& am, SmtEngine* smt) { + static inline table_type& get(AttributeManager& am) { return am.d_ptrs; } - static inline const table_type& get(const AttributeManager& am, SmtEngine* smt) { + static inline const table_type& get(const AttributeManager& am) { return am.d_ptrs; } }; @@ -330,105 +292,14 @@ template <class T> struct getTable<const T*, false> { static const AttrTableId id = AttrTablePointer; typedef AttrHash<void*> table_type; - static inline table_type& get(AttributeManager& am, SmtEngine* smt) { + static inline table_type& get(AttributeManager& am) { return am.d_ptrs; } - static inline const table_type& get(const AttributeManager& am, SmtEngine* smt) { + static inline const table_type& get(const AttributeManager& am) { return am.d_ptrs; } }; -/** Access the "d_cdbools" member of AttributeManager. */ -template <> -struct getTable<bool, true> { - static const AttrTableId id = AttrTableCDBool; - typedef CDAttrHash<bool> table_type; - static inline table_type& get(AttributeManager& am, SmtEngine* smt) { - return am.getSmtAttributes(smt).d_cdbools; - } - static inline const table_type& get(const AttributeManager& am, SmtEngine* smt) { - return am.getSmtAttributes(smt).d_cdbools; - } -}; - -/** Access the "d_cdints" member of AttributeManager. */ -template <> -struct getTable<uint64_t, true> { - static const AttrTableId id = AttrTableCDUInt64; - typedef CDAttrHash<uint64_t> table_type; - static inline table_type& get(AttributeManager& am, SmtEngine* smt) { - return am.getSmtAttributes(smt).d_cdints; - } - static inline const table_type& get(const AttributeManager& am, SmtEngine* smt) { - return am.getSmtAttributes(smt).d_cdints; - } -}; - -/** Access the "d_tnodes" member of AttributeManager. */ -template <> -struct getTable<TNode, true> { - static const AttrTableId id = AttrTableCDTNode; - typedef CDAttrHash<TNode> table_type; - static inline table_type& get(AttributeManager& am, SmtEngine* smt) { - return am.getSmtAttributes(smt).d_cdtnodes; - } - static inline const table_type& get(const AttributeManager& am, SmtEngine* smt) { - return am.getSmtAttributes(smt).d_cdtnodes; - } -}; - -/** Access the "d_cdnodes" member of AttributeManager. */ -template <> -struct getTable<Node, true> { - static const AttrTableId id = AttrTableCDNode; - typedef CDAttrHash<Node> table_type; - static inline table_type& get(AttributeManager& am, SmtEngine* smt) { - return am.getSmtAttributes(smt).d_cdnodes; - } - static inline const table_type& get(const AttributeManager& am, SmtEngine* smt) { - return am.getSmtAttributes(smt).d_cdnodes; - } -}; - -/** Access the "d_cdstrings" member of AttributeManager. */ -template <> -struct getTable<std::string, true> { - static const AttrTableId id = AttrTableCDString; - typedef CDAttrHash<std::string> table_type; - static inline table_type& get(AttributeManager& am, SmtEngine* smt) { - return am.getSmtAttributes(smt).d_cdstrings; - } - static inline const table_type& get(const AttributeManager& am, SmtEngine* smt) { - return am.getSmtAttributes(smt).d_cdstrings; - } -}; - -/** Access the "d_cdptrs" member of AttributeManager. */ -template <class T> -struct getTable<T*, true> { - static const AttrTableId id = AttrTableCDPointer; - typedef CDAttrHash<void*> table_type; - static inline table_type& get(AttributeManager& am, SmtEngine* smt) { - return am.getSmtAttributes(smt).d_cdptrs; - } - static inline const table_type& get(const AttributeManager& am, SmtEngine* smt) { - return am.getSmtAttributes(smt).d_cdptrs; - } -}; - -/** Access the "d_cdptrs" member of AttributeManager. */ -template <class T> -struct getTable<const T*, true> { - static const AttrTableId id = AttrTableCDPointer; - typedef CDAttrHash<void*> table_type; - static inline table_type& get(AttributeManager& am, SmtEngine* smt) { - return am.getSmtAttributes(smt).d_cdptrs; - } - static inline const table_type& get(const AttributeManager& am, SmtEngine* smt) { - return am.getSmtAttributes(smt).d_cdptrs; - } -}; - }/* CVC4::expr::attr namespace */ // ATTRIBUTE MANAGER IMPLEMENTATIONS =========================================== @@ -445,7 +316,7 @@ AttributeManager::getAttribute(NodeValue* nv, const AttrKind&) const { table_type table_type; const table_type& ah = - getTable<value_type, AttrKind::context_dependent>::get(*this, smt::s_smtEngine_current); + getTable<value_type, AttrKind::context_dependent>::get(*this); typename table_type::const_iterator i = ah.find(std::make_pair(AttrKind::getId(), nv)); @@ -488,7 +359,7 @@ struct HasAttribute<true, AttrKind> { table_type; const table_type& ah = - getTable<value_type, AttrKind::context_dependent>::get(*am, smt::s_smtEngine_current); + getTable<value_type, AttrKind::context_dependent>::get(*am); typename table_type::const_iterator i = ah.find(std::make_pair(AttrKind::getId(), nv)); @@ -516,7 +387,7 @@ struct HasAttribute<false, AttrKind> { table_type table_type; const table_type& ah = - getTable<value_type, AttrKind::context_dependent>::get(*am, smt::s_smtEngine_current); + getTable<value_type, AttrKind::context_dependent>::get(*am); typename table_type::const_iterator i = ah.find(std::make_pair(AttrKind::getId(), nv)); @@ -536,7 +407,7 @@ struct HasAttribute<false, AttrKind> { table_type table_type; const table_type& ah = - getTable<value_type, AttrKind::context_dependent>::get(*am, smt::s_smtEngine_current); + getTable<value_type, AttrKind::context_dependent>::get(*am); typename table_type::const_iterator i = ah.find(std::make_pair(AttrKind::getId(), nv)); @@ -576,7 +447,7 @@ AttributeManager::setAttribute(NodeValue* nv, table_type table_type; table_type& ah = - getTable<value_type, AttrKind::context_dependent>::get(*this, smt::s_smtEngine_current); + getTable<value_type, AttrKind::context_dependent>::get(*this); ah[std::make_pair(AttrKind::getId(), nv)] = mapping::convert(value); } @@ -606,17 +477,6 @@ inline void AttributeManager::deleteFromTable(AttrHash<T>& table, } /** - * Obliterate a NodeValue from a (context-dependent) attribute table. - */ -template <class T> -inline void SmtAttributes::deleteFromTable(CDAttrHash<T>& table, - NodeValue* nv) { - for(unsigned id = 0; id < attr::LastAttributeId<T, true>::getId(); ++id) { - table.obliterate(std::make_pair(id, nv)); - } -} - -/** * Remove all attributes from the table calling the cleanup function * if one is defined. */ diff --git a/src/expr/attribute_internals.h b/src/expr/attribute_internals.h index 861739932..37c7b6a0b 100644 --- a/src/expr/attribute_internals.h +++ b/src/expr/attribute_internals.h @@ -23,9 +23,7 @@ #ifndef __CVC4__EXPR__ATTRIBUTE_INTERNALS_H #define __CVC4__EXPR__ATTRIBUTE_INTERNALS_H -#include <ext/hash_map> - -#include "context/cdhashmap.h" +#include <unordered_map> namespace CVC4 { namespace expr { @@ -152,7 +150,7 @@ namespace attr { */ template <class value_type> class AttrHash : - public __gnu_cxx::hash_map<std::pair<uint64_t, NodeValue*>, + public std::unordered_map<std::pair<uint64_t, NodeValue*>, value_type, AttrHashFunction> { };/* class AttrHash<> */ @@ -163,12 +161,12 @@ class AttrHash : */ template <> class AttrHash<bool> : - protected __gnu_cxx::hash_map<NodeValue*, + protected std::unordered_map<NodeValue*, uint64_t, AttrBoolHashFunction> { /** A "super" type, like in Java, for easy reference below. */ - typedef __gnu_cxx::hash_map<NodeValue*, uint64_t, AttrBoolHashFunction> super; + typedef std::unordered_map<NodeValue*, uint64_t, AttrBoolHashFunction> super; /** * BitAccessor allows us to return a bit "by reference." Of course, @@ -368,217 +366,6 @@ public: } };/* class AttrHash<bool> */ -/** - * A "CDAttrHash<value_type>"---the hash table underlying - * attributes---is simply a context-dependent mapping of - * pair<unique-attribute-id, Node> to value_type using our specialized - * hash function for these pairs. - */ -template <class value_type> -class CDAttrHash : - public context::CDHashMap<std::pair<uint64_t, NodeValue*>, - value_type, - AttrHashFunction> { -public: - CDAttrHash(context::Context* ctxt) : - context::CDHashMap<std::pair<uint64_t, NodeValue*>, - value_type, - AttrHashFunction>(ctxt) { - } -};/* class CDAttrHash<> */ - -/** - * In the case of Boolean-valued attributes we have a special - * "CDAttrHash<bool>" to pack bits together in words. - */ -template <> -class CDAttrHash<bool> : - protected context::CDHashMap<NodeValue*, - uint64_t, - AttrBoolHashFunction> { - - /** A "super" type, like in Java, for easy reference below. */ - typedef context::CDHashMap<NodeValue*, uint64_t, AttrBoolHashFunction> super; - - /** - * BitAccessor allows us to return a bit "by reference." Of course, - * we don't require bit-addressibility supported by the system, we - * do it with a complex type. - */ - class BitAccessor { - - super& d_map; - - NodeValue* d_key; - - uint64_t d_word; - - unsigned d_bit; - - public: - - BitAccessor(super& map, NodeValue* key, uint64_t word, unsigned bit) : - d_map(map), - d_key(key), - d_word(word), - d_bit(bit) { - /* - Debug.printf("cdboolattr", - "CDAttrHash<bool>::BitAccessor(%p, %p, %016llx, %u)\n", - &map, key, (unsigned long long) word, bit); - */ - } - - BitAccessor& operator=(bool b) { - if(b) { - // set the bit - d_word |= (1 << d_bit); - d_map.insert(d_key, d_word); - /* - Debug.printf("cdboolattr", - "CDAttrHash<bool>::BitAccessor::set(%p, %p, %016llx, %u)\n", - &d_map, d_key, (unsigned long long) d_word, d_bit); - */ - } else { - // clear the bit - d_word &= ~(1 << d_bit); - d_map.insert(d_key, d_word); - /* - Debug.printf("cdboolattr", - "CDAttrHash<bool>::BitAccessor::clr(%p, %p, %016llx, %u)\n", - &d_map, d_key, (unsigned long long) d_word, d_bit); - */ - } - - return *this; - } - - operator bool() const { - /* - Debug.printf("cdboolattr", - "CDAttrHash<bool>::BitAccessor::toBool(%p, %p, %016llx, %u)\n", - &d_map, d_key, (unsigned long long) d_word, d_bit); - */ - return (d_word & (1 << d_bit)) ? true : false; - } - };/* class CDAttrHash<bool>::BitAccessor */ - - /** - * A (somewhat degenerate) const_iterator over boolean-valued - * attributes. This const_iterator doesn't support anything except - * comparison and dereference. It's intended just for the result of - * find() on the table. - */ - class ConstBitIterator { - - const std::pair<NodeValue* const, uint64_t> d_entry; - - unsigned d_bit; - - public: - - ConstBitIterator() : - d_entry(), - d_bit(0) { - } - - ConstBitIterator(const std::pair<NodeValue* const, uint64_t>& entry, - unsigned bit) : - d_entry(entry), - d_bit(bit) { - } - - std::pair<NodeValue* const, bool> operator*() { - return std::make_pair(d_entry.first, - (d_entry.second & (1 << d_bit)) ? true : false); - } - - bool operator==(const ConstBitIterator& b) { - return d_entry == b.d_entry && d_bit == b.d_bit; - } - };/* class CDAttrHash<bool>::ConstBitIterator */ - - /* remove non-permitted operations */ - CDAttrHash(const CDAttrHash<bool>&) CVC4_UNDEFINED; - CDAttrHash<bool>& operator=(const CDAttrHash<bool>&) CVC4_UNDEFINED; - -public: - - CDAttrHash(context::Context* context) : super(context) { } - - typedef std::pair<uint64_t, NodeValue*> key_type; - typedef bool data_type; - typedef std::pair<const key_type, data_type> value_type; - - /** an iterator type; see above for limitations */ - typedef ConstBitIterator iterator; - /** a const_iterator type; see above for limitations */ - typedef ConstBitIterator const_iterator; - - /** - * Find the boolean value in the hash table. Returns something == - * end() if not found. - */ - ConstBitIterator find(const std::pair<uint64_t, NodeValue*>& k) const { - super::const_iterator i = super::find(k.second); - if(i == super::end()) { - return ConstBitIterator(); - } - /* - Debug.printf("cdboolattr", - "underlying word at address looks like 0x%016llx, bit is %u\n", - (unsigned long long)((*i).second), - unsigned(k.first)); - */ - return ConstBitIterator(*i, k.first); - } - - /** The "off the end" const_iterator */ - ConstBitIterator end() const { - return ConstBitIterator(); - } - - /** - * Access the hash table using the underlying operator[]. Inserts - * the key into the table (associated to default value) if it's not - * already there. - */ - BitAccessor operator[](const std::pair<uint64_t, NodeValue*>& k) { - uint64_t word = super::operator[](k.second); - return BitAccessor(*this, k.second, word, k.first); - } - - /** - * Delete all flags from the given node. Simply calls superclass's - * obliterate(). Note this removes all attributes at all context - * levels for this NodeValue! This is important when the NodeValue - * is no longer referenced and is being collected, but otherwise - * it probably isn't useful to do this. - */ - void erase(NodeValue* nv) { - super::obliterate(nv); - } - - /** - * Clear the hash table. This simply exposes the protected superclass - * version of clear() to clients. - */ - void clear() { - super::clear(); - } - - /** Is the hash table empty? */ - bool empty() const { - return super::empty(); - } - - /** This is currently very misleading! */ - size_t size() const { - return super::size(); - } - -};/* class CDAttrHash<bool> */ - }/* CVC4::expr::attr namespace */ // ATTRIBUTE CLEANUP FUNCTIONS ================================================= @@ -853,17 +640,6 @@ public: };/* class Attribute<..., bool, ...> */ /** - * This is a context-dependent attribute kind (the only difference - * between CDAttribute<> and Attribute<> (with the fourth argument - * "true") is that you cannot supply a cleanup function (a no-op one - * is used). - */ -template <class T, - class value_type> -struct CDAttribute : - public Attribute<T, value_type, attr::NullCleanupStrategy, true> {}; - -/** * This is a managed attribute kind (the only difference between * ManagedAttribute<> and Attribute<> is the default cleanup function * and the fact that ManagedAttributes cannot be context-dependent). diff --git a/src/expr/datatype.h b/src/expr/datatype.h index 84588fef0..27057ca99 100644 --- a/src/expr/datatype.h +++ b/src/expr/datatype.h @@ -20,6 +20,7 @@ #ifndef __CVC4__DATATYPE_H #define __CVC4__DATATYPE_H +#include <functional> #include <iostream> #include <string> #include <vector> @@ -788,16 +789,16 @@ public: */ struct CVC4_PUBLIC DatatypeHashFunction { inline size_t operator()(const Datatype& dt) const { - return StringHashFunction()(dt.getName()); + return std::hash<std::string>()(dt.getName()); } inline size_t operator()(const Datatype* dt) const { - return StringHashFunction()(dt->getName()); + return std::hash<std::string>()(dt->getName()); } inline size_t operator()(const DatatypeConstructor& dtc) const { - return StringHashFunction()(dtc.getName()); + return std::hash<std::string>()(dtc.getName()); } inline size_t operator()(const DatatypeConstructor* dtc) const { - return StringHashFunction()(dtc->getName()); + return std::hash<std::string>()(dtc->getName()); } };/* struct DatatypeHashFunction */ diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp index cee154743..b0611ccbb 100644 --- a/src/expr/expr_template.cpp +++ b/src/expr/expr_template.cpp @@ -115,7 +115,7 @@ static Node exportConstant(TNode n, NodeManager* to, ExprManagerMapCollection& v class ExportPrivate { private: - typedef std::hash_map <NodeTemplate<false>, NodeTemplate<true>, TNodeHashFunction> ExportCache; + typedef std::unordered_map <NodeTemplate<false>, NodeTemplate<true>, TNodeHashFunction> ExportCache; ExprManager* from; ExprManager* to; ExprManagerMapCollection& vmap; @@ -393,7 +393,7 @@ static inline NodePairIteratorAdaptor<Iterator> mkNodePairIteratorAdaptor(Iterat return NodePairIteratorAdaptor<Iterator>(i); } -Expr Expr::substitute(const std::hash_map<Expr, Expr, ExprHashFunction> map) const { +Expr Expr::substitute(const std::unordered_map<Expr, Expr, ExprHashFunction> map) const { ExprManagerScope ems(*this); return Expr(d_exprManager, new Node(d_node->substitute(mkNodePairIteratorAdaptor(map.begin()), mkNodePairIteratorAdaptor(map.end())))); } diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h index 57b4ff93a..d2ad45dee 100644 --- a/src/expr/expr_template.h +++ b/src/expr/expr_template.h @@ -29,8 +29,8 @@ ${includes} #include <stdint.h> #include <iostream> #include <iterator> - #include <string> +#include <unordered_map> #include "base/exception.h" #include "options/language.h" @@ -433,7 +433,7 @@ public: /** * Substitute pairs of (ex,replacement) from the given map. */ - Expr substitute(const std::hash_map<Expr, Expr, ExprHashFunction> map) const; + Expr substitute(const std::unordered_map<Expr, Expr, ExprHashFunction> map) const; /** * Returns the string representation of the expression. diff --git a/src/expr/node.h b/src/expr/node.h index 69bb98f95..7a8bafe38 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -22,13 +22,16 @@ #ifndef __CVC4__NODE_H #define __CVC4__NODE_H -#include <vector> -#include <string> -#include <iostream> -#include <utility> +#include <stdint.h> + #include <algorithm> #include <functional> -#include <stdint.h> +#include <iostream> +#include <string> +#include <unordered_map> +#include <unordered_set> +#include <utility> +#include <vector> #include "base/configuration.h" #include "base/cvc4_assert.h" @@ -42,7 +45,6 @@ #include "options/language.h" #include "options/set_language.h" #include "util/utility.h" -#include "util/hash.h" namespace CVC4 { @@ -243,7 +245,7 @@ public: * member function with a similar signature. */ Node substitute(TNode node, TNode replacement, - std::hash_map<TNode, TNode, TNodeHashFunction>& cache) const; + std::unordered_map<TNode, TNode, TNodeHashFunction>& cache) const; /** * Cache-aware, recursive version of substitute() used by the public @@ -252,7 +254,7 @@ public: template <class Iterator1, class Iterator2> Node substitute(Iterator1 nodesBegin, Iterator1 nodesEnd, Iterator2 replacementsBegin, Iterator2 replacementsEnd, - std::hash_map<TNode, TNode, TNodeHashFunction>& cache) const; + std::unordered_map<TNode, TNode, TNodeHashFunction>& cache) const; /** * Cache-aware, recursive version of substitute() used by the public @@ -260,7 +262,7 @@ public: */ template <class Iterator> Node substitute(Iterator substitutionsBegin, Iterator substitutionsEnd, - std::hash_map<TNode, TNode, TNodeHashFunction>& cache) const; + std::unordered_map<TNode, TNode, TNodeHashFunction>& cache) const; /** Default constructor, makes a null expression. */ NodeTemplate() : d_nv(&expr::NodeValue::null()) { } @@ -943,8 +945,6 @@ inline std::ostream& operator<<(std::ostream& out, }/* CVC4 namespace */ -#include <ext/hash_map> - //#include "expr/attribute.h" #include "expr/node_manager.h" #include "expr/type_checker.h" @@ -1296,14 +1296,14 @@ NodeTemplate<ref_count>::substitute(TNode node, TNode replacement) const { if (node == *this) { return replacement; } - std::hash_map<TNode, TNode, TNodeHashFunction> cache; + std::unordered_map<TNode, TNode, TNodeHashFunction> cache; return substitute(node, replacement, cache); } template <bool ref_count> Node NodeTemplate<ref_count>::substitute(TNode node, TNode replacement, - std::hash_map<TNode, TNode, TNodeHashFunction>& cache) const { + std::unordered_map<TNode, TNode, TNodeHashFunction>& cache) const { Assert(node != *this); if (getNumChildren() == 0) { @@ -1311,7 +1311,7 @@ NodeTemplate<ref_count>::substitute(TNode node, TNode replacement, } // in cache? - typename std::hash_map<TNode, TNode, TNodeHashFunction>::const_iterator i = cache.find(*this); + typename std::unordered_map<TNode, TNode, TNodeHashFunction>::const_iterator i = cache.find(*this); if(i != cache.end()) { return (*i).second; } @@ -1351,7 +1351,7 @@ NodeTemplate<ref_count>::substitute(Iterator1 nodesBegin, Iterator1 nodesEnd, Iterator2 replacementsBegin, Iterator2 replacementsEnd) const { - std::hash_map<TNode, TNode, TNodeHashFunction> cache; + std::unordered_map<TNode, TNode, TNodeHashFunction> cache; return substitute(nodesBegin, nodesEnd, replacementsBegin, replacementsEnd, cache); } @@ -1363,9 +1363,9 @@ NodeTemplate<ref_count>::substitute(Iterator1 nodesBegin, Iterator1 nodesEnd, Iterator2 replacementsBegin, Iterator2 replacementsEnd, - std::hash_map<TNode, TNode, TNodeHashFunction>& cache) const { + std::unordered_map<TNode, TNode, TNodeHashFunction>& cache) const { // in cache? - typename std::hash_map<TNode, TNode, TNodeHashFunction>::const_iterator i = cache.find(*this); + typename std::unordered_map<TNode, TNode, TNodeHashFunction>::const_iterator i = cache.find(*this); if(i != cache.end()) { return (*i).second; } @@ -1410,7 +1410,7 @@ template <class Iterator> inline Node NodeTemplate<ref_count>::substitute(Iterator substitutionsBegin, Iterator substitutionsEnd) const { - std::hash_map<TNode, TNode, TNodeHashFunction> cache; + std::unordered_map<TNode, TNode, TNodeHashFunction> cache; return substitute(substitutionsBegin, substitutionsEnd, cache); } @@ -1419,9 +1419,9 @@ template <class Iterator> Node NodeTemplate<ref_count>::substitute(Iterator substitutionsBegin, Iterator substitutionsEnd, - std::hash_map<TNode, TNode, TNodeHashFunction>& cache) const { + std::unordered_map<TNode, TNode, TNodeHashFunction>& cache) const { // in cache? - typename std::hash_map<TNode, TNode, TNodeHashFunction>::const_iterator i = cache.find(*this); + typename std::unordered_map<TNode, TNode, TNodeHashFunction>::const_iterator i = cache.find(*this); if(i != cache.end()) { return (*i).second; } @@ -1468,7 +1468,7 @@ inline Node NodeTemplate<true>::fromExpr(const Expr& e) { template<bool ref_count> bool NodeTemplate<ref_count>::hasSubterm(NodeTemplate<false> t, bool strict) const { - typedef std::hash_set<TNode, TNodeHashFunction> node_set; + typedef std::unordered_set<TNode, TNodeHashFunction> node_set; if (!strict && *this == t) { return true; diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index f7a1d98d6..e440261cb 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -18,7 +18,6 @@ #include "expr/node_manager.h" #include <algorithm> -#include <ext/hash_set> #include <stack> #include <utility> @@ -36,7 +35,6 @@ using namespace std; using namespace CVC4::expr; -using __gnu_cxx::hash_set; namespace CVC4 { diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 44c116558..f112381d8 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -30,7 +30,7 @@ #include <vector> #include <string> -#include <ext/hash_set> +#include <unordered_set> #include "base/tls.h" #include "expr/kind.h" @@ -95,12 +95,12 @@ class NodeManager { bool operator()(expr::NodeValue* nv) { return nv->d_rc > 0; } }; - typedef __gnu_cxx::hash_set<expr::NodeValue*, - expr::NodeValuePoolHashFunction, - expr::NodeValuePoolEq> NodeValuePool; - typedef __gnu_cxx::hash_set<expr::NodeValue*, - expr::NodeValueIDHashFunction, - expr::NodeValueIDEquality> NodeValueIDSet; + typedef std::unordered_set<expr::NodeValue*, + expr::NodeValuePoolHashFunction, + expr::NodeValuePoolEq> NodeValuePool; + typedef std::unordered_set<expr::NodeValue*, + expr::NodeValueIDHashFunction, + expr::NodeValueIDEquality> NodeValueIDSet; static CVC4_THREADLOCAL(NodeManager*) s_current; diff --git a/src/expr/record.h b/src/expr/record.h index 685756112..7c5854db2 100644 --- a/src/expr/record.h +++ b/src/expr/record.h @@ -19,11 +19,11 @@ #ifndef __CVC4__RECORD_H #define __CVC4__RECORD_H +#include <functional> #include <iostream> #include <string> #include <vector> #include <utility> -#include "util/hash.h" // Forward Declarations namespace CVC4 { @@ -56,13 +56,13 @@ public: struct CVC4_PUBLIC RecordSelectHashFunction { inline size_t operator()(const RecordSelect& t) const { - return StringHashFunction()(t.getField()); + return std::hash<std::string>()(t.getField()); } };/* struct RecordSelectHashFunction */ struct CVC4_PUBLIC RecordUpdateHashFunction { inline size_t operator()(const RecordUpdate& t) const { - return StringHashFunction()(t.getField()); + return std::hash<std::string>()(t.getField()); } };/* struct RecordUpdateHashFunction */ diff --git a/src/expr/symbol_table.cpp b/src/expr/symbol_table.cpp index 864ade423..7fd938a9b 100644 --- a/src/expr/symbol_table.cpp +++ b/src/expr/symbol_table.cpp @@ -36,8 +36,8 @@ namespace CVC4 { SymbolTable::SymbolTable() : d_context(new Context()), - d_exprMap(new(true) CDHashMap<std::string, Expr, StringHashFunction>(d_context)), - d_typeMap(new(true) CDHashMap<std::string, pair<vector<Type>, Type>, StringHashFunction>(d_context)), + d_exprMap(new(true) CDHashMap<std::string, Expr>(d_context)), + d_typeMap(new(true) CDHashMap<std::string, pair<vector<Type>, Type>>(d_context)), d_functions(new(true) CDHashSet<Expr, ExprHashFunction>(d_context)) { } @@ -74,7 +74,7 @@ bool SymbolTable::isBound(const std::string& name) const throw() { } bool SymbolTable::isBoundDefinedFunction(const std::string& name) const throw() { - CDHashMap<std::string, Expr, StringHashFunction>::iterator found = + CDHashMap<std::string, Expr>::iterator found = d_exprMap->find(name); return found != d_exprMap->end() && d_functions->contains((*found).second); } diff --git a/src/expr/symbol_table.h b/src/expr/symbol_table.h index cefa65d0a..7c3b13003 100644 --- a/src/expr/symbol_table.h +++ b/src/expr/symbol_table.h @@ -21,7 +21,6 @@ #include <vector> #include <utility> -#include <ext/hash_map> #include "expr/expr.h" #include "util/hash.h" @@ -50,10 +49,11 @@ class CVC4_PUBLIC SymbolTable { context::Context* d_context; /** A map for expressions. */ - context::CDHashMap<std::string, Expr, StringHashFunction> *d_exprMap; + context::CDHashMap<std::string, Expr>* d_exprMap; /** A map for types. */ - context::CDHashMap<std::string, std::pair<std::vector<Type>, Type>, StringHashFunction> *d_typeMap; + context::CDHashMap<std::string, std::pair<std::vector<Type>, Type> >* + d_typeMap; /** A set of defined functions. */ context::CDHashSet<Expr, ExprHashFunction> *d_functions; diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp index 383a31dd0..a4ab2f3b7 100644 --- a/src/expr/type_node.cpp +++ b/src/expr/type_node.cpp @@ -31,9 +31,9 @@ TypeNode TypeNode::s_null( &expr::NodeValue::null() ); TypeNode TypeNode::substitute(const TypeNode& type, const TypeNode& replacement, - std::hash_map<TypeNode, TypeNode, HashFunction>& cache) const { + std::unordered_map<TypeNode, TypeNode, HashFunction>& cache) const { // in cache? - std::hash_map<TypeNode, TypeNode, HashFunction>::const_iterator i = cache.find(*this); + std::unordered_map<TypeNode, TypeNode, HashFunction>::const_iterator i = cache.find(*this); if(i != cache.end()) { return (*i).second; } diff --git a/src/expr/type_node.h b/src/expr/type_node.h index 8dd80bc37..65b422a53 100644 --- a/src/expr/type_node.h +++ b/src/expr/type_node.h @@ -22,11 +22,13 @@ #ifndef __CVC4__TYPE_NODE_H #define __CVC4__TYPE_NODE_H -#include <vector> -#include <string> -#include <iostream> #include <stdint.h> +#include <iostream> +#include <string> +#include <unordered_map> +#include <vector> + #include "base/cvc4_assert.h" #include "expr/kind.h" #include "expr/metakind.h" @@ -93,7 +95,7 @@ private: * member function with a similar signature. */ TypeNode substitute(const TypeNode& type, const TypeNode& replacement, - std::hash_map<TypeNode, TypeNode, HashFunction>& cache) const; + std::unordered_map<TypeNode, TypeNode, HashFunction>& cache) const; /** * Cache-aware, recursive version of substitute() used by the public @@ -102,7 +104,7 @@ private: template <class Iterator1, class Iterator2> TypeNode substitute(Iterator1 typesBegin, Iterator1 typesEnd, Iterator2 replacementsBegin, Iterator2 replacementsEnd, - std::hash_map<TypeNode, TypeNode, HashFunction>& cache) const; + std::unordered_map<TypeNode, TypeNode, HashFunction>& cache) const; public: @@ -670,8 +672,6 @@ typedef TypeNode::HashFunction TypeNodeHashFunction; }/* CVC4 namespace */ -#include <ext/hash_map> - #include "expr/node_manager.h" namespace CVC4 { @@ -687,7 +687,7 @@ inline TypeNode TypeNode::fromType(const Type& t) { inline TypeNode TypeNode::substitute(const TypeNode& type, const TypeNode& replacement) const { - std::hash_map<TypeNode, TypeNode, HashFunction> cache; + std::unordered_map<TypeNode, TypeNode, HashFunction> cache; return substitute(type, replacement, cache); } @@ -697,7 +697,7 @@ TypeNode::substitute(Iterator1 typesBegin, Iterator1 typesEnd, Iterator2 replacementsBegin, Iterator2 replacementsEnd) const { - std::hash_map<TypeNode, TypeNode, HashFunction> cache; + std::unordered_map<TypeNode, TypeNode, HashFunction> cache; return substitute(typesBegin, typesEnd, replacementsBegin, replacementsEnd, cache); } @@ -707,9 +707,9 @@ TypeNode TypeNode::substitute(Iterator1 typesBegin, Iterator1 typesEnd, Iterator2 replacementsBegin, Iterator2 replacementsEnd, - std::hash_map<TypeNode, TypeNode, HashFunction>& cache) const { + std::unordered_map<TypeNode, TypeNode, HashFunction>& cache) const { // in cache? - std::hash_map<TypeNode, TypeNode, HashFunction>::const_iterator i = cache.find(*this); + std::unordered_map<TypeNode, TypeNode, HashFunction>::const_iterator i = cache.find(*this); if(i != cache.end()) { return (*i).second; } diff --git a/src/expr/variable_type_map.h b/src/expr/variable_type_map.h index 739a8d425..94d9c2f67 100644 --- a/src/expr/variable_type_map.h +++ b/src/expr/variable_type_map.h @@ -20,8 +20,9 @@ #ifndef __CVC4__VARIABLE_TYPE_MAP_H #define __CVC4__VARIABLE_TYPE_MAP_H +#include <unordered_map> + #include "expr/expr.h" -#include "util/hash.h" namespace CVC4 { @@ -35,13 +36,13 @@ class CVC4_PUBLIC VariableTypeMap { * A map Expr -> Expr, intended to be used for a mapping of variables * between two ExprManagers. */ - std::hash_map<Expr, Expr, ExprHashFunction> d_variables; + std::unordered_map<Expr, Expr, ExprHashFunction> d_variables; /** * A map Type -> Type, intended to be used for a mapping of types * between two ExprManagers. */ - std::hash_map<Type, Type, TypeHashFunction> d_types; + std::unordered_map<Type, Type, TypeHashFunction> d_types; public: Expr& operator[](Expr e) { return d_variables[e]; } @@ -49,7 +50,7 @@ public: };/* class VariableTypeMap */ -typedef __gnu_cxx::hash_map<uint64_t, uint64_t> VarMap; +typedef std::unordered_map<uint64_t, uint64_t> VarMap; struct CVC4_PUBLIC ExprManagerMapCollection { VariableTypeMap d_typeMap; diff --git a/src/parser/smt1/smt1.cpp b/src/parser/smt1/smt1.cpp index 02f0566a7..c4e670f6d 100644 --- a/src/parser/smt1/smt1.cpp +++ b/src/parser/smt1/smt1.cpp @@ -12,21 +12,17 @@ ** Definitions of SMT-LIB (v1) constants. **/ -#include <ext/hash_map> -namespace std { - using namespace __gnu_cxx; -} +#include "parser/smt1/smt1.h" #include "expr/type.h" #include "smt/command.h" #include "parser/parser.h" -#include "parser/smt1/smt1.h" namespace CVC4 { namespace parser { -std::hash_map<const std::string, Smt1::Logic, CVC4::StringHashFunction> Smt1::newLogicMap() { - std::hash_map<const std::string, Smt1::Logic, CVC4::StringHashFunction> logicMap; +std::unordered_map<std::string, Smt1::Logic> Smt1::newLogicMap() { + std::unordered_map<std::string, Smt1::Logic> logicMap; logicMap["AUFLIA"] = AUFLIA; logicMap["AUFLIRA"] = AUFLIRA; logicMap["AUFNIRA"] = AUFNIRA; @@ -68,7 +64,7 @@ std::hash_map<const std::string, Smt1::Logic, CVC4::StringHashFunction> Smt1::ne } Smt1::Logic Smt1::toLogic(const std::string& name) { - static std::hash_map<const std::string, Smt1::Logic, CVC4::StringHashFunction> logicMap = newLogicMap(); + static std::unordered_map<std::string, Smt1::Logic> logicMap = newLogicMap(); return logicMap[name]; } diff --git a/src/parser/smt1/smt1.h b/src/parser/smt1/smt1.h index 7036aad64..e9dbea1a9 100644 --- a/src/parser/smt1/smt1.h +++ b/src/parser/smt1/smt1.h @@ -17,10 +17,9 @@ #ifndef __CVC4__PARSER__SMT1_H #define __CVC4__PARSER__SMT1_H -#include <ext/hash_map> -namespace std { using namespace __gnu_cxx; } +#include <string> +#include <unordered_map> -#include "util/hash.h" #include "parser/parser.h" namespace CVC4 { @@ -117,7 +116,7 @@ public: private: void addArithmeticOperators(); - static std::hash_map<const std::string, Logic, CVC4::StringHashFunction> newLogicMap(); + static std::unordered_map<std::string, Logic> newLogicMap(); };/* class Smt1 */ }/* CVC4::parser namespace */ diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 88709c29a..c7156635d 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -117,6 +117,7 @@ namespace CVC4 { #include <set> #include <sstream> #include <string> +#include <unordered_set> #include <vector> #include "base/output.h" @@ -150,7 +151,7 @@ using namespace CVC4::parser; #define MK_CONST EXPR_MANAGER->mkConst #define UNSUPPORTED PARSER_STATE->unimplementedFeature -static bool isClosed(const Expr& e, std::set<Expr>& free, std::hash_set<Expr, ExprHashFunction>& closedCache) { +static bool isClosed(const Expr& e, std::set<Expr>& free, std::unordered_set<Expr, ExprHashFunction>& closedCache) { if(closedCache.find(e) != closedCache.end()) { return true; } @@ -181,7 +182,7 @@ static bool isClosed(const Expr& e, std::set<Expr>& free, std::hash_set<Expr, Ex } static inline bool isClosed(const Expr& e, std::set<Expr>& free) { - std::hash_set<Expr, ExprHashFunction> cache; + std::unordered_set<Expr, ExprHashFunction> cache; return isClosed(e, free, cache); } @@ -898,7 +899,7 @@ sygusGTerm[CVC4::SygusGTerm& sgt, std::string& fun] sgt.d_gterm_type = SygusGTerm::gterm_op; sgt.d_expr = EXPR_MANAGER->operatorOf(k); } - | LET_TOK LPAREN_TOK { + | SYGUS_LET_TOK LPAREN_TOK { sgt.d_name = std::string("let"); sgt.d_gterm_type = SygusGTerm::gterm_let; PARSER_STATE->pushScope(true); @@ -1798,12 +1799,11 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2] Expr attexpr; std::vector<Expr> patexprs; std::vector<Expr> patconds; - std::hash_set<std::string, StringHashFunction> names; + std::unordered_set<std::string> names; std::vector< std::pair<std::string, Expr> > binders; Type type; std::string s; bool isBuiltinOperator = false; - bool readLetSort = false; int match_vindex = -1; std::vector<Type> match_ptypes; } @@ -2005,27 +2005,41 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2] expr = MK_CONST( ::CVC4::ArrayStoreAll(type, f) ); } ) - | /* a let binding */ - LPAREN_TOK LET_TOK LPAREN_TOK - { PARSER_STATE->pushScope(true); } - ( LPAREN_TOK symbol[name,CHECK_NONE,SYM_VARIABLE] - (term[expr, f2] | sortSymbol[type,CHECK_DECLARED] - { readLetSort = true; } term[expr, f2] - ) - RPAREN_TOK - // this is a parallel let, so we have to save up all the contributions - // of the let and define them only later on - { if( !PARSER_STATE->sygus() && readLetSort ){ - PARSER_STATE->parseError("Bad syntax for let term."); - }else if(names.count(name) == 1) { - std::stringstream ss; - ss << "warning: symbol `" << name << "' bound multiple times by let;" - << " the last binding will be used, shadowing earlier ones"; - PARSER_STATE->warning(ss.str()); - } else { - names.insert(name); - } - binders.push_back(std::make_pair(name, expr)); } )+ + | /* a let or sygus let binding */ + LPAREN_TOK ( + LET_TOK LPAREN_TOK + { PARSER_STATE->pushScope(true); } + ( LPAREN_TOK symbol[name,CHECK_NONE,SYM_VARIABLE] + term[expr, f2] + RPAREN_TOK + // this is a parallel let, so we have to save up all the contributions + // of the let and define them only later on + { if(names.count(name) == 1) { + std::stringstream ss; + ss << "warning: symbol `" << name << "' bound multiple times by let;" + << " the last binding will be used, shadowing earlier ones"; + PARSER_STATE->warning(ss.str()); + } else { + names.insert(name); + } + binders.push_back(std::make_pair(name, expr)); } )+ | + SYGUS_LET_TOK LPAREN_TOK + { PARSER_STATE->pushScope(true); } + ( LPAREN_TOK symbol[name,CHECK_NONE,SYM_VARIABLE] + sortSymbol[type,CHECK_DECLARED] + term[expr, f2] + RPAREN_TOK + // this is a parallel let, so we have to save up all the contributions + // of the let and define them only later on + { if(names.count(name) == 1) { + std::stringstream ss; + ss << "warning: symbol `" << name << "' bound multiple times by let;" + << " the last binding will be used, shadowing earlier ones"; + PARSER_STATE->warning(ss.str()); + } else { + names.insert(name); + } + binders.push_back(std::make_pair(name, expr)); } )+ ) { // now implement these bindings for(std::vector< std::pair<std::string, Expr> >::iterator i = binders.begin(); i != binders.end(); ++i) { @@ -3004,7 +3018,8 @@ EXIT_TOK : 'exit'; RESET_TOK : { PARSER_STATE->v2_5(false) }? 'reset'; RESET_ASSERTIONS_TOK : 'reset-assertions'; ITE_TOK : 'ite'; -LET_TOK : 'let'; +LET_TOK : { !PARSER_STATE->sygus() }? 'let'; +SYGUS_LET_TOK : { PARSER_STATE->sygus() }? 'let'; ATTRIBUTE_TOK : '!'; LPAREN_TOK : '('; RPAREN_TOK : ')'; diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h index 3eed0e871..e470c8111 100644 --- a/src/parser/smt2/smt2.h +++ b/src/parser/smt2/smt2.h @@ -22,6 +22,7 @@ #include <sstream> #include <stack> #include <string> +#include <unordered_map> #include <utility> #include "parser/parser.h" @@ -58,7 +59,7 @@ public: private: bool d_logicSet; LogicInfo d_logic; - std::hash_map<std::string, Kind, StringHashFunction> operatorKindMap; + std::unordered_map<std::string, Kind> operatorKindMap; std::pair<Expr, std::string> d_lastNamedTerm; // this is a user-context stack std::stack< std::map<Expr, std::string> > d_unsatCoreNames; diff --git a/src/parser/tptp/tptp.h b/src/parser/tptp/tptp.h index f137a9d92..3afd29415 100644 --- a/src/parser/tptp/tptp.h +++ b/src/parser/tptp/tptp.h @@ -22,7 +22,8 @@ #define __CVC4__PARSER__TPTP_H #include <cassert> -#include <ext/hash_set> +#include <unordered_map> +#include <unordered_set> #include "parser/parser.h" #include "smt/command.h" @@ -45,8 +46,8 @@ class Tptp : public Parser { Expr d_utr_op; Expr d_uts_op; // The set of expression that already have a bridge - std::hash_set<Expr, ExprHashFunction> d_r_converted; - std::hash_map<std::string, Expr, StringHashFunction> d_distinct_objects; + std::unordered_set<Expr, ExprHashFunction> d_r_converted; + std::unordered_map<std::string, Expr> d_distinct_objects; std::vector< pANTLR3_INPUT_STREAM > d_in_created; diff --git a/src/printer/dagification_visitor.h b/src/printer/dagification_visitor.h index 1f89d36f6..6cbe5f863 100644 --- a/src/printer/dagification_visitor.h +++ b/src/printer/dagification_visitor.h @@ -19,12 +19,13 @@ #ifndef __CVC4__PRINTER__DAGIFICATION_VISITOR_H #define __CVC4__PRINTER__DAGIFICATION_VISITOR_H +#include <string> +#include <unordered_map> +#include <vector> + #include "expr/node.h" #include "util/hash.h" -#include <vector> -#include <string> - namespace CVC4 { namespace context { @@ -65,7 +66,7 @@ class DagificationVisitor { /** * A map of subexprs to their occurrence count. */ - std::hash_map<TNode, unsigned, TNodeHashFunction> d_nodeCount; + std::unordered_map<TNode, unsigned, TNodeHashFunction> d_nodeCount; /** * The top-most node we are visiting. @@ -109,7 +110,7 @@ class DagificationVisitor { * in independently dagifying the child. (If it is beyond the threshold * and occurs in more than one parent, we'll independently dagify.) */ - std::hash_map<TNode, TNode, TNodeHashFunction> d_uniqueParent; + std::unordered_map<TNode, TNode, TNodeHashFunction> d_uniqueParent; /** * A list of all nodes that meet the occurrence threshold and therefore diff --git a/src/proof/arith_proof.h b/src/proof/arith_proof.h index a3868fe46..3de53f866 100644 --- a/src/proof/arith_proof.h +++ b/src/proof/arith_proof.h @@ -19,6 +19,8 @@ #ifndef __CVC4__ARITH__PROOF_H #define __CVC4__ARITH__PROOF_H +#include <unordered_set> + #include "expr/expr.h" #include "proof/proof_manager.h" #include "proof/theory_proof.h" @@ -45,7 +47,7 @@ class TheoryArith; } } -typedef __gnu_cxx::hash_set<Type, TypeHashFunction > TypeSet; +typedef std::unordered_set<Type, TypeHashFunction > TypeSet; class ArithProof : public TheoryProof { diff --git a/src/proof/array_proof.h b/src/proof/array_proof.h index 507b65fef..9a2eef9e7 100644 --- a/src/proof/array_proof.h +++ b/src/proof/array_proof.h @@ -19,6 +19,8 @@ #ifndef __CVC4__ARRAY__PROOF_H #define __CVC4__ARRAY__PROOF_H +#include <unordered_set> + #include "expr/expr.h" #include "proof/proof_manager.h" #include "proof/theory_proof.h" @@ -94,7 +96,7 @@ class TheoryArrays; } /* namespace CVC4::theory::arrays */ } /* namespace CVC4::theory */ -typedef __gnu_cxx::hash_set<Type, TypeHashFunction > TypeSet; +typedef std::unordered_set<Type, TypeHashFunction > TypeSet; class ArrayProof : public TheoryProof { // TODO: whatever goes in this theory diff --git a/src/proof/bitvector_proof.h b/src/proof/bitvector_proof.h index 4c390e86f..69f9e774b 100644 --- a/src/proof/bitvector_proof.h +++ b/src/proof/bitvector_proof.h @@ -19,12 +19,11 @@ #ifndef __CVC4__BITVECTOR__PROOF_H #define __CVC4__BITVECTOR__PROOF_H -//#include <cstdint> -#include <ext/hash_map> -#include <ext/hash_set> #include <iostream> #include <set> #include <sstream> +#include <unordered_map> +#include <unordered_set> #include <vector> #include "expr/expr.h" @@ -56,11 +55,11 @@ typedef TSatProof< CVC4::BVMinisat::Solver> BVSatProof; template <class Solver> class LFSCSatProof; typedef LFSCSatProof< CVC4::BVMinisat::Solver> LFSCBVSatProof; -typedef __gnu_cxx::hash_set<Expr, ExprHashFunction> ExprSet; -typedef __gnu_cxx::hash_map<Expr, ClauseId, ExprHashFunction> ExprToClauseId; -typedef __gnu_cxx::hash_map<Expr, unsigned, ExprHashFunction> ExprToId; -typedef __gnu_cxx::hash_map<Expr, Expr, ExprHashFunction> ExprToExpr; -typedef __gnu_cxx::hash_map<Expr, std::string, ExprHashFunction> ExprToString; +typedef std::unordered_set<Expr, ExprHashFunction> ExprSet; +typedef std::unordered_map<Expr, ClauseId, ExprHashFunction> ExprToClauseId; +typedef std::unordered_map<Expr, unsigned, ExprHashFunction> ExprToId; +typedef std::unordered_map<Expr, Expr, ExprHashFunction> ExprToExpr; +typedef std::unordered_map<Expr, std::string, ExprHashFunction> ExprToString; class BitVectorProof : public TheoryProof { protected: diff --git a/src/proof/cnf_proof.h b/src/proof/cnf_proof.h index 0cc0bf93e..a0d7096c0 100644 --- a/src/proof/cnf_proof.h +++ b/src/proof/cnf_proof.h @@ -21,9 +21,9 @@ #ifndef __CVC4__CNF_PROOF_H #define __CVC4__CNF_PROOF_H -#include <ext/hash_map> -#include <ext/hash_set> #include <iosfwd> +#include <unordered_map> +#include <unordered_set> #include "context/cdhashmap.h" #include "proof/clause_id.h" @@ -38,9 +38,9 @@ namespace prop { class CnfProof; -typedef __gnu_cxx::hash_map<prop::SatVariable, Expr> SatVarToExpr; -typedef __gnu_cxx::hash_map<Node, Node, NodeHashFunction> NodeToNode; -typedef __gnu_cxx::hash_set<ClauseId> ClauseIdSet; +typedef std::unordered_map<prop::SatVariable, Expr> SatVarToExpr; +typedef std::unordered_map<Node, Node, NodeHashFunction> NodeToNode; +typedef std::unordered_set<ClauseId> ClauseIdSet; typedef context::CDHashMap<ClauseId, Node> ClauseIdToNode; typedef context::CDHashMap<Node, ProofRule, NodeHashFunction> NodeToProofRule; diff --git a/src/proof/proof_manager.h b/src/proof/proof_manager.h index 2510b770a..f77a96726 100644 --- a/src/proof/proof_manager.h +++ b/src/proof/proof_manager.h @@ -20,7 +20,9 @@ #define __CVC4__PROOF_MANAGER_H #include <iosfwd> -#include <map> +#include <unordered_map> +#include <unordered_set> + #include "expr/node.h" #include "context/cdhashset.h" #include "context/cdhashmap.h" @@ -96,13 +98,11 @@ enum ProofFormat { std::string append(const std::string& str, uint64_t num); -typedef __gnu_cxx::hash_map < ClauseId, prop::SatClause* > IdToSatClause; -typedef __gnu_cxx::hash_set<Expr, ExprHashFunction> ExprSet; +typedef std::unordered_map<ClauseId, prop::SatClause*> IdToSatClause; typedef context::CDHashSet<Expr, ExprHashFunction> CDExprSet; -typedef __gnu_cxx::hash_set<Node, NodeHashFunction > NodeSet; -typedef __gnu_cxx::hash_map<Node, std::vector<Node>, NodeHashFunction > NodeToNodes; -typedef context::CDHashMap<Node, std::vector<Node>, NodeHashFunction > CDNodeToNodes; -typedef std::hash_set<ClauseId> IdHashSet; +typedef std::unordered_map<Node, std::vector<Node>, NodeHashFunction> NodeToNodes; +typedef context::CDHashMap<Node, std::vector<Node>, NodeHashFunction> CDNodeToNodes; +typedef std::unordered_set<ClauseId> IdHashSet; enum ProofRule { RULE_GIVEN, /* input assertion */ diff --git a/src/proof/proof_output_channel.h b/src/proof/proof_output_channel.h index 74d159bec..b114ec25f 100644 --- a/src/proof/proof_output_channel.h +++ b/src/proof/proof_output_channel.h @@ -16,6 +16,8 @@ #ifndef __CVC4__PROOF_OUTPUT_CHANNEL_H #define __CVC4__PROOF_OUTPUT_CHANNEL_H +#include <unordered_set> + #include "theory/output_channel.h" namespace CVC4 { @@ -42,7 +44,7 @@ public: class MyPreRegisterVisitor { theory::Theory* d_theory; - __gnu_cxx::hash_set<TNode, TNodeHashFunction> d_visited; + std::unordered_set<TNode, TNodeHashFunction> d_visited; public: typedef void return_type; MyPreRegisterVisitor(theory::Theory* theory); diff --git a/src/proof/proof_utils.h b/src/proof/proof_utils.h index d7ac80fc8..7c0660a83 100644 --- a/src/proof/proof_utils.h +++ b/src/proof/proof_utils.h @@ -20,14 +20,16 @@ #pragma once #include <set> -#include <vector> #include <sstream> +#include <unordered_set> +#include <vector> + #include "expr/node_manager.h" namespace CVC4 { -typedef __gnu_cxx::hash_set<Expr, ExprHashFunction> ExprSet; -typedef __gnu_cxx::hash_set<Node, NodeHashFunction> NodeSet; +typedef std::unordered_set<Expr, ExprHashFunction> ExprSet; +typedef std::unordered_set<Node, NodeHashFunction> NodeSet; typedef std::pair<Node, Node> NodePair; typedef std::set<NodePair> NodePairSet; diff --git a/src/proof/sat_proof.h b/src/proof/sat_proof.h index 7c9631896..6b2b39fd4 100644 --- a/src/proof/sat_proof.h +++ b/src/proof/sat_proof.h @@ -21,11 +21,10 @@ #include <stdint.h> -#include <ext/hash_map> -#include <ext/hash_set> #include <iosfwd> #include <set> #include <sstream> +#include <unordered_map> #include <vector> #include "context/cdhashmap.h" @@ -101,18 +100,18 @@ class TSatProof { typedef std::set<typename Solver::TLit> LitSet; typedef std::set<typename Solver::TVar> VarSet; - typedef std::hash_map<ClauseId, typename Solver::TCRef> IdCRefMap; - typedef std::hash_map<typename Solver::TCRef, ClauseId> ClauseIdMap; + typedef std::unordered_map<ClauseId, typename Solver::TCRef> IdCRefMap; + typedef std::unordered_map<typename Solver::TCRef, ClauseId> ClauseIdMap; typedef context::CDHashMap<ClauseId, typename Solver::TLit> IdUnitMap; typedef context::CDHashMap<int, ClauseId> UnitIdMap; typedef context::CDHashMap<ClauseId, ResolutionChain*> IdResMap; - typedef std::hash_map<ClauseId, uint64_t> IdProofRuleMap; + typedef std::unordered_map<ClauseId, uint64_t> IdProofRuleMap; typedef std::vector<ResolutionChain*> ResStack; typedef std::set<ClauseId> IdSet; typedef std::vector<typename Solver::TLit> LitVector; - typedef __gnu_cxx::hash_map<ClauseId, typename Solver::TClause&> + typedef std::unordered_map<ClauseId, typename Solver::TClause&> IdToMinisatClause; - typedef __gnu_cxx::hash_map<ClauseId, LitVector*> IdToConflicts; + typedef std::unordered_map<ClauseId, LitVector*> IdToConflicts; public: TSatProof(Solver* solver, context::Context* context, @@ -362,7 +361,7 @@ class TSatProof { IdToSatClause d_seenLemmas; private: - __gnu_cxx::hash_map<ClauseId, int> d_glueMap; + std::unordered_map<ClauseId, int> d_glueMap; struct Statistics { IntStat d_numLearnedClauses; IntStat d_numLearnedInProof; diff --git a/src/proof/skolemization_manager.cpp b/src/proof/skolemization_manager.cpp index 2234b7b19..a666e23d3 100644 --- a/src/proof/skolemization_manager.cpp +++ b/src/proof/skolemization_manager.cpp @@ -57,11 +57,11 @@ void SkolemizationManager::clear() { d_skolemToDisequality.clear(); } -std::hash_map<Node, Node, NodeHashFunction>::const_iterator SkolemizationManager::begin() { +std::unordered_map<Node, Node, NodeHashFunction>::const_iterator SkolemizationManager::begin() { return d_disequalityToSkolem.begin(); } -std::hash_map<Node, Node, NodeHashFunction>::const_iterator SkolemizationManager::end() { +std::unordered_map<Node, Node, NodeHashFunction>::const_iterator SkolemizationManager::end() { return d_disequalityToSkolem.end(); } diff --git a/src/proof/skolemization_manager.h b/src/proof/skolemization_manager.h index 02aa6b6f0..7ec594859 100644 --- a/src/proof/skolemization_manager.h +++ b/src/proof/skolemization_manager.h @@ -21,7 +21,8 @@ #define __CVC4__SKOLEMIZATION_MANAGER_H #include <iostream> -#include <map> +#include <unordered_map> + #include "proof/proof.h" #include "util/proof.h" #include "expr/node.h" @@ -39,12 +40,12 @@ public: bool isSkolem(Node skolem); void clear(); - std::hash_map<Node, Node, NodeHashFunction>::const_iterator begin(); - std::hash_map<Node, Node, NodeHashFunction>::const_iterator end(); + std::unordered_map<Node, Node, NodeHashFunction>::const_iterator begin(); + std::unordered_map<Node, Node, NodeHashFunction>::const_iterator end(); private: - std::hash_map<Node, Node, NodeHashFunction> d_disequalityToSkolem; - std::hash_map<Node, Node, NodeHashFunction> d_skolemToDisequality; + std::unordered_map<Node, Node, NodeHashFunction> d_disequalityToSkolem; + std::unordered_map<Node, Node, NodeHashFunction> d_skolemToDisequality; }; }/* CVC4 namespace */ diff --git a/src/proof/theory_proof.h b/src/proof/theory_proof.h index 541e4ce82..15ac533b7 100644 --- a/src/proof/theory_proof.h +++ b/src/proof/theory_proof.h @@ -20,8 +20,9 @@ #ifndef __CVC4__THEORY_PROOF_H #define __CVC4__THEORY_PROOF_H -#include <ext/hash_set> #include <iosfwd> +#include <unordered_map> +#include <unordered_set> #include "expr/expr.h" #include "proof/clause_id.h" @@ -35,11 +36,11 @@ namespace theory { class Theory; } /* namespace CVC4::theory */ -typedef __gnu_cxx::hash_map < ClauseId, prop::SatClause* > IdToSatClause; +typedef std::unordered_map < ClauseId, prop::SatClause* > IdToSatClause; class TheoryProof; -typedef __gnu_cxx::hash_set<Expr, ExprHashFunction > ExprSet; +typedef std::unordered_set<Expr, ExprHashFunction > ExprSet; typedef std::map<theory::TheoryId, TheoryProof* > TheoryProofTable; typedef std::set<theory::TheoryId> TheoryIdSet; diff --git a/src/proof/uf_proof.h b/src/proof/uf_proof.h index 1fb1c4683..b817ceb69 100644 --- a/src/proof/uf_proof.h +++ b/src/proof/uf_proof.h @@ -19,6 +19,8 @@ #ifndef __CVC4__UF__PROOF_H #define __CVC4__UF__PROOF_H +#include <unordered_set> + #include "expr/expr.h" #include "proof/proof_manager.h" #include "theory/uf/equality_engine.h" @@ -45,7 +47,7 @@ class TheoryUF; } } -typedef __gnu_cxx::hash_set<Type, TypeHashFunction > TypeSet; +typedef std::unordered_set<Type, TypeHashFunction > TypeSet; class UFProof : public TheoryProof { diff --git a/src/prop/bvminisat/core/Solver.cc b/src/prop/bvminisat/core/Solver.cc index d626a5d15..0213ef7e3 100644 --- a/src/prop/bvminisat/core/Solver.cc +++ b/src/prop/bvminisat/core/Solver.cc @@ -990,7 +990,7 @@ lbool Solver::search(int nof_conflicts, UIP uip) if(d_bvp){ ClauseId id = d_bvp->getSatProof()->registerClause(cr, LEARNT); PSTATS( - __gnu_cxx::hash_set<int> cl_levels; + std::unordered_set<int> cl_levels; for (int i = 0; i < learnt_clause.size(); ++i) { cl_levels.insert(level(var(learnt_clause[i]))); } diff --git a/src/prop/bvminisat/core/Solver.h b/src/prop/bvminisat/core/Solver.h index 555495149..485eb8535 100644 --- a/src/prop/bvminisat/core/Solver.h +++ b/src/prop/bvminisat/core/Solver.h @@ -21,7 +21,6 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #ifndef BVMinisat_Solver_h #define BVMinisat_Solver_h -#include <ext/hash_set> #include <vector> #include "context/context.h" diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h index affcc2999..80f8742a3 100644 --- a/src/prop/cnf_stream.h +++ b/src/prop/cnf_stream.h @@ -25,8 +25,6 @@ #ifndef __CVC4__PROP__CNF_STREAM_H #define __CVC4__PROP__CNF_STREAM_H -#include <ext/hash_map> - #include "context/cdinsert_hashmap.h" #include "context/cdlist.h" #include "expr/node.h" diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc index 0bf5d5d7c..2b58f2f17 100644 --- a/src/prop/minisat/core/Solver.cc +++ b/src/prop/minisat/core/Solver.cc @@ -23,6 +23,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include <math.h> #include <iostream> +#include <unordered_set> #include "base/output.h" #include "options/prop_options.h" @@ -1219,7 +1220,7 @@ lbool Solver::search(int nof_conflicts) PROOF( ClauseId id = ProofManager::getSatProof()->registerClause(cr, LEARNT); PSTATS( - __gnu_cxx::hash_set<int> cl_levels; + std::unordered_set<int> cl_levels; for (int i = 0; i < learnt_clause.size(); ++i) { cl_levels.insert(level(var(learnt_clause[i]))); } diff --git a/src/prop/theory_proxy.h b/src/prop/theory_proxy.h index 510a12eb2..67d3b3b7e 100644 --- a/src/prop/theory_proxy.h +++ b/src/prop/theory_proxy.h @@ -24,6 +24,7 @@ #define __CVC4_USE_MINISAT #include <iosfwd> +#include <unordered_set> #include "context/cdqueue.h" #include "expr/expr_stream.h" @@ -138,7 +139,7 @@ public: * Set of all lemmas that have been "shared" in the portfolio---i.e., * all imported and exported lemmas. */ - std::hash_set<Node, NodeHashFunction> d_shared; + std::unordered_set<Node, NodeHashFunction> d_shared; /** * Statistic: the number of replayed decisions (via --replay). diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 327f978e4..704303826 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -18,7 +18,8 @@ #include <algorithm> #include <cctype> -#include <ext/hash_map> +#include <unordered_map> +#include <unordered_set> #include <iterator> #include <sstream> #include <stack> @@ -463,8 +464,8 @@ class PrintSuccessListener : public Listener { class SmtEnginePrivate : public NodeManagerListener { SmtEngine& d_smt; - typedef hash_map<Node, Node, NodeHashFunction> NodeToNodeHashMap; - typedef hash_map<Node, bool, NodeHashFunction> NodeToBoolHashMap; + typedef unordered_map<Node, Node, NodeHashFunction> NodeToNodeHashMap; + typedef unordered_map<Node, bool, NodeHashFunction> NodeToBoolHashMap; /** * Manager for limiting time and abstract resource usage. @@ -634,7 +635,7 @@ private: * conjuncts. */ size_t removeFromConjunction(Node& n, - const std::hash_set<unsigned long>& toRemove); + const std::unordered_set<unsigned long>& toRemove); /** Scrub miplib encodings. */ void doMiplibTrick(); @@ -794,9 +795,7 @@ public: } } - void nmNotifyDeleteNode(TNode n) { - d_smt.d_smtAttributes->deleteAllAttributes(n); - } + void nmNotifyDeleteNode(TNode n) {} Node applySubstitutions(TNode node) const { return Rewriter::rewrite(d_topLevelSubstitutions.apply(node)); @@ -981,14 +980,12 @@ SmtEngine::SmtEngine(ExprManager* em) throw() : d_status(), d_replayStream(NULL), d_private(NULL), - d_smtAttributes(NULL), d_statisticsRegistry(NULL), d_stats(NULL), d_channels(new LemmaChannels()) { SmtScope smts(this); d_originalOptions.copyValues(em->getOptions()); - d_smtAttributes = new expr::attr::SmtAttributes(d_context); d_private = new smt::SmtEnginePrivate(*this); d_statisticsRegistry = new StatisticsRegistry(); d_stats = new SmtEngineStatistics(); @@ -1204,9 +1201,6 @@ SmtEngine::~SmtEngine() throw() { delete d_private; d_private = NULL; - delete d_smtAttributes; - d_smtAttributes = NULL; - delete d_userContext; d_userContext = NULL; delete d_context; @@ -2262,7 +2256,7 @@ bool SmtEngine::isDefinedFunction( Expr func ){ return d_definedFunctions->find(nf) != d_definedFunctions->end(); } -Node SmtEnginePrivate::expandDefinitions(TNode n, hash_map<Node, Node, NodeHashFunction>& cache, bool expandOnly) +Node SmtEnginePrivate::expandDefinitions(TNode n, unordered_map<Node, Node, NodeHashFunction>& cache, bool expandOnly) throw(TypeCheckingException, LogicException, UnsafeInterruptException) { stack< triple<Node, Node, bool> > worklist; @@ -2302,7 +2296,7 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, hash_map<Node, Node, NodeHashF } // maybe it's in the cache - hash_map<Node, Node, NodeHashFunction>::iterator cacheHit = cache.find(n); + unordered_map<Node, Node, NodeHashFunction>::iterator cacheHit = cache.find(n); if(cacheHit != cache.end()) { TNode ret = (*cacheHit).second; result.push(ret.isNull() ? n : ret); @@ -2434,7 +2428,7 @@ struct intToBV_stack_element { : node(node), children_added(false) {} };/* struct intToBV_stack_element */ -typedef std::hash_map<Node, Node, NodeHashFunction> NodeMap; +typedef std::unordered_map<Node, Node, NodeHashFunction> NodeMap; Node SmtEnginePrivate::intToBVMakeBinary(TNode n, NodeMap& cache) { // Do a topological sort of the subexpressions and substitute them @@ -3038,7 +3032,7 @@ bool SmtEnginePrivate::nonClausalSimplify() { Trace("simplify") << "Resize non-clausal learned literals to " << j << std::endl; d_nonClausalLearnedLiterals.resize(j); - hash_set<TNode, TNodeHashFunction> s; + unordered_set<TNode, TNodeHashFunction> s; Trace("debugging") << "NonClausal simplify pre-preprocess\n"; for (unsigned i = 0; i < d_assertions.size(); ++ i) { Node assertion = d_assertions[i]; @@ -3273,7 +3267,7 @@ void SmtEnginePrivate::traceBackToAssertions(const std::vector<Node>& nodes, std } } -size_t SmtEnginePrivate::removeFromConjunction(Node& n, const std::hash_set<unsigned long>& toRemove) { +size_t SmtEnginePrivate::removeFromConjunction(Node& n, const std::unordered_set<unsigned long>& toRemove) { Assert(n.getKind() == kind::AND); size_t removals = 0; for(Node::iterator j = n.begin(); j != n.end(); ++j) { @@ -3327,12 +3321,12 @@ void SmtEnginePrivate::doMiplibTrick() { Assert(!options::incrementalSolving()); const booleans::CircuitPropagator::BackEdgesMap& backEdges = d_propagator.getBackEdges(); - hash_set<unsigned long> removeAssertions; + unordered_set<unsigned long> removeAssertions; NodeManager* nm = NodeManager::currentNM(); Node zero = nm->mkConst(Rational(0)), one = nm->mkConst(Rational(1)); - hash_map<TNode, Node, TNodeHashFunction> intVars; + unordered_map<TNode, Node, TNodeHashFunction> intVars; for(vector<Node>::const_iterator i = d_boolVars.begin(); i != d_boolVars.end(); ++i) { if(d_propagator.isAssigned(*i)) { Debug("miplib") << "ineligible: " << *i << " because assigned " << d_propagator.getAssignment(*i) << endl; @@ -3826,9 +3820,9 @@ Result SmtEngine::quickCheck() { } -void SmtEnginePrivate::collectSkolems(TNode n, set<TNode>& skolemSet, hash_map<Node, bool, NodeHashFunction>& cache) +void SmtEnginePrivate::collectSkolems(TNode n, set<TNode>& skolemSet, unordered_map<Node, bool, NodeHashFunction>& cache) { - hash_map<Node, bool, NodeHashFunction>::iterator it; + unordered_map<Node, bool, NodeHashFunction>::iterator it; it = cache.find(n); if (it != cache.end()) { return; @@ -3852,9 +3846,9 @@ void SmtEnginePrivate::collectSkolems(TNode n, set<TNode>& skolemSet, hash_map<N } -bool SmtEnginePrivate::checkForBadSkolems(TNode n, TNode skolem, hash_map<Node, bool, NodeHashFunction>& cache) +bool SmtEnginePrivate::checkForBadSkolems(TNode n, TNode skolem, unordered_map<Node, bool, NodeHashFunction>& cache) { - hash_map<Node, bool, NodeHashFunction>::iterator it; + unordered_map<Node, bool, NodeHashFunction>::iterator it; it = cache.find(n); if (it != cache.end()) { return (*it).second; @@ -3925,7 +3919,7 @@ void SmtEnginePrivate::processAssertions() { Chat() << "expanding definitions..." << endl; Trace("simplify") << "SmtEnginePrivate::simplify(): expanding definitions" << endl; TimerStat::CodeTimer codeTimer(d_smt.d_stats->d_definitionExpansionTime); - hash_map<Node, Node, NodeHashFunction> cache; + unordered_map<Node, Node, NodeHashFunction> cache; for(unsigned i = 0; i < d_assertions.size(); ++ i) { d_assertions.replace(i, expandDefinitions(d_assertions[i], cache)); } @@ -3944,8 +3938,8 @@ void SmtEnginePrivate::processAssertions() { Debug("smt") << " d_assertions : " << d_assertions.size() << endl; if( options::nlExtPurify() ){ - hash_map<Node, Node, NodeHashFunction> cache; - hash_map<Node, Node, NodeHashFunction> bcache; + unordered_map<Node, Node, NodeHashFunction> cache; + unordered_map<Node, Node, NodeHashFunction> bcache; std::vector< Node > var_eq; for (unsigned i = 0; i < d_assertions.size(); ++ i) { d_assertions.replace(i, purifyNlTerms(d_assertions[i], cache, bcache, var_eq)); @@ -3966,7 +3960,7 @@ void SmtEnginePrivate::processAssertions() { if (options::solveRealAsInt()) { Chat() << "converting reals to ints..." << endl; - hash_map<Node, Node, NodeHashFunction> cache; + unordered_map<Node, Node, NodeHashFunction> cache; std::vector< Node > var_eq; for(unsigned i = 0; i < d_assertions.size(); ++ i) { d_assertions.replace(i, realToInt(d_assertions[i], cache, var_eq)); @@ -3982,7 +3976,7 @@ void SmtEnginePrivate::processAssertions() { if (options::solveIntAsBV() > 0) { Chat() << "converting ints to bit-vectors..." << endl; - hash_map<Node, Node, NodeHashFunction> cache; + unordered_map<Node, Node, NodeHashFunction> cache; for(unsigned i = 0; i < d_assertions.size(); ++ i) { d_assertions.replace(i, intToBV(d_assertions[i], cache)); } @@ -4210,7 +4204,7 @@ void SmtEnginePrivate::processAssertions() { // For each skolem variable sk, let iteExpr = iteMap(sk) be the ite expr mapped to by sk. // cache for expression traversal - hash_map<Node, bool, NodeHashFunction> cache; + unordered_map<Node, bool, NodeHashFunction> cache; // First, find all skolems that appear in the substitution map - their associated iteExpr will need // to be moved to the main assertion set @@ -4663,7 +4657,7 @@ Expr SmtEngine::expandDefinitions(const Expr& ex) throw(TypeCheckingException, L if(Dump.isOn("benchmark")) { Dump("benchmark") << ExpandDefinitionsCommand(e); } - hash_map<Node, Node, NodeHashFunction> cache; + unordered_map<Node, Node, NodeHashFunction> cache; Node n = d_private->expandDefinitions(Node::fromExpr(e), cache, /* expandOnly = */ true); n = postprocess(n, TypeNode::fromType(e.getType())); @@ -4708,7 +4702,7 @@ Expr SmtEngine::getValue(const Expr& ex) const throw(ModalException, TypeCheckin TypeNode expectedType = n.getType(); // Expand, then normalize - hash_map<Node, Node, NodeHashFunction> cache; + unordered_map<Node, Node, NodeHashFunction> cache; n = d_private->expandDefinitions(n, cache); // There are two ways model values for terms are computed (for historical // reasons). One way is that used in check-model; the other is that @@ -4821,7 +4815,7 @@ CVC4::SExpr SmtEngine::getAssignment() { Trace("smt") << "--- getting value of " << *i << endl; // Expand, then normalize - hash_map<Node, Node, NodeHashFunction> cache; + unordered_map<Node, Node, NodeHashFunction> cache; Node n = d_private->expandDefinitions(*i, cache); n = Rewriter::rewrite(n); @@ -5063,7 +5057,7 @@ void SmtEngine::checkModel(bool hardFailure) { // Apply any define-funs from the problem. { - hash_map<Node, Node, NodeHashFunction> cache; + unordered_map<Node, Node, NodeHashFunction> cache; n = d_private->expandDefinitions(n, cache); } Notice() << "SmtEngine::checkModel(): -- expands to " << n << endl; diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 3df1dbea8..ed265e2b8 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -74,13 +74,6 @@ namespace prop { class PropEngine; }/* CVC4::prop namespace */ -namespace expr { - namespace attr { - class AttributeManager; - struct SmtAttributes; - }/* CVC4::expr::attr namespace */ -}/* CVC4::expr namespace */ - namespace smt { /** * Representation of a defined function. We keep these around in @@ -357,20 +350,9 @@ class CVC4_PUBLIC SmtEngine { // to access d_modelCommands friend class ::CVC4::Model; friend class ::CVC4::theory::TheoryModel; - // to access SmtAttributes - friend class expr::attr::AttributeManager; // to access getModel(), which is private (for now) friend class GetModelCommand; - /** - * There's something of a handshake between the expr package's - * AttributeManager and the SmtEngine because the expr package - * doesn't have a Context on its own (that's owned by the - * SmtEngine). Thus all context-dependent attributes are stored - * here. - */ - expr::attr::SmtAttributes* d_smtAttributes; - StatisticsRegistry* d_statisticsRegistry; smt::SmtEngineStatistics* d_stats; diff --git a/src/smt/term_formula_removal.h b/src/smt/term_formula_removal.h index 535e6fb52..854ddc61e 100644 --- a/src/smt/term_formula_removal.h +++ b/src/smt/term_formula_removal.h @@ -18,6 +18,7 @@ #pragma once +#include <unordered_map> #include <vector> #include "context/cdinsert_hashmap.h" @@ -33,7 +34,7 @@ namespace theory { class ContainsTermITEVisitor; }/* CVC4::theory namespace */ -typedef std::hash_map<Node, unsigned, NodeHashFunction> IteSkolemMap; +typedef std::unordered_map<Node, unsigned, NodeHashFunction> IteSkolemMap; class RemoveTermFormulas { typedef context::CDInsertHashMap< std::pair<Node, int>, Node, PairHashFunction<Node, int, NodeHashFunction, BoolHashFunction> > ITECache; diff --git a/src/smt_util/nary_builder.h b/src/smt_util/nary_builder.h index 244420e66..dde7e1ccd 100644 --- a/src/smt_util/nary_builder.h +++ b/src/smt_util/nary_builder.h @@ -20,7 +20,9 @@ #pragma once +#include <unordered_map> #include <vector> + #include "expr/node.h" namespace CVC4{ @@ -47,7 +49,7 @@ private: Node case_assoccomm(TNode n); Node case_other(TNode n); - typedef std::hash_map<Node, Node, NodeHashFunction> NodeMap; + typedef std::unordered_map<Node, Node, NodeHashFunction> NodeMap; NodeMap d_cache; };/* class RePairAssocCommutativeOperators */ diff --git a/src/theory/arith/arith_ite_utils.h b/src/theory/arith/arith_ite_utils.h index 47f1caf9e..e2d0d2baf 100644 --- a/src/theory/arith/arith_ite_utils.h +++ b/src/theory/arith/arith_ite_utils.h @@ -15,11 +15,6 @@ ** \todo document this file **/ - - - - - // Pass 1: label the ite as (constant) or (+ constant variable) #include "cvc4_private.h" @@ -27,9 +22,9 @@ #ifndef __CVC4__THEORY__ARITH__ARITH_ITE_UTILS_H #define __CVC4__THEORY__ARITH__ARITH_ITE_UTILS_H +#include <unordered_map> + #include "expr/node.h" -#include <ext/hash_map> -#include <ext/hash_set> #include "context/cdo.h" #include "context/cdtrail_hashmap.h" @@ -46,7 +41,7 @@ class ArithIteUtils { SubstitutionMap* d_subs; TheoryModel* d_model; - typedef std::hash_map<Node, Node, NodeHashFunction> NodeMap; + typedef std::unordered_map<Node, Node, NodeHashFunction> NodeMap; // cache for reduce vars NodeMap d_reduceVar; // if reduceVars[n].isNull(), treat reduceVars[n] == n @@ -56,7 +51,7 @@ class ArithIteUtils { NodeMap d_reduceGcd; - typedef std::hash_map<Node, Integer, NodeHashFunction> NodeIntegerMap; + typedef std::unordered_map<Node, Integer, NodeHashFunction> NodeIntegerMap; NodeIntegerMap d_gcds; Integer d_one; diff --git a/src/theory/arith/arith_utilities.h b/src/theory/arith/arith_utilities.h index 68d4d8f1a..4a9539d49 100644 --- a/src/theory/arith/arith_utilities.h +++ b/src/theory/arith/arith_utilities.h @@ -19,7 +19,8 @@ #ifndef __CVC4__THEORY__ARITH__ARITH_UTILITIES_H #define __CVC4__THEORY__ARITH__ARITH_UTILITIES_H -#include <ext/hash_map> +#include <unordered_map> +#include <unordered_set> #include <vector> #include "context/cdhashset.h" @@ -35,12 +36,12 @@ namespace theory { namespace arith { //Sets of Nodes -typedef __gnu_cxx::hash_set<Node, NodeHashFunction> NodeSet; -typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> TNodeSet; +typedef std::unordered_set<Node, NodeHashFunction> NodeSet; +typedef std::unordered_set<TNode, TNodeHashFunction> TNodeSet; typedef context::CDHashSet<Node, NodeHashFunction> CDNodeSet; //Maps from Nodes -> ArithVars, and vice versa -typedef __gnu_cxx::hash_map<Node, ArithVar, NodeHashFunction> NodeToArithVarMap; +typedef std::unordered_map<Node, ArithVar, NodeHashFunction> NodeToArithVarMap; typedef DenseMap<Node> ArithVarToNodeMap; inline Node mkRationalNode(const Rational& q){ diff --git a/src/theory/arith/constraint.cpp b/src/theory/arith/constraint.cpp index 9ba4074c1..3427edbd3 100644 --- a/src/theory/arith/constraint.cpp +++ b/src/theory/arith/constraint.cpp @@ -16,8 +16,9 @@ **/ #include "theory/arith/constraint.h" -#include <ostream> #include <algorithm> +#include <ostream> +#include <unordered_set> #include "base/output.h" #include "proof/proof.h" @@ -1333,7 +1334,7 @@ struct ConstraintCPHash { }; void Constraint::assertionFringe(ConstraintCPVec& v){ - hash_set<ConstraintCP, ConstraintCPHash> visited; + unordered_set<ConstraintCP, ConstraintCPHash> visited; size_t writePos = 0; if(!v.empty()){ diff --git a/src/theory/arith/constraint.h b/src/theory/arith/constraint.h index 662327301..25f838567 100644 --- a/src/theory/arith/constraint.h +++ b/src/theory/arith/constraint.h @@ -75,7 +75,7 @@ #ifndef __CVC4__THEORY__ARITH__CONSTRAINT_H #define __CVC4__THEORY__ARITH__CONSTRAINT_H -#include <ext/hash_map> +#include <unordered_map> #include <list> #include <set> #include <vector> @@ -145,7 +145,7 @@ enum ConstraintType {LowerBound, Equality, UpperBound, Disequality}; typedef context::CDList<ConstraintCP> CDConstraintList; -typedef __gnu_cxx::hash_map<Node, ConstraintP, NodeHashFunction> NodetoConstraintMap; +typedef std::unordered_map<Node, ConstraintP, NodeHashFunction> NodetoConstraintMap; typedef size_t ConstraintRuleID; static const ConstraintRuleID ConstraintRuleIdSentinel = std::numeric_limits<ConstraintRuleID>::max(); diff --git a/src/theory/arith/cut_log.h b/src/theory/arith/cut_log.h index 77273f609..7d41666e7 100644 --- a/src/theory/arith/cut_log.h +++ b/src/theory/arith/cut_log.h @@ -20,7 +20,7 @@ #pragma once -#include <ext/hash_map> +#include <unordered_map> #include <map> #include <set> #include <vector> @@ -179,7 +179,7 @@ private: int d_upId; public: - typedef __gnu_cxx::hash_map<int, ArithVar> RowIdMap; + typedef std::unordered_map<int, ArithVar> RowIdMap; private: RowIdMap d_rowId2ArithVar; diff --git a/src/theory/arith/dio_solver.cpp b/src/theory/arith/dio_solver.cpp index d862dabbd..5b61385f3 100644 --- a/src/theory/arith/dio_solver.cpp +++ b/src/theory/arith/dio_solver.cpp @@ -304,7 +304,7 @@ bool DioSolver::queueEmpty() const{ } Node DioSolver::columnGcdIsOne() const{ - std::hash_map<Node, Integer, NodeHashFunction> gcdMap; + std::unordered_map<Node, Integer, NodeHashFunction> gcdMap; std::deque<TrailIndex>::const_iterator iter, end; for(iter = d_currentF.begin(), end = d_currentF.end(); iter != end; ++iter){ diff --git a/src/theory/arith/dio_solver.h b/src/theory/arith/dio_solver.h index 2b8b64e75..292f2b856 100644 --- a/src/theory/arith/dio_solver.h +++ b/src/theory/arith/dio_solver.h @@ -20,6 +20,7 @@ #ifndef __CVC4__THEORY__ARITH__DIO_SOLVER_H #define __CVC4__THEORY__ARITH__DIO_SOLVER_H +#include <unordered_map> #include <utility> #include <vector> @@ -68,7 +69,7 @@ private: * We maintain a map from the variables associated with proofs to an input constraint. * These variables can then be used in polynomial manipulations. */ - typedef std::hash_map<Node, InputConstraintIndex, NodeHashFunction> NodeToInputConstraintIndexMap; + typedef std::unordered_map<Node, InputConstraintIndex, NodeHashFunction> NodeToInputConstraintIndexMap; NodeToInputConstraintIndexMap d_varToInputConstraintMap; Node proofVariableToReason(const Variable& v) const{ diff --git a/src/theory/arith/pseudoboolean_proc.h b/src/theory/arith/pseudoboolean_proc.h index 471e37fa1..0b91ed074 100644 --- a/src/theory/arith/pseudoboolean_proc.h +++ b/src/theory/arith/pseudoboolean_proc.h @@ -19,7 +19,7 @@ #pragma once -#include <ext/hash_set> +#include <unordered_set> #include <vector> #include "context/cdhashmap.h" @@ -43,7 +43,7 @@ private: CDNode2PairMap d_pbBounds; SubstitutionMap d_subCache; - typedef __gnu_cxx::hash_set<Node, NodeHashFunction> NodeSet; + typedef std::unordered_set<Node, NodeHashFunction> NodeSet; NodeSet d_learningCache; context::CDO<unsigned> d_pbs; diff --git a/src/theory/arith/simplex.h b/src/theory/arith/simplex.h index 13fba2c77..bd983e0bf 100644 --- a/src/theory/arith/simplex.h +++ b/src/theory/arith/simplex.h @@ -53,6 +53,8 @@ #pragma once +#include <unordered_map> + #include "theory/arith/arithvar.h" #include "theory/arith/delta_rational.h" #include "theory/arith/error_set.h" @@ -199,7 +201,7 @@ protected: } }; - typedef std::hash_map< std::pair<ArithVar, int>, ArithVarVec, ArithVarIntPairHashFunc> sgn_table; + typedef std::unordered_map< std::pair<ArithVar, int>, ArithVarVec, ArithVarIntPairHashFunc> sgn_table; static inline int determinizeSgn(int sgn){ return sgn < 0 ? -1 : (sgn == 0 ? 0 : 1); diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index 5fb31e93f..ab5a19858 100644 --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/theory_arith_private.cpp @@ -4268,7 +4268,7 @@ void TheoryArithPrivate::collectModelInfo( TheoryModel* m ){ // Delta lasts at least the duration of the function call const Rational& delta = d_partialModel.getDelta(); - std::hash_set<TNode, TNodeHashFunction> shared = d_containing.currentlySharedTerms(); + std::unordered_set<TNode, TNodeHashFunction> shared = d_containing.currentlySharedTerms(); // TODO: // This is not very good for user push/pop.... diff --git a/src/theory/arrays/array_info.h b/src/theory/arrays/array_info.h index cc5fddf25..5955fb4e4 100644 --- a/src/theory/arrays/array_info.h +++ b/src/theory/arrays/array_info.h @@ -18,10 +18,9 @@ #ifndef __CVC4__THEORY__ARRAYS__ARRAY_INFO_H #define __CVC4__THEORY__ARRAYS__ARRAY_INFO_H -#include <ext/hash_set> -#include <ext/hash_map> #include <iostream> #include <map> +#include <unordered_map> #include "context/backtrackable.h" #include "context/cdlist.h" @@ -92,7 +91,7 @@ public: };/* class Info */ -typedef __gnu_cxx::hash_map<Node, Info*, NodeHashFunction> CNodeInfoMap; +typedef std::unordered_map<Node, Info*, NodeHashFunction> CNodeInfoMap; /** * Class keeping track of the following information for canonical diff --git a/src/theory/arrays/static_fact_manager.h b/src/theory/arrays/static_fact_manager.h index 53d935813..4a08838fe 100644 --- a/src/theory/arrays/static_fact_manager.h +++ b/src/theory/arrays/static_fact_manager.h @@ -23,7 +23,7 @@ #include <utility> #include <vector> -#include <ext/hash_map> +#include <unordered_map> #include "expr/node.h" @@ -33,7 +33,7 @@ namespace arrays { class StaticFactManager { /** Our underlying map type. */ - typedef __gnu_cxx::hash_map<Node, Node, NodeHashFunction> MapType; + typedef std::unordered_map<Node, Node, NodeHashFunction> MapType; /** * Our map of Nodes to their canonical representatives. diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index bde88abab..2f5a9a14f 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -551,7 +551,7 @@ void TheoryArrays::weakEquivMakeRepIndex(TNode node) { } void TheoryArrays::weakEquivAddSecondary(TNode index, TNode arrayFrom, TNode arrayTo, TNode reason) { - std::hash_set<TNode, TNodeHashFunction> marked; + std::unordered_set<TNode, TNodeHashFunction> marked; vector<TNode> index_trail; vector<TNode>::iterator it, iend; Node equivalence_trail = reason; @@ -1198,7 +1198,7 @@ void TheoryArrays::collectModelInfo( TheoryModel* m ) /* } else { - std::hash_map<Node, Node, NodeHashFunction>::iterator it = d_skolemCache.find(n); + std::unordered_map<Node, Node, NodeHashFunction>::iterator it = d_skolemCache.find(n); if (it == d_skolemCache.end()) { rep = nm->mkSkolem("array_collect_model_var", n.getType(), "base model variable for array collectModelInfo"); d_skolemCache[n] = rep; @@ -1240,7 +1240,7 @@ void TheoryArrays::presolve() Node TheoryArrays::getSkolem(TNode ref, const string& name, const TypeNode& type, const string& comment, bool makeEqual) { Node skolem; - std::hash_map<Node, Node, NodeHashFunction>::iterator it = d_skolemCache.find(ref); + std::unordered_map<Node, Node, NodeHashFunction>::iterator it = d_skolemCache.find(ref); if (it == d_skolemCache.end()) { NodeManager* nm = NodeManager::currentNM(); skolem = nm->mkSkolem(name, type, comment); diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h index 7e8831733..3ef9578ef 100644 --- a/src/theory/arrays/theory_arrays.h +++ b/src/theory/arrays/theory_arrays.h @@ -19,6 +19,8 @@ #ifndef __CVC4__THEORY__ARRAYS__THEORY_ARRAYS_H #define __CVC4__THEORY__ARRAYS__THEORY_ARRAYS_H +#include <unordered_map> + #include "context/cdhashmap.h" #include "context/cdhashset.h" #include "context/cdqueue.h" @@ -384,7 +386,7 @@ class TheoryArrays : public Theory { // When a new read term is created, we check the index to see if we know the model value. If so, we add it to d_constReads (and d_constReadsList) // If not, we push it onto d_reads and figure out where it goes at computeCareGraph time. // d_constReadsList is used as a backup in case we can't compute the model at computeCareGraph time. - typedef std::hash_map<Node, CTNodeList*, NodeHashFunction> CNodeNListMap; + typedef std::unordered_map<Node, CTNodeList*, NodeHashFunction> CNodeNListMap; CNodeNListMap d_constReads; context::CDList<TNode> d_reads; context::CDList<TNode> d_constReadsList; @@ -408,7 +410,7 @@ class TheoryArrays : public Theory { };/* class ContextPopper */ ContextPopper d_contextPopper; - std::hash_map<Node, Node, NodeHashFunction> d_skolemCache; + std::unordered_map<Node, Node, NodeHashFunction> d_skolemCache; context::CDO<unsigned> d_skolemIndex; std::vector<Node> d_skolemAssertions; @@ -425,7 +427,7 @@ class TheoryArrays : public Theory { typedef context::CDHashMap<Node,Node,NodeHashFunction> DefValMap; DefValMap d_defValues; - typedef std::hash_map<std::pair<TNode, TNode>, CTNodeList*, TNodePairHashFunction> ReadBucketMap; + typedef std::unordered_map<std::pair<TNode, TNode>, CTNodeList*, TNodePairHashFunction> ReadBucketMap; ReadBucketMap d_readBucketTable; context::Context* d_readTableContext; context::CDList<Node> d_arrayMerges; diff --git a/src/theory/arrays/theory_arrays_rewriter.h b/src/theory/arrays/theory_arrays_rewriter.h index 4a05f3789..04d199971 100644 --- a/src/theory/arrays/theory_arrays_rewriter.h +++ b/src/theory/arrays/theory_arrays_rewriter.h @@ -20,6 +20,9 @@ #ifndef __CVC4__THEORY__ARRAYS__THEORY_ARRAYS_REWRITER_H #define __CVC4__THEORY__ARRAYS__THEORY_ARRAYS_REWRITER_H +#include <unordered_map> +#include <unordered_set> + #include "theory/rewriter.h" #include "theory/type_enumerator.h" @@ -150,9 +153,9 @@ public: // Bad case: have to recompute value counts and/or possibly switch out // default value store = n; - std::hash_set<TNode, TNodeHashFunction> indexSet; - std::hash_map<TNode, unsigned, TNodeHashFunction> elementsMap; - std::hash_map<TNode, unsigned, TNodeHashFunction>::iterator it; + std::unordered_set<TNode, TNodeHashFunction> indexSet; + std::unordered_map<TNode, unsigned, TNodeHashFunction> elementsMap; + std::unordered_map<TNode, unsigned, TNodeHashFunction>::iterator it; unsigned count; unsigned max = 0; TNode maxValue; diff --git a/src/theory/arrays/union_find.h b/src/theory/arrays/union_find.h index e896784ef..eb60f339b 100644 --- a/src/theory/arrays/union_find.h +++ b/src/theory/arrays/union_find.h @@ -23,7 +23,7 @@ #include <utility> #include <vector> -#include <ext/hash_map> +#include <unordered_map> #include "expr/node.h" #include "context/cdo.h" @@ -41,7 +41,7 @@ namespace arrays { template <class NodeType, class NodeHash> class UnionFind : context::ContextNotifyObj { /** Our underlying map type. */ - typedef __gnu_cxx::hash_map<NodeType, NodeType, NodeHash> MapType; + typedef std::unordered_map<NodeType, NodeType, NodeHash> MapType; /** * Our map of Nodes to their canonical representatives. diff --git a/src/theory/booleans/circuit_propagator.h b/src/theory/booleans/circuit_propagator.h index 03c811eee..78e01f690 100644 --- a/src/theory/booleans/circuit_propagator.h +++ b/src/theory/booleans/circuit_propagator.h @@ -19,8 +19,9 @@ #ifndef __CVC4__THEORY__BOOLEANS__CIRCUIT_PROPAGATOR_H #define __CVC4__THEORY__BOOLEANS__CIRCUIT_PROPAGATOR_H -#include <vector> #include <functional> +#include <unordered_map> +#include <vector> #include "theory/theory.h" #include "context/context.h" @@ -64,7 +65,7 @@ public: else return ASSIGNED_TO_TRUE; } - typedef std::hash_map<Node, std::vector<Node>, NodeHashFunction> BackEdgesMap; + typedef std::unordered_map<Node, std::vector<Node>, NodeHashFunction> BackEdgesMap; private: diff --git a/src/theory/booleans/theory_bool_rewriter.cpp b/src/theory/booleans/theory_bool_rewriter.cpp index b5f7e37d4..8373f636b 100644 --- a/src/theory/booleans/theory_bool_rewriter.cpp +++ b/src/theory/booleans/theory_bool_rewriter.cpp @@ -16,6 +16,8 @@ **/ #include <algorithm> +#include <unordered_set> + #include "theory/booleans/theory_bool_rewriter.h" namespace CVC4 { @@ -41,7 +43,7 @@ RewriteResponse TheoryBoolRewriter::postRewrite(TNode node) { */ RewriteResponse flattenNode(TNode n, TNode trivialNode, TNode skipNode) { - typedef std::hash_set<TNode, TNodeHashFunction> node_set; + typedef std::unordered_set<TNode, TNodeHashFunction> node_set; node_set visited; visited.insert(skipNode); diff --git a/src/theory/bv/abstraction.h b/src/theory/bv/abstraction.h index ed4b8aeb6..0d7e0ff2a 100644 --- a/src/theory/bv/abstraction.h +++ b/src/theory/bv/abstraction.h @@ -19,8 +19,8 @@ #ifndef __CVC4__THEORY__BV__ABSTRACTION_H #define __CVC4__THEORY__BV__ABSTRACTION_H -#include <ext/hash_map> -#include <ext/hash_set> +#include <unordered_map> +#include <unordered_set> #include "expr/node.h" #include "theory/substitutions.h" @@ -64,10 +64,10 @@ class AbstractionModule { }; class ArgsTable { - __gnu_cxx::hash_map<TNode, ArgsTableEntry, TNodeHashFunction > d_data; + std::unordered_map<TNode, ArgsTableEntry, TNodeHashFunction > d_data; bool hasEntry(TNode signature) const; public: - typedef __gnu_cxx::hash_map<TNode, ArgsTableEntry, TNodeHashFunction >::iterator iterator; + typedef std::unordered_map<TNode, ArgsTableEntry, TNodeHashFunction >::iterator iterator; ArgsTable() {} void addEntry(TNode signature, const ArgsVec& args); ArgsTableEntry& getEntry(TNode signature); @@ -122,16 +122,16 @@ class AbstractionModule { }; - typedef __gnu_cxx::hash_map<Node, std::vector<Node>, NodeHashFunction> NodeVecMap; - typedef __gnu_cxx::hash_map<Node, TNode, NodeHashFunction> NodeTNodeMap; - typedef __gnu_cxx::hash_map<TNode, TNode, TNodeHashFunction> TNodeTNodeMap; - typedef __gnu_cxx::hash_map<Node, Node, NodeHashFunction> NodeNodeMap; - typedef __gnu_cxx::hash_map<Node, TNode, NodeHashFunction> TNodeNodeMap; - typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> TNodeSet; - typedef __gnu_cxx::hash_map<unsigned, Node> IntNodeMap; - typedef __gnu_cxx::hash_map<unsigned, unsigned> IndexMap; - typedef __gnu_cxx::hash_map<unsigned, std::vector<Node> > SkolemMap; - typedef __gnu_cxx::hash_map<TNode, unsigned, TNodeHashFunction > SignatureMap; + typedef std::unordered_map<Node, std::vector<Node>, NodeHashFunction> NodeVecMap; + typedef std::unordered_map<Node, TNode, NodeHashFunction> NodeTNodeMap; + typedef std::unordered_map<TNode, TNode, TNodeHashFunction> TNodeTNodeMap; + typedef std::unordered_map<Node, Node, NodeHashFunction> NodeNodeMap; + typedef std::unordered_map<Node, TNode, NodeHashFunction> TNodeNodeMap; + typedef std::unordered_set<TNode, TNodeHashFunction> TNodeSet; + typedef std::unordered_map<unsigned, Node> IntNodeMap; + typedef std::unordered_map<unsigned, unsigned> IndexMap; + typedef std::unordered_map<unsigned, std::vector<Node> > SkolemMap; + typedef std::unordered_map<TNode, unsigned, TNodeHashFunction > SignatureMap; ArgsTable d_argsTable; diff --git a/src/theory/bv/bitblaster_template.h b/src/theory/bv/bitblaster_template.h index b6b2e2926..565c454e3 100644 --- a/src/theory/bv/bitblaster_template.h +++ b/src/theory/bv/bitblaster_template.h @@ -19,7 +19,8 @@ #ifndef __CVC4__BITBLASTER_TEMPLATE_H #define __CVC4__BITBLASTER_TEMPLATE_H -#include <ext/hash_map> +#include <unordered_map> +#include <unordered_set> #include <vector> #include "bitblast_strategies_template.h" @@ -58,8 +59,8 @@ namespace bv { class BitblastingRegistrar; -typedef __gnu_cxx::hash_set<Node, NodeHashFunction> NodeSet; -typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> TNodeSet; +typedef std::unordered_set<Node, NodeHashFunction> NodeSet; +typedef std::unordered_set<TNode, TNodeHashFunction> TNodeSet; class AbstractionModule; @@ -73,9 +74,9 @@ template <class T> class TBitblaster { protected: typedef std::vector<T> Bits; - typedef __gnu_cxx::hash_map <Node, Bits, NodeHashFunction> TermDefMap; - typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> TNodeSet; - typedef __gnu_cxx::hash_map<Node, Node, NodeHashFunction> ModelCache; + typedef std::unordered_map <Node, Bits, NodeHashFunction> TermDefMap; + typedef std::unordered_set<TNode, TNodeHashFunction> TNodeSet; + typedef std::unordered_map<Node, Node, NodeHashFunction> ModelCache; typedef void (*TermBBStrategy) (TNode, Bits&, TBitblaster<T>*); typedef T (*AtomBBStrategy) (TNode, TBitblaster<T>*); @@ -258,7 +259,7 @@ public: class EagerBitblaster : public TBitblaster<Node> { - typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> TNodeSet; + typedef std::unordered_set<TNode, TNodeHashFunction> TNodeSet; // sat solver used for bitblasting and associated CnfStream prop::SatSolver* d_satSolver; BitblastingRegistrar* d_bitblastingRegistrar; @@ -305,8 +306,8 @@ public: }; /* class Registrar */ class AigBitblaster : public TBitblaster<Abc_Obj_t*> { - typedef std::hash_map<TNode, Abc_Obj_t*, TNodeHashFunction > TNodeAigMap; - typedef std::hash_map<Node, Abc_Obj_t*, NodeHashFunction > NodeAigMap; + typedef std::unordered_map<TNode, Abc_Obj_t*, TNodeHashFunction > TNodeAigMap; + typedef std::unordered_map<Node, Abc_Obj_t*, NodeHashFunction > NodeAigMap; static Abc_Ntk_t* abcAigNetwork; context::Context* d_nullContext; diff --git a/src/theory/bv/bv_eager_solver.h b/src/theory/bv/bv_eager_solver.h index 380d06349..ec6cbad09 100644 --- a/src/theory/bv/bv_eager_solver.h +++ b/src/theory/bv/bv_eager_solver.h @@ -9,18 +9,21 @@ ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** - ** \brief Eager bit-blasting solver. + ** \brief Eager bit-blasting solver. ** ** Eager bit-blasting solver. **/ #include "cvc4_private.h" + +#pragma once + +#include <unordered_set> +#include <vector> + #include "expr/node.h" #include "theory/theory_model.h" #include "theory/bv/theory_bv.h" -#include <vector> -#pragma once - namespace CVC4 { namespace theory { @@ -33,7 +36,7 @@ class AigBitblaster; * BitblastSolver */ class EagerBitblastSolver { - typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> AssertionSet; + typedef std::unordered_set<TNode, TNodeHashFunction> AssertionSet; AssertionSet d_assertionSet; /** Bitblasters */ EagerBitblaster* d_bitblaster; diff --git a/src/theory/bv/bv_inequality_graph.h b/src/theory/bv/bv_inequality_graph.h index f85d8a835..30270b3c3 100644 --- a/src/theory/bv/bv_inequality_graph.h +++ b/src/theory/bv/bv_inequality_graph.h @@ -9,7 +9,7 @@ ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** - ** \brief Algebraic solver. + ** \brief Algebraic solver. ** ** Algebraic solver. **/ @@ -19,23 +19,25 @@ #ifndef __CVC4__THEORY__BV__BV_INEQUALITY__GRAPH_H #define __CVC4__THEORY__BV__BV_INEQUALITY__GRAPH_H -#include "context/context.h" +#include <list> +#include <queue> +#include <unordered_map> +#include <unordered_set> + #include "context/cdqueue.h" -#include "theory/uf/equality_engine.h" +#include "context/context.h" #include "theory/theory.h" -#include <queue> -#include <list> +#include "theory/uf/equality_engine.h" + namespace CVC4 { namespace theory { - - namespace bv { -typedef unsigned TermId; +typedef unsigned TermId; typedef unsigned ReasonId; extern const TermId UndefinedTermId; extern const ReasonId UndefinedReasonId; -extern const ReasonId AxiomReasonId; +extern const ReasonId AxiomReasonId; class InequalityGraph : public context::ContextNotifyObj{ @@ -100,15 +102,15 @@ class InequalityGraph : public context::ContextNotifyObj{ } }; - typedef __gnu_cxx::hash_map<TNode, ReasonId, TNodeHashFunction> ReasonToIdMap; - typedef __gnu_cxx::hash_map<TNode, TermId, TNodeHashFunction> TermNodeToIdMap; + typedef std::unordered_map<TNode, ReasonId, TNodeHashFunction> ReasonToIdMap; + typedef std::unordered_map<TNode, TermId, TNodeHashFunction> TermNodeToIdMap; typedef std::vector<InequalityEdge> Edges; - typedef __gnu_cxx::hash_set<TermId> TermIdSet; + typedef std::unordered_set<TermId> TermIdSet; typedef std::priority_queue<TermId, std::vector<TermId>, QueueComparator> BFSQueue; - typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> TNodeSet; - typedef __gnu_cxx::hash_set<Node, NodeHashFunction> NodeSet; + typedef std::unordered_set<TNode, TNodeHashFunction> TNodeSet; + typedef std::unordered_set<Node, NodeHashFunction> NodeSet; std::vector<InequalityNode> d_ineqNodes; std::vector< Edges > d_ineqEdges; diff --git a/src/theory/bv/bv_quick_check.h b/src/theory/bv/bv_quick_check.h index dcd3f1062..c5fe63ad6 100644 --- a/src/theory/bv/bv_quick_check.h +++ b/src/theory/bv/bv_quick_check.h @@ -20,7 +20,7 @@ #define __CVC4__BV_QUICK_CHECK_H #include <vector> -#include <ext/hash_map> +#include <unordered_set> #include "context/cdo.h" #include "expr/node.h" @@ -99,7 +99,7 @@ public: uint64_t computeAtomWeight(TNode atom, NodeSet& seen); void collectModelInfo(theory::TheoryModel* model, bool fullModel); - typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction>::const_iterator vars_iterator; + typedef std::unordered_set<TNode, TNodeHashFunction>::const_iterator vars_iterator; vars_iterator beginVars(); vars_iterator endVars(); diff --git a/src/theory/bv/bv_subtheory_algebraic.h b/src/theory/bv/bv_subtheory_algebraic.h index 3730ebc90..4b4103e44 100644 --- a/src/theory/bv/bv_subtheory_algebraic.h +++ b/src/theory/bv/bv_subtheory_algebraic.h @@ -14,12 +14,16 @@ ** Algebraic solver. **/ +#include "cvc4_private.h" + #pragma once -#include "cvc4_private.h" +#include <unordered_map> +#include <unordered_set> + #include "theory/bv/bv_subtheory.h" -#include "theory/substitutions.h" #include "theory/bv/slicer.h" +#include "theory/substitutions.h" namespace CVC4 { namespace theory { @@ -60,8 +64,8 @@ class SubstitutionEx { {} }; - typedef __gnu_cxx::hash_map<Node, SubstitutionElement, NodeHashFunction> Substitutions; - typedef __gnu_cxx::hash_map<Node, SubstitutionElement, NodeHashFunction> SubstitutionsCache; + typedef std::unordered_map<Node, SubstitutionElement, NodeHashFunction> Substitutions; + typedef std::unordered_map<Node, SubstitutionElement, NodeHashFunction> SubstitutionsCache; Substitutions d_substitutions; SubstitutionsCache d_cache; @@ -104,9 +108,9 @@ struct WorklistElement { }; -typedef __gnu_cxx::hash_map<Node, Node, NodeHashFunction> NodeNodeMap; -typedef __gnu_cxx::hash_map<Node, unsigned, NodeHashFunction> NodeIdMap; -typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> TNodeSet; +typedef std::unordered_map<Node, Node, NodeHashFunction> NodeNodeMap; +typedef std::unordered_map<Node, unsigned, NodeHashFunction> NodeIdMap; +typedef std::unordered_set<TNode, TNodeHashFunction> TNodeSet; class ExtractSkolemizer { @@ -123,7 +127,7 @@ class ExtractSkolemizer { ExtractList() : base(1), extracts() {} void addExtract(Extract& e); }; - typedef __gnu_cxx::hash_map<Node, ExtractList, NodeHashFunction> VarExtractMap; + typedef std::unordered_map<Node, ExtractList, NodeHashFunction> VarExtractMap; context::Context d_emptyContext; VarExtractMap d_varToExtract; theory::SubstitutionMap* d_modelMap; diff --git a/src/theory/bv/bv_subtheory_bitblast.h b/src/theory/bv/bv_subtheory_bitblast.h index c9fb81195..4bbe4327e 100644 --- a/src/theory/bv/bv_subtheory_bitblast.h +++ b/src/theory/bv/bv_subtheory_bitblast.h @@ -18,6 +18,8 @@ #pragma once +#include <unordered_map> + #include "theory/bv/bitblaster_template.h" #include "theory/bv/bv_subtheory.h" @@ -47,7 +49,7 @@ class BitblastSolver : public SubtheorySolver { context::CDQueue<TNode> d_bitblastQueue; Statistics d_statistics; - typedef std::hash_map<Node, Node, NodeHashFunction> NodeMap; + typedef std::unordered_map<Node, Node, NodeHashFunction> NodeMap; NodeMap d_modelCache; context::CDO<bool> d_validModelCache; diff --git a/src/theory/bv/bv_subtheory_core.h b/src/theory/bv/bv_subtheory_core.h index 662f8835e..b416e019d 100644 --- a/src/theory/bv/bv_subtheory_core.h +++ b/src/theory/bv/bv_subtheory_core.h @@ -14,12 +14,16 @@ ** Algebraic solver. **/ +#include "cvc4_private.h" + #pragma once -#include "cvc4_private.h" -#include "theory/bv/bv_subtheory.h" +#include <unordered_map> +#include <unordered_set> + #include "context/cdhashmap.h" #include "context/cdhashset.h" +#include "theory/bv/bv_subtheory.h" namespace CVC4 { namespace theory { @@ -31,9 +35,9 @@ class Base; * Bitvector equality solver */ class CoreSolver : public SubtheorySolver { - typedef __gnu_cxx::hash_map<TNode, Node, TNodeHashFunction> ModelValue; - typedef __gnu_cxx::hash_map<TNode, bool, TNodeHashFunction> TNodeBoolMap; - typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> TNodeSet; + typedef std::unordered_map<TNode, Node, TNodeHashFunction> ModelValue; + typedef std::unordered_map<TNode, bool, TNodeHashFunction> TNodeBoolMap; + typedef std::unordered_set<TNode, TNodeHashFunction> TNodeSet; struct Statistics { diff --git a/src/theory/bv/bv_subtheory_inequality.h b/src/theory/bv/bv_subtheory_inequality.h index 37d3723ac..1123d15ae 100644 --- a/src/theory/bv/bv_subtheory_inequality.h +++ b/src/theory/bv/bv_subtheory_inequality.h @@ -19,10 +19,12 @@ #ifndef __CVC4__THEORY__BV__BV_SUBTHEORY__INEQUALITY_H #define __CVC4__THEORY__BV__BV_SUBTHEORY__INEQUALITY_H -#include "theory/bv/bv_subtheory.h" -#include "theory/bv/bv_inequality_graph.h" +#include <unordered_set> + #include "context/cdhashset.h" #include "expr/attribute.h" +#include "theory/bv/bv_inequality_graph.h" +#include "theory/bv/bv_subtheory.h" namespace CVC4 { namespace theory { @@ -47,7 +49,7 @@ class InequalitySolver: public SubtheorySolver { InequalityGraph d_inequalityGraph; context::CDHashMap<Node, TNode, NodeHashFunction> d_explanations; context::CDO<bool> d_isComplete; - typedef __gnu_cxx::hash_set<Node, NodeHashFunction> NodeSet; + typedef std::unordered_set<Node, NodeHashFunction> NodeSet; NodeSet d_ineqTerms; bool isInequalityOnly(TNode node); bool addInequality(TNode a, TNode b, bool strict, TNode fact); diff --git a/src/theory/bv/bv_to_bool.h b/src/theory/bv/bv_to_bool.h index a934cf045..93a83626e 100644 --- a/src/theory/bv/bv_to_bool.h +++ b/src/theory/bv/bv_to_bool.h @@ -19,6 +19,8 @@ #ifndef __CVC4__THEORY__BV__BV_TO_BOOL_H #define __CVC4__THEORY__BV__BV_TO_BOOL_H +#include <unordered_map> + #include "theory/bv/theory_bv_utils.h" #include "util/statistics_registry.h" @@ -26,7 +28,7 @@ namespace CVC4 { namespace theory { namespace bv { -typedef __gnu_cxx::hash_map<Node, Node, NodeHashFunction> NodeNodeMap; +typedef std::unordered_map<Node, Node, NodeHashFunction> NodeNodeMap; class BvToBoolPreprocessor { diff --git a/src/theory/bv/bvintropow2.h b/src/theory/bv/bvintropow2.h index 935cbb7ed..e335c1339 100644 --- a/src/theory/bv/bvintropow2.h +++ b/src/theory/bv/bvintropow2.h @@ -21,7 +21,7 @@ #include "expr/node.h" #include <vector> -#include <ext/hash_map> +#include <unordered_map> #ifndef __CVC4__THEORY__BV__BV_INTRO_POW_H #define __CVC4__THEORY__BV__BV_INTRO_POW_H @@ -36,7 +36,7 @@ public: static void pow2Rewrite(std::vector<Node>& assertionsToPreprocess); private: - typedef __gnu_cxx::hash_map<Node, Node, NodeHashFunction> NodeMap; + typedef std::unordered_map<Node, Node, NodeHashFunction> NodeMap; static Node pow2Rewrite(Node assertionsToPreprocess, NodeMap& cache); }; diff --git a/src/theory/bv/slicer.h b/src/theory/bv/slicer.h index b594d5fec..dc8d333c4 100644 --- a/src/theory/bv/slicer.h +++ b/src/theory/bv/slicer.h @@ -20,7 +20,7 @@ #include <vector> #include <list> -#include <ext/hash_map> +#include <unordered_map> #include "expr/node.h" #include "theory/bv/theory_bv_utils.h" @@ -79,7 +79,7 @@ public: * UnionFind * */ -typedef __gnu_cxx::hash_set<TermId> TermSet; +typedef std::unordered_set<TermId> TermSet; typedef std::vector<TermId> Decomposition; struct ExtractTerm { @@ -226,9 +226,9 @@ public: }; class Slicer { - __gnu_cxx::hash_map<TermId, TNode> d_idToNode; - __gnu_cxx::hash_map<TNode, TermId, TNodeHashFunction> d_nodeToId; - __gnu_cxx::hash_map<TNode, bool, TNodeHashFunction> d_coreTermCache; + std::unordered_map<TermId, TNode> d_idToNode; + std::unordered_map<TNode, TermId, TNodeHashFunction> d_nodeToId; + std::unordered_map<TNode, bool, TNodeHashFunction> d_coreTermCache; UnionFind d_unionFind; ExtractTerm registerTerm(TNode node); public: diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h index f8d3e6509..c20df35d5 100644 --- a/src/theory/bv/theory_bv.h +++ b/src/theory/bv/theory_bv.h @@ -19,6 +19,9 @@ #ifndef __CVC4__THEORY__BV__THEORY_BV_H #define __CVC4__THEORY__BV__THEORY_BV_H +#include <unordered_map> +#include <unordered_set> + #include "context/cdhashset.h" #include "context/cdlist.h" #include "context/context.h" @@ -51,7 +54,7 @@ class TheoryBV : public Theory { context::CDHashSet<Node, NodeHashFunction> d_sharedTermsSet; std::vector<SubtheorySolver*> d_subtheories; - __gnu_cxx::hash_map<SubTheory, SubtheorySolver*, std::hash<int> > d_subtheoryMap; + std::unordered_map<SubTheory, SubtheorySolver*, std::hash<int> > d_subtheoryMap; public: @@ -129,22 +132,22 @@ private: */ Node getBVDivByZero(Kind k, unsigned width); - typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> TNodeSet; + typedef std::unordered_set<TNode, TNodeHashFunction> TNodeSet; void collectFunctionSymbols(TNode term, TNodeSet& seen); void storeFunction(TNode func, TNode term); - typedef __gnu_cxx::hash_set<Node, NodeHashFunction> NodeSet; + typedef std::unordered_set<Node, NodeHashFunction> NodeSet; NodeSet d_staticLearnCache; /** * Maps from bit-vector width to division-by-zero uninterpreted * function symbols. */ - __gnu_cxx::hash_map<unsigned, Node> d_BVDivByZero; - __gnu_cxx::hash_map<unsigned, Node> d_BVRemByZero; + std::unordered_map<unsigned, Node> d_BVDivByZero; + std::unordered_map<unsigned, Node> d_BVRemByZero; - typedef __gnu_cxx::hash_map<Node, NodeSet, NodeHashFunction> FunctionToArgs; - typedef __gnu_cxx::hash_map<Node, Node, NodeHashFunction> NodeToNode; + typedef std::unordered_map<Node, NodeSet, NodeHashFunction> FunctionToArgs; + typedef std::unordered_map<Node, Node, NodeHashFunction> NodeToNode; // for ackermanization FunctionToArgs d_funcToArgs; CVC4::theory::SubstitutionMap d_funcToSkolem; diff --git a/src/theory/bv/theory_bv_rewrite_rules_normalization.h b/src/theory/bv/theory_bv_rewrite_rules_normalization.h index 46297cb68..61f072643 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_normalization.h +++ b/src/theory/bv/theory_bv_rewrite_rules_normalization.h @@ -19,6 +19,9 @@ #pragma once +#include <unordered_map> +#include <unordered_set> + #include "theory/rewriter.h" #include "theory/bv/theory_bv_rewrite_rules.h" #include "theory/bv/theory_bv_utils.h" @@ -922,7 +925,7 @@ struct Count { {} }; -inline static void insert(std::hash_map<TNode, Count, TNodeHashFunction>& map, TNode node, bool neg) { +inline static void insert(std::unordered_map<TNode, Count, TNodeHashFunction>& map, TNode node, bool neg) { if(map.find(node) == map.end()) { Count c = neg? Count(0,1) : Count(1, 0); map[node] = c; @@ -945,7 +948,7 @@ Node RewriteRule<AndSimplify>::apply(TNode node) { Debug("bv-rewrite") << "RewriteRule<AndSimplify>(" << node << ")" << std::endl; // this will remove duplicates - std::hash_map<TNode, Count, TNodeHashFunction> subterms; + std::unordered_map<TNode, Count, TNodeHashFunction> subterms; unsigned size = utils::getSize(node); BitVector constant = utils::mkBitVectorOnes(size); @@ -974,7 +977,7 @@ Node RewriteRule<AndSimplify>::apply(TNode node) { children.push_back(utils::mkConst(constant)); } - std::hash_map<TNode, Count, TNodeHashFunction>::const_iterator it = subterms.begin(); + std::unordered_map<TNode, Count, TNodeHashFunction>::const_iterator it = subterms.begin(); for (; it != subterms.end(); ++it) { if (it->second.pos > 0 && it->second.neg > 0) { @@ -1018,7 +1021,7 @@ Node RewriteRule<FlattenAssocCommutNoDuplicates>::apply(TNode node) { Debug("bv-rewrite") << "RewriteRule<FlattenAssocCommut>(" << node << ")" << std::endl; std::vector<Node> processingStack; processingStack.push_back(node); - __gnu_cxx::hash_set<TNode, TNodeHashFunction> processed; + std::unordered_set<TNode, TNodeHashFunction> processed; std::vector<Node> children; Kind kind = node.getKind(); @@ -1053,7 +1056,7 @@ Node RewriteRule<OrSimplify>::apply(TNode node) { Debug("bv-rewrite") << "RewriteRule<OrSimplify>(" << node << ")" << std::endl; // this will remove duplicates - std::hash_map<TNode, Count, TNodeHashFunction> subterms; + std::unordered_map<TNode, Count, TNodeHashFunction> subterms; unsigned size = utils::getSize(node); BitVector constant(size, (unsigned)0); @@ -1082,7 +1085,7 @@ Node RewriteRule<OrSimplify>::apply(TNode node) { children.push_back(utils::mkConst(constant)); } - std::hash_map<TNode, Count, TNodeHashFunction>::const_iterator it = subterms.begin(); + std::unordered_map<TNode, Count, TNodeHashFunction>::const_iterator it = subterms.begin(); for (; it != subterms.end(); ++it) { if (it->second.pos > 0 && it->second.neg > 0) { @@ -1116,7 +1119,7 @@ Node RewriteRule<XorSimplify>::apply(TNode node) { Debug("bv-rewrite") << "RewriteRule<XorSimplify>(" << node << ")" << std::endl; - std::hash_map<TNode, Count, TNodeHashFunction> subterms; + std::unordered_map<TNode, Count, TNodeHashFunction> subterms; unsigned size = utils::getSize(node); BitVector constant; bool const_set = false; @@ -1144,7 +1147,7 @@ Node RewriteRule<XorSimplify>::apply(TNode node) { std::vector<Node> children; - std::hash_map<TNode, Count, TNodeHashFunction>::const_iterator it = subterms.begin(); + std::unordered_map<TNode, Count, TNodeHashFunction>::const_iterator it = subterms.begin(); unsigned true_count = 0; bool seen_false = false; for (; it != subterms.end(); ++it) { diff --git a/src/theory/bv/theory_bv_utils.h b/src/theory/bv/theory_bv_utils.h index 5bae1af4f..8b8d5e003 100644 --- a/src/theory/bv/theory_bv_utils.h +++ b/src/theory/bv/theory_bv_utils.h @@ -17,19 +17,22 @@ #include "cvc4_private.h" -#pragma once +#pragma once #include <set> -#include <vector> #include <sstream> +#include <unordered_map> +#include <unordered_set> +#include <vector> + #include "expr/node_manager.h" namespace CVC4 { namespace theory { namespace bv { -typedef __gnu_cxx::hash_set<Node, NodeHashFunction> NodeSet; -typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> TNodeSet; +typedef std::unordered_set<Node, NodeHashFunction> NodeSet; +typedef std::unordered_set<TNode, TNodeHashFunction> TNodeSet; namespace utils { @@ -505,11 +508,11 @@ inline T gcd(T a, T b) { return a; } -typedef __gnu_cxx::hash_map<TNode, bool, TNodeHashFunction> TNodeBoolMap; +typedef std::unordered_map<TNode, bool, TNodeHashFunction> TNodeBoolMap; bool isCoreTerm(TNode term, TNodeBoolMap& cache); bool isEqualityTerm(TNode term, TNodeBoolMap& cache); -typedef __gnu_cxx::hash_set<Node, NodeHashFunction> NodeSet; +typedef std::unordered_set<Node, NodeHashFunction> NodeSet; uint64_t numNodes(TNode node, NodeSet& seen); diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h index fd79e3fdc..a0333ed8b 100644 --- a/src/theory/datatypes/theory_datatypes.h +++ b/src/theory/datatypes/theory_datatypes.h @@ -19,7 +19,6 @@ #ifndef __CVC4__THEORY__DATATYPES__THEORY_DATATYPES_H #define __CVC4__THEORY__DATATYPES__THEORY_DATATYPES_H -#include <ext/hash_set> #include <iostream> #include <map> diff --git a/src/theory/ite_utilities.cpp b/src/theory/ite_utilities.cpp index e32fa1e71..6d81dbab0 100644 --- a/src/theory/ite_utilities.cpp +++ b/src/theory/ite_utilities.cpp @@ -1092,7 +1092,7 @@ bool ITESimplifier::leavesAreConst(TNode e, TheoryId tid) return true; } - hash_map<Node, bool, NodeHashFunction>::iterator it; + unordered_map<Node, bool, NodeHashFunction>::iterator it; it = d_leavesConstCache.find(e); if (it != d_leavesConstCache.end()) { return (*it).second; @@ -1173,7 +1173,7 @@ Node ITESimplifier::simpConstants(TNode simpContext, TNode iteNode, TNode simpVa Node ITESimplifier::getSimpVar(TypeNode t) { - std::hash_map<TypeNode, Node, TypeNode::HashFunction>::iterator it; + std::unordered_map<TypeNode, Node, TypeNode::HashFunction>::iterator it; it = d_simpVars.find(t); if (it != d_simpVars.end()) { return (*it).second; @@ -1231,7 +1231,7 @@ Node ITESimplifier::createSimpContext(TNode c, Node& iteNode, Node& simpVar) d_simpContextCache[c] = result; return result; } -typedef std::hash_set<Node, NodeHashFunction> NodeSet; +typedef std::unordered_set<Node, NodeHashFunction> NodeSet; void countReachable_(Node x, Kind k, NodeSet& visited, uint32_t& reached){ if(visited.find(x) != visited.end()){ return; diff --git a/src/theory/ite_utilities.h b/src/theory/ite_utilities.h index 29f4f7f1f..4aad9a3f0 100644 --- a/src/theory/ite_utilities.h +++ b/src/theory/ite_utilities.h @@ -22,8 +22,7 @@ #ifndef __CVC4__ITE_UTILITIES_H #define __CVC4__ITE_UTILITIES_H -#include <ext/hash_map> -#include <ext/hash_set> +#include <unordered_map> #include <vector> #include "expr/node.h" @@ -80,7 +79,7 @@ public: size_t cache_size() const { return d_cache.size(); } private: - typedef std::hash_map<Node, bool, NodeHashFunction> NodeBoolMap; + typedef std::unordered_map<Node, bool, NodeHashFunction> NodeBoolMap; NodeBoolMap d_cache; }; @@ -100,7 +99,7 @@ public: } void clear(); private: - typedef std::hash_map<Node, uint32_t, NodeHashFunction> NodeCountMap; + typedef std::unordered_map<Node, uint32_t, NodeHashFunction> NodeCountMap; NodeCountMap d_reachCount; bool d_skipVariables; @@ -131,7 +130,7 @@ public: size_t cache_size() const; private: - typedef std::hash_map<Node, uint32_t, NodeHashFunction> NodeCountMap; + typedef std::unordered_map<Node, uint32_t, NodeHashFunction> NodeCountMap; NodeCountMap d_termITEHeight; }; /* class TermITEHeightCounter */ @@ -158,7 +157,7 @@ private: std::vector<Node>* d_assertions; IncomingArcCounter d_incoming; - typedef std::hash_map<Node, Node, NodeHashFunction> NodeMap; + typedef std::unordered_map<Node, Node, NodeHashFunction> NodeMap; NodeMap d_compressed; void reset(); @@ -206,7 +205,7 @@ private: // constant // or termITE(cnd, ConstantIte, ConstantIte) typedef std::vector<Node> NodeVec; - typedef std::hash_map<Node, NodeVec*, NodeHashFunction > ConstantLeavesMap; + typedef std::unordered_map<Node, NodeVec*, NodeHashFunction > ConstantLeavesMap; ConstantLeavesMap d_constantLeaves; // d_constantLeaves satisfies the following invariants: @@ -249,23 +248,23 @@ private: return hash; } };/* struct ITESimplifier::NodePairHashFunction */ - typedef std::hash_map<NodePair, Node, NodePairHashFunction> NodePairMap; + typedef std::unordered_map<NodePair, Node, NodePairHashFunction> NodePairMap; NodePairMap d_constantIteEqualsConstantCache; NodePairMap d_replaceOverCache; NodePairMap d_replaceOverTermIteCache; Node replaceOver(Node n, Node replaceWith, Node simpVar); Node replaceOverTermIte(Node term, Node simpAtom, Node simpVar); - std::hash_map<Node, bool, NodeHashFunction> d_leavesConstCache; + std::unordered_map<Node, bool, NodeHashFunction> d_leavesConstCache; bool leavesAreConst(TNode e, theory::TheoryId tid); bool leavesAreConst(TNode e); NodePairMap d_simpConstCache; Node simpConstants(TNode simpContext, TNode iteNode, TNode simpVar); - std::hash_map<TypeNode, Node, TypeNode::HashFunction> d_simpVars; + std::unordered_map<TypeNode, Node, TypeNode::HashFunction> d_simpVars; Node getSimpVar(TypeNode t); - typedef std::hash_map<Node, Node, NodeHashFunction> NodeMap; + typedef std::unordered_map<Node, Node, NodeHashFunction> NodeMap; NodeMap d_simpContextCache; Node createSimpContext(TNode c, Node& iteNode, Node& simpVar); @@ -314,7 +313,7 @@ private: Node d_true; Node d_false; - typedef std::hash_map<TNode, Node, TNodeHashFunction> TNodeMap; + typedef std::unordered_map<TNode, Node, TNodeHashFunction> TNodeMap; class CareSetPtr; class CareSetPtrVal { diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp index a635568fe..cb8e6f200 100644 --- a/src/theory/quantifiers/ce_guided_instantiation.cpp +++ b/src/theory/quantifiers/ce_guided_instantiation.cpp @@ -924,7 +924,9 @@ void CegInstantiation::printSynthSolution( std::ostream& out ) { if( d_last_inst_si ){ Assert( d_conj->getCegConjectureSingleInv() != NULL ); sol = d_conj->getSingleInvocationSolution( i, tn, status ); - sol = sol.getKind()==LAMBDA ? sol[1] : sol; + if( !sol.isNull() ){ + sol = sol.getKind()==LAMBDA ? sol[1] : sol; + } }else{ Node cprog = d_conj->getCandidate( i ); if( !d_conj->d_cinfo[cprog].d_inst.empty() ){ diff --git a/src/theory/quantifiers/ce_guided_single_inv.cpp b/src/theory/quantifiers/ce_guided_single_inv.cpp index a8dcd5887..f25d42284 100644 --- a/src/theory/quantifiers/ce_guided_single_inv.cpp +++ b/src/theory/quantifiers/ce_guided_single_inv.cpp @@ -888,6 +888,8 @@ Node CegConjectureSingleInv::reconstructToSyntax( Node s, TypeNode stn, int& rec Node sol; if( reconstructed==1 ){ sol = d_sygus_solution; + }else if( reconstructed==-1 ){ + return Node::null(); }else{ sol = d_solution; } diff --git a/src/theory/quantifiers/ce_guided_single_inv_sol.cpp b/src/theory/quantifiers/ce_guided_single_inv_sol.cpp index 9e65be202..1eafe1a93 100644 --- a/src/theory/quantifiers/ce_guided_single_inv_sol.cpp +++ b/src/theory/quantifiers/ce_guided_single_inv_sol.cpp @@ -714,8 +714,10 @@ Node CegConjectureSingleInvSol::reconstructSolution( Node sol, TypeNode stn, int } }while( !active.empty() ); - //if solution is null, we ran out of elements, return the original solution - return sol; + // we ran out of elements, return null + reconstructed = -1; + Warning() << CommandFailure("Cannot get synth function: reconstruction to syntax failed."); + return Node::null(); // return sol; } } diff --git a/src/theory/quantifiers/equality_infer.h b/src/theory/quantifiers/equality_infer.h index 4c1c93c17..5b714c2d3 100644 --- a/src/theory/quantifiers/equality_infer.h +++ b/src/theory/quantifiers/equality_infer.h @@ -17,7 +17,6 @@ #ifndef __CVC4__THEORY__QUANTIFIERS__EQUALITY_INFER_H #define __CVC4__THEORY__QUANTIFIERS__EQUALITY_INFER_H -#include <ext/hash_set> #include <iostream> #include <map> #include <vector> diff --git a/src/theory/quantifiers/inst_match.h b/src/theory/quantifiers/inst_match.h index 8d41c75d8..8597755c9 100644 --- a/src/theory/quantifiers/inst_match.h +++ b/src/theory/quantifiers/inst_match.h @@ -17,13 +17,10 @@ #ifndef __CVC4__THEORY__QUANTIFIERS__INST_MATCH_H #define __CVC4__THEORY__QUANTIFIERS__INST_MATCH_H -#include "util/hash.h" -#include "context/cdo.h" - -#include <ext/hash_set> #include <map> #include "context/cdlist.h" +#include "context/cdo.h" #include "expr/node.h" namespace CVC4 { diff --git a/src/theory/quantifiers/quant_util.h b/src/theory/quantifiers/quant_util.h index 40a5b5849..f46b73b1c 100644 --- a/src/theory/quantifiers/quant_util.h +++ b/src/theory/quantifiers/quant_util.h @@ -17,13 +17,12 @@ #ifndef __CVC4__THEORY__QUANT_UTIL_H #define __CVC4__THEORY__QUANT_UTIL_H -#include "theory/theory.h" -#include "theory/uf/equality_engine.h" - -#include <ext/hash_set> #include <iostream> #include <map> +#include "theory/theory.h" +#include "theory/uf/equality_engine.h" + namespace CVC4 { namespace theory { diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 93390facb..ec5fc633d 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -720,7 +720,7 @@ bool TermDb::reset( Theory::Effort effort ){ } } //explicitly add inst closure terms to the equality engine to ensure only EE terms are indexed - for( std::hash_set< Node, NodeHashFunction >::iterator it = d_iclosure_processed.begin(); it !=d_iclosure_processed.end(); ++it ){ + for( std::unordered_set< Node, NodeHashFunction >::iterator it = d_iclosure_processed.begin(); it !=d_iclosure_processed.end(); ++it ){ Node n = *it; if( !ee->hasTerm( n ) ){ ee->addTerm( n ); @@ -2288,4 +2288,3 @@ Node TermDb::getQAttrQuantIdNumNode( Node q ) { }/* CVC4::theory::quantifiers namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ - diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index f187e5989..4650cc5d4 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -17,12 +17,14 @@ #ifndef __CVC4__THEORY__QUANTIFIERS__TERM_DATABASE_H #define __CVC4__THEORY__QUANTIFIERS__TERM_DATABASE_H +#include <map> +#include <unordered_set> + #include "expr/attribute.h" #include "theory/theory.h" #include "theory/type_enumerator.h" #include "theory/quantifiers/quant_util.h" -#include <map> namespace CVC4 { namespace theory { @@ -194,9 +196,9 @@ private: /** reference to the quantifiers engine */ QuantifiersEngine* d_quantEngine; /** terms processed */ - std::hash_set< Node, NodeHashFunction > d_processed; + std::unordered_set< Node, NodeHashFunction > d_processed; /** terms processed */ - std::hash_set< Node, NodeHashFunction > d_iclosure_processed; + std::unordered_set< Node, NodeHashFunction > d_iclosure_processed; /** select op map */ std::map< Node, std::map< TypeNode, Node > > d_par_op_map; /** whether master equality engine is UF-inconsistent */ diff --git a/src/theory/quantifiers/theory_quantifiers.h b/src/theory/quantifiers/theory_quantifiers.h index d1412500e..9c621dbd6 100644 --- a/src/theory/quantifiers/theory_quantifiers.h +++ b/src/theory/quantifiers/theory_quantifiers.h @@ -19,25 +19,19 @@ #ifndef __CVC4__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_H #define __CVC4__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_H -#include <ext/hash_set> -#include <iostream> -#include <map> - #include "context/cdhashmap.h" +#include "context/context.h" +#include "expr/node.h" +#include "theory/output_channel.h" #include "theory/theory.h" -#include "util/hash.h" +#include "theory/theory_engine.h" +#include "theory/valuation.h" #include "util/statistics_registry.h" namespace CVC4 { -class TheoryEngine; - namespace theory { - namespace quantifiers { -class ModelEngine; -class InstantiationEngine; - class TheoryQuantifiers : public Theory { private: typedef context::CDHashMap< Node, bool, NodeHashFunction > BoolMap; diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index faf14e0c7..fa1394f39 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -1882,7 +1882,7 @@ Node EqualityQueryQuantifiersEngine::getInternalRepresentative( Node a, Node f, r_best = r; } //now, make sure that no other member of the class is an instance - std::hash_map<TNode, Node, TNodeHashFunction> cache; + std::unordered_map<TNode, Node, TNodeHashFunction> cache; r_best = getInstance( r_best, eqc, cache ); //store that this representative was chosen at this point if( d_rep_score.find( r_best )==d_rep_score.end() ){ @@ -2001,7 +2001,7 @@ TNode EqualityQueryQuantifiersEngine::getCongruentTerm( Node f, std::vector< TNo //helper functions -Node EqualityQueryQuantifiersEngine::getInstance( Node n, const std::vector< Node >& eqc, std::hash_map<TNode, Node, TNodeHashFunction>& cache ){ +Node EqualityQueryQuantifiersEngine::getInstance( Node n, const std::vector< Node >& eqc, std::unordered_map<TNode, Node, TNodeHashFunction>& cache ){ if(cache.find(n) != cache.end()) { return cache[n]; } diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index 92dfcdae5..7d8f5354b 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -17,9 +17,9 @@ #ifndef __CVC4__THEORY__QUANTIFIERS_ENGINE_H #define __CVC4__THEORY__QUANTIFIERS_ENGINE_H -#include <ext/hash_set> #include <iostream> #include <map> +#include <unordered_map> #include "context/cdchunk_list.h" #include "context/cdhashset.h" @@ -449,7 +449,7 @@ private: /** processInferences : will merge equivalence classes in master equality engine, if possible */ bool processInferences( Theory::Effort e ); /** node contains */ - Node getInstance( Node n, const std::vector< Node >& eqc, std::hash_map<TNode, Node, TNodeHashFunction>& cache ); + Node getInstance( Node n, const std::vector< Node >& eqc, std::unordered_map<TNode, Node, TNodeHashFunction>& cache ); /** get score */ int getRepScore( Node n, Node f, int index, TypeNode v_tn ); /** flatten representatives */ diff --git a/src/theory/rewriter.cpp b/src/theory/rewriter.cpp index 27ab7615c..0c20c48a4 100644 --- a/src/theory/rewriter.cpp +++ b/src/theory/rewriter.cpp @@ -35,7 +35,7 @@ static TheoryId theoryOf(TNode node) { } #ifdef CVC4_ASSERTIONS -static CVC4_THREADLOCAL(std::hash_set<Node, NodeHashFunction>*) s_rewriteStack = NULL; +static CVC4_THREADLOCAL(std::unordered_set<Node, NodeHashFunction>*) s_rewriteStack = NULL; #endif /* CVC4_ASSERTIONS */ class RewriterInitializer { @@ -94,7 +94,7 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node node) { bool isEquality = node.getKind() == kind::EQUAL && (!node[0].getType().isBoolean()); if(s_rewriteStack == NULL) { - s_rewriteStack = new std::hash_set<Node, NodeHashFunction>(); + s_rewriteStack = new std::unordered_set<Node, NodeHashFunction>(); } #endif diff --git a/src/theory/sets/theory_sets_rels.cpp b/src/theory/sets/theory_sets_rels.cpp index 34c17a34c..beb5e946c 100644 --- a/src/theory/sets/theory_sets_rels.cpp +++ b/src/theory/sets/theory_sets_rels.cpp @@ -27,9 +27,9 @@ namespace sets { typedef std::map< Node, std::vector< Node > >::iterator MEM_IT; typedef std::map< kind::Kind_t, std::vector< Node > >::iterator KIND_TERM_IT; -typedef std::map< Node, std::hash_set< Node, NodeHashFunction > >::iterator TC_GRAPH_IT; +typedef std::map< Node, std::unordered_set< Node, NodeHashFunction > >::iterator TC_GRAPH_IT; typedef std::map< Node, std::map< kind::Kind_t, std::vector< Node > > >::iterator TERM_IT; -typedef std::map< Node, std::map< Node, std::hash_set< Node, NodeHashFunction > > >::iterator TC_IT; +typedef std::map< Node, std::map< Node, std::unordered_set< Node, NodeHashFunction > > >::iterator TC_IT; void TheorySetsRels::check(Theory::Effort level) { Trace("rels") << "\n[sets-rels] ******************************* Start the relational solver, effort = " << level << " *******************************\n" << std::endl; @@ -240,7 +240,7 @@ typedef std::map< Node, std::map< Node, std::hash_set< Node, NodeHashFunction > } Node join_image_rel = join_image_term[0]; - std::hash_set< Node, NodeHashFunction > hasChecked; + std::unordered_set< Node, NodeHashFunction > hasChecked; Node join_image_rel_rep = getRepresentative( join_image_rel ); std::vector< Node >::iterator mem_rep_it = (*rel_mem_it).second.begin(); MEM_IT rel_mem_exp_it = d_rReps_memberReps_exp_cache.find( join_image_rel_rep ); @@ -480,14 +480,14 @@ typedef std::map< Node, std::map< Node, std::hash_set< Node, NodeHashFunction > if( tc_graph_it != (tc_it->second).end() ) { (tc_graph_it->second).insert( mem_rep_snd ); } else { - std::hash_set< Node, NodeHashFunction > sets; + std::unordered_set< Node, NodeHashFunction > sets; sets.insert( mem_rep_snd ); (tc_it->second)[mem_rep_fst] = sets; } } else { std::map< Node, Node > exp_map; - std::hash_set< Node, NodeHashFunction > sets; - std::map< Node, std::hash_set<Node, NodeHashFunction> > element_map; + std::unordered_set< Node, NodeHashFunction > sets; + std::map< Node, std::unordered_set<Node, NodeHashFunction> > element_map; sets.insert( mem_rep_snd ); element_map[mem_rep_fst] = sets; d_tcr_tcGraph[tc_rel] = element_map; @@ -529,7 +529,7 @@ typedef std::map< Node, std::map< Node, std::hash_set< Node, NodeHashFunction > TC_IT tc_it = d_rRep_tcGraph.find( getRepresentative(tc_rel[0]) ); if( tc_it != d_rRep_tcGraph.end() ) { bool isReachable = false; - std::hash_set<Node, NodeHashFunction> seen; + std::unordered_set<Node, NodeHashFunction> seen; isTCReachable( getRepresentative( RelsUtils::nthElementOfTuple(mem_rep, 0) ), getRepresentative( RelsUtils::nthElementOfTuple(mem_rep, 1) ), seen, tc_it->second, isReachable ); return isReachable; @@ -537,8 +537,8 @@ typedef std::map< Node, std::map< Node, std::hash_set< Node, NodeHashFunction > return false; } - void TheorySetsRels::isTCReachable( Node start, Node dest, std::hash_set<Node, NodeHashFunction>& hasSeen, - std::map< Node, std::hash_set< Node, NodeHashFunction > >& tc_graph, bool& isReachable ) { + void TheorySetsRels::isTCReachable( Node start, Node dest, std::unordered_set<Node, NodeHashFunction>& hasSeen, + std::map< Node, std::unordered_set< Node, NodeHashFunction > >& tc_graph, bool& isReachable ) { if(hasSeen.find(start) == hasSeen.end()) { hasSeen.insert(start); } @@ -550,7 +550,7 @@ typedef std::map< Node, std::map< Node, std::hash_set< Node, NodeHashFunction > isReachable = true; return; } else { - std::hash_set< Node, NodeHashFunction >::iterator set_it = pair_set_it->second.begin(); + std::unordered_set< Node, NodeHashFunction >::iterator set_it = pair_set_it->second.begin(); while( set_it != pair_set_it->second.end() ) { // need to check if *set_it has been looked already @@ -565,7 +565,7 @@ typedef std::map< Node, std::map< Node, std::hash_set< Node, NodeHashFunction > void TheorySetsRels::buildTCGraphForRel( Node tc_rel ) { std::map< Node, Node > rel_tc_graph_exps; - std::map< Node, std::hash_set<Node, NodeHashFunction> > rel_tc_graph; + std::map< Node, std::unordered_set<Node, NodeHashFunction> > rel_tc_graph; Node rel_rep = getRepresentative( tc_rel[0] ); Node tc_rel_rep = getRepresentative( tc_rel ); @@ -576,10 +576,10 @@ typedef std::map< Node, std::map< Node, std::hash_set< Node, NodeHashFunction > Node fst_element_rep = getRepresentative( RelsUtils::nthElementOfTuple( members[i], 0 )); Node snd_element_rep = getRepresentative( RelsUtils::nthElementOfTuple( members[i], 1 )); Node tuple_rep = RelsUtils::constructPair( rel_rep, fst_element_rep, snd_element_rep ); - std::map< Node, std::hash_set<Node, NodeHashFunction> >::iterator rel_tc_graph_it = rel_tc_graph.find( fst_element_rep ); + std::map< Node, std::unordered_set<Node, NodeHashFunction> >::iterator rel_tc_graph_it = rel_tc_graph.find( fst_element_rep ); if( rel_tc_graph_it == rel_tc_graph.end() ) { - std::hash_set< Node, NodeHashFunction > snd_elements; + std::unordered_set< Node, NodeHashFunction > snd_elements; snd_elements.insert( snd_element_rep ); rel_tc_graph[fst_element_rep] = snd_elements; rel_tc_graph_exps[tuple_rep] = exps[i]; @@ -596,13 +596,13 @@ typedef std::map< Node, std::map< Node, std::hash_set< Node, NodeHashFunction > } } - void TheorySetsRels::doTCInference( std::map< Node, std::hash_set<Node, NodeHashFunction> > rel_tc_graph, std::map< Node, Node > rel_tc_graph_exps, Node tc_rel ) { + void TheorySetsRels::doTCInference( std::map< Node, std::unordered_set<Node, NodeHashFunction> > rel_tc_graph, std::map< Node, Node > rel_tc_graph_exps, Node tc_rel ) { Trace("rels-debug") << "[Theory::Rels] ****** doTCInference !" << std::endl; for( TC_GRAPH_IT tc_graph_it = rel_tc_graph.begin(); tc_graph_it != rel_tc_graph.end(); tc_graph_it++ ) { - for( std::hash_set< Node, NodeHashFunction >::iterator snd_elements_it = tc_graph_it->second.begin(); + for( std::unordered_set< Node, NodeHashFunction >::iterator snd_elements_it = tc_graph_it->second.begin(); snd_elements_it != tc_graph_it->second.end(); snd_elements_it++ ) { std::vector< Node > reasons; - std::hash_set<Node, NodeHashFunction> seen; + std::unordered_set<Node, NodeHashFunction> seen; Node tuple = RelsUtils::constructPair( tc_rel, getRepresentative( tc_graph_it->first ), getRepresentative( *snd_elements_it) ); Assert( rel_tc_graph_exps.find( tuple ) != rel_tc_graph_exps.end() ); Node exp = rel_tc_graph_exps.find( tuple )->second; @@ -615,8 +615,8 @@ typedef std::map< Node, std::map< Node, std::hash_set< Node, NodeHashFunction > Trace("rels-debug") << "[Theory::Rels] ****** Done with doTCInference !" << std::endl; } - void TheorySetsRels::doTCInference(Node tc_rel, std::vector< Node > reasons, std::map< Node, std::hash_set< Node, NodeHashFunction > >& tc_graph, - std::map< Node, Node >& rel_tc_graph_exps, Node start_node_rep, Node cur_node_rep, std::hash_set< Node, NodeHashFunction >& seen ) { + void TheorySetsRels::doTCInference(Node tc_rel, std::vector< Node > reasons, std::map< Node, std::unordered_set< Node, NodeHashFunction > >& tc_graph, + std::map< Node, Node >& rel_tc_graph_exps, Node start_node_rep, Node cur_node_rep, std::unordered_set< Node, NodeHashFunction >& seen ) { Node tc_mem = RelsUtils::constructPair( tc_rel, RelsUtils::nthElementOfTuple((reasons.front())[0], 0), RelsUtils::nthElementOfTuple((reasons.back())[0], 1) ); std::vector< Node > all_reasons( reasons ); @@ -646,7 +646,7 @@ typedef std::map< Node, std::map< Node, std::hash_set< Node, NodeHashFunction > seen.insert( cur_node_rep ); TC_GRAPH_IT cur_set = tc_graph.find( cur_node_rep ); if( cur_set != tc_graph.end() ) { - for( std::hash_set< Node, NodeHashFunction >::iterator set_it = cur_set->second.begin(); + for( std::unordered_set< Node, NodeHashFunction >::iterator set_it = cur_set->second.begin(); set_it != cur_set->second.end(); set_it++ ) { Node new_pair = RelsUtils::constructPair( tc_rel, cur_node_rep, *set_it ); std::vector< Node > new_reasons( reasons ); diff --git a/src/theory/sets/theory_sets_rels.h b/src/theory/sets/theory_sets_rels.h index 16770671a..eb97405dc 100644 --- a/src/theory/sets/theory_sets_rels.h +++ b/src/theory/sets/theory_sets_rels.h @@ -17,11 +17,13 @@ #ifndef SRC_THEORY_SETS_THEORY_SETS_RELS_H_ #define SRC_THEORY_SETS_THEORY_SETS_RELS_H_ -#include "theory/theory.h" -#include "theory/uf/equality_engine.h" -#include "context/cdhashset.h" +#include <unordered_set> + #include "context/cdchunk_list.h" +#include "context/cdhashset.h" #include "theory/sets/rels_utils.h" +#include "theory/theory.h" +#include "theory/uf/equality_engine.h" namespace CVC4 { namespace theory { @@ -103,12 +105,12 @@ private: std::map< Node, Node > d_pending_facts; - std::hash_set< Node, NodeHashFunction > d_rel_nodes; + std::unordered_set< Node, NodeHashFunction > d_rel_nodes; std::map< Node, std::vector<Node> > d_tuple_reps; std::map< Node, TupleTrie > d_membership_trie; /** Symbolic tuple variables that has been reduced to concrete ones */ - std::hash_set< Node, NodeHashFunction > d_symbolic_tuples; + std::unordered_set< Node, NodeHashFunction > d_symbolic_tuples; /** Mapping between relation and its member representatives */ std::map< Node, std::vector< Node > > d_rReps_memberReps_cache; @@ -120,8 +122,8 @@ private: std::map< Node, std::map<kind::Kind_t, std::vector<Node> > > d_terms_cache; /** Mapping between transitive closure relation TC(r) and its TC graph constructed based on the members of r*/ - std::map< Node, std::map< Node, std::hash_set<Node, NodeHashFunction> > > d_rRep_tcGraph; - std::map< Node, std::map< Node, std::hash_set<Node, NodeHashFunction> > > d_tcr_tcGraph; + std::map< Node, std::map< Node, std::unordered_set<Node, NodeHashFunction> > > d_rRep_tcGraph; + std::map< Node, std::map< Node, std::unordered_set<Node, NodeHashFunction> > > d_tcr_tcGraph; std::map< Node, std::map< Node, Node > > d_tcr_tcGraph_exps; std::map< Node, std::vector< Node > > d_tc_lemmas_last; @@ -154,9 +156,9 @@ private: void applyTCRule( Node mem, Node rel, Node rel_rep, Node exp); void buildTCGraphForRel( Node tc_rel ); void doTCInference(); - void doTCInference( std::map< Node, std::hash_set<Node, NodeHashFunction> > rel_tc_graph, std::map< Node, Node > rel_tc_graph_exps, Node tc_rel ); - void doTCInference(Node tc_rel, std::vector< Node > reasons, std::map< Node, std::hash_set< Node, NodeHashFunction > >& tc_graph, - std::map< Node, Node >& rel_tc_graph_exps, Node start_node_rep, Node cur_node_rep, std::hash_set< Node, NodeHashFunction >& seen ); + void doTCInference( std::map< Node, std::unordered_set<Node, NodeHashFunction> > rel_tc_graph, std::map< Node, Node > rel_tc_graph_exps, Node tc_rel ); + void doTCInference(Node tc_rel, std::vector< Node > reasons, std::map< Node, std::unordered_set< Node, NodeHashFunction > >& tc_graph, + std::map< Node, Node >& rel_tc_graph_exps, Node start_node_rep, Node cur_node_rep, std::unordered_set< Node, NodeHashFunction >& seen ); void composeMembersForRels( Node ); void computeMembersForBinOpRel( Node ); @@ -165,8 +167,8 @@ private: void computeMembersForJoinImageTerm( Node ); bool isTCReachable( Node mem_rep, Node tc_rel ); - void isTCReachable( Node start, Node dest, std::hash_set<Node, NodeHashFunction>& hasSeen, - std::map< Node, std::hash_set< Node, NodeHashFunction > >& tc_graph, bool& isReachable ); + void isTCReachable( Node start, Node dest, std::unordered_set<Node, NodeHashFunction>& hasSeen, + std::map< Node, std::unordered_set< Node, NodeHashFunction > >& tc_graph, bool& isReachable ); void addSharedTerm( TNode n ); diff --git a/src/theory/sets/theory_sets_rewriter.cpp b/src/theory/sets/theory_sets_rewriter.cpp index 3cce08398..8c3fe67d3 100644 --- a/src/theory/sets/theory_sets_rewriter.cpp +++ b/src/theory/sets/theory_sets_rewriter.cpp @@ -25,7 +25,7 @@ namespace theory { namespace sets { typedef std::set<TNode> Elements; -typedef std::hash_map<TNode, Elements, TNodeHashFunction> SettermElementsMap; +typedef std::unordered_map<TNode, Elements, TNodeHashFunction> SettermElementsMap; struct FlattenedNodeTag {}; typedef expr::Attribute<FlattenedNodeTag, bool> flattened; @@ -50,7 +50,7 @@ RewriteResponse flattenNode(TNode n, TNode trivialNode, TNode skipNode) return RewriteResponse(REWRITE_DONE, n); } - typedef std::hash_set<TNode, TNodeHashFunction> node_set; + typedef std::unordered_set<TNode, TNodeHashFunction> node_set; node_set visited; visited.insert(skipNode); diff --git a/src/theory/shared_terms_database.h b/src/theory/shared_terms_database.h index 6b78a1698..5ca625751 100644 --- a/src/theory/shared_terms_database.h +++ b/src/theory/shared_terms_database.h @@ -17,6 +17,8 @@ #pragma once +#include <unordered_map> + #include "context/cdhashset.h" #include "expr/node.h" #include "theory/theory.h" @@ -43,7 +45,7 @@ private: IntStat d_statSharedTerms; // Needs to be a map from Nodes as after a backtrack they might not exist - typedef std::hash_map<Node, shared_terms_list, TNodeHashFunction> SharedTermsMap; + typedef std::unordered_map<Node, shared_terms_list, TNodeHashFunction> SharedTermsMap; /** A map from atoms to a list of shared terms */ SharedTermsMap d_atomsToTerms; diff --git a/src/theory/substitutions.h b/src/theory/substitutions.h index 5a6618175..cca39a62e 100644 --- a/src/theory/substitutions.h +++ b/src/theory/substitutions.h @@ -19,9 +19,10 @@ #ifndef __CVC4__THEORY__SUBSTITUTIONS_H #define __CVC4__THEORY__SUBSTITUTIONS_H +//#include <algorithm> #include <utility> #include <vector> -#include <algorithm> +#include <unordered_map> #include "expr/node.h" #include "context/context.h" @@ -51,7 +52,7 @@ public: private: - typedef std::hash_map<Node, Node, NodeHashFunction> NodeCache; + typedef std::unordered_map<Node, Node, NodeHashFunction> NodeCache; /** The variables, in order of addition */ NodeMap d_substitutions; diff --git a/src/theory/term_registration_visitor.h b/src/theory/term_registration_visitor.h index 39cce27f9..2a84a7995 100644 --- a/src/theory/term_registration_visitor.h +++ b/src/theory/term_registration_visitor.h @@ -20,7 +20,7 @@ #include "context/context.h" #include "theory/shared_terms_database.h" -#include <ext/hash_map> +#include <unordered_map> namespace CVC4 { @@ -105,7 +105,7 @@ class SharedTermsVisitor { /** * Cache from preprocessing of atoms. */ - typedef std::hash_map<TNode, theory::Theory::Set, TNodeHashFunction> TNodeVisitedMap; + typedef std::unordered_map<TNode, theory::Theory::Set, TNodeHashFunction> TNodeVisitedMap; TNodeVisitedMap d_visited; /** diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp index f010798cd..8509e84ab 100644 --- a/src/theory/theory.cpp +++ b/src/theory/theory.cpp @@ -220,8 +220,8 @@ void Theory::debugPrintFacts() const{ printFacts(DebugChannel.getStream()); } -std::hash_set<TNode, TNodeHashFunction> Theory::currentlySharedTerms() const{ - std::hash_set<TNode, TNodeHashFunction> currentlyShared; +std::unordered_set<TNode, TNodeHashFunction> Theory::currentlySharedTerms() const{ + std::unordered_set<TNode, TNodeHashFunction> currentlyShared; for (shared_terms_iterator i = shared_terms_begin(), i_end = shared_terms_end(); i != i_end; ++i) { currentlyShared.insert (*i); diff --git a/src/theory/theory.h b/src/theory/theory.h index 82607a165..73102a6e2 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -19,11 +19,11 @@ #ifndef __CVC4__THEORY__THEORY_H #define __CVC4__THEORY__THEORY_H -#include <ext/hash_set> #include <iosfwd> #include <map> #include <set> #include <string> +#include <unordered_set> #include "context/cdlist.h" #include "context/cdhashset.h" @@ -760,7 +760,7 @@ public: * This is a utility function for constructing a copy of the currently shared terms * in a queriable form. As this is */ - std::hash_set<TNode, TNodeHashFunction> currentlySharedTerms() const; + std::unordered_set<TNode, TNodeHashFunction> currentlySharedTerms() const; /** * This allows the theory to be queried for whether a literal, lit, is diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 7369b7c1f..1023071dc 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -1645,7 +1645,7 @@ Node TheoryEngine::getExplanation(TNode node) { struct AtomsCollect { std::vector<TNode> d_atoms; - std::hash_set<TNode, TNodeHashFunction> d_visited; + std::unordered_set<TNode, TNodeHashFunction> d_visited; public: diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 82283ef7b..408bff228 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -21,6 +21,7 @@ #include <deque> #include <set> +#include <unordered_map> #include <vector> #include <utility> @@ -189,8 +190,8 @@ class TheoryEngine { theory::TheoryEngineModelBuilder* d_curr_model_builder; bool d_aloc_curr_model_builder; - typedef std::hash_map<Node, Node, NodeHashFunction> NodeMap; - typedef std::hash_map<TNode, Node, TNodeHashFunction> TNodeMap; + typedef std::unordered_map<Node, Node, NodeHashFunction> NodeMap; + typedef std::unordered_map<TNode, Node, TNodeHashFunction> TNodeMap; /** * Cache for theory-preprocessing of assertions diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp index b9a08e3ac..0f92f976e 100644 --- a/src/theory/theory_model.cpp +++ b/src/theory/theory_model.cpp @@ -132,7 +132,7 @@ Cardinality TheoryModel::getCardinality( Type t ) const{ Node TheoryModel::getModelValue(TNode n, bool hasBoundVars, bool useDontCares) const { - std::hash_map<Node, Node, NodeHashFunction>::iterator it = d_modelCache.find(n); + std::unordered_map<Node, Node, NodeHashFunction>::iterator it = d_modelCache.find(n); if (it != d_modelCache.end()) { return (*it).second; } diff --git a/src/theory/theory_model.h b/src/theory/theory_model.h index 126de1e46..c1c57795b 100644 --- a/src/theory/theory_model.h +++ b/src/theory/theory_model.h @@ -17,6 +17,9 @@ #ifndef __CVC4__THEORY__THEORY_MODEL_H #define __CVC4__THEORY__THEORY_MODEL_H +#include <unordered_map> +#include <unordered_set> + #include "smt/model.h" #include "theory/uf/equality_engine.h" #include "theory/rep_set.h" @@ -52,7 +55,7 @@ public: /** true/false nodes */ Node d_true; Node d_false; - mutable std::hash_map<Node, Node, NodeHashFunction> d_modelCache; + mutable std::unordered_map<Node, Node, NodeHashFunction> d_modelCache; public: /** comment stream to include in printing */ std::stringstream d_comment_str; @@ -140,8 +143,8 @@ public: */ class TypeSet { public: - typedef std::hash_map<TypeNode, std::set<Node>*, TypeNodeHashFunction> TypeSetMap; - typedef std::hash_map<TypeNode, TypeEnumerator*, TypeNodeHashFunction> TypeToTypeEnumMap; + typedef std::unordered_map<TypeNode, std::set<Node>*, TypeNodeHashFunction> TypeSetMap; + typedef std::unordered_map<TypeNode, TypeEnumerator*, TypeNodeHashFunction> TypeToTypeEnumMap; typedef TypeSetMap::iterator iterator; typedef TypeSetMap::const_iterator const_iterator; private: @@ -265,9 +268,9 @@ class TheoryEngineModelBuilder : public ModelBuilder protected: /** pointer to theory engine */ TheoryEngine* d_te; - typedef std::hash_map<Node, Node, NodeHashFunction> NodeMap; + typedef std::unordered_map<Node, Node, NodeHashFunction> NodeMap; NodeMap d_normalizedCache; - typedef std::hash_set<Node, NodeHashFunction> NodeSet; + typedef std::unordered_set<Node, NodeHashFunction> NodeSet; std::map< Node, Node > d_constantReps; /** process build model */ diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h index 7c8e27575..5be32ab90 100644 --- a/src/theory/uf/equality_engine.h +++ b/src/theory/uf/equality_engine.h @@ -20,8 +20,8 @@ #pragma once #include <deque> -#include <ext/hash_map> #include <queue> +#include <unordered_map> #include <vector> #include "base/output.h" @@ -234,10 +234,10 @@ private: std::map<unsigned, const PathReconstructionNotify*> d_pathReconstructionTriggers; /** Map from nodes to their ids */ - __gnu_cxx::hash_map<TNode, EqualityNodeId, TNodeHashFunction> d_nodeIds; + std::unordered_map<TNode, EqualityNodeId, TNodeHashFunction> d_nodeIds; /** Map from function applications to their ids */ - typedef __gnu_cxx::hash_map<FunctionApplication, EqualityNodeId, FunctionApplicationHashFunction> ApplicationIdsMap; + typedef std::unordered_map<FunctionApplication, EqualityNodeId, FunctionApplicationHashFunction> ApplicationIdsMap; /** * A map from a pair (a', b') to a function application f(a, b), where a' and b' are the current representatives @@ -611,7 +611,7 @@ private: */ std::vector<TriggerTermSetRef> d_nodeIndividualTrigger; - typedef std::hash_map<EqualityPair, DisequalityReasonRef, EqualityPairHashFunction> DisequalityReasonsMap; + typedef std::unordered_map<EqualityPair, DisequalityReasonRef, EqualityPairHashFunction> DisequalityReasonsMap; /** * A map from pairs of disequal terms, to the reason why we deduced they are disequal. diff --git a/src/theory/uf/symmetry_breaker.cpp b/src/theory/uf/symmetry_breaker.cpp index cffa367cf..8a1c30ba6 100644 --- a/src/theory/uf/symmetry_breaker.cpp +++ b/src/theory/uf/symmetry_breaker.cpp @@ -61,7 +61,7 @@ SymmetryBreaker::Template::Template() : } TNode SymmetryBreaker::Template::find(TNode n) { - hash_map<TNode, TNode, TNodeHashFunction>::iterator i = d_reps.find(n); + unordered_map<TNode, TNode, TNodeHashFunction>::iterator i = d_reps.find(n); if(i == d_reps.end()) { return n; } else { @@ -400,8 +400,8 @@ void SymmetryBreaker::assertFormula(TNode phi) { break; } } - hash_map<TNode, set<TNode>, TNodeHashFunction>& ps = t.partitions(); - for(hash_map<TNode, set<TNode>, TNodeHashFunction>::iterator i = ps.begin(); + unordered_map<TNode, set<TNode>, TNodeHashFunction>& ps = t.partitions(); + for(unordered_map<TNode, set<TNode>, TNodeHashFunction>::iterator i = ps.begin(); i != ps.end(); ++i) { Debug("ufsymm") << "UFSYMM partition*: " << (*i).first; @@ -421,9 +421,9 @@ void SymmetryBreaker::assertFormula(TNode phi) { } if(!d_template.match(phi)) { // we hit a bad match, extract the partitions and reset the template - hash_map<TNode, set<TNode>, TNodeHashFunction>& ps = d_template.partitions(); + unordered_map<TNode, set<TNode>, TNodeHashFunction>& ps = d_template.partitions(); Debug("ufsymm") << "UFSYMM hit a bad match---have " << ps.size() << " partitions:" << endl; - for(hash_map<TNode, set<TNode>, TNodeHashFunction>::iterator i = ps.begin(); + for(unordered_map<TNode, set<TNode>, TNodeHashFunction>::iterator i = ps.begin(); i != ps.end(); ++i) { Debug("ufsymm") << "UFSYMM partition: " << (*i).first; diff --git a/src/theory/uf/symmetry_breaker.h b/src/theory/uf/symmetry_breaker.h index a814c670b..64ca41df2 100644 --- a/src/theory/uf/symmetry_breaker.h +++ b/src/theory/uf/symmetry_breaker.h @@ -46,6 +46,7 @@ #include <iostream> #include <list> +#include <unordered_map> #include <vector> #include "context/cdlist.h" @@ -64,8 +65,8 @@ class SymmetryBreaker : public context::ContextNotifyObj { class Template { Node d_template; NodeBuilder<> d_assertions; - std::hash_map<TNode, std::set<TNode>, TNodeHashFunction> d_sets; - std::hash_map<TNode, TNode, TNodeHashFunction> d_reps; + std::unordered_map<TNode, std::set<TNode>, TNodeHashFunction> d_sets; + std::unordered_map<TNode, TNode, TNodeHashFunction> d_reps; TNode find(TNode n); bool matchRecursive(TNode t, TNode n); @@ -73,7 +74,7 @@ class SymmetryBreaker : public context::ContextNotifyObj { public: Template(); bool match(TNode n); - std::hash_map<TNode, std::set<TNode>, TNodeHashFunction>& partitions() { return d_sets; } + std::unordered_map<TNode, std::set<TNode>, TNodeHashFunction>& partitions() { return d_sets; } Node assertions() { switch(d_assertions.getNumChildren()) { case 0: return Node::null(); @@ -91,7 +92,7 @@ public: typedef TNode Term; typedef std::list<Term> Terms; typedef std::set<Term> TermEq; - typedef std::hash_map<Term, TermEq, TNodeHashFunction> TermEqs; + typedef std::unordered_map<Term, TermEq, TNodeHashFunction> TermEqs; private: @@ -113,7 +114,7 @@ private: Permutations d_permutations; Terms d_terms; Template d_template; - std::hash_map<Node, Node, NodeHashFunction> d_normalizationCache; + std::unordered_map<Node, Node, NodeHashFunction> d_normalizationCache; TermEqs d_termEqs; TermEqs d_termEqsOnly; diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index 783585f8f..6d4d96a87 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -300,7 +300,7 @@ void TheoryUF::ppStaticLearn(TNode n, NodeBuilder<>& learned) { vector<TNode> workList; workList.push_back(n); - __gnu_cxx::hash_set<TNode, TNodeHashFunction> processed; + std::unordered_set<TNode, TNodeHashFunction> processed; while(!workList.empty()) { n = workList.back(); diff --git a/src/theory/unconstrained_simplifier.h b/src/theory/unconstrained_simplifier.h index a32dd076e..04c32f408 100644 --- a/src/theory/unconstrained_simplifier.h +++ b/src/theory/unconstrained_simplifier.h @@ -20,8 +20,10 @@ #ifndef __CVC4__UNCONSTRAINED_SIMPLIFIER_H #define __CVC4__UNCONSTRAINED_SIMPLIFIER_H -#include <vector> +#include <unordered_map> +#include <unordered_set> #include <utility> +#include <vector> #include "expr/node.h" #include "theory/substitutions.h" @@ -37,9 +39,9 @@ class UnconstrainedSimplifier { /** number of expressions eliminated due to unconstrained simplification */ IntStat d_numUnconstrainedElim; - typedef std::hash_map<TNode, unsigned, TNodeHashFunction> TNodeCountMap; - typedef std::hash_map<TNode, TNode, TNodeHashFunction> TNodeMap; - typedef std::hash_set<TNode, TNodeHashFunction> TNodeSet; + typedef std::unordered_map<TNode, unsigned, TNodeHashFunction> TNodeCountMap; + typedef std::unordered_map<TNode, TNode, TNodeHashFunction> TNodeMap; + typedef std::unordered_set<TNode, TNodeHashFunction> TNodeSet; TNodeCountMap d_visited; TNodeMap d_visitedOnce; diff --git a/src/util/cache.h b/src/util/cache.h index 6f5bac8eb..38dc0fc99 100644 --- a/src/util/cache.h +++ b/src/util/cache.h @@ -21,8 +21,10 @@ #ifndef __CVC4__CACHE_H #define __CVC4__CACHE_H -#include <utility> #include <functional> +#include <unordered_map> +#include <utility> +#include <vector> namespace CVC4 { @@ -33,7 +35,7 @@ namespace CVC4 { */ template <class T, class U, class Hasher = std::hash<T> > class Cache { - typedef std::hash_map<T, U, Hasher> Map; + typedef std::unordered_map<T, U, Hasher> Map; Map d_map; std::vector<T> d_current; typename Map::iterator d_result; diff --git a/src/util/hash.h b/src/util/hash.h index af468e25b..b04fb8bb5 100644 --- a/src/util/hash.h +++ b/src/util/hash.h @@ -20,13 +20,10 @@ #ifndef __CVC4__HASH_H #define __CVC4__HASH_H -// in case it's not been declared as a namespace yet -namespace __gnu_cxx {} +#include <functional> +#include <string> -#include <ext/hash_map> -#include <ext/hash_set> - -namespace __gnu_cxx { +namespace std { #ifdef CVC4_NEED_HASH_UINT64_T // on some versions and architectures of GNU C++, we need a @@ -39,18 +36,10 @@ struct hash<uint64_t> { };/* struct hash<uint64_t> */ #endif /* CVC4_NEED_HASH_UINT64_T */ -}/* __gnu_cxx namespace */ - -// hackish: treat hash stuff as if it were in std namespace -namespace std { using namespace __gnu_cxx; } +}/* std namespace */ namespace CVC4 { -struct StringHashFunction { - size_t operator()(const std::string& str) const { - return __gnu_cxx::hash<const char*>()(str.c_str()); - } -};/* struct StringHashFunction */ template <class T, class U, class HashT = std::hash<T>, class HashU = std::hash<U> > struct PairHashFunction { diff --git a/src/util/hash.i b/src/util/hash.i index 470447fc3..f2f1e6652 100644 --- a/src/util/hash.i +++ b/src/util/hash.i @@ -2,6 +2,4 @@ #include "util/hash.h" %} -%rename(apply) CVC4::StringHashFunction::operator()(const std::string&) const; - %include "util/hash.h" diff --git a/src/util/proof.h b/src/util/proof.h index af68efa97..b34e4aed9 100644 --- a/src/util/proof.h +++ b/src/util/proof.h @@ -21,7 +21,7 @@ #define __CVC4__PROOF_H #include <iosfwd> -#include <ext/hash_map> +#include <unordered_map> namespace CVC4 { @@ -29,7 +29,7 @@ class Expr; class ProofLetCount; struct ExprHashFunction; -typedef __gnu_cxx::hash_map<Expr, ProofLetCount, ExprHashFunction> ProofLetMap; +typedef std::unordered_map<Expr, ProofLetCount, ExprHashFunction> ProofLetMap; class CVC4_PUBLIC Proof { public: diff --git a/src/util/regexp.h b/src/util/regexp.h index 9fb8aea60..f451a8dec 100644 --- a/src/util/regexp.h +++ b/src/util/regexp.h @@ -21,6 +21,7 @@ #define __CVC4__REGEXP_H #include <cstddef> +#include <functional> #include <ostream> #include <string> #include <vector> diff --git a/test/regress/regress0/sygus/Makefile.am b/test/regress/regress0/sygus/Makefile.am index 0786c3f31..c22f64b93 100644 --- a/test/regress/regress0/sygus/Makefile.am +++ b/test/regress/regress0/sygus/Makefile.am @@ -61,7 +61,8 @@ TESTS = commutative.sy \ strings-trivial.sy \ General_plus10.sy \ qe.sy \ - cggmp.sy + cggmp.sy \ + parse-bv-let.sy # sygus tests currently taking too long for make regress diff --git a/test/regress/regress0/sygus/parse-bv-let.sy b/test/regress/regress0/sygus/parse-bv-let.sy new file mode 100644 index 000000000..88ddcf139 --- /dev/null +++ b/test/regress/regress0/sygus/parse-bv-let.sy @@ -0,0 +1,20 @@ +; EXPECT: unsat +; COMMAND-LINE: --no-dump-synth +(set-logic BV) + +(define-fun bit-reset ((x (BitVec 32)) (bit (BitVec 32))) (BitVec 32) + (let ((modulo-shift (BitVec 32) (bvand bit #x0000001f))) + (bvand modulo-shift x))) + +(synth-fun btr ((x (BitVec 32)) (bit (BitVec 32))) (BitVec 32) + ((Start (BitVec 32) ( + (Constant (BitVec 32)) + (Variable (BitVec 32)) + (bvneg Start) (bvnot Start) (bvadd Start Start) (bvand Start Start) (bvlshr Start Start) (bvmul Start Start) (bvor Start Start) (bvshl Start Start) + )))) + +(declare-var x (BitVec 32)) +(declare-var bit (BitVec 32)) +(constraint (= (btr x bit) #b00000000000000000000000000000000)) + +(check-synth) diff --git a/test/unit/context/cdmap_black.h b/test/unit/context/cdmap_black.h index 1b9e1fa7b..d0db0cc0f 100644 --- a/test/unit/context/cdmap_black.h +++ b/test/unit/context/cdmap_black.h @@ -16,178 +16,97 @@ #include <cxxtest/TestSuite.h> +#include <map> + +#include "base/cvc4_assert.h" +#include "context/context.h" #include "context/cdhashmap.h" #include "context/cdlist.h" -using namespace std; -using namespace CVC4; -using namespace CVC4::context; +using CVC4::AssertionException; +using CVC4::context::Context; +using CVC4::context::CDHashMap; class CDMapBlack : public CxxTest::TestSuite { - Context* d_context; -public: - + public: void setUp() { d_context = new Context; - //Debug.on("context"); - //Debug.on("gc"); - //Debug.on("pushpop"); + // Debug.on("context"); + // Debug.on("gc"); + // Debug.on("pushpop"); } - void tearDown() { - delete d_context; + void tearDown() { delete d_context; } + + // Returns the elements in a CDHashMap. + static std::map<int, int> GetElements(const CDHashMap<int, int>& map) { + return std::map<int, int>{map.begin(), map.end()}; + } + + // Returns true if the elements in map are the same as expected. + // NOTE: This is mostly to help the type checker for matching expected within + // a TS_ASSERT. + static bool ElementsAre(const CDHashMap<int, int>& map, + const std::map<int, int>& expected) { + return GetElements(map) == expected; } void testSimpleSequence() { CDHashMap<int, int> map(d_context); - - TS_ASSERT(map.find(3) == map.end()); - TS_ASSERT(map.find(5) == map.end()); - TS_ASSERT(map.find(9) == map.end()); - TS_ASSERT(map.find(1) == map.end()); - TS_ASSERT(map.find(23) == map.end()); + TS_ASSERT(ElementsAre(map, {})); map.insert(3, 4); - - TS_ASSERT(map.find(3) != map.end()); - TS_ASSERT(map.find(5) == map.end()); - TS_ASSERT(map.find(9) == map.end()); - TS_ASSERT(map.find(1) == map.end()); - TS_ASSERT(map.find(23) == map.end()); - TS_ASSERT(map[3] == 4); + TS_ASSERT(ElementsAre(map, {{3, 4}})); { d_context->push(); - - TS_ASSERT(map.find(3) != map.end()); - TS_ASSERT(map.find(5) == map.end()); - TS_ASSERT(map.find(9) == map.end()); - TS_ASSERT(map.find(1) == map.end()); - TS_ASSERT(map.find(23) == map.end()); - TS_ASSERT(map[3] == 4); + TS_ASSERT(ElementsAre(map, {{3, 4}})); map.insert(5, 6); map.insert(9, 8); - - TS_ASSERT(map.find(3) != map.end()); - TS_ASSERT(map.find(5) != map.end()); - TS_ASSERT(map.find(9) != map.end()); - TS_ASSERT(map.find(1) == map.end()); - TS_ASSERT(map.find(23) == map.end()); - TS_ASSERT(map[3] == 4); - TS_ASSERT(map[5] == 6); - TS_ASSERT(map[9] == 8); + TS_ASSERT(ElementsAre(map, {{3, 4}, {5, 6}, {9, 8}})); { d_context->push(); - - TS_ASSERT(map.find(3) != map.end()); - TS_ASSERT(map.find(5) != map.end()); - TS_ASSERT(map.find(9) != map.end()); - TS_ASSERT(map.find(1) == map.end()); - TS_ASSERT(map.find(23) == map.end()); - TS_ASSERT(map[3] == 4); - TS_ASSERT(map[5] == 6); - TS_ASSERT(map[9] == 8); + TS_ASSERT(ElementsAre(map, {{3, 4}, {5, 6}, {9, 8}})); map.insert(1, 2); - - TS_ASSERT(map.find(3) != map.end()); - TS_ASSERT(map.find(5) != map.end()); - TS_ASSERT(map.find(9) != map.end()); - TS_ASSERT(map.find(1) != map.end()); - TS_ASSERT(map.find(23) == map.end()); - TS_ASSERT(map[3] == 4); - TS_ASSERT(map[5] == 6); - TS_ASSERT(map[9] == 8); - TS_ASSERT(map[1] == 2); + TS_ASSERT(ElementsAre(map, {{1, 2}, {3, 4}, {5, 6}, {9, 8}})); { d_context->push(); - - TS_ASSERT(map.find(3) != map.end()); - TS_ASSERT(map.find(5) != map.end()); - TS_ASSERT(map.find(9) != map.end()); - TS_ASSERT(map.find(1) != map.end()); - TS_ASSERT(map.find(23) == map.end()); - TS_ASSERT(map[3] == 4); - TS_ASSERT(map[5] == 6); - TS_ASSERT(map[9] == 8); - TS_ASSERT(map[1] == 2); + TS_ASSERT(ElementsAre(map, {{1, 2}, {3, 4}, {5, 6}, {9, 8}})); map.insertAtContextLevelZero(23, 317); map.insert(1, 45); - TS_ASSERT(map.find(3) != map.end()); - TS_ASSERT(map.find(5) != map.end()); - TS_ASSERT(map.find(9) != map.end()); - TS_ASSERT(map.find(1) != map.end()); - TS_ASSERT(map.find(23) != map.end()); - TS_ASSERT(map[3] == 4); - TS_ASSERT(map[5] == 6); - TS_ASSERT(map[9] == 8); - TS_ASSERT(map[1] == 45); - TS_ASSERT(map[23] == 317); - + TS_ASSERT( + ElementsAre(map, {{1, 45}, {3, 4}, {5, 6}, {9, 8}, {23, 317}})); map.insert(23, 324); - TS_ASSERT(map.find(3) != map.end()); - TS_ASSERT(map.find(5) != map.end()); - TS_ASSERT(map.find(9) != map.end()); - TS_ASSERT(map.find(1) != map.end()); - TS_ASSERT(map.find(23) != map.end()); - TS_ASSERT(map[3] == 4); - TS_ASSERT(map[5] == 6); - TS_ASSERT(map[9] == 8); - TS_ASSERT(map[1] == 45); - TS_ASSERT(map[23] == 324); - + TS_ASSERT( + ElementsAre(map, {{1, 45}, {3, 4}, {5, 6}, {9, 8}, {23, 324}})); d_context->pop(); } - TS_ASSERT(map.find(3) != map.end()); - TS_ASSERT(map.find(5) != map.end()); - TS_ASSERT(map.find(9) != map.end()); - TS_ASSERT(map.find(1) != map.end()); - TS_ASSERT(map.find(23) != map.end()); - TS_ASSERT(map[3] == 4); - TS_ASSERT(map[5] == 6); - TS_ASSERT(map[9] == 8); - TS_ASSERT(map[1] == 2); - TS_ASSERT(map[23] == 317); - + TS_ASSERT( + ElementsAre(map, {{1, 2}, {3, 4}, {5, 6}, {9, 8}, {23, 317}})); d_context->pop(); } - TS_ASSERT(map.find(3) != map.end()); - TS_ASSERT(map.find(5) != map.end()); - TS_ASSERT(map.find(9) != map.end()); - TS_ASSERT(map.find(1) == map.end()); - TS_ASSERT(map.find(23) != map.end()); - TS_ASSERT(map[3] == 4); - TS_ASSERT(map[5] == 6); - TS_ASSERT(map[9] == 8); - TS_ASSERT(map[23] == 317); - + TS_ASSERT(ElementsAre(map, {{3, 4}, {5, 6}, {9, 8}, {23, 317}})); d_context->pop(); } - TS_ASSERT(map.find(3) != map.end()); - TS_ASSERT(map.find(5) == map.end()); - TS_ASSERT(map.find(9) == map.end()); - TS_ASSERT(map.find(1) == map.end()); - TS_ASSERT(map.find(23) != map.end()); - TS_ASSERT(map[3] == 4); - TS_ASSERT(map[23] == 317); + TS_ASSERT(ElementsAre(map, {{3, 4}, {23, 317}})); } // no intervening find() in this one // (under the theory that this could trigger a bug) void testSimpleSequenceFewerFinds() { CDHashMap<int, int> map(d_context); - map.insert(3, 4); { @@ -201,18 +120,9 @@ public: map.insert(1, 2); - TS_ASSERT(map.find(1) != map.end()); - TS_ASSERT(map.find(9) != map.end()); - TS_ASSERT(map.find(5) != map.end()); - TS_ASSERT(map.find(7) == map.end()); - TS_ASSERT(map.find(23) == map.end()); - TS_ASSERT(map[1] == 2); - TS_ASSERT(map[9] == 8); - TS_ASSERT(map[5] == 6); - + TS_ASSERT(ElementsAre(map, {{1, 2}, {3, 4}, {5, 6}, {9, 8}})); { d_context->push(); - d_context->pop(); } @@ -223,416 +133,34 @@ public: } } - void testObliterate() { - CDHashMap<int, int> map(d_context); - - map.insert(3, 4); - - TS_ASSERT(map.find(3) != map.end()); - TS_ASSERT(map.find(5) == map.end()); - TS_ASSERT(map.find(9) == map.end()); - TS_ASSERT(map.find(1) == map.end()); - TS_ASSERT(map.find(23) == map.end()); - TS_ASSERT(map[3] == 4); - - { - d_context->push(); - - TS_ASSERT(map.find(3) != map.end()); - TS_ASSERT(map.find(5) == map.end()); - TS_ASSERT(map.find(9) == map.end()); - TS_ASSERT(map.find(1) == map.end()); - TS_ASSERT(map.find(23) == map.end()); - TS_ASSERT(map[3] == 4); - - map.insert(5, 6); - map.insert(9, 8); - - TS_ASSERT(map.find(3) != map.end()); - TS_ASSERT(map.find(5) != map.end()); - TS_ASSERT(map.find(9) != map.end()); - TS_ASSERT(map.find(1) == map.end()); - TS_ASSERT(map.find(23) == map.end()); - TS_ASSERT(map[3] == 4); - TS_ASSERT(map[5] == 6); - TS_ASSERT(map[9] == 8); - - { - d_context->push(); - - TS_ASSERT(map.find(3) != map.end()); - TS_ASSERT(map.find(5) != map.end()); - TS_ASSERT(map.find(9) != map.end()); - TS_ASSERT(map.find(1) == map.end()); - TS_ASSERT(map.find(23) == map.end()); - TS_ASSERT(map[3] == 4); - TS_ASSERT(map[5] == 6); - TS_ASSERT(map[9] == 8); - - map.insertAtContextLevelZero(23, 317); - map.insert(1, 2); - - TS_ASSERT(map.find(3) != map.end()); - TS_ASSERT(map.find(5) != map.end()); - TS_ASSERT(map.find(9) != map.end()); - TS_ASSERT(map.find(1) != map.end()); - TS_ASSERT(map.find(23) != map.end()); - TS_ASSERT(map[3] == 4); - TS_ASSERT(map[5] == 6); - TS_ASSERT(map[9] == 8); - TS_ASSERT(map[1] == 2); - TS_ASSERT(map[23] == 317); - - map.obliterate(5); - - TS_ASSERT(map.find(3) != map.end()); - TS_ASSERT(map.find(5) == map.end()); - TS_ASSERT(map.find(9) != map.end()); - TS_ASSERT(map.find(1) != map.end()); - TS_ASSERT(map.find(23) != map.end()); - TS_ASSERT(map[3] == 4); - TS_ASSERT(map[9] == 8); - TS_ASSERT(map[1] == 2); - TS_ASSERT(map[23] == 317); - - { - d_context->push(); - - TS_ASSERT(map.find(3) != map.end()); - TS_ASSERT(map.find(5) == map.end()); - TS_ASSERT(map.find(9) != map.end()); - TS_ASSERT(map.find(1) != map.end()); - TS_ASSERT(map.find(23) != map.end()); - TS_ASSERT(map[3] == 4); - TS_ASSERT(map[9] == 8); - TS_ASSERT(map[1] == 2); - TS_ASSERT(map[23] == 317); - - d_context->pop(); - } - - TS_ASSERT(map.find(3) != map.end()); - TS_ASSERT(map.find(5) == map.end()); - TS_ASSERT(map.find(9) != map.end()); - TS_ASSERT(map.find(1) != map.end()); - TS_ASSERT(map.find(23) != map.end()); - TS_ASSERT(map[3] == 4); - TS_ASSERT(map[9] == 8); - TS_ASSERT(map[1] == 2); - TS_ASSERT(map[23] == 317); - - map.obliterate(23); - - TS_ASSERT(map.find(3) != map.end()); - TS_ASSERT(map.find(5) == map.end()); - TS_ASSERT(map.find(9) != map.end()); - TS_ASSERT(map.find(1) != map.end()); - TS_ASSERT(map.find(23) == map.end()); - TS_ASSERT(map[3] == 4); - TS_ASSERT(map[9] == 8); - TS_ASSERT(map[1] == 2); - - d_context->pop(); - } - - TS_ASSERT(map.find(3) != map.end()); - TS_ASSERT(map.find(5) == map.end()); - TS_ASSERT(map.find(9) != map.end()); - TS_ASSERT(map.find(1) == map.end()); - TS_ASSERT(map.find(23) == map.end()); - TS_ASSERT(map[3] == 4); - TS_ASSERT(map[9] == 8); - - d_context->pop(); - } - - TS_ASSERT(map.find(3) != map.end()); - TS_ASSERT(map.find(5) == map.end()); - TS_ASSERT(map.find(9) == map.end()); - TS_ASSERT(map.find(1) == map.end()); - TS_ASSERT(map.find(23) == map.end()); - TS_ASSERT(map[3] == 4); - } - - void testObliteratePrimordial() { - CDHashMap<int, int> map(d_context); - - map.insert(3, 4); - - TS_ASSERT(map.find(3) != map.end()); - TS_ASSERT(map.find(5) == map.end()); - TS_ASSERT(map.find(9) == map.end()); - TS_ASSERT(map.find(1) == map.end()); - TS_ASSERT(map[3] == 4); - - { - d_context->push(); - - TS_ASSERT(map.find(3) != map.end()); - TS_ASSERT(map.find(5) == map.end()); - TS_ASSERT(map.find(9) == map.end()); - TS_ASSERT(map.find(1) == map.end()); - TS_ASSERT(map[3] == 4); - - map.insert(5, 6); - map.insert(9, 8); - - TS_ASSERT(map.find(3) != map.end()); - TS_ASSERT(map.find(5) != map.end()); - TS_ASSERT(map.find(9) != map.end()); - TS_ASSERT(map.find(1) == map.end()); - TS_ASSERT(map[3] == 4); - TS_ASSERT(map[5] == 6); - TS_ASSERT(map[9] == 8); - - { - d_context->push(); - - TS_ASSERT(map.find(3) != map.end()); - TS_ASSERT(map.find(5) != map.end()); - TS_ASSERT(map.find(9) != map.end()); - TS_ASSERT(map.find(1) == map.end()); - TS_ASSERT(map[3] == 4); - TS_ASSERT(map[5] == 6); - TS_ASSERT(map[9] == 8); - map.insert(1, 2); - - TS_ASSERT(map.find(3) != map.end()); - TS_ASSERT(map.find(5) != map.end()); - TS_ASSERT(map.find(9) != map.end()); - TS_ASSERT(map.find(1) != map.end()); - TS_ASSERT(map[3] == 4); - TS_ASSERT(map[5] == 6); - TS_ASSERT(map[9] == 8); - TS_ASSERT(map[1] == 2); - - map.obliterate(3); - - TS_ASSERT(map.find(3) == map.end()); - TS_ASSERT(map.find(5) != map.end()); - TS_ASSERT(map.find(9) != map.end()); - TS_ASSERT(map.find(1) != map.end()); - TS_ASSERT(map[5] == 6); - TS_ASSERT(map[9] == 8); - TS_ASSERT(map[1] == 2); - - { - d_context->push(); - - TS_ASSERT(map.find(3) == map.end()); - TS_ASSERT(map.find(5) != map.end()); - TS_ASSERT(map.find(9) != map.end()); - TS_ASSERT(map.find(1) != map.end()); - TS_ASSERT(map[5] == 6); - TS_ASSERT(map[9] == 8); - TS_ASSERT(map[1] == 2); - - d_context->pop(); - } - - TS_ASSERT(map.find(3) == map.end()); - TS_ASSERT(map.find(5) != map.end()); - TS_ASSERT(map.find(9) != map.end()); - TS_ASSERT(map.find(1) != map.end()); - TS_ASSERT(map[5] == 6); - TS_ASSERT(map[9] == 8); - TS_ASSERT(map[1] == 2); - - d_context->pop(); - } - - TS_ASSERT(map.find(3) == map.end()); - TS_ASSERT(map.find(5) != map.end()); - TS_ASSERT(map.find(9) != map.end()); - TS_ASSERT(map.find(1) == map.end()); - TS_ASSERT(map[5] == 6); - TS_ASSERT(map[9] == 8); - - d_context->pop(); - } - - TS_ASSERT(map.find(3) == map.end()); - TS_ASSERT(map.find(5) == map.end()); - TS_ASSERT(map.find(9) == map.end()); - TS_ASSERT(map.find(1) == map.end()); - } - - void testObliterateCurrent() { - CDHashMap<int, int> map(d_context); - - map.insert(3, 4); - - TS_ASSERT(map.find(3) != map.end()); - TS_ASSERT(map.find(5) == map.end()); - TS_ASSERT(map.find(9) == map.end()); - TS_ASSERT(map.find(1) == map.end()); - TS_ASSERT(map[3] == 4); - - { - d_context->push(); - - TS_ASSERT(map.find(3) != map.end()); - TS_ASSERT(map.find(5) == map.end()); - TS_ASSERT(map.find(9) == map.end()); - TS_ASSERT(map.find(1) == map.end()); - TS_ASSERT(map[3] == 4); - - map.insert(5, 6); - map.insert(9, 8); - - TS_ASSERT(map.find(3) != map.end()); - TS_ASSERT(map.find(5) != map.end()); - TS_ASSERT(map.find(9) != map.end()); - TS_ASSERT(map.find(1) == map.end()); - TS_ASSERT(map[3] == 4); - TS_ASSERT(map[5] == 6); - TS_ASSERT(map[9] == 8); - - { - d_context->push(); - - TS_ASSERT(map.find(3) != map.end()); - TS_ASSERT(map.find(5) != map.end()); - TS_ASSERT(map.find(9) != map.end()); - TS_ASSERT(map.find(1) == map.end()); - TS_ASSERT(map[3] == 4); - TS_ASSERT(map[5] == 6); - TS_ASSERT(map[9] == 8); - - map.insert(1, 2); - - TS_ASSERT(map.find(3) != map.end()); - TS_ASSERT(map.find(5) != map.end()); - TS_ASSERT(map.find(9) != map.end()); - TS_ASSERT(map.find(1) != map.end()); - TS_ASSERT(map[3] == 4); - TS_ASSERT(map[5] == 6); - TS_ASSERT(map[9] == 8); - TS_ASSERT(map[1] == 2); - - map.obliterate(1); - - TS_ASSERT(map.find(3) != map.end()); - TS_ASSERT(map.find(5) != map.end()); - TS_ASSERT(map.find(9) != map.end()); - TS_ASSERT(map.find(1) == map.end()); - TS_ASSERT(map[3] == 4); - TS_ASSERT(map[5] == 6); - TS_ASSERT(map[9] == 8); - - { - d_context->push(); - - TS_ASSERT(map.find(3) != map.end()); - TS_ASSERT(map.find(5) != map.end()); - TS_ASSERT(map.find(9) != map.end()); - TS_ASSERT(map.find(1) == map.end()); - TS_ASSERT(map[3] == 4); - TS_ASSERT(map[5] == 6); - TS_ASSERT(map[9] == 8); - - d_context->pop(); - } - - TS_ASSERT(map.find(3) != map.end()); - TS_ASSERT(map.find(5) != map.end()); - TS_ASSERT(map.find(9) != map.end()); - TS_ASSERT(map.find(1) == map.end()); - TS_ASSERT(map[3] == 4); - TS_ASSERT(map[5] == 6); - TS_ASSERT(map[9] == 8); - - d_context->pop(); - } - - TS_ASSERT(map.find(3) != map.end()); - TS_ASSERT(map.find(5) != map.end()); - TS_ASSERT(map.find(9) != map.end()); - TS_ASSERT(map.find(1) == map.end()); - TS_ASSERT(map[3] == 4); - TS_ASSERT(map[5] == 6); - TS_ASSERT(map[9] == 8); - - d_context->pop(); - } - - TS_ASSERT(map.find(3) != map.end()); - TS_ASSERT(map.find(5) == map.end()); - TS_ASSERT(map.find(9) == map.end()); - TS_ASSERT(map.find(1) == map.end()); - TS_ASSERT(map[3] == 4); - } - void testInsertAtContextLevelZero() { CDHashMap<int, int> map(d_context); map.insert(3, 4); - TS_ASSERT(map.find(3) != map.end()); - TS_ASSERT(map.find(5) == map.end()); - TS_ASSERT(map.find(9) == map.end()); - TS_ASSERT(map.find(1) == map.end()); - TS_ASSERT(map.find(23) == map.end()); - TS_ASSERT(map[3] == 4); - + TS_ASSERT(ElementsAre(map, {{3, 4}})); { d_context->push(); - - TS_ASSERT(map.find(3) != map.end()); - TS_ASSERT(map.find(5) == map.end()); - TS_ASSERT(map.find(9) == map.end()); - TS_ASSERT(map.find(1) == map.end()); - TS_ASSERT(map.find(23) == map.end()); - TS_ASSERT(map[3] == 4); + TS_ASSERT(ElementsAre(map, {{3, 4}})); map.insert(5, 6); map.insert(9, 8); - TS_ASSERT(map.find(3) != map.end()); - TS_ASSERT(map.find(5) != map.end()); - TS_ASSERT(map.find(9) != map.end()); - TS_ASSERT(map.find(1) == map.end()); - TS_ASSERT(map.find(23) == map.end()); - TS_ASSERT(map[3] == 4); - TS_ASSERT(map[5] == 6); - TS_ASSERT(map[9] == 8); + TS_ASSERT(ElementsAre(map, {{3, 4}, {5, 6}, {9, 8}})); { d_context->push(); - TS_ASSERT(map.find(3) != map.end()); - TS_ASSERT(map.find(5) != map.end()); - TS_ASSERT(map.find(9) != map.end()); - TS_ASSERT(map.find(1) == map.end()); - TS_ASSERT(map.find(23) == map.end()); - TS_ASSERT(map[3] == 4); - TS_ASSERT(map[5] == 6); - TS_ASSERT(map[9] == 8); + TS_ASSERT(ElementsAre(map, {{3, 4}, {5, 6}, {9, 8}})); map.insert(1, 2); - TS_ASSERT(map.find(3) != map.end()); - TS_ASSERT(map.find(5) != map.end()); - TS_ASSERT(map.find(9) != map.end()); - TS_ASSERT(map.find(1) != map.end()); - TS_ASSERT(map.find(23) == map.end()); - TS_ASSERT(map[3] == 4); - TS_ASSERT(map[5] == 6); - TS_ASSERT(map[9] == 8); - TS_ASSERT(map[1] == 2); + TS_ASSERT(ElementsAre(map, {{1, 2}, {3, 4}, {5, 6}, {9, 8}})); map.insertAtContextLevelZero(23, 317); - TS_ASSERT(map.find(3) != map.end()); - TS_ASSERT(map.find(5) != map.end()); - TS_ASSERT(map.find(9) != map.end()); - TS_ASSERT(map.find(1) != map.end()); - TS_ASSERT(map.find(23) != map.end()); - TS_ASSERT(map[3] == 4); - TS_ASSERT(map[5] == 6); - TS_ASSERT(map[9] == 8); - TS_ASSERT(map[1] == 2); - TS_ASSERT(map[23] == 317); + TS_ASSERT( + ElementsAre(map, {{1, 2}, {3, 4}, {5, 6}, {9, 8}, {23, 317}})); TS_ASSERT_THROWS(map.insertAtContextLevelZero(23, 317), AssertionException); @@ -640,278 +168,42 @@ public: AssertionException); map.insert(23, 472); - TS_ASSERT(map.find(3) != map.end()); - TS_ASSERT(map.find(5) != map.end()); - TS_ASSERT(map.find(9) != map.end()); - TS_ASSERT(map.find(1) != map.end()); - TS_ASSERT(map.find(23) != map.end()); - TS_ASSERT(map[3] == 4); - TS_ASSERT(map[5] == 6); - TS_ASSERT(map[9] == 8); - TS_ASSERT(map[1] == 2); - TS_ASSERT(map[23] == 472); - + TS_ASSERT( + ElementsAre(map, {{1, 2}, {3, 4}, {5, 6}, {9, 8}, {23, 472}})); { d_context->push(); - TS_ASSERT(map.find(3) != map.end()); - TS_ASSERT(map.find(5) != map.end()); - TS_ASSERT(map.find(9) != map.end()); - TS_ASSERT(map.find(1) != map.end()); - TS_ASSERT(map.find(23) != map.end()); - TS_ASSERT(map[3] == 4); - TS_ASSERT(map[5] == 6); - TS_ASSERT(map[9] == 8); - TS_ASSERT(map[1] == 2); - TS_ASSERT(map[23] == 472); + TS_ASSERT( + ElementsAre(map, {{1, 2}, {3, 4}, {5, 6}, {9, 8}, {23, 472}})); TS_ASSERT_THROWS(map.insertAtContextLevelZero(23, 0), AssertionException); map.insert(23, 1024); - TS_ASSERT(map.find(3) != map.end()); - TS_ASSERT(map.find(5) != map.end()); - TS_ASSERT(map.find(9) != map.end()); - TS_ASSERT(map.find(1) != map.end()); - TS_ASSERT(map.find(23) != map.end()); - TS_ASSERT(map[3] == 4); - TS_ASSERT(map[5] == 6); - TS_ASSERT(map[9] == 8); - TS_ASSERT(map[1] == 2); - TS_ASSERT(map[23] == 1024); - + TS_ASSERT( + ElementsAre(map, {{1, 2}, {3, 4}, {5, 6}, {9, 8}, {23, 1024}})); d_context->pop(); } - - TS_ASSERT(map.find(3) != map.end()); - TS_ASSERT(map.find(5) != map.end()); - TS_ASSERT(map.find(9) != map.end()); - TS_ASSERT(map.find(1) != map.end()); - TS_ASSERT(map.find(23) != map.end()); - TS_ASSERT(map[3] == 4); - TS_ASSERT(map[5] == 6); - TS_ASSERT(map[9] == 8); - TS_ASSERT(map[1] == 2); - TS_ASSERT(map[23] == 472); - + TS_ASSERT( + ElementsAre(map, {{1, 2}, {3, 4}, {5, 6}, {9, 8}, {23, 472}})); d_context->pop(); } - TS_ASSERT(map.find(3) != map.end()); - TS_ASSERT(map.find(5) != map.end()); - TS_ASSERT(map.find(9) != map.end()); - TS_ASSERT(map.find(1) == map.end()); - TS_ASSERT(map.find(23) != map.end()); - TS_ASSERT(map[3] == 4); - TS_ASSERT(map[5] == 6); - TS_ASSERT(map[9] == 8); - TS_ASSERT(map[23] == 317); - - TS_ASSERT_THROWS(map.insertAtContextLevelZero(23, 0), - AssertionException); - map.insert(23, 477); - - TS_ASSERT(map.find(3) != map.end()); - TS_ASSERT(map.find(5) != map.end()); - TS_ASSERT(map.find(9) != map.end()); - TS_ASSERT(map.find(1) == map.end()); - TS_ASSERT(map.find(23) != map.end()); - TS_ASSERT(map[3] == 4); - TS_ASSERT(map[5] == 6); - TS_ASSERT(map[9] == 8); - TS_ASSERT(map[23] == 477); - - d_context->pop(); - } - - TS_ASSERT_THROWS(map.insertAtContextLevelZero(23, 0), - AssertionException); - - TS_ASSERT(map.find(3) != map.end()); - TS_ASSERT(map.find(5) == map.end()); - TS_ASSERT(map.find(9) == map.end()); - TS_ASSERT(map.find(1) == map.end()); - TS_ASSERT(map.find(23) != map.end()); - TS_ASSERT(map[3] == 4); - TS_ASSERT(map[23] == 317); - } - - void testObliterateInsertedAtContextLevelZero() { - CDHashMap<int, int> map(d_context); - - map.insert(3, 4); - - TS_ASSERT(map.find(3) != map.end()); - TS_ASSERT(map.find(5) == map.end()); - TS_ASSERT(map.find(9) == map.end()); - TS_ASSERT(map.find(1) == map.end()); - TS_ASSERT(map.find(23) == map.end()); - TS_ASSERT(map[3] == 4); - - { - d_context->push(); - - TS_ASSERT(map.find(3) != map.end()); - TS_ASSERT(map.find(5) == map.end()); - TS_ASSERT(map.find(9) == map.end()); - TS_ASSERT(map.find(1) == map.end()); - TS_ASSERT(map.find(23) == map.end()); - TS_ASSERT(map[3] == 4); - - map.insert(5, 6); - map.insert(9, 8); - - TS_ASSERT(map.find(3) != map.end()); - TS_ASSERT(map.find(5) != map.end()); - TS_ASSERT(map.find(9) != map.end()); - TS_ASSERT(map.find(1) == map.end()); - TS_ASSERT(map.find(23) == map.end()); - TS_ASSERT(map[3] == 4); - TS_ASSERT(map[5] == 6); - TS_ASSERT(map[9] == 8); - - { - d_context->push(); - - TS_ASSERT(map.find(3) != map.end()); - TS_ASSERT(map.find(5) != map.end()); - TS_ASSERT(map.find(9) != map.end()); - TS_ASSERT(map.find(1) == map.end()); - TS_ASSERT(map.find(23) == map.end()); - TS_ASSERT(map[3] == 4); - TS_ASSERT(map[5] == 6); - TS_ASSERT(map[9] == 8); - - map.insert(1, 2); - - TS_ASSERT(map.find(3) != map.end()); - TS_ASSERT(map.find(5) != map.end()); - TS_ASSERT(map.find(9) != map.end()); - TS_ASSERT(map.find(1) != map.end()); - TS_ASSERT(map.find(23) == map.end()); - TS_ASSERT(map[3] == 4); - TS_ASSERT(map[5] == 6); - TS_ASSERT(map[9] == 8); - TS_ASSERT(map[1] == 2); - - map.insertAtContextLevelZero(23, 317); - - TS_ASSERT(map.find(3) != map.end()); - TS_ASSERT(map.find(5) != map.end()); - TS_ASSERT(map.find(9) != map.end()); - TS_ASSERT(map.find(1) != map.end()); - TS_ASSERT(map.find(23) != map.end()); - TS_ASSERT(map[3] == 4); - TS_ASSERT(map[5] == 6); - TS_ASSERT(map[9] == 8); - TS_ASSERT(map[1] == 2); - TS_ASSERT(map[23] == 317); - - TS_ASSERT_THROWS(map.insertAtContextLevelZero(23, 317), - AssertionException); - TS_ASSERT_THROWS(map.insertAtContextLevelZero(23, 472), - AssertionException); - map.insert(23, 472); - - TS_ASSERT(map.find(3) != map.end()); - TS_ASSERT(map.find(5) != map.end()); - TS_ASSERT(map.find(9) != map.end()); - TS_ASSERT(map.find(1) != map.end()); - TS_ASSERT(map.find(23) != map.end()); - TS_ASSERT(map[3] == 4); - TS_ASSERT(map[5] == 6); - TS_ASSERT(map[9] == 8); - TS_ASSERT(map[1] == 2); - TS_ASSERT(map[23] == 472); - - { - d_context->push(); - - TS_ASSERT(map.find(3) != map.end()); - TS_ASSERT(map.find(5) != map.end()); - TS_ASSERT(map.find(9) != map.end()); - TS_ASSERT(map.find(1) != map.end()); - TS_ASSERT(map.find(23) != map.end()); - TS_ASSERT(map[3] == 4); - TS_ASSERT(map[5] == 6); - TS_ASSERT(map[9] == 8); - TS_ASSERT(map[1] == 2); - TS_ASSERT(map[23] == 472); - - TS_ASSERT_THROWS(map.insertAtContextLevelZero(23, 0), - AssertionException); - map.insert(23, 1024); - - TS_ASSERT(map.find(3) != map.end()); - TS_ASSERT(map.find(5) != map.end()); - TS_ASSERT(map.find(9) != map.end()); - TS_ASSERT(map.find(1) != map.end()); - TS_ASSERT(map.find(23) != map.end()); - TS_ASSERT(map[3] == 4); - TS_ASSERT(map[5] == 6); - TS_ASSERT(map[9] == 8); - TS_ASSERT(map[1] == 2); - TS_ASSERT(map[23] == 1024); - - d_context->pop(); - } - TS_ASSERT(map.find(3) != map.end()); - TS_ASSERT(map.find(5) != map.end()); - TS_ASSERT(map.find(9) != map.end()); - TS_ASSERT(map.find(1) != map.end()); - TS_ASSERT(map.find(23) != map.end()); - TS_ASSERT(map[3] == 4); - TS_ASSERT(map[5] == 6); - TS_ASSERT(map[9] == 8); - TS_ASSERT(map[1] == 2); - TS_ASSERT(map[23] == 472); - - map.obliterate(23); - - TS_ASSERT(map.find(3) != map.end()); - TS_ASSERT(map.find(5) != map.end()); - TS_ASSERT(map.find(9) != map.end()); - TS_ASSERT(map.find(1) != map.end()); - TS_ASSERT(map.find(23) == map.end()); - TS_ASSERT(map[3] == 4); - TS_ASSERT(map[5] == 6); - TS_ASSERT(map[9] == 8); - TS_ASSERT(map[1] == 2); + TS_ASSERT( + ElementsAre(map, {{3, 4}, {5, 6}, {9, 8}, {23, 317}})); - d_context->pop(); - } - - TS_ASSERT(map.find(3) != map.end()); - TS_ASSERT(map.find(5) != map.end()); - TS_ASSERT(map.find(9) != map.end()); - TS_ASSERT(map.find(1) == map.end()); - TS_ASSERT(map.find(23) == map.end()); - TS_ASSERT(map[3] == 4); - TS_ASSERT(map[5] == 6); - TS_ASSERT(map[9] == 8); - - // reinsert as a normal map entry + TS_ASSERT_THROWS(map.insertAtContextLevelZero(23, 0), AssertionException); map.insert(23, 477); - TS_ASSERT(map.find(3) != map.end()); - TS_ASSERT(map.find(5) != map.end()); - TS_ASSERT(map.find(9) != map.end()); - TS_ASSERT(map.find(1) == map.end()); - TS_ASSERT(map.find(23) != map.end()); - TS_ASSERT(map[3] == 4); - TS_ASSERT(map[5] == 6); - TS_ASSERT(map[9] == 8); - TS_ASSERT(map[23] == 477); - + TS_ASSERT( + ElementsAre(map, {{3, 4}, {5, 6}, {9, 8}, {23, 477}})); d_context->pop(); } - TS_ASSERT(map.find(3) != map.end()); - TS_ASSERT(map.find(5) == map.end()); - TS_ASSERT(map.find(9) == map.end()); - TS_ASSERT(map.find(1) == map.end()); - TS_ASSERT(map.find(23) == map.end()); - TS_ASSERT(map[3] == 4); + TS_ASSERT_THROWS(map.insertAtContextLevelZero(23, 0), AssertionException); + + TS_ASSERT( + ElementsAre(map, {{3, 4}, {23, 317}})); } }; diff --git a/test/unit/expr/attribute_black.h b/test/unit/expr/attribute_black.h index d919bcbe3..d3f043f36 100644 --- a/test/unit/expr/attribute_black.h +++ b/test/unit/expr/attribute_black.h @@ -88,10 +88,7 @@ public: } struct PrimitiveIntAttributeId {}; - struct CDPrimitiveIntAttributeId {}; - typedef expr::Attribute<PrimitiveIntAttributeId,uint64_t> PrimitiveIntAttribute; - typedef expr::CDAttribute<CDPrimitiveIntAttributeId,uint64_t> CDPrimitiveIntAttribute; void testInts(){ TypeNode booleanType = d_nodeManager->booleanType(); Node* node = new Node(d_nodeManager->mkSkolem("b", booleanType)); @@ -105,21 +102,12 @@ public: TS_ASSERT(node->getAttribute(attr, data1)); TS_ASSERT_EQUALS(data1, val); - uint64_t data2 = 0; - uint64_t data3 = 0; - CDPrimitiveIntAttribute cdattr; - TS_ASSERT(!node->getAttribute(cdattr, data2)); - node->setAttribute(cdattr, val); - TS_ASSERT(node->getAttribute(cdattr, data3)); - TS_ASSERT_EQUALS(data3, val); delete node; } struct TNodeAttributeId {}; - struct CDTNodeAttributeId {}; typedef expr::Attribute<TNodeAttributeId, TNode> TNodeAttribute; - typedef expr::CDAttribute<CDTNodeAttributeId, TNode> CDTNodeAttribute; void testTNodes(){ TypeNode booleanType = d_nodeManager->booleanType(); Node* node = new Node(d_nodeManager->mkSkolem("b", booleanType)); @@ -134,13 +122,6 @@ public: TS_ASSERT(node->getAttribute(attr, data1)); TS_ASSERT_EQUALS(data1, val); - TNode data2; - TNode data3; - CDTNodeAttribute cdattr; - TS_ASSERT(!node->getAttribute(cdattr, data2)); - node->setAttribute(cdattr, val); - TS_ASSERT(node->getAttribute(cdattr, data3)); - TS_ASSERT_EQUALS(data3, val); delete node; } @@ -152,10 +133,8 @@ public: }; struct PtrAttributeId {}; - struct CDPtrAttributeId {}; typedef expr::Attribute<PtrAttributeId, Foo*> PtrAttribute; - typedef expr::CDAttribute<CDPtrAttributeId, Foo*> CDPtrAttribute; void testPtrs(){ TypeNode booleanType = d_nodeManager->booleanType(); Node* node = new Node(d_nodeManager->mkSkolem("b", booleanType)); @@ -170,25 +149,14 @@ public: TS_ASSERT(node->getAttribute(attr, data1)); TS_ASSERT_EQUALS(data1, val); - Foo* data2 = NULL; - Foo* data3 = NULL; - CDPtrAttribute cdattr; - TS_ASSERT(!node->getAttribute(cdattr, data2)); - node->setAttribute(cdattr, val); - TS_ASSERT(node->getAttribute(cdattr, data3)); - TS_ASSERT(data3 != NULL); - TS_ASSERT_EQUALS(63489, data3->getBar()); - TS_ASSERT_EQUALS(data3, val); delete node; delete val; } struct ConstPtrAttributeId {}; - struct CDConstPtrAttributeId {}; typedef expr::Attribute<ConstPtrAttributeId, const Foo*> ConstPtrAttribute; - typedef expr::CDAttribute<CDConstPtrAttributeId, const Foo*> CDConstPtrAttribute; void testConstPtrs(){ TypeNode booleanType = d_nodeManager->booleanType(); Node* node = new Node(d_nodeManager->mkSkolem("b", booleanType)); @@ -203,22 +171,12 @@ public: TS_ASSERT(node->getAttribute(attr, data1)); TS_ASSERT_EQUALS(data1, val); - const Foo* data2 = NULL; - const Foo* data3 = NULL; - CDConstPtrAttribute cdattr; - TS_ASSERT(!node->getAttribute(cdattr, data2)); - node->setAttribute(cdattr, val); - TS_ASSERT(node->getAttribute(cdattr, data3)); - TS_ASSERT_EQUALS(data3, val); delete node; delete val; } struct StringAttributeId {}; - struct CDStringAttributeId {}; - typedef expr::Attribute<StringAttributeId, std::string> StringAttribute; - typedef expr::CDAttribute<CDStringAttributeId, std::string> CDStringAttribute; void testStrings(){ TypeNode booleanType = d_nodeManager->booleanType(); Node* node = new Node(d_nodeManager->mkSkolem("b", booleanType)); @@ -233,21 +191,11 @@ public: TS_ASSERT(node->getAttribute(attr, data1)); TS_ASSERT_EQUALS(data1, val); - std::string data2; - std::string data3; - CDStringAttribute cdattr; - TS_ASSERT(!node->getAttribute(cdattr, data2)); - node->setAttribute(cdattr, val); - TS_ASSERT(node->getAttribute(cdattr, data3)); - TS_ASSERT_EQUALS(data3, val); delete node; } struct BoolAttributeId {}; - struct CDBoolAttributeId {}; - typedef expr::Attribute<BoolAttributeId, bool> BoolAttribute; - typedef expr::CDAttribute<CDBoolAttributeId, bool> CDBoolAttribute; void testBools(){ TypeNode booleanType = d_nodeManager->booleanType(); Node* node = new Node(d_nodeManager->mkSkolem("b", booleanType)); @@ -263,14 +211,6 @@ public: TS_ASSERT(node->getAttribute(attr, data1)); TS_ASSERT_EQUALS(data1, val); - bool data2 = false; - bool data3 = false; - CDBoolAttribute cdattr; - TS_ASSERT(node->getAttribute(cdattr, data2)); - TS_ASSERT_EQUALS(false, data2); - node->setAttribute(cdattr, val); - TS_ASSERT(node->getAttribute(cdattr, data3)); - TS_ASSERT_EQUALS(data3, val); delete node; } diff --git a/test/unit/expr/attribute_white.h b/test/unit/expr/attribute_white.h index e4786b8e3..60a83b5c7 100644 --- a/test/unit/expr/attribute_white.h +++ b/test/unit/expr/attribute_white.h @@ -47,18 +47,12 @@ struct Test5; typedef Attribute<Test1, std::string> TestStringAttr1; typedef Attribute<Test2, std::string> TestStringAttr2; -// it would be nice to have CDAttribute<> for context-dependence -typedef CDAttribute<Test1, bool> TestCDFlag; - typedef Attribute<Test1, bool> TestFlag1; typedef Attribute<Test2, bool> TestFlag2; typedef Attribute<Test3, bool> TestFlag3; typedef Attribute<Test4, bool> TestFlag4; typedef Attribute<Test5, bool> TestFlag5; -typedef CDAttribute<Test1, bool> TestFlag1cd; -typedef CDAttribute<Test2, bool> TestFlag2cd; - class AttributeWhite : public CxxTest::TestSuite { ExprManager* d_em; @@ -127,11 +121,6 @@ public: TS_ASSERT_DIFFERS(TestFlag4::s_id, TestFlag5::s_id); lastId = attr::LastAttributeId<bool, true>::getId(); - TS_ASSERT_LESS_THAN(TestFlag1cd::s_id, lastId); - TS_ASSERT_LESS_THAN(TestFlag2cd::s_id, lastId); - TS_ASSERT_DIFFERS(TestFlag1cd::s_id, TestFlag2cd::s_id); - cout << "1: " << TestFlag1cd::s_id << endl; - cout << "2: " << TestFlag2cd::s_id << endl; lastId = attr::LastAttributeId<Node, false>::getId(); // TS_ASSERT_LESS_THAN(theory::PreRewriteCache::s_id, lastId); @@ -149,132 +138,6 @@ public: TS_ASSERT_LESS_THAN(TypeAttr::s_id, lastId); } - void testCDAttributes() { - //Debug.on("cdboolattr"); - - Node a = d_nm->mkVar(*d_booleanType); - Node b = d_nm->mkVar(*d_booleanType); - Node c = d_nm->mkVar(*d_booleanType); - - Debug("cdboolattr") << "get flag 1 on a (should be F)\n"; - TS_ASSERT(! a.getAttribute(TestFlag1cd())); - Debug("cdboolattr") << "get flag 1 on b (should be F)\n"; - TS_ASSERT(! b.getAttribute(TestFlag1cd())); - Debug("cdboolattr") << "get flag 1 on c (should be F)\n"; - TS_ASSERT(! c.getAttribute(TestFlag1cd())); - - d_smtEngine->push(); // level 1 - - // test that all boolean flags are FALSE to start - Debug("cdboolattr") << "get flag 1 on a (should be F)\n"; - TS_ASSERT(! a.getAttribute(TestFlag1cd())); - Debug("cdboolattr") << "get flag 1 on b (should be F)\n"; - TS_ASSERT(! b.getAttribute(TestFlag1cd())); - Debug("cdboolattr") << "get flag 1 on c (should be F)\n"; - TS_ASSERT(! c.getAttribute(TestFlag1cd())); - - // test that they all HAVE the boolean attributes - TS_ASSERT(a.hasAttribute(TestFlag1cd())); - TS_ASSERT(b.hasAttribute(TestFlag1cd())); - TS_ASSERT(c.hasAttribute(TestFlag1cd())); - - // test two-arg version of hasAttribute() - bool bb = false; - Debug("cdboolattr") << "get flag 1 on a (should be F)\n"; - TS_ASSERT(a.getAttribute(TestFlag1cd(), bb)); - TS_ASSERT(! bb); - Debug("cdboolattr") << "get flag 1 on b (should be F)\n"; - TS_ASSERT(b.getAttribute(TestFlag1cd(), bb)); - TS_ASSERT(! bb); - Debug("cdboolattr") << "get flag 1 on c (should be F)\n"; - TS_ASSERT(c.getAttribute(TestFlag1cd(), bb)); - TS_ASSERT(! bb); - - // setting boolean flags - Debug("cdboolattr") << "set flag 1 on a to T\n"; - a.setAttribute(TestFlag1cd(), true); - Debug("cdboolattr") << "set flag 1 on b to F\n"; - b.setAttribute(TestFlag1cd(), false); - Debug("cdboolattr") << "set flag 1 on c to F\n"; - c.setAttribute(TestFlag1cd(), false); - - Debug("cdboolattr") << "get flag 1 on a (should be T)\n"; - TS_ASSERT(a.getAttribute(TestFlag1cd())); - Debug("cdboolattr") << "get flag 1 on b (should be F)\n"; - TS_ASSERT(! b.getAttribute(TestFlag1cd())); - Debug("cdboolattr") << "get flag 1 on c (should be F)\n"; - TS_ASSERT(! c.getAttribute(TestFlag1cd())); - - d_smtEngine->push(); // level 2 - - Debug("cdboolattr") << "get flag 1 on a (should be T)\n"; - TS_ASSERT(a.getAttribute(TestFlag1cd())); - Debug("cdboolattr") << "get flag 1 on b (should be F)\n"; - TS_ASSERT(! b.getAttribute(TestFlag1cd())); - Debug("cdboolattr") << "get flag 1 on c (should be F)\n"; - TS_ASSERT(! c.getAttribute(TestFlag1cd())); - - Debug("cdboolattr") << "set flag 1 on a to F\n"; - a.setAttribute(TestFlag1cd(), false); - Debug("cdboolattr") << "set flag 1 on b to T\n"; - b.setAttribute(TestFlag1cd(), true); - - Debug("cdboolattr") << "get flag 1 on a (should be F)\n"; - TS_ASSERT(! a.getAttribute(TestFlag1cd())); - Debug("cdboolattr") << "get flag 1 on b (should be T)\n"; - TS_ASSERT(b.getAttribute(TestFlag1cd())); - Debug("cdboolattr") << "get flag 1 on c (should be F)\n"; - TS_ASSERT(! c.getAttribute(TestFlag1cd())); - - d_smtEngine->push(); // level 3 - - Debug("cdboolattr") << "get flag 1 on a (should be F)\n"; - TS_ASSERT(! a.getAttribute(TestFlag1cd())); - Debug("cdboolattr") << "get flag 1 on b (should be T)\n"; - TS_ASSERT(b.getAttribute(TestFlag1cd())); - Debug("cdboolattr") << "get flag 1 on c (should be F)\n"; - TS_ASSERT(! c.getAttribute(TestFlag1cd())); - - Debug("cdboolattr") << "set flag 1 on c to T\n"; - c.setAttribute(TestFlag1cd(), true); - - Debug("cdboolattr") << "get flag 1 on a (should be F)\n"; - TS_ASSERT(! a.getAttribute(TestFlag1cd())); - Debug("cdboolattr") << "get flag 1 on b (should be T)\n"; - TS_ASSERT(b.getAttribute(TestFlag1cd())); - Debug("cdboolattr") << "get flag 1 on c (should be T)\n"; - TS_ASSERT(c.getAttribute(TestFlag1cd())); - - d_smtEngine->pop(); // level 2 - - Debug("cdboolattr") << "get flag 1 on a (should be F)\n"; - TS_ASSERT(! a.getAttribute(TestFlag1cd())); - Debug("cdboolattr") << "get flag 1 on b (should be T)\n"; - TS_ASSERT(b.getAttribute(TestFlag1cd())); - Debug("cdboolattr") << "get flag 1 on c (should be F)\n"; - TS_ASSERT(! c.getAttribute(TestFlag1cd())); - - d_smtEngine->pop(); // level 1 - - Debug("cdboolattr") << "get flag 1 on a (should be T)\n"; - TS_ASSERT(a.getAttribute(TestFlag1cd())); - Debug("cdboolattr") << "get flag 1 on b (should be F)\n"; - TS_ASSERT(! b.getAttribute(TestFlag1cd())); - Debug("cdboolattr") << "get flag 1 on c (should be F)\n"; - TS_ASSERT(! c.getAttribute(TestFlag1cd())); - - d_smtEngine->pop(); // level 0 - - Debug("cdboolattr") << "get flag 1 on a (should be F)\n"; - TS_ASSERT(! a.getAttribute(TestFlag1cd())); - Debug("cdboolattr") << "get flag 1 on b (should be F)\n"; - TS_ASSERT(! b.getAttribute(TestFlag1cd())); - Debug("cdboolattr") << "get flag 1 on c (should be F)\n"; - TS_ASSERT(! c.getAttribute(TestFlag1cd())); - - TS_ASSERT_THROWS( d_smtEngine->pop(), ModalException ); - } - void testAttributes() { //Debug.on("boolattr"); diff --git a/test/unit/theory/type_enumerator_white.h b/test/unit/theory/type_enumerator_white.h index 3094345bd..af1d9ab48 100644 --- a/test/unit/theory/type_enumerator_white.h +++ b/test/unit/theory/type_enumerator_white.h @@ -17,6 +17,8 @@ #include <cxxtest/TestSuite.h> +#include <unordered_set> + #include "expr/array_store_all.h" #include "expr/expr_manager.h" #include "expr/kind.h" @@ -252,7 +254,7 @@ std::cout<<"here\n"; void testArraysInfinite() { TypeEnumerator te(d_nm->mkArrayType(d_nm->integerType(), d_nm->integerType())); - hash_set<Node, NodeHashFunction> elts; + unordered_set<Node, NodeHashFunction> elts; for(size_t i = 0; i < 1000; ++i) { TS_ASSERT( ! te.isFinished() ); Node elt = *te++; |