Expand the definition of a "simple" farkas proof.
authorAlex Ozdemir <aozdemir@hmc.edu>
Wed, 4 Mar 2020 08:20:10 +0000 (00:20 -0800)
committerAlex Ozdemir <aozdemir@hmc.edu>
Mon, 16 Mar 2020 23:52:50 +0000 (16:52 -0700)
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
src/theory/arith/constraint.h

index 56703c12a16c43d3ea418f0538e057490fbcc860..98ce07fbc6d06a12585876fce01b4b4dfc65ac91 100644 (file)
@@ -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;
 }
index 225bf555e1e12ae6dfe0c98c71e6b92666f0616e..17b4fa4e3c2ff1a61aa71bf595918477b398b0e8 100644 (file)
@@ -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).
    *