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";
enum clang::sema::@1655::IndirectLocalPathEntry::EntryKind Kind
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.