From: Gereon Kremer <gkremer@stanford.edu>
Date: Fri, 18 Dec 2020 07:26:55 +0000 (+0100)
Subject: Add proof for split zero check. (#5699)
X-Git-Tag: cvc5-1.0.0~2425
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=0ae11d1abec9017784eefa2252d8e8ea7dfb4f74;p=cvc5.git

Add proof for split zero check. (#5699)

This PR adds a proof for the nl-ext check to split at zero. As we can use the SPLIT rule, this requires no new proof rule.
---

diff --git a/src/theory/arith/nl/ext/split_zero_check.cpp b/src/theory/arith/nl/ext/split_zero_check.cpp
index fcbf84be4..d158281cc 100644
--- a/src/theory/arith/nl/ext/split_zero_check.cpp
+++ b/src/theory/arith/nl/ext/split_zero_check.cpp
@@ -24,8 +24,8 @@ namespace theory {
 namespace arith {
 namespace nl {
 
-SplitZeroCheck::SplitZeroCheck(ExtState* data, context::Context* ctx)
-    : d_data(data), d_zero_split(ctx)
+SplitZeroCheck::SplitZeroCheck(ExtState* data)
+    : d_data(data), d_zero_split(d_data->d_ctx)
 {
 }
 
@@ -36,14 +36,16 @@ void SplitZeroCheck::check()
     Node v = d_data->d_ms_vars[i];
     if (d_zero_split.insert(v))
     {
-      Node eq = v.eqNode(d_data->d_zero);
-      eq = Rewriter::rewrite(eq);
+      Node eq = Rewriter::rewrite(v.eqNode(d_data->d_zero));
+      Node lem = eq.orNode(eq.negate());
+      CDProof* proof = nullptr;
+      if (d_data->isProofEnabled())
+      {
+        proof = d_data->getProof();
+        proof->addStep(lem, PfRule::SPLIT, {}, {eq});
+      }
       d_data->d_im.addPendingPhaseRequirement(eq, true);
-      ArithLemma lem(eq.orNode(eq.negate()),
-                     LemmaProperty::NONE,
-                     nullptr,
-                     InferenceId::NL_SPLIT_ZERO);
-      d_data->d_im.addPendingArithLemma(lem);
+      d_data->d_im.addPendingArithLemma(lem, InferenceId::NL_SPLIT_ZERO, proof);
     }
   }
 }
@@ -51,4 +53,4 @@ void SplitZeroCheck::check()
 }  // namespace nl
 }  // namespace arith
 }  // namespace theory
-}  // namespace CVC4
\ No newline at end of file
+}  // namespace CVC4
diff --git a/src/theory/arith/nl/ext/split_zero_check.h b/src/theory/arith/nl/ext/split_zero_check.h
index 131ad4c99..e8730e496 100644
--- a/src/theory/arith/nl/ext/split_zero_check.h
+++ b/src/theory/arith/nl/ext/split_zero_check.h
@@ -26,7 +26,7 @@ namespace nl {
 class SplitZeroCheck
 {
  public:
-  SplitZeroCheck(ExtState* data, context::Context* ctx);
+  SplitZeroCheck(ExtState* data);
 
   /** check split zero
    *
diff --git a/src/theory/arith/nl/nonlinear_extension.cpp b/src/theory/arith/nl/nonlinear_extension.cpp
index e4a71b34d..d52095e95 100644
--- a/src/theory/arith/nl/nonlinear_extension.cpp
+++ b/src/theory/arith/nl/nonlinear_extension.cpp
@@ -52,7 +52,7 @@ NonlinearExtension::NonlinearExtension(TheoryArith& containing,
       d_factoringSlv(d_im, d_model),
       d_monomialBoundsSlv(&d_extState),
       d_monomialSlv(&d_extState),
-      d_splitZeroSlv(&d_extState, state.getUserContext()),
+      d_splitZeroSlv(&d_extState),
       d_tangentPlaneSlv(&d_extState),
       d_cadSlv(d_im, d_model),
       d_icpSlv(d_im),