From: makaimann <makaim@stanford.edu>
Date: Tue, 2 Jun 2020 22:18:15 +0000 (-0700)
Subject: Add hash Op, Sort and Term in Python bindings (#4498)
X-Git-Tag: cvc5-1.0.0~3270
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=37d97be56ccba9c8da9b58fc5a7309ba2f4b1765;p=cvc5.git

Add hash Op, Sort and Term in Python bindings (#4498)
---

diff --git a/src/api/python/cvc4.pxd b/src/api/python/cvc4.pxd
index d81d0c0bf..5bcc3c5c3 100644
--- a/src/api/python/cvc4.pxd
+++ b/src/api/python/cvc4.pxd
@@ -81,6 +81,10 @@ cdef extern from "api/cvc4cpp.h" namespace "CVC4::api":
         T getIndices[T]() except +
         string toString() except +
 
+    cdef cppclass OpHashFunction:
+        OpHashFunction() except +
+        size_t operator()(const Op & o) except +
+
 
     cdef cppclass Result:
     # Note: don't even need constructor
@@ -229,6 +233,10 @@ cdef extern from "api/cvc4cpp.h" namespace "CVC4::api":
         bint isUninterpretedSortParameterized() except +
         string toString() except +
 
+    cdef cppclass SortHashFunction:
+        SortHashFunction() except +
+        size_t operator()(const Sort & s) except +
+
     cdef cppclass Term:
         Term()
         bint operator==(const Term&) except +
@@ -255,6 +263,10 @@ cdef extern from "api/cvc4cpp.h" namespace "CVC4::api":
         const_iterator begin() except +
         const_iterator end() except +
 
+    cdef cppclass TermHashFunction:
+        TermHashFunction() except +
+        size_t operator()(const Term & t) except +
+
 
 cdef extern from "api/cvc4cpp.h" namespace "CVC4::api::RoundingMode":
     cdef RoundingMode ROUND_NEAREST_TIES_TO_EVEN,
diff --git a/src/api/python/cvc4.pxi b/src/api/python/cvc4.pxi
index 1489b34a6..080f24c8b 100644
--- a/src/api/python/cvc4.pxi
+++ b/src/api/python/cvc4.pxi
@@ -15,11 +15,14 @@ from cvc4 cimport DatatypeSelector as c_DatatypeSelector
 from cvc4 cimport Result as c_Result
 from cvc4 cimport RoundingMode as c_RoundingMode
 from cvc4 cimport Op as c_Op
+from cvc4 cimport OpHashFunction as c_OpHashFunction
 from cvc4 cimport Solver as c_Solver
 from cvc4 cimport Sort as c_Sort
+from cvc4 cimport SortHashFunction as c_SortHashFunction
 from cvc4 cimport ROUND_NEAREST_TIES_TO_EVEN, ROUND_TOWARD_POSITIVE
 from cvc4 cimport ROUND_TOWARD_ZERO, ROUND_NEAREST_TIES_TO_AWAY
 from cvc4 cimport Term as c_Term
+from cvc4 cimport TermHashFunction as c_TermHashFunction
 
 from cvc4kinds cimport Kind as c_Kind
 
@@ -52,6 +55,12 @@ def expand_list_arg(num_req_args=0):
 #### Result class can have default because it's pure python
 
 
+## Objects for hashing
+cdef c_OpHashFunction cophash = c_OpHashFunction()
+cdef c_SortHashFunction csorthash = c_SortHashFunction()
+cdef c_TermHashFunction ctermhash = c_TermHashFunction()
+
+
 cdef class Datatype:
     cdef c_Datatype cd
     def __cinit__(self):
@@ -188,6 +197,9 @@ cdef class Op:
     def __repr__(self):
         return self.cop.toString().decode()
 
+    def __hash__(self):
+        return cophash(self.cop)
+
     def getKind(self):
         return kind(<int> self.cop.getKind())
 
@@ -953,6 +965,9 @@ cdef class Sort:
     def __repr__(self):
         return self.csort.toString().decode()
 
+    def __hash__(self):
+        return csorthash(self.csort)
+
     def isBoolean(self):
         return self.csort.isBoolean()
 
@@ -1054,6 +1069,9 @@ cdef class Term:
             term.cterm = ci
             yield term
 
+    def __hash__(self):
+        return ctermhash(self.cterm)
+
     def getKind(self):
         return kind(<int> self.cterm.getKind())