Generalize congruence handling for HO in eq proofs (#6883)

Previously we were not considering proofs for HO equalities (i.e., between operators) that were transitivity chains. This commit generalizes the elaboration procedure in eq_proof to do so.

Fix for context on input proof generator (#6873)

The preprocess proof generator uses a dummy CDProof to mark input assertions that do not need justification. This CDProof should be user-context dependent to avoid rare cases where an input assertion was the symmetric equality of another, it was previously context independent.

This also refactors the debugging traces in this class.

Move synthesis verification check to own file (#6882)

In preparation for more extensions to this aspect of the synthesis solver.

Refactor setup of proof equality engine for central EE (#6831)

Users of an equality engine should each use the same proof equality engine that wraps it. This ensures that theory inference managers do so, by tracking the official proof equality engine for an equality engine in theory inference manager.

This is in preparation for (proper equality proofs for) central equality engine.

It also adds some debugging code that is highly useful for debugging issues related to when equalities are processed in theory inference manager.

Fix models for sequences of infinite element type (#6870)

This fixes our model construction for sequences of infinite element type.

We were relying on getModelValue in our model construction which is incorrect since it assumes that the element type's theory can provide concrete values during model generation time. This makes the sequence model construction more robust by generalizing how model values are assigned: we use skeletons instead of concrete values when the element type is infinite.

This fixes some open model generation issues with Facebook benchmarks.

Clean up option usage in command executor (#6844)

This PR makes the CommandExecutor class use the options object from its SmtEngine instead of the driver one. This makes sure that options that are set via (set-option ...) are in effect for the CommandExecutor. It still stores the driver options, though, as they are used for resets.
The PR also does some minor cleanups along the way (remove unused pOptions, make things const).
Fixes #2376.

Add missing space for check macro error messages. (#6875)

bv: Add missing BV_EAGER_ATOM proof rule. (#6874)

Fixes an issue with --proof-eager-checking and --bitblast=eager.

bv: Simplify BV_BITBLAST_* proof rules. (#6871)

Introduces BV_BITBLAST_STEP rule, which replaces BV_BITBLAST_X rules.

[rewriter] Add rewrite to order IFF (equality for Booleans) (#6872)

Not doing this rewrite for Booleans is probably an artifact of the old IFF kind being removed. This rewrite is important to simplify the generation of proofs for the SAT solver, as clarified in the new comment in the SAT proof manager.

bv: Do not rewrite below BV leafs in BBProof's TConvProofGenerator. (#6869)

Introduces a TermContext class that can be used to skip rewrites below theory leafs. Fixes issues related to bit-vector leafs begin incorrectly rewritten.

Add branch and bound lemma if linear arithmetic generates a non-integer assignment (#6868)

This double checks that TheoryArithPrivate generates a model that does not assign real values to integer variables.

This is done outside of TheoryArithPrivate intentionally, so that it can be checked independently.

This code should very rarely be applied but would have caught the incorrect model which led to wrong results in the UFNIA division of smtcomp 2021.

bv: Expand bitblast proof steps in the proof post processor. (#6867)

This commit changes BV proof logging to record coarse-grained bit-blast steps during solving and expanding these steps on-demand in the proof post processor.

Add branch and bound (#6865)

This PR moves https://github.com/cvc5/cvc5/blob/master/src/theory/arith/theory_arith_private.cpp#L3451 to its own module.

The next PR will connect this module to theory_arith / theory_arith_private.

Towards ensuring type constraints are met for linear arithmetic models.

Fix for learned rewrite pass, add regression (#6850)

Fixes #4791.

Fix ANTLR build on CMake <3.11 (#6864)

With CMake 3.11 and later, `<DOWNLOAD_DIR>` is substituted in
`ExternalProject_Add` but not in older versions [0]. To maintain
compatibility with older versions of CMake, this commit changes
`ExternalProject_Add` to use `<DOWNLOADED_FILE>` instead, which is both
nicer and substituted in older versions of CMake.

[0] https://cmake.org/cmake/help/latest/release/3.11.html#modules

Add arithmetic preprocess rewrite equality module (#6860)

This is the first part of a refactoring which will ensure that the linear arithmetic solver does not violate integer type constraints in its model.

This PR moves the method https://github.com/ajreynol/CVC4/blob/master/src/theory/arith/theory_arith.cpp#L129 to its own module / file.

Add trace for combination splits (#6862)

Followup PRs will unify these with the lemmas / stats infrastructure in theory inference manager.

Use default visibility for `cvc5::Exception` (#6856)

Currently, `cvc5::Exception` does not have default visibility, which can
cause cvc5 to terminate when trying to catch it in `main.cpp`.
Presumably, this is because the necessary typeinfo is missing [0]. Due
to this issue, production builds for M1 on macOS crashed when parser
exceptions were thrown. The commit changes the visibility of the
exception.

[0] https://gcc.gnu.org/wiki/Visibility,
    "Problems with C++ exceptions (please read!)"

Improvements to debug check model (#6861)

This makes it so that debug-check-models applies in production mode, not just in debug mode. It also verifies that type constraints are met.

test also with default cores (#6858)

Have unsat cores regression tested also with default mode.

Make regression test `issue4971-0` more robust (#6857)

When compiling and running cvc5 on macOS with an M1 CPU, the regression
test regress0/cores/issue4971-0.smt2 returned unsat instead of the
expected unknown for the first (check-sat) command. This commit
makes the regression more robust by adding --cegqi-full and expecting
unsat.

Use newer config.sub to fix build on Apple M1 (#6854)

When building cvc5 on macOS for M1 natively, ANTLR's version of
`config.sub` does not recognize `aarch64-apple-darwin20.5.0`. This
commit fixes that issue by downloading the latest version of
`config.sub` (similar to what we are already doing for `config.guess`).
The commit also updates the URLs for `config.guess` and `config.sub` to
the URLs recommended in the files themselves. The commit also does some
minor cleanup/simplifications of the commands for building ANTLR.

Fix sets cardinality inference involving equivalent parents (#6855)

This fixes an unsoundness issue in the sets + cardinality solver.

One rule of this solver applies in sets when two parents of a child of a cardinality graph are equal, in which case we know that child or one of its siblings must be equal to the opposite parent. For example, this rule tells us that:

if T = (union T S), then (intersect T S) = S.

The explanation of this rule could consider the representative term of one the parents instead of the term itself say (union T S) is representative T, giving the unsound inference: if (union T S) = (union T S), then (intersect T S) = S. This ensures we use the original terms.

This PR also does some minor cleanup.

Implement stop-only for new justification heuristic (#6847)

This also refactors decision engine so that we use inheritance instead of a dummy flag + members to determine which implementation to use.

Disable ordering heuristic for justification by default (#6848)

Add script to build wheel for pycvc5 (#6839)

This PR adds a script for building a wheel distribution for pycvc5. It automatically reads the top-level CMakeLists.txt to obtain the current version number, and then runs the standard setup from setuptools with an extension command class that configures and builds cvc5 with Python bindings. This wheel file is sufficient for uploading to Pypi. Although, note that we need to build for different operating systems and different Python versions because of the extension modules.

Note: another option is to use the scikit-build instead of doing the configuring and building manually. However, I ran into some issues when the setup.py file was not at the top-level. Because we prefer to have it hidden in a sub-folder, I took the manual route for now. In the future, we could consider changing this.

[proof] [dot] Print let map (of terms in proof) as part of dot proof (#6853)

The let map is printed as JSON-like dictionary via a comment of the dot output.

[unsat cores] Adding regressions from #4971 (#6852)

Adds remaining regressions from issue #4791, which we can handle with the different new unsat-core modes. Note that issue4971-1.smt2 requires the sat-proof mode for unsat cores.

pow2: Update NEWS. (#6851)

Rename operator pow2 to int.pow2. (#6849)

This name is the name of the symbol we parse. Internally, we still call
it POW2. This is a fix for the problem that `pow2` may clash (and
already does clash on SMT-LIB benchmarks) with user-defined symbols.

Fix regressions for competition build (#6846)

Fixes one of the issues in the nightlies.

Standard output for trigger selection (#6841)

Fixes #6259.

Integrate Lazard into CAD module (#6812)

This PR adds two new command line options that govern how the CAD module does projection and lifting, allowing to use the new Lazard evaluation. By default, we use McCallum with regular lifting which does not require CoCoA.
Additionally, this PR adds a bunch of unit tests for the CAD module.

Integrate learned rewrite preprocessing pass (#6840)

This adds the learned rewrite preprocessing pass, which rewrites the input formula based on (typically theory specific) reasoning about learned literals. The main motivation is for preprocessing ints division/modulus based on bounds.

Add implementation of learned rewrite pass (#6843)

Add learned rewrite preprocessing pass (#6842)

Adds the basic skeleton of the pass.

Porting C++ API examples to SMT-LIB examples (#6789)

SyGuS examples will come later.

Add some printing functions for OptimizationObjective and OptimizationResult (#6809)

Implement the operator << with std::ostream for OptimizationObjective and OptimizationResult. Currently only supports SMTLib2 or Sygus as output languages.
Objective: (maximize [node] :signed) or (minimize [node]) or ...
Result: (sat [expr]) or (unsat) or (unknown([explanation]) [expr/null])

Add doc page about transcendentals (#6755)

This PR adds a theory reference page for the transcendental extension.

[Strings] Fix incorrect rewrite (#6837)

Fixes #6834. There were two cases in our extended rewriter for string
equalities that were modifying the node without returning and without
updating information computed from the original node. This mismatch led
to incorrect rewrites. This commit fixes the issue by adding a flag to
returnRewrite() that determines whether node that was an equality
before and after the rewrite should be rewritten again with the extended
rewriter. We generally do not do that (we'd run in danger of rewriting
equality nodes with the extended rewriter even though we shouldn't) but
for the rewrites that were previously continuing to rewrite the node, we
set this flag and return. This ensures that we do not have an issue with
information being out of date. The commit additionally fixes an issue
where we would apply the rewrite STR_EQ_UNIFY even though the node
hadn't changed.

Make buffered inference manager more robust to backtracking (#6833)

This makes TheoryEngine notify all theories when a theory sends a conflict. This means that buffered inference managers always clear their buffers when any theory sends a conflict.

This is required for making theories robust to conflicts that may arise when using the central equality engine, where a different theory may raise a conflict during another theory's check.

Fix performance of string regression (#6832)

Regression cmu-dis-0707-3.smt2 has been timing out when using an ASan
build after commit a4f38d6. Before that
commit --strings-exp implicitly enabled --fmf-bound. After the
commit, the solver was supposed to apply the same reasoning but only to
interal quantifiers and without enabling --fmf-bound. However, the
commit missed some options checks that now also have to check whether
--strings-exp is enabled. This commit updates those option checks.
With this fix, we get a slightly different value for bug590.smt2 after
replying unknown. This commit updates the regression to be more lenient
with the value returned.

Add output tags -o, --output. (#6826)

Output tags are similar to debug/trace tags, but are always enabled
(except for muzzled builds) to provide useful information for users.

Available output tags can be queried via -o help/--output help and are
specified in the base options module via enum values.

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

Fix bv assert input reset assertions (#6820)

If reset-assertions was called it will now reset the SAT solver and the
CNF stream if clauses were permanently added to the SAT solver via
option --bv-assert-input.

Fix rewriter for negative constant seq.nth (#6827)

Fixes #6777.

Fix CaDiCaL auto-download on macOS (#6828)

* Fix CaDiCaL auto-download on macOS

If we are auto-downloading CaDiCaL, we are manually instantiating its makefile.
To do that, we use `CMAKE_CXX_COMPILER` for the compiler and assemble some
flags. However, we are missing the platform dependent flags. Specifically, we
need to set `-isysroot` on macOS to make sure that the header files are found
because they are not at /usr/include on newer versions of Apple's XCode [0].
Unfortunately, I could not find a CMake variable with the platform specific
flags. They are assembled here [1]. To solve this problem, the commit checks if
`CMAKE_OSX_SYSROOT` is set and adds a corresponding compiler flag if it is.

[0] https://developer.apple.com/documentation/xcode-release-notes/xcode-10-release-notes
[1] https://github.com/Kitware/CMake/blob/d60d6c269ae7ad15adbb82028e9ab50290db2a2b/Source/cmLocalGenerator.cxx#L1900-L1923

Refactor lexer for SMT-LIB in sphinx (#6805)

This PR refactors the lexer used by sphinx for highlighting SMT-LIB files. This new lexer properly checks for word boundaries and uses the proper character sets from the SMT-LIB standard.

Add reverse iterators to `Node`/`TNode` (#6825)

This feature is useful for example for succinctly inserting children of
a node in the reverse order. To make this work, the commit fixes the
declaration of `reference` in the `NodeValue::iterator`. The
`std::reverse_iterator` adapter expects the `reference` type to match
the return type of `operator*` in the corresponding iterator (as
mandated by the standard). Despite its name, `reference` does not have
to be a C++ reference. Note that we cannot actually make it a C++
reference because `NodeValue::iterator` wraps the `NodeValue*` in a
`Node`/`TNode` in `operator*`.

Add recursive function definitions to subsolver in sygus (#6824)

This passes recursive function definitions to the verification subsolver in sygus, with a default bounded limit of 3. This required improving the interface for setting up subsolvers by allowing custom options; the sygus solver statically computes an instance of the options that it uses in all calls.

This allows us to solve non-PBE sygus problems with recursive function definitions. The PR adds an example.

Fix message to show that cadical and symfpu are required (#6823)

As mentioned in #6822, we are currently printing an incorrect message if CaDiCaL or SymFPU are not found but auto-download is disabled. This PR fixes this issue.

Add option to limit the number of instantiation rounds (#6818)

This adds an option to limit the number of instantiation rounds used by quantifiers engine.

This option may be generally useful for making quantifiers terminating. It also is necessary to update the new default behavior of SyGuS + recursive functions. A followup PR will make sygus verification calls set the option added on this PR automatically, so that we use incomplete + termination strategies for (non-PBE) sygus in the presence of recursive functions.

This PR also makes minor improvements to the quantifier utility infrastructure.

Use SAT context level for --bv-assert-input instead of decision level. (#6758)

The decision level as previously implemented was not accurate since it
did not consider the user context level. This resulted in facts being
incorrectly recognized as input assertions, which happened for
incremental benchmarks.

Use authored date instead of commit date. (#6815)

This commit fixes a subtle issue with pruning the old docs from docs-ci. We remove docs that are older than one week. However, we used the commit date instead of the authored date. Since we actually squash the old commits (that are older than four weeks) regularly, the commit date is always newer.

pow2: new test (#6819)

This PR adds a more "real life" unit test for the pow2 solver. Thanks @4tXJ7f for the help with the options.

Do not notify during equality engine initialization (#6817)

This is an alternative fix to https://github.com/cvc5/cvc5/pull/6808.

This ensures that we do not notify the provided class of an equality engine during initialization.

Do not apply fmfBound to standard quantifiers when only stringsExp is enabled (#6816)

There are compelling use cases that combine strings/sequences and quantifiers. Prior to this PR, strings enabled "bounded integer" quantifier instantiation so that internally generated quantifiers for strings reductions are handled in a complete manner. However, this enabled bounded integer quantifier instantiation globally. This degrades performance for "unsat" on quantified formulas in general.

After this PR, we do not enable bounded integer quantifier globally. Instead, we ensure that bounded integer quantification is applied to at least the internally generated quantified formulas; all other quantified formulas are handled as usual.

Notice this required ensuring that all quantified formulas generated by strings are marked properly. It also required adding --fmf-bound to a few regressions that explicitly require it.

Fix pre vs. post-rewrite in proofs for theory preprocessor (#6801)

This changes an annotation of a step of rewriting from "post" to "pre" in the theory preprocessor.
Fixes #6754.

int-to-bv: correct model values (#6811)

the int-to-bv preprocessing pass produced wrong models.
This PR fixes this in a similar fashion to other preprocessing passes, by adding a substitution to the preprocessing pass context. This requires moving the main translation function to be a class method, rather than a helper method in an empty namespace.

Thanks to @alex-ozdemir for raising this issue and producing a triggering benchmark (added to regressions in this PR).

Add new variants for the CAD projection (#6794)

This PR adds variants for the CAD projection operator to use Lazard's projection operator.

Fix statistics in AigBitblaster. (#6810)

Fixes #6788

FP: Refactor, rewrite and clean up word blasting. (#6802)

This rewrites the word blasting function FpConverter::convert to be
easier to follow and read. It further cleans up several things.

This additionally prepares for allowing to convert incoming facts rather
than terms registered with theory FP. That is, when word blasting more
lazily, in preNotifyFact rather than in registerTerm.

Rewrite POW to POW2 when the base is 2 (#6806)

This PR introduces a rewrite from (^ 2 t) to (pow2 t) in order to make use of the specialized pow2 solver.
One regression that expects an error when t is not a constant is changed accordingly.

Rename internal string kinds to match API (#6797)

This commit replaces (old) internal string kind names to match the API / smt2 standard names.

Further fix #6453 (#6804)

There's one spot left in issue #6453, that is the call to `std::allocator<T>::destroy` in `mkMetaKind`. And this commit fixes it.

[proof] [dot] Make dot printer stateful (#6799)

In preparation for further changes in the printer.

pow2 -- final changes (#6800)

This commit adds the remaining changes for a working and integrated `pow2` solver.

In particular, it adds a rewrite and a lemma that identify `pow2(x)` with `0` whenever `x<0`.
Regressions are added as well, including `pow2-native-0.smt2` that shows the semantics of `pow2` on negative values.

The next steps are new rewrites and and more lemma schemas.

pow2: Adding monotonicity lemma  (#6793)

We add the lemma x<=y --> pow2(x)<=pow2(y) to the pow2 solver.
Additionally, some renaming of variables is introduced for better clarity.

api: getRealValue: Fix printing of integer values. (#6795)

cmake: Add new code coverage targets. (#6796)

This commit adds the following new code coverage targets:

- coverage-reset: Resets the code coverage counters

- coverage: Generates code coverage report for all cvc5 executions since the
            last coverage-reset

- coverage-test: This was previously the coverage target that runs the
                 tests and generates the coverage report (as used for
                 nightlies).

By using `make coverage-reset` and `make coverage` it is now possible to
generate coverage reports for arbitrary executions of cvc5.

Fix linear arithmetic for duplicate lemmas in incremental (#6784)

The linear arithmetic solver was not robust to cases where a duplicate lemma is emitted. This leads to non-linear arithmetic not being called to check at full effort, leading to potential model soundness issues.

Fixes #6773.

Add CoCoA implementation (#6733)

This PR adds the actual implementation for the Lazard evaluation based on CoCoALib. It is only used if CoCoALib is available and falls back to a default libpoly-based implementation otherwise.

[hol] Disable bound fmf when HOL (#6792)

Fixes #6536

pow2: more implementations (#6756)

This PR adds implementations of functions from the pow2 solver, rewriter and type checker.

[regressions] Adding regression from #5371 (#6791)

[proofs] [dot] Adding a counter for subproofs (#6735)

[parser] [hol] Fix parser check for allowing functions when HOL is enabled (#6790)

Fixes #6526

docs: Add quickstart guide. (#6782)

FP: Remove sections guarded with undefined macro SYMFPUPROPISBOOL. (#6786)

Remove `--tear-down-incremental` (#6745)

Recent experiments have shown that `--tear-down-incremental` is actually
not really helping anymore and it has always been a bit of a workaround.
It is also broken on current master. This commit removes the option.

Avoid full normalization of lambdas in getValue (#6787)

This ensures that we don't apply lambda rewriting, which involves array value normalization, to lambda terms returned by TheoryModel::getValue.

This can significantly speed up our time to return function terms for getValue.

python api unit tests for Op (#6785)

Unit tests are translated from https://github.com/cvc5/cvc5/blob/master/test/unit/api/op_black.cpp
to python.

The only thing that is not faithfully translated is that the `cpp` tests expect the template function `[getIndices](https://github.com/cvc5/cvc5/blob/master/src/api/cpp/cvc5.h#L841)` to fail when an inappropriate type is given to it, while in the [`python` API](https://github.com/cvc5/cvc5/blob/90d19f7cdbaf41e389bdcbd099471f658a35ce98/src/api/python/cvc5.pxi#L343) this function is not a template, but just tries every supported type.

For example, the following line is not translated:
https://github.com/cvc5/cvc5/blob/90d19f7cdbaf41e389bdcbd099471f658a35ce98/test/unit/api/op_black.cpp#L206

modular bv2int: Stubs and some implementations (#6760)

This PR adds the file int_blaster.cpp. Most of the functions are not yet implemented. Two main functions are implemented.
Additionally, code that will no longer be needed is removed from the BV rewriter.

Minor simplification to equality engine notifications (#6726)

This removes the d_performNotify flag from equality engine which was supposedly used to guard a very old dependency concerning notifications during initialization. We are now robust to this and hence the flag can be removed.

Always check legal eliminations in quantified logics (#6720)

Fixes #6699.

Fix type enumeration for non first-class sorts in FMF (#6719)

Fixes #6690.

Python api unit tests for Result (#6763)

This PR translates the cpp API unit tests about results to python.
The original cpp file is: https://github.com/cvc5/cvc5/blob/master/test/unit/api/result_black.cpp

The translation made rise to one addition to the python API:
The UnknownExplanation object from the cpp API was represented by a string in the python API.
Now we have a more faithful representation, as an enum.

Fix cases of ITE within regular expressions (#6783)

Fixes #6776.

Our computation of when a regular expression was constant did not account for when ITE was embedded in an RE, leading to an unsound rewrite.

That benchmark now gives:

(error "Regular expression variables are not supported.")

Set up fine grained equality notifications (#6734)

This adds fields to equality engine setup information which will be used to hook up theories to the central equality engine.

This PR does not impact any behavior.

This is in preparation for the central equality engine.

Update to CaDiCaL 1.4.1. (#6780)

docs: Split out and merge C++ class hierarchy. (#6781)

This restructures the entry page for the C++ API documentation in
preparation for adding a quickstart and linking to examples and adding
more content.

[Attributes] Remove parameter `context_dependent` (#6772)

After commit d70a63324c95210f1d78c2efc46395d2369d2e2b, context-dependent
attributes have not been supported and, as a result, the template
parameter `context_dependent` of `Attribute` has not been used.
Context-dependent attributes also do not fit with our current design of
sharing attributes across different solvers, so it is unlikely that we
will add that feature back in the future. This commit removes the unused
template parameter.

Fix model issues with --bitblast=eager. (#6753)

For model construction we only compute model values for relevant terms. The set of relevant terms is computed in https://github.com/cvc5/cvc5/blob/master/src/theory/model_manager_distributed.cpp#L58, which skips equalities by default because equalities are usually handled by the equality engine.
When --bitblast=eager is enabled all assertions are wrapped into BITVECTOR_EAGER_ATOM nodes and passed to the BV solver, which results in equalities below BITVECTOR_EAGER_ATOM nodes not being handled by the equality engine but by the BV solver directly. These equalities, however, are skipped when computing the relevant terms and therefore the BV solver is not asked to compute model values for variables below these equalities.

If --bitblast=eager is enabled the BV solver now additionally adds the variables encountered during bit-blasting to the relevant terms via computeRelevantTerms.

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

Add Grammar.java to the java API (#6388)

This commit adds Grammar.java GrammarTest.java and cvc5_Grammar.cpp to the java api.

Move cnfConversionTime statistic to CnfStream. (#6769)

The statistic in `smt_solver.cpp` was not accurate.

Make CaDiCaL a required dependency. (#6761)

Since the new BV solver is enabled by default and uses CaDiCaL
(and optionally CryptoMiniSat) we make CaDiCaL a required dependency.

[proof] Fix documentation of array rule (#6770)

Adding python API test part 5 (#6743)

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

1. Adding getNullSort() and mkEmptyBag() functions.
2. Allowing mkOp() with a list of arguments (previously allowed at most 2).
3. Allowing mkString() with additional boolean argument useEscSequences.
4. Corresponding changes to the tests.

docs: Fix config to produce unique Sphinx section labels. (#6767)

[CI] Build with all available cores (#6768)

macOS virtual machines have three available cores but we were only using two of them for our CI. This commit changes the CI to retrieve the number of available cores and then to use that to number to build and test cvc5.