Cython `cdef` classes without an explicit `__init__` constructor have an
implicit `__init__` that accepts any number of arguments. (Python
classes, by contrast, default to an `__init__` that takes no arguments.)
This can lead to confusing situations where arguments appear to be
accepted but are discarded. This PR fixes the issue by adding explicit
`__init__` methods to the Cython classes.
Additionally, this PR removes some unnecessary field initializations in
the Cython classes.
This allows us to terminate quickly during preprocessing if a false assertion is encountered.
The other flags allow more generic handling of how to post-process results of check-sat.
This significantly refactors the internal result class. Entailments and "which" field are deleted, "Sat" is renamed to "Status". Moreover "TYPE_NONE" is made into a status.
Simplifies the usage of this class throughout the code.
It also changes the API Result method isSatUnknown to isUnknown.
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)
