clang 18.0.0git
|
#include <cassert>
#include <cstddef>
#include <cstdint>
#include <queue>
#include <vector>
#include "clang/Analysis/FlowSensitive/Formula.h"
#include "clang/Analysis/FlowSensitive/Solver.h"
#include "clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h"
#include "llvm/ADT/ArrayRef.h"
#include "llvm/ADT/DenseMap.h"
#include "llvm/ADT/DenseSet.h"
#include "llvm/ADT/SmallVector.h"
#include "llvm/ADT/STLExtras.h"
Go to the source code of this file.
Classes | |
struct | clang::dataflow::CNFFormula |
A boolean formula in conjunctive normal form. More... | |
struct | clang::dataflow::CNFFormulaBuilder |
Applies simplifications while building up a BooleanFormula. More... | |
class | clang::dataflow::WatchedLiteralsSolverImpl |
Namespaces | |
namespace | clang |
namespace | clang::dataflow |
Dataflow Directional Tag Classes. | |
Typedefs | |
using | clang::dataflow::Variable = uint32_t |
Boolean variables are represented as positive integers. | |
using | clang::dataflow::Literal = uint32_t |
Literals are represented as positive integers. | |
using | clang::dataflow::ClauseID = uint32_t |
Clause identifiers are represented as positive integers. | |
Functions | |
static constexpr Literal | clang::dataflow::posLit (Variable V) |
Returns the positive literal V . | |
static constexpr bool | clang::dataflow::isPosLit (Literal L) |
static constexpr bool | clang::dataflow::isNegLit (Literal L) |
static constexpr Literal | clang::dataflow::negLit (Variable V) |
Returns the negative literal !V . | |
static constexpr Literal | clang::dataflow::notLit (Literal L) |
Returns the negated literal !L . | |
static constexpr Variable | clang::dataflow::var (Literal L) |
Returns the variable of L . | |
CNFFormula | clang::dataflow::buildCNF (const llvm::ArrayRef< const Formula * > &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. | |
Variables | |
static constexpr Variable | clang::dataflow::NullVar = 0 |
A null boolean variable is used as a placeholder in various data structures and algorithms. | |
static constexpr Literal | clang::dataflow::NullLit = 0 |
A null literal is used as a placeholder in various data structures and algorithms. | |
static constexpr ClauseID | clang::dataflow::NullClause = 0 |
A null clause identifier is used as a placeholder in various data structures and algorithms. | |