/Users/buildslave/jenkins/workspace/coverage/llvm-project/clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp
Line | Count | Source (jump to first uncovered line) |
1 | | //===- WatchedLiteralsSolver.cpp --------------------------------*- 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 | | // This file defines a SAT solver implementation that can be used by dataflow |
10 | | // analyses. |
11 | | // |
12 | | //===----------------------------------------------------------------------===// |
13 | | |
14 | | #include <cassert> |
15 | | #include <cstdint> |
16 | | #include <iterator> |
17 | | #include <queue> |
18 | | #include <vector> |
19 | | |
20 | | #include "clang/Analysis/FlowSensitive/Solver.h" |
21 | | #include "clang/Analysis/FlowSensitive/Value.h" |
22 | | #include "clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h" |
23 | | #include "llvm/ADT/DenseMap.h" |
24 | | #include "llvm/ADT/DenseSet.h" |
25 | | #include "llvm/ADT/STLExtras.h" |
26 | | |
27 | | namespace clang { |
28 | | namespace dataflow { |
29 | | |
30 | | // `WatchedLiteralsSolver` is an implementation of Algorithm D from Knuth's |
31 | | // The Art of Computer Programming Volume 4: Satisfiability, Fascicle 6. It is |
32 | | // based on the backtracking DPLL algorithm [1], keeps references to a single |
33 | | // "watched" literal per clause, and uses a set of "active" variables to perform |
34 | | // unit propagation. |
35 | | // |
36 | | // The solver expects that its input is a boolean formula in conjunctive normal |
37 | | // form that consists of clauses of at least one literal. A literal is either a |
38 | | // boolean variable or its negation. Below we define types, data structures, and |
39 | | // utilities that are used to represent boolean formulas in conjunctive normal |
40 | | // form. |
41 | | // |
42 | | // [1] https://en.wikipedia.org/wiki/DPLL_algorithm |
43 | | |
44 | | /// Boolean variables are represented as positive integers. |
45 | | using Variable = uint32_t; |
46 | | |
47 | | /// A null boolean variable is used as a placeholder in various data structures |
48 | | /// and algorithms. |
49 | | static constexpr Variable NullVar = 0; |
50 | | |
51 | | /// Literals are represented as positive integers. Specifically, for a boolean |
52 | | /// variable `V` that is represented as the positive integer `I`, the positive |
53 | | /// literal `V` is represented as the integer `2*I` and the negative literal |
54 | | /// `!V` is represented as the integer `2*I+1`. |
55 | | using Literal = uint32_t; |
56 | | |
57 | | /// A null literal is used as a placeholder in various data structures and |
58 | | /// algorithms. |
59 | | static constexpr Literal NullLit = 0; |
60 | | |
61 | | /// Returns the positive literal `V`. |
62 | 2.57M | static constexpr Literal posLit(Variable V) { return 2 * V; } |
63 | | |
64 | | /// Returns the negative literal `!V`. |
65 | 195k | static constexpr Literal negLit(Variable V) { return 2 * V + 1; } |
66 | | |
67 | | /// Returns the negated literal `!L`. |
68 | 5.70k | static constexpr Literal notLit(Literal L) { return L ^ 1; } |
69 | | |
70 | | /// Returns the variable of `L`. |
71 | 7.17M | static constexpr Variable var(Literal L) { return L >> 1; } |
72 | | |
73 | | /// Clause identifiers are represented as positive integers. |
74 | | using ClauseID = uint32_t; |
75 | | |
76 | | /// A null clause identifier is used as a placeholder in various data structures |
77 | | /// and algorithms. |
78 | | static constexpr ClauseID NullClause = 0; |
79 | | |
80 | | /// A boolean formula in conjunctive normal form. |
81 | | struct BooleanFormula { |
82 | | /// `LargestVar` is equal to the largest positive integer that represents a |
83 | | /// variable in the formula. |
84 | | const Variable LargestVar; |
85 | | |
86 | | /// Literals of all clauses in the formula. |
87 | | /// |
88 | | /// The element at index 0 stands for the literal in the null clause. It is |
89 | | /// set to 0 and isn't used. Literals of clauses in the formula start from the |
90 | | /// element at index 1. |
91 | | /// |
92 | | /// For example, for the formula `(L1 v L2) ^ (L2 v L3 v L4)` the elements of |
93 | | /// `Clauses` will be `[0, L1, L2, L2, L3, L4]`. |
94 | | std::vector<Literal> Clauses; |
95 | | |
96 | | /// Start indices of clauses of the formula in `Clauses`. |
97 | | /// |
98 | | /// The element at index 0 stands for the start index of the null clause. It |
99 | | /// is set to 0 and isn't used. Start indices of clauses in the formula start |
100 | | /// from the element at index 1. |
101 | | /// |
102 | | /// For example, for the formula `(L1 v L2) ^ (L2 v L3 v L4)` the elements of |
103 | | /// `ClauseStarts` will be `[0, 1, 3]`. Note that the literals of the first |
104 | | /// clause always start at index 1. The start index for the literals of the |
105 | | /// second clause depends on the size of the first clause and so on. |
106 | | std::vector<size_t> ClauseStarts; |
107 | | |
108 | | /// Maps literals (indices of the vector) to clause identifiers (elements of |
109 | | /// the vector) that watch the respective literals. |
110 | | /// |
111 | | /// For a given clause, its watched literal is always its first literal in |
112 | | /// `Clauses`. This invariant is maintained when watched literals change. |
113 | | std::vector<ClauseID> WatchedHead; |
114 | | |
115 | | /// Maps clause identifiers (elements of the vector) to identifiers of other |
116 | | /// clauses that watch the same literals, forming a set of linked lists. |
117 | | /// |
118 | | /// The element at index 0 stands for the identifier of the clause that |
119 | | /// follows the null clause. It is set to 0 and isn't used. Identifiers of |
120 | | /// clauses in the formula start from the element at index 1. |
121 | | std::vector<ClauseID> NextWatched; |
122 | | |
123 | | /// Stores the variable identifier and value location for atomic booleans in |
124 | | /// the formula. |
125 | | llvm::DenseMap<Variable, AtomicBoolValue *> Atomics; |
126 | | |
127 | | explicit BooleanFormula(Variable LargestVar, |
128 | | llvm::DenseMap<Variable, AtomicBoolValue *> Atomics) |
129 | 716 | : LargestVar(LargestVar), Atomics(std::move(Atomics)) { |
130 | 716 | Clauses.push_back(0); |
131 | 716 | ClauseStarts.push_back(0); |
132 | 716 | NextWatched.push_back(0); |
133 | 716 | const size_t NumLiterals = 2 * LargestVar + 1; |
134 | 716 | WatchedHead.resize(NumLiterals + 1, 0); |
135 | 716 | } |
136 | | |
137 | | /// Adds the `L1 v L2 v L3` clause to the formula. If `L2` or `L3` are |
138 | | /// `NullLit` they are respectively omitted from the clause. |
139 | | /// |
140 | | /// Requirements: |
141 | | /// |
142 | | /// `L1` must not be `NullLit`. |
143 | | /// |
144 | | /// All literals in the input that are not `NullLit` must be distinct. |
145 | 74.0k | void addClause(Literal L1, Literal L2 = NullLit, Literal L3 = NullLit) { |
146 | | // The literals are guaranteed to be distinct from properties of BoolValue |
147 | | // and the construction in `buildBooleanFormula`. |
148 | 74.0k | assert(L1 != NullLit && L1 != L2 && L1 != L3 && |
149 | 74.0k | (L2 != L3 || L2 == NullLit)); |
150 | | |
151 | 0 | const ClauseID C = ClauseStarts.size(); |
152 | 74.0k | const size_t S = Clauses.size(); |
153 | 74.0k | ClauseStarts.push_back(S); |
154 | | |
155 | 74.0k | Clauses.push_back(L1); |
156 | 74.0k | if (L2 != NullLit) |
157 | 65.8k | Clauses.push_back(L2); |
158 | 74.0k | if (L3 != NullLit) |
159 | 16.1k | Clauses.push_back(L3); |
160 | | |
161 | | // Designate the first literal as the "watched" literal of the clause. |
162 | 74.0k | NextWatched.push_back(WatchedHead[L1]); |
163 | 74.0k | WatchedHead[L1] = C; |
164 | 74.0k | } |
165 | | |
166 | | /// Returns the number of literals in clause `C`. |
167 | 173k | size_t clauseSize(ClauseID C) const { |
168 | 173k | return C == ClauseStarts.size() - 1 ? Clauses.size() - ClauseStarts[C]2.39k |
169 | 173k | : ClauseStarts[C + 1] - ClauseStarts[C]170k ; |
170 | 173k | } |
171 | | |
172 | | /// Returns the literals of clause `C`. |
173 | 173k | llvm::ArrayRef<Literal> clauseLiterals(ClauseID C) const { |
174 | 173k | return llvm::ArrayRef<Literal>(&Clauses[ClauseStarts[C]], clauseSize(C)); |
175 | 173k | } |
176 | | }; |
177 | | |
178 | | /// Converts the conjunction of `Vals` into a formula in conjunctive normal |
179 | | /// form where each clause has at least one and at most three literals. |
180 | 716 | BooleanFormula buildBooleanFormula(const llvm::DenseSet<BoolValue *> &Vals) { |
181 | | // The general strategy of the algorithm implemented below is to map each |
182 | | // of the sub-values in `Vals` to a unique variable and use these variables in |
183 | | // the resulting CNF expression to avoid exponential blow up. The number of |
184 | | // literals in the resulting formula is guaranteed to be linear in the number |
185 | | // of sub-values in `Vals`. |
186 | | |
187 | | // Map each sub-value in `Vals` to a unique variable. |
188 | 716 | llvm::DenseMap<BoolValue *, Variable> SubValsToVar; |
189 | | // Store variable identifiers and value location of atomic booleans. |
190 | 716 | llvm::DenseMap<Variable, AtomicBoolValue *> Atomics; |
191 | 716 | Variable NextVar = 1; |
192 | 716 | { |
193 | 716 | std::queue<BoolValue *> UnprocessedSubVals; |
194 | 716 | for (BoolValue *Val : Vals) |
195 | 8.18k | UnprocessedSubVals.push(Val); |
196 | 49.8k | while (!UnprocessedSubVals.empty()) { |
197 | 49.1k | Variable Var = NextVar; |
198 | 49.1k | BoolValue *Val = UnprocessedSubVals.front(); |
199 | 49.1k | UnprocessedSubVals.pop(); |
200 | | |
201 | 49.1k | if (!SubValsToVar.try_emplace(Val, Var).second) |
202 | 16.3k | continue; |
203 | 32.8k | ++NextVar; |
204 | | |
205 | | // Visit the sub-values of `Val`. |
206 | 32.8k | switch (Val->getKind()) { |
207 | 6.01k | case Value::Kind::Conjunction: { |
208 | 6.01k | auto *C = cast<ConjunctionValue>(Val); |
209 | 6.01k | UnprocessedSubVals.push(&C->getLeftSubValue()); |
210 | 6.01k | UnprocessedSubVals.push(&C->getRightSubValue()); |
211 | 6.01k | break; |
212 | 0 | } |
213 | 10.1k | case Value::Kind::Disjunction: { |
214 | 10.1k | auto *D = cast<DisjunctionValue>(Val); |
215 | 10.1k | UnprocessedSubVals.push(&D->getLeftSubValue()); |
216 | 10.1k | UnprocessedSubVals.push(&D->getRightSubValue()); |
217 | 10.1k | break; |
218 | 0 | } |
219 | 8.70k | case Value::Kind::Negation: { |
220 | 8.70k | auto *N = cast<NegationValue>(Val); |
221 | 8.70k | UnprocessedSubVals.push(&N->getSubVal()); |
222 | 8.70k | break; |
223 | 0 | } |
224 | 7.96k | case Value::Kind::AtomicBool: { |
225 | 7.96k | Atomics[Var] = cast<AtomicBoolValue>(Val); |
226 | 7.96k | break; |
227 | 0 | } |
228 | 0 | default: |
229 | 0 | llvm_unreachable("buildBooleanFormula: unhandled value kind"); |
230 | 32.8k | } |
231 | 32.8k | } |
232 | 716 | } |
233 | | |
234 | 98.3k | auto GetVar = [&SubValsToVar](const BoolValue *Val) 716 { |
235 | 98.3k | auto ValIt = SubValsToVar.find(Val); |
236 | 98.3k | assert(ValIt != SubValsToVar.end()); |
237 | 0 | return ValIt->second; |
238 | 98.3k | }; |
239 | | |
240 | 716 | BooleanFormula Formula(NextVar - 1, std::move(Atomics)); |
241 | 716 | std::vector<bool> ProcessedSubVals(NextVar, false); |
242 | | |
243 | | // Add a conjunct for each variable that represents a top-level conjunction |
244 | | // value in `Vals`. |
245 | 716 | for (BoolValue *Val : Vals) |
246 | 8.18k | Formula.addClause(posLit(GetVar(Val))); |
247 | | |
248 | | // Add conjuncts that represent the mapping between newly-created variables |
249 | | // and their corresponding sub-values. |
250 | 716 | std::queue<BoolValue *> UnprocessedSubVals; |
251 | 716 | for (BoolValue *Val : Vals) |
252 | 8.18k | UnprocessedSubVals.push(Val); |
253 | 49.8k | while (!UnprocessedSubVals.empty()) { |
254 | 49.1k | const BoolValue *Val = UnprocessedSubVals.front(); |
255 | 49.1k | UnprocessedSubVals.pop(); |
256 | 49.1k | const Variable Var = GetVar(Val); |
257 | | |
258 | 49.1k | if (ProcessedSubVals[Var]) |
259 | 16.3k | continue; |
260 | 32.8k | ProcessedSubVals[Var] = true; |
261 | | |
262 | 32.8k | if (auto *C = dyn_cast<ConjunctionValue>(Val)) { |
263 | 6.01k | const Variable LeftSubVar = GetVar(&C->getLeftSubValue()); |
264 | 6.01k | const Variable RightSubVar = GetVar(&C->getRightSubValue()); |
265 | | |
266 | | // `X <=> (A ^ B)` is equivalent to `(!X v A) ^ (!X v B) ^ (X v !A v !B)` |
267 | | // which is already in conjunctive normal form. Below we add each of the |
268 | | // conjuncts of the latter expression to the result. |
269 | 6.01k | Formula.addClause(negLit(Var), posLit(LeftSubVar)); |
270 | 6.01k | Formula.addClause(negLit(Var), posLit(RightSubVar)); |
271 | 6.01k | Formula.addClause(posLit(Var), negLit(LeftSubVar), negLit(RightSubVar)); |
272 | | |
273 | | // Visit the sub-values of `Val`. |
274 | 6.01k | UnprocessedSubVals.push(&C->getLeftSubValue()); |
275 | 6.01k | UnprocessedSubVals.push(&C->getRightSubValue()); |
276 | 26.7k | } else if (auto *D = dyn_cast<DisjunctionValue>(Val)) { |
277 | 10.1k | const Variable LeftSubVar = GetVar(&D->getLeftSubValue()); |
278 | 10.1k | const Variable RightSubVar = GetVar(&D->getRightSubValue()); |
279 | | |
280 | | // `X <=> (A v B)` is equivalent to `(!X v A v B) ^ (X v !A) ^ (X v !B)` |
281 | | // which is already in conjunctive normal form. Below we add each of the |
282 | | // conjuncts of the latter expression to the result. |
283 | 10.1k | Formula.addClause(negLit(Var), posLit(LeftSubVar), posLit(RightSubVar)); |
284 | 10.1k | Formula.addClause(posLit(Var), negLit(LeftSubVar)); |
285 | 10.1k | Formula.addClause(posLit(Var), negLit(RightSubVar)); |
286 | | |
287 | | // Visit the sub-values of `Val`. |
288 | 10.1k | UnprocessedSubVals.push(&D->getLeftSubValue()); |
289 | 10.1k | UnprocessedSubVals.push(&D->getRightSubValue()); |
290 | 16.6k | } else if (auto *N = dyn_cast<NegationValue>(Val)) { |
291 | 8.70k | const Variable SubVar = GetVar(&N->getSubVal()); |
292 | | |
293 | | // `X <=> !Y` is equivalent to `(!X v !Y) ^ (X v Y)` which is already in |
294 | | // conjunctive normal form. Below we add each of the conjuncts of the |
295 | | // latter expression to the result. |
296 | 8.70k | Formula.addClause(negLit(Var), negLit(SubVar)); |
297 | 8.70k | Formula.addClause(posLit(Var), posLit(SubVar)); |
298 | | |
299 | | // Visit the sub-values of `Val`. |
300 | 8.70k | UnprocessedSubVals.push(&N->getSubVal()); |
301 | 8.70k | } |
302 | 32.8k | } |
303 | | |
304 | 716 | return Formula; |
305 | 716 | } |
306 | | |
307 | | class WatchedLiteralsSolverImpl { |
308 | | /// A boolean formula in conjunctive normal form that the solver will attempt |
309 | | /// to prove satisfiable. The formula will be modified in the process. |
310 | | BooleanFormula Formula; |
311 | | |
312 | | /// The search for a satisfying assignment of the variables in `Formula` will |
313 | | /// proceed in levels, starting from 1 and going up to `Formula.LargestVar` |
314 | | /// (inclusive). The current level is stored in `Level`. At each level the |
315 | | /// solver will assign a value to an unassigned variable. If this leads to a |
316 | | /// consistent partial assignment, `Level` will be incremented. Otherwise, if |
317 | | /// it results in a conflict, the solver will backtrack by decrementing |
318 | | /// `Level` until it reaches the most recent level where a decision was made. |
319 | | size_t Level = 0; |
320 | | |
321 | | /// Maps levels (indices of the vector) to variables (elements of the vector) |
322 | | /// that are assigned values at the respective levels. |
323 | | /// |
324 | | /// The element at index 0 isn't used. Variables start from the element at |
325 | | /// index 1. |
326 | | std::vector<Variable> LevelVars; |
327 | | |
328 | | /// State of the solver at a particular level. |
329 | | enum class State : uint8_t { |
330 | | /// Indicates that the solver made a decision. |
331 | | Decision = 0, |
332 | | |
333 | | /// Indicates that the solver made a forced move. |
334 | | Forced = 1, |
335 | | }; |
336 | | |
337 | | /// State of the solver at a particular level. It keeps track of previous |
338 | | /// decisions that the solver can refer to when backtracking. |
339 | | /// |
340 | | /// The element at index 0 isn't used. States start from the element at index |
341 | | /// 1. |
342 | | std::vector<State> LevelStates; |
343 | | |
344 | | enum class Assignment : int8_t { |
345 | | Unassigned = -1, |
346 | | AssignedFalse = 0, |
347 | | AssignedTrue = 1 |
348 | | }; |
349 | | |
350 | | /// Maps variables (indices of the vector) to their assignments (elements of |
351 | | /// the vector). |
352 | | /// |
353 | | /// The element at index 0 isn't used. Variable assignments start from the |
354 | | /// element at index 1. |
355 | | std::vector<Assignment> VarAssignments; |
356 | | |
357 | | /// A set of unassigned variables that appear in watched literals in |
358 | | /// `Formula`. The vector is guaranteed to contain unique elements. |
359 | | std::vector<Variable> ActiveVars; |
360 | | |
361 | | public: |
362 | | explicit WatchedLiteralsSolverImpl(const llvm::DenseSet<BoolValue *> &Vals) |
363 | | : Formula(buildBooleanFormula(Vals)), LevelVars(Formula.LargestVar + 1), |
364 | 716 | LevelStates(Formula.LargestVar + 1) { |
365 | 716 | assert(!Vals.empty()); |
366 | | |
367 | | // Initialize the state at the root level to a decision so that in |
368 | | // `reverseForcedMoves` we don't have to check that `Level >= 0` on each |
369 | | // iteration. |
370 | 0 | LevelStates[0] = State::Decision; |
371 | | |
372 | | // Initialize all variables as unassigned. |
373 | 716 | VarAssignments.resize(Formula.LargestVar + 1, Assignment::Unassigned); |
374 | | |
375 | | // Initialize the active variables. |
376 | 33.5k | for (Variable Var = Formula.LargestVar; Var != NullVar; --Var32.8k ) { |
377 | 32.8k | if (isWatched(posLit(Var)) || isWatched(negLit(Var))5.97k ) |
378 | 26.8k | ActiveVars.push_back(Var); |
379 | 32.8k | } |
380 | 716 | } |
381 | | |
382 | 716 | Solver::Result solve() && { |
383 | 716 | size_t I = 0; |
384 | 66.9k | while (I < ActiveVars.size()) { |
385 | | // Assert that the following invariants hold: |
386 | | // 1. All active variables are unassigned. |
387 | | // 2. All active variables form watched literals. |
388 | | // 3. Unassigned variables that form watched literals are active. |
389 | | // FIXME: Consider replacing these with test cases that fail if the any |
390 | | // of the invariants is broken. That might not be easy due to the |
391 | | // transformations performed by `buildBooleanFormula`. |
392 | 66.5k | assert(activeVarsAreUnassigned()); |
393 | 0 | assert(activeVarsFormWatchedLiterals()); |
394 | 0 | assert(unassignedVarsFormingWatchedLiteralsAreActive()); |
395 | | |
396 | 0 | const Variable ActiveVar = ActiveVars[I]; |
397 | | |
398 | | // Look for unit clauses that contain the active variable. |
399 | 66.5k | const bool unitPosLit = watchedByUnitClause(posLit(ActiveVar)); |
400 | 66.5k | const bool unitNegLit = watchedByUnitClause(negLit(ActiveVar)); |
401 | 66.5k | if (unitPosLit && unitNegLit21.8k ) { |
402 | | // We found a conflict! |
403 | | |
404 | | // Backtrack and rewind the `Level` until the most recent non-forced |
405 | | // assignment. |
406 | 566 | reverseForcedMoves(); |
407 | | |
408 | | // If the root level is reached, then all possible assignments lead to |
409 | | // a conflict. |
410 | 566 | if (Level == 0) |
411 | 379 | return Solver::Result::Unsatisfiable(); |
412 | | |
413 | | // Otherwise, take the other branch at the most recent level where a |
414 | | // decision was made. |
415 | 187 | LevelStates[Level] = State::Forced; |
416 | 187 | const Variable Var = LevelVars[Level]; |
417 | 187 | VarAssignments[Var] = VarAssignments[Var] == Assignment::AssignedTrue |
418 | 187 | ? Assignment::AssignedFalse29 |
419 | 187 | : Assignment::AssignedTrue158 ; |
420 | | |
421 | 187 | updateWatchedLiterals(); |
422 | 66.0k | } else if (unitPosLit || unitNegLit44.7k ) { |
423 | | // We found a unit clause! The value of its unassigned variable is |
424 | | // forced. |
425 | 27.9k | ++Level; |
426 | | |
427 | 27.9k | LevelVars[Level] = ActiveVar; |
428 | 27.9k | LevelStates[Level] = State::Forced; |
429 | 27.9k | VarAssignments[ActiveVar] = |
430 | 27.9k | unitPosLit ? Assignment::AssignedTrue21.2k : Assignment::AssignedFalse6.71k ; |
431 | | |
432 | | // Remove the variable that was just assigned from the set of active |
433 | | // variables. |
434 | 27.9k | if (I + 1 < ActiveVars.size()) { |
435 | | // Replace the variable that was just assigned with the last active |
436 | | // variable for efficient removal. |
437 | 25.8k | ActiveVars[I] = ActiveVars.back(); |
438 | 25.8k | } else { |
439 | | // This was the last active variable. Repeat the process from the |
440 | | // beginning. |
441 | 2.16k | I = 0; |
442 | 2.16k | } |
443 | 27.9k | ActiveVars.pop_back(); |
444 | | |
445 | 27.9k | updateWatchedLiterals(); |
446 | 38.0k | } else if (I + 1 == ActiveVars.size()) { |
447 | | // There are no remaining unit clauses in the formula! Make a decision |
448 | | // for one of the active variables at the current level. |
449 | 449 | ++Level; |
450 | | |
451 | 449 | LevelVars[Level] = ActiveVar; |
452 | 449 | LevelStates[Level] = State::Decision; |
453 | 449 | VarAssignments[ActiveVar] = decideAssignment(ActiveVar); |
454 | | |
455 | | // Remove the variable that was just assigned from the set of active |
456 | | // variables. |
457 | 449 | ActiveVars.pop_back(); |
458 | | |
459 | 449 | updateWatchedLiterals(); |
460 | | |
461 | | // This was the last active variable. Repeat the process from the |
462 | | // beginning. |
463 | 449 | I = 0; |
464 | 37.5k | } else { |
465 | 37.5k | ++I; |
466 | 37.5k | } |
467 | 66.5k | } |
468 | 337 | return Solver::Result::Satisfiable(buildSolution()); |
469 | 716 | } |
470 | | |
471 | | private: |
472 | | /// Returns a satisfying truth assignment to the atomic values in the boolean |
473 | | /// formula. |
474 | | llvm::DenseMap<AtomicBoolValue *, Solver::Result::Assignment> |
475 | 337 | buildSolution() { |
476 | 337 | llvm::DenseMap<AtomicBoolValue *, Solver::Result::Assignment> Solution; |
477 | 4.32k | for (auto &Atomic : Formula.Atomics) { |
478 | | // A variable may have a definite true/false assignment, or it may be |
479 | | // unassigned indicating its truth value does not affect the result of |
480 | | // the formula. Unassigned variables are assigned to true as a default. |
481 | 4.32k | Solution[Atomic.second] = |
482 | 4.32k | VarAssignments[Atomic.first] == Assignment::AssignedFalse |
483 | 4.32k | ? Solver::Result::Assignment::AssignedFalse981 |
484 | 4.32k | : Solver::Result::Assignment::AssignedTrue3.34k ; |
485 | 4.32k | } |
486 | 337 | return Solution; |
487 | 337 | } |
488 | | |
489 | | /// Reverses forced moves until the most recent level where a decision was |
490 | | /// made on the assignment of a variable. |
491 | 566 | void reverseForcedMoves() { |
492 | 10.9k | for (; LevelStates[Level] == State::Forced; --Level10.3k ) { |
493 | 10.3k | const Variable Var = LevelVars[Level]; |
494 | | |
495 | 10.3k | VarAssignments[Var] = Assignment::Unassigned; |
496 | | |
497 | | // If the variable that we pass through is watched then we add it to the |
498 | | // active variables. |
499 | 10.3k | if (isWatched(posLit(Var)) || isWatched(negLit(Var))2.37k ) |
500 | 10.3k | ActiveVars.push_back(Var); |
501 | 10.3k | } |
502 | 566 | } |
503 | | |
504 | | /// Updates watched literals that are affected by a variable assignment. |
505 | 28.6k | void updateWatchedLiterals() { |
506 | 28.6k | const Variable Var = LevelVars[Level]; |
507 | | |
508 | | // Update the watched literals of clauses that currently watch the literal |
509 | | // that falsifies `Var`. |
510 | 28.6k | const Literal FalseLit = VarAssignments[Var] == Assignment::AssignedTrue |
511 | 28.6k | ? negLit(Var)21.4k |
512 | 28.6k | : posLit(Var)7.13k ; |
513 | 28.6k | ClauseID FalseLitWatcher = Formula.WatchedHead[FalseLit]; |
514 | 28.6k | Formula.WatchedHead[FalseLit] = NullClause; |
515 | 61.6k | while (FalseLitWatcher != NullClause) { |
516 | 33.0k | const ClauseID NextFalseLitWatcher = Formula.NextWatched[FalseLitWatcher]; |
517 | | |
518 | | // Pick the first non-false literal as the new watched literal. |
519 | 33.0k | const size_t FalseLitWatcherStart = Formula.ClauseStarts[FalseLitWatcher]; |
520 | 33.0k | size_t NewWatchedLitIdx = FalseLitWatcherStart + 1; |
521 | 39.5k | while (isCurrentlyFalse(Formula.Clauses[NewWatchedLitIdx])) |
522 | 6.59k | ++NewWatchedLitIdx; |
523 | 33.0k | const Literal NewWatchedLit = Formula.Clauses[NewWatchedLitIdx]; |
524 | 33.0k | const Variable NewWatchedLitVar = var(NewWatchedLit); |
525 | | |
526 | | // Swap the old watched literal for the new one in `FalseLitWatcher` to |
527 | | // maintain the invariant that the watched literal is at the beginning of |
528 | | // the clause. |
529 | 33.0k | Formula.Clauses[NewWatchedLitIdx] = FalseLit; |
530 | 33.0k | Formula.Clauses[FalseLitWatcherStart] = NewWatchedLit; |
531 | | |
532 | | // If the new watched literal isn't watched by any other clause and its |
533 | | // variable isn't assigned we need to add it to the active variables. |
534 | 33.0k | if (!isWatched(NewWatchedLit) && !isWatched(notLit(NewWatchedLit))5.70k && |
535 | 33.0k | VarAssignments[NewWatchedLitVar] == Assignment::Unassigned4.98k ) |
536 | 4.82k | ActiveVars.push_back(NewWatchedLitVar); |
537 | | |
538 | 33.0k | Formula.NextWatched[FalseLitWatcher] = Formula.WatchedHead[NewWatchedLit]; |
539 | 33.0k | Formula.WatchedHead[NewWatchedLit] = FalseLitWatcher; |
540 | | |
541 | | // Go to the next clause that watches `FalseLit`. |
542 | 33.0k | FalseLitWatcher = NextFalseLitWatcher; |
543 | 33.0k | } |
544 | 28.6k | } |
545 | | |
546 | | /// Returns true if and only if one of the clauses that watch `Lit` is a unit |
547 | | /// clause. |
548 | 133k | bool watchedByUnitClause(Literal Lit) const { |
549 | 133k | for (ClauseID LitWatcher = Formula.WatchedHead[Lit]; |
550 | 277k | LitWatcher != NullClause; |
551 | 173k | LitWatcher = Formula.NextWatched[LitWatcher]144k ) { |
552 | 173k | llvm::ArrayRef<Literal> Clause = Formula.clauseLiterals(LitWatcher); |
553 | | |
554 | | // Assert the invariant that the watched literal is always the first one |
555 | | // in the clause. |
556 | | // FIXME: Consider replacing this with a test case that fails if the |
557 | | // invariant is broken by `updateWatchedLiterals`. That might not be easy |
558 | | // due to the transformations performed by `buildBooleanFormula`. |
559 | 173k | assert(Clause.front() == Lit); |
560 | | |
561 | 173k | if (isUnit(Clause)) |
562 | 29.1k | return true; |
563 | 173k | } |
564 | 104k | return false; |
565 | 133k | } |
566 | | |
567 | | /// Returns true if and only if `Clause` is a unit clause. |
568 | 173k | bool isUnit(llvm::ArrayRef<Literal> Clause) const { |
569 | 173k | return llvm::all_of(Clause.drop_front(), |
570 | 193k | [this](Literal L) { return isCurrentlyFalse(L); }); |
571 | 173k | } |
572 | | |
573 | | /// Returns true if and only if `Lit` evaluates to `false` in the current |
574 | | /// partial assignment. |
575 | 233k | bool isCurrentlyFalse(Literal Lit) const { |
576 | 233k | return static_cast<int8_t>(VarAssignments[var(Lit)]) == |
577 | 233k | static_cast<int8_t>(Lit & 1); |
578 | 233k | } |
579 | | |
580 | | /// Returns true if and only if `Lit` is watched by a clause in `Formula`. |
581 | 91.0k | bool isWatched(Literal Lit) const { |
582 | 91.0k | return Formula.WatchedHead[Lit] != NullClause; |
583 | 91.0k | } |
584 | | |
585 | | /// Returns an assignment for an unassigned variable. |
586 | 449 | Assignment decideAssignment(Variable Var) const { |
587 | 449 | return !isWatched(posLit(Var)) || isWatched(negLit(Var))413 |
588 | 449 | ? Assignment::AssignedFalse398 |
589 | 449 | : Assignment::AssignedTrue51 ; |
590 | 449 | } |
591 | | |
592 | | /// Returns a set of all watched literals. |
593 | 133k | llvm::DenseSet<Literal> watchedLiterals() const { |
594 | 133k | llvm::DenseSet<Literal> WatchedLiterals; |
595 | 21.5M | for (Literal Lit = 2; Lit < Formula.WatchedHead.size(); Lit++21.4M ) { |
596 | 21.4M | if (Formula.WatchedHead[Lit] == NullClause) |
597 | 7.61M | continue; |
598 | 13.8M | WatchedLiterals.insert(Lit); |
599 | 13.8M | } |
600 | 133k | return WatchedLiterals; |
601 | 133k | } |
602 | | |
603 | | /// Returns true if and only if all active variables are unassigned. |
604 | 66.5k | bool activeVarsAreUnassigned() const { |
605 | 2.37M | return llvm::all_of(ActiveVars, [this](Variable Var) { |
606 | 2.37M | return VarAssignments[Var] == Assignment::Unassigned; |
607 | 2.37M | }); |
608 | 66.5k | } |
609 | | |
610 | | /// Returns true if and only if all active variables form watched literals. |
611 | 66.5k | bool activeVarsFormWatchedLiterals() const { |
612 | 66.5k | const llvm::DenseSet<Literal> WatchedLiterals = watchedLiterals(); |
613 | 2.37M | return llvm::all_of(ActiveVars, [&WatchedLiterals](Variable Var) { |
614 | 2.37M | return WatchedLiterals.contains(posLit(Var)) || |
615 | 2.37M | WatchedLiterals.contains(negLit(Var))26.9k ; |
616 | 2.37M | }); |
617 | 66.5k | } |
618 | | |
619 | | /// Returns true if and only if all unassigned variables that are forming |
620 | | /// watched literals are active. |
621 | 66.5k | bool unassignedVarsFormingWatchedLiteralsAreActive() const { |
622 | 66.5k | const llvm::DenseSet<Variable> ActiveVarsSet(ActiveVars.begin(), |
623 | 66.5k | ActiveVars.end()); |
624 | 6.90M | for (Literal Lit : watchedLiterals()) { |
625 | 6.90M | const Variable Var = var(Lit); |
626 | 6.90M | if (VarAssignments[Var] != Assignment::Unassigned) |
627 | 2.28M | continue; |
628 | 4.61M | if (ActiveVarsSet.contains(Var)) |
629 | 4.61M | continue; |
630 | 0 | return false; |
631 | 4.61M | } |
632 | 66.5k | return true; |
633 | 66.5k | } |
634 | | }; |
635 | | |
636 | 716 | Solver::Result WatchedLiteralsSolver::solve(llvm::DenseSet<BoolValue *> Vals) { |
637 | 716 | return Vals.empty() ? Solver::Result::Satisfiable({{}})0 |
638 | 716 | : WatchedLiteralsSolverImpl(Vals).solve(); |
639 | 716 | } |
640 | | |
641 | | } // namespace dataflow |
642 | | } // namespace clang |