MLIR  20.0.0git
PWMAFunction.cpp
Go to the documentation of this file.
1 //===- PWMAFunction.cpp - MLIR PWMAFunction Class -------------------------===//
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 
14 #include "llvm/ADT/STLExtras.h"
15 #include "llvm/ADT/STLFunctionalExtras.h"
16 #include "llvm/ADT/SmallVector.h"
17 #include "llvm/Support/raw_ostream.h"
18 #include <algorithm>
19 #include <cassert>
20 #include <optional>
21 
22 using namespace mlir;
23 using namespace presburger;
24 
25 void MultiAffineFunction::assertIsConsistent() const {
26  assert(space.getNumVars() - space.getNumRangeVars() + 1 ==
27  output.getNumColumns() &&
28  "Inconsistent number of output columns");
29  assert(space.getNumDomainVars() + space.getNumSymbolVars() ==
30  divs.getNumNonDivs() &&
31  "Inconsistent number of non-division variables in divs");
32  assert(space.getNumRangeVars() == output.getNumRows() &&
33  "Inconsistent number of output rows");
34  assert(space.getNumLocalVars() == divs.getNumDivs() &&
35  "Inconsistent number of divisions.");
36  assert(divs.hasAllReprs() && "All divisions should have a representation");
37 }
38 
39 // Return the result of subtracting the two given vectors pointwise.
40 // The vectors must be of the same size.
41 // e.g., [3, 4, 6] - [2, 5, 1] = [1, -1, 5].
44  assert(vecA.size() == vecB.size() &&
45  "Cannot subtract vectors of differing lengths!");
47  result.reserve(vecA.size());
48  for (unsigned i = 0, e = vecA.size(); i < e; ++i)
49  result.emplace_back(vecA[i] - vecB[i]);
50  return result;
51 }
52 
55  for (const Piece &piece : pieces)
56  domain.unionInPlace(piece.domain);
57  return domain;
58 }
59 
60 void MultiAffineFunction::print(raw_ostream &os) const {
61  space.print(os);
62  os << "Division Representation:\n";
63  divs.print(os);
64  os << "Output:\n";
65  output.print(os);
66 }
67 
70  assert(point.size() == getNumDomainVars() + getNumSymbolVars() &&
71  "Point has incorrect dimensionality!");
72 
73  SmallVector<DynamicAPInt, 8> pointHomogenous{llvm::to_vector(point)};
74  // Get the division values at this point.
76  divs.divValuesAt(point);
77  // The given point didn't include the values of the divs which the output is a
78  // function of; we have computed one possible set of values and use them here.
79  pointHomogenous.reserve(pointHomogenous.size() + divValues.size());
80  for (const std::optional<DynamicAPInt> &divVal : divValues)
81  pointHomogenous.emplace_back(*divVal);
82  // The matrix `output` has an affine expression in the ith row, corresponding
83  // to the expression for the ith value in the output vector. The last column
84  // of the matrix contains the constant term. Let v be the input point with
85  // a 1 appended at the end. We can see that output * v gives the desired
86  // output vector.
87  pointHomogenous.emplace_back(1);
89  output.postMultiplyWithColumn(pointHomogenous);
90  assert(result.size() == getNumOutputs());
91  return result;
92 }
93 
95  assert(space.isCompatible(other.space) &&
96  "Spaces should be compatible for equality check.");
97  return getAsRelation().isEqual(other.getAsRelation());
98 }
99 
101  const IntegerPolyhedron &domain) const {
102  assert(space.isCompatible(other.space) &&
103  "Spaces should be compatible for equality check.");
104  IntegerRelation restrictedThis = getAsRelation();
105  restrictedThis.intersectDomain(domain);
106 
107  IntegerRelation restrictedOther = other.getAsRelation();
108  restrictedOther.intersectDomain(domain);
109 
110  return restrictedThis.isEqual(restrictedOther);
111 }
112 
114  const PresburgerSet &domain) const {
115  assert(space.isCompatible(other.space) &&
116  "Spaces should be compatible for equality check.");
117  return llvm::all_of(domain.getAllDisjuncts(),
118  [&](const IntegerRelation &disjunct) {
119  return isEqual(other, IntegerPolyhedron(disjunct));
120  });
121 }
122 
123 void MultiAffineFunction::removeOutputs(unsigned start, unsigned end) {
124  assert(end <= getNumOutputs() && "Invalid range");
125 
126  if (start >= end)
127  return;
128 
129  space.removeVarRange(VarKind::Range, start, end);
130  output.removeRows(start, end - start);
131 }
132 
134  assert(space.isCompatible(other.space) && "Functions should be compatible");
135 
136  unsigned nDivs = getNumDivs();
137  unsigned divOffset = divs.getDivOffset();
138 
139  other.divs.insertDiv(0, nDivs);
140 
141  SmallVector<DynamicAPInt, 8> div(other.divs.getNumVars() + 1);
142  for (unsigned i = 0; i < nDivs; ++i) {
143  // Zero fill.
144  std::fill(div.begin(), div.end(), 0);
145  // Fill div with dividend from `divs`. Do not fill the constant.
146  std::copy(divs.getDividend(i).begin(), divs.getDividend(i).end() - 1,
147  div.begin());
148  // Fill constant.
149  div.back() = divs.getDividend(i).back();
150  other.divs.setDiv(i, div, divs.getDenom(i));
151  }
152 
153  other.space.insertVar(VarKind::Local, 0, nDivs);
154  other.output.insertColumns(divOffset, nDivs);
155 
156  auto merge = [&](unsigned i, unsigned j) {
157  // We only merge from local at pos j to local at pos i, where j > i.
158  if (i >= j)
159  return false;
160 
161  // If i < nDivs, we are trying to merge duplicate divs in `this`. Since we
162  // do not want to merge duplicates in `this`, we ignore this call.
163  if (j < nDivs)
164  return false;
165 
166  // Merge things in space and output.
167  other.space.removeVarRange(VarKind::Local, j, j + 1);
168  other.output.addToColumn(divOffset + i, divOffset + j, 1);
169  other.output.removeColumn(divOffset + j);
170  return true;
171  };
172 
173  other.divs.removeDuplicateDivs(merge);
174 
175  unsigned newDivs = other.divs.getNumDivs() - nDivs;
176 
177  space.insertVar(VarKind::Local, nDivs, newDivs);
178  output.insertColumns(divOffset + nDivs, newDivs);
179  divs = other.divs;
180 
181  // Check consistency.
182  assertIsConsistent();
183  other.assertIsConsistent();
184 }
185 
188  const MultiAffineFunction &other) const {
189  assert(getSpace().isCompatible(other.getSpace()) &&
190  "Output space of funcs should be compatible");
191 
192  // Create copies of functions and merge their local space.
193  MultiAffineFunction funcA = *this;
194  MultiAffineFunction funcB = other;
195  funcA.mergeDivs(funcB);
196 
197  // We first create the set `result`, corresponding to the set where output
198  // of funcA is lexicographically larger/smaller than funcB. This is done by
199  // creating a PresburgerSet with the following constraints:
200  //
201  // (outA[0] > outB[0]) U
202  // (outA[0] = outB[0], outA[1] > outA[1]) U
203  // (outA[0] = outB[0], outA[1] = outA[1], outA[2] > outA[2]) U
204  // ...
205  // (outA[0] = outB[0], ..., outA[n-2] = outB[n-2], outA[n-1] > outB[n-1])
206  //
207  // where `n` is the number of outputs.
208  // If `lexMin` is set, the complement inequality is used:
209  //
210  // (outA[0] < outB[0]) U
211  // (outA[0] = outB[0], outA[1] < outA[1]) U
212  // (outA[0] = outB[0], outA[1] = outA[1], outA[2] < outA[2]) U
213  // ...
214  // (outA[0] = outB[0], ..., outA[n-2] = outB[n-2], outA[n-1] < outB[n-1])
215  PresburgerSpace resultSpace = funcA.getDomainSpace();
216  PresburgerSet result =
218  IntegerPolyhedron levelSet(
219  /*numReservedInequalities=*/1 + 2 * resultSpace.getNumLocalVars(),
220  /*numReservedEqualities=*/funcA.getNumOutputs(),
221  /*numReservedCols=*/resultSpace.getNumVars() + 1, resultSpace);
222 
223  // Add division inequalities to `levelSet`.
224  for (unsigned i = 0, e = funcA.getNumDivs(); i < e; ++i) {
225  levelSet.addInequality(getDivUpperBound(funcA.divs.getDividend(i),
226  funcA.divs.getDenom(i),
227  funcA.divs.getDivOffset() + i));
228  levelSet.addInequality(getDivLowerBound(funcA.divs.getDividend(i),
229  funcA.divs.getDenom(i),
230  funcA.divs.getDivOffset() + i));
231  }
232 
233  for (unsigned level = 0; level < funcA.getNumOutputs(); ++level) {
234  // Create the expression `outA - outB` for this level.
236  subtractExprs(funcA.getOutputExpr(level), funcB.getOutputExpr(level));
237 
238  // TODO: Implement all comparison cases.
239  switch (comp) {
240  case OrderingKind::LT:
241  // For less than, we add an upper bound of -1:
242  // outA - outB <= -1
243  // outA <= outB - 1
244  // outA < outB
245  levelSet.addBound(BoundType::UB, subExpr, DynamicAPInt(-1));
246  break;
247  case OrderingKind::GT:
248  // For greater than, we add a lower bound of 1:
249  // outA - outB >= 1
250  // outA > outB + 1
251  // outA > outB
252  levelSet.addBound(BoundType::LB, subExpr, DynamicAPInt(1));
253  break;
254  case OrderingKind::GE:
255  case OrderingKind::LE:
256  case OrderingKind::EQ:
257  case OrderingKind::NE:
258  assert(false && "Not implemented case");
259  }
260 
261  // Union the set with the result.
262  result.unionInPlace(levelSet);
263  // The last inequality in `levelSet` is the bound we inserted. We remove
264  // that for next iteration.
265  levelSet.removeInequality(levelSet.getNumInequalities() - 1);
266  // Add equality `outA - outB == 0` for this level for next iteration.
267  levelSet.addEquality(subExpr);
268  }
269 
270  return result;
271 }
272 
273 /// Two PWMAFunctions are equal if they have the same dimensionalities,
274 /// the same domain, and take the same value at every point in the domain.
275 bool PWMAFunction::isEqual(const PWMAFunction &other) const {
276  if (!space.isCompatible(other.space))
277  return false;
278 
279  if (!this->getDomain().isEqual(other.getDomain()))
280  return false;
281 
282  // Check if, whenever the domains of a piece of `this` and a piece of `other`
283  // overlap, they take the same output value. If `this` and `other` have the
284  // same domain (checked above), then this check passes iff the two functions
285  // have the same output at every point in the domain.
286  return llvm::all_of(this->pieces, [&other](const Piece &pieceA) {
287  return llvm::all_of(other.pieces, [&pieceA](const Piece &pieceB) {
288  PresburgerSet commonDomain = pieceA.domain.intersect(pieceB.domain);
289  return pieceA.output.isEqual(pieceB.output, commonDomain);
290  });
291  });
292 }
293 
294 void PWMAFunction::addPiece(const Piece &piece) {
295  assert(piece.isConsistent() && "Piece should be consistent");
296  assert(piece.domain.intersect(getDomain()).isIntegerEmpty() &&
297  "Piece should be disjoint from the function");
298  pieces.emplace_back(piece);
299 }
300 
301 void PWMAFunction::print(raw_ostream &os) const {
302  space.print(os);
303  os << getNumPieces() << " pieces:\n";
304  for (const Piece &piece : pieces) {
305  os << "Domain of piece:\n";
306  piece.domain.print(os);
307  os << "Output of piece\n";
308  piece.output.print(os);
309  }
310 }
311 
312 void PWMAFunction::dump() const { print(llvm::errs()); }
313 
314 PWMAFunction PWMAFunction::unionFunction(
315  const PWMAFunction &func,
316  llvm::function_ref<PresburgerSet(Piece maf1, Piece maf2)> tiebreak) const {
317  assert(getNumOutputs() == func.getNumOutputs() &&
318  "Ranges of functions should be same.");
319  assert(getSpace().isCompatible(func.getSpace()) &&
320  "Space is not compatible.");
321 
322  // The algorithm used here is as follows:
323  // - Add the output of pieceB for the part of the domain where both pieceA and
324  // pieceB are defined, and `tiebreak` chooses the output of pieceB.
325  // - Add the output of pieceA, where pieceB is not defined or `tiebreak`
326  // chooses
327  // pieceA over pieceB.
328  // - Add the output of pieceB, where pieceA is not defined.
329 
330  // Add parts of the common domain where pieceB's output is used. Also
331  // add all the parts where pieceA's output is used, both common and
332  // non-common.
333  PWMAFunction result(getSpace());
334  for (const Piece &pieceA : pieces) {
335  PresburgerSet dom(pieceA.domain);
336  for (const Piece &pieceB : func.pieces) {
337  PresburgerSet better = tiebreak(pieceB, pieceA);
338  // Add the output of pieceB, where it is better than output of pieceA.
339  // The disjuncts in "better" will be disjoint as tiebreak should gurantee
340  // that.
341  result.addPiece({better, pieceB.output});
342  dom = dom.subtract(better);
343  }
344  // Add output of pieceA, where it is better than pieceB, or pieceB is not
345  // defined.
346  //
347  // `dom` here is guranteed to be disjoint from already added pieces
348  // because the pieces added before are either:
349  // - Subsets of the domain of other MAFs in `this`, which are guranteed
350  // to be disjoint from `dom`, or
351  // - They are one of the pieces added for `pieceB`, and we have been
352  // subtracting all such pieces from `dom`, so `dom` is disjoint from those
353  // pieces as well.
354  result.addPiece({dom, pieceA.output});
355  }
356 
357  // Add parts of pieceB which are not shared with pieceA.
358  PresburgerSet dom = getDomain();
359  for (const Piece &pieceB : func.pieces)
360  result.addPiece({pieceB.domain.subtract(dom), pieceB.output});
361 
362  return result;
363 }
364 
365 /// A tiebreak function which breaks ties by comparing the outputs
366 /// lexicographically based on the given comparison operator.
367 /// This is templated since it is passed as a lambda.
368 template <OrderingKind comp>
370  const PWMAFunction::Piece &pieceB) {
371  PresburgerSet result = pieceA.output.getLexSet(comp, pieceB.output);
372  result = result.intersect(pieceA.domain).intersect(pieceB.domain);
373 
374  return result;
375 }
376 
378  return unionFunction(func, tiebreakLex</*comp=*/OrderingKind::LT>);
379 }
380 
382  return unionFunction(func, tiebreakLex</*comp=*/OrderingKind::GT>);
383 }
384 
386  assert(space.isCompatible(other.space) &&
387  "Spaces should be compatible for subtraction.");
388 
389  MultiAffineFunction copyOther = other;
390  mergeDivs(copyOther);
391  for (unsigned i = 0, e = getNumOutputs(); i < e; ++i)
392  output.addToRow(i, copyOther.getOutputExpr(i), DynamicAPInt(-1));
393 
394  // Check consistency.
395  assertIsConsistent();
396 }
397 
398 /// Adds division constraints corresponding to local variables, given a
399 /// relation and division representations of the local variables in the
400 /// relation.
402  const DivisionRepr &divs) {
403  assert(divs.hasAllReprs() &&
404  "All divisions in divs should have a representation");
405  assert(rel.getNumVars() == divs.getNumVars() &&
406  "Relation and divs should have the same number of vars");
407  assert(rel.getNumLocalVars() == divs.getNumDivs() &&
408  "Relation and divs should have the same number of local vars");
409 
410  for (unsigned i = 0, e = divs.getNumDivs(); i < e; ++i) {
411  rel.addInequality(getDivUpperBound(divs.getDividend(i), divs.getDenom(i),
412  divs.getDivOffset() + i));
413  rel.addInequality(getDivLowerBound(divs.getDividend(i), divs.getDenom(i),
414  divs.getDivOffset() + i));
415  }
416 }
417 
419  // Create a relation corressponding to the input space plus the divisions
420  // used in outputs.
422  space.getNumDomainVars(), 0, space.getNumSymbolVars(),
423  space.getNumLocalVars()));
424  // Add division constraints corresponding to divisions used in outputs.
425  addDivisionConstraints(result, divs);
426  // The outputs are represented as range variables in the relation. We add
427  // range variables for the outputs.
428  result.insertVar(VarKind::Range, 0, getNumOutputs());
429 
430  // Add equalities such that the i^th range variable is equal to the i^th
431  // output expression.
433  for (unsigned i = 0, e = getNumOutputs(); i < e; ++i) {
434  // TODO: Add functions to get VarKind offsets in output in MAF and use them
435  // here.
436  // The output expression does not contain range variables, while the
437  // equality does. So, we need to copy all variables and mark all range
438  // variables as 0 in the equality.
440  // Copy domain variables in `expr` to domain variables in `eq`.
441  std::copy(expr.begin(), expr.begin() + getNumDomainVars(), eq.begin());
442  // Fill the range variables in `eq` as zero.
443  std::fill(eq.begin() + result.getVarKindOffset(VarKind::Range),
444  eq.begin() + result.getVarKindEnd(VarKind::Range), 0);
445  // Copy remaining variables in `expr` to the remaining variables in `eq`.
446  std::copy(expr.begin() + getNumDomainVars(), expr.end(),
447  eq.begin() + result.getVarKindEnd(VarKind::Range));
448 
449  // Set the i^th range var to -1 in `eq` to equate the output expression to
450  // this range var.
451  eq[result.getVarKindOffset(VarKind::Range) + i] = -1;
452  // Add the equality `rangeVar_i = output[i]`.
453  result.addEquality(eq);
454  }
455 
456  return result;
457 }
458 
459 void PWMAFunction::removeOutputs(unsigned start, unsigned end) {
460  space.removeVarRange(VarKind::Range, start, end);
461  for (Piece &piece : pieces)
462  piece.output.removeOutputs(start, end);
463 }
464 
465 std::optional<SmallVector<DynamicAPInt, 8>>
467  assert(point.size() == getNumDomainVars() + getNumSymbolVars());
468 
469  for (const Piece &piece : pieces)
470  if (piece.domain.containsPoint(point))
471  return piece.output.valueAt(point);
472  return std::nullopt;
473 }
static void copy(Location loc, Value dst, Value src, Value size, OpBuilder &builder)
Copies the given number of bytes from src to dst pointers.
static SmallVector< DynamicAPInt, 8 > subtractExprs(ArrayRef< DynamicAPInt > vecA, ArrayRef< DynamicAPInt > vecB)
static PresburgerSet tiebreakLex(const PWMAFunction::Piece &pieceA, const PWMAFunction::Piece &pieceB)
A tiebreak function which breaks ties by comparing the outputs lexicographically based on the given c...
static void addDivisionConstraints(IntegerRelation &rel, const DivisionRepr &divs)
Adds division constraints corresponding to local variables, given a relation and division representat...
Class storing division representation of local variables of a constraint system.
Definition: Utils.h:117
void removeDuplicateDivs(llvm::function_ref< bool(unsigned i, unsigned j)> merge)
Removes duplicate divisions.
Definition: Utils.cpp:441
bool hasAllReprs() const
Definition: Utils.h:133
unsigned getNumNonDivs() const
Definition: Utils.h:126
unsigned getNumVars() const
Definition: Utils.h:124
unsigned getDivOffset() const
Definition: Utils.h:128
void print(raw_ostream &os) const
Definition: Utils.cpp:512
unsigned getNumDivs() const
Definition: Utils.h:125
SmallVector< std::optional< DynamicAPInt >, 4 > divValuesAt(ArrayRef< DynamicAPInt > point) const
Definition: Utils.cpp:392
DynamicAPInt & getDenom(unsigned i)
Definition: Utils.h:153
void insertDiv(unsigned pos, ArrayRef< DynamicAPInt > dividend, const DynamicAPInt &divisor)
Definition: Utils.cpp:495
void setDiv(unsigned i, ArrayRef< DynamicAPInt > dividend, const DynamicAPInt &divisor)
Definition: Utils.h:158
MutableArrayRef< DynamicAPInt > getDividend(unsigned i)
Definition: Utils.h:139
An IntegerPolyhedron represents the set of points from a PresburgerSpace that satisfy a list of affin...
An IntegerRelation represents the set of points from a PresburgerSpace that satisfy a list of affine ...
unsigned getVarKindEnd(VarKind kind) const
Return the index at Which the specified kind of vars ends.
void addBound(BoundType type, unsigned pos, const DynamicAPInt &value)
Adds a constant bound for the specified variable.
virtual unsigned insertVar(VarKind kind, unsigned pos, unsigned num=1)
Insert num variables of the specified kind at position pos.
void intersectDomain(const IntegerPolyhedron &poly)
Intersect the given poly with the domain in-place.
bool isEqual(const IntegerRelation &other) const
Return whether this and other are equal.
void addEquality(ArrayRef< DynamicAPInt > eq)
Adds an equality from the coefficients specified in eq.
unsigned getNumCols() const
Returns the number of columns in the constraint system.
void addInequality(ArrayRef< DynamicAPInt > inEq)
Adds an inequality (>= 0) from the coefficients specified in inEq.
unsigned getVarKindOffset(VarKind kind) const
Return the index at which the specified kind of vars starts.
unsigned getNumRows() const
Definition: Matrix.h:86
void removeColumn(unsigned pos)
Definition: Matrix.cpp:194
void addToColumn(unsigned sourceColumn, unsigned targetColumn, const T &scale)
Add scale multiples of the source column to the target column.
Definition: Matrix.cpp:319
void print(raw_ostream &os) const
Print the matrix.
Definition: Matrix.cpp:400
void insertColumns(unsigned pos, unsigned count)
Insert columns having positions pos, pos + 1, ...
Definition: Matrix.cpp:152
unsigned getNumColumns() const
Definition: Matrix.h:88
SmallVector< T, 8 > postMultiplyWithColumn(ArrayRef< T > colVec) const
The given vector is interpreted as a column vector v.
Definition: Matrix.cpp:357
void addToRow(unsigned sourceRow, unsigned targetRow, const T &scale)
Add scale multiples of the source row to the target row.
Definition: Matrix.cpp:299
void removeRows(unsigned pos, unsigned count)
Remove the rows having positions pos, pos + 1, ...
Definition: Matrix.cpp:234
This class represents a multi-affine function with the domain as Z^d, where d is the number of domain...
Definition: PWMAFunction.h:41
void subtract(const MultiAffineFunction &other)
void removeOutputs(unsigned start, unsigned end)
Remove the specified range of outputs.
void print(raw_ostream &os) const
const PresburgerSpace & getSpace() const
Get the space of this function.
Definition: PWMAFunction.h:61
PresburgerSpace getDomainSpace() const
Get the domain/output space of the function.
Definition: PWMAFunction.h:64
PresburgerSet getLexSet(OrderingKind comp, const MultiAffineFunction &other) const
Return the set of domain points where the output of this and other are ordered lexicographically acco...
ArrayRef< DynamicAPInt > getOutputExpr(unsigned i) const
Get the i^th output expression.
Definition: PWMAFunction.h:70
SmallVector< DynamicAPInt, 8 > valueAt(ArrayRef< DynamicAPInt > point) const
void mergeDivs(MultiAffineFunction &other)
Given a MAF other, merges division variables such that both functions have the union of the division ...
IntegerRelation getAsRelation() const
Get this function as a relation.
bool isEqual(const MultiAffineFunction &other) const
Return whether the this and other are equal when the domain is restricted to domain.
This class represents a piece-wise MultiAffineFunction.
Definition: PWMAFunction.h:153
const PresburgerSpace & getSpace() const
Definition: PWMAFunction.h:170
void addPiece(const Piece &piece)
unsigned getNumDomainVars() const
Definition: PWMAFunction.h:179
void print(raw_ostream &os) const
PWMAFunction unionLexMax(const PWMAFunction &func)
void removeOutputs(unsigned start, unsigned end)
Remove the specified range of outputs.
unsigned getNumOutputs() const
Definition: PWMAFunction.h:180
PWMAFunction unionLexMin(const PWMAFunction &func)
Return a function defined on the union of the domains of this and func, such that when only one of th...
std::optional< SmallVector< DynamicAPInt, 8 > > valueAt(ArrayRef< DynamicAPInt > point) const
Return the output of the function at the given point.
PresburgerSet getDomain() const
Return the domain of this piece-wise MultiAffineFunction.
PresburgerSpace getDomainSpace() const
Get the domain/output space of the function.
Definition: PWMAFunction.h:188
unsigned getNumSymbolVars() const
Definition: PWMAFunction.h:181
bool isEqual(const PWMAFunction &other) const
Return whether this and other are equal as PWMAFunctions, i.e.
void unionInPlace(const IntegerRelation &disjunct)
Mutate this set, turning it into the union of this set and the given disjunct.
ArrayRef< IntegerRelation > getAllDisjuncts() const
Return a reference to the list of disjuncts.
PresburgerSet intersect(const PresburgerRelation &set) const
static PresburgerSet getEmpty(const PresburgerSpace &space)
Return an empty set of the specified type that contains no points.
PresburgerSpace is the space of all possible values of a tuple of integer valued variables/variables.
void removeVarRange(VarKind kind, unsigned varStart, unsigned varLimit)
Removes variables of the specified kind in the column range [varStart, varLimit).
bool isCompatible(const PresburgerSpace &other) const
Returns true if both the spaces are compatible i.e.
void print(llvm::raw_ostream &os) const
PresburgerSpace getSpaceWithoutLocals() const
Get the space without local variables.
static PresburgerSpace getRelationSpace(unsigned numDomain=0, unsigned numRange=0, unsigned numSymbols=0, unsigned numLocals=0)
unsigned insertVar(VarKind kind, unsigned pos, unsigned num=1)
Insert num variables of the specified kind at position pos.
OrderingKind
Enum representing a binary comparison operator: equal, not equal, less than, less than or equal,...
Definition: PWMAFunction.h:28
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 ...
Definition: Utils.cpp:316
SmallVector< DynamicAPInt, 8 > getDivLowerBound(ArrayRef< DynamicAPInt > dividend, const DynamicAPInt &divisor, unsigned localVarIdx)
Definition: Utils.cpp:328
Include the generated interface declarations.
Eliminates variable at the specified position using Fourier-Motzkin variable elimination.