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

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 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.


Definition at line 30 of file Solver.h.
◆ Assignment
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.
◆ 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 
◆ 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:
 include/clang/Analysis/FlowSensitive/Solver.h