[Mlir-commits] [mlir] [MLIR][Presburger] Helper functions to compute the constant term of a generating function (PR #77819)

[Arjun P]

================
@@ -144,3 +145,106 @@ GeneratingFunction mlir::presburger::detail::unimodularConeGeneratingFunction(
                             std::vector({numerator}),
                             std::vector({denominator}));
 }
+
+/// We use an iterative procedure to find a vector not orthogonal
+/// to a given set, ignoring the null vectors.
+/// Let the inputs be {x_1, ..., x_k}, all vectors of length n.
+///
+/// In the following,
+/// vs[:i] means the elements of vs up to and including the i'th one,
+/// <vs, us> means the dot product of vs and us,
+/// vs ++ [v] means the vector vs with the new element v appended to it.
+///
+/// We proceed iteratively; for steps d = 0, ... n-1, we construct a vector
+/// which is not orthogonal to any of {x_1[:i], ..., x_n[:i]}, ignoring
+/// the null vectors.
+/// At step d = 0, we let vs = [1]. Clearly this is not orthogonal to
+/// any vector in the set {x_1[0], ..., x_n[0]}, except the null ones,
+/// which we ignore.
+/// At step d = t + 1, we need a number v
+/// s.t. <x_i[:t+1], vs++[v]> != 0 for all i.
+/// => <x_i[:t], vs> + x_i[t+1]*v != 0
+/// => v != - <x_i[:t], vs> / x_i[t+1]
----------------
Superty wrote:

personally I would just use `d` and `d - 1` again instead of introducing a new `t + 1` and `t`

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