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.
Currently, `CVC5ApiException` inherits from `Exception`, which is a
*checked exception* in Java. Checked exceptions must be declared in the
`throws` clause of any method that may throw them; failing to do so
prevents Java code using the method from catching the exception as a
`CVC5ApiException`. This PR changes `CVC5ApiException` to be a subclass
of `RuntimeException`, which is an *unchecked exception*. Unchecked
exceptions may optionally be listed in the *throws* clause, but omitting
them does not prevent code from catching them.
Fixes#12117
This PR adds new targets, `build-cppapitests` and `cppapitests`, for
building and running the C++ API tests, and uses `build-apitests` and
`apitests` for building and running the API tests across all languages
(C++, C, Python, etc.). It also adds a new target, `pyapitests`, for
running the Python API tests, and fixes the `capitests` target to run
the correct set of C API tests. In addition, it moves all issue-related
Python API tests to their own directory, as is already done for the C++
and C API tests.
This adds `stable` as a build type, which is similar to `safe` but
permits incomplete proofs in regressions and the use of regular options
with `no-support:` fields.
This makes the checks for kinds more robust. In particular we now catch
assertions with illegal kinds that otherwise could be dropped. We also
check for illegal types.
This fixes proofs in CPC in safe mode on 2 regressions.
---------
Co-authored-by: Mathias Preiner <mathias.preiner@gmail.com>
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.
This ensures that regressions pass when configuring in `safe-mode`. Note
that *all* regression testers must now take into account whether we are
in a safe-mode (safe mode itself is not a new tester).
This makes the following changes:
- `safe-mode: yes|no` is now an entry in `--show-config`
- LibPoly and Cocoa are disabled by default when configuring with
`safe-mode`. We give a warning if the user specified otherwise.
- A few regressions are updated to have the appropriate options.
- Option and logic exceptions that are "admissible" in safe mode are
updated to contain the text `"in safe mode"`.
- Various options that are used in run_regression.py are upgraded to
"common" to ensure safe-mode is compatible with the tester. Removes a
few unecessary options in run_regression.py.
- Disables a number of unit tests and examples (in the CMake) that are
not applicable in safe mode.
- Adds a CI job to test a safe-mode build.
Note that the CPC tester fails due to not guarding against some unsafe
operators in the rewriter. I will address this in a separate PR.
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.
This adds options that guard the usage of "experimental" theories or
extensions thereof when `--safe-options` is enabled.
This includes bags, finite fields, separation logic, higher-order logic,
and extensions of arithmetic (including transcendentals, iand and pow2).
The options `--sets-exp` (renamed from `--sets-ext` in this PR) and
`--fp-exp` continue to be disabled by default, thus do not need to
change.
Similar to other expert options, these theories can still be used with
`safe-options` if they are enabled prior to setting `safe-options`, e.g.
`--ho-exp --safe-options ...` allows HOL to be used. The options
configuration will only override the setting of `*-exp` options if not
set by user.
This does not impact the behavior of cvc5 when `--safe-options` is not
set.
FYI @alex-ozdemir @mudathirmahgoub @yoni206 .
When using the incremental input interface, the parser had the behavior
that if it was ever finished, it did not reset its "finished" flag even
if more input was added.
This makes the parser internally reallocate a lexer and parser if the
user had exhausted all their input.
Fixes#11069.
---------
Co-authored-by: Aina Niemetz <aina.niemetz@gmail.com>
Co-authored-by: Daniel Larraz <daniel-larraz@users.noreply.github.com>
