1 //===- SDBM.cpp - MLIR SDBM implementation --------------------------------===//
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 // A striped difference-bound matrix (SDBM) is a set in Z^N (or R^N) defined
10 // as {(x_1, ... x_n) | f(x_1, ... x_n) >= 0} where f is an SDBM expression.
11 //
12 //===----------------------------------------------------------------------===//
13
14 #include "mlir/Dialect/SDBM/SDBM.h"
15 #include "mlir/Dialect/SDBM/SDBMExpr.h"
16
17 #include "llvm/ADT/DenseMap.h"
18 #include "llvm/ADT/SetVector.h"
19 #include "llvm/Support/FormatVariadic.h"
20 #include "llvm/Support/raw_ostream.h"
21
22 using namespace mlir;
23
24 // Helper function for SDBM construction that collects information necessary to
25 // start building an SDBM in one sweep. In particular, it records the largest
26 // position of a dimension in `dim`, that of a symbol in `symbol` as well as
27 // collects all unique stripe expressions in `stripes`. Uses SetVector to
28 // ensure these expressions always have the same order.
collectSDBMBuildInfo(SDBMExpr expr,int & dim,int & symbol,llvm::SmallSetVector<SDBMExpr,8> & stripes)29 static void collectSDBMBuildInfo(SDBMExpr expr, int &dim, int &symbol,
30 llvm::SmallSetVector<SDBMExpr, 8> &stripes) {
31 struct Visitor : public SDBMVisitor<Visitor> {
32 void visitDim(SDBMDimExpr dimExpr) {
33 int p = dimExpr.getPosition();
34 if (p > maxDimPosition)
35 maxDimPosition = p;
36 }
37 void visitSymbol(SDBMSymbolExpr symbExpr) {
38 int p = symbExpr.getPosition();
39 if (p > maxSymbPosition)
40 maxSymbPosition = p;
41 }
42 void visitStripe(SDBMStripeExpr stripeExpr) { stripes.insert(stripeExpr); }
43
44 Visitor(llvm::SmallSetVector<SDBMExpr, 8> &stripes) : stripes(stripes) {}
45
46 int maxDimPosition = -1;
47 int maxSymbPosition = -1;
48 llvm::SmallSetVector<SDBMExpr, 8> &stripes;
49 };
50
51 Visitor visitor(stripes);
52 visitor.walkPostorder(expr);
53 dim = std::max(dim, visitor.maxDimPosition);
54 symbol = std::max(symbol, visitor.maxSymbPosition);
55 }
56
57 namespace {
58 // Utility class for SDBMBuilder. Represents a value that can be inserted in
59 // the SDB matrix that corresponds to "v0 - v1 + C <= 0", where v0 and v1 is
60 // any combination of the positive and negative positions. Since multiple
61 // variables can be declared equal to the same stripe expression, the
62 // constraints on this expression must be reflected to all these variables. For
63 // example, if
64 // d0 = s0 # 42
65 // d1 = s0 # 42
66 // d2 = s1 # 2
67 // d3 = s1 # 2
68 // the constraint
69 // s0 # 42 - s1 # 2 <= C
70 // should be reflected in the DB matrix as
71 // d0 - d2 <= C
72 // d1 - d2 <= C
73 // d0 - d3 <= C
74 // d1 - d3 <= C
75 // since the DB matrix has no knowledge of the transitive equality between d0,
76 // d1 and s0 # 42 as well as between d2, d3 and s1 # 2. This knowledge can be
77 // obtained by computing a transitive closure, which is impossible until the
78 // DBM is actually built.
79 struct SDBMBuilderResult {
80 // Positions in the matrix of the variables taken with the "+" sign in the
81 // difference expression, 0 if it is a constant rather than a variable.
82 SmallVector<unsigned, 2> positivePos;
83
84 // Positions in the matrix of the variables taken with the "-" sign in the
85 // difference expression, 0 if it is a constant rather than a variable.
86 SmallVector<unsigned, 2> negativePos;
87
88 // Constant value in the difference expression.
89 int64_t value = 0;
90 };
91
92 // Visitor for building an SDBM from SDBM expressions. After traversing an SDBM
93 // expression, produces an update to the SDB matrix specifying the positions in
94 // the matrix and the negated value that should be stored. Both the positive
95 // and the negative positions may be lists of indices in cases where multiple
96 // variables are equal to the same stripe expression. In such cases, the update
97 // applies to the cross product of positions because elements involved in the
98 // update are (transitively) equal and should have the same constraints, but we
99 // may not have an explicit equality for them.
100 struct SDBMBuilder : public SDBMVisitor<SDBMBuilder, SDBMBuilderResult> {
101 public:
102 // A difference expression produces both the positive and the negative
103 // coordinate in the matrix, recursively traversing the LHS and the RHS. The
104 // value is the difference between values obtained from LHS and RHS.
visitDiff__anon05fb83b90111::SDBMBuilder105 SDBMBuilderResult visitDiff(SDBMDiffExpr diffExpr) {
106 auto lhs = visit(diffExpr.getLHS());
107 auto rhs = visit(diffExpr.getRHS());
108 assert(lhs.negativePos.size() == 1 && lhs.negativePos[0] == 0 &&
109 "unexpected negative expression in a difference expression");
110 assert(rhs.negativePos.size() == 1 && lhs.negativePos[0] == 0 &&
111 "unexpected negative expression in a difference expression");
112
113 SDBMBuilderResult result;
114 result.positivePos = lhs.positivePos;
115 result.negativePos = rhs.positivePos;
116 result.value = lhs.value - rhs.value;
117 return result;
118 }
119
120 // An input expression is always taken with the "+" sign and therefore
121 // produces a positive coordinate keeping the negative coordinate zero for an
122 // eventual constant.
visitInput__anon05fb83b90111::SDBMBuilder123 SDBMBuilderResult visitInput(SDBMInputExpr expr) {
124 SDBMBuilderResult r;
125 r.positivePos.push_back(linearPosition(expr));
126 r.negativePos.push_back(0);
127 return r;
128 }
129
130 // A stripe expression is always equal to one or more variables, which may be
131 // temporaries, and appears with a "+" sign in the SDBM expression tree. Take
132 // the positions of the corresponding variables as positive coordinates.
visitStripe__anon05fb83b90111::SDBMBuilder133 SDBMBuilderResult visitStripe(SDBMStripeExpr expr) {
134 SDBMBuilderResult r;
135 assert(pointExprToStripe.count(expr));
136 r.positivePos = pointExprToStripe[expr];
137 r.negativePos.push_back(0);
138 return r;
139 }
140
141 // A constant expression has both coordinates at zero.
visitConstant__anon05fb83b90111::SDBMBuilder142 SDBMBuilderResult visitConstant(SDBMConstantExpr expr) {
143 SDBMBuilderResult r;
144 r.positivePos.push_back(0);
145 r.negativePos.push_back(0);
146 r.value = expr.getValue();
147 return r;
148 }
149
150 // A negation expression swaps the positive and the negative coordinates
151 // and also negates the constant value.
visitNeg__anon05fb83b90111::SDBMBuilder152 SDBMBuilderResult visitNeg(SDBMNegExpr expr) {
153 SDBMBuilderResult result = visit(expr.getVar());
154 std::swap(result.positivePos, result.negativePos);
155 result.value = -result.value;
156 return result;
157 }
158
159 // The RHS of a sum expression must be a constant and therefore must have both
160 // positive and negative coordinates at zero. Take the sum of the values
161 // between LHS and RHS and keep LHS coordinates.
visitSum__anon05fb83b90111::SDBMBuilder162 SDBMBuilderResult visitSum(SDBMSumExpr expr) {
163 auto lhs = visit(expr.getLHS());
164 auto rhs = visit(expr.getRHS());
165 for (auto pos : rhs.negativePos) {
166 (void)pos;
167 assert(pos == 0 && "unexpected variable on the RHS of SDBM sum");
168 }
169 for (auto pos : rhs.positivePos) {
170 (void)pos;
171 assert(pos == 0 && "unexpected variable on the RHS of SDBM sum");
172 }
173
174 lhs.value += rhs.value;
175 return lhs;
176 }
177
SDBMBuilder__anon05fb83b90111::SDBMBuilder178 SDBMBuilder(DenseMap<SDBMExpr, SmallVector<unsigned, 2>> &pointExprToStripe,
179 function_ref<unsigned(SDBMInputExpr)> callback)
180 : pointExprToStripe(pointExprToStripe), linearPosition(callback) {}
181
182 DenseMap<SDBMExpr, SmallVector<unsigned, 2>> &pointExprToStripe;
183 function_ref<unsigned(SDBMInputExpr)> linearPosition;
184 };
185 } // namespace
186
get(ArrayRef<SDBMExpr> inequalities,ArrayRef<SDBMExpr> equalities)187 SDBM SDBM::get(ArrayRef<SDBMExpr> inequalities, ArrayRef<SDBMExpr> equalities) {
188 SDBM result;
189
190 // TODO: consider detecting equalities in the list of inequalities.
191 // This is potentially expensive and requires to
192 // - create a list of negated inequalities (may allocate under lock);
193 // - perform a pairwise comparison of direct and negated inequalities;
194 // - copy the lists of equalities and inequalities, and move entries between
195 // them;
196 // only for the purpose of sparing a temporary variable in cases where an
197 // implicit equality between a variable and a stripe expression is present in
198 // the input.
199
200 // Do the first sweep over (in)equalities to collect the information necessary
201 // to allocate the SDB matrix (number of dimensions, symbol and temporary
202 // variables required for stripe expressions).
203 llvm::SmallSetVector<SDBMExpr, 8> stripes;
204 int maxDim = -1;
205 int maxSymbol = -1;
206 for (auto expr : inequalities)
207 collectSDBMBuildInfo(expr, maxDim, maxSymbol, stripes);
208 for (auto expr : equalities)
209 collectSDBMBuildInfo(expr, maxDim, maxSymbol, stripes);
210 // Indexing of dimensions starts with 0, obtain the number of dimensions by
211 // incrementing the maximal position of the dimension seen in expressions.
212 result.numDims = maxDim + 1;
213 result.numSymbols = maxSymbol + 1;
214 result.numTemporaries = 0;
215
216 // Helper function that returns the position of the variable represented by
217 // an SDBM input expression.
218 auto linearPosition = [result](SDBMInputExpr expr) {
219 if (expr.isa<SDBMDimExpr>())
220 return result.getDimPosition(expr.getPosition());
221 return result.getSymbolPosition(expr.getPosition());
222 };
223
224 // Check if some stripe expressions are equal to another variable. In
225 // particular, look for the equalities of the form
226 // d0 - stripe-expression = 0, or
227 // stripe-expression - d0 = 0.
228 // There may be multiple variables that are equal to the same stripe
229 // expression. Keep track of those in pointExprToStripe.
230 // There may also be multiple stripe expressions equal to the same variable.
231 // Introduce a temporary variable for each of those.
232 DenseMap<SDBMExpr, SmallVector<unsigned, 2>> pointExprToStripe;
233 unsigned numTemporaries = 0;
234
235 auto updateStripePointMaps = [&numTemporaries, &result, &pointExprToStripe,
236 linearPosition](SDBMInputExpr input,
237 SDBMExpr expr) {
238 unsigned position = linearPosition(input);
239 if (result.stripeToPoint.count(position) &&
240 result.stripeToPoint[position] != expr) {
241 position = result.getNumVariables() + numTemporaries++;
242 }
243 pointExprToStripe[expr].push_back(position);
244 result.stripeToPoint.insert(std::make_pair(position, expr));
245 };
246
247 for (auto eq : equalities) {
248 auto diffExpr = eq.dyn_cast<SDBMDiffExpr>();
249 if (!diffExpr)
250 continue;
251
252 auto lhs = diffExpr.getLHS();
253 auto rhs = diffExpr.getRHS();
254 auto lhsInput = lhs.dyn_cast<SDBMInputExpr>();
255 auto rhsInput = rhs.dyn_cast<SDBMInputExpr>();
256
257 if (lhsInput && stripes.count(rhs))
258 updateStripePointMaps(lhsInput, rhs);
259 if (rhsInput && stripes.count(lhs))
260 updateStripePointMaps(rhsInput, lhs);
261 }
262
263 // Assign the remaining stripe expressions to temporary variables. These
264 // expressions are the ones that could not be associated with an existing
265 // variable in the previous step.
266 for (auto expr : stripes) {
267 if (pointExprToStripe.count(expr))
268 continue;
269 unsigned position = result.getNumVariables() + numTemporaries++;
270 pointExprToStripe[expr].push_back(position);
271 result.stripeToPoint.insert(std::make_pair(position, expr));
272 }
273
274 // Create the DBM matrix, initialized to infinity values for the least tight
275 // possible bound (x - y <= infinity is always true).
276 result.numTemporaries = numTemporaries;
277 result.matrix.resize(result.getNumVariables() * result.getNumVariables(),
278 IntInfty::infinity());
279
280 SDBMBuilder builder(pointExprToStripe, linearPosition);
281
282 // Only keep the tightest constraint. Since we transform everything into
283 // less-than-or-equals-to inequalities, keep the smallest constant. For
284 // example, if we have d0 - d1 <= 42 and d0 - d1 <= 2, we keep the latter.
285 // Note that the input expressions are in the shape of d0 - d1 + -42 <= 0
286 // so we negate the value before storing it.
287 // In case where the positive and the negative positions are equal, the
288 // corresponding expression has the form d0 - d0 + -42 <= 0. If the constant
289 // value is positive, the set defined by SDBM is trivially empty. We store
290 // this value anyway and continue processing to maintain the correspondence
291 // between the matrix form and the list-of-SDBMExpr form.
292 // TODO: we may want to reconsider this once we have canonicalization
293 // or simplification in place
294 auto updateMatrix = [](SDBM &sdbm, const SDBMBuilderResult &r) {
295 for (auto positivePos : r.positivePos) {
296 for (auto negativePos : r.negativePos) {
297 auto &m = sdbm.at(negativePos, positivePos);
298 m = m < -r.value ? m : -r.value;
299 }
300 }
301 };
302
303 // Do the second sweep on (in)equalities, updating the SDB matrix to reflect
304 // the constraints.
305 for (auto ineq : inequalities)
306 updateMatrix(result, builder.visit(ineq));
307
308 // An equality f(x) = 0 is represented as a pair of inequalities {f(x) >= 0;
309 // f(x) <= 0} or, alternatively, {-f(x) <= 0 and f(x) <= 0}.
310 for (auto eq : equalities) {
311 updateMatrix(result, builder.visit(eq));
312 updateMatrix(result, builder.visit(-eq));
313 }
314
315 // Add the inequalities induced by stripe equalities.
316 // t = x # C => t <= x <= t + C - 1
317 // which is equivalent to
318 // {t - x <= 0;
319 // x - t - (C - 1) <= 0}.
320 for (const auto &pair : result.stripeToPoint) {
321 auto stripe = pair.second.cast<SDBMStripeExpr>();
322 SDBMBuilderResult update = builder.visit(stripe.getLHS());
323 assert(update.negativePos.size() == 1 && update.negativePos[0] == 0 &&
324 "unexpected negated variable in stripe expression");
325 assert(update.value == 0 &&
326 "unexpected non-zero value in stripe expression");
327 update.negativePos.clear();
328 update.negativePos.push_back(pair.first);
329 update.value = -(stripe.getStripeFactor().getValue() - 1);
330 updateMatrix(result, update);
331
332 std::swap(update.negativePos, update.positivePos);
333 update.value = 0;
334 updateMatrix(result, update);
335 }
336
337 return result;
338 }
339
340 // Given a row and a column position in the square DBM, insert one equality
341 // or up to two inequalities that correspond the entries (col, row) and (row,
342 // col) in the DBM. `rowExpr` and `colExpr` contain the expressions such that
343 // colExpr - rowExpr <= V where V is the value at (row, col) in the DBM.
344 // If one of the expressions is derived from another using a stripe operation,
345 // check if the inequalities induced by the stripe operation subsume the
346 // inequalities defined in the DBM and if so, elide these inequalities.
convertDBMElement(unsigned row,unsigned col,SDBMTermExpr rowExpr,SDBMTermExpr colExpr,SmallVectorImpl<SDBMExpr> & inequalities,SmallVectorImpl<SDBMExpr> & equalities)347 void SDBM::convertDBMElement(unsigned row, unsigned col, SDBMTermExpr rowExpr,
348 SDBMTermExpr colExpr,
349 SmallVectorImpl<SDBMExpr> &inequalities,
350 SmallVectorImpl<SDBMExpr> &equalities) {
351 using ops_assertions::operator+;
352 using ops_assertions::operator-;
353
354 auto diffIJValue = at(col, row);
355 auto diffJIValue = at(row, col);
356
357 // If symmetric entries are opposite, the corresponding expressions are equal.
358 if (diffIJValue.isFinite() &&
359 diffIJValue.getValue() == -diffJIValue.getValue()) {
360 equalities.push_back(rowExpr - colExpr - diffIJValue.getValue());
361 return;
362 }
363
364 // Given an inequality x0 - x1 <= A, check if x0 is a stripe variable derived
365 // from x1: x0 = x1 # B. If so, it would imply the constraints
366 // x0 <= x1 <= x0 + (B - 1) <=> x0 - x1 <= 0 and x1 - x0 <= (B - 1).
367 // Therefore, if A >= 0, this inequality is subsumed by that implied
368 // by the stripe equality and thus can be elided.
369 // Similarly, check if x1 is a stripe variable derived from x0: x1 = x0 # C.
370 // If so, it would imply the constraints x1 <= x0 <= x1 + (C - 1) <=>
371 // <=> x1 - x0 <= 0 and x0 - x1 <= (C - 1). Therefore, if A >= (C - 1), this
372 // inequality can be elided.
373 //
374 // Note: x0 and x1 may be a stripe expressions themselves, we rely on stripe
375 // expressions being stored without temporaries on the RHS and being passed
376 // into this function as is.
377 auto canElide = [this](unsigned x0, unsigned x1, SDBMExpr x0Expr,
378 SDBMExpr x1Expr, int64_t value) {
379 if (stripeToPoint.count(x0)) {
380 auto stripe = stripeToPoint[x0].cast<SDBMStripeExpr>();
381 SDBMDirectExpr var = stripe.getLHS();
382 if (x1Expr == var && value >= 0)
383 return true;
384 }
385 if (stripeToPoint.count(x1)) {
386 auto stripe = stripeToPoint[x1].cast<SDBMStripeExpr>();
387 SDBMDirectExpr var = stripe.getLHS();
388 if (x0Expr == var && value >= stripe.getStripeFactor().getValue() - 1)
389 return true;
390 }
391 return false;
392 };
393
394 // Check row - col.
395 if (diffIJValue.isFinite() &&
396 !canElide(row, col, rowExpr, colExpr, diffIJValue.getValue())) {
397 inequalities.push_back(rowExpr - colExpr - diffIJValue.getValue());
398 }
399 // Check col - row.
400 if (diffJIValue.isFinite() &&
401 !canElide(col, row, colExpr, rowExpr, diffJIValue.getValue())) {
402 inequalities.push_back(colExpr - rowExpr - diffJIValue.getValue());
403 }
404 }
405
406 // The values on the main diagonal correspond to the upper bound on the
407 // difference between a variable and itself: d0 - d0 <= C, or alternatively
408 // to -C <= 0. Only construct the inequalities when C is negative, which
409 // are trivially false but necessary for the returned system of inequalities
410 // to indicate that the set it defines is empty.
convertDBMDiagonalElement(unsigned pos,SDBMTermExpr expr,SmallVectorImpl<SDBMExpr> & inequalities)411 void SDBM::convertDBMDiagonalElement(unsigned pos, SDBMTermExpr expr,
412 SmallVectorImpl<SDBMExpr> &inequalities) {
413 auto selfDifference = at(pos, pos);
414 if (selfDifference.isFinite() && selfDifference < 0) {
415 auto selfDifferenceValueExpr =
416 SDBMConstantExpr::get(expr.getDialect(), -selfDifference.getValue());
417 inequalities.push_back(selfDifferenceValueExpr);
418 }
419 }
420
getSDBMExpressions(SDBMDialect * dialect,SmallVectorImpl<SDBMExpr> & inequalities,SmallVectorImpl<SDBMExpr> & equalities)421 void SDBM::getSDBMExpressions(SDBMDialect *dialect,
422 SmallVectorImpl<SDBMExpr> &inequalities,
423 SmallVectorImpl<SDBMExpr> &equalities) {
424 using ops_assertions::operator-;
425 using ops_assertions::operator+;
426
427 // Helper function that creates an SDBMInputExpr given the linearized position
428 // of variable in the DBM.
429 auto getInput = [dialect, this](unsigned matrixPos) -> SDBMInputExpr {
430 if (matrixPos < numDims)
431 return SDBMDimExpr::get(dialect, matrixPos);
432 return SDBMSymbolExpr::get(dialect, matrixPos - numDims);
433 };
434
435 // The top-left value corresponds to inequality 0 <= C. If C is negative, the
436 // set defined by SDBM is trivially empty and we add the constraint -C <= 0 to
437 // the list of inequalities. Otherwise, the constraint is trivially true and
438 // we ignore it.
439 auto difference = at(0, 0);
440 if (difference.isFinite() && difference < 0) {
441 inequalities.push_back(
442 SDBMConstantExpr::get(dialect, -difference.getValue()));
443 }
444
445 // Traverse the segment of the matrix that involves non-temporary variables.
446 unsigned numTrueVariables = numDims + numSymbols;
447 for (unsigned i = 0; i < numTrueVariables; ++i) {
448 // The first row and column represent numerical upper and lower bound on
449 // each variable. Transform them into inequalities if they are finite.
450 auto upperBound = at(0, 1 + i);
451 auto lowerBound = at(1 + i, 0);
452 auto inputExpr = getInput(i);
453 if (upperBound.isFinite() &&
454 upperBound.getValue() == -lowerBound.getValue()) {
455 equalities.push_back(inputExpr - upperBound.getValue());
456 } else if (upperBound.isFinite()) {
457 inequalities.push_back(inputExpr - upperBound.getValue());
458 } else if (lowerBound.isFinite()) {
459 inequalities.push_back(-inputExpr - lowerBound.getValue());
460 }
461
462 // Introduce trivially false inequalities if required by diagonal elements.
463 convertDBMDiagonalElement(1 + i, inputExpr, inequalities);
464
465 // Introduce equalities or inequalities between non-temporary variables.
466 for (unsigned j = 0; j < i; ++j) {
467 convertDBMElement(1 + i, 1 + j, getInput(i), getInput(j), inequalities,
468 equalities);
469 }
470 }
471
472 // Add equalities for stripe expressions that define non-temporary
473 // variables. Temporary variables will be substituted into their uses and
474 // should not appear in the resulting equalities.
475 for (const auto &stripePair : stripeToPoint) {
476 unsigned position = stripePair.first;
477 if (position < 1 + numTrueVariables) {
478 equalities.push_back(getInput(position - 1) - stripePair.second);
479 }
480 }
481
482 // Add equalities / inequalities involving temporaries by replacing the
483 // temporaries with stripe expressions that define them.
484 for (unsigned i = 1 + numTrueVariables, e = getNumVariables(); i < e; ++i) {
485 // Mixed constraints involving one temporary (j) and one non-temporary (i)
486 // variable.
487 for (unsigned j = 0; j < numTrueVariables; ++j) {
488 convertDBMElement(i, 1 + j, stripeToPoint[i].cast<SDBMStripeExpr>(),
489 getInput(j), inequalities, equalities);
490 }
491
492 // Constraints involving only temporary variables.
493 for (unsigned j = 1 + numTrueVariables; j < i; ++j) {
494 convertDBMElement(i, j, stripeToPoint[i].cast<SDBMStripeExpr>(),
495 stripeToPoint[j].cast<SDBMStripeExpr>(), inequalities,
496 equalities);
497 }
498
499 // Introduce trivially false inequalities if required by diagonal elements.
500 convertDBMDiagonalElement(i, stripeToPoint[i].cast<SDBMStripeExpr>(),
501 inequalities);
502 }
503 }
504
print(raw_ostream & os)505 void SDBM::print(raw_ostream &os) {
506 unsigned numVariables = getNumVariables();
507
508 // Helper function that prints the name of the variable given its linearized
509 // position in the DBM.
510 auto getVarName = [this](unsigned matrixPos) -> std::string {
511 if (matrixPos == 0)
512 return "cst";
513 matrixPos -= 1;
514 if (matrixPos < numDims)
515 return std::string(llvm::formatv("d{0}", matrixPos));
516 matrixPos -= numDims;
517 if (matrixPos < numSymbols)
518 return std::string(llvm::formatv("s{0}", matrixPos));
519 matrixPos -= numSymbols;
520 return std::string(llvm::formatv("t{0}", matrixPos));
521 };
522
523 // Header row.
524 os << " cst";
525 for (unsigned i = 1; i < numVariables; ++i) {
526 os << llvm::formatv(" {0,4}", getVarName(i));
527 }
528 os << '\n';
529
530 // Data rows.
531 for (unsigned i = 0; i < numVariables; ++i) {
532 os << llvm::formatv("{0,-4}", getVarName(i));
533 for (unsigned j = 0; j < numVariables; ++j) {
534 IntInfty value = operator()(i, j);
535 if (!value.isFinite())
536 os << " inf";
537 else
538 os << llvm::formatv(" {0,4}", value.getValue());
539 }
540 os << '\n';
541 }
542
543 // Explanation of temporaries.
544 for (const auto &pair : stripeToPoint) {
545 os << getVarName(pair.first) << " = ";
546 pair.second.print(os);
547 os << '\n';
548 }
549 }
550
dump()551 void SDBM::dump() { print(llvm::errs()); }
552