Add a test for '<<' for the proof format mode
Add this test to the uncovered functions for Python and Java
Return placeholder value if Proof object is empty
Add tests for this (and add them to uncovered functions)
This pull requests makes the enum that lists all proof rules a part of the API.
It also renames the enum from PfRule to ProofRule. It also renames some unrelated types and function names that share the PfRule name (such as DslPfRule).
This rename unfortunately touches many files since PfRule is not an uncommon type. (second to last commit)
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).
Work towards supporting (find-synth :X).
This adds a unified utility SynthFinder for implementing the functionality removed in #9796.
It introduces "find synth targets" as different things that can be found using find-synth.
Further PRs will connect this utility to the API.
Also changes the name of the enum for now to have a prefix, since we are not using enum classes.
Furthermore this excludes true from being a preprocessed learned literal.
Solver::printStatisticsSafe() is private right now. There is no real reason for that, and as we claim that the driver is only using the regular API we should just make it public.
This PR adds a C++ unit test that explicitly calls into API functions that are not exposed by the python API. This fixes the issue of false positives in our API coverage checks, as some parts of the C++ API are legitimately not used by the python API.
