This PR adds the proper checks for the parser API. It furthermore adds examples and unit tests for the parser API.
Note that InputParser::nextCommand and InputParser::nextTerm don't catch exceptions, since we want to throw ParserExceptions containing the parsing information, not API exceptions.
Also, at the moment, the InputParser can throw an exception during initialization, which is not caught either.
Fixescvc5/cvc5-projects#654.
Fixes include:
sygus-core-connective algorithm should be robust to candidates involving partial functions
sygus interpolation module should avoid repeated variables in input list
sygus interpolation default grammar construction should rely on the internal subsolver. in particular this ensures internal heuristics, e.g. sygus-add-const-grammar are leveraged.
The rewrites had led to complications with the cardinality solver and moreover weren't sound if the universe set was e.g. intersected with a term that was not a subset of elements from set variables.
This furthermore corrects an issue cvc5/cvc5-projects#644, which was triggered by the unsoundness in these rewrites.
Fixescvc5/cvc5-projects#644.
This introduces a general way to use public enums both in the C++ and
the (upcoming) C API. For the C++ case, we now use enum classes rather
than enums for public enums. This also includes definitions for
C API to_string conversions for public enums. C API definitions in
cvc5_types.h are only included from the C API, guarded via a macro
(thus, for now, not included yet when the header is included).
This is another step towards the parser API.
It hides the symbol manager's interface entirely. The old implementation is now contained via a new class SymManager.
The last step will be to move this (+ command.h, input_parser.h) from parser/api/cpp/ to include/cvc5/.
The cmake FIXTURES workaround broke the nightly builds in a nondeterministic manner.
As we come up with a different solution, as discussed offline, this PR disables the workaround.
This is work towards a major refactor of our algorithms for expression mining (rewrite rule synthesis and verification, query generation). The plan is to make these available via a find-synth command, see the changes in the regressions for examples. Currently, these algorithms are available via options that "hijack" calls to check-sat/check-synth, which is highly non-intuitive and requires modifications to the core of the SyGuS solver.
This changes the interface to expression miner in preparation for this change.
Note this currently removes our support for expression mining via options (which is marked as expert options only). Support for these will be available again when support for find-synth is completed. Several regressions are disabled in the meantime.
The parallel option -j does not seem to be accepted by cmake in some situations. This PR removes this option from commands that build tests. These commands were part of a recent workaround to have 'make test' work (#9750).
Fixes#9569.
We must ensure that the cvc5 binary is built before running any tests. In principle, this would just be a matter of adding a dependency on the 'test' target (defined by CTest). However, that built-in targets are not accessible via user code.
This seems to be a legacy cmake bug from +10 years ago (8774, 8438).
In order to have 'make test' work properly I use a CMake feature called FIXTURES to add 'test_setup' as the first test which builds the target 'build-tests'.
Otherwise we timeout for get-abduct with unsatisfiable side conditions. Also leads to assertion failures with sygus-core-connective for empty unsat cores.
Fixescvc5/cvc5-projects#587.
