clang 20.0.0git
Public Member Functions | List of all members
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:
Inheritance graph
[legend]

Public Member Functions

 WatchedLiteralsSolver ()=default
 
 WatchedLiteralsSolver (std::int64_t WorkLimit)
 
Result solve (llvm::ArrayRef< const Formula * > Vals) override
 Checks if the conjunction of Vals is satisfiable and returns the corresponding result.
 
bool reachedLimit () const override
 
- Public Member Functions inherited from clang::dataflow::Solver
virtual ~Solver ()=default
 
virtual Result solve (llvm::ArrayRef< const Formula * > Vals)=0
 Checks if the conjunction of Vals is satisfiable and returns the corresponding result.
 
virtual bool reachedLimit () const =0
 

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 [1], keeps references to a single "watched" literal per clause, and uses a set of "active" variables for unit propagation.

Definition at line 31 of file WatchedLiteralsSolver.h.

Constructor & Destructor Documentation

◆ WatchedLiteralsSolver() [1/2]

clang::dataflow::WatchedLiteralsSolver::WatchedLiteralsSolver ( )
default

◆ WatchedLiteralsSolver() [2/2]

clang::dataflow::WatchedLiteralsSolver::WatchedLiteralsSolver ( std::int64_t  WorkLimit)
inlineexplicit

Definition at line 47 of file WatchedLiteralsSolver.h.

Member Function Documentation

◆ reachedLimit()

bool clang::dataflow::WatchedLiteralsSolver::reachedLimit ( ) const
inlineoverridevirtual

Implements clang::dataflow::Solver.

Definition at line 52 of file WatchedLiteralsSolver.h.

◆ solve()

Solver::Result clang::dataflow::WatchedLiteralsSolver::solve ( llvm::ArrayRef< const Formula * >  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 409 of file WatchedLiteralsSolver.cpp.

References clang::dataflow::Solver::Result::Satisfiable.


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