diff options
author | Gereon Kremer <gereon.kremer@cs.rwth-aachen.de> | 2020-11-20 14:08:45 +0100 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-11-20 07:08:45 -0600 |
commit | de0d36b8972954c281f1e97b15d37c07a861cbc1 (patch) | |
tree | 23063fd32dd8c7d2509684014fca07fe92887b48 /src/theory/arith/inference_manager.h | |
parent | f2ed7b1aebc175b971e3cebf4c0b2fff6e4e895f (diff) |
Allow to pass ProofGenerator to arithmetic inference manager. (#5488)
This PR prepares the addition of proofs for the arithmetic theory by making addPendingArithLemma() accept a ProofGenerator*.
Diffstat (limited to 'src/theory/arith/inference_manager.h')
-rw-r--r-- | src/theory/arith/inference_manager.h | 15 |
1 files changed, 8 insertions, 7 deletions
diff --git a/src/theory/arith/inference_manager.h b/src/theory/arith/inference_manager.h index f2784ed89..66710cd7b 100644 --- a/src/theory/arith/inference_manager.h +++ b/src/theory/arith/inference_manager.h @@ -37,7 +37,7 @@ class TheoryArith; * arithmetic theory. * * It adds some convenience methods to send ArithLemma and adds a mechanism for - * waiting lemmas that can be flushed into the pending lemmas of the this + * waiting lemmas that can be flushed into the pending lemmas of this * buffered inference manager. * It also extends the caching mechanism of TheoryInferenceManager to cache * preprocessing lemmas and non-preprocessing lemmas separately. For the former, @@ -51,29 +51,30 @@ class InferenceManager : public InferenceManagerBuffered InferenceManager(TheoryArith& ta, ArithState& astate, ProofNodeManager* pnm); /** - * Add a lemma as pending lemma to the this inference manager. + * Add a lemma as pending lemma to this inference manager. * If isWaiting is true, the lemma is first stored as waiting lemma and only * added as pending lemma when calling flushWaitingLemmas. */ void addPendingArithLemma(std::unique_ptr<ArithLemma> lemma, bool isWaiting = false); /** - * Add a lemma as pending lemma to the this inference manager. + * Add a lemma as pending lemma to this inference manager. * If isWaiting is true, the lemma is first stored as waiting lemma and only * added as pending lemma when calling flushWaitingLemmas. */ void addPendingArithLemma(const ArithLemma& lemma, bool isWaiting = false); /** - * Add a lemma as pending lemma to the this inference manager. + * Add a lemma as pending lemma to this inference manager. * If isWaiting is true, the lemma is first stored as waiting lemma and only * added as pending lemma when calling flushWaitingLemmas. */ void addPendingArithLemma(const Node& lemma, InferenceId inftype, + ProofGenerator* pg = nullptr, bool isWaiting = false); /** - * Flush all waiting lemmas to the this inference manager (as pending + * Flush all waiting lemmas to this inference manager (as pending * lemmas). To actually send them, call doPendingLemmas() afterwards. */ void flushWaitingLemmas(); @@ -84,8 +85,8 @@ class InferenceManager : public InferenceManagerBuffered void clearWaitingLemmas(); /** - * Checks whether we have made any progress, that is whether a conflict, lemma - * or fact was added or whether a lemma or fact is pending. + * Checks whether we have made any progress, that is whether a conflict, + * lemma or fact was added or whether a lemma or fact is pending. */ bool hasUsed() const; |