clang::dataflow::Formula Class Reference

#include "clang/Analysis/FlowSensitive/Formula.h"

Public Types
enum	Kind : unsigned {   AtomRef , Literal , Not , And ,   Or , Implies , Equal }
using	AtomNames = llvm::DenseMap< Atom, std::string >

Public Member Functions
Kind	kind () const
Atom	getAtom () const
bool	literal () const
bool	isLiteral (bool b) const
ArrayRef< const Formula * >	operands () const
void	print (llvm::raw_ostream &OS, const AtomNames *=nullptr) const

Static Public Member Functions
static const Formula &	create (llvm::BumpPtrAllocator &Alloc, Kind K, ArrayRef< const Formula * > Operands, unsigned Value=0)

Detailed Description

Definition at line 49 of file Formula.h.

Member Typedef Documentation

AtomNames

using clang::dataflow::Formula::AtomNames = llvm::DenseMap<Atom, std::string>

Definition at line 87 of file Formula.h.

Member Enumeration Documentation

Kind

enum clang::dataflow::Formula::Kind : unsigned

Enumerator
AtomRef	A reference to an atomic boolean variable. We name these e.g. "V3", where 3 == atom identity == Value.
Literal	Constant true or false.
Not
And	True if its only operand is false.
Or	True if LHS and RHS are both true.
Implies	True if either LHS or RHS is true.
Equal	True if LHS is false or RHS is true.

Definition at line 51 of file Formula.h.

Member Function Documentation

create()

const Formula & clang::dataflow::Formula::create ( llvm::BumpPtrAllocator &  Alloc, Kind  K, ArrayRef< const Formula * >  Operands, unsigned  Value = 0  )

static

Definition at line 20 of file Formula.cpp.

References clang::Result.

Referenced by clang::dataflow::Arena::makeAnd(), clang::dataflow::Arena::makeAtomRef(), clang::dataflow::Arena::makeEquals(), clang::dataflow::Arena::makeImplies(), clang::dataflow::Arena::makeNot(), and clang::dataflow::Arena::makeOr().

getAtom()

Atom clang::dataflow::Formula::getAtom ( ) const

inline

Definition at line 68 of file Formula.h.

References AtomRef, and kind().

Referenced by clang::dataflow::buildCNF(), clang::dataflow::TopBoolValue::getAtom(), clang::dataflow::AtomicBoolValue::getAtom(), print(), and clang::dataflow::substitute().

isLiteral()

bool clang::dataflow::Formula::isLiteral ( bool  b ) const

inline

Definition at line 78 of file Formula.h.

References b, and kind().

Referenced by clang::dataflow::DataflowAnalysisContext::flowConditionAllows(), clang::dataflow::DataflowAnalysisContext::flowConditionImplies(), and clang::dataflow::simplifyConstraints().

kind()

Kind clang::dataflow::Formula::kind ( ) const

inline

Definition at line 66 of file Formula.h.

Referenced by clang::dataflow::AtomicBoolValue::AtomicBoolValue(), clang::dataflow::buildCNF(), clang::dataflow::FormulaBoolValue::FormulaBoolValue(), getAtom(), isLiteral(), literal(), clang::dataflow::Arena::makeAnd(), clang::dataflow::Arena::makeBoolValue(), clang::dataflow::Arena::makeEquals(), clang::dataflow::Arena::makeImplies(), clang::dataflow::Arena::makeNot(), clang::dataflow::Arena::makeOr(), operands(), print(), clang::dataflow::simplifyConstraints(), clang::dataflow::substitute(), and clang::dataflow::TopBoolValue::TopBoolValue().

literal()

bool clang::dataflow::Formula::literal ( ) const

inline

Definition at line 73 of file Formula.h.

References kind().

Referenced by clang::dataflow::buildCNF(), clang::dataflow::Arena::makeAnd(), clang::dataflow::Arena::makeEquals(), clang::dataflow::Arena::makeImplies(), clang::dataflow::Arena::makeNot(), clang::dataflow::Arena::makeOr(), and print().

operands()

ArrayRef< const Formula * > clang::dataflow::Formula::operands ( ) const

inline

Definition at line 82 of file Formula.h.

References kind().

Referenced by clang::dataflow::buildCNF(), clang::dataflow::Arena::makeNot(), print(), clang::dataflow::simplifyConstraints(), and clang::dataflow::substitute().

print()

void clang::dataflow::Formula::print	(	llvm::raw_ostream &	OS,
		const AtomNames *	Names = nullptr
	)		const

Definition at line 58 of file Formula.cpp.

References AtomRef, getAtom(), kind(), Literal, literal(), operands(), and clang::dataflow::sigil().

Referenced by clang::dataflow::operator<<().

---

The documentation for this class was generated from the following files:

• include/clang/Analysis/FlowSensitive/Formula.h
• lib/Analysis/FlowSensitive/Formula.cpp