[Mlir-commits] [mlir] [MLIR][FPL] Fix dark shadow of Fourier-Motzkin (PR #217581)

[llvmlistbot at llvm.org]

llvmorg-github-actions[bot] wrote:


<!--LLVM PR SUMMARY COMMENT-->

@llvm/pr-subscribers-mlir

Author: Yue Huang (AdUhTkJm)

<details>
<summary>Changes</summary>

Currently, the Omega test is of the opposite sign.

Suppose we are eliminating `x`. For `ax >= l` and `bx <= u` (a, b positive), the Omega test says that if `au - bl >= (a-1)(b-1)` then there must be an integer solution. But in FPL it actually generates `au - bl + (a-1)(b-1) >= 0`, which is the opposite.

This PR fixes it.

---
Full diff: https://github.com/llvm/llvm-project/pull/217581.diff


2 Files Affected:

- (modified) mlir/lib/Analysis/Presburger/IntegerRelation.cpp (+1-1) 
- (modified) mlir/unittests/Analysis/Presburger/IntegerRelationTest.cpp (+32) 


``````````diff
diff --git a/mlir/lib/Analysis/Presburger/IntegerRelation.cpp b/mlir/lib/Analysis/Presburger/IntegerRelation.cpp
index 94a15dc3f8663..5191c0cbaecc7 100644
--- a/mlir/lib/Analysis/Presburger/IntegerRelation.cpp
+++ b/mlir/lib/Analysis/Presburger/IntegerRelation.cpp
@@ -2124,7 +2124,7 @@ void IntegerRelation::fourierMotzkinEliminate(unsigned pos, bool darkShadow,
       if (darkShadow) {
         // The dark shadow is a convex subset of the exact integer shadow. If
         // there is a point here, it proves the existence of a solution.
-        ineq[ineq.size() - 1] += lbCoeff * ubCoeff - lbCoeff - ubCoeff + 1;
+        ineq[ineq.size() - 1] -= lbCoeff * ubCoeff - lbCoeff - ubCoeff + 1;
       }
       // TODO: we need to have a way to add inequalities in-place in
       // IntegerRelation instead of creating and copying over.
diff --git a/mlir/unittests/Analysis/Presburger/IntegerRelationTest.cpp b/mlir/unittests/Analysis/Presburger/IntegerRelationTest.cpp
index c3da1c1556d26..08c37798f5f47 100644
--- a/mlir/unittests/Analysis/Presburger/IntegerRelationTest.cpp
+++ b/mlir/unittests/Analysis/Presburger/IntegerRelationTest.cpp
@@ -777,3 +777,35 @@ TEST(IntegerRelationTest, isFullDim) {
   rel = parseRelationFromSet("(x): (-1 >= 0)", 1);
   EXPECT_FALSE(rel.isFullDim());
 }
+
+namespace {
+/// Exposes the protected Fourier-Motzkin elimination so that the dark shadow
+/// variant can be tested.
+class DarkShadowTestRelation : public IntegerRelation {
+public:
+  DarkShadowTestRelation(const IntegerRelation &rel) : IntegerRelation(rel) {}
+  using IntegerRelation::fourierMotzkinEliminate;
+};
+} // namespace
+
+TEST(IntegerRelationTest, fourierMotzkinDarkShadow) {
+  // The dark shadow is a convex integer subset of the exact integer shadow.
+  //
+  // Consider the relation 2*i == j + 1, i.e. j + 1 <= 2i <= j + 1.
+  // Eliminating i, the rational shadow is the entire j-line, but the exact
+  // integer shadow is "j is odd".
+  IntegerRelation parsed =
+      parseRelationFromSet("(j, i) : (2*i - j - 1 >= 0, -2*i + j + 1 >= 0)", 2);
+
+  // The rational shadow should contain j = 0.
+  DarkShadowTestRelation rationalShadow = parsed;
+  rationalShadow.fourierMotzkinEliminate(/*pos=*/1, /*darkShadow=*/false);
+  rationalShadow.addEquality({1, 0});
+  EXPECT_FALSE(rationalShadow.isIntegerEmpty());
+
+  // The dark shadow must not contain j = 0.
+  DarkShadowTestRelation darkShadow = parsed;
+  darkShadow.fourierMotzkinEliminate(/*pos=*/1, /*darkShadow=*/true);
+  darkShadow.addEquality({1, 0});
+  EXPECT_TRUE(darkShadow.isIntegerEmpty());
+}

``````````

</details>


https://github.com/llvm/llvm-project/pull/217581