From aba33913501586fc695e0a8be4169b962877edfc Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Wed, 9 Mar 2022 17:37:13 +0100 Subject: [PATCH] Clear obsolete pending lemmas in arithmetic (#8236) Arithmetic generally generates nonlinear lemmas as full effort checks, but only sends them out in the subsequent last call effort check. If this one does not happen, the next full effort check still has pending lemmas that may not only be irrelevant now, but possibly carry proofs that are already out of scope. This PR makes sure that such lemmas are always pruned. Fixes cvc5/cvc5-projects#465 --- src/theory/arith/theory_arith.cpp | 24 ++++++++++++------- test/regress/CMakeLists.txt | 4 +++- .../nl/proj-issue-465-asan-proofs.smt2 | 11 +++++++++ ....15.RTE.Terminate_System.Int32_approx.smt2 | 1 + .../regress1/nl/arrowsmith-050317.smt2 | 1 + test/unit/api/cpp/theory_arith_nl_black.cpp | 4 ++++ 6 files changed, 35 insertions(+), 10 deletions(-) create mode 100644 test/regress/regress0/nl/proj-issue-465-asan-proofs.smt2 diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index 26e3c52f1..252dd5d54 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -164,19 +164,25 @@ void TheoryArith::postCheck(Effort level) { d_im.reset(); Trace("arith-check") << "TheoryArith::postCheck " << level << std::endl; + if (Theory::fullEffort(level)) + { + // Make sure we don't have old lemmas floating around. This can happen if we + // didn't actually reach a last call effort check, but backtracked for some + // other reason. In such a case, these lemmas are likely to be irrelevant + // and possibly even harmful. If we produce proofs, their proofs have most + // likely been deallocated already as well. + d_im.clearPending(); + d_im.clearWaitingLemmas(); + } // check with the non-linear solver at last call if (level == Theory::EFFORT_LAST_CALL) { - if (d_nonlinearExtension != nullptr) + // If we computed lemmas in the last FULL_EFFORT check, send them now. + if (d_im.hasPendingLemma()) { - // If we computed lemmas in the last FULL_EFFORT check, send them now. - if (d_im.hasPendingLemma()) - { - d_im.doPendingFacts(); - d_im.doPendingLemmas(); - d_im.doPendingPhaseRequirements(); - return; - } + d_im.doPendingFacts(); + d_im.doPendingLemmas(); + d_im.doPendingPhaseRequirements(); } return; } diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 474f44640..c4c85c8f0 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -825,6 +825,7 @@ set(regress_0_tests regress0/nl/proj-issue-444-memout-eqelim.smt2 regress0/nl/proj-issue-451-ran-combination-1.smt2 regress0/nl/proj-issue-451-ran-combination-2.smt2 + regress0/nl/proj-issue-465-asan-proofs.smt2 regress0/nl/real-as-int.smt2 regress0/nl/real-div-ufnra.smt2 regress0/nl/sin-cos-346-b-chunk-0169.smt2 @@ -1974,7 +1975,6 @@ set(regress_1_tests regress1/nl/proj-issue215.smt2 regress1/nl/proj-issue231.smt2 regress1/nl/proj-issue232.smt2 - regress1/nl/proj-issue251.smt2 regress1/nl/proj-issue253.smt2 regress1/nl/proj-issue279.smt2 regress1/nl/proj-issue280.smt2 @@ -3058,6 +3058,8 @@ set(regression_disabled_tests regress1/nl/NAVIGATION2.smt2 # sat or unknown in different builds regress1/nl/issue3307.smt2 + # times out after changes to nl-ext in #8236 + regress1/nl/proj-issue251.smt2 # slow with sygus-inference after removing anti-skolemization regress1/quantifiers/anti-sk-simp.smt2 # no longer support snorm option diff --git a/test/regress/regress0/nl/proj-issue-465-asan-proofs.smt2 b/test/regress/regress0/nl/proj-issue-465-asan-proofs.smt2 new file mode 100644 index 000000000..abb7d394d --- /dev/null +++ b/test/regress/regress0/nl/proj-issue-465-asan-proofs.smt2 @@ -0,0 +1,11 @@ +; COMMAND-LINE: -i -q --produce-proofs +; EXPECT: sat +; EXPECT: sat +(set-logic NRA) +(declare-fun v () Real) +(push) +(assert (and (forall ((V Real)) (and (< 0.0 (/ 0.0 v)) (= (/ 0.0 0.0) (/ (- 1.0) (- v 1.0))))))) +(check-sat) +(pop) +(assert (= 0 (* v v))) +(check-sat) diff --git a/test/regress/regress0/use_approx/specsharp-WindowsCard.15.RTE.Terminate_System.Int32_approx.smt2 b/test/regress/regress0/use_approx/specsharp-WindowsCard.15.RTE.Terminate_System.Int32_approx.smt2 index 729c5cdd2..6ae950512 100644 --- a/test/regress/regress0/use_approx/specsharp-WindowsCard.15.RTE.Terminate_System.Int32_approx.smt2 +++ b/test/regress/regress0/use_approx/specsharp-WindowsCard.15.RTE.Terminate_System.Int32_approx.smt2 @@ -1,4 +1,5 @@ ; REQUIRES: glpk +; DISABLE-TESTER: unsat-core ; COMMAND-LINE: --use-approx ; EXPECT: unsat (set-logic UFNIA) diff --git a/test/regress/regress1/nl/arrowsmith-050317.smt2 b/test/regress/regress1/nl/arrowsmith-050317.smt2 index 762d617ad..a62ba6012 100644 --- a/test/regress/regress1/nl/arrowsmith-050317.smt2 +++ b/test/regress/regress1/nl/arrowsmith-050317.smt2 @@ -1,3 +1,4 @@ +; DISABLE-TESTER: unsat-core ; COMMAND-LINE: --nl-ext=full ; EXPECT: unsat (set-logic QF_NRAT) diff --git a/test/unit/api/cpp/theory_arith_nl_black.cpp b/test/unit/api/cpp/theory_arith_nl_black.cpp index 9fc19fb79..f902378cd 100644 --- a/test/unit/api/cpp/theory_arith_nl_black.cpp +++ b/test/unit/api/cpp/theory_arith_nl_black.cpp @@ -90,6 +90,10 @@ TEST_F(TestTheoryBlackArithNl, proj_issue421) TEST_F(TestTheoryBlackArithNl, cvc5Projects455) { + if (!Configuration::isBuiltWithPoly()) + { + return; + } Solver slv; slv.setLogic("QF_UFNRA"); slv.setOption("produce-unsat-assumptions", "true"); -- 2.30.2