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.

5 files changed, 150 insertions, 106 deletions

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<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 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<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:
   /**
@@ -1283,14 +1315,6 @@ class CVC5_EXPORT Term
 };
 
 /**
- * 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
  * @param t the term to be serialized to the given 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 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<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 83d811a1d..6302b7e43 100644
--- 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 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: