WatchedLiteralsSolver.cpp File Reference

#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.