diff options
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; |