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 PR introduces the initial header and setup for the Piand solver
module.
---------
Signed-off-by: Berger Zvika <youremail@example.com>
Co-authored-by: Berger Zvika <youremail@example.com>
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).
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.
This generalizes `--safe-options` to `--safe-mode=safe`.
An additional mode `--safe-mode=stable` is added which permits regular
options that do not support an essential feature (models and proofs).
This adds a field `no_support:` to the options toml files to list (as
strings) the features that are not supported by this option. This field
is expected to be maintained only for `regular` options. That is,
`common` options are assumed to have full support for all features, and
it is inconsequential which features `expert` options are supported with
(as they are not permitted in safe modes).
Marks `solve-bv-as-int`, `bv-solver`, and `cegqi-bv` as having no proof
support. Ensures the latter three are manually set by default when
`--safe-mode=safe`. Note that proof support for all 3 of these should be
available in the near future.
Restores `nl-cov`, `symmetry-breaker`, `cegqi-midpoint` as regular
options that do not support proofs.
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.
Adds 2 macro rewrite rules that rely on this, updates the string
rewriter to use the new utility in these 2 places. Note that in both
cases the rewrites now applicable in these cases are more powerful.
The elaboration for these rules will be added in a followup PR, and
depends on https://github.com/cvc5/cvc5/pull/11600.
My dev branch showed no performance regression on SMT-LIB and an
industrial set with this change.
The motivation is to have a more consistent policy regarding whether an
illegal combination of options is recoverable or unrecoverable. This is
currently unintuitive since we are detecting some cases eagerly (in
SolverEngine::setOptions) and some lazily (in SetDefaults::setDefaults).
This makes both *un*recoverable.
---------
Co-authored-by: Aina Niemetz <aina.niemetz@gmail.com>
