projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: f845c04) | patch
[Python API] Add missing methods to Datatype/Term (#4998)
authorAndres Noetzli <andres.noetzli@gmail.com>
Wed, 2 Sep 2020 21:02:26 +0000 (14:02 -0700)
committerGitHub <noreply@github.com>
Wed, 2 Sep 2020 21:02:26 +0000 (16:02 -0500)
commit0f9fb31069d51e003a39b0e93f506324dec2bdac
treee59f8a6d5a6290ad7e4d83abc2c721c5efd6757ftree
parentf845c04a147021937f1b0a942ee2080df950cda3commit | diff
[Python API] Add missing methods to Datatype/Term (#4998)

Fixes #4942. The Python API was missing some methods related to
datatypes. Most importantly, it was missing mkDatatypeSorts, which
meant that datatypes with unresolved placeholders could not be resolved.
This commit adds missing methods and ports the corresponding tests of
datatype_api_black.h to Python. The commit also adds support for
__getitem__ in Term.
src/api/cvc4cpp.cpp diff | blob | history
src/api/cvc4cpp.h diff | blob | history
src/api/python/cvc4.pxd diff | blob | history
src/api/python/cvc4.pxi diff | blob | history
test/unit/api/python/test_datatype_api.py [new file with mode: 0644] blob
test/unit/api/python/test_term.py diff | blob | history