This commit removes `Op::getIndices()`. As discussed offline, the
semantics of that method were confusing and the use cases are covered by
`Op::getNumIndices()` and `Op::operator[]()` (which mirror
`Term::getNumChildren()` and `Term::operator[]()`).
Future changes are going to update the Python and Java bindings to
support `Op::operator[]()`.
Removes checkEntailed from Solver.
Removes isEntailed, isNotEntailed, isEntailedUnknown from Result.
Removes isSubsortOf, isFunctionLike, getUninterpretedSortName, getSortConstructorName from Sort.
Updates examples and unit tests.
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)
This PR updates the update-copyright.pl script to also update/add copyright headers to CMake specific files. It further fixes a small typo in the header.
This renames api::Solver::checkValidAssuming to checkEntailed and
removes api::Solver::checkValid. Internally, SmtEngine::query is renamed
to SmtEngine::checkEntailed, and these changes are further propagated to
the Result class.
