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.
