Coverage Report

Created: 2022-05-17 06:19

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