From 2937d0770d448e74b5cf9f9b02de31145a7c5738 Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Wed, 23 Dec 2020 04:40:45 +0100 Subject: [PATCH] Add proofs for nonlinear sign lemmas. (#5707) This PR adds proof support for NL_SIGN lemmas. --- src/theory/arith/nl/ext/monomial_check.cpp | 15 ++++++++++++--- 1 file changed, 12 insertions(+), 3 deletions(-) diff --git a/src/theory/arith/nl/ext/monomial_check.cpp b/src/theory/arith/nl/ext/monomial_check.cpp index a70fa1bc0..199ba1746 100644 --- a/src/theory/arith/nl/ext/monomial_check.cpp +++ b/src/theory/arith/nl/ext/monomial_check.cpp @@ -311,8 +311,17 @@ int MonomialCheck::compareSign( { if (mvaoa.getConst().sgn() != 0) { - Node lemma = av.eqNode(d_data->d_zero).impNode(oa.eqNode(d_data->d_zero)); - d_data->d_im.addPendingArithLemma(lemma, InferenceId::NL_SIGN); + Node prem = av.eqNode(d_data->d_zero); + Node conc = oa.eqNode(d_data->d_zero); + Node lemma = prem.impNode(conc); + CDProof* proof = nullptr; + if (d_data->isProofEnabled()) + { + proof = d_data->getProof(); + proof->addStep(conc, PfRule::MACRO_SR_PRED_INTRO, {prem}, {conc}); + proof->addStep(lemma, PfRule::SCOPE, {conc}, {prem}); + } + d_data->d_im.addPendingArithLemma(lemma, InferenceId::NL_SIGN, proof); } return 0; } @@ -737,4 +746,4 @@ void MonomialCheck::setMonomialFactor(Node a, } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC4 \ No newline at end of file +} // namespace CVC4 -- 2.30.2