clang  15.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 
124  Clauses.push_back(0);
125  ClauseStarts.push_back(0);
126  NextWatched.push_back(0);
127  const size_t NumLiterals = 2 * LargestVar + 1;
128  WatchedHead.resize(NumLiterals + 1, 0);
129  }
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.
140  // The literals are guaranteed to be distinct from properties of BoolValue
141  // and the construction in `buildBooleanFormula`.
142  assert(L1 != NullLit && L1 != L2 && L1 != L3 &&
143  (L2 != L3 || L2 == NullLit));
144 
145  const ClauseID C = ClauseStarts.size();
146  const size_t S = Clauses.size();
147  ClauseStarts.push_back(S);
148 
149  Clauses.push_back(L1);
150  if (L2 != NullLit)
151  Clauses.push_back(L2);
152  if (L3 != NullLit)
153  Clauses.push_back(L3);
154 
155  // Designate the first literal as the "watched" literal of the clause.
156  NextWatched.push_back(WatchedHead[L1]);
157  WatchedHead[L1] = C;
158  }
159 
160  /// Returns the number of literals in clause `C`.
161  size_t clauseSize(ClauseID C) const {
162  return C == ClauseStarts.size() - 1 ? Clauses.size() - ClauseStarts[C]
163  : ClauseStarts[C + 1] - ClauseStarts[C];
164  }
165 
166  /// Returns the literals of clause `C`.
169  }
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.
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  llvm::DenseMap<BoolValue *, Variable> SubValsToVar;
183  Variable NextVar = 1;
184  {
185  std::queue<BoolValue *> UnprocessedSubVals;
186  for (BoolValue *Val : Vals)
187  UnprocessedSubVals.push(Val);
188  while (!UnprocessedSubVals.empty()) {
189  BoolValue *Val = UnprocessedSubVals.front();
190  UnprocessedSubVals.pop();
191 
192  if (!SubValsToVar.try_emplace(Val, NextVar).second)
193  continue;
194  ++NextVar;
195 
196  // Visit the sub-values of `Val`.
197  if (auto *C = dyn_cast<ConjunctionValue>(Val)) {
198  UnprocessedSubVals.push(&C->getLeftSubValue());
199  UnprocessedSubVals.push(&C->getRightSubValue());
200  } else if (auto *D = dyn_cast<DisjunctionValue>(Val)) {
201  UnprocessedSubVals.push(&D->getLeftSubValue());
202  UnprocessedSubVals.push(&D->getRightSubValue());
203  } else if (auto *N = dyn_cast<NegationValue>(Val)) {
204  UnprocessedSubVals.push(&N->getSubVal());
205  }
206  }
207  }
208 
209  auto GetVar = [&SubValsToVar](const BoolValue *Val) {
210  auto ValIt = SubValsToVar.find(Val);
211  assert(ValIt != SubValsToVar.end());
212  return ValIt->second;
213  };
214 
215  BooleanFormula Formula(NextVar - 1);
216  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  for (BoolValue *Val : Vals)
221  Formula.addClause(posLit(GetVar(Val)));
222 
223  // Add conjuncts that represent the mapping between newly-created variables
224  // and their corresponding sub-values.
225  std::queue<BoolValue *> UnprocessedSubVals;
226  for (BoolValue *Val : Vals)
227  UnprocessedSubVals.push(Val);
228  while (!UnprocessedSubVals.empty()) {
229  const BoolValue *Val = UnprocessedSubVals.front();
230  UnprocessedSubVals.pop();
231  const Variable Var = GetVar(Val);
232 
233  if (ProcessedSubVals[Var])
234  continue;
235  ProcessedSubVals[Var] = true;
236 
237  if (auto *C = dyn_cast<ConjunctionValue>(Val)) {
238  const Variable LeftSubVar = GetVar(&C->getLeftSubValue());
239  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  Formula.addClause(negLit(Var), posLit(LeftSubVar));
245  Formula.addClause(negLit(Var), posLit(RightSubVar));
246  Formula.addClause(posLit(Var), negLit(LeftSubVar), negLit(RightSubVar));
247 
248  // Visit the sub-values of `Val`.
249  UnprocessedSubVals.push(&C->getLeftSubValue());
250  UnprocessedSubVals.push(&C->getRightSubValue());
251  } else if (auto *D = dyn_cast<DisjunctionValue>(Val)) {
252  const Variable LeftSubVar = GetVar(&D->getLeftSubValue());
253  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  Formula.addClause(negLit(Var), posLit(LeftSubVar), posLit(RightSubVar));
259  Formula.addClause(posLit(Var), negLit(LeftSubVar));
260  Formula.addClause(posLit(Var), negLit(RightSubVar));
261 
262  // Visit the sub-values of `Val`.
263  UnprocessedSubVals.push(&D->getLeftSubValue());
264  UnprocessedSubVals.push(&D->getRightSubValue());
265  } else if (auto *N = dyn_cast<NegationValue>(Val)) {
266  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  Formula.addClause(negLit(Var), negLit(SubVar));
272  Formula.addClause(posLit(Var), posLit(SubVar));
273 
274  // Visit the sub-values of `Val`.
275  UnprocessedSubVals.push(&N->getSubVal());
276  }
277  }
278 
279  return Formula;
280 }
281 
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:
338  : Formula(buildBooleanFormula(Vals)), LevelVars(Formula.LargestVar + 1),
339  LevelStates(Formula.LargestVar + 1) {
340  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  LevelStates[0] = State::Decision;
346 
347  // Initialize all variables as unassigned.
348  VarAssignments.resize(Formula.LargestVar + 1, Assignment::Unassigned);
349 
350  // Initialize the active variables.
351  for (Variable Var = Formula.LargestVar; Var != NullVar; --Var) {
352  if (isWatched(posLit(Var)) || isWatched(negLit(Var)))
353  ActiveVars.push_back(Var);
354  }
355  }
356 
358  size_t I = 0;
359  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  assert(activeVarsAreUnassigned());
368  assert(activeVarsFormWatchedLiterals());
369  assert(unassignedVarsFormingWatchedLiteralsAreActive());
370 
371  const Variable ActiveVar = ActiveVars[I];
372 
373  // Look for unit clauses that contain the active variable.
374  const bool unitPosLit = watchedByUnitClause(posLit(ActiveVar));
375  const bool unitNegLit = watchedByUnitClause(negLit(ActiveVar));
376  if (unitPosLit && unitNegLit) {
377  // We found a conflict!
378 
379  // Backtrack and rewind the `Level` until the most recent non-forced
380  // assignment.
381  reverseForcedMoves();
382 
383  // If the root level is reached, then all possible assignments lead to
384  // a conflict.
385  if (Level == 0)
387 
388  // Otherwise, take the other branch at the most recent level where a
389  // decision was made.
390  LevelStates[Level] = State::Forced;
391  const Variable Var = LevelVars[Level];
392  VarAssignments[Var] = VarAssignments[Var] == Assignment::AssignedTrue
393  ? Assignment::AssignedFalse
394  : Assignment::AssignedTrue;
395 
396  updateWatchedLiterals();
397  } else if (unitPosLit || unitNegLit) {
398  // We found a unit clause! The value of its unassigned variable is
399  // forced.
400  ++Level;
401 
402  LevelVars[Level] = ActiveVar;
403  LevelStates[Level] = State::Forced;
404  VarAssignments[ActiveVar] =
405  unitPosLit ? Assignment::AssignedTrue : Assignment::AssignedFalse;
406 
407  // Remove the variable that was just assigned from the set of active
408  // variables.
409  if (I + 1 < ActiveVars.size()) {
410  // Replace the variable that was just assigned with the last active
411  // variable for efficient removal.
412  ActiveVars[I] = ActiveVars.back();
413  } else {
414  // This was the last active variable. Repeat the process from the
415  // beginning.
416  I = 0;
417  }
418  ActiveVars.pop_back();
419 
420  updateWatchedLiterals();
421  } else if (I + 1 == ActiveVars.size()) {
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  ++Level;
425 
426  LevelVars[Level] = ActiveVar;
427  LevelStates[Level] = State::Decision;
428  VarAssignments[ActiveVar] = decideAssignment(ActiveVar);
429 
430  // Remove the variable that was just assigned from the set of active
431  // variables.
432  ActiveVars.pop_back();
433 
434  updateWatchedLiterals();
435 
436  // This was the last active variable. Repeat the process from the
437  // beginning.
438  I = 0;
439  } else {
440  ++I;
441  }
442  }
444  }
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  void reverseForcedMoves() {
450  for (; LevelStates[Level] == State::Forced; --Level) {
451  const Variable Var = LevelVars[Level];
452 
453  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  if (isWatched(posLit(Var)) || isWatched(negLit(Var)))
458  ActiveVars.push_back(Var);
459  }
460  }
461 
462  // Updates watched literals that are affected by a variable assignment.
463  void updateWatchedLiterals() {
464  const Variable Var = LevelVars[Level];
465 
466  // Update the watched literals of clauses that currently watch the literal
467  // that falsifies `Var`.
468  const Literal FalseLit = VarAssignments[Var] == Assignment::AssignedTrue
469  ? negLit(Var)
470  : posLit(Var);
471  ClauseID FalseLitWatcher = Formula.WatchedHead[FalseLit];
472  Formula.WatchedHead[FalseLit] = NullClause;
473  while (FalseLitWatcher != NullClause) {
474  const ClauseID NextFalseLitWatcher = Formula.NextWatched[FalseLitWatcher];
475 
476  // Pick the first non-false literal as the new watched literal.
477  const size_t FalseLitWatcherStart = Formula.ClauseStarts[FalseLitWatcher];
478  size_t NewWatchedLitIdx = FalseLitWatcherStart + 1;
479  while (isCurrentlyFalse(Formula.Clauses[NewWatchedLitIdx]))
480  ++NewWatchedLitIdx;
481  const Literal NewWatchedLit = Formula.Clauses[NewWatchedLitIdx];
482  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  Formula.Clauses[NewWatchedLitIdx] = FalseLit;
488  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  if (!isWatched(NewWatchedLit) && !isWatched(notLit(NewWatchedLit)) &&
493  VarAssignments[NewWatchedLitVar] == Assignment::Unassigned)
494  ActiveVars.push_back(NewWatchedLitVar);
495 
496  Formula.NextWatched[FalseLitWatcher] = Formula.WatchedHead[NewWatchedLit];
497  Formula.WatchedHead[NewWatchedLit] = FalseLitWatcher;
498 
499  // Go to the next clause that watches `FalseLit`.
500  FalseLitWatcher = NextFalseLitWatcher;
501  }
502  }
503 
504  /// Returns true if and only if one of the clauses that watch `Lit` is a unit
505  /// clause.
506  bool watchedByUnitClause(Literal Lit) const {
507  for (ClauseID LitWatcher = Formula.WatchedHead[Lit];
508  LitWatcher != NullClause;
509  LitWatcher = Formula.NextWatched[LitWatcher]) {
510  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  assert(Clause.front() == Lit);
518 
519  if (isUnit(Clause))
520  return true;
521  }
522  return false;
523  }
524 
525  /// Returns true if and only if `Clause` is a unit clause.
526  bool isUnit(llvm::ArrayRef<Literal> Clause) const {
527  return llvm::all_of(Clause.drop_front(),
528  [this](Literal L) { return isCurrentlyFalse(L); });
529  }
530 
531  /// Returns true if and only if `Lit` evaluates to `false` in the current
532  /// partial assignment.
533  bool isCurrentlyFalse(Literal Lit) const {
534  return static_cast<int8_t>(VarAssignments[var(Lit)]) ==
535  static_cast<int8_t>(Lit & 1);
536  }
537 
538  /// Returns true if and only if `Lit` is watched by a clause in `Formula`.
539  bool isWatched(Literal Lit) const {
540  return Formula.WatchedHead[Lit] != NullClause;
541  }
542 
543  /// Returns an assignment for an unassigned variable.
544  Assignment decideAssignment(Variable Var) const {
545  return !isWatched(posLit(Var)) || isWatched(negLit(Var))
546  ? Assignment::AssignedFalse
547  : Assignment::AssignedTrue;
548  }
549 
550  /// Returns a set of all watched literals.
551  llvm::DenseSet<Literal> watchedLiterals() const {
552  llvm::DenseSet<Literal> WatchedLiterals;
553  for (Literal Lit = 2; Lit < Formula.WatchedHead.size(); Lit++) {
554  if (Formula.WatchedHead[Lit] == NullClause)
555  continue;
556  WatchedLiterals.insert(Lit);
557  }
558  return WatchedLiterals;
559  }
560 
561  /// Returns true if and only if all active variables are unassigned.
562  bool activeVarsAreUnassigned() const {
563  return llvm::all_of(ActiveVars, [this](Variable Var) {
564  return VarAssignments[Var] == Assignment::Unassigned;
565  });
566  }
567 
568  /// Returns true if and only if all active variables form watched literals.
569  bool activeVarsFormWatchedLiterals() const {
570  const llvm::DenseSet<Literal> WatchedLiterals = watchedLiterals();
571  return llvm::all_of(ActiveVars, [&WatchedLiterals](Variable Var) {
572  return WatchedLiterals.contains(posLit(Var)) ||
573  WatchedLiterals.contains(negLit(Var));
574  });
575  }
576 
577  /// Returns true if and only if all unassigned variables that are forming
578  /// watched literals are active.
579  bool unassignedVarsFormingWatchedLiteralsAreActive() const {
580  const llvm::DenseSet<Variable> ActiveVarsSet(ActiveVars.begin(),
581  ActiveVars.end());
582  for (Literal Lit : watchedLiterals()) {
583  const Variable Var = var(Lit);
584  if (VarAssignments[Var] != Assignment::Unassigned)
585  continue;
586  if (ActiveVarsSet.contains(Var))
587  continue;
588  return false;
589  }
590  return true;
591  }
592 };
593 
595  return Vals.empty() ? WatchedLiteralsSolver::Result::Satisfiable
597 }
598 
599 } // namespace dataflow
600 } // 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:337
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::Solver::Result
Result
Definition: Solver.h:26
clang::dataflow::BooleanFormula::clauseSize
size_t clauseSize(ClauseID C) const
Returns the number of literals in clause C.
Definition: WatchedLiteralsSolver.cpp:161
clang::dataflow::Literal
uint32_t Literal
Literals are represented as positive integers.
Definition: WatchedLiteralsSolver.cpp:55
V
#define V(N, I)
Definition: ASTContext.h:3176
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:139
Solver.h
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:594
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::Solver::Result::Satisfiable
@ Satisfiable
Indicates that there exists a satisfying assignment for a boolean formula.
clang::dataflow::negLit
static constexpr Literal negLit(Variable V)
Returns the negative literal !V.
Definition: WatchedLiteralsSolver.cpp:65
clang::dataflow::BoolValue
Models a boolean.
Definition: Value.h:79
llvm::ArrayRef
Definition: LLVM.h:34
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:174
clang::dataflow::BooleanFormula::clauseLiterals
llvm::ArrayRef< Literal > clauseLiterals(ClauseID C) const
Returns the literals of clause C.
Definition: WatchedLiteralsSolver.cpp:167
clang::dataflow::BooleanFormula::BooleanFormula
BooleanFormula(Variable LargestVar)
Definition: WatchedLiteralsSolver.cpp:123
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
clang::dataflow::Solver::Result::Unsatisfiable
@ Unsatisfiable
Indicates that there is no satisfying assignment for a boolean formula.
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::BooleanFormula::Clauses
std::vector< Literal > Clauses
Literals of all clauses in the formula.
Definition: WatchedLiteralsSolver.cpp:94
clang::dataflow::WatchedLiteralsSolverImpl
Definition: WatchedLiteralsSolver.cpp:282
WatchedLiteralsSolver.h
clang::dataflow::WatchedLiteralsSolverImpl::solve
Solver::Result solve() &&
Definition: WatchedLiteralsSolver.cpp:357
clang::dataflow::posLit
static constexpr Literal posLit(Variable V)
Returns the positive literal V.
Definition: WatchedLiteralsSolver.cpp:62
Value.h