181ad6265SDimitry Andric //===- WatchedLiteralsSolver.cpp --------------------------------*- C++ -*-===//
281ad6265SDimitry Andric //
381ad6265SDimitry Andric // Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
481ad6265SDimitry Andric // See https://llvm.org/LICENSE.txt for license information.
581ad6265SDimitry Andric // SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
681ad6265SDimitry Andric //
781ad6265SDimitry Andric //===----------------------------------------------------------------------===//
881ad6265SDimitry Andric //
981ad6265SDimitry Andric // This file defines a SAT solver implementation that can be used by dataflow
1081ad6265SDimitry Andric // analyses.
1181ad6265SDimitry Andric //
1281ad6265SDimitry Andric //===----------------------------------------------------------------------===//
1381ad6265SDimitry Andric
1481ad6265SDimitry Andric #include <cassert>
15*5f757f3fSDimitry Andric #include <cstddef>
1681ad6265SDimitry Andric #include <cstdint>
1781ad6265SDimitry Andric #include <queue>
1881ad6265SDimitry Andric #include <vector>
1981ad6265SDimitry Andric
2006c3fb27SDimitry Andric #include "clang/Analysis/FlowSensitive/Formula.h"
2181ad6265SDimitry Andric #include "clang/Analysis/FlowSensitive/Solver.h"
2281ad6265SDimitry Andric #include "clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h"
2306c3fb27SDimitry Andric #include "llvm/ADT/ArrayRef.h"
2481ad6265SDimitry Andric #include "llvm/ADT/DenseMap.h"
2581ad6265SDimitry Andric #include "llvm/ADT/DenseSet.h"
26*5f757f3fSDimitry Andric #include "llvm/ADT/SmallVector.h"
2781ad6265SDimitry Andric #include "llvm/ADT/STLExtras.h"
2881ad6265SDimitry Andric
29*5f757f3fSDimitry Andric
3081ad6265SDimitry Andric namespace clang {
3181ad6265SDimitry Andric namespace dataflow {
3281ad6265SDimitry Andric
3381ad6265SDimitry Andric // `WatchedLiteralsSolver` is an implementation of Algorithm D from Knuth's
3481ad6265SDimitry Andric // The Art of Computer Programming Volume 4: Satisfiability, Fascicle 6. It is
3581ad6265SDimitry Andric // based on the backtracking DPLL algorithm [1], keeps references to a single
3681ad6265SDimitry Andric // "watched" literal per clause, and uses a set of "active" variables to perform
3781ad6265SDimitry Andric // unit propagation.
3881ad6265SDimitry Andric //
3981ad6265SDimitry Andric // The solver expects that its input is a boolean formula in conjunctive normal
4081ad6265SDimitry Andric // form that consists of clauses of at least one literal. A literal is either a
4181ad6265SDimitry Andric // boolean variable or its negation. Below we define types, data structures, and
4281ad6265SDimitry Andric // utilities that are used to represent boolean formulas in conjunctive normal
4381ad6265SDimitry Andric // form.
4481ad6265SDimitry Andric //
4581ad6265SDimitry Andric // [1] https://en.wikipedia.org/wiki/DPLL_algorithm
4681ad6265SDimitry Andric
4781ad6265SDimitry Andric /// Boolean variables are represented as positive integers.
4881ad6265SDimitry Andric using Variable = uint32_t;
4981ad6265SDimitry Andric
5081ad6265SDimitry Andric /// A null boolean variable is used as a placeholder in various data structures
5181ad6265SDimitry Andric /// and algorithms.
5281ad6265SDimitry Andric static constexpr Variable NullVar = 0;
5381ad6265SDimitry Andric
5481ad6265SDimitry Andric /// Literals are represented as positive integers. Specifically, for a boolean
5581ad6265SDimitry Andric /// variable `V` that is represented as the positive integer `I`, the positive
5681ad6265SDimitry Andric /// literal `V` is represented as the integer `2*I` and the negative literal
5781ad6265SDimitry Andric /// `!V` is represented as the integer `2*I+1`.
5881ad6265SDimitry Andric using Literal = uint32_t;
5981ad6265SDimitry Andric
6081ad6265SDimitry Andric /// A null literal is used as a placeholder in various data structures and
6181ad6265SDimitry Andric /// algorithms.
62*5f757f3fSDimitry Andric [[maybe_unused]] static constexpr Literal NullLit = 0;
6381ad6265SDimitry Andric
6481ad6265SDimitry Andric /// Returns the positive literal `V`.
posLit(Variable V)6581ad6265SDimitry Andric static constexpr Literal posLit(Variable V) { return 2 * V; }
6681ad6265SDimitry Andric
isPosLit(Literal L)67*5f757f3fSDimitry Andric static constexpr bool isPosLit(Literal L) { return 0 == (L & 1); }
68*5f757f3fSDimitry Andric
isNegLit(Literal L)69*5f757f3fSDimitry Andric static constexpr bool isNegLit(Literal L) { return 1 == (L & 1); }
70*5f757f3fSDimitry Andric
7181ad6265SDimitry Andric /// Returns the negative literal `!V`.
negLit(Variable V)7281ad6265SDimitry Andric static constexpr Literal negLit(Variable V) { return 2 * V + 1; }
7381ad6265SDimitry Andric
7481ad6265SDimitry Andric /// Returns the negated literal `!L`.
notLit(Literal L)7581ad6265SDimitry Andric static constexpr Literal notLit(Literal L) { return L ^ 1; }
7681ad6265SDimitry Andric
7781ad6265SDimitry Andric /// Returns the variable of `L`.
var(Literal L)7881ad6265SDimitry Andric static constexpr Variable var(Literal L) { return L >> 1; }
7981ad6265SDimitry Andric
8081ad6265SDimitry Andric /// Clause identifiers are represented as positive integers.
8181ad6265SDimitry Andric using ClauseID = uint32_t;
8281ad6265SDimitry Andric
8381ad6265SDimitry Andric /// A null clause identifier is used as a placeholder in various data structures
8481ad6265SDimitry Andric /// and algorithms.
8581ad6265SDimitry Andric static constexpr ClauseID NullClause = 0;
8681ad6265SDimitry Andric
8781ad6265SDimitry Andric /// A boolean formula in conjunctive normal form.
8806c3fb27SDimitry Andric struct CNFFormula {
8981ad6265SDimitry Andric /// `LargestVar` is equal to the largest positive integer that represents a
9081ad6265SDimitry Andric /// variable in the formula.
9181ad6265SDimitry Andric const Variable LargestVar;
9281ad6265SDimitry Andric
9381ad6265SDimitry Andric /// Literals of all clauses in the formula.
9481ad6265SDimitry Andric ///
9581ad6265SDimitry Andric /// The element at index 0 stands for the literal in the null clause. It is
9681ad6265SDimitry Andric /// set to 0 and isn't used. Literals of clauses in the formula start from the
9781ad6265SDimitry Andric /// element at index 1.
9881ad6265SDimitry Andric ///
9981ad6265SDimitry Andric /// For example, for the formula `(L1 v L2) ^ (L2 v L3 v L4)` the elements of
10081ad6265SDimitry Andric /// `Clauses` will be `[0, L1, L2, L2, L3, L4]`.
10181ad6265SDimitry Andric std::vector<Literal> Clauses;
10281ad6265SDimitry Andric
10381ad6265SDimitry Andric /// Start indices of clauses of the formula in `Clauses`.
10481ad6265SDimitry Andric ///
10581ad6265SDimitry Andric /// The element at index 0 stands for the start index of the null clause. It
10681ad6265SDimitry Andric /// is set to 0 and isn't used. Start indices of clauses in the formula start
10781ad6265SDimitry Andric /// from the element at index 1.
10881ad6265SDimitry Andric ///
10981ad6265SDimitry Andric /// For example, for the formula `(L1 v L2) ^ (L2 v L3 v L4)` the elements of
11081ad6265SDimitry Andric /// `ClauseStarts` will be `[0, 1, 3]`. Note that the literals of the first
11181ad6265SDimitry Andric /// clause always start at index 1. The start index for the literals of the
11281ad6265SDimitry Andric /// second clause depends on the size of the first clause and so on.
11381ad6265SDimitry Andric std::vector<size_t> ClauseStarts;
11481ad6265SDimitry Andric
11581ad6265SDimitry Andric /// Maps literals (indices of the vector) to clause identifiers (elements of
11681ad6265SDimitry Andric /// the vector) that watch the respective literals.
11781ad6265SDimitry Andric ///
11881ad6265SDimitry Andric /// For a given clause, its watched literal is always its first literal in
11981ad6265SDimitry Andric /// `Clauses`. This invariant is maintained when watched literals change.
12081ad6265SDimitry Andric std::vector<ClauseID> WatchedHead;
12181ad6265SDimitry Andric
12281ad6265SDimitry Andric /// Maps clause identifiers (elements of the vector) to identifiers of other
12381ad6265SDimitry Andric /// clauses that watch the same literals, forming a set of linked lists.
12481ad6265SDimitry Andric ///
12581ad6265SDimitry Andric /// The element at index 0 stands for the identifier of the clause that
12681ad6265SDimitry Andric /// follows the null clause. It is set to 0 and isn't used. Identifiers of
12781ad6265SDimitry Andric /// clauses in the formula start from the element at index 1.
12881ad6265SDimitry Andric std::vector<ClauseID> NextWatched;
12981ad6265SDimitry Andric
13006c3fb27SDimitry Andric /// Stores the variable identifier and Atom for atomic booleans in the
13106c3fb27SDimitry Andric /// formula.
13206c3fb27SDimitry Andric llvm::DenseMap<Variable, Atom> Atomics;
133753f127fSDimitry Andric
134*5f757f3fSDimitry Andric /// Indicates that we already know the formula is unsatisfiable.
135*5f757f3fSDimitry Andric /// During construction, we catch simple cases of conflicting unit-clauses.
136*5f757f3fSDimitry Andric bool KnownContradictory;
137*5f757f3fSDimitry Andric
CNFFormulaclang::dataflow::CNFFormula13806c3fb27SDimitry Andric explicit CNFFormula(Variable LargestVar,
13906c3fb27SDimitry Andric llvm::DenseMap<Variable, Atom> Atomics)
140*5f757f3fSDimitry Andric : LargestVar(LargestVar), Atomics(std::move(Atomics)),
141*5f757f3fSDimitry Andric KnownContradictory(false) {
14281ad6265SDimitry Andric Clauses.push_back(0);
14381ad6265SDimitry Andric ClauseStarts.push_back(0);
14481ad6265SDimitry Andric NextWatched.push_back(0);
14581ad6265SDimitry Andric const size_t NumLiterals = 2 * LargestVar + 1;
14681ad6265SDimitry Andric WatchedHead.resize(NumLiterals + 1, 0);
14781ad6265SDimitry Andric }
14881ad6265SDimitry Andric
149*5f757f3fSDimitry Andric /// Adds the `L1 v ... v Ln` clause to the formula.
15081ad6265SDimitry Andric /// Requirements:
15181ad6265SDimitry Andric ///
152*5f757f3fSDimitry Andric /// `Li` must not be `NullLit`.
15381ad6265SDimitry Andric ///
15481ad6265SDimitry Andric /// All literals in the input that are not `NullLit` must be distinct.
addClauseclang::dataflow::CNFFormula155*5f757f3fSDimitry Andric void addClause(ArrayRef<Literal> lits) {
156*5f757f3fSDimitry Andric assert(!lits.empty());
157*5f757f3fSDimitry Andric assert(llvm::all_of(lits, [](Literal L) { return L != NullLit; }));
15881ad6265SDimitry Andric
15981ad6265SDimitry Andric const ClauseID C = ClauseStarts.size();
16081ad6265SDimitry Andric const size_t S = Clauses.size();
16181ad6265SDimitry Andric ClauseStarts.push_back(S);
162*5f757f3fSDimitry Andric Clauses.insert(Clauses.end(), lits.begin(), lits.end());
16381ad6265SDimitry Andric
16481ad6265SDimitry Andric // Designate the first literal as the "watched" literal of the clause.
165*5f757f3fSDimitry Andric NextWatched.push_back(WatchedHead[lits.front()]);
166*5f757f3fSDimitry Andric WatchedHead[lits.front()] = C;
16781ad6265SDimitry Andric }
16881ad6265SDimitry Andric
16981ad6265SDimitry Andric /// Returns the number of literals in clause `C`.
clauseSizeclang::dataflow::CNFFormula17081ad6265SDimitry Andric size_t clauseSize(ClauseID C) const {
17181ad6265SDimitry Andric return C == ClauseStarts.size() - 1 ? Clauses.size() - ClauseStarts[C]
17281ad6265SDimitry Andric : ClauseStarts[C + 1] - ClauseStarts[C];
17381ad6265SDimitry Andric }
17481ad6265SDimitry Andric
17581ad6265SDimitry Andric /// Returns the literals of clause `C`.
clauseLiteralsclang::dataflow::CNFFormula17681ad6265SDimitry Andric llvm::ArrayRef<Literal> clauseLiterals(ClauseID C) const {
17781ad6265SDimitry Andric return llvm::ArrayRef<Literal>(&Clauses[ClauseStarts[C]], clauseSize(C));
17881ad6265SDimitry Andric }
17981ad6265SDimitry Andric };
18081ad6265SDimitry Andric
181*5f757f3fSDimitry Andric /// Applies simplifications while building up a BooleanFormula.
182*5f757f3fSDimitry Andric /// We keep track of unit clauses, which tell us variables that must be
183*5f757f3fSDimitry Andric /// true/false in any model that satisfies the overall formula.
184*5f757f3fSDimitry Andric /// Such variables can be dropped from subsequently-added clauses, which
185*5f757f3fSDimitry Andric /// may in turn yield more unit clauses or even a contradiction.
186*5f757f3fSDimitry Andric /// The total added complexity of this preprocessing is O(N) where we
187*5f757f3fSDimitry Andric /// for every clause, we do a lookup for each unit clauses.
188*5f757f3fSDimitry Andric /// The lookup is O(1) on average. This method won't catch all
189*5f757f3fSDimitry Andric /// contradictory formulas, more passes can in principle catch
190*5f757f3fSDimitry Andric /// more cases but we leave all these and the general case to the
191*5f757f3fSDimitry Andric /// proper SAT solver.
192*5f757f3fSDimitry Andric struct CNFFormulaBuilder {
193*5f757f3fSDimitry Andric // Formula should outlive CNFFormulaBuilder.
CNFFormulaBuilderclang::dataflow::CNFFormulaBuilder194*5f757f3fSDimitry Andric explicit CNFFormulaBuilder(CNFFormula &CNF)
195*5f757f3fSDimitry Andric : Formula(CNF) {}
196*5f757f3fSDimitry Andric
197*5f757f3fSDimitry Andric /// Adds the `L1 v ... v Ln` clause to the formula. Applies
198*5f757f3fSDimitry Andric /// simplifications, based on single-literal clauses.
199*5f757f3fSDimitry Andric ///
200*5f757f3fSDimitry Andric /// Requirements:
201*5f757f3fSDimitry Andric ///
202*5f757f3fSDimitry Andric /// `Li` must not be `NullLit`.
203*5f757f3fSDimitry Andric ///
204*5f757f3fSDimitry Andric /// All literals must be distinct.
addClauseclang::dataflow::CNFFormulaBuilder205*5f757f3fSDimitry Andric void addClause(ArrayRef<Literal> Literals) {
206*5f757f3fSDimitry Andric // We generate clauses with up to 3 literals in this file.
207*5f757f3fSDimitry Andric assert(!Literals.empty() && Literals.size() <= 3);
208*5f757f3fSDimitry Andric // Contains literals of the simplified clause.
209*5f757f3fSDimitry Andric llvm::SmallVector<Literal> Simplified;
210*5f757f3fSDimitry Andric for (auto L : Literals) {
211*5f757f3fSDimitry Andric assert(L != NullLit &&
212*5f757f3fSDimitry Andric llvm::all_of(Simplified,
213*5f757f3fSDimitry Andric [L](Literal S) { return S != L; }));
214*5f757f3fSDimitry Andric auto X = var(L);
215*5f757f3fSDimitry Andric if (trueVars.contains(X)) { // X must be true
216*5f757f3fSDimitry Andric if (isPosLit(L))
217*5f757f3fSDimitry Andric return; // Omit clause `(... v X v ...)`, it is `true`.
218*5f757f3fSDimitry Andric else
219*5f757f3fSDimitry Andric continue; // Omit `!X` from `(... v !X v ...)`.
220*5f757f3fSDimitry Andric }
221*5f757f3fSDimitry Andric if (falseVars.contains(X)) { // X must be false
222*5f757f3fSDimitry Andric if (isNegLit(L))
223*5f757f3fSDimitry Andric return; // Omit clause `(... v !X v ...)`, it is `true`.
224*5f757f3fSDimitry Andric else
225*5f757f3fSDimitry Andric continue; // Omit `X` from `(... v X v ...)`.
226*5f757f3fSDimitry Andric }
227*5f757f3fSDimitry Andric Simplified.push_back(L);
228*5f757f3fSDimitry Andric }
229*5f757f3fSDimitry Andric if (Simplified.empty()) {
230*5f757f3fSDimitry Andric // Simplification made the clause empty, which is equivalent to `false`.
231*5f757f3fSDimitry Andric // We already know that this formula is unsatisfiable.
232*5f757f3fSDimitry Andric Formula.KnownContradictory = true;
233*5f757f3fSDimitry Andric // We can add any of the input literals to get an unsatisfiable formula.
234*5f757f3fSDimitry Andric Formula.addClause(Literals[0]);
235*5f757f3fSDimitry Andric return;
236*5f757f3fSDimitry Andric }
237*5f757f3fSDimitry Andric if (Simplified.size() == 1) {
238*5f757f3fSDimitry Andric // We have new unit clause.
239*5f757f3fSDimitry Andric const Literal lit = Simplified.front();
240*5f757f3fSDimitry Andric const Variable v = var(lit);
241*5f757f3fSDimitry Andric if (isPosLit(lit))
242*5f757f3fSDimitry Andric trueVars.insert(v);
243*5f757f3fSDimitry Andric else
244*5f757f3fSDimitry Andric falseVars.insert(v);
245*5f757f3fSDimitry Andric }
246*5f757f3fSDimitry Andric Formula.addClause(Simplified);
247*5f757f3fSDimitry Andric }
248*5f757f3fSDimitry Andric
249*5f757f3fSDimitry Andric /// Returns true if we observed a contradiction while adding clauses.
250*5f757f3fSDimitry Andric /// In this case then the formula is already known to be unsatisfiable.
isKnownContradictoryclang::dataflow::CNFFormulaBuilder251*5f757f3fSDimitry Andric bool isKnownContradictory() { return Formula.KnownContradictory; }
252*5f757f3fSDimitry Andric
253*5f757f3fSDimitry Andric private:
254*5f757f3fSDimitry Andric CNFFormula &Formula;
255*5f757f3fSDimitry Andric llvm::DenseSet<Variable> trueVars;
256*5f757f3fSDimitry Andric llvm::DenseSet<Variable> falseVars;
257*5f757f3fSDimitry Andric };
258*5f757f3fSDimitry Andric
25981ad6265SDimitry Andric /// Converts the conjunction of `Vals` into a formula in conjunctive normal
26081ad6265SDimitry Andric /// form where each clause has at least one and at most three literals.
buildCNF(const llvm::ArrayRef<const Formula * > & Vals)26106c3fb27SDimitry Andric CNFFormula buildCNF(const llvm::ArrayRef<const Formula *> &Vals) {
26281ad6265SDimitry Andric // The general strategy of the algorithm implemented below is to map each
26381ad6265SDimitry Andric // of the sub-values in `Vals` to a unique variable and use these variables in
26481ad6265SDimitry Andric // the resulting CNF expression to avoid exponential blow up. The number of
26581ad6265SDimitry Andric // literals in the resulting formula is guaranteed to be linear in the number
26606c3fb27SDimitry Andric // of sub-formulas in `Vals`.
26781ad6265SDimitry Andric
26806c3fb27SDimitry Andric // Map each sub-formula in `Vals` to a unique variable.
26906c3fb27SDimitry Andric llvm::DenseMap<const Formula *, Variable> SubValsToVar;
27006c3fb27SDimitry Andric // Store variable identifiers and Atom of atomic booleans.
27106c3fb27SDimitry Andric llvm::DenseMap<Variable, Atom> Atomics;
27281ad6265SDimitry Andric Variable NextVar = 1;
27381ad6265SDimitry Andric {
27406c3fb27SDimitry Andric std::queue<const Formula *> UnprocessedSubVals;
27506c3fb27SDimitry Andric for (const Formula *Val : Vals)
27681ad6265SDimitry Andric UnprocessedSubVals.push(Val);
27781ad6265SDimitry Andric while (!UnprocessedSubVals.empty()) {
278753f127fSDimitry Andric Variable Var = NextVar;
27906c3fb27SDimitry Andric const Formula *Val = UnprocessedSubVals.front();
28081ad6265SDimitry Andric UnprocessedSubVals.pop();
28181ad6265SDimitry Andric
282753f127fSDimitry Andric if (!SubValsToVar.try_emplace(Val, Var).second)
28381ad6265SDimitry Andric continue;
28481ad6265SDimitry Andric ++NextVar;
28581ad6265SDimitry Andric
28606c3fb27SDimitry Andric for (const Formula *F : Val->operands())
28706c3fb27SDimitry Andric UnprocessedSubVals.push(F);
28806c3fb27SDimitry Andric if (Val->kind() == Formula::AtomRef)
28906c3fb27SDimitry Andric Atomics[Var] = Val->getAtom();
29081ad6265SDimitry Andric }
29181ad6265SDimitry Andric }
29281ad6265SDimitry Andric
29306c3fb27SDimitry Andric auto GetVar = [&SubValsToVar](const Formula *Val) {
29481ad6265SDimitry Andric auto ValIt = SubValsToVar.find(Val);
29581ad6265SDimitry Andric assert(ValIt != SubValsToVar.end());
29681ad6265SDimitry Andric return ValIt->second;
29781ad6265SDimitry Andric };
29881ad6265SDimitry Andric
29906c3fb27SDimitry Andric CNFFormula CNF(NextVar - 1, std::move(Atomics));
30081ad6265SDimitry Andric std::vector<bool> ProcessedSubVals(NextVar, false);
301*5f757f3fSDimitry Andric CNFFormulaBuilder builder(CNF);
30281ad6265SDimitry Andric
303*5f757f3fSDimitry Andric // Add a conjunct for each variable that represents a top-level conjunction
304*5f757f3fSDimitry Andric // value in `Vals`.
30506c3fb27SDimitry Andric for (const Formula *Val : Vals)
306*5f757f3fSDimitry Andric builder.addClause(posLit(GetVar(Val)));
30781ad6265SDimitry Andric
30881ad6265SDimitry Andric // Add conjuncts that represent the mapping between newly-created variables
30906c3fb27SDimitry Andric // and their corresponding sub-formulas.
31006c3fb27SDimitry Andric std::queue<const Formula *> UnprocessedSubVals;
31106c3fb27SDimitry Andric for (const Formula *Val : Vals)
31281ad6265SDimitry Andric UnprocessedSubVals.push(Val);
31381ad6265SDimitry Andric while (!UnprocessedSubVals.empty()) {
31406c3fb27SDimitry Andric const Formula *Val = UnprocessedSubVals.front();
31581ad6265SDimitry Andric UnprocessedSubVals.pop();
31681ad6265SDimitry Andric const Variable Var = GetVar(Val);
31781ad6265SDimitry Andric
31881ad6265SDimitry Andric if (ProcessedSubVals[Var])
31981ad6265SDimitry Andric continue;
32081ad6265SDimitry Andric ProcessedSubVals[Var] = true;
32181ad6265SDimitry Andric
32206c3fb27SDimitry Andric switch (Val->kind()) {
32306c3fb27SDimitry Andric case Formula::AtomRef:
32406c3fb27SDimitry Andric break;
325*5f757f3fSDimitry Andric case Formula::Literal:
326*5f757f3fSDimitry Andric CNF.addClause(Val->literal() ? posLit(Var) : negLit(Var));
327*5f757f3fSDimitry Andric break;
32806c3fb27SDimitry Andric case Formula::And: {
32906c3fb27SDimitry Andric const Variable LHS = GetVar(Val->operands()[0]);
33006c3fb27SDimitry Andric const Variable RHS = GetVar(Val->operands()[1]);
33181ad6265SDimitry Andric
33206c3fb27SDimitry Andric if (LHS == RHS) {
333972a253aSDimitry Andric // `X <=> (A ^ A)` is equivalent to `(!X v A) ^ (X v !A)` which is
334972a253aSDimitry Andric // already in conjunctive normal form. Below we add each of the
335972a253aSDimitry Andric // conjuncts of the latter expression to the result.
336*5f757f3fSDimitry Andric builder.addClause({negLit(Var), posLit(LHS)});
337*5f757f3fSDimitry Andric builder.addClause({posLit(Var), negLit(LHS)});
338972a253aSDimitry Andric } else {
339*5f757f3fSDimitry Andric // `X <=> (A ^ B)` is equivalent to `(!X v A) ^ (!X v B) ^ (X v !A v
340*5f757f3fSDimitry Andric // !B)` which is already in conjunctive normal form. Below we add each
341*5f757f3fSDimitry Andric // of the conjuncts of the latter expression to the result.
342*5f757f3fSDimitry Andric builder.addClause({negLit(Var), posLit(LHS)});
343*5f757f3fSDimitry Andric builder.addClause({negLit(Var), posLit(RHS)});
344*5f757f3fSDimitry Andric builder.addClause({posLit(Var), negLit(LHS), negLit(RHS)});
345972a253aSDimitry Andric }
34606c3fb27SDimitry Andric break;
34706c3fb27SDimitry Andric }
34806c3fb27SDimitry Andric case Formula::Or: {
34906c3fb27SDimitry Andric const Variable LHS = GetVar(Val->operands()[0]);
35006c3fb27SDimitry Andric const Variable RHS = GetVar(Val->operands()[1]);
35181ad6265SDimitry Andric
35206c3fb27SDimitry Andric if (LHS == RHS) {
353972a253aSDimitry Andric // `X <=> (A v A)` is equivalent to `(!X v A) ^ (X v !A)` which is
354972a253aSDimitry Andric // already in conjunctive normal form. Below we add each of the
355972a253aSDimitry Andric // conjuncts of the latter expression to the result.
356*5f757f3fSDimitry Andric builder.addClause({negLit(Var), posLit(LHS)});
357*5f757f3fSDimitry Andric builder.addClause({posLit(Var), negLit(LHS)});
358972a253aSDimitry Andric } else {
35906c3fb27SDimitry Andric // `X <=> (A v B)` is equivalent to `(!X v A v B) ^ (X v !A) ^ (X v
36006c3fb27SDimitry Andric // !B)` which is already in conjunctive normal form. Below we add each
36106c3fb27SDimitry Andric // of the conjuncts of the latter expression to the result.
362*5f757f3fSDimitry Andric builder.addClause({negLit(Var), posLit(LHS), posLit(RHS)});
363*5f757f3fSDimitry Andric builder.addClause({posLit(Var), negLit(LHS)});
364*5f757f3fSDimitry Andric builder.addClause({posLit(Var), negLit(RHS)});
365972a253aSDimitry Andric }
36606c3fb27SDimitry Andric break;
36706c3fb27SDimitry Andric }
36806c3fb27SDimitry Andric case Formula::Not: {
36906c3fb27SDimitry Andric const Variable Operand = GetVar(Val->operands()[0]);
37081ad6265SDimitry Andric
37106c3fb27SDimitry Andric // `X <=> !Y` is equivalent to `(!X v !Y) ^ (X v Y)` which is
37206c3fb27SDimitry Andric // already in conjunctive normal form. Below we add each of the
37306c3fb27SDimitry Andric // conjuncts of the latter expression to the result.
374*5f757f3fSDimitry Andric builder.addClause({negLit(Var), negLit(Operand)});
375*5f757f3fSDimitry Andric builder.addClause({posLit(Var), posLit(Operand)});
37606c3fb27SDimitry Andric break;
37706c3fb27SDimitry Andric }
37806c3fb27SDimitry Andric case Formula::Implies: {
37906c3fb27SDimitry Andric const Variable LHS = GetVar(Val->operands()[0]);
38006c3fb27SDimitry Andric const Variable RHS = GetVar(Val->operands()[1]);
381972a253aSDimitry Andric
382972a253aSDimitry Andric // `X <=> (A => B)` is equivalent to
383972a253aSDimitry Andric // `(X v A) ^ (X v !B) ^ (!X v !A v B)` which is already in
38406c3fb27SDimitry Andric // conjunctive normal form. Below we add each of the conjuncts of
38506c3fb27SDimitry Andric // the latter expression to the result.
386*5f757f3fSDimitry Andric builder.addClause({posLit(Var), posLit(LHS)});
387*5f757f3fSDimitry Andric builder.addClause({posLit(Var), negLit(RHS)});
388*5f757f3fSDimitry Andric builder.addClause({negLit(Var), negLit(LHS), posLit(RHS)});
38906c3fb27SDimitry Andric break;
39006c3fb27SDimitry Andric }
39106c3fb27SDimitry Andric case Formula::Equal: {
39206c3fb27SDimitry Andric const Variable LHS = GetVar(Val->operands()[0]);
39306c3fb27SDimitry Andric const Variable RHS = GetVar(Val->operands()[1]);
394972a253aSDimitry Andric
39506c3fb27SDimitry Andric if (LHS == RHS) {
396*5f757f3fSDimitry Andric // `X <=> (A <=> A)` is equivalent to `X` which is already in
397972a253aSDimitry Andric // conjunctive normal form. Below we add each of the conjuncts of the
398972a253aSDimitry Andric // latter expression to the result.
399*5f757f3fSDimitry Andric builder.addClause(posLit(Var));
400972a253aSDimitry Andric
401972a253aSDimitry Andric // No need to visit the sub-values of `Val`.
40206c3fb27SDimitry Andric continue;
40306c3fb27SDimitry Andric }
404972a253aSDimitry Andric // `X <=> (A <=> B)` is equivalent to
40506c3fb27SDimitry Andric // `(X v A v B) ^ (X v !A v !B) ^ (!X v A v !B) ^ (!X v !A v B)` which
40606c3fb27SDimitry Andric // is already in conjunctive normal form. Below we add each of the
40706c3fb27SDimitry Andric // conjuncts of the latter expression to the result.
408*5f757f3fSDimitry Andric builder.addClause({posLit(Var), posLit(LHS), posLit(RHS)});
409*5f757f3fSDimitry Andric builder.addClause({posLit(Var), negLit(LHS), negLit(RHS)});
410*5f757f3fSDimitry Andric builder.addClause({negLit(Var), posLit(LHS), negLit(RHS)});
411*5f757f3fSDimitry Andric builder.addClause({negLit(Var), negLit(LHS), posLit(RHS)});
41206c3fb27SDimitry Andric break;
413972a253aSDimitry Andric }
41481ad6265SDimitry Andric }
415*5f757f3fSDimitry Andric if (builder.isKnownContradictory()) {
416*5f757f3fSDimitry Andric return CNF;
417*5f757f3fSDimitry Andric }
41806c3fb27SDimitry Andric for (const Formula *Child : Val->operands())
41906c3fb27SDimitry Andric UnprocessedSubVals.push(Child);
42081ad6265SDimitry Andric }
42181ad6265SDimitry Andric
422*5f757f3fSDimitry Andric // Unit clauses that were added later were not
423*5f757f3fSDimitry Andric // considered for the simplification of earlier clauses. Do a final
424*5f757f3fSDimitry Andric // pass to find more opportunities for simplification.
425*5f757f3fSDimitry Andric CNFFormula FinalCNF(NextVar - 1, std::move(CNF.Atomics));
426*5f757f3fSDimitry Andric CNFFormulaBuilder FinalBuilder(FinalCNF);
427*5f757f3fSDimitry Andric
428*5f757f3fSDimitry Andric // Collect unit clauses.
429*5f757f3fSDimitry Andric for (ClauseID C = 1; C < CNF.ClauseStarts.size(); ++C) {
430*5f757f3fSDimitry Andric if (CNF.clauseSize(C) == 1) {
431*5f757f3fSDimitry Andric FinalBuilder.addClause(CNF.clauseLiterals(C)[0]);
432*5f757f3fSDimitry Andric }
433*5f757f3fSDimitry Andric }
434*5f757f3fSDimitry Andric
435*5f757f3fSDimitry Andric // Add all clauses that were added previously, preserving the order.
436*5f757f3fSDimitry Andric for (ClauseID C = 1; C < CNF.ClauseStarts.size(); ++C) {
437*5f757f3fSDimitry Andric FinalBuilder.addClause(CNF.clauseLiterals(C));
438*5f757f3fSDimitry Andric if (FinalBuilder.isKnownContradictory()) {
439*5f757f3fSDimitry Andric break;
440*5f757f3fSDimitry Andric }
441*5f757f3fSDimitry Andric }
442*5f757f3fSDimitry Andric // It is possible there were new unit clauses again, but
443*5f757f3fSDimitry Andric // we stop here and leave the rest to the solver algorithm.
444*5f757f3fSDimitry Andric return FinalCNF;
44581ad6265SDimitry Andric }
44681ad6265SDimitry Andric
44781ad6265SDimitry Andric class WatchedLiteralsSolverImpl {
44881ad6265SDimitry Andric /// A boolean formula in conjunctive normal form that the solver will attempt
44981ad6265SDimitry Andric /// to prove satisfiable. The formula will be modified in the process.
45006c3fb27SDimitry Andric CNFFormula CNF;
45181ad6265SDimitry Andric
45281ad6265SDimitry Andric /// The search for a satisfying assignment of the variables in `Formula` will
45381ad6265SDimitry Andric /// proceed in levels, starting from 1 and going up to `Formula.LargestVar`
45481ad6265SDimitry Andric /// (inclusive). The current level is stored in `Level`. At each level the
45581ad6265SDimitry Andric /// solver will assign a value to an unassigned variable. If this leads to a
45681ad6265SDimitry Andric /// consistent partial assignment, `Level` will be incremented. Otherwise, if
45781ad6265SDimitry Andric /// it results in a conflict, the solver will backtrack by decrementing
45881ad6265SDimitry Andric /// `Level` until it reaches the most recent level where a decision was made.
45981ad6265SDimitry Andric size_t Level = 0;
46081ad6265SDimitry Andric
46181ad6265SDimitry Andric /// Maps levels (indices of the vector) to variables (elements of the vector)
46281ad6265SDimitry Andric /// that are assigned values at the respective levels.
46381ad6265SDimitry Andric ///
46481ad6265SDimitry Andric /// The element at index 0 isn't used. Variables start from the element at
46581ad6265SDimitry Andric /// index 1.
46681ad6265SDimitry Andric std::vector<Variable> LevelVars;
46781ad6265SDimitry Andric
46881ad6265SDimitry Andric /// State of the solver at a particular level.
46981ad6265SDimitry Andric enum class State : uint8_t {
47081ad6265SDimitry Andric /// Indicates that the solver made a decision.
47181ad6265SDimitry Andric Decision = 0,
47281ad6265SDimitry Andric
47381ad6265SDimitry Andric /// Indicates that the solver made a forced move.
47481ad6265SDimitry Andric Forced = 1,
47581ad6265SDimitry Andric };
47681ad6265SDimitry Andric
47781ad6265SDimitry Andric /// State of the solver at a particular level. It keeps track of previous
47881ad6265SDimitry Andric /// decisions that the solver can refer to when backtracking.
47981ad6265SDimitry Andric ///
48081ad6265SDimitry Andric /// The element at index 0 isn't used. States start from the element at index
48181ad6265SDimitry Andric /// 1.
48281ad6265SDimitry Andric std::vector<State> LevelStates;
48381ad6265SDimitry Andric
48481ad6265SDimitry Andric enum class Assignment : int8_t {
48581ad6265SDimitry Andric Unassigned = -1,
48681ad6265SDimitry Andric AssignedFalse = 0,
48781ad6265SDimitry Andric AssignedTrue = 1
48881ad6265SDimitry Andric };
48981ad6265SDimitry Andric
49081ad6265SDimitry Andric /// Maps variables (indices of the vector) to their assignments (elements of
49181ad6265SDimitry Andric /// the vector).
49281ad6265SDimitry Andric ///
49381ad6265SDimitry Andric /// The element at index 0 isn't used. Variable assignments start from the
49481ad6265SDimitry Andric /// element at index 1.
49581ad6265SDimitry Andric std::vector<Assignment> VarAssignments;
49681ad6265SDimitry Andric
49781ad6265SDimitry Andric /// A set of unassigned variables that appear in watched literals in
49881ad6265SDimitry Andric /// `Formula`. The vector is guaranteed to contain unique elements.
49981ad6265SDimitry Andric std::vector<Variable> ActiveVars;
50081ad6265SDimitry Andric
50181ad6265SDimitry Andric public:
WatchedLiteralsSolverImpl(const llvm::ArrayRef<const Formula * > & Vals)50206c3fb27SDimitry Andric explicit WatchedLiteralsSolverImpl(
50306c3fb27SDimitry Andric const llvm::ArrayRef<const Formula *> &Vals)
50406c3fb27SDimitry Andric : CNF(buildCNF(Vals)), LevelVars(CNF.LargestVar + 1),
50506c3fb27SDimitry Andric LevelStates(CNF.LargestVar + 1) {
50681ad6265SDimitry Andric assert(!Vals.empty());
50781ad6265SDimitry Andric
50881ad6265SDimitry Andric // Initialize the state at the root level to a decision so that in
50981ad6265SDimitry Andric // `reverseForcedMoves` we don't have to check that `Level >= 0` on each
51081ad6265SDimitry Andric // iteration.
51181ad6265SDimitry Andric LevelStates[0] = State::Decision;
51281ad6265SDimitry Andric
51381ad6265SDimitry Andric // Initialize all variables as unassigned.
51406c3fb27SDimitry Andric VarAssignments.resize(CNF.LargestVar + 1, Assignment::Unassigned);
51581ad6265SDimitry Andric
51681ad6265SDimitry Andric // Initialize the active variables.
51706c3fb27SDimitry Andric for (Variable Var = CNF.LargestVar; Var != NullVar; --Var) {
51881ad6265SDimitry Andric if (isWatched(posLit(Var)) || isWatched(negLit(Var)))
51981ad6265SDimitry Andric ActiveVars.push_back(Var);
52081ad6265SDimitry Andric }
52181ad6265SDimitry Andric }
52281ad6265SDimitry Andric
52306c3fb27SDimitry Andric // Returns the `Result` and the number of iterations "remaining" from
52406c3fb27SDimitry Andric // `MaxIterations` (that is, `MaxIterations` - iterations in this call).
solve(std::int64_t MaxIterations)52506c3fb27SDimitry Andric std::pair<Solver::Result, std::int64_t> solve(std::int64_t MaxIterations) && {
526*5f757f3fSDimitry Andric if (CNF.KnownContradictory) {
527*5f757f3fSDimitry Andric // Short-cut the solving process. We already found out at CNF
528*5f757f3fSDimitry Andric // construction time that the formula is unsatisfiable.
529*5f757f3fSDimitry Andric return std::make_pair(Solver::Result::Unsatisfiable(), MaxIterations);
530*5f757f3fSDimitry Andric }
53181ad6265SDimitry Andric size_t I = 0;
53281ad6265SDimitry Andric while (I < ActiveVars.size()) {
53306c3fb27SDimitry Andric if (MaxIterations == 0)
53406c3fb27SDimitry Andric return std::make_pair(Solver::Result::TimedOut(), 0);
53506c3fb27SDimitry Andric --MaxIterations;
53606c3fb27SDimitry Andric
53781ad6265SDimitry Andric // Assert that the following invariants hold:
53881ad6265SDimitry Andric // 1. All active variables are unassigned.
53981ad6265SDimitry Andric // 2. All active variables form watched literals.
54081ad6265SDimitry Andric // 3. Unassigned variables that form watched literals are active.
54181ad6265SDimitry Andric // FIXME: Consider replacing these with test cases that fail if the any
54281ad6265SDimitry Andric // of the invariants is broken. That might not be easy due to the
54306c3fb27SDimitry Andric // transformations performed by `buildCNF`.
54481ad6265SDimitry Andric assert(activeVarsAreUnassigned());
54581ad6265SDimitry Andric assert(activeVarsFormWatchedLiterals());
54681ad6265SDimitry Andric assert(unassignedVarsFormingWatchedLiteralsAreActive());
54781ad6265SDimitry Andric
54881ad6265SDimitry Andric const Variable ActiveVar = ActiveVars[I];
54981ad6265SDimitry Andric
55081ad6265SDimitry Andric // Look for unit clauses that contain the active variable.
55181ad6265SDimitry Andric const bool unitPosLit = watchedByUnitClause(posLit(ActiveVar));
55281ad6265SDimitry Andric const bool unitNegLit = watchedByUnitClause(negLit(ActiveVar));
55381ad6265SDimitry Andric if (unitPosLit && unitNegLit) {
55481ad6265SDimitry Andric // We found a conflict!
55581ad6265SDimitry Andric
55681ad6265SDimitry Andric // Backtrack and rewind the `Level` until the most recent non-forced
55781ad6265SDimitry Andric // assignment.
55881ad6265SDimitry Andric reverseForcedMoves();
55981ad6265SDimitry Andric
56081ad6265SDimitry Andric // If the root level is reached, then all possible assignments lead to
56181ad6265SDimitry Andric // a conflict.
56281ad6265SDimitry Andric if (Level == 0)
56306c3fb27SDimitry Andric return std::make_pair(Solver::Result::Unsatisfiable(), MaxIterations);
56481ad6265SDimitry Andric
56581ad6265SDimitry Andric // Otherwise, take the other branch at the most recent level where a
56681ad6265SDimitry Andric // decision was made.
56781ad6265SDimitry Andric LevelStates[Level] = State::Forced;
56881ad6265SDimitry Andric const Variable Var = LevelVars[Level];
56981ad6265SDimitry Andric VarAssignments[Var] = VarAssignments[Var] == Assignment::AssignedTrue
57081ad6265SDimitry Andric ? Assignment::AssignedFalse
57181ad6265SDimitry Andric : Assignment::AssignedTrue;
57281ad6265SDimitry Andric
57381ad6265SDimitry Andric updateWatchedLiterals();
57481ad6265SDimitry Andric } else if (unitPosLit || unitNegLit) {
57581ad6265SDimitry Andric // We found a unit clause! The value of its unassigned variable is
57681ad6265SDimitry Andric // forced.
57781ad6265SDimitry Andric ++Level;
57881ad6265SDimitry Andric
57981ad6265SDimitry Andric LevelVars[Level] = ActiveVar;
58081ad6265SDimitry Andric LevelStates[Level] = State::Forced;
58181ad6265SDimitry Andric VarAssignments[ActiveVar] =
58281ad6265SDimitry Andric unitPosLit ? Assignment::AssignedTrue : Assignment::AssignedFalse;
58381ad6265SDimitry Andric
58481ad6265SDimitry Andric // Remove the variable that was just assigned from the set of active
58581ad6265SDimitry Andric // variables.
58681ad6265SDimitry Andric if (I + 1 < ActiveVars.size()) {
58781ad6265SDimitry Andric // Replace the variable that was just assigned with the last active
58881ad6265SDimitry Andric // variable for efficient removal.
58981ad6265SDimitry Andric ActiveVars[I] = ActiveVars.back();
59081ad6265SDimitry Andric } else {
59181ad6265SDimitry Andric // This was the last active variable. Repeat the process from the
59281ad6265SDimitry Andric // beginning.
59381ad6265SDimitry Andric I = 0;
59481ad6265SDimitry Andric }
59581ad6265SDimitry Andric ActiveVars.pop_back();
59681ad6265SDimitry Andric
59781ad6265SDimitry Andric updateWatchedLiterals();
59881ad6265SDimitry Andric } else if (I + 1 == ActiveVars.size()) {
59981ad6265SDimitry Andric // There are no remaining unit clauses in the formula! Make a decision
60081ad6265SDimitry Andric // for one of the active variables at the current level.
60181ad6265SDimitry Andric ++Level;
60281ad6265SDimitry Andric
60381ad6265SDimitry Andric LevelVars[Level] = ActiveVar;
60481ad6265SDimitry Andric LevelStates[Level] = State::Decision;
60581ad6265SDimitry Andric VarAssignments[ActiveVar] = decideAssignment(ActiveVar);
60681ad6265SDimitry Andric
60781ad6265SDimitry Andric // Remove the variable that was just assigned from the set of active
60881ad6265SDimitry Andric // variables.
60981ad6265SDimitry Andric ActiveVars.pop_back();
61081ad6265SDimitry Andric
61181ad6265SDimitry Andric updateWatchedLiterals();
61281ad6265SDimitry Andric
61381ad6265SDimitry Andric // This was the last active variable. Repeat the process from the
61481ad6265SDimitry Andric // beginning.
61581ad6265SDimitry Andric I = 0;
61681ad6265SDimitry Andric } else {
61781ad6265SDimitry Andric ++I;
61881ad6265SDimitry Andric }
61981ad6265SDimitry Andric }
620*5f757f3fSDimitry Andric return std::make_pair(Solver::Result::Satisfiable(buildSolution()),
621*5f757f3fSDimitry Andric MaxIterations);
62281ad6265SDimitry Andric }
62381ad6265SDimitry Andric
62481ad6265SDimitry Andric private:
62506c3fb27SDimitry Andric /// Returns a satisfying truth assignment to the atoms in the boolean formula.
buildSolution()62606c3fb27SDimitry Andric llvm::DenseMap<Atom, Solver::Result::Assignment> buildSolution() {
62706c3fb27SDimitry Andric llvm::DenseMap<Atom, Solver::Result::Assignment> Solution;
62806c3fb27SDimitry Andric for (auto &Atomic : CNF.Atomics) {
629753f127fSDimitry Andric // A variable may have a definite true/false assignment, or it may be
630753f127fSDimitry Andric // unassigned indicating its truth value does not affect the result of
631753f127fSDimitry Andric // the formula. Unassigned variables are assigned to true as a default.
632753f127fSDimitry Andric Solution[Atomic.second] =
633753f127fSDimitry Andric VarAssignments[Atomic.first] == Assignment::AssignedFalse
634753f127fSDimitry Andric ? Solver::Result::Assignment::AssignedFalse
635753f127fSDimitry Andric : Solver::Result::Assignment::AssignedTrue;
636753f127fSDimitry Andric }
637753f127fSDimitry Andric return Solution;
638753f127fSDimitry Andric }
639753f127fSDimitry Andric
640753f127fSDimitry Andric /// Reverses forced moves until the most recent level where a decision was
641753f127fSDimitry Andric /// made on the assignment of a variable.
reverseForcedMoves()64281ad6265SDimitry Andric void reverseForcedMoves() {
64381ad6265SDimitry Andric for (; LevelStates[Level] == State::Forced; --Level) {
64481ad6265SDimitry Andric const Variable Var = LevelVars[Level];
64581ad6265SDimitry Andric
64681ad6265SDimitry Andric VarAssignments[Var] = Assignment::Unassigned;
64781ad6265SDimitry Andric
64881ad6265SDimitry Andric // If the variable that we pass through is watched then we add it to the
64981ad6265SDimitry Andric // active variables.
65081ad6265SDimitry Andric if (isWatched(posLit(Var)) || isWatched(negLit(Var)))
65181ad6265SDimitry Andric ActiveVars.push_back(Var);
65281ad6265SDimitry Andric }
65381ad6265SDimitry Andric }
65481ad6265SDimitry Andric
655753f127fSDimitry Andric /// Updates watched literals that are affected by a variable assignment.
updateWatchedLiterals()65681ad6265SDimitry Andric void updateWatchedLiterals() {
65781ad6265SDimitry Andric const Variable Var = LevelVars[Level];
65881ad6265SDimitry Andric
65981ad6265SDimitry Andric // Update the watched literals of clauses that currently watch the literal
66081ad6265SDimitry Andric // that falsifies `Var`.
66181ad6265SDimitry Andric const Literal FalseLit = VarAssignments[Var] == Assignment::AssignedTrue
66281ad6265SDimitry Andric ? negLit(Var)
66381ad6265SDimitry Andric : posLit(Var);
66406c3fb27SDimitry Andric ClauseID FalseLitWatcher = CNF.WatchedHead[FalseLit];
66506c3fb27SDimitry Andric CNF.WatchedHead[FalseLit] = NullClause;
66681ad6265SDimitry Andric while (FalseLitWatcher != NullClause) {
66706c3fb27SDimitry Andric const ClauseID NextFalseLitWatcher = CNF.NextWatched[FalseLitWatcher];
66881ad6265SDimitry Andric
66981ad6265SDimitry Andric // Pick the first non-false literal as the new watched literal.
67006c3fb27SDimitry Andric const size_t FalseLitWatcherStart = CNF.ClauseStarts[FalseLitWatcher];
67181ad6265SDimitry Andric size_t NewWatchedLitIdx = FalseLitWatcherStart + 1;
67206c3fb27SDimitry Andric while (isCurrentlyFalse(CNF.Clauses[NewWatchedLitIdx]))
67381ad6265SDimitry Andric ++NewWatchedLitIdx;
67406c3fb27SDimitry Andric const Literal NewWatchedLit = CNF.Clauses[NewWatchedLitIdx];
67581ad6265SDimitry Andric const Variable NewWatchedLitVar = var(NewWatchedLit);
67681ad6265SDimitry Andric
67781ad6265SDimitry Andric // Swap the old watched literal for the new one in `FalseLitWatcher` to
67881ad6265SDimitry Andric // maintain the invariant that the watched literal is at the beginning of
67981ad6265SDimitry Andric // the clause.
68006c3fb27SDimitry Andric CNF.Clauses[NewWatchedLitIdx] = FalseLit;
68106c3fb27SDimitry Andric CNF.Clauses[FalseLitWatcherStart] = NewWatchedLit;
68281ad6265SDimitry Andric
68381ad6265SDimitry Andric // If the new watched literal isn't watched by any other clause and its
68481ad6265SDimitry Andric // variable isn't assigned we need to add it to the active variables.
68581ad6265SDimitry Andric if (!isWatched(NewWatchedLit) && !isWatched(notLit(NewWatchedLit)) &&
68681ad6265SDimitry Andric VarAssignments[NewWatchedLitVar] == Assignment::Unassigned)
68781ad6265SDimitry Andric ActiveVars.push_back(NewWatchedLitVar);
68881ad6265SDimitry Andric
68906c3fb27SDimitry Andric CNF.NextWatched[FalseLitWatcher] = CNF.WatchedHead[NewWatchedLit];
69006c3fb27SDimitry Andric CNF.WatchedHead[NewWatchedLit] = FalseLitWatcher;
69181ad6265SDimitry Andric
69281ad6265SDimitry Andric // Go to the next clause that watches `FalseLit`.
69381ad6265SDimitry Andric FalseLitWatcher = NextFalseLitWatcher;
69481ad6265SDimitry Andric }
69581ad6265SDimitry Andric }
69681ad6265SDimitry Andric
69781ad6265SDimitry Andric /// Returns true if and only if one of the clauses that watch `Lit` is a unit
69881ad6265SDimitry Andric /// clause.
watchedByUnitClause(Literal Lit) const69981ad6265SDimitry Andric bool watchedByUnitClause(Literal Lit) const {
70006c3fb27SDimitry Andric for (ClauseID LitWatcher = CNF.WatchedHead[Lit]; LitWatcher != NullClause;
70106c3fb27SDimitry Andric LitWatcher = CNF.NextWatched[LitWatcher]) {
70206c3fb27SDimitry Andric llvm::ArrayRef<Literal> Clause = CNF.clauseLiterals(LitWatcher);
70381ad6265SDimitry Andric
70481ad6265SDimitry Andric // Assert the invariant that the watched literal is always the first one
70581ad6265SDimitry Andric // in the clause.
70681ad6265SDimitry Andric // FIXME: Consider replacing this with a test case that fails if the
70781ad6265SDimitry Andric // invariant is broken by `updateWatchedLiterals`. That might not be easy
70806c3fb27SDimitry Andric // due to the transformations performed by `buildCNF`.
70981ad6265SDimitry Andric assert(Clause.front() == Lit);
71081ad6265SDimitry Andric
71181ad6265SDimitry Andric if (isUnit(Clause))
71281ad6265SDimitry Andric return true;
71381ad6265SDimitry Andric }
71481ad6265SDimitry Andric return false;
71581ad6265SDimitry Andric }
71681ad6265SDimitry Andric
71781ad6265SDimitry Andric /// Returns true if and only if `Clause` is a unit clause.
isUnit(llvm::ArrayRef<Literal> Clause) const71881ad6265SDimitry Andric bool isUnit(llvm::ArrayRef<Literal> Clause) const {
71981ad6265SDimitry Andric return llvm::all_of(Clause.drop_front(),
72081ad6265SDimitry Andric [this](Literal L) { return isCurrentlyFalse(L); });
72181ad6265SDimitry Andric }
72281ad6265SDimitry Andric
72381ad6265SDimitry Andric /// Returns true if and only if `Lit` evaluates to `false` in the current
72481ad6265SDimitry Andric /// partial assignment.
isCurrentlyFalse(Literal Lit) const72581ad6265SDimitry Andric bool isCurrentlyFalse(Literal Lit) const {
72681ad6265SDimitry Andric return static_cast<int8_t>(VarAssignments[var(Lit)]) ==
72781ad6265SDimitry Andric static_cast<int8_t>(Lit & 1);
72881ad6265SDimitry Andric }
72981ad6265SDimitry Andric
73081ad6265SDimitry Andric /// Returns true if and only if `Lit` is watched by a clause in `Formula`.
isWatched(Literal Lit) const73181ad6265SDimitry Andric bool isWatched(Literal Lit) const {
73206c3fb27SDimitry Andric return CNF.WatchedHead[Lit] != NullClause;
73381ad6265SDimitry Andric }
73481ad6265SDimitry Andric
73581ad6265SDimitry Andric /// Returns an assignment for an unassigned variable.
decideAssignment(Variable Var) const73681ad6265SDimitry Andric Assignment decideAssignment(Variable Var) const {
73781ad6265SDimitry Andric return !isWatched(posLit(Var)) || isWatched(negLit(Var))
73881ad6265SDimitry Andric ? Assignment::AssignedFalse
73981ad6265SDimitry Andric : Assignment::AssignedTrue;
74081ad6265SDimitry Andric }
74181ad6265SDimitry Andric
74281ad6265SDimitry Andric /// Returns a set of all watched literals.
watchedLiterals() const74381ad6265SDimitry Andric llvm::DenseSet<Literal> watchedLiterals() const {
74481ad6265SDimitry Andric llvm::DenseSet<Literal> WatchedLiterals;
74506c3fb27SDimitry Andric for (Literal Lit = 2; Lit < CNF.WatchedHead.size(); Lit++) {
74606c3fb27SDimitry Andric if (CNF.WatchedHead[Lit] == NullClause)
74781ad6265SDimitry Andric continue;
74881ad6265SDimitry Andric WatchedLiterals.insert(Lit);
74981ad6265SDimitry Andric }
75081ad6265SDimitry Andric return WatchedLiterals;
75181ad6265SDimitry Andric }
75281ad6265SDimitry Andric
75381ad6265SDimitry Andric /// Returns true if and only if all active variables are unassigned.
activeVarsAreUnassigned() const75481ad6265SDimitry Andric bool activeVarsAreUnassigned() const {
75581ad6265SDimitry Andric return llvm::all_of(ActiveVars, [this](Variable Var) {
75681ad6265SDimitry Andric return VarAssignments[Var] == Assignment::Unassigned;
75781ad6265SDimitry Andric });
75881ad6265SDimitry Andric }
75981ad6265SDimitry Andric
76081ad6265SDimitry Andric /// Returns true if and only if all active variables form watched literals.
activeVarsFormWatchedLiterals() const76181ad6265SDimitry Andric bool activeVarsFormWatchedLiterals() const {
76281ad6265SDimitry Andric const llvm::DenseSet<Literal> WatchedLiterals = watchedLiterals();
76381ad6265SDimitry Andric return llvm::all_of(ActiveVars, [&WatchedLiterals](Variable Var) {
76481ad6265SDimitry Andric return WatchedLiterals.contains(posLit(Var)) ||
76581ad6265SDimitry Andric WatchedLiterals.contains(negLit(Var));
76681ad6265SDimitry Andric });
76781ad6265SDimitry Andric }
76881ad6265SDimitry Andric
76981ad6265SDimitry Andric /// Returns true if and only if all unassigned variables that are forming
77081ad6265SDimitry Andric /// watched literals are active.
unassignedVarsFormingWatchedLiteralsAreActive() const77181ad6265SDimitry Andric bool unassignedVarsFormingWatchedLiteralsAreActive() const {
77281ad6265SDimitry Andric const llvm::DenseSet<Variable> ActiveVarsSet(ActiveVars.begin(),
77381ad6265SDimitry Andric ActiveVars.end());
77481ad6265SDimitry Andric for (Literal Lit : watchedLiterals()) {
77581ad6265SDimitry Andric const Variable Var = var(Lit);
77681ad6265SDimitry Andric if (VarAssignments[Var] != Assignment::Unassigned)
77781ad6265SDimitry Andric continue;
77881ad6265SDimitry Andric if (ActiveVarsSet.contains(Var))
77981ad6265SDimitry Andric continue;
78081ad6265SDimitry Andric return false;
78181ad6265SDimitry Andric }
78281ad6265SDimitry Andric return true;
78381ad6265SDimitry Andric }
78481ad6265SDimitry Andric };
78581ad6265SDimitry Andric
78606c3fb27SDimitry Andric Solver::Result
solve(llvm::ArrayRef<const Formula * > Vals)78706c3fb27SDimitry Andric WatchedLiteralsSolver::solve(llvm::ArrayRef<const Formula *> Vals) {
78806c3fb27SDimitry Andric if (Vals.empty())
78906c3fb27SDimitry Andric return Solver::Result::Satisfiable({{}});
790*5f757f3fSDimitry Andric auto [Res, Iterations] = WatchedLiteralsSolverImpl(Vals).solve(MaxIterations);
79106c3fb27SDimitry Andric MaxIterations = Iterations;
79206c3fb27SDimitry Andric return Res;
79381ad6265SDimitry Andric }
79481ad6265SDimitry Andric
79581ad6265SDimitry Andric } // namespace dataflow
79681ad6265SDimitry Andric } // namespace clang
797