diff options
author | yoni206 <yoni206@users.noreply.github.com> | 2021-05-12 22:32:55 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-05-13 05:32:55 +0000 |
commit | 304064c6bb3bf7ea7a7d54b66e2ad152e8fc4525 (patch) | |
tree | cb33046f6006c7da77ed1b39909ab3148e414bbd /src | |
parent | b837f24d835ce529c749a089ae0e29e471512512 (diff) |
Adding functions to the python API and testing them -- part 2 (#6517)
This PR adds some functions that are missing in the python API, along with unit tests for them.
The unit tests are translated from https://github.com/cvc5/cvc5/blob/master/test/unit/api/term_black.cpp
Diffstat (limited to 'src')
-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. |