1 | //===- Utils.cpp - General utilities for Presburger library ---------------===// |
---|---|
2 | // |
3 | // Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions. |
4 | // See https://llvm.org/LICENSE.txt for license information. |
5 | // SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception |
6 | // |
7 | //===----------------------------------------------------------------------===// |
8 | // |
9 | // Utility functions required by the Presburger Library. |
10 | // |
11 | //===----------------------------------------------------------------------===// |
12 | |
13 | #include "mlir/Analysis/Presburger/Utils.h" |
14 | #include "mlir/Analysis/Presburger/IntegerRelation.h" |
15 | #include "mlir/Analysis/Presburger/PresburgerSpace.h" |
16 | #include "llvm/ADT/STLFunctionalExtras.h" |
17 | #include "llvm/ADT/SmallBitVector.h" |
18 | #include "llvm/Support/LogicalResult.h" |
19 | #include "llvm/Support/raw_ostream.h" |
20 | #include <cassert> |
21 | #include <cstdint> |
22 | #include <numeric> |
23 | #include <optional> |
24 | |
25 | using namespace mlir; |
26 | using namespace presburger; |
27 | using llvm::dynamicAPIntFromInt64; |
28 | |
29 | /// Normalize a division's `dividend` and the `divisor` by their GCD. For |
30 | /// example: if the dividend and divisor are [2,0,4] and 4 respectively, |
31 | /// they get normalized to [1,0,2] and 2. The divisor must be non-negative; |
32 | /// it is allowed for the divisor to be zero, but nothing is done in this case. |
33 | static void normalizeDivisionByGCD(MutableArrayRef<DynamicAPInt> dividend, |
34 | DynamicAPInt &divisor) { |
35 | assert(divisor > 0 && "divisor must be non-negative!"); |
36 | if (dividend.empty()) |
37 | return; |
38 | // We take the absolute value of dividend's coefficients to make sure that |
39 | // `gcd` is positive. |
40 | DynamicAPInt gcd = llvm::gcd(A: abs(X: dividend.front()), B: divisor); |
41 | |
42 | // The reason for ignoring the constant term is as follows. |
43 | // For a division: |
44 | // floor((a + m.f(x))/(m.d)) |
45 | // It can be replaced by: |
46 | // floor((floor(a/m) + f(x))/d) |
47 | // Since `{a/m}/d` in the dividend satisfies 0 <= {a/m}/d < 1/d, it will not |
48 | // influence the result of the floor division and thus, can be ignored. |
49 | for (size_t i = 1, m = dividend.size() - 1; i < m; i++) { |
50 | gcd = llvm::gcd(A: abs(X: dividend[i]), B: gcd); |
51 | if (gcd == 1) |
52 | return; |
53 | } |
54 | |
55 | // Normalize the dividend and the denominator. |
56 | std::transform(first: dividend.begin(), last: dividend.end(), result: dividend.begin(), |
57 | unary_op: [gcd](DynamicAPInt &n) { return floorDiv(LHS: n, RHS: gcd); }); |
58 | divisor /= gcd; |
59 | } |
60 | |
61 | /// Check if the pos^th variable can be represented as a division using upper |
62 | /// bound inequality at position `ubIneq` and lower bound inequality at position |
63 | /// `lbIneq`. |
64 | /// |
65 | /// Let `var` be the pos^th variable, then `var` is equivalent to |
66 | /// `expr floordiv divisor` if there are constraints of the form: |
67 | /// 0 <= expr - divisor * var <= divisor - 1 |
68 | /// Rearranging, we have: |
69 | /// divisor * var - expr + (divisor - 1) >= 0 <-- Lower bound for 'var' |
70 | /// -divisor * var + expr >= 0 <-- Upper bound for 'var' |
71 | /// |
72 | /// For example: |
73 | /// 32*k >= 16*i + j - 31 <-- Lower bound for 'k' |
74 | /// 32*k <= 16*i + j <-- Upper bound for 'k' |
75 | /// expr = 16*i + j, divisor = 32 |
76 | /// k = ( 16*i + j ) floordiv 32 |
77 | /// |
78 | /// 4q >= i + j - 2 <-- Lower bound for 'q' |
79 | /// 4q <= i + j + 1 <-- Upper bound for 'q' |
80 | /// expr = i + j + 1, divisor = 4 |
81 | /// q = (i + j + 1) floordiv 4 |
82 | // |
83 | /// This function also supports detecting divisions from bounds that are |
84 | /// strictly tighter than the division bounds described above, since tighter |
85 | /// bounds imply the division bounds. For example: |
86 | /// 4q - i - j + 2 >= 0 <-- Lower bound for 'q' |
87 | /// -4q + i + j >= 0 <-- Tight upper bound for 'q' |
88 | /// |
89 | /// To extract floor divisions with tighter bounds, we assume that the |
90 | /// constraints are of the form: |
91 | /// c <= expr - divisior * var <= divisor - 1, where 0 <= c <= divisor - 1 |
92 | /// Rearranging, we have: |
93 | /// divisor * var - expr + (divisor - 1) >= 0 <-- Lower bound for 'var' |
94 | /// -divisor * var + expr - c >= 0 <-- Upper bound for 'var' |
95 | /// |
96 | /// If successful, `expr` is set to dividend of the division and `divisor` is |
97 | /// set to the denominator of the division, which will be positive. |
98 | /// The final division expression is normalized by GCD. |
99 | static LogicalResult getDivRepr(const IntegerRelation &cst, unsigned pos, |
100 | unsigned ubIneq, unsigned lbIneq, |
101 | MutableArrayRef<DynamicAPInt> expr, |
102 | DynamicAPInt &divisor) { |
103 | |
104 | assert(pos <= cst.getNumVars() && "Invalid variable position"); |
105 | assert(ubIneq <= cst.getNumInequalities() && |
106 | "Invalid upper bound inequality position"); |
107 | assert(lbIneq <= cst.getNumInequalities() && |
108 | "Invalid upper bound inequality position"); |
109 | assert(expr.size() == cst.getNumCols() && "Invalid expression size"); |
110 | assert(cst.atIneq(lbIneq, pos) > 0 && "lbIneq is not a lower bound!"); |
111 | assert(cst.atIneq(ubIneq, pos) < 0 && "ubIneq is not an upper bound!"); |
112 | |
113 | // Extract divisor from the lower bound. |
114 | divisor = cst.atIneq(i: lbIneq, j: pos); |
115 | |
116 | // First, check if the constraints are opposite of each other except the |
117 | // constant term. |
118 | unsigned i = 0, e = 0; |
119 | for (i = 0, e = cst.getNumVars(); i < e; ++i) |
120 | if (cst.atIneq(i: ubIneq, j: i) != -cst.atIneq(i: lbIneq, j: i)) |
121 | break; |
122 | |
123 | if (i < e) |
124 | return failure(); |
125 | |
126 | // Then, check if the constant term is of the proper form. |
127 | // Due to the form of the upper/lower bound inequalities, the sum of their |
128 | // constants is `divisor - 1 - c`. From this, we can extract c: |
129 | DynamicAPInt constantSum = cst.atIneq(i: lbIneq, j: cst.getNumCols() - 1) + |
130 | cst.atIneq(i: ubIneq, j: cst.getNumCols() - 1); |
131 | DynamicAPInt c = divisor - 1 - constantSum; |
132 | |
133 | // Check if `c` satisfies the condition `0 <= c <= divisor - 1`. |
134 | // This also implictly checks that `divisor` is positive. |
135 | if (!(0 <= c && c <= divisor - 1)) // NOLINT |
136 | return failure(); |
137 | |
138 | // The inequality pair can be used to extract the division. |
139 | // Set `expr` to the dividend of the division except the constant term, which |
140 | // is set below. |
141 | for (i = 0, e = cst.getNumVars(); i < e; ++i) |
142 | if (i != pos) |
143 | expr[i] = cst.atIneq(i: ubIneq, j: i); |
144 | |
145 | // From the upper bound inequality's form, its constant term is equal to the |
146 | // constant term of `expr`, minus `c`. From this, |
147 | // constant term of `expr` = constant term of upper bound + `c`. |
148 | expr.back() = cst.atIneq(i: ubIneq, j: cst.getNumCols() - 1) + c; |
149 | normalizeDivisionByGCD(dividend: expr, divisor); |
150 | |
151 | return success(); |
152 | } |
153 | |
154 | /// Check if the pos^th variable can be represented as a division using |
155 | /// equality at position `eqInd`. |
156 | /// |
157 | /// For example: |
158 | /// 32*k == 16*i + j - 31 <-- `eqInd` for 'k' |
159 | /// expr = 16*i + j - 31, divisor = 32 |
160 | /// k = (16*i + j - 31) floordiv 32 |
161 | /// |
162 | /// If successful, `expr` is set to dividend of the division and `divisor` is |
163 | /// set to the denominator of the division. The final division expression is |
164 | /// normalized by GCD. |
165 | static LogicalResult getDivRepr(const IntegerRelation &cst, unsigned pos, |
166 | unsigned eqInd, |
167 | MutableArrayRef<DynamicAPInt> expr, |
168 | DynamicAPInt &divisor) { |
169 | |
170 | assert(pos <= cst.getNumVars() && "Invalid variable position"); |
171 | assert(eqInd <= cst.getNumEqualities() && "Invalid equality position"); |
172 | assert(expr.size() == cst.getNumCols() && "Invalid expression size"); |
173 | |
174 | // Extract divisor, the divisor can be negative and hence its sign information |
175 | // is stored in `signDiv` to reverse the sign of dividend's coefficients. |
176 | // Equality must involve the pos-th variable and hence `tempDiv` != 0. |
177 | DynamicAPInt tempDiv = cst.atEq(i: eqInd, j: pos); |
178 | if (tempDiv == 0) |
179 | return failure(); |
180 | int signDiv = tempDiv < 0 ? -1 : 1; |
181 | |
182 | // The divisor is always a positive integer. |
183 | divisor = tempDiv * signDiv; |
184 | |
185 | for (unsigned i = 0, e = cst.getNumVars(); i < e; ++i) |
186 | if (i != pos) |
187 | expr[i] = -signDiv * cst.atEq(i: eqInd, j: i); |
188 | |
189 | expr.back() = -signDiv * cst.atEq(i: eqInd, j: cst.getNumCols() - 1); |
190 | normalizeDivisionByGCD(dividend: expr, divisor); |
191 | |
192 | return success(); |
193 | } |
194 | |
195 | // Returns `false` if the constraints depends on a variable for which an |
196 | // explicit representation has not been found yet, otherwise returns `true`. |
197 | static bool checkExplicitRepresentation(const IntegerRelation &cst, |
198 | ArrayRef<bool> foundRepr, |
199 | ArrayRef<DynamicAPInt> dividend, |
200 | unsigned pos) { |
201 | // Exit to avoid circular dependencies between divisions. |
202 | for (unsigned c = 0, e = cst.getNumVars(); c < e; ++c) { |
203 | if (c == pos) |
204 | continue; |
205 | |
206 | if (!foundRepr[c] && dividend[c] != 0) { |
207 | // Expression can't be constructed as it depends on a yet unknown |
208 | // variable. |
209 | // |
210 | // TODO: Visit/compute the variables in an order so that this doesn't |
211 | // happen. More complex but much more efficient. |
212 | return false; |
213 | } |
214 | } |
215 | |
216 | return true; |
217 | } |
218 | |
219 | /// Check if the pos^th variable can be expressed as a floordiv of an affine |
220 | /// function of other variables (where the divisor is a positive constant). |
221 | /// `foundRepr` contains a boolean for each variable indicating if the |
222 | /// explicit representation for that variable has already been computed. |
223 | /// Returns the `MaybeLocalRepr` struct which contains the indices of the |
224 | /// constraints that can be expressed as a floordiv of an affine function. If |
225 | /// the representation could be computed, `dividend` and `denominator` are set. |
226 | /// If the representation could not be computed, the kind attribute in |
227 | /// `MaybeLocalRepr` is set to None. |
228 | MaybeLocalRepr presburger::computeSingleVarRepr( |
229 | const IntegerRelation &cst, ArrayRef<bool> foundRepr, unsigned pos, |
230 | MutableArrayRef<DynamicAPInt> dividend, DynamicAPInt &divisor) { |
231 | assert(pos < cst.getNumVars() && "invalid position"); |
232 | assert(foundRepr.size() == cst.getNumVars() && |
233 | "Size of foundRepr does not match total number of variables"); |
234 | assert(dividend.size() == cst.getNumCols() && "Invalid dividend size"); |
235 | |
236 | SmallVector<unsigned, 4> lbIndices, ubIndices, eqIndices; |
237 | cst.getLowerAndUpperBoundIndices(pos, lbIndices: &lbIndices, ubIndices: &ubIndices, eqIndices: &eqIndices); |
238 | MaybeLocalRepr repr{}; |
239 | |
240 | for (unsigned ubPos : ubIndices) { |
241 | for (unsigned lbPos : lbIndices) { |
242 | // Attempt to get divison representation from ubPos, lbPos. |
243 | if (getDivRepr(cst, pos, ubIneq: ubPos, lbIneq: lbPos, expr: dividend, divisor).failed()) |
244 | continue; |
245 | |
246 | if (!checkExplicitRepresentation(cst, foundRepr, dividend, pos)) |
247 | continue; |
248 | |
249 | repr.kind = ReprKind::Inequality; |
250 | repr.repr.inequalityPair = {.lowerBoundIdx: ubPos, .upperBoundIdx: lbPos}; |
251 | return repr; |
252 | } |
253 | } |
254 | for (unsigned eqPos : eqIndices) { |
255 | // Attempt to get divison representation from eqPos. |
256 | if (getDivRepr(cst, pos, eqInd: eqPos, expr: dividend, divisor).failed()) |
257 | continue; |
258 | |
259 | if (!checkExplicitRepresentation(cst, foundRepr, dividend, pos)) |
260 | continue; |
261 | |
262 | repr.kind = ReprKind::Equality; |
263 | repr.repr.equalityIdx = eqPos; |
264 | return repr; |
265 | } |
266 | return repr; |
267 | } |
268 | |
269 | MaybeLocalRepr presburger::computeSingleVarRepr( |
270 | const IntegerRelation &cst, ArrayRef<bool> foundRepr, unsigned pos, |
271 | SmallVector<int64_t, 8> ÷nd, unsigned &divisor) { |
272 | SmallVector<DynamicAPInt, 8> dividendDynamicAPInt(cst.getNumCols()); |
273 | DynamicAPInt divisorDynamicAPInt; |
274 | MaybeLocalRepr result = computeSingleVarRepr( |
275 | cst, foundRepr, pos, dividend: dividendDynamicAPInt, divisor&: divisorDynamicAPInt); |
276 | dividend = getInt64Vec(range: dividendDynamicAPInt); |
277 | divisor = unsigned(int64_t(divisorDynamicAPInt)); |
278 | return result; |
279 | } |
280 | |
281 | llvm::SmallBitVector presburger::getSubrangeBitVector(unsigned len, |
282 | unsigned setOffset, |
283 | unsigned numSet) { |
284 | llvm::SmallBitVector vec(len, false); |
285 | vec.set(I: setOffset, E: setOffset + numSet); |
286 | return vec; |
287 | } |
288 | |
289 | void presburger::mergeLocalVars( |
290 | IntegerRelation &relA, IntegerRelation &relB, |
291 | llvm::function_ref<bool(unsigned i, unsigned j)> merge) { |
292 | assert(relA.getSpace().isCompatible(relB.getSpace()) && |
293 | "Spaces should be compatible."); |
294 | |
295 | // Merge local vars of relA and relB without using division information, |
296 | // i.e. append local vars of `relB` to `relA` and insert local vars of `relA` |
297 | // to `relB` at start of its local vars. |
298 | unsigned initLocals = relA.getNumLocalVars(); |
299 | relA.insertVar(kind: VarKind::Local, pos: relA.getNumLocalVars(), |
300 | num: relB.getNumLocalVars()); |
301 | relB.insertVar(kind: VarKind::Local, pos: 0, num: initLocals); |
302 | |
303 | // Get division representations from each rel. |
304 | DivisionRepr divsA = relA.getLocalReprs(); |
305 | DivisionRepr divsB = relB.getLocalReprs(); |
306 | |
307 | for (unsigned i = initLocals, e = divsB.getNumDivs(); i < e; ++i) |
308 | divsA.setDiv(i, dividend: divsB.getDividend(i), divisor: divsB.getDenom(i)); |
309 | |
310 | // Remove duplicate divisions from divsA. The removing duplicate divisions |
311 | // call, calls `merge` to effectively merge divisions in relA and relB. |
312 | divsA.removeDuplicateDivs(merge); |
313 | } |
314 | |
315 | SmallVector<DynamicAPInt, 8> |
316 | presburger::getDivUpperBound(ArrayRef<DynamicAPInt> dividend, |
317 | const DynamicAPInt &divisor, |
318 | unsigned localVarIdx) { |
319 | assert(divisor > 0 && "divisor must be positive!"); |
320 | assert(dividend[localVarIdx] == 0 && |
321 | "Local to be set to division must have zero coeff!"); |
322 | SmallVector<DynamicAPInt, 8> ineq(dividend); |
323 | ineq[localVarIdx] = -divisor; |
324 | return ineq; |
325 | } |
326 | |
327 | SmallVector<DynamicAPInt, 8> |
328 | presburger::getDivLowerBound(ArrayRef<DynamicAPInt> dividend, |
329 | const DynamicAPInt &divisor, |
330 | unsigned localVarIdx) { |
331 | assert(divisor > 0 && "divisor must be positive!"); |
332 | assert(dividend[localVarIdx] == 0 && |
333 | "Local to be set to division must have zero coeff!"); |
334 | SmallVector<DynamicAPInt, 8> ineq(dividend.size()); |
335 | std::transform(first: dividend.begin(), last: dividend.end(), result: ineq.begin(), |
336 | unary_op: std::negate<DynamicAPInt>()); |
337 | ineq[localVarIdx] = divisor; |
338 | ineq.back() += divisor - 1; |
339 | return ineq; |
340 | } |
341 | |
342 | DynamicAPInt presburger::gcdRange(ArrayRef<DynamicAPInt> range) { |
343 | DynamicAPInt gcd(0); |
344 | for (const DynamicAPInt &elem : range) { |
345 | gcd = llvm::gcd(A: gcd, B: abs(X: elem)); |
346 | if (gcd == 1) |
347 | return gcd; |
348 | } |
349 | return gcd; |
350 | } |
351 | |
352 | DynamicAPInt presburger::normalizeRange(MutableArrayRef<DynamicAPInt> range) { |
353 | DynamicAPInt gcd = gcdRange(range); |
354 | if ((gcd == 0) || (gcd == 1)) |
355 | return gcd; |
356 | for (DynamicAPInt &elem : range) |
357 | elem /= gcd; |
358 | return gcd; |
359 | } |
360 | |
361 | void presburger::normalizeDiv(MutableArrayRef<DynamicAPInt> num, |
362 | DynamicAPInt &denom) { |
363 | assert(denom > 0 && "denom must be positive!"); |
364 | DynamicAPInt gcd = llvm::gcd(A: gcdRange(range: num), B: denom); |
365 | if (gcd == 1) |
366 | return; |
367 | for (DynamicAPInt &coeff : num) |
368 | coeff /= gcd; |
369 | denom /= gcd; |
370 | } |
371 | |
372 | SmallVector<DynamicAPInt, 8> |
373 | presburger::getNegatedCoeffs(ArrayRef<DynamicAPInt> coeffs) { |
374 | SmallVector<DynamicAPInt, 8> negatedCoeffs; |
375 | negatedCoeffs.reserve(N: coeffs.size()); |
376 | for (const DynamicAPInt &coeff : coeffs) |
377 | negatedCoeffs.emplace_back(Args: -coeff); |
378 | return negatedCoeffs; |
379 | } |
380 | |
381 | SmallVector<DynamicAPInt, 8> |
382 | presburger::getComplementIneq(ArrayRef<DynamicAPInt> ineq) { |
383 | SmallVector<DynamicAPInt, 8> coeffs; |
384 | coeffs.reserve(N: ineq.size()); |
385 | for (const DynamicAPInt &coeff : ineq) |
386 | coeffs.emplace_back(Args: -coeff); |
387 | --coeffs.back(); |
388 | return coeffs; |
389 | } |
390 | |
391 | SmallVector<std::optional<DynamicAPInt>, 4> |
392 | DivisionRepr::divValuesAt(ArrayRef<DynamicAPInt> point) const { |
393 | assert(point.size() == getNumNonDivs() && "Incorrect point size"); |
394 | |
395 | SmallVector<std::optional<DynamicAPInt>, 4> divValues(getNumDivs(), |
396 | std::nullopt); |
397 | bool changed = true; |
398 | while (changed) { |
399 | changed = false; |
400 | for (unsigned i = 0, e = getNumDivs(); i < e; ++i) { |
401 | // If division value is found, continue; |
402 | if (divValues[i]) |
403 | continue; |
404 | |
405 | ArrayRef<DynamicAPInt> dividend = getDividend(i); |
406 | DynamicAPInt divVal(0); |
407 | |
408 | // Check if we have all the division values required for this division. |
409 | unsigned j, f; |
410 | for (j = 0, f = getNumDivs(); j < f; ++j) { |
411 | if (dividend[getDivOffset() + j] == 0) |
412 | continue; |
413 | // Division value required, but not found yet. |
414 | if (!divValues[j]) |
415 | break; |
416 | divVal += dividend[getDivOffset() + j] * *divValues[j]; |
417 | } |
418 | |
419 | // We have some division values that are still not found, but are required |
420 | // to find the value of this division. |
421 | if (j < f) |
422 | continue; |
423 | |
424 | // Fill remaining values. |
425 | divVal = std::inner_product(first1: point.begin(), last1: point.end(), first2: dividend.begin(), |
426 | init: divVal); |
427 | // Add constant. |
428 | divVal += dividend.back(); |
429 | // Take floor division with denominator. |
430 | divVal = floorDiv(LHS: divVal, RHS: denoms[i]); |
431 | |
432 | // Set div value and continue. |
433 | divValues[i] = divVal; |
434 | changed = true; |
435 | } |
436 | } |
437 | |
438 | return divValues; |
439 | } |
440 | |
441 | void DivisionRepr::removeDuplicateDivs( |
442 | llvm::function_ref<bool(unsigned i, unsigned j)> merge) { |
443 | |
444 | // Find and merge duplicate divisions. |
445 | // TODO: Add division normalization to support divisions that differ by |
446 | // a constant. |
447 | // TODO: Add division ordering such that a division representation for local |
448 | // variable at position `i` only depends on local variables at position < |
449 | // `i`. This would make sure that all divisions depending on other local |
450 | // variables that can be merged, are merged. |
451 | normalizeDivs(); |
452 | for (unsigned i = 0; i < getNumDivs(); ++i) { |
453 | // Check if a division representation exists for the `i^th` local var. |
454 | if (denoms[i] == 0) |
455 | continue; |
456 | // Check if a division exists which is a duplicate of the division at `i`. |
457 | for (unsigned j = i + 1; j < getNumDivs(); ++j) { |
458 | // Check if a division representation exists for the `j^th` local var. |
459 | if (denoms[j] == 0) |
460 | continue; |
461 | // Check if the denominators match. |
462 | if (denoms[i] != denoms[j]) |
463 | continue; |
464 | // Check if the representations are equal. |
465 | if (dividends.getRow(row: i) != dividends.getRow(row: j)) |
466 | continue; |
467 | |
468 | // Merge divisions at position `j` into division at position `i`. If |
469 | // merge fails, do not merge these divs. |
470 | bool mergeResult = merge(i, j); |
471 | if (!mergeResult) |
472 | continue; |
473 | |
474 | // Update division information to reflect merging. |
475 | unsigned divOffset = getDivOffset(); |
476 | dividends.addToColumn(sourceColumn: divOffset + j, targetColumn: divOffset + i, /*scale=*/1); |
477 | dividends.removeColumn(pos: divOffset + j); |
478 | dividends.removeRow(pos: j); |
479 | denoms.erase(CI: denoms.begin() + j); |
480 | |
481 | // Since `j` can never be zero, we do not need to worry about overflows. |
482 | --j; |
483 | } |
484 | } |
485 | } |
486 | |
487 | void DivisionRepr::normalizeDivs() { |
488 | for (unsigned i = 0, e = getNumDivs(); i < e; ++i) { |
489 | if (getDenom(i) == 0 || getDividend(i).empty()) |
490 | continue; |
491 | normalizeDiv(num: getDividend(i), denom&: getDenom(i)); |
492 | } |
493 | } |
494 | |
495 | void DivisionRepr::insertDiv(unsigned pos, ArrayRef<DynamicAPInt> dividend, |
496 | const DynamicAPInt &divisor) { |
497 | assert(pos <= getNumDivs() && "Invalid insertion position"); |
498 | assert(dividend.size() == getNumVars() + 1 && "Incorrect dividend size"); |
499 | |
500 | dividends.appendExtraRow(elems: dividend); |
501 | denoms.insert(I: denoms.begin() + pos, Elt: divisor); |
502 | dividends.insertColumn(pos: getDivOffset() + pos); |
503 | } |
504 | |
505 | void DivisionRepr::insertDiv(unsigned pos, unsigned num) { |
506 | assert(pos <= getNumDivs() && "Invalid insertion position"); |
507 | dividends.insertColumns(pos: getDivOffset() + pos, count: num); |
508 | dividends.insertRows(pos, count: num); |
509 | denoms.insert(I: denoms.begin() + pos, NumToInsert: num, Elt: DynamicAPInt(0)); |
510 | } |
511 | |
512 | void DivisionRepr::print(raw_ostream &os) const { |
513 | os << "Dividends:\n"; |
514 | dividends.print(os); |
515 | os << "Denominators\n"; |
516 | for (const DynamicAPInt &denom : denoms) |
517 | os << denom << " "; |
518 | os << "\n"; |
519 | } |
520 | |
521 | void DivisionRepr::dump() const { print(os&: llvm::errs()); } |
522 | |
523 | SmallVector<DynamicAPInt, 8> |
524 | presburger::getDynamicAPIntVec(ArrayRef<int64_t> range) { |
525 | SmallVector<DynamicAPInt, 8> result(range.size()); |
526 | std::transform(first: range.begin(), last: range.end(), result: result.begin(), |
527 | unary_op: dynamicAPIntFromInt64); |
528 | return result; |
529 | } |
530 | |
531 | SmallVector<int64_t, 8> presburger::getInt64Vec(ArrayRef<DynamicAPInt> range) { |
532 | SmallVector<int64_t, 8> result(range.size()); |
533 | std::transform(first: range.begin(), last: range.end(), result: result.begin(), |
534 | unary_op: int64fromDynamicAPInt); |
535 | return result; |
536 | } |
537 | |
538 | Fraction presburger::dotProduct(ArrayRef<Fraction> a, ArrayRef<Fraction> b) { |
539 | assert(a.size() == b.size() && |
540 | "dot product is only valid for vectors of equal sizes!"); |
541 | Fraction sum = 0; |
542 | for (unsigned i = 0, e = a.size(); i < e; i++) |
543 | sum += a[i] * b[i]; |
544 | return sum; |
545 | } |
546 | |
547 | /// Find the product of two polynomials, each given by an array of |
548 | /// coefficients, by taking the convolution. |
549 | std::vector<Fraction> presburger::multiplyPolynomials(ArrayRef<Fraction> a, |
550 | ArrayRef<Fraction> b) { |
551 | // The length of the convolution is the sum of the lengths |
552 | // of the two sequences. We pad the shorter one with zeroes. |
553 | unsigned len = a.size() + b.size() - 1; |
554 | |
555 | // We define accessors to avoid out-of-bounds errors. |
556 | auto getCoeff = [](ArrayRef<Fraction> arr, unsigned i) -> Fraction { |
557 | if (i < arr.size()) |
558 | return arr[i]; |
559 | return 0; |
560 | }; |
561 | |
562 | std::vector<Fraction> convolution; |
563 | convolution.reserve(n: len); |
564 | for (unsigned k = 0; k < len; ++k) { |
565 | Fraction sum(0, 1); |
566 | for (unsigned l = 0; l <= k; ++l) |
567 | sum += getCoeff(a, l) * getCoeff(b, k - l); |
568 | convolution.emplace_back(args&: sum); |
569 | } |
570 | return convolution; |
571 | } |
572 | |
573 | bool presburger::isRangeZero(ArrayRef<Fraction> arr) { |
574 | return llvm::all_of(Range&: arr, P: [](const Fraction &f) { return f == 0; }); |
575 | } |
576 |
Definitions
- normalizeDivisionByGCD
- getDivRepr
- getDivRepr
- checkExplicitRepresentation
- computeSingleVarRepr
- computeSingleVarRepr
- getSubrangeBitVector
- mergeLocalVars
- getDivUpperBound
- getDivLowerBound
- gcdRange
- normalizeRange
- normalizeDiv
- getNegatedCoeffs
- getComplementIneq
- divValuesAt
- removeDuplicateDivs
- normalizeDivs
- insertDiv
- insertDiv
- dump
- getDynamicAPIntVec
- getInt64Vec
- dotProduct
- multiplyPolynomials
Learn to use CMake with our Intro Training
Find out more