[PATCH] D80860: Exact integer emptiness checks for FlatAffineConstraints

Mon Jun 22 06:25:02 PDT 2020

ftynse accepted this revision.
ftynse added a comment.

Thanks for providing more detailed documentation!

I did not extensively analyze the algorithms. At a glance, the implementation looks plausible. Again, given the complexity, I would encourage you to get 100% test coverage on the core functions. Another way to stress-test this would be to generate a bunch of arbitrary sets and run this + gcd emptiness checks and analyze the differences manually to make sure they only happen when gcd is not supposed to be correct.

I don't have any further comments.

@andydavis1 had a bug which might have been related to integer exactness, but I don't know if it is still active.

================
Comment at: mlir/include/mlir/Analysis/Presburger/Simplex.h:37
+/// set is empty if no solution exists. Currently, this only works for bounded
+/// sets. SImplex can also be constructed from a FlatAffineConstraints object.
+///
----------------
Nit: SImplex -> simplex

================
Comment at: mlir/include/mlir/Analysis/Presburger/Simplex.h:45
+/// We define variables, constraints, and unknowns. Consider the example of a
+/// two-dimensional set defined by 1 + 2x + 3y >= 0 and 2x - 3z >= 0. Here,
+/// x, y, are variables while 1 + 2x + 3y >= 0, 2x - 3y >= 0 are
----------------
Nit: 2x - 3y >= 0  (currently uses `z`)

Repository:
  rG LLVM Github Monorepo

CHANGES SINCE LAST ACTION
  https://reviews.llvm.org/D80860/new/

https://reviews.llvm.org/D80860