231 lines · cpp
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-exception6//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 the24 // paper Pugh, William. "The Omega test: a fast and practical integer25 // programming algorithm for dependence26 // 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 to35 // 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)41 Row1.pop_back();42 R1++;43 } else {44 std::swap(Constraints[R1], Constraints.back());45 RemainingRows.push_back(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 copy54 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: 360 // LowerLast: -261 int64_t UpperLast = getLastCoefficient(RemainingRows[R2], LastIdx);62 int64_t LowerLast = getLastCoefficient(RemainingRows[R1], 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(LowerR, UpperR);74 std::swap(LowerLast, 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(UpperRow[IdxUpper].Id, CurrentId);94 }95 if (IdxLower < LowerRow.size()) {96 CurrentId = std::min(LowerRow[IdxLower].Id, CurrentId);97 }98 99 if (IdxUpper < UpperRow.size() && UpperRow[IdxUpper].Id == CurrentId) {100 UpperV = UpperRow[IdxUpper].Coefficient;101 IdxUpper++;102 }103 104 if (MulOverflow(UpperV, -1 * LowerLast, 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(LowerV, UpperLast, M2))112 return false;113 // This algorithm is a variant of sparse Gaussian elimination.114 //115 // The new coefficient for CurrentId is116 // N = UpperV * (-1) * LowerLast + LowerV * UpperLast117 //118 // UpperRow: { 3, 2, 3 }, LowerLast: -2119 // LowerRow: { 0, 1, -2 }, UpperLast: 3120 //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 * x127 if (AddOverflow(M1, M2, N))128 return false;129 // Skip variable that is completely eliminated.130 if (N == 0)131 continue;132 NR.emplace_back(N, CurrentId);133 }134 if (NR.empty())135 continue;136 Constraints.push_back(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(Constraints, [](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 NDEBUG168 for (auto &[V, Index] : Value2Index) {169 std::string OperandName;170 if (V->getName().empty())171 OperandName = V->getNameOrAsOperand();172 else173 OperandName = std::string("%") + V->getName().str();174 Names[Index - 1] = OperandName;175 }176#endif177 return Names;178}179 180void ConstraintSystem::dump() const {181#ifndef NDEBUG182 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#endif205}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(ArrayRef(R).drop_front(1), [](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, the222 // 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