blob: 9739c6af5769a4348781fc00a649f024f382e9c7 [file] [log] [blame]
//===- ConstraintSytem.cpp - A system of linear constraints. ----*- C++ -*-===//
//
// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
// See https://llvm.org/LICENSE.txt for license information.
// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
//
//===----------------------------------------------------------------------===//
#include "llvm/Analysis/ConstraintSystem.h"
#include "llvm/ADT/SmallVector.h"
#include "llvm/Support/MathExtras.h"
#include "llvm/ADT/StringExtras.h"
#include "llvm/Support/Debug.h"
#include <algorithm>
#include <string>
using namespace llvm;
#define DEBUG_TYPE "constraint-system"
bool ConstraintSystem::eliminateUsingFM() {
// Implementation of Fourier–Motzkin elimination, with some tricks from the
// paper Pugh, William. "The Omega test: a fast and practical integer
// programming algorithm for dependence
// analysis."
// Supercomputing'91: Proceedings of the 1991 ACM/
// IEEE conference on Supercomputing. IEEE, 1991.
assert(!Constraints.empty() &&
"should only be called for non-empty constraint systems");
unsigned NumVariables = Constraints[0].size();
SmallVector<SmallVector<int64_t, 8>, 4> NewSystem;
unsigned NumConstraints = Constraints.size();
uint32_t NewGCD = 1;
// FIXME do not use copy
for (unsigned R1 = 0; R1 < NumConstraints; R1++) {
if (Constraints[R1][1] == 0) {
SmallVector<int64_t, 8> NR;
NR.push_back(Constraints[R1][0]);
for (unsigned i = 2; i < NumVariables; i++) {
NR.push_back(Constraints[R1][i]);
}
NewSystem.push_back(std::move(NR));
continue;
}
// FIXME do not use copy
for (unsigned R2 = R1 + 1; R2 < NumConstraints; R2++) {
if (R1 == R2)
continue;
// FIXME: can we do better than just dropping things here?
if (Constraints[R2][1] == 0)
continue;
if ((Constraints[R1][1] < 0 && Constraints[R2][1] < 0) ||
(Constraints[R1][1] > 0 && Constraints[R2][1] > 0))
continue;
unsigned LowerR = R1;
unsigned UpperR = R2;
if (Constraints[UpperR][1] < 0)
std::swap(LowerR, UpperR);
SmallVector<int64_t, 8> NR;
for (unsigned I = 0; I < NumVariables; I++) {
if (I == 1)
continue;
int64_t M1, M2, N;
if (MulOverflow(Constraints[UpperR][I],
((-1) * Constraints[LowerR][1] / GCD), M1))
return false;
if (MulOverflow(Constraints[LowerR][I],
(Constraints[UpperR][1] / GCD), M2))
return false;
if (AddOverflow(M1, M2, N))
return false;
NR.push_back(N);
NewGCD = APIntOps::GreatestCommonDivisor({32, (uint32_t)NR.back()},
{32, NewGCD})
.getZExtValue();
}
NewSystem.push_back(std::move(NR));
// Give up if the new system gets too big.
if (NewSystem.size() > 500)
return false;
}
}
Constraints = std::move(NewSystem);
GCD = NewGCD;
return true;
}
bool ConstraintSystem::mayHaveSolutionImpl() {
while (!Constraints.empty() && Constraints[0].size() > 1) {
if (!eliminateUsingFM())
return true;
}
if (Constraints.empty() || Constraints[0].size() > 1)
return true;
return all_of(Constraints, [](auto &R) { return R[0] >= 0; });
}
void ConstraintSystem::dump(ArrayRef<std::string> Names) const {
if (Constraints.empty())
return;
for (auto &Row : Constraints) {
SmallVector<std::string, 16> Parts;
for (unsigned I = 1, S = Row.size(); I < S; ++I) {
if (Row[I] == 0)
continue;
std::string Coefficient;
if (Row[I] != 1)
Coefficient = std::to_string(Row[I]) + " * ";
Parts.push_back(Coefficient + Names[I - 1]);
}
assert(!Parts.empty() && "need to have at least some parts");
LLVM_DEBUG(dbgs() << join(Parts, std::string(" + "))
<< " <= " << std::to_string(Row[0]) << "\n");
}
}
void ConstraintSystem::dump() const {
SmallVector<std::string, 16> Names;
for (unsigned i = 1; i < Constraints.back().size(); ++i)
Names.push_back("x" + std::to_string(i));
LLVM_DEBUG(dbgs() << "---\n");
dump(Names);
}
bool ConstraintSystem::mayHaveSolution() {
LLVM_DEBUG(dump());
bool HasSolution = mayHaveSolutionImpl();
LLVM_DEBUG(dbgs() << (HasSolution ? "sat" : "unsat") << "\n");
return HasSolution;
}
bool ConstraintSystem::isConditionImplied(SmallVector<int64_t, 8> R) {
// If all variable coefficients are 0, we have 'C >= 0'. If the constant is >=
// 0, R is always true, regardless of the system.
if (all_of(makeArrayRef(R).drop_front(1), [](int64_t C) { return C == 0; }))
return R[0] >= 0;
// If there is no solution with the negation of R added to the system, the
// condition must hold based on the existing constraints.
R = ConstraintSystem::negate(R);
auto NewSystem = *this;
NewSystem.addVariableRow(R);
return !NewSystem.mayHaveSolution();
}