clang  16.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 
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 static constexpr Literal posLit(Variable V) { return 2 * V; }
63 
64 /// Returns the negative literal `!V`.
65 static constexpr Literal negLit(Variable V) { return 2 * V + 1; }
66 
67 /// Returns the negated literal `!L`.
68 static constexpr Literal notLit(Literal L) { return L ^ 1; }
69 
70 /// Returns the variable of `L`.
71 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.
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)
129  : LargestVar(LargestVar), Atomics(std::move(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  }
219  case Value::Kind::Negation: {
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 
440 public:
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 
550 private:
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
clang::dataflow::NullClause
static constexpr ClauseID NullClause
A null clause identifier is used as a placeholder in various data structures and algorithms.
Definition: WatchedLiteralsSolver.cpp:78
clang::dataflow::BooleanFormula::WatchedHead
std::vector< ClauseID > WatchedHead
Maps literals (indices of the vector) to clause identifiers (elements of the vector) that watch the r...
Definition: WatchedLiteralsSolver.cpp:113
clang::dataflow::NullVar
static constexpr Variable NullVar
A null boolean variable is used as a placeholder in various data structures and algorithms.
Definition: WatchedLiteralsSolver.cpp:49
clang::dataflow::BooleanFormula::NextWatched
std::vector< ClauseID > NextWatched
Maps clause identifiers (elements of the vector) to identifiers of other clauses that watch the same ...
Definition: WatchedLiteralsSolver.cpp:121
clang::dataflow::Variable
uint32_t Variable
Boolean variables are represented as positive integers.
Definition: WatchedLiteralsSolver.cpp:45
clang::dataflow::ClauseID
uint32_t ClauseID
Clause identifiers are represented as positive integers.
Definition: WatchedLiteralsSolver.cpp:74
clang::dataflow::WatchedLiteralsSolverImpl::WatchedLiteralsSolverImpl
WatchedLiteralsSolverImpl(const llvm::DenseSet< BoolValue * > &Vals)
Definition: WatchedLiteralsSolver.cpp:441
clang::dataflow::Solver::Result::Unsatisfiable
static Result Unsatisfiable()
Constructs a result indicating that the queried boolean formula is unsatisfiable.
Definition: Solver.h:55
clang::dataflow::NullLit
static constexpr Literal NullLit
A null literal is used as a placeholder in various data structures and algorithms.
Definition: WatchedLiteralsSolver.cpp:59
clang::dataflow::Value::Kind::Disjunction
@ Disjunction
clang::dataflow::BooleanFormula::clauseSize
size_t clauseSize(ClauseID C) const
Returns the number of literals in clause C.
Definition: WatchedLiteralsSolver.cpp:167
clang::dataflow::Literal
uint32_t Literal
Literals are represented as positive integers.
Definition: WatchedLiteralsSolver.cpp:55
V
#define V(N, I)
Definition: ASTContext.h:3237
clang::dataflow::BooleanFormula::addClause
void addClause(Literal L1, Literal L2=NullLit, Literal L3=NullLit)
Adds the L1 v L2 v L3 clause to the formula.
Definition: WatchedLiteralsSolver.cpp:145
Solver.h
clang::dataflow::BooleanFormula::Atomics
llvm::DenseMap< Variable, AtomicBoolValue * > Atomics
Stores the variable identifier and value location for atomic booleans in the formula.
Definition: WatchedLiteralsSolver.cpp:125
clang::dataflow::Value::Kind::TopBool
@ TopBool
clang::dataflow::WatchedLiteralsSolver::solve
Result solve(llvm::DenseSet< BoolValue * > Vals) override
Checks if the conjunction of Vals is satisfiable and returns the corresponding result.
Definition: WatchedLiteralsSolver.cpp:715
clang::dataflow::var
static constexpr Variable var(Literal L)
Returns the variable of L.
Definition: WatchedLiteralsSolver.cpp:71
llvm::DenseSet
Definition: Sema.h:77
clang::dataflow::negLit
static constexpr Literal negLit(Variable V)
Returns the negative literal !V.
Definition: WatchedLiteralsSolver.cpp:65
clang::dataflow::BooleanFormula::BooleanFormula
BooleanFormula(Variable LargestVar, llvm::DenseMap< Variable, AtomicBoolValue * > Atomics)
Definition: WatchedLiteralsSolver.cpp:127
clang::dataflow::Value::Kind::Conjunction
@ Conjunction
clang::dataflow::Value::Kind::Negation
@ Negation
clang::dataflow::BoolValue
Models a boolean.
Definition: Value.h:92
llvm::ArrayRef
Definition: LLVM.h:34
clang::dataflow::Solver::Result::Satisfiable
static Result Satisfiable(llvm::DenseMap< AtomicBoolValue *, Assignment > Solution)
Constructs a result indicating that the queried boolean formula is satisfiable.
Definition: Solver.h:49
clang::dataflow::buildBooleanFormula
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...
Definition: WatchedLiteralsSolver.cpp:180
clang::dataflow::BooleanFormula::clauseLiterals
llvm::ArrayRef< Literal > clauseLiterals(ClauseID C) const
Returns the literals of clause C.
Definition: WatchedLiteralsSolver.cpp:173
clang::dataflow::Solver::Result::Assignment::AssignedTrue
@ AssignedTrue
clang::dataflow::notLit
static constexpr Literal notLit(Literal L)
Returns the negated literal !L.
Definition: WatchedLiteralsSolver.cpp:68
clang::dataflow::BooleanFormula
A boolean formula in conjunctive normal form.
Definition: WatchedLiteralsSolver.cpp:81
clang::dataflow::BooleanFormula::LargestVar
const Variable LargestVar
LargestVar is equal to the largest positive integer that represents a variable in the formula.
Definition: WatchedLiteralsSolver.cpp:84
std
Definition: Format.h:4477
clang::dataflow::BooleanFormula::ClauseStarts
std::vector< size_t > ClauseStarts
Start indices of clauses of the formula in Clauses.
Definition: WatchedLiteralsSolver.cpp:106
clang
Definition: CalledOnceCheck.h:17
clang::dataflow::Value::Kind::AtomicBool
@ AtomicBool
clang::dataflow::BooleanFormula::Clauses
std::vector< Literal > Clauses
Literals of all clauses in the formula.
Definition: WatchedLiteralsSolver.cpp:94
clang::prec::Level
Level
Definition: OperatorPrecedence.h:26
clang::dataflow::Solver::Result::Assignment::AssignedFalse
@ AssignedFalse
clang::dataflow::Solver::Result
Definition: Solver.h:28
clang::dataflow::WatchedLiteralsSolverImpl
Definition: WatchedLiteralsSolver.cpp:386
WatchedLiteralsSolver.h
clang::dataflow::Value::Kind::Implication
@ Implication
clang::dataflow::WatchedLiteralsSolverImpl::solve
Solver::Result solve() &&
Definition: WatchedLiteralsSolver.cpp:461
clang::dataflow::posLit
static constexpr Literal posLit(Variable V)
Returns the positive literal V.
Definition: WatchedLiteralsSolver.cpp:62
clang::dataflow::Value::getKind
Kind getKind() const
Definition: Value.h:60
Value.h
clang::dataflow::Value::Kind::Biconditional
@ Biconditional