1 //===- ConstraintSytem.cpp - A system of linear constraints. ----*- C++ -*-===//
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
7 //===----------------------------------------------------------------------===//
9 #include "llvm/Analysis/ConstraintSystem.h"
10 #include "llvm/ADT/SmallVector.h"
11 #include "llvm/Support/MathExtras.h"
12 #include "llvm/ADT/StringExtras.h"
13 #include "llvm/IR/Value.h"
14 #include "llvm/Support/Debug.h"
20 #define DEBUG_TYPE "constraint-system"
22 bool 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
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");
32 unsigned LastIdx
= NumVariables
- 1;
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(Row1
, LastIdx
) == 0) {
40 if (Row1
.size() > 0 && Row1
.back().Id
== LastIdx
)
44 std::swap(Constraints
[R1
], Constraints
.back());
45 RemainingRows
.push_back(std::move(Constraints
.back()));
46 Constraints
.pop_back();
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
++) {
58 int64_t UpperLast
= getLastCoefficient(RemainingRows
[R2
], LastIdx
);
59 int64_t LowerLast
= getLastCoefficient(RemainingRows
[R1
], LastIdx
);
61 UpperLast
!= 0 && LowerLast
!= 0 &&
62 "RemainingRows should only contain rows where the variable is != 0");
64 if ((LowerLast
< 0 && UpperLast
< 0) || (LowerLast
> 0 && UpperLast
> 0))
70 std::swap(LowerR
, UpperR
);
71 std::swap(LowerLast
, UpperLast
);
74 SmallVector
<Entry
, 8> NR
;
75 unsigned IdxUpper
= 0;
76 unsigned IdxLower
= 0;
77 auto &LowerRow
= RemainingRows
[LowerR
];
78 auto &UpperRow
= RemainingRows
[UpperR
];
80 if (IdxUpper
>= UpperRow
.size() || IdxLower
>= LowerRow
.size())
85 uint16_t CurrentId
= std::numeric_limits
<uint16_t>::max();
86 if (IdxUpper
< UpperRow
.size()) {
87 CurrentId
= std::min(UpperRow
[IdxUpper
].Id
, CurrentId
);
89 if (IdxLower
< LowerRow
.size()) {
90 CurrentId
= std::min(LowerRow
[IdxLower
].Id
, CurrentId
);
93 if (IdxUpper
< UpperRow
.size() && UpperRow
[IdxUpper
].Id
== CurrentId
) {
94 UpperV
= UpperRow
[IdxUpper
].Coefficient
;
98 if (MulOverflow(UpperV
, -1 * LowerLast
, M1
))
100 if (IdxLower
< LowerRow
.size() && LowerRow
[IdxLower
].Id
== CurrentId
) {
101 LowerV
= LowerRow
[IdxLower
].Coefficient
;
105 if (MulOverflow(LowerV
, UpperLast
, M2
))
107 if (AddOverflow(M1
, M2
, N
))
111 NR
.emplace_back(N
, CurrentId
);
115 Constraints
.push_back(std::move(NR
));
116 // Give up if the new system gets too big.
117 if (Constraints
.size() > 500)
126 bool ConstraintSystem::mayHaveSolutionImpl() {
127 while (!Constraints
.empty() && NumVariables
> 1) {
128 if (!eliminateUsingFM())
132 if (Constraints
.empty() || NumVariables
> 1)
135 return all_of(Constraints
, [](auto &R
) {
139 return R
[0].Coefficient
>= 0;
144 SmallVector
<std::string
> ConstraintSystem::getVarNamesList() const {
145 SmallVector
<std::string
> Names(Value2Index
.size(), "");
147 for (auto &[V
, Index
] : Value2Index
) {
148 std::string OperandName
;
149 if (V
->getName().empty())
150 OperandName
= V
->getNameOrAsOperand();
152 OperandName
= std::string("%") + V
->getName().str();
153 Names
[Index
- 1] = OperandName
;
159 void ConstraintSystem::dump() const {
161 if (Constraints
.empty())
163 SmallVector
<std::string
> Names
= getVarNamesList();
164 for (const auto &Row
: Constraints
) {
165 SmallVector
<std::string
, 16> Parts
;
166 for (unsigned I
= 0, S
= Row
.size(); I
< S
; ++I
) {
167 if (Row
[I
].Id
>= NumVariables
)
171 std::string Coefficient
;
172 if (Row
[I
].Coefficient
!= 1)
173 Coefficient
= std::to_string(Row
[I
].Coefficient
) + " * ";
174 Parts
.push_back(Coefficient
+ Names
[Row
[I
].Id
- 1]);
176 // assert(!Parts.empty() && "need to have at least some parts");
177 int64_t ConstPart
= 0;
179 ConstPart
= Row
[0].Coefficient
;
180 LLVM_DEBUG(dbgs() << join(Parts
, std::string(" + "))
181 << " <= " << std::to_string(ConstPart
) << "\n");
186 bool ConstraintSystem::mayHaveSolution() {
187 LLVM_DEBUG(dbgs() << "---\n");
189 bool HasSolution
= mayHaveSolutionImpl();
190 LLVM_DEBUG(dbgs() << (HasSolution
? "sat" : "unsat") << "\n");
194 bool ConstraintSystem::isConditionImplied(SmallVector
<int64_t, 8> R
) const {
195 // If all variable coefficients are 0, we have 'C >= 0'. If the constant is >=
196 // 0, R is always true, regardless of the system.
197 if (all_of(ArrayRef(R
).drop_front(1), [](int64_t C
) { return C
== 0; }))
200 // If there is no solution with the negation of R added to the system, the
201 // condition must hold based on the existing constraints.
202 R
= ConstraintSystem::negate(R
);
206 auto NewSystem
= *this;
207 NewSystem
.addVariableRow(R
);
208 return !NewSystem
.mayHaveSolution();