|
clang 19.0.0git
|
A boolean formula in conjunctive normal form. More...
Public Member Functions | |
| CNFFormula (Variable LargestVar, llvm::DenseMap< Variable, Atom > Atomics) | |
| void | addClause (ArrayRef< Literal > lits) |
Adds the L1 v ... v Ln clause to the formula. | |
| size_t | clauseSize (ClauseID C) const |
Returns the number of literals in clause C. | |
| llvm::ArrayRef< Literal > | clauseLiterals (ClauseID C) const |
Returns the literals of clause C. | |
Public Attributes | |
| const Variable | LargestVar |
LargestVar is equal to the largest positive integer that represents a variable in the formula. | |
| std::vector< Literal > | Clauses |
| Literals of all clauses in the formula. | |
| std::vector< size_t > | ClauseStarts |
Start indices of clauses of the formula in Clauses. | |
| std::vector< ClauseID > | WatchedHead |
| Maps literals (indices of the vector) to clause identifiers (elements of the vector) that watch the respective literals. | |
| std::vector< ClauseID > | NextWatched |
| Maps clause identifiers (elements of the vector) to identifiers of other clauses that watch the same literals, forming a set of linked lists. | |
| llvm::DenseMap< Variable, Atom > | Atomics |
| Stores the variable identifier and Atom for atomic booleans in the formula. | |
| bool | KnownContradictory |
| Indicates that we already know the formula is unsatisfiable. | |
A boolean formula in conjunctive normal form.
Definition at line 88 of file WatchedLiteralsSolver.cpp.
|
inlineexplicit |
Definition at line 138 of file WatchedLiteralsSolver.cpp.
References Clauses, ClauseStarts, LargestVar, NextWatched, and WatchedHead.
Adds the L1 v ... v Ln clause to the formula.
Requirements:
Li must not be NullLit.
All literals in the input that are not NullLit must be distinct.
Definition at line 155 of file WatchedLiteralsSolver.cpp.
References clang::C, Clauses, ClauseStarts, NextWatched, clang::dataflow::NullLit, and WatchedHead.
Referenced by clang::dataflow::buildCNF().
|
inline |
Returns the literals of clause C.
Definition at line 176 of file WatchedLiteralsSolver.cpp.
References clang::C, Clauses, clauseSize(), and ClauseStarts.
Referenced by clang::dataflow::buildCNF().
Returns the number of literals in clause C.
Definition at line 170 of file WatchedLiteralsSolver.cpp.
References clang::C, Clauses, and ClauseStarts.
Referenced by clang::dataflow::buildCNF(), and clauseLiterals().
Stores the variable identifier and Atom for atomic booleans in the formula.
Definition at line 132 of file WatchedLiteralsSolver.cpp.
Referenced by clang::dataflow::buildCNF().
| std::vector<Literal> clang::dataflow::CNFFormula::Clauses |
Literals of all clauses in the formula.
The element at index 0 stands for the literal in the null clause. It is set to 0 and isn't used. Literals of clauses in the formula start from the element at index 1.
For example, for the formula (L1 v L2) ^ (L2 v L3 v L4) the elements of Clauses will be [0, L1, L2, L2, L3, L4].
Definition at line 101 of file WatchedLiteralsSolver.cpp.
Referenced by addClause(), clauseLiterals(), clauseSize(), and CNFFormula().
| std::vector<size_t> clang::dataflow::CNFFormula::ClauseStarts |
Start indices of clauses of the formula in Clauses.
The element at index 0 stands for the start index of the null clause. It is set to 0 and isn't used. Start indices of clauses in the formula start from the element at index 1.
For example, for the formula (L1 v L2) ^ (L2 v L3 v L4) the elements of ClauseStarts will be [0, 1, 3]. Note that the literals of the first clause always start at index 1. The start index for the literals of the second clause depends on the size of the first clause and so on.
Definition at line 113 of file WatchedLiteralsSolver.cpp.
Referenced by addClause(), clang::dataflow::buildCNF(), clauseLiterals(), clauseSize(), and CNFFormula().
| bool clang::dataflow::CNFFormula::KnownContradictory |
Indicates that we already know the formula is unsatisfiable.
During construction, we catch simple cases of conflicting unit-clauses.
Definition at line 136 of file WatchedLiteralsSolver.cpp.
Referenced by clang::dataflow::WatchedLiteralsSolverImpl::solve().
| const Variable clang::dataflow::CNFFormula::LargestVar |
LargestVar is equal to the largest positive integer that represents a variable in the formula.
Definition at line 91 of file WatchedLiteralsSolver.cpp.
Referenced by CNFFormula(), and clang::dataflow::WatchedLiteralsSolverImpl::WatchedLiteralsSolverImpl().
| std::vector<ClauseID> clang::dataflow::CNFFormula::NextWatched |
Maps clause identifiers (elements of the vector) to identifiers of other clauses that watch the same literals, forming a set of linked lists.
The element at index 0 stands for the identifier of the clause that follows the null clause. It is set to 0 and isn't used. Identifiers of clauses in the formula start from the element at index 1.
Definition at line 128 of file WatchedLiteralsSolver.cpp.
Referenced by addClause(), and CNFFormula().
| std::vector<ClauseID> clang::dataflow::CNFFormula::WatchedHead |
Maps literals (indices of the vector) to clause identifiers (elements of the vector) that watch the respective literals.
For a given clause, its watched literal is always its first literal in Clauses. This invariant is maintained when watched literals change.
Definition at line 120 of file WatchedLiteralsSolver.cpp.
Referenced by addClause(), and CNFFormula().
1.9.6