clang 17.0.0git
|
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"
Public Member Functions | |
Result | solve (llvm::DenseSet< BoolValue * > Vals) override |
Checks if the conjunction of Vals is satisfiable and returns the corresponding result. | |
![]() | |
virtual | ~Solver ()=default |
virtual Result | solve (llvm::DenseSet< BoolValue * > Vals)=0 |
Checks if the conjunction of Vals is satisfiable and returns the corresponding result. | |
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.
|
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().