Remove references to `bv-div-zero-const` in docs (#6672)

The bv-div-zero-const option has been removed and is now always
enabled, so this commit updates the documentation of the kinds to
reflect that. It also makes the language to describe the special cases a
bit more uniform.

Fixes for printing define-fun-rec (#6673)

Remove option to ignore negative memberships (#6665)

Fixes #6661. The option `--strings-inm` could be used to ignore negative
membership constraints. However, this option made the string solver
model-unsound or produced incorrect models if the user provided a
benchmark that actually contained negative membership constraints. The
solver did not check for negative membership constraints and did not
warn the user about them. Because the option is not really being used,
this commit removes it.

Adding getters to the python API and testing them (#6652)

This PR adds missing API functions from the cpp Term API to the python API.
Corresponding tests are translated from term_black.cpp.

Remove redundant logic ALL_SUPPORTED. (#6664)

Move `toPythonObj` tests to the new API unit test directory (#6656)

This is the last test file that we move from the old directory to the new one, and so the old directory is deleted.

Use proper variable name (#6670)

This PR fixes the driver which used an incorrect variable name in competition mode.

Fix unsat core proofs (#6655)

Fixes cases of satisfiable unsat cores when proofs are enabled.

Unfortunately, this bug was also preventing us from doing the final scope check for all proof checking. As this was not being tested, this PR uncovers that proof checking is now failing on 6 regressions. I'm disabling proof checking here and will address these issues on later PRs.

Make `STRINGS_CTN_DECOMPOSE` an explicit conflict  (#6663)

Fixes #6643. The STRINGS_CTN_DECOMPOSE inference is always a conflict
but we sometimes sent it as an inference. To make sure that the
inference manager actually recognizes the inference as a conflict, this
commit ensures that the conclusion is always false and modifies the
explanation accordingly.

Remove `Options::operator[]` (#6649)

This PR removes the next heavily specialized template function Options::operator[] in favor of direct access to the option data.

Move public wrapper functions out of options class (#6600)

This PR moves options wrapper functions out of the Options class. These wrapper functions are meant to be called by "external" code that should not access the options modules. This PR thereby significantly reduces the interface of the Options class.

Fix issues with double negation in circuit propagator (#6669)

This PR fixes a subtle issue with double negations when producing proofs in the circuit propagator.
Adds the test case as a new regression, as well as some similar instances.
Fixes cvc5/cvc5-projects#277.

Fix issues when poly is disabled (#6668)

Recent changes introduced issues when libpoly is disabled.

Make `Options::assign()` specializations free functions (#6648)

This PR removes the next two heavily specialized template functions. Both Options::assign() and Options::assignBool() are only used within options.cpp now and there is thus no reason to keep them in the public interface. Furthermore, we can just make them properly named functions instead of template functions.

Do manual squash cleanup for docs (#6646)

This PR abandons the attempt to do the cleanup in a single rebase command, and instead squashes the old commits manually. The current solution does not handle conflicts properly. The new approach (which seems to be more robust) proceeds as follows (to squash $first..$last):

- checkout $last
- soft reset to $first (checkout $first, but keep changes in working copy)
- commit to squashed commit
- cherry-pick $last..HEAD from main branch

docs: Migrate input languages page. (#6659)

This migrates page https://cvc4.github.io/input-languages.

docs: Restructure index page, fix style issue. (#6657)

Some additions to the datatypes python API (#6640)

This commit makes the following additions, in order to sync the python API with the cpp API.

1. adding `getName` functions to datatypes related classes
2. allowing `mkDatatypeSorts` with 1 or 2 arguments (previously allowed only 2).
3. In case there is a second argument to `mkDatatypeSorts`, we make sure it is a set.
4. Corresponding changes to the tests.

Use top-level substitutions in ITE simp (#6651)

With this PR, we use the central top-level substitutions instance in the ITE simplification preprocessing pass. Previously the ITE simplification pass maintained its own copy of the substitutions.

Since the top-level substitutions now are the authority on models, this led to model failures after this change: ac8cf53#diff-30677c5a1752b1d0e83ef25fd2cfb8949576ea42cf7821fe0ac00ebbd0122f8aL276.
This PR corrects the issue.

This is required for SMT-COMP.

Disable timeout regressions (#6650)

Disables two regressions that have been timing out causing nightlies to fail.

FP value support in python API (#6644)

This PR adds new is* functions from the cpp API to the python API.
In particular, it adds getFloatingPointValue() function from the cpp API.
A test (translated from term_black.cpp) is added.

getFloatingPointValue() returns a tuple, and so this requires importing an instance of tuples into cython.

Remove Options::ref() (#6647)

This PR gets rid of the templated Options::ref() method (and all its specializations for every option).

Remove invalid options from run scripts (#6645)

This commit removes some of the options in the run scripts that are not
supported anymore: `--bv-div-zero-const` and `--rewrite-divk`. Both of
those options are effectively enabled by default in cvc5.

Update `toPythonObj` to use new getters -- part 1 (#6623)

Following #6496 , this PR adds new getters to the python API, as well as tests for them. This makes toPythonObj simpler.

A future PR will add more getters to the python API.

Co-authored-by: Gereon Kremer nafur42@gmail.com

Compute model values for nested sequences in order (#6631)

Fixes #6337 (the other benchmarks in this issue are either solved
correctly or time out after the changes in #6615) and fixes #5665.

While computing the model for a nested equivalence class containing
seq.unit, we were looking up the representative of the argument in
(seq.unit (seq.unit j)) and the representative was simpliy (seq.unit j). However, we had assigned (seq.unit 0) to (seq.unit j) earlier.
A second equivalence class of type (Seq (Seq Int)) and length 1 was
later assigned (seq.unit (seq.unit 0)) and we didn't detect that
(seq.unit (seq.unit j)) and (seq.unit (seq.unit 0)) have the same
value. This was incorrect because we do not allow assigning the same
value to different equivalence classes. In this case, it led to one of
the assertions being false.

This commit fixes the issues in two ways: it ensures that types are
processed in ascending order of nesting (e.g., (Seq Int) terms are
processed before (Seq (Seq Int)) terms) and it changes the procedure
to look up the representative in the model instead of the theory state
to take into account the model values assigned to the elements of
sequences.

cc @yoni206

Remove `Options::set()` method (#6556)

This PR gets rid of the Options::set() method, replacing it by direct access to the options data.
This method was only used internally and did nothing except for resolving the options data from the option tag type via template specializations (via ref()), which is no longer necessary.

(Optimization) remove popObjective, add resetObjectives, rename pushObjective => addObjective (#6634)

In order for OptimizationSolver to support pushing & popping,
we could remove popObjective because it might be difficult to handle cases like:

optSlv->pushObjective(...);
optSlv->push();
optSlv->popObjective();
optSlv->pop();
In this case we need to add back the popped objective...
If push/pop is supported, pop does not bring back objectives if you resetObjective
but it will revert the objs you add.
just like assertFormula and resetAssertions.

Python API: bugfix + translating tests from cpp unit tests (#6559)

This PR fixes an issue in the python API for datatypes, and also introduces tests translated from https://github.com/cvc5/cvc5/blob/master/test/unit/api/datatype_api_black.cpp

The next PR will translate more tests and will also introduce missing functions in the python API for datatypes.

Add non-templated method to set option defaults (#6540)

This PR replaces the templated Options::setDefault() methods by new non-templated free functions options::{module}::setDefault{option}().
These methods should be used instead of the common if (!set by user) { set option value } pattern.

Disable `--jh-rlv-order` for slow regressions (#6633)

This commit adds --no-jh-rlv-order to two string regressions that take
over 2 minutes to run in debug after #6613, which increases the overall
regression runtime significantly.

`STRINGS_CTN_DECOMPOSE`: Avoid multiple conflicts (#6632)

Fixes #5508. `STRINGS_CTN_DECOMPOSE` could be triggered multiple times
by the same term, which resulted in an assertion failure. This commit
returns immediately after the first conflict to avoid the assertion
failure.

Fix regular expression aggressive elim (#6627)

Fixes #6620, fixes #6622. Fixes cvc5/cvc5-projects#254.

The benchmarks from the 2 issues timeout, a regression is added for the projects issue.

Fix `str.replace_re` and `str.replace_re_all` (#6615)

Fixes #6057. The reductions of `str.replace_re` and `str.replace_re_all`
were not correctly enforcing that the operations replace the _first_
occurrence of some regular expression in a string. This commit fixes the
issue by introducing a new operator `str.indexof_re(s, r, n)`, which,
analoguously to `str.indexof`, returns the index of the first match of
the regular expression `r` in `s`. The commit adds basic rewrites for
evaluating the operator as well as its reduction. Additionally, it
converts the reductions of `str.replace_re` and `str.replace_re_all` to
use that new operator. This simplifies the reductions of the two
operators and ensures that the semantics are consistent between the two.

Add Lexicographic + Pareto Optimizations (#6626)

Lexicographic optimizations: Optimize the objectives one-by-one, in the order they are pushed.
Pareto optimizations: Optimize the objectives to the extend that further optimization on any objective will worsen the other objective.
Units tests are of course added.

Lexicographic optimization is using iterative implementation, pretty similar to the naive box optimization.

Update proof namespaces (#6614)

This removes namespace theory from proof utilities, and moves MethodId to its own file in src/proof/.

Fix CEGQI for datatypes with Boolean subfields (#6630)

Fixes a solution soundness issue caused by allowing ineligible terms of kind BOOLEAN_TERM_VARIABLE to appear in instantiations.

This also corrects the expected solution on a benchmark that had an incorrect status.

Fixes #6603.

Fix spurious assertion for trivial abduction (#6629)

Fixes 2nd benchmark from #6605.

FP: Rename FLOATINGPOINT_PLUS to FLOATINGPOINT_ADD. (#6628)

This is to make it consistent with the name of the SMT-LIB operator
(fp.add).

Return `REWRITE_AGAIN` after rewriting bvcomp (#6624)

This commit fixes an assertion failure in the rewriter on some of the
SMT-LIB QF_ABVFP benchmarks (the regression in this commit is the
minified version of
`non_incremental/QF_ABVFP/20170428-Liew-KLEE/imperial_gsl_benchmarks_statistics_klee.x86_64/query.14.smt2`).
The problem was that after applying the `BvComp` rewrite, the bit-vector
rewriter was returning `REWRITE_DONE` instead of `REWRITE_AGAIN`. The
rewrite simplifies expressions of the form `bvcomp(t, c)` where `c` is a
constant of bit-width 1. If `c` is zero, then the rewrite returns
`bvnot(t)`. This node can potentially be rewritten further, e.g., if `t`
is `bvnot(x)`. This commit fixes the response and adds the corresponding
tests.

Add support for Box optimization (#6599)

Add support for box optimization -- independently optimize each goal as if the other goals do not exist.
Single minimize() / maximize() now maintains the pushed / popped context.
Of course unit tests are here as well.

Avoid uploading docs if they did not change (#6621)

Fixes an oversight from #6601.

Enable new justification heuristic by default (#6613)

This enables the new implementation of justification heuristic by default.

Fixes #5454, fixes #5785. Fixes wishues 114, 115, 149, 160.

Use references instead of getter functions (#6597)

This PR follows a suggestions of @ajreynol to use public references instead of getter functions to access the individual option modules.

 More precise includes of `Node` constants (#6617)

We store constants, e.g., BitVector and Rational, in our node infrastructure. As a result, we were indirectly including some headers in almost all files, e.g., the GMP headers. This commit changes that by forward-declaring the classes for the constants. As a result, we have to include headers like util/rational.h explicitly when we use Rational but it saves about 3 minutes in compile time (CPU time).

The commit changes RoundingMode from an enum to an enum class such that it can be forward declared.

Add more examples to the documentation (#6569)

This PR adds (most of) the existing examples to the documentation, and does some other minor updates on the documentation. Some details:
- for consistency, all cpp examples are moved from examples/api to examples/api/cpp
- add capabilities for SMT-LIB examples, and two simple smt2 examples
- more docs/examples/*.rst files
- two new documentation categories: installation (how to obtain, compile and install cvc5) and binary (about the cvc5 binary)

Ensure proper types in unit tests (#6598)

This PR fixes a type mixup (the usual long vs long long mixup on macos systems) in the unit tests for the new api::Term getters.
Fixes #6594.

Reduce size of sphinx-gh output (#6601)

This PR reduces the disk size of the docs generated by make sphinx-gh.
Apart from reformatting the cmake source, we now not only remove the _sources folder, but also .doctrees (essentially the sphinx cache) and _static/fonts/ (the fonts that are actually used live in _static/css/fonts).
In combination, this now reduces the disk size from about 20MB (sphinx) to less than 6MB (sphinx-gh).
Furthermore this PR only uploads the generated documentation if it differs from whatever we currently have for master.
This is relevant to make the docs-ci repository smaller (which already has more than 5GB...)

api docs: Fix and tweak style for home and top links. (#6618)

Replace deprecated calls to `std::allocator` (#6606)

Fixes #6453. This commit replaces all calls to std::allocator with calls to
std::allocator_traits. Strictly speaking, allocate() and deallocate() are
not deprecated but the commit replaces them for uniformity.

[Unit tests] Fix path of Java bindings (#6616)

Currently, when configuring cvc5 with Java bindings, CMake complains
about `get_filename_component(CVC5_JNI_PATH ${CVC5_JAR_PATH} DIRECTORY)`
not using the correct number of arguments in the Java unit tests. The
issue is that `${CVC5_JAR_PATH}` is empty. The value of
`${CVC5_JAR_PATH}` was computed in the Java API bindings but then not
shared with the rest of the build system. Because `${CVC5_JAR_PATH}` is
not used anywhere else, this commit moves the computation of
`${CVC5_JAR_PATH}` to the unit tests. The commit also ensures that the
API subdirectories are processed before the test subdirectories.

Fix non-fixed length case in re-elim (#6612)

Fixes followup issues from #6604.

Implementation of the new justification heuristic (#6465)

This adds the new implementation of the justification heuristic. It does not enable this strategy yet.

A followup PR will activate this strategy within DecisionEngine.

Move proof utilities to src/proof/ (#6611)

This moves all generic proof utilites from src/expr/ and src/theory/ to src/proof/.

It also changes the include for term conversion proof generator to conv_proof_generator in preparation to rename this utility on a followup PR (to avoid confusion with the use of "Term").

Fix re-elim length requirement for symbolic RE memberships (#6609)

Fixes #6604.

Previously, re-elim was solution unsound for cases where the LHS and a component of the RHS were both empty. This ensures a length requirement is given for the LHS to ensure proper containment.

Fix instance of no rewrite in extended rewriter (#6610)

Fixes #6545.

An assertion failure was being raised indicating that we were reporting a rewrite that was not changing the original term.

Better formalization of regular expression unfolding skolems (#6602)

This replaces our previous formalization of RE unfolding skolems with a more explicit one that is amenable to external proof conversion. It adds a few associated utility methods to SkolemManager required for LFSC proof conversion for RE_UNFOLD_POS.

It also changes the order of equalities in the RE_UNFOLD_POS rule, which simplifies LFSC proof checking.

Fix tests of unsat cores (#6593)

This updates all regressions that pass check-unsat-cores to enable check-unsat-cores. This includes any incremental benchmark, which was disabled in run_regression.py previously.

It adds --no-check-unsat-cores to a few corner benchmarks that were previously disabled based on --incremental.

It also reverts a change to when proofs are disabled: options like sygus-inference should not permit proofs (or unsat cores).

Fix and refactor relevant domain (#6528)

In a handcrafted case, one can make the body of quantified formula another quantified formula when special attributes are used. The relevant domain utility was not robust to this case, leading to instantiations with free variables.

This fixes the issue and also updates its style to use a term context stack, which also avoids a tree traversal of the bodies of quantified formulas in this utility.

Fixes #6476. The benchmark from that issue now times out.

Formalize shared selectors as skolem functions (#6591)

This is work towards properly printing shared selectors in external proofs.

Minor simplification to boolean proof checker (#6590)

(proof-new) Minor documentation sync (#6592)

Add utility to get all types occurring in a term (#6588)

Required for external proof conversions.

Update to sygus standard output for check-synth responses (#6521)

This PR does two things:
(1) It eliminates the ad-hoc implementation of printSynthSolutions and removes it from the API. Now, printing response to a check-synth command is done in a more standard way, using the API + symbol manager. This is analogous to recent refactoring to get-model.
(2) It updates cvc5's output in response to check-synth to be compliant with the upcoming sygus 2.1 standard. The standard has changed slightly: responses to check-synth are now closed in parentheses, mirroring the smt2 response to get-model.

It also removes the unused command GetSynthSolutionCommand.

Support braced-init-lists with `mkNode()` (#6580)

This commit adds support for braced-init-lists in calls to `mkNode()`,
e.g., `mkNode(REGEXP_EMPTY, {})`. Previously, such a call would result
in a node of kind `REGEXP_EMPTY` with a single null node as a child
because the compiler chose the `mkNode(Kind kind, TNode child1)` variant
and converted `{}` to a node using the default constructor. This commit
adds an overload of `mkNode()` that takes an `initializer_list<TNode>`
to allow this use case. It also adds a `mkNode()` overload with zero children
for convenience and removes the 4- and 5-children variants because they
saw little use. Finally, it makes the default constructor of `NodeTemplate`
explicit to avoid accidental conversions.

api docs: Tweak and fix style. (#6582)

This fixes the style for narrow layouts. It further fixes and improves
the style for the menu.

api docs: Update copyright. (#6596)

Use scikit-build CMake files for pycvc5 (#6543)

This PR removes copied CMake files for the pycvc5 Cython target, and instead adds a dependency on scikit-build (where those CMake files originated anyway). This keeps us up to date with fixes. Furthermore, the PR switches from distutils to the more modern setuptools. This does add another dependency but it's a fairly reasonable one. setuptools is not part of the base Python distribution, but my understanding is that it is now the de facto standard, and most package managers install it automatically with Python. The main motivation for switching is in preparation for building wheels.

This PR is a piece of this old one (#5657) which I am closing and splitting up.

Move option names out of struct (#6554)

This PR moves the option names out of the option struct (which will be removed) to free constexpr string constants.

BV: Rename BITVECTOR_PLUS to BITVECTOR_ADD. (#6589)

Update version of CaDiCaL. (#6583)

Disable unit testing for clang builds. (#6595)

We currently have issues with clang 11 failing for white unit tests.
This disables unit tests for clang builds.

Properly initialize. (#6586)

This PR fixes a missing initialization that lead to a valgrind warning.

Remove old unsat cores (#6581)

This commit removes the remaining old proof code and the code to produce unsat cores based on it.

Use most recent version of libpoly (#6587)

This PR updates to the most recent version of libpoly which fixes some memory leaks.

Avoid using printSynthSolution in the python API and examples (#6564)

The function printSynthSolution declared here is going to be removed in #6521.

This PR removes it from the python API.
Following #6530, this PR also replaces its usages in the examples by a utility function.
For this, we also add support for getSynthSolutions in the python API.

Minor improvements to the API (#6585)

This PR does some minor improvements to the API:
- remove getConstSequenceElements(), use getSequenceValue() instead
- improve documentation for Term

Fix echo printing. (#6573)

Previously, echo surpressed leading, trailing and escape quotes of the
string to print. However, the SMT-LIB standard states that the string is
to be printed as is, including those quote characters.

Add more getters for api::Term (#6496)

This PR adds more getter functions for api::Term to retrieve values from constant terms (and terms that the average API use might consider constant).
It also introduces std::wstring as regular representation for string constants instead of std::vector<uint32> for the SMT-LIB parser and the String class.

Expand arith's farkas lemma rule as a macro (#6577)

reflects that it is a macro, which we will eliminate

Remove unused methods from `NodeManager` (#6578)

Correctly handle negated assertions for assumption-based unsat cores. (#6579)

Pass empty vector when constructing re empty, fixes rewrite (#6576)

Fixes #6567.

Adding python API test part 4 (#6553)

This commit (follow #6552) adds more unit tests for python API.
Subsequent commits will include additional missing functions and unit tests.

Make output list of `mkoptions.py` more accurate (#6572)

After commit 6dc5b74, cvc5 was always
being almost completely rebuilt, even if there hadn't been any changes
if cvc5 was configured not to produce documentation (the default).
This was because mkoptions.py only produces the
options_generated.rst file when documentation is enabled. However, it
was unconditionally declared to be an output of the script in
CMakeLists.txt. As a result, the options (and thus most of the code
base) were rebuilt every time because the file was missing in builds
without documentation. This commit modifies the output list depending on
the configuration.

Make strings emp inference an unhandled inference for proofs (#6575)

The strings inference id STRINGS_INFER_EMP is a rare inference that currently leads to a segfault when proof reconstruction is tried for it. This PR makes it unhandled.

This was caught by a new regression on the soon-to-be-merged jh-new branch.

Adding regressions that failed on old unsat cores (#6574)

We can thus close #3455, #3651, #4925, #5079, #5238, #5902, #5908, and #5604.

Change the default unsat cores (#6571)

This commit changes the default unsat cores to those based on solving-under-assumptions in the SAT solver and the (new) preprocessing proofs.

The evaluation below on all the non-fp non-incremental SMT-LIB benchmarks, 120s timeout, shows the differences of the unsat cores based on the old proofs, the new ones based on SAT assumptions + preprocessing proofs, and the new ones based on SAT and preprocessing proofs. Note that the union of the last two is on par with the first.

```
                                      status  total  solved   sat  unsat  best  timeout  memout  error  uniq  disagr  time_cpu    memory
benchmark config
AUFDTLIRA newUnsatCoresAssumps-safe/     ee     35       4     0      4     4        7       0     23     2       0     954.0    1267.5
          newUnsatCoresProofs            ok     35      31     0     31    25        4       0      0     0       0     894.1    1692.9
          oldUnsatCores                  ok     35      32     0     32    30        3       0      0     1       0     799.2    1428.5
AUFLIA    newUnsatCoresAssumps-safe/     ok     11       7     0      7     7        4       0      0     7       0     532.2    7604.4
          newUnsatCoresProofs            ok     11       4     0      4     1        6       0      0     0       0     829.0   12459.8
          oldUnsatCores                  ok     11       4     0      4     3        6       0      0     0       0     818.2    7764.4
AUFLIRA   newUnsatCoresAssumps-safe/     to      2       0     0      0     0        2       0      0     0       0     241.6     125.6
          newUnsatCoresProofs            ok      2       2     0      2     1        0       0      0     0       0      54.2      45.5
          oldUnsatCores                  ok      2       2     0      2     2        0       0      0     0       0      49.4      79.7
AUFNIRA   newUnsatCoresAssumps-safe/     ok     10       5     0      5     5        5       0      0     2       0     748.4    1630.0
          newUnsatCoresProofs            ok     10       4     0      4     0        6       0      0     0       0     850.7    2978.8
          oldUnsatCores                  ok     10       8     0      8     5        2       0      0     1       0     502.7    2048.5
BV        newUnsatCoresAssumps-safe/     ok      7       1     1      0     1        6       0      0     1       0     734.2    2065.0
          newUnsatCoresProofs            ok      7       6     3      3     4        1       0      0     0       0     246.7    1023.9
          oldUnsatCores                  ok      7       6     3      3     3        1       0      0     0       0     248.6     992.0
LIA       newUnsatCoresAssumps-safe/     to      1       0     0      0     0        1       0      0     0       0     120.9      47.7
          newUnsatCoresProofs            ok      1       1     0      1     1        0       0      0     0       0       0.3       6.5
          oldUnsatCores                  ok      1       1     0      1     1        0       0      0     0       0       0.3       5.3
LRA       newUnsatCoresAssumps-safe/     ok      5       3     0      3     3        2       0      0     3       0     450.7     260.4
          newUnsatCoresProofs            ok      5       2     0      2     0        3       0      0     0       0     537.8     424.5
          oldUnsatCores                  ok      5       2     0      2     2        3       0      0     0       0     533.8     298.5
NIA       newUnsatCoresAssumps-safe/     to      1       0     0      0     0        1       0      0     0       0     120.8      22.0
          newUnsatCoresProofs            ok      1       1     0      1     0        0       0      0     0       0      46.3      48.0
          oldUnsatCores                  ok      1       1     0      1     1        0       0      0     0       0      43.3      40.3
QF_ABV    newUnsatCoresAssumps-safe/     ok    105      70    59     11    70       35       0      0    63       0    8195.5   19363.3
          newUnsatCoresProofs            ok    105      34    24     10    17       71       0      0     5       0   11099.5   35756.7
          oldUnsatCores                  ok    105      37    23     14    18       69       0      0     1       0   11198.0   26878.1
QF_ANIA   newUnsatCoresAssumps-safe/     to      4       0     0      0     0        4       0      0     0       0     483.5    1631.8
          newUnsatCoresProofs            ok      4       4     3      1     2        0       0      0     0       0     175.1    1513.6
          oldUnsatCores                  ok      4       4     3      1     3        0       0      0     0       0     173.8    1495.1
QF_AUFLIA newUnsatCoresAssumps-safe/     ok     35       6     1      5     6       29       0      0     3       0    3718.4     524.1
          newUnsatCoresProofs            ok     35      24     4     20     1       11       0      0     0       0    2357.2   36556.0
          oldUnsatCores                  ok     35      32     5     27    29        3       0      0     5       0    1857.6   10067.7
QF_AUFNIA newUnsatCoresAssumps-safe/     ok      3       1     0      1     1        2       0      0     0       0     324.7     543.6
          newUnsatCoresProofs            ok      3       2     2      0     1        1       0      0     1       0     223.1     509.0
          oldUnsatCores                  ok      3       2     1      1     1        1       0      0     0       0     268.5     484.3
QF_AX     newUnsatCoresAssumps-safe/     ok     12       1     0      1     1       11       0      0     0       0    1379.2     391.3
          newUnsatCoresProofs            ok     12      10     0     10     0        2       0      0     0       0     528.7    7433.9
          oldUnsatCores                  ok     12      12     0     12    11        0       0      0     1       0     343.0    2855.2
QF_BV     newUnsatCoresAssumps-safe/     ok     96      56    30     26    49       39       2      0    35       0    9248.2   98058.7
          newUnsatCoresProofs            ok     96      37    26     11    23       52       7      0     7       0    9781.9  135924.7
          oldUnsatCores                  ok     96      50    29     21    24       43       3      0     7       0    9155.6  107216.0
QF_IDL    newUnsatCoresAssumps-safe/     ok    109      51    39     12    43       58       0      0    33       0   10427.2   50846.5
          newUnsatCoresProofs            ok    109      33    32      1     2       76       0      0     0       0   11692.8  108963.1
          oldUnsatCores                  ok    109      75    55     20    64       34       0      0    26       0   10088.1   53105.6
QF_LIA    newUnsatCoresAssumps-safe/     ok    306     155   111     44   138      151       0      0   119       0   25346.4   50556.0
          newUnsatCoresProofs            ok    306     117    95     22    49      189       0      0     0       0   27092.6  122894.9
          oldUnsatCores                  ok    306     187   110     77   152      119       0      0    34       0   24521.0   61261.1
QF_LRA    newUnsatCoresAssumps-safe/     ok     72      39    20     19    38       33       0      0    31       0    7475.3   16892.2
          newUnsatCoresProofs            ok     72      31    16     15     2       41       0      0     0       0    7569.3   35658.7
          oldUnsatCores                  ok     72      41    18     23    32       31       0      0     2       0    7243.2   20593.9
QF_NIA    newUnsatCoresAssumps-safe/     ok   4389    2009  1862    147  2002      903       0      0  1931       0  163975.7  280779.3
          newUnsatCoresProofs            ok   4389    2326  2156    170   752      792       0      0    37       0  151051.9  387779.8
          oldUnsatCores                  ok   4389    2394  2199    195  2174      730       0      0    81       0  146419.3  259669.8
QF_NRA    newUnsatCoresAssumps-safe/     ok    135      65    57      8    57       70       0      0    45       0   10195.7   24701.4
          newUnsatCoresProofs            ok    135      71    49     22    35       64       0      0     5       0   10825.3   32982.8
          oldUnsatCores                  ok    135      75    54     21    51       61       0      0     9       0   10865.3   27260.9
QF_RDL    newUnsatCoresAssumps-safe/     ok      7       5     1      4     5        2       0      0     1       0     564.7     958.4
          newUnsatCoresProofs            ok      7       1     1      0     0        6       0      0     0       0     842.0   11029.6
          oldUnsatCores                  ok      7       6     1      5     2        1       0      0     1       0     665.8    1982.6
QF_S      newUnsatCoresAssumps-safe/     ok      5       1     1      0     0        4       0      0     0       0     603.3     191.4
          newUnsatCoresProofs            ok      5       5     5      0     2        0       0      0     0       0     161.9     285.8
          oldUnsatCores                  ok      5       4     4      0     3        1       0      0     0       0     225.9     219.3
QF_SLIA   newUnsatCoresAssumps-safe/     ok    258      74    67      7    70      184       0      0    64       0   27245.9   20290.4
          newUnsatCoresProofs            ok    258     179   163     16    47       79       0      0     6       0   18996.0   33722.6
          oldUnsatCores                  ok    258     184   162     22   149       74       0      0     9       0   18395.8   23004.3
QF_UF     newUnsatCoresAssumps-safe/     ok     29      25     0     25     6        4       0      0     2       0    2362.4    7504.3
          newUnsatCoresProofs            ok     29       0     0      0     0       28       1      0     0       0    3508.0  124190.7
          oldUnsatCores                  ok     29      27     0     27    23        2       0      0     4       0    1866.3   13635.1
QF_UFBV   newUnsatCoresAssumps-safe/     ok      2       2     0      2     1        0       0      0     1       0     189.5    1599.3
          newUnsatCoresProofs            to      2       0     0      0     0        2       0      0     0       0     241.8    1818.8
          oldUnsatCores                  ok      2       1     0      1     1        1       0      0     0       0     193.7    1500.9
QF_UFIDL  newUnsatCoresAssumps-safe/     ok      9       9     0      9     7        0       0      0     4       0     697.0    1133.0
          newUnsatCoresProofs            to      9       0     0      0     0        9       0      0     0       0    1088.0   14652.6
          oldUnsatCores                  ok      9       5     0      5     2        4       0      0     0       0     848.5    2079.6
QF_UFLIA  newUnsatCoresAssumps-safe/     ok      1       1     0      1     0        0       0      0     0       0     117.1      76.4
          newUnsatCoresProofs            to      1       0     0      0     0        1       0      0     0       0     120.9     208.5
          oldUnsatCores                  ok      1       1     0      1     1        0       0      0     0       0     110.6     127.7
QF_UFLRA  newUnsatCoresAssumps-safe/     ok      7       4     1      3     0        0       3      0     0       0     266.6   55098.3
          newUnsatCoresProofs            mo      7       0     0      0     0        0       7      0     0       0     261.7   56000.0
          oldUnsatCores                  ok      7       7     4      3     7        0       0      0     3       0     408.4   20933.4
QF_UFNIA  newUnsatCoresAssumps-safe/     ok     48      21    19      2    21        4       0      0    20       0     592.3     880.6
          newUnsatCoresProofs            ok     48      27    22      5    18        4       0      0     1       0     641.4    1548.8
          oldUnsatCores                  ok     48      26    21      5    26        7       0      0     1       0     887.5    1044.6
QF_UFNRA  newUnsatCoresAssumps-safe/     ok      1       1     1      0     1        0       0      0     1       0     108.3      17.9
          newUnsatCoresProofs            to      1       0     0      0     0        1       0      0     0       0     120.8      19.0
          oldUnsatCores                  to      1       0     0      0     0        1       0      0     0       0     120.8      14.7
UF        newUnsatCoresAssumps-safe/     ok     21       5     0      5     5       16       0      0     5       0    2123.8    3168.7
          newUnsatCoresProofs            ok     21      13     0     13     6        8       0      0     0       0    1496.3    6617.8
          oldUnsatCores                  ok     21      16     0     16    11        5       0      0     3       0    1443.3    3919.2
UFDT      newUnsatCoresAssumps-safe/     ok     35       6     0      6     6       29       0      0     5       0    3777.0    4485.5
          newUnsatCoresProofs            ok     35      28     0     28    15        7       0      0     0       0    1416.9    4293.6
          oldUnsatCores                  ok     35      30     0     30    26        5       0      0     1       0    1406.9    3188.5
UFDTLIA   newUnsatCoresAssumps-safe/     to      4       0     0      0     0        4       0      0     0       0     483.5    1640.5
          newUnsatCoresProofs            ok      4       4     0      4     1        0       0      0     0       0     139.3     942.3
          oldUnsatCores                  ok      4       4     0      4     3        0       0      0     0       0     156.4     851.8
UFDTLIRA  newUnsatCoresAssumps-safe/     ok      1       1     0      1     1        0       0      0     1       0       0.0       3.1
          newUnsatCoresProofs            ok      1       0     0      0     0        0       0      0     0       0       0.0       3.2
          oldUnsatCores                  ok      1       0     0      0     0        0       0      0     0       0       0.0       2.7
UFDTNIRA  newUnsatCoresAssumps-safe/     ok     10       3     0      3     3        6       0      0     3       0     754.8    1386.9
          newUnsatCoresProofs            ok     10       7     0      7     5        3       0      0     0       0     377.0     848.8
          oldUnsatCores                  ok     10       7     0      7     7        3       0      0     0       0     376.5     563.4
UFLIA     newUnsatCoresAssumps-safe/     ok     24       8     0      8     8       16       0      0     8       0    2231.6    3179.2
          newUnsatCoresProofs            ok     24      14     0     14     3       10       0      0     1       0    1915.5    5131.1
          oldUnsatCores                  ok     24      15     0     15    14        9       0      0     2       0    1857.5    3479.7
UFNIA     newUnsatCoresAssumps-safe/     ok    354     183    28    155   116      133       0      0   113       0   25941.4  839089.7
          newUnsatCoresProofs            ok    354     107    17     90    28      107      92      0     2       0   23496.9 1020258.1
          oldUnsatCores                  ok    354     237    19    218   233       72       0      0    66       0   19906.9  914273.0
```

Adding python API test part 3 (#6552)

This commit (follow #6551) adds more unit tests for python API.
Subsequent commits will include additional missing functions and unit tests.

Fix strings rewriter for non-standard re range (#6570)

Fixes #6561.

Previously we missed a case where a rewrite fired for (re.range x x) where x is not a character.

Add more missing inference ids (#6313)

This also makes the relations solver use the inference manager in the standard way.

bv: Add support for --bitblast=eager. (#6516)

This PR adds support for handling --bitblast=eager in the new bitblast solver.

Fix positive contains indexof rewrites for empty string second argument (#6566)

Fixes #6560.

Remove accidental print (#6568)

Generate command line options for sphinx docs (#6555)

This PR adds documentation about the command line options to the sphinx documentation. It is mostly a reformatted version of what --help would print.

Improve handling of `:named` attributes (#6549)

Currently, when a :named attribute is used in a binder, the parser
complains about an illegal argument. This is because an argument check
in the SymbolManager fails. This is not very user friendly. This
commit makes the error message clearer for the user:

Cannot name a term in a binder (e.g., quantifiers, definitions)

To do this, the commit changes the return type for
SymbolManager::setExpressionName to include more information that can
then be used by the parser to generate an appropriate error message.

The commit also changes define-fun to not push/pop the local scope
if it has zero arguments because it is semantically equivalent to a
define-const, which allows :named terms.

Fix handling of non-standard re.range terms (#6563)

Fixes #6561. That benchmark now gives an error:
(error "expecting a single constant string term in regexp range").

This PR also makes isConstRegExp do a non-recursive dag traversal.

Loop over terms to reconstruct instead of obligations. (#6504)

This PR modifies the rcons algorithm to loop over terms to reconstruct instead of obligations. It also modifies the Obs data structure to reflect this change. The rest of the PR is mostly updating documentation and refactoring the affected code.

Fix `collectEmptyEqs()` in string utils (#6562)

Fixes #6483. The benchmark in the issue was performing the following
incorrect rewrite:

 Rewrite (str.replace "B" (str.replace (str.++ (str.replace "B" a "B") a) "B" "") "B") to (str.replace "B" a "B") by RPL_X_Y_X_SIMP.
The rewrite RPL_X_Y_X_SIMP rewrites terms of the form (str.replace x y x), where x is of length one and (= y "") rewrites to a
conjunction of equalities of the form (= y_i "") where y_i is some
term. The function responsible for collecting the terms y_i from this
conjunction, collectEmptyEqs(), returns a bool and a vector of
Nodes. The bool indicates whether all equalities in the conjunction
were of the form (= y_i ""). The rewrite RPL_X_Y_X_SIMP only applies
if this is true. However, collectEmptyEqs() had a bug where it would
not return false when all of the conjuncts were equalities but not all
of them were equalities with the empty string. This commit fixes
collectEmptyEqs() and adds tests.

Adding python API test part 2 (#6551)

This commit (follow #6546) adds more unit tests for python API.
Subsequent commits will include additional missing functions and unit tests.

(proof-new) Miscellaneous updates to strings from proof-new (#6557)

This includes:
(1) The type rule for `re.range` no longer insists on constant arguments, or a non-empty range. This is required for LFSC proof conversion, where re.range terms take arguments that are not (cvc5 internal) constants.
(2) Simplifications to reductions for indexof, which fixes proof checking errors in LFSC.