| Age | Commit message (Collapse) | Author |
|---|
|
and regressions (#6943)
This commit makes TheoryEngine take into account whether theories are using the central equality engine.
With this commit, the central equality engine can now be optionally enabled via `--ee-mode=central`.
|
|
Minor reorganization to make calls to theory engine from combination engine / shared solver more organized.
|
|
This moves all generic proof utilites from src/expr/ and src/theory/ to src/proof/.
It also changes the include for term conversion proof generator to conv_proof_generator in preparation to rename this utility on a followup PR (to avoid confusion with the use of "Term").
|
|
This unifies top-level substitutions and theory model substitutions. Env is now passed to the TheoryModel, which has access to top-level substitutions.
The former was used for simplfying assertions in the preprocessor, the latter was used for evaluating terms in the model.
There is no reason to have these two things be separate.
|
|
This is work towards making the initialization of theory engine, theory models, quantifiers engine more flexible.
This makes it so that the specialized quantifiers models classes (FirstOrderModel) do not inherit from TheoryModel. There is no longer any reason for this, since FirstOrderModel does not have any override methods.
As a result of this PR, there is only one kind of TheoryModel and it is constructed immediately when ModelManager is constructed.
This required refactoring the initialization of when FirstOrderModel is constructed in ModelBuilder classes in quantifiers.
This also avoids the need for casting TheoryModel to FirstOrderModel.
|
|
|
|
|
|
|
|
This PR does some more cleanup of the includes.
|
|
|
|
This makes it so that TheoryEngine::lemma returns void not LemmaStatus.
Currently, there was only one use of LemmaStatus by theory solvers, which was CEGQI using it as a way of getting the preprocessed form of a lemma. This makes it so that there is an explicit method in Valuation for getting the preprocessed form of a term + its skolems and their definition assertions.
It also simplifies a few things, e.g. Valuation calls are forwarded to PropEngine instead of going through TheoryEngine. It fixes a few issues in TermFormulaRemoval related to getSkolems.
|
|
This refactors quantifiers so that it uses the standard interfaces for setting up an equality engine and using it via TheoryState.
This eliminates the need for several special interfaces including getMasterEqualityEngine, CombinationEngine::getCoreEqualityEngine, and most uses of EqualityQuery.
|
|
This makes the shared terms database use a proof equality engine as a layer on top of its equality engine, analogous to how this done in theories.
|
|
This makes SharedSolver the main communication point for TheoryEngine during solving for combination-related solving tasks. This class is a generalization of SharedTermsDatabase, and in the distributed architecture is a wrapper around shared terms database.
It has 5 callbacks in theory engine: for preregistration, preNotifyFact (which calls addSharedTerms on theories), assertSharedEquality, explain, getEqualityStatus.
This PR has no intended behavior changes.
FYI @barrettcw
|
|
This PR updates the update-copyright.pl script to also update/add copyright headers to CMake specific files. It further fixes a small typo in the header.
|
|
This PR makes it so that the distributed model manager can be used independently of the architecture for equality engine management for theories, meaning the choice of using a separate equality engine for the model can be done in both the current distributed architecture, or the proposed central architecture (where there would be 2 equality engines, the central one and the model one). The "central model manager" on the other hand will only be combined with the central architecture. This will make it easier to test the centralized equality engine manager, since all things related to model construction can be preserved when using a central architecture.
This PR moves some of the responsibilities from the (distributed) equality engine manager to the distributed model manager, including the management of the context of the model equality engine and the allocation of its equality engine.
This PR is not intended to make any behavior changes to the current architecture.
|
|
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.
|
|
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).
|
|
Makes combination engine proof producing (for Boolean splits). Followup PRs will start to add proof production in TheoryEngine.
|
|
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.
|
