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.

diff --git a/docs/CMakeLists.txt b/docs/CMakeLists.txt
index 23e3c2dd6b1c4f520ac3b95ca5dcc90c66fd470e..b08668afa464f4eb6d6c58365fc53bb392a399d4 100644 (file)
--- 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 ad4f177deab580ad4a0db6ed8b7a31199f2c530e..a2e9289279a46c114403dce798dd6f68150b84a1 100644 (file)
--- 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<datatype>`
-
-    * class :doc:`datatypeconstructor`
-
-      * class :ref:`DatatypeConstructor::const_iterator<datatypeconstructor>`
-
-    * 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<term>`
-
-    * enum :doc:`kind`
-
-    * enum :doc:`roundingmode`
-
-    * struct :ref:`KindHashFunction<kind>`
-
-    * struct :ref:`OpHashFunction<op>`
-
-    * struct :ref:`SortHashFunction<sort>`
-
-    * 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 <cvc5::api::CVC5ApiException>`
+  * class :cpp:class:`CVC5ApiRecoverableException <cvc5::api::CVC5ApiRecoverableException>`
+
+  * class :cpp:class:`Datatype <cvc5::api::Datatype>`
+
+    * class :cpp:class:`const_iterator <cvc5::api::Datatype::const_iterator>`
+
+  * class :cpp:class:`DatatypeConstructor <cvc5::api::DatatypeConstructor>`
+
+    * class :cpp:class:`const_iterator <cvc5::api::DatatypeConstructor::const_iterator>`
+  
+  * class :cpp:class:`DatatypeConstructorDecl <cvc5::api::DatatypeConstructorDecl>`
+  * class :cpp:class:`DatatypeDecl <cvc5::api::DatatypeDecl>`
+  * class :cpp:class:`DatatypeSelector <cvc5::api::DatatypeSelector>`
+
+  * class :cpp:class:`Grammar <cvc5::api::Grammar>`
+
+  * enum :cpp:enum:`Kind <cvc5::api::Kind>`
+  
+  * class :cpp:class:`Op <cvc5::api::Op>`
+
+  * class :cpp:class:`Result <cvc5::api::Result>`
+
+    * enum :cpp:enum:`UnknownExplanation <cvc5::api::Result::UnknownExplanation>`
+
+  * enum :cpp:enum:`RoundingMode <cvc5::api::RoundingMode>`
+  
+  * class :cpp:class:`Solver <cvc5::api::Solver>`
+
+  * class :cpp:class:`Sort <cvc5::api::Sort>`
+
+  * class :cpp:class:`Stat <cvc5::api::Stat>`
+
+  * class :cpp:class:`Statistics <cvc5::api::Statistics>`
+  
+  * class :cpp:class:`Term <cvc5::api::Term>`
+
+    * class :cpp:class:`const_iterator <cvc5::api::Term::const_iterator>`

diff --git a/docs/cpp/kind.rst b/docs/cpp/kind.rst
index 2f74ee5fe39f6f1c9f24de34ab09cbbb7393b544..579407c8542f44e5bd793ff4108b9020ace4f97e 100644 (file)
--- 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 cee7a1920678525a63c9729950cb600b76acbc70..a320125a2caf66ef10745625d6a7881c7efde29c 100644 (file)
--- 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 fb7a01d79801f4e3c72df33a99994b17dd7b4fdf..a54d1a65c295037c8ffc52856ec10253a2a95f3d 100644 (file)
--- 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 64b631d633328a3884d06e08996b8bded07503ea..b19b82942a9267d467baeb2bddc93a9e47f7fd1c 100644 (file)
--- 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 c17d7494524fd99152c93709f1485d16bca2eb74..022c570b540ab1576bcfab997b198182230c22f8 100644 (file)
--- 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 c5472cdfe4794ffde8e727349391748105c92664..ce065a75f0408542039dde7204ee9b1d222e295d 100644 (file)
--- 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<Kind, cvc5::Kind, KindHashFunction> s_kinds{
+const static std::unordered_map<Kind, cvc5::Kind> 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<cvc5::Kind, Kind, cvc5::kind::KindHashFunction>
     };
 
 /* Set of kinds for indexed operators */
-const static std::unordered_set<Kind, KindHashFunction> s_indexed_kinds(
+const static std::unordered_set<Kind> 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<Term>& set)
   return out;
 }
 
-std::ostream& operator<<(
-    std::ostream& out,
-    const std::unordered_set<Term, TermHashFunction>& unordered_set)
+std::ostream& operator<<(std::ostream& out,
+                         const std::unordered_set<Term>& unordered_set)
 {
   container_to_stream(out, unordered_set);
   return out;
@@ -2772,19 +2752,13 @@ std::ostream& operator<<(std::ostream& out, const std::map<Term, V>& map)
 }
 
 template <typename V>
-std::ostream& operator<<(
-    std::ostream& out,
-    const std::unordered_map<Term, V, TermHashFunction>& unordered_map)
+std::ostream& operator<<(std::ostream& out,
+                         const std::unordered_map<Term, V>& 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<Term, Sort, TermHashFunction> ntsToUnres(d_ntSyms.size());
+  std::unordered_map<Term, Sort> 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<Term, Sort, TermHashFunction>& ntsToUnres) const
+    const std::unordered_map<Term, Sort>& ntsToUnres) const
 {
   CVC5_API_TRY_CATCH_BEGIN;
   CVC5_API_CHECK_DTDECL(dt);
@@ -3975,7 +3949,7 @@ Term Grammar::purifySygusGTerm(
     const Term& term,
     std::vector<Term>& args,
     std::vector<Sort>& cargs,
-    const std::unordered_map<Term, Sort, TermHashFunction>& ntsToUnres) const
+    const std::unordered_map<Term, Sort>& 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<Term, Sort, TermHashFunction>::const_iterator itn =
-      ntsToUnres.find(term);
+  std::unordered_map<Term, Sort>::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<RoundingMode, cvc5::RoundingMode, RoundingModeHashFunction>
-        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<RoundingMode, cvc5::RoundingMode> 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<cvc5::RoundingMode,
                                 RoundingMode,
@@ -4106,11 +4077,6 @@ const static std::unordered_map<cvc5::RoundingMode,
          ROUND_NEAREST_TIES_TO_AWAY},
     };
 
-size_t RoundingModeHashFunction::operator()(const RoundingMode& rm) const
-{
-  return size_t(rm);
-}
-
 /* -------------------------------------------------------------------------- */
 /* Statistics                                                                 */
 /* -------------------------------------------------------------------------- */
@@ -4169,7 +4135,8 @@ bool Stat::isString() const
 const std::string& Stat::getString() const
 {
   CVC5_API_TRY_CATCH_BEGIN;
-  CVC5_API_RECOVERABLE_CHECK(isString()) << "Expected Stat of type std::string.";
+  CVC5_API_RECOVERABLE_CHECK(isString())
+      << "Expected Stat of type std::string.";
   return std::get<std::string>(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<HistogramData>(d_data->data);
   CVC5_API_TRY_CATCH_END;
 }
@@ -4759,7 +4727,8 @@ void Solver::resetStatistics()
             "api::CONSTANT"),
         d_smtEngine->getStatisticsRegistry().registerHistogram<TypeConstant>(
             "api::VARIABLE"),
-        d_smtEngine->getStatisticsRegistry().registerHistogram<Kind>("api::TERM"),
+        d_smtEngine->getStatisticsRegistry().registerHistogram<Kind>(
+            "api::TERM"),
     });
   }
 }
@@ -7108,3 +7077,40 @@ Statistics Solver::getStatistics() const
 }  // namespace api
 
 }  // namespace cvc5
+
+namespace std {
+
+size_t hash<cvc5::api::Kind>::operator()(cvc5::api::Kind k) const
+{
+  return static_cast<size_t>(k);
+}
+
+size_t hash<cvc5::api::Op>::operator()(const cvc5::api::Op& t) const
+{
+  if (t.isIndexedHelper())
+  {
+    return cvc5::NodeHashFunction()(*t.d_node);
+  }
+  else
+  {
+    return std::hash<cvc5::api::Kind>()(t.d_kind);
+  }
+}
+
+size_t std::hash<cvc5::api::RoundingMode>::operator()(
+    cvc5::api::RoundingMode rm) const
+{
+  return static_cast<size_t>(rm);
+}
+
+size_t std::hash<cvc5::api::Sort>::operator()(const cvc5::api::Sort& s) const
+{
+  return cvc5::TypeNodeHashFunction()(*s.d_type);
+}
+
+size_t std::hash<cvc5::api::Term>::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 b3785c10efc5bf9f0307707efb09254cbcde1232..1e857085b53df17b8882e2d679b0e628f3081774 100644 (file)
--- 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<Sort>;
   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<cvc5::api::Sort>
 {
-  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<Op>;
 
  public:
   /**
@@ -889,6 +899,28 @@ class CVC5_EXPORT Op
   std::shared_ptr<cvc5::Node> 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<cvc5::api::Op>
+{
+  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<Term>;
 
  public:
   /**
@@ -1282,14 +1314,6 @@ class CVC5_EXPORT Term
   std::shared_ptr<cvc5::Node> 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<Term, TermHashFunction>&
-                             unordered_set) CVC5_EXPORT;
+                         const std::unordered_set<Term>& unordered_set)
+    CVC5_EXPORT;
 
 /**
  * Serialize a map of terms to the given stream.
@@ -1347,24 +1371,23 @@ std::ostream& operator<<(std::ostream& out,
  */
 template <typename V>
 std::ostream& operator<<(std::ostream& out,
-                         const std::unordered_map<Term, V, TermHashFunction>&
-                             unordered_map) CVC5_EXPORT;
+                         const std::unordered_map<Term, V>& 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<cvc5::api::Term>
 {
-  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<Term, Sort, TermHashFunction>& ntsToUnres) const;
+      const std::unordered_map<Term, Sort>& 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<Term>& args,
-      std::vector<Sort>& cargs,
-      const std::unordered_map<Term, Sort, TermHashFunction>& ntsToUnres) const;
+  Term purifySygusGTerm(const Term& term,
+                        std::vector<Term>& args,
+                        std::vector<Sort>& cargs,
+                        const std::unordered_map<Term, Sort>& 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<Term> d_ntSyms;
   /** The mapping from non-terminal symbols to their production terms. */
-  std::unordered_map<Term, std::vector<Term>, TermHashFunction> d_ntsToTerms;
+  std::unordered_map<Term, std::vector<Term>> d_ntsToTerms;
   /** The set of non-terminals that can be arbitrary constants. */
-  std::unordered_set<Term, TermHashFunction> d_allowConst;
+  std::unordered_set<Term> d_allowConst;
   /** The set of non-terminals that can be sygus variables. */
-  std::unordered_set<Term, TermHashFunction> d_allowVars;
+  std::unordered_set<Term> 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<cvc5::api::RoundingMode>
 {
-  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<Random> 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 7d0f7b9b7e30d47ffbd9840d134d05121ce05201..f7658412cdc2ab416543614641e12811823cc38c 100644 (file)
--- 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<cvc5::api::Kind>
 {
   /**
    * 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 83d811a1d7407d576398c8b21074041353389f89..6302b7e4332e2a99e4a0da631ebbb8db95bd2625 100644 (file)
--- a/src/api/python/cvc5.pxd
+++ b/src/api/python/cvc5.pxd
@@ -14,6 +14,12 @@ cdef extern from "<iostream>" namespace "std":
     ostream cout
 
 
+cdef extern from "<functional>" 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 0ee56cd55a5f98b703ca4429fff71c611269b02f..fb3a6b37772d6e96c2540cd8cd1c265bd9f397f8 100644 (file)
--- 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 4e9b7822b35171d15fe97347a8f7e2ce099a6bc4..c6eb8d08ef03d3e4ac425a60a0d6d22d0e846527 100644 (file)
--- a/src/expr/symbol_manager.cpp
+++ b/src/expr/symbol_manager.cpp
@@ -28,8 +28,8 @@ namespace cvc5 {
 
 class SymbolManager::Implementation
 {
-  using TermStringMap = CDHashMap<api::Term, std::string, api::TermHashFunction>;
-  using TermSet = CDHashSet<api::Term, api::TermHashFunction>;
+  using TermStringMap = CDHashMap<api::Term, std::string, std::hash<api::Term>>;
+  using TermSet = CDHashSet<api::Term, std::hash<api::Term>>;
   using SortList = CDList<api::Sort>;
   using TermList = CDList<api::Term>;
 

diff --git a/src/expr/symbol_table.cpp b/src/expr/symbol_table.cpp
index 9e1fe95823dcd8db4c5e5cff161f298f327c42f9..762120b5b619316229765261a293968e6ce90a4e 100644 (file)
--- 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<api::Term, api::TermHashFunction>(c)),
+            new (true) CDHashSet<api::Term, std::hash<api::Term>>(c)),
         d_allowFunctionVariants(allowFunVariants)
   {
   }
@@ -153,7 +153,7 @@ class OverloadedTypeTrie {
    * above. */
   std::unordered_map<std::string, TypeArgTrie> d_overload_type_arg_trie;
   /** The set of overloaded symbols. */
-  CDHashSet<api::Term, api::TermHashFunction>* d_overloaded_symbols;
+  CDHashSet<api::Term, std::hash<api::Term>>* 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 daeb5be5815a544debfd09c38f402f326e83bbf7..0be74c79d417ef97d1c32faafad54f108d63e271 100644 (file)
--- 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<api::Term, api::TermHashFunction> d_r_converted;
+  std::unordered_set<api::Term> d_r_converted;
   std::unordered_map<std::string, api::Term> d_distinct_objects;
 
   std::vector< pANTLR3_INPUT_STREAM > d_in_created;