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 PR applies several changes required to compile cvc5 on Windows
ARM64 using MSYS2 CLANGARM64. In particular, `thread_local` class fields
and local function variables in classes and functions exported in the
API are not allowed, so they have been converted into global variables
within the compilation unit. Moreover, some functions in the cvc5 parser
library were using non-exported functions from the cvc5 base library.
This PR exports these functions and converts the ones that were inlined
into non-inlined functions to make them exportable.
Here is a summary of the results of running the cvc5 version in main and
in this branch:
```
config status total solved sat unsat best timeout memout error uniq dis time_cpu memory
main ee 450474 385375 173928 211447 256627 57617 719 5 36 0 18909500.3 42742499.9
pr ee 450474 385370 173923 211447 192564 57621 720 5 31 0 18914388.1 42779989.7
```
It seems that the Windows ARM64 changes do not significantly affect
solver performance compared to the main branch.
The new version of the Pythonic API ensures that each `Context` has its
own `TermManager`, and that every object uses the correct `Context`.
This fixes#11941.
Additionally, this PR adds tests for the Pythonic versions of the
examples to ensure they continue to work correctly after future changes.
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.
Unlike the previous approach in PR #11251, this solution ensures
platform independence by using PRI macros for formatted printing.
Additionally, this PR enables the `-Werror` flag in the CI build for
examples, ensuring that future warnings are caught as errors.
It addresses the following warnings triggered by clang on macOS:
```
warning: format specifies type 'long' but the argument has type 'int64_t' (aka 'long long') [-Wformat]
printf("value for x: %ld/%lu\n", x_num, x_den);
~~~ ^~~~~
%lld
warning: format specifies type 'unsigned long' but the argument has type 'uint64_t' (aka 'unsigned long long') [-Wformat]
printf("value for x: %ld/%lu\n", x_num, x_den);
~~~ ^~~~~
%llu
```
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 .
It also replaces calls to deprecated functions of `Solver` with the
corresponding function of `TermManager`.
---------
Co-authored-by: mudathirmahgoub <mudathirmahgoub@gmail.com>
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.
