diff --git a/clang/include/clang/Analysis/FlowSensitive/Arena.h b/clang/include/clang/Analysis/FlowSensitive/Arena.h
index 83b4ddeec0256..b6c62e7624625 100644
--- a/clang/include/clang/Analysis/FlowSensitive/Arena.h
+++ b/clang/include/clang/Analysis/FlowSensitive/Arena.h
@@ -8,6 +8,7 @@
 #ifndef LLVM_CLANG_ANALYSIS_FLOWSENSITIVE__ARENA_H
 #define LLVM_CLANG_ANALYSIS_FLOWSENSITIVE__ARENA_H
 
+#include "clang/Analysis/FlowSensitive/Formula.h"
 #include "clang/Analysis/FlowSensitive/StorageLocation.h"
 #include "clang/Analysis/FlowSensitive/Value.h"
 #include <vector>
@@ -104,7 +105,17 @@ class Arena {
     return create<AtomicBoolValue>();
   }
 
+  /// Gets the boolean formula equivalent of a BoolValue.
+  /// Each unique Top values is translated to an Atom.
+  /// TODO: migrate to storing Formula directly in Values instead.
+  const Formula &getFormula(const BoolValue &);
+
+  /// Returns a new atomic boolean variable, distinct from any other.
+  Atom makeAtom() { return static_cast<Atom>(NextAtom++); };
+
 private:
+  llvm::BumpPtrAllocator Alloc;
+
   // Storage for the state of a program.
   std::vector<std::unique_ptr<StorageLocation>> Locs;
   std::vector<std::unique_ptr<Value>> Vals;
@@ -122,6 +133,9 @@ class Arena {
   llvm::DenseMap<std::pair<BoolValue *, BoolValue *>, BiconditionalValue *>
       BiconditionalVals;
 
+  llvm::DenseMap<const BoolValue *, const Formula *> ValToFormula;
+  unsigned NextAtom = 0;
+
   AtomicBoolValue &TrueVal;
   AtomicBoolValue &FalseVal;
 };
diff --git a/clang/include/clang/Analysis/FlowSensitive/DebugSupport.h b/clang/include/clang/Analysis/FlowSensitive/DebugSupport.h
index 360786b02729f..6b9f3681490af 100644
--- a/clang/include/clang/Analysis/FlowSensitive/DebugSupport.h
+++ b/clang/include/clang/Analysis/FlowSensitive/DebugSupport.h
@@ -19,7 +19,6 @@
 
 #include "clang/Analysis/FlowSensitive/Solver.h"
 #include "clang/Analysis/FlowSensitive/Value.h"
-#include "llvm/ADT/DenseMap.h"
 #include "llvm/ADT/StringRef.h"
 
 namespace clang {
@@ -28,52 +27,9 @@ namespace dataflow {
 /// Returns a string representation of a value kind.
 llvm::StringRef debugString(Value::Kind Kind);
 
-/// Returns a string representation of a boolean assignment to true or false.
-llvm::StringRef debugString(Solver::Result::Assignment Assignment);
-
 /// Returns a string representation of the result status of a SAT check.
 llvm::StringRef 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
-/// either specified in `AtomNames` or created by default rules as B0, B1, ...
-///
-/// Requirements:
-///
-///   Names assigned to atoms should not be repeated in `AtomNames`.
-std::string debugString(
-    const BoolValue &B,
-    llvm::DenseMap<const AtomicBoolValue *, std::string> AtomNames = {{}});
-
-/// Returns a string representation for `Constraints` - a collection of boolean
-/// formulas.
-///
-/// Atomic booleans appearing in the boolean value `Constraints` are assigned to
-/// labels either specified in `AtomNames` or created by default rules as B0,
-/// B1, ...
-///
-/// Requirements:
-///
-///   Names assigned to atoms should not be repeated in `AtomNames`.
-std::string debugString(
-    const llvm::ArrayRef<BoolValue *> Constraints,
-    llvm::DenseMap<const AtomicBoolValue *, std::string> AtomNames = {{}});
-
-/// Returns a string representation for `Constraints` - a collection of boolean
-/// formulas and the `Result` of satisfiability checking.
-///
-/// Atomic booleans appearing in `Constraints` and `Result` are assigned to
-/// labels either specified in `AtomNames` or created by default rules as B0,
-/// B1, ...
-///
-/// Requirements:
-///
-///   Names assigned to atoms should not be repeated in `AtomNames`.
-std::string debugString(
-    ArrayRef<BoolValue *> Constraints, const Solver::Result &Result,
-    llvm::DenseMap<const AtomicBoolValue *, std::string> AtomNames = {{}});
-
 } // namespace dataflow
 } // namespace clang
 
diff --git a/clang/include/clang/Analysis/FlowSensitive/Formula.h b/clang/include/clang/Analysis/FlowSensitive/Formula.h
new file mode 100644
index 0000000000000..0c7b1ecd02b17
--- /dev/null
+++ b/clang/include/clang/Analysis/FlowSensitive/Formula.h
@@ -0,0 +1,137 @@
+//===- Formula.h - Boolean formulas -----------------------------*- C++ -*-===//
+//
+// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
+// See https://llvm.org/LICENSE.txt for license information.
+// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+//
+//===----------------------------------------------------------------------===//
+
+#ifndef LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_FORMULA_H
+#define LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_FORMULA_H
+
+#include "clang/Basic/LLVM.h"
+#include "llvm/ADT/ArrayRef.h"
+#include "llvm/ADT/DenseMap.h"
+#include "llvm/ADT/DenseMapInfo.h"
+#include "llvm/ADT/STLFunctionalExtras.h"
+#include "llvm/Support/Allocator.h"
+#include "llvm/Support/raw_ostream.h"
+#include <cassert>
+#include <string>
+#include <type_traits>
+
+namespace clang::dataflow {
+
+/// Identifies an atomic boolean variable such as "V1".
+///
+/// This often represents an assertion that is interesting to the analysis but
+/// cannot immediately be proven true or false. For example:
+/// - V1 may mean "the program reaches this point",
+/// - V2 may mean "the parameter was null"
+///
+/// We can use these variables in formulas to describe relationships we know
+/// to be true: "if the parameter was null, the program reaches this point".
+/// We also express hypotheses as formulas, and use a SAT solver to check
+/// whether they are consistent with the known facts.
+enum class Atom : unsigned {};
+
+/// A boolean expression such as "true" or "V1 & !V2".
+/// Expressions may refer to boolean atomic variables. These should take a
+/// consistent true/false value across the set of formulas being considered.
+///
+/// (Formulas are always expressions in terms of boolean variables rather than
+/// e.g. integers because our underlying model is SAT rather than e.g. SMT).
+///
+/// Simple formulas such as "true" and "V1" are self-contained.
+/// Compound formulas connect other formulas, e.g. "(V1 & V2) || V3" is an 'or'
+/// formula, with pointers to its operands "(V1 & V2)" and "V3" stored as
+/// trailing objects.
+/// For this reason, Formulas are Arena-allocated and over-aligned.
+class Formula;
+class alignas(const Formula *) Formula {
+public:
+  enum Kind : unsigned {
+    /// A reference to an atomic boolean variable.
+    /// We name these e.g. "V3", where 3 == atom identity == Value.
+    AtomRef,
+    // FIXME: add const true/false rather than modeling them as variables
+
+    Not, /// True if its only operand is false
+
+    // These kinds connect two operands LHS and RHS
+    And,     /// True if LHS and RHS are both true
+    Or,      /// True if either LHS or RHS is true
+    Implies, /// True if LHS is false or RHS is true
+    Equal,   /// True if LHS and RHS have the same truth value
+  };
+  Kind kind() const { return FormulaKind; }
+
+  Atom getAtom() const {
+    assert(kind() == AtomRef);
+    return static_cast<Atom>(Value);
+  }
+
+  ArrayRef<const Formula *> operands() const {
+    return ArrayRef(reinterpret_cast<Formula *const *>(this + 1),
+                    numOperands(kind()));
+  }
+
+  using AtomNames = llvm::DenseMap<Atom, std::string>;
+  // Produce a stable human-readable representation of this formula.
+  // For example: (V3 | !(V1 & V2))
+  // If AtomNames is provided, these override the default V0, V1... names.
+  void print(llvm::raw_ostream &OS, const AtomNames * = nullptr) const;
+
+  // Allocate Formulas using Arena rather than calling this function directly.
+  static Formula &create(llvm::BumpPtrAllocator &Alloc, Kind K,
+                         ArrayRef<const Formula *> Operands,
+                         unsigned Value = 0);
+
+private:
+  Formula() = default;
+  Formula(const Formula &) = delete;
+  Formula &operator=(const Formula &) = delete;
+
+  static unsigned numOperands(Kind K) {
+    switch (K) {
+    case AtomRef:
+      return 0;
+    case Not:
+      return 1;
+    case And:
+    case Or:
+    case Implies:
+    case Equal:
+      return 2;
+    }
+  }
+
+  Kind FormulaKind;
+  // Some kinds of formula have scalar values, e.g. AtomRef's atom number.
+  unsigned Value;
+};
+
+// The default names of atoms are V0, V1 etc in order of creation.
+inline llvm::raw_ostream &operator<<(llvm::raw_ostream &OS, Atom A) {
+  return OS << 'V' << static_cast<unsigned>(A);
+}
+inline llvm::raw_ostream &operator<<(llvm::raw_ostream &OS, const Formula &F) {
+  F.print(OS);
+  return OS;
+}
+
+} // namespace clang::dataflow
+namespace llvm {
+template <> struct DenseMapInfo<clang::dataflow::Atom> {
+  using Atom = clang::dataflow::Atom;
+  using Underlying = std::underlying_type_t<Atom>;
+
+  static inline Atom getEmptyKey() { return Atom(Underlying(-1)); }
+  static inline Atom getTombstoneKey() { return Atom(Underlying(-2)); }
+  static unsigned getHashValue(const Atom &Val) {
+    return DenseMapInfo<Underlying>::getHashValue(Underlying(Val));
+  }
+  static bool isEqual(const Atom &LHS, const Atom &RHS) { return LHS == RHS; }
+};
+} // namespace llvm
+#endif
diff --git a/clang/include/clang/Analysis/FlowSensitive/Solver.h b/clang/include/clang/Analysis/FlowSensitive/Solver.h
index 10964eab8c34c..079f6802f241e 100644
--- a/clang/include/clang/Analysis/FlowSensitive/Solver.h
+++ b/clang/include/clang/Analysis/FlowSensitive/Solver.h
@@ -14,12 +14,10 @@
 #ifndef LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_SOLVER_H
 #define LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_SOLVER_H
 
-#include "clang/Analysis/FlowSensitive/Value.h"
+#include "clang/Analysis/FlowSensitive/Formula.h"
 #include "clang/Basic/LLVM.h"
 #include "llvm/ADT/ArrayRef.h"
 #include "llvm/ADT/DenseMap.h"
-#include "llvm/ADT/DenseSet.h"
-#include "llvm/Support/Compiler.h"
 #include <optional>
 #include <vector>
 
@@ -49,8 +47,7 @@ class Solver {
 
     /// Constructs a result indicating that the queried boolean formula is
     /// satisfiable. The result will hold a solution found by the solver.
-    static Result
-    Satisfiable(llvm::DenseMap<AtomicBoolValue *, Assignment> Solution) {
+    static Result Satisfiable(llvm::DenseMap<Atom, Assignment> Solution) {
       return Result(Status::Satisfiable, std::move(Solution));
     }
 
@@ -68,19 +65,17 @@ class Solver {
 
     /// Returns a truth assignment to boolean values that satisfies the queried
     /// boolean formula if available. Otherwise, an empty optional is returned.
-    std::optional<llvm::DenseMap<AtomicBoolValue *, Assignment>>
-    getSolution() const {
+    std::optional<llvm::DenseMap<Atom, Assignment>> getSolution() const {
       return Solution;
     }
 
   private:
-    Result(
-        enum Status SATCheckStatus,
-        std::optional<llvm::DenseMap<AtomicBoolValue *, Assignment>> Solution)
+    Result(Status SATCheckStatus,
+           std::optional<llvm::DenseMap<Atom, Assignment>> Solution)
         : SATCheckStatus(SATCheckStatus), Solution(std::move(Solution)) {}
 
     Status SATCheckStatus;
-    std::optional<llvm::DenseMap<AtomicBoolValue *, Assignment>> Solution;
+    std::optional<llvm::DenseMap<Atom, Assignment>> Solution;
   };
 
   virtual ~Solver() = default;
@@ -91,14 +86,12 @@ class Solver {
   /// Requirements:
   ///
   ///  All elements in `Vals` must not be null.
-  virtual Result solve(llvm::ArrayRef<BoolValue *> Vals) = 0;
-
-  LLVM_DEPRECATED("Pass ArrayRef for determinism", "")
-  virtual Result solve(llvm::DenseSet<BoolValue *> Vals) {
-    return solve(ArrayRef(std::vector<BoolValue *>(Vals.begin(), Vals.end())));
-  }
+  virtual Result solve(llvm::ArrayRef<const Formula *> Vals) = 0;
 };
 
+llvm::raw_ostream &operator<<(llvm::raw_ostream &, const Solver::Result &);
+llvm::raw_ostream &operator<<(llvm::raw_ostream &, Solver::Result::Assignment);
+
 } // namespace dataflow
 } // namespace clang
 
diff --git a/clang/include/clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h b/clang/include/clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h
index b69cc01542c55..a0cdce93c9d47 100644
--- a/clang/include/clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h
+++ b/clang/include/clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h
@@ -14,8 +14,8 @@
 #ifndef LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_WATCHEDLITERALSSOLVER_H
 #define LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_WATCHEDLITERALSSOLVER_H
 
+#include "clang/Analysis/FlowSensitive/Formula.h"
 #include "clang/Analysis/FlowSensitive/Solver.h"
-#include "clang/Analysis/FlowSensitive/Value.h"
 #include "llvm/ADT/ArrayRef.h"
 #include <limits>
 
@@ -46,7 +46,7 @@ class WatchedLiteralsSolver : public Solver {
   explicit WatchedLiteralsSolver(std::int64_t WorkLimit)
       : MaxIterations(WorkLimit) {}
 
-  Result solve(llvm::ArrayRef<BoolValue *> Vals) override;
+  Result solve(llvm::ArrayRef<const Formula *> Vals) override;
 };
 
 } // namespace dataflow
diff --git a/clang/lib/Analysis/FlowSensitive/Arena.cpp b/clang/lib/Analysis/FlowSensitive/Arena.cpp
index cff6c45e18542..e576affc6a41b 100644
--- a/clang/lib/Analysis/FlowSensitive/Arena.cpp
+++ b/clang/lib/Analysis/FlowSensitive/Arena.cpp
@@ -76,4 +76,50 @@ IntegerValue &Arena::makeIntLiteral(llvm::APInt Value) {
   return *It->second;
 }
 
+const Formula &Arena::getFormula(const BoolValue &B) {
+  auto It = ValToFormula.find(&B);
+  if (It != ValToFormula.end())
+    return *It->second;
+  Formula &F = [&]() -> Formula & {
+    switch (B.getKind()) {
+    case Value::Kind::Integer:
+    case Value::Kind::Reference:
+    case Value::Kind::Pointer:
+    case Value::Kind::Struct:
+      llvm_unreachable("not a boolean");
+    case Value::Kind::TopBool:
+    case Value::Kind::AtomicBool:
+      // TODO: assign atom numbers on creation rather than in getFormula(), so
+      // they will be deterministic and maybe even meaningful.
+      return Formula::create(Alloc, Formula::AtomRef, {},
+                             static_cast<unsigned>(makeAtom()));
+    case Value::Kind::Conjunction:
+      return Formula::create(
+          Alloc, Formula::And,
+          {&getFormula(cast<ConjunctionValue>(B).getLeftSubValue()),
+           &getFormula(cast<ConjunctionValue>(B).getRightSubValue())});
+    case Value::Kind::Disjunction:
+      return Formula::create(
+          Alloc, Formula::Or,
+          {&getFormula(cast<DisjunctionValue>(B).getLeftSubValue()),
+           &getFormula(cast<DisjunctionValue>(B).getRightSubValue())});
+    case Value::Kind::Negation:
+      return Formula::create(Alloc, Formula::Not,
+                             {&getFormula(cast<NegationValue>(B).getSubVal())});
+    case Value::Kind::Implication:
+      return Formula::create(
+          Alloc, Formula::Implies,
+          {&getFormula(cast<ImplicationValue>(B).getLeftSubValue()),
+           &getFormula(cast<ImplicationValue>(B).getRightSubValue())});
+    case Value::Kind::Biconditional:
+      return Formula::create(
+          Alloc, Formula::Equal,
+          {&getFormula(cast<BiconditionalValue>(B).getLeftSubValue()),
+           &getFormula(cast<BiconditionalValue>(B).getRightSubValue())});
+    }
+  }();
+  ValToFormula.try_emplace(&B, &F);
+  return F;
+}
+
 } // namespace clang::dataflow
diff --git a/clang/lib/Analysis/FlowSensitive/CMakeLists.txt b/clang/lib/Analysis/FlowSensitive/CMakeLists.txt
index d59bebf6a5a12..171884afe8f4b 100644
--- a/clang/lib/Analysis/FlowSensitive/CMakeLists.txt
+++ b/clang/lib/Analysis/FlowSensitive/CMakeLists.txt
@@ -3,6 +3,7 @@ add_clang_library(clangAnalysisFlowSensitive
   ControlFlowContext.cpp
   DataflowAnalysisContext.cpp
   DataflowEnvironment.cpp
+  Formula.cpp
   HTMLLogger.cpp
   Logger.cpp
   RecordOps.cpp
diff --git a/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp b/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
index 37bcc8be95879..42cc6d4c3d143 100644
--- a/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
+++ b/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
@@ -15,6 +15,7 @@
 #include "clang/Analysis/FlowSensitive/DataflowAnalysisContext.h"
 #include "clang/AST/ExprCXX.h"
 #include "clang/Analysis/FlowSensitive/DebugSupport.h"
+#include "clang/Analysis/FlowSensitive/Formula.h"
 #include "clang/Analysis/FlowSensitive/Logger.h"
 #include "clang/Analysis/FlowSensitive/Value.h"
 #include "llvm/ADT/SetOperations.h"
@@ -23,9 +24,12 @@
 #include "llvm/Support/Debug.h"
 #include "llvm/Support/FileSystem.h"
 #include "llvm/Support/Path.h"
+#include "llvm/Support/raw_ostream.h"
 #include <cassert>
 #include <memory>
+#include <string>
 #include <utility>
+#include <vector>
 
 static llvm::cl::opt<std::string> DataflowLog(
     "dataflow-log", llvm::cl::Hidden, llvm::cl::ValueOptional,
@@ -129,7 +133,10 @@ Solver::Result
 DataflowAnalysisContext::querySolver(llvm::SetVector<BoolValue *> Constraints) {
   Constraints.insert(&arena().makeLiteral(true));
   Constraints.insert(&arena().makeNot(arena().makeLiteral(false)));
-  return S->solve(Constraints.getArrayRef());
+  std::vector<const Formula *> Formulas;
+  for (const BoolValue *Constraint : Constraints)
+    Formulas.push_back(&arena().getFormula(*Constraint));
+  return S->solve(Formulas);
 }
 
 bool DataflowAnalysisContext::flowConditionImplies(AtomicBoolValue &Token,
@@ -191,15 +198,21 @@ void DataflowAnalysisContext::addTransitiveFlowConditionConstraints(
 
 void DataflowAnalysisContext::dumpFlowCondition(AtomicBoolValue &Token,
                                                 llvm::raw_ostream &OS) {
+  // TODO: accumulate formulas directly instead
   llvm::SetVector<BoolValue *> Constraints;
   Constraints.insert(&Token);
   llvm::DenseSet<AtomicBoolValue *> VisitedTokens;
   addTransitiveFlowConditionConstraints(Token, Constraints, VisitedTokens);
 
-  llvm::DenseMap<const AtomicBoolValue *, std::string> AtomNames = {
-      {&arena().makeLiteral(false), "False"},
-      {&arena().makeLiteral(true), "True"}};
-  OS << debugString(Constraints.getArrayRef(), AtomNames);
+  // TODO: have formulas know about true/false directly instead
+  Atom True = arena().getFormula(arena().makeLiteral(true)).getAtom();
+  Atom False = arena().getFormula(arena().makeLiteral(false)).getAtom();
+  Formula::AtomNames Names = {{False, "false"}, {True, "true"}};
+
+  for (const auto *Constraint : Constraints) {
+    arena().getFormula(*Constraint).print(OS, &Names);
+    OS << "\n";
+  }
 }
 
 const ControlFlowContext *
diff --git a/clang/lib/Analysis/FlowSensitive/DebugSupport.cpp b/clang/lib/Analysis/FlowSensitive/DebugSupport.cpp
index 25225ed6266fb..34e53249ba4d8 100644
--- a/clang/lib/Analysis/FlowSensitive/DebugSupport.cpp
+++ b/clang/lib/Analysis/FlowSensitive/DebugSupport.cpp
@@ -16,22 +16,12 @@
 #include "clang/Analysis/FlowSensitive/DebugSupport.h"
 #include "clang/Analysis/FlowSensitive/Solver.h"
 #include "clang/Analysis/FlowSensitive/Value.h"
-#include "llvm/ADT/DenseMap.h"
-#include "llvm/ADT/STLExtras.h"
 #include "llvm/ADT/StringRef.h"
-#include "llvm/ADT/StringSet.h"
 #include "llvm/Support/ErrorHandling.h"
-#include "llvm/Support/FormatAdapters.h"
-#include "llvm/Support/FormatCommon.h"
-#include "llvm/Support/FormatVariadic.h"
 
 namespace clang {
 namespace dataflow {
 
-using llvm::AlignStyle;
-using llvm::fmt_pad;
-using llvm::formatv;
-
 llvm::StringRef debugString(Value::Kind Kind) {
   switch (Kind) {
   case Value::Kind::Integer:
@@ -60,12 +50,13 @@ llvm::StringRef debugString(Value::Kind Kind) {
   llvm_unreachable("Unhandled value kind");
 }
 
-llvm::StringRef debugString(Solver::Result::Assignment Assignment) {
+llvm::raw_ostream &operator<<(llvm::raw_ostream &OS,
+                              Solver::Result::Assignment Assignment) {
   switch (Assignment) {
   case Solver::Result::Assignment::AssignedFalse:
-    return "False";
+    return OS << "False";
   case Solver::Result::Assignment::AssignedTrue:
-    return "True";
+    return OS << "True";
   }
   llvm_unreachable("Booleans can only be assigned true/false");
 }
@@ -82,174 +73,16 @@ llvm::StringRef debugString(Solver::Result::Status Status) {
   llvm_unreachable("Unhandled SAT check result status");
 }
 
-namespace {
-
-class DebugStringGenerator {
-public:
-  explicit DebugStringGenerator(
-      llvm::DenseMap<const AtomicBoolValue *, std::string> AtomNamesArg)
-      : Counter(0), AtomNames(std::move(AtomNamesArg)) {
-#ifndef NDEBUG
-    llvm::StringSet<> Names;
-    for (auto &N : AtomNames) {
-      assert(Names.insert(N.second).second &&
-             "The same name must not assigned to different atoms");
-    }
-#endif
-  }
-
-  /// Returns a string representation of a boolean value `B`.
-  std::string debugString(const BoolValue &B, size_t Depth = 0) {
-    std::string S;
-    switch (B.getKind()) {
-    case Value::Kind::AtomicBool: {
-      S = getAtomName(&cast<AtomicBoolValue>(B));
-      break;
-    }
-    case Value::Kind::TopBool: {
-      S = "top";
-      break;
-    }
-    case Value::Kind::Conjunction: {
-      auto &C = cast<ConjunctionValue>(B);
-      auto L = debugString(C.getLeftSubValue(), Depth + 1);
-      auto R = debugString(C.getRightSubValue(), Depth + 1);
-      S = formatv("(and\n{0}\n{1})", L, R);
-      break;
-    }
-    case Value::Kind::Disjunction: {
-      auto &D = cast<DisjunctionValue>(B);
-      auto L = debugString(D.getLeftSubValue(), Depth + 1);
-      auto R = debugString(D.getRightSubValue(), Depth + 1);
-      S = formatv("(or\n{0}\n{1})", L, R);
-      break;
-    }
-    case Value::Kind::Negation: {
-      auto &N = cast<NegationValue>(B);
-      S = formatv("(not\n{0})", debugString(N.getSubVal(), Depth + 1));
-      break;
-    }
-    case Value::Kind::Implication: {
-      auto &IV = cast<ImplicationValue>(B);
-      auto L = debugString(IV.getLeftSubValue(), Depth + 1);
-      auto R = debugString(IV.getRightSubValue(), Depth + 1);
-      S = formatv("(=>\n{0}\n{1})", L, R);
-      break;
-    }
-    case Value::Kind::Biconditional: {
-      auto &BV = cast<BiconditionalValue>(B);
-      auto L = debugString(BV.getLeftSubValue(), Depth + 1);
-      auto R = debugString(BV.getRightSubValue(), Depth + 1);
-      S = formatv("(=\n{0}\n{1})", L, R);
-      break;
-    }
-    default:
-      llvm_unreachable("Unhandled value kind");
-    }
-    auto Indent = Depth * 4;
-    return formatv("{0}", fmt_pad(S, Indent, 0));
-  }
-
-  std::string debugString(const llvm::ArrayRef<BoolValue *> &Constraints) {
-    std::string Result;
-    for (const BoolValue *S : Constraints) {
-      Result += debugString(*S);
-      Result += '\n';
-    }
-    return Result;
-  }
-
-  /// Returns a string representation of a set of boolean `Constraints` and the
-  /// `Result` of satisfiability checking on the `Constraints`.
-  std::string debugString(ArrayRef<BoolValue *> &Constraints,
-                          const Solver::Result &Result) {
-    auto Template = R"(
-Constraints
-------------
-{0:$[
-
-]}
-------------
-{1}.
-{2}
-)";
-
-    std::vector<std::string> ConstraintsStrings;
-    ConstraintsStrings.reserve(Constraints.size());
-    for (auto &Constraint : Constraints) {
-      ConstraintsStrings.push_back(debugString(*Constraint));
-    }
-
-    auto StatusString = clang::dataflow::debugString(Result.getStatus());
-    auto Solution = Result.getSolution();
-    auto SolutionString = Solution ? "\n" + debugString(*Solution) : "";
-
-    return formatv(
-        Template,
-        llvm::make_range(ConstraintsStrings.begin(), ConstraintsStrings.end()),
-        StatusString, SolutionString);
-  }
-
-private:
-  /// Returns a string representation of a truth assignment to atom booleans.
-  std::string debugString(
-      const llvm::DenseMap<AtomicBoolValue *, Solver::Result::Assignment>
-          &AtomAssignments) {
-    size_t MaxNameLength = 0;
-    for (auto &AtomName : AtomNames) {
-      MaxNameLength = std::max(MaxNameLength, AtomName.second.size());
-    }
-
-    std::vector<std::string> Lines;
-    for (auto &AtomAssignment : AtomAssignments) {
-      auto Line = formatv("{0} = {1}",
-                          fmt_align(getAtomName(AtomAssignment.first),
-                                    AlignStyle::Left, MaxNameLength),
-                          clang::dataflow::debugString(AtomAssignment.second));
-      Lines.push_back(Line);
-    }
-    llvm::sort(Lines);
-
-    return formatv("{0:$[\n]}", llvm::make_range(Lines.begin(), Lines.end()));
+llvm::raw_ostream &operator<<(llvm::raw_ostream &OS, const Solver::Result &R) {
+  OS << debugString(R.getStatus()) << "\n";
+  if (auto Solution = R.getSolution()) {
+    std::vector<std::pair<Atom, Solver::Result::Assignment>> Sorted = {
+        Solution->begin(), Solution->end()};
+    llvm::sort(Sorted);
+    for (const auto &Entry : Sorted)
+      OS << Entry.first << " = " << Entry.second << "\n";
   }
-
-  /// Returns the name assigned to `Atom`, either user-specified or created by
-  /// default rules (B0, B1, ...).
-  std::string getAtomName(const AtomicBoolValue *Atom) {
-    auto Entry = AtomNames.try_emplace(Atom, formatv("B{0}", Counter));
-    if (Entry.second) {
-      Counter++;
-    }
-    return Entry.first->second;
-  }
-
-  // Keep track of number of atoms without a user-specified name, used to assign
-  // non-repeating default names to such atoms.
-  size_t Counter;
-
-  // Keep track of names assigned to atoms.
-  llvm::DenseMap<const AtomicBoolValue *, std::string> AtomNames;
-};
-
-} // namespace
-
-std::string
-debugString(const BoolValue &B,
-            llvm::DenseMap<const AtomicBoolValue *, std::string> AtomNames) {
-  return DebugStringGenerator(std::move(AtomNames)).debugString(B);
-}
-
-std::string
-debugString(llvm::ArrayRef<BoolValue *> Constraints,
-            llvm::DenseMap<const AtomicBoolValue *, std::string> AtomNames) {
-  return DebugStringGenerator(std::move(AtomNames)).debugString(Constraints);
-}
-
-std::string
-debugString(ArrayRef<BoolValue *> Constraints, const Solver::Result &Result,
-            llvm::DenseMap<const AtomicBoolValue *, std::string> AtomNames) {
-  return DebugStringGenerator(std::move(AtomNames))
-      .debugString(Constraints, Result);
+  return OS;
 }
 
 } // namespace dataflow
diff --git a/clang/lib/Analysis/FlowSensitive/Formula.cpp b/clang/lib/Analysis/FlowSensitive/Formula.cpp
new file mode 100644
index 0000000000000..504ad2fb7938a
--- /dev/null
+++ b/clang/lib/Analysis/FlowSensitive/Formula.cpp
@@ -0,0 +1,82 @@
+//===- Formula.cpp ----------------------------------------------*- C++ -*-===//
+//
+// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
+// See https://llvm.org/LICENSE.txt for license information.
+// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+//
+//===----------------------------------------------------------------------===//
+
+#include "clang/Analysis/FlowSensitive/Formula.h"
+#include "clang/Basic/LLVM.h"
+#include "llvm/ADT/STLExtras.h"
+#include "llvm/ADT/StringRef.h"
+#include "llvm/Support/Allocator.h"
+#include "llvm/Support/ErrorHandling.h"
+#include <cassert>
+
+namespace clang::dataflow {
+
+Formula &Formula::create(llvm::BumpPtrAllocator &Alloc, Kind K,
+                         ArrayRef<const Formula *> Operands, unsigned Value) {
+  assert(Operands.size() == numOperands(K));
+  if (Value != 0) // Currently, formulas have values or operands, not both.
+    assert(numOperands(K) == 0);
+  void *Mem = Alloc.Allocate(sizeof(Formula) +
+                                 Operands.size() * sizeof(Operands.front()),
+                             alignof(Formula));
+  Formula *Result = new (Mem) Formula();
+  Result->FormulaKind = K;
+  Result->Value = Value;
+  // Operands are stored as `const Formula *`s after the formula itself.
+  // We don't need to construct an object as pointers are trivial types.
+  // Formula is alignas(const Formula *), so alignment is satisfied.
+  llvm::copy(Operands, reinterpret_cast<const Formula **>(Result + 1));
+  return *Result;
+}
+
+static llvm::StringLiteral sigil(Formula::Kind K) {
+  switch (K) {
+  case Formula::AtomRef:
+    return "";
+  case Formula::Not:
+    return "!";
+  case Formula::And:
+    return " & ";
+  case Formula::Or:
+    return " | ";
+  case Formula::Implies:
+    return " => ";
+  case Formula::Equal:
+    return " = ";
+  }
+  llvm_unreachable("unhandled formula kind");
+}
+
+void Formula::print(llvm::raw_ostream &OS, const AtomNames *Names) const {
+  if (Names && kind() == AtomRef)
+    if (auto It = Names->find(getAtom()); It != Names->end()) {
+      OS << It->second;
+      return;
+    }
+
+  switch (numOperands(kind())) {
+  case 0:
+    OS << getAtom();
+    break;
+  case 1:
+    OS << sigil(kind());
+    operands()[0]->print(OS, Names);
+    break;
+  case 2:
+    OS << '(';
+    operands()[0]->print(OS, Names);
+    OS << sigil(kind());
+    operands()[1]->print(OS, Names);
+    OS << ')';
+    break;
+  default:
+    llvm_unreachable("unhandled formula arity");
+  }
+}
+
+} // namespace clang::dataflow
\ No newline at end of file
diff --git a/clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp b/clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp
index db2e1d694457b..037886d09c4f7 100644
--- a/clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp
+++ b/clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp
@@ -17,8 +17,8 @@
 #include <queue>
 #include <vector>
 
+#include "clang/Analysis/FlowSensitive/Formula.h"
 #include "clang/Analysis/FlowSensitive/Solver.h"
-#include "clang/Analysis/FlowSensitive/Value.h"
 #include "clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h"
 #include "llvm/ADT/ArrayRef.h"
 #include "llvm/ADT/DenseMap.h"
@@ -79,7 +79,7 @@ using ClauseID = uint32_t;
 static constexpr ClauseID NullClause = 0;
 
 /// A boolean formula in conjunctive normal form.
-struct BooleanFormula {
+struct CNFFormula {
   /// `LargestVar` is equal to the largest positive integer that represents a
   /// variable in the formula.
   const Variable LargestVar;
@@ -121,12 +121,12 @@ struct BooleanFormula {
   /// clauses in the formula start from the element at index 1.
   std::vector<ClauseID> NextWatched;
 
-  /// Stores the variable identifier and value location for atomic booleans in
-  /// the formula.
-  llvm::DenseMap<Variable, AtomicBoolValue *> Atomics;
+  /// Stores the variable identifier and Atom for atomic booleans in the
+  /// formula.
+  llvm::DenseMap<Variable, Atom> Atomics;
 
-  explicit BooleanFormula(Variable LargestVar,
-                          llvm::DenseMap<Variable, AtomicBoolValue *> Atomics)
+  explicit CNFFormula(Variable LargestVar,
+                      llvm::DenseMap<Variable, Atom> Atomics)
       : LargestVar(LargestVar), Atomics(std::move(Atomics)) {
     Clauses.push_back(0);
     ClauseStarts.push_back(0);
@@ -144,8 +144,8 @@ struct BooleanFormula {
   ///
   ///  All literals in the input that are not `NullLit` must be distinct.
   void addClause(Literal L1, Literal L2 = NullLit, Literal L3 = NullLit) {
-    // The literals are guaranteed to be distinct from properties of BoolValue
-    // and the construction in `buildBooleanFormula`.
+    // The literals are guaranteed to be distinct from properties of Formula
+    // and the construction in `buildCNF`.
     assert(L1 != NullLit && L1 != L2 && L1 != L3 &&
            (L2 != L3 || L2 == NullLit));
 
@@ -178,98 +178,59 @@ struct BooleanFormula {
 
 /// Converts the conjunction of `Vals` into a formula in conjunctive normal
 /// form where each clause has at least one and at most three literals.
-BooleanFormula buildBooleanFormula(const llvm::ArrayRef<BoolValue *> &Vals) {
+CNFFormula buildCNF(const llvm::ArrayRef<const Formula *> &Vals) {
   // The general strategy of the algorithm implemented below is to map each
   // of the sub-values in `Vals` to a unique variable and use these variables in
   // the resulting CNF expression to avoid exponential blow up. The number of
   // literals in the resulting formula is guaranteed to be linear in the number
-  // of sub-values in `Vals`.
+  // of sub-formulas in `Vals`.
 
-  // Map each sub-value in `Vals` to a unique variable.
-  llvm::DenseMap<BoolValue *, Variable> SubValsToVar;
-  // Store variable identifiers and value location of atomic booleans.
-  llvm::DenseMap<Variable, AtomicBoolValue *> Atomics;
+  // Map each sub-formula in `Vals` to a unique variable.
+  llvm::DenseMap<const Formula *, Variable> SubValsToVar;
+  // Store variable identifiers and Atom of atomic booleans.
+  llvm::DenseMap<Variable, Atom> Atomics;
   Variable NextVar = 1;
   {
-    std::queue<BoolValue *> UnprocessedSubVals;
-    for (BoolValue *Val : Vals)
+    std::queue<const Formula *> UnprocessedSubVals;
+    for (const Formula *Val : Vals)
       UnprocessedSubVals.push(Val);
     while (!UnprocessedSubVals.empty()) {
       Variable Var = NextVar;
-      BoolValue *Val = UnprocessedSubVals.front();
+      const Formula *Val = UnprocessedSubVals.front();
       UnprocessedSubVals.pop();
 
       if (!SubValsToVar.try_emplace(Val, Var).second)
         continue;
       ++NextVar;
 
-      // Visit the sub-values of `Val`.
-      switch (Val->getKind()) {
-      case Value::Kind::Conjunction: {
-        auto *C = cast<ConjunctionValue>(Val);
-        UnprocessedSubVals.push(&C->getLeftSubValue());
-        UnprocessedSubVals.push(&C->getRightSubValue());
-        break;
-      }
-      case Value::Kind::Disjunction: {
-        auto *D = cast<DisjunctionValue>(Val);
-        UnprocessedSubVals.push(&D->getLeftSubValue());
-        UnprocessedSubVals.push(&D->getRightSubValue());
-        break;
-      }
-      case Value::Kind::Negation: {
-        auto *N = cast<NegationValue>(Val);
-        UnprocessedSubVals.push(&N->getSubVal());
-        break;
-      }
-      case Value::Kind::Implication: {
-        auto *I = cast<ImplicationValue>(Val);
-        UnprocessedSubVals.push(&I->getLeftSubValue());
-        UnprocessedSubVals.push(&I->getRightSubValue());
-        break;
-      }
-      case Value::Kind::Biconditional: {
-        auto *B = cast<BiconditionalValue>(Val);
-        UnprocessedSubVals.push(&B->getLeftSubValue());
-        UnprocessedSubVals.push(&B->getRightSubValue());
-        break;
-      }
-      case Value::Kind::TopBool:
-        // Nothing more to do. This `TopBool` instance has already been mapped
-        // to a fresh solver variable (`NextVar`, above) and is thereafter
-        // anonymous. The solver never sees `Top`.
-        break;
-      case Value::Kind::AtomicBool: {
-        Atomics[Var] = cast<AtomicBoolValue>(Val);
-        break;
-      }
-      default:
-        llvm_unreachable("buildBooleanFormula: unhandled value kind");
-      }
+      for (const Formula *F : Val->operands())
+        UnprocessedSubVals.push(F);
+      if (Val->kind() == Formula::AtomRef)
+        Atomics[Var] = Val->getAtom();
     }
   }
 
-  auto GetVar = [&SubValsToVar](const BoolValue *Val) {
+  auto GetVar = [&SubValsToVar](const Formula *Val) {
     auto ValIt = SubValsToVar.find(Val);
     assert(ValIt != SubValsToVar.end());
     return ValIt->second;
   };
 
-  BooleanFormula Formula(NextVar - 1, std::move(Atomics));
+  CNFFormula CNF(NextVar - 1, std::move(Atomics));
   std::vector<bool> ProcessedSubVals(NextVar, false);
 
-  // Add a conjunct for each variable that represents a top-level conjunction
-  // value in `Vals`.
-  for (BoolValue *Val : Vals)
-    Formula.addClause(posLit(GetVar(Val)));
+  // Add a conjunct for each variable that represents a top-level formula in
+  // `Vals`.
+  for (const Formula *Val : Vals)
+    CNF.addClause(posLit(GetVar(Val)));
 
   // Add conjuncts that represent the mapping between newly-created variables
-  // and their corresponding sub-values.
-  std::queue<BoolValue *> UnprocessedSubVals;
-  for (BoolValue *Val : Vals)
+  // and their corresponding sub-formulas.
+  std::queue<const Formula *> UnprocessedSubVals;
+  for (const Formula *Val : Vals)
     UnprocessedSubVals.push(Val);
   while (!UnprocessedSubVals.empty()) {
-    const BoolValue *Val = UnprocessedSubVals.front();
+    const Formula *Val = UnprocessedSubVals.front();
     UnprocessedSubVals.pop();
     const Variable Var = GetVar(Val);
 
@@ -277,117 +238,107 @@ BooleanFormula buildBooleanFormula(const llvm::ArrayRef<BoolValue *> &Vals) {
       continue;
     ProcessedSubVals[Var] = true;
 
-    if (auto *C = dyn_cast<ConjunctionValue>(Val)) {
-      const Variable LeftSubVar = GetVar(&C->getLeftSubValue());
-      const Variable RightSubVar = GetVar(&C->getRightSubValue());
+    switch (Val->kind()) {
+    case Formula::AtomRef:
+      break;
+    case Formula::And: {
+      const Variable LHS = GetVar(Val->operands()[0]);
+      const Variable RHS = GetVar(Val->operands()[1]);
 
-      if (LeftSubVar == RightSubVar) {
+      if (LHS == RHS) {
         // `X <=> (A ^ A)` is equivalent to `(!X v A) ^ (X v !A)` which is
         // already in conjunctive normal form. Below we add each of the
         // conjuncts of the latter expression to the result.
-        Formula.addClause(negLit(Var), posLit(LeftSubVar));
-        Formula.addClause(posLit(Var), negLit(LeftSubVar));
-
-        // Visit a sub-value of `Val` (pick any, they are identical).
-        UnprocessedSubVals.push(&C->getLeftSubValue());
+        CNF.addClause(negLit(Var), posLit(LHS));
+        CNF.addClause(posLit(Var), negLit(LHS));
       } else {
         // `X <=> (A ^ B)` is equivalent to `(!X v A) ^ (!X v B) ^ (X v !A v !B)`
         // which is already in conjunctive normal form. Below we add each of the
         // conjuncts of the latter expression to the result.
-        Formula.addClause(negLit(Var), posLit(LeftSubVar));
-        Formula.addClause(negLit(Var), posLit(RightSubVar));
-        Formula.addClause(posLit(Var), negLit(LeftSubVar), negLit(RightSubVar));
-
-        // Visit the sub-values of `Val`.
-        UnprocessedSubVals.push(&C->getLeftSubValue());
-        UnprocessedSubVals.push(&C->getRightSubValue());
+        CNF.addClause(negLit(Var), posLit(LHS));
+        CNF.addClause(negLit(Var), posLit(RHS));
+        CNF.addClause(posLit(Var), negLit(LHS), negLit(RHS));
       }
-    } else if (auto *D = dyn_cast<DisjunctionValue>(Val)) {
-      const Variable LeftSubVar = GetVar(&D->getLeftSubValue());
-      const Variable RightSubVar = GetVar(&D->getRightSubValue());
+      break;
+    }
+    case Formula::Or: {
+      const Variable LHS = GetVar(Val->operands()[0]);
+      const Variable RHS = GetVar(Val->operands()[1]);
 
-      if (LeftSubVar == RightSubVar) {
+      if (LHS == RHS) {
         // `X <=> (A v A)` is equivalent to `(!X v A) ^ (X v !A)` which is
         // already in conjunctive normal form. Below we add each of the
         // conjuncts of the latter expression to the result.
-        Formula.addClause(negLit(Var), posLit(LeftSubVar));
-        Formula.addClause(posLit(Var), negLit(LeftSubVar));
-
-        // Visit a sub-value of `Val` (pick any, they are identical).
-        UnprocessedSubVals.push(&D->getLeftSubValue());
+        CNF.addClause(negLit(Var), posLit(LHS));
+        CNF.addClause(posLit(Var), negLit(LHS));
       } else {
-        // `X <=> (A v B)` is equivalent to `(!X v A v B) ^ (X v !A) ^ (X v !B)`
-        // which is already in conjunctive normal form. Below we add each of the
-        // conjuncts of the latter expression to the result.
-        Formula.addClause(negLit(Var), posLit(LeftSubVar), posLit(RightSubVar));
-        Formula.addClause(posLit(Var), negLit(LeftSubVar));
-        Formula.addClause(posLit(Var), negLit(RightSubVar));
-
-        // Visit the sub-values of `Val`.
-        UnprocessedSubVals.push(&D->getLeftSubValue());
-        UnprocessedSubVals.push(&D->getRightSubValue());
+        // `X <=> (A v B)` is equivalent to `(!X v A v B) ^ (X v !A) ^ (X v
+        // !B)` which is already in conjunctive normal form. Below we add each
+        // of the conjuncts of the latter expression to the result.
+        CNF.addClause(negLit(Var), posLit(LHS), posLit(RHS));
+        CNF.addClause(posLit(Var), negLit(LHS));
+        CNF.addClause(posLit(Var), negLit(RHS));
       }
-    } else if (auto *N = dyn_cast<NegationValue>(Val)) {
-      const Variable SubVar = GetVar(&N->getSubVal());
-
-      // `X <=> !Y` is equivalent to `(!X v !Y) ^ (X v Y)` which is already in
-      // conjunctive normal form. Below we add each of the conjuncts of the
-      // latter expression to the result.
-      Formula.addClause(negLit(Var), negLit(SubVar));
-      Formula.addClause(posLit(Var), posLit(SubVar));
-
-      // Visit the sub-values of `Val`.
-      UnprocessedSubVals.push(&N->getSubVal());
-    } else if (auto *I = dyn_cast<ImplicationValue>(Val)) {
-      const Variable LeftSubVar = GetVar(&I->getLeftSubValue());
-      const Variable RightSubVar = GetVar(&I->getRightSubValue());
+      break;
+    }
+    case Formula::Not: {
+      const Variable Operand = GetVar(Val->operands()[0]);
+
+      // `X <=> !Y` is equivalent to `(!X v !Y) ^ (X v Y)` which is
+      // already in conjunctive normal form. Below we add each of the
+      // conjuncts of the latter expression to the result.
+      CNF.addClause(negLit(Var), negLit(Operand));
+      CNF.addClause(posLit(Var), posLit(Operand));
+      break;
+    }
+    case Formula::Implies: {
+      const Variable LHS = GetVar(Val->operands()[0]);
+      const Variable RHS = GetVar(Val->operands()[1]);
 
       // `X <=> (A => B)` is equivalent to
       // `(X v A) ^ (X v !B) ^ (!X v !A v B)` which is already in
-      // conjunctive normal form. Below we add each of the conjuncts of the
-      // latter expression to the result.
-      Formula.addClause(posLit(Var), posLit(LeftSubVar));
-      Formula.addClause(posLit(Var), negLit(RightSubVar));
-      Formula.addClause(negLit(Var), negLit(LeftSubVar), posLit(RightSubVar));
-
-      // Visit the sub-values of `Val`.
-      UnprocessedSubVals.push(&I->getLeftSubValue());
-      UnprocessedSubVals.push(&I->getRightSubValue());
-    } else if (auto *B = dyn_cast<BiconditionalValue>(Val)) {
-      const Variable LeftSubVar = GetVar(&B->getLeftSubValue());
-      const Variable RightSubVar = GetVar(&B->getRightSubValue());
-
-      if (LeftSubVar == RightSubVar) {
+      // conjunctive normal form. Below we add each of the conjuncts of
+      // the latter expression to the result.
+      CNF.addClause(posLit(Var), posLit(LHS));
+      CNF.addClause(posLit(Var), negLit(RHS));
+      CNF.addClause(negLit(Var), negLit(LHS), posLit(RHS));
+      break;
+    }
+    case Formula::Equal: {
+      const Variable LHS = GetVar(Val->operands()[0]);
+      const Variable RHS = GetVar(Val->operands()[1]);
+
+      if (LHS == RHS) {
         // `X <=> (A <=> A)` is equvalent to `X` which is already in
         // conjunctive normal form. Below we add each of the conjuncts of the
         // latter expression to the result.
-        Formula.addClause(posLit(Var));
+        CNF.addClause(posLit(Var));
 
         // No need to visit the sub-values of `Val`.
-      } else {
-        // `X <=> (A <=> B)` is equivalent to
-        // `(X v A v B) ^ (X v !A v !B) ^ (!X v A v !B) ^ (!X v !A v B)` which is
-        // already in conjunctive normal form. Below we add each of the conjuncts
-        // of the latter expression to the result.
-        Formula.addClause(posLit(Var), posLit(LeftSubVar), posLit(RightSubVar));
-        Formula.addClause(posLit(Var), negLit(LeftSubVar), negLit(RightSubVar));
-        Formula.addClause(negLit(Var), posLit(LeftSubVar), negLit(RightSubVar));
-        Formula.addClause(negLit(Var), negLit(LeftSubVar), posLit(RightSubVar));
-
-        // Visit the sub-values of `Val`.
-        UnprocessedSubVals.push(&B->getLeftSubValue());
-        UnprocessedSubVals.push(&B->getRightSubValue());
+        continue;
       }
+      // `X <=> (A <=> B)` is equivalent to
+      // `(X v A v B) ^ (X v !A v !B) ^ (!X v A v !B) ^ (!X v !A v B)` which
+      // is already in conjunctive normal form. Below we add each of the
+      // conjuncts of the latter expression to the result.
+      CNF.addClause(posLit(Var), posLit(LHS), posLit(RHS));
+      CNF.addClause(posLit(Var), negLit(LHS), negLit(RHS));
+      CNF.addClause(negLit(Var), posLit(LHS), negLit(RHS));
+      CNF.addClause(negLit(Var), negLit(LHS), posLit(RHS));
+      break;
+    }
     }
+    for (const Formula *Child : Val->operands())
+      UnprocessedSubVals.push(Child);
   }
 
-  return Formula;
+  return CNF;
 }
 
 class WatchedLiteralsSolverImpl {
   /// A boolean formula in conjunctive normal form that the solver will attempt
   /// to prove satisfiable. The formula will be modified in the process.
-  BooleanFormula Formula;
+  CNFFormula CNF;
 
   /// The search for a satisfying assignment of the variables in `Formula` will
   /// proceed in levels, starting from 1 and going up to `Formula.LargestVar`
@@ -439,9 +390,10 @@ class WatchedLiteralsSolverImpl {
   std::vector<Variable> ActiveVars;
 
 public:
-  explicit WatchedLiteralsSolverImpl(const llvm::ArrayRef<BoolValue *> &Vals)
-      : Formula(buildBooleanFormula(Vals)), LevelVars(Formula.LargestVar + 1),
-        LevelStates(Formula.LargestVar + 1) {
+  explicit WatchedLiteralsSolverImpl(
+      const llvm::ArrayRef<const Formula *> &Vals)
+      : CNF(buildCNF(Vals)), LevelVars(CNF.LargestVar + 1),
+        LevelStates(CNF.LargestVar + 1) {
     assert(!Vals.empty());
 
     // Initialize the state at the root level to a decision so that in
@@ -450,10 +402,10 @@ class WatchedLiteralsSolverImpl {
     LevelStates[0] = State::Decision;
 
     // Initialize all variables as unassigned.
-    VarAssignments.resize(Formula.LargestVar + 1, Assignment::Unassigned);
+    VarAssignments.resize(CNF.LargestVar + 1, Assignment::Unassigned);
 
     // Initialize the active variables.
-    for (Variable Var = Formula.LargestVar; Var != NullVar; --Var) {
+    for (Variable Var = CNF.LargestVar; Var != NullVar; --Var) {
       if (isWatched(posLit(Var)) || isWatched(negLit(Var)))
         ActiveVars.push_back(Var);
     }
@@ -474,7 +426,7 @@ class WatchedLiteralsSolverImpl {
       // 3. Unassigned variables that form watched literals are active.
       // FIXME: Consider replacing these with test cases that fail if the any
       // of the invariants is broken. That might not be easy due to the
-      // transformations performed by `buildBooleanFormula`.
+      // transformations performed by `buildCNF`.
       assert(activeVarsAreUnassigned());
       assert(activeVarsFormWatchedLiterals());
       assert(unassignedVarsFormingWatchedLiteralsAreActive());
@@ -555,12 +507,10 @@ class WatchedLiteralsSolverImpl {
   }
 
 private:
-  /// Returns a satisfying truth assignment to the atomic values in the boolean
-  /// formula.
-  llvm::DenseMap<AtomicBoolValue *, Solver::Result::Assignment>
-  buildSolution() {
-    llvm::DenseMap<AtomicBoolValue *, Solver::Result::Assignment> Solution;
-    for (auto &Atomic : Formula.Atomics) {
+  /// Returns a satisfying truth assignment to the atoms in the boolean formula.
+  llvm::DenseMap<Atom, Solver::Result::Assignment> buildSolution() {
+    llvm::DenseMap<Atom, Solver::Result::Assignment> Solution;
+    for (auto &Atomic : CNF.Atomics) {
       // A variable may have a definite true/false assignment, or it may be
       // unassigned indicating its truth value does not affect the result of
       // the formula. Unassigned variables are assigned to true as a default.
@@ -596,24 +546,24 @@ class WatchedLiteralsSolverImpl {
     const Literal FalseLit = VarAssignments[Var] == Assignment::AssignedTrue
                                  ? negLit(Var)
                                  : posLit(Var);
-    ClauseID FalseLitWatcher = Formula.WatchedHead[FalseLit];
-    Formula.WatchedHead[FalseLit] = NullClause;
+    ClauseID FalseLitWatcher = CNF.WatchedHead[FalseLit];
+    CNF.WatchedHead[FalseLit] = NullClause;
     while (FalseLitWatcher != NullClause) {
-      const ClauseID NextFalseLitWatcher = Formula.NextWatched[FalseLitWatcher];
+      const ClauseID NextFalseLitWatcher = CNF.NextWatched[FalseLitWatcher];
 
       // Pick the first non-false literal as the new watched literal.
-      const size_t FalseLitWatcherStart = Formula.ClauseStarts[FalseLitWatcher];
+      const size_t FalseLitWatcherStart = CNF.ClauseStarts[FalseLitWatcher];
       size_t NewWatchedLitIdx = FalseLitWatcherStart + 1;
-      while (isCurrentlyFalse(Formula.Clauses[NewWatchedLitIdx]))
+      while (isCurrentlyFalse(CNF.Clauses[NewWatchedLitIdx]))
         ++NewWatchedLitIdx;
-      const Literal NewWatchedLit = Formula.Clauses[NewWatchedLitIdx];
+      const Literal NewWatchedLit = CNF.Clauses[NewWatchedLitIdx];
       const Variable NewWatchedLitVar = var(NewWatchedLit);
 
       // Swap the old watched literal for the new one in `FalseLitWatcher` to
       // maintain the invariant that the watched literal is at the beginning of
       // the clause.
-      Formula.Clauses[NewWatchedLitIdx] = FalseLit;
-      Formula.Clauses[FalseLitWatcherStart] = NewWatchedLit;
+      CNF.Clauses[NewWatchedLitIdx] = FalseLit;
+      CNF.Clauses[FalseLitWatcherStart] = NewWatchedLit;
 
       // If the new watched literal isn't watched by any other clause and its
       // variable isn't assigned we need to add it to the active variables.
@@ -621,8 +571,8 @@ class WatchedLiteralsSolverImpl {
           VarAssignments[NewWatchedLitVar] == Assignment::Unassigned)
         ActiveVars.push_back(NewWatchedLitVar);
 
-      Formula.NextWatched[FalseLitWatcher] = Formula.WatchedHead[NewWatchedLit];
-      Formula.WatchedHead[NewWatchedLit] = FalseLitWatcher;
+      CNF.NextWatched[FalseLitWatcher] = CNF.WatchedHead[NewWatchedLit];
+      CNF.WatchedHead[NewWatchedLit] = FalseLitWatcher;
 
       // Go to the next clause that watches `FalseLit`.
       FalseLitWatcher = NextFalseLitWatcher;
@@ -632,16 +582,15 @@ class WatchedLiteralsSolverImpl {
   /// Returns true if and only if one of the clauses that watch `Lit` is a unit
   /// clause.
   bool watchedByUnitClause(Literal Lit) const {
-    for (ClauseID LitWatcher = Formula.WatchedHead[Lit];
-         LitWatcher != NullClause;
-         LitWatcher = Formula.NextWatched[LitWatcher]) {
-      llvm::ArrayRef<Literal> Clause = Formula.clauseLiterals(LitWatcher);
+    for (ClauseID LitWatcher = CNF.WatchedHead[Lit]; LitWatcher != NullClause;
+         LitWatcher = CNF.NextWatched[LitWatcher]) {
+      llvm::ArrayRef<Literal> Clause = CNF.clauseLiterals(LitWatcher);
 
       // Assert the invariant that the watched literal is always the first one
       // in the clause.
       // FIXME: Consider replacing this with a test case that fails if the
       // invariant is broken by `updateWatchedLiterals`. That might not be easy
-      // due to the transformations performed by `buildBooleanFormula`.
+      // due to the transformations performed by `buildCNF`.
       assert(Clause.front() == Lit);
 
       if (isUnit(Clause))
@@ -665,7 +614,7 @@ class WatchedLiteralsSolverImpl {
 
   /// Returns true if and only if `Lit` is watched by a clause in `Formula`.
   bool isWatched(Literal Lit) const {
-    return Formula.WatchedHead[Lit] != NullClause;
+    return CNF.WatchedHead[Lit] != NullClause;
   }
 
   /// Returns an assignment for an unassigned variable.
@@ -678,8 +627,8 @@ class WatchedLiteralsSolverImpl {
   /// Returns a set of all watched literals.
   llvm::DenseSet<Literal> watchedLiterals() const {
     llvm::DenseSet<Literal> WatchedLiterals;
-    for (Literal Lit = 2; Lit < Formula.WatchedHead.size(); Lit++) {
-      if (Formula.WatchedHead[Lit] == NullClause)
+    for (Literal Lit = 2; Lit < CNF.WatchedHead.size(); Lit++) {
+      if (CNF.WatchedHead[Lit] == NullClause)
         continue;
       WatchedLiterals.insert(Lit);
     }
@@ -719,7 +668,8 @@ class WatchedLiteralsSolverImpl {
   }
 };
 
-Solver::Result WatchedLiteralsSolver::solve(llvm::ArrayRef<BoolValue *> Vals) {
+Solver::Result
+WatchedLiteralsSolver::solve(llvm::ArrayRef<const Formula *> Vals) {
   if (Vals.empty())
     return Solver::Result::Satisfiable({{}});
   auto [Res, Iterations] =
diff --git a/clang/unittests/Analysis/FlowSensitive/ArenaTest.cpp b/clang/unittests/Analysis/FlowSensitive/ArenaTest.cpp
index 407abf58529a5..53131723ff5ce 100644
--- a/clang/unittests/Analysis/FlowSensitive/ArenaTest.cpp
+++ b/clang/unittests/Analysis/FlowSensitive/ArenaTest.cpp
@@ -7,6 +7,7 @@
 //===----------------------------------------------------------------------===//
 
 #include "clang/Analysis/FlowSensitive/Arena.h"
+#include "llvm/Support/ScopedPrinter.h"
 #include "gmock/gmock.h"
 #include "gtest/gtest.h"
 
@@ -125,5 +126,26 @@ TEST_F(ArenaTest, GetOrCreateIffReturnsSameExprOnSubsequentCalls) {
   EXPECT_NE(&XIffY1, &XIffZ);
 }
 
+TEST_F(ArenaTest, ValueToFormula) {
+  auto &X = A.create<AtomicBoolValue>();
+  auto &Y = A.create<AtomicBoolValue>();
+  auto &XIffY = A.makeEquals(X, Y);
+  auto &XOrNotY = A.makeOr(X, A.makeNot(Y));
+  auto &Implies = A.makeImplies(XIffY, XOrNotY);
+
+  EXPECT_EQ(llvm::to_string(A.getFormula(Implies)),
+            "((V0 = V1) => (V0 | !V1))");
+}
+
+TEST_F(ArenaTest, ValueToFormulaCached) {
+  auto &X = A.create<AtomicBoolValue>();
+  auto &Y = A.create<AtomicBoolValue>();
+  auto &XIffY = A.makeEquals(X, Y);
+
+  auto &Formula1 = A.getFormula(XIffY);
+  auto &Formula2 = A.getFormula(XIffY);
+  EXPECT_EQ(&Formula1, &Formula2);
+}
+
 } // namespace
 } // namespace clang::dataflow
diff --git a/clang/unittests/Analysis/FlowSensitive/DebugSupportTest.cpp b/clang/unittests/Analysis/FlowSensitive/DebugSupportTest.cpp
index 10fcd204c9ab0..8ee56ae08b98a 100644
--- a/clang/unittests/Analysis/FlowSensitive/DebugSupportTest.cpp
+++ b/clang/unittests/Analysis/FlowSensitive/DebugSupportTest.cpp
@@ -8,8 +8,9 @@
 
 #include "clang/Analysis/FlowSensitive/DebugSupport.h"
 #include "TestingSupport.h"
-#include "clang/Analysis/FlowSensitive/Value.h"
-#include "clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h"
+#include "clang/Analysis/FlowSensitive/Formula.h"
+#include "llvm/Support/ScopedPrinter.h"
+#include "llvm/Support/raw_ostream.h"
 #include "gmock/gmock.h"
 #include "gtest/gtest.h"
 
@@ -22,429 +23,88 @@ using test::ConstraintContext;
 using testing::StrEq;
 
 TEST(BoolValueDebugStringTest, AtomicBoolean) {
-  // B0
   ConstraintContext Ctx;
   auto B = Ctx.atom();
 
-  auto Expected = R"(B0)";
-  EXPECT_THAT(debugString(*B), StrEq(Expected));
-}
-
-TEST(BoolValueDebugStringTest, Top) {
-  ConstraintContext Ctx;
-  auto B = Ctx.top();
-
-  auto Expected = R"(top)";
-  EXPECT_THAT(debugString(*B), StrEq(Expected));
+  auto Expected = "V0";
+  EXPECT_THAT(llvm::to_string(*B), StrEq(Expected));
 }
 
 TEST(BoolValueDebugStringTest, Negation) {
-  // !B0
   ConstraintContext Ctx;
   auto B = Ctx.neg(Ctx.atom());
 
-  auto Expected = R"((not
-    B0))";
-  EXPECT_THAT(debugString(*B), StrEq(Expected));
+  auto Expected = "!V0";
+  EXPECT_THAT(llvm::to_string(*B), StrEq(Expected));
 }
 
 TEST(BoolValueDebugStringTest, Conjunction) {
-  // B0 ^ B1
   ConstraintContext Ctx;
   auto B = Ctx.conj(Ctx.atom(), Ctx.atom());
 
-  auto Expected = R"((and
-    B0
-    B1))";
-  EXPECT_THAT(debugString(*B), StrEq(Expected));
+  auto Expected = "(V0 & V1)";
+  EXPECT_THAT(llvm::to_string(*B), StrEq(Expected));
 }
 
 TEST(BoolValueDebugStringTest, Disjunction) {
-  // B0 v B1
   ConstraintContext Ctx;
   auto B = Ctx.disj(Ctx.atom(), Ctx.atom());
 
-  auto Expected = R"((or
-    B0
-    B1))";
-  EXPECT_THAT(debugString(*B), StrEq(Expected));
+  auto Expected = "(V0 | V1)";
+  EXPECT_THAT(llvm::to_string(*B), StrEq(Expected));
 }
 
 TEST(BoolValueDebugStringTest, Implication) {
-  // B0 => B1
   ConstraintContext Ctx;
   auto B = Ctx.impl(Ctx.atom(), Ctx.atom());
 
-  auto Expected = R"((=>
-    B0
-    B1))";
-  EXPECT_THAT(debugString(*B), StrEq(Expected));
+  auto Expected = "(V0 => V1)";
+  EXPECT_THAT(llvm::to_string(*B), StrEq(Expected));
 }
 
 TEST(BoolValueDebugStringTest, Iff) {
-  // B0 <=> B1
   ConstraintContext Ctx;
   auto B = Ctx.iff(Ctx.atom(), Ctx.atom());
 
-  auto Expected = R"((=
-    B0
-    B1))";
-  EXPECT_THAT(debugString(*B), StrEq(Expected));
+  auto Expected = "(V0 = V1)";
+  EXPECT_THAT(llvm::to_string(*B), StrEq(Expected));
 }
 
 TEST(BoolValueDebugStringTest, Xor) {
-  // (B0 ^ !B1) V (!B0 ^ B1)
   ConstraintContext Ctx;
   auto B0 = Ctx.atom();
   auto B1 = Ctx.atom();
   auto B = Ctx.disj(Ctx.conj(B0, Ctx.neg(B1)), Ctx.conj(Ctx.neg(B0), B1));
 
-  auto Expected = R"((or
-    (and
-        B0
-        (not
-            B1))
-    (and
-        (not
-            B0)
-        B1)))";
-  EXPECT_THAT(debugString(*B), StrEq(Expected));
+  auto Expected = "((V0 & !V1) | (!V0 & V1))";
+  EXPECT_THAT(llvm::to_string(*B), StrEq(Expected));
 }
 
 TEST(BoolValueDebugStringTest, NestedBoolean) {
-  // B0 ^ (B1 v (B2 ^ (B3 v B4)))
   ConstraintContext Ctx;
   auto B = Ctx.conj(
       Ctx.atom(),
       Ctx.disj(Ctx.atom(),
                Ctx.conj(Ctx.atom(), Ctx.disj(Ctx.atom(), Ctx.atom()))));
 
-  auto Expected = R"((and
-    B0
-    (or
-        B1
-        (and
-            B2
-            (or
-                B3
-                B4)))))";
-  EXPECT_THAT(debugString(*B), StrEq(Expected));
-}
-
-TEST(BoolValueDebugStringTest, AtomicBooleanWithName) {
-  // True
-  ConstraintContext Ctx;
-  auto True = cast<AtomicBoolValue>(Ctx.atom());
-  auto B = True;
-
-  auto Expected = R"(True)";
-  EXPECT_THAT(debugString(*B, {{True, "True"}}), StrEq(Expected));
-}
-
-TEST(BoolValueDebugStringTest, ComplexBooleanWithNames) {
-  // (Cond ^ Then ^ !Else) v (!Cond ^ !Then ^ Else)
-  ConstraintContext Ctx;
-  auto Cond = cast<AtomicBoolValue>(Ctx.atom());
-  auto Then = cast<AtomicBoolValue>(Ctx.atom());
-  auto Else = cast<AtomicBoolValue>(Ctx.atom());
-  auto B = Ctx.disj(Ctx.conj(Cond, Ctx.conj(Then, Ctx.neg(Else))),
-                    Ctx.conj(Ctx.neg(Cond), Ctx.conj(Ctx.neg(Then), Else)));
-
-  auto Expected = R"((or
-    (and
-        Cond
-        (and
-            Then
-            (not
-                Else)))
-    (and
-        (not
-            Cond)
-        (and
-            (not
-                Then)
-            Else))))";
-  EXPECT_THAT(debugString(*B, {{Cond, "Cond"}, {Then, "Then"}, {Else, "Else"}}),
-              StrEq(Expected));
+  auto Expected = "(V0 & (V1 | (V2 & (V3 | V4))))";
+  EXPECT_THAT(llvm::to_string(*B), StrEq(Expected));
 }
 
 TEST(BoolValueDebugStringTest, ComplexBooleanWithSomeNames) {
-  // (False && B0) v (True v B1)
   ConstraintContext Ctx;
-  auto True = cast<AtomicBoolValue>(Ctx.atom());
-  auto False = cast<AtomicBoolValue>(Ctx.atom());
+  auto True = Ctx.atom();
+  auto False = Ctx.atom();
+  Formula::AtomNames Names;
+  Names[True->getAtom()] = "true";
+  Names[False->getAtom()] = "false";
   auto B = Ctx.disj(Ctx.conj(False, Ctx.atom()), Ctx.disj(True, Ctx.atom()));
 
-  auto Expected = R"((or
-    (and
-        False
-        B0)
-    (or
-        True
-        B1)))";
-  EXPECT_THAT(debugString(*B, {{True, "True"}, {False, "False"}}),
-              StrEq(Expected));
-}
-
-TEST(ConstraintSetDebugStringTest, Empty) {
-  llvm::ArrayRef<BoolValue *> Constraints;
-  EXPECT_THAT(debugString(Constraints), StrEq(""));
-}
-
-TEST(ConstraintSetDebugStringTest, Simple) {
-  ConstraintContext Ctx;
-  std::vector<BoolValue *> Constraints;
-  auto X = cast<AtomicBoolValue>(Ctx.atom());
-  auto Y = cast<AtomicBoolValue>(Ctx.atom());
-  Constraints.push_back(Ctx.disj(X, Y));
-  Constraints.push_back(Ctx.disj(X, Ctx.neg(Y)));
-
-  auto Expected = R"((or
-    X
-    Y)
-(or
-    X
-    (not
-        Y))
-)";
-  EXPECT_THAT(debugString(Constraints, {{X, "X"}, {Y, "Y"}}),
-              StrEq(Expected));
-}
-
-Solver::Result CheckSAT(std::vector<BoolValue *> Constraints) {
-  return WatchedLiteralsSolver().solve(std::move(Constraints));
-}
-
-TEST(SATCheckDebugStringTest, AtomicBoolean) {
-  // B0
-  ConstraintContext Ctx;
-  std::vector<BoolValue *> Constraints({Ctx.atom()});
-  auto Result = CheckSAT(Constraints);
-
-  auto Expected = R"(
-Constraints
-------------
-B0
-------------
-Satisfiable.
-
-B0 = True
-)";
-  EXPECT_THAT(debugString(Constraints, Result), StrEq(Expected));
-}
-
-TEST(SATCheckDebugStringTest, AtomicBooleanAndNegation) {
-  // B0, !B0
-  ConstraintContext Ctx;
-  auto B0 = Ctx.atom();
-  std::vector<BoolValue *> Constraints({B0, Ctx.neg(B0)});
-  auto Result = CheckSAT(Constraints);
-
-  auto Expected = R"(
-Constraints
-------------
-B0
-
-(not
-    B0)
-------------
-Unsatisfiable.
-
-)";
-  EXPECT_THAT(debugString(Constraints, Result), StrEq(Expected));
-}
-
-TEST(SATCheckDebugStringTest, MultipleAtomicBooleans) {
-  // B0, B1
-  ConstraintContext Ctx;
-  std::vector<BoolValue *> Constraints({Ctx.atom(), Ctx.atom()});
-  auto Result = CheckSAT(Constraints);
-
-  auto Expected = R"(
-Constraints
-------------
-B0
-
-B1
-------------
-Satisfiable.
-
-B0 = True
-B1 = True
-)";
-  EXPECT_THAT(debugString(Constraints, Result), StrEq(Expected));
-}
-
-TEST(SATCheckDebugStringTest, Implication) {
-  // B0, B0 => B1
-  ConstraintContext Ctx;
-  auto B0 = Ctx.atom();
-  auto B1 = Ctx.atom();
-  auto Impl = Ctx.disj(Ctx.neg(B0), B1);
-  std::vector<BoolValue *> Constraints({B0, Impl});
-  auto Result = CheckSAT(Constraints);
-
-  auto Expected = R"(
-Constraints
-------------
-B0
-
-(or
-    (not
-        B0)
-    B1)
-------------
-Satisfiable.
-
-B0 = True
-B1 = True
-)";
-  EXPECT_THAT(debugString(Constraints, Result), StrEq(Expected));
+  auto Expected = R"(((false & V2) | (true | V3)))";
+  std::string Actual;
+  llvm::raw_string_ostream OS(Actual);
+  B->print(OS, &Names);
+  EXPECT_THAT(Actual, StrEq(Expected));
 }
 
-TEST(SATCheckDebugStringTest, Iff) {
-  // B0, B0 <=> B1
-  ConstraintContext Ctx;
-  auto B0 = Ctx.atom();
-  auto B1 = Ctx.atom();
-  auto Iff = Ctx.conj(Ctx.disj(Ctx.neg(B0), B1), Ctx.disj(B0, Ctx.neg(B1)));
-  std::vector<BoolValue *> Constraints({B0, Iff});
-  auto Result = CheckSAT(Constraints);
-
-  auto Expected = R"(
-Constraints
-------------
-B0
-
-(and
-    (or
-        (not
-            B0)
-        B1)
-    (or
-        B0
-        (not
-            B1)))
-------------
-Satisfiable.
-
-B0 = True
-B1 = True
-)";
-  EXPECT_THAT(debugString(Constraints, Result), StrEq(Expected));
-}
-
-TEST(SATCheckDebugStringTest, Xor) {
-  // B0, XOR(B0, B1)
-  ConstraintContext Ctx;
-  auto B0 = Ctx.atom();
-  auto B1 = Ctx.atom();
-  auto XOR = Ctx.disj(Ctx.conj(B0, Ctx.neg(B1)), Ctx.conj(Ctx.neg(B0), B1));
-  std::vector<BoolValue *> Constraints({B0, XOR});
-  auto Result = CheckSAT(Constraints);
-
-  auto Expected = R"(
-Constraints
-------------
-B0
-
-(or
-    (and
-        B0
-        (not
-            B1))
-    (and
-        (not
-            B0)
-        B1))
-------------
-Satisfiable.
-
-B0 = True
-B1 = False
-)";
-  EXPECT_THAT(debugString(Constraints, Result), StrEq(Expected));
-}
-
-TEST(SATCheckDebugStringTest, ComplexBooleanWithNames) {
-  // Cond, (Cond ^ Then ^ !Else) v (!Cond ^ !Then ^ Else)
-  ConstraintContext Ctx;
-  auto Cond = cast<AtomicBoolValue>(Ctx.atom());
-  auto Then = cast<AtomicBoolValue>(Ctx.atom());
-  auto Else = cast<AtomicBoolValue>(Ctx.atom());
-  auto B = Ctx.disj(Ctx.conj(Cond, Ctx.conj(Then, Ctx.neg(Else))),
-                    Ctx.conj(Ctx.neg(Cond), Ctx.conj(Ctx.neg(Then), Else)));
-  std::vector<BoolValue *> Constraints({Cond, B});
-  auto Result = CheckSAT(Constraints);
-
-  auto Expected = R"(
-Constraints
-------------
-Cond
-
-(or
-    (and
-        Cond
-        (and
-            Then
-            (not
-                Else)))
-    (and
-        (not
-            Cond)
-        (and
-            (not
-                Then)
-            Else)))
-------------
-Satisfiable.
-
-Cond = True
-Else = False
-Then = True
-)";
-  EXPECT_THAT(debugString(Constraints, Result,
-                          {{Cond, "Cond"}, {Then, "Then"}, {Else, "Else"}}),
-              StrEq(Expected));
-}
-
-TEST(SATCheckDebugStringTest, ComplexBooleanWithLongNames) {
-  // ThisIntEqZero, !IntsAreEq, ThisIntEqZero ^ OtherIntEqZero => IntsAreEq
-  ConstraintContext Ctx;
-  auto IntsAreEq = cast<AtomicBoolValue>(Ctx.atom());
-  auto ThisIntEqZero = cast<AtomicBoolValue>(Ctx.atom());
-  auto OtherIntEqZero = cast<AtomicBoolValue>(Ctx.atom());
-  auto BothZeroImpliesEQ =
-      Ctx.disj(Ctx.neg(Ctx.conj(ThisIntEqZero, OtherIntEqZero)), IntsAreEq);
-  std::vector<BoolValue *> Constraints(
-      {ThisIntEqZero, Ctx.neg(IntsAreEq), BothZeroImpliesEQ});
-  auto Result = CheckSAT(Constraints);
-
-  auto Expected = R"(
-Constraints
-------------
-ThisIntEqZero
-
-(not
-    IntsAreEq)
-
-(or
-    (not
-        (and
-            ThisIntEqZero
-            OtherIntEqZero))
-    IntsAreEq)
-------------
-Satisfiable.
-
-IntsAreEq      = False
-OtherIntEqZero = False
-ThisIntEqZero  = True
-)";
-  EXPECT_THAT(debugString(Constraints, Result,
-                          {{IntsAreEq, "IntsAreEq"},
-                           {ThisIntEqZero, "ThisIntEqZero"},
-                           {OtherIntEqZero, "OtherIntEqZero"}}),
-              StrEq(Expected));
-}
 } // namespace
diff --git a/clang/unittests/Analysis/FlowSensitive/SolverTest.cpp b/clang/unittests/Analysis/FlowSensitive/SolverTest.cpp
index 9999dd3a475f1..ba0a77a910d7c 100644
--- a/clang/unittests/Analysis/FlowSensitive/SolverTest.cpp
+++ b/clang/unittests/Analysis/FlowSensitive/SolverTest.cpp
@@ -9,9 +9,10 @@
 #include <utility>
 
 #include "TestingSupport.h"
+#include "clang/Analysis/FlowSensitive/Formula.h"
 #include "clang/Analysis/FlowSensitive/Solver.h"
-#include "clang/Analysis/FlowSensitive/Value.h"
 #include "clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h"
+#include "llvm/ADT/ArrayRef.h"
 #include "gmock/gmock.h"
 #include "gtest/gtest.h"
 
@@ -23,26 +24,31 @@ using namespace dataflow;
 using test::ConstraintContext;
 using testing::_;
 using testing::AnyOf;
-using testing::IsEmpty;
-using testing::Optional;
 using testing::Pair;
 using testing::UnorderedElementsAre;
 
+constexpr auto AssignedTrue = Solver::Result::Assignment::AssignedTrue;
+constexpr auto AssignedFalse = Solver::Result::Assignment::AssignedFalse;
+
 // Checks if the conjunction of `Vals` is satisfiable and returns the
 // corresponding result.
-Solver::Result solve(llvm::ArrayRef<BoolValue *> Vals) {
+Solver::Result solve(llvm::ArrayRef<const Formula *> Vals) {
   return WatchedLiteralsSolver().solve(Vals);
 }
 
-void expectUnsatisfiable(Solver::Result Result) {
-  EXPECT_EQ(Result.getStatus(), Solver::Result::Status::Unsatisfiable);
-  EXPECT_FALSE(Result.getSolution().has_value());
+MATCHER(unsat, "") {
+  return arg.getStatus() == Solver::Result::Status::Unsatisfiable;
 }
-
-template <typename Matcher>
-void expectSatisfiable(Solver::Result Result, Matcher Solution) {
-  EXPECT_EQ(Result.getStatus(), Solver::Result::Status::Satisfiable);
-  EXPECT_THAT(Result.getSolution(), Optional(Solution));
+MATCHER_P(sat, SolutionMatcher,
+          "is satisfiable, where solution " +
+              (testing::DescribeMatcher<
+                  llvm::DenseMap<Atom, Solver::Result::Assignment>>(
+                  SolutionMatcher))) {
+  if (arg.getStatus() != Solver::Result::Status::Satisfiable)
+    return false;
+  auto Solution = *arg.getSolution();
+  return testing::ExplainMatchResult(SolutionMatcher, Solution,
+                                     result_listener);
 }
 
 TEST(SolverTest, Var) {
@@ -50,9 +56,8 @@ TEST(SolverTest, Var) {
   auto X = Ctx.atom();
 
   // X
-  expectSatisfiable(
-      solve({X}),
-      UnorderedElementsAre(Pair(X, Solver::Result::Assignment::AssignedTrue)));
+  EXPECT_THAT(solve({X}),
+              sat(UnorderedElementsAre(Pair(X->getAtom(), AssignedTrue))));
 }
 
 TEST(SolverTest, NegatedVar) {
@@ -61,9 +66,8 @@ TEST(SolverTest, NegatedVar) {
   auto NotX = Ctx.neg(X);
 
   // !X
-  expectSatisfiable(
-      solve({NotX}),
-      UnorderedElementsAre(Pair(X, Solver::Result::Assignment::AssignedFalse)));
+  EXPECT_THAT(solve({NotX}),
+              sat(UnorderedElementsAre(Pair(X->getAtom(), AssignedFalse))));
 }
 
 TEST(SolverTest, UnitConflict) {
@@ -72,7 +76,7 @@ TEST(SolverTest, UnitConflict) {
   auto NotX = Ctx.neg(X);
 
   // X ^ !X
-  expectUnsatisfiable(solve({X, NotX}));
+  EXPECT_THAT(solve({X, NotX}), unsat());
 }
 
 TEST(SolverTest, DistinctVars) {
@@ -82,36 +86,9 @@ TEST(SolverTest, DistinctVars) {
   auto NotY = Ctx.neg(Y);
 
   // X ^ !Y
-  expectSatisfiable(
-      solve({X, NotY}),
-      UnorderedElementsAre(Pair(X, Solver::Result::Assignment::AssignedTrue),
-                           Pair(Y, Solver::Result::Assignment::AssignedFalse)));
-}
-
-TEST(SolverTest, Top) {
-  ConstraintContext Ctx;
-  auto X = Ctx.top();
-
-  // X. Since Top is anonymous, we do not get any results in the solution.
-  expectSatisfiable(solve({X}), IsEmpty());
-}
-
-TEST(SolverTest, NegatedTop) {
-  ConstraintContext Ctx;
-  auto X = Ctx.top();
-
-  // !X
-  expectSatisfiable(solve({Ctx.neg(X)}), IsEmpty());
-}
-
-TEST(SolverTest, DistinctTops) {
-  ConstraintContext Ctx;
-  auto X = Ctx.top();
-  auto Y = Ctx.top();
-  auto NotY = Ctx.neg(Y);
-
-  // X ^ !Y
-  expectSatisfiable(solve({X, NotY}), IsEmpty());
+  EXPECT_THAT(solve({X, NotY}),
+              sat(UnorderedElementsAre(Pair(X->getAtom(), AssignedTrue),
+                                       Pair(Y->getAtom(), AssignedFalse))));
 }
 
 TEST(SolverTest, DoubleNegation) {
@@ -121,7 +98,7 @@ TEST(SolverTest, DoubleNegation) {
   auto NotNotX = Ctx.neg(NotX);
 
   // !!X ^ !X
-  expectUnsatisfiable(solve({NotNotX, NotX}));
+  EXPECT_THAT(solve({NotNotX, NotX}), unsat());
 }
 
 TEST(SolverTest, NegatedDisjunction) {
@@ -132,7 +109,7 @@ TEST(SolverTest, NegatedDisjunction) {
   auto NotXOrY = Ctx.neg(XOrY);
 
   // !(X v Y) ^ (X v Y)
-  expectUnsatisfiable(solve({NotXOrY, XOrY}));
+  EXPECT_THAT(solve({NotXOrY, XOrY}), unsat());
 }
 
 TEST(SolverTest, NegatedConjunction) {
@@ -143,7 +120,7 @@ TEST(SolverTest, NegatedConjunction) {
   auto NotXAndY = Ctx.neg(XAndY);
 
   // !(X ^ Y) ^ (X ^ Y)
-  expectUnsatisfiable(solve({NotXAndY, XAndY}));
+  EXPECT_THAT(solve({NotXAndY, XAndY}), unsat());
 }
 
 TEST(SolverTest, DisjunctionSameVarWithNegation) {
@@ -153,7 +130,7 @@ TEST(SolverTest, DisjunctionSameVarWithNegation) {
   auto XOrNotX = Ctx.disj(X, NotX);
 
   // X v !X
-  expectSatisfiable(solve({XOrNotX}), _);
+  EXPECT_THAT(solve({XOrNotX}), sat(_));
 }
 
 TEST(SolverTest, DisjunctionSameVar) {
@@ -162,7 +139,7 @@ TEST(SolverTest, DisjunctionSameVar) {
   auto XOrX = Ctx.disj(X, X);
 
   // X v X
-  expectSatisfiable(solve({XOrX}), _);
+  EXPECT_THAT(solve({XOrX}), sat(_));
 }
 
 TEST(SolverTest, ConjunctionSameVarsConflict) {
@@ -172,7 +149,7 @@ TEST(SolverTest, ConjunctionSameVarsConflict) {
   auto XAndNotX = Ctx.conj(X, NotX);
 
   // X ^ !X
-  expectUnsatisfiable(solve({XAndNotX}));
+  EXPECT_THAT(solve({XAndNotX}), unsat());
 }
 
 TEST(SolverTest, ConjunctionSameVar) {
@@ -181,7 +158,7 @@ TEST(SolverTest, ConjunctionSameVar) {
   auto XAndX = Ctx.conj(X, X);
 
   // X ^ X
-  expectSatisfiable(solve({XAndX}), _);
+  EXPECT_THAT(solve({XAndX}), sat(_));
 }
 
 TEST(SolverTest, PureVar) {
@@ -194,10 +171,9 @@ TEST(SolverTest, PureVar) {
   auto NotXOrNotY = Ctx.disj(NotX, NotY);
 
   // (!X v Y) ^ (!X v !Y)
-  expectSatisfiable(
-      solve({NotXOrY, NotXOrNotY}),
-      UnorderedElementsAre(Pair(X, Solver::Result::Assignment::AssignedFalse),
-                           Pair(Y, _)));
+  EXPECT_THAT(solve({NotXOrY, NotXOrNotY}),
+              sat(UnorderedElementsAre(Pair(X->getAtom(), AssignedFalse),
+                                       Pair(Y->getAtom(), _))));
 }
 
 TEST(SolverTest, MustAssumeVarIsFalse) {
@@ -211,10 +187,9 @@ TEST(SolverTest, MustAssumeVarIsFalse) {
   auto NotXOrNotY = Ctx.disj(NotX, NotY);
 
   // (X v Y) ^ (!X v Y) ^ (!X v !Y)
-  expectSatisfiable(
-      solve({XOrY, NotXOrY, NotXOrNotY}),
-      UnorderedElementsAre(Pair(X, Solver::Result::Assignment::AssignedFalse),
-                           Pair(Y, Solver::Result::Assignment::AssignedTrue)));
+  EXPECT_THAT(solve({XOrY, NotXOrY, NotXOrNotY}),
+              sat(UnorderedElementsAre(Pair(X->getAtom(), AssignedFalse),
+                                       Pair(Y->getAtom(), AssignedTrue))));
 }
 
 TEST(SolverTest, DeepConflict) {
@@ -229,7 +204,7 @@ TEST(SolverTest, DeepConflict) {
   auto XOrNotY = Ctx.disj(X, NotY);
 
   // (X v Y) ^ (!X v Y) ^ (!X v !Y) ^ (X v !Y)
-  expectUnsatisfiable(solve({XOrY, NotXOrY, NotXOrNotY, XOrNotY}));
+  EXPECT_THAT(solve({XOrY, NotXOrY, NotXOrNotY, XOrNotY}), unsat());
 }
 
 TEST(SolverTest, IffIsEquivalentToDNF) {
@@ -243,7 +218,7 @@ TEST(SolverTest, IffIsEquivalentToDNF) {
   auto NotEquivalent = Ctx.neg(Ctx.iff(XIffY, XIffYDNF));
 
   // !((X <=> Y) <=> ((X ^ Y) v (!X ^ !Y)))
-  expectUnsatisfiable(solve({NotEquivalent}));
+  EXPECT_THAT(solve({NotEquivalent}), unsat());
 }
 
 TEST(SolverTest, IffSameVars) {
@@ -252,7 +227,7 @@ TEST(SolverTest, IffSameVars) {
   auto XEqX = Ctx.iff(X, X);
 
   // X <=> X
-  expectSatisfiable(solve({XEqX}), _);
+  EXPECT_THAT(solve({XEqX}), sat(_));
 }
 
 TEST(SolverTest, IffDistinctVars) {
@@ -262,14 +237,12 @@ TEST(SolverTest, IffDistinctVars) {
   auto XEqY = Ctx.iff(X, Y);
 
   // X <=> Y
-  expectSatisfiable(
+  EXPECT_THAT(
       solve({XEqY}),
-      AnyOf(UnorderedElementsAre(
-                Pair(X, Solver::Result::Assignment::AssignedTrue),
-                Pair(Y, Solver::Result::Assignment::AssignedTrue)),
-            UnorderedElementsAre(
-                Pair(X, Solver::Result::Assignment::AssignedFalse),
-                Pair(Y, Solver::Result::Assignment::AssignedFalse))));
+      sat(AnyOf(UnorderedElementsAre(Pair(X->getAtom(), AssignedTrue),
+                                     Pair(Y->getAtom(), AssignedTrue)),
+                UnorderedElementsAre(Pair(X->getAtom(), AssignedFalse),
+                                     Pair(Y->getAtom(), AssignedFalse)))));
 }
 
 TEST(SolverTest, IffWithUnits) {
@@ -279,10 +252,9 @@ TEST(SolverTest, IffWithUnits) {
   auto XEqY = Ctx.iff(X, Y);
 
   // (X <=> Y) ^ X ^ Y
-  expectSatisfiable(
-      solve({XEqY, X, Y}),
-      UnorderedElementsAre(Pair(X, Solver::Result::Assignment::AssignedTrue),
-                           Pair(Y, Solver::Result::Assignment::AssignedTrue)));
+  EXPECT_THAT(solve({XEqY, X, Y}),
+              sat(UnorderedElementsAre(Pair(X->getAtom(), AssignedTrue),
+                                       Pair(Y->getAtom(), AssignedTrue))));
 }
 
 TEST(SolverTest, IffWithUnitsConflict) {
@@ -293,7 +265,7 @@ TEST(SolverTest, IffWithUnitsConflict) {
   auto NotY = Ctx.neg(Y);
 
   // (X <=> Y) ^ X  !Y
-  expectUnsatisfiable(solve({XEqY, X, NotY}));
+  EXPECT_THAT(solve({XEqY, X, NotY}), unsat());
 }
 
 TEST(SolverTest, IffTransitiveConflict) {
@@ -306,7 +278,7 @@ TEST(SolverTest, IffTransitiveConflict) {
   auto NotX = Ctx.neg(X);
 
   // (X <=> Y) ^ (Y <=> Z) ^ Z ^ !X
-  expectUnsatisfiable(solve({XEqY, YEqZ, Z, NotX}));
+  EXPECT_THAT(solve({XEqY, YEqZ, Z, NotX}), unsat());
 }
 
 TEST(SolverTest, DeMorgan) {
@@ -323,7 +295,7 @@ TEST(SolverTest, DeMorgan) {
   auto B = Ctx.iff(Ctx.neg(Ctx.conj(Z, W)), Ctx.disj(Ctx.neg(Z), Ctx.neg(W)));
 
   // A ^ B
-  expectSatisfiable(solve({A, B}), _);
+  EXPECT_THAT(solve({A, B}), sat(_));
 }
 
 TEST(SolverTest, RespectsAdditionalConstraints) {
@@ -334,7 +306,7 @@ TEST(SolverTest, RespectsAdditionalConstraints) {
   auto NotY = Ctx.neg(Y);
 
   // (X <=> Y) ^ X ^ !Y
-  expectUnsatisfiable(solve({XEqY, X, NotY}));
+  EXPECT_THAT(solve({XEqY, X, NotY}), unsat());
 }
 
 TEST(SolverTest, ImplicationIsEquivalentToDNF) {
@@ -346,7 +318,7 @@ TEST(SolverTest, ImplicationIsEquivalentToDNF) {
   auto NotEquivalent = Ctx.neg(Ctx.iff(XImpliesY, XImpliesYDNF));
 
   // !((X => Y) <=> (!X v Y))
-  expectUnsatisfiable(solve({NotEquivalent}));
+  EXPECT_THAT(solve({NotEquivalent}), unsat());
 }
 
 TEST(SolverTest, ImplicationConflict) {
@@ -357,7 +329,7 @@ TEST(SolverTest, ImplicationConflict) {
   auto *XAndNotY = Ctx.conj(X, Ctx.neg(Y));
 
   // X => Y ^ X ^ !Y
-  expectUnsatisfiable(solve({XImplY, XAndNotY}));
+  EXPECT_THAT(solve({XImplY, XAndNotY}), unsat());
 }
 
 TEST(SolverTest, LowTimeoutResultsInTimedOut) {
diff --git a/clang/unittests/Analysis/FlowSensitive/TestingSupport.h b/clang/unittests/Analysis/FlowSensitive/TestingSupport.h
index 856737d034855..507fd5290aef5 100644
--- a/clang/unittests/Analysis/FlowSensitive/TestingSupport.h
+++ b/clang/unittests/Analysis/FlowSensitive/TestingSupport.h
@@ -43,6 +43,7 @@
 #include "llvm/ADT/DenseMap.h"
 #include "llvm/ADT/StringMap.h"
 #include "llvm/ADT/StringRef.h"
+#include "llvm/Support/Allocator.h"
 #include "llvm/Support/Errc.h"
 #include "llvm/Support/Error.h"
 #include "llvm/Testing/Annotations/Annotations.h"
@@ -467,55 +468,44 @@ ValueT &getValueForDecl(ASTContext &ASTCtx, const Environment &Env,
 
 /// Creates and owns constraints which are boolean values.
 class ConstraintContext {
-public:
-  // Creates an atomic boolean value.
-  BoolValue *atom() {
-    Vals.push_back(std::make_unique<AtomicBoolValue>());
-    return Vals.back().get();
-  }
+  unsigned NextAtom = 0;
+  llvm::BumpPtrAllocator A;
 
-  // Creates an instance of the Top boolean value.
-  BoolValue *top() {
-    Vals.push_back(std::make_unique<TopBoolValue>());
-    return Vals.back().get();
+  const Formula *make(Formula::Kind K,
+                      llvm::ArrayRef<const Formula *> Operands) {
+    return &Formula::create(A, K, Operands);
   }
 
-  // Creates a boolean conjunction value.
-  BoolValue *conj(BoolValue *LeftSubVal, BoolValue *RightSubVal) {
-    Vals.push_back(
-        std::make_unique<ConjunctionValue>(*LeftSubVal, *RightSubVal));
-    return Vals.back().get();
+public:
+  // Returns a reference to a fresh atomic variable.
+  const Formula *atom() {
+    return &Formula::create(A, Formula::AtomRef, {}, NextAtom++);
   }
 
-  // Creates a boolean disjunction value.
-  BoolValue *disj(BoolValue *LeftSubVal, BoolValue *RightSubVal) {
-    Vals.push_back(
-        std::make_unique<DisjunctionValue>(*LeftSubVal, *RightSubVal));
-    return Vals.back().get();
+  // Creates a boolean conjunction.
+  const Formula *conj(const Formula *LHS, const Formula *RHS) {
+    return make(Formula::And, {LHS, RHS});
   }
 
-  // Creates a boolean negation value.
-  BoolValue *neg(BoolValue *SubVal) {
-    Vals.push_back(std::make_unique<NegationValue>(*SubVal));
-    return Vals.back().get();
+  // Creates a boolean disjunction.
+  const Formula *disj(const Formula *LHS, const Formula *RHS) {
+    return make(Formula::Or, {LHS, RHS});
   }
 
-  // Creates a boolean implication value.
-  BoolValue *impl(BoolValue *LeftSubVal, BoolValue *RightSubVal) {
-    Vals.push_back(
-        std::make_unique<ImplicationValue>(*LeftSubVal, *RightSubVal));
-    return Vals.back().get();
+  // Creates a boolean negation.
+  const Formula *neg(const Formula *Operand) {
+    return make(Formula::Not, {Operand});
   }
 
-  // Creates a boolean biconditional value.
-  BoolValue *iff(BoolValue *LeftSubVal, BoolValue *RightSubVal) {
-    Vals.push_back(
-        std::make_unique<BiconditionalValue>(*LeftSubVal, *RightSubVal));
-    return Vals.back().get();
+  // Creates a boolean implication.
+  const Formula *impl(const Formula *LHS, const Formula *RHS) {
+    return make(Formula::Implies, {LHS, RHS});
   }
 
-private:
-  std::vector<std::unique_ptr<BoolValue>> Vals;
+  // Creates a boolean biconditional.
+  const Formula *iff(const Formula *LHS, const Formula *RHS) {
+    return make(Formula::Equal, {LHS, RHS});
+  }
 };
 
 } // namespace test