* 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.
# Check to see if this version/architecture of GNU C++ explicitly
-# instantiates __gnu_cxx::hash<uint64_t> or not. Some do, some don't.
+# instantiates std::hash<uint64_t> or not. Some do, some don't.
# See src/util/hash.h.
-AC_MSG_CHECKING([whether __gnu_cxx::hash<uint64_t> is already specialized])
+AC_MSG_CHECKING([whether std::hash<uint64_t> is already specialized])
AC_LANG_PUSH([C++])
AC_COMPILE_IFELSE([AC_LANG_SOURCE([
-#include <stdint.h>
-#include <ext/hash_map>
-namespace __gnu_cxx { template<> struct hash<uint64_t> {}; }])],
+#include <cstdint>
+#include <functional>
+namespace std { template<> struct hash<uint64_t> {}; }])],
[AC_MSG_RESULT([no]); CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_NEED_HASH_UINT64_T"],
[AC_MSG_RESULT([yes])])
AC_LANG_POP([C++])
#include <iostream>
#include <string>
#include <typeinfo>
+#include <unordered_map>
#include <vector>
#include "expr/expr.h"
set< Type > setTypes;
map< Type, Type > mapTypes;
map< pair<Type, Kind>, Expr > setoperators;
- hash_map< Expr, Expr, ExprHashFunction > substitutions;
+ unordered_map< Expr, Expr, ExprHashFunction > substitutions;
ostringstream sout;
ExprManager* em;
int depth;
#include <stdio.h>
#include <stdlib.h>
-/* #include <cvc4/bindings/compat/c/c_interface.h> /* use this after CVC4 is properly installed */
+// Use this after CVC4 is properly installed.
+// #include <cvc4/bindings/compat/c/c_interface.h>
#include "bindings/compat/c/c_interface.h"
int main() {
#include <iosfwd>
#include <iterator>
#include <sstream>
-#include <string>
#include "base/exception.h"
#include "base/output.h"
#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"
// ExprManager-to-ExprManager import).
static std::map<CVC4::ExprManager*, ValidityChecker*> s_validityCheckers;
-static std::hash_map<Type, Expr, CVC4::TypeHashFunction> s_typeToExpr;
-static std::hash_map<Expr, Type, CVC4::ExprHashFunction> s_exprToType;
+static std::unordered_map<Type, Expr, CVC4::TypeHashFunction> s_typeToExpr;
+static std::unordered_map<Expr, Type, CVC4::ExprHashFunction> s_exprToType;
static bool typeHasExpr(const Type& t) {
- std::hash_map<Type, Expr, CVC4::TypeHashFunction>::const_iterator i = s_typeToExpr.find(t);
+ std::unordered_map<Type, Expr, CVC4::TypeHashFunction>::const_iterator i = s_typeToExpr.find(t);
return i != s_typeToExpr.end();
}
static Expr typeToExpr(const Type& t) {
- std::hash_map<Type, Expr, CVC4::TypeHashFunction>::const_iterator i = s_typeToExpr.find(t);
+ std::unordered_map<Type, Expr, CVC4::TypeHashFunction>::const_iterator i = s_typeToExpr.find(t);
assert(i != s_typeToExpr.end());
return (*i).second;
}
static Type exprToType(const Expr& e) {
- std::hash_map<Expr, Type, CVC4::ExprHashFunction>::const_iterator i = s_exprToType.find(e);
+ std::unordered_map<Expr, Type, CVC4::ExprHashFunction>::const_iterator i = s_exprToType.find(e);
assert(i != s_exprToType.end());
return (*i).second;
}
}
Expr Expr::substExpr(const ExprHashMap<Expr>& oldToNew) const {
- const hash_map<CVC4::Expr, CVC4::Expr, CVC4::ExprHashFunction>& o2n =
- *reinterpret_cast<const hash_map<CVC4::Expr, CVC4::Expr, CVC4::ExprHashFunction>*>(&oldToNew);
+ const unordered_map<CVC4::Expr, CVC4::Expr, CVC4::ExprHashFunction>& o2n =
+ *reinterpret_cast<const unordered_map<CVC4::Expr, CVC4::Expr, CVC4::ExprHashFunction>*>(&oldToNew);
return Expr(substitute(o2n));
}
#define _cvc3__include__formula_value_h_
#include <stdlib.h>
+
#include <map>
+#include <string>
+#include <unordered_map>
#include <utility>
#include "base/exception.h"
#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"
};/* class ExprMap<T> */
template <class T>
-class CVC4_PUBLIC ExprHashMap : public std::hash_map<Expr, T, CVC4::ExprHashFunction> {
+class CVC4_PUBLIC ExprHashMap : public std::unordered_map<Expr, T, CVC4::ExprHashFunction> {
public:
void insert(Expr a, Expr b);
};/* class ExprHashMap<T> */
friend class Type; // to reach in to d_exprTypeMapRemove
- typedef std::hash_map<std::string, const CVC4::Datatype*, CVC4::StringHashFunction> ConstructorMap;
- typedef std::hash_map<std::string, std::pair<const CVC4::Datatype*, std::string>, CVC4::StringHashFunction> SelectorMap;
+ typedef std::unordered_map<std::string, const CVC4::Datatype*> ConstructorMap;
+ typedef std::unordered_map<std::string, std::pair<const CVC4::Datatype*, std::string>> SelectorMap;
ConstructorMap d_constructors;
SelectorMap d_selectors;
** 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.
#ifndef __CVC4__CONTEXT__CDHASHMAP_H
#define __CVC4__CONTEXT__CDHASHMAP_H
-#include <ext/hash_map>
+#include <functional>
#include <iterator>
+#include <unordered_map>
#include <vector>
#include "base/cvc4_assert.h"
// Auxiliary class: almost the same as CDO (see cdo.h)
-template <class Key, class Data, class HashFcn = __gnu_cxx::hash<Key> >
+template <class Key, class Data, class HashFcn = std::hash<Key> >
class CDOhash_map : public ContextObj {
friend class CDHashMap<Key, Data, HashFcn>;
class CDHashMap : public ContextObj {
typedef CDOhash_map<Key, Data, HashFcn> Element;
- typedef __gnu_cxx::hash_map<Key, Element*, HashFcn> table_type;
+ typedef std::unordered_map<Key, Element*, HashFcn> table_type;
friend class CDOhash_map<Key, Data, HashFcn>;
#ifndef __CVC4__CONTEXT__CDHASHMAP_FORWARD_H
#define __CVC4__CONTEXT__CDHASHMAP_FORWARD_H
+#include <functional>
+
/// \cond internals
-namespace __gnu_cxx {
- template <class Key> struct hash;
-}/* __gnu_cxx namespace */
namespace CVC4 {
namespace context {
- template <class Key, class Data, class HashFcn = __gnu_cxx::hash<Key> >
+ template <class Key, class Data, class HashFcn = std::hash<Key> >
class CDHashMap;
}/* CVC4::context namespace */
}/* CVC4 namespace */
#include "cvc4_private.h"
#include <deque>
-#include <ext/hash_map>
+#include <functional>
+#include <unordered_map>
#include <utility>
#include "base/cvc4_assert.h"
namespace context {
-template <class Key, class Data, class HashFcn = __gnu_cxx::hash<Key> >
+template <class Key, class Data, class HashFcn = std::hash<Key> >
class InsertHashMap {
private:
typedef std::deque<Key> KeyVec;
/** A list of the keys in the map maintained as a stack. */
KeyVec d_keys;
- typedef __gnu_cxx::hash_map<Key, Data, HashFcn> HashMap;
+ typedef std::unordered_map<Key, Data, HashFcn> HashMap;
/** The hash_map used for element lookup. */
HashMap d_hashMap;
#pragma once
-#include <ext/hash_map>
#include <deque>
+#include <functional>
+#include <unordered_map>
#include <utility>
#include "base/cvc4_assert.h"
namespace context {
-template <class Key, class Data, class HashFcn = __gnu_cxx::hash<Key> >
+template <class Key, class Data, class HashFcn = std::hash<Key> >
class TrailHashMap {
public:
/** A pair of Key and Data that mirrors hash_map::value_type. */
KDTVec d_kdts;
- typedef __gnu_cxx::hash_map<Key, size_t, HashFcn> PositionMap;
+ typedef std::unordered_map<Key, size_t, HashFcn> PositionMap;
typedef typename PositionMap::iterator PM_iterator;
typedef typename PositionMap::const_iterator PM_const_iterator;
#pragma once
-namespace __gnu_cxx {
- template <class Key> struct hash;
-}/* __gnu_cxx namespace */
+#include <functional>
namespace CVC4 {
namespace context {
- template <class Key, class Data, class HashFcn = __gnu_cxx::hash<Key> >
+ template <class Key, class Data, class HashFcn = std::hash<Key> >
class CDTrailHashMap;
}/* CVC4::context namespace */
}/* CVC4 namespace */
-
class istream;
class ostream;
template <class T> class set {};
- template <class K, class V, class H> class hash_map {};
+ template <class K, class V, class H> class unordered_map {};
}
%{
using namespace CVC4;
#include <cassert>
-#include <ext/hash_map>
+#include <unordered_map>
#include <iosfwd>
#include <set>
#include <string>
%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
#ifndef __CVC4__DECISION__JUSTIFICATION_HEURISTIC
#define __CVC4__DECISION__JUSTIFICATION_HEURISTIC
+#include <unordered_set>
+
#include "context/cdhashmap.h"
#include "context/cdhashset.h"
#include "context/cdlist.h"
* splitter. Can happen when exploring assertion corresponding to a
* term-ITE.
*/
- hash_set<TNode,TNodeHashFunction> d_visited;
+ std::unordered_set<TNode,TNodeHashFunction> d_visited;
/**
* Set to track visited nodes in a dfs search done in computeITE
* function
*/
- hash_set<TNode,TNodeHashFunction> d_visitedComputeITE;
+ std::unordered_set<TNode,TNodeHashFunction> d_visitedComputeITE;
/** current decision for the recursive call */
SatLiteral d_curDecision;
};/* class JustificationHeuristic */
}/* namespace decision */
-
}/* namespace CVC4 */
#endif /* __CVC4__DECISION__JUSTIFICATION_HEURISTIC */
#ifndef __CVC4__EXPR__ATTRIBUTE_INTERNALS_H
#define __CVC4__EXPR__ATTRIBUTE_INTERNALS_H
-#include <ext/hash_map>
+#include <unordered_map>
namespace CVC4 {
namespace expr {
*/
template <class value_type>
class AttrHash :
- public __gnu_cxx::hash_map<std::pair<uint64_t, NodeValue*>,
+ public std::unordered_map<std::pair<uint64_t, NodeValue*>,
value_type,
AttrHashFunction> {
};/* class AttrHash<> */
*/
template <>
class AttrHash<bool> :
- protected __gnu_cxx::hash_map<NodeValue*,
+ protected std::unordered_map<NodeValue*,
uint64_t,
AttrBoolHashFunction> {
/** A "super" type, like in Java, for easy reference below. */
- typedef __gnu_cxx::hash_map<NodeValue*, uint64_t, AttrBoolHashFunction> super;
+ typedef std::unordered_map<NodeValue*, uint64_t, AttrBoolHashFunction> super;
/**
* BitAccessor allows us to return a bit "by reference." Of course,
#ifndef __CVC4__DATATYPE_H
#define __CVC4__DATATYPE_H
+#include <functional>
#include <iostream>
#include <string>
#include <vector>
*/
struct CVC4_PUBLIC DatatypeHashFunction {
inline size_t operator()(const Datatype& dt) const {
- return StringHashFunction()(dt.getName());
+ return std::hash<std::string>()(dt.getName());
}
inline size_t operator()(const Datatype* dt) const {
- return StringHashFunction()(dt->getName());
+ return std::hash<std::string>()(dt->getName());
}
inline size_t operator()(const DatatypeConstructor& dtc) const {
- return StringHashFunction()(dtc.getName());
+ return std::hash<std::string>()(dtc.getName());
}
inline size_t operator()(const DatatypeConstructor* dtc) const {
- return StringHashFunction()(dtc->getName());
+ return std::hash<std::string>()(dtc->getName());
}
};/* struct DatatypeHashFunction */
class ExportPrivate {
private:
- typedef std::hash_map <NodeTemplate<false>, NodeTemplate<true>, TNodeHashFunction> ExportCache;
+ typedef std::unordered_map <NodeTemplate<false>, NodeTemplate<true>, TNodeHashFunction> ExportCache;
ExprManager* from;
ExprManager* to;
ExprManagerMapCollection& vmap;
return NodePairIteratorAdaptor<Iterator>(i);
}
-Expr Expr::substitute(const std::hash_map<Expr, Expr, ExprHashFunction> map) const {
+Expr Expr::substitute(const std::unordered_map<Expr, Expr, ExprHashFunction> map) const {
ExprManagerScope ems(*this);
return Expr(d_exprManager, new Node(d_node->substitute(mkNodePairIteratorAdaptor(map.begin()), mkNodePairIteratorAdaptor(map.end()))));
}
#include <stdint.h>
#include <iostream>
#include <iterator>
-
#include <string>
+#include <unordered_map>
#include "base/exception.h"
#include "options/language.h"
/**
* Substitute pairs of (ex,replacement) from the given map.
*/
- Expr substitute(const std::hash_map<Expr, Expr, ExprHashFunction> map) const;
+ Expr substitute(const std::unordered_map<Expr, Expr, ExprHashFunction> map) const;
/**
* Returns the string representation of the expression.
#ifndef __CVC4__NODE_H
#define __CVC4__NODE_H
-#include <vector>
-#include <string>
-#include <iostream>
-#include <utility>
+#include <stdint.h>
+
#include <algorithm>
#include <functional>
-#include <stdint.h>
+#include <iostream>
+#include <string>
+#include <unordered_map>
+#include <unordered_set>
+#include <utility>
+#include <vector>
#include "base/configuration.h"
#include "base/cvc4_assert.h"
#include "options/language.h"
#include "options/set_language.h"
#include "util/utility.h"
-#include "util/hash.h"
namespace CVC4 {
* member function with a similar signature.
*/
Node substitute(TNode node, TNode replacement,
- std::hash_map<TNode, TNode, TNodeHashFunction>& cache) const;
+ std::unordered_map<TNode, TNode, TNodeHashFunction>& cache) const;
/**
* Cache-aware, recursive version of substitute() used by the public
template <class Iterator1, class Iterator2>
Node substitute(Iterator1 nodesBegin, Iterator1 nodesEnd,
Iterator2 replacementsBegin, Iterator2 replacementsEnd,
- std::hash_map<TNode, TNode, TNodeHashFunction>& cache) const;
+ std::unordered_map<TNode, TNode, TNodeHashFunction>& cache) const;
/**
* Cache-aware, recursive version of substitute() used by the public
*/
template <class Iterator>
Node substitute(Iterator substitutionsBegin, Iterator substitutionsEnd,
- std::hash_map<TNode, TNode, TNodeHashFunction>& cache) const;
+ std::unordered_map<TNode, TNode, TNodeHashFunction>& cache) const;
/** Default constructor, makes a null expression. */
NodeTemplate() : d_nv(&expr::NodeValue::null()) { }
}/* CVC4 namespace */
-#include <ext/hash_map>
-
//#include "expr/attribute.h"
#include "expr/node_manager.h"
#include "expr/type_checker.h"
if (node == *this) {
return replacement;
}
- std::hash_map<TNode, TNode, TNodeHashFunction> cache;
+ std::unordered_map<TNode, TNode, TNodeHashFunction> cache;
return substitute(node, replacement, cache);
}
template <bool ref_count>
Node
NodeTemplate<ref_count>::substitute(TNode node, TNode replacement,
- std::hash_map<TNode, TNode, TNodeHashFunction>& cache) const {
+ std::unordered_map<TNode, TNode, TNodeHashFunction>& cache) const {
Assert(node != *this);
if (getNumChildren() == 0) {
}
// in cache?
- typename std::hash_map<TNode, TNode, TNodeHashFunction>::const_iterator i = cache.find(*this);
+ typename std::unordered_map<TNode, TNode, TNodeHashFunction>::const_iterator i = cache.find(*this);
if(i != cache.end()) {
return (*i).second;
}
Iterator1 nodesEnd,
Iterator2 replacementsBegin,
Iterator2 replacementsEnd) const {
- std::hash_map<TNode, TNode, TNodeHashFunction> cache;
+ std::unordered_map<TNode, TNode, TNodeHashFunction> cache;
return substitute(nodesBegin, nodesEnd,
replacementsBegin, replacementsEnd, cache);
}
Iterator1 nodesEnd,
Iterator2 replacementsBegin,
Iterator2 replacementsEnd,
- std::hash_map<TNode, TNode, TNodeHashFunction>& cache) const {
+ std::unordered_map<TNode, TNode, TNodeHashFunction>& cache) const {
// in cache?
- typename std::hash_map<TNode, TNode, TNodeHashFunction>::const_iterator i = cache.find(*this);
+ typename std::unordered_map<TNode, TNode, TNodeHashFunction>::const_iterator i = cache.find(*this);
if(i != cache.end()) {
return (*i).second;
}
inline Node
NodeTemplate<ref_count>::substitute(Iterator substitutionsBegin,
Iterator substitutionsEnd) const {
- std::hash_map<TNode, TNode, TNodeHashFunction> cache;
+ std::unordered_map<TNode, TNode, TNodeHashFunction> cache;
return substitute(substitutionsBegin, substitutionsEnd, cache);
}
Node
NodeTemplate<ref_count>::substitute(Iterator substitutionsBegin,
Iterator substitutionsEnd,
- std::hash_map<TNode, TNode, TNodeHashFunction>& cache) const {
+ std::unordered_map<TNode, TNode, TNodeHashFunction>& cache) const {
// in cache?
- typename std::hash_map<TNode, TNode, TNodeHashFunction>::const_iterator i = cache.find(*this);
+ typename std::unordered_map<TNode, TNode, TNodeHashFunction>::const_iterator i = cache.find(*this);
if(i != cache.end()) {
return (*i).second;
}
template<bool ref_count>
bool NodeTemplate<ref_count>::hasSubterm(NodeTemplate<false> t, bool strict) const {
- typedef std::hash_set<TNode, TNodeHashFunction> node_set;
+ typedef std::unordered_set<TNode, TNodeHashFunction> node_set;
if (!strict && *this == t) {
return true;
#include "expr/node_manager.h"
#include <algorithm>
-#include <ext/hash_set>
#include <stack>
#include <utility>
using namespace std;
using namespace CVC4::expr;
-using __gnu_cxx::hash_set;
namespace CVC4 {
#include <vector>
#include <string>
-#include <ext/hash_set>
+#include <unordered_set>
#include "base/tls.h"
#include "expr/kind.h"
bool operator()(expr::NodeValue* nv) { return nv->d_rc > 0; }
};
- typedef __gnu_cxx::hash_set<expr::NodeValue*,
- expr::NodeValuePoolHashFunction,
- expr::NodeValuePoolEq> NodeValuePool;
- typedef __gnu_cxx::hash_set<expr::NodeValue*,
- expr::NodeValueIDHashFunction,
- expr::NodeValueIDEquality> NodeValueIDSet;
+ typedef std::unordered_set<expr::NodeValue*,
+ expr::NodeValuePoolHashFunction,
+ expr::NodeValuePoolEq> NodeValuePool;
+ typedef std::unordered_set<expr::NodeValue*,
+ expr::NodeValueIDHashFunction,
+ expr::NodeValueIDEquality> NodeValueIDSet;
static CVC4_THREADLOCAL(NodeManager*) s_current;
#ifndef __CVC4__RECORD_H
#define __CVC4__RECORD_H
+#include <functional>
#include <iostream>
#include <string>
#include <vector>
#include <utility>
-#include "util/hash.h"
// Forward Declarations
namespace CVC4 {
struct CVC4_PUBLIC RecordSelectHashFunction {
inline size_t operator()(const RecordSelect& t) const {
- return StringHashFunction()(t.getField());
+ return std::hash<std::string>()(t.getField());
}
};/* struct RecordSelectHashFunction */
struct CVC4_PUBLIC RecordUpdateHashFunction {
inline size_t operator()(const RecordUpdate& t) const {
- return StringHashFunction()(t.getField());
+ return std::hash<std::string>()(t.getField());
}
};/* struct RecordUpdateHashFunction */
SymbolTable::SymbolTable() :
d_context(new Context()),
- d_exprMap(new(true) CDHashMap<std::string, Expr, StringHashFunction>(d_context)),
- d_typeMap(new(true) CDHashMap<std::string, pair<vector<Type>, Type>, StringHashFunction>(d_context)),
+ d_exprMap(new(true) CDHashMap<std::string, Expr>(d_context)),
+ d_typeMap(new(true) CDHashMap<std::string, pair<vector<Type>, Type>>(d_context)),
d_functions(new(true) CDHashSet<Expr, ExprHashFunction>(d_context)) {
}
}
bool SymbolTable::isBoundDefinedFunction(const std::string& name) const throw() {
- CDHashMap<std::string, Expr, StringHashFunction>::iterator found =
+ CDHashMap<std::string, Expr>::iterator found =
d_exprMap->find(name);
return found != d_exprMap->end() && d_functions->contains((*found).second);
}
#include <vector>
#include <utility>
-#include <ext/hash_map>
#include "expr/expr.h"
#include "util/hash.h"
context::Context* d_context;
/** A map for expressions. */
- context::CDHashMap<std::string, Expr, StringHashFunction> *d_exprMap;
+ context::CDHashMap<std::string, Expr>* d_exprMap;
/** A map for types. */
- context::CDHashMap<std::string, std::pair<std::vector<Type>, Type>, StringHashFunction> *d_typeMap;
+ context::CDHashMap<std::string, std::pair<std::vector<Type>, Type> >*
+ d_typeMap;
/** A set of defined functions. */
context::CDHashSet<Expr, ExprHashFunction> *d_functions;
TypeNode TypeNode::substitute(const TypeNode& type,
const TypeNode& replacement,
- std::hash_map<TypeNode, TypeNode, HashFunction>& cache) const {
+ std::unordered_map<TypeNode, TypeNode, HashFunction>& cache) const {
// in cache?
- std::hash_map<TypeNode, TypeNode, HashFunction>::const_iterator i = cache.find(*this);
+ std::unordered_map<TypeNode, TypeNode, HashFunction>::const_iterator i = cache.find(*this);
if(i != cache.end()) {
return (*i).second;
}
#ifndef __CVC4__TYPE_NODE_H
#define __CVC4__TYPE_NODE_H
-#include <vector>
-#include <string>
-#include <iostream>
#include <stdint.h>
+#include <iostream>
+#include <string>
+#include <unordered_map>
+#include <vector>
+
#include "base/cvc4_assert.h"
#include "expr/kind.h"
#include "expr/metakind.h"
* member function with a similar signature.
*/
TypeNode substitute(const TypeNode& type, const TypeNode& replacement,
- std::hash_map<TypeNode, TypeNode, HashFunction>& cache) const;
+ std::unordered_map<TypeNode, TypeNode, HashFunction>& cache) const;
/**
* Cache-aware, recursive version of substitute() used by the public
template <class Iterator1, class Iterator2>
TypeNode substitute(Iterator1 typesBegin, Iterator1 typesEnd,
Iterator2 replacementsBegin, Iterator2 replacementsEnd,
- std::hash_map<TypeNode, TypeNode, HashFunction>& cache) const;
+ std::unordered_map<TypeNode, TypeNode, HashFunction>& cache) const;
public:
}/* CVC4 namespace */
-#include <ext/hash_map>
-
#include "expr/node_manager.h"
namespace CVC4 {
inline TypeNode
TypeNode::substitute(const TypeNode& type,
const TypeNode& replacement) const {
- std::hash_map<TypeNode, TypeNode, HashFunction> cache;
+ std::unordered_map<TypeNode, TypeNode, HashFunction> cache;
return substitute(type, replacement, cache);
}
Iterator1 typesEnd,
Iterator2 replacementsBegin,
Iterator2 replacementsEnd) const {
- std::hash_map<TypeNode, TypeNode, HashFunction> cache;
+ std::unordered_map<TypeNode, TypeNode, HashFunction> cache;
return substitute(typesBegin, typesEnd,
replacementsBegin, replacementsEnd, cache);
}
Iterator1 typesEnd,
Iterator2 replacementsBegin,
Iterator2 replacementsEnd,
- std::hash_map<TypeNode, TypeNode, HashFunction>& cache) const {
+ std::unordered_map<TypeNode, TypeNode, HashFunction>& cache) const {
// in cache?
- std::hash_map<TypeNode, TypeNode, HashFunction>::const_iterator i = cache.find(*this);
+ std::unordered_map<TypeNode, TypeNode, HashFunction>::const_iterator i = cache.find(*this);
if(i != cache.end()) {
return (*i).second;
}
#ifndef __CVC4__VARIABLE_TYPE_MAP_H
#define __CVC4__VARIABLE_TYPE_MAP_H
+#include <unordered_map>
+
#include "expr/expr.h"
-#include "util/hash.h"
namespace CVC4 {
* A map Expr -> Expr, intended to be used for a mapping of variables
* between two ExprManagers.
*/
- std::hash_map<Expr, Expr, ExprHashFunction> d_variables;
+ std::unordered_map<Expr, Expr, ExprHashFunction> d_variables;
/**
* A map Type -> Type, intended to be used for a mapping of types
* between two ExprManagers.
*/
- std::hash_map<Type, Type, TypeHashFunction> d_types;
+ std::unordered_map<Type, Type, TypeHashFunction> d_types;
public:
Expr& operator[](Expr e) { return d_variables[e]; }
};/* class VariableTypeMap */
-typedef __gnu_cxx::hash_map<uint64_t, uint64_t> VarMap;
+typedef std::unordered_map<uint64_t, uint64_t> VarMap;
struct CVC4_PUBLIC ExprManagerMapCollection {
VariableTypeMap d_typeMap;
** Definitions of SMT-LIB (v1) constants.
**/
-#include <ext/hash_map>
-namespace std {
- using namespace __gnu_cxx;
-}
+#include "parser/smt1/smt1.h"
#include "expr/type.h"
#include "smt/command.h"
#include "parser/parser.h"
-#include "parser/smt1/smt1.h"
namespace CVC4 {
namespace parser {
-std::hash_map<const std::string, Smt1::Logic, CVC4::StringHashFunction> Smt1::newLogicMap() {
- std::hash_map<const std::string, Smt1::Logic, CVC4::StringHashFunction> logicMap;
+std::unordered_map<std::string, Smt1::Logic> Smt1::newLogicMap() {
+ std::unordered_map<std::string, Smt1::Logic> logicMap;
logicMap["AUFLIA"] = AUFLIA;
logicMap["AUFLIRA"] = AUFLIRA;
logicMap["AUFNIRA"] = AUFNIRA;
}
Smt1::Logic Smt1::toLogic(const std::string& name) {
- static std::hash_map<const std::string, Smt1::Logic, CVC4::StringHashFunction> logicMap = newLogicMap();
+ static std::unordered_map<std::string, Smt1::Logic> logicMap = newLogicMap();
return logicMap[name];
}
#ifndef __CVC4__PARSER__SMT1_H
#define __CVC4__PARSER__SMT1_H
-#include <ext/hash_map>
-namespace std { using namespace __gnu_cxx; }
+#include <string>
+#include <unordered_map>
-#include "util/hash.h"
#include "parser/parser.h"
namespace CVC4 {
private:
void addArithmeticOperators();
- static std::hash_map<const std::string, Logic, CVC4::StringHashFunction> newLogicMap();
+ static std::unordered_map<std::string, Logic> newLogicMap();
};/* class Smt1 */
}/* CVC4::parser namespace */
#include <set>
#include <sstream>
#include <string>
+#include <unordered_set>
#include <vector>
#include "base/output.h"
#define MK_CONST EXPR_MANAGER->mkConst
#define UNSUPPORTED PARSER_STATE->unimplementedFeature
-static bool isClosed(const Expr& e, std::set<Expr>& free, std::hash_set<Expr, ExprHashFunction>& closedCache) {
+static bool isClosed(const Expr& e, std::set<Expr>& free, std::unordered_set<Expr, ExprHashFunction>& closedCache) {
if(closedCache.find(e) != closedCache.end()) {
return true;
}
}
static inline bool isClosed(const Expr& e, std::set<Expr>& free) {
- std::hash_set<Expr, ExprHashFunction> cache;
+ std::unordered_set<Expr, ExprHashFunction> cache;
return isClosed(e, free, cache);
}
Expr attexpr;
std::vector<Expr> patexprs;
std::vector<Expr> patconds;
- std::hash_set<std::string, StringHashFunction> names;
+ std::unordered_set<std::string> names;
std::vector< std::pair<std::string, Expr> > binders;
Type type;
std::string s;
#include <sstream>
#include <stack>
#include <string>
+#include <unordered_map>
#include <utility>
#include "parser/parser.h"
private:
bool d_logicSet;
LogicInfo d_logic;
- std::hash_map<std::string, Kind, StringHashFunction> operatorKindMap;
+ std::unordered_map<std::string, Kind> operatorKindMap;
std::pair<Expr, std::string> d_lastNamedTerm;
// this is a user-context stack
std::stack< std::map<Expr, std::string> > d_unsatCoreNames;
#define __CVC4__PARSER__TPTP_H
#include <cassert>
-#include <ext/hash_set>
+#include <unordered_map>
+#include <unordered_set>
#include "parser/parser.h"
#include "smt/command.h"
Expr d_utr_op;
Expr d_uts_op;
// The set of expression that already have a bridge
- std::hash_set<Expr, ExprHashFunction> d_r_converted;
- std::hash_map<std::string, Expr, StringHashFunction> d_distinct_objects;
+ std::unordered_set<Expr, ExprHashFunction> d_r_converted;
+ std::unordered_map<std::string, Expr> d_distinct_objects;
std::vector< pANTLR3_INPUT_STREAM > d_in_created;
#ifndef __CVC4__PRINTER__DAGIFICATION_VISITOR_H
#define __CVC4__PRINTER__DAGIFICATION_VISITOR_H
+#include <string>
+#include <unordered_map>
+#include <vector>
+
#include "expr/node.h"
#include "util/hash.h"
-#include <vector>
-#include <string>
-
namespace CVC4 {
namespace context {
/**
* A map of subexprs to their occurrence count.
*/
- std::hash_map<TNode, unsigned, TNodeHashFunction> d_nodeCount;
+ std::unordered_map<TNode, unsigned, TNodeHashFunction> d_nodeCount;
/**
* The top-most node we are visiting.
* in independently dagifying the child. (If it is beyond the threshold
* and occurs in more than one parent, we'll independently dagify.)
*/
- std::hash_map<TNode, TNode, TNodeHashFunction> d_uniqueParent;
+ std::unordered_map<TNode, TNode, TNodeHashFunction> d_uniqueParent;
/**
* A list of all nodes that meet the occurrence threshold and therefore
#ifndef __CVC4__ARITH__PROOF_H
#define __CVC4__ARITH__PROOF_H
+#include <unordered_set>
+
#include "expr/expr.h"
#include "proof/proof_manager.h"
#include "proof/theory_proof.h"
}
}
-typedef __gnu_cxx::hash_set<Type, TypeHashFunction > TypeSet;
+typedef std::unordered_set<Type, TypeHashFunction > TypeSet;
class ArithProof : public TheoryProof {
#ifndef __CVC4__ARRAY__PROOF_H
#define __CVC4__ARRAY__PROOF_H
+#include <unordered_set>
+
#include "expr/expr.h"
#include "proof/proof_manager.h"
#include "proof/theory_proof.h"
} /* namespace CVC4::theory::arrays */
} /* namespace CVC4::theory */
-typedef __gnu_cxx::hash_set<Type, TypeHashFunction > TypeSet;
+typedef std::unordered_set<Type, TypeHashFunction > TypeSet;
class ArrayProof : public TheoryProof {
// TODO: whatever goes in this theory
#ifndef __CVC4__BITVECTOR__PROOF_H
#define __CVC4__BITVECTOR__PROOF_H
-//#include <cstdint>
-#include <ext/hash_map>
-#include <ext/hash_set>
#include <iostream>
#include <set>
#include <sstream>
+#include <unordered_map>
+#include <unordered_set>
#include <vector>
#include "expr/expr.h"
template <class Solver> class LFSCSatProof;
typedef LFSCSatProof< CVC4::BVMinisat::Solver> LFSCBVSatProof;
-typedef __gnu_cxx::hash_set<Expr, ExprHashFunction> ExprSet;
-typedef __gnu_cxx::hash_map<Expr, ClauseId, ExprHashFunction> ExprToClauseId;
-typedef __gnu_cxx::hash_map<Expr, unsigned, ExprHashFunction> ExprToId;
-typedef __gnu_cxx::hash_map<Expr, Expr, ExprHashFunction> ExprToExpr;
-typedef __gnu_cxx::hash_map<Expr, std::string, ExprHashFunction> ExprToString;
+typedef std::unordered_set<Expr, ExprHashFunction> ExprSet;
+typedef std::unordered_map<Expr, ClauseId, ExprHashFunction> ExprToClauseId;
+typedef std::unordered_map<Expr, unsigned, ExprHashFunction> ExprToId;
+typedef std::unordered_map<Expr, Expr, ExprHashFunction> ExprToExpr;
+typedef std::unordered_map<Expr, std::string, ExprHashFunction> ExprToString;
class BitVectorProof : public TheoryProof {
protected:
#ifndef __CVC4__CNF_PROOF_H
#define __CVC4__CNF_PROOF_H
-#include <ext/hash_map>
-#include <ext/hash_set>
#include <iosfwd>
+#include <unordered_map>
+#include <unordered_set>
#include "context/cdhashmap.h"
#include "proof/clause_id.h"
class CnfProof;
-typedef
__gnu_cxx::hash_map<prop::SatVariable, Expr> SatVarToExpr;
-typedef __gnu_cxx::hash_map<Node, Node, NodeHashFunction> NodeToNode;
-typedef __gnu_cxx::hash_set<ClauseId> ClauseIdSet;
+typedef
std::unordered_map<prop::SatVariable, Expr> SatVarToExpr;
+typedef std::unordered_map<Node, Node, NodeHashFunction> NodeToNode;
+typedef std::unordered_set<ClauseId> ClauseIdSet;
typedef context::CDHashMap<ClauseId, Node> ClauseIdToNode;
typedef context::CDHashMap<Node, ProofRule, NodeHashFunction> NodeToProofRule;
#define __CVC4__PROOF_MANAGER_H
#include <iosfwd>
-#include <map>
+#include <unordered_map>
+#include <unordered_set>
+
#include "expr/node.h"
#include "context/cdhashset.h"
#include "context/cdhashmap.h"
std::string append(const std::string& str, uint64_t num);
-typedef __gnu_cxx::hash_map < ClauseId, prop::SatClause* > IdToSatClause;
-typedef __gnu_cxx::hash_set<Expr, ExprHashFunction> ExprSet;
+typedef std::unordered_map<ClauseId, prop::SatClause*> IdToSatClause;
typedef context::CDHashSet<Expr, ExprHashFunction> CDExprSet;
-typedef __gnu_cxx::hash_set<Node, NodeHashFunction > NodeSet;
-typedef __gnu_cxx::hash_map<Node, std::vector<Node>, NodeHashFunction > NodeToNodes;
-typedef context::CDHashMap<Node, std::vector<Node>, NodeHashFunction > CDNodeToNodes;
-typedef std::hash_set<ClauseId> IdHashSet;
+typedef std::unordered_map<Node, std::vector<Node>, NodeHashFunction> NodeToNodes;
+typedef context::CDHashMap<Node, std::vector<Node>, NodeHashFunction> CDNodeToNodes;
+typedef std::unordered_set<ClauseId> IdHashSet;
enum ProofRule {
RULE_GIVEN, /* input assertion */
#ifndef __CVC4__PROOF_OUTPUT_CHANNEL_H
#define __CVC4__PROOF_OUTPUT_CHANNEL_H
+#include <unordered_set>
+
#include "theory/output_channel.h"
namespace CVC4 {
class MyPreRegisterVisitor {
theory::Theory* d_theory;
- __gnu_cxx::hash_set<TNode, TNodeHashFunction> d_visited;
+ std::unordered_set<TNode, TNodeHashFunction> d_visited;
public:
typedef void return_type;
MyPreRegisterVisitor(theory::Theory* theory);
#pragma once
#include <set>
-#include <vector>
#include <sstream>
+#include <unordered_set>
+#include <vector>
+
#include "expr/node_manager.h"
namespace CVC4 {
-typedef __gnu_cxx::hash_set<Expr, ExprHashFunction> ExprSet;
-typedef __gnu_cxx::hash_set<Node, NodeHashFunction> NodeSet;
+typedef std::unordered_set<Expr, ExprHashFunction> ExprSet;
+typedef std::unordered_set<Node, NodeHashFunction> NodeSet;
typedef std::pair<Node, Node> NodePair;
typedef std::set<NodePair> NodePairSet;
#include <stdint.h>
-#include <ext/hash_map>
-#include <ext/hash_set>
#include <iosfwd>
#include <set>
#include <sstream>
+#include <unordered_map>
#include <vector>
#include "context/cdhashmap.h"
typedef std::set<typename Solver::TLit> LitSet;
typedef std::set<typename Solver::TVar> VarSet;
- typedef std::hash_map<ClauseId, typename Solver::TCRef> IdCRefMap;
- typedef std::hash_map<typename Solver::TCRef, ClauseId> ClauseIdMap;
+ typedef std::unordered_map<ClauseId, typename Solver::TCRef> IdCRefMap;
+ typedef std::unordered_map<typename Solver::TCRef, ClauseId> ClauseIdMap;
typedef context::CDHashMap<ClauseId, typename Solver::TLit> IdUnitMap;
typedef context::CDHashMap<int, ClauseId> UnitIdMap;
typedef context::CDHashMap<ClauseId, ResolutionChain*> IdResMap;
- typedef std::hash_map<ClauseId, uint64_t> IdProofRuleMap;
+ typedef std::unordered_map<ClauseId, uint64_t> IdProofRuleMap;
typedef std::vector<ResolutionChain*> ResStack;
typedef std::set<ClauseId> IdSet;
typedef std::vector<typename Solver::TLit> LitVector;
- typedef __gnu_cxx::hash_map<ClauseId, typename Solver::TClause&>
+ typedef std::unordered_map<ClauseId, typename Solver::TClause&>
IdToMinisatClause;
- typedef __gnu_cxx::hash_map<ClauseId, LitVector*> IdToConflicts;
+ typedef std::unordered_map<ClauseId, LitVector*> IdToConflicts;
public:
TSatProof(Solver* solver, context::Context* context,
IdToSatClause d_seenLemmas;
private:
- __gnu_cxx::hash_map<ClauseId, int> d_glueMap;
+ std::unordered_map<ClauseId, int> d_glueMap;
struct Statistics {
IntStat d_numLearnedClauses;
IntStat d_numLearnedInProof;
d_skolemToDisequality.clear();
}
-std::hash_map<Node, Node, NodeHashFunction>::const_iterator SkolemizationManager::begin() {
+std::unordered_map<Node, Node, NodeHashFunction>::const_iterator SkolemizationManager::begin() {
return d_disequalityToSkolem.begin();
}
-std::hash_map<Node, Node, NodeHashFunction>::const_iterator SkolemizationManager::end() {
+std::unordered_map<Node, Node, NodeHashFunction>::const_iterator SkolemizationManager::end() {
return d_disequalityToSkolem.end();
}
#define __CVC4__SKOLEMIZATION_MANAGER_H
#include <iostream>
-#include <map>
+#include <unordered_map>
+
#include "proof/proof.h"
#include "util/proof.h"
#include "expr/node.h"
bool isSkolem(Node skolem);
void clear();
- std::hash_map<Node, Node, NodeHashFunction>::const_iterator begin();
- std::hash_map<Node, Node, NodeHashFunction>::const_iterator end();
+ std::unordered_map<Node, Node, NodeHashFunction>::const_iterator begin();
+ std::unordered_map<Node, Node, NodeHashFunction>::const_iterator end();
private:
- std::hash_map<Node, Node, NodeHashFunction> d_disequalityToSkolem;
- std::hash_map<Node, Node, NodeHashFunction> d_skolemToDisequality;
+ std::unordered_map<Node, Node, NodeHashFunction> d_disequalityToSkolem;
+ std::unordered_map<Node, Node, NodeHashFunction> d_skolemToDisequality;
};
}/* CVC4 namespace */
#ifndef __CVC4__THEORY_PROOF_H
#define __CVC4__THEORY_PROOF_H
-#include <ext/hash_set>
#include <iosfwd>
+#include <unordered_map>
+#include <unordered_set>
#include "expr/expr.h"
#include "proof/clause_id.h"
class Theory;
} /* namespace CVC4::theory */
-typedef __gnu_cxx::hash_map < ClauseId, prop::SatClause* > IdToSatClause;
+typedef std::unordered_map < ClauseId, prop::SatClause* > IdToSatClause;
class TheoryProof;
-typedef __gnu_cxx::hash_set<Expr, ExprHashFunction > ExprSet;
+typedef std::unordered_set<Expr, ExprHashFunction > ExprSet;
typedef std::map<theory::TheoryId, TheoryProof* > TheoryProofTable;
typedef std::set<theory::TheoryId> TheoryIdSet;
#ifndef __CVC4__UF__PROOF_H
#define __CVC4__UF__PROOF_H
+#include <unordered_set>
+
#include "expr/expr.h"
#include "proof/proof_manager.h"
#include "theory/uf/equality_engine.h"
}
}
-typedef __gnu_cxx::hash_set<Type, TypeHashFunction > TypeSet;
+typedef std::unordered_set<Type, TypeHashFunction > TypeSet;
class UFProof : public TheoryProof {
if(d_bvp){
ClauseId id = d_bvp->getSatProof()->registerClause(cr, LEARNT);
PSTATS(
- __gnu_cxx::hash_set<int> cl_levels;
+ std::unordered_set<int> cl_levels;
for (int i = 0; i < learnt_clause.size(); ++i) {
cl_levels.insert(level(var(learnt_clause[i])));
}
#ifndef BVMinisat_Solver_h
#define BVMinisat_Solver_h
-#include <ext/hash_set>
#include <vector>
#include "context/context.h"
#ifndef __CVC4__PROP__CNF_STREAM_H
#define __CVC4__PROP__CNF_STREAM_H
-#include <ext/hash_map>
-
#include "context/cdinsert_hashmap.h"
#include "context/cdlist.h"
#include "expr/node.h"
#include <math.h>
#include <iostream>
+#include <unordered_set>
#include "base/output.h"
#include "options/prop_options.h"
PROOF(
ClauseId id = ProofManager::getSatProof()->registerClause(cr, LEARNT);
PSTATS(
- __gnu_cxx::hash_set<int> cl_levels;
+ std::unordered_set<int> cl_levels;
for (int i = 0; i < learnt_clause.size(); ++i) {
cl_levels.insert(level(var(learnt_clause[i])));
}
#define __CVC4_USE_MINISAT
#include <iosfwd>
+#include <unordered_set>
#include "context/cdqueue.h"
#include "expr/expr_stream.h"
* Set of all lemmas that have been "shared" in the portfolio---i.e.,
* all imported and exported lemmas.
*/
- std::hash_set<Node, NodeHashFunction> d_shared;
+ std::unordered_set<Node, NodeHashFunction> d_shared;
/**
* Statistic: the number of replayed decisions (via --replay).
#include <algorithm>
#include <cctype>
-#include <ext/hash_map>
+#include <unordered_map>
+#include <unordered_set>
#include <iterator>
#include <sstream>
#include <stack>
class SmtEnginePrivate : public NodeManagerListener {
SmtEngine& d_smt;
- typedef hash_map<Node, Node, NodeHashFunction> NodeToNodeHashMap;
- typedef hash_map<Node, bool, NodeHashFunction> NodeToBoolHashMap;
+ typedef unordered_map<Node, Node, NodeHashFunction> NodeToNodeHashMap;
+ typedef unordered_map<Node, bool, NodeHashFunction> NodeToBoolHashMap;
/**
* Manager for limiting time and abstract resource usage.
* conjuncts.
*/
size_t removeFromConjunction(Node& n,
- const std::hash_set<unsigned long>& toRemove);
+ const std::unordered_set<unsigned long>& toRemove);
/** Scrub miplib encodings. */
void doMiplibTrick();
return d_definedFunctions->find(nf) != d_definedFunctions->end();
}
-Node SmtEnginePrivate::expandDefinitions(TNode n, hash_map<Node, Node, NodeHashFunction>& cache, bool expandOnly)
+Node SmtEnginePrivate::expandDefinitions(TNode n, unordered_map<Node, Node, NodeHashFunction>& cache, bool expandOnly)
throw(TypeCheckingException, LogicException, UnsafeInterruptException) {
stack< triple<Node, Node, bool> > worklist;
}
// maybe it's in the cache
- hash_map<Node, Node, NodeHashFunction>::iterator cacheHit = cache.find(n);
+ unordered_map<Node, Node, NodeHashFunction>::iterator cacheHit = cache.find(n);
if(cacheHit != cache.end()) {
TNode ret = (*cacheHit).second;
result.push(ret.isNull() ? n : ret);
: node(node), children_added(false) {}
};/* struct intToBV_stack_element */
-typedef std::hash_map<Node, Node, NodeHashFunction> NodeMap;
+typedef std::unordered_map<Node, Node, NodeHashFunction> NodeMap;
Node SmtEnginePrivate::intToBVMakeBinary(TNode n, NodeMap& cache) {
// Do a topological sort of the subexpressions and substitute them
Trace("simplify") << "Resize non-clausal learned literals to " << j << std::endl;
d_nonClausalLearnedLiterals.resize(j);
- hash_set<TNode, TNodeHashFunction> s;
+ unordered_set<TNode, TNodeHashFunction> s;
Trace("debugging") << "NonClausal simplify pre-preprocess\n";
for (unsigned i = 0; i < d_assertions.size(); ++ i) {
Node assertion = d_assertions[i];
}
}
-size_t SmtEnginePrivate::removeFromConjunction(Node& n, const std::hash_set<unsigned long>& toRemove) {
+size_t SmtEnginePrivate::removeFromConjunction(Node& n, const std::unordered_set<unsigned long>& toRemove) {
Assert(n.getKind() == kind::AND);
size_t removals = 0;
for(Node::iterator j = n.begin(); j != n.end(); ++j) {
Assert(!options::incrementalSolving());
const booleans::CircuitPropagator::BackEdgesMap& backEdges = d_propagator.getBackEdges();
- hash_set<unsigned long> removeAssertions;
+ unordered_set<unsigned long> removeAssertions;
NodeManager* nm = NodeManager::currentNM();
Node zero = nm->mkConst(Rational(0)), one = nm->mkConst(Rational(1));
- hash_map<TNode, Node, TNodeHashFunction> intVars;
+ unordered_map<TNode, Node, TNodeHashFunction> intVars;
for(vector<Node>::const_iterator i = d_boolVars.begin(); i != d_boolVars.end(); ++i) {
if(d_propagator.isAssigned(*i)) {
Debug("miplib") << "ineligible: " << *i << " because assigned " << d_propagator.getAssignment(*i) << endl;
}
-void SmtEnginePrivate::collectSkolems(TNode n, set<TNode>& skolemSet, hash_map<Node, bool, NodeHashFunction>& cache)
+void SmtEnginePrivate::collectSkolems(TNode n, set<TNode>& skolemSet, unordered_map<Node, bool, NodeHashFunction>& cache)
{
- hash_map<Node, bool, NodeHashFunction>::iterator it;
+ unordered_map<Node, bool, NodeHashFunction>::iterator it;
it = cache.find(n);
if (it != cache.end()) {
return;
}
-bool SmtEnginePrivate::checkForBadSkolems(TNode n, TNode skolem, hash_map<Node, bool, NodeHashFunction>& cache)
+bool SmtEnginePrivate::checkForBadSkolems(TNode n, TNode skolem, unordered_map<Node, bool, NodeHashFunction>& cache)
{
- hash_map<Node, bool, NodeHashFunction>::iterator it;
+ unordered_map<Node, bool, NodeHashFunction>::iterator it;
it = cache.find(n);
if (it != cache.end()) {
return (*it).second;
Chat() << "expanding definitions..." << endl;
Trace("simplify") << "SmtEnginePrivate::simplify(): expanding definitions" << endl;
TimerStat::CodeTimer codeTimer(d_smt.d_stats->d_definitionExpansionTime);
- hash_map<Node, Node, NodeHashFunction> cache;
+ unordered_map<Node, Node, NodeHashFunction> cache;
for(unsigned i = 0; i < d_assertions.size(); ++ i) {
d_assertions.replace(i, expandDefinitions(d_assertions[i], cache));
}
Debug("smt") << " d_assertions : " << d_assertions.size() << endl;
if( options::nlExtPurify() ){
- hash_map<Node, Node, NodeHashFunction> cache;
- hash_map<Node, Node, NodeHashFunction> bcache;
+ unordered_map<Node, Node, NodeHashFunction> cache;
+ unordered_map<Node, Node, NodeHashFunction> bcache;
std::vector< Node > var_eq;
for (unsigned i = 0; i < d_assertions.size(); ++ i) {
d_assertions.replace(i, purifyNlTerms(d_assertions[i], cache, bcache, var_eq));
if (options::solveRealAsInt()) {
Chat() << "converting reals to ints..." << endl;
- hash_map<Node, Node, NodeHashFunction> cache;
+ unordered_map<Node, Node, NodeHashFunction> cache;
std::vector< Node > var_eq;
for(unsigned i = 0; i < d_assertions.size(); ++ i) {
d_assertions.replace(i, realToInt(d_assertions[i], cache, var_eq));
if (options::solveIntAsBV() > 0) {
Chat() << "converting ints to bit-vectors..." << endl;
- hash_map<Node, Node, NodeHashFunction> cache;
+ unordered_map<Node, Node, NodeHashFunction> cache;
for(unsigned i = 0; i < d_assertions.size(); ++ i) {
d_assertions.replace(i, intToBV(d_assertions[i], cache));
}
// For each skolem variable sk, let iteExpr = iteMap(sk) be the ite expr mapped to by sk.
// cache for expression traversal
- hash_map<Node, bool, NodeHashFunction> cache;
+ unordered_map<Node, bool, NodeHashFunction> cache;
// First, find all skolems that appear in the substitution map - their associated iteExpr will need
// to be moved to the main assertion set
if(Dump.isOn("benchmark")) {
Dump("benchmark") << ExpandDefinitionsCommand(e);
}
- hash_map<Node, Node, NodeHashFunction> cache;
+ unordered_map<Node, Node, NodeHashFunction> cache;
Node n = d_private->expandDefinitions(Node::fromExpr(e), cache, /* expandOnly = */ true);
n = postprocess(n, TypeNode::fromType(e.getType()));
TypeNode expectedType = n.getType();
// Expand, then normalize
- hash_map<Node, Node, NodeHashFunction> cache;
+ unordered_map<Node, Node, NodeHashFunction> cache;
n = d_private->expandDefinitions(n, cache);
// There are two ways model values for terms are computed (for historical
// reasons). One way is that used in check-model; the other is that
Trace("smt") << "--- getting value of " << *i << endl;
// Expand, then normalize
- hash_map<Node, Node, NodeHashFunction> cache;
+ unordered_map<Node, Node, NodeHashFunction> cache;
Node n = d_private->expandDefinitions(*i, cache);
n = Rewriter::rewrite(n);
// Apply any define-funs from the problem.
{
- hash_map<Node, Node, NodeHashFunction> cache;
+ unordered_map<Node, Node, NodeHashFunction> cache;
n = d_private->expandDefinitions(n, cache);
}
Notice() << "SmtEngine::checkModel(): -- expands to " << n << endl;
#pragma once
+#include <unordered_map>
#include <vector>
#include "context/cdinsert_hashmap.h"
class ContainsTermITEVisitor;
}/* CVC4::theory namespace */
-typedef std::hash_map<Node, unsigned, NodeHashFunction> IteSkolemMap;
+typedef std::unordered_map<Node, unsigned, NodeHashFunction> IteSkolemMap;
class RemoveTermFormulas {
typedef context::CDInsertHashMap< std::pair<Node, int>, Node, PairHashFunction<Node, int, NodeHashFunction, BoolHashFunction> > ITECache;
#pragma once
+#include <unordered_map>
#include <vector>
+
#include "expr/node.h"
namespace CVC4{
Node case_assoccomm(TNode n);
Node case_other(TNode n);
- typedef std::hash_map<Node, Node, NodeHashFunction> NodeMap;
+ typedef std::unordered_map<Node, Node, NodeHashFunction> NodeMap;
NodeMap d_cache;
};/* class RePairAssocCommutativeOperators */
** \todo document this file
**/
-
-
-
-
-
// Pass 1: label the ite as (constant) or (+ constant variable)
#include "cvc4_private.h"
#ifndef __CVC4__THEORY__ARITH__ARITH_ITE_UTILS_H
#define __CVC4__THEORY__ARITH__ARITH_ITE_UTILS_H
+#include <unordered_map>
+
#include "expr/node.h"
-#include <ext/hash_map>
-#include <ext/hash_set>
#include "context/cdo.h"
#include "context/cdtrail_hashmap.h"
SubstitutionMap* d_subs;
TheoryModel* d_model;
- typedef std::hash_map<Node, Node, NodeHashFunction> NodeMap;
+ typedef std::unordered_map<Node, Node, NodeHashFunction> NodeMap;
// cache for reduce vars
NodeMap d_reduceVar; // if reduceVars[n].isNull(), treat reduceVars[n] == n
NodeMap d_reduceGcd;
- typedef std::hash_map<Node, Integer, NodeHashFunction> NodeIntegerMap;
+ typedef std::unordered_map<Node, Integer, NodeHashFunction> NodeIntegerMap;
NodeIntegerMap d_gcds;
Integer d_one;
#ifndef __CVC4__THEORY__ARITH__ARITH_UTILITIES_H
#define __CVC4__THEORY__ARITH__ARITH_UTILITIES_H
-#include <ext/hash_map>
+#include <unordered_map>
+#include <unordered_set>
#include <vector>
#include "context/cdhashset.h"
namespace arith {
//Sets of Nodes
-typedef __gnu_cxx::hash_set<Node, NodeHashFunction> NodeSet;
-typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> TNodeSet;
+typedef std::unordered_set<Node, NodeHashFunction> NodeSet;
+typedef std::unordered_set<TNode, TNodeHashFunction> TNodeSet;
typedef context::CDHashSet<Node, NodeHashFunction> CDNodeSet;
//Maps from Nodes -> ArithVars, and vice versa
-typedef __gnu_cxx::hash_map<Node, ArithVar, NodeHashFunction> NodeToArithVarMap;
+typedef std::unordered_map<Node, ArithVar, NodeHashFunction> NodeToArithVarMap;
typedef DenseMap<Node> ArithVarToNodeMap;
inline Node mkRationalNode(const Rational& q){
**/
#include "theory/arith/constraint.h"
-#include <ostream>
#include <algorithm>
+#include <ostream>
+#include <unordered_set>
#include "base/output.h"
#include "proof/proof.h"
};
void Constraint::assertionFringe(ConstraintCPVec& v){
- hash_set<ConstraintCP, ConstraintCPHash> visited;
+ unordered_set<ConstraintCP, ConstraintCPHash> visited;
size_t writePos = 0;
if(!v.empty()){
#ifndef __CVC4__THEORY__ARITH__CONSTRAINT_H
#define __CVC4__THEORY__ARITH__CONSTRAINT_H
-#include <ext/hash_map>
+#include <unordered_map>
#include <list>
#include <set>
#include <vector>
typedef context::CDList<ConstraintCP> CDConstraintList;
-typedef __gnu_cxx::hash_map<Node, ConstraintP, NodeHashFunction> NodetoConstraintMap;
+typedef std::unordered_map<Node, ConstraintP, NodeHashFunction> NodetoConstraintMap;
typedef size_t ConstraintRuleID;
static const ConstraintRuleID ConstraintRuleIdSentinel = std::numeric_limits<ConstraintRuleID>::max();
#pragma once
-#include <ext/hash_map>
+#include <unordered_map>
#include <map>
#include <set>
#include <vector>
int d_upId;
public:
- typedef __gnu_cxx::hash_map<int, ArithVar> RowIdMap;
+ typedef std::unordered_map<int, ArithVar> RowIdMap;
private:
RowIdMap d_rowId2ArithVar;
}
Node DioSolver::columnGcdIsOne() const{
- std::hash_map<Node, Integer, NodeHashFunction> gcdMap;
+ std::unordered_map<Node, Integer, NodeHashFunction> gcdMap;
std::deque<TrailIndex>::const_iterator iter, end;
for(iter = d_currentF.begin(), end = d_currentF.end(); iter != end; ++iter){
#ifndef __CVC4__THEORY__ARITH__DIO_SOLVER_H
#define __CVC4__THEORY__ARITH__DIO_SOLVER_H
+#include <unordered_map>
#include <utility>
#include <vector>
* We maintain a map from the variables associated with proofs to an input constraint.
* These variables can then be used in polynomial manipulations.
*/
- typedef std::hash_map<Node, InputConstraintIndex, NodeHashFunction> NodeToInputConstraintIndexMap;
+ typedef std::unordered_map<Node, InputConstraintIndex, NodeHashFunction> NodeToInputConstraintIndexMap;
NodeToInputConstraintIndexMap d_varToInputConstraintMap;
Node proofVariableToReason(const Variable& v) const{
#pragma once
-#include <ext/hash_set>
+#include <unordered_set>
#include <vector>
#include "context/cdhashmap.h"
CDNode2PairMap d_pbBounds;
SubstitutionMap d_subCache;
- typedef __gnu_cxx::hash_set<Node, NodeHashFunction> NodeSet;
+ typedef std::unordered_set<Node, NodeHashFunction> NodeSet;
NodeSet d_learningCache;
context::CDO<unsigned> d_pbs;
#pragma once
+#include <unordered_map>
+
#include "theory/arith/arithvar.h"
#include "theory/arith/delta_rational.h"
#include "theory/arith/error_set.h"
}
};
- typedef std::
hash_map< std::pair<ArithVar, int>, ArithVarVec, ArithVarIntPairHashFunc> sgn_table;
+ typedef std::
unordered_map< std::pair<ArithVar, int>, ArithVarVec, ArithVarIntPairHashFunc> sgn_table;
static inline int determinizeSgn(int sgn){
return sgn < 0 ? -1 : (sgn == 0 ? 0 : 1);
// Delta lasts at least the duration of the function call
const Rational& delta = d_partialModel.getDelta();
- std::hash_set<TNode, TNodeHashFunction> shared = d_containing.currentlySharedTerms();
+ std::unordered_set<TNode, TNodeHashFunction> shared = d_containing.currentlySharedTerms();
// TODO:
// This is not very good for user push/pop....
#ifndef __CVC4__THEORY__ARRAYS__ARRAY_INFO_H
#define __CVC4__THEORY__ARRAYS__ARRAY_INFO_H
-#include <ext/hash_set>
-#include <ext/hash_map>
#include <iostream>
#include <map>
+#include <unordered_map>
#include "context/backtrackable.h"
#include "context/cdlist.h"
};/* class Info */
-typedef __gnu_cxx::hash_map<Node, Info*, NodeHashFunction> CNodeInfoMap;
+typedef std::unordered_map<Node, Info*, NodeHashFunction> CNodeInfoMap;
/**
* Class keeping track of the following information for canonical
#include <utility>
#include <vector>
-#include <ext/hash_map>
+#include <unordered_map>
#include "expr/node.h"
class StaticFactManager {
/** Our underlying map type. */
- typedef __gnu_cxx::hash_map<Node, Node, NodeHashFunction> MapType;
+ typedef std::unordered_map<Node, Node, NodeHashFunction> MapType;
/**
* Our map of Nodes to their canonical representatives.
}
void TheoryArrays::weakEquivAddSecondary(TNode index, TNode arrayFrom, TNode arrayTo, TNode reason) {
- std::hash_set<TNode, TNodeHashFunction> marked;
+ std::unordered_set<TNode, TNodeHashFunction> marked;
vector<TNode> index_trail;
vector<TNode>::iterator it, iend;
Node equivalence_trail = reason;
/*
}
else {
- std::hash_map<Node, Node, NodeHashFunction>::iterator it = d_skolemCache.find(n);
+ std::unordered_map<Node, Node, NodeHashFunction>::iterator it = d_skolemCache.find(n);
if (it == d_skolemCache.end()) {
rep = nm->mkSkolem("array_collect_model_var", n.getType(), "base model variable for array collectModelInfo");
d_skolemCache[n] = rep;
Node TheoryArrays::getSkolem(TNode ref, const string& name, const TypeNode& type, const string& comment, bool makeEqual)
{
Node skolem;
- std::hash_map<Node, Node, NodeHashFunction>::iterator it = d_skolemCache.find(ref);
+ std::unordered_map<Node, Node, NodeHashFunction>::iterator it = d_skolemCache.find(ref);
if (it == d_skolemCache.end()) {
NodeManager* nm = NodeManager::currentNM();
skolem = nm->mkSkolem(name, type, comment);
#ifndef __CVC4__THEORY__ARRAYS__THEORY_ARRAYS_H
#define __CVC4__THEORY__ARRAYS__THEORY_ARRAYS_H
+#include <unordered_map>
+
#include "context/cdhashmap.h"
#include "context/cdhashset.h"
#include "context/cdqueue.h"
// When a new read term is created, we check the index to see if we know the model value. If so, we add it to d_constReads (and d_constReadsList)
// If not, we push it onto d_reads and figure out where it goes at computeCareGraph time.
// d_constReadsList is used as a backup in case we can't compute the model at computeCareGraph time.
- typedef std::hash_map<Node, CTNodeList*, NodeHashFunction> CNodeNListMap;
+ typedef std::unordered_map<Node, CTNodeList*, NodeHashFunction> CNodeNListMap;
CNodeNListMap d_constReads;
context::CDList<TNode> d_reads;
context::CDList<TNode> d_constReadsList;
};/* class ContextPopper */
ContextPopper d_contextPopper;
- std::hash_map<Node, Node, NodeHashFunction> d_skolemCache;
+ std::unordered_map<Node, Node, NodeHashFunction> d_skolemCache;
context::CDO<unsigned> d_skolemIndex;
std::vector<Node> d_skolemAssertions;
typedef context::CDHashMap<Node,Node,NodeHashFunction> DefValMap;
DefValMap d_defValues;
- typedef std::hash_map<std::pair<TNode, TNode>, CTNodeList*, TNodePairHashFunction> ReadBucketMap;
+ typedef std::unordered_map<std::pair<TNode, TNode>, CTNodeList*, TNodePairHashFunction> ReadBucketMap;
ReadBucketMap d_readBucketTable;
context::Context* d_readTableContext;
context::CDList<Node> d_arrayMerges;
#ifndef __CVC4__THEORY__ARRAYS__THEORY_ARRAYS_REWRITER_H
#define __CVC4__THEORY__ARRAYS__THEORY_ARRAYS_REWRITER_H
+#include <unordered_map>
+#include <unordered_set>
+
#include "theory/rewriter.h"
#include "theory/type_enumerator.h"
// Bad case: have to recompute value counts and/or possibly switch out
// default value
store = n;
- std::hash_set<TNode, TNodeHashFunction> indexSet;
- std::hash_map<TNode, unsigned, TNodeHashFunction> elementsMap;
- std::hash_map<TNode, unsigned, TNodeHashFunction>::iterator it;
+ std::unordered_set<TNode, TNodeHashFunction> indexSet;
+ std::unordered_map<TNode, unsigned, TNodeHashFunction> elementsMap;
+ std::unordered_map<TNode, unsigned, TNodeHashFunction>::iterator it;
unsigned count;
unsigned max = 0;
TNode maxValue;
#include <utility>
#include <vector>
-#include <ext/hash_map>
+#include <unordered_map>
#include "expr/node.h"
#include "context/cdo.h"
template <class NodeType, class NodeHash>
class UnionFind : context::ContextNotifyObj {
/** Our underlying map type. */
- typedef __gnu_cxx::hash_map<NodeType, NodeType, NodeHash> MapType;
+ typedef std::unordered_map<NodeType, NodeType, NodeHash> MapType;
/**
* Our map of Nodes to their canonical representatives.
#ifndef __CVC4__THEORY__BOOLEANS__CIRCUIT_PROPAGATOR_H
#define __CVC4__THEORY__BOOLEANS__CIRCUIT_PROPAGATOR_H
-#include <vector>
#include <functional>
+#include <unordered_map>
+#include <vector>
#include "theory/theory.h"
#include "context/context.h"
else return ASSIGNED_TO_TRUE;
}
- typedef std::hash_map<Node, std::vector<Node>, NodeHashFunction> BackEdgesMap;
+ typedef std::unordered_map<Node, std::vector<Node>, NodeHashFunction> BackEdgesMap;
private:
**/
#include <algorithm>
+#include <unordered_set>
+
#include "theory/booleans/theory_bool_rewriter.h"
namespace CVC4 {
*/
RewriteResponse flattenNode(TNode n, TNode trivialNode, TNode skipNode)
{
- typedef std::hash_set<TNode, TNodeHashFunction> node_set;
+ typedef std::unordered_set<TNode, TNodeHashFunction> node_set;
node_set visited;
visited.insert(skipNode);
#ifndef __CVC4__THEORY__BV__ABSTRACTION_H
#define __CVC4__THEORY__BV__ABSTRACTION_H
-#include <ext/hash_map>
-#include <ext/hash_set>
+#include <unordered_map>
+#include <unordered_set>
#include "expr/node.h"
#include "theory/substitutions.h"
};
class ArgsTable {
- __gnu_cxx::hash_map<TNode, ArgsTableEntry, TNodeHashFunction > d_data;
+ std::unordered_map<TNode, ArgsTableEntry, TNodeHashFunction > d_data;
bool hasEntry(TNode signature) const;
public:
- typedef __gnu_cxx::hash_map<TNode, ArgsTableEntry, TNodeHashFunction >::iterator iterator;
+ typedef std::unordered_map<TNode, ArgsTableEntry, TNodeHashFunction >::iterator iterator;
ArgsTable() {}
void addEntry(TNode signature, const ArgsVec& args);
ArgsTableEntry& getEntry(TNode signature);
};
- typedef __gnu_cxx::hash_map<Node, std::vector<Node>, NodeHashFunction> NodeVecMap;
- typedef __gnu_cxx::hash_map<Node, TNode, NodeHashFunction> NodeTNodeMap;
- typedef __gnu_cxx::hash_map<TNode, TNode, TNodeHashFunction> TNodeTNodeMap;
- typedef __gnu_cxx::hash_map<Node, Node, NodeHashFunction> NodeNodeMap;
- typedef __gnu_cxx::hash_map<Node, TNode, NodeHashFunction> TNodeNodeMap;
- typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> TNodeSet;
- typedef __gnu_cxx::hash_map<unsigned, Node> IntNodeMap;
- typedef __gnu_cxx::hash_map<unsigned, unsigned> IndexMap;
- typedef __gnu_cxx::hash_map<unsigned, std::vector<Node> > SkolemMap;
- typedef __gnu_cxx::hash_map<TNode, unsigned, TNodeHashFunction > SignatureMap;
+ typedef std::unordered_map<Node, std::vector<Node>, NodeHashFunction> NodeVecMap;
+ typedef std::unordered_map<Node, TNode, NodeHashFunction> NodeTNodeMap;
+ typedef std::unordered_map<TNode, TNode, TNodeHashFunction> TNodeTNodeMap;
+ typedef std::unordered_map<Node, Node, NodeHashFunction> NodeNodeMap;
+ typedef std::unordered_map<Node, TNode, NodeHashFunction> TNodeNodeMap;
+ typedef std::unordered_set<TNode, TNodeHashFunction> TNodeSet;
+ typedef std::unordered_map<unsigned, Node> IntNodeMap;
+ typedef std::unordered_map<unsigned, unsigned> IndexMap;
+ typedef std::unordered_map<unsigned, std::vector<Node> > SkolemMap;
+ typedef std::unordered_map<TNode, unsigned, TNodeHashFunction > SignatureMap;
ArgsTable d_argsTable;
#ifndef __CVC4__BITBLASTER_TEMPLATE_H
#define __CVC4__BITBLASTER_TEMPLATE_H
-#include <ext/hash_map>
+#include <unordered_map>
+#include <unordered_set>
#include <vector>
#include "bitblast_strategies_template.h"
class BitblastingRegistrar;
-typedef __gnu_cxx::hash_set<Node, NodeHashFunction> NodeSet;
-typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> TNodeSet;
+typedef std::unordered_set<Node, NodeHashFunction> NodeSet;
+typedef std::unordered_set<TNode, TNodeHashFunction> TNodeSet;
class AbstractionModule;
class TBitblaster {
protected:
typedef std::vector<T> Bits;
- typedef __gnu_cxx::hash_map <Node, Bits, NodeHashFunction> TermDefMap;
- typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> TNodeSet;
- typedef __gnu_cxx::hash_map<Node, Node, NodeHashFunction> ModelCache;
+ typedef std::unordered_map <Node, Bits, NodeHashFunction> TermDefMap;
+ typedef std::unordered_set<TNode, TNodeHashFunction> TNodeSet;
+ typedef std::unordered_map<Node, Node, NodeHashFunction> ModelCache;
typedef void (*TermBBStrategy) (TNode, Bits&, TBitblaster<T>*);
typedef T (*AtomBBStrategy) (TNode, TBitblaster<T>*);
class EagerBitblaster : public TBitblaster<Node> {
- typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> TNodeSet;
+ typedef std::unordered_set<TNode, TNodeHashFunction> TNodeSet;
// sat solver used for bitblasting and associated CnfStream
prop::SatSolver* d_satSolver;
BitblastingRegistrar* d_bitblastingRegistrar;
}; /* class Registrar */
class AigBitblaster : public TBitblaster<Abc_Obj_t*> {
- typedef std::hash_map<TNode, Abc_Obj_t*, TNodeHashFunction > TNodeAigMap;
- typedef std::hash_map<Node, Abc_Obj_t*, NodeHashFunction > NodeAigMap;
+ typedef std::unordered_map<TNode, Abc_Obj_t*, TNodeHashFunction > TNodeAigMap;
+ typedef std::unordered_map<Node, Abc_Obj_t*, NodeHashFunction > NodeAigMap;
static Abc_Ntk_t* abcAigNetwork;
context::Context* d_nullContext;
** All rights reserved. See the file COPYING in the top-level source
** directory for licensing information.\endverbatim
**
- ** \brief Eager bit-blasting solver.
+ ** \brief Eager bit-blasting solver.
**
** Eager bit-blasting solver.
**/
#include "cvc4_private.h"
+
+#pragma once
+
+#include <unordered_set>
+#include <vector>
+
#include "expr/node.h"
#include "theory/theory_model.h"
#include "theory/bv/theory_bv.h"
-#include <vector>
-#pragma once
-
namespace CVC4 {
namespace theory {
* BitblastSolver
*/
class EagerBitblastSolver {
- typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> AssertionSet;
+ typedef std::unordered_set<TNode, TNodeHashFunction> AssertionSet;
AssertionSet d_assertionSet;
/** Bitblasters */
EagerBitblaster* d_bitblaster;
** 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.
**/
#ifndef __CVC4__THEORY__BV__BV_INEQUALITY__GRAPH_H
#define __CVC4__THEORY__BV__BV_INEQUALITY__GRAPH_H
-#include "context/context.h"
+#include <list>
+#include <queue>
+#include <unordered_map>
+#include <unordered_set>
+
#include "context/cdqueue.h"
-#include "theory/uf/equality_engine.h"
+#include "context/context.h"
#include "theory/theory.h"
-#include <queue>
-#include <list>
+#include "theory/uf/equality_engine.h"
+
namespace CVC4 {
namespace theory {
-
-
namespace bv {
-typedef unsigned TermId;
+typedef unsigned TermId;
typedef unsigned ReasonId;
extern const TermId UndefinedTermId;
extern const ReasonId UndefinedReasonId;
-extern const ReasonId AxiomReasonId;
+extern const ReasonId AxiomReasonId;
class InequalityGraph : public context::ContextNotifyObj{
}
};
- typedef __gnu_cxx::hash_map<TNode, ReasonId, TNodeHashFunction> ReasonToIdMap;
- typedef __gnu_cxx::hash_map<TNode, TermId, TNodeHashFunction> TermNodeToIdMap;
+ typedef std::unordered_map<TNode, ReasonId, TNodeHashFunction> ReasonToIdMap;
+ typedef std::unordered_map<TNode, TermId, TNodeHashFunction> TermNodeToIdMap;
typedef std::vector<InequalityEdge> Edges;
- typedef __gnu_cxx::hash_set<TermId> TermIdSet;
+ typedef std::unordered_set<TermId> TermIdSet;
typedef std::priority_queue<TermId, std::vector<TermId>, QueueComparator> BFSQueue;
- typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> TNodeSet;
- typedef __gnu_cxx::hash_set<Node, NodeHashFunction> NodeSet;
+ typedef std::unordered_set<TNode, TNodeHashFunction> TNodeSet;
+ typedef std::unordered_set<Node, NodeHashFunction> NodeSet;
std::vector<InequalityNode> d_ineqNodes;
std::vector< Edges > d_ineqEdges;
#define __CVC4__BV_QUICK_CHECK_H
#include <vector>
-#include <ext/hash_map>
+#include <unordered_set>
#include "context/cdo.h"
#include "expr/node.h"
uint64_t computeAtomWeight(TNode atom, NodeSet& seen);
void collectModelInfo(theory::TheoryModel* model, bool fullModel);
- typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction>::const_iterator vars_iterator;
+ typedef std::unordered_set<TNode, TNodeHashFunction>::const_iterator vars_iterator;
vars_iterator beginVars();
vars_iterator endVars();
** Algebraic solver.
**/
+#include "cvc4_private.h"
+
#pragma once
-#include "cvc4_private.h"
+#include <unordered_map>
+#include <unordered_set>
+
#include "theory/bv/bv_subtheory.h"
-#include "theory/substitutions.h"
#include "theory/bv/slicer.h"
+#include "theory/substitutions.h"
namespace CVC4 {
namespace theory {
{}
};
- typedef __gnu_cxx::hash_map<Node, SubstitutionElement, NodeHashFunction> Substitutions;
- typedef __gnu_cxx::hash_map<Node, SubstitutionElement, NodeHashFunction> SubstitutionsCache;
+ typedef std::unordered_map<Node, SubstitutionElement, NodeHashFunction> Substitutions;
+ typedef std::unordered_map<Node, SubstitutionElement, NodeHashFunction> SubstitutionsCache;
Substitutions d_substitutions;
SubstitutionsCache d_cache;
};
-typedef __gnu_cxx::hash_map<Node, Node, NodeHashFunction> NodeNodeMap;
-typedef __gnu_cxx::hash_map<Node, unsigned, NodeHashFunction> NodeIdMap;
-typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> TNodeSet;
+typedef std::unordered_map<Node, Node, NodeHashFunction> NodeNodeMap;
+typedef std::unordered_map<Node, unsigned, NodeHashFunction> NodeIdMap;
+typedef std::unordered_set<TNode, TNodeHashFunction> TNodeSet;
class ExtractSkolemizer {
ExtractList() : base(1), extracts() {}
void addExtract(Extract& e);
};
- typedef __gnu_cxx::hash_map<Node, ExtractList, NodeHashFunction> VarExtractMap;
+ typedef std::unordered_map<Node, ExtractList, NodeHashFunction> VarExtractMap;
context::Context d_emptyContext;
VarExtractMap d_varToExtract;
theory::SubstitutionMap* d_modelMap;
#pragma once
+#include <unordered_map>
+
#include "theory/bv/bitblaster_template.h"
#include "theory/bv/bv_subtheory.h"
context::CDQueue<TNode> d_bitblastQueue;
Statistics d_statistics;
- typedef std::hash_map<Node, Node, NodeHashFunction> NodeMap;
+ typedef std::unordered_map<Node, Node, NodeHashFunction> NodeMap;
NodeMap d_modelCache;
context::CDO<bool> d_validModelCache;
** Algebraic solver.
**/
+#include "cvc4_private.h"
+
#pragma once
-#include "cvc4_private.h"
-#include "theory/bv/bv_subtheory.h"
+#include <unordered_map>
+#include <unordered_set>
+
#include "context/cdhashmap.h"
#include "context/cdhashset.h"
+#include "theory/bv/bv_subtheory.h"
namespace CVC4 {
namespace theory {
* Bitvector equality solver
*/
class CoreSolver : public SubtheorySolver {
- typedef __gnu_cxx::hash_map<TNode, Node, TNodeHashFunction> ModelValue;
- typedef __gnu_cxx::hash_map<TNode, bool, TNodeHashFunction> TNodeBoolMap;
- typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> TNodeSet;
+ typedef std::unordered_map<TNode, Node, TNodeHashFunction> ModelValue;
+ typedef std::unordered_map<TNode, bool, TNodeHashFunction> TNodeBoolMap;
+ typedef std::unordered_set<TNode, TNodeHashFunction> TNodeSet;
struct Statistics {
#ifndef __CVC4__THEORY__BV__BV_SUBTHEORY__INEQUALITY_H
#define __CVC4__THEORY__BV__BV_SUBTHEORY__INEQUALITY_H
-#include "theory/bv/bv_subtheory.h"
-#include "theory/bv/bv_inequality_graph.h"
+#include <unordered_set>
+
#include "context/cdhashset.h"
#include "expr/attribute.h"
+#include "theory/bv/bv_inequality_graph.h"
+#include "theory/bv/bv_subtheory.h"
namespace CVC4 {
namespace theory {
InequalityGraph d_inequalityGraph;
context::CDHashMap<Node, TNode, NodeHashFunction> d_explanations;
context::CDO<bool> d_isComplete;
- typedef __gnu_cxx::hash_set<Node, NodeHashFunction> NodeSet;
+ typedef std::unordered_set<Node, NodeHashFunction> NodeSet;
NodeSet d_ineqTerms;
bool isInequalityOnly(TNode node);
bool addInequality(TNode a, TNode b, bool strict, TNode fact);
#ifndef __CVC4__THEORY__BV__BV_TO_BOOL_H
#define __CVC4__THEORY__BV__BV_TO_BOOL_H
+#include <unordered_map>
+
#include "theory/bv/theory_bv_utils.h"
#include "util/statistics_registry.h"
namespace theory {
namespace bv {
-typedef __gnu_cxx::hash_map<Node, Node, NodeHashFunction> NodeNodeMap;
+typedef std::unordered_map<Node, Node, NodeHashFunction> NodeNodeMap;
class BvToBoolPreprocessor {
#include "expr/node.h"
#include <vector>
-#include <ext/hash_map>
+#include <unordered_map>
#ifndef __CVC4__THEORY__BV__BV_INTRO_POW_H
#define __CVC4__THEORY__BV__BV_INTRO_POW_H
static void pow2Rewrite(std::vector<Node>& assertionsToPreprocess);
private:
- typedef __gnu_cxx::hash_map<Node, Node, NodeHashFunction> NodeMap;
+ typedef std::unordered_map<Node, Node, NodeHashFunction> NodeMap;
static Node pow2Rewrite(Node assertionsToPreprocess, NodeMap& cache);
};
#include <vector>
#include <list>
-#include <ext/hash_map>
+#include <unordered_map>
#include "expr/node.h"
#include "theory/bv/theory_bv_utils.h"
* UnionFind
*
*/
-typedef __gnu_cxx::hash_set<TermId> TermSet;
+typedef std::unordered_set<TermId> TermSet;
typedef std::vector<TermId> Decomposition;
struct ExtractTerm {
};
class Slicer {
- __gnu_cxx::hash_map<TermId, TNode> d_idToNode;
- __gnu_cxx::hash_map<TNode, TermId, TNodeHashFunction> d_nodeToId;
- __gnu_cxx::hash_map<TNode, bool, TNodeHashFunction> d_coreTermCache;
+ std::unordered_map<TermId, TNode> d_idToNode;
+ std::unordered_map<TNode, TermId, TNodeHashFunction> d_nodeToId;
+ std::unordered_map<TNode, bool, TNodeHashFunction> d_coreTermCache;
UnionFind d_unionFind;
ExtractTerm registerTerm(TNode node);
public:
#ifndef __CVC4__THEORY__BV__THEORY_BV_H
#define __CVC4__THEORY__BV__THEORY_BV_H
+#include <unordered_map>
+#include <unordered_set>
+
#include "context/cdhashset.h"
#include "context/cdlist.h"
#include "context/context.h"
context::CDHashSet<Node, NodeHashFunction> d_sharedTermsSet;
std::vector<SubtheorySolver*> d_subtheories;
- __gnu_cxx::hash_map<SubTheory, SubtheorySolver*, std::hash<int> > d_subtheoryMap;
+ std::unordered_map<SubTheory, SubtheorySolver*, std::hash<int> > d_subtheoryMap;
public:
*/
Node getBVDivByZero(Kind k, unsigned width);
- typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> TNodeSet;
+ typedef std::unordered_set<TNode, TNodeHashFunction> TNodeSet;
void collectFunctionSymbols(TNode term, TNodeSet& seen);
void storeFunction(TNode func, TNode term);
- typedef __gnu_cxx::hash_set<Node, NodeHashFunction> NodeSet;
+ typedef std::unordered_set<Node, NodeHashFunction> NodeSet;
NodeSet d_staticLearnCache;
/**
* Maps from bit-vector width to division-by-zero uninterpreted
* function symbols.
*/
- __gnu_cxx::hash_map<unsigned, Node> d_BVDivByZero;
- __gnu_cxx::hash_map<unsigned, Node> d_BVRemByZero;
+ std::unordered_map<unsigned, Node> d_BVDivByZero;
+ std::unordered_map<unsigned, Node> d_BVRemByZero;
- typedef __gnu_cxx::hash_map<Node, NodeSet, NodeHashFunction> FunctionToArgs;
- typedef __gnu_cxx::hash_map<Node, Node, NodeHashFunction> NodeToNode;
+ typedef std::unordered_map<Node, NodeSet, NodeHashFunction> FunctionToArgs;
+ typedef std::unordered_map<Node, Node, NodeHashFunction> NodeToNode;
// for ackermanization
FunctionToArgs d_funcToArgs;
CVC4::theory::SubstitutionMap d_funcToSkolem;
#pragma once
+#include <unordered_map>
+#include <unordered_set>
+
#include "theory/rewriter.h"
#include "theory/bv/theory_bv_rewrite_rules.h"
#include "theory/bv/theory_bv_utils.h"
{}
};
-inline static void insert(std::hash_map<TNode, Count, TNodeHashFunction>& map, TNode node, bool neg) {
+inline static void insert(std::unordered_map<TNode, Count, TNodeHashFunction>& map, TNode node, bool neg) {
if(map.find(node) == map.end()) {
Count c = neg? Count(0,1) : Count(1, 0);
map[node] = c;
Debug("bv-rewrite") << "RewriteRule<AndSimplify>(" << node << ")" << std::endl;
// this will remove duplicates
- std::hash_map<TNode, Count, TNodeHashFunction> subterms;
+ std::unordered_map<TNode, Count, TNodeHashFunction> subterms;
unsigned size = utils::getSize(node);
BitVector constant = utils::mkBitVectorOnes(size);
children.push_back(utils::mkConst(constant));
}
- std::hash_map<TNode, Count, TNodeHashFunction>::const_iterator it = subterms.begin();
+ std::unordered_map<TNode, Count, TNodeHashFunction>::const_iterator it = subterms.begin();
for (; it != subterms.end(); ++it) {
if (it->second.pos > 0 && it->second.neg > 0) {
Debug("bv-rewrite") << "RewriteRule<FlattenAssocCommut>(" << node << ")" << std::endl;
std::vector<Node> processingStack;
processingStack.push_back(node);
- __gnu_cxx::hash_set<TNode, TNodeHashFunction> processed;
+ std::unordered_set<TNode, TNodeHashFunction> processed;
std::vector<Node> children;
Kind kind = node.getKind();
Debug("bv-rewrite") << "RewriteRule<OrSimplify>(" << node << ")" << std::endl;
// this will remove duplicates
- std::hash_map<TNode, Count, TNodeHashFunction> subterms;
+ std::unordered_map<TNode, Count, TNodeHashFunction> subterms;
unsigned size = utils::getSize(node);
BitVector constant(size, (unsigned)0);
children.push_back(utils::mkConst(constant));
}
- std::hash_map<TNode, Count, TNodeHashFunction>::const_iterator it = subterms.begin();
+ std::unordered_map<TNode, Count, TNodeHashFunction>::const_iterator it = subterms.begin();
for (; it != subterms.end(); ++it) {
if (it->second.pos > 0 && it->second.neg > 0) {
Debug("bv-rewrite") << "RewriteRule<XorSimplify>(" << node << ")" << std::endl;
- std::hash_map<TNode, Count, TNodeHashFunction> subterms;
+ std::unordered_map<TNode, Count, TNodeHashFunction> subterms;
unsigned size = utils::getSize(node);
BitVector constant;
bool const_set = false;
std::vector<Node> children;
- std::hash_map<TNode, Count, TNodeHashFunction>::const_iterator it = subterms.begin();
+ std::unordered_map<TNode, Count, TNodeHashFunction>::const_iterator it = subterms.begin();
unsigned true_count = 0;
bool seen_false = false;
for (; it != subterms.end(); ++it) {
#include "cvc4_private.h"
-#pragma once
+#pragma once
#include <set>
-#include <vector>
#include <sstream>
+#include <unordered_map>
+#include <unordered_set>
+#include <vector>
+
#include "expr/node_manager.h"
namespace CVC4 {
namespace theory {
namespace bv {
-typedef __gnu_cxx::hash_set<Node, NodeHashFunction> NodeSet;
-typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> TNodeSet;
+typedef std::unordered_set<Node, NodeHashFunction> NodeSet;
+typedef std::unordered_set<TNode, TNodeHashFunction> TNodeSet;
namespace utils {
return a;
}
-typedef __gnu_cxx::hash_map<TNode, bool, TNodeHashFunction> TNodeBoolMap;
+typedef std::unordered_map<TNode, bool, TNodeHashFunction> TNodeBoolMap;
bool isCoreTerm(TNode term, TNodeBoolMap& cache);
bool isEqualityTerm(TNode term, TNodeBoolMap& cache);
-typedef __gnu_cxx::hash_set<Node, NodeHashFunction> NodeSet;
+typedef std::unordered_set<Node, NodeHashFunction> NodeSet;
uint64_t numNodes(TNode node, NodeSet& seen);
#ifndef __CVC4__THEORY__DATATYPES__THEORY_DATATYPES_H
#define __CVC4__THEORY__DATATYPES__THEORY_DATATYPES_H
-#include <ext/hash_set>
#include <iostream>
#include <map>
return true;
}
- hash_map<Node, bool, NodeHashFunction>::iterator it;
+ unordered_map<Node, bool, NodeHashFunction>::iterator it;
it = d_leavesConstCache.find(e);
if (it != d_leavesConstCache.end()) {
return (*it).second;
Node ITESimplifier::getSimpVar(TypeNode t)
{
- std::hash_map<TypeNode, Node, TypeNode::HashFunction>::iterator it;
+ std::unordered_map<TypeNode, Node, TypeNode::HashFunction>::iterator it;
it = d_simpVars.find(t);
if (it != d_simpVars.end()) {
return (*it).second;
d_simpContextCache[c] = result;
return result;
}
-typedef std::hash_set<Node, NodeHashFunction> NodeSet;
+typedef std::unordered_set<Node, NodeHashFunction> NodeSet;
void countReachable_(Node x, Kind k, NodeSet& visited, uint32_t& reached){
if(visited.find(x) != visited.end()){
return;
#ifndef __CVC4__ITE_UTILITIES_H
#define __CVC4__ITE_UTILITIES_H
-#include <ext/hash_map>
-#include <ext/hash_set>
+#include <unordered_map>
#include <vector>
#include "expr/node.h"
size_t cache_size() const { return d_cache.size(); }
private:
- typedef std::hash_map<Node, bool, NodeHashFunction> NodeBoolMap;
+ typedef std::unordered_map<Node, bool, NodeHashFunction> NodeBoolMap;
NodeBoolMap d_cache;
};
}
void clear();
private:
- typedef std::hash_map<Node, uint32_t, NodeHashFunction> NodeCountMap;
+ typedef std::unordered_map<Node, uint32_t, NodeHashFunction> NodeCountMap;
NodeCountMap d_reachCount;
bool d_skipVariables;
size_t cache_size() const;
private:
- typedef std::hash_map<Node, uint32_t, NodeHashFunction> NodeCountMap;
+ typedef std::unordered_map<Node, uint32_t, NodeHashFunction> NodeCountMap;
NodeCountMap d_termITEHeight;
}; /* class TermITEHeightCounter */
std::vector<Node>* d_assertions;
IncomingArcCounter d_incoming;
- typedef std::hash_map<Node, Node, NodeHashFunction> NodeMap;
+ typedef std::unordered_map<Node, Node, NodeHashFunction> NodeMap;
NodeMap d_compressed;
void reset();
// constant
// or termITE(cnd, ConstantIte, ConstantIte)
typedef std::vector<Node> NodeVec;
- typedef std::hash_map<Node, NodeVec*, NodeHashFunction > ConstantLeavesMap;
+ typedef std::unordered_map<Node, NodeVec*, NodeHashFunction > ConstantLeavesMap;
ConstantLeavesMap d_constantLeaves;
// d_constantLeaves satisfies the following invariants:
return hash;
}
};/* struct ITESimplifier::NodePairHashFunction */
- typedef std::hash_map<NodePair, Node, NodePairHashFunction> NodePairMap;
+ typedef std::unordered_map<NodePair, Node, NodePairHashFunction> NodePairMap;
NodePairMap d_constantIteEqualsConstantCache;
NodePairMap d_replaceOverCache;
NodePairMap d_replaceOverTermIteCache;
Node replaceOver(Node n, Node replaceWith, Node simpVar);
Node replaceOverTermIte(Node term, Node simpAtom, Node simpVar);
- std::hash_map<Node, bool, NodeHashFunction> d_leavesConstCache;
+ std::unordered_map<Node, bool, NodeHashFunction> d_leavesConstCache;
bool leavesAreConst(TNode e, theory::TheoryId tid);
bool leavesAreConst(TNode e);
NodePairMap d_simpConstCache;
Node simpConstants(TNode simpContext, TNode iteNode, TNode simpVar);
- std::hash_map<TypeNode, Node, TypeNode::HashFunction> d_simpVars;
+ std::unordered_map<TypeNode, Node, TypeNode::HashFunction> d_simpVars;
Node getSimpVar(TypeNode t);
- typedef std::hash_map<Node, Node, NodeHashFunction> NodeMap;
+ typedef std::unordered_map<Node, Node, NodeHashFunction> NodeMap;
NodeMap d_simpContextCache;
Node createSimpContext(TNode c, Node& iteNode, Node& simpVar);
Node d_true;
Node d_false;
- typedef std::hash_map<TNode, Node, TNodeHashFunction> TNodeMap;
+ typedef std::unordered_map<TNode, Node, TNodeHashFunction> TNodeMap;
class CareSetPtr;
class CareSetPtrVal {
#ifndef __CVC4__THEORY__QUANTIFIERS__EQUALITY_INFER_H
#define __CVC4__THEORY__QUANTIFIERS__EQUALITY_INFER_H
-#include <ext/hash_set>
#include <iostream>
#include <map>
#include <vector>
#ifndef __CVC4__THEORY__QUANTIFIERS__INST_MATCH_H
#define __CVC4__THEORY__QUANTIFIERS__INST_MATCH_H
-#include "util/hash.h"
-#include "context/cdo.h"
-
-#include <ext/hash_set>
#include <map>
#include "context/cdlist.h"
+#include "context/cdo.h"
#include "expr/node.h"
namespace CVC4 {
#ifndef __CVC4__THEORY__QUANT_UTIL_H
#define __CVC4__THEORY__QUANT_UTIL_H
-#include "theory/theory.h"
-#include "theory/uf/equality_engine.h"
-
-#include <ext/hash_set>
#include <iostream>
#include <map>
+#include "theory/theory.h"
+#include "theory/uf/equality_engine.h"
+
namespace CVC4 {
namespace theory {
}
}
//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 );
}/* CVC4::theory::quantifiers namespace */
}/* CVC4::theory namespace */
}/* CVC4 namespace */
-
#ifndef __CVC4__THEORY__QUANTIFIERS__TERM_DATABASE_H
#define __CVC4__THEORY__QUANTIFIERS__TERM_DATABASE_H
+#include <map>
+#include <unordered_set>
+
#include "expr/attribute.h"
#include "theory/theory.h"
#include "theory/type_enumerator.h"
#include "theory/quantifiers/quant_util.h"
-#include <map>
namespace CVC4 {
namespace theory {
/** 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 */
#ifndef __CVC4__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_H
#define __CVC4__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_H
-#include <ext/hash_set>
-#include <iostream>
-#include <map>
-
#include "context/cdhashmap.h"
+#include "context/context.h"
+#include "expr/node.h"
+#include "theory/output_channel.h"
#include "theory/theory.h"
-#include "util/hash.h"
+#include "theory/theory_engine.h"
+#include "theory/valuation.h"
#include "util/statistics_registry.h"
namespace CVC4 {
-class TheoryEngine;
-
namespace theory {
-
namespace quantifiers {
-class ModelEngine;
-class InstantiationEngine;
-
class TheoryQuantifiers : public Theory {
private:
typedef context::CDHashMap< Node, bool, NodeHashFunction > BoolMap;
r_best = r;
}
//now, make sure that no other member of the class is an instance
- std::hash_map<TNode, Node, TNodeHashFunction> cache;
+ std::unordered_map<TNode, Node, TNodeHashFunction> cache;
r_best = getInstance( r_best, eqc, cache );
//store that this representative was chosen at this point
if( d_rep_score.find( r_best )==d_rep_score.end() ){
//helper functions
-Node EqualityQueryQuantifiersEngine::getInstance( Node n, const std::vector< Node >& eqc, std::hash_map<TNode, Node, TNodeHashFunction>& cache ){
+Node EqualityQueryQuantifiersEngine::getInstance( Node n, const std::vector< Node >& eqc, std::unordered_map<TNode, Node, TNodeHashFunction>& cache ){
if(cache.find(n) != cache.end()) {
return cache[n];
}
#ifndef __CVC4__THEORY__QUANTIFIERS_ENGINE_H
#define __CVC4__THEORY__QUANTIFIERS_ENGINE_H
-#include <ext/hash_set>
#include <iostream>
#include <map>
+#include <unordered_map>
#include "context/cdchunk_list.h"
#include "context/cdhashset.h"
/** processInferences : will merge equivalence classes in master equality engine, if possible */
bool processInferences( Theory::Effort e );
/** node contains */
- Node getInstance( Node n, const std::vector< Node >& eqc, std::hash_map<TNode, Node, TNodeHashFunction>& cache );
+ Node getInstance( Node n, const std::vector< Node >& eqc, std::unordered_map<TNode, Node, TNodeHashFunction>& cache );
/** get score */
int getRepScore( Node n, Node f, int index, TypeNode v_tn );
/** flatten representatives */
}
#ifdef CVC4_ASSERTIONS
-static CVC4_THREADLOCAL(std::hash_set<Node, NodeHashFunction>*) s_rewriteStack = NULL;
+static CVC4_THREADLOCAL(std::unordered_set<Node, NodeHashFunction>*) s_rewriteStack = NULL;
#endif /* CVC4_ASSERTIONS */
class RewriterInitializer {
bool isEquality = node.getKind() == kind::EQUAL && (!node[0].getType().isBoolean());
if(s_rewriteStack == NULL) {
- s_rewriteStack = new std::hash_set<Node, NodeHashFunction>();
+ s_rewriteStack = new std::unordered_set<Node, NodeHashFunction>();
}
#endif
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;
}
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 );
if( tc_graph_it != (tc_it->second).end() ) {
(tc_graph_it->second).insert( mem_rep_snd );
} else {
- std::hash_set< Node, NodeHashFunction > sets;
+ std::unordered_set< Node, NodeHashFunction > sets;
sets.insert( mem_rep_snd );
(tc_it->second)[mem_rep_fst] = sets;
}
} else {
std::map< Node, Node > exp_map;
- std::hash_set< Node, NodeHashFunction > sets;
- std::map< Node, std::hash_set<Node, NodeHashFunction> > element_map;
+ std::unordered_set< Node, NodeHashFunction > sets;
+ std::map< Node, std::unordered_set<Node, NodeHashFunction> > element_map;
sets.insert( mem_rep_snd );
element_map[mem_rep_fst] = sets;
d_tcr_tcGraph[tc_rel] = element_map;
TC_IT tc_it = d_rRep_tcGraph.find( getRepresentative(tc_rel[0]) );
if( tc_it != d_rRep_tcGraph.end() ) {
bool isReachable = false;
- std::hash_set<Node, NodeHashFunction> seen;
+ std::unordered_set<Node, NodeHashFunction> seen;
isTCReachable( getRepresentative( RelsUtils::nthElementOfTuple(mem_rep, 0) ),
getRepresentative( RelsUtils::nthElementOfTuple(mem_rep, 1) ), seen, tc_it->second, isReachable );
return isReachable;
return false;
}
- void TheorySetsRels::isTCReachable( Node start, Node dest, std::hash_set<Node, NodeHashFunction>& hasSeen,
- std::map< Node, std::hash_set< Node, NodeHashFunction > >& tc_graph, bool& isReachable ) {
+ void TheorySetsRels::isTCReachable( Node start, Node dest, std::unordered_set<Node, NodeHashFunction>& hasSeen,
+ std::map< Node, std::unordered_set< Node, NodeHashFunction > >& tc_graph, bool& isReachable ) {
if(hasSeen.find(start) == hasSeen.end()) {
hasSeen.insert(start);
}
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
void TheorySetsRels::buildTCGraphForRel( Node tc_rel ) {
std::map< Node, Node > rel_tc_graph_exps;
- std::map< Node, std::hash_set<Node, NodeHashFunction> > rel_tc_graph;
+ std::map< Node, std::unordered_set<Node, NodeHashFunction> > rel_tc_graph;
Node rel_rep = getRepresentative( tc_rel[0] );
Node tc_rel_rep = getRepresentative( tc_rel );
Node fst_element_rep = getRepresentative( RelsUtils::nthElementOfTuple( members[i], 0 ));
Node snd_element_rep = getRepresentative( RelsUtils::nthElementOfTuple( members[i], 1 ));
Node tuple_rep = RelsUtils::constructPair( rel_rep, fst_element_rep, snd_element_rep );
- std::map< Node, std::hash_set<Node, NodeHashFunction> >::iterator rel_tc_graph_it = rel_tc_graph.find( fst_element_rep );
+ std::map< Node, std::unordered_set<Node, NodeHashFunction> >::iterator rel_tc_graph_it = rel_tc_graph.find( fst_element_rep );
if( rel_tc_graph_it == rel_tc_graph.end() ) {
- std::hash_set< Node, NodeHashFunction > snd_elements;
+ std::unordered_set< Node, NodeHashFunction > snd_elements;
snd_elements.insert( snd_element_rep );
rel_tc_graph[fst_element_rep] = snd_elements;
rel_tc_graph_exps[tuple_rep] = exps[i];
}
}
- void TheorySetsRels::doTCInference( std::map< Node, std::hash_set<Node, NodeHashFunction> > rel_tc_graph, std::map< Node, Node > rel_tc_graph_exps, Node tc_rel ) {
+ void TheorySetsRels::doTCInference( std::map< Node, std::unordered_set<Node, NodeHashFunction> > rel_tc_graph, std::map< Node, Node > rel_tc_graph_exps, Node tc_rel ) {
Trace("rels-debug") << "[Theory::Rels] ****** doTCInference !" << std::endl;
for( TC_GRAPH_IT tc_graph_it = rel_tc_graph.begin(); tc_graph_it != rel_tc_graph.end(); tc_graph_it++ ) {
- for( std::hash_set< Node, NodeHashFunction >::iterator snd_elements_it = tc_graph_it->second.begin();
+ for( std::unordered_set< Node, NodeHashFunction >::iterator snd_elements_it = tc_graph_it->second.begin();
snd_elements_it != tc_graph_it->second.end(); snd_elements_it++ ) {
std::vector< Node > reasons;
- std::hash_set<Node, NodeHashFunction> seen;
+ std::unordered_set<Node, NodeHashFunction> seen;
Node tuple = RelsUtils::constructPair( tc_rel, getRepresentative( tc_graph_it->first ), getRepresentative( *snd_elements_it) );
Assert( rel_tc_graph_exps.find( tuple ) != rel_tc_graph_exps.end() );
Node exp = rel_tc_graph_exps.find( tuple )->second;
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 );
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 );
#ifndef SRC_THEORY_SETS_THEORY_SETS_RELS_H_
#define SRC_THEORY_SETS_THEORY_SETS_RELS_H_
-#include "theory/theory.h"
-#include "theory/uf/equality_engine.h"
-#include "context/cdhashset.h"
+#include <unordered_set>
+
#include "context/cdchunk_list.h"
+#include "context/cdhashset.h"
#include "theory/sets/rels_utils.h"
+#include "theory/theory.h"
+#include "theory/uf/equality_engine.h"
namespace CVC4 {
namespace theory {
std::map< Node, Node > d_pending_facts;
- std::hash_set< Node, NodeHashFunction > d_rel_nodes;
+ std::unordered_set< Node, NodeHashFunction > d_rel_nodes;
std::map< Node, std::vector<Node> > d_tuple_reps;
std::map< Node, TupleTrie > d_membership_trie;
/** Symbolic tuple variables that has been reduced to concrete ones */
- std::hash_set< Node, NodeHashFunction > d_symbolic_tuples;
+ std::unordered_set< Node, NodeHashFunction > d_symbolic_tuples;
/** Mapping between relation and its member representatives */
std::map< Node, std::vector< Node > > d_rReps_memberReps_cache;
std::map< Node, std::map<kind::Kind_t, std::vector<Node> > > d_terms_cache;
/** Mapping between transitive closure relation TC(r) and its TC graph constructed based on the members of r*/
- std::map< Node, std::map< Node, std::hash_set<Node, NodeHashFunction> > > d_rRep_tcGraph;
- std::map< Node, std::map< Node, std::hash_set<Node, NodeHashFunction> > > d_tcr_tcGraph;
+ std::map< Node, std::map< Node, std::unordered_set<Node, NodeHashFunction> > > d_rRep_tcGraph;
+ std::map< Node, std::map< Node, std::unordered_set<Node, NodeHashFunction> > > d_tcr_tcGraph;
std::map< Node, std::map< Node, Node > > d_tcr_tcGraph_exps;
std::map< Node, std::vector< Node > > d_tc_lemmas_last;
void applyTCRule( Node mem, Node rel, Node rel_rep, Node exp);
void buildTCGraphForRel( Node tc_rel );
void doTCInference();
- void doTCInference( std::map< Node, std::hash_set<Node, NodeHashFunction> > rel_tc_graph, std::map< Node, Node > rel_tc_graph_exps, Node tc_rel );
- void doTCInference(Node tc_rel, std::vector< Node > reasons, std::map< Node, std::hash_set< Node, NodeHashFunction > >& tc_graph,
- std::map< Node, Node >& rel_tc_graph_exps, Node start_node_rep, Node cur_node_rep, std::hash_set< Node, NodeHashFunction >& seen );
+ void doTCInference( std::map< Node, std::unordered_set<Node, NodeHashFunction> > rel_tc_graph, std::map< Node, Node > rel_tc_graph_exps, Node tc_rel );
+ void doTCInference(Node tc_rel, std::vector< Node > reasons, std::map< Node, std::unordered_set< Node, NodeHashFunction > >& tc_graph,
+ std::map< Node, Node >& rel_tc_graph_exps, Node start_node_rep, Node cur_node_rep, std::unordered_set< Node, NodeHashFunction >& seen );
void composeMembersForRels( Node );
void computeMembersForBinOpRel( Node );
void computeMembersForJoinImageTerm( Node );
bool isTCReachable( Node mem_rep, Node tc_rel );
- void isTCReachable( Node start, Node dest, std::hash_set<Node, NodeHashFunction>& hasSeen,
- std::map< Node, std::hash_set< Node, NodeHashFunction > >& tc_graph, bool& isReachable );
+ void isTCReachable( Node start, Node dest, std::unordered_set<Node, NodeHashFunction>& hasSeen,
+ std::map< Node, std::unordered_set< Node, NodeHashFunction > >& tc_graph, bool& isReachable );
void addSharedTerm( TNode n );
namespace sets {
typedef std::set<TNode> Elements;
-typedef std::hash_map<TNode, Elements, TNodeHashFunction> SettermElementsMap;
+typedef std::unordered_map<TNode, Elements, TNodeHashFunction> SettermElementsMap;
struct FlattenedNodeTag {};
typedef expr::Attribute<FlattenedNodeTag, bool> flattened;
return RewriteResponse(REWRITE_DONE, n);
}
- typedef std::hash_set<TNode, TNodeHashFunction> node_set;
+ typedef std::unordered_set<TNode, TNodeHashFunction> node_set;
node_set visited;
visited.insert(skipNode);
#pragma once
+#include <unordered_map>
+
#include "context/cdhashset.h"
#include "expr/node.h"
#include "theory/theory.h"
IntStat d_statSharedTerms;
// Needs to be a map from Nodes as after a backtrack they might not exist
- typedef std::hash_map<Node, shared_terms_list, TNodeHashFunction> SharedTermsMap;
+ typedef std::unordered_map<Node, shared_terms_list, TNodeHashFunction> SharedTermsMap;
/** A map from atoms to a list of shared terms */
SharedTermsMap d_atomsToTerms;
#ifndef __CVC4__THEORY__SUBSTITUTIONS_H
#define __CVC4__THEORY__SUBSTITUTIONS_H
+//#include <algorithm>
#include <utility>
#include <vector>
-#include <algorithm>
+#include <unordered_map>
#include "expr/node.h"
#include "context/context.h"
private:
- typedef std::hash_map<Node, Node, NodeHashFunction> NodeCache;
+ typedef std::unordered_map<Node, Node, NodeHashFunction> NodeCache;
/** The variables, in order of addition */
NodeMap d_substitutions;
#include "context/context.h"
#include "theory/shared_terms_database.h"
-#include <ext/hash_map>
+#include <unordered_map>
namespace CVC4 {
/**
* Cache from preprocessing of atoms.
*/
- typedef std::hash_map<TNode, theory::Theory::Set, TNodeHashFunction> TNodeVisitedMap;
+ typedef std::unordered_map<TNode, theory::Theory::Set, TNodeHashFunction> TNodeVisitedMap;
TNodeVisitedMap d_visited;
/**
printFacts(DebugChannel.getStream());
}
-std::hash_set<TNode, TNodeHashFunction> Theory::currentlySharedTerms() const{
- std::hash_set<TNode, TNodeHashFunction> currentlyShared;
+std::unordered_set<TNode, TNodeHashFunction> Theory::currentlySharedTerms() const{
+ std::unordered_set<TNode, TNodeHashFunction> currentlyShared;
for (shared_terms_iterator i = shared_terms_begin(),
i_end = shared_terms_end(); i != i_end; ++i) {
currentlyShared.insert (*i);
#ifndef __CVC4__THEORY__THEORY_H
#define __CVC4__THEORY__THEORY_H
-#include <ext/hash_set>
#include <iosfwd>
#include <map>
#include <set>
#include <string>
+#include <unordered_set>
#include "context/cdlist.h"
#include "context/cdhashset.h"
* This is a utility function for constructing a copy of the currently shared terms
* in a queriable form. As this is
*/
- std::hash_set<TNode, TNodeHashFunction> currentlySharedTerms() const;
+ std::unordered_set<TNode, TNodeHashFunction> currentlySharedTerms() const;
/**
* This allows the theory to be queried for whether a literal, lit, is
struct AtomsCollect {
std::vector<TNode> d_atoms;
- std::hash_set<TNode, TNodeHashFunction> d_visited;
+ std::unordered_set<TNode, TNodeHashFunction> d_visited;
public:
#include <deque>
#include <set>
+#include <unordered_map>
#include <vector>
#include <utility>
theory::TheoryEngineModelBuilder* d_curr_model_builder;
bool d_aloc_curr_model_builder;
- typedef std::hash_map<Node, Node, NodeHashFunction> NodeMap;
- typedef std::hash_map<TNode, Node, TNodeHashFunction> TNodeMap;
+ typedef std::unordered_map<Node, Node, NodeHashFunction> NodeMap;
+ typedef std::unordered_map<TNode, Node, TNodeHashFunction> TNodeMap;
/**
* Cache for theory-preprocessing of assertions
Node TheoryModel::getModelValue(TNode n, bool hasBoundVars, bool useDontCares) const
{
- std::hash_map<Node, Node, NodeHashFunction>::iterator it = d_modelCache.find(n);
+ std::unordered_map<Node, Node, NodeHashFunction>::iterator it = d_modelCache.find(n);
if (it != d_modelCache.end()) {
return (*it).second;
}
#ifndef __CVC4__THEORY__THEORY_MODEL_H
#define __CVC4__THEORY__THEORY_MODEL_H
+#include <unordered_map>
+#include <unordered_set>
+
#include "smt/model.h"
#include "theory/uf/equality_engine.h"
#include "theory/rep_set.h"
/** true/false nodes */
Node d_true;
Node d_false;
- mutable std::hash_map<Node, Node, NodeHashFunction> d_modelCache;
+ mutable std::unordered_map<Node, Node, NodeHashFunction> d_modelCache;
public:
/** comment stream to include in printing */
std::stringstream d_comment_str;
*/
class TypeSet {
public:
- typedef std::hash_map<TypeNode, std::set<Node>*, TypeNodeHashFunction> TypeSetMap;
- typedef std::hash_map<TypeNode, TypeEnumerator*, TypeNodeHashFunction> TypeToTypeEnumMap;
+ typedef std::unordered_map<TypeNode, std::set<Node>*, TypeNodeHashFunction> TypeSetMap;
+ typedef std::unordered_map<TypeNode, TypeEnumerator*, TypeNodeHashFunction> TypeToTypeEnumMap;
typedef TypeSetMap::iterator iterator;
typedef TypeSetMap::const_iterator const_iterator;
private:
protected:
/** pointer to theory engine */
TheoryEngine* d_te;
- typedef std::hash_map<Node, Node, NodeHashFunction> NodeMap;
+ typedef std::unordered_map<Node, Node, NodeHashFunction> NodeMap;
NodeMap d_normalizedCache;
- typedef std::hash_set<Node, NodeHashFunction> NodeSet;
+ typedef std::unordered_set<Node, NodeHashFunction> NodeSet;
std::map< Node, Node > d_constantReps;
/** process build model */
#pragma once
#include <deque>
-#include <ext/hash_map>
#include <queue>
+#include <unordered_map>
#include <vector>
#include "base/output.h"
std::map<unsigned, const PathReconstructionNotify*> d_pathReconstructionTriggers;
/** Map from nodes to their ids */
- __gnu_cxx::hash_map<TNode, EqualityNodeId, TNodeHashFunction> d_nodeIds;
+ std::unordered_map<TNode, EqualityNodeId, TNodeHashFunction> d_nodeIds;
/** Map from function applications to their ids */
- typedef __gnu_cxx::hash_map<FunctionApplication, EqualityNodeId, FunctionApplicationHashFunction> ApplicationIdsMap;
+ typedef std::unordered_map<FunctionApplication, EqualityNodeId, FunctionApplicationHashFunction> ApplicationIdsMap;
/**
* A map from a pair (a', b') to a function application f(a, b), where a' and b' are the current representatives
*/
std::vector<TriggerTermSetRef> d_nodeIndividualTrigger;
- typedef std::hash_map<EqualityPair, DisequalityReasonRef, EqualityPairHashFunction> DisequalityReasonsMap;
+ typedef std::unordered_map<EqualityPair, DisequalityReasonRef, EqualityPairHashFunction> DisequalityReasonsMap;
/**
* A map from pairs of disequal terms, to the reason why we deduced they are disequal.
}
TNode SymmetryBreaker::Template::find(TNode n) {
- hash_map<TNode, TNode, TNodeHashFunction>::iterator i = d_reps.find(n);
+ unordered_map<TNode, TNode, TNodeHashFunction>::iterator i = d_reps.find(n);
if(i == d_reps.end()) {
return n;
} else {
break;
}
}
- hash_map<TNode, set<TNode>, TNodeHashFunction>& ps = t.partitions();
- for(hash_map<TNode, set<TNode>, TNodeHashFunction>::iterator i = ps.begin();
+ unordered_map<TNode, set<TNode>, TNodeHashFunction>& ps = t.partitions();
+ for(unordered_map<TNode, set<TNode>, TNodeHashFunction>::iterator i = ps.begin();
i != ps.end();
++i) {
Debug("ufsymm") << "UFSYMM partition*: " << (*i).first;
}
if(!d_template.match(phi)) {
// we hit a bad match, extract the partitions and reset the template
- hash_map<TNode, set<TNode>, TNodeHashFunction>& ps = d_template.partitions();
+ unordered_map<TNode, set<TNode>, TNodeHashFunction>& ps = d_template.partitions();
Debug("ufsymm") << "UFSYMM hit a bad match---have " << ps.size() << " partitions:" << endl;
- for(hash_map<TNode, set<TNode>, TNodeHashFunction>::iterator i = ps.begin();
+ for(unordered_map<TNode, set<TNode>, TNodeHashFunction>::iterator i = ps.begin();
i != ps.end();
++i) {
Debug("ufsymm") << "UFSYMM partition: " << (*i).first;
#include <iostream>
#include <list>
+#include <unordered_map>
#include <vector>
#include "context/cdlist.h"
class Template {
Node d_template;
NodeBuilder<> d_assertions;
- std::hash_map<TNode, std::set<TNode>, TNodeHashFunction> d_sets;
- std::hash_map<TNode, TNode, TNodeHashFunction> d_reps;
+ std::unordered_map<TNode, std::set<TNode>, TNodeHashFunction> d_sets;
+ std::unordered_map<TNode, TNode, TNodeHashFunction> d_reps;
TNode find(TNode n);
bool matchRecursive(TNode t, TNode n);
public:
Template();
bool match(TNode n);
- std::hash_map<TNode, std::set<TNode>, TNodeHashFunction>& partitions() { return d_sets; }
+ std::unordered_map<TNode, std::set<TNode>, TNodeHashFunction>& partitions() { return d_sets; }
Node assertions() {
switch(d_assertions.getNumChildren()) {
case 0: return Node::null();
typedef TNode Term;
typedef std::list<Term> Terms;
typedef std::set<Term> TermEq;
- typedef std::hash_map<Term, TermEq, TNodeHashFunction> TermEqs;
+ typedef std::unordered_map<Term, TermEq, TNodeHashFunction> TermEqs;
private:
Permutations d_permutations;
Terms d_terms;
Template d_template;
- std::hash_map<Node, Node, NodeHashFunction> d_normalizationCache;
+ std::unordered_map<Node, Node, NodeHashFunction> d_normalizationCache;
TermEqs d_termEqs;
TermEqs d_termEqsOnly;
vector<TNode> workList;
workList.push_back(n);
- __gnu_cxx::hash_set<TNode, TNodeHashFunction> processed;
+ std::unordered_set<TNode, TNodeHashFunction> processed;
while(!workList.empty()) {
n = workList.back();
#ifndef __CVC4__UNCONSTRAINED_SIMPLIFIER_H
#define __CVC4__UNCONSTRAINED_SIMPLIFIER_H
-#include <vector>
+#include <unordered_map>
+#include <unordered_set>
#include <utility>
+#include <vector>
#include "expr/node.h"
#include "theory/substitutions.h"
/** number of expressions eliminated due to unconstrained simplification */
IntStat d_numUnconstrainedElim;
- typedef std::hash_map<TNode, unsigned, TNodeHashFunction> TNodeCountMap;
- typedef std::hash_map<TNode, TNode, TNodeHashFunction> TNodeMap;
- typedef std::hash_set<TNode, TNodeHashFunction> TNodeSet;
+ typedef std::unordered_map<TNode, unsigned, TNodeHashFunction> TNodeCountMap;
+ typedef std::unordered_map<TNode, TNode, TNodeHashFunction> TNodeMap;
+ typedef std::unordered_set<TNode, TNodeHashFunction> TNodeSet;
TNodeCountMap d_visited;
TNodeMap d_visitedOnce;
#ifndef __CVC4__CACHE_H
#define __CVC4__CACHE_H
-#include <utility>
#include <functional>
+#include <unordered_map>
+#include <utility>
+#include <vector>
namespace CVC4 {
*/
template <class T, class U, class Hasher = std::hash<T> >
class Cache {
- typedef std::hash_map<T, U, Hasher> Map;
+ typedef std::unordered_map<T, U, Hasher> Map;
Map d_map;
std::vector<T> d_current;
typename Map::iterator d_result;
#ifndef __CVC4__HASH_H
#define __CVC4__HASH_H
-// in case it's not been declared as a namespace yet
-namespace __gnu_cxx {}
+#include <functional>
+#include <string>
-#include <ext/hash_map>
-#include <ext/hash_set>
-
-namespace __gnu_cxx {
+namespace std {
#ifdef CVC4_NEED_HASH_UINT64_T
// on some versions and architectures of GNU C++, we need a
};/* struct hash<uint64_t> */
#endif /* CVC4_NEED_HASH_UINT64_T */
-}/* __gnu_cxx namespace */
-
-// hackish: treat hash stuff as if it were in std namespace
-namespace std { using namespace __gnu_cxx; }
+}/* std namespace */
namespace CVC4 {
-struct StringHashFunction {
- size_t operator()(const std::string& str) const {
- return __gnu_cxx::hash<const char*>()(str.c_str());
- }
-};/* struct StringHashFunction */
template <class T, class U, class HashT = std::hash<T>, class HashU = std::hash<U> >
struct PairHashFunction {
#include "util/hash.h"
%}
-%rename(apply) CVC4::StringHashFunction::operator()(const std::string&) const;
-
%include "util/hash.h"
#define __CVC4__PROOF_H
#include <iosfwd>
-#include <ext/hash_map>
+#include <unordered_map>
namespace CVC4 {
class ProofLetCount;
struct ExprHashFunction;
-typedef __gnu_cxx::hash_map<Expr, ProofLetCount, ExprHashFunction> ProofLetMap;
+typedef std::unordered_map<Expr, ProofLetCount, ExprHashFunction> ProofLetMap;
class CVC4_PUBLIC Proof {
public:
#include "util/regexp.h"
+#include <algorithm>
#include <iomanip>
#include <iostream>
#ifndef __CVC4__REGEXP_H
#define __CVC4__REGEXP_H
-#include <vector>
-#include <string>
+#include <algorithm>
+#include <cassert>
+#include <functional>
#include <set>
#include <sstream>
-#include <cassert>
+#include <string>
+#include <vector>
#include "base/exception.h"
#include "util/hash.h"
struct CVC4_PUBLIC StringHashFunction {
size_t operator()(const ::CVC4::String& s) const {
- return __gnu_cxx::hash<const char*>()(s.toString().c_str());
+ return std::hash<std::string>()(s.toString());
}
};/* struct StringHashFunction */
#include <cxxtest/TestSuite.h>
+#include <unordered_set>
+
#include "expr/array_store_all.h"
#include "expr/expr_manager.h"
#include "expr/kind.h"
void testArraysInfinite() {
TypeEnumerator te(d_nm->mkArrayType(d_nm->integerType(), d_nm->integerType()));
- hash_set<Node, NodeHashFunction> elts;
+ unordered_set<Node, NodeHashFunction> elts;
for(size_t i = 0; i < 1000; ++i) {
TS_ASSERT( ! te.isFinished() );
Node elt = *te++;
projects / cvc5.git / commitdiff