From 20820daece2eaf340a944ff386ffbafed1b79b75 Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Tue, 27 Apr 2021 07:31:58 +0200 Subject: [PATCH] Use std::hash for API types (#6432) This PR replaces all api::*HashFunction objects by specializations of std::hash. std::hash is meant to be extended in this way, and it allows for a much cleaner usage of std::unordered_set and std::unordered_map with these types. --- docs/CMakeLists.txt | 1 + docs/cpp/cpp.rst | 100 ++++++++++++++---------------- docs/cpp/kind.rst | 4 +- docs/cpp/op.rst | 8 +-- docs/cpp/roundingmode.rst | 4 +- docs/cpp/sort.rst | 6 +- docs/cpp/term.rst | 6 +- src/api/cpp/cvc5.cpp | 118 +++++++++++++++++++----------------- src/api/cpp/cvc5.h | 109 +++++++++++++++++++++------------ src/api/cpp/cvc5_kind.h | 13 ++-- src/api/python/cvc5.pxd | 6 ++ src/api/python/cvc5.pxi | 10 ++- src/expr/symbol_manager.cpp | 4 +- src/expr/symbol_table.cpp | 4 +- src/parser/tptp/tptp.h | 2 +- 15 files changed, 215 insertions(+), 180 deletions(-) diff --git a/docs/CMakeLists.txt b/docs/CMakeLists.txt index 23e3c2dd6..b08668afa 100644 --- a/docs/CMakeLists.txt +++ b/docs/CMakeLists.txt @@ -31,6 +31,7 @@ add_custom_target(docs ALL -c ${CMAKE_CURRENT_BINARY_DIR} # Tell Breathe where to find the Doxygen output -Dbreathe_projects.cvc5=${CPP_DOXYGEN_XML_FOLDER} + -Dbreathe_projects.std=${CPP_DOXYGEN_XML_FOLDER} ${SPHINX_INPUT_DIR} ${SPHINX_OUTPUT_DIR} WORKING_DIRECTORY ${CMAKE_CURRENT_BINARY_DIR} COMMENT "Generating Sphinx Api docs") diff --git a/docs/cpp/cpp.rst b/docs/cpp/cpp.rst index ad4f177de..a2e928927 100644 --- a/docs/cpp/cpp.rst +++ b/docs/cpp/cpp.rst @@ -1,61 +1,6 @@ C++ API Documentation ===================== -Class Hierarchy ---------------- - -* namespace ``cvc5`` - - * namespace ``api`` - - * class :cpp:class:`cvc5::api::CVC4ApiException` - - * class :cpp:class:`cvc5::api::CVC4ApiRecoverableException` - - * class :doc:`datatype` - - * class :ref:`Datatype::const_iterator` - - * class :doc:`datatypeconstructor` - - * class :ref:`DatatypeConstructor::const_iterator` - - * class :doc:`datatypeconstructordecl` - - * class :doc:`datatypedecl` - - * class :doc:`datatypeselector` - - * class :doc:`grammar` - - * class :doc:`op` - - * class :doc:`result` - - * class :doc:`solver` - - * class :doc:`term` - - * class :ref:`Term::const_iterator` - - * enum :doc:`kind` - - * enum :doc:`roundingmode` - - * struct :ref:`KindHashFunction` - - * struct :ref:`OpHashFunction` - - * struct :ref:`SortHashFunction` - - * class :cpp:class:`cvc5::api::Statistics` - * class :cpp:class:`cvc5::api::Stat` - - - -Full API Documentation ----------------------- - .. toctree:: :maxdepth: 2 @@ -74,3 +19,48 @@ Full API Documentation sort statistics term + + +Class Hierarchy +--------------- + +* namespace ``cvc5::api`` + + * class :cpp:class:`CVC5ApiException ` + * class :cpp:class:`CVC5ApiRecoverableException ` + + * class :cpp:class:`Datatype ` + + * class :cpp:class:`const_iterator ` + + * class :cpp:class:`DatatypeConstructor ` + + * class :cpp:class:`const_iterator ` + + * class :cpp:class:`DatatypeConstructorDecl ` + * class :cpp:class:`DatatypeDecl ` + * class :cpp:class:`DatatypeSelector ` + + * class :cpp:class:`Grammar ` + + * enum :cpp:enum:`Kind ` + + * class :cpp:class:`Op ` + + * class :cpp:class:`Result ` + + * enum :cpp:enum:`UnknownExplanation ` + + * enum :cpp:enum:`RoundingMode ` + + * class :cpp:class:`Solver ` + + * class :cpp:class:`Sort ` + + * class :cpp:class:`Stat ` + + * class :cpp:class:`Statistics ` + + * class :cpp:class:`Term ` + + * class :cpp:class:`const_iterator ` diff --git a/docs/cpp/kind.rst b/docs/cpp/kind.rst index 2f74ee5fe..579407c85 100644 --- a/docs/cpp/kind.rst +++ b/docs/cpp/kind.rst @@ -16,7 +16,7 @@ to its corresponding internal kinds. .. doxygenenum:: cvc5::api::Kind :project: cvc5 -.. doxygenstruct:: cvc5::api::KindHashFunction - :project: cvc5 +.. doxygenstruct:: std::hash< cvc5::api::Kind > + :project: std :members: :undoc-members: diff --git a/docs/cpp/op.rst b/docs/cpp/op.rst index cee7a1920..a320125a2 100644 --- a/docs/cpp/op.rst +++ b/docs/cpp/op.rst @@ -1,11 +1,11 @@ Op == -.. doxygenstruct:: cvc5::api::OpHashFunction +.. doxygenclass:: cvc5::api::Op :project: cvc5 :members: - :undoc-members: -.. doxygenclass:: cvc5::api::Op - :project: cvc5 +.. doxygenstruct:: std::hash< cvc5::api::Op > + :project: std :members: + :undoc-members: diff --git a/docs/cpp/roundingmode.rst b/docs/cpp/roundingmode.rst index fb7a01d79..a54d1a65c 100644 --- a/docs/cpp/roundingmode.rst +++ b/docs/cpp/roundingmode.rst @@ -4,7 +4,7 @@ RoundingMode .. doxygenenum:: cvc5::api::RoundingMode :project: cvc5 -.. doxygenstruct:: cvc5::api::RoundingModeHashFunction - :project: cvc5 +.. doxygenstruct:: std::hash< cvc5::api::RoundingMode > + :project: std :members: :undoc-members: diff --git a/docs/cpp/sort.rst b/docs/cpp/sort.rst index 64b631d63..b19b82942 100644 --- a/docs/cpp/sort.rst +++ b/docs/cpp/sort.rst @@ -1,12 +1,12 @@ Sort ==== -.. doxygenstruct:: cvc5::api::SortHashFunction +.. doxygenclass:: cvc5::api::Sort :project: cvc5 :members: :undoc-members: -.. doxygenclass:: cvc5::api::Sort - :project: cvc5 +.. doxygenstruct:: std::hash< cvc5::api::Sort > + :project: std :members: :undoc-members: diff --git a/docs/cpp/term.rst b/docs/cpp/term.rst index c17d74945..022c570b5 100644 --- a/docs/cpp/term.rst +++ b/docs/cpp/term.rst @@ -1,12 +1,12 @@ Term ==== -.. doxygenstruct:: cvc5::api::TermHashFunction +.. doxygenclass:: cvc5::api::Term :project: cvc5 :members: :undoc-members: -.. doxygenclass:: cvc5::api::Term - :project: cvc5 +.. doxygenstruct:: std::hash< cvc5::api::Term > + :project: std :members: :undoc-members: diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp index c5472cdfe..ce065a75f 100644 --- a/src/api/cpp/cvc5.cpp +++ b/src/api/cpp/cvc5.cpp @@ -84,7 +84,7 @@ struct APIStatistics /* -------------------------------------------------------------------------- */ /* Mapping from external (API) kind to internal kind. */ -const static std::unordered_map s_kinds{ +const static std::unordered_map s_kinds{ {INTERNAL_KIND, cvc5::Kind::UNDEFINED_KIND}, {UNDEFINED_KIND, cvc5::Kind::UNDEFINED_KIND}, {NULL_EXPR, cvc5::Kind::NULL_EXPR}, @@ -658,7 +658,7 @@ const static std::unordered_map }; /* Set of kinds for indexed operators */ -const static std::unordered_set s_indexed_kinds( +const static std::unordered_set s_indexed_kinds( {RECORD_UPDATE, DIVISIBLE, IAND, @@ -785,8 +785,6 @@ std::ostream& operator<<(std::ostream& out, Kind k) return out; } -size_t KindHashFunction::operator()(Kind k) const { return k; } - /* -------------------------------------------------------------------------- */ /* API guard helpers */ /* -------------------------------------------------------------------------- */ @@ -1751,11 +1749,6 @@ std::ostream& operator<<(std::ostream& out, const Sort& s) return out; } -size_t SortHashFunction::operator()(const Sort& s) const -{ - return TypeNodeHashFunction()(*s.d_type); -} - /* Helpers */ /* -------------------------------------------------------------------------- */ @@ -2059,18 +2052,6 @@ std::ostream& operator<<(std::ostream& out, const Op& t) return out; } -size_t OpHashFunction::operator()(const Op& t) const -{ - if (t.isIndexedHelper()) - { - return NodeHashFunction()(*t.d_node); - } - else - { - return KindHashFunction()(t.d_kind); - } -} - /* Helpers */ /* -------------------------------------------------------------------------- */ @@ -2756,9 +2737,8 @@ std::ostream& operator<<(std::ostream& out, const std::set& set) return out; } -std::ostream& operator<<( - std::ostream& out, - const std::unordered_set& unordered_set) +std::ostream& operator<<(std::ostream& out, + const std::unordered_set& unordered_set) { container_to_stream(out, unordered_set); return out; @@ -2772,19 +2752,13 @@ std::ostream& operator<<(std::ostream& out, const std::map& map) } template -std::ostream& operator<<( - std::ostream& out, - const std::unordered_map& unordered_map) +std::ostream& operator<<(std::ostream& out, + const std::unordered_map& unordered_map) { container_to_stream(out, unordered_map); return out; } -size_t TermHashFunction::operator()(const Term& t) const -{ - return NodeHashFunction()(*t.d_node); -} - /* Helpers */ /* -------------------------------------------------------------------------- */ @@ -3874,7 +3848,7 @@ Sort Grammar::resolve() cvc5::kind::BOUND_VAR_LIST, Term::termVectorToNodes(d_sygusVars))); } - std::unordered_map ntsToUnres(d_ntSyms.size()); + std::unordered_map ntsToUnres(d_ntSyms.size()); for (Term ntsymbol : d_ntSyms) { @@ -3933,7 +3907,7 @@ Sort Grammar::resolve() void Grammar::addSygusConstructorTerm( DatatypeDecl& dt, const Term& term, - const std::unordered_map& ntsToUnres) const + const std::unordered_map& ntsToUnres) const { CVC5_API_TRY_CATCH_BEGIN; CVC5_API_CHECK_DTDECL(dt); @@ -3975,7 +3949,7 @@ Term Grammar::purifySygusGTerm( const Term& term, std::vector& args, std::vector& cargs, - const std::unordered_map& ntsToUnres) const + const std::unordered_map& ntsToUnres) const { CVC5_API_TRY_CATCH_BEGIN; CVC5_API_CHECK_TERM(term); @@ -3984,8 +3958,7 @@ Term Grammar::purifySygusGTerm( CVC5_API_CHECK_TERMS_MAP(ntsToUnres); //////// all checks before this line - std::unordered_map::const_iterator itn = - ntsToUnres.find(term); + std::unordered_map::const_iterator itn = ntsToUnres.find(term); if (itn != ntsToUnres.cend()) { Term ret = @@ -4081,17 +4054,15 @@ std::ostream& operator<<(std::ostream& out, const Grammar& grammar) /* Rounding Mode for Floating Points */ /* -------------------------------------------------------------------------- */ -const static std:: - unordered_map - s_rmodes{ - {ROUND_NEAREST_TIES_TO_EVEN, - cvc5::RoundingMode::ROUND_NEAREST_TIES_TO_EVEN}, - {ROUND_TOWARD_POSITIVE, cvc5::RoundingMode::ROUND_TOWARD_POSITIVE}, - {ROUND_TOWARD_NEGATIVE, cvc5::RoundingMode::ROUND_TOWARD_NEGATIVE}, - {ROUND_TOWARD_ZERO, cvc5::RoundingMode::ROUND_TOWARD_ZERO}, - {ROUND_NEAREST_TIES_TO_AWAY, - cvc5::RoundingMode::ROUND_NEAREST_TIES_TO_AWAY}, - }; +const static std::unordered_map s_rmodes{ + {ROUND_NEAREST_TIES_TO_EVEN, + cvc5::RoundingMode::ROUND_NEAREST_TIES_TO_EVEN}, + {ROUND_TOWARD_POSITIVE, cvc5::RoundingMode::ROUND_TOWARD_POSITIVE}, + {ROUND_TOWARD_NEGATIVE, cvc5::RoundingMode::ROUND_TOWARD_NEGATIVE}, + {ROUND_TOWARD_ZERO, cvc5::RoundingMode::ROUND_TOWARD_ZERO}, + {ROUND_NEAREST_TIES_TO_AWAY, + cvc5::RoundingMode::ROUND_NEAREST_TIES_TO_AWAY}, +}; const static std::unordered_map(d_data->data); CVC5_API_TRY_CATCH_END; } @@ -4180,7 +4147,8 @@ bool Stat::isHistogram() const const Stat::HistogramData& Stat::getHistogram() const { CVC5_API_TRY_CATCH_BEGIN; - CVC5_API_RECOVERABLE_CHECK(isHistogram()) << "Expected Stat of type histogram."; + CVC5_API_RECOVERABLE_CHECK(isHistogram()) + << "Expected Stat of type histogram."; return std::get(d_data->data); CVC5_API_TRY_CATCH_END; } @@ -4759,7 +4727,8 @@ void Solver::resetStatistics() "api::CONSTANT"), d_smtEngine->getStatisticsRegistry().registerHistogram( "api::VARIABLE"), - d_smtEngine->getStatisticsRegistry().registerHistogram("api::TERM"), + d_smtEngine->getStatisticsRegistry().registerHistogram( + "api::TERM"), }); } } @@ -7108,3 +7077,40 @@ Statistics Solver::getStatistics() const } // namespace api } // namespace cvc5 + +namespace std { + +size_t hash::operator()(cvc5::api::Kind k) const +{ + return static_cast(k); +} + +size_t hash::operator()(const cvc5::api::Op& t) const +{ + if (t.isIndexedHelper()) + { + return cvc5::NodeHashFunction()(*t.d_node); + } + else + { + return std::hash()(t.d_kind); + } +} + +size_t std::hash::operator()( + cvc5::api::RoundingMode rm) const +{ + return static_cast(rm); +} + +size_t std::hash::operator()(const cvc5::api::Sort& s) const +{ + return cvc5::TypeNodeHashFunction()(*s.d_type); +} + +size_t std::hash::operator()(const cvc5::api::Term& t) const +{ + return cvc5::NodeHashFunction()(*t.d_node); +} + +} // namespace std diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h index b3785c10e..1e857085b 100644 --- a/src/api/cpp/cvc5.h +++ b/src/api/cpp/cvc5.h @@ -260,7 +260,7 @@ class CVC5_EXPORT Sort friend class Op; friend class Solver; friend class Grammar; - friend struct SortHashFunction; + friend struct std::hash; friend class Term; public: @@ -751,14 +751,24 @@ class CVC5_EXPORT Sort */ std::ostream& operator<<(std::ostream& out, const Sort& s) CVC5_EXPORT; +} // namespace api +} // namespace cvc5 + +namespace std { + /** * Hash function for Sorts. */ -struct CVC5_EXPORT SortHashFunction +template <> +struct CVC5_EXPORT hash { - size_t operator()(const Sort& s) const; + size_t operator()(const cvc5::api::Sort& s) const; }; +} // namespace std + +namespace cvc5::api { + /* -------------------------------------------------------------------------- */ /* Op */ /* -------------------------------------------------------------------------- */ @@ -772,7 +782,7 @@ class CVC5_EXPORT Op { friend class Solver; friend class Term; - friend struct OpHashFunction; + friend struct std::hash; public: /** @@ -889,6 +899,28 @@ class CVC5_EXPORT Op std::shared_ptr d_node; }; +/** + * Serialize an operator to given stream. + * @param out the output stream + * @param t the operator to be serialized to the given output stream + * @return the output stream + */ +std::ostream& operator<<(std::ostream& out, const Op& t) CVC5_EXPORT; + +} // namespace cvc5::api + +namespace std { +/** + * Hash function for Ops. + */ +template <> +struct CVC5_EXPORT hash +{ + size_t operator()(const cvc5::api::Op& t) const; +}; +} // namespace std + +namespace cvc5::api { /* -------------------------------------------------------------------------- */ /* Term */ /* -------------------------------------------------------------------------- */ @@ -904,7 +936,7 @@ class CVC5_EXPORT Term friend class DatatypeSelector; friend class Solver; friend class Grammar; - friend struct TermHashFunction; + friend struct std::hash; public: /** @@ -1282,14 +1314,6 @@ class CVC5_EXPORT Term std::shared_ptr d_node; }; -/** - * Hash function for Terms. - */ -struct CVC5_EXPORT TermHashFunction -{ - size_t operator()(const Term& t) const; -}; - /** * Serialize a term to given stream. * @param out the output stream @@ -1324,8 +1348,8 @@ std::ostream& operator<<(std::ostream& out, * @return the output stream */ std::ostream& operator<<(std::ostream& out, - const std::unordered_set& - unordered_set) CVC5_EXPORT; + const std::unordered_set& unordered_set) + CVC5_EXPORT; /** * Serialize a map of terms to the given stream. @@ -1347,24 +1371,23 @@ std::ostream& operator<<(std::ostream& out, */ template std::ostream& operator<<(std::ostream& out, - const std::unordered_map& - unordered_map) CVC5_EXPORT; + const std::unordered_map& unordered_map) + CVC5_EXPORT; -/** - * Serialize an operator to given stream. - * @param out the output stream - * @param t the operator to be serialized to the given output stream - * @return the output stream - */ -std::ostream& operator<<(std::ostream& out, const Op& t) CVC5_EXPORT; +} // namespace cvc5::api +namespace std { /** - * Hash function for Ops. + * Hash function for Terms. */ -struct CVC5_EXPORT OpHashFunction +template <> +struct CVC5_EXPORT hash { - size_t operator()(const Op& t) const; + size_t operator()(const cvc5::api::Term& t) const; }; +} // namespace std + +namespace cvc5::api { /* -------------------------------------------------------------------------- */ /* Datatypes */ @@ -2206,7 +2229,7 @@ class CVC5_EXPORT Grammar void addSygusConstructorTerm( DatatypeDecl& dt, const Term& term, - const std::unordered_map& ntsToUnres) const; + const std::unordered_map& ntsToUnres) const; /** * Purify SyGuS grammar term. @@ -2226,11 +2249,10 @@ class CVC5_EXPORT Grammar * @param ntsToUnres mapping from non-terminals to their unresolved sorts * @return the purfied term */ - Term purifySygusGTerm( - const Term& term, - std::vector& args, - std::vector& cargs, - const std::unordered_map& ntsToUnres) const; + Term purifySygusGTerm(const Term& term, + std::vector& args, + std::vector& cargs, + const std::unordered_map& ntsToUnres) const; /** * This adds constructors to \p dt for sygus variables in \p d_sygusVars @@ -2257,11 +2279,11 @@ class CVC5_EXPORT Grammar /** The non-terminal symbols of this grammar. */ std::vector d_ntSyms; /** The mapping from non-terminal symbols to their production terms. */ - std::unordered_map, TermHashFunction> d_ntsToTerms; + std::unordered_map> d_ntsToTerms; /** The set of non-terminals that can be arbitrary constants. */ - std::unordered_set d_allowConst; + std::unordered_set d_allowConst; /** The set of non-terminals that can be sygus variables. */ - std::unordered_set d_allowVars; + std::unordered_set d_allowVars; /** Did we call resolve() before? */ bool d_isResolved; }; @@ -2328,13 +2350,20 @@ enum CVC5_EXPORT RoundingMode ROUND_NEAREST_TIES_TO_AWAY, }; +} // namespace cvc5::api + +namespace std { + /** * Hash function for RoundingModes. */ -struct CVC5_EXPORT RoundingModeHashFunction +template <> +struct CVC5_EXPORT hash { - inline size_t operator()(const RoundingMode& rm) const; + size_t operator()(cvc5::api::RoundingMode rm) const; }; +} // namespace std +namespace cvc5::api { /* -------------------------------------------------------------------------- */ /* Statistics */ @@ -4054,6 +4083,6 @@ class CVC5_EXPORT Solver std::unique_ptr d_rng; }; -} // namespace api -} // namespace cvc5 +} // namespace cvc5::api + #endif diff --git a/src/api/cpp/cvc5_kind.h b/src/api/cpp/cvc5_kind.h index 7d0f7b9b7..f7658412c 100644 --- a/src/api/cpp/cvc5_kind.h +++ b/src/api/cpp/cvc5_kind.h @@ -3441,18 +3441,23 @@ std::string kindToString(Kind k) CVC5_EXPORT; */ std::ostream& operator<<(std::ostream& out, Kind k) CVC5_EXPORT; +} // namespace api +} // namespace cvc5 + +namespace std { + /** * Hash function for Kinds. */ -struct CVC5_EXPORT KindHashFunction +template<> +struct CVC5_EXPORT hash { /** * Hashes a Kind to a size_t. */ - size_t operator()(Kind k) const; + size_t operator()(cvc5::api::Kind k) const; }; -} // namespace api -} // namespace cvc5 +} #endif diff --git a/src/api/python/cvc5.pxd b/src/api/python/cvc5.pxd index 83d811a1d..6302b7e43 100644 --- a/src/api/python/cvc5.pxd +++ b/src/api/python/cvc5.pxd @@ -14,6 +14,12 @@ cdef extern from "" namespace "std": ostream cout +cdef extern from "" namespace "std" nogil: + cdef cppclass hash[T]: + hash() + size_t operator()(T t) + + cdef extern from "api/cpp/cvc5.h" namespace "cvc5": cdef cppclass Options: pass diff --git a/src/api/python/cvc5.pxi b/src/api/python/cvc5.pxi index 0ee56cd55..fb3a6b377 100644 --- a/src/api/python/cvc5.pxi +++ b/src/api/python/cvc5.pxi @@ -18,16 +18,14 @@ from cvc5 cimport DatatypeSelector as c_DatatypeSelector from cvc5 cimport Result as c_Result from cvc5 cimport RoundingMode as c_RoundingMode from cvc5 cimport Op as c_Op -from cvc5 cimport OpHashFunction as c_OpHashFunction from cvc5 cimport Solver as c_Solver from cvc5 cimport Grammar as c_Grammar from cvc5 cimport Sort as c_Sort -from cvc5 cimport SortHashFunction as c_SortHashFunction from cvc5 cimport ROUND_NEAREST_TIES_TO_EVEN, ROUND_TOWARD_POSITIVE from cvc5 cimport ROUND_TOWARD_NEGATIVE, ROUND_TOWARD_ZERO from cvc5 cimport ROUND_NEAREST_TIES_TO_AWAY from cvc5 cimport Term as c_Term -from cvc5 cimport TermHashFunction as c_TermHashFunction +from cvc5 cimport hash as c_hash from cvc5kinds cimport Kind as c_Kind @@ -76,9 +74,9 @@ def expand_list_arg(num_req_args=0): ## Objects for hashing -cdef c_OpHashFunction cophash = c_OpHashFunction() -cdef c_SortHashFunction csorthash = c_SortHashFunction() -cdef c_TermHashFunction ctermhash = c_TermHashFunction() +cdef c_hash[c_Op] cophash = c_hash[c_Op]() +cdef c_hash[c_Sort] csorthash = c_hash[c_Sort]() +cdef c_hash[c_Term] ctermhash = c_hash[c_Term]() cdef class Datatype: diff --git a/src/expr/symbol_manager.cpp b/src/expr/symbol_manager.cpp index 4e9b7822b..c6eb8d08e 100644 --- a/src/expr/symbol_manager.cpp +++ b/src/expr/symbol_manager.cpp @@ -28,8 +28,8 @@ namespace cvc5 { class SymbolManager::Implementation { - using TermStringMap = CDHashMap; - using TermSet = CDHashSet; + using TermStringMap = CDHashMap>; + using TermSet = CDHashSet>; using SortList = CDList; using TermList = CDList; diff --git a/src/expr/symbol_table.cpp b/src/expr/symbol_table.cpp index 9e1fe9582..762120b5b 100644 --- a/src/expr/symbol_table.cpp +++ b/src/expr/symbol_table.cpp @@ -91,7 +91,7 @@ class OverloadedTypeTrie { public: OverloadedTypeTrie(Context* c, bool allowFunVariants = false) : d_overloaded_symbols( - new (true) CDHashSet(c)), + new (true) CDHashSet>(c)), d_allowFunctionVariants(allowFunVariants) { } @@ -153,7 +153,7 @@ class OverloadedTypeTrie { * above. */ std::unordered_map d_overload_type_arg_trie; /** The set of overloaded symbols. */ - CDHashSet* d_overloaded_symbols; + CDHashSet>* d_overloaded_symbols; /** allow function variants * This is true if we allow overloading (non-constant) functions that expect * the same argument types. diff --git a/src/parser/tptp/tptp.h b/src/parser/tptp/tptp.h index daeb5be58..0be74c79d 100644 --- a/src/parser/tptp/tptp.h +++ b/src/parser/tptp/tptp.h @@ -193,7 +193,7 @@ class Tptp : public Parser { api::Term d_utr_op; api::Term d_uts_op; // The set of expression that already have a bridge - std::unordered_set d_r_converted; + std::unordered_set d_r_converted; std::unordered_map d_distinct_objects; std::vector< pANTLR3_INPUT_STREAM > d_in_created; -- 2.30.2