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 <vector>
16
17#include "clang/Analysis/FlowSensitive/CNFFormula.h"
18#include "clang/Analysis/FlowSensitive/Formula.h"
19#include "clang/Analysis/FlowSensitive/Solver.h"
20#include "clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h"
21#include "llvm/ADT/ArrayRef.h"
22#include "llvm/ADT/DenseMap.h"
23#include "llvm/ADT/DenseSet.h"
24#include "llvm/ADT/STLExtras.h"
25
26
27namespace clang {
28namespace dataflow {
29
30namespace {
31
32class WatchedLiteralsSolverImpl {
33 /// Stores the variable identifier and Atom for atomic booleans in the
34 /// formula.
35 llvm::DenseMap<Variable, Atom> Atomics;
36
37 /// A boolean formula in conjunctive normal form that the solver will attempt
38 /// to prove satisfiable. The formula will be modified in the process.
39 CNFFormula CNF;
40
41 /// Maps literals (indices of the vector) to clause identifiers (elements of
42 /// the vector) that watch the respective literals.
43 ///
44 /// For a given clause, its watched literal is always its first literal in
45 /// `Clauses`. This invariant is maintained when watched literals change.
46 std::vector<ClauseID> WatchedHead;
47
48 /// Maps clause identifiers (elements of the vector) to identifiers of other
49 /// clauses that watch the same literals, forming a set of linked lists.
50 ///
51 /// The element at index 0 stands for the identifier of the clause that
52 /// follows the null clause. It is set to 0 and isn't used. Identifiers of
53 /// clauses in the formula start from the element at index 1.
54 std::vector<ClauseID> NextWatched;
55
56 /// The search for a satisfying assignment of the variables in `Formula` will
57 /// proceed in levels, starting from 1 and going up to `Formula.LargestVar`
58 /// (inclusive). The current level is stored in `Level`. At each level the
59 /// solver will assign a value to an unassigned variable. If this leads to a
60 /// consistent partial assignment, `Level` will be incremented. Otherwise, if
61 /// it results in a conflict, the solver will backtrack by decrementing
62 /// `Level` until it reaches the most recent level where a decision was made.
63 size_t Level = 0;
64
65 /// Maps levels (indices of the vector) to variables (elements of the vector)
66 /// that are assigned values at the respective levels.
67 ///
68 /// The element at index 0 isn't used. Variables start from the element at
69 /// index 1.
70 std::vector<Variable> LevelVars;
71
72 /// State of the solver at a particular level.
73 enum class State : uint8_t {
74 /// Indicates that the solver made a decision.
75 Decision = 0,
76
77 /// Indicates that the solver made a forced move.
78 Forced = 1,
79 };
80
81 /// State of the solver at a particular level. It keeps track of previous
82 /// decisions that the solver can refer to when backtracking.
83 ///
84 /// The element at index 0 isn't used. States start from the element at index
85 /// 1.
86 std::vector<State> LevelStates;
87
88 enum class Assignment : int8_t {
89 Unassigned = -1,
90 AssignedFalse = 0,
91 AssignedTrue = 1
92 };
93
94 /// Maps variables (indices of the vector) to their assignments (elements of
95 /// the vector).
96 ///
97 /// The element at index 0 isn't used. Variable assignments start from the
98 /// element at index 1.
99 std::vector<Assignment> VarAssignments;
100
101 /// A set of unassigned variables that appear in watched literals in
102 /// `Formula`. The vector is guaranteed to contain unique elements.
103 std::vector<Variable> ActiveVars;
104
105public:
106 explicit WatchedLiteralsSolverImpl(
107 const llvm::ArrayRef<const Formula *> &Vals)
108 // `Atomics` needs to be initialized first so that we can use it as an
109 // output argument of `buildCNF()`.
110 : Atomics(), CNF(buildCNF(Formulas: Vals, Atomics)),
111 LevelVars(CNF.largestVar() + 1), LevelStates(CNF.largestVar() + 1) {
112 assert(!Vals.empty());
113
114 // Skip initialization if the formula is known to be contradictory.
115 if (CNF.knownContradictory())
116 return;
117
118 // Initialize `NextWatched` and `WatchedHead`.
119 NextWatched.push_back(x: 0);
120 const size_t NumLiterals = 2 * CNF.largestVar() + 1;
121 WatchedHead.resize(new_size: NumLiterals + 1, x: 0);
122 for (ClauseID C = 1; C <= CNF.numClauses(); ++C) {
123 // Designate the first literal as the "watched" literal of the clause.
124 Literal FirstLit = CNF.clauseLiterals(C).front();
125 NextWatched.push_back(x: WatchedHead[FirstLit]);
126 WatchedHead[FirstLit] = C;
127 }
128
129 // Initialize the state at the root level to a decision so that in
130 // `reverseForcedMoves` we don't have to check that `Level >= 0` on each
131 // iteration.
132 LevelStates[0] = State::Decision;
133
134 // Initialize all variables as unassigned.
135 VarAssignments.resize(new_size: CNF.largestVar() + 1, x: Assignment::Unassigned);
136
137 // Initialize the active variables.
138 for (Variable Var = CNF.largestVar(); Var != NullVar; --Var) {
139 if (isWatched(Lit: posLit(V: Var)) || isWatched(Lit: negLit(V: Var)))
140 ActiveVars.push_back(x: Var);
141 }
142 }
143
144 // Returns the `Result` and the number of iterations "remaining" from
145 // `MaxIterations` (that is, `MaxIterations` - iterations in this call).
146 std::pair<Solver::Result, std::int64_t> solve(std::int64_t MaxIterations) && {
147 if (CNF.knownContradictory()) {
148 // Short-cut the solving process. We already found out at CNF
149 // construction time that the formula is unsatisfiable.
150 return std::make_pair(x: Solver::Result::Unsatisfiable(), y&: MaxIterations);
151 }
152 size_t I = 0;
153 while (I < ActiveVars.size()) {
154 if (MaxIterations == 0)
155 return std::make_pair(x: Solver::Result::TimedOut(), y: 0);
156 --MaxIterations;
157
158 // Assert that the following invariants hold:
159 // 1. All active variables are unassigned.
160 // 2. All active variables form watched literals.
161 // 3. Unassigned variables that form watched literals are active.
162 // FIXME: Consider replacing these with test cases that fail if the any
163 // of the invariants is broken. That might not be easy due to the
164 // transformations performed by `buildCNF`.
165#ifdef EXPENSIVE_CHECKS
166 assert(activeVarsAreUnassigned());
167 assert(activeVarsFormWatchedLiterals());
168 assert(unassignedVarsFormingWatchedLiteralsAreActive());
169#endif
170
171 const Variable ActiveVar = ActiveVars[I];
172
173 // Look for unit clauses that contain the active variable.
174 const bool unitPosLit = watchedByUnitClause(Lit: posLit(V: ActiveVar));
175 const bool unitNegLit = watchedByUnitClause(Lit: negLit(V: ActiveVar));
176 if (unitPosLit && unitNegLit) {
177 // We found a conflict!
178
179 // Backtrack and rewind the `Level` until the most recent non-forced
180 // assignment.
181 reverseForcedMoves();
182
183 // If the root level is reached, then all possible assignments lead to
184 // a conflict.
185 if (Level == 0)
186 return std::make_pair(x: Solver::Result::Unsatisfiable(), y&: MaxIterations);
187
188 // Otherwise, take the other branch at the most recent level where a
189 // decision was made.
190 LevelStates[Level] = State::Forced;
191 const Variable Var = LevelVars[Level];
192 VarAssignments[Var] = VarAssignments[Var] == Assignment::AssignedTrue
193 ? Assignment::AssignedFalse
194 : Assignment::AssignedTrue;
195
196 updateWatchedLiterals();
197 } else if (unitPosLit || unitNegLit) {
198 // We found a unit clause! The value of its unassigned variable is
199 // forced.
200 ++Level;
201
202 LevelVars[Level] = ActiveVar;
203 LevelStates[Level] = State::Forced;
204 VarAssignments[ActiveVar] =
205 unitPosLit ? Assignment::AssignedTrue : Assignment::AssignedFalse;
206
207 // Remove the variable that was just assigned from the set of active
208 // variables.
209 if (I + 1 < ActiveVars.size()) {
210 // Replace the variable that was just assigned with the last active
211 // variable for efficient removal.
212 ActiveVars[I] = ActiveVars.back();
213 } else {
214 // This was the last active variable. Repeat the process from the
215 // beginning.
216 I = 0;
217 }
218 ActiveVars.pop_back();
219
220 updateWatchedLiterals();
221 } else if (I + 1 == ActiveVars.size()) {
222 // There are no remaining unit clauses in the formula! Make a decision
223 // for one of the active variables at the current level.
224 ++Level;
225
226 LevelVars[Level] = ActiveVar;
227 LevelStates[Level] = State::Decision;
228 VarAssignments[ActiveVar] = decideAssignment(Var: ActiveVar);
229
230 // Remove the variable that was just assigned from the set of active
231 // variables.
232 ActiveVars.pop_back();
233
234 updateWatchedLiterals();
235
236 // This was the last active variable. Repeat the process from the
237 // beginning.
238 I = 0;
239 } else {
240 ++I;
241 }
242 }
243 return std::make_pair(x: Solver::Result::Satisfiable(Solution: buildSolution()),
244 y&: MaxIterations);
245 }
246
247private:
248 /// Returns a satisfying truth assignment to the atoms in the boolean formula.
249 llvm::DenseMap<Atom, Solver::Result::Assignment> buildSolution() {
250 llvm::DenseMap<Atom, Solver::Result::Assignment> Solution;
251 for (auto &Atomic : Atomics) {
252 // A variable may have a definite true/false assignment, or it may be
253 // unassigned indicating its truth value does not affect the result of
254 // the formula. Unassigned variables are assigned to true as a default.
255 Solution[Atomic.second] =
256 VarAssignments[Atomic.first] == Assignment::AssignedFalse
257 ? Solver::Result::Assignment::AssignedFalse
258 : Solver::Result::Assignment::AssignedTrue;
259 }
260 return Solution;
261 }
262
263 /// Reverses forced moves until the most recent level where a decision was
264 /// made on the assignment of a variable.
265 void reverseForcedMoves() {
266 for (; LevelStates[Level] == State::Forced; --Level) {
267 const Variable Var = LevelVars[Level];
268
269 VarAssignments[Var] = Assignment::Unassigned;
270
271 // If the variable that we pass through is watched then we add it to the
272 // active variables.
273 if (isWatched(Lit: posLit(V: Var)) || isWatched(Lit: negLit(V: Var)))
274 ActiveVars.push_back(x: Var);
275 }
276 }
277
278 /// Updates watched literals that are affected by a variable assignment.
279 void updateWatchedLiterals() {
280 const Variable Var = LevelVars[Level];
281
282 // Update the watched literals of clauses that currently watch the literal
283 // that falsifies `Var`.
284 const Literal FalseLit = VarAssignments[Var] == Assignment::AssignedTrue
285 ? negLit(V: Var)
286 : posLit(V: Var);
287 ClauseID FalseLitWatcher = WatchedHead[FalseLit];
288 WatchedHead[FalseLit] = NullClause;
289 while (FalseLitWatcher != NullClause) {
290 const ClauseID NextFalseLitWatcher = NextWatched[FalseLitWatcher];
291
292 // Pick the first non-false literal as the new watched literal.
293 const CNFFormula::Iterator FalseLitWatcherStart =
294 CNF.startOfClause(C: FalseLitWatcher);
295 CNFFormula::Iterator NewWatchedLitIter = FalseLitWatcherStart.next();
296 while (isCurrentlyFalse(Lit: *NewWatchedLitIter))
297 ++NewWatchedLitIter;
298 const Literal NewWatchedLit = *NewWatchedLitIter;
299 const Variable NewWatchedLitVar = var(L: NewWatchedLit);
300
301 // Swap the old watched literal for the new one in `FalseLitWatcher` to
302 // maintain the invariant that the watched literal is at the beginning of
303 // the clause.
304 *NewWatchedLitIter = FalseLit;
305 *FalseLitWatcherStart = NewWatchedLit;
306
307 // If the new watched literal isn't watched by any other clause and its
308 // variable isn't assigned we need to add it to the active variables.
309 if (!isWatched(Lit: NewWatchedLit) && !isWatched(Lit: notLit(L: NewWatchedLit)) &&
310 VarAssignments[NewWatchedLitVar] == Assignment::Unassigned)
311 ActiveVars.push_back(x: NewWatchedLitVar);
312
313 NextWatched[FalseLitWatcher] = WatchedHead[NewWatchedLit];
314 WatchedHead[NewWatchedLit] = FalseLitWatcher;
315
316 // Go to the next clause that watches `FalseLit`.
317 FalseLitWatcher = NextFalseLitWatcher;
318 }
319 }
320
321 /// Returns true if and only if one of the clauses that watch `Lit` is a unit
322 /// clause.
323 bool watchedByUnitClause(Literal Lit) const {
324 for (ClauseID LitWatcher = WatchedHead[Lit]; LitWatcher != NullClause;
325 LitWatcher = NextWatched[LitWatcher]) {
326 llvm::ArrayRef<Literal> Clause = CNF.clauseLiterals(C: LitWatcher);
327
328 // Assert the invariant that the watched literal is always the first one
329 // in the clause.
330 // FIXME: Consider replacing this with a test case that fails if the
331 // invariant is broken by `updateWatchedLiterals`. That might not be easy
332 // due to the transformations performed by `buildCNF`.
333 assert(Clause.front() == Lit);
334
335 if (isUnit(Clause))
336 return true;
337 }
338 return false;
339 }
340
341 /// Returns true if and only if `Clause` is a unit clause.
342 bool isUnit(llvm::ArrayRef<Literal> Clause) const {
343 return llvm::all_of(Range: Clause.drop_front(),
344 P: [this](Literal L) { return isCurrentlyFalse(Lit: L); });
345 }
346
347 /// Returns true if and only if `Lit` evaluates to `false` in the current
348 /// partial assignment.
349 bool isCurrentlyFalse(Literal Lit) const {
350 return static_cast<int8_t>(VarAssignments[var(L: Lit)]) ==
351 static_cast<int8_t>(Lit & 1);
352 }
353
354 /// Returns true if and only if `Lit` is watched by a clause in `Formula`.
355 bool isWatched(Literal Lit) const { return WatchedHead[Lit] != NullClause; }
356
357 /// Returns an assignment for an unassigned variable.
358 Assignment decideAssignment(Variable Var) const {
359 return !isWatched(Lit: posLit(V: Var)) || isWatched(Lit: negLit(V: Var))
360 ? Assignment::AssignedFalse
361 : Assignment::AssignedTrue;
362 }
363
364 /// Returns a set of all watched literals.
365 llvm::DenseSet<Literal> watchedLiterals() const {
366 llvm::DenseSet<Literal> WatchedLiterals;
367 for (Literal Lit = 2; Lit < WatchedHead.size(); Lit++) {
368 if (WatchedHead[Lit] == NullClause)
369 continue;
370 WatchedLiterals.insert(V: Lit);
371 }
372 return WatchedLiterals;
373 }
374
375 /// Returns true if and only if all active variables are unassigned.
376 bool activeVarsAreUnassigned() const {
377 return llvm::all_of(Range: ActiveVars, P: [this](Variable Var) {
378 return VarAssignments[Var] == Assignment::Unassigned;
379 });
380 }
381
382 /// Returns true if and only if all active variables form watched literals.
383 bool activeVarsFormWatchedLiterals() const {
384 const llvm::DenseSet<Literal> WatchedLiterals = watchedLiterals();
385 return llvm::all_of(Range: ActiveVars, P: [&WatchedLiterals](Variable Var) {
386 return WatchedLiterals.contains(V: posLit(V: Var)) ||
387 WatchedLiterals.contains(V: negLit(V: Var));
388 });
389 }
390
391 /// Returns true if and only if all unassigned variables that are forming
392 /// watched literals are active.
393 bool unassignedVarsFormingWatchedLiteralsAreActive() const {
394 const llvm::DenseSet<Variable> ActiveVarsSet(ActiveVars.begin(),
395 ActiveVars.end());
396 for (Literal Lit : watchedLiterals()) {
397 const Variable Var = var(L: Lit);
398 if (VarAssignments[Var] != Assignment::Unassigned)
399 continue;
400 if (ActiveVarsSet.contains(V: Var))
401 continue;
402 return false;
403 }
404 return true;
405 }
406};
407
408} // namespace
409
410Solver::Result
411WatchedLiteralsSolver::solve(llvm::ArrayRef<const Formula *> Vals) {
412 if (Vals.empty())
413 return Solver::Result::Satisfiable(Solution: {{}});
414 auto [Res, Iterations] = WatchedLiteralsSolverImpl(Vals).solve(MaxIterations);
415 MaxIterations = Iterations;
416 return Res;
417}
418
419} // namespace dataflow
420} // namespace clang
421