diff options
Diffstat (limited to 'src/api/python')
| -rw-r--r-- | src/api/python/cvc5.pxd | 6 | ||||
| -rw-r--r-- | src/api/python/cvc5.pxi | 17 |
2 files changed, 23 insertions, 0 deletions
diff --git a/src/api/python/cvc5.pxd b/src/api/python/cvc5.pxd index b91a9e9c5..a044c79f5 100644 --- a/src/api/python/cvc5.pxd +++ b/src/api/python/cvc5.pxd @@ -341,6 +341,11 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api": Term() bint operator==(const Term&) except + bint operator!=(const Term&) except + + bint operator<(const Term&) except + + bint operator>(const Term&) except + + bint operator<=(const Term&) except + + bint operator>=(const Term&) except + + size_t getNumChildren() except + Term operator[](size_t idx) except + uint64_t getId() except + Kind getKind() except + @@ -367,6 +372,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 + cdef cppclass TermHashFunction: TermHashFunction() except + diff --git a/src/api/python/cvc5.pxi b/src/api/python/cvc5.pxi index fc14c1fca..a512a17a8 100644 --- a/src/api/python/cvc5.pxi +++ b/src/api/python/cvc5.pxi @@ -1460,6 +1460,18 @@ cdef class Term: def __ne__(self, Term other): return self.cterm != other.cterm + def __lt__(self, Term other): + return self.cterm < other.cterm + + def __gt__(self, Term other): + return self.cterm > other.cterm + + def __le__(self, Term other): + return self.cterm <= other.cterm + + def __ge__(self, Term other): + return self.cterm >= other.cterm + def __getitem__(self, int index): cdef Term term = Term(self.solver) if index >= 0: @@ -1483,6 +1495,8 @@ cdef class Term: def __hash__(self): return ctermhash(self.cterm) + def getNumChildren(self): + return self.cterm.getNumChildren() def getId(self): return self.cterm.getId() @@ -1584,6 +1598,9 @@ cdef class Term: term.cterm = self.cterm.iteTerm(then_t.cterm, else_t.cterm) return term + def isInteger(self): + return self.cterm.isInteger() + def toPythonObj(self): ''' Converts a constant value Term to a Python object. |