clang  16.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  Status { Status::Satisfiable, Status::Unsatisfiable, Status::TimedOut }
 
enum  Assignment : uint8_t { Assignment::AssignedFalse = 0, Assignment::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. More...
 
llvm::Optional< llvm::DenseMap< AtomicBoolValue *, Assignment > > getSolution () const
 Returns a truth assignment to boolean values that satisfies the queried boolean formula if available. More...
 

Static Public Member Functions

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

Detailed Description

Definition at line 28 of file Solver.h.

Member Enumeration Documentation

◆ Assignment

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

Enumerator
AssignedFalse 
AssignedTrue 

Definition at line 44 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 29 of file Solver.h.

Member Function Documentation

◆ getSolution()

llvm::Optional<llvm::DenseMap<AtomicBoolValue *, 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.

◆ getStatus()

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

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

Definition at line 63 of file Solver.h.

◆ Satisfiable()

static Result clang::dataflow::Solver::Result::Satisfiable ( llvm::DenseMap< AtomicBoolValue *, 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 49 of file Solver.h.

References Satisfiable.

Referenced by clang::dataflow::WatchedLiteralsSolver::solve(), and clang::dataflow::WatchedLiteralsSolverImpl::solve().

◆ 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 59 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 55 of file Solver.h.

References Unsatisfiable.

Referenced by clang::dataflow::WatchedLiteralsSolverImpl::solve().


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