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 fcbf84be43b5c285fc84671d2cc28613a4a4db19..d158281ccf672b18ce11b9538e01e8c2de1f0336 100644 (file)
--- 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 131ad4c99d13e957700a46c3b206549bcbbcc568..e8730e496dd941300f36233d475d65fe92654b87 100644 (file)
--- 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 e4a71b34ddf541d480dd99b5c71aa32295bce36a..d52095e958ae06bd03bcdf7c52e961e822df1732 100644 (file)
--- 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),