From 708c5a14bca031100b05000ddae65a9828d76da0 Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Mon, 21 Dec 2020 17:20:23 +0100 Subject: [PATCH] (proof-new) Make nl-ext factoring lemmas proof producing. (#5698) This PR adds proofs for the lemmas from the nonlinear factoring check. --- src/theory/arith/nl/ext/factoring_check.cpp | 43 +++++++++++++++------ src/theory/arith/nl/ext/factoring_check.h | 20 +++++----- src/theory/arith/nl/nonlinear_extension.cpp | 2 +- 3 files changed, 44 insertions(+), 21 deletions(-) diff --git a/src/theory/arith/nl/ext/factoring_check.cpp b/src/theory/arith/nl/ext/factoring_check.cpp index 71c584e91..098f4500d 100644 --- a/src/theory/arith/nl/ext/factoring_check.cpp +++ b/src/theory/arith/nl/ext/factoring_check.cpp @@ -15,6 +15,7 @@ #include "theory/arith/nl/ext/factoring_check.h" #include "expr/node.h" +#include "expr/skolem_manager.h" #include "theory/arith/arith_msum.h" #include "theory/arith/inference_manager.h" #include "theory/arith/nl/nl_model.h" @@ -24,8 +25,7 @@ namespace theory { namespace arith { namespace nl { -FactoringCheck::FactoringCheck(InferenceManager& im, NlModel& model) - : d_im(im), d_model(model) +FactoringCheck::FactoringCheck(ExtState* data) : d_data(data) { d_zero = NodeManager::currentNM()->mkConst(Rational(0)); d_one = NodeManager::currentNM()->mkConst(Rational(1)); @@ -40,7 +40,7 @@ void FactoringCheck::check(const std::vector& asserts, { bool polarity = lit.getKind() != Kind::NOT; Node atom = lit.getKind() == Kind::NOT ? lit[0] : lit; - Node litv = d_model.computeConcreteModelValue(lit); + Node litv = d_data->d_model.computeConcreteModelValue(lit); bool considerLit = false; // Only consider literals that are in false_asserts. considerLit = std::find(false_asserts.begin(), false_asserts.end(), lit) @@ -120,7 +120,13 @@ void FactoringCheck::check(const std::vector& asserts, sum = Rewriter::rewrite(sum); Trace("nl-ext-factor") << "* Factored sum for " << x << " : " << sum << std::endl; - Node kf = getFactorSkolem(sum); + + CDProof* proof = nullptr; + if (d_data->isProofEnabled()) + { + proof = d_data->getProof(); + } + Node kf = getFactorSkolem(sum, proof); std::vector poly; poly.push_back(nm->mkNode(Kind::MULT, x, kf)); std::map >::iterator itfo = @@ -149,26 +155,41 @@ void FactoringCheck::check(const std::vector& asserts, } std::vector lemma_disj; - lemma_disj.push_back(lit.negate()); lemma_disj.push_back(conc_lit); + lemma_disj.push_back(lit.negate()); Node flem = nm->mkNode(Kind::OR, lemma_disj); Trace("nl-ext-factor") << "...lemma is " << flem << std::endl; - d_im.addPendingArithLemma(flem, InferenceId::NL_FACTOR); + if (d_data->isProofEnabled()) + { + Node k_eq = kf.eqNode(sum); + Node split = nm->mkNode(Kind::OR, lit, lit.notNode()); + proof->addStep(split, PfRule::SPLIT, {}, {lit}); + proof->addStep( + flem, PfRule::MACRO_SR_PRED_TRANSFORM, {split, k_eq}, {flem}); + } + d_data->d_im.addPendingArithLemma( + flem, InferenceId::NL_FACTOR, proof); } } } } } -Node FactoringCheck::getFactorSkolem(Node n) +Node FactoringCheck::getFactorSkolem(Node n, CDProof* proof) { std::map::iterator itf = d_factor_skolem.find(n); if (itf == d_factor_skolem.end()) { NodeManager* nm = NodeManager::currentNM(); - Node k = nm->mkSkolem("kf", n.getType()); - Node k_eq = Rewriter::rewrite(k.eqNode(n)); - d_im.addPendingArithLemma(k_eq, InferenceId::NL_FACTOR); + Node k = nm->getSkolemManager()->mkPurifySkolem(n, "kf"); + Node k_eq = k.eqNode(n); + Trace("nl-ext-factor") << "...adding factor skolem " << k << " == " << n + << std::endl; + if (d_data->isProofEnabled()) + { + proof->addStep(k_eq, PfRule::MACRO_SR_PRED_INTRO, {}, {k_eq}); + } + d_data->d_im.addPendingArithLemma(k_eq, InferenceId::NL_FACTOR, proof); d_factor_skolem[n] = k; return k; } @@ -178,4 +199,4 @@ Node FactoringCheck::getFactorSkolem(Node n) } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC4 \ No newline at end of file +} // namespace CVC4 diff --git a/src/theory/arith/nl/ext/factoring_check.h b/src/theory/arith/nl/ext/factoring_check.h index 9f879aa39..fa0f8239a 100644 --- a/src/theory/arith/nl/ext/factoring_check.h +++ b/src/theory/arith/nl/ext/factoring_check.h @@ -18,8 +18,7 @@ #include #include "expr/node.h" -#include "theory/arith/inference_manager.h" -#include "theory/arith/nl/nl_model.h" +#include "theory/arith/nl/ext/ext_state.h" namespace CVC4 { namespace theory { @@ -29,12 +28,12 @@ namespace nl { class FactoringCheck { public: - FactoringCheck(InferenceManager& im, NlModel& model); + FactoringCheck(ExtState* data); /** check factoring * * Returns a set of valid theory lemmas, based on a - * lemma schema that states a relationship betwen monomials + * lemma schema that states a relationship between monomials * with common factors that occur in the same constraint. * * Examples: @@ -47,17 +46,20 @@ class FactoringCheck const std::vector& false_asserts); private: - /** The inference manager that we push conflicts and lemmas to. */ - InferenceManager& d_im; - /** Reference to the non-linear model object */ - NlModel& d_model; + /** Basic data that is shared with other checks */ + ExtState* d_data; + /** maps nodes to their factor skolems */ std::map d_factor_skolem; Node d_zero; Node d_one; - Node getFactorSkolem(Node n); + /** + * Introduces a new purification skolem k for n and adds k=n as lemma. + * If proof is not nullptr, it proves this lemma via MACRO_SR_PRED_INTRO. + */ + Node getFactorSkolem(Node n, CDProof* proof); }; } // namespace nl diff --git a/src/theory/arith/nl/nonlinear_extension.cpp b/src/theory/arith/nl/nonlinear_extension.cpp index b97a53f95..c6787140d 100644 --- a/src/theory/arith/nl/nonlinear_extension.cpp +++ b/src/theory/arith/nl/nonlinear_extension.cpp @@ -49,7 +49,7 @@ NonlinearExtension::NonlinearExtension(TheoryArith& containing, d_model(containing.getSatContext()), d_trSlv(d_im, d_model, pnm, containing.getUserContext()), d_extState(d_im, d_model, pnm, containing.getUserContext()), - d_factoringSlv(d_im, d_model), + d_factoringSlv(&d_extState), d_monomialBoundsSlv(&d_extState), d_monomialSlv(&d_extState), d_splitZeroSlv(&d_extState), -- 2.30.2