diff options
author | makaimann <makaim@stanford.edu> | 2020-06-02 15:18:15 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-06-02 17:18:15 -0500 |
commit | 37d97be56ccba9c8da9b58fc5a7309ba2f4b1765 (patch) | |
tree | c8c30a02b0af26dca2f040e2799ef5812c905a6e /src/api | |
parent | 6ae4eda75d5717543f7c847d4b2f58ccbbb611bf (diff) |
Add hash Op, Sort and Term in Python bindings (#4498)
Diffstat (limited to 'src/api')
-rw-r--r-- | src/api/python/cvc4.pxd | 12 | ||||
-rw-r--r-- | src/api/python/cvc4.pxi | 18 |
2 files changed, 30 insertions, 0 deletions
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()) |