diff --git a/clang/include/clang/Analysis/FlowSensitive/DebugSupport.h b/clang/include/clang/Analysis/FlowSensitive/DebugSupport.h --- a/clang/include/clang/Analysis/FlowSensitive/DebugSupport.h +++ b/clang/include/clang/Analysis/FlowSensitive/DebugSupport.h @@ -23,6 +23,13 @@ namespace clang { namespace dataflow { + +/// Returns a string representation of a boolean assignment to true or false. +std::string debugString(Solver::Result::Assignment Assignment); + +/// Returns a string representation of the result status of a SAT check. +std::string debugString(Solver::Result::Status Status); + /// Returns a string representation for the boolean value `B`. /// /// Atomic booleans appearing in the boolean value `B` are assigned to labels diff --git a/clang/lib/Analysis/FlowSensitive/DebugSupport.cpp b/clang/lib/Analysis/FlowSensitive/DebugSupport.cpp --- a/clang/lib/Analysis/FlowSensitive/DebugSupport.cpp +++ b/clang/lib/Analysis/FlowSensitive/DebugSupport.cpp @@ -30,6 +30,30 @@ using llvm::fmt_pad; using llvm::formatv; +/// Returns a string representation of a boolean assignment to true or false. +std::string debugString(Solver::Result::Assignment Assignment) { + switch (Assignment) { + case Solver::Result::Assignment::AssignedFalse: + return "False"; + case Solver::Result::Assignment::AssignedTrue: + return "True"; + } + llvm_unreachable("Booleans can only be assigned true/false"); +} + +/// Returns a string representation of the result status of a SAT check. +std::string debugString(Solver::Result::Status Status) { + switch (Status) { + case Solver::Result::Status::Satisfiable: + return "Satisfiable"; + case Solver::Result::Status::Unsatisfiable: + return "Unsatisfiable"; + case Solver::Result::Status::TimedOut: + return "TimedOut"; + } + llvm_unreachable("Unhandled SAT check result status"); +} + namespace { class DebugStringGenerator { @@ -134,30 +158,6 @@ return formatv("{0:$[\n]}", llvm::make_range(Lines.begin(), Lines.end())); } - /// Returns a string representation of a boolean assignment to true or false. - std::string debugString(Solver::Result::Assignment Assignment) { - switch (Assignment) { - case Solver::Result::Assignment::AssignedFalse: - return "False"; - case Solver::Result::Assignment::AssignedTrue: - return "True"; - } - llvm_unreachable("Booleans can only be assigned true/false"); - } - - /// Returns a string representation of the result status of a SAT check. - std::string debugString(Solver::Result::Status Status) { - switch (Status) { - case Solver::Result::Status::Satisfiable: - return "Satisfiable"; - case Solver::Result::Status::Unsatisfiable: - return "Unsatisfiable"; - case Solver::Result::Status::TimedOut: - return "TimedOut"; - } - llvm_unreachable("Unhandled SAT check result status"); - } - /// Returns the name assigned to `Atom`, either user-specified or created by /// default rules (B0, B1, ...). std::string getAtomName(const AtomicBoolValue *Atom) {