clang 17.0.0git
WatchedLiteralsSolver.cpp
Go to the documentation of this file.
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
23#include "llvm/ADT/DenseMap.h"
24#include "llvm/ADT/DenseSet.h"
25#include "llvm/ADT/STLExtras.h"
26
27namespace clang {
28namespace 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.
45using Variable = uint32_t;
46
47/// A null boolean variable is used as a placeholder in various data structures
48/// and algorithms.
49static 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`.
55using Literal = uint32_t;
56
57/// A null literal is used as a placeholder in various data structures and
58/// algorithms.
59static constexpr Literal NullLit = 0;
60
61/// Returns the positive literal `V`.
62static constexpr Literal posLit(Variable V) { return 2 * V; }
63
64/// Returns the negative literal `!V`.
65static constexpr Literal negLit(Variable V) { return 2 * V + 1; }
66
67/// Returns the negated literal `!L`.
68static constexpr Literal notLit(Literal L) { return L ^ 1; }
69
70/// Returns the variable of `L`.
71static constexpr Variable var(Literal L) { return L >> 1; }
72
73/// Clause identifiers are represented as positive integers.
74using ClauseID = uint32_t;
75
76/// A null clause identifier is used as a placeholder in various data structures
77/// and algorithms.
78static constexpr ClauseID NullClause = 0;
79
80/// A boolean formula in conjunctive normal form.
82 /// `LargestVar` is equal to the largest positive integer that represents a
83 /// variable in the formula.
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
128 llvm::DenseMap<Variable, AtomicBoolValue *> Atomics)
130 Clauses.push_back(0);
131 ClauseStarts.push_back(0);
132 NextWatched.push_back(0);
133 const size_t NumLiterals = 2 * LargestVar + 1;
134 WatchedHead.resize(NumLiterals + 1, 0);
135 }
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.
146 // The literals are guaranteed to be distinct from properties of BoolValue
147 // and the construction in `buildBooleanFormula`.
148 assert(L1 != NullLit && L1 != L2 && L1 != L3 &&
149 (L2 != L3 || L2 == NullLit));
150
151 const ClauseID C = ClauseStarts.size();
152 const size_t S = Clauses.size();
153 ClauseStarts.push_back(S);
154
155 Clauses.push_back(L1);
156 if (L2 != NullLit)
157 Clauses.push_back(L2);
158 if (L3 != NullLit)
159 Clauses.push_back(L3);
160
161 // Designate the first literal as the "watched" literal of the clause.
162 NextWatched.push_back(WatchedHead[L1]);
163 WatchedHead[L1] = C;
164 }
165
166 /// Returns the number of literals in clause `C`.
167 size_t clauseSize(ClauseID C) const {
168 return C == ClauseStarts.size() - 1 ? Clauses.size() - ClauseStarts[C]
169 : ClauseStarts[C + 1] - ClauseStarts[C];
170 }
171
172 /// Returns the literals of clause `C`.
175 }
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.
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 llvm::DenseMap<BoolValue *, Variable> SubValsToVar;
189 // Store variable identifiers and value location of atomic booleans.
190 llvm::DenseMap<Variable, AtomicBoolValue *> Atomics;
191 Variable NextVar = 1;
192 {
193 std::queue<BoolValue *> UnprocessedSubVals;
194 for (BoolValue *Val : Vals)
195 UnprocessedSubVals.push(Val);
196 while (!UnprocessedSubVals.empty()) {
197 Variable Var = NextVar;
198 BoolValue *Val = UnprocessedSubVals.front();
199 UnprocessedSubVals.pop();
200
201 if (!SubValsToVar.try_emplace(Val, Var).second)
202 continue;
203 ++NextVar;
204
205 // Visit the sub-values of `Val`.
206 switch (Val->getKind()) {
208 auto *C = cast<ConjunctionValue>(Val);
209 UnprocessedSubVals.push(&C->getLeftSubValue());
210 UnprocessedSubVals.push(&C->getRightSubValue());
211 break;
212 }
214 auto *D = cast<DisjunctionValue>(Val);
215 UnprocessedSubVals.push(&D->getLeftSubValue());
216 UnprocessedSubVals.push(&D->getRightSubValue());
217 break;
218 }
220 auto *N = cast<NegationValue>(Val);
221 UnprocessedSubVals.push(&N->getSubVal());
222 break;
223 }
225 auto *I = cast<ImplicationValue>(Val);
226 UnprocessedSubVals.push(&I->getLeftSubValue());
227 UnprocessedSubVals.push(&I->getRightSubValue());
228 break;
229 }
231 auto *B = cast<BiconditionalValue>(Val);
232 UnprocessedSubVals.push(&B->getLeftSubValue());
233 UnprocessedSubVals.push(&B->getRightSubValue());
234 break;
235 }
237 // Nothing more to do. This `TopBool` instance has already been mapped
238 // to a fresh solver variable (`NextVar`, above) and is thereafter
239 // anonymous. The solver never sees `Top`.
240 break;
242 Atomics[Var] = cast<AtomicBoolValue>(Val);
243 break;
244 }
245 default:
246 llvm_unreachable("buildBooleanFormula: unhandled value kind");
247 }
248 }
249 }
250
251 auto GetVar = [&SubValsToVar](const BoolValue *Val) {
252 auto ValIt = SubValsToVar.find(Val);
253 assert(ValIt != SubValsToVar.end());
254 return ValIt->second;
255 };
256
257 BooleanFormula Formula(NextVar - 1, std::move(Atomics));
258 std::vector<bool> ProcessedSubVals(NextVar, false);
259
260 // Add a conjunct for each variable that represents a top-level conjunction
261 // value in `Vals`.
262 for (BoolValue *Val : Vals)
263 Formula.addClause(posLit(GetVar(Val)));
264
265 // Add conjuncts that represent the mapping between newly-created variables
266 // and their corresponding sub-values.
267 std::queue<BoolValue *> UnprocessedSubVals;
268 for (BoolValue *Val : Vals)
269 UnprocessedSubVals.push(Val);
270 while (!UnprocessedSubVals.empty()) {
271 const BoolValue *Val = UnprocessedSubVals.front();
272 UnprocessedSubVals.pop();
273 const Variable Var = GetVar(Val);
274
275 if (ProcessedSubVals[Var])
276 continue;
277 ProcessedSubVals[Var] = true;
278
279 if (auto *C = dyn_cast<ConjunctionValue>(Val)) {
280 const Variable LeftSubVar = GetVar(&C->getLeftSubValue());
281 const Variable RightSubVar = GetVar(&C->getRightSubValue());
282
283 if (LeftSubVar == RightSubVar) {
284 // `X <=> (A ^ A)` is equivalent to `(!X v A) ^ (X v !A)` which is
285 // already in conjunctive normal form. Below we add each of the
286 // conjuncts of the latter expression to the result.
287 Formula.addClause(negLit(Var), posLit(LeftSubVar));
288 Formula.addClause(posLit(Var), negLit(LeftSubVar));
289
290 // Visit a sub-value of `Val` (pick any, they are identical).
291 UnprocessedSubVals.push(&C->getLeftSubValue());
292 } else {
293 // `X <=> (A ^ B)` is equivalent to `(!X v A) ^ (!X v B) ^ (X v !A v !B)`
294 // which is already in conjunctive normal form. Below we add each of the
295 // conjuncts of the latter expression to the result.
296 Formula.addClause(negLit(Var), posLit(LeftSubVar));
297 Formula.addClause(negLit(Var), posLit(RightSubVar));
298 Formula.addClause(posLit(Var), negLit(LeftSubVar), negLit(RightSubVar));
299
300 // Visit the sub-values of `Val`.
301 UnprocessedSubVals.push(&C->getLeftSubValue());
302 UnprocessedSubVals.push(&C->getRightSubValue());
303 }
304 } else if (auto *D = dyn_cast<DisjunctionValue>(Val)) {
305 const Variable LeftSubVar = GetVar(&D->getLeftSubValue());
306 const Variable RightSubVar = GetVar(&D->getRightSubValue());
307
308 if (LeftSubVar == RightSubVar) {
309 // `X <=> (A v A)` is equivalent to `(!X v A) ^ (X v !A)` which is
310 // already in conjunctive normal form. Below we add each of the
311 // conjuncts of the latter expression to the result.
312 Formula.addClause(negLit(Var), posLit(LeftSubVar));
313 Formula.addClause(posLit(Var), negLit(LeftSubVar));
314
315 // Visit a sub-value of `Val` (pick any, they are identical).
316 UnprocessedSubVals.push(&D->getLeftSubValue());
317 } else {
318 // `X <=> (A v B)` is equivalent to `(!X v A v B) ^ (X v !A) ^ (X v !B)`
319 // which is already in conjunctive normal form. Below we add each of the
320 // conjuncts of the latter expression to the result.
321 Formula.addClause(negLit(Var), posLit(LeftSubVar), posLit(RightSubVar));
322 Formula.addClause(posLit(Var), negLit(LeftSubVar));
323 Formula.addClause(posLit(Var), negLit(RightSubVar));
324
325 // Visit the sub-values of `Val`.
326 UnprocessedSubVals.push(&D->getLeftSubValue());
327 UnprocessedSubVals.push(&D->getRightSubValue());
328 }
329 } else if (auto *N = dyn_cast<NegationValue>(Val)) {
330 const Variable SubVar = GetVar(&N->getSubVal());
331
332 // `X <=> !Y` is equivalent to `(!X v !Y) ^ (X v Y)` which is already in
333 // conjunctive normal form. Below we add each of the conjuncts of the
334 // latter expression to the result.
335 Formula.addClause(negLit(Var), negLit(SubVar));
336 Formula.addClause(posLit(Var), posLit(SubVar));
337
338 // Visit the sub-values of `Val`.
339 UnprocessedSubVals.push(&N->getSubVal());
340 } else if (auto *I = dyn_cast<ImplicationValue>(Val)) {
341 const Variable LeftSubVar = GetVar(&I->getLeftSubValue());
342 const Variable RightSubVar = GetVar(&I->getRightSubValue());
343
344 // `X <=> (A => B)` is equivalent to
345 // `(X v A) ^ (X v !B) ^ (!X v !A v B)` which is already in
346 // conjunctive normal form. Below we add each of the conjuncts of the
347 // latter expression to the result.
348 Formula.addClause(posLit(Var), posLit(LeftSubVar));
349 Formula.addClause(posLit(Var), negLit(RightSubVar));
350 Formula.addClause(negLit(Var), negLit(LeftSubVar), posLit(RightSubVar));
351
352 // Visit the sub-values of `Val`.
353 UnprocessedSubVals.push(&I->getLeftSubValue());
354 UnprocessedSubVals.push(&I->getRightSubValue());
355 } else if (auto *B = dyn_cast<BiconditionalValue>(Val)) {
356 const Variable LeftSubVar = GetVar(&B->getLeftSubValue());
357 const Variable RightSubVar = GetVar(&B->getRightSubValue());
358
359 if (LeftSubVar == RightSubVar) {
360 // `X <=> (A <=> A)` is equvalent to `X` which is already in
361 // conjunctive normal form. Below we add each of the conjuncts of the
362 // latter expression to the result.
363 Formula.addClause(posLit(Var));
364
365 // No need to visit the sub-values of `Val`.
366 } else {
367 // `X <=> (A <=> B)` is equivalent to
368 // `(X v A v B) ^ (X v !A v !B) ^ (!X v A v !B) ^ (!X v !A v B)` which is
369 // already in conjunctive normal form. Below we add each of the conjuncts
370 // of the latter expression to the result.
371 Formula.addClause(posLit(Var), posLit(LeftSubVar), posLit(RightSubVar));
372 Formula.addClause(posLit(Var), negLit(LeftSubVar), negLit(RightSubVar));
373 Formula.addClause(negLit(Var), posLit(LeftSubVar), negLit(RightSubVar));
374 Formula.addClause(negLit(Var), negLit(LeftSubVar), posLit(RightSubVar));
375
376 // Visit the sub-values of `Val`.
377 UnprocessedSubVals.push(&B->getLeftSubValue());
378 UnprocessedSubVals.push(&B->getRightSubValue());
379 }
380 }
381 }
382
383 return Formula;
384}
385
387 /// A boolean formula in conjunctive normal form that the solver will attempt
388 /// to prove satisfiable. The formula will be modified in the process.
389 BooleanFormula Formula;
390
391 /// The search for a satisfying assignment of the variables in `Formula` will
392 /// proceed in levels, starting from 1 and going up to `Formula.LargestVar`
393 /// (inclusive). The current level is stored in `Level`. At each level the
394 /// solver will assign a value to an unassigned variable. If this leads to a
395 /// consistent partial assignment, `Level` will be incremented. Otherwise, if
396 /// it results in a conflict, the solver will backtrack by decrementing
397 /// `Level` until it reaches the most recent level where a decision was made.
398 size_t Level = 0;
399
400 /// Maps levels (indices of the vector) to variables (elements of the vector)
401 /// that are assigned values at the respective levels.
402 ///
403 /// The element at index 0 isn't used. Variables start from the element at
404 /// index 1.
405 std::vector<Variable> LevelVars;
406
407 /// State of the solver at a particular level.
408 enum class State : uint8_t {
409 /// Indicates that the solver made a decision.
410 Decision = 0,
411
412 /// Indicates that the solver made a forced move.
413 Forced = 1,
414 };
415
416 /// State of the solver at a particular level. It keeps track of previous
417 /// decisions that the solver can refer to when backtracking.
418 ///
419 /// The element at index 0 isn't used. States start from the element at index
420 /// 1.
421 std::vector<State> LevelStates;
422
423 enum class Assignment : int8_t {
424 Unassigned = -1,
425 AssignedFalse = 0,
426 AssignedTrue = 1
427 };
428
429 /// Maps variables (indices of the vector) to their assignments (elements of
430 /// the vector).
431 ///
432 /// The element at index 0 isn't used. Variable assignments start from the
433 /// element at index 1.
434 std::vector<Assignment> VarAssignments;
435
436 /// A set of unassigned variables that appear in watched literals in
437 /// `Formula`. The vector is guaranteed to contain unique elements.
438 std::vector<Variable> ActiveVars;
439
440public:
442 : Formula(buildBooleanFormula(Vals)), LevelVars(Formula.LargestVar + 1),
443 LevelStates(Formula.LargestVar + 1) {
444 assert(!Vals.empty());
445
446 // Initialize the state at the root level to a decision so that in
447 // `reverseForcedMoves` we don't have to check that `Level >= 0` on each
448 // iteration.
449 LevelStates[0] = State::Decision;
450
451 // Initialize all variables as unassigned.
452 VarAssignments.resize(Formula.LargestVar + 1, Assignment::Unassigned);
453
454 // Initialize the active variables.
455 for (Variable Var = Formula.LargestVar; Var != NullVar; --Var) {
456 if (isWatched(posLit(Var)) || isWatched(negLit(Var)))
457 ActiveVars.push_back(Var);
458 }
459 }
460
462 size_t I = 0;
463 while (I < ActiveVars.size()) {
464 // Assert that the following invariants hold:
465 // 1. All active variables are unassigned.
466 // 2. All active variables form watched literals.
467 // 3. Unassigned variables that form watched literals are active.
468 // FIXME: Consider replacing these with test cases that fail if the any
469 // of the invariants is broken. That might not be easy due to the
470 // transformations performed by `buildBooleanFormula`.
471 assert(activeVarsAreUnassigned());
472 assert(activeVarsFormWatchedLiterals());
473 assert(unassignedVarsFormingWatchedLiteralsAreActive());
474
475 const Variable ActiveVar = ActiveVars[I];
476
477 // Look for unit clauses that contain the active variable.
478 const bool unitPosLit = watchedByUnitClause(posLit(ActiveVar));
479 const bool unitNegLit = watchedByUnitClause(negLit(ActiveVar));
480 if (unitPosLit && unitNegLit) {
481 // We found a conflict!
482
483 // Backtrack and rewind the `Level` until the most recent non-forced
484 // assignment.
485 reverseForcedMoves();
486
487 // If the root level is reached, then all possible assignments lead to
488 // a conflict.
489 if (Level == 0)
491
492 // Otherwise, take the other branch at the most recent level where a
493 // decision was made.
494 LevelStates[Level] = State::Forced;
495 const Variable Var = LevelVars[Level];
496 VarAssignments[Var] = VarAssignments[Var] == Assignment::AssignedTrue
497 ? Assignment::AssignedFalse
498 : Assignment::AssignedTrue;
499
500 updateWatchedLiterals();
501 } else if (unitPosLit || unitNegLit) {
502 // We found a unit clause! The value of its unassigned variable is
503 // forced.
504 ++Level;
505
506 LevelVars[Level] = ActiveVar;
507 LevelStates[Level] = State::Forced;
508 VarAssignments[ActiveVar] =
509 unitPosLit ? Assignment::AssignedTrue : Assignment::AssignedFalse;
510
511 // Remove the variable that was just assigned from the set of active
512 // variables.
513 if (I + 1 < ActiveVars.size()) {
514 // Replace the variable that was just assigned with the last active
515 // variable for efficient removal.
516 ActiveVars[I] = ActiveVars.back();
517 } else {
518 // This was the last active variable. Repeat the process from the
519 // beginning.
520 I = 0;
521 }
522 ActiveVars.pop_back();
523
524 updateWatchedLiterals();
525 } else if (I + 1 == ActiveVars.size()) {
526 // There are no remaining unit clauses in the formula! Make a decision
527 // for one of the active variables at the current level.
528 ++Level;
529
530 LevelVars[Level] = ActiveVar;
531 LevelStates[Level] = State::Decision;
532 VarAssignments[ActiveVar] = decideAssignment(ActiveVar);
533
534 // Remove the variable that was just assigned from the set of active
535 // variables.
536 ActiveVars.pop_back();
537
538 updateWatchedLiterals();
539
540 // This was the last active variable. Repeat the process from the
541 // beginning.
542 I = 0;
543 } else {
544 ++I;
545 }
546 }
547 return Solver::Result::Satisfiable(buildSolution());
548 }
549
550private:
551 /// Returns a satisfying truth assignment to the atomic values in the boolean
552 /// formula.
553 llvm::DenseMap<AtomicBoolValue *, Solver::Result::Assignment>
554 buildSolution() {
555 llvm::DenseMap<AtomicBoolValue *, Solver::Result::Assignment> Solution;
556 for (auto &Atomic : Formula.Atomics) {
557 // A variable may have a definite true/false assignment, or it may be
558 // unassigned indicating its truth value does not affect the result of
559 // the formula. Unassigned variables are assigned to true as a default.
560 Solution[Atomic.second] =
561 VarAssignments[Atomic.first] == Assignment::AssignedFalse
564 }
565 return Solution;
566 }
567
568 /// Reverses forced moves until the most recent level where a decision was
569 /// made on the assignment of a variable.
570 void reverseForcedMoves() {
571 for (; LevelStates[Level] == State::Forced; --Level) {
572 const Variable Var = LevelVars[Level];
573
574 VarAssignments[Var] = Assignment::Unassigned;
575
576 // If the variable that we pass through is watched then we add it to the
577 // active variables.
578 if (isWatched(posLit(Var)) || isWatched(negLit(Var)))
579 ActiveVars.push_back(Var);
580 }
581 }
582
583 /// Updates watched literals that are affected by a variable assignment.
584 void updateWatchedLiterals() {
585 const Variable Var = LevelVars[Level];
586
587 // Update the watched literals of clauses that currently watch the literal
588 // that falsifies `Var`.
589 const Literal FalseLit = VarAssignments[Var] == Assignment::AssignedTrue
590 ? negLit(Var)
591 : posLit(Var);
592 ClauseID FalseLitWatcher = Formula.WatchedHead[FalseLit];
593 Formula.WatchedHead[FalseLit] = NullClause;
594 while (FalseLitWatcher != NullClause) {
595 const ClauseID NextFalseLitWatcher = Formula.NextWatched[FalseLitWatcher];
596
597 // Pick the first non-false literal as the new watched literal.
598 const size_t FalseLitWatcherStart = Formula.ClauseStarts[FalseLitWatcher];
599 size_t NewWatchedLitIdx = FalseLitWatcherStart + 1;
600 while (isCurrentlyFalse(Formula.Clauses[NewWatchedLitIdx]))
601 ++NewWatchedLitIdx;
602 const Literal NewWatchedLit = Formula.Clauses[NewWatchedLitIdx];
603 const Variable NewWatchedLitVar = var(NewWatchedLit);
604
605 // Swap the old watched literal for the new one in `FalseLitWatcher` to
606 // maintain the invariant that the watched literal is at the beginning of
607 // the clause.
608 Formula.Clauses[NewWatchedLitIdx] = FalseLit;
609 Formula.Clauses[FalseLitWatcherStart] = NewWatchedLit;
610
611 // If the new watched literal isn't watched by any other clause and its
612 // variable isn't assigned we need to add it to the active variables.
613 if (!isWatched(NewWatchedLit) && !isWatched(notLit(NewWatchedLit)) &&
614 VarAssignments[NewWatchedLitVar] == Assignment::Unassigned)
615 ActiveVars.push_back(NewWatchedLitVar);
616
617 Formula.NextWatched[FalseLitWatcher] = Formula.WatchedHead[NewWatchedLit];
618 Formula.WatchedHead[NewWatchedLit] = FalseLitWatcher;
619
620 // Go to the next clause that watches `FalseLit`.
621 FalseLitWatcher = NextFalseLitWatcher;
622 }
623 }
624
625 /// Returns true if and only if one of the clauses that watch `Lit` is a unit
626 /// clause.
627 bool watchedByUnitClause(Literal Lit) const {
628 for (ClauseID LitWatcher = Formula.WatchedHead[Lit];
629 LitWatcher != NullClause;
630 LitWatcher = Formula.NextWatched[LitWatcher]) {
631 llvm::ArrayRef<Literal> Clause = Formula.clauseLiterals(LitWatcher);
632
633 // Assert the invariant that the watched literal is always the first one
634 // in the clause.
635 // FIXME: Consider replacing this with a test case that fails if the
636 // invariant is broken by `updateWatchedLiterals`. That might not be easy
637 // due to the transformations performed by `buildBooleanFormula`.
638 assert(Clause.front() == Lit);
639
640 if (isUnit(Clause))
641 return true;
642 }
643 return false;
644 }
645
646 /// Returns true if and only if `Clause` is a unit clause.
647 bool isUnit(llvm::ArrayRef<Literal> Clause) const {
648 return llvm::all_of(Clause.drop_front(),
649 [this](Literal L) { return isCurrentlyFalse(L); });
650 }
651
652 /// Returns true if and only if `Lit` evaluates to `false` in the current
653 /// partial assignment.
654 bool isCurrentlyFalse(Literal Lit) const {
655 return static_cast<int8_t>(VarAssignments[var(Lit)]) ==
656 static_cast<int8_t>(Lit & 1);
657 }
658
659 /// Returns true if and only if `Lit` is watched by a clause in `Formula`.
660 bool isWatched(Literal Lit) const {
661 return Formula.WatchedHead[Lit] != NullClause;
662 }
663
664 /// Returns an assignment for an unassigned variable.
665 Assignment decideAssignment(Variable Var) const {
666 return !isWatched(posLit(Var)) || isWatched(negLit(Var))
667 ? Assignment::AssignedFalse
668 : Assignment::AssignedTrue;
669 }
670
671 /// Returns a set of all watched literals.
672 llvm::DenseSet<Literal> watchedLiterals() const {
673 llvm::DenseSet<Literal> WatchedLiterals;
674 for (Literal Lit = 2; Lit < Formula.WatchedHead.size(); Lit++) {
675 if (Formula.WatchedHead[Lit] == NullClause)
676 continue;
677 WatchedLiterals.insert(Lit);
678 }
679 return WatchedLiterals;
680 }
681
682 /// Returns true if and only if all active variables are unassigned.
683 bool activeVarsAreUnassigned() const {
684 return llvm::all_of(ActiveVars, [this](Variable Var) {
685 return VarAssignments[Var] == Assignment::Unassigned;
686 });
687 }
688
689 /// Returns true if and only if all active variables form watched literals.
690 bool activeVarsFormWatchedLiterals() const {
691 const llvm::DenseSet<Literal> WatchedLiterals = watchedLiterals();
692 return llvm::all_of(ActiveVars, [&WatchedLiterals](Variable Var) {
693 return WatchedLiterals.contains(posLit(Var)) ||
694 WatchedLiterals.contains(negLit(Var));
695 });
696 }
697
698 /// Returns true if and only if all unassigned variables that are forming
699 /// watched literals are active.
700 bool unassignedVarsFormingWatchedLiteralsAreActive() const {
701 const llvm::DenseSet<Variable> ActiveVarsSet(ActiveVars.begin(),
702 ActiveVars.end());
703 for (Literal Lit : watchedLiterals()) {
704 const Variable Var = var(Lit);
705 if (VarAssignments[Var] != Assignment::Unassigned)
706 continue;
707 if (ActiveVarsSet.contains(Var))
708 continue;
709 return false;
710 }
711 return true;
712 }
713};
714
716 return Vals.empty() ? Solver::Result::Satisfiable({{}})
718}
719
720} // namespace dataflow
721} // namespace clang
#define V(N, I)
Definition: ASTContext.h:3217
Models a boolean.
Definition: Value.h:93
Kind getKind() const
Definition: Value.h:61
WatchedLiteralsSolverImpl(const llvm::DenseSet< BoolValue * > &Vals)
Result solve(llvm::DenseSet< BoolValue * > Vals) override
Checks if the conjunction of Vals is satisfiable and returns the corresponding result.
uint32_t ClauseID
Clause identifiers are represented as positive integers.
static constexpr Variable NullVar
A null boolean variable is used as a placeholder in various data structures and algorithms.
BooleanFormula buildBooleanFormula(const llvm::DenseSet< BoolValue * > &Vals)
Converts the conjunction of Vals into a formula in conjunctive normal form where each clause has at l...
static constexpr Literal negLit(Variable V)
Returns the negative literal !V.
static constexpr Literal notLit(Literal L)
Returns the negated literal !L.
static constexpr Literal NullLit
A null literal is used as a placeholder in various data structures and algorithms.
static constexpr Literal posLit(Variable V)
Returns the positive literal V.
static constexpr ClauseID NullClause
A null clause identifier is used as a placeholder in various data structures and algorithms.
uint32_t Literal
Literals are represented as positive integers.
static constexpr Variable var(Literal L)
Returns the variable of L.
uint32_t Variable
Boolean variables are represented as positive integers.
@ C
Languages that the frontend can parse and compile.
Definition: Format.h:4657
A boolean formula in conjunctive normal form.
std::vector< Literal > Clauses
Literals of all clauses in the formula.
std::vector< size_t > ClauseStarts
Start indices of clauses of the formula in Clauses.
llvm::ArrayRef< Literal > clauseLiterals(ClauseID C) const
Returns the literals of clause C.
std::vector< ClauseID > WatchedHead
Maps literals (indices of the vector) to clause identifiers (elements of the vector) that watch the r...
void addClause(Literal L1, Literal L2=NullLit, Literal L3=NullLit)
Adds the L1 v L2 v L3 clause to the formula.
const Variable LargestVar
LargestVar is equal to the largest positive integer that represents a variable in the formula.
size_t clauseSize(ClauseID C) const
Returns the number of literals in clause C.
BooleanFormula(Variable LargestVar, llvm::DenseMap< Variable, AtomicBoolValue * > Atomics)
llvm::DenseMap< Variable, AtomicBoolValue * > Atomics
Stores the variable identifier and value location for atomic booleans in the formula.
std::vector< ClauseID > NextWatched
Maps clause identifiers (elements of the vector) to identifiers of other clauses that watch the same ...
static Result Unsatisfiable()
Constructs a result indicating that the queried boolean formula is unsatisfiable.
Definition: Solver.h:55
@ Satisfiable
Indicates that there exists a satisfying assignment for a boolean formula.