clang::dataflow::CNFFormula Class Reference

A boolean formula in 3-CNF (conjunctive normal form with at most 3 literals per clause). More...

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

Classes
class	Iterator
	An iterator over all literals of all clauses in the formula. More...

Public Member Functions
	CNFFormula (Variable LargestVar)
void	addClause (ArrayRef< Literal > lits)
	Adds the L1 v ... v Ln clause to the formula.
bool	knownContradictory () const
	Returns whether the formula is known to be contradictory.
Variable	largestVar () const
	Returns the largest variable in the formula.
ClauseID	numClauses () const
	Returns the number of clauses in the formula.
size_t	clauseSize (ClauseID C) const
	Returns the number of literals in clause C.
llvm::ArrayRef< Literal >	clauseLiterals (ClauseID C) const
	Returns the literals of clause C.
Iterator	startOfClause (ClauseID C)
	Returns an iterator to the first literal of clause C.

Friends
class	Iterator

Detailed Description

A boolean formula in 3-CNF (conjunctive normal form with at most 3 literals per clause).

Definition at line 68 of file CNFFormula.h.

Constructor & Destructor Documentation

CNFFormula()

clang::dataflow::CNFFormula::CNFFormula ( Variable  LargestVar )

explicit

Definition at line 99 of file CNFFormula.cpp.

Member Function Documentation

addClause()

void clang::dataflow::CNFFormula::addClause

(

ArrayRef< Literal >

lits

)

Adds the L1 v ... v Ln clause to the formula.

Requirements:

Li must not be NullLit.

All literals in the input that are not NullLit must be distinct.

Definition at line 105 of file CNFFormula.cpp.

References clang::dataflow::NullLit.

Referenced by clang::dataflow::buildCNF().

clauseLiterals()

llvm::ArrayRef< Literal > clang::dataflow::CNFFormula::clauseLiterals ( ClauseID  C ) const

inline

Returns the literals of clause C.

If knownContradictory() is false, each clause has at least one literal.

Definition at line 129 of file CNFFormula.h.

References clang::C, and clauseSize().

Referenced by clang::dataflow::buildCNF().

clauseSize()

size_t clang::dataflow::CNFFormula::clauseSize ( ClauseID  C ) const

inline

Returns the number of literals in clause C.

Definition at line 122 of file CNFFormula.h.

References clang::C.

Referenced by clang::dataflow::buildCNF(), and clauseLiterals().

knownContradictory()

bool clang::dataflow::CNFFormula::knownContradictory ( ) const

inline

Returns whether the formula is known to be contradictory.

This is the case if any of the clauses is empty.

Definition at line 112 of file CNFFormula.h.

largestVar()

Variable clang::dataflow::CNFFormula::largestVar ( ) const

inline

Returns the largest variable in the formula.

Definition at line 115 of file CNFFormula.h.

numClauses()

ClauseID clang::dataflow::CNFFormula::numClauses ( ) const

inline

Returns the number of clauses in the formula.

Valid clause IDs are in the range [1, numClauses()].

Definition at line 119 of file CNFFormula.h.

Referenced by clang::dataflow::buildCNF().

startOfClause()

Iterator clang::dataflow::CNFFormula::startOfClause ( ClauseID  C )

inline

Returns an iterator to the first literal of clause C.

Definition at line 166 of file CNFFormula.h.

References clang::C.

Friends And Related Function Documentation

Iterator

friend class Iterator

friend

Definition at line 163 of file CNFFormula.h.

---

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

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