#include <cassert>#include <cstdint>#include <iterator>#include <queue>#include <vector>#include "clang/Analysis/FlowSensitive/Solver.h"#include "clang/Analysis/FlowSensitive/Value.h"#include "clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h"#include "llvm/ADT/DenseMap.h"#include "llvm/ADT/DenseSet.h"#include "llvm/ADT/STLExtras.h"
Include dependency graph for WatchedLiteralsSolver.cpp:
Go to the source code of this file.
Classes | |
| struct | clang::dataflow::BooleanFormula |
| A boolean formula in conjunctive normal form. More... | |
| class | clang::dataflow::WatchedLiteralsSolverImpl |
Namespaces | |
| clang | |
| clang::dataflow | |
| Dataflow Directional Tag Classes. | |
Typedefs | |
| using | clang::dataflow::Variable = uint32_t |
| Boolean variables are represented as positive integers. More... | |
| using | clang::dataflow::Literal = uint32_t |
| Literals are represented as positive integers. More... | |
| using | clang::dataflow::ClauseID = uint32_t |
| Clause identifiers are represented as positive integers. More... | |
Functions | |
| static constexpr Literal | clang::dataflow::posLit (Variable V) |
Returns the positive literal V. More... | |
| static constexpr Literal | clang::dataflow::negLit (Variable V) |
Returns the negative literal !V. More... | |
| static constexpr Literal | clang::dataflow::notLit (Literal L) |
Returns the negated literal !L. More... | |
| static constexpr Variable | clang::dataflow::var (Literal L) |
Returns the variable of L. More... | |
| BooleanFormula | clang::dataflow::buildBooleanFormula (const llvm::DenseSet< BoolValue * > &Vals) |
Converts the conjunction of Vals into a formula in conjunctive normal form where each clause has at least one and at most three literals. More... | |
Variables | |
| static constexpr Variable | clang::dataflow::NullVar = 0 |
| A null boolean variable is used as a placeholder in various data structures and algorithms. More... | |
| static constexpr Literal | clang::dataflow::NullLit = 0 |
| A null literal is used as a placeholder in various data structures and algorithms. More... | |
| static constexpr ClauseID | clang::dataflow::NullClause = 0 |
| A null clause identifier is used as a placeholder in various data structures and algorithms. More... | |
