6 files changed, 291 insertions, 366 deletions

diff --git a/clang/lib/Analysis/FlowSensitive/Arena.cpp b/clang/lib/Analysis/FlowSensitive/Arena.cpp
index cff6c45..e576aff 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 d59bebf..171884a 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 37bcc8b..42cc6d4 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 25225ed..34e53249 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 0000000..504ad2f
--- /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 db2e1d6..037886d 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 @@ public:
     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 @@ public:
       // 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 @@ public:
   }
 
 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 @@ private:
     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 @@ private:
           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 @@ private:
   /// 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 @@ private:
 
   /// 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 @@ private:
   /// 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 @@ private:
   }
 };
 
-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] =