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

diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 26e3c52f1788df9a42ee15a25271829903093166..252dd5d54d160bcb018da93e3fe4ba5c93e55fcf 100644 (file)
--- 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 474f446409fdf6c99cf4a4498e0efda40aa2f7fe..c4c85c8f016b203e9e6dc5bb11aac89dc92b661a 100644 (file)
--- 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 (file)
index 0000000..abb7d39
--- /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 729c5cdd2daaeb49a5b58bb7c4ce3be05b6a707d..6ae950512daa645ef527a61f42043e28ed54e298 100644 (file)
--- 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 762d617ad6d6ec12a63f7421a1bb8e078d914f1c..a62ba6012bebc3f203b348e84935e48eeeec534f 100644 (file)
--- 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 9fc19fb79529a26fa6cd3094c638f8371ad0a745..f902378cd78d710497492d903945fec6c642c151 100644 (file)
--- 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");