[llvm-branch-commits] [mlir] 9f32f1d - [MLIR] Support checking if two FlatAffineConstraints are equal

2021-01-18 Thread Arjun P via llvm-branch-commits

Author: Arjun P
Date: 2021-01-18T21:46:01+05:30
New Revision: 9f32f1d6fbfa4f4d654876e29c1c2b84e18b1a2e

URL: 
https://github.com/llvm/llvm-project/commit/9f32f1d6fbfa4f4d654876e29c1c2b84e18b1a2e
DIFF: 
https://github.com/llvm/llvm-project/commit/9f32f1d6fbfa4f4d654876e29c1c2b84e18b1a2e.diff

LOG: [MLIR] Support checking if two FlatAffineConstraints are equal

This patch adds support for checking if two PresburgerSets are equal. In 
particular, one can check if two FlatAffineConstraints are equal by 
constructing PrebsurgerSets from them and comparing these.

Reviewed By: ftynse

Differential Revision: https://reviews.llvm.org/D94915

Added: 


Modified: 
mlir/include/mlir/Analysis/PresburgerSet.h
mlir/lib/Analysis/PresburgerSet.cpp
mlir/unittests/Analysis/PresburgerSetTest.cpp

Removed: 




diff  --git a/mlir/include/mlir/Analysis/PresburgerSet.h 
b/mlir/include/mlir/Analysis/PresburgerSet.h
index 1f3a10a8a624..4970adf0f42b 100644
--- a/mlir/include/mlir/Analysis/PresburgerSet.h
+++ b/mlir/include/mlir/Analysis/PresburgerSet.h
@@ -60,7 +60,7 @@ class PresburgerSet {
   /// Return the intersection of this set and the given set.
   PresburgerSet intersect(const PresburgerSet &set) const;
 
-  /// Return true if the set contains the given point, or false otherwise.
+  /// Return true if the set contains the given point, and false otherwise.
   bool containsPoint(ArrayRef point) const;
 
   /// Print the set's internal state.
@@ -74,6 +74,9 @@ class PresburgerSet {
   /// return `this \ set`.
   PresburgerSet subtract(const PresburgerSet &set) const;
 
+  /// Return true if this set is equal to the given set, and false otherwise.
+  bool isEqual(const PresburgerSet &set) const;
+
   /// Return a universe set of the specified type that contains all points.
   static PresburgerSet getUniverse(unsigned nDim = 0, unsigned nSym = 0);
   /// Return an empty set of the specified type that contains no points.

diff  --git a/mlir/lib/Analysis/PresburgerSet.cpp 
b/mlir/lib/Analysis/PresburgerSet.cpp
index 323dc3e56d54..12df06b7221e 100644
--- a/mlir/lib/Analysis/PresburgerSet.cpp
+++ b/mlir/lib/Analysis/PresburgerSet.cpp
@@ -281,6 +281,22 @@ PresburgerSet PresburgerSet::subtract(const PresburgerSet 
&set) const {
   return result;
 }
 
+/// Two sets S and T are equal iff S contains T and T contains S.
+/// By "S contains T", we mean that S is a superset of or equal to T.
+///
+/// S contains T iff T \ S is empty, since if T \ S contains a
+/// point then this is a point that is contained in T but not S.
+///
+/// Therefore, S is equal to T iff S \ T and T \ S are both empty.
+bool PresburgerSet::isEqual(const PresburgerSet &set) const {
+  assertDimensionsCompatible(set, *this);
+  PresburgerSet thisMinusSet = subtract(set);
+  if (!thisMinusSet.isIntegerEmpty())
+return false;
+  PresburgerSet setMinusThis = set.subtract(*this);
+  return setMinusThis.isIntegerEmpty();
+}
+
 /// Return true if all the sets in the union are known to be integer empty,
 /// false otherwise.
 bool PresburgerSet::isIntegerEmpty() const {

diff  --git a/mlir/unittests/Analysis/PresburgerSetTest.cpp 
b/mlir/unittests/Analysis/PresburgerSetTest.cpp
index 99a0e8622232..20c56274b9be 100644
--- a/mlir/unittests/Analysis/PresburgerSetTest.cpp
+++ b/mlir/unittests/Analysis/PresburgerSetTest.cpp
@@ -6,10 +6,11 @@
 //
 
//===--===//
 //
-// This file contains tests for PresburgerSet. Each test works by computing
-// an operation (union, intersection, subtract, or complement) on two sets
-// and checking, for a set of points, that the resulting set contains the point
-// iff the result is supposed to contain it.
+// This file contains tests for PresburgerSet. The tests for union,
+// intersection, subtract, and complement work by computing the operation on
+// two sets and checking, for a set of points, that the resulting set contains
+// the point iff the result is supposed to contain it. The test for isEqual 
just
+// checks if the result for two sets matches the expected result.
 //
 
//===--===//
 
@@ -34,7 +35,7 @@ static void testUnionAtPoints(PresburgerSet s, PresburgerSet 
t,
 }
 
 /// Compute the intersection of s and t, and check that each of the given 
points
-/// belongs to the intersection iff it belongs to both of s and t.
+/// belongs to the intersection iff it belongs to both s and t.
 static void testIntersectAtPoints(PresburgerSet s, PresburgerSet t,
   ArrayRef> points) {
   PresburgerSet intersection = s.intersect(t);
@@ -521,4 +522,73 @@ TEST(SetTest, Complement) {
{1, 10}});
 }
 
+TEST(SetTest, isEqual) {
+  // set = [2, 8] U [10, 20].
+  PresburgerSet universe = PresburgerSet::getUniverse(1);
+  PresburgerSet emptySet = PresburgerSet::getEmptySet(1);
+

[llvm-branch-commits] [mlir] fa9851e - [MLIR] NFC: simplify PresburgerSet::isEqual

2021-01-18 Thread Arjun P via llvm-branch-commits

Author: Arjun P
Date: 2021-01-18T22:47:25+05:30
New Revision: fa9851ebfee48014a1c48a7e7d625d9ecff3ebad

URL: 
https://github.com/llvm/llvm-project/commit/fa9851ebfee48014a1c48a7e7d625d9ecff3ebad
DIFF: 
https://github.com/llvm/llvm-project/commit/fa9851ebfee48014a1c48a7e7d625d9ecff3ebad.diff

LOG: [MLIR] NFC: simplify PresburgerSet::isEqual

Reviewed By: ftynse

Differential Revision: https://reviews.llvm.org/D94918

Added: 


Modified: 
mlir/lib/Analysis/PresburgerSet.cpp

Removed: 




diff  --git a/mlir/lib/Analysis/PresburgerSet.cpp 
b/mlir/lib/Analysis/PresburgerSet.cpp
index 12df06b7221e..051010e09861 100644
--- a/mlir/lib/Analysis/PresburgerSet.cpp
+++ b/mlir/lib/Analysis/PresburgerSet.cpp
@@ -290,11 +290,8 @@ PresburgerSet PresburgerSet::subtract(const PresburgerSet 
&set) const {
 /// Therefore, S is equal to T iff S \ T and T \ S are both empty.
 bool PresburgerSet::isEqual(const PresburgerSet &set) const {
   assertDimensionsCompatible(set, *this);
-  PresburgerSet thisMinusSet = subtract(set);
-  if (!thisMinusSet.isIntegerEmpty())
-return false;
-  PresburgerSet setMinusThis = set.subtract(*this);
-  return setMinusThis.isIntegerEmpty();
+  return this->subtract(set).isIntegerEmpty() &&
+ set.subtract(*this).isIntegerEmpty();
 }
 
 /// Return true if all the sets in the union are known to be integer empty,



___
llvm-branch-commits mailing list
llvm-branch-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/llvm-branch-commits


[llvm-branch-commits] [mlir] 14056df - [MLIR] Add support for extracting an integer sample point (if one exists) from an unbounded FlatAffineConstraints.

2021-01-22 Thread Arjun P via llvm-branch-commits

Author: Arjun P
Date: 2021-01-22T22:28:38+05:30
New Revision: 14056dfb4dc7b289fbd12c3bc82f68485bf9377c

URL: 
https://github.com/llvm/llvm-project/commit/14056dfb4dc7b289fbd12c3bc82f68485bf9377c
DIFF: 
https://github.com/llvm/llvm-project/commit/14056dfb4dc7b289fbd12c3bc82f68485bf9377c.diff

LOG: [MLIR] Add support for extracting an integer sample point (if one exists) 
from an unbounded FlatAffineConstraints.

With this, we have complete support for finding integer sample points in 
FlatAffineConstraints.

Reviewed By: ftynse

Differential Revision: https://reviews.llvm.org/D95047

Added: 


Modified: 
mlir/include/mlir/Analysis/AffineStructures.h
mlir/include/mlir/Analysis/LinearTransform.h
mlir/include/mlir/Analysis/Presburger/Simplex.h
mlir/lib/Analysis/AffineStructures.cpp
mlir/lib/Analysis/LinearTransform.cpp
mlir/lib/Analysis/Presburger/Simplex.cpp
mlir/unittests/Analysis/AffineStructuresTest.cpp
mlir/unittests/Analysis/LinearTransformTest.cpp

Removed: 




diff  --git a/mlir/include/mlir/Analysis/AffineStructures.h 
b/mlir/include/mlir/Analysis/AffineStructures.h
index fa80db7d4b63..fa42db500684 100644
--- a/mlir/include/mlir/Analysis/AffineStructures.h
+++ b/mlir/include/mlir/Analysis/AffineStructures.h
@@ -147,11 +147,8 @@ class FlatAffineConstraints {
   /// returns true, no integer solution to the equality constraints can exist.
   bool isEmptyByGCDTest() const;
 
-  /// Runs the GCD test heuristic. If it proves inconclusive, falls back to
-  /// generalized basis reduction if the set is bounded.
-  ///
   /// Returns true if the set of constraints is found to have no solution,
-  /// false if a solution exists or all tests were inconclusive.
+  /// false if a solution exists. Uses the same algorithm as findIntegerSample.
   bool isIntegerEmpty() const;
 
   // Returns a matrix where each row is a vector along which the polytope is
@@ -160,11 +157,12 @@ class FlatAffineConstraints {
   // independent. This function should not be called on empty sets.
   Matrix getBoundedDirections() const;
 
-  /// Find a sample point satisfying the constraints. This uses a branch and
-  /// bound algorithm with generalized basis reduction, which always works if
-  /// the set is bounded. This should not be called for unbounded sets.
+  /// Find an integer sample point satisfying the constraints using a
+  /// branch and bound algorithm with generalized basis reduction, with some
+  /// additional processing using Simplex for unbounded sets.
   ///
-  /// Returns such a point if one exists, or an empty Optional otherwise.
+  /// Returns an integer sample point if one exists, or an empty Optional
+  /// otherwise.
   Optional> findIntegerSample() const;
 
   /// Returns true if the given point satisfies the constraints, or false
@@ -387,8 +385,9 @@ class FlatAffineConstraints {
   /// Changes all symbol identifiers which are loop IVs to dim identifiers.
   void convertLoopIVSymbolsToDims();
 
-  /// Sets the specified identifier to a constant and removes it.
-  void setAndEliminate(unsigned pos, int64_t constVal);
+  /// Sets the values.size() identifiers starting at pos to the specified 
values
+  /// and removes them.
+  void setAndEliminate(unsigned pos, ArrayRef values);
 
   /// Tries to fold the specified identifier to a constant using a trivial
   /// equality detection; if successful, the constant is substituted for the

diff  --git a/mlir/include/mlir/Analysis/LinearTransform.h 
b/mlir/include/mlir/Analysis/LinearTransform.h
index 0850f5a00609..2f3aaf800ab0 100644
--- a/mlir/include/mlir/Analysis/LinearTransform.h
+++ b/mlir/include/mlir/Analysis/LinearTransform.h
@@ -35,10 +35,15 @@ class LinearTransform {
 
   // Returns a FlatAffineConstraints having a constraint vector vT for every
   // constraint vector v in fac, where T is this transform.
-  FlatAffineConstraints applyTo(const FlatAffineConstraints &fac);
+  FlatAffineConstraints applyTo(const FlatAffineConstraints &fac) const;
 
-  // Post-multiply the given vector v with this transform, say T, returning vT.
-  SmallVector applyTo(ArrayRef v);
+  // The given vector is interpreted as a row vector v. Post-multiply v with
+  // this transform, say T, and return vT.
+  SmallVector postMultiplyRow(ArrayRef rowVec) const;
+
+  // The given vector is interpreted as a column vector v. Pre-multiply v with
+  // this transform, say T, and return Tv.
+  SmallVector preMultiplyColumn(ArrayRef colVec) const;
 
 private:
   Matrix matrix;

diff  --git a/mlir/include/mlir/Analysis/Presburger/Simplex.h 
b/mlir/include/mlir/Analysis/Presburger/Simplex.h
index 370035cbc7ba..d64b86d11dec 100644
--- a/mlir/include/mlir/Analysis/Presburger/Simplex.h
+++ b/mlir/include/mlir/Analysis/Presburger/Simplex.h
@@ -218,7 +218,11 @@ class Simplex {
   /// tableau A and one in B.
   static Simplex makeProduct(const Simplex &a, const Simplex &b);
 
-  /// R