clang::dataflow::Solver Class Reference

An interface for a SAT solver that can be used by dataflow analyses. More...

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

Inheritance diagram for clang::dataflow::Solver:

Classes
struct	Result

Public Member Functions
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

An interface for a SAT solver that can be used by dataflow analyses.

Definition at line 28 of file Solver.h.

Constructor & Destructor Documentation

~Solver()

virtual clang::dataflow::Solver::~Solver ( )

virtualdefault

Member Function Documentation

reachedLimit()

virtual bool clang::dataflow::Solver::reachedLimit ( ) const

pure virtual

Implemented in clang::dataflow::WatchedLiteralsSolver.

Referenced by clang::dataflow::diagnoseFunction().

solve()

virtual Result clang::dataflow::Solver::solve ( llvm::ArrayRef< const Formula * >  Vals )

pure virtual

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

Requirements:

All elements in Vals must not be null.

Implemented in clang::dataflow::WatchedLiteralsSolver.

---

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

• include/clang/Analysis/FlowSensitive/Solver.h