clang  16.0.0git
Classes | Namespaces | Typedefs | Functions | Variables
WatchedLiteralsSolver.cpp File Reference
#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...