Adds necessary API methods for supporting abstract sorts in the cpp, java, python APIs.
An abstract sort represents a class of sorts. It is parameterized by a kind. For example, the abstract sort parameterized by the kind BITVECTOR_SORT denotes bitvectors of unspecified bit-width.
To support the above functionality, the kinds of Sort must be exported in the API, which is done in this PR.
This is the first step towards supporting the rewrite DSL for parameterized sorts, and planned SyGuS extensions that use gradual typing.
This PR addresses a few issues in the Python API:
the implementation of defineFunsRec() lacked the call to the C++ function
a bunch of tests for defineFunsRec() were missing
the test for getInstantiations() was incorrectly named and thus not valled.
add missing test for hashing of Sort
This PR removes the expand_list_arg decorator from the python API. It was used to allow calling a function f(x, *args) with a list as second argument and automatically expand the list into *args. While it merely allows for calling f(x, l) instead of f(x, *l), it adds considerable complexity to the code and documentation. Thus, following the Zen of python (have only one way to do it) we remove this decorator. This is also consistent with the pythonic API, were we made the same decision.
This adds a function to retrieve the sort arguments an instantiated
sort has been instantiated with. It further deletes
Sort::getDatatypeParamSorts() and
Sort::getUninterpretedSortParamSorts().
Previously, Sort::isParametricDatatype() returned true for both
instantiated and non-instantiated parametric datatypes.
This deletes the method, instead one can check getDatatype().isParametric(). Parametric datatypes will be distinguished from instantiated parametric datatypes via a forthcoming method Sort::isInstantiated.
Co-authored-by: ajreynol <andrew.j.reynolds@gmail.com>
Removes checkEntailed from Solver.
Removes isEntailed, isNotEntailed, isEntailedUnknown from Result.
Removes isSubsortOf, isFunctionLike, getUninterpretedSortName, getSortConstructorName from Sort.
Updates examples and unit tests.
Since we do not support arithmetic subtyping on the API level anymore,
this function is obsolete. Consequently, this now requires that
replacement terms as arguments to Term::substitute() are of the same
sort as the replaced terms.
This PR does multiple things:
- the kinds are changed from custom objects to a proper enum.Enum class
(including according changes to the cython code and the kind generation scripts)
- all examples and tests are modified to account for the change how to use kinds
(Kind instead of kinds)
- add docstrings to the kind enum values
- add a custom documenter that properly renders enums via autodoc
- extend doxygen setup so that we can write comments as rst (allowing us to copy
the documentation for kinds from the cpp api to the other apis)
