[Mlir-commits] [mlir] [MLIR][Presburger] Helper functions to compute the constant term of a generating function (PR #77819)
Arjun P
llvmlistbot at llvm.org
Fri Jan 12 11:10:34 PST 2024
================
@@ -144,3 +145,110 @@ GeneratingFunction mlir::presburger::detail::unimodularConeGeneratingFunction(
std::vector({numerator}),
std::vector({denominator}));
}
+
+/// We use a recursive 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 (not 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 i = 2, ... n, we construct a vector
+/// which is not orthogonal to any of {x_1[:i], ..., x_n[:i]}, ignoring
+/// the null vectors.
+/// At step i = 2, 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 i = k + 1, we need a number v
+/// s.t. <x_i[:k+1], vs++[v]> != 0 for all i.
+/// => <x_i[:k], vs> + x_i[k]*v != 0
+/// => v != - <x_i[:k], vs> / x_i[k]
+/// We compute this value for all x_i, and then
+/// set v to be the maximum element of this set plus one. Thus
+/// v is outside the set as desired, and we append it to vs
+/// to obtain the result of the k+1'th step.
+///
+/// The base case is given in one dimension,
+/// where the vector [1] is not orthogonal to any
+/// of the input vectors (since they are all nonzero).
+Point mlir::presburger::detail::getNonOrthogonalVector(
+ std::vector<Point> vectors) {
+ unsigned dim = vectors[0].size();
+
+ SmallVector<Fraction> newPoint = {Fraction(1, 1)};
+ std::vector<Fraction> lowerDimDotProducts;
+ Fraction dotProduct;
+ Fraction maxDisallowedValue = Fraction(-1, 0),
+ disallowedValue = Fraction(0, 1);
+ Fraction newValue;
+
+ for (unsigned d = 2; d <= dim; d++) {
+ lowerDimDotProducts.clear();
+
+ // Compute the set of dot products <x_i[:d-1], vs> for each i.
+ for (const Point &vector : vectors) {
+ dotProduct = Fraction(0, 1);
+ for (unsigned i = 0; i < d - 1; i++)
+ dotProduct = dotProduct + vector[i] * newPoint[i];
+ lowerDimDotProducts.push_back(dotProduct);
+ }
+
+ // Compute - <x_i[:n-1], vs> / x_i[-1] for each i,
+ // and find the biggest such value.
----------------
Superty wrote:
If you change the meaning of `[:i]`, change it here too
https://github.com/llvm/llvm-project/pull/77819
More information about the Mlir-commits
mailing list