Coverage Report

Created: 2022-07-16 07:03

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