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/SmallVector.h"
11#include "llvm/ADT/StringExtras.h"
12#include "llvm/IR/Value.h"
13#include "llvm/Support/Debug.h"
14#include "llvm/Support/MathExtras.h"
15
16#include <string>
17
18using namespace llvm;
19
20#define DEBUG_TYPE "constraint-system"
21
22bool ConstraintSystem::eliminateUsingFM() {
23 // Implementation of Fourier–Motzkin elimination, with some tricks from the
24 // paper Pugh, William. "The Omega test: a fast and practical integer
25 // programming algorithm for dependence
26 // analysis."
27 // Supercomputing'91: Proceedings of the 1991 ACM/
28 // IEEE conference on Supercomputing. IEEE, 1991.
29 assert(!Constraints.empty() &&
30 "should only be called for non-empty constraint systems");
31
32 unsigned LastIdx = NumVariables - 1;
33
34 // First, either remove the variable in place if it is 0 or add the row to
35 // RemainingRows and remove it from the system.
36 SmallVector<SmallVector<Entry, 8>, 4> RemainingRows;
37 for (unsigned R1 = 0; R1 < Constraints.size();) {
38 SmallVector<Entry, 8> &Row1 = Constraints[R1];
39 if (getLastCoefficient(Row: Row1, Id: LastIdx) == 0) {
40 if (Row1.size() > 0 && Row1.back().Id == LastIdx)
41 Row1.pop_back();
42 R1++;
43 } else {
44 std::swap(LHS&: Constraints[R1], RHS&: Constraints.back());
45 RemainingRows.push_back(Elt: std::move(Constraints.back()));
46 Constraints.pop_back();
47 }
48 }
49
50 // Process rows where the variable is != 0.
51 unsigned NumRemainingConstraints = RemainingRows.size();
52 for (unsigned R1 = 0; R1 < NumRemainingConstraints; R1++) {
53 // FIXME do not use copy
54 for (unsigned R2 = R1 + 1; R2 < NumRemainingConstraints; R2++) {
55 // Examples of constraints stored as {Constant, Coeff_x, Coeff_y}
56 // R1: 0 >= 1 * x + (-2) * y => { 0, 1, -2 }
57 // R2: 3 >= 2 * x + 3 * y => { 3, 2, 3 }
58 // LastIdx = 2 (tracking coefficient of y)
59 // UpperLast: 3
60 // LowerLast: -2
61 int64_t UpperLast = getLastCoefficient(Row: RemainingRows[R2], Id: LastIdx);
62 int64_t LowerLast = getLastCoefficient(Row: RemainingRows[R1], Id: LastIdx);
63 assert(
64 UpperLast != 0 && LowerLast != 0 &&
65 "RemainingRows should only contain rows where the variable is != 0");
66
67 if ((LowerLast < 0 && UpperLast < 0) || (LowerLast > 0 && UpperLast > 0))
68 continue;
69
70 unsigned LowerR = R1;
71 unsigned UpperR = R2;
72 if (UpperLast < 0) {
73 std::swap(a&: LowerR, b&: UpperR);
74 std::swap(a&: LowerLast, b&: UpperLast);
75 }
76
77 SmallVector<Entry, 8> NR;
78 unsigned IdxUpper = 0;
79 unsigned IdxLower = 0;
80 auto &LowerRow = RemainingRows[LowerR];
81 auto &UpperRow = RemainingRows[UpperR];
82 // Update constant and coefficients of both constraints.
83 // Stops until every coefficient is updated or overflows.
84 while (true) {
85 if (IdxUpper >= UpperRow.size() || IdxLower >= LowerRow.size())
86 break;
87 int64_t M1, M2, N;
88 // Starts with index 0 and updates every coefficients.
89 int64_t UpperV = 0;
90 int64_t LowerV = 0;
91 uint16_t CurrentId = std::numeric_limits<uint16_t>::max();
92 if (IdxUpper < UpperRow.size()) {
93 CurrentId = std::min(a: UpperRow[IdxUpper].Id, b: CurrentId);
94 }
95 if (IdxLower < LowerRow.size()) {
96 CurrentId = std::min(a: LowerRow[IdxLower].Id, b: CurrentId);
97 }
98
99 if (IdxUpper < UpperRow.size() && UpperRow[IdxUpper].Id == CurrentId) {
100 UpperV = UpperRow[IdxUpper].Coefficient;
101 IdxUpper++;
102 }
103
104 if (MulOverflow(X: UpperV, Y: -1 * LowerLast, Result&: M1))
105 return false;
106 if (IdxLower < LowerRow.size() && LowerRow[IdxLower].Id == CurrentId) {
107 LowerV = LowerRow[IdxLower].Coefficient;
108 IdxLower++;
109 }
110
111 if (MulOverflow(X: LowerV, Y: UpperLast, Result&: M2))
112 return false;
113 // This algorithm is a variant of sparse Gaussian elimination.
114 //
115 // The new coefficient for CurrentId is
116 // N = UpperV * (-1) * LowerLast + LowerV * UpperLast
117 //
118 // UpperRow: { 3, 2, 3 }, LowerLast: -2
119 // LowerRow: { 0, 1, -2 }, UpperLast: 3
120 //
121 // After multiplication:
122 // UpperRow: { 6, 4, 6 }
123 // LowerRow: { 0, 3, -6 }
124 //
125 // Eliminates y after addition:
126 // N: { 6, 7, 0 } => 6 >= 7 * x
127 if (AddOverflow(X: M1, Y: M2, Result&: N))
128 return false;
129 // Skip variable that is completely eliminated.
130 if (N == 0)
131 continue;
132 NR.emplace_back(Args&: N, Args&: CurrentId);
133 }
134 if (NR.empty())
135 continue;
136 Constraints.push_back(Elt: std::move(NR));
137 // Give up if the new system gets too big.
138 if (Constraints.size() > 500)
139 return false;
140 }
141 }
142 NumVariables -= 1;
143
144 return true;
145}
146
147bool ConstraintSystem::mayHaveSolutionImpl() {
148 while (!Constraints.empty() && NumVariables > 1) {
149 if (!eliminateUsingFM())
150 return true;
151 }
152
153 if (Constraints.empty() || NumVariables > 1)
154 return true;
155
156 return all_of(Range&: Constraints, P: [](auto &R) {
157 if (R.empty())
158 return true;
159 if (R[0].Id == 0)
160 return R[0].Coefficient >= 0;
161 return true;
162 });
163}
164
165SmallVector<std::string> ConstraintSystem::getVarNamesList() const {
166 SmallVector<std::string> Names(Value2Index.size(), "");
167#ifndef NDEBUG
168 for (auto &[V, Index] : Value2Index) {
169 std::string OperandName;
170 if (V->getName().empty())
171 OperandName = V->getNameOrAsOperand();
172 else
173 OperandName = std::string("%") + V->getName().str();
174 Names[Index - 1] = OperandName;
175 }
176#endif
177 return Names;
178}
179
180void ConstraintSystem::dump() const {
181#ifndef NDEBUG
182 if (Constraints.empty())
183 return;
184 SmallVector<std::string> Names = getVarNamesList();
185 for (const auto &Row : Constraints) {
186 SmallVector<std::string, 16> Parts;
187 for (const Entry &E : Row) {
188 if (E.Id >= NumVariables)
189 break;
190 if (E.Id == 0)
191 continue;
192 std::string Coefficient;
193 if (E.Coefficient != 1)
194 Coefficient = std::to_string(E.Coefficient) + " * ";
195 Parts.push_back(Coefficient + Names[E.Id - 1]);
196 }
197 // assert(!Parts.empty() && "need to have at least some parts");
198 int64_t ConstPart = 0;
199 if (Row[0].Id == 0)
200 ConstPart = Row[0].Coefficient;
201 LLVM_DEBUG(dbgs() << join(Parts, std::string(" + "))
202 << " <= " << std::to_string(ConstPart) << "\n");
203 }
204#endif
205}
206
207bool ConstraintSystem::mayHaveSolution() {
208 LLVM_DEBUG(dbgs() << "---\n");
209 LLVM_DEBUG(dump());
210 bool HasSolution = mayHaveSolutionImpl();
211 LLVM_DEBUG(dbgs() << (HasSolution ? "sat" : "unsat") << "\n");
212 return HasSolution;
213}
214
215bool ConstraintSystem::isConditionImplied(SmallVector<int64_t, 8> R) const {
216 // If all variable coefficients are 0, we have 'C >= 0'. If the constant is >=
217 // 0, R is always true, regardless of the system.
218 if (all_of(Range: ArrayRef(R).drop_front(N: 1), P: [](int64_t C) { return C == 0; }))
219 return R[0] >= 0;
220
221 // If there is no solution with the negation of R added to the system, the
222 // condition must hold based on the existing constraints.
223 R = ConstraintSystem::negate(R);
224 if (R.empty())
225 return false;
226
227 auto NewSystem = *this;
228 NewSystem.addVariableRow(R);
229 return !NewSystem.mayHaveSolution();
230}
231