From: Gereon Kremer <gkremer@cs.stanford.edu>
Date: Wed, 9 Mar 2022 16:37:13 +0000 (+0100)
Subject: Clear obsolete pending lemmas in arithmetic (#8236)
X-Git-Tag: cvc5-1.0.0~292
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=aba33913501586fc695e0a8be4169b962877edfc;p=cvc5.git

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 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");