CNFFormula.h File Reference

#include <cstdint>
#include <vector>
#include "clang/Analysis/FlowSensitive/Formula.h"

Go to the source code of this file.

Classes
class	clang::dataflow::CNFFormula
	A boolean formula in 3-CNF (conjunctive normal form with at most 3 literals per clause). More...
class	clang::dataflow::CNFFormula::Iterator
	An iterator over all literals of all clauses in the formula. More...

Namespaces
namespace	clang
	The JSON file list parser is used to communicate input to InstallAPI.
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
constexpr Literal	clang::dataflow::posLit (Variable V)
	Returns the positive literal V.
constexpr Literal	clang::dataflow::negLit (Variable V)
	Returns the negative literal !V.
constexpr bool	clang::dataflow::isPosLit (Literal L)
	Returns whether L is a positive literal.
constexpr bool	clang::dataflow::isNegLit (Literal L)
	Returns whether L is a negative literal.
constexpr Literal	clang::dataflow::notLit (Literal L)
	Returns the negated literal !L.
constexpr Variable	clang::dataflow::var (Literal L)
	Returns the variable of L.
CNFFormula	clang::dataflow::buildCNF (const llvm::ArrayRef< const Formula * > &Formulas, llvm::DenseMap< Variable, Atom > &Atomics)
	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
constexpr Variable	clang::dataflow::NullVar = 0
	A null boolean variable is used as a placeholder in various data structures and algorithms.
constexpr Literal	clang::dataflow::NullLit = 0
	A null literal is used as a placeholder in various data structures and algorithms.
constexpr ClauseID	clang::dataflow::NullClause = 0
	A null clause identifier is used as a placeholder in various data structures and algorithms.