| Age | Commit message (Collapse) | Author |
|---|
|
We now use std::unique_ptr instead of std::shared_ptr when storing TheoryInference objects.
|
|
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.
|
|
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 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.
|
