Organizing the PR a bit:
we hook up the subtheories to TheoryFf
we expose FF-related things via the C++/Pytohn API and SMT-LIB2 interface.
we add a bunch of tests against these interfaces.
Fixes#8869. We are not using `libjawt.so` or `libjvm.so` (we are not
using the Java Invocation API), so we don't need to link `libcvc5jni`
against `JNI_LIBRARIES`. This change allows us to use cvc5 from Java
without linking against the JNI libraries (see changes in the `examples`
folder).
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 adds the code for printing synthesis solutions to the docs. Various other changes are made to increase the consistency between the different bindings.
Signed-off-by: Abdalrhman M Mohamed <abdalrhman-mohamed@uiowa.edu>
Also extends to non-trivial unit test of SynthResult.
Note this also changes the expected output when using --sygus-out=status from unsat/sat/unknown to feasible/infeasible/fail (the option is used mostly just for our regressions). The output mode status-or-def is now equivalent to standard and is hence deleted.
This commit ensures we don't segfault in the SyGuS API (for non-text inputs) if the option sygus is not set to true. It also renames mkSygusVar to declareSygusVar for consistency with the sygus input format.
For SyGuS API inputs, we now use the option sygus to true instead of setting the language to sygus2.
This furthermore changes a few details in set-defaults regarding the relationship between the language, the sygus option, and when to apply default options for sygus.
It also adds a unit test for checkSynth.
Removes checkEntailed from Solver.
Removes isEntailed, isNotEntailed, isEntailedUnknown from Result.
Removes isSubsortOf, isFunctionLike, getUninterpretedSortName, getSortConstructorName from Sort.
Updates examples and unit tests.
This renames the arithmetic internal and API kind PLUS to ADD for
consistency with our naming scheme for other operators (e.g.,
BITVECTOR_ADD, FLOATINGPOINT_ADD).
This renames the arithmetic kinds MINUS and UMINUS on the
API level for consistency with our naming scheme for other
operators (e.g., BITVECTOR_SUB, FLOATINGPOINT_SUB).
