ConstraintSystem.cpp Source File (original) (raw)

16#include

18using namespace llvm;

20#define DEBUG_TYPE "constraint-system"

22bool ConstraintSystem::eliminateUsingFM() {

29 assert(!Constraints.empty() &&

30 "should only be called for non-empty constraint systems");

32 unsigned LastIdx = NumVariables - 1;

37 for (unsigned R1 = 0; R1 < Constraints.size();) {

39 if (getLastCoefficient(Row1, LastIdx) == 0) {

40 if (Row1.size() > 0 && Row1.back().Id == LastIdx)

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 }

51 unsigned NumRemainingConstraints = RemainingRows.size();

52 for (unsigned R1 = 0; R1 < NumRemainingConstraints; R1++) {

54 for (unsigned R2 = R1 + 1; R2 < NumRemainingConstraints; R2++) {

61 int64_t UpperLast = getLastCoefficient(RemainingRows[R2], LastIdx);

62 int64_t LowerLast = getLastCoefficient(RemainingRows[R1], LastIdx);

64 UpperLast != 0 && LowerLast != 0 &&

65 "RemainingRows should only contain rows where the variable is != 0");

67 if ((LowerLast < 0 && UpperLast < 0) || (LowerLast > 0 && UpperLast > 0))

68 continue;

70 unsigned LowerR = R1;

71 unsigned UpperR = R2;

72 if (UpperLast < 0) {

75 }

78 unsigned IdxUpper = 0;

79 unsigned IdxLower = 0;

80 auto &LowerRow = RemainingRows[LowerR];

81 auto &UpperRow = RemainingRows[UpperR];

84 while (true) {

85 if (IdxUpper >= UpperRow.size() || IdxLower >= LowerRow.size())

86 break;

87 int64_t M1, M2, N;

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 }

99 if (IdxUpper < UpperRow.size() && UpperRow[IdxUpper].Id == CurrentId) {

100 UpperV = UpperRow[IdxUpper].Coefficient;

101 IdxUpper++;

102 }

103

105 return false;

106 if (IdxLower < LowerRow.size() && LowerRow[IdxLower].Id == CurrentId) {

107 LowerV = LowerRow[IdxLower].Coefficient;

108 IdxLower++;

109 }

110

112 return false;

113

114

115

116

117

118

119

120

121

122

123

124

125

126

128 return false;

129

130 if (N == 0)

131 continue;

133 }

135 continue;

136 Constraints.push_back(std::move(NR));

137

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

166 SmallVectorstd::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

181#ifndef NDEBUG

182 if (Constraints.empty())

183 return;

185 for (const auto &Row : Constraints) {

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

198 int64_t ConstPart = 0;

199 if (Row[0].Id == 0)

200 ConstPart = Row[0].Coefficient;

202 << " <= " << std::to_string(ConstPart) << "\n");

203 }

204#endif

205}

206

210 bool HasSolution = mayHaveSolutionImpl();

211 LLVM_DEBUG(dbgs() << (HasSolution ? "sat" : "unsat") << "\n");

212 return HasSolution;

213}

214

216

217

218 if (all_of(ArrayRef(R).drop_front(1), [](int64_t C) { return C == 0; }))

219 return R[0] >= 0;

220

221

222

224 if (R.empty())

225 return false;

226

227 auto NewSystem = *this;

228 NewSystem.addVariableRow(R);

229 return !NewSystem.mayHaveSolution();

230}

assert(UImm &&(UImm !=~static_cast< T >(0)) &&"Invalid immediate!")

This file defines the SmallVector class.

static SmallVector< int64_t, 8 > negate(SmallVector< int64_t, 8 > R)

LLVM_ABI bool mayHaveSolution()

Returns true if there may be a solution for the constraints in the system.

Definition ConstraintSystem.cpp:207

LLVM_ABI bool isConditionImplied(SmallVector< int64_t, 8 > R) const

Definition ConstraintSystem.cpp:215

LLVM_ABI void dump() const

Print the constraints in the system.

Definition ConstraintSystem.cpp:180

reference emplace_back(ArgTypes &&... Args)

void push_back(const T &Elt)

This is a 'vector' (really, a variable-sized array), optimized for the case when the array is small.

@ C

The default llvm calling convention, compatible with C.

This is an optimization pass for GlobalISel generic memory operations.

std::enable_if_t< std::is_signed_v< T >, T > MulOverflow(T X, T Y, T &Result)

Multiply two signed integers, computing the two's complement truncated result, returning true if an o...

bool all_of(R &&range, UnaryPredicate P)

Provide wrappers to std::all_of which take ranges instead of having to pass begin/end explicitly.

unsigned M1(unsigned Val)

LLVM_ABI raw_ostream & dbgs()

dbgs() - This returns a reference to a raw_ostream for debugging messages.

std::string join(IteratorT Begin, IteratorT End, StringRef Separator)

Joins the strings in the range [Begin, End), adding Separator between the elements.

ArrayRef(const T &OneElt) -> ArrayRef< T >

std::enable_if_t< std::is_signed_v< T >, T > AddOverflow(T X, T Y, T &Result)

Add two signed integers, computing the two's complement truncated result, returning true if overflow ...

void swap(llvm::BitVector &LHS, llvm::BitVector &RHS)

Implement std::swap in terms of BitVector swap.