This PR introduces the new C++ methods `Term TermManager::mkString(const
std::u32string& s)` and `std::u32string Term::getU32StringValue()` to
replace old methods `Term TermManager::mkString(const std::wstring& s)`
and `std::wstring Term::getStringValue()`.
The reason for this change is that `wchar_t` has a platform-dependent
size: on Windows, it is 16-bit (UTF-16), while on Linux and macOS, it is
32-bit (UTF-32). However, the current implementation assumes that
`wchar_t` is always 32 bits. In contrast, `char32_t` and
`std::u32string` are explicitly designed for Unicode and have consistent
32-bit size across platforms.
Similarly, this PR also introduces C functions
`cvc5_mk_string_from_char32` and `cvc5_term_get_u32string_value`
to replace old functions `cvc5_mk_string_from_wchar` and
`cvc5_term_get_string_value`.
Although `char32_t` is part of the C11 standard, the `<uchar.h>` header
(which should define `char32_t`) is missing in Apple Clang. Therefore,
we explicitly provide a definition in such cases.
---------
Co-authored-by: Aina Niemetz <aina.niemetz@gmail.com>
Enum OptionCategory was introduced in #11931, which did not include
implementations for `std::to_string(cvc5::modes::OptionCategory)` and
`cvc5_modes_option_category_to_str(Cvc5OptionCategory)`.
This adds implementations for these functions and further adds uncovered
tests for C, Python and Java (fixes coverage build in nightlies).
This PR implements one approach to exposing DSL Proof rules to the user: by making the DSL rule enum public.
Notes:
The safe toString method is not included in safe_print.h because it's generated by the RARE parser.
To test the hash and toString, for all enum values, a "last" enum value is needed. However, the current last enum value (DISTINCT_BINARY_ELIM) used in the test is generated by the RARE parser and may change in the future. Potential fixes include: adding LAST enum value, moving NONE to the end, or defining a LAST whose value is generated by the RARE parser.
This introduces a TermManager object, which will, in the future, be the
sole object responsible for handling/managing terms and sorts. For now,
all corresponding functions in `cvc5::Solver` are marked as deprecated,
as is constructor `cvc5::Solver::Solver()`, since in the future a solver
instance must be constructed from a term manager instance. Currently, we
maintain a static thread_local term manager instance to not break the
API and continue providing constructor `cvc5::Solver::Solver()`.
Note that this already converts all C++ unit tests to use the
TermManager except for a single test `getStatistics()` in
`test/unit/api/cpp/solver_black.cpp`. Statistics handling is currently
still maintained on the solver level. The statistics we maintain,
however, concern terms only and will eventually be refactored to be
tracked in the NodeManager.
Further note that the Java and Python APIs will be refactored in
separate PRs.
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.
