diff options
author | Gereon Kremer <gkremer@stanford.edu> | 2020-12-18 08:26:55 +0100 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-12-18 08:26:55 +0100 |
commit | 0ae11d1abec9017784eefa2252d8e8ea7dfb4f74 (patch) | |
tree | eaca05442c315dcd9956047ebb6f5eaa63c56102 /src/theory | |
parent | 9b099b715cec0dc60048fdc64b4d61b977d14096 (diff) |
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.
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/arith/nl/ext/split_zero_check.cpp | 22 | ||||
-rw-r--r-- | src/theory/arith/nl/ext/split_zero_check.h | 2 | ||||
-rw-r--r-- | 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), |