class WatchedLiteralsSolver

Declaration

class WatchedLiteralsSolver : public Solver { /* full declaration omitted */ };

Description

A SAT solver that is an implementation of Algorithm D from Knuth's The Art of Computer Programming Volume 4: Satisfiability, Fascicle 6. It is based on the Davis-Putnam-Logemann-Loveland (DPLL) algorithm, keeps references to a single "watched" literal per clause, and uses a set of "active" variables for unit propagation.

Declared at: clang/include/clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h:29

Inherits from: Solver

Method Overview

• public clang::dataflow::Solver::Result solve(llvm::DenseSet<BoolValue *> Vals)

Inherited from Solver:

• public solve

Methods

¶clang::dataflow::Solver::Result solve(
    llvm::DenseSet<BoolValue*> Vals)

Description

Checks if the conjunction of `Vals` is satisfiable and returns the corresponding result. Requirements: All elements in `Vals` must not be null.

Declared at: clang/include/clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h:31

Parameters

llvm::DenseSet<BoolValue*> Vals