This PR builds and stores the JNI library in a directory structured
according to the OS and CPU architecture. This allows a single JAR to
contain native JNI libraries for multiple OSes and CPU architectures
simultaneously, and prevents file collisions when multiple JARs
containing a native JNI library for the same OS but different
architectures are added to the classpath.
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).
This PR uses Java 8 in CI, except on macOS arm64, where the minimum
supported Java version is 11. This ensures that the Java bindings, Java
API tests, and Java examples are compatible with the minimum required
Java version. It also ensures that the published Java bindings on GitHub
can run with this older version. Previously, CMake enforced
compatibility for the Java bindings, but not for the Java API tests or
the Java examples. This change provides a more centralized solution.
This PR also fixes a Java unit test to make it compatible with Java 8.
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
