8
8
9
9
#include " mlir/Analysis/Presburger/Barvinok.h"
10
10
#include " llvm/ADT/Sequence.h"
11
+ #include < algorithm>
11
12
12
13
using namespace mlir ;
13
14
using namespace presburger ;
@@ -144,3 +145,100 @@ GeneratingFunction mlir::presburger::detail::unimodularConeGeneratingFunction(
144
145
std::vector ({numerator}),
145
146
std::vector ({denominator}));
146
147
}
148
+
149
+ // / We use an iterative procedure to find a vector not orthogonal
150
+ // / to a given set, ignoring the null vectors.
151
+ // / Let the inputs be {x_1, ..., x_k}, all vectors of length n.
152
+ // /
153
+ // / In the following,
154
+ // / vs[:i] means the elements of vs up to and including the i'th one,
155
+ // / <vs, us> means the dot product of vs and us,
156
+ // / vs ++ [v] means the vector vs with the new element v appended to it.
157
+ // /
158
+ // / We proceed iteratively; for steps d = 0, ... n-1, we construct a vector
159
+ // / which is not orthogonal to any of {x_1[:d], ..., x_n[:d]}, ignoring
160
+ // / the null vectors.
161
+ // / At step d = 0, we let vs = [1]. Clearly this is not orthogonal to
162
+ // / any vector in the set {x_1[0], ..., x_n[0]}, except the null ones,
163
+ // / which we ignore.
164
+ // / At step d > 0 , we need a number v
165
+ // / s.t. <x_i[:d], vs++[v]> != 0 for all i.
166
+ // / => <x_i[:d-1], vs> + x_i[d]*v != 0
167
+ // / => v != - <x_i[:d-1], vs> / x_i[d]
168
+ // / We compute this value for all x_i, and then
169
+ // / set v to be the maximum element of this set plus one. Thus
170
+ // / v is outside the set as desired, and we append it to vs
171
+ // / to obtain the result of the d'th step.
172
+ Point mlir::presburger::detail::getNonOrthogonalVector (
173
+ ArrayRef<Point> vectors) {
174
+ unsigned dim = vectors[0 ].size ();
175
+ for (const Point &vector : vectors)
176
+ assert (vector.size () == dim && " all vectors need to be the same size!" );
177
+
178
+ SmallVector<Fraction> newPoint = {Fraction (1 , 1 )};
179
+ Fraction maxDisallowedValue = -Fraction (1 , 0 ),
180
+ disallowedValue = Fraction (0 , 1 );
181
+
182
+ for (unsigned d = 1 ; d < dim; ++d) {
183
+ // Compute the disallowed values - <x_i[:d-1], vs> / x_i[d] for each i.
184
+ maxDisallowedValue = -Fraction (1 , 0 );
185
+ for (const Point &vector : vectors) {
186
+ if (vector[d] == 0 )
187
+ continue ;
188
+ disallowedValue =
189
+ -dotProduct (ArrayRef (vector).slice (0 , d), newPoint) / vector[d];
190
+
191
+ // Find the biggest such value
192
+ maxDisallowedValue = std::max (maxDisallowedValue, disallowedValue);
193
+ }
194
+ newPoint.push_back (maxDisallowedValue + 1 );
195
+ }
196
+ return newPoint;
197
+ }
198
+
199
+ // / We use the following recursive formula to find the coefficient of
200
+ // / s^power in the rational function given by P(s)/Q(s).
201
+ // /
202
+ // / Let P[i] denote the coefficient of s^i in the polynomial P(s).
203
+ // / (P/Q)[r] =
204
+ // / if (r == 0) then
205
+ // / P[0]/Q[0]
206
+ // / else
207
+ // / (P[r] - {Σ_{i=1}^r (P/Q)[r-i] * Q[i])}/(Q[0])
208
+ // / We therefore recursively call `getCoefficientInRationalFunction` on
209
+ // / all i \in [0, power).
210
+ // /
211
+ // / https://math.ucdavis.edu/~deloera/researchsummary/
212
+ // / barvinokalgorithm-latte1.pdf, p. 1285
213
+ QuasiPolynomial mlir::presburger::detail::getCoefficientInRationalFunction (
214
+ unsigned power, ArrayRef<QuasiPolynomial> num, ArrayRef<Fraction> den) {
215
+ assert (den.size () != 0 &&
216
+ " division by empty denominator in rational function!" );
217
+
218
+ unsigned numParam = num[0 ].getNumInputs ();
219
+ for (const QuasiPolynomial &qp : num)
220
+ // We use the `isEqual` method of PresburgerSpace, which QuasiPolynomial
221
+ // inherits from.
222
+ assert (num[0 ].isEqual (qp) &&
223
+ " the quasipolynomials should all belong to the same space!" );
224
+
225
+ std::vector<QuasiPolynomial> coefficients;
226
+ coefficients.reserve (power + 1 );
227
+
228
+ coefficients.push_back (num[0 ] / den[0 ]);
229
+ for (unsigned i = 1 ; i <= power; ++i) {
230
+ // If the power is not there in the numerator, the coefficient is zero.
231
+ coefficients.push_back (i < num.size () ? num[i]
232
+ : QuasiPolynomial (numParam, 0 ));
233
+
234
+ // After den.size(), the coefficients are zero, so we stop
235
+ // subtracting at that point (if it is less than i).
236
+ unsigned limit = std::min<unsigned long >(i, den.size () - 1 );
237
+ for (unsigned j = 1 ; j <= limit; ++j)
238
+ coefficients[i] = coefficients[i] -
239
+ coefficients[i - j] * QuasiPolynomial (numParam, den[j]);
240
+
241
+ coefficients[i] = coefficients[i] / den[0 ];
242
+ }
243
+ return coefficients[power].simplify ();
244
+ }
0 commit comments