diff options
author | Gereon Kremer <gereon.kremer@cs.rwth-aachen.de> | 2020-09-02 15:48:12 +0200 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-09-02 08:48:12 -0500 |
commit | 02e682821028bc704c57a762dadeb6f82bb70ebf (patch) | |
tree | 4eb20c4d3e6b06eaee58b808909e603da013b554 /src/theory/inference_manager_buffered.h | |
parent | 78917e16f6521b0e8a074f3649fc6adf37614617 (diff) |
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.
Diffstat (limited to 'src/theory/inference_manager_buffered.h')
-rw-r--r-- | src/theory/inference_manager_buffered.h | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/src/theory/inference_manager_buffered.h b/src/theory/inference_manager_buffered.h index e6e7822c5..762b7d4e0 100644 --- a/src/theory/inference_manager_buffered.h +++ b/src/theory/inference_manager_buffered.h @@ -35,7 +35,7 @@ class InferenceManagerBuffered : public TheoryInferenceManager InferenceManagerBuffered(Theory& t, TheoryState& state, ProofNodeManager* pnm); - ~InferenceManagerBuffered() {} + virtual ~InferenceManagerBuffered() {} /** * Have we processed an inference during this call to check? In particular, * this returns true if we have a pending fact or lemma, or have encountered @@ -124,6 +124,11 @@ class InferenceManagerBuffered : public TheoryInferenceManager /** Clear pending phase requirements, without processing */ void clearPendingPhaseRequirements(); + /** Returns the number of pending lemmas. */ + std::size_t numPendingLemmas() const; + /** Returns the number of pending facts. */ + std::size_t numPendingFacts() const; + protected: /** A set of pending inferences to be processed as lemmas */ std::vector<std::shared_ptr<TheoryInference>> d_pendingLem; |