From 8b0659e6cd342ae40b676781b5e819d5fd2b3af7 Mon Sep 17 00:00:00 2001 From: Tim King Date: Thu, 20 Jul 2017 17:04:30 -0700 Subject: [PATCH] Moving from the gnu extensions for hash maps to the c++11 hash maps * Replacing __gnu_cxx::hash_map with std::unordered_map. * Replacing __gnu_cxx::hash_set with std::unordered_set. * Replacing __gnu_cxx::hash with std::hash. * Adding missing includes. --- configure.ac | 10 ++-- examples/sets-translate/sets_translate.cpp | 3 +- examples/simple_vc_compat_c.c | 3 +- src/compat/cvc3_compat.cpp | 18 +++---- src/compat/cvc3_compat.h | 10 ++-- src/context/cdhashmap.h | 9 ++-- src/context/cdhashmap_forward.h | 7 ++- src/context/cdinsert_hashmap.h | 7 +-- src/context/cdtrail_hashmap.h | 7 +-- src/context/cdtrail_hashmap_forward.h | 7 +-- src/cvc4.i | 6 +-- src/decision/justification_heuristic.h | 7 +-- src/expr/attribute_internals.h | 8 +-- src/expr/datatype.h | 9 ++-- src/expr/expr_template.cpp | 4 +- src/expr/expr_template.h | 4 +- src/expr/node.h | 42 +++++++-------- src/expr/node_manager.cpp | 2 - src/expr/node_manager.h | 14 ++--- src/expr/record.h | 6 +-- src/expr/symbol_table.cpp | 6 +-- src/expr/symbol_table.h | 6 +-- src/expr/type_node.cpp | 4 +- src/expr/type_node.h | 22 ++++---- src/expr/variable_type_map.h | 9 ++-- src/parser/smt1/smt1.cpp | 12 ++--- src/parser/smt1/smt1.h | 7 ++- src/parser/smt2/Smt2.g | 7 +-- src/parser/smt2/smt2.h | 3 +- src/parser/tptp/tptp.h | 7 +-- src/printer/dagification_visitor.h | 11 ++-- src/proof/arith_proof.h | 4 +- src/proof/array_proof.h | 4 +- src/proof/bitvector_proof.h | 15 +++--- src/proof/cnf_proof.h | 10 ++-- src/proof/proof_manager.h | 14 ++--- src/proof/proof_output_channel.h | 4 +- src/proof/proof_utils.h | 8 +-- src/proof/sat_proof.h | 15 +++--- src/proof/skolemization_manager.cpp | 4 +- src/proof/skolemization_manager.h | 11 ++-- src/proof/theory_proof.h | 7 +-- src/proof/uf_proof.h | 4 +- src/prop/bvminisat/core/Solver.cc | 2 +- src/prop/bvminisat/core/Solver.h | 1 - src/prop/cnf_stream.h | 2 - src/prop/minisat/core/Solver.cc | 3 +- src/prop/theory_proxy.h | 3 +- src/smt/smt_engine.cpp | 51 ++++++++++--------- src/smt/term_formula_removal.h | 3 +- src/smt_util/nary_builder.h | 4 +- src/theory/arith/arith_ite_utils.h | 13 ++--- src/theory/arith/arith_utilities.h | 9 ++-- src/theory/arith/constraint.cpp | 5 +- src/theory/arith/constraint.h | 4 +- src/theory/arith/cut_log.h | 4 +- src/theory/arith/dio_solver.cpp | 2 +- src/theory/arith/dio_solver.h | 3 +- src/theory/arith/pseudoboolean_proc.h | 4 +- src/theory/arith/simplex.h | 4 +- src/theory/arith/theory_arith_private.cpp | 2 +- src/theory/arrays/array_info.h | 5 +- src/theory/arrays/static_fact_manager.h | 4 +- src/theory/arrays/theory_arrays.cpp | 6 +-- src/theory/arrays/theory_arrays.h | 8 +-- src/theory/arrays/theory_arrays_rewriter.h | 9 ++-- src/theory/arrays/union_find.h | 4 +- src/theory/booleans/circuit_propagator.h | 5 +- src/theory/booleans/theory_bool_rewriter.cpp | 4 +- src/theory/bv/abstraction.h | 28 +++++----- src/theory/bv/bitblaster_template.h | 19 +++---- src/theory/bv/bv_eager_solver.h | 13 +++-- src/theory/bv/bv_inequality_graph.h | 30 ++++++----- src/theory/bv/bv_quick_check.h | 4 +- src/theory/bv/bv_subtheory_algebraic.h | 20 +++++--- src/theory/bv/bv_subtheory_bitblast.h | 4 +- src/theory/bv/bv_subtheory_core.h | 14 +++-- src/theory/bv/bv_subtheory_inequality.h | 8 +-- src/theory/bv/bv_to_bool.h | 4 +- src/theory/bv/bvintropow2.h | 4 +- src/theory/bv/slicer.h | 10 ++-- src/theory/bv/theory_bv.h | 17 ++++--- .../theory_bv_rewrite_rules_normalization.h | 19 ++++--- src/theory/bv/theory_bv_utils.h | 15 +++--- src/theory/datatypes/theory_datatypes.h | 1 - src/theory/ite_utilities.cpp | 6 +-- src/theory/ite_utilities.h | 23 ++++----- src/theory/quantifiers/equality_infer.h | 1 - src/theory/quantifiers/inst_match.h | 5 +- src/theory/quantifiers/quant_util.h | 7 ++- src/theory/quantifiers/term_database.cpp | 3 +- src/theory/quantifiers/term_database.h | 8 +-- src/theory/quantifiers/theory_quantifiers.h | 16 ++---- src/theory/quantifiers_engine.cpp | 4 +- src/theory/quantifiers_engine.h | 4 +- src/theory/rewriter.cpp | 4 +- src/theory/sets/theory_sets_rels.cpp | 38 +++++++------- src/theory/sets/theory_sets_rels.h | 26 +++++----- src/theory/sets/theory_sets_rewriter.cpp | 4 +- src/theory/shared_terms_database.h | 4 +- src/theory/substitutions.h | 5 +- src/theory/term_registration_visitor.h | 4 +- src/theory/theory.cpp | 4 +- src/theory/theory.h | 4 +- src/theory/theory_engine.cpp | 2 +- src/theory/theory_engine.h | 5 +- src/theory/theory_model.cpp | 2 +- src/theory/theory_model.h | 13 +++-- src/theory/uf/equality_engine.h | 8 +-- src/theory/uf/symmetry_breaker.cpp | 10 ++-- src/theory/uf/symmetry_breaker.h | 11 ++-- src/theory/uf/theory_uf.cpp | 2 +- src/theory/unconstrained_simplifier.h | 10 ++-- src/util/cache.h | 6 ++- src/util/hash.h | 19 ++----- src/util/hash.i | 2 - src/util/proof.h | 4 +- src/util/regexp.cpp | 1 + src/util/regexp.h | 10 ++-- test/unit/theory/type_enumerator_white.h | 4 +- 120 files changed, 536 insertions(+), 494 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 or not. Some do, some don't. +# instantiates std::hash or not. Some do, some don't. # See src/util/hash.h. -AC_MSG_CHECKING([whether __gnu_cxx::hash is already specialized]) +AC_MSG_CHECKING([whether std::hash is already specialized]) AC_LANG_PUSH([C++]) AC_COMPILE_IFELSE([AC_LANG_SOURCE([ -#include -#include -namespace __gnu_cxx { template<> struct hash {}; }])], +#include +#include +namespace std { template<> struct hash {}; }])], [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 #include #include +#include #include #include "expr/expr.h" @@ -83,7 +84,7 @@ class Mapper { set< Type > setTypes; map< Type, Type > mapTypes; map< pair, 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 #include -/* #include /* use this after CVC4 is properly installed */ +// Use this after CVC4 is properly installed. +// #include #include "bindings/compat/c/c_interface.h" int main() { diff --git a/src/compat/cvc3_compat.cpp b/src/compat/cvc3_compat.cpp index 3309ce442..ffb299394 100644 --- a/src/compat/cvc3_compat.cpp +++ b/src/compat/cvc3_compat.cpp @@ -21,7 +21,6 @@ #include #include #include -#include #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 s_validityCheckers; -static std::hash_map s_typeToExpr; -static std::hash_map s_exprToType; +static std::unordered_map s_typeToExpr; +static std::unordered_map s_exprToType; static bool typeHasExpr(const Type& t) { - std::hash_map::const_iterator i = s_typeToExpr.find(t); + std::unordered_map::const_iterator i = s_typeToExpr.find(t); return i != s_typeToExpr.end(); } static Expr typeToExpr(const Type& t) { - std::hash_map::const_iterator i = s_typeToExpr.find(t); + std::unordered_map::const_iterator i = s_typeToExpr.find(t); assert(i != s_typeToExpr.end()); return (*i).second; } static Type exprToType(const Expr& e) { - std::hash_map::const_iterator i = s_exprToType.find(e); + std::unordered_map::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& oldTerms, } Expr Expr::substExpr(const ExprHashMap& oldToNew) const { - const hash_map& o2n = - *reinterpret_cast*>(&oldToNew); + const unordered_map& o2n = + *reinterpret_cast*>(&oldToNew); return Expr(substitute(o2n)); } 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 + #include +#include +#include #include #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 { };/* class ExprMap */ template -class CVC4_PUBLIC ExprHashMap : public std::hash_map { +class CVC4_PUBLIC ExprHashMap : public std::unordered_map { public: void insert(Expr a, Expr b); };/* class ExprHashMap */ @@ -521,8 +523,8 @@ class CVC4_PUBLIC ValidityChecker { friend class Type; // to reach in to d_exprTypeMapRemove - typedef std::hash_map ConstructorMap; - typedef std::hash_map, CVC4::StringHashFunction> SelectorMap; + typedef std::unordered_map ConstructorMap; + typedef std::unordered_map> SelectorMap; ConstructorMap d_constructors; SelectorMap d_selectors; diff --git a/src/context/cdhashmap.h b/src/context/cdhashmap.h index 575bde120..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. @@ -82,8 +82,9 @@ #ifndef __CVC4__CONTEXT__CDHASHMAP_H #define __CVC4__CONTEXT__CDHASHMAP_H -#include +#include #include +#include #include #include "base/cvc4_assert.h" @@ -95,7 +96,7 @@ namespace context { // Auxiliary class: almost the same as CDO (see cdo.h) -template > +template > class CDOhash_map : public ContextObj { friend class CDHashMap; @@ -268,7 +269,7 @@ template class CDHashMap : public ContextObj { typedef CDOhash_map Element; - typedef __gnu_cxx::hash_map table_type; + typedef std::unordered_map table_type; friend class CDOhash_map; 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 + /// \cond internals -namespace __gnu_cxx { - template struct hash; -}/* __gnu_cxx namespace */ namespace CVC4 { namespace context { - template > + template > 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 -#include +#include +#include #include #include "base/cvc4_assert.h" @@ -50,14 +51,14 @@ namespace CVC4 { namespace context { -template > +template > class InsertHashMap { private: typedef std::deque KeyVec; /** A list of the keys in the map maintained as a stack. */ KeyVec d_keys; - typedef __gnu_cxx::hash_map HashMap; + typedef std::unordered_map 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 #include +#include +#include #include #include "base/cvc4_assert.h" @@ -58,7 +59,7 @@ namespace CVC4 { namespace context { -template > +template > 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 PositionMap; + typedef std::unordered_map 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 struct hash; -}/* __gnu_cxx namespace */ +#include namespace CVC4 { namespace context { - template > + template > class CDTrailHashMap; }/* CVC4::context namespace */ }/* CVC4 namespace */ - 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 set {}; - template class hash_map {}; + template class unordered_map {}; } %{ @@ -41,7 +41,7 @@ namespace CVC4 {} using namespace CVC4; #include -#include +#include #include #include #include @@ -86,7 +86,7 @@ std::set 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 + #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 d_visited; + std::unordered_set d_visited; /** * Set to track visited nodes in a dfs search done in computeITE * function */ - hash_set d_visitedComputeITE; + std::unordered_set 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_internals.h b/src/expr/attribute_internals.h index 28c618cb0..37c7b6a0b 100644 --- a/src/expr/attribute_internals.h +++ b/src/expr/attribute_internals.h @@ -23,7 +23,7 @@ #ifndef __CVC4__EXPR__ATTRIBUTE_INTERNALS_H #define __CVC4__EXPR__ATTRIBUTE_INTERNALS_H -#include +#include namespace CVC4 { namespace expr { @@ -150,7 +150,7 @@ namespace attr { */ template class AttrHash : - public __gnu_cxx::hash_map, + public std::unordered_map, value_type, AttrHashFunction> { };/* class AttrHash<> */ @@ -161,12 +161,12 @@ class AttrHash : */ template <> class AttrHash : - protected __gnu_cxx::hash_map { /** A "super" type, like in Java, for easy reference below. */ - typedef __gnu_cxx::hash_map super; + typedef std::unordered_map super; /** * BitAccessor allows us to return a bit "by reference." Of course, 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 #include #include #include @@ -788,16 +789,16 @@ public: */ struct CVC4_PUBLIC DatatypeHashFunction { inline size_t operator()(const Datatype& dt) const { - return StringHashFunction()(dt.getName()); + return std::hash()(dt.getName()); } inline size_t operator()(const Datatype* dt) const { - return StringHashFunction()(dt->getName()); + return std::hash()(dt->getName()); } inline size_t operator()(const DatatypeConstructor& dtc) const { - return StringHashFunction()(dtc.getName()); + return std::hash()(dtc.getName()); } inline size_t operator()(const DatatypeConstructor* dtc) const { - return StringHashFunction()(dtc->getName()); + return std::hash()(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, TNodeHashFunction> ExportCache; + typedef std::unordered_map , NodeTemplate, TNodeHashFunction> ExportCache; ExprManager* from; ExprManager* to; ExprManagerMapCollection& vmap; @@ -393,7 +393,7 @@ static inline NodePairIteratorAdaptor mkNodePairIteratorAdaptor(Iterat return NodePairIteratorAdaptor(i); } -Expr Expr::substitute(const std::hash_map map) const { +Expr Expr::substitute(const std::unordered_map 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 #include #include - #include +#include #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 map) const; + Expr substitute(const std::unordered_map 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 -#include -#include -#include +#include + #include #include -#include +#include +#include +#include +#include +#include +#include #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& cache) const; + std::unordered_map& cache) const; /** * Cache-aware, recursive version of substitute() used by the public @@ -252,7 +254,7 @@ public: template Node substitute(Iterator1 nodesBegin, Iterator1 nodesEnd, Iterator2 replacementsBegin, Iterator2 replacementsEnd, - std::hash_map& cache) const; + std::unordered_map& cache) const; /** * Cache-aware, recursive version of substitute() used by the public @@ -260,7 +262,7 @@ public: */ template Node substitute(Iterator substitutionsBegin, Iterator substitutionsEnd, - std::hash_map& cache) const; + std::unordered_map& 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 - //#include "expr/attribute.h" #include "expr/node_manager.h" #include "expr/type_checker.h" @@ -1296,14 +1296,14 @@ NodeTemplate::substitute(TNode node, TNode replacement) const { if (node == *this) { return replacement; } - std::hash_map cache; + std::unordered_map cache; return substitute(node, replacement, cache); } template Node NodeTemplate::substitute(TNode node, TNode replacement, - std::hash_map& cache) const { + std::unordered_map& cache) const { Assert(node != *this); if (getNumChildren() == 0) { @@ -1311,7 +1311,7 @@ NodeTemplate::substitute(TNode node, TNode replacement, } // in cache? - typename std::hash_map::const_iterator i = cache.find(*this); + typename std::unordered_map::const_iterator i = cache.find(*this); if(i != cache.end()) { return (*i).second; } @@ -1351,7 +1351,7 @@ NodeTemplate::substitute(Iterator1 nodesBegin, Iterator1 nodesEnd, Iterator2 replacementsBegin, Iterator2 replacementsEnd) const { - std::hash_map cache; + std::unordered_map cache; return substitute(nodesBegin, nodesEnd, replacementsBegin, replacementsEnd, cache); } @@ -1363,9 +1363,9 @@ NodeTemplate::substitute(Iterator1 nodesBegin, Iterator1 nodesEnd, Iterator2 replacementsBegin, Iterator2 replacementsEnd, - std::hash_map& cache) const { + std::unordered_map& cache) const { // in cache? - typename std::hash_map::const_iterator i = cache.find(*this); + typename std::unordered_map::const_iterator i = cache.find(*this); if(i != cache.end()) { return (*i).second; } @@ -1410,7 +1410,7 @@ template inline Node NodeTemplate::substitute(Iterator substitutionsBegin, Iterator substitutionsEnd) const { - std::hash_map cache; + std::unordered_map cache; return substitute(substitutionsBegin, substitutionsEnd, cache); } @@ -1419,9 +1419,9 @@ template Node NodeTemplate::substitute(Iterator substitutionsBegin, Iterator substitutionsEnd, - std::hash_map& cache) const { + std::unordered_map& cache) const { // in cache? - typename std::hash_map::const_iterator i = cache.find(*this); + typename std::unordered_map::const_iterator i = cache.find(*this); if(i != cache.end()) { return (*i).second; } @@ -1468,7 +1468,7 @@ inline Node NodeTemplate::fromExpr(const Expr& e) { template bool NodeTemplate::hasSubterm(NodeTemplate t, bool strict) const { - typedef std::hash_set node_set; + typedef std::unordered_set 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 -#include #include #include @@ -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 #include -#include +#include #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 NodeValuePool; - typedef __gnu_cxx::hash_set NodeValueIDSet; + typedef std::unordered_set NodeValuePool; + typedef std::unordered_set 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 #include #include #include #include -#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()(t.getField()); } };/* struct RecordSelectHashFunction */ struct CVC4_PUBLIC RecordUpdateHashFunction { inline size_t operator()(const RecordUpdate& t) const { - return StringHashFunction()(t.getField()); + return std::hash()(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(d_context)), - d_typeMap(new(true) CDHashMap, Type>, StringHashFunction>(d_context)), + d_exprMap(new(true) CDHashMap(d_context)), + d_typeMap(new(true) CDHashMap, Type>>(d_context)), d_functions(new(true) CDHashSet(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::iterator found = + CDHashMap::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 #include -#include #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 *d_exprMap; + context::CDHashMap* d_exprMap; /** A map for types. */ - context::CDHashMap, Type>, StringHashFunction> *d_typeMap; + context::CDHashMap, Type> >* + d_typeMap; /** A set of defined functions. */ context::CDHashSet *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& cache) const { + std::unordered_map& cache) const { // in cache? - std::hash_map::const_iterator i = cache.find(*this); + std::unordered_map::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 -#include -#include #include +#include +#include +#include +#include + #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& cache) const; + std::unordered_map& cache) const; /** * Cache-aware, recursive version of substitute() used by the public @@ -102,7 +104,7 @@ private: template TypeNode substitute(Iterator1 typesBegin, Iterator1 typesEnd, Iterator2 replacementsBegin, Iterator2 replacementsEnd, - std::hash_map& cache) const; + std::unordered_map& cache) const; public: @@ -670,8 +672,6 @@ typedef TypeNode::HashFunction TypeNodeHashFunction; }/* CVC4 namespace */ -#include - #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 cache; + std::unordered_map cache; return substitute(type, replacement, cache); } @@ -697,7 +697,7 @@ TypeNode::substitute(Iterator1 typesBegin, Iterator1 typesEnd, Iterator2 replacementsBegin, Iterator2 replacementsEnd) const { - std::hash_map cache; + std::unordered_map 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& cache) const { + std::unordered_map& cache) const { // in cache? - std::hash_map::const_iterator i = cache.find(*this); + std::unordered_map::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 + #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 d_variables; + std::unordered_map d_variables; /** * A map Type -> Type, intended to be used for a mapping of types * between two ExprManagers. */ - std::hash_map d_types; + std::unordered_map d_types; public: Expr& operator[](Expr e) { return d_variables[e]; } @@ -49,7 +50,7 @@ public: };/* class VariableTypeMap */ -typedef __gnu_cxx::hash_map VarMap; +typedef std::unordered_map 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 -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 Smt1::newLogicMap() { - std::hash_map logicMap; +std::unordered_map Smt1::newLogicMap() { + std::unordered_map logicMap; logicMap["AUFLIA"] = AUFLIA; logicMap["AUFLIRA"] = AUFLIRA; logicMap["AUFNIRA"] = AUFNIRA; @@ -68,7 +64,7 @@ std::hash_map Smt1::ne } Smt1::Logic Smt1::toLogic(const std::string& name) { - static std::hash_map logicMap = newLogicMap(); + static std::unordered_map 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 -namespace std { using namespace __gnu_cxx; } +#include +#include -#include "util/hash.h" #include "parser/parser.h" namespace CVC4 { @@ -117,7 +116,7 @@ public: private: void addArithmeticOperators(); - static std::hash_map newLogicMap(); + static std::unordered_map newLogicMap(); };/* class Smt1 */ }/* CVC4::parser namespace */ diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index a2c859055..c7156635d 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -117,6 +117,7 @@ namespace CVC4 { #include #include #include +#include #include #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& free, std::hash_set& closedCache) { +static bool isClosed(const Expr& e, std::set& free, std::unordered_set& closedCache) { if(closedCache.find(e) != closedCache.end()) { return true; } @@ -181,7 +182,7 @@ static bool isClosed(const Expr& e, std::set& free, std::hash_set& free) { - std::hash_set cache; + std::unordered_set cache; return isClosed(e, free, cache); } @@ -1798,7 +1799,7 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2] Expr attexpr; std::vector patexprs; std::vector patconds; - std::hash_set names; + std::unordered_set names; std::vector< std::pair > binders; Type type; std::string s; 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 #include #include +#include #include #include "parser/parser.h" @@ -58,7 +59,7 @@ public: private: bool d_logicSet; LogicInfo d_logic; - std::hash_map operatorKindMap; + std::unordered_map operatorKindMap; std::pair d_lastNamedTerm; // this is a user-context stack std::stack< std::map > 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 -#include +#include +#include #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 d_r_converted; - std::hash_map d_distinct_objects; + std::unordered_set d_r_converted; + std::unordered_map 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 +#include +#include + #include "expr/node.h" #include "util/hash.h" -#include -#include - namespace CVC4 { namespace context { @@ -65,7 +66,7 @@ class DagificationVisitor { /** * A map of subexprs to their occurrence count. */ - std::hash_map d_nodeCount; + std::unordered_map 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 d_uniqueParent; + std::unordered_map 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 + #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 TypeSet; +typedef std::unordered_set 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 + #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 TypeSet; +typedef std::unordered_set 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 -#include -#include #include #include #include +#include +#include #include #include "expr/expr.h" @@ -56,11 +55,11 @@ typedef TSatProof< CVC4::BVMinisat::Solver> BVSatProof; template class LFSCSatProof; typedef LFSCSatProof< CVC4::BVMinisat::Solver> LFSCBVSatProof; -typedef __gnu_cxx::hash_set ExprSet; -typedef __gnu_cxx::hash_map ExprToClauseId; -typedef __gnu_cxx::hash_map ExprToId; -typedef __gnu_cxx::hash_map ExprToExpr; -typedef __gnu_cxx::hash_map ExprToString; +typedef std::unordered_set ExprSet; +typedef std::unordered_map ExprToClauseId; +typedef std::unordered_map ExprToId; +typedef std::unordered_map ExprToExpr; +typedef std::unordered_map 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 -#include #include +#include +#include #include "context/cdhashmap.h" #include "proof/clause_id.h" @@ -38,9 +38,9 @@ namespace prop { class CnfProof; -typedef __gnu_cxx::hash_map SatVarToExpr; -typedef __gnu_cxx::hash_map NodeToNode; -typedef __gnu_cxx::hash_set ClauseIdSet; +typedef std::unordered_map SatVarToExpr; +typedef std::unordered_map NodeToNode; +typedef std::unordered_set ClauseIdSet; typedef context::CDHashMap ClauseIdToNode; typedef context::CDHashMap 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 -#include +#include +#include + #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 ExprSet; +typedef std::unordered_map IdToSatClause; typedef context::CDHashSet CDExprSet; -typedef __gnu_cxx::hash_set NodeSet; -typedef __gnu_cxx::hash_map, NodeHashFunction > NodeToNodes; -typedef context::CDHashMap, NodeHashFunction > CDNodeToNodes; -typedef std::hash_set IdHashSet; +typedef std::unordered_map, NodeHashFunction> NodeToNodes; +typedef context::CDHashMap, NodeHashFunction> CDNodeToNodes; +typedef std::unordered_set 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 + #include "theory/output_channel.h" namespace CVC4 { @@ -42,7 +44,7 @@ public: class MyPreRegisterVisitor { theory::Theory* d_theory; - __gnu_cxx::hash_set d_visited; + std::unordered_set 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 -#include #include +#include +#include + #include "expr/node_manager.h" namespace CVC4 { -typedef __gnu_cxx::hash_set ExprSet; -typedef __gnu_cxx::hash_set NodeSet; +typedef std::unordered_set ExprSet; +typedef std::unordered_set NodeSet; typedef std::pair NodePair; typedef std::set 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 -#include -#include #include #include #include +#include #include #include "context/cdhashmap.h" @@ -101,18 +100,18 @@ class TSatProof { typedef std::set LitSet; typedef std::set VarSet; - typedef std::hash_map IdCRefMap; - typedef std::hash_map ClauseIdMap; + typedef std::unordered_map IdCRefMap; + typedef std::unordered_map ClauseIdMap; typedef context::CDHashMap IdUnitMap; typedef context::CDHashMap UnitIdMap; typedef context::CDHashMap IdResMap; - typedef std::hash_map IdProofRuleMap; + typedef std::unordered_map IdProofRuleMap; typedef std::vector ResStack; typedef std::set IdSet; typedef std::vector LitVector; - typedef __gnu_cxx::hash_map + typedef std::unordered_map IdToMinisatClause; - typedef __gnu_cxx::hash_map IdToConflicts; + typedef std::unordered_map IdToConflicts; public: TSatProof(Solver* solver, context::Context* context, @@ -362,7 +361,7 @@ class TSatProof { IdToSatClause d_seenLemmas; private: - __gnu_cxx::hash_map d_glueMap; + std::unordered_map 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::const_iterator SkolemizationManager::begin() { +std::unordered_map::const_iterator SkolemizationManager::begin() { return d_disequalityToSkolem.begin(); } -std::hash_map::const_iterator SkolemizationManager::end() { +std::unordered_map::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 -#include +#include + #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::const_iterator begin(); - std::hash_map::const_iterator end(); + std::unordered_map::const_iterator begin(); + std::unordered_map::const_iterator end(); private: - std::hash_map d_disequalityToSkolem; - std::hash_map d_skolemToDisequality; + std::unordered_map d_disequalityToSkolem; + std::unordered_map 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 #include +#include +#include #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 ExprSet; +typedef std::unordered_set ExprSet; typedef std::map TheoryProofTable; typedef std::set 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 + #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 TypeSet; +typedef std::unordered_set 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 cl_levels; + std::unordered_set 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 #include #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 - #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 #include +#include #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 cl_levels; + std::unordered_set 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 +#include #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 d_shared; + std::unordered_set 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 837968aa2..704303826 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -18,7 +18,8 @@ #include #include -#include +#include +#include #include #include #include @@ -463,8 +464,8 @@ class PrintSuccessListener : public Listener { class SmtEnginePrivate : public NodeManagerListener { SmtEngine& d_smt; - typedef hash_map NodeToNodeHashMap; - typedef hash_map NodeToBoolHashMap; + typedef unordered_map NodeToNodeHashMap; + typedef unordered_map NodeToBoolHashMap; /** * Manager for limiting time and abstract resource usage. @@ -634,7 +635,7 @@ private: * conjuncts. */ size_t removeFromConjunction(Node& n, - const std::hash_set& toRemove); + const std::unordered_set& toRemove); /** Scrub miplib encodings. */ void doMiplibTrick(); @@ -2255,7 +2256,7 @@ bool SmtEngine::isDefinedFunction( Expr func ){ return d_definedFunctions->find(nf) != d_definedFunctions->end(); } -Node SmtEnginePrivate::expandDefinitions(TNode n, hash_map& cache, bool expandOnly) +Node SmtEnginePrivate::expandDefinitions(TNode n, unordered_map& cache, bool expandOnly) throw(TypeCheckingException, LogicException, UnsafeInterruptException) { stack< triple > worklist; @@ -2295,7 +2296,7 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, hash_map::iterator cacheHit = cache.find(n); + unordered_map::iterator cacheHit = cache.find(n); if(cacheHit != cache.end()) { TNode ret = (*cacheHit).second; result.push(ret.isNull() ? n : ret); @@ -2427,7 +2428,7 @@ struct intToBV_stack_element { : node(node), children_added(false) {} };/* struct intToBV_stack_element */ -typedef std::hash_map NodeMap; +typedef std::unordered_map NodeMap; Node SmtEnginePrivate::intToBVMakeBinary(TNode n, NodeMap& cache) { // Do a topological sort of the subexpressions and substitute them @@ -3031,7 +3032,7 @@ bool SmtEnginePrivate::nonClausalSimplify() { Trace("simplify") << "Resize non-clausal learned literals to " << j << std::endl; d_nonClausalLearnedLiterals.resize(j); - hash_set s; + unordered_set s; Trace("debugging") << "NonClausal simplify pre-preprocess\n"; for (unsigned i = 0; i < d_assertions.size(); ++ i) { Node assertion = d_assertions[i]; @@ -3266,7 +3267,7 @@ void SmtEnginePrivate::traceBackToAssertions(const std::vector& nodes, std } } -size_t SmtEnginePrivate::removeFromConjunction(Node& n, const std::hash_set& toRemove) { +size_t SmtEnginePrivate::removeFromConjunction(Node& n, const std::unordered_set& toRemove) { Assert(n.getKind() == kind::AND); size_t removals = 0; for(Node::iterator j = n.begin(); j != n.end(); ++j) { @@ -3320,12 +3321,12 @@ void SmtEnginePrivate::doMiplibTrick() { Assert(!options::incrementalSolving()); const booleans::CircuitPropagator::BackEdgesMap& backEdges = d_propagator.getBackEdges(); - hash_set removeAssertions; + unordered_set removeAssertions; NodeManager* nm = NodeManager::currentNM(); Node zero = nm->mkConst(Rational(0)), one = nm->mkConst(Rational(1)); - hash_map intVars; + unordered_map intVars; for(vector::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; @@ -3819,9 +3820,9 @@ Result SmtEngine::quickCheck() { } -void SmtEnginePrivate::collectSkolems(TNode n, set& skolemSet, hash_map& cache) +void SmtEnginePrivate::collectSkolems(TNode n, set& skolemSet, unordered_map& cache) { - hash_map::iterator it; + unordered_map::iterator it; it = cache.find(n); if (it != cache.end()) { return; @@ -3845,9 +3846,9 @@ void SmtEnginePrivate::collectSkolems(TNode n, set& skolemSet, hash_map& cache) +bool SmtEnginePrivate::checkForBadSkolems(TNode n, TNode skolem, unordered_map& cache) { - hash_map::iterator it; + unordered_map::iterator it; it = cache.find(n); if (it != cache.end()) { return (*it).second; @@ -3918,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 cache; + unordered_map cache; for(unsigned i = 0; i < d_assertions.size(); ++ i) { d_assertions.replace(i, expandDefinitions(d_assertions[i], cache)); } @@ -3937,8 +3938,8 @@ void SmtEnginePrivate::processAssertions() { Debug("smt") << " d_assertions : " << d_assertions.size() << endl; if( options::nlExtPurify() ){ - hash_map cache; - hash_map bcache; + unordered_map cache; + unordered_map 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)); @@ -3959,7 +3960,7 @@ void SmtEnginePrivate::processAssertions() { if (options::solveRealAsInt()) { Chat() << "converting reals to ints..." << endl; - hash_map cache; + unordered_map 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)); @@ -3975,7 +3976,7 @@ void SmtEnginePrivate::processAssertions() { if (options::solveIntAsBV() > 0) { Chat() << "converting ints to bit-vectors..." << endl; - hash_map cache; + unordered_map cache; for(unsigned i = 0; i < d_assertions.size(); ++ i) { d_assertions.replace(i, intToBV(d_assertions[i], cache)); } @@ -4203,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 cache; + unordered_map cache; // First, find all skolems that appear in the substitution map - their associated iteExpr will need // to be moved to the main assertion set @@ -4656,7 +4657,7 @@ Expr SmtEngine::expandDefinitions(const Expr& ex) throw(TypeCheckingException, L if(Dump.isOn("benchmark")) { Dump("benchmark") << ExpandDefinitionsCommand(e); } - hash_map cache; + unordered_map cache; Node n = d_private->expandDefinitions(Node::fromExpr(e), cache, /* expandOnly = */ true); n = postprocess(n, TypeNode::fromType(e.getType())); @@ -4701,7 +4702,7 @@ Expr SmtEngine::getValue(const Expr& ex) const throw(ModalException, TypeCheckin TypeNode expectedType = n.getType(); // Expand, then normalize - hash_map cache; + unordered_map 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 @@ -4814,7 +4815,7 @@ CVC4::SExpr SmtEngine::getAssignment() { Trace("smt") << "--- getting value of " << *i << endl; // Expand, then normalize - hash_map cache; + unordered_map cache; Node n = d_private->expandDefinitions(*i, cache); n = Rewriter::rewrite(n); @@ -5056,7 +5057,7 @@ void SmtEngine::checkModel(bool hardFailure) { // Apply any define-funs from the problem. { - hash_map cache; + unordered_map cache; n = d_private->expandDefinitions(n, cache); } Notice() << "SmtEngine::checkModel(): -- expands to " << n << endl; 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 #include #include "context/cdinsert_hashmap.h" @@ -33,7 +34,7 @@ namespace theory { class ContainsTermITEVisitor; }/* CVC4::theory namespace */ -typedef std::hash_map IteSkolemMap; +typedef std::unordered_map IteSkolemMap; class RemoveTermFormulas { typedef context::CDInsertHashMap< std::pair, Node, PairHashFunction > 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 #include + #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 NodeMap; + typedef std::unordered_map 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 + #include "expr/node.h" -#include -#include #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 NodeMap; + typedef std::unordered_map 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 NodeIntegerMap; + typedef std::unordered_map 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 +#include +#include #include #include "context/cdhashset.h" @@ -35,12 +36,12 @@ namespace theory { namespace arith { //Sets of Nodes -typedef __gnu_cxx::hash_set NodeSet; -typedef __gnu_cxx::hash_set TNodeSet; +typedef std::unordered_set NodeSet; +typedef std::unordered_set TNodeSet; typedef context::CDHashSet CDNodeSet; //Maps from Nodes -> ArithVars, and vice versa -typedef __gnu_cxx::hash_map NodeToArithVarMap; +typedef std::unordered_map NodeToArithVarMap; typedef DenseMap 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 #include +#include +#include #include "base/output.h" #include "proof/proof.h" @@ -1333,7 +1334,7 @@ struct ConstraintCPHash { }; void Constraint::assertionFringe(ConstraintCPVec& v){ - hash_set visited; + unordered_set 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 +#include #include #include #include @@ -145,7 +145,7 @@ enum ConstraintType {LowerBound, Equality, UpperBound, Disequality}; typedef context::CDList CDConstraintList; -typedef __gnu_cxx::hash_map NodetoConstraintMap; +typedef std::unordered_map NodetoConstraintMap; typedef size_t ConstraintRuleID; static const ConstraintRuleID ConstraintRuleIdSentinel = std::numeric_limits::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 +#include #include #include #include @@ -179,7 +179,7 @@ private: int d_upId; public: - typedef __gnu_cxx::hash_map RowIdMap; + typedef std::unordered_map 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 gcdMap; + std::unordered_map gcdMap; std::deque::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 #include #include @@ -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 NodeToInputConstraintIndexMap; + typedef std::unordered_map 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 +#include #include #include "context/cdhashmap.h" @@ -43,7 +43,7 @@ private: CDNode2PairMap d_pbBounds; SubstitutionMap d_subCache; - typedef __gnu_cxx::hash_set NodeSet; + typedef std::unordered_set NodeSet; NodeSet d_learningCache; context::CDO 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 + #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, ArithVarVec, ArithVarIntPairHashFunc> sgn_table; + typedef std::unordered_map< std::pair, 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 shared = d_containing.currentlySharedTerms(); + std::unordered_set 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 -#include #include #include +#include #include "context/backtrackable.h" #include "context/cdlist.h" @@ -92,7 +91,7 @@ public: };/* class Info */ -typedef __gnu_cxx::hash_map CNodeInfoMap; +typedef std::unordered_map 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 #include -#include +#include #include "expr/node.h" @@ -33,7 +33,7 @@ namespace arrays { class StaticFactManager { /** Our underlying map type. */ - typedef __gnu_cxx::hash_map MapType; + typedef std::unordered_map 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 marked; + std::unordered_set marked; vector index_trail; vector::iterator it, iend; Node equivalence_trail = reason; @@ -1198,7 +1198,7 @@ void TheoryArrays::collectModelInfo( TheoryModel* m ) /* } else { - std::hash_map::iterator it = d_skolemCache.find(n); + std::unordered_map::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::iterator it = d_skolemCache.find(ref); + std::unordered_map::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 + #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 CNodeNListMap; + typedef std::unordered_map CNodeNListMap; CNodeNListMap d_constReads; context::CDList d_reads; context::CDList d_constReadsList; @@ -408,7 +410,7 @@ class TheoryArrays : public Theory { };/* class ContextPopper */ ContextPopper d_contextPopper; - std::hash_map d_skolemCache; + std::unordered_map d_skolemCache; context::CDO d_skolemIndex; std::vector d_skolemAssertions; @@ -425,7 +427,7 @@ class TheoryArrays : public Theory { typedef context::CDHashMap DefValMap; DefValMap d_defValues; - typedef std::hash_map, CTNodeList*, TNodePairHashFunction> ReadBucketMap; + typedef std::unordered_map, CTNodeList*, TNodePairHashFunction> ReadBucketMap; ReadBucketMap d_readBucketTable; context::Context* d_readTableContext; context::CDList 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 +#include + #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 indexSet; - std::hash_map elementsMap; - std::hash_map::iterator it; + std::unordered_set indexSet; + std::unordered_map elementsMap; + std::unordered_map::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 #include -#include +#include #include "expr/node.h" #include "context/cdo.h" @@ -41,7 +41,7 @@ namespace arrays { template class UnionFind : context::ContextNotifyObj { /** Our underlying map type. */ - typedef __gnu_cxx::hash_map MapType; + typedef std::unordered_map 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 #include +#include +#include #include "theory/theory.h" #include "context/context.h" @@ -64,7 +65,7 @@ public: else return ASSIGNED_TO_TRUE; } - typedef std::hash_map, NodeHashFunction> BackEdgesMap; + typedef std::unordered_map, 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 +#include + #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 node_set; + typedef std::unordered_set 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 -#include +#include +#include #include "expr/node.h" #include "theory/substitutions.h" @@ -64,10 +64,10 @@ class AbstractionModule { }; class ArgsTable { - __gnu_cxx::hash_map d_data; + std::unordered_map d_data; bool hasEntry(TNode signature) const; public: - typedef __gnu_cxx::hash_map::iterator iterator; + typedef std::unordered_map::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, NodeHashFunction> NodeVecMap; - typedef __gnu_cxx::hash_map NodeTNodeMap; - typedef __gnu_cxx::hash_map TNodeTNodeMap; - typedef __gnu_cxx::hash_map NodeNodeMap; - typedef __gnu_cxx::hash_map TNodeNodeMap; - typedef __gnu_cxx::hash_set TNodeSet; - typedef __gnu_cxx::hash_map IntNodeMap; - typedef __gnu_cxx::hash_map IndexMap; - typedef __gnu_cxx::hash_map > SkolemMap; - typedef __gnu_cxx::hash_map SignatureMap; + typedef std::unordered_map, NodeHashFunction> NodeVecMap; + typedef std::unordered_map NodeTNodeMap; + typedef std::unordered_map TNodeTNodeMap; + typedef std::unordered_map NodeNodeMap; + typedef std::unordered_map TNodeNodeMap; + typedef std::unordered_set TNodeSet; + typedef std::unordered_map IntNodeMap; + typedef std::unordered_map IndexMap; + typedef std::unordered_map > SkolemMap; + typedef std::unordered_map 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 +#include +#include #include #include "bitblast_strategies_template.h" @@ -58,8 +59,8 @@ namespace bv { class BitblastingRegistrar; -typedef __gnu_cxx::hash_set NodeSet; -typedef __gnu_cxx::hash_set TNodeSet; +typedef std::unordered_set NodeSet; +typedef std::unordered_set TNodeSet; class AbstractionModule; @@ -73,9 +74,9 @@ template class TBitblaster { protected: typedef std::vector Bits; - typedef __gnu_cxx::hash_map TermDefMap; - typedef __gnu_cxx::hash_set TNodeSet; - typedef __gnu_cxx::hash_map ModelCache; + typedef std::unordered_map TermDefMap; + typedef std::unordered_set TNodeSet; + typedef std::unordered_map ModelCache; typedef void (*TermBBStrategy) (TNode, Bits&, TBitblaster*); typedef T (*AtomBBStrategy) (TNode, TBitblaster*); @@ -258,7 +259,7 @@ public: class EagerBitblaster : public TBitblaster { - typedef __gnu_cxx::hash_set TNodeSet; + typedef std::unordered_set 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 { - typedef std::hash_map TNodeAigMap; - typedef std::hash_map NodeAigMap; + typedef std::unordered_map TNodeAigMap; + typedef std::unordered_map 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 +#include + #include "expr/node.h" #include "theory/theory_model.h" #include "theory/bv/theory_bv.h" -#include -#pragma once - namespace CVC4 { namespace theory { @@ -33,7 +36,7 @@ class AigBitblaster; * BitblastSolver */ class EagerBitblastSolver { - typedef __gnu_cxx::hash_set AssertionSet; + typedef std::unordered_set 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 +#include +#include +#include + #include "context/cdqueue.h" -#include "theory/uf/equality_engine.h" +#include "context/context.h" #include "theory/theory.h" -#include -#include +#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 ReasonToIdMap; - typedef __gnu_cxx::hash_map TermNodeToIdMap; + typedef std::unordered_map ReasonToIdMap; + typedef std::unordered_map TermNodeToIdMap; typedef std::vector Edges; - typedef __gnu_cxx::hash_set TermIdSet; + typedef std::unordered_set TermIdSet; typedef std::priority_queue, QueueComparator> BFSQueue; - typedef __gnu_cxx::hash_set TNodeSet; - typedef __gnu_cxx::hash_set NodeSet; + typedef std::unordered_set TNodeSet; + typedef std::unordered_set NodeSet; std::vector 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 -#include +#include #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::const_iterator vars_iterator; + typedef std::unordered_set::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 +#include + #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 Substitutions; - typedef __gnu_cxx::hash_map SubstitutionsCache; + typedef std::unordered_map Substitutions; + typedef std::unordered_map SubstitutionsCache; Substitutions d_substitutions; SubstitutionsCache d_cache; @@ -104,9 +108,9 @@ struct WorklistElement { }; -typedef __gnu_cxx::hash_map NodeNodeMap; -typedef __gnu_cxx::hash_map NodeIdMap; -typedef __gnu_cxx::hash_set TNodeSet; +typedef std::unordered_map NodeNodeMap; +typedef std::unordered_map NodeIdMap; +typedef std::unordered_set TNodeSet; class ExtractSkolemizer { @@ -123,7 +127,7 @@ class ExtractSkolemizer { ExtractList() : base(1), extracts() {} void addExtract(Extract& e); }; - typedef __gnu_cxx::hash_map VarExtractMap; + typedef std::unordered_map 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 + #include "theory/bv/bitblaster_template.h" #include "theory/bv/bv_subtheory.h" @@ -47,7 +49,7 @@ class BitblastSolver : public SubtheorySolver { context::CDQueue d_bitblastQueue; Statistics d_statistics; - typedef std::hash_map NodeMap; + typedef std::unordered_map NodeMap; NodeMap d_modelCache; context::CDO 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 +#include + #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 ModelValue; - typedef __gnu_cxx::hash_map TNodeBoolMap; - typedef __gnu_cxx::hash_set TNodeSet; + typedef std::unordered_map ModelValue; + typedef std::unordered_map TNodeBoolMap; + typedef std::unordered_set 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 + #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 d_explanations; context::CDO d_isComplete; - typedef __gnu_cxx::hash_set NodeSet; + typedef std::unordered_set 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 + #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 NodeNodeMap; +typedef std::unordered_map 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 -#include +#include #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& assertionsToPreprocess); private: - typedef __gnu_cxx::hash_map NodeMap; + typedef std::unordered_map 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 #include -#include +#include #include "expr/node.h" #include "theory/bv/theory_bv_utils.h" @@ -79,7 +79,7 @@ public: * UnionFind * */ -typedef __gnu_cxx::hash_set TermSet; +typedef std::unordered_set TermSet; typedef std::vector Decomposition; struct ExtractTerm { @@ -226,9 +226,9 @@ public: }; class Slicer { - __gnu_cxx::hash_map d_idToNode; - __gnu_cxx::hash_map d_nodeToId; - __gnu_cxx::hash_map d_coreTermCache; + std::unordered_map d_idToNode; + std::unordered_map d_nodeToId; + std::unordered_map 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 +#include + #include "context/cdhashset.h" #include "context/cdlist.h" #include "context/context.h" @@ -51,7 +54,7 @@ class TheoryBV : public Theory { context::CDHashSet d_sharedTermsSet; std::vector d_subtheories; - __gnu_cxx::hash_map > d_subtheoryMap; + std::unordered_map > d_subtheoryMap; public: @@ -129,22 +132,22 @@ private: */ Node getBVDivByZero(Kind k, unsigned width); - typedef __gnu_cxx::hash_set TNodeSet; + typedef std::unordered_set TNodeSet; void collectFunctionSymbols(TNode term, TNodeSet& seen); void storeFunction(TNode func, TNode term); - typedef __gnu_cxx::hash_set NodeSet; + typedef std::unordered_set NodeSet; NodeSet d_staticLearnCache; /** * Maps from bit-vector width to division-by-zero uninterpreted * function symbols. */ - __gnu_cxx::hash_map d_BVDivByZero; - __gnu_cxx::hash_map d_BVRemByZero; + std::unordered_map d_BVDivByZero; + std::unordered_map d_BVRemByZero; - typedef __gnu_cxx::hash_map FunctionToArgs; - typedef __gnu_cxx::hash_map NodeToNode; + typedef std::unordered_map FunctionToArgs; + typedef std::unordered_map 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 +#include + #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& map, TNode node, bool neg) { +inline static void insert(std::unordered_map& 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::apply(TNode node) { Debug("bv-rewrite") << "RewriteRule(" << node << ")" << std::endl; // this will remove duplicates - std::hash_map subterms; + std::unordered_map subterms; unsigned size = utils::getSize(node); BitVector constant = utils::mkBitVectorOnes(size); @@ -974,7 +977,7 @@ Node RewriteRule::apply(TNode node) { children.push_back(utils::mkConst(constant)); } - std::hash_map::const_iterator it = subterms.begin(); + std::unordered_map::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::apply(TNode node) { Debug("bv-rewrite") << "RewriteRule(" << node << ")" << std::endl; std::vector processingStack; processingStack.push_back(node); - __gnu_cxx::hash_set processed; + std::unordered_set processed; std::vector children; Kind kind = node.getKind(); @@ -1053,7 +1056,7 @@ Node RewriteRule::apply(TNode node) { Debug("bv-rewrite") << "RewriteRule(" << node << ")" << std::endl; // this will remove duplicates - std::hash_map subterms; + std::unordered_map subterms; unsigned size = utils::getSize(node); BitVector constant(size, (unsigned)0); @@ -1082,7 +1085,7 @@ Node RewriteRule::apply(TNode node) { children.push_back(utils::mkConst(constant)); } - std::hash_map::const_iterator it = subterms.begin(); + std::unordered_map::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::apply(TNode node) { Debug("bv-rewrite") << "RewriteRule(" << node << ")" << std::endl; - std::hash_map subterms; + std::unordered_map subterms; unsigned size = utils::getSize(node); BitVector constant; bool const_set = false; @@ -1144,7 +1147,7 @@ Node RewriteRule::apply(TNode node) { std::vector children; - std::hash_map::const_iterator it = subterms.begin(); + std::unordered_map::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 -#include #include +#include +#include +#include + #include "expr/node_manager.h" namespace CVC4 { namespace theory { namespace bv { -typedef __gnu_cxx::hash_set NodeSet; -typedef __gnu_cxx::hash_set TNodeSet; +typedef std::unordered_set NodeSet; +typedef std::unordered_set TNodeSet; namespace utils { @@ -505,11 +508,11 @@ inline T gcd(T a, T b) { return a; } -typedef __gnu_cxx::hash_map TNodeBoolMap; +typedef std::unordered_map TNodeBoolMap; bool isCoreTerm(TNode term, TNodeBoolMap& cache); bool isEqualityTerm(TNode term, TNodeBoolMap& cache); -typedef __gnu_cxx::hash_set NodeSet; +typedef std::unordered_set 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 #include #include 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::iterator it; + unordered_map::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::iterator it; + std::unordered_map::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 NodeSet; +typedef std::unordered_set 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 -#include +#include #include #include "expr/node.h" @@ -80,7 +79,7 @@ public: size_t cache_size() const { return d_cache.size(); } private: - typedef std::hash_map NodeBoolMap; + typedef std::unordered_map NodeBoolMap; NodeBoolMap d_cache; }; @@ -100,7 +99,7 @@ public: } void clear(); private: - typedef std::hash_map NodeCountMap; + typedef std::unordered_map NodeCountMap; NodeCountMap d_reachCount; bool d_skipVariables; @@ -131,7 +130,7 @@ public: size_t cache_size() const; private: - typedef std::hash_map NodeCountMap; + typedef std::unordered_map NodeCountMap; NodeCountMap d_termITEHeight; }; /* class TermITEHeightCounter */ @@ -158,7 +157,7 @@ private: std::vector* d_assertions; IncomingArcCounter d_incoming; - typedef std::hash_map NodeMap; + typedef std::unordered_map NodeMap; NodeMap d_compressed; void reset(); @@ -206,7 +205,7 @@ private: // constant // or termITE(cnd, ConstantIte, ConstantIte) typedef std::vector NodeVec; - typedef std::hash_map ConstantLeavesMap; + typedef std::unordered_map ConstantLeavesMap; ConstantLeavesMap d_constantLeaves; // d_constantLeaves satisfies the following invariants: @@ -249,23 +248,23 @@ private: return hash; } };/* struct ITESimplifier::NodePairHashFunction */ - typedef std::hash_map NodePairMap; + typedef std::unordered_map 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 d_leavesConstCache; + std::unordered_map 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 d_simpVars; + std::unordered_map d_simpVars; Node getSimpVar(TypeNode t); - typedef std::hash_map NodeMap; + typedef std::unordered_map 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 TNodeMap; + typedef std::unordered_map TNodeMap; class CareSetPtr; class CareSetPtrVal { 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 #include #include #include 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 #include #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 #include #include +#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 +#include + #include "expr/attribute.h" #include "theory/theory.h" #include "theory/type_enumerator.h" #include "theory/quantifiers/quant_util.h" -#include 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 -#include -#include - #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 cache; + std::unordered_map 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& cache ){ +Node EqualityQueryQuantifiersEngine::getInstance( Node n, const std::vector< Node >& eqc, std::unordered_map& 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 #include #include +#include #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& cache ); + Node getInstance( Node n, const std::vector< Node >& eqc, std::unordered_map& 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*) s_rewriteStack = NULL; +static CVC4_THREADLOCAL(std::unordered_set*) 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(); + s_rewriteStack = new std::unordered_set(); } #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 > element_map; + std::unordered_set< Node, NodeHashFunction > sets; + std::map< Node, std::unordered_set > 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 seen; + std::unordered_set 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& hasSeen, - std::map< Node, std::hash_set< Node, NodeHashFunction > >& tc_graph, bool& isReachable ) { + void TheorySetsRels::isTCReachable( Node start, Node dest, std::unordered_set& 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 > rel_tc_graph; + std::map< Node, std::unordered_set > 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 >::iterator rel_tc_graph_it = rel_tc_graph.find( fst_element_rep ); + std::map< Node, std::unordered_set >::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 > rel_tc_graph, std::map< Node, Node > rel_tc_graph_exps, Node tc_rel ) { + void TheorySetsRels::doTCInference( std::map< Node, std::unordered_set > 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 seen; + std::unordered_set 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 + #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 > 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 > > 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 > > d_rRep_tcGraph; - std::map< Node, std::map< Node, std::hash_set > > d_tcr_tcGraph; + std::map< Node, std::map< Node, std::unordered_set > > d_rRep_tcGraph; + std::map< Node, std::map< Node, std::unordered_set > > 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 > 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 > 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& hasSeen, - std::map< Node, std::hash_set< Node, NodeHashFunction > >& tc_graph, bool& isReachable ); + void isTCReachable( Node start, Node dest, std::unordered_set& 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 Elements; -typedef std::hash_map SettermElementsMap; +typedef std::unordered_map SettermElementsMap; struct FlattenedNodeTag {}; typedef expr::Attribute flattened; @@ -50,7 +50,7 @@ RewriteResponse flattenNode(TNode n, TNode trivialNode, TNode skipNode) return RewriteResponse(REWRITE_DONE, n); } - typedef std::hash_set node_set; + typedef std::unordered_set 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 + #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 SharedTermsMap; + typedef std::unordered_map 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 #include #include -#include +#include #include "expr/node.h" #include "context/context.h" @@ -51,7 +52,7 @@ public: private: - typedef std::hash_map NodeCache; + typedef std::unordered_map 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 +#include namespace CVC4 { @@ -105,7 +105,7 @@ class SharedTermsVisitor { /** * Cache from preprocessing of atoms. */ - typedef std::hash_map TNodeVisitedMap; + typedef std::unordered_map 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 Theory::currentlySharedTerms() const{ - std::hash_set currentlyShared; +std::unordered_set Theory::currentlySharedTerms() const{ + std::unordered_set 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 #include #include #include #include +#include #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 currentlySharedTerms() const; + std::unordered_set 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 d_atoms; - std::hash_set d_visited; + std::unordered_set 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 #include +#include #include #include @@ -189,8 +190,8 @@ class TheoryEngine { theory::TheoryEngineModelBuilder* d_curr_model_builder; bool d_aloc_curr_model_builder; - typedef std::hash_map NodeMap; - typedef std::hash_map TNodeMap; + typedef std::unordered_map NodeMap; + typedef std::unordered_map 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::iterator it = d_modelCache.find(n); + std::unordered_map::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 +#include + #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 d_modelCache; + mutable std::unordered_map 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*, TypeNodeHashFunction> TypeSetMap; - typedef std::hash_map TypeToTypeEnumMap; + typedef std::unordered_map*, TypeNodeHashFunction> TypeSetMap; + typedef std::unordered_map 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 NodeMap; + typedef std::unordered_map NodeMap; NodeMap d_normalizedCache; - typedef std::hash_set NodeSet; + typedef std::unordered_set 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 -#include #include +#include #include #include "base/output.h" @@ -234,10 +234,10 @@ private: std::map d_pathReconstructionTriggers; /** Map from nodes to their ids */ - __gnu_cxx::hash_map d_nodeIds; + std::unordered_map d_nodeIds; /** Map from function applications to their ids */ - typedef __gnu_cxx::hash_map ApplicationIdsMap; + typedef std::unordered_map 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 d_nodeIndividualTrigger; - typedef std::hash_map DisequalityReasonsMap; + typedef std::unordered_map 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::iterator i = d_reps.find(n); + unordered_map::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, TNodeHashFunction>& ps = t.partitions(); - for(hash_map, TNodeHashFunction>::iterator i = ps.begin(); + unordered_map, TNodeHashFunction>& ps = t.partitions(); + for(unordered_map, 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, TNodeHashFunction>& ps = d_template.partitions(); + unordered_map, TNodeHashFunction>& ps = d_template.partitions(); Debug("ufsymm") << "UFSYMM hit a bad match---have " << ps.size() << " partitions:" << endl; - for(hash_map, TNodeHashFunction>::iterator i = ps.begin(); + for(unordered_map, 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 #include +#include #include #include "context/cdlist.h" @@ -64,8 +65,8 @@ class SymmetryBreaker : public context::ContextNotifyObj { class Template { Node d_template; NodeBuilder<> d_assertions; - std::hash_map, TNodeHashFunction> d_sets; - std::hash_map d_reps; + std::unordered_map, TNodeHashFunction> d_sets; + std::unordered_map 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, TNodeHashFunction>& partitions() { return d_sets; } + std::unordered_map, 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 Terms; typedef std::set TermEq; - typedef std::hash_map TermEqs; + typedef std::unordered_map TermEqs; private: @@ -113,7 +114,7 @@ private: Permutations d_permutations; Terms d_terms; Template d_template; - std::hash_map d_normalizationCache; + std::unordered_map 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 workList; workList.push_back(n); - __gnu_cxx::hash_set processed; + std::unordered_set 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 +#include +#include #include +#include #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 TNodeCountMap; - typedef std::hash_map TNodeMap; - typedef std::hash_set TNodeSet; + typedef std::unordered_map TNodeCountMap; + typedef std::unordered_map TNodeMap; + typedef std::unordered_set 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 #include +#include +#include +#include namespace CVC4 { @@ -33,7 +35,7 @@ namespace CVC4 { */ template > class Cache { - typedef std::hash_map Map; + typedef std::unordered_map Map; Map d_map; std::vector 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 +#include -#include -#include - -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 { };/* struct hash */ #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()(str.c_str()); - } -};/* struct StringHashFunction */ template , class HashU = std::hash > 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 -#include +#include namespace CVC4 { @@ -29,7 +29,7 @@ class Expr; class ProofLetCount; struct ExprHashFunction; -typedef __gnu_cxx::hash_map ProofLetMap; +typedef std::unordered_map ProofLetMap; class CVC4_PUBLIC Proof { public: diff --git a/src/util/regexp.cpp b/src/util/regexp.cpp index 9915d480d..c32b42bad 100644 --- a/src/util/regexp.cpp +++ b/src/util/regexp.cpp @@ -17,6 +17,7 @@ #include "util/regexp.h" +#include #include #include diff --git a/src/util/regexp.h b/src/util/regexp.h index beb0ee097..e7c8c5806 100644 --- a/src/util/regexp.h +++ b/src/util/regexp.h @@ -20,11 +20,13 @@ #ifndef __CVC4__REGEXP_H #define __CVC4__REGEXP_H -#include -#include +#include +#include +#include #include #include -#include +#include +#include #include "base/exception.h" #include "util/hash.h" @@ -333,7 +335,7 @@ namespace strings { struct CVC4_PUBLIC StringHashFunction { size_t operator()(const ::CVC4::String& s) const { - return __gnu_cxx::hash()(s.toString().c_str()); + return std::hash()(s.toString()); } };/* struct StringHashFunction */ 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 +#include + #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 elts; + unordered_set elts; for(size_t i = 0; i < 1000; ++i) { TS_ASSERT( ! te.isFinished() ); Node elt = *te++; -- 2.30.2