Make env hold a pointer to the original options to properly initialize subsolvers (#6705)

This PR extends the Env class to hold a pointer to the original options that are owned by the api::Solver. These original options will be used to properly initialize subsolvers as using the current options leads to subtle issues as setDefaults is not (in general) idempotent.

Remove `binary_name` option (#6693)

The binary_name is solely used as a temporary storage to pass the data from the options parser back to the runCvc5 method where it is put in a static variable. This PR gets rid of the option and the public option getter in favor of directly storing the program name in the static variable using an additional argument to parseOptions().

Change output of getRealValue to a fraction. (#6692)

Our documentation for `toPythonObj` says that real values are represented as Fractions. However, getRealValue yields a float approximation thereof.

We should probably stick to Fractions, since they allow us to precisely capture values in LRA. Also, that's more aligned with the C++ API, which returns a string representation of the (unapproximated) Rational.

Also, document some (potential) weirdness with calling mkReal on floating-point values.

Make TheoryUF compatible with central equality engine (#6695)

Work towards central equality engine.

This does some minor reorganization to TheoryUF, related to UF+cardinality constraints that makes it compatible with central equality engine. In particular, preNotifyFact is removed in favor of adding conflicts after cardinality constraints are added to the equality engine. This ensures that the central equality engine can explain conflicts that involve cardinality constraints (which will no longer be the responsibility of UF when --ee-mode=central).

Fix str.update reduction (#6696)

Fixes the 2nd benchmark from #6653.

(proof-new) Fix missing connection in trust substitution proofs (#6685)

This PR fixes a missing connection in trust substitution proofs, which was the cause of open proofs when solved equalities from ppAssert were not justified by proofs.

Also distinguishes TRUST_SUBS_EQ from TRUST_SUBS_MAP for clarity.

Remove `Options::wasSetByUser()` (#6682)

This PR removes the next heavily specialized template function Options::wasSetByUser() in favor of direct access to the *WasSetByUser flags.

(proof-new) Lazy proof chain debug names (#6680)

Support public option modules (#6691)

This PR adds the possibility to make option modules public. As shown on the example of the main driver options, this allows to get rid of the wrappers from options_public.h. We plan to make only very few option modules public (i.e. main and parser).

Remove unwanted side effects in `SPLIT_EQ_STRIP_L` (#6689)

Fixes #6681. When checking whether SPLIT_EQ_STRIP_L applies, we were
using sripSymbolicLength, which changes its inputs depending on how
many elements of the concatenation it could strip. However, one of the
arguments, pfxv0, was reused across multiple checks if the strip did
not result in a rewrite. Later invocations were wrong as a result. This
commit changes the call to stripSymbolicLength() to use a new copy of
the vector instead.

Miscellaneous changes from central ee branch (#6687)

Minor reorganization to make calls to theory engine from combination engine / shared solver more organized.

pow2: header file for pow2 solver (#6676)

This PR adds a header file for the pow2 solver. It also includes an empty test file, to trigger compilation of the header file. The next PR will include implementations and tests.

bv: Enable bitblast solver by default. (#6660)

This commit enables the new bitblast solver by default. This commit also fixes model generation for Boolean variables when --bitblast=eager is enabled.

Fixes #3958, #5396, #5736, #5743, #5947.

Add missing dereference (#6684)

Fix handling of start index in `str.indexof_re` (#6674)

Fixes #6636, fixes #6637. When the start index was non-zero, the result of
str.indexof_re was not properly restricted to be greater or equal to
the start index. This commit fixes the issue by making the eager
reduction lemma more precise. Additionally, the commit fixes an issue
with the lower bound of the length of the match in str.indexof_re.

Some cleanup in `mkoptions.py` (#6667)

This PR does some general cleanup in the mkoptions.py script: removal of obsolete code and some fixes to the comments.

docs: Migrate datatypes theory reference. (#6662)

This migrates https://cvc4.github.io/datatypes.

Adding unit tests for the datatypes python API (#6658)

This commit adds unit tests that are translated from `datatype_api_black.cpp`. One API function is also added to the python API.
This is the last part of the python api unit tests for datatypes.

Co-authored-by: Andres Noetzli <andres.noetzli@gmail.com>

Simplify automatic set-logic in smt2 parser (#6678)

This simplifies the smt2 parser so that automatically setting the logic is done directly instead of being buffered as a command.

This prevents spurious errors for features that require (A) checking the logic is set and (B) fully intialize the underlying SMT engine.  `declare-pool` is an example of an smt2 command where the user will get an error (instead of a warning) when set-logic is not used due to setting the logic, after fully initing SMT engine and then executing the buffered set-logic command.

Note this should also make dump=raw-benchmark more accurate (no set-logic is included when dumping benchmarks with no set-logic command).

[GitHub Actions] Make caching of dependencies depend on image version (#6677)

Our Clang builds started to fail to link when the environment changed. This commit changes our CI to only use cached dependencies if the build environment has not changed.

Renaming pow2 to p2 in regression tests (#6675)

We plan to add a unary pow2 operator to cvc5, that is obtained from the binary operator pow by fixing the first argument to 2.
An initial working branch is here: https://github.com/yoni206/cvc5/tree/pow2

This PR does the first step, which is to rename some uninterpreted symbols in regression tests from pow2 to p2, to avoid clashing with the new operator.

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