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.
Previously, we were using io.github.cvc5.api to mirror the C++
namespace that the API was in. The namespace of the C++ API changed to
simply cvc5 and so this commit updates the Java package accordingly.
This PR patches cross reference links in Kind.java comments for now until a proper way is implemented that handles documentation for cpp, python and Java API.
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 enables CI for java tests by adding --java-bindings to ci.yml.
It also replaces the unreliable finalize method and instead uses AutoCloseable and explicit close method to clean up dynamic memory allocated by java native interface.
The PR fixes compile errors for SolverTest.java and runtime errors for Solver.defineFun.
