19#include "llvm/ADT/StringRef.h"
20#include "llvm/Support/ErrorHandling.h"
40 llvm_unreachable(
"Unhandled value kind");
51 llvm_unreachable(
"Booleans can only be assigned true/false");
59 return "Unsatisfiable";
63 llvm_unreachable(
"Unhandled SAT check result status");
69 std::vector<std::pair<Atom, Solver::Result::Assignment>> Sorted = {
70 Solution->begin(), Solution->end()};
72 for (
const auto &Entry : Sorted)
73 OS << Entry.first <<
" = " << Entry.second <<
"\n";
llvm::StringRef debugString(Value::Kind Kind)
Returns a string representation of a value kind.
llvm::raw_ostream & operator<<(llvm::raw_ostream &OS, Atom A)
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.