Age | Commit message (Collapse) | Author |
|
|
|
|
|
|
|
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.
|