diff options
| author | yoni206 <yoni206@users.noreply.github.com> | 2021-06-22 16:02:00 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-06-22 23:02:00 +0000 |
| commit | 39f90ff035a5e5024fe0cd11b965f1103d83e88d (patch) | |
| tree | 8aebfebd2801837e5ee79b902820ede73c674b0c /src | |
| parent | 40bee7cad0f2b6a5f9eac7e8fda2199e582e18d1 (diff) | |
python api unit tests for Op (#6785)
Unit tests are translated from https://github.com/cvc5/cvc5/blob/master/test/unit/api/op_black.cpp
to python.
The only thing that is not faithfully translated is that the `cpp` tests expect the template function `[getIndices](https://github.com/cvc5/cvc5/blob/master/src/api/cpp/cvc5.h#L841)` to fail when an inappropriate type is given to it, while in the [`python` API](https://github.com/cvc5/cvc5/blob/90d19f7cdbaf41e389bdcbd099471f658a35ce98/src/api/python/cvc5.pxi#L343) this function is not a template, but just tries every supported type.
For example, the following line is not translated:
https://github.com/cvc5/cvc5/blob/90d19f7cdbaf41e389bdcbd099471f658a35ce98/test/unit/api/op_black.cpp#L206
Diffstat (limited to 'src')
| -rw-r--r-- | src/api/python/cvc5.pxd | 1 | ||||
| -rw-r--r-- | src/api/python/cvc5.pxi | 5 |
2 files changed, 5 insertions, 1 deletions
diff --git a/src/api/python/cvc5.pxd b/src/api/python/cvc5.pxd index ada34e75d..99e471b0a 100644 --- a/src/api/python/cvc5.pxd +++ b/src/api/python/cvc5.pxd @@ -122,6 +122,7 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api": Sort getSort() except + bint isNull() except + bint isIndexed() except + + size_t getNumIndices() except + T getIndices[T]() except + string toString() except + diff --git a/src/api/python/cvc5.pxi b/src/api/python/cvc5.pxi index 7f01cb8a1..d31fdc126 100644 --- a/src/api/python/cvc5.pxi +++ b/src/api/python/cvc5.pxi @@ -345,10 +345,13 @@ cdef class Op: def isNull(self): return self.cop.isNull() + def getNumIndices(self): + return self.cop.getNumIndices() + def getIndices(self): indices = None try: - indices = self.cop.getIndices[string]() + indices = self.cop.getIndices[string]().decode() except: pass |