From: Gereon Kremer <gereon.kremer@cs.rwth-aachen.de>
Date: Wed, 23 Dec 2020 03:40:45 +0000 (+0100)
Subject: Add proofs for nonlinear sign lemmas. (#5707)
X-Git-Tag: cvc5-1.0.0~2407
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=2937d0770d448e74b5cf9f9b02de31145a7c5738;p=cvc5.git

Add proofs for nonlinear sign lemmas. (#5707)

This PR adds proof support for NL_SIGN lemmas.
---

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<Rational>().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