clang 20.0.0git
CNFFormula.h
Go to the documentation of this file.
1//===- CNFFormula.h ---------------------------------------------*- 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// A representation of a boolean formula in 3-CNF.
10//
11//===----------------------------------------------------------------------===//
12
13#ifndef LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_CNFFORMULA_H
14#define LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_CNFFORMULA_H
15
16#include <cstdint>
17#include <vector>
18
20
21namespace clang {
22namespace dataflow {
23
24/// Boolean variables are represented as positive integers.
25using Variable = uint32_t;
26
27/// A null boolean variable is used as a placeholder in various data structures
28/// and algorithms.
29constexpr Variable NullVar = 0;
30
31/// Literals are represented as positive integers. Specifically, for a boolean
32/// variable `V` that is represented as the positive integer `I`, the positive
33/// literal `V` is represented as the integer `2*I` and the negative literal
34/// `!V` is represented as the integer `2*I+1`.
35using Literal = uint32_t;
36
37/// A null literal is used as a placeholder in various data structures and
38/// algorithms.
39constexpr Literal NullLit = 0;
40
41/// Clause identifiers are represented as positive integers.
42using ClauseID = uint32_t;
43
44/// A null clause identifier is used as a placeholder in various data structures
45/// and algorithms.
46constexpr ClauseID NullClause = 0;
47
48/// Returns the positive literal `V`.
49inline constexpr Literal posLit(Variable V) { return 2 * V; }
50
51/// Returns the negative literal `!V`.
52inline constexpr Literal negLit(Variable V) { return 2 * V + 1; }
53
54/// Returns whether `L` is a positive literal.
55inline constexpr bool isPosLit(Literal L) { return 0 == (L & 1); }
56
57/// Returns whether `L` is a negative literal.
58inline constexpr bool isNegLit(Literal L) { return 1 == (L & 1); }
59
60/// Returns the negated literal `!L`.
61inline constexpr Literal notLit(Literal L) { return L ^ 1; }
62
63/// Returns the variable of `L`.
64inline constexpr Variable var(Literal L) { return L >> 1; }
65
66/// A boolean formula in 3-CNF (conjunctive normal form with at most 3 literals
67/// per clause).
69 /// `LargestVar` is equal to the largest positive integer that represents a
70 /// variable in the formula.
71 const Variable LargestVar;
72
73 /// Literals of all clauses in the formula.
74 ///
75 /// The element at index 0 stands for the literal in the null clause. It is
76 /// set to 0 and isn't used. Literals of clauses in the formula start from the
77 /// element at index 1.
78 ///
79 /// For example, for the formula `(L1 v L2) ^ (L2 v L3 v L4)` the elements of
80 /// `Clauses` will be `[0, L1, L2, L2, L3, L4]`.
81 std::vector<Literal> Clauses;
82
83 /// Start indices of clauses of the formula in `Clauses`.
84 ///
85 /// The element at index 0 stands for the start index of the null clause. It
86 /// is set to 0 and isn't used. Start indices of clauses in the formula start
87 /// from the element at index 1.
88 ///
89 /// For example, for the formula `(L1 v L2) ^ (L2 v L3 v L4)` the elements of
90 /// `ClauseStarts` will be `[0, 1, 3]`. Note that the literals of the first
91 /// clause always start at index 1. The start index for the literals of the
92 /// second clause depends on the size of the first clause and so on.
93 std::vector<size_t> ClauseStarts;
94
95 /// Indicates that we already know the formula is unsatisfiable.
96 /// During construction, we catch simple cases of conflicting unit-clauses.
97 bool KnownContradictory;
98
99public:
100 explicit CNFFormula(Variable LargestVar);
101
102 /// Adds the `L1 v ... v Ln` clause to the formula.
103 /// Requirements:
104 ///
105 /// `Li` must not be `NullLit`.
106 ///
107 /// All literals in the input that are not `NullLit` must be distinct.
108 void addClause(ArrayRef<Literal> lits);
109
110 /// Returns whether the formula is known to be contradictory.
111 /// This is the case if any of the clauses is empty.
112 bool knownContradictory() const { return KnownContradictory; }
113
114 /// Returns the largest variable in the formula.
115 Variable largestVar() const { return LargestVar; }
116
117 /// Returns the number of clauses in the formula.
118 /// Valid clause IDs are in the range [1, `numClauses()`].
119 ClauseID numClauses() const { return ClauseStarts.size() - 1; }
120
121 /// Returns the number of literals in clause `C`.
122 size_t clauseSize(ClauseID C) const {
123 return C == ClauseStarts.size() - 1 ? Clauses.size() - ClauseStarts[C]
124 : ClauseStarts[C + 1] - ClauseStarts[C];
125 }
126
127 /// Returns the literals of clause `C`.
128 /// If `knownContradictory()` is false, each clause has at least one literal.
130 size_t S = clauseSize(C);
131 if (S == 0)
133 return llvm::ArrayRef<Literal>(&Clauses[ClauseStarts[C]], S);
134 }
135
136 /// An iterator over all literals of all clauses in the formula.
137 /// The iterator allows mutation of the literal through the `*` operator.
138 /// This is to support solvers that mutate the formula during solving.
139 class Iterator {
140 friend class CNFFormula;
141 CNFFormula *CNF;
142 size_t Idx;
143 Iterator(CNFFormula *CNF, size_t Idx) : CNF(CNF), Idx(Idx) {}
144
145 public:
146 Iterator(const Iterator &) = default;
147 Iterator &operator=(const Iterator &) = default;
148
150 ++Idx;
151 assert(Idx < CNF->Clauses.size() && "Iterator out of bounds");
152 return *this;
153 }
154
155 Iterator next() const {
156 Iterator I = *this;
157 ++I;
158 return I;
159 }
160
161 Literal &operator*() const { return CNF->Clauses[Idx]; }
162 };
163 friend class Iterator;
164
165 /// Returns an iterator to the first literal of clause `C`.
166 Iterator startOfClause(ClauseID C) { return Iterator(this, ClauseStarts[C]); }
167};
168
169/// Converts the conjunction of `Vals` into a formula in conjunctive normal
170/// form where each clause has at least one and at most three literals.
171/// `Atomics` is populated with a mapping from `Variables` to the corresponding
172/// `Atom`s for atomic booleans in the input formulas.
173CNFFormula buildCNF(const llvm::ArrayRef<const Formula *> &Formulas,
174 llvm::DenseMap<Variable, Atom> &Atomics);
175
176} // namespace dataflow
177} // namespace clang
178
179#endif // LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_CNFFORMULA_H
#define V(N, I)
Definition: ASTContext.h:3341
An iterator over all literals of all clauses in the formula.
Definition: CNFFormula.h:139
Iterator & operator=(const Iterator &)=default
Iterator(const Iterator &)=default
A boolean formula in 3-CNF (conjunctive normal form with at most 3 literals per clause).
Definition: CNFFormula.h:68
bool knownContradictory() const
Returns whether the formula is known to be contradictory.
Definition: CNFFormula.h:112
size_t clauseSize(ClauseID C) const
Returns the number of literals in clause C.
Definition: CNFFormula.h:122
llvm::ArrayRef< Literal > clauseLiterals(ClauseID C) const
Returns the literals of clause C.
Definition: CNFFormula.h:129
ClauseID numClauses() const
Returns the number of clauses in the formula.
Definition: CNFFormula.h:119
Iterator startOfClause(ClauseID C)
Returns an iterator to the first literal of clause C.
Definition: CNFFormula.h:166
void addClause(ArrayRef< Literal > lits)
Adds the L1 v ... v Ln clause to the formula.
Definition: CNFFormula.cpp:105
Variable largestVar() const
Returns the largest variable in the formula.
Definition: CNFFormula.h:115
uint32_t ClauseID
Clause identifiers are represented as positive integers.
Definition: CNFFormula.h:42
constexpr Literal posLit(Variable V)
Returns the positive literal V.
Definition: CNFFormula.h:49
constexpr bool isNegLit(Literal L)
Returns whether L is a negative literal.
Definition: CNFFormula.h:58
constexpr Variable NullVar
A null boolean variable is used as a placeholder in various data structures and algorithms.
Definition: CNFFormula.h:29
CNFFormula buildCNF(const llvm::ArrayRef< const Formula * > &Formulas, llvm::DenseMap< Variable, Atom > &Atomics)
Converts the conjunction of Vals into a formula in conjunctive normal form where each clause has at l...
Definition: CNFFormula.cpp:116
constexpr Literal NullLit
A null literal is used as a placeholder in various data structures and algorithms.
Definition: CNFFormula.h:39
constexpr ClauseID NullClause
A null clause identifier is used as a placeholder in various data structures and algorithms.
Definition: CNFFormula.h:46
constexpr Variable var(Literal L)
Returns the variable of L.
Definition: CNFFormula.h:64
constexpr Literal negLit(Variable V)
Returns the negative literal !V.
Definition: CNFFormula.h:52
uint32_t Literal
Literals are represented as positive integers.
Definition: CNFFormula.h:35
uint32_t Variable
Boolean variables are represented as positive integers.
Definition: CNFFormula.h:25
constexpr bool isPosLit(Literal L)
Returns whether L is a positive literal.
Definition: CNFFormula.h:55
constexpr Literal notLit(Literal L)
Returns the negated literal !L.
Definition: CNFFormula.h:61
The JSON file list parser is used to communicate input to InstallAPI.