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 .
