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.

Add a few basic extensions for equality engine (#4937)

This includes a standard method for safe explanations and the option to disable all trigger terms.

Fix memory issue in AntlrInput::parseError (#4873)

The `parseErrorHelper` message can run into memory errors when the it prints the last line and this last line is not terminated by a newline. I suspect other conditions may trigger it as well (like only using `\r` as line terminator).
This comit computes the size of the buffer from the start of the current line to the end of the buffer and makes sure that we never go beyond this buffer. The calculation looks a bit awkward, I've not been able to obtain this information from the ANTLR input stream in a nicer way...
(I found this issue when looking at #4866).
Fixes #4069 .

Do not use relevance during non-linear check model (#4938)

This led to a model soundness issue in rare cases where a relevant literal was dropped due to an entailment check by an irrelevant literal.

Increase regress level to 2 for production build. (#4888)

Add the distributed model manager (#4934)

This class is responsible for model building when using a distributed approach for equality engines.

This PR defines the class but does not yet activate it in TheoryEngine.

This includes some model-specific things from TheoryEngine which will be migrated to this class on the next PR.

Extend the standard Theory template based on equality engine (#4929)

Apart from { quantifiers, bool, builtin }, each Theory now has an official equality engine. This PR elaborates on the standard recommended template that Theory should follow, which applies to all theories, regardless of whether they have an equality engine.

This includes:

A standard check method. The Theory is now expected to implement 4 callbacks (preCheck, postCheck, preNotifyFact, notifyFact).
A standard collectModelInfo method. The Theory is now expected to implement 2 callbacks (computeRelevantTerms, collectModelValues).
Additionally, 2 more methods have an obvious default:
(1) getEqualityStatus, which returns information based on an equality engine if it exists,
(2) addSharedTerm, which adds the term as a trigger term to the equality engine of the theory if it exists. Notice that for the sake of more consistent naming, theories now implement notifySharedTerm (previously TheoryEngine called theory-independent addSharedTermInternal which called addSharedTerm, this is updated now to addSharedTerm/notifySharedTerm).

Other methods will not be standardized yet e.g. preRegisterTerm, since they vary per theory.

FYI @barrettcw

Each theory on the branch https://github.com/ajreynol/CVC4/tree/centralEe conforms to this template (e.g. they do not override check or collectModelInfo). The next step will be to pull the new implementation of each Theory from that branch.

Remove unecessary theory model builder base class (#4933)

Dynamic allocation of model equality engine (#4911)

This makes the equality engine manager responsible for initializing the equality engine of the model.

It also moves the base equality engine manager class to its own file.

Notice the code in TheoryEngine will undergo significant cleaning in forthcoming PRs when the "ModelManagerDistributed" is added. This PR adds temporary calls there to preserve the current behavior.

Limit trigger terms to shared terms in arrays (#4932)

There is a non-standard use of trigger terms in the array theory via `EqualityEngine::addTriggerTerm`.

Trigger terms are only supposed to be shared terms, and are added to the equality engine for the sake of propagating equalities between shared terms.  The array theory does two non-standard things:
(1) it registers (possibly) non-shared terms as triggers in its `preRegisterInternal` method,
(2) it filters propagations between anything except non-shared arrays in its `eqNotifyTriggerTermEquality` method.

The latter is only necessary because of the former.  It is unnecessary to do *either* of these things. Instead, the array theory should simply add the terms to the equality engine (as non-triggers) during preRegisterInternal.  Note that it additionally correctly adds trigger terms in its `notifySharedTerm` method.

With this commit, the array theory uses the equality engine (wrt propagation) in a standard way.

Remove spurious theory methods calls (#4931)

This PR removes spurious theory method calls that are not implemented.

It also renames a common "propagate(TNode lit)" pattern to "propagateLit(TNode lit)" to avoid confusion with "propagate(Effort e)".

Connect the relevance manager to TheoryEngine and use it in non-linear arithmetic (#4930)

This PR activates the use of the relevance manager in TheoryEngine and makes use of it (via Valuation) in the non-linear extension in arith. It removes a deprecated hack (addTautology) for doing this.

This addresses CVC4/cvc4-projects#113.

Note that the best method for relevance is interleaving, where roughly you gain on SMT-LIB:

QF_NIA: +484-53 unsat +792-440 sat
QF_NRA: +32-19 unsat +57-23 sat
However, this PR does not (yet) enable this method by default.

Note that more work is necessary to determine which lemmas require NEEDS_JUSTIFY, this PR identifies 2 cases of lemmas that need justification (skolemization and strings reductions). Regardless, the use of the relevance manager is limited to non-linear arithmetic for now, which is only able to answer "sat" when only arithmetic is present in assertions.

Simplify and fix care graph for ufHo (#4924)

We now separate APPLY_UF and HO_APPLY. We do not generate care pairs based on comparing APPLY_UF terms with HO_APPLY terms, which led to type errors previously.

Fixes #4990.

Remove BV equality slicer (#4928)

This class is not used based on our coverage tests (although it appears to be possibly enabled based on non-standard runtime checking of assertions), and uses the equality engine in a highly nonstandard way that will be a burden to the new standardization of equality engine in theory solvers.

FYI @aniemetz @mpreiner

Add TheoryState objects to each Theory (#4920)

This initializes all theories with a TheoryState object (apart from bool and builtin which do not require one).

Two additional theories are known to require special state objects: TheoryArith, which has a custom way of detecting when in conflict, and TheoryQuantifiers, which can leverage a special state object for the purposes of refactoring and splitting apart QuantifiersEngine further. All other theories use default TheoryState objects.

Notice this PR does not update the theories to use these states yet, it simply adds the objects.

Split QuantElimSolver from SmtEngine (#4919)

Towards refactoring SmtEngine / converting Expr -> Node.

Simplify trigger notifications in equality engine (#4921)

This is further work towards a centralized approach for equality engines.

This PR merges the eqNotifyTriggerEquality callback with the eqNotifyTriggerPredicate callback, and adds assertions that capture the current behavior. It furthermore makes addTriggerEquality private in equality engine and invoked as a special case of addTriggerPredicate. Note this PR does not impact the internal implementation of these methods in equality engine, which indeed is different.

There are two reasons to merge these callbacks:
(1) all theories implement exactly the same method for the two callbacks, whenever they implement both. It would be trivial to do something different (by case splitting on the kind of predicate that is being notified), and moreover it is not recommended they do anything other than immediately propagate the predicate (regardless of whether it is an equality).
(2) It leads to some confusion with eqNotifyTriggerTermEquality, which is invoked when two trigger terms are merged.

Remove example theory (#4922)

This code is unused and obsolete.

Add strings-exp to regression (#4923)

str.at expands to str.substr, thus this benchmark (may) require strings-exp if things do not rewrite/preprocess. This triggers a regress0 failure on proof-new currently.

(cad solver) Add a partial check method. (#4904)

This PR extends the CAD-based solver to enable partial checks. Essentially, we only collect the first interval that is excluded for the first variable and return that one as a lemma. This does not leave a lot of choice on "how partial" the check should be, but it is fairly easy to implement and does not add additional overhead.
It also fixes some confusion in excluding_interval_to_lemma...

Make sets and strings solver states inherit from TheoryState (#4918)

This is towards the new standard for theory solvers.

This PR makes the custom states of sets and strings inherit from the standard base class TheoryState. It also makes a minor change to InferenceManager/SolverState to make sets more in line with the plan for a standard base class InferenceManager.

Followup PRs will establish the official TheoryState classes for all other theories (which in most cases will be an instance of the base class).

Require `--strings-exp` when using `str.substr` (#4916)

Fixes #4915. Previously, `str.substr` did not require `--strings-exp`.
However, when `--strings-exp` is not active, we do not send terms to the
extended solver for registration, which meant that `str.substr` was
never reduced. This commit adds `str.substr` to the operators that
require `--strings-exp`.

Changes assertion (about maximum set cardinality) to an exception. (#4907)

Changes the assertion that checks for the maximum cardinality of set models to an exception, following #4374.
Also cleans up the code around it: previously, the Rational was checked against LONG_MAX, converted to std::uint32_t and then stored into an unsigned. Now we use std::uint32_t all the way.
Fixes #4374.

[Regressions] Do not test `--check-proofs` anymore (#4914)

In preparation of removing the old proof module, this commit changes the
regression runner to not add the flag --check-proofs anymore when
running the regressions.

Fix SmtEngine::reset() (#4917)

Calling (reset) multiple times produced parsing problems (#4866) and could probably lead to all kinds of interesting issues.
In a nutshell, reset() failed to properly reset d_initialOptions (which is used to properly reset d_options) so that all options defaulted after the second call to reset().
This PR properly sets d_initialOptions after a reset (and the filename as well).

Fixes #4866.

Refactor functions that print commands (Part 2) (#4905)

This PR is a step towards migrating commands to the Term/Sort level. It replaces the dynamic casts for printing commands with direct calls to corresponding functions. Those functions now take node level arguments instead of commands to make them available for internal code.

(proof-new) Theory preprocessor proof producing (#4807)

This makes the theory preprocessor proof producing in the new infrastructure, which involves updating its interfaces to TrustNode in a few places.

Introduce the theory state object (#4910)

This will be used as a standard way of querying and tracking state information in a Theory. The TheoryState object has a standard role in a number of the new standard templates for Theory:: methods.

The theory state is a collection of 4 Theory members (SAT context, user context, valuation, equality engine), as well as a SAT-context dependent "conflict" flag that indicates whether we have sent a conflict in this SAT conflict. It contains (safe) versions of equality engine queries, which are highly common in many theory solvers.

The next step will be to have the SolverState objects in theory of sets and strings inherit from this class.

Standardize collectModelInfo and theory-specific collectRelevantTerms (#4909)

This is work towards a configurable approach to equality engine management. This PR does not change any behavior, it only reorganizes the code.

This PR introduces the standard template for collectModelInfo, which isolates the usage of equality engine in relation to the model. In the future, theories will be encouraged to use the standard template for collectModelInfo and override collectRelevantTerms/collectModelValues only. This is to allow custom theory-independent modifications to building models (e.g. don't assert equality engine to model if we are using a centralized approach).

This PR standardizes TheoryArrays and TheoryDatatypes custom implementation of collectRelevantTerms as work towards using the standard template for collectModelInfo. Notice this required separating two portions of a loop in TheoryArrays::collectModelInfo which was doing two different things (collecting arrays and relevant terms).

(proof-new) Minor updates to trust node (#4900)

(proof-new) SMT proof postprocess callback (#4883)

This is the callback class for processing the final proof, which connects proofs of preprocessing and expands unwanted macro steps based on proof granularity mode.

The next step will be to add the ProofNodeUpdater that uses this callback and runs final sanity checks for checking proofs.

Quantifiers engine stores a pointer to the master equality engine (#4908)

This is work towards a configurable approach to theory combination.

Setting the master equality engine in QuantifiersEngine mimics setting EqualityEngine in Theory.

Split SygusSolver from SmtEngine (#4891)

This is the solver for standard SyGuS queries. Notice it now depends only on SmtSolver and not SmtEngine.

This PR updates Expr -> Node for the sygus interface in SmtEngine.

SmtEnginePrivate is no longer needed and is deleted with this PR.

Add the relevance manager module (#4894)

This PR adds the relevance manager module, which will be used in forthcoming PRs to query assignments for whether a literal is "relevant" (e.g. critical for satisfying the input formula). Leveraging this technique has led to noticeable improvements for non-linear arithmetic (https://github.com/ajreynol/CVC4/tree/relManager).

This PR does not enable it, but adds the module only.

(proof-new) Callbacks for term-context-sensitive terms (#4842)

Callbacks for term-context-sensitive terms.

It gives two examples of such callbacks, "remove term formula (rtf) context" to be used in the remove term formulas pass and "polarity context" which is a highly common pattern in preprocessing.

These utilities will be critical for maintain proofs for term-context-sensitive rewrites. An example user of these utilities is TermFormulaRemoval, which rewrites terms depending on whether they occur beneath quantifiers/terms. This utility currently has bugs in its proof generation since its proof cache does not consider the term context. This PR updates that class to use this utility. Its proof generator will be similarly extended in proof-new to synchronize its cache, relative to term context identifiers. Concretely, a TermContext callback will be passed to TConvProofGenerator, which will put together proof skeletons in a term-context-sensitive manner.

Add identifier name for side condition. (#4902)

```
(! sc (^ ...)
      ^ this is the identifier!
```

We require that side-conditions have an identifier. We usually provide
this identifier, but in this one case we did not.

The old lexer accepted the side condition without the identifier. The
new one does not.

[CI] Update package list (#4906)

Since
https://github.com/CVC4/LFSC/commit/1d1c55fa17b08e2bc8cb686b9d07ec63bf0dd4a2
LFSC requires Flex, so we need to install the corresponding packages in
our CI environment. This commit also removes SWIG from the list of
packages to install since we do not use it anymore.

Dynamic allocation of equality engine in Theory (#4890)

This commit updates Theory so that equality engines are allocated dynamically. The plan is to make this configurable based on the theory combination method.

The fundamental changes include:
- Add `d_equalityEngine` (raw) pointer to Theory, which is the "official" equality engine of the theory.
- Standardize methods for initializing Theory. This is now made more explicit in the documentation in theory.h, and includes a method `finishInitStandalone` for users of Theory that don't have an associated TheoryEngine.
- Refactor TheoryEngine::finishInit, including how Theory is initialized to incorporate the new policy.
- Things related to master equality engine are now specific to EqEngineManagerDistributed and hence can be removed from TheoryEngine. This will be further refactored in forthcoming PRs.

Note that the majority of changes are due to changing `d_equalityEngine.` to `d_equalityEngine->` throughout.

(proof-new) Prepare the theory of strings for proof reconstruction (#4885)

This updates the internal data structure for strings inferences "InferInfo" such that it is amenable to proof reconstruction.

Currently, the explanation for a conclusion is in two parts:
(1) d_ant, the antecedents that can be explained by the current equality engine,
(2) d_antn, the antecedents that cannot.

For proof reconstruction, the order of some antecedents matters. This is difficult with the above data structure since elements in these two vectors are not given an ordering relative to each other. After this PR, we store:
(1) d_ant, all antecedants, which are ordered in a way that is amenable to proofs (to be introduced on following PRs),
(2) d_noExplain, the subset of d_ant that cannot be explained by the current equality engine.

This PR modifies calls to InferenceManager in preparation for extending it with a proof reconstructor InferProofCons which will convert strings::InferInfo into instructions for building ProofNode.

Add non-emptiness to conclusion of positive RE star unfolding. (#4899)

A recent commit (77e9881) simplified the form of the conclusion in regular expression star unfolding for the sake of uniformity in our internal proof calculus. However, this led to a noticeable drop in performance on a few specific RE benchmarks (the Norn set). This preserves the old behavior by extending the core rule for RE unfolding.

It also makes one minor change to the strings proof checker carried over from the proof-new branch.

(cad solver) Use the current model as initial assignment (#4893)

This PR implements a first naive way to employ the linear model (obtained from the nonlinear extension) to guide the initial sampling within the cad solver.

Minor cleanup related to notifications (#4898)

This includes eliminating TheoryBV's call to eqNotifyNewEqClass and fixing an issue with string's eqNotifyNewEqClass method, which was registering constant integers.

It also removes some unnecessary methods in Theory.

Add finishInit method to PropEngine (#4895)

This changes an initialization issue in regarding PropEngine and TheoryEngine.

In the constructor for PropEngine, we convert and assert literals for true and false to CNF stream. Doing so triggers several things, including calls that preregister these literals with the associated TheoryEngine. This means that literals are preregistered to TheoryEngine before it has been fully initialized (TheoryEngine::finishInit). This is not currently an issue since this only involves modules that are constructed statically (e.g. SharedTermsDatabase), but this will lead to issues when the TheoryEngine is more configurable.

The solution is to additionally have a PropEngine::finishInit, which is called after TheoryEngine::finishInit, which does this step. The PropEngine should not assert anything to CNF before this method is called.

(proof-new) Add the strings proof checker (#4858)

It also adds enumeration for two new rules that have been recently added.

Simplify equality engine notifications (#4896)

Previously, there was methods for being informed just before and just after equivalence classes are merged (eqNotifyPreMerge and eqNotifyPostMerge). The purpose of this was to allow e.g. the theory to inspect the equivalence classes in question before the equality engine modified them. However this is no longer used, and moreover is discouraged since Theory should generally buffer their usage of EqualityEngine while it is making internal calls.

TheoryStrings was the only theory to use eqNotifyPreMerge (somewhat arbitrarily), all others used eqNotifyPostMerge. This makes post-merge the default, renames it to eqNotifyMerge and removes pre notifications.

This will simplify the work of the new theory combination methods as well as leading to fewer spurious calls to callbacks in equality engine.

correctly parse sygus lang option (#4884)

--lang sygus is a synonym for --lang sygus2
also fixes typo in error message for language options parsing

Signed-off-by: polgreen <epolgreen@gmail.com>

Inspect roots to avoid certain resultants (Algorithm 4, lines 8,9). (#4892)

This PR adds a small improvement to the CAD solver.
In Algorithm 4 of https://arxiv.org/pdf/2003.05633.pdf in lines 8 and 9, we only consider polynomials for resultant computations that have roots outside of the current interval.
This PR implements this check.
Fixes CVC4/cvc4-projects#210.

Split SmtSolver from SmtEngine (#4880)

This class is responsible for maintaining TheoryEngine and PropEngine and implementing the check-sat command. It also has an interface for processing/pushing the current assertions into the PropEngine.

This class will be used directly by other extension solvers (for abduction, interpolation, qe, sygus, etc.).

Fixes for corner case of decision tree learning with different types (#4887)

There was a last minute change was a typo when merging 103b5ea .
Also the fix in that commit needed to be slightly more robust to the case when either branch of an ITE had a different sygus type.

Fixes regress1.

More basic fix for dumping synth-fun (#4886)

The commit (079a04b) appears to have broken the nightlies due to compile issues related a necessary addition to the Dump class (so that std::string could be printing on Dump streams).

This changes the temporary solution so that we simply print a string on the standard output, when the Dump is enabled. This is required for temporarily keeping dump=raw-benchmark working for synth-fun commands.

Add the distributed equality engine manager (#4867)

This is the first step towards making the approach for theory combination in CVC4 configurable.

This PR introduces the "distributed equality engine manager", which encapsulates the current policy that TheoryEngine uses regarding equality engines: each Theory creates a separate copy of an equality engine. The eventual plan is that the official equality engine of Theory is not necessarily unique to the theory, if equality engines are shared. A variant of this class could implement that policy.

This PR does not impact the code, it simply adds the definition of the class. A forthcoming PR will integrate this class into TheoryEngine, which will use dynamic allocation for equality engine objects.

FYI @barrettcw

[proof-new] Adding support for corner case of transitivity simulating MERGED_THROUGH_CONSTANTS (#4879)

generalize handling MERGED_THROUGH_CONSTANST in EqProof conversion (#4878)

Now that we are using the constant folding in equality engine for more than equality it is necessary to generalize the previously-hard-coded handling of MERGED_THROUGH_CONSTANTS.

Refactor functions that print commands (Part 1) (#4869)

This PR is a step towards migrating commands to the Term/Sort level. The functions for printing synth-fun command and its grammar were modified to remove their dependency on command objects and use nodes instead of exprs and types. Similar changes to other functions that print commands will follow.

Fixes for degenerate case of sygus decision tree learning (#4800)

Fixes #4790.

Fixes two bugs in the decision tree learning solver for sygus, one involving evaluation of "templated" enumerators, and one involving ITE strategies where child types are different than the root.

(proof-new) Improve robustness of CONG rule (#4882)

This makes it so that the explicit Kind is wrapped in a Node as an argument to the CONG proof rule. This allows us to distinguish applications with the same parameterized operator but different kinds (e.g. APPLY_SELECTOR vs APPLY_SELECTOR_TOTAL).

(proof-new) Proof support in the strings term registry. (#4876)

Adds basic support for proofs in the strings term registry. This code is not yet active until further parts of proof-new are merged.

(proof-new) Improve interfaces to proof generators (#4803)

This includes configurable naming and a caching policy for term conversion proof generator.

Also corrects a subtle issue in LazyCDProof related to making getProofFor idempotent using the notion of owned proofs.

Add option to only build library (#4801)

This PR would add an option to only build the CVC4 library and not the parser or executable. This can be used for projects that only intend to use CVC4 through the API.

It seems to be working now, but it's not necessarily the cleanest solution. In particular, if you'd like the polarity to be different I'm happy to change that. Polarity meaning something like "${WITH_BINARY}" STREQUAL "YES" instead of NOT "${LIB_ONLY} STREQUAL "YES" which is admittedly a little strange.

(proof-new) Witness form proof generator (#4782)

This class is responsible for the connection between terms and their witness form in the final proof.

Add naive support for integer variables. (#4835)

This PR adds naive support for integer reasoning to the CAD-based solver.
Essentially, it checks whether the sampled value is integral. If this is not the case, we "invent" a new interval covering the area between the two neighbouring integers with appropriate border polynomials.

(proof-new) Improving proof-production in Equality Engine (#4871)

This commit improves functionalities of the equality engine so that it is easier to produce proofs for its reasoning. They are:

avoiding assertion of already entailed predicates/equalities.
better EqProof of disequalities with constants
correct EqProof involving n-ary congruence kinds

Fix connection to master equality engine in sets (#4877)

This corrects an issue introduced by a merge of a previous commit (b5b2858) which dropped the connection from sets to its master equality engine.

Fixes several issues in sets regressions, including a timeout in regress0.