19#include "llvm/ADT/StringRef.h" 
   20#include "llvm/Support/ErrorHandling.h" 
   38  llvm_unreachable(
"Unhandled value kind");
 
 
   49  llvm_unreachable(
"Booleans can only be assigned true/false");
 
 
   57    return "Unsatisfiable";
 
   61  llvm_unreachable(
"Unhandled SAT check result status");
 
 
   67    std::vector<std::pair<Atom, Solver::Result::Assignment>> Sorted = {
 
   68        Solution->begin(), Solution->end()};
 
   70    for (
const auto &Entry : Sorted)
 
   71      OS << Entry.first << 
" = " << Entry.second << 
"\n";
 
 
Dataflow Directional Tag Classes.
llvm::StringRef debugString(Value::Kind Kind)
Returns a string representation of a value kind.
llvm::raw_ostream & operator<<(llvm::raw_ostream &OS, Atom A)
The JSON file list parser is used to communicate input to InstallAPI.
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.
Assignment
A boolean value is set to true or false in a truth assignment.
@ TimedOut
Indicates that the solver gave up trying to find a satisfying assignment for a boolean formula.
@ Unsatisfiable
Indicates that there is no satisfying assignment for a boolean formula.
@ Satisfiable
Indicates that there exists a satisfying assignment for a boolean formula.