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"
26 using namespace presburger;
27 using llvm::dynamicAPIntFromInt64;
34 DynamicAPInt &divisor) {
35 assert(divisor > 0 &&
"divisor must be non-negative!");
40 DynamicAPInt gcd = llvm::gcd(
abs(dividend.front()), divisor);
49 for (
size_t i = 1, m = dividend.size() - 1; i < m; i++) {
50 gcd = llvm::gcd(
abs(dividend[i]), gcd);
56 std::transform(dividend.begin(), dividend.end(), dividend.begin(),
57 [gcd](DynamicAPInt &n) { return floorDiv(n, gcd); });
100 unsigned ubIneq,
unsigned lbIneq,
102 DynamicAPInt &divisor) {
104 assert(pos <= cst.
getNumVars() &&
"Invalid variable position");
106 "Invalid upper bound inequality position");
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!");
114 divisor = cst.
atIneq(lbIneq, pos);
118 unsigned i = 0, e = 0;
131 DynamicAPInt c = divisor - 1 - constantSum;
135 if (!(0 <= c && c <= divisor - 1))
143 expr[i] = cst.
atIneq(ubIneq, i);
168 DynamicAPInt &divisor) {
170 assert(pos <= cst.
getNumVars() &&
"Invalid variable position");
172 assert(expr.size() == cst.
getNumCols() &&
"Invalid expression size");
177 DynamicAPInt tempDiv = cst.
atEq(eqInd, pos);
180 int signDiv = tempDiv < 0 ? -1 : 1;
183 divisor = tempDiv * signDiv;
185 for (
unsigned i = 0, e = cst.
getNumVars(); i < e; ++i)
187 expr[i] = -signDiv * cst.
atEq(eqInd, i);
202 for (
unsigned c = 0, e = cst.
getNumVars(); c < e; ++c) {
206 if (!foundRepr[c] && dividend[c] != 0) {
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");
240 for (
unsigned ubPos : ubIndices) {
241 for (
unsigned lbPos : lbIndices) {
243 if (
getDivRepr(cst, pos, ubPos, lbPos, dividend, divisor).failed())
250 repr.repr.inequalityPair = {ubPos, lbPos};
254 for (
unsigned eqPos : eqIndices) {
256 if (
getDivRepr(cst, pos, eqPos, dividend, divisor).failed())
263 repr.repr.equalityIdx = eqPos;
273 DynamicAPInt divisorDynamicAPInt;
275 cst, foundRepr, pos, dividendDynamicAPInt, divisorDynamicAPInt);
277 divisor = unsigned(int64_t(divisorDynamicAPInt));
284 llvm::SmallBitVector vec(len,
false);
285 vec.set(setOffset, setOffset + numSet);
293 "Spaces should be compatible.");
307 for (
unsigned i = initLocals, e = divsB.
getNumDivs(); i < e; ++i)
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!");
323 ineq[localVarIdx] = -divisor;
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!");
335 std::transform(dividend.begin(), dividend.end(), ineq.begin(),
336 std::negate<DynamicAPInt>());
337 ineq[localVarIdx] = divisor;
338 ineq.back() += divisor - 1;
344 for (
const DynamicAPInt &elem : range) {
345 gcd = llvm::gcd(gcd,
abs(elem));
354 if ((gcd == 0) || (gcd == 1))
356 for (DynamicAPInt &elem : range)
362 DynamicAPInt &denom) {
363 assert(denom > 0 &&
"denom must be positive!");
364 DynamicAPInt gcd = llvm::gcd(
gcdRange(num), denom);
367 for (DynamicAPInt &coeff : num)
375 negatedCoeffs.reserve(coeffs.size());
376 for (
const DynamicAPInt &coeff : coeffs)
377 negatedCoeffs.emplace_back(-coeff);
378 return negatedCoeffs;
384 coeffs.reserve(ineq.size());
385 for (
const DynamicAPInt &coeff : ineq)
386 coeffs.emplace_back(-coeff);
393 assert(point.size() ==
getNumNonDivs() &&
"Incorrect point size");
400 for (
unsigned i = 0, e =
getNumDivs(); i < e; ++i) {
406 DynamicAPInt divVal(0);
425 divVal = std::inner_product(point.begin(), point.end(), dividend.begin(),
428 divVal += dividend.back();
430 divVal = floorDiv(divVal, denoms[i]);
433 divValues[i] = divVal;
462 if (denoms[i] != denoms[
j])
470 bool mergeResult = merge(i,
j);
479 denoms.erase(denoms.begin() +
j);
488 for (
unsigned i = 0, e =
getNumDivs(); i < e; ++i) {
496 const DynamicAPInt &divisor) {
497 assert(pos <=
getNumDivs() &&
"Invalid insertion position");
498 assert(dividend.size() ==
getNumVars() + 1 &&
"Incorrect dividend size");
501 denoms.insert(denoms.begin() + pos, divisor);
506 assert(pos <=
getNumDivs() &&
"Invalid insertion position");
509 denoms.insert(denoms.begin() + pos, num, DynamicAPInt(0));
513 os <<
"Dividends:\n";
515 os <<
"Denominators\n";
516 for (
const DynamicAPInt &denom : denoms)
526 std::transform(range.begin(), range.end(), result.begin(),
527 dynamicAPIntFromInt64);
533 std::transform(range.begin(), range.end(), result.begin(),
534 int64fromDynamicAPInt);
539 assert(a.size() == b.size() &&
540 "dot product is only valid for vectors of equal sizes!");
542 for (
unsigned i = 0, e = a.size(); i < e; i++)
553 unsigned len = a.size() + b.size() - 1;
562 std::vector<Fraction> convolution;
563 convolution.reserve(len);
564 for (
unsigned k = 0; k < len; ++k) {
566 for (
unsigned l = 0; l <= k; ++l)
567 sum += getCoeff(a, l) * getCoeff(b, k - l);
568 convolution.emplace_back(sum);
574 return llvm::all_of(arr, [](
const Fraction &f) {
return f == 0; });
static LogicalResult getDivRepr(const IntegerRelation &cst, unsigned pos, unsigned ubIneq, unsigned lbIneq, MutableArrayRef< DynamicAPInt > expr, DynamicAPInt &divisor)
Check if the pos^th variable can be represented as a division using upper bound inequality at positio...
static bool checkExplicitRepresentation(const IntegerRelation &cst, ArrayRef< bool > foundRepr, ArrayRef< DynamicAPInt > dividend, unsigned pos)
static void normalizeDivisionByGCD(MutableArrayRef< DynamicAPInt > dividend, DynamicAPInt &divisor)
Normalize a division's dividend and the divisor by their GCD.
Class storing division representation of local variables of a constraint system.
void removeDuplicateDivs(llvm::function_ref< bool(unsigned i, unsigned j)> merge)
Removes duplicate divisions.
unsigned getNumNonDivs() const
unsigned getNumVars() const
unsigned getDivOffset() const
void print(raw_ostream &os) const
unsigned getNumDivs() const
SmallVector< std::optional< DynamicAPInt >, 4 > divValuesAt(ArrayRef< DynamicAPInt > point) const
DynamicAPInt & getDenom(unsigned i)
void insertDiv(unsigned pos, ArrayRef< DynamicAPInt > dividend, const DynamicAPInt &divisor)
void setDiv(unsigned i, ArrayRef< DynamicAPInt > dividend, const DynamicAPInt &divisor)
MutableArrayRef< DynamicAPInt > getDividend(unsigned i)
An IntegerRelation represents the set of points from a PresburgerSpace that satisfy a list of affine ...
DynamicAPInt atIneq(unsigned i, unsigned j) const
Returns the value at the specified inequality row and column.
virtual unsigned insertVar(VarKind kind, unsigned pos, unsigned num=1)
Insert num variables of the specified kind at position pos.
DynamicAPInt atEq(unsigned i, unsigned j) const
Returns the value at the specified equality row and column.
unsigned getNumVars() const
unsigned getNumLocalVars() const
unsigned getNumCols() const
Returns the number of columns in the constraint system.
void getLowerAndUpperBoundIndices(unsigned pos, SmallVectorImpl< unsigned > *lbIndices, SmallVectorImpl< unsigned > *ubIndices, SmallVectorImpl< unsigned > *eqIndices=nullptr, unsigned offset=0, unsigned num=0) const
Gather positions of all lower and upper bounds of the variable at pos, and optionally any equalities ...
DivisionRepr getLocalReprs(std::vector< MaybeLocalRepr > *repr=nullptr) const
Returns a DivisonRepr representing the division representation of local variables in the constraint s...
unsigned getNumInequalities() const
const PresburgerSpace & getSpace() const
Returns a reference to the underlying space.
unsigned getNumEqualities() const
void insertRows(unsigned pos, unsigned count)
Insert rows having positions pos, pos + 1, ...
void removeColumn(unsigned pos)
unsigned appendExtraRow()
Add an extra row at the bottom of the matrix and return its position.
void addToColumn(unsigned sourceColumn, unsigned targetColumn, const T &scale)
Add scale multiples of the source column to the target column.
void print(raw_ostream &os) const
Print the matrix.
void insertColumn(unsigned pos)
MutableArrayRef< T > getRow(unsigned row)
Get a [Mutable]ArrayRef corresponding to the specified row.
void insertColumns(unsigned pos, unsigned count)
Insert columns having positions pos, pos + 1, ...
void removeRow(unsigned pos)
bool isCompatible(const PresburgerSpace &other) const
Returns true if both the spaces are compatible i.e.
void normalizeDiv(MutableArrayRef< DynamicAPInt > num, DynamicAPInt &denom)
Normalize the given (numerator, denominator) pair by dividing out the common factors between them.
SmallVector< DynamicAPInt, 8 > getDynamicAPIntVec(ArrayRef< int64_t > range)
Check if the pos^th variable can be expressed as a floordiv of an affine function of other variables ...
DynamicAPInt gcdRange(ArrayRef< DynamicAPInt > range)
Compute the gcd of the range.
MaybeLocalRepr computeSingleVarRepr(const IntegerRelation &cst, ArrayRef< bool > foundRepr, unsigned pos, MutableArrayRef< DynamicAPInt > dividend, DynamicAPInt &divisor)
Returns the MaybeLocalRepr struct which contains the indices of the constraints that can be expressed...
void mergeLocalVars(IntegerRelation &relA, IntegerRelation &relB, llvm::function_ref< bool(unsigned i, unsigned j)> merge)
Given two relations, A and B, add additional local vars to the sets such that both have the union of ...
SmallVector< DynamicAPInt, 8 > getNegatedCoeffs(ArrayRef< DynamicAPInt > coeffs)
Return coeffs with all the elements negated.
Fraction abs(const Fraction &f)
Fraction dotProduct(ArrayRef< Fraction > a, ArrayRef< Fraction > b)
Compute the dot product of two vectors.
SmallVector< int64_t, 8 > getInt64Vec(ArrayRef< DynamicAPInt > range)
Return the given array as an array of int64_t.
SmallVector< DynamicAPInt, 8 > getDivUpperBound(ArrayRef< DynamicAPInt > dividend, const DynamicAPInt &divisor, unsigned localVarIdx)
If q is defined to be equal to expr floordiv d, this equivalent to saying that q is an integer and q ...
bool isRangeZero(ArrayRef< Fraction > arr)
std::vector< Fraction > multiplyPolynomials(ArrayRef< Fraction > a, ArrayRef< Fraction > b)
Find the product of two polynomials, each given by an array of coefficients.
llvm::SmallBitVector getSubrangeBitVector(unsigned len, unsigned setOffset, unsigned numSet)
SmallVector< DynamicAPInt, 8 > getDivLowerBound(ArrayRef< DynamicAPInt > dividend, const DynamicAPInt &divisor, unsigned localVarIdx)
DynamicAPInt normalizeRange(MutableArrayRef< DynamicAPInt > range)
Divide the range by its gcd and return the gcd.
SmallVector< DynamicAPInt, 8 > getComplementIneq(ArrayRef< DynamicAPInt > ineq)
Return the complement of the given inequality.
Include the generated interface declarations.
A class to represent fractions.
MaybeLocalRepr contains the indices of the constraints that can be expressed as a floordiv of an affi...
Eliminates variable at the specified position using Fourier-Motzkin variable elimination.