/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 | 399k | static constexpr Literal posLit(Variable V) { return 2 * V; } |
63 | | |
64 | | /// Returns the negative literal `!V`. |
65 | 51.7k | static constexpr Literal negLit(Variable V) { return 2 * V + 1; } |
66 | | |
67 | | /// Returns the negated literal `!L`. |
68 | 2.30k | static constexpr Literal notLit(Literal L) { return L ^ 1; } |
69 | | |
70 | | /// Returns the variable of `L`. |
71 | 942k | 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 | 447 | explicit BooleanFormula(Variable LargestVar) : LargestVar(LargestVar) { |
124 | 447 | Clauses.push_back(0); |
125 | 447 | ClauseStarts.push_back(0); |
126 | 447 | NextWatched.push_back(0); |
127 | 447 | const size_t NumLiterals = 2 * LargestVar + 1; |
128 | 447 | WatchedHead.resize(NumLiterals + 1, 0); |
129 | 447 | } |
130 | | |
131 | | /// Adds the `L1 v L2 v L3` clause to the formula. If `L2` or `L3` are |
132 | | /// `NullLit` they are respectively omitted from the clause. |
133 | | /// |
134 | | /// Requirements: |
135 | | /// |
136 | | /// `L1` must not be `NullLit`. |
137 | | /// |
138 | | /// All literals in the input that are not `NullLit` must be distinct. |
139 | 24.8k | void addClause(Literal L1, Literal L2 = NullLit, Literal L3 = NullLit) { |
140 | | // The literals are guaranteed to be distinct from properties of BoolValue |
141 | | // and the construction in `buildBooleanFormula`. |
142 | 24.8k | assert(L1 != NullLit && L1 != L2 && L1 != L3 && |
143 | 24.8k | (L2 != L3 || L2 == NullLit)); |
144 | | |
145 | 0 | const ClauseID C = ClauseStarts.size(); |
146 | 24.8k | const size_t S = Clauses.size(); |
147 | 24.8k | ClauseStarts.push_back(S); |
148 | | |
149 | 24.8k | Clauses.push_back(L1); |
150 | 24.8k | if (L2 != NullLit) |
151 | 19.0k | Clauses.push_back(L2); |
152 | 24.8k | if (L3 != NullLit) |
153 | 4.13k | Clauses.push_back(L3); |
154 | | |
155 | | // Designate the first literal as the "watched" literal of the clause. |
156 | 24.8k | NextWatched.push_back(WatchedHead[L1]); |
157 | 24.8k | WatchedHead[L1] = C; |
158 | 24.8k | } |
159 | | |
160 | | /// Returns the number of literals in clause `C`. |
161 | 40.0k | size_t clauseSize(ClauseID C) const { |
162 | 40.0k | return C == ClauseStarts.size() - 1 ? Clauses.size() - ClauseStarts[C]991 |
163 | 40.0k | : ClauseStarts[C + 1] - ClauseStarts[C]39.0k ; |
164 | 40.0k | } |
165 | | |
166 | | /// Returns the literals of clause `C`. |
167 | 40.0k | llvm::ArrayRef<Literal> clauseLiterals(ClauseID C) const { |
168 | 40.0k | return llvm::ArrayRef<Literal>(&Clauses[ClauseStarts[C]], clauseSize(C)); |
169 | 40.0k | } |
170 | | }; |
171 | | |
172 | | /// Converts the conjunction of `Vals` into a formula in conjunctive normal |
173 | | /// form where each clause has at least one and at most three literals. |
174 | 447 | BooleanFormula buildBooleanFormula(const llvm::DenseSet<BoolValue *> &Vals) { |
175 | | // The general strategy of the algorithm implemented below is to map each |
176 | | // of the sub-values in `Vals` to a unique variable and use these variables in |
177 | | // the resulting CNF expression to avoid exponential blow up. The number of |
178 | | // literals in the resulting formula is guaranteed to be linear in the number |
179 | | // of sub-values in `Vals`. |
180 | | |
181 | | // Map each sub-value in `Vals` to a unique variable. |
182 | 447 | llvm::DenseMap<BoolValue *, Variable> SubValsToVar; |
183 | 447 | Variable NextVar = 1; |
184 | 447 | { |
185 | 447 | std::queue<BoolValue *> UnprocessedSubVals; |
186 | 447 | for (BoolValue *Val : Vals) |
187 | 5.79k | UnprocessedSubVals.push(Val); |
188 | 17.8k | while (!UnprocessedSubVals.empty()) { |
189 | 17.4k | BoolValue *Val = UnprocessedSubVals.front(); |
190 | 17.4k | UnprocessedSubVals.pop(); |
191 | | |
192 | 17.4k | if (!SubValsToVar.try_emplace(Val, NextVar).second) |
193 | 6.59k | continue; |
194 | 10.8k | ++NextVar; |
195 | | |
196 | | // Visit the sub-values of `Val`. |
197 | 10.8k | if (auto *C = dyn_cast<ConjunctionValue>(Val)) { |
198 | 36 | UnprocessedSubVals.push(&C->getLeftSubValue()); |
199 | 36 | UnprocessedSubVals.push(&C->getRightSubValue()); |
200 | 10.7k | } else if (auto *D = dyn_cast<DisjunctionValue>(Val)) { |
201 | 4.09k | UnprocessedSubVals.push(&D->getLeftSubValue()); |
202 | 4.09k | UnprocessedSubVals.push(&D->getRightSubValue()); |
203 | 6.68k | } else if (auto *N = dyn_cast<NegationValue>(Val)) { |
204 | 3.34k | UnprocessedSubVals.push(&N->getSubVal()); |
205 | 3.34k | } |
206 | 10.8k | } |
207 | 447 | } |
208 | | |
209 | 34.8k | auto GetVar = [&SubValsToVar](const BoolValue *Val) { |
210 | 34.8k | auto ValIt = SubValsToVar.find(Val); |
211 | 34.8k | assert(ValIt != SubValsToVar.end()); |
212 | 0 | return ValIt->second; |
213 | 34.8k | }; |
214 | | |
215 | 447 | BooleanFormula Formula(NextVar - 1); |
216 | 447 | std::vector<bool> ProcessedSubVals(NextVar, false); |
217 | | |
218 | | // Add a conjunct for each variable that represents a top-level conjunction |
219 | | // value in `Vals`. |
220 | 447 | for (BoolValue *Val : Vals) |
221 | 5.79k | Formula.addClause(posLit(GetVar(Val))); |
222 | | |
223 | | // Add conjuncts that represent the mapping between newly-created variables |
224 | | // and their corresponding sub-values. |
225 | 447 | std::queue<BoolValue *> UnprocessedSubVals; |
226 | 447 | for (BoolValue *Val : Vals) |
227 | 5.79k | UnprocessedSubVals.push(Val); |
228 | 17.8k | while (!UnprocessedSubVals.empty()) { |
229 | 17.4k | const BoolValue *Val = UnprocessedSubVals.front(); |
230 | 17.4k | UnprocessedSubVals.pop(); |
231 | 17.4k | const Variable Var = GetVar(Val); |
232 | | |
233 | 17.4k | if (ProcessedSubVals[Var]) |
234 | 6.59k | continue; |
235 | 10.8k | ProcessedSubVals[Var] = true; |
236 | | |
237 | 10.8k | if (auto *C = dyn_cast<ConjunctionValue>(Val)) { |
238 | 36 | const Variable LeftSubVar = GetVar(&C->getLeftSubValue()); |
239 | 36 | const Variable RightSubVar = GetVar(&C->getRightSubValue()); |
240 | | |
241 | | // `X <=> (A ^ B)` is equivalent to `(!X v A) ^ (!X v B) ^ (X v !A v !B)` |
242 | | // which is already in conjunctive normal form. Below we add each of the |
243 | | // conjuncts of the latter expression to the result. |
244 | 36 | Formula.addClause(negLit(Var), posLit(LeftSubVar)); |
245 | 36 | Formula.addClause(negLit(Var), posLit(RightSubVar)); |
246 | 36 | Formula.addClause(posLit(Var), negLit(LeftSubVar), negLit(RightSubVar)); |
247 | | |
248 | | // Visit the sub-values of `Val`. |
249 | 36 | UnprocessedSubVals.push(&C->getLeftSubValue()); |
250 | 36 | UnprocessedSubVals.push(&C->getRightSubValue()); |
251 | 10.7k | } else if (auto *D = dyn_cast<DisjunctionValue>(Val)) { |
252 | 4.09k | const Variable LeftSubVar = GetVar(&D->getLeftSubValue()); |
253 | 4.09k | const Variable RightSubVar = GetVar(&D->getRightSubValue()); |
254 | | |
255 | | // `X <=> (A v B)` is equivalent to `(!X v A v B) ^ (X v !A) ^ (X v !B)` |
256 | | // which is already in conjunctive normal form. Below we add each of the |
257 | | // conjuncts of the latter expression to the result. |
258 | 4.09k | Formula.addClause(negLit(Var), posLit(LeftSubVar), posLit(RightSubVar)); |
259 | 4.09k | Formula.addClause(posLit(Var), negLit(LeftSubVar)); |
260 | 4.09k | Formula.addClause(posLit(Var), negLit(RightSubVar)); |
261 | | |
262 | | // Visit the sub-values of `Val`. |
263 | 4.09k | UnprocessedSubVals.push(&D->getLeftSubValue()); |
264 | 4.09k | UnprocessedSubVals.push(&D->getRightSubValue()); |
265 | 6.68k | } else if (auto *N = dyn_cast<NegationValue>(Val)) { |
266 | 3.34k | const Variable SubVar = GetVar(&N->getSubVal()); |
267 | | |
268 | | // `X <=> !Y` is equivalent to `(!X v !Y) ^ (X v Y)` which is already in |
269 | | // conjunctive normal form. Below we add each of the conjuncts of the |
270 | | // latter expression to the result. |
271 | 3.34k | Formula.addClause(negLit(Var), negLit(SubVar)); |
272 | 3.34k | Formula.addClause(posLit(Var), posLit(SubVar)); |
273 | | |
274 | | // Visit the sub-values of `Val`. |
275 | 3.34k | UnprocessedSubVals.push(&N->getSubVal()); |
276 | 3.34k | } |
277 | 10.8k | } |
278 | | |
279 | 447 | return Formula; |
280 | 447 | } |
281 | | |
282 | | class WatchedLiteralsSolverImpl { |
283 | | /// A boolean formula in conjunctive normal form that the solver will attempt |
284 | | /// to prove satisfiable. The formula will be modified in the process. |
285 | | BooleanFormula Formula; |
286 | | |
287 | | /// The search for a satisfying assignment of the variables in `Formula` will |
288 | | /// proceed in levels, starting from 1 and going up to `Formula.LargestVar` |
289 | | /// (inclusive). The current level is stored in `Level`. At each level the |
290 | | /// solver will assign a value to an unassigned variable. If this leads to a |
291 | | /// consistent partial assignment, `Level` will be incremented. Otherwise, if |
292 | | /// it results in a conflict, the solver will backtrack by decrementing |
293 | | /// `Level` until it reaches the most recent level where a decision was made. |
294 | | size_t Level = 0; |
295 | | |
296 | | /// Maps levels (indices of the vector) to variables (elements of the vector) |
297 | | /// that are assigned values at the respective levels. |
298 | | /// |
299 | | /// The element at index 0 isn't used. Variables start from the element at |
300 | | /// index 1. |
301 | | std::vector<Variable> LevelVars; |
302 | | |
303 | | /// State of the solver at a particular level. |
304 | | enum class State : uint8_t { |
305 | | /// Indicates that the solver made a decision. |
306 | | Decision = 0, |
307 | | |
308 | | /// Indicates that the solver made a forced move. |
309 | | Forced = 1, |
310 | | }; |
311 | | |
312 | | /// State of the solver at a particular level. It keeps track of previous |
313 | | /// decisions that the solver can refer to when backtracking. |
314 | | /// |
315 | | /// The element at index 0 isn't used. States start from the element at index |
316 | | /// 1. |
317 | | std::vector<State> LevelStates; |
318 | | |
319 | | enum class Assignment : int8_t { |
320 | | Unassigned = -1, |
321 | | AssignedFalse = 0, |
322 | | AssignedTrue = 1 |
323 | | }; |
324 | | |
325 | | /// Maps variables (indices of the vector) to their assignments (elements of |
326 | | /// the vector). |
327 | | /// |
328 | | /// The element at index 0 isn't used. Variable assignments start from the |
329 | | /// element at index 1. |
330 | | std::vector<Assignment> VarAssignments; |
331 | | |
332 | | /// A set of unassigned variables that appear in watched literals in |
333 | | /// `Formula`. The vector is guaranteed to contain unique elements. |
334 | | std::vector<Variable> ActiveVars; |
335 | | |
336 | | public: |
337 | | explicit WatchedLiteralsSolverImpl(const llvm::DenseSet<BoolValue *> &Vals) |
338 | | : Formula(buildBooleanFormula(Vals)), LevelVars(Formula.LargestVar + 1), |
339 | 447 | LevelStates(Formula.LargestVar + 1) { |
340 | 447 | assert(!Vals.empty()); |
341 | | |
342 | | // Initialize the state at the root level to a decision so that in |
343 | | // `reverseForcedMoves` we don't have to check that `Level >= 0` on each |
344 | | // iteration. |
345 | 0 | LevelStates[0] = State::Decision; |
346 | | |
347 | | // Initialize all variables as unassigned. |
348 | 447 | VarAssignments.resize(Formula.LargestVar + 1, Assignment::Unassigned); |
349 | | |
350 | | // Initialize the active variables. |
351 | 11.2k | for (Variable Var = Formula.LargestVar; Var != NullVar; --Var10.8k ) { |
352 | 10.8k | if (isWatched(posLit(Var)) || isWatched(negLit(Var))2.06k ) |
353 | 8.74k | ActiveVars.push_back(Var); |
354 | 10.8k | } |
355 | 447 | } |
356 | | |
357 | 447 | Solver::Result solve() && { |
358 | 447 | size_t I = 0; |
359 | 17.2k | while (I < ActiveVars.size()) { |
360 | | // Assert that the following invariants hold: |
361 | | // 1. All active variables are unassigned. |
362 | | // 2. All active variables form watched literals. |
363 | | // 3. Unassigned variables that form watched literals are active. |
364 | | // FIXME: Consider replacing these with test cases that fail if the any |
365 | | // of the invariants is broken. That might not be easy due to the |
366 | | // transformations performed by `buildBooleanFormula`. |
367 | 17.0k | assert(activeVarsAreUnassigned()); |
368 | 0 | assert(activeVarsFormWatchedLiterals()); |
369 | 0 | assert(unassignedVarsFormingWatchedLiteralsAreActive()); |
370 | | |
371 | 0 | const Variable ActiveVar = ActiveVars[I]; |
372 | | |
373 | | // Look for unit clauses that contain the active variable. |
374 | 17.0k | const bool unitPosLit = watchedByUnitClause(posLit(ActiveVar)); |
375 | 17.0k | const bool unitNegLit = watchedByUnitClause(negLit(ActiveVar)); |
376 | 17.0k | if (unitPosLit && unitNegLit6.81k ) { |
377 | | // We found a conflict! |
378 | | |
379 | | // Backtrack and rewind the `Level` until the most recent non-forced |
380 | | // assignment. |
381 | 320 | reverseForcedMoves(); |
382 | | |
383 | | // If the root level is reached, then all possible assignments lead to |
384 | | // a conflict. |
385 | 320 | if (Level == 0) |
386 | 252 | return WatchedLiteralsSolver::Result::Unsatisfiable; |
387 | | |
388 | | // Otherwise, take the other branch at the most recent level where a |
389 | | // decision was made. |
390 | 68 | LevelStates[Level] = State::Forced; |
391 | 68 | const Variable Var = LevelVars[Level]; |
392 | 68 | VarAssignments[Var] = VarAssignments[Var] == Assignment::AssignedTrue |
393 | 68 | ? Assignment::AssignedFalse40 |
394 | 68 | : Assignment::AssignedTrue28 ; |
395 | | |
396 | 68 | updateWatchedLiterals(); |
397 | 16.7k | } else if (unitPosLit || unitNegLit10.2k ) { |
398 | | // We found a unit clause! The value of its unassigned variable is |
399 | | // forced. |
400 | 8.68k | ++Level; |
401 | | |
402 | 8.68k | LevelVars[Level] = ActiveVar; |
403 | 8.68k | LevelStates[Level] = State::Forced; |
404 | 8.68k | VarAssignments[ActiveVar] = |
405 | 8.68k | unitPosLit ? Assignment::AssignedTrue6.49k : Assignment::AssignedFalse2.18k ; |
406 | | |
407 | | // Remove the variable that was just assigned from the set of active |
408 | | // variables. |
409 | 8.68k | if (I + 1 < ActiveVars.size()) { |
410 | | // Replace the variable that was just assigned with the last active |
411 | | // variable for efficient removal. |
412 | 7.91k | ActiveVars[I] = ActiveVars.back(); |
413 | 7.91k | } else { |
414 | | // This was the last active variable. Repeat the process from the |
415 | | // beginning. |
416 | 770 | I = 0; |
417 | 770 | } |
418 | 8.68k | ActiveVars.pop_back(); |
419 | | |
420 | 8.68k | updateWatchedLiterals(); |
421 | 8.68k | } else if (8.03k I + 1 == ActiveVars.size()8.03k ) { |
422 | | // There are no remaining unit clauses in the formula! Make a decision |
423 | | // for one of the active variables at the current level. |
424 | 179 | ++Level; |
425 | | |
426 | 179 | LevelVars[Level] = ActiveVar; |
427 | 179 | LevelStates[Level] = State::Decision; |
428 | 179 | VarAssignments[ActiveVar] = decideAssignment(ActiveVar); |
429 | | |
430 | | // Remove the variable that was just assigned from the set of active |
431 | | // variables. |
432 | 179 | ActiveVars.pop_back(); |
433 | | |
434 | 179 | updateWatchedLiterals(); |
435 | | |
436 | | // This was the last active variable. Repeat the process from the |
437 | | // beginning. |
438 | 179 | I = 0; |
439 | 7.85k | } else { |
440 | 7.85k | ++I; |
441 | 7.85k | } |
442 | 17.0k | } |
443 | 195 | return WatchedLiteralsSolver::Result::Satisfiable; |
444 | 447 | } |
445 | | |
446 | | private: |
447 | | // Reverses forced moves until the most recent level where a decision was made |
448 | | // on the assignment of a variable. |
449 | 320 | void reverseForcedMoves() { |
450 | 4.39k | for (; LevelStates[Level] == State::Forced; --Level4.07k ) { |
451 | 4.07k | const Variable Var = LevelVars[Level]; |
452 | | |
453 | 4.07k | VarAssignments[Var] = Assignment::Unassigned; |
454 | | |
455 | | // If the variable that we pass through is watched then we add it to the |
456 | | // active variables. |
457 | 4.07k | if (isWatched(posLit(Var)) || isWatched(negLit(Var))872 ) |
458 | 4.05k | ActiveVars.push_back(Var); |
459 | 4.07k | } |
460 | 320 | } |
461 | | |
462 | | // Updates watched literals that are affected by a variable assignment. |
463 | 8.92k | void updateWatchedLiterals() { |
464 | 8.92k | const Variable Var = LevelVars[Level]; |
465 | | |
466 | | // Update the watched literals of clauses that currently watch the literal |
467 | | // that falsifies `Var`. |
468 | 8.92k | const Literal FalseLit = VarAssignments[Var] == Assignment::AssignedTrue |
469 | 8.92k | ? negLit(Var)6.59k |
470 | 8.92k | : posLit(Var)2.33k ; |
471 | 8.92k | ClauseID FalseLitWatcher = Formula.WatchedHead[FalseLit]; |
472 | 8.92k | Formula.WatchedHead[FalseLit] = NullClause; |
473 | 15.4k | while (FalseLitWatcher != NullClause) { |
474 | 6.53k | const ClauseID NextFalseLitWatcher = Formula.NextWatched[FalseLitWatcher]; |
475 | | |
476 | | // Pick the first non-false literal as the new watched literal. |
477 | 6.53k | const size_t FalseLitWatcherStart = Formula.ClauseStarts[FalseLitWatcher]; |
478 | 6.53k | size_t NewWatchedLitIdx = FalseLitWatcherStart + 1; |
479 | 6.87k | while (isCurrentlyFalse(Formula.Clauses[NewWatchedLitIdx])) |
480 | 346 | ++NewWatchedLitIdx; |
481 | 6.53k | const Literal NewWatchedLit = Formula.Clauses[NewWatchedLitIdx]; |
482 | 6.53k | const Variable NewWatchedLitVar = var(NewWatchedLit); |
483 | | |
484 | | // Swap the old watched literal for the new one in `FalseLitWatcher` to |
485 | | // maintain the invariant that the watched literal is at the beginning of |
486 | | // the clause. |
487 | 6.53k | Formula.Clauses[NewWatchedLitIdx] = FalseLit; |
488 | 6.53k | Formula.Clauses[FalseLitWatcherStart] = NewWatchedLit; |
489 | | |
490 | | // If the new watched literal isn't watched by any other clause and its |
491 | | // variable isn't assigned we need to add it to the active variables. |
492 | 6.53k | if (!isWatched(NewWatchedLit) && !isWatched(notLit(NewWatchedLit))2.30k && |
493 | 6.53k | VarAssignments[NewWatchedLitVar] == Assignment::Unassigned1.96k ) |
494 | 1.92k | ActiveVars.push_back(NewWatchedLitVar); |
495 | | |
496 | 6.53k | Formula.NextWatched[FalseLitWatcher] = Formula.WatchedHead[NewWatchedLit]; |
497 | 6.53k | Formula.WatchedHead[NewWatchedLit] = FalseLitWatcher; |
498 | | |
499 | | // Go to the next clause that watches `FalseLit`. |
500 | 6.53k | FalseLitWatcher = NextFalseLitWatcher; |
501 | 6.53k | } |
502 | 8.92k | } |
503 | | |
504 | | /// Returns true if and only if one of the clauses that watch `Lit` is a unit |
505 | | /// clause. |
506 | 34.0k | bool watchedByUnitClause(Literal Lit) const { |
507 | 34.0k | for (ClauseID LitWatcher = Formula.WatchedHead[Lit]; |
508 | 64.7k | LitWatcher != NullClause; |
509 | 40.0k | LitWatcher = Formula.NextWatched[LitWatcher]30.6k ) { |
510 | 40.0k | llvm::ArrayRef<Literal> Clause = Formula.clauseLiterals(LitWatcher); |
511 | | |
512 | | // Assert the invariant that the watched literal is always the first one |
513 | | // in the clause. |
514 | | // FIXME: Consider replacing this with a test case that fails if the |
515 | | // invariant is broken by `updateWatchedLiterals`. That might not be easy |
516 | | // due to the transformations performed by `buildBooleanFormula`. |
517 | 40.0k | assert(Clause.front() == Lit); |
518 | | |
519 | 40.0k | if (isUnit(Clause)) |
520 | 9.32k | return true; |
521 | 40.0k | } |
522 | 24.7k | return false; |
523 | 34.0k | } |
524 | | |
525 | | /// Returns true if and only if `Clause` is a unit clause. |
526 | 40.0k | bool isUnit(llvm::ArrayRef<Literal> Clause) const { |
527 | 40.0k | return llvm::all_of(Clause.drop_front(), |
528 | 41.5k | [this](Literal L) { return isCurrentlyFalse(L); }); |
529 | 40.0k | } |
530 | | |
531 | | /// Returns true if and only if `Lit` evaluates to `false` in the current |
532 | | /// partial assignment. |
533 | 48.4k | bool isCurrentlyFalse(Literal Lit) const { |
534 | 48.4k | return static_cast<int8_t>(VarAssignments[var(Lit)]) == |
535 | 48.4k | static_cast<int8_t>(Lit & 1); |
536 | 48.4k | } |
537 | | |
538 | | /// Returns true if and only if `Lit` is watched by a clause in `Formula`. |
539 | 27.0k | bool isWatched(Literal Lit) const { |
540 | 27.0k | return Formula.WatchedHead[Lit] != NullClause; |
541 | 27.0k | } |
542 | | |
543 | | /// Returns an assignment for an unassigned variable. |
544 | 179 | Assignment decideAssignment(Variable Var) const { |
545 | 179 | return !isWatched(posLit(Var)) || isWatched(negLit(Var))178 |
546 | 179 | ? Assignment::AssignedFalse112 |
547 | 179 | : Assignment::AssignedTrue67 ; |
548 | 179 | } |
549 | | |
550 | | /// Returns a set of all watched literals. |
551 | 34.0k | llvm::DenseSet<Literal> watchedLiterals() const { |
552 | 34.0k | llvm::DenseSet<Literal> WatchedLiterals; |
553 | 2.71M | for (Literal Lit = 2; Lit < Formula.WatchedHead.size(); Lit++2.68M ) { |
554 | 2.68M | if (Formula.WatchedHead[Lit] == NullClause) |
555 | 910k | continue; |
556 | 1.77M | WatchedLiterals.insert(Lit); |
557 | 1.77M | } |
558 | 34.0k | return WatchedLiterals; |
559 | 34.0k | } |
560 | | |
561 | | /// Returns true if and only if all active variables are unassigned. |
562 | 17.0k | bool activeVarsAreUnassigned() const { |
563 | 336k | return llvm::all_of(ActiveVars, [this](Variable Var) { |
564 | 336k | return VarAssignments[Var] == Assignment::Unassigned; |
565 | 336k | }); |
566 | 17.0k | } |
567 | | |
568 | | /// Returns true if and only if all active variables form watched literals. |
569 | 17.0k | bool activeVarsFormWatchedLiterals() const { |
570 | 17.0k | const llvm::DenseSet<Literal> WatchedLiterals = watchedLiterals(); |
571 | 336k | return llvm::all_of(ActiveVars, [&WatchedLiterals](Variable Var) { |
572 | 336k | return WatchedLiterals.contains(posLit(Var)) || |
573 | 336k | WatchedLiterals.contains(negLit(Var))5.84k ; |
574 | 336k | }); |
575 | 17.0k | } |
576 | | |
577 | | /// Returns true if and only if all unassigned variables that are forming |
578 | | /// watched literals are active. |
579 | 17.0k | bool unassignedVarsFormingWatchedLiteralsAreActive() const { |
580 | 17.0k | const llvm::DenseSet<Variable> ActiveVarsSet(ActiveVars.begin(), |
581 | 17.0k | ActiveVars.end()); |
582 | 887k | for (Literal Lit : watchedLiterals()) { |
583 | 887k | const Variable Var = var(Lit); |
584 | 887k | if (VarAssignments[Var] != Assignment::Unassigned) |
585 | 289k | continue; |
586 | 598k | if (ActiveVarsSet.contains(Var)) |
587 | 598k | continue; |
588 | 0 | return false; |
589 | 598k | } |
590 | 17.0k | return true; |
591 | 17.0k | } |
592 | | }; |
593 | | |
594 | 447 | Solver::Result WatchedLiteralsSolver::solve(llvm::DenseSet<BoolValue *> Vals) { |
595 | 447 | return Vals.empty() ? WatchedLiteralsSolver::Result::Satisfiable0 |
596 | 447 | : WatchedLiteralsSolverImpl(Vals).solve(); |
597 | 447 | } |
598 | | |
599 | | } // namespace dataflow |
600 | | } // namespace clang |