From d5141e4086898bb66809c76d4614503e3a2efd6e Mon Sep 17 00:00:00 2001
From: Alex Ozdemir <aozdemir@hmc.edu>
Date: Mon, 27 Jul 2020 10:20:07 -0700
Subject: [PATCH] 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>
---
 src/theory/arith/constraint.cpp           | 25 ++++++++++++-----------
 src/theory/arith/constraint.h             |  5 +++++
 src/theory/arith/theory_arith_private.cpp |  3 ++-
 test/regress/CMakeLists.txt               |  1 +
 test/regress/regress3/issue4714.smt2      | 12 +++++++++++
 5 files changed, 33 insertions(+), 13 deletions(-)
 create mode 100644 test/regress/regress3/issue4714.smt2

diff --git a/src/theory/arith/constraint.cpp b/src/theory/arith/constraint.cpp
index abfaca954..6a04e70d1 100644
--- 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 873b33ced..b32616a04 100644
--- 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 39a3a6558..cdf3c16c7 100644
--- 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 8118d8d79..a3dbd847a 100644
--- 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
index 000000000..ee3e59a32
--- /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)
-- 
2.30.2