From 53a07d0331d71656904a7333b5ed0c835d7d4c38 Mon Sep 17 00:00:00 2001
From: Alex Ozdemir <aozdemir@hmc.edu>
Date: Wed, 4 Mar 2020 00:20:10 -0800
Subject: [PATCH] Expand the definition of a "simple" farkas proof.

Before, a "simple farkas proof" was one that just applied the farkas
lemma.

Now it allows for the antecedents to (optionally) be tightened.

Note that hasSimpleFarkasProof was (and is) dead code.

We will use it to decide whether to print a proof or a hole.
---
 src/theory/arith/constraint.cpp | 36 ++++++++++++++++++++++++---------
 src/theory/arith/constraint.h   |  9 +++++----
 2 files changed, 32 insertions(+), 13 deletions(-)

diff --git a/src/theory/arith/constraint.cpp b/src/theory/arith/constraint.cpp
index 56703c12a..98ce07fbc 100644
--- a/src/theory/arith/constraint.cpp
+++ b/src/theory/arith/constraint.cpp
@@ -500,21 +500,39 @@ bool Constraint::hasSimpleFarkasProof() const
                                << std::endl;
     return false;
   }
-  const ConstraintRule& rule = getConstraintRule();
-  AntecedentId antId = rule.d_antecedentEnd;
-  ConstraintCP antecdent = d_database->getAntecedent(antId);
-  while (antecdent != NullConstraint)
+
+  // For each antecdent ...
+  for (AntecedentId i = getConstraintRule().d_antecedentEnd;
+       i != AntecedentIdSentinel;
+       --i)
   {
-    if (antecdent->getProofType() != AssumeAP)
+    ConstraintCP 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())
+
+    {
+      continue;
+    }
+
+    // ... otherwise, we do not have a simple Farkas proof.
+    if (Debug.isOn("constraints::hsfp"))
     {
       Debug("constraints::hsfp") << "There is no simple Farkas proof b/c there "
                                     "is an antecdent w/ rule ";
-      antecdent->getConstraintRule().print(Debug("constraints::hsfp"));
+      a->getConstraintRule().print(Debug("constraints::hsfp"));
       Debug("constraints::hsfp") << std::endl;
-      return false;
     }
-    --antId;
-    antecdent = d_database->getAntecedent(antId);
+
+    return false;
   }
   return true;
 }
diff --git a/src/theory/arith/constraint.h b/src/theory/arith/constraint.h
index 225bf555e..17b4fa4e3 100644
--- a/src/theory/arith/constraint.h
+++ b/src/theory/arith/constraint.h
@@ -496,15 +496,16 @@ class Constraint {
 
   /**
    * @brief Returns whether this constraint is provable using a Farkas
-   * proof that has input assertions as its antecedents.
+   * proof applied to (possibly tightened) input assertions.
    *
    * An example of a constraint that has a simple Farkas proof:
    *    x <= 0 proven from x + y <= 0 and x - y <= 0.
    *
-   * An example of a constraint that does not have a simple Farkas proof:
+   * An example of another constraint that has a simple Farkas proof:
    *    x <= 0 proven from x + y <= 0 and x - y <= 0.5 for integers x, y
-   *       (since integer reasoning is also required!).
-   * Another example of a constraint that might be proven without a simple
+   *       (integer bound-tightening is applied first!).
+   *
+   * An example of a constraint that might be proven **without** a simple
    * Farkas proof:
    *    x < 0 proven from not(x == 0) and not(x > 0).
    *
-- 
2.30.2