diff options
Diffstat (limited to 'src/api/python/cvc5.pxd')
| -rw-r--r-- | src/api/python/cvc5.pxd | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/src/api/python/cvc5.pxd b/src/api/python/cvc5.pxd index a044c79f5..24f8ac0a0 100644 --- a/src/api/python/cvc5.pxd +++ b/src/api/python/cvc5.pxd @@ -1,6 +1,7 @@ # import dereference and increment operators from cython.operator cimport dereference as deref, preincrement as inc from libc.stdint cimport int32_t, int64_t, uint32_t, uint64_t +from libc.stddef cimport wchar_t from libcpp.set cimport set from libcpp.string cimport string from libcpp.vector cimport vector @@ -19,6 +20,9 @@ cdef extern from "<functional>" namespace "std" nogil: hash() size_t operator()(T t) +cdef extern from "<string>" namespace "std": + cdef cppclass wstring: + wstring(const wchar_t*, size_t) except + cdef extern from "api/cpp/cvc5.h" namespace "cvc5": cdef cppclass Options: @@ -191,7 +195,7 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api": Term mkEmptySet(Sort s) except + Term mkSepNil(Sort sort) except + Term mkString(const string& s) except + - Term mkString(const vector[unsigned]& s) except + + Term mkString(const wstring& s) except + Term mkEmptySequence(Sort sort) except + Term mkUniverseSet(Sort sort) except + Term mkBitVector(uint32_t size) except + @@ -372,7 +376,7 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api": Term operator*() except + const_iterator begin() except + const_iterator end() except + - bint isInteger() except + + bint isIntegerValue() except + cdef cppclass TermHashFunction: TermHashFunction() except + |