From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 24 Jun 2021 11:37:20 +0000 (-0500)
Subject: Fix linear arithmetic for duplicate lemmas in incremental (#6784)
X-Git-Tag: cvc5-1.0.0~1558
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=4eaef5e472121396ee77023d49b23556ac69b747;p=cvc5.git

Fix linear arithmetic for duplicate lemmas in incremental (#6784)

The linear arithmetic solver was not robust to cases where a duplicate lemma is emitted. This leads to non-linear arithmetic not being called to check at full effort, leading to potential model soundness issues.

Fixes #6773.
---

diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index 97b29b6b3..98de1eeee 100644
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -1830,15 +1830,15 @@ void TheoryArithPrivate::outputConflicts(){
   }
 }
 
-void TheoryArithPrivate::outputTrustedLemma(TrustNode lemma, InferenceId id)
+bool TheoryArithPrivate::outputTrustedLemma(TrustNode lemma, InferenceId id)
 {
   Debug("arith::channel") << "Arith trusted lemma: " << lemma << std::endl;
-  d_containing.d_im.trustedLemma(lemma, id);
+  return d_containing.d_im.trustedLemma(lemma, id);
 }
 
-void TheoryArithPrivate::outputLemma(TNode lem, InferenceId id) {
+bool TheoryArithPrivate::outputLemma(TNode lem, InferenceId id) {
   Debug("arith::channel") << "Arith lemma: " << lem << std::endl;
-  d_containing.d_im.lemma(lem, id);
+  return d_containing.d_im.lemma(lem, id);
 }
 
 void TheoryArithPrivate::outputTrustedConflict(TrustNode conf, InferenceId id)
@@ -3391,11 +3391,13 @@ bool TheoryArithPrivate::postCheck(Theory::Effort effortLevel)
       if(getDioCuttingResource()){
         TrustNode possibleLemma = dioCutting();
         if(!possibleLemma.isNull()){
-          emmittedConflictOrSplit = true;
           d_hasDoneWorkSinceCut = false;
           d_cutCount = d_cutCount + 1;
           Debug("arith::lemma") << "dio cut   " << possibleLemma << endl;
-          outputTrustedLemma(possibleLemma, InferenceId::ARITH_DIO_CUT);
+          if (outputTrustedLemma(possibleLemma, InferenceId::ARITH_DIO_CUT))
+          {
+            emmittedConflictOrSplit = true;
+          }
         }
       }
     }
@@ -3406,10 +3408,12 @@ bool TheoryArithPrivate::postCheck(Theory::Effort effortLevel)
       {
         ++(d_statistics.d_externalBranchAndBounds);
         d_cutCount = d_cutCount + 1;
-        emmittedConflictOrSplit = true;
         Debug("arith::lemma") << "rrbranch lemma"
                               << possibleLemma << endl;
-        outputTrustedLemma(possibleLemma, InferenceId::ARITH_BB_LEMMA);
+        if (outputTrustedLemma(possibleLemma, InferenceId::ARITH_BB_LEMMA))
+        {
+          emmittedConflictOrSplit = true;
+        }
       }
     }
 
diff --git a/src/theory/arith/theory_arith_private.h b/src/theory/arith/theory_arith_private.h
index b25fa4f69..dc3c8bbb8 100644
--- a/src/theory/arith/theory_arith_private.h
+++ b/src/theory/arith/theory_arith_private.h
@@ -695,8 +695,8 @@ private:
   inline TheoryId theoryOf(TNode x) const { return d_containing.theoryOf(x); }
   inline void debugPrintFacts() const { d_containing.debugPrintFacts(); }
   inline context::Context* getSatContext() const { return d_containing.getSatContext(); }
-  void outputTrustedLemma(TrustNode lem, InferenceId id);
-  void outputLemma(TNode lem, InferenceId id);
+  bool outputTrustedLemma(TrustNode lem, InferenceId id);
+  bool outputLemma(TNode lem, InferenceId id);
   void outputTrustedConflict(TrustNode conf, InferenceId id);
   void outputConflict(TNode lit, InferenceId id);
   void outputPropagate(TNode lit);
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 45b695cd9..24eee5998 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1768,6 +1768,7 @@ set(regress_1_tests
   regress1/push-pop/fuzz_7.smt2
   regress1/push-pop/fuzz_8.smt2
   regress1/push-pop/fuzz_9.smt2
+  regress1/push-pop/issue6773-arith-no-check.smt2
   regress1/push-pop/model-unsound-ania.smt2
   regress1/push-pop/quant-fun-proc-unmacro.smt2
   regress1/push-pop/quant-fun-proc.smt2
diff --git a/test/regress/regress1/push-pop/issue6773-arith-no-check.smt2 b/test/regress/regress1/push-pop/issue6773-arith-no-check.smt2
new file mode 100644
index 000000000..3c9063af2
--- /dev/null
+++ b/test/regress/regress1/push-pop/issue6773-arith-no-check.smt2
@@ -0,0 +1,13 @@
+; COMMAND-LINE: -i
+; EXPECT: sat
+; EXPECT: sat
+(set-logic NIA)
+(declare-fun i3 () Int)
+(declare-fun i9 () Int)
+(push)
+(assert (>= (- 1 1 i3 i9 1) i3))
+(check-sat)
+(pop)
+(assert (or (= 0 i9) (< i3 0)))
+(assert (= 1 (* i9 i9)))
+(check-sat)