clang  15.0.0git
Public Member Functions | Public Attributes | List of all members
clang::dataflow::BooleanFormula Struct Reference

A boolean formula in conjunctive normal form. More...

Collaboration diagram for clang::dataflow::BooleanFormula:
Collaboration graph
[legend]

Public Member Functions

 BooleanFormula (Variable LargestVar, llvm::DenseMap< Variable, AtomicBoolValue * > Atomics)
 
void addClause (Literal L1, Literal L2=NullLit, Literal L3=NullLit)
 Adds the L1 v L2 v L3 clause to the formula. More...
 
size_t clauseSize (ClauseID C) const
 Returns the number of literals in clause C. More...
 
llvm::ArrayRef< LiteralclauseLiterals (ClauseID C) const
 Returns the literals of clause C. More...
 

Public Attributes

const Variable LargestVar
 LargestVar is equal to the largest positive integer that represents a variable in the formula. More...
 
std::vector< LiteralClauses
 Literals of all clauses in the formula. More...
 
std::vector< size_tClauseStarts
 Start indices of clauses of the formula in Clauses. More...
 
std::vector< ClauseIDWatchedHead
 Maps literals (indices of the vector) to clause identifiers (elements of the vector) that watch the respective literals. More...
 
std::vector< ClauseIDNextWatched
 Maps clause identifiers (elements of the vector) to identifiers of other clauses that watch the same literals, forming a set of linked lists. More...
 
llvm::DenseMap< Variable, AtomicBoolValue * > Atomics
 Stores the variable identifier and value location for atomic booleans in the formula. More...
 

Detailed Description

A boolean formula in conjunctive normal form.

Definition at line 81 of file WatchedLiteralsSolver.cpp.

Constructor & Destructor Documentation

◆ BooleanFormula()

clang::dataflow::BooleanFormula::BooleanFormula ( Variable  LargestVar,
llvm::DenseMap< Variable, AtomicBoolValue * >  Atomics 
)
inlineexplicit

Definition at line 127 of file WatchedLiteralsSolver.cpp.

References Clauses, ClauseStarts, LargestVar, NextWatched, and WatchedHead.

Member Function Documentation

◆ addClause()

void clang::dataflow::BooleanFormula::addClause ( Literal  L1,
Literal  L2 = NullLit,
Literal  L3 = NullLit 
)
inline

Adds the L1 v L2 v L3 clause to the formula.

If L2 or L3 are NullLit they are respectively omitted from the clause.

Requirements:

L1 must not be NullLit.

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

Definition at line 145 of file WatchedLiteralsSolver.cpp.

References ClauseStarts, and clang::dataflow::NullLit.

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

◆ clauseLiterals()

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

Returns the literals of clause C.

Definition at line 173 of file WatchedLiteralsSolver.cpp.

References Clauses, clauseSize(), and ClauseStarts.

◆ clauseSize()

size_t clang::dataflow::BooleanFormula::clauseSize ( ClauseID  C) const
inline

Returns the number of literals in clause C.

Definition at line 167 of file WatchedLiteralsSolver.cpp.

References Clauses, and ClauseStarts.

Referenced by clauseLiterals().

Member Data Documentation

◆ Atomics

llvm::DenseMap<Variable, AtomicBoolValue *> clang::dataflow::BooleanFormula::Atomics

Stores the variable identifier and value location for atomic booleans in the formula.

Definition at line 125 of file WatchedLiteralsSolver.cpp.

◆ Clauses

std::vector<Literal> clang::dataflow::BooleanFormula::Clauses

Literals of all clauses in the formula.

The element at index 0 stands for the literal in the null clause. It is set to 0 and isn't used. Literals of clauses in the formula start from the element at index 1.

For example, for the formula (L1 v L2) ^ (L2 v L3 v L4) the elements of Clauses will be [0, L1, L2, L2, L3, L4].

Definition at line 94 of file WatchedLiteralsSolver.cpp.

Referenced by BooleanFormula(), clauseLiterals(), and clauseSize().

◆ ClauseStarts

std::vector<size_t> clang::dataflow::BooleanFormula::ClauseStarts

Start indices of clauses of the formula in Clauses.

The element at index 0 stands for the start index of the null clause. It is set to 0 and isn't used. Start indices of clauses in the formula start from the element at index 1.

For example, for the formula (L1 v L2) ^ (L2 v L3 v L4) the elements of ClauseStarts will be [0, 1, 3]. Note that the literals of the first clause always start at index 1. The start index for the literals of the second clause depends on the size of the first clause and so on.

Definition at line 106 of file WatchedLiteralsSolver.cpp.

Referenced by addClause(), BooleanFormula(), clauseLiterals(), and clauseSize().

◆ LargestVar

const Variable clang::dataflow::BooleanFormula::LargestVar

LargestVar is equal to the largest positive integer that represents a variable in the formula.

Definition at line 84 of file WatchedLiteralsSolver.cpp.

Referenced by BooleanFormula(), and clang::dataflow::WatchedLiteralsSolverImpl::WatchedLiteralsSolverImpl().

◆ NextWatched

std::vector<ClauseID> clang::dataflow::BooleanFormula::NextWatched

Maps clause identifiers (elements of the vector) to identifiers of other clauses that watch the same literals, forming a set of linked lists.

The element at index 0 stands for the identifier of the clause that follows the null clause. It is set to 0 and isn't used. Identifiers of clauses in the formula start from the element at index 1.

Definition at line 121 of file WatchedLiteralsSolver.cpp.

Referenced by BooleanFormula().

◆ WatchedHead

std::vector<ClauseID> clang::dataflow::BooleanFormula::WatchedHead

Maps literals (indices of the vector) to clause identifiers (elements of the vector) that watch the respective literals.

For a given clause, its watched literal is always its first literal in Clauses. This invariant is maintained when watched literals change.

Definition at line 113 of file WatchedLiteralsSolver.cpp.

Referenced by BooleanFormula().


The documentation for this struct was generated from the following file: