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

enum class clang::dataflow::Solver::Result::Status

strong

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.

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

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.

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

---

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

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