MLIR  20.0.0git
Simplex.h
Go to the documentation of this file.
1 //===- Simplex.h - MLIR Simplex Class ---------------------------*- C++ -*-===//
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 // Functionality to perform analysis on an IntegerRelation. In particular,
10 // support for performing emptiness checks, redundancy checks and obtaining the
11 // lexicographically minimum rational element in a set.
12 //
13 //===----------------------------------------------------------------------===//
14 
15 #ifndef MLIR_ANALYSIS_PRESBURGER_SIMPLEX_H
16 #define MLIR_ANALYSIS_PRESBURGER_SIMPLEX_H
17 
23 #include "llvm/ADT/SmallBitVector.h"
24 #include <optional>
25 
26 namespace mlir {
27 namespace presburger {
28 
29 class GBRSimplex;
30 
31 /// The Simplex class implements a version of the Simplex and Generalized Basis
32 /// Reduction algorithms, which can perform analysis of integer sets with affine
33 /// inequalities and equalities. A Simplex can be constructed
34 /// by specifying the dimensionality of the set. It supports adding affine
35 /// inequalities and equalities, and can perform emptiness checks, i.e., it can
36 /// find a solution to the set of constraints if one exists, or say that the
37 /// set is empty if no solution exists. Furthermore, it can find a subset of
38 /// these constraints that are redundant, i.e. a subset of constraints that
39 /// doesn't constrain the affine set further after adding the non-redundant
40 /// constraints. The LexSimplex class provides support for computing the
41 /// lexicographic minimum of an IntegerRelation. The SymbolicLexOpt class
42 /// provides support for computing symbolic lexicographic minimums. All of these
43 /// classes can be constructed from an IntegerRelation, and all inherit common
44 /// functionality from SimplexBase.
45 ///
46 /// The implementations of the Simplex and SimplexBase classes, other than the
47 /// functionality for obtaining an integer sample, are based on the paper
48 /// "Simplify: A Theorem Prover for Program Checking"
49 /// by D. Detlefs, G. Nelson, J. B. Saxe.
50 ///
51 /// We define variables, constraints, and unknowns. Consider the example of a
52 /// two-dimensional set defined by 1 + 2x + 3y >= 0 and 2x - 3y >= 0. Here,
53 /// x, y, are variables while 1 + 2x + 3y >= 0, 2x - 3y >= 0 are constraints.
54 /// Unknowns are either variables or constraints, i.e., x, y, 1 + 2x + 3y >= 0,
55 /// 2x - 3y >= 0 are all unknowns.
56 ///
57 /// The implementation involves a matrix called a tableau, which can be thought
58 /// of as a 2D matrix of rational numbers having number of rows equal to the
59 /// number of constraints and number of columns equal to one plus the number of
60 /// variables. In our implementation, instead of storing rational numbers, we
61 /// store a common denominator for each row, so it is in fact a matrix of
62 /// integers with number of rows equal to number of constraints and number of
63 /// columns equal to _two_ plus the number of variables. For example, instead of
64 /// storing a row of three rationals [1/2, 2/3, 3], we would store [6, 3, 4, 18]
65 /// since 3/6 = 1/2, 4/6 = 2/3, and 18/6 = 3.
66 ///
67 /// Every row and column except the first and second columns is associated with
68 /// an unknown and every unknown is associated with a row or column. An unknown
69 /// associated with a row or column is said to be in row or column orientation
70 /// respectively. As described above, the first column is the common
71 /// denominator. The second column represents the constant term, explained in
72 /// more detail below. These two are _fixed columns_; they always retain their
73 /// position as the first and second columns. Additionally, LexSimplexBase
74 /// stores a so-call big M parameter (explained below) in the third column, so
75 /// LexSimplexBase has three fixed columns. Finally, SymbolicLexSimplex has
76 /// `nSymbol` variables designated as symbols. These occupy the next `nSymbol`
77 /// columns, viz. the columns [3, 3 + nSymbol). For more information on symbols,
78 /// see LexSimplexBase and SymbolicLexSimplex.
79 ///
80 /// LexSimplexBase does not directly support variables which can be negative, so
81 /// we introduce the so-called big M parameter, an artificial variable that is
82 /// considered to have an arbitrarily large value. We then transform the
83 /// variables, say x, y, z, ... to M, M + x, M + y, M + z. Since M has been
84 /// added to these variables, they are now known to have non-negative values.
85 /// For more details, see the documentation for LexSimplexBase. The big M
86 /// parameter is not considered a real unknown and is not stored in the `var`
87 /// data structure; rather the tableau just has an extra fixed column for it
88 /// just like the constant term.
89 ///
90 /// The vectors var and con store information about the variables and
91 /// constraints respectively, namely, whether they are in row or column
92 /// position, which row or column they are associated with, and whether they
93 /// correspond to a variable or a constraint.
94 ///
95 /// An unknown is addressed by its index. If the index i is non-negative, then
96 /// the variable var[i] is being addressed. If the index i is negative, then
97 /// the constraint con[~i] is being addressed. Effectively this maps
98 /// 0 -> var[0], 1 -> var[1], -1 -> con[0], -2 -> con[1], etc. rowUnknown[r] and
99 /// colUnknown[c] are the indexes of the unknowns associated with row r and
100 /// column c, respectively.
101 ///
102 /// The unknowns in column position are together called the basis. Initially the
103 /// basis is the set of variables -- in our example above, the initial basis is
104 /// x, y.
105 ///
106 /// The unknowns in row position are represented in terms of the basis unknowns.
107 /// If the basis unknowns are u_1, u_2, ... u_m, and a row in the tableau is
108 /// d, c, a_1, a_2, ... a_m, this represents the unknown for that row as
109 /// (c + a_1*u_1 + a_2*u_2 + ... + a_m*u_m)/d. In our running example, if the
110 /// basis is the initial basis of x, y, then the constraint 1 + 2x + 3y >= 0
111 /// would be represented by the row [1, 1, 2, 3].
112 ///
113 /// The association of unknowns to rows and columns can be changed by a process
114 /// called pivoting, where a row unknown and a column unknown exchange places
115 /// and the remaining row variables' representation is changed accordingly
116 /// by eliminating the old column unknown in favour of the new column unknown.
117 /// If we had pivoted the column for x with the row for 2x - 3y >= 0,
118 /// the new row for x would be [2, 1, 3] since x = (1*(2x - 3y) + 3*y)/2.
119 /// See the documentation for the pivot member function for details.
120 ///
121 /// The association of unknowns to rows and columns is called the _tableau
122 /// configuration_. The _sample value_ of an unknown in a particular tableau
123 /// configuration is its value if all the column unknowns were set to zero.
124 /// Concretely, for unknowns in column position the sample value is zero; when
125 /// the big M parameter is not used, for unknowns in row position the sample
126 /// value is the constant term divided by the common denominator. When the big M
127 /// parameter is used, if d is the denominator, p is the big M coefficient, and
128 /// c is the constant term, then the sample value is (p*M + c)/d. Since M is
129 /// considered to be positive infinity, this is positive (negative) infinity
130 /// when p is positive or negative, and c/d when p is zero.
131 ///
132 /// The tableau configuration is called _consistent_ if the sample value of all
133 /// restricted unknowns is non-negative. Initially there are no constraints, and
134 /// the tableau is consistent. When a new constraint is added, its sample value
135 /// in the current tableau configuration may be negative. In that case, we try
136 /// to find a series of pivots to bring us to a consistent tableau
137 /// configuration, i.e. we try to make the new constraint's sample value
138 /// non-negative without making that of any other constraints negative. (See
139 /// findPivot and findPivotRow for details.) If this is not possible, then the
140 /// set of constraints is mutually contradictory and the tableau is marked
141 /// _empty_, which means the set of constraints has no solution.
142 ///
143 /// This SimplexBase class also supports taking snapshots of the current state
144 /// and rolling back to prior snapshots. This works by maintaining an undo log
145 /// of operations. Snapshots are just pointers to a particular location in the
146 /// log, and rolling back to a snapshot is done by reverting each log entry's
147 /// operation from the end until we reach the snapshot's location. SimplexBase
148 /// also supports taking a snapshot including the exact set of basis unknowns;
149 /// if this functionality is used, then on rolling back the exact basis will
150 /// also be restored. This is used by LexSimplexBase because the lex algorithm,
151 /// unlike `Simplex`, is sensitive to the exact basis used at a point.
152 class SimplexBase {
153 public:
154  SimplexBase() = delete;
155  virtual ~SimplexBase() = default;
156 
157  /// Returns true if the tableau is empty (has conflicting constraints),
158  /// false otherwise.
159  bool isEmpty() const;
160 
161  /// Add an inequality to the tableau. If coeffs is c_0, c_1, ... c_n, where n
162  /// is the current number of variables, then the corresponding inequality is
163  /// c_n + c_0*x_0 + c_1*x_1 + ... + c_{n-1}*x_{n-1} >= 0.
164  virtual void addInequality(ArrayRef<DynamicAPInt> coeffs) = 0;
165 
166  /// Returns the number of variables in the tableau.
167  unsigned getNumVariables() const;
168 
169  /// Returns the number of constraints in the tableau.
170  unsigned getNumConstraints() const;
171 
172  /// Add an equality to the tableau. If coeffs is c_0, c_1, ... c_n, where n
173  /// is the current number of variables, then the corresponding equality is
174  /// c_n + c_0*x_0 + c_1*x_1 + ... + c_{n-1}*x_{n-1} == 0.
175  void addEquality(ArrayRef<DynamicAPInt> coeffs);
176 
177  /// Add new variables to the end of the list of variables.
178  void appendVariable(unsigned count = 1);
179 
180  /// Append a new variable to the simplex and constrain it such that its only
181  /// integer value is the floor div of `coeffs` and `denom`.
182  ///
183  /// `denom` must be positive.
185  const DynamicAPInt &denom);
186 
187  /// Mark the tableau as being empty.
188  void markEmpty();
189 
190  /// Get a snapshot of the current state. This is used for rolling back.
191  /// The same basis will not necessarily be restored on rolling back.
192  /// The snapshot only captures the set of variables and constraints present
193  /// in the Simplex.
194  unsigned getSnapshot() const;
195 
196  /// Get a snapshot of the current state including the basis. When rolling
197  /// back, the exact basis will be restored.
198  unsigned getSnapshotBasis();
199 
200  /// Rollback to a snapshot. This invalidates all later snapshots.
201  void rollback(unsigned snapshot);
202 
203  /// Add all the constraints from the given IntegerRelation.
204  void intersectIntegerRelation(const IntegerRelation &rel);
205 
206  /// Print the tableau's internal state.
207  void print(raw_ostream &os) const;
208  void dump() const;
209 
210 protected:
211  /// Construct a SimplexBase with the specified number of variables and fixed
212  /// columns. The first overload should be used when there are nosymbols.
213  /// With the second overload, the specified range of vars will be marked
214  /// as symbols. With the third overload, `isSymbol` is a bitmask denoting
215  /// which vars are symbols. The size of `isSymbol` must be `nVar`.
216  ///
217  /// For example, Simplex uses two fixed columns: the denominator and the
218  /// constant term, whereas LexSimplex has an extra fixed column for the
219  /// so-called big M parameter. For more information see the documentation for
220  /// LexSimplex.
221  SimplexBase(unsigned nVar, bool mustUseBigM);
222  SimplexBase(unsigned nVar, bool mustUseBigM,
223  const llvm::SmallBitVector &isSymbol);
224 
225  enum class Orientation { Row, Column };
226 
227  /// An Unknown is either a variable or a constraint. It is always associated
228  /// with either a row or column. Whether it's a row or a column is specified
229  /// by the orientation and pos identifies the specific row or column it is
230  /// associated with. If the unknown is restricted, then it has a
231  /// non-negativity constraint associated with it, i.e., its sample value must
232  /// always be non-negative and if it cannot be made non-negative without
233  /// violating other constraints, the tableau is empty.
234  struct Unknown {
235  Unknown(Orientation oOrientation, bool oRestricted, unsigned oPos,
236  bool oIsSymbol = false)
237  : pos(oPos), orientation(oOrientation), restricted(oRestricted),
238  isSymbol(oIsSymbol) {}
239  unsigned pos;
241  bool restricted : 1;
242  bool isSymbol : 1;
243 
244  void print(raw_ostream &os) const {
245  os << (orientation == Orientation::Row ? "r" : "c");
246  os << pos;
247  if (restricted)
248  os << " [>=0]";
249  }
250  };
251 
252  struct Pivot {
253  unsigned row, column;
254  };
255 
256  /// Return any row that this column can be pivoted with, ignoring tableau
257  /// consistency.
258  ///
259  /// Returns an empty optional if no pivot is possible, which happens only when
260  /// the column unknown is a variable and no constraint has a non-zero
261  /// coefficient for it.
262  std::optional<unsigned> findAnyPivotRow(unsigned col);
263 
264  /// Swap the row with the column in the tableau's data structures but not the
265  /// tableau itself. This is used by pivot.
266  void swapRowWithCol(unsigned row, unsigned col);
267 
268  /// Pivot the row with the column.
269  void pivot(unsigned row, unsigned col);
270  void pivot(Pivot pair);
271 
272  /// Returns the unknown associated with index.
273  const Unknown &unknownFromIndex(int index) const;
274  /// Returns the unknown associated with col.
275  const Unknown &unknownFromColumn(unsigned col) const;
276  /// Returns the unknown associated with row.
277  const Unknown &unknownFromRow(unsigned row) const;
278  /// Returns the unknown associated with index.
279  Unknown &unknownFromIndex(int index);
280  /// Returns the unknown associated with col.
281  Unknown &unknownFromColumn(unsigned col);
282  /// Returns the unknown associated with row.
283  Unknown &unknownFromRow(unsigned row);
284 
285  /// Add a new row to the tableau and the associated data structures. The row
286  /// is initialized to zero. Returns the index of the added row.
287  unsigned addZeroRow(bool makeRestricted = false);
288 
289  /// Add a new row to the tableau and the associated data structures.
290  /// The new row is considered to be a constraint; the new Unknown lives in
291  /// con.
292  ///
293  /// Returns the index of the new Unknown in con.
294  unsigned addRow(ArrayRef<DynamicAPInt> coeffs, bool makeRestricted = false);
295 
296  /// Swap the two rows/columns in the tableau and associated data structures.
297  void swapRows(unsigned i, unsigned j);
298  void swapColumns(unsigned i, unsigned j);
299 
300  /// Enum to denote operations that need to be undone during rollback.
301  enum class UndoLogEntry {
304  UnmarkEmpty,
307  };
308 
309  /// Undo the addition of the last constraint. This will only be called from
310  /// undo, when rolling back.
311  virtual void undoLastConstraint() = 0;
312 
313  /// Remove the last constraint, which must be in row orientation.
315 
316  /// Undo the operation represented by the log entry.
317  void undo(UndoLogEntry entry);
318 
319  /// Return the number of fixed columns, as described in the constructor above,
320  /// this is the number of columns beyond those for the variables in var.
321  unsigned getNumFixedCols() const { return usingBigM ? 3u : 2u; }
322  unsigned getNumRows() const { return tableau.getNumRows(); }
323  unsigned getNumColumns() const { return tableau.getNumColumns(); }
324 
325  /// Stores whether or not a big M column is present in the tableau.
326  bool usingBigM;
327 
328  /// The number of redundant rows in the tableau. These are the first
329  /// nRedundant rows.
330  unsigned nRedundant;
331 
332  /// The number of parameters. This must be consistent with the number of
333  /// Unknowns in `var` below that have `isSymbol` set to true.
334  unsigned nSymbol;
335 
336  /// The matrix representing the tableau.
338 
339  /// This is true if the tableau has been detected to be empty, false
340  /// otherwise.
341  bool empty;
342 
343  /// Holds a log of operations, used for rolling back to a previous state.
345 
346  /// Holds a vector of bases. The ith saved basis is the basis that should be
347  /// restored when processing the ith occurrance of UndoLogEntry::RestoreBasis
348  /// in undoLog. This is used by getSnapshotBasis.
350 
351  /// These hold the indexes of the unknown at a given row or column position.
352  /// We keep these as signed integers since that makes it convenient to check
353  /// if an index corresponds to a variable or a constraint by checking the
354  /// sign.
355  ///
356  /// colUnknown is padded with two null indexes at the front since the first
357  /// two columns don't correspond to any unknowns.
359 
360  /// These hold information about each unknown.
362 };
363 
364 /// Simplex class using the lexicographic pivot rule. Used for lexicographic
365 /// optimization. The implementation of this class is based on the paper
366 /// "Parametric Integer Programming" by Paul Feautrier.
367 ///
368 /// This does not directly support negative-valued variables, so it uses the big
369 /// M parameter trick to make all the variables non-negative. Basically we
370 /// introduce an artifical variable M that is considered to have a value of
371 /// +infinity and instead of the variables x, y, z, we internally use variables
372 /// M + x, M + y, M + z, which are now guaranteed to be non-negative. See the
373 /// documentation for SimplexBase for more details. M is also considered to be
374 /// an integer that is divisible by everything.
375 ///
376 /// The whole algorithm is performed with M treated as a symbol;
377 /// it is just considered to be infinite throughout and it never appears in the
378 /// final outputs. We will deal with sample values throughout that may in
379 /// general be some affine expression involving M, like pM + q or aM + b. We can
380 /// compare these with each other. They have a total order:
381 ///
382 /// aM + b < pM + q iff a < p or (a == p and b < q).
383 /// In particular, aM + b < 0 iff a < 0 or (a == 0 and b < 0).
384 ///
385 /// When performing symbolic optimization, sample values will be affine
386 /// expressions in M and the symbols. For example, we could have sample values
387 /// aM + bS + c and pM + qS + r, where S is a symbol. Now we have
388 /// aM + bS + c < pM + qS + r iff (a < p) or (a == p and bS + c < qS + r).
389 /// bS + c < qS + r can be always true, always false, or neither,
390 /// depending on the set of values S can take. The symbols are always stored
391 /// in columns [3, 3 + nSymbols). For more details, see the
392 /// documentation for SymbolicLexSimplex.
393 ///
394 /// Initially all the constraints to be added are added as rows, with no attempt
395 /// to keep the tableau consistent. Pivots are only performed when some query
396 /// is made, such as a call to getRationalLexMin. Care is taken to always
397 /// maintain a lexicopositive basis transform, explained below.
398 ///
399 /// Let the variables be x = (x_1, ... x_n).
400 /// Let the symbols be s = (s_1, ... s_m). Let the basis unknowns at a
401 /// particular point be y = (y_1, ... y_n). We know that x = A*y + T*s + b for
402 /// some n x n matrix A, n x m matrix s, and n x 1 column vector b. We want
403 /// every column in A to be lexicopositive, i.e., have at least one non-zero
404 /// element, with the first such element being positive. This property is
405 /// preserved throughout the operation of LexSimplexBase. Note that on
406 /// construction, the basis transform A is the identity matrix and so every
407 /// column is lexicopositive. Note that for LexSimplexBase, for the tableau to
408 /// be consistent we must have non-negative sample values not only for the
409 /// constraints but also for the variables. So if the tableau is consistent then
410 /// x >= 0 and y >= 0, by which we mean every element in these vectors is
411 /// non-negative. (note that this is a different concept from lexicopositivity!)
412 class LexSimplexBase : public SimplexBase {
413 public:
414  ~LexSimplexBase() override = default;
415 
416  /// Add an inequality to the tableau. If coeffs is c_0, c_1, ... c_n, where n
417  /// is the current number of variables, then the corresponding inequality is
418  /// c_n + c_0*x_0 + c_1*x_1 + ... + c_{n-1}*x_{n-1} >= 0.
419  ///
420  /// This just adds the inequality to the tableau and does not try to create a
421  /// consistent tableau configuration.
422  void addInequality(ArrayRef<DynamicAPInt> coeffs) final;
423 
424  /// Get a snapshot of the current state. This is used for rolling back.
426 
427 protected:
428  LexSimplexBase(unsigned nVar) : SimplexBase(nVar, /*mustUseBigM=*/true) {}
429  LexSimplexBase(unsigned nVar, const llvm::SmallBitVector &isSymbol)
430  : SimplexBase(nVar, /*mustUseBigM=*/true, isSymbol) {}
431  explicit LexSimplexBase(const IntegerRelation &constraints)
432  : LexSimplexBase(constraints.getNumVars()) {
433  intersectIntegerRelation(constraints);
434  }
435  explicit LexSimplexBase(const IntegerRelation &constraints,
436  const llvm::SmallBitVector &isSymbol)
437  : LexSimplexBase(constraints.getNumVars(), isSymbol) {
438  intersectIntegerRelation(constraints);
439  }
440 
441  /// Add new symbolic variables to the end of the list of variables.
442  void appendSymbol();
443 
444  /// Try to move the specified row to column orientation while preserving the
445  /// lexicopositivity of the basis transform. The row must have a non-positive
446  /// sample value. If this is not possible, return failure. This occurs when
447  /// the constraints have no solution or the sample value is zero.
448  LogicalResult moveRowUnknownToColumn(unsigned row);
449 
450  /// Given a row that has a non-integer sample value, add an inequality to cut
451  /// away this fractional sample value from the polytope without removing any
452  /// integer points. The integer lexmin, if one existed, remains the same on
453  /// return.
454  ///
455  /// This assumes that the symbolic part of the sample is integral,
456  /// i.e., if the symbolic sample is (c + aM + b_1*s_1 + ... b_n*s_n)/d,
457  /// where s_1, ... s_n are symbols, this assumes that
458  /// (b_1*s_1 + ... + b_n*s_n)/s is integral.
459  ///
460  /// Return failure if the tableau became empty, and success if it didn't.
461  /// Failure status indicates that the polytope was integer empty.
462  LogicalResult addCut(unsigned row);
463 
464  /// Undo the addition of the last constraint. This is only called while
465  /// rolling back.
466  void undoLastConstraint() final;
467 
468  /// Given two potential pivot columns for a row, return the one that results
469  /// in the lexicographically smallest sample vector. The row's sample value
470  /// must be negative. If symbols are involved, the sample value must be
471  /// negative for all possible assignments to the symbols.
472  unsigned getLexMinPivotColumn(unsigned row, unsigned colA,
473  unsigned colB) const;
474 };
475 
476 /// A class for lexicographic optimization without any symbols. This also
477 /// provides support for integer-exact redundancy and separateness checks.
478 class LexSimplex : public LexSimplexBase {
479 public:
480  explicit LexSimplex(unsigned nVar) : LexSimplexBase(nVar) {}
481  // Note that LexSimplex does NOT support symbolic lexmin;
482  // use SymbolicLexSimplex if that is required. LexSimplex ignores the VarKinds
483  // of the passed IntegerRelation. Symbols will be treated as ordinary vars.
484  explicit LexSimplex(const IntegerRelation &constraints)
485  : LexSimplexBase(constraints) {}
486 
487  /// Return the lexicographically minimum rational solution to the constraints.
488  MaybeOptimum<SmallVector<Fraction, 8>> findRationalLexMin();
489 
490  /// Return the lexicographically minimum integer solution to the constraints.
491  ///
492  /// Note: this should be used only when the lexmin is really needed. To obtain
493  /// any integer sample, use Simplex::findIntegerSample as that is more robust.
494  MaybeOptimum<SmallVector<DynamicAPInt, 8>> findIntegerLexMin();
495 
496  /// Return whether the specified inequality is redundant/separate for the
497  /// polytope. Redundant means every point satisfies the given inequality, and
498  /// separate means no point satisfies it.
499  ///
500  /// These checks are integer-exact.
501  bool isSeparateInequality(ArrayRef<DynamicAPInt> coeffs);
502  bool isRedundantInequality(ArrayRef<DynamicAPInt> coeffs);
503 
504 private:
505  /// Returns the current sample point, which may contain non-integer (rational)
506  /// coordinates. Returns an empty optimum when the tableau is empty.
507  ///
508  /// Returns an unbounded optimum when the big M parameter is used and a
509  /// variable has a non-zero big M coefficient, meaning its value is infinite
510  /// or unbounded.
511  MaybeOptimum<SmallVector<Fraction, 8>> getRationalSample() const;
512 
513  /// Make the tableau configuration consistent.
514  LogicalResult restoreRationalConsistency();
515 
516  /// Return whether the specified row is violated;
517  bool rowIsViolated(unsigned row) const;
518 
519  /// Get a constraint row that is violated, if one exists.
520  /// Otherwise, return an empty optional.
521  std::optional<unsigned> maybeGetViolatedRow() const;
522 
523  /// Get a row corresponding to a var that has a non-integral sample value, if
524  /// one exists. Otherwise, return an empty optional.
525  std::optional<unsigned> maybeGetNonIntegralVarRow() const;
526 };
527 
528 /// Represents the result of a symbolic lexicographic optimization computation.
531  : lexopt(space),
532  unboundedDomain(PresburgerSet::getEmpty(space.getDomainSpace())) {}
533 
534  /// This maps assignments of symbols to the corresponding lexopt.
535  /// Takes no value when no integer sample exists for the assignment or if the
536  /// lexopt is unbounded.
538  /// Contains all assignments to the symbols that made the lexopt unbounded.
539  /// Note that the symbols of the input set to the symbolic lexopt are dims
540  /// of this PrebsurgerSet.
542 };
543 
544 /// A class to perform symbolic lexicographic optimization,
545 /// i.e., to find, for every assignment to the symbols the specified
546 /// `symbolDomain`, the lexicographically minimum value integer value attained
547 /// by the non-symbol variables.
548 ///
549 /// The input is a set parametrized by some symbols, i.e., the constant terms
550 /// of the constraints in the set are affine expressions in the symbols, and
551 /// every assignment to the symbols defines a non-symbolic set.
552 ///
553 /// Accordingly, the sample values of the rows in our tableau will be affine
554 /// expressions in the symbols, and every assignment to the symbols will define
555 /// a non-symbolic LexSimplex. We then run the algorithm of
556 /// LexSimplex::findIntegerLexMin simultaneously for every value of the symbols
557 /// in the domain.
558 ///
559 /// Often, the pivot to be performed is the same for all values of the symbols,
560 /// in which case we just do it. For example, if the symbolic sample of a row is
561 /// negative for all values in the symbol domain, the row needs to be pivoted
562 /// irrespective of the precise value of the symbols. To answer queries like
563 /// "Is this symbolic sample always negative in the symbol domain?", we maintain
564 /// a `LexSimplex domainSimplex` correponding to the symbol domain.
565 ///
566 /// In other cases, it may be that the symbolic sample is violated at some
567 /// values in the symbol domain and not violated at others. In this case,
568 /// the pivot to be performed does depend on the value of the symbols. We
569 /// handle this by splitting the symbol domain. We run the algorithm for the
570 /// case where the row isn't violated, and then come back and run the case
571 /// where it is.
573 public:
574  /// `constraints` is the set for which the symbolic lexopt will be computed.
575  /// `symbolDomain` is the set of values of the symbols for which the lexopt
576  /// will be computed. `symbolDomain` should have a dim var for every symbol in
577  /// `constraints`, and no other vars. `isSymbol` specifies which vars of
578  /// `constraints` should be considered as symbols.
579  ///
580  /// The resulting SymbolicLexOpt's space will be compatible with that of
581  /// symbolDomain.
583  const IntegerPolyhedron &symbolDomain,
584  const llvm::SmallBitVector &isSymbol)
585  : LexSimplexBase(constraints, isSymbol), domainPoly(symbolDomain),
586  domainSimplex(symbolDomain) {
587  // TODO consider supporting this case. It amounts
588  // to just returning the input constraints.
589  assert(domainPoly.getNumVars() > 0 &&
590  "there must be some non-symbols to optimize!");
591  }
592 
593  /// An overload to select some subrange of ids as symbols for lexopt.
594  /// The symbol ids are the range of ids with absolute index
595  /// [symbolOffset, symbolOffset + symbolDomain.getNumVars())
596  SymbolicLexSimplex(const IntegerRelation &constraints, unsigned symbolOffset,
597  const IntegerPolyhedron &symbolDomain)
598  : SymbolicLexSimplex(constraints, symbolDomain,
599  getSubrangeBitVector(constraints.getNumVars(),
600  symbolOffset,
601  symbolDomain.getNumVars())) {}
602 
603  /// An overload to select the symbols of `constraints` as symbols for lexopt.
605  const IntegerPolyhedron &symbolDomain)
606  : SymbolicLexSimplex(constraints,
607  constraints.getVarKindOffset(VarKind::Symbol),
608  symbolDomain) {
609  assert(constraints.getNumSymbolVars() == symbolDomain.getNumVars() &&
610  "symbolDomain must have as many vars as constraints has symbols!");
611  }
612 
613  /// The lexmin will be stored as a function `lexopt` from symbols to
614  /// non-symbols in the result.
615  ///
616  /// For some values of the symbols, the lexmin may be unbounded.
617  /// These parts of the symbol domain will be stored in `unboundedDomain`.
618  ///
619  /// The spaces of the sets in the result are compatible with the symbolDomain
620  /// passed in the SymbolicLexSimplex constructor.
621  SymbolicLexOpt computeSymbolicIntegerLexMin();
622 
623 private:
624  /// Perform all pivots that do not require branching.
625  ///
626  /// Return failure if the tableau became empty, indicating that the polytope
627  /// is always integer empty in the current symbol domain.
628  /// Return success otherwise.
629  LogicalResult doNonBranchingPivots();
630 
631  /// Get a row that is always violated in the current domain, if one exists.
632  std::optional<unsigned> maybeGetAlwaysViolatedRow();
633 
634  /// Get a row corresponding to a variable with non-integral sample value, if
635  /// one exists.
636  std::optional<unsigned> maybeGetNonIntegralVarRow();
637 
638  /// Given a row that has a non-integer sample value, cut away this fractional
639  /// sample value witahout removing any integer points, i.e., the integer
640  /// lexmin, if it exists, remains the same after a call to this function. This
641  /// may add constraints or local variables to the tableau, as well as to the
642  /// domain.
643  ///
644  /// Returns whether the cut constraint could be enforced, i.e. failure if the
645  /// cut made the polytope empty, and success if it didn't. Failure status
646  /// indicates that the polytope is always integer empty in the symbol domain
647  /// at the time of the call. (This function may modify the symbol domain, but
648  /// failure statu indicates that the polytope was empty for all symbol values
649  /// in the initial domain.)
650  LogicalResult addSymbolicCut(unsigned row);
651 
652  /// Get the numerator of the symbolic sample of the specific row.
653  /// This is an affine expression in the symbols with integer coefficients.
654  /// The last element is the constant term. This ignores the big M coefficient.
655  SmallVector<DynamicAPInt, 8> getSymbolicSampleNumerator(unsigned row) const;
656 
657  /// Get an affine inequality in the symbols with integer coefficients that
658  /// holds iff the symbolic sample of the specified row is non-negative.
659  SmallVector<DynamicAPInt, 8> getSymbolicSampleIneq(unsigned row) const;
660 
661  /// Return whether all the coefficients of the symbolic sample are integers.
662  ///
663  /// This does not consult the domain to check if the specified expression
664  /// is always integral despite coefficients being fractional.
665  bool isSymbolicSampleIntegral(unsigned row) const;
666 
667  /// Record a lexmin. The tableau must be consistent with all variables
668  /// having symbolic samples with integer coefficients.
669  void recordOutput(SymbolicLexOpt &result) const;
670 
671  /// The symbol domain.
672  IntegerPolyhedron domainPoly;
673  /// Simplex corresponding to the symbol domain.
674  LexSimplex domainSimplex;
675 };
676 
677 /// The Simplex class uses the Normal pivot rule and supports integer emptiness
678 /// checks as well as detecting redundancies.
679 ///
680 /// The Simplex class supports redundancy checking via detectRedundant and
681 /// isMarkedRedundant. A redundant constraint is one which is never violated as
682 /// long as the other constraints are not violated, i.e., removing a redundant
683 /// constraint does not change the set of solutions to the constraints. As a
684 /// heuristic, constraints that have been marked redundant can be ignored for
685 /// most operations. Therefore, these constraints are kept in rows 0 to
686 /// nRedundant - 1, where nRedundant is a member variable that tracks the number
687 /// of constraints that have been marked redundant.
688 ///
689 /// Finding an integer sample is done with the Generalized Basis Reduction
690 /// algorithm. See the documentation for findIntegerSample and reduceBasis.
691 class Simplex : public SimplexBase {
692 public:
693  enum class Direction { Up, Down };
694 
695  Simplex() = delete;
696  explicit Simplex(unsigned nVar) : SimplexBase(nVar, /*mustUseBigM=*/false) {}
697  explicit Simplex(const IntegerRelation &constraints)
698  : Simplex(constraints.getNumVars()) {
699  intersectIntegerRelation(constraints);
700  }
701  ~Simplex() override = default;
702 
703  /// Add an inequality to the tableau. If coeffs is c_0, c_1, ... c_n, where n
704  /// is the current number of variables, then the corresponding inequality is
705  /// c_n + c_0*x_0 + c_1*x_1 + ... + c_{n-1}*x_{n-1} >= 0.
706  ///
707  /// This also tries to restore the tableau configuration to a consistent
708  /// state and marks the Simplex empty if this is not possible.
709  void addInequality(ArrayRef<DynamicAPInt> coeffs) final;
710 
711  /// Compute the maximum or minimum value of the given row, depending on
712  /// direction. The specified row is never pivoted. On return, the row may
713  /// have a negative sample value if the direction is down.
714  ///
715  /// Returns a Fraction denoting the optimum, or a null value if no optimum
716  /// exists, i.e., if the expression is unbounded in this direction.
717  MaybeOptimum<Fraction> computeRowOptimum(Direction direction, unsigned row);
718 
719  /// Compute the maximum or minimum value of the given expression, depending on
720  /// direction. Should not be called when the Simplex is empty.
721  ///
722  /// Returns a Fraction denoting the optimum, or a null value if no optimum
723  /// exists, i.e., if the expression is unbounded in this direction.
724  MaybeOptimum<Fraction> computeOptimum(Direction direction,
725  ArrayRef<DynamicAPInt> coeffs);
726 
727  /// Returns whether the perpendicular of the specified constraint is a
728  /// is a direction along which the polytope is bounded.
729  bool isBoundedAlongConstraint(unsigned constraintIndex);
730 
731  /// Returns whether the specified constraint has been marked as redundant.
732  /// Constraints are numbered from 0 starting at the first added inequality.
733  /// Equalities are added as a pair of inequalities and so correspond to two
734  /// inequalities with successive indices.
735  bool isMarkedRedundant(unsigned constraintIndex) const;
736 
737  /// Finds a subset of constraints that is redundant, i.e., such that
738  /// the set of solutions does not change if these constraints are removed.
739  /// Marks these constraints as redundant. Whether a specific constraint has
740  /// been marked redundant can be queried using isMarkedRedundant.
741  ///
742  /// The first overload only tries to find redundant constraints with indices
743  /// in the range [offset, offset + count), by scanning constraints from left
744  /// to right in this range. If `count` is not provided, all constraints
745  /// starting at `offset` are scanned, and if neither are provided, all
746  /// constraints are scanned, starting from 0 and going to the last constraint.
747  ///
748  /// As an example, in the set (x) : (x >= 0, x >= 0, x >= 0), calling
749  /// `detectRedundant` with no parameters will result in the first two
750  /// constraints being marked redundant. All copies cannot be marked redundant
751  /// because removing all the constraints changes the set. The first two are
752  /// the ones marked redundant because we scan from left to right. Thus, when
753  /// there is some preference among the constraints as to which should be
754  /// marked redundant with priority when there are multiple possibilities, this
755  /// could be accomplished by succesive calls to detectRedundant(offset,
756  /// count).
757  void detectRedundant(unsigned offset, unsigned count);
758  void detectRedundant(unsigned offset) {
759  assert(offset <= con.size() && "invalid offset!");
760  detectRedundant(offset, con.size() - offset);
761  }
762  void detectRedundant() { detectRedundant(0, con.size()); }
763 
764  /// Returns a (min, max) pair denoting the minimum and maximum integer values
765  /// of the given expression. If no integer value exists, both results will be
766  /// of kind Empty.
767  std::pair<MaybeOptimum<DynamicAPInt>, MaybeOptimum<DynamicAPInt>>
768  computeIntegerBounds(ArrayRef<DynamicAPInt> coeffs);
769 
770  /// Check if the simplex takes only one rational value along the
771  /// direction of `coeffs`.
772  ///
773  /// `this` must be nonempty.
774  bool isFlatAlong(ArrayRef<DynamicAPInt> coeffs);
775 
776  /// Returns true if the polytope is unbounded, i.e., extends to infinity in
777  /// some direction. Otherwise, returns false.
778  bool isUnbounded();
779 
780  /// Make a tableau to represent a pair of points in the given tableaus, one in
781  /// tableau A and one in B.
782  static Simplex makeProduct(const Simplex &a, const Simplex &b);
783 
784  /// Returns an integer sample point if one exists, or std::nullopt
785  /// otherwise. This should only be called for bounded sets.
786  std::optional<SmallVector<DynamicAPInt, 8>> findIntegerSample();
787 
788  enum class IneqType { Redundant, Cut, Separate };
789 
790  /// Returns the type of the inequality with coefficients `coeffs`.
791  ///
792  /// Possible types are:
793  /// Redundant The inequality is satisfied in the polytope
794  /// Cut The inequality is satisfied by some points, but not by others
795  /// Separate The inequality is not satisfied by any point
796  IneqType findIneqType(ArrayRef<DynamicAPInt> coeffs);
797 
798  /// Check if the specified inequality already holds in the polytope.
799  bool isRedundantInequality(ArrayRef<DynamicAPInt> coeffs);
800 
801  /// Check if the specified equality already holds in the polytope.
802  bool isRedundantEquality(ArrayRef<DynamicAPInt> coeffs);
803 
804  /// Returns true if this Simplex's polytope is a rational subset of `rel`.
805  /// Otherwise, returns false.
806  bool isRationalSubsetOf(const IntegerRelation &rel);
807 
808  /// Returns the current sample point if it is integral. Otherwise, returns
809  /// std::nullopt.
810  std::optional<SmallVector<DynamicAPInt, 8>> getSamplePointIfIntegral() const;
811 
812  /// Returns the current sample point, which may contain non-integer (rational)
813  /// coordinates. Returns an empty optional when the tableau is empty.
814  std::optional<SmallVector<Fraction, 8>> getRationalSample() const;
815 
816 private:
817  friend class GBRSimplex;
818 
819  /// Restore the unknown to a non-negative sample value.
820  ///
821  /// Returns success if the unknown was successfully restored to a non-negative
822  /// sample value, failure otherwise.
823  LogicalResult restoreRow(Unknown &u);
824 
825  /// Find a pivot to change the sample value of row in the specified
826  /// direction while preserving tableau consistency, except that if the
827  /// direction is down then the pivot may make the specified row take a
828  /// negative value. The returned pivot row will be row if and only if the
829  /// unknown is unbounded in the specified direction.
830  ///
831  /// Returns a (row, col) pair denoting a pivot, or an empty Optional if
832  /// no valid pivot exists.
833  std::optional<Pivot> findPivot(int row, Direction direction) const;
834 
835  /// Find a row that can be used to pivot the column in the specified
836  /// direction. If skipRow is not null, then this row is excluded
837  /// from consideration. The returned pivot will maintain all constraints
838  /// except the column itself and skipRow, if it is set. (if these unknowns
839  /// are restricted).
840  ///
841  /// Returns the row to pivot to, or an empty Optional if the column
842  /// is unbounded in the specified direction.
843  std::optional<unsigned> findPivotRow(std::optional<unsigned> skipRow,
844  Direction direction, unsigned col) const;
845 
846  /// Undo the addition of the last constraint while preserving tableau
847  /// consistency.
848  void undoLastConstraint() final;
849 
850  /// Compute the maximum or minimum of the specified Unknown, depending on
851  /// direction. The specified unknown may be pivoted. If the unknown is
852  /// restricted, it will have a non-negative sample value on return.
853  /// Should not be called if the Simplex is empty.
854  ///
855  /// Returns a Fraction denoting the optimum, or a null value if no optimum
856  /// exists, i.e., if the expression is unbounded in this direction.
857  MaybeOptimum<Fraction> computeOptimum(Direction direction, Unknown &u);
858 
859  /// Mark the specified unknown redundant. This operation is added to the undo
860  /// log and will be undone by rollbacks. The specified unknown must be in row
861  /// orientation.
862  void markRowRedundant(Unknown &u);
863 
864  /// Reduce the given basis, starting at the specified level, using general
865  /// basis reduction.
866  void reduceBasis(IntMatrix &basis, unsigned level);
867 };
868 
869 /// Takes a snapshot of the simplex state on construction and rolls back to the
870 /// snapshot on destruction.
871 ///
872 /// Useful for performing operations in a "transient context", all changes from
873 /// which get rolled back on scope exit.
875 public:
876  SimplexRollbackScopeExit(SimplexBase &simplex) : simplex(simplex) {
877  snapshot = simplex.getSnapshot();
878  };
879  ~SimplexRollbackScopeExit() { simplex.rollback(snapshot); }
880 
881 private:
882  SimplexBase &simplex;
883  unsigned snapshot;
884 };
885 
886 } // namespace presburger
887 } // namespace mlir
888 
889 #endif // MLIR_ANALYSIS_PRESBURGER_SIMPLEX_H
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 ...
Simplex class using the lexicographic pivot rule.
Definition: Simplex.h:412
void undoLastConstraint() final
Undo the addition of the last constraint.
Definition: Simplex.cpp:1213
LexSimplexBase(const IntegerRelation &constraints)
Definition: Simplex.h:431
LogicalResult moveRowUnknownToColumn(unsigned row)
Try to move the specified row to column orientation while preserving the lexicopositivity of the basi...
Definition: Simplex.cpp:777
~LexSimplexBase() override=default
LexSimplexBase(const IntegerRelation &constraints, const llvm::SmallBitVector &isSymbol)
Definition: Simplex.h:435
LexSimplexBase(unsigned nVar, const llvm::SmallBitVector &isSymbol)
Definition: Simplex.h:429
LogicalResult addCut(unsigned row)
Given a row that has a non-integer sample value, add an inequality to cut away this fractional sample...
Definition: Simplex.cpp:281
unsigned getLexMinPivotColumn(unsigned row, unsigned colA, unsigned colB) const
Given two potential pivot columns for a row, return the one that results in the lexicographically sma...
Definition: Simplex.cpp:793
void addInequality(ArrayRef< DynamicAPInt > coeffs) final
Add an inequality to the tableau.
Definition: Simplex.cpp:1592
LexSimplexBase(unsigned nVar)
Definition: Simplex.h:428
unsigned getSnapshot()
Get a snapshot of the current state. This is used for rolling back.
Definition: Simplex.h:425
void appendSymbol()
Add new symbolic variables to the end of the list of variables.
Definition: Simplex.cpp:365
A class for lexicographic optimization without any symbols.
Definition: Simplex.h:478
LexSimplex(const IntegerRelation &constraints)
Definition: Simplex.h:484
LexSimplex(unsigned nVar)
Definition: Simplex.h:480
unsigned getNumRows() const
Definition: Matrix.h:86
unsigned getNumColumns() const
Definition: Matrix.h:88
This class represents a piece-wise MultiAffineFunction.
Definition: PWMAFunction.h:153
PresburgerSpace is the space of all possible values of a tuple of integer valued variables/variables.
The Simplex class implements a version of the Simplex and Generalized Basis Reduction algorithms,...
Definition: Simplex.h:152
unsigned addZeroRow(bool makeRestricted=false)
Add a new row to the tableau and the associated data structures.
Definition: Simplex.cpp:107
bool isEmpty() const
Returns true if the tableau is empty (has conflicting constraints), false otherwise.
Definition: Simplex.cpp:1070
void appendVariable(unsigned count=1)
Add new variables to the end of the list of variables.
Definition: Simplex.cpp:1321
virtual void undoLastConstraint()=0
Undo the addition of the last constraint.
SmallVector< int, 8 > rowUnknown
These hold the indexes of the unknown at a given row or column position.
Definition: Simplex.h:358
SmallVector< SmallVector< int, 8 >, 8 > savedBases
Holds a vector of bases.
Definition: Simplex.h:349
void intersectIntegerRelation(const IntegerRelation &rel)
Add all the constraints from the given IntegerRelation.
Definition: Simplex.cpp:1336
SmallVector< UndoLogEntry, 8 > undoLog
Holds a log of operations, used for rolling back to a previous state.
Definition: Simplex.h:344
bool usingBigM
Stores whether or not a big M column is present in the tableau.
Definition: Simplex.h:326
unsigned getSnapshot() const
Get a snapshot of the current state.
Definition: Simplex.cpp:1137
void print(raw_ostream &os) const
Print the tableau's internal state.
Definition: Simplex.cpp:2129
UndoLogEntry
Enum to denote operations that need to be undone during rollback.
Definition: Simplex.h:301
unsigned getNumRows() const
Definition: Simplex.h:322
const Unknown & unknownFromRow(unsigned row) const
Returns the unknown associated with row.
Definition: Simplex.cpp:87
SmallVector< int, 8 > colUnknown
Definition: Simplex.h:358
SmallVector< Unknown, 8 > var
Definition: Simplex.h:361
void addEquality(ArrayRef< DynamicAPInt > coeffs)
Add an equality to the tableau.
Definition: Simplex.cpp:1123
unsigned getSnapshotBasis()
Get a snapshot of the current state including the basis.
Definition: Simplex.cpp:1139
unsigned getNumFixedCols() const
Return the number of fixed columns, as described in the constructor above, this is the number of colu...
Definition: Simplex.h:321
SmallVector< Unknown, 8 > con
These hold information about each unknown.
Definition: Simplex.h:361
void markEmpty()
Mark the tableau as being empty.
Definition: Simplex.cpp:1093
bool empty
This is true if the tableau has been detected to be empty, false otherwise.
Definition: Simplex.h:341
void addDivisionVariable(ArrayRef< DynamicAPInt > coeffs, const DynamicAPInt &denom)
Append a new variable to the simplex and constrain it such that its only integer value is the floor d...
Definition: Simplex.cpp:1304
void swapColumns(unsigned i, unsigned j)
Definition: Simplex.cpp:1081
void removeLastConstraintRowOrientation()
Remove the last constraint, which must be in row orientation.
Definition: Simplex.cpp:1152
virtual ~SimplexBase()=default
std::optional< unsigned > findAnyPivotRow(unsigned col)
Return any row that this column can be pivoted with, ignoring tableau consistency.
Definition: Simplex.cpp:1175
virtual void addInequality(ArrayRef< DynamicAPInt > coeffs)=0
Add an inequality to the tableau.
const Unknown & unknownFromColumn(unsigned col) const
Returns the unknown associated with col.
Definition: Simplex.cpp:82
void rollback(unsigned snapshot)
Rollback to a snapshot. This invalidates all later snapshots.
Definition: Simplex.cpp:1291
IntMatrix tableau
The matrix representing the tableau.
Definition: Simplex.h:337
void pivot(unsigned row, unsigned col)
Pivot the row with the column.
Definition: Simplex.cpp:951
void swapRows(unsigned i, unsigned j)
Swap the two rows/columns in the tableau and associated data structures.
Definition: Simplex.cpp:1072
void undo(UndoLogEntry entry)
Undo the operation represented by the log entry.
Definition: Simplex.cpp:1229
const Unknown & unknownFromIndex(int index) const
Returns the unknown associated with index.
Definition: Simplex.cpp:77
unsigned nSymbol
The number of parameters.
Definition: Simplex.h:334
unsigned nRedundant
The number of redundant rows in the tableau.
Definition: Simplex.h:330
unsigned addRow(ArrayRef< DynamicAPInt > coeffs, bool makeRestricted=false)
Add a new row to the tableau and the associated data structures.
Definition: Simplex.cpp:121
unsigned getNumVariables() const
Returns the number of variables in the tableau.
Definition: Simplex.cpp:1132
void swapRowWithCol(unsigned row, unsigned col)
Swap the row with the column in the tableau's data structures but not the tableau itself.
Definition: Simplex.cpp:914
unsigned getNumColumns() const
Definition: Simplex.h:323
unsigned getNumConstraints() const
Returns the number of constraints in the tableau.
Definition: Simplex.cpp:1133
Takes a snapshot of the simplex state on construction and rolls back to the snapshot on destruction.
Definition: Simplex.h:874
SimplexRollbackScopeExit(SimplexBase &simplex)
Definition: Simplex.h:876
The Simplex class uses the Normal pivot rule and supports integer emptiness checks as well as detecti...
Definition: Simplex.h:691
void detectRedundant(unsigned offset)
Definition: Simplex.h:758
Simplex(unsigned nVar)
Definition: Simplex.h:696
Simplex(const IntegerRelation &constraints)
Definition: Simplex.h:697
~Simplex() override=default
A class to perform symbolic lexicographic optimization, i.e., to find, for every assignment to the sy...
Definition: Simplex.h:572
SymbolicLexSimplex(const IntegerRelation &constraints, const IntegerPolyhedron &symbolDomain, const llvm::SmallBitVector &isSymbol)
constraints is the set for which the symbolic lexopt will be computed.
Definition: Simplex.h:582
SymbolicLexSimplex(const IntegerRelation &constraints, unsigned symbolOffset, const IntegerPolyhedron &symbolDomain)
An overload to select some subrange of ids as symbols for lexopt.
Definition: Simplex.h:596
SymbolicLexSimplex(const IntegerRelation &constraints, const IntegerPolyhedron &symbolDomain)
An overload to select the symbols of constraints as symbols for lexopt.
Definition: Simplex.h:604
Given a simplex for a polytope, construct a new simplex whose variables are identified with a pair of...
Definition: Simplex.cpp:1655
VarKind
Kind of variable.
llvm::SmallBitVector getSubrangeBitVector(unsigned len, unsigned setOffset, unsigned numSet)
Definition: Utils.cpp:281
Include the generated interface declarations.
A class to represent fractions.
Definition: Fraction.h:29
An Unknown is either a variable or a constraint.
Definition: Simplex.h:234
void print(raw_ostream &os) const
Definition: Simplex.h:244
Unknown(Orientation oOrientation, bool oRestricted, unsigned oPos, bool oIsSymbol=false)
Definition: Simplex.h:235
Represents the result of a symbolic lexicographic optimization computation.
Definition: Simplex.h:529
PWMAFunction lexopt
This maps assignments of symbols to the corresponding lexopt.
Definition: Simplex.h:537
SymbolicLexOpt(const PresburgerSpace &space)
Definition: Simplex.h:530
PresburgerSet unboundedDomain
Contains all assignments to the symbols that made the lexopt unbounded.
Definition: Simplex.h:541
Eliminates variable at the specified position using Fourier-Motzkin variable elimination.