From: Alex Ozdemir <aozdemir@hmc.edu>
Date: Wed, 4 Mar 2020 08:20:10 +0000 (-0800)
Subject: Expand the definition of a "simple" farkas proof.
X-Git-Tag: cvc5-1.0.0~3487
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=53a07d0331d71656904a7333b5ed0c835d7d4c38;p=cvc5.git

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.
---

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).
    *