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 FlatAffineConstraints. In particular, 10 // support for performing emptiness checks and redundancy checks. 11 // 12 //===----------------------------------------------------------------------===// 13 14 #ifndef MLIR_ANALYSIS_PRESBURGER_SIMPLEX_H 15 #define MLIR_ANALYSIS_PRESBURGER_SIMPLEX_H 16 17 #include "mlir/Analysis/AffineStructures.h" 18 #include "mlir/Analysis/Presburger/Fraction.h" 19 #include "mlir/Analysis/Presburger/Matrix.h" 20 #include "mlir/IR/Location.h" 21 #include "mlir/Support/LogicalResult.h" 22 #include "llvm/ADT/ArrayRef.h" 23 #include "llvm/ADT/Optional.h" 24 #include "llvm/ADT/SmallVector.h" 25 #include "llvm/Support/StringSaver.h" 26 #include "llvm/Support/raw_ostream.h" 27 28 namespace mlir { 29 30 class GBRSimplex; 31 32 /// This class implements a version of the Simplex and Generalized Basis 33 /// Reduction algorithms, which can perform analysis of integer sets with affine 34 /// inequalities and equalities. A Simplex can be constructed 35 /// by specifying the dimensionality of the set. It supports adding affine 36 /// inequalities and equalities, and can perform emptiness checks, i.e., it can 37 /// find a solution to the set of constraints if one exists, or say that the 38 /// set is empty if no solution exists. Currently, this only works for bounded 39 /// sets. Furthermore, it can find a subset of these constraints that are 40 /// redundant, i.e. a subset of constraints that doesn't constrain the affine 41 /// set further after adding the non-redundant constraints. Simplex can also be 42 /// constructed from a FlatAffineConstraints object. 43 /// 44 /// The implementation of this Simplex class, other than the functionality 45 /// for sampling, is based on the paper 46 /// "Simplify: A Theorem Prover for Program Checking" 47 /// by D. Detlefs, G. Nelson, J. B. Saxe. 48 /// 49 /// We define variables, constraints, and unknowns. Consider the example of a 50 /// two-dimensional set defined by 1 + 2x + 3y >= 0 and 2x - 3y >= 0. Here, 51 /// x, y, are variables while 1 + 2x + 3y >= 0, 2x - 3y >= 0 are 52 /// constraints. Unknowns are either variables or constraints, i.e., x, y, 53 /// 1 + 2x + 3y >= 0, 2x - 3y >= 0 are all unknowns. 54 /// 55 /// The implementation involves a matrix called a tableau, which can be thought 56 /// of as a 2D matrix of rational numbers having number of rows equal to the 57 /// number of constraints and number of columns equal to one plus the number of 58 /// variables. In our implementation, instead of storing rational numbers, we 59 /// store a common denominator for each row, so it is in fact a matrix of 60 /// integers with number of rows equal to number of constraints and number of 61 /// columns equal to _two_ plus the number of variables. For example, instead of 62 /// storing a row of three rationals [1/2, 2/3, 3], we would store [6, 3, 4, 18] 63 /// since 3/6 = 1/2, 4/6 = 2/3, and 18/6 = 3. 64 /// 65 /// Every row and column except the first and second columns is associated with 66 /// an unknown and every unknown is associated with a row or column. The second 67 /// column represents the constant, explained in more detail below. An unknown 68 /// associated with a row or column is said to be in row or column position 69 /// respectively. 70 /// 71 /// The vectors var and con store information about the variables and 72 /// constraints respectively, namely, whether they are in row or column 73 /// position, which row or column they are associated with, and whether they 74 /// correspond to a variable or a constraint. 75 /// 76 /// An unknown is addressed by its index. If the index i is non-negative, then 77 /// the variable var[i] is being addressed. If the index i is negative, then 78 /// the constraint con[~i] is being addressed. Effectively this maps 79 /// 0 -> var[0], 1 -> var[1], -1 -> con[0], -2 -> con[1], etc. rowUnknown[r] and 80 /// colUnknown[c] are the indexes of the unknowns associated with row r and 81 /// column c, respectively. 82 /// 83 /// The unknowns in column position are together called the basis. Initially the 84 /// basis is the set of variables -- in our example above, the initial basis is 85 /// x, y. 86 /// 87 /// The unknowns in row position are represented in terms of the basis unknowns. 88 /// If the basis unknowns are u_1, u_2, ... u_m, and a row in the tableau is 89 /// d, c, a_1, a_2, ... a_m, this represents the unknown for that row as 90 /// (c + a_1*u_1 + a_2*u_2 + ... + a_m*u_m)/d. In our running example, if the 91 /// basis is the initial basis of x, y, then the constraint 1 + 2x + 3y >= 0 92 /// would be represented by the row [1, 1, 2, 3]. 93 /// 94 /// The association of unknowns to rows and columns can be changed by a process 95 /// called pivoting, where a row unknown and a column unknown exchange places 96 /// and the remaining row variables' representation is changed accordingly 97 /// by eliminating the old column unknown in favour of the new column unknown. 98 /// If we had pivoted the column for x with the row for 2x - 3y >= 0, 99 /// the new row for x would be [2, 1, 3] since x = (1*(2x - 3y) + 3*y)/2. 100 /// See the documentation for the pivot member function for details. 101 /// 102 /// The association of unknowns to rows and columns is called the _tableau 103 /// configuration_. The _sample value_ of an unknown in a particular tableau 104 /// configuration is its value if all the column unknowns were set to zero. 105 /// Concretely, for unknowns in column position the sample value is zero and 106 /// for unknowns in row position the sample value is the constant term divided 107 /// by the common denominator. 108 /// 109 /// The tableau configuration is called _consistent_ if the sample value of all 110 /// restricted unknowns is non-negative. Initially there are no constraints, and 111 /// the tableau is consistent. When a new constraint is added, its sample value 112 /// in the current tableau configuration may be negative. In that case, we try 113 /// to find a series of pivots to bring us to a consistent tableau 114 /// configuration, i.e. we try to make the new constraint's sample value 115 /// non-negative without making that of any other constraints negative. (See 116 /// findPivot and findPivotRow for details.) If this is not possible, then the 117 /// set of constraints is mutually contradictory and the tableau is marked 118 /// _empty_, which means the set of constraints has no solution. 119 /// 120 /// The Simplex class supports redundancy checking via detectRedundant and 121 /// isMarkedRedundant. A redundant constraint is one which is never violated as 122 /// long as the other constraints are not violated, i.e., removing a redundant 123 /// constraint does not change the set of solutions to the constraints. As a 124 /// heuristic, constraints that have been marked redundant can be ignored for 125 /// most operations. Therefore, these constraints are kept in rows 0 to 126 /// nRedundant - 1, where nRedundant is a member variable that tracks the number 127 /// of constraints that have been marked redundant. 128 /// 129 /// This Simplex class also supports taking snapshots of the current state 130 /// and rolling back to prior snapshots. This works by maintaining an undo log 131 /// of operations. Snapshots are just pointers to a particular location in the 132 /// log, and rolling back to a snapshot is done by reverting each log entry's 133 /// operation from the end until we reach the snapshot's location. 134 /// 135 /// Finding an integer sample is done with the Generalized Basis Reduction 136 /// algorithm. See the documentation for findIntegerSample and reduceBasis. 137 class Simplex { 138 public: 139 enum class Direction { Up, Down }; 140 141 Simplex() = delete; 142 explicit Simplex(unsigned nVar); 143 explicit Simplex(const FlatAffineConstraints &constraints); 144 145 /// Returns true if the tableau is empty (has conflicting constraints), 146 /// false otherwise. 147 bool isEmpty() const; 148 149 /// Add an inequality to the tableau. If coeffs is c_0, c_1, ... c_n, where n 150 /// is the current number of variables, then the corresponding inequality is 151 /// c_n + c_0*x_0 + c_1*x_1 + ... + c_{n-1}*x_{n-1} >= 0. 152 void addInequality(ArrayRef<int64_t> coeffs); 153 154 /// Returns the number of variables in the tableau. 155 unsigned numVariables() const; 156 157 /// Returns the number of constraints in the tableau. 158 unsigned numConstraints() const; 159 160 /// Add an equality to the tableau. If coeffs is c_0, c_1, ... c_n, where n 161 /// is the current number of variables, then the corresponding equality is 162 /// c_n + c_0*x_0 + c_1*x_1 + ... + c_{n-1}*x_{n-1} == 0. 163 void addEquality(ArrayRef<int64_t> coeffs); 164 165 /// Mark the tableau as being empty. 166 void markEmpty(); 167 168 /// Get a snapshot of the current state. This is used for rolling back. 169 unsigned getSnapshot() const; 170 171 /// Rollback to a snapshot. This invalidates all later snapshots. 172 void rollback(unsigned snapshot); 173 174 /// Add all the constraints from the given FlatAffineConstraints. 175 void intersectFlatAffineConstraints(const FlatAffineConstraints &fac); 176 177 /// Compute the maximum or minimum value of the given row, depending on 178 /// direction. The specified row is never pivoted. On return, the row may 179 /// have a negative sample value if the direction is down. 180 /// 181 /// Returns a Fraction denoting the optimum, or a null value if no optimum 182 /// exists, i.e., if the expression is unbounded in this direction. 183 Optional<Fraction> computeRowOptimum(Direction direction, unsigned row); 184 185 /// Compute the maximum or minimum value of the given expression, depending on 186 /// direction. Should not be called when the Simplex is empty. 187 /// 188 /// Returns a Fraction denoting the optimum, or a null value if no optimum 189 /// exists, i.e., if the expression is unbounded in this direction. 190 Optional<Fraction> computeOptimum(Direction direction, 191 ArrayRef<int64_t> coeffs); 192 193 /// Returns whether the perpendicular of the specified constraint is a 194 /// is a direction along which the polytope is bounded. 195 bool isBoundedAlongConstraint(unsigned constraintIndex); 196 197 /// Returns whether the specified constraint has been marked as redundant. 198 /// Constraints are numbered from 0 starting at the first added inequality. 199 /// Equalities are added as a pair of inequalities and so correspond to two 200 /// inequalities with successive indices. 201 bool isMarkedRedundant(unsigned constraintIndex) const; 202 203 /// Finds a subset of constraints that is redundant, i.e., such that 204 /// the set of solutions does not change if these constraints are removed. 205 /// Marks these constraints as redundant. Whether a specific constraint has 206 /// been marked redundant can be queried using isMarkedRedundant. 207 void detectRedundant(); 208 209 /// Returns a (min, max) pair denoting the minimum and maximum integer values 210 /// of the given expression. 211 std::pair<int64_t, int64_t> computeIntegerBounds(ArrayRef<int64_t> coeffs); 212 213 /// Returns true if the polytope is unbounded, i.e., extends to infinity in 214 /// some direction. Otherwise, returns false. 215 bool isUnbounded(); 216 217 /// Make a tableau to represent a pair of points in the given tableaus, one in 218 /// tableau A and one in B. 219 static Simplex makeProduct(const Simplex &a, const Simplex &b); 220 221 /// Returns a rational sample point. This should not be called when Simplex is 222 /// empty. 223 SmallVector<Fraction, 8> getRationalSample() const; 224 225 /// Returns the current sample point if it is integral. Otherwise, returns 226 /// None. 227 Optional<SmallVector<int64_t, 8>> getSamplePointIfIntegral() const; 228 229 /// Returns an integer sample point if one exists, or None 230 /// otherwise. This should only be called for bounded sets. 231 Optional<SmallVector<int64_t, 8>> findIntegerSample(); 232 233 /// Print the tableau's internal state. 234 void print(raw_ostream &os) const; 235 void dump() const; 236 237 private: 238 friend class GBRSimplex; 239 240 enum class Orientation { Row, Column }; 241 242 /// An Unknown is either a variable or a constraint. It is always associated 243 /// with either a row or column. Whether it's a row or a column is specified 244 /// by the orientation and pos identifies the specific row or column it is 245 /// associated with. If the unknown is restricted, then it has a 246 /// non-negativity constraint associated with it, i.e., its sample value must 247 /// always be non-negative and if it cannot be made non-negative without 248 /// violating other constraints, the tableau is empty. 249 struct Unknown { UnknownUnknown250 Unknown(Orientation oOrientation, bool oRestricted, unsigned oPos) 251 : pos(oPos), orientation(oOrientation), restricted(oRestricted) {} 252 unsigned pos; 253 Orientation orientation; 254 bool restricted : 1; 255 printUnknown256 void print(raw_ostream &os) const { 257 os << (orientation == Orientation::Row ? "r" : "c"); 258 os << pos; 259 if (restricted) 260 os << " [>=0]"; 261 } 262 }; 263 264 struct Pivot { 265 unsigned row, column; 266 }; 267 268 /// Find a pivot to change the sample value of row in the specified 269 /// direction. The returned pivot row will be row if and only 270 /// if the unknown is unbounded in the specified direction. 271 /// 272 /// Returns a (row, col) pair denoting a pivot, or an empty Optional if 273 /// no valid pivot exists. 274 Optional<Pivot> findPivot(int row, Direction direction) const; 275 276 /// Swap the row with the column in the tableau's data structures but not the 277 /// tableau itself. This is used by pivot. 278 void swapRowWithCol(unsigned row, unsigned col); 279 280 /// Pivot the row with the column. 281 void pivot(unsigned row, unsigned col); 282 void pivot(Pivot pair); 283 284 /// Returns the unknown associated with index. 285 const Unknown &unknownFromIndex(int index) const; 286 /// Returns the unknown associated with col. 287 const Unknown &unknownFromColumn(unsigned col) const; 288 /// Returns the unknown associated with row. 289 const Unknown &unknownFromRow(unsigned row) const; 290 /// Returns the unknown associated with index. 291 Unknown &unknownFromIndex(int index); 292 /// Returns the unknown associated with col. 293 Unknown &unknownFromColumn(unsigned col); 294 /// Returns the unknown associated with row. 295 Unknown &unknownFromRow(unsigned row); 296 297 /// Add a new row to the tableau and the associated data structures. 298 unsigned addRow(ArrayRef<int64_t> coeffs); 299 300 /// Normalize the given row by removing common factors between the numerator 301 /// and the denominator. 302 void normalizeRow(unsigned row); 303 304 /// Swap the two rows in the tableau and associated data structures. 305 void swapRows(unsigned i, unsigned j); 306 307 /// Restore the unknown to a non-negative sample value. 308 /// 309 /// Returns true if the unknown was successfully restored to a non-negative 310 /// sample value, false otherwise. 311 LogicalResult restoreRow(Unknown &u); 312 313 /// Compute the maximum or minimum of the specified Unknown, depending on 314 /// direction. The specified unknown may be pivoted. If the unknown is 315 /// restricted, it will have a non-negative sample value on return. 316 /// Should not be called if the Simplex is empty. 317 /// 318 /// Returns a Fraction denoting the optimum, or a null value if no optimum 319 /// exists, i.e., if the expression is unbounded in this direction. 320 Optional<Fraction> computeOptimum(Direction direction, Unknown &u); 321 322 /// Mark the specified unknown redundant. This operation is added to the undo 323 /// log and will be undone by rollbacks. The specified unknown must be in row 324 /// orientation. 325 void markRowRedundant(Unknown &u); 326 327 /// Enum to denote operations that need to be undone during rollback. 328 enum class UndoLogEntry { 329 RemoveLastConstraint, 330 UnmarkEmpty, 331 UnmarkLastRedundant 332 }; 333 334 /// Undo the operation represented by the log entry. 335 void undo(UndoLogEntry entry); 336 337 /// Find a row that can be used to pivot the column in the specified 338 /// direction. If skipRow is not null, then this row is excluded 339 /// from consideration. The returned pivot will maintain all constraints 340 /// except the column itself and skipRow, if it is set. (if these unknowns 341 /// are restricted). 342 /// 343 /// Returns the row to pivot to, or an empty Optional if the column 344 /// is unbounded in the specified direction. 345 Optional<unsigned> findPivotRow(Optional<unsigned> skipRow, 346 Direction direction, unsigned col) const; 347 348 /// Reduce the given basis, starting at the specified level, using general 349 /// basis reduction. 350 void reduceBasis(Matrix &basis, unsigned level); 351 352 /// The number of rows in the tableau. 353 unsigned nRow; 354 355 /// The number of columns in the tableau, including the common denominator 356 /// and the constant column. 357 unsigned nCol; 358 359 /// The number of redundant rows in the tableau. These are the first 360 /// nRedundant rows. 361 unsigned nRedundant; 362 363 /// The matrix representing the tableau. 364 Matrix tableau; 365 366 /// This is true if the tableau has been detected to be empty, false 367 /// otherwise. 368 bool empty; 369 370 /// Holds a log of operations, used for rolling back to a previous state. 371 SmallVector<UndoLogEntry, 8> undoLog; 372 373 /// These hold the indexes of the unknown at a given row or column position. 374 /// We keep these as signed integers since that makes it convenient to check 375 /// if an index corresponds to a variable or a constraint by checking the 376 /// sign. 377 /// 378 /// colUnknown is padded with two null indexes at the front since the first 379 /// two columns don't correspond to any unknowns. 380 SmallVector<int, 8> rowUnknown, colUnknown; 381 382 /// These hold information about each unknown. 383 SmallVector<Unknown, 8> con, var; 384 }; 385 386 } // namespace mlir 387 388 #endif // MLIR_ANALYSIS_PRESBURGER_SIMPLEX_H 389