diff options
| author | yoni206 <yoni206@users.noreply.github.com> | 2021-06-01 14:24:43 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-06-01 21:24:43 +0000 |
| commit | 172573dba45f7d231ec06a3a3992f41cf794b75e (patch) | |
| tree | c2c5b893f0555c68f8051831d70efcf6b8e2928f /src/api/python/cvc5.pxd | |
| parent | 7eff8fb5145752b100a9d04c834973e794d9a860 (diff) | |
Some additions to the datatypes python API (#6640)
This commit makes the following additions, in order to sync the python API with the cpp API.
1. adding `getName` functions to datatypes related classes
2. allowing `mkDatatypeSorts` with 1 or 2 arguments (previously allowed only 2).
3. In case there is a second argument to `mkDatatypeSorts`, we make sure it is a set.
4. Corresponding changes to the tests.
Diffstat (limited to 'src/api/python/cvc5.pxd')
| -rw-r--r-- | src/api/python/cvc5.pxd | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/api/python/cvc5.pxd b/src/api/python/cvc5.pxd index 87a646666..fdcbfa997 100644 --- a/src/api/python/cvc5.pxd +++ b/src/api/python/cvc5.pxd @@ -49,6 +49,7 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api": DatatypeConstructor getConstructor(const string& name) except + Term getConstructorTerm(const string& name) except + DatatypeSelector getSelector(const string& name) except + + string getName() except + size_t getNumConstructors() except + bint isParametric() except + bint isCodatatype() except + @@ -100,6 +101,7 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api": size_t getNumConstructors() except + bint isParametric() except + string toString() except + + string getName() except + cdef cppclass DatatypeSelector: |