Consider negation's proof before triggering arith pfs. (#4776)

The current arith proof machinery can prove conflicts which are
explained by assumptions and tightened assumptions.

Previously we verified that the conflict constraint was explained in
terms of assumptions and tightened assumptions, before trying to
save/produce a proof.

We did not verify that the negated constraint was an assumption or
tightened assumption.

This caused us to attempt to prove conflicts around constraints whose
negations where proven by general means (in the case of #4714, by the
equality engine), which the proof machinery was not prepared to handle.

This PR also checks that the negate constraint is an assumption or
tightened assumption, before saving the proof.

Thanks, Gereon, for doing the initial investigation into this!

fixes 4714

Co-authored-by: Gereon Kremer <nafur42@gmail.com>

diff --git a/src/theory/arith/constraint.cpp b/src/theory/arith/constraint.cpp
index abfaca954478bce8a3f4b10d7c6596e5a797a2ba..6a04e70d1c847a83230578359802adfd5d85636e 100644 (file)
--- a/src/theory/arith/constraint.cpp
+++ b/src/theory/arith/constraint.cpp
@@ -506,18 +506,8 @@ bool Constraint::hasSimpleFarkasProof() const
   for (ConstraintCP a = d_database->getAntecedent(i); a != NullConstraint;
        a = d_database->getAntecedent(--i))
   {
-    // ... that antecdent must be an assumption ...
-    if (a->isAssumption())
-    {
-      continue;
-    }
-
-    // ... OR a tightened assumption ...
-    if (a->hasIntTightenProof()
-        && a->getConstraintRule().d_antecedentEnd != AntecedentIdSentinel
-        && d_database->getAntecedent(a->getConstraintRule().d_antecedentEnd)
-               ->isAssumption())
-
+    // ... that antecdent must be an assumption OR a tightened assumption ...
+    if (a->isPossiblyTightenedAssumption())
     {
       continue;
     }
@@ -536,6 +526,17 @@ bool Constraint::hasSimpleFarkasProof() const
   return true;
 }
 
+bool Constraint::isPossiblyTightenedAssumption() const
+{
+  // ... that antecdent must be an assumption ...
+
+  if (isAssumption()) return true;
+  if (!hasIntTightenProof()) return false;
+  if (getConstraintRule().d_antecedentEnd == AntecedentIdSentinel) return false;
+  return d_database->getAntecedent(getConstraintRule().d_antecedentEnd)
+      ->isAssumption();
+}
+
 bool Constraint::hasIntTightenProof() const {
   return getProofType() == IntTightenAP;
 }

diff --git a/src/theory/arith/constraint.h b/src/theory/arith/constraint.h
index 873b33ced7e51654f993c831cbf654bb5493b852..b32616a04414f95ba86f20c810793c399972fdc8 100644 (file)
--- a/src/theory/arith/constraint.h
+++ b/src/theory/arith/constraint.h
@@ -514,6 +514,11 @@ class Constraint {
    *
    */
   bool hasSimpleFarkasProof() const;
+  /**
+   * Returns whether this constraint is an assumption or a tightened
+   * assumption.
+   */
+  bool isPossiblyTightenedAssumption() const;
 
   /** Returns true if the node has a int bound tightening proof. */
   bool hasIntTightenProof() const;

diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index 39a3a655840718a2a22ca0b19a875a0368bceca5..cdf3c16c7672acf00a830225f99db39cd310f5ef 100644 (file)
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -1933,7 +1933,8 @@ void TheoryArithPrivate::outputConflicts(){
         }
 
         Assert(conflict.getNumChildren() == pf.d_farkasCoefficients->size());
-        if (confConstraint->hasSimpleFarkasProof())
+        if (confConstraint->hasSimpleFarkasProof()
+            && confConstraint->getNegation()->isPossiblyTightenedAssumption())
         {
           d_containing.d_proofRecorder->saveFarkasCoefficients(
               conflictInFarkasCoefficientOrder, pf.d_farkasCoefficients);

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 8118d8d79fe202e7db29e566af4b8f53f0c4b242..a3dbd847a947e45ef816ace07ddef06a6f8d4afb 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -2167,6 +2167,7 @@ set(regress_3_tests
   regress3/incorrect1.smtv1.smt2
   regress3/issue2429.smt2
   regress3/issue4170.smt2
+  regress3/issue4714.smt2
   regress3/pp-regfile.smtv1.smt2
   regress3/qwh.35.405.shuffled-as.sat03-1651.smtv1.smt2
   regress3/siegel-nl-bases.smt2

diff --git a/test/regress/regress3/issue4714.smt2 b/test/regress/regress3/issue4714.smt2
new file mode 100644 (file)
index 0000000..ee3e59a
--- /dev/null
+++ b/test/regress/regress3/issue4714.smt2
@@ -0,0 +1,12 @@
+; COMMAND-LINE: --check-models
+; EXPECT: unknown
+(set-logic UFNIRA)
+(declare-fun c (Int) Int)
+(define-fun d ((k Int)) Int (- (c k) 10))
+(define-fun j ((k Int) (e Int)) Bool (<= 0 e (d k)))
+(define-fun f ((k Int) (a Int) (b Int)) Int (ite (= b 1) a (mod a b)))
+(define-fun g ((k Int) (a Int) (b Int)) Int (f k (* a (c b)) (c k)))
+(define-fun h ((k Int) (a Int) (b Int)) Int (f k (+ a b) (c k)))
+(assert (= (c 0) 1))
+(assert (exists ((l Int) (k Int)) (and (j k l) (distinct (g k (h k l (g k l l)) l) (g k (h k l 0) l)))))
+(check-sat)