Do not eagerly preprocess seq.nth (#8937)

Fixes #8936.

Revert usage of seq.nth in reductions (#8939)

Fixes #8932. Fixes #8926.

Fix pto handling for heaps that are not a subset of the base heap (#8942)

These require a downwards rule to be compatible with our propagation rules for pto.

Fixes #8863.

Add rel.project operator to sets (#8929)

Update SMT-COMP scripts (#8930)

Remove `Theory::postsolve()` (#8924)

The feature was not used. This commit also uses the removal to simplify
`SolverEngine` a bit.

Remove spurious pto singleton inference (#8925)

This removes a spurious lemma schema that is already covered by SEP_POS_REDUCTION.

[SMT-COMP] Update use of `--decision` option (#8922)

The name of the mode changed from justification-stoponly to just
stoponly.

Fix injectivity inferences for seq.nth applied to strings (#8920)

Fixes #8916.

Fix type issue in substitutions from covering solver (#8921)

Fixes #8895. The benchmark in that issue now times out.

Add  set.aggr operator to sets (#8878)

This PR depends on #8876

Fix reduction for seq.nth for strings (#8919)

Fixes #8918.

Fix model construction for str.unit (#8917)

Fixes #8915.

Add rel.group operator to sets (#8876)

This PR is dependent on #8819 and #8867.

Move `SymbolManager` and `SymbolTable` to parser (#8910)

This moves `SymbolManager` and `SymbolTable` to the parser. To do so, it
modifies headers in the `context` package to be public to the parser
(changes `cvc5_private.h` to `cvc5parser_public.h`), because they are
shared between the parser and the main library.

[Docs] Update `EnumDocumenter` for newer Sphinx (#8914)

The `no_docstring` argument of
`sphinx.ext.autodoc.Documenter.add_content()` has been
[deprecated](https://www.sphinx-doc.org/en/master/changes.html) since
Sphinx 3.4.0 (released in December 2020). It seems that newer Sphinx
versions have removed that argument, which breaks our `EnumDocumenter`
(e.g., see the following
[example](https://github.com/cvc5/cvc5/runs/7081097179?check_suite_focus=true)).
This commit updates our use of
`sphinx.ext.autodoc.Documenter.add_content()`.

Revert change in lemma order in prop engine (#8911)

This reverts the change in lemma order from #8301.

Add inference rules for table.group (#8819)

Remove `CommandSequence` command (#8904)

The CommandSequence command was not widely used and was essentially
just replicating the functionality of a vector of commands. This is work
towards a streamlined parser API.

Move non-stream options out of `printer_options.toml` (#8909)

After #8827, we automatically generate code for the options listed in printer_options.toml, which allows those options to be set on input/output streams. Some of the options that are currently in printer_options.toml are not a good fit for that and this commit moves them out of the file. This is in preparation of making that stream options public (or at public in the parser), because some commands require setting stream options.

Fix explanation for strings unit oob inference (#8908)

Fixes #8906.

Add set.fold operator (#8867)

Fix rewrite for `(to_int real.pi)` (#8907)

Fixes #8905. (to_int real.pi) was returning a real constant instead of
an integer, making the type of the rewritten term wrong.

Fix handling of injectivity for str.unit (#8899)

Fixes #8890.

print run_process command (#8859)

Remove `Command::clone()` (#8903)

This code was unused. This is work towards a streamlined parser API.

Simplify printing of command results (#8902)

This moves redundant code from `Command::printResult()` overrides to the
base method. This is a step towards simplifying printing options, which
is needed to fix #8893 (which itself is a step towards a parser API).

Avoid quoting symbols already surrounded with vertical bars (#8896)

This PR fixes the issue of replacing bars with underscores in already quoted symbols.
For example previously this line would print |_a _|

std::cout << d_solver.declareFun("|a |", {}, d_solver.getRealSort());
Now it prints |a |.

Fix sort inference for equality over finite types (#8897)

Sort inference for equality was not considering equality over some finite types, leading to potential solution soundness.

Fixes #8883.

Add type to uninterpreted constant values (#8891)

Before
```smt2
(define-fun x () UInt (as @a_0 UInt))
(define-fun y () Atom (as @a_0 Atom))
```
After

```smt2
(define-fun x () UInt (as @UInt_0 UInt))
(define-fun y () Atom (as @Atom_0 Atom))
```

[Parser] Rename generated `.c` to `.cpp` files (#8894)

Using Clang on my machine, I am seeing the following warning:

```
clang-13: warning: treating 'c' input as 'c++' when in C++ mode, this behavior is deprecated [-Wdeprecated]
```

This is because we are treating the generated `.c` files as C++
files. To make our build system more robust, this commit
changes our command for generating files to rename the
generated files to use the `.cpp` extension.

Remove unused `DeclarationSequence` command (#8892)

Remove redundant projection operators (#8889)

This removes all projection operators for tuples and tables except a generic one `ProjectOp`.
It also updates the number of indices and other issues in cvc5.cpp

Add support for operators with same payload (#8886)

This fixes an issue with supporting operators with the same payload. It
changes the API to use the `mkConst()` overload that passes an explicit
kind, which is required when the same payload is shared by multiple
kinds.

[CMake] Remove redundant code (#8885)

Disable parser regression for competition builds (#8884)

Competition builds do not print parser errors. This leads to a Buildbot
failure on one of our regressions for the competition build. Thus, this
commit changes the failing regression to be skipped for competition
builds.

[Regressions] Disable ASan on slow regression (#8882)

This should fix one of our Buildbot failures.

[CMake] Fix `install()` commands (#8879)

This fixes two issues related to `install()` commands:

- It removes the installation of object files from the parser. Before,
  `make install` would add unnecessary object files to the library
  directory.
- It ensures that all artifacts related to the `cvc5` target are
  installed in the library directory. DLL files [count as `RUNTIME`
  artifacts](https://cmake.org/cmake/help/latest/command/install.html),
  so `libcvc5.dll` was not installed in the `lib/` directory with `make
  install`.

bv sat solvers: Update CaDiCaL and Kissat to most recent release versions. (#8877)

Infrastructure for portfolio solving (#8709)

We want to replace the set of competition scripts by an internal portfolio mechanism. It seems that this portfolio mechanism is best implemented from scratch in the driver instead of using, e.g., --tlimit or --tlimit-per.

This PR introduces the infrastructure for that, implementing the following approach:
first parse the input until a logic has been specified; if more than one configuration is to be used, parse the remaining commands into a vector; for every configuration, we fork the main process, and in the child process configure the solver and replay the vectors.

[Win64] Use `CC_FOR_BUILD` when compiling GMP (#8874)

This restores the use of the `CC_FOR_BUILD` environment variable. It was
(accidentally) removed in 4337cdb8e2a071ded73dbc9236c8bb2f4d42e6e5 after
it was added in b0500dd28ec42d6a1bada80d34b74ce8aea896cc. Without
`CC_FOR_BUILD`, cross-compilation of GMP fails on Arch Linux.

[Java API] Do not link JNI libraries (#8870)

Fixes #8869. We are not using `libjawt.so` or `libjvm.so` (we are not
using the Java Invocation API), so we don't need to link `libcvc5jni`
against `JNI_LIBRARIES`. This change allows us to use cvc5 from Java
without linking against the JNI libraries (see changes in the `examples`
folder).

Move slow regression (#8866)

To address a buildbot failure.

Allow mixed int/real equalities in non-strict parsing mode (#8865)

Add set.filter operator and its inference rules (#8856)

Remove redundant options headers from TPTP parser. (#8864)

Fixes #8861.

Add str.unit to LFSC signature (#8862)

Fixes buildbot failure.

Add set.map signature to lfsc (#8860)

Fix buildbot failure

Use STRING_NTH in strings reductions and eliminate STRING_TO_CODE (#8851)

This updates our string reductions for `to_lower`, `to_upper`, `from_int`, `to_int` to use STRING_NTH instead of STRING_TO_CODE applied to STRING_SUBSTR.

It optionally replaces STRING_TO_CODE with STRING_NTH during preprocessing (true by default).

This is work towards efficient support for `to_lower`/`to_upper`.

[CMake] Improve FindGMP (#8846)

Fixes #8792. This commit fixes issues with/improves our current
implementation of FindGMP:

- Version check that does not rely on regex matches in `gmp.h`. Instead,
  this commit uses a test program that checks at compile-time whether
  the GMP version is recent enough. This is more robust, because on some
  systems (such as Fedora), `gmp.h` includes another file that has that
  version information.
- It now also checks for the `gmpxx.h` header and the `gmpxx` library.
- The commit changes the compile test to use the include directories and
  libraries that were found using `find_path` and `find_library`.

Disable `lfsc` tester if `proof` tester is disabled. (#8857)

This automatically disables the `lfsc` tester for regressions where `proof` tester is disabled.

Add MBQI to SMT comp script (#8858)

Also fixes 2 existing issues in the script (that @nafur pointed out).

Add declareOracleFun to the Java API (#8815)

Disable LFSC for regression with learned rewrite (#8855)

Fixes buildbot issues.

Fix corner case of interpolants from conjectures with no free variables (#8853)

Fixes #8852.

Add inference rules for set.map operator (#8849)

Fix check for whether a term contains an uninterpreted constant (#8845)

Fixes #8842.

We now say "unknown" for the benchmark on that issue.

Disable arithmetic static learning when unsat cores are enabled (#8830)

The arithmetic static learner uses non-local reasoning and does not have proof support. Thus it may rewrite A ^ B to A ^ B' where ( A ^ B ) => B', but the preprocessor by default assumes that the replacement is such that B => B'.

This disables the arithmetic static learner when unsat cores are enabled. Other static learning appears to be local and is still enabled.

This further corrects an issue in set_defaults that checked incompatibility with unsat cores based on whether proofs are enabled. We now check compatibility independent of whether proofs are enabled. This also corrects several restrictions on things that previously were treated as being incompatible with unsat cores (but not proof unsat cores) that were spurious.

Fixes #8822.

Eliminate static options access from pattern term selector (#8825)

Towards eliminating options scopes.

Preparation for SEQ_NTH applied to strings (#8779)

No behavior changes in this commit for current main.

[proofs] [sat] [cores] Fix unsat cores based on the SAT proof (#8850)

The justifications for the theory lemmas (i.e., THEORY_LEMMA steps) sometimes was not being properly connected with the actual clause inserted into the SAT solver, leading to open proofs. The issue was triggered by a regression being added in ##8819, so we don't need to add one here.

Fix missing conclusion for sep pto neg prop (#8844)

Was introduced in the refactoring in #8768.

Fixes #8841.

Restricting the bit-width in int-to-bv (#8814)

`cvc5` only supports bit-widths of `unsigned` size for BitVector sorts (see, e.g., [here](https://github.com/cvc5/cvc5/blob/4338d9d49a41022d34cd4cbabf17a66fdf39efae/src/expr/node_manager_template.cpp#L178)).

This checks that the provided bit-width for the `int-to-bv` option is in the right range.

Fixes https://github.com/cvc5/cvc5-projects/issues/425 and includes a regression that is based on the test from the issue.

Disable arrays in eager bit-blasting (#8785)

Fixes cvc5/cvc5-projects#461 . This does not allow arrays in eager bit-blasting, that is, only QF_BV and QF_UFBV are allowed. The reason is that Ackermannization (which is turned on in eager bit-blasting) eliminates array operators but does not eliminate array variables, that later cause a logic exception.

Make interpolation robust to conjectures with no shared variables (#8840)

Fixes #8833.

Refactor how options are passed to the printer (#8827)

Right now, the printers expect some options to be passed explicitly and read other options statically from the options object.
This refactors this, using the `ioutils` utility which we already use to store option values in the private storage associated with output streams. In detail, does a couple of things:
- the `mkoptions.py` script now generates the `options/io_utils.*` files to handle all options defined in the `printer` options module
- reading the necessary options from the ostreams is pushed into the printers themselves
- explicit options are removed from (almost) all `toStream()` functions
- a few options are moved to the `printer` options module (making the `printSuccess` utility obsolete)

Make subs minimize utility robust to non-constant evaluation (#8839)

Fixes #8834.

Fix issues with to_real around coverings solver (#8837)

This PR fixes two issues with the (missing) handling of to_real.
The first is that equality substitution was not aware of to_real yet, possible introducing models for both x and (to_real x).
The second is that the conversion to libpoly polynomials would also not properly unpack to_real expressions.
Fixes #8835.

Fix FindCaDiCaL script (#8838)

This fixes issues with finding a system-installed cadical.
Fixes #8836.

Update to GoogleTest 1.11.0 (#8813)

Using GoogleTest 1.10.0, when trying to build unit tests on m1 mac an error about deprecated methods fails the compilation of gtest.

Eliminate more static options accesses (#8832)

Eliminate static options access for central ee (#8823)

Also refactors TheoryEngine to not maintain its own reference to logic info and an accessor to it.

Towards eliminating option scopes.

Eliminate static options access in skolemize (#8831)

Fix mixed arithmetic issue in relevant domain (#8826)

Fixes #8821.

Eliminate static options access in BV inverter (#8829)

Make Rewriter::rewrite non-static (#8828)

This furthermore eliminates smt::currentSolverEngine.

Use function array constants in HO solver (#8818)

This makes lambdas rewrite to function array constants when possible. This extends our HO solver and utilities to be robust to check whether a node represents a lambda (uf::FunctionConst::toLambda).

This furthermore removes the isConst rule for LAMBDA; lambdas are never constant.

The PR also improves our check-model so that warnings are not thrown if rewriting can show that the model value of a term is equivalent modulo rewriting to its representative in the model equality engine.

This eliminates the last remaining static calls to rewrite. This is work towards eliminating SmtEngineScope.

Make sure phase-shift lemma is properly typed (#8824)

This PR addresses #8773 by making sure that the phase shift lemmas generated by the sine solver are properly typed.

Eliminate some static options access (#8795)

In preparation for eliminating options scopes.

[proofs] [alethe] Remove static call to options from post-processor (#8817)

Add model-based quantifier instantiation (#8729)

This is a straightforward reimplementation of Ge/deMoura from CAV 2009.

Eliminate static access to dtSharedSelectors (#8804)

Towards eliminating option scopes.

Eliminate more static options accesses (#8802)

A block of code changed indentation in the induction solver, this is cleaned to conform to guidelines.

Introduce function array constant (#8793)

This introduces the FUNCTION_ARRAY_CONST kind and its payload FunctionArrayConst.

This is in preparation for refactoring isConst for functions in higher-order.

In particular, the plan is to never consider LAMBDA to denote a value of function sort. Instead, lambdas may be written to function array constants, whose uniqueness is trivial to justify.

This refactoring when completed will furthermore eliminate the last remaining static calls to the rewriter, to be done in a followup PR.

Fix subtype issues in proofs for nonlinear solver (#8782)

Causes a debug proof failure on proof-new.

bv: Disable rule ExtractArith. (#8816)

Add table.group operator (#8731)

Add declareOracleFun to API (#8794)

Java and Python will be added in followup PRs.

Remove spurious assertion in isLegalElimination (#8812)

Fixes #8805.

The isLegalElimination method correctly catches Int -> Real as an illegal elimination.

Make model core robust to when we cannot show the model satisfies input (#8811)

Fixes #8807.

bv: Add resource limits support for CaDiCaL. (#8788)

Fixes #8776.

Simplification of smt2 printer for type ascriptions (#8801)

Previously had code for dealing with subtypes

Move smt_util to preprocessing/util (#8799)

src/smt_util contains a single file that is only used by the miplib trick preprocessing pass. This moves it to preprocessing/util.

Reenable assertion in skolem definition manager (#8797)

This reenables a variant of an assertion that was deleted in #8749, a weaker version of that assertion should now hold.

Add option to send all instantiations in a bounded range (#8796)

There is a block of code in FMF instantiation that is questionable whether it is helpful, in particular for dealing with string reductions for long strings.

Add cross-compilation for arm64 on macOS (#8758)

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

More removing of unused code (#8806)

Trying to break cycles when printing a .dot DAG (#8698)

Change the way cvc5 traverse and print the proof when --proof-dot-dag option is used. The main change is related to the way the printer deals with cycles between proof nodes that are in a ancestor/descendant relationship. The new conditions are:

- If any proof node under a first proof node has the hash equal to the first one, this would introduces a cycle. To avoid it, then no sharing between nodes happens in this case.

Signed-off-by: Vinícius Braga Freire vinicius.braga.freire@gmail.com

New way to identify THEORY_LEMMA clusters when printing in the .dot format (#8745)

Change the way cvc5 identifies THEORY_LEMMA clusters when --print-dot-clusters option is used. Previously, only proof nodes with SCOPE rule after a CNF cluster could identify a THEORY_LEMMA cluster. Now, any of the following rules, after a CNF cluster, can identify it:

1. SCOPE
2. THEORY_LEMMA
3. Any rule R in the following range: CNF_ITE_NEG3 < R < LFSC_RULE

Signed-off-by: Vinícius Braga Freire vinicius.braga.freire@gmail.com

Minor deleting of unused code (#8800)

Towards improving coverage.