diff --git a/mlir/lib/Analysis/Presburger/Utils.cpp b/mlir/lib/Analysis/Presburger/Utils.cpp --- a/mlir/lib/Analysis/Presburger/Utils.cpp +++ b/mlir/lib/Analysis/Presburger/Utils.cpp @@ -40,6 +40,9 @@ return; } + // `gcd` may be negative and hence made positive. + gcd = std::abs(gcd); + // Normalize the dividend and the denominator. std::transform(dividend.begin(), dividend.end(), dividend.begin(), [gcd](int64_t &n) { return floor(n / gcd); }); diff --git a/mlir/unittests/Analysis/Presburger/IntegerPolyhedronTest.cpp b/mlir/unittests/Analysis/Presburger/IntegerPolyhedronTest.cpp --- a/mlir/unittests/Analysis/Presburger/IntegerPolyhedronTest.cpp +++ b/mlir/unittests/Analysis/Presburger/IntegerPolyhedronTest.cpp @@ -969,4 +969,28 @@ } } +TEST(IntegerPolyhedronTest, negativeDividends) { + // (x) : (exists y = [-x + 1 / 2], z = [-x - 2 / 3]: y + z >= x). + IntegerPolyhedron poly1(1); + poly1.addLocalFloorDiv({-1, 1}, 2); // y = [x + 1 / 2]. + // Normalization test with negative dividends + poly1.addLocalFloorDiv({-3, 0, -6}, 9); // z = [3x + 6 / 9] -> [x + 2 / 3]. + poly1.addInequality({-1, 1, 1, 0}); // y + z >= x. + + // (x) : (exists y = [x + 1 / 3], z = [x + 2 / 3]: y + z <= x). + IntegerPolyhedron poly2(1); + // Normalization test. + poly2.addLocalFloorDiv({-2, 2}, 4); // y = [-2x + 2 / 4] -> [-x + 1 / 2]. + poly2.addLocalFloorDiv({-1, 0, -2}, 3); // z = [-x - 2 / 3]. + poly2.addInequality({1, -1, -1, 0}); // y + z <= x. + + poly1.mergeLocalIds(poly2); + + // Merging triggers normalization. + std::vector> divisions = {{-1, 0, 0, 1}, + {-1, 0, 0, -2}}; + SmallVector denoms = {2, 3}; + checkDivisionRepresentation(poly1, divisions, denoms); +} + } // namespace mlir