| Age | Commit message (Collapse) | Author |
|---|
|
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.
|
|
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.
|
|
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.
|
|
This makes the CAD solver use the new arith::InferenceManager instead of the previously used lemma collection scheme.
|
|
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.
|
|
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.
|
|
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.
|
|
These updates are inspired by the current inference manager for sets.
|
|
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.
|
|
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.
|
|
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.
|
|
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.
|
|
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.
|
