clang 18.0.0git

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

strong 

strong 

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

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

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.

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

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