clang::dataflow::WatchedLiteralsSolver Class Reference

A SAT solver that is an implementation of Algorithm D from Knuth's The Art of Computer Programming Volume 4: Satisfiability, Fascicle 6. More...

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

Inheritance diagram for clang::dataflow::WatchedLiteralsSolver:

Collaboration diagram for clang::dataflow::WatchedLiteralsSolver:

Public Member Functions
Result	solve (llvm::DenseSet< BoolValue * > Vals) override
	Checks if the conjunction of Vals is satisfiable and returns the corresponding result.
Public Member Functions inherited from clang::dataflow::Solver
virtual	~Solver ()=default
virtual Result	solve (llvm::DenseSet< BoolValue * > Vals)=0
	Checks if the conjunction of Vals is satisfiable and returns the corresponding result.

Detailed 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.

Definition at line 29 of file WatchedLiteralsSolver.h.

Member Function Documentation

solve()

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

overridevirtual

Checks if the conjunction of Vals is satisfiable and returns the corresponding result.

Requirements:

All elements in Vals must not be null.

Implements clang::dataflow::Solver.

Definition at line 715 of file WatchedLiteralsSolver.cpp.

References clang::dataflow::Solver::Result::Satisfiable, and clang::dataflow::WatchedLiteralsSolverImpl::solve().

---

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

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