struct BooleanFormula

Declaration

struct BooleanFormula { /* full declaration omitted */ };

Description

A boolean formula in conjunctive normal form.

Declared at: clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp:81

Member Variables

public const clang::dataflow::Variable LargestVar

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

public std::vector<Literal> Clauses

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]`.

public std::vector<size_t> ClauseStarts

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.

public std::vector<ClauseID> WatchedHead

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

public std::vector<ClauseID> NextWatched

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.

public llvm::DenseMap<Variable, AtomicBoolValue*> Atomics

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

Method Overview

• public BooleanFormula(clang::dataflow::Variable LargestVar, llvm::DenseMap<Variable, AtomicBoolValue *> Atomics)
• public void addClause(clang::dataflow::Literal L1, clang::dataflow::Literal L2 = NullLit, clang::dataflow::Literal L3 = NullLit)
• public llvm::ArrayRef<Literal> clauseLiterals(clang::dataflow::ClauseID C) const
• public size_t clauseSize(clang::dataflow::ClauseID C) const

Methods

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

Declared at: clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp:127

Parameters

clang::dataflow::Variable LargestVar

llvm::DenseMap<Variable, AtomicBoolValue*> Atomics

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

Description

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.

Declared at: clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp:145

Parameters

clang::dataflow::Literal L1

clang::dataflow::Literal L2 = NullLit

clang::dataflow::Literal L3 = NullLit

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

Description

Returns the literals of clause `C`.

Declared at: clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp:173

Parameters

clang::dataflow::ClauseID C

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

Description

Returns the number of literals in clause `C`.

Declared at: clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp:167

Parameters

clang::dataflow::ClauseID C