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
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
Removes checkEntailed from Solver.
Removes isEntailed, isNotEntailed, isEntailedUnknown from Result.
Removes isSubsortOf, isFunctionLike, getUninterpretedSortName, getSortConstructorName from Sort.
Updates examples and unit tests.
This PR removes the code that translates from bit-vectors to integers from the bv_to_int preprocessing pass, and replaces it with a call to the IntBlaster module.
Tests are updated and added, as well as other minor changes.
Solves the following issues (and contains corresponding tests):
cvc5/cvc5-projects#345cvc5/cvc5-projects#344cvc5/cvc5-projects#343
@mpreiner FYI