clang 20.0.0git
Classes | Public Member Functions | List of all members
clang::dataflow::Solver Class Referenceabstract

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:
Inheritance graph
[legend]

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

◆ 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: