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.
This PR moves the public API headers into a top-level include directory. This makes it easier to find the public API of cvc5 and makes the install headers script obsolete.
Fixes#9553Fixes#9556
This experimental option causes cvc5 to synthesize rewrite rules based on the input. The code for this is a preprocessing pass which used to rewrite the input to a sygus conjecture. This is confusing since it changes the semantics of the input. We now call a separate subsolver.
This also cleans up set defaults. The options required for synthesizing rewrite rules are now applied locally to the subsolver spawned by the preprocessing pass.
We now terminate with an exception in the rare case when rewrite rule synthesis terminates.
This is required for further enhancements to the sygus solver for answering infeasible.
The public cvc5 API now lives in the cvc5 namespace. All internal parts were moved into the (new) internal namespace.
The final hierarchy will be as follows:
cvc5
~~ public API
::context
::internal
::parser
::main
After this PR it will be:
cvc5
~~ public API
::internal
::context
::main
::parser
Fixes https://github.com/cvc5/cvc5-projects/issues/445. Fixes
https://github.com/cvc5/cvc5-projects/issues/446. The issue is related
to the preprocessing pass for doing rewrite rule synthesis based on the
input. It was removing duplicate arguments from both chaining operators
and non-chaining operators when constructing the corresponding
datatypes. In the case of non-chaining operators, it could happen that
the constructor of the datatype did not have the correct number of
arguments for a given kind if there was a term where multiple arguments
were the same. This commit fixes the issue by doing the duplicate
elimination only for chaining operators.
