From 0ae11d1abec9017784eefa2252d8e8ea7dfb4f74 Mon Sep 17 00:00:00 2001
From: Gereon Kremer <gkremer@stanford.edu>
Date: Fri, 18 Dec 2020 08:26:55 +0100
Subject: [PATCH] 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.
---
 src/theory/arith/nl/ext/split_zero_check.cpp | 22 +++++++++++---------
 src/theory/arith/nl/ext/split_zero_check.h   |  2 +-
 src/theory/arith/nl/nonlinear_extension.cpp  |  2 +-
 3 files changed, 14 insertions(+), 12 deletions(-)

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),
-- 
2.30.2