class WatchedLiteralsSolverImpl

Declaration

class WatchedLiteralsSolverImpl { /* full declaration omitted */ };

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

Member Variables

private clang::dataflow::BooleanFormula Formula
A boolean formula in conjunctive normal form that the solver will attempt to prove satisfiable. The formula will be modified in the process.
private size_t Level = 0
The search for a satisfying assignment of the variables in `Formula` will proceed in levels, starting from 1 and going up to `Formula.LargestVar` (inclusive). The current level is stored in `Level`. At each level the solver will assign a value to an unassigned variable. If this leads to a consistent partial assignment, `Level` will be incremented. Otherwise, if it results in a conflict, the solver will backtrack by decrementing `Level` until it reaches the most recent level where a decision was made.
private std::vector<Variable> LevelVars
The element at index 0 isn't used. Variables start from the element at index 1.
private std::vector<State> LevelStates
The element at index 0 isn't used. States start from the element at index 1.
private std::vector<Assignment> VarAssignments
The element at index 0 isn't used. Variable assignments start from the element at index 1.
private std::vector<Variable> ActiveVars
A set of unassigned variables that appear in watched literals in `Formula`. The vector is guaranteed to contain unique elements.

Method Overview

Methods

WatchedLiteralsSolverImpl(
    const llvm::DenseSet<BoolValue*>& Vals)

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

Parameters

const llvm::DenseSet<BoolValue*>& Vals

bool activeVarsAreUnassigned() const

Description

Returns true if and only if all active variables are unassigned.

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

bool activeVarsFormWatchedLiterals() const

Description

Returns true if and only if all active variables form watched literals.

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

llvm::DenseMap<AtomicBoolValue*,
               Solver::Result::Assignment>
buildSolution()

Description

Returns a satisfying truth assignment to the atomic values in the boolean formula.

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

clang::dataflow::WatchedLiteralsSolverImpl::
    Assignment
    decideAssignment(
        clang::dataflow::Variable Var) const

Description

Returns an assignment for an unassigned variable.

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

Parameters

clang::dataflow::Variable Var

bool isCurrentlyFalse(
    clang::dataflow::Literal Lit) const

Description

Returns true if and only if `Lit` evaluates to `false` in the current partial assignment.

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

Parameters

clang::dataflow::Literal Lit

bool isUnit(llvm::ArrayRef<Literal> Clause) const

Description

Returns true if and only if `Clause` is a unit clause.

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

Parameters

llvm::ArrayRef<Literal> Clause

bool isWatched(clang::dataflow::Literal Lit) const

Description

Returns true if and only if `Lit` is watched by a clause in `Formula`.

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

Parameters

clang::dataflow::Literal Lit

void reverseForcedMoves()

Description

Reverses forced moves until the most recent level where a decision was made on the assignment of a variable.

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

Solver::Result solve() &&

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

bool unassignedVarsFormingWatchedLiteralsAreActive()
    const

Description

Returns true if and only if all unassigned variables that are forming watched literals are active.

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

void updateWatchedLiterals()

Description

Updates watched literals that are affected by a variable assignment.

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

bool watchedByUnitClause(
    clang::dataflow::Literal Lit) const

Description

Returns true if and only if one of the clauses that watch `Lit` is a unit clause.

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

Parameters

clang::dataflow::Literal Lit

llvm::DenseSet<Literal> watchedLiterals() const

Description

Returns a set of all watched literals.

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