19 #include "llvm/ADT/DenseMap.h"
20 #include "llvm/ADT/STLExtras.h"
21 #include "llvm/ADT/StringRef.h"
22 #include "llvm/ADT/StringSet.h"
23 #include "llvm/Support/ErrorHandling.h"
24 #include "llvm/Support/FormatAdapters.h"
25 #include "llvm/Support/FormatCommon.h"
26 #include "llvm/Support/FormatVariadic.h"
31 using llvm::AlignStyle;
58 return "Biconditional";
60 llvm_unreachable(
"Unhandled value kind");
70 llvm_unreachable(
"Booleans can only be assigned true/false");
78 return "Unsatisfiable";
82 llvm_unreachable(
"Unhandled SAT check result status");
87 class DebugStringGenerator {
89 explicit DebugStringGenerator(
90 llvm::DenseMap<const AtomicBoolValue *, std::string> AtomNamesArg)
91 : Counter(0), AtomNames(
std::move(AtomNamesArg)) {
93 llvm::StringSet<> Names;
94 for (
auto &N : AtomNames) {
95 assert(Names.insert(N.second).second &&
96 "The same name must not assigned to different atoms");
104 switch (B.getKind()) {
106 S = getAtomName(&cast<AtomicBoolValue>(B));
110 auto &
C = cast<ConjunctionValue>(B);
113 S = formatv(
"(and\n{0}\n{1})", L, R);
117 auto &D = cast<DisjunctionValue>(B);
120 S = formatv(
"(or\n{0}\n{1})", L, R);
124 auto &N = cast<NegationValue>(B);
129 auto &IV = cast<ImplicationValue>(B);
132 S = formatv(
"(=>\n{0}\n{1})", L, R);
136 auto &BV = cast<BiconditionalValue>(B);
139 S = formatv(
"(=\n{0}\n{1})", L, R);
143 llvm_unreachable(
"Unhandled value kind");
146 return formatv(
"{0}", fmt_pad(S,
Indent, 0));
150 std::vector<std::string> ConstraintsStrings;
151 ConstraintsStrings.reserve(Constraints.size());
152 for (BoolValue *Constraint : Constraints) {
153 ConstraintsStrings.push_back(
debugString(*Constraint));
155 llvm::sort(ConstraintsStrings);
168 const Solver::Result &Result) {
180 std::vector<std::string> ConstraintsStrings;
181 ConstraintsStrings.reserve(Constraints.size());
182 for (
auto &Constraint : Constraints) {
183 ConstraintsStrings.push_back(
debugString(*Constraint));
187 auto Solution = Result.getSolution();
188 auto SolutionString = Solution ?
"\n" +
debugString(*Solution) :
"";
192 llvm::make_range(ConstraintsStrings.begin(), ConstraintsStrings.end()),
193 StatusString, SolutionString);
199 const llvm::DenseMap<AtomicBoolValue *, Solver::Result::Assignment>
201 size_t MaxNameLength = 0;
202 for (
auto &AtomName : AtomNames) {
203 MaxNameLength =
std::max(MaxNameLength, AtomName.second.size());
206 std::vector<std::string> Lines;
207 for (
auto &AtomAssignment : AtomAssignments) {
208 auto Line = formatv(
"{0} = {1}",
209 fmt_align(getAtomName(AtomAssignment.first),
210 AlignStyle::Left, MaxNameLength),
212 Lines.push_back(
Line);
216 return formatv(
"{0:$[\n]}", llvm::make_range(Lines.begin(), Lines.end()));
221 std::string getAtomName(
const AtomicBoolValue *Atom) {
222 auto Entry = AtomNames.try_emplace(Atom, formatv(
"B{0}", Counter));
226 return Entry.first->second;
234 llvm::DenseMap<const AtomicBoolValue *, std::string> AtomNames;
241 llvm::DenseMap<const AtomicBoolValue *, std::string> AtomNames) {
242 return DebugStringGenerator(std::move(AtomNames)).debugString(B);
247 llvm::DenseMap<const AtomicBoolValue *, std::string> AtomNames) {
248 return DebugStringGenerator(std::move(AtomNames)).debugString(Constraints);
253 llvm::DenseMap<const AtomicBoolValue *, std::string> AtomNames) {
254 return DebugStringGenerator(std::move(AtomNames))
255 .debugString(Constraints, Result);