1//===- ConstraintSytem.cpp - A system of linear constraints. ----*- 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#include "llvm/Analysis/ConstraintSystem.h"
10#include "llvm/ADT/SmallBitVector.h"
11#include "llvm/ADT/SmallVector.h"
12#include "llvm/ADT/StringExtras.h"
13#include "llvm/IR/Value.h"
14#include "llvm/Support/Debug.h"
15#include "llvm/Support/MathExtras.h"
16
17#include <string>
18
19using namespace llvm;
20
21#define DEBUG_TYPE "constraint-system"
22
23bool ConstraintSystem::eliminateUsingFM() {
24 // Implementation of Fourier–Motzkin elimination, with some tricks from the
25 // paper Pugh, William. "The Omega test: a fast and practical integer
26 // programming algorithm for dependence
27 // analysis."
28 // Supercomputing'91: Proceedings of the 1991 ACM/
29 // IEEE conference on Supercomputing. IEEE, 1991.
30 assert(!Constraints.empty() &&
31 "should only be called for non-empty constraint systems");
32
33 unsigned LastIdx = NumVariables;
34
35 // First, either remove the variable in place if it is 0 or add the row to
36 // RemainingRows and remove it from the system.
37 SmallVector<RowTy, 4> RemainingRows;
38 for (unsigned R1 = 0; R1 < Constraints.size();) {
39 RowTy &Row1 = Constraints[R1];
40 if (getLastCoefficient(R: Row1, Id: LastIdx) == 0) {
41 if (Row1.size() > 0 && Row1.back().Id == LastIdx)
42 Row1.pop_back();
43 R1++;
44 } else {
45 std::swap(LHS&: Constraints[R1], RHS&: Constraints.back());
46 RemainingRows.push_back(Elt: std::move(Constraints.back()));
47 Constraints.pop_back();
48 }
49 }
50
51 // Process rows where the variable is != 0.
52 unsigned NumRemainingConstraints = RemainingRows.size();
53 for (unsigned R1 = 0; R1 < NumRemainingConstraints; R1++) {
54 // FIXME do not use copy
55 for (unsigned R2 = R1 + 1; R2 < NumRemainingConstraints; R2++) {
56 // Examples of constraints stored as {Constant, Coeff_x, Coeff_y}
57 // R1: 0 >= 1 * x + (-2) * y => { 0, 1, -2 }
58 // R2: 3 >= 2 * x + 3 * y => { 3, 2, 3 }
59 // LastIdx = 2 (tracking coefficient of y)
60 // UpperLast: 3
61 // LowerLast: -2
62 int64_t UpperLast = getLastCoefficient(R: RemainingRows[R2], Id: LastIdx);
63 int64_t LowerLast = getLastCoefficient(R: RemainingRows[R1], Id: LastIdx);
64 assert(
65 UpperLast != 0 && LowerLast != 0 &&
66 "RemainingRows should only contain rows where the variable is != 0");
67
68 if ((LowerLast < 0 && UpperLast < 0) || (LowerLast > 0 && UpperLast > 0))
69 continue;
70
71 unsigned LowerR = R1;
72 unsigned UpperR = R2;
73 if (UpperLast < 0) {
74 std::swap(a&: LowerR, b&: UpperR);
75 std::swap(a&: LowerLast, b&: UpperLast);
76 }
77
78 RowTy NR;
79 unsigned IdxUpper = 0;
80 unsigned IdxLower = 0;
81 auto &LowerRow = RemainingRows[LowerR];
82 auto &UpperRow = RemainingRows[UpperR];
83 // Combine the two rows to eliminate the variable. If any coefficient
84 // computation overflows, skip them.
85 bool Overflow = false;
86 // Update constant and coefficients of both constraints.
87 // Stops until every coefficient is updated or overflows.
88 while (true) {
89 if (IdxUpper >= UpperRow.size() || IdxLower >= LowerRow.size())
90 break;
91 int64_t M1, M2, N;
92 // Starts with index 0 and updates every coefficients.
93 int64_t UpperV = 0;
94 int64_t LowerV = 0;
95 uint16_t CurrentId = std::numeric_limits<uint16_t>::max();
96 if (IdxUpper < UpperRow.size()) {
97 CurrentId = std::min(a: UpperRow[IdxUpper].Id, b: CurrentId);
98 }
99 if (IdxLower < LowerRow.size()) {
100 CurrentId = std::min(a: LowerRow[IdxLower].Id, b: CurrentId);
101 }
102
103 if (IdxUpper < UpperRow.size() && UpperRow[IdxUpper].Id == CurrentId) {
104 UpperV = UpperRow[IdxUpper].Coefficient;
105 IdxUpper++;
106 }
107
108 if (MulOverflow(X: UpperV, Y: -1 * LowerLast, Result&: M1)) {
109 Overflow = true;
110 break;
111 }
112 if (IdxLower < LowerRow.size() && LowerRow[IdxLower].Id == CurrentId) {
113 LowerV = LowerRow[IdxLower].Coefficient;
114 IdxLower++;
115 }
116
117 if (MulOverflow(X: LowerV, Y: UpperLast, Result&: M2)) {
118 Overflow = true;
119 break;
120 }
121 // This algorithm is a variant of sparse Gaussian elimination.
122 //
123 // The new coefficient for CurrentId is
124 // N = UpperV * (-1) * LowerLast + LowerV * UpperLast
125 //
126 // UpperRow: { 3, 2, 3 }, LowerLast: -2
127 // LowerRow: { 0, 1, -2 }, UpperLast: 3
128 //
129 // After multiplication:
130 // UpperRow: { 6, 4, 6 }
131 // LowerRow: { 0, 3, -6 }
132 //
133 // Eliminates y after addition:
134 // N: { 6, 7, 0 } => 6 >= 7 * x
135 if (AddOverflow(X: M1, Y: M2, Result&: N)) {
136 Overflow = true;
137 break;
138 }
139 // Skip variable that is completely eliminated.
140 if (N == 0)
141 continue;
142 NR.emplace_back(Args&: N, Args&: CurrentId);
143 }
144 if (Overflow || NR.empty())
145 continue;
146 Constraints.push_back(Elt: std::move(NR));
147 // Give up if the new system gets too big.
148 if (Constraints.size() > 500)
149 return false;
150 }
151 }
152 NumVariables -= 1;
153
154 return true;
155}
156
157bool ConstraintSystem::mayHaveSolutionImpl() {
158 while (!Constraints.empty() && NumVariables > 0) {
159 if (!eliminateUsingFM())
160 return true;
161 }
162
163 assert((Constraints.empty() || NumVariables == 0) &&
164 "non-empty system must have all variables eliminated");
165 return all_of(Range&: Constraints,
166 P: [](ArrayRef<Entry> R) { return getConstant(R) >= 0; });
167}
168
169SmallVector<std::string> ConstraintSystem::getVarNamesList() const {
170 SmallVector<std::string> Names(Value2Index.size(), "");
171#ifndef NDEBUG
172 for (auto &[V, Index] : Value2Index) {
173 std::string OperandName;
174 if (V->getName().empty())
175 OperandName = V->getNameOrAsOperand();
176 else
177 OperandName = std::string("%") + V->getName().str();
178 Names[Index - 1] = OperandName;
179 }
180#endif
181 return Names;
182}
183
184void ConstraintSystem::dump() const {
185#ifndef NDEBUG
186 if (Constraints.empty())
187 return;
188 SmallVector<std::string> Names = getVarNamesList();
189 for (const auto &Row : Constraints) {
190 SmallVector<std::string, 16> Parts;
191 for (const Entry &E : Row) {
192 if (E.Id > NumVariables)
193 break;
194 if (E.Id == 0)
195 continue;
196 // The Value2Index map (and hence Names) may be absent, e.g. for the
197 // temporary system solved in isConditionImplied. Fall back to a generic
198 // variable name in that case.
199 std::string Name = E.Id <= Names.size() ? Names[E.Id - 1]
200 : ("%v" + std::to_string(E.Id));
201 std::string Coefficient;
202 if (E.Coefficient != 1)
203 Coefficient = std::to_string(E.Coefficient) + " * ";
204 Parts.push_back(Coefficient + Name);
205 }
206 LLVM_DEBUG(dbgs() << join(Parts, " + ") << " <= " << getConstant(Row)
207 << "\n");
208 }
209#endif
210}
211
212bool ConstraintSystem::mayHaveSolution() {
213 LLVM_DEBUG(dbgs() << "---\n");
214 LLVM_DEBUG(dump());
215 bool HasSolution = mayHaveSolutionImpl();
216 LLVM_DEBUG(dbgs() << (HasSolution ? "sat" : "unsat") << "\n");
217 return HasSolution;
218}
219
220std::pair<ConstraintSystem, ConstraintSystem::RowTy>
221ConstraintSystem::getSubSystem(ArrayRef<Entry> R) const {
222 // Only constraints that share a variable (transitively) with a query R can
223 // affect whether system + !R has a solution.
224 //
225 // Mark variables in the query and collect to the transitive closure over
226 // variables that co-occur in a constraint row.
227 ConstraintSystem SubSystem;
228 SmallBitVector InSystem(NumVariables + 1, false);
229 for (const Entry &E : R)
230 if (E.Id != 0)
231 InSystem[E.Id] = true;
232 auto SharesVariable = [&InSystem](ArrayRef<Entry> Row) {
233 return any_of(Range&: Row, P: [&InSystem](const Entry &E) {
234 return E.Id != 0 && InSystem[E.Id];
235 });
236 };
237 bool Changed = true;
238 while (Changed) {
239 Changed = false;
240 for (const RowTy &Row : Constraints) {
241 // No common variables, skip.
242 if (!SharesVariable(Row))
243 continue;
244 for (const Entry &E : Row)
245 if (E.Id != 0 && !InSystem[E.Id]) {
246 InSystem[E.Id] = true;
247 Changed = true;
248 }
249 }
250 }
251
252 // Assign compact indices to the variables of the sub-system.
253 SmallVector<unsigned, 16> OldToNew(NumVariables + 1, 0);
254 unsigned NextIdx = 1;
255 for (unsigned Id : InSystem.set_bits())
256 OldToNew[Id] = NextIdx++;
257
258 // Build new compact set of rows.
259 SubSystem.NumVariables = NextIdx - 1;
260 for (const RowTy &Row : Constraints) {
261 if (!SharesVariable(Row))
262 continue;
263 RowTy NewRow;
264 for (const Entry &E : Row) {
265 unsigned New = OldToNew[E.Id];
266 assert((E.Id == 0) == (New == 0) && "constant entry must be preserved");
267 NewRow.emplace_back(Args: E.Coefficient, Args&: New);
268 }
269 SubSystem.Constraints.push_back(Elt: std::move(NewRow));
270 }
271
272 // Remap the query row into the component's compact index space.
273 RowTy NewR(1, Entry(getConstant(R), 0));
274 for (const Entry &E : R)
275 if (E.Id != 0)
276 NewR.emplace_back(Args: E.Coefficient, Args&: OldToNew[E.Id]);
277 return {std::move(SubSystem), std::move(NewR)};
278}
279
280bool ConstraintSystem::isConditionImplied(RowTy R) const {
281 // If all variable coefficients are 0, we have 'C >= 0'. If the constant is >=
282 // 0, R is always true, regardless of the system.
283 if (isConstantOnly(R))
284 return getConstant(R) >= 0;
285
286 // If there is no solution with the negation of R added to the system, the
287 // condition must hold based on the existing constraints.
288 R = ConstraintSystem::negate(R: std::move(R));
289 if (R.empty())
290 return false;
291
292 auto Copy = *this;
293 Copy.addRow(R, NumVars: NumVariables);
294 return !Copy.mayHaveSolution();
295}
296
297bool ConstraintSystem::isConditionImpliedInSubSystem(ArrayRef<Entry> R) const {
298 if (R.empty())
299 return false;
300
301 // Queries with no variables are trivially decided without building any
302 // component.
303 if (isConstantOnly(R))
304 return getConstant(R) >= 0;
305
306 // A single query: build the component and solve it in place.
307 const auto &[SubCS, NewR] = getSubSystem(R);
308 return SubCS.isConditionImplied(R: NewR);
309}
310