clang 20.0.0git
Public Types | Public Member Functions | Static Public Member Functions | List of all members
clang::dataflow::Solver::Result Struct Reference

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

Public Types

enum class  Status { Satisfiable , Unsatisfiable , TimedOut }
 
enum class  Assignment : uint8_t { AssignedFalse = 0 , AssignedTrue = 1 }
 A boolean value is set to true or false in a truth assignment. More...
 

Public Member Functions

Status getStatus () const
 Returns the status of satisfiability checking on the queried boolean formula.
 
std::optional< llvm::DenseMap< Atom, Assignment > > getSolution () const
 Returns a truth assignment to boolean values that satisfies the queried boolean formula if available.
 

Static Public Member Functions

static Result Satisfiable (llvm::DenseMap< Atom, Assignment > Solution)
 Constructs a result indicating that the queried boolean formula is satisfiable.
 
static Result Unsatisfiable ()
 Constructs a result indicating that the queried boolean formula is unsatisfiable.
 
static Result TimedOut ()
 Constructs a result indicating that satisfiability checking on the queried boolean formula was not completed.
 

Detailed Description

Definition at line 30 of file Solver.h.

Member Enumeration Documentation

◆ Assignment

enum class clang::dataflow::Solver::Result::Assignment : uint8_t
strong

A boolean value is set to true or false in a truth assignment.

Enumerator
AssignedFalse 
AssignedTrue 

Definition at line 46 of file Solver.h.

◆ Status

Enumerator
Satisfiable 

Indicates that there exists a satisfying assignment for a boolean formula.

Unsatisfiable 

Indicates that there is no satisfying assignment for a boolean formula.

TimedOut 

Indicates that the solver gave up trying to find a satisfying assignment for a boolean formula.

Definition at line 31 of file Solver.h.

Member Function Documentation

◆ getSolution()

std::optional< llvm::DenseMap< Atom, Assignment > > clang::dataflow::Solver::Result::getSolution ( ) const
inline

Returns a truth assignment to boolean values that satisfies the queried boolean formula if available.

Otherwise, an empty optional is returned.

Definition at line 68 of file Solver.h.

Referenced by clang::dataflow::operator<<().

◆ getStatus()

Status clang::dataflow::Solver::Result::getStatus ( ) const
inline

Returns the status of satisfiability checking on the queried boolean formula.

Definition at line 64 of file Solver.h.

Referenced by clang::dataflow::operator<<().

◆ Satisfiable()

static Result clang::dataflow::Solver::Result::Satisfiable ( llvm::DenseMap< Atom, Assignment Solution)
inlinestatic

Constructs a result indicating that the queried boolean formula is satisfiable.

The result will hold a solution found by the solver.

Definition at line 50 of file Solver.h.

References Satisfiable.

◆ TimedOut()

static Result clang::dataflow::Solver::Result::TimedOut ( )
inlinestatic

Constructs a result indicating that satisfiability checking on the queried boolean formula was not completed.

Definition at line 60 of file Solver.h.

References TimedOut.

◆ Unsatisfiable()

static Result clang::dataflow::Solver::Result::Unsatisfiable ( )
inlinestatic

Constructs a result indicating that the queried boolean formula is unsatisfiable.

Definition at line 56 of file Solver.h.

References Unsatisfiable.


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