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 - 1;
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<SmallVector<Entry, 8>, 4> RemainingRows;
38 for (unsigned R1 = 0; R1 < Constraints.size();) {
39 SmallVector<Entry, 8> &Row1 = Constraints[R1];
40 if (getLastCoefficient(Row: 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(Row: RemainingRows[R2], Id: LastIdx);
63 int64_t LowerLast = getLastCoefficient(Row: 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 SmallVector<Entry, 8> 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 > 1) {
159 if (!eliminateUsingFM())
160 return true;
161 }
162
163 if (Constraints.empty() || NumVariables > 1)
164 return true;
165
166 return all_of(Range&: Constraints, P: [](auto &R) {
167 if (R.empty())
168 return true;
169 if (R[0].Id == 0)
170 return R[0].Coefficient >= 0;
171 return true;
172 });
173}
174
175SmallVector<std::string> ConstraintSystem::getVarNamesList() const {
176 SmallVector<std::string> Names(Value2Index.size(), "");
177#ifndef NDEBUG
178 for (auto &[V, Index] : Value2Index) {
179 std::string OperandName;
180 if (V->getName().empty())
181 OperandName = V->getNameOrAsOperand();
182 else
183 OperandName = std::string("%") + V->getName().str();
184 Names[Index - 1] = OperandName;
185 }
186#endif
187 return Names;
188}
189
190void ConstraintSystem::dump() const {
191#ifndef NDEBUG
192 if (Constraints.empty())
193 return;
194 SmallVector<std::string> Names = getVarNamesList();
195 for (const auto &Row : Constraints) {
196 SmallVector<std::string, 16> Parts;
197 for (const Entry &E : Row) {
198 if (E.Id >= NumVariables)
199 break;
200 if (E.Id == 0)
201 continue;
202 // The Value2Index map (and hence Names) may be absent, e.g. for the
203 // temporary system solved in isConditionImplied. Fall back to a generic
204 // variable name in that case.
205 std::string Name = E.Id <= Names.size() ? Names[E.Id - 1]
206 : ("%v" + std::to_string(E.Id));
207 std::string Coefficient;
208 if (E.Coefficient != 1)
209 Coefficient = std::to_string(E.Coefficient) + " * ";
210 Parts.push_back(Coefficient + Name);
211 }
212 // assert(!Parts.empty() && "need to have at least some parts");
213 int64_t ConstPart = 0;
214 if (Row[0].Id == 0)
215 ConstPart = Row[0].Coefficient;
216 LLVM_DEBUG(dbgs() << join(Parts, std::string(" + "))
217 << " <= " << std::to_string(ConstPart) << "\n");
218 }
219#endif
220}
221
222bool ConstraintSystem::mayHaveSolution() {
223 LLVM_DEBUG(dbgs() << "---\n");
224 LLVM_DEBUG(dump());
225 bool HasSolution = mayHaveSolutionImpl();
226 LLVM_DEBUG(dbgs() << (HasSolution ? "sat" : "unsat") << "\n");
227 return HasSolution;
228}
229
230std::pair<ConstraintSystem, SmallVector<int64_t, 8>>
231ConstraintSystem::getSubSystem(ArrayRef<int64_t> R) const {
232 // Only constraints that share a variable (transitively) with a query R can
233 // affect whether system + !R has a solution.
234 //
235 // Mark variables in the query and collect to the transitive closure over
236 // variables that co-occur in a constraint row.
237 ConstraintSystem SubSystem;
238 SmallBitVector InSystem(NumVariables + 1, false);
239 for (unsigned Id = 1, E = R.size(); Id < E; ++Id)
240 if (R[Id] != 0)
241 InSystem[Id] = true;
242 bool Changed = true;
243 while (Changed) {
244 Changed = false;
245 for (const auto &Row : Constraints) {
246 // No common variables, skip.
247 if (none_of(Range: Row,
248 P: [&](const Entry &E) { return E.Id != 0 && InSystem[E.Id]; }))
249 continue;
250 for (const Entry &E : Row)
251 if (E.Id != 0 && !InSystem[E.Id]) {
252 InSystem[E.Id] = true;
253 Changed = true;
254 }
255 }
256 }
257
258 // Assign compact indices to the variables of the sub-system.
259 SmallVector<unsigned, 16> OldToNew;
260 OldToNew.assign(NumElts: NumVariables + 1, Elt: 0);
261 unsigned NextIdx = 1;
262 for (unsigned Id : InSystem.set_bits())
263 OldToNew[Id] = NextIdx++;
264
265 // Build new compact set of rows.
266 SubSystem.NumVariables = NextIdx;
267 for (const auto &Row : Constraints) {
268 if (none_of(Range: Row,
269 P: [&](const Entry &E) { return E.Id != 0 && InSystem[E.Id]; }))
270 continue;
271 SmallVector<Entry, 8> NewRow;
272 for (const Entry &E : Row) {
273 if (!E.Id)
274 NewRow.emplace_back(Args: E.Coefficient, Args: E.Id);
275 else if (unsigned New = OldToNew[E.Id])
276 NewRow.emplace_back(Args: E.Coefficient, Args&: New);
277 }
278 SubSystem.Constraints.push_back(Elt: std::move(NewRow));
279 }
280
281 // Remap the query row into the component's compact index space.
282 SmallVector<int64_t, 8> NewR(SubSystem.NumVariables, 0);
283 NewR[0] = R[0];
284 for (unsigned Id = 1, E = R.size(); Id < E; ++Id)
285 if (R[Id] != 0)
286 NewR[OldToNew[Id]] = R[Id];
287 return {std::move(SubSystem), std::move(NewR)};
288}
289
290bool ConstraintSystem::isConditionImplied(SmallVector<int64_t, 8> R) const {
291 // If all variable coefficients are 0, we have 'C >= 0'. If the constant is >=
292 // 0, R is always true, regardless of the system.
293 if (all_of(Range: ArrayRef(R).drop_front(N: 1), P: equal_to(Arg: 0)))
294 return R[0] >= 0;
295
296 // If there is no solution with the negation of R added to the system, the
297 // condition must hold based on the existing constraints.
298 R = ConstraintSystem::negate(R);
299 if (R.empty())
300 return false;
301
302 auto Copy = *this;
303 Copy.addVariableRow(R);
304 return !Copy.mayHaveSolution();
305}
306
307bool ConstraintSystem::isConditionImpliedInSubSystem(
308 SmallVector<int64_t, 8> R) const {
309 if (R.empty())
310 return false;
311
312 // Queries with no variables are trivially decided without building any
313 // component.
314 if (all_of(Range: ArrayRef(R).drop_front(N: 1), P: equal_to(Arg: 0)))
315 return R[0] >= 0;
316
317 // A single query: build the component and solve it in place.
318 const auto &[SubCS, NewR] = getSubSystem(R);
319 return SubCS.isConditionImplied(R: NewR);
320}
321