Cython `cdef` classes without an explicit `__init__` constructor have an
implicit `__init__` that accepts any number of arguments. (Python
classes, by contrast, default to an `__init__` that takes no arguments.)
This can lead to confusing situations where arguments appear to be
accepted but are discarded. This PR fixes the issue by adding explicit
`__init__` methods to the Cython classes.
Additionally, this PR removes some unnecessary field initializations in
the Cython classes.
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 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
This PR exposes hashing and equality of proofs in the API to avoid
reconstructing the same proof step multiple times from the Lean side.
Notes:
- Proof equality in this PR is referential, not syntactical. However,
this is still useful for caching (and better than nothing).
- A default constructor, `Proof()`, is added to the Java API to mirror
the C++ and Python APIs and the `Term()` constructor in the Java API.
This changes the default behavior of `simplify` not to apply top-level
substitutions.
This behavior is can be unintuitive and may e.g. introduce internal
skolems into the term the user simplifies.
The previous behavior can be enabled by passing `applySubs` to true.
