clang
15.0.0git
|
#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"
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... | |