From de0d36b8972954c281f1e97b15d37c07a861cbc1 Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Fri, 20 Nov 2020 14:08:45 +0100 Subject: [PATCH] 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*. --- src/theory/arith/inference_manager.cpp | 3 ++- src/theory/arith/inference_manager.h | 15 ++++++++------- src/theory/arith/nl/ext/monomial_bounds_check.cpp | 4 ++-- src/theory/arith/nl/ext/tangent_plane_check.cpp | 4 ++-- src/theory/arith/nl/iand_solver.cpp | 6 ++++-- src/theory/arith/nl/transcendental_solver.cpp | 2 +- 6 files changed, 19 insertions(+), 15 deletions(-) diff --git a/src/theory/arith/inference_manager.cpp b/src/theory/arith/inference_manager.cpp index 43359c460..08d223137 100644 --- a/src/theory/arith/inference_manager.cpp +++ b/src/theory/arith/inference_manager.cpp @@ -68,10 +68,11 @@ void InferenceManager::addPendingArithLemma(const ArithLemma& lemma, } void InferenceManager::addPendingArithLemma(const Node& lemma, InferenceId inftype, + ProofGenerator* pg, bool isWaiting) { addPendingArithLemma(std::unique_ptr(new ArithLemma( - lemma, LemmaProperty::NONE, nullptr, inftype)), + lemma, LemmaProperty::NONE, pg, inftype)), isWaiting); } 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 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; diff --git a/src/theory/arith/nl/ext/monomial_bounds_check.cpp b/src/theory/arith/nl/ext/monomial_bounds_check.cpp index fe4b1b83a..de6a3c65d 100644 --- a/src/theory/arith/nl/ext/monomial_bounds_check.cpp +++ b/src/theory/arith/nl/ext/monomial_bounds_check.cpp @@ -320,7 +320,7 @@ void MonomialBoundsCheck::checkBounds(const std::vector& asserts, // Trace("nl-ext-bound-lemma") << " intro new // monomials = " << introNewTerms << std::endl; d_data->d_im.addPendingArithLemma( - iblem, InferenceId::NL_INFER_BOUNDS_NT, introNewTerms); + iblem, InferenceId::NL_INFER_BOUNDS_NT, nullptr, introNewTerms); } } } @@ -497,4 +497,4 @@ void MonomialBoundsCheck::checkResBounds() } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC4 \ No newline at end of file +} // namespace CVC4 diff --git a/src/theory/arith/nl/ext/tangent_plane_check.cpp b/src/theory/arith/nl/ext/tangent_plane_check.cpp index 5235b7d43..3849c8424 100644 --- a/src/theory/arith/nl/ext/tangent_plane_check.cpp +++ b/src/theory/arith/nl/ext/tangent_plane_check.cpp @@ -133,7 +133,7 @@ void TangentPlaneCheck::check(bool asWaitingLemmas) Trace("nl-ext-tplanes") << "Tangent plane lemma : " << tlem << std::endl; d_data->d_im.addPendingArithLemma( - tlem, InferenceId::NL_TANGENT_PLANE, asWaitingLemmas); + tlem, InferenceId::NL_TANGENT_PLANE, nullptr, asWaitingLemmas); } } } @@ -145,4 +145,4 @@ void TangentPlaneCheck::check(bool asWaitingLemmas) } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC4 \ No newline at end of file +} // namespace CVC4 diff --git a/src/theory/arith/nl/iand_solver.cpp b/src/theory/arith/nl/iand_solver.cpp index 30441a8f4..e33cfa6cd 100644 --- a/src/theory/arith/nl/iand_solver.cpp +++ b/src/theory/arith/nl/iand_solver.cpp @@ -151,7 +151,8 @@ void IAndSolver::checkFullRefine() Node lem = sumBasedLemma(i); // add lemmas based on sum mode Trace("iand-lemma") << "IAndSolver::Lemma: " << lem << " ; SUM_REFINE" << std::endl; - d_im.addPendingArithLemma(lem, InferenceId::NL_IAND_SUM_REFINE, true); + d_im.addPendingArithLemma( + lem, InferenceId::NL_IAND_SUM_REFINE, nullptr, true); } else if (options::iandMode() == options::IandMode::BITWISE) { @@ -163,7 +164,8 @@ void IAndSolver::checkFullRefine() Node lem = valueBasedLemma(i); Trace("iand-lemma") << "IAndSolver::Lemma: " << lem << " ; VALUE_REFINE" << std::endl; - d_im.addPendingArithLemma(lem, InferenceId::NL_IAND_VALUE_REFINE, true); + d_im.addPendingArithLemma( + lem, InferenceId::NL_IAND_VALUE_REFINE, nullptr, true); } } } diff --git a/src/theory/arith/nl/transcendental_solver.cpp b/src/theory/arith/nl/transcendental_solver.cpp index b3248119b..2e25f1642 100644 --- a/src/theory/arith/nl/transcendental_solver.cpp +++ b/src/theory/arith/nl/transcendental_solver.cpp @@ -875,7 +875,7 @@ bool TranscendentalSolver::checkTfTangentPlanesFun(Node tf, << "*** Tangent plane lemma : " << lem << std::endl; Assert(d_model.computeAbstractModelValue(lem) == d_false); // Figure 3 : line 9 - d_im.addPendingArithLemma(lem, InferenceId::NL_T_TANGENT, true); + d_im.addPendingArithLemma(lem, InferenceId::NL_T_TANGENT, nullptr, true); } else if (is_secant) { -- 2.30.2