This adds an expert option to allow regular expressions to appear
anywhere in constraints, including in datatype fields, or as arguments
to uninterpreted functions.
This is required for reasoning about the correctness of CPC for proof
rules involving regular expressions.
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).
The latest SMT-LIB release has standardized arithmetic/bitvector
conversions (https://smt-lib.org/theories-FixedSizeBitVectors.shtml).
This adds support for them.
In particular, the kind Kind::INT_TO_BITVECTOR now has recommended
syntax int_to_bv, while int2bv is supported (deprecated) in non-strict
mode for now for backwards compatibility.
The kind Kind::BITVECTOR_TO_NAT and the smt2 syntax bv2nat for now is
maintained but should be deprecated. In particular,
Kind::BITVECTOR_TO_NAT is silently converted to
Kind::BITVECTOR_UBV_TO_INT in the API.
We add Kind::BITVECTOR_UBV_TO_INT and Kind::BITVECTOR_SBV_TO_INT in the
API.
The internal kind BITVECTOR_TO_NAT is renamed BITVECTOR_UBV_TO_INT, and
add internal kind BITVECTOR_SBV_TO_INT.
Updates the proof infrastructure to use the new naming scheme.
The helper method `create_rewrite_proof` no longer generates rewrite
rule holes on my dev branch, since the given rewrite is handled by
ARITH_POLY_NORM now.
The later uses only ASCII letters instead of Unicode characters. This
currently leads to a build issue with the Java headers on FreeBSD:
https://github.com/cvc5/cvc5/issues/11145
