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 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.
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 .
Note that this fixes a serious problem with DTypeSelector::getName()
where the delimiting 0-byte for self selectors was included, which
caused cutting off the name string for C strings.
This introduces a TermManager object, which will, in the future, be the
sole object responsible for handling/managing terms and sorts. For now,
all corresponding functions in `cvc5::Solver` are marked as deprecated,
as is constructor `cvc5::Solver::Solver()`, since in the future a solver
instance must be constructed from a term manager instance. Currently, we
maintain a static thread_local term manager instance to not break the
API and continue providing constructor `cvc5::Solver::Solver()`.
Note that this already converts all C++ unit tests to use the
TermManager except for a single test `getStatistics()` in
`test/unit/api/cpp/solver_black.cpp`. Statistics handling is currently
still maintained on the solver level. The statistics we maintain,
however, concern terms only and will eventually be refactored to be
tracked in the NodeManager.
Further note that the Java and Python APIs will be refactored in
separate PRs.
