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.
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.
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 .
This PR:
Updates the functionality of setIncrementalStringInput / appendIncrementalStringInput to a more intuitive behavior where append does not replace the current contents of the input.
Adds setStringInput to the API and updates the interactive shell to use this interface.
Updates the examples
Adds new unit tests
This PR adds minor improvements to the SyGuS solver:
Changes the weight of identity rules in the grammar, giving them higher priority during enumeration.
Replaces n-ary operators with their binary version before matching in rcons.
Splits the pattern enumerator for rcons into two enumerators: pattern enumerator and term enumerator.
Adds an option to control geometric distribution parameter used to interleave the 2 enumerators.
Additionally, this PR moves the implementation of the grammar API to an internal class with the Grammar class now a wrapper for the internal class.
