[proof-new] A simple proof generator for buffered proof steps (#5069)

This commit also modifies proof equality engine to use this new proof generator rather than the FactProofGenerator, on which this new one is based.

Co-authored-by: Andrew Reynolds <andrew.j.reynolds@gmail.com>

(proof-new) Make proofs mandatory in proof equality engine (#5059)

All uses of proof equality engine are now guarded such that the ordinary equality engine is used when proofs are not enabled. Thus, we can make proofs mandatory in proof equality engine. This eliminates the need for some guards.

Some indentation changed, but there are no additions in this PR.

Move sets member propagation to SolverState (#5045)

This eliminates the parent relationship from solver state to theory sets.

Rename system tests to api tests and remove obsolete Java test. (#5066)

Move quantifiers engine private to own file (#5053)

This moves and renames the quantifiers engine private class to QuantifiersModules. This is in preparation for using a standard state and inference manager object in TheoryQuantifiers and QuantifiersEngine.

Initializing quantifiers engine is a bit non-standard since it is intentionally a separate entity from TheoryQuantifiers. However, the plan is for quantifiers engine to use the state and inference manager of TheoryQuantifiers.

This PR additionally moves the initialization of quantifiers modules to a QuantifiersEngine::finishInit() method. The motivation for is that we do not have a state and inference manager during construction of QuantifiersEngine, since these will live in TheoryQuantifiers and will be passed to QuantifiersEngine during TheoryQuantifiers::finishInit. This means that we need a final pass to initialize quantifiers engine after these are initialized, which thus must come as the last step of TheoryEngine::finishInit.

The next PR will connect the state and inference manager to QuantifiersEngine during TheoryQuantifiers::finishInit. Then, the plan is for many of the core utilities in QuantifiersEngine to migrate to state/inference manager, and finally for its modules to reference state and inference manager instead of QuantifiersEngine.

Fix needsModel method for CEGQI (#5048)

There was a bug in CEGQI's needModel method which could say that it doesnt need a model built when there are no active quantifiers. However, computing active quantifiers is not done in QuantifiersEngine::check until after this method is called, meaning it was using stale data on whether a quantifier was active or not. This could lead to the use of bogus models in CEGQI in incremental mode in some corner cases, leading to the assertion failure in #5019.

Fixes #5019.

Standard equality engine notify class for Theory (#5042)

This makes a standard equality engine notify class that forwards the 3 mandatory callbacks to the provided inference manager (the other 3 callbacks may be specific to the theory). It updates TheoryUF to use this class, other theories will be updated to this style as more inference manager are added.

Notice that we could also forward the other 3 callbacks in this class to Theory, making eqNotifyNewClass, eqNotifyMerge, and eqNotifyDisequal virtual methods in Theory, which can be done on a future PR if needed.

Fix ABC build (#5061)

For some reason, our ABC build was including cnf_stream.h in an
extern "C" block instead of outside of it, which made the build fail
because the header indirectly includes cdqueue.h, which uses
templates. This change is older
(e9bfbb2)
but only started causing problems with our nightly builds recently.

Interpolation: Add implementation for SyGuS interpolation module (final) (#5063)

Add interface for SyGuS Interpolation module. Adding the API for (get-interpol s B), which is aim for computes an I that A->I and I->B. Here A is the assertions in the stack.

bv2int: simpler translation for plus and times (#5055)

This PR makes the translation of plus and times by:

using plain mod rather than introducing a skolem. If this proves to be a bottleneck, we can try to tackle it where mod is treated in the solver in the future. This will make it easier to introduce support for quantifiers, as we don't need to introduce new variables under quantification.
Making sure everything is binarized in more places of the translation.

Refactoring the rewriter of sets (#4856)

Changes it so that we don't flatten unions if at least one child is non-constant, since this may lead to children that are non-constant by mixing constant/non-constant elements and is generally expensive for large unions of singleton elements.

The previous rewriting policy was causing an incorrect model in a separation logic benchmark reported by Andrew Jones, due to unions of constant elements that were unsorted (and hence not considered constants). We now have the invariant that all subterms that are unions of constant elements are set constants.

Note this PR changes the normal form of set constants to be (union (singleton c1) ... (union (singleton cn-1) (singleton cn) ... ) not (union ... (union (singleton c1) (singleton c2)) ... (singleton cn)).

It changes a unit test which was impacted by this change which was failing due to hardcoding the enumeration order in the unit test. The test is now agnostic to the order of elements.

Fix type for Windows build (#5062)

The BVToInt preprocessing pass was using uint, which appears to be
undefined when we cross-compile for Windows. This commit fixes the issue
by using size_t.

Standardize uses of inference manager in datatypes (#5035)

Datatypes now has an inference manager. This is work towards making it use the inference manager in all places where it should.

In particular, this makes many of the places where conflicts are determined using `InferenceManager::conflictExp` (explained conflict) instead of `InferenceManager::conflict` + custom calls to explain in TheoryDatatypes.  The goal here is to ensure that all explanations from the equality engine are managed by inference manager, which is required for proofs.

(proof-new) Add SMT proof manager (#5054)

This module is responsible for constructing the proof checker, proof node manager, and implementing dumping and checking of the final proof.

This PR includes setting up some connections into the various modules for proof production.

(proof-new) Update TheoryEngine lemma and conflict to TrustNode (#5056)

This updates the theory engine interfaces for conflicts and lemmas to be in terms of TrustNode not Node.

This also updates the return value of getExplanation methods in TheoryEngine to TrustNode, but it does not yet add the proof generation code to that method yet, which will come in a separate PR.

Move finite model minimization to UF last call effort (#5050)

This moves model minimization happen in TheoryUF's last call effort check instead of being a custom call in quantifiers finite model finding. This is both a better design and avoids bugs when quantifiers are not enabled (for QF_UF+cardinality constraints).

Fixes #4850.

(proof-new) Handle mismatched assumptions in proof equality engine during mkScope (#5012)

This modifies the fix for Boolean equalities with constants so that is addressed lazily during ProofNodeManager mkScope instead of when asserting assumptions to the proof equality engine. This ensures that the default method for asserting facts to the equality engine for external assertions does not have any special cases.

A previously abandoned solution to this issue had made this a part of CDProof. Instead, this PR modifies the mkScope method only. The fix makes mkScope robust to any assumption mismatches in mkScope that can be fixed by rewriting, not just Boolean equality with constants. It is intended to be used infrequently as a last resort when mkScope has mismatched assumptions. The handling of mismatches due to symmetry remains in this method.

(proof-new) Use deep copy for final lemma step in proof equality engine (#5013)

Previously, strings on proof-new used a ProofStepBuffer for deriving the final conclusion of lemmas in proof equality engine (assertLemma). This was recently changed to use the more standard ProofGenerator interface of assertLemma. However, there was a bug in this method: the steps from this proof need to be deep copied into the proof we are generating or otherwise the explanation of these literals are not connected in the CDProof. This updates the proof equality engine so that it instructs the proof generator to do a deep copy in this case. Notice this is very rarely more than a single step.

Add witness to cvc printer. (#5057)

bv2int: refactoring the main translation loop (#5051)

This PR introduces a refactoring of the main translation loop in bv2int preprocessing pass.
Many parts are wrapped by helper functions and so the main loop becomes smaller.

remark: selecting "Hide whitespace changes" cuts the diff by ~50%.

Parser error for wrong number of datatypes (#5049)

Fixes #4973.

bv2int: improvement in lazy failures (#5020)

Previously, in case we encountered a term we cannot translate to integers (e.g. a bit-vector array), we would fail.
This PR improves that behavior by keeping the original term, and potentially wrapping it BV_TO_NAT and INT_TO_BV operators.

A test which includes a bit-vector array is included, which was not supported before.

In addition, the treatment of uninterpreted functions is refactored and documented better.

Use state and inference manager in UF CardinalityExtension (#5036)

Previously, the cardinality extension of UF maintained its own (SAT-context-dependent) conflict flag, made custom calls to output channel, and maintained its own cache of lemmas. This standardizes the CardinalityExtension so that it uses state and inference manager of UF, which means that UF and the cardinality extension are fully syncronized concerning whether we are in a conflicting state at all times (d_state.isInConflict). It further cleans up some of the interfaces in CardinalityExtension. This required adding a forwarding method for setIncomplete in inference manager.

(proof-new) Minor changes to proof node updater (#5011)

This includes some changes to proof node updater that are not currently on master.

This includes:
(1) Explicitly passing the result of the current proof node we are updating,
(2) Caching the results of updates based on Node. In other words, proofs (in the same scope) that we have already seen that prove the same thing as the current proof node are reused.

It also enables the compilation of proof post-processor, which was missing on master and makes Rewriter of SmtEngine public which is required for doing so.

(proof-new) Make proofs in term formula removal term context sensitive (#5008)

Previously term formula removal proofs didnt not take the term context into account. This updates it to make use of the term context sensitive support in TConvProofGenerator. More generally, it uses the term context computation as the standard way of caching the results of rewrites in this class (regardless of proofs).

(proof-new) Generalize single step helper in eager proof generator (#5046)

This allows single step proofs to have premises, closed by a SCOPE. This will be useful for array lemmas.

Fixes for regular expressions + sygus (#5044)

Includes not constructing a default value for non-first class types (e.g. RegLan) and a missing printer case for re.diff.

Add is_singleton operator to the theory of sets (#5033)

This pull request adds a new operator is_singleton for sets to determine whether a set is a singleton.
Before this operator, the user either uses an existential quantifier or the cardinality operator in smtlib. The former affects the performance especially when polarity is negative. The latter requires the cardinality extension in sets theory.
The implementation of is_singleton only uses an internal existential quantifier with the hope of optimizing it later.
New rewriting rules:

(is_singleton (singleton x)) is rewritten as true.
(is_singleton A) is rewritten as (= A (singleton x)) where x is a fresh skolem of the same type of elements of A.
(choose (singleton x)) is rewritten as x.

Split term registry from theory state in sets (#5037)

Currently, the theory state object SolverState in sets sends lemmas and has a reference to the parent theory. This PR is work towards eliminating these dependencies.

This adds a TermRegistry object which is responsible for some of the tasks currently done by SolverState, including all those involving lemmas.

Notice this also makes a bug fix in getUnivSetEqClass where the universe set was being returned instead of its representative.

A followup PR will make SolverState maintain SAT-context-dependent membership lists which is also required for breaking the dependence on the parent theory.

Fix printing of fp values. (#5041)

Fixes #5032

Make CVC/API BV div/mod semantics match SMT-LIB (#4997)

This commit changes the semantics of the CVC language and with the
default semantics of the API for `BVUDIV`, `BVUREM`, `BVSDIV`, `BVSREM`,
and `BVSMOD` to match the semantics of SMT-LIB >=2.6. Relatedly, the
commit also adds comments to our API documentation for the different
semantics enabled by the `bv-div-zero-const` option.

Eliminate a custom use of TheorySep in quantifiers engine for EPR (#5039)

This moves the initialization of the connection between separation logic and EPR to the separation logic theory, which is a more logical place for this. This eliminates a backwards reference to theory engine from quantifiers engine.

Add asLemma flag to theory inference process (#5030)

This is required for strings, which uses the same data structure, InferInfo, for both lemmas and facts. This ensures the process method of theory inference knows where we are a pending lemma or a pending fact.

It also makes a few changes necessary for the proof-new branch, including disabling the proof node manager in the inference manager for datatypes.

[Regressions] Fix regression issues related to BV proofs (#5029)

(new theory) Update TheoryBV to new standard for collectModelValues (#5025)

This makes collectModelValues the main model interface in BV instead of collectModelInfo. BV is no longer responsible for asserting its equality engine or computing relevant/asserted terms.

This involved updating the interface on many subsolvers of BvSolverLazy. This includes moving the responsibility of addSharedTerm (regarding trigger terms) from the subsolvers to TheoryBV, this eventually will be automatically handled in Theory once all theories are migrated to the new standard.

This ensures that TheoryBV is updated to the new standard (check was already migrated on c9e23f6).

Fix non-lib-poly-build issues  (#5028)

Use Result::Sat instead of BenchmarkStatus in printers. (#5026)

This PR modifies the printers to use Result::Sat, "internal" version of BenchmarkStatus, for printing benchmark status commands.

Use arith::InferenceManager for CAD lemmas (#5015)

This makes the CAD solver use the new arith::InferenceManager instead of the previously used lemma collection scheme.

Change the unavailable ABC mercury repository for the ABC solver code base on  GitHub (#4989)

Signed-off-by: Malte Mues (mail.mues@gmail.com)

Split lazy bit-vector solver from TheoryBV  (#5009)

This commit separates the lazy bit-vector solver from TheoryBV, which is now a thin wrapper around a bit-vector solver d_internal . This will allow us to easily swap out the bit-vector solver in the future.

Add interfaces for making trust nodes in TheoryInferenceManager. (#5016)

This gives theories a finer grained control over explained lemmas and conflicts.

A theory may now use an inference manager to construct "explained" lemmas/conflicts e.g. via mkLemmaExp, subsequently do any theory-specific debugging or modification to that lemma before sending it via trustedLemma.

This is required for the new strings inference manager on proof-new.

This also adds a missing variant of conflicts for the proof equality engine. It also does a minor simplification of a previous variant for constructing conflicts from proof equality engine based on a proof step buffer.

Update sets inference manager to inherit from InferenceManagerBuffered (#5007)

This updates the inference manager of sets to inherit from the standard base class InferenceManagerBuffered.

It matches that base class almost exactly, with cosmetic changes.

Notice that sets currently has a design issue: the state object sends lemmas and hence currently requires a pointer to the theory. This will be untangled in a future PR.

This PR makes a few very minor changes to the behavior, including not to use the "preprocess" property for subtype lemmas.

Added a new rule to simplify (bvugt (bvurem T x) x) (#4993)

Motivated by #4936, this PR adds a new BV rewrite rule:
(bvugt (bvurem T x) x) ==> (ite (= x 0) (bvugt T 0) false)
Fixes #4936.

Minor cleanup of quantifiers engine (#4994)

Eventually, QuanitifersEngine should not depend on TheoryEngine. This is a first step in this direction. It eliminates some uses of TheoryEngine and eliminates a unnecessary friend relationship between quantifiers::TermDb and TheoryEngine. Further refactoring will be done in future PRs.

Changing the handled operators in bv2int preprocessing pass (#4970)

Some of the bit-vector operators are directly translated to integers, while others are eliminated before the translation.
This PR changes the set of operators that we eliminate (and as a consequence, also the set of operators that we handle directly):

The only bit-wise operator that is translated is bvand. The rest are now eliminated.
bvneg is now eliminated.
The various division operators are still eliminated, but using different rewrite rules.
zero-extend and sign-extend are now handled directly.
shifting is changed to favor ITEs over non-linear multiplication.

Basic integration of arith::InferenceManager (#4999)

This PR adds a first basic integration of the arith::InferenceManager into the arithmetic theory and the nonlinear extension in particular.
While the lemma collection mechanism (in the nonlinear extension) remains unchanged, the lemmas are ultimately not directly pushed to the output channel but instead added to the inference manager. Additionally, we no longer use the cache within the nonlinear extension but instead rely on the inference manager.
This PR is based on #4960.

Make nonlinear extension (more) deterministic (#4996)

This PR tries to make the nonlinear extension more deterministic by keeping the order of input assertion (instead of taking them from a hash set). This makes the ordering somewhat more robust against varying node ids, which proved to be a problem for debugging...
Also adds a few logging messages at interesting places.

Drop {INCLUDE,LIBRARY,RUNTIME}_INSTALL_DIR variables in CMakeLists.txt (#4979)

On Debian (for instance), libraries aren't installed into `/usr/lib/`, but into something like `/usr/lib/x86_64-linux-gnu/`. In particular, this means that setting the `LIBRARY_INSTALL_DIR` to `lib` in the top-level `CMakeLists.txt` file is wrong.

Luckily, there is a simple solution: CMake provides [`CMAKE_INSTALL_LIBDIR`](https://cmake.org/cmake/help/v3.0/module/GNUInstallDirs.html) for this very purpose, which has sensible defaults and can be set by the user. In particular, since `CMAKE_INSTALL_LIBDIR` is a standardized variable, tools like the ones used for building Debian packages can set it to what they want it to be, whereas using a custom variable like `LIBRARY_INSTALL_DIR` wouldn't work in this setting.

Signed-off-by: Fabian Wolff <fabi.wolff@arcor.de>

Make ExtTheory independent of Theory (#5010)

This makes it so that ExtTheory uses a generic callback instead of relying on Theory.

The primary purpose of this commit is to eliminate the connection of TheoryBV and ExtTheory. This commit moves all things related to ExtTheory in BV into CoreSolver.

It also refactors the use of ExtTheory in strings and arithmetic.

(proof-new) Support proofs of quantifier instantiation (#5001)

This adds basic support for proofs of quantifier instantiation, which is the main method for sending lemmas from TheoryQuantifiers. Quantifier instantiation is also heavily used for solving extended string functions.

(proof-new) Improve debugging infrastructure for open proofs (#4984)

This includes more versions of checking whether a proof node is closed and standardizing output.

Fix CryptoMiniSat build, regression (#5006)

This commit fixes builds that include CryptoMiniSat after commit
8ad308b removed them. It also fixes one
of the regressions that requires unsat cores but was run when the build
was configured without them.

[Python API] Add missing methods to Datatype/Term (#4998)

Fixes #4942. The Python API was missing some methods related to
datatypes. Most importantly, it was missing mkDatatypeSorts, which
meant that datatypes with unresolved placeholders could not be resolved.
This commit adds missing methods and ports the corresponding tests of
datatype_api_black.h to Python. The commit also adds support for
__getitem__ in Term.

Remove #line directives from generated files. (#5005)

This PR removes any usage of the #line directive.
We no longer consider it particularly useful, and it obstructs reproducible builds (see #4980).
Fixes #4980.

(proof-new) Updates to builtin proof checker (#4962)

This includes support for some trusted rules (whose use is to come). It also modifies THEORY_REWRITE so that it is a "trusted" rule, that is, it is not re-checked. The reason for this is that TheoryRewriter is not deterministic. An example of non-determinism in TheoryRewriter are rules that introduce bound variables (e.g. quantifiers rewriter) since these bound variables are fresh each time it is invoked. Non-deterministic theory rewriters cannot be rechecked, which was leading to failures on proof-new at proof check time. The other way to fix this would be to cache TheoryRewriter responses, but then the checker would only be verifying that the caching was being done properly. This is not worthwhile.

(proof-new) Add proof support in TheoryUF (#5002)

This makes TheoryUF use a standard theory inference manager, which thus makes it proof producing when proof-new is enabled.

This additionally cleans HoExtension so that it does not keep a backwards reference to TheoryUF and instead takes its inference manager. This additionally adds two rules for higher-order that are required to make its equality engine proofs correct.

Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>

Use SMT-COMP configuration for competition build (#4995)

This commit changes our `competition` build to include the libraries
that we have used for SMT-COMP by default. This makes it easier for
users to reproduce our SMT-COMP configuration for performance
measurements. We are using GPL libraries for this build type, so the
commit adds color to highlight the fact that this build type produces a
GPL build.

(proof-new) Make term conversion proof generator optionally term-context sensitive (#4972)

This will be used by TermFormulaRemoval.

Migrating from using the 'glpk-cut-log' repo to using an official GPLK release + a set of patches (#4775)

This PR attempts to migrate from @timothy-king's repo for glpk-cut-log to using a set of patches against the official release that 'glpk-cut-log' was based off of (4.52).

This is in preparation of trying to rework these patches to be against the latest GPLK release (4.65). If we can do this, then it makes it easier for CVC4's dependancy on GPLK to be able to follow upstream (rather than being stuck on a release that is 6.5 years old!).

I have added GPLK as an option for CI, but I do not know if we actually want this. My concern with adding this to CI is that we're then not testing non-GPL builds, which doesn't seem ideal.

However, before starting to rework the patches to be against 4.65, I want to make sure that things are actually working/stable against 4.52; so having at least one CI target that does use GPLK would be great.

Signed-off-by: Andrew V. Jones andrew.jones@vector.com

Introduce an internal version of Commands. (#4988)

This PR is a step towards the migration of Commands to the public API. Node versions of some Commands are introduced for internal use (as necessary). The DumpManager is refactored to make use of those commands.

Minor updates to theory inference manager (#5004)

These updates are inspired by the current inference manager for sets.

(new theory) Update TheoryArrays to the new standard (#5000)

This includes using the standard d_conflict flag in TheoryState and splitting its check into 3 callbacks.

It also deletes some unused code and eliminates an assertion (line 791 of theory_arrays.cpp) which doesn't hold in a central architecture.

Further work on standardization for arrays will add an InferenceManager to guard its uses of asserting facts to equality engine (both for proofs and configurable theory combination).

FYI @barrettcw

Use std::unique_ptr instead of std::shared_ptr for inference manager (#5003)

We now use std::unique_ptr instead of std::shared_ptr when storing TheoryInference objects.

Add ArithLemma and arith::InferenceManager (#4960)

This PR adds a new ArithLemma that is essentiall NlLemma, but derived from the new theory::Lemma and meant to be used all across the arithmetic theory.
Also, based on theory::InferenceManagerBuffered this PR adds arith::InferenceManager that shall become the sole interface between the arithmetic theory and the OutputChannel.

(new theory) Update TheorySets to the new interface (#4951)

This updates the theory of sets to the new interface (see #4929).

[API] Fix Python Examples (#4943)

When testing the API examples, Python examples were not included. This
commit changes that and fixes multiple minor issues that came up once
the tests were enabled:

- It adds `Solver::supportsFloatingPoint()` as an API method that
  returns whether CVC4 is configured to support floating-point numbers
  or not (this is useful for failing gracefully when floating-point
  support is not available, e.g. in the case of our floating-point
  example).
- It updates the `expections.py` example to use the new API.
- It fixes the `sygus-fun.py` example. The example was passing a _set_
  of non-terminals to `Solver::mkSygusGrammar()` but the order in which
  the non-terminals are passed in matters because the first non-terminal
  is considered to be the starting terminal. The commit also updates the
  documentation of that function.
- It fixes the Python API for datatypes. The `__getitem__` function had
  a typo and the `datatypes.py` example was crashing as a result.

Removes old proof code (#4964)

This deletes much of the old proof code. Basically everything but the minimal necessary infra-structure for producing unsat cores. That includes dependency tracking in preprocessing, the prop engine proof and the unsat core computation code in the old proof manager. These should also go once we fully integrate into master the new proof infrastructure.

It also cleans interfaces that were using old-proof-code-specific constructs (such as LemmaProofRecipe). When possible or when it made sense standalone local proof production code was kept, but deactivated (such is in the equality engine and in the arithmetic solver).

 (new theory) Update TheoryDatatypes to the new standard (#4986)

Updates it to use the new inference manager as well as updating its check to the standard callbacks.

Add TheoryInference base class (#4990)

This introduces a TheoryInference base class, which is a generalization and cleaner version of the former Lemma object. This changes the name of Lemma -> SimpleTheoryLemma, and makes the callback responsible for calling the inference manager.

This PR also updates the datatypes inference manager to use the new style. This required adding some additional interfaces to TheoryInferenceManager.

CMS: Update to version 5.8.0. (#4991)

Add arithmetic-specific, runtime, proof-macros. (#4992)

We'll use this to gate farkas-coefficient machinery after we remove the
old proof-macros.

I've changed the macros slightly from the proof-new branch: I removed the dependence on options::proof() (no longer wanted) and options::unsatCores() (I had copied this from the original proof macros, but it's not needed either, since we're in a theory).

'fix-install-headers.sh' should respect DESTDIR environment variable (#4978)

When using CMake with Unix Makefiles, one can invoke `make install` as
```
make install DESTDIR=/a/b/c
```
so that the files will be installed into `$DESTDIR$CMAKE_INSTALL_PREFIX` (see the [documentation](https://cmake.org/cmake/help/latest/envvar/DESTDIR.html) for details). This currently doesn't work with the `fix-install-headers.sh` script:
```
[...]
-- Installing: /<<PKGBUILDDIR>>/debian/tmp/usr/include/cvc4/util/integer.h
-- Installing: /<<PKGBUILDDIR>>/debian/tmp/usr/include/cvc4/util/rational.h
find: ‘/usr/include/cvc4/’: No such file or directory
```
Here, `CMAKE_INSTALL_PREFIX` is `/usr` but `DESTDIR` is `/<<PKGBUILDDIR>>/debian/tmp/`.

This commit makes the script consider `DESTDIR` (if it is not set, then `$DESTDIR` will be empty and nothing changes) to fix this issue.

Signed-off-by: Fabian Wolff <fabi.wolff@arcor.de>

Add the inference manager for datatypes (#4968)

This is in preparation for converting datatypes to the new standard. It adds a specialized version of inference manager buffered that datatypes uses. This required adding several utility methods to its base classes.

A follow up PR will connect this to TheoryDatatypes.

Fix spelling errors (#4977)

Signed-off-by: Fabian Wolff <fabi.wolff@arcor.de>

(new theory) Update TheoryStrings to new standard (#4963)

This updates theory of strings to the new standard.

This makes strings use the standard template for check and collectModelInfo. It also updates its inference manager to the standard and makes use of assertFactInternal for processing internal facts. This now enables preNotifyFact and notifyFact to be defined in TheoryStrings instead of inside inference manager, which is clearer and eliminates some dependencies within inference manager.

Note that the inference manager of strings for now inherits from TheoryInferenceManager. Further standardization will make it inherit from the new InferenceManagerBuffered class.

This design will be merged into proof-new, which also has significant changes to strings inference manager.

Fix --ackermann in the presence on syntactically different but possibly equal selects (#4981)

The implementation of --ackermann mishandled selects in a subtle way:
If select is applied to two syntactically different arrays (that may be semantically equal), the ackermann preprocessing failed to generate the "all arguments equal implies terms equal" lemmas.
The problem is that we used the first argument (that is: the array) as lookup to identify terms that need to be considered for these lemmas. Instead we now use their operator (select) just like for uninterpreted function applications.

Fixes #4957 . Also adds a regression.

Simplify interface for computing relevant terms. (#4966)

This is a followup to #4945 which simplifies the contract for computeRelevantTerms.

[CI] Fix Cython installation (#4983)

Cython has been causing issues recently, see e.g.
https://github.com/CVC4/CVC4/pull/4982/checks?check_run_id=1052433862.
It looks like the issue is that globally installed packages can't be
found by Python (maybe the global site-package directories changed/are
not included in the search paths anymore?). This commit changes the
installation of Cython to install it locally to the user instead of
globally. It also adds `bin` in the user base directory to `PATH` s.t.
CMake is able to find the `cython` binary.

Basic proof support in inference manager (#4975)

This adds basic support for asserting internal facts with proofs in the inference manager class.

The purpose of this PR is twofold:
(1) From the point of view of proofs, this PR standardizes the management of proof equality engine within inference manager. Theories no longer have to manually construct proof equality engines, and instead are recommended to create inference managers.
(2) From the point of view of the new approach to theory combination, this PR ensures standard theory callbacks (preNotifyFact / notifyFact) are used for internal facts, regardless of whether proofs are enabled.

This will simplify several of the current (unmerged) changes for proof production in theory solvers on proof-new.

Notice this PR adds the utility method NodeManager::mkAnd, which is arguably long overdue.

Also notice this code is not yet active, but will be used on proof-new after this PR is merged.

(proof-new) More term context utilities. (#4912)

These utilities will be used for making some of the core proof utilities term-context-sensitve.

New C++ API: Add REGEXP_{REPEAT,LOOP}_OP handling in getIndices. (#4969)

Replace Theory::Set with TheoryIdSet (#4959)

This makes it so that equality_engine.h does not include theory.h. This is a bad dependency since Theory contains EqualityEngine.

This dependency between equality engine and theory was due to the use of a helper (Theory::Set) for representing sets of theories that is inlined into Theory. This PR moves this definition and utilities to theory_id.h.

It fixes the resulting include dependencies which are broken by changing the include theory.h -> theory_id.h in equality_engine.h.

This avoids a circular dependency in the includes between Theory -> InferenceManager -> ProofEqualityEngine -> EqualityEngine -> Theory.

Incremental support for bv_to_int (#4967)

This PR adds support for incremental solving in bv_to_int.
This amounts to:

using context dependent data structures
adding a test
In addition, we check for parametrized operations in a more robust way (using kind::metakind::PARAMETERIZED) and rename some tests for convenience.

(proof-new) Make CombinationEngine proof producing (#4955)

Makes combination engine proof producing (for Boolean splits). Followup PRs will start to add proof production in TheoryEngine.

(new theory) Update TheoryQuantifiers to the new interface (#4950)

TheoryQuantifiers is a theory that passes quantified formulas to QuantifiersEngine. This updates it to the new check template (see #4929).

Also does some minor cleanup in the cpp file.

(proof-new) Add the SMT proof post processor (#4913)

This PR adds the proof post-processor, which is the final authority on putting together the overall proof. It additionally implements lazy pedantic failures and statistics.

This PR also corrects a subtle bug in the elimination of SUBS which requires a TRUE_INTRO/FALSE_INTRO in certain cases.

(new theory) Update TheoryFP to the new interface (#4953)

This updates the theory of floating points to the new interface (see #4929).

Notice that TheoryFP was not adding trigger terms to its equality engine (which should be done during notifySharedTerm), and thus was not propagating equalities between shared terms in combined theories. This PR updates its notifySharedTerm method to the default one.

FYI @martin-cs

(cad-solver) Fixed excluding lemma generation. (#4958)

The lemma generation for partial cad checks had a number of issues that have been fixed in this PR.
The previous version had both soundness issues and a very naive approach to handling algebraic numbers.
This new version is sound (fingers crossed) and allows to construct more precise, but also more complex lemmas.
To avoid constructing very large lemmas, a (somewhat arbitrary) limit based on the size of coefficients was added.

Do not delay processing equivalence class merges in datatypes (#4952)

Currently, the theory of datatypes buffers its processing of when equivalence class merges are processed. This was an earlier design to avoid using the equality engine while it was doing internal operations. Now, equivalence class merge callbacks are called at a time when it is safe to use the equality engine and thus this level of indirection is unnecessary.

This will simplify further work on datatypes towards having a standard inference manager.

Add the buffered inference manager (#4954)

This class implements a highly common pattern of buffering facts and lemmas to send on the output channel. It is planned that the inference managers of strings, sets, datatypes, (non-linear) arithmetic, sep, quantifiers will inherit from this class.

This PR adds basic calls to add lemmas on the output channel from InferenceManager.

It introduces a Lemma virtual class which arith::nl::NlLemma and strings::InferInfo will inherit from.

This is required to begin refactoring a flexible configurable strategy for non-linear arithmetic, and will make it easier to further develop towards a configurable approach for theory combination.

(new theory) Update TheorySep to new interface (#4947)

This updates the theory of separation logic to the new interface, which involves splitting up its check method based on the 4 check callbacks and using the theory state in the standard way.

No behavior changes, unfortunately a lot of code had to change indentation and was updated to new coding guidelines.

Make iand lemmas use proper Inference types. (#4956)

For some reason, the nl subsolver for IAND did not annotate its lemmas with `Inference` types yet. This commit adds appropriate `Inference` values and makes the IAND solver use them.

(proof-new) Add the proof equality engine (#4881)

This is a (partial) layer on top of EqualityEngine that is a universal black box proof generator for users of the equality engine.

Add irrelevant kinds infrastructure to TheoryModel (#4945)

Currently, Theory is responsible for implementing a computeRelevantTerms method collects the union of:
(1) The terms appearing in its assertions and its shared terms,
(2) The set of additional terms the theory believes are relevant.

Currently, (1) is computed by an internal Theory method computeRelevantTermsInternal, and the overall computeRelevantTerms is overridden by the theory (for datatypes and arrays only) for also including (2).

The new plan is that Theory will only need to compute (2). Computing (1) will be the job of ModelManager::collectAssertedTerms and the model manager will call Theory::computeRelevantTerms as an additional step prior to its calls to collect model info.

This will make certain optimizations possible in theory combination (e.g. tracking asserted terms incrementally).

This PR adds the ModelManager::collectAssertedTerms method and also adds infrastructure for irrelevant kinds in the model object (which have an analogous interface as when "unevaluated" kinds are marked during initialization). It does not connect the implementation yet.

FYI @barrettcw

Add the theory inference manager (#4948)

This class is a wrapper around OutputChannel and EqualityEngine. It is preferred that the Theory use this interface when asserting "internal facts" to the equality engine, and for sending lemmas, conflicts and propagations on the output channel.

This class will be useful when trying new methods for theory combination, where all theories behavior can be modified in a standard way based on modifications to the base inference manager class.

(new theory) Update TheoryUF to new interface (#4944)

This updates TheoryUF to use the 4 check callbacks instead of implementing check, and uses the official TheoryState object instead of its context::CDO<bool> d_conflict field.

It also makes a minor change to collectModelValues for const and to preNotifyFact to include an isInternal flag.

Connect combination engine to theory engine (#4940)

This connects the implementation of CombinationEngine into TheoryEngine. By default, the combination engine of theory engine is CombinationCareGraph.

This PR also consolidates and simplifies how models are built, note that:

The TheoryModel object no longer tracks whether it is built, instead that is the job of ModelManager,
The TheoryModelBuilder object is no longer responsible for calling TheoryEngine's collect model info method.
Quantifiers engine uses a simpler interface for ensuring that TheoryEngine's model is built.
This PR also makes some minor simplifications to TheoryEngine from the centralEe branch.

Note that no significant behavior changes are intended in this PR.

Replace Expr-level datatype with Node-level DType (#4875)

This PR makes two simultaneous changes:

The new API uses Node-level DType instead of Expr-level Datatype. This required converting 2 of the last remaining calls in the parser that used Expr to use the new API.
Internally constructed datatypes (e.g. for sygus) use Node-level DType instead of Expr-level Datatype. Note this required moving a block of code for handling a corner case of sygus from Datatype -> DType.
This PR removes :

ExprManger::mkDatatypeType.
The Expr-level datatype itself. This PR removes all references to its include file.
It also updates one remaining unit test from Expr -> Node.

This PR will enable further removal of other datatype-specific things in the Expr layer.

Eliminating spurious replay of commands for define funs expansion when checking unsat cores (#4941)

Doing it via commands being added to the coreChecker SMT engine is not necessary since we can directly add assertions after expansion from the original SMT engine.

Add the combination engine (#4939)

This adds the combination engine, which is the module of TheoryEngine which implements the combineTheories method and owns the various components of theory combination, which includes equality engine manager, model manager, and the "shared solver" (to come later). It will have two variants, CombinationCareGraph and CombinationModelBased, the former is added with this PR.

FYI @barrettcw

The next PR will connect this module to TheoryEngine and remove a few existing methods from TheoryEngine, as they are implemented in the modules of this class.