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