Revert "Reland "[dataflow] Add dedicated representation of boolean formulas" and followups

These changes are OK, but they break downstream stuff that needs more time to adapt :-(

This reverts commit 71579569f4399d3cf6bc618dcd449b5388d749cc.
This reverts commit 5e4ad816bf100b0325ed45ab1cfea18deb3ab3d1.
This reverts commit 1c3ac8dfa16c42a631968aadd0396cfe7f7778e0.

9 files changed, 568 insertions, 411 deletions

diff --git a/clang/lib/Analysis/FlowSensitive/Arena.cpp b/clang/lib/Analysis/FlowSensitive/Arena.cpp
index a61887a..cff6c45 100644
--- a/clang/lib/Analysis/FlowSensitive/Arena.cpp
+++ b/clang/lib/Analysis/FlowSensitive/Arena.cpp
@@ -7,95 +7,65 @@
 //===----------------------------------------------------------------------===//
 
 #include "clang/Analysis/FlowSensitive/Arena.h"
-#include "clang/Analysis/FlowSensitive/Value.h"
 
 namespace clang::dataflow {
 
-static std::pair<const Formula *, const Formula *>
-canonicalFormulaPair(const Formula &LHS, const Formula &RHS) {
+static std::pair<BoolValue *, BoolValue *>
+makeCanonicalBoolValuePair(BoolValue &LHS, BoolValue &RHS) {
   auto Res = std::make_pair(&LHS, &RHS);
-  if (&RHS < &LHS) // FIXME: use a deterministic order instead
+  if (&RHS < &LHS)
     std::swap(Res.first, Res.second);
   return Res;
 }
 
-template <class Key, class ComputeFunc>
-const Formula &cached(llvm::DenseMap<Key, const Formula *> &Cache, Key K,
-                      ComputeFunc &&Compute) {
-  auto [It, Inserted] = Cache.try_emplace(std::forward<Key>(K));
-  if (Inserted)
-    It->second = Compute();
-  return *It->second;
-}
+BoolValue &Arena::makeAnd(BoolValue &LHS, BoolValue &RHS) {
+  if (&LHS == &RHS)
+    return LHS;
 
-const Formula &Arena::makeAtomRef(Atom A) {
-  return cached(AtomRefs, A, [&] {
-    return &Formula::create(Alloc, Formula::AtomRef, {},
-                            static_cast<unsigned>(A));
-  });
+  auto Res = ConjunctionVals.try_emplace(makeCanonicalBoolValuePair(LHS, RHS),
+                                         nullptr);
+  if (Res.second)
+    Res.first->second = &create<ConjunctionValue>(LHS, RHS);
+  return *Res.first->second;
 }
 
-const Formula &Arena::makeAnd(const Formula &LHS, const Formula &RHS) {
-  return cached(Ands, canonicalFormulaPair(LHS, RHS), [&] {
-    if (&LHS == &RHS)
-      return &LHS;
-    if (LHS.kind() == Formula::Literal)
-      return LHS.literal() ? &RHS : &LHS;
-    if (RHS.kind() == Formula::Literal)
-      return RHS.literal() ? &LHS : &RHS;
+BoolValue &Arena::makeOr(BoolValue &LHS, BoolValue &RHS) {
+  if (&LHS == &RHS)
+    return LHS;
 
-    return &Formula::create(Alloc, Formula::And, {&LHS, &RHS});
-  });
+  auto Res = DisjunctionVals.try_emplace(makeCanonicalBoolValuePair(LHS, RHS),
+                                         nullptr);
+  if (Res.second)
+    Res.first->second = &create<DisjunctionValue>(LHS, RHS);
+  return *Res.first->second;
 }
 
-const Formula &Arena::makeOr(const Formula &LHS, const Formula &RHS) {
-  return cached(Ors, canonicalFormulaPair(LHS, RHS), [&] {
-    if (&LHS == &RHS)
-      return &LHS;
-    if (LHS.kind() == Formula::Literal)
-      return LHS.literal() ? &LHS : &RHS;
-    if (RHS.kind() == Formula::Literal)
-      return RHS.literal() ? &RHS : &LHS;
-
-    return &Formula::create(Alloc, Formula::Or, {&LHS, &RHS});
-  });
+BoolValue &Arena::makeNot(BoolValue &Val) {
+  auto Res = NegationVals.try_emplace(&Val, nullptr);
+  if (Res.second)
+    Res.first->second = &create<NegationValue>(Val);
+  return *Res.first->second;
 }
 
-const Formula &Arena::makeNot(const Formula &Val) {
-  return cached(Nots, &Val, [&] {
-    if (Val.kind() == Formula::Not)
-      return Val.operands()[0];
-    if (Val.kind() == Formula::Literal)
-      return &makeLiteral(!Val.literal());
+BoolValue &Arena::makeImplies(BoolValue &LHS, BoolValue &RHS) {
+  if (&LHS == &RHS)
+    return makeLiteral(true);
 
-    return &Formula::create(Alloc, Formula::Not, {&Val});
-  });
+  auto Res = ImplicationVals.try_emplace(std::make_pair(&LHS, &RHS), nullptr);
+  if (Res.second)
+    Res.first->second = &create<ImplicationValue>(LHS, RHS);
+  return *Res.first->second;
 }
 
-const Formula &Arena::makeImplies(const Formula &LHS, const Formula &RHS) {
-  return cached(Implies, std::make_pair(&LHS, &RHS), [&] {
-    if (&LHS == &RHS)
-      return &makeLiteral(true);
-    if (LHS.kind() == Formula::Literal)
-      return LHS.literal() ? &RHS : &makeLiteral(true);
-    if (RHS.kind() == Formula::Literal)
-      return RHS.literal() ? &RHS : &makeNot(LHS);
+BoolValue &Arena::makeEquals(BoolValue &LHS, BoolValue &RHS) {
+  if (&LHS == &RHS)
+    return makeLiteral(true);
 
-    return &Formula::create(Alloc, Formula::Implies, {&LHS, &RHS});
-  });
-}
-
-const Formula &Arena::makeEquals(const Formula &LHS, const Formula &RHS) {
-  return cached(Equals, canonicalFormulaPair(LHS, RHS), [&] {
-    if (&LHS == &RHS)
-      return &makeLiteral(true);
-    if (LHS.kind() == Formula::Literal)
-      return LHS.literal() ? &RHS : &makeNot(RHS);
-    if (RHS.kind() == Formula::Literal)
-      return RHS.literal() ? &LHS : &makeNot(LHS);
-
-    return &Formula::create(Alloc, Formula::Equal, {&LHS, &RHS});
-  });
+  auto Res = BiconditionalVals.try_emplace(makeCanonicalBoolValuePair(LHS, RHS),
+                                           nullptr);
+  if (Res.second)
+    Res.first->second = &create<BiconditionalValue>(LHS, RHS);
+  return *Res.first->second;
 }
 
 IntegerValue &Arena::makeIntLiteral(llvm::APInt Value) {
@@ -106,13 +76,4 @@ IntegerValue &Arena::makeIntLiteral(llvm::APInt Value) {
   return *It->second;
 }
 
-BoolValue &Arena::makeBoolValue(const Formula &F) {
-  auto [It, Inserted] = FormulaValues.try_emplace(&F);
-  if (Inserted)
-    It->second = (F.kind() == Formula::AtomRef)
-                     ? (BoolValue *)&create<AtomicBoolValue>(F)
-                     : &create<FormulaBoolValue>(F);
-  return *It->second;
-}
-
 } // namespace clang::dataflow
diff --git a/clang/lib/Analysis/FlowSensitive/CMakeLists.txt b/clang/lib/Analysis/FlowSensitive/CMakeLists.txt
index 171884a..d59bebf 100644
--- a/clang/lib/Analysis/FlowSensitive/CMakeLists.txt
+++ b/clang/lib/Analysis/FlowSensitive/CMakeLists.txt
@@ -3,7 +3,6 @@ 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 2971df6..37bcc8b 100644
--- a/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
+++ b/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
@@ -15,7 +15,6 @@
 #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"
@@ -24,12 +23,9 @@
 #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,
@@ -102,107 +98,108 @@ DataflowAnalysisContext::getOrCreateNullPointerValue(QualType PointeeType) {
 }
 
 void DataflowAnalysisContext::addFlowConditionConstraint(
-    Atom Token, const Formula &Constraint) {
-  auto Res = FlowConditionConstraints.try_emplace(Token, &Constraint);
+    AtomicBoolValue &Token, BoolValue &Constraint) {
+  auto Res = FlowConditionConstraints.try_emplace(&Token, &Constraint);
   if (!Res.second) {
     Res.first->second =
         &arena().makeAnd(*Res.first->second, Constraint);
   }
 }
 
-Atom DataflowAnalysisContext::forkFlowCondition(Atom Token) {
-  Atom ForkToken = arena().makeFlowConditionToken();
-  FlowConditionDeps[ForkToken].insert(Token);
-  addFlowConditionConstraint(ForkToken, arena().makeAtomRef(Token));
+AtomicBoolValue &
+DataflowAnalysisContext::forkFlowCondition(AtomicBoolValue &Token) {
+  auto &ForkToken = arena().makeFlowConditionToken();
+  FlowConditionDeps[&ForkToken].insert(&Token);
+  addFlowConditionConstraint(ForkToken, Token);
   return ForkToken;
 }
 
-Atom 
-DataflowAnalysisContext::joinFlowConditions(Atom FirstToken,
-                                            Atom SecondToken) {
-  Atom Token = arena().makeFlowConditionToken();
-  FlowConditionDeps[Token].insert(FirstToken);
-  FlowConditionDeps[Token].insert(SecondToken);
-  addFlowConditionConstraint(Token,
-                             arena().makeOr(arena().makeAtomRef(FirstToken),
-                                            arena().makeAtomRef(SecondToken)));
+AtomicBoolValue &
+DataflowAnalysisContext::joinFlowConditions(AtomicBoolValue &FirstToken,
+                                            AtomicBoolValue &SecondToken) {
+  auto &Token = arena().makeFlowConditionToken();
+  FlowConditionDeps[&Token].insert(&FirstToken);
+  FlowConditionDeps[&Token].insert(&SecondToken);
+  addFlowConditionConstraint(
+      Token, arena().makeOr(FirstToken, SecondToken));
   return Token;
 }
 
-Solver::Result DataflowAnalysisContext::querySolver(
-    llvm::SetVector<const Formula *> Constraints) {
+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());
 }
 
-bool DataflowAnalysisContext::flowConditionImplies(Atom Token,
-                                                   const Formula &Val) {
+bool DataflowAnalysisContext::flowConditionImplies(AtomicBoolValue &Token,
+                                                   BoolValue &Val) {
   // Returns true if and only if truth assignment of the flow condition implies
   // that `Val` is also true. We prove whether or not this property holds by
   // reducing the problem to satisfiability checking. In other words, we attempt
   // to show that assuming `Val` is false makes the constraints induced by the
   // flow condition unsatisfiable.
-  llvm::SetVector<const Formula *> Constraints;
-  Constraints.insert(&arena().makeAtomRef(Token));
+  llvm::SetVector<BoolValue *> Constraints;
+  Constraints.insert(&Token);
   Constraints.insert(&arena().makeNot(Val));
-  llvm::DenseSet<Atom> VisitedTokens;
+  llvm::DenseSet<AtomicBoolValue *> VisitedTokens;
   addTransitiveFlowConditionConstraints(Token, Constraints, VisitedTokens);
   return isUnsatisfiable(std::move(Constraints));
 }
 
-bool DataflowAnalysisContext::flowConditionIsTautology(Atom Token) {
+bool DataflowAnalysisContext::flowConditionIsTautology(AtomicBoolValue &Token) {
   // Returns true if and only if we cannot prove that the flow condition can
   // ever be false.
-  llvm::SetVector<const Formula *> Constraints;
-  Constraints.insert(&arena().makeNot(arena().makeAtomRef(Token)));
-  llvm::DenseSet<Atom> VisitedTokens;
+  llvm::SetVector<BoolValue *> Constraints;
+  Constraints.insert(&arena().makeNot(Token));
+  llvm::DenseSet<AtomicBoolValue *> VisitedTokens;
   addTransitiveFlowConditionConstraints(Token, Constraints, VisitedTokens);
   return isUnsatisfiable(std::move(Constraints));
 }
 
-bool DataflowAnalysisContext::equivalentFormulas(const Formula &Val1,
-                                                 const Formula &Val2) {
-  llvm::SetVector<const Formula *> Constraints;
+bool DataflowAnalysisContext::equivalentBoolValues(BoolValue &Val1,
+                                                   BoolValue &Val2) {
+  llvm::SetVector<BoolValue*> Constraints;
   Constraints.insert(&arena().makeNot(arena().makeEquals(Val1, Val2)));
   return isUnsatisfiable(std::move(Constraints));
 }
 
 void DataflowAnalysisContext::addTransitiveFlowConditionConstraints(
-    Atom Token, llvm::SetVector<const Formula *> &Constraints,
-    llvm::DenseSet<Atom> &VisitedTokens) {
-  auto Res = VisitedTokens.insert(Token);
+    AtomicBoolValue &Token, llvm::SetVector<BoolValue *> &Constraints,
+    llvm::DenseSet<AtomicBoolValue *> &VisitedTokens) {
+  auto Res = VisitedTokens.insert(&Token);
   if (!Res.second)
     return;
 
-  auto ConstraintsIt = FlowConditionConstraints.find(Token);
+  auto ConstraintsIt = FlowConditionConstraints.find(&Token);
   if (ConstraintsIt == FlowConditionConstraints.end()) {
-    Constraints.insert(&arena().makeAtomRef(Token));
+    Constraints.insert(&Token);
   } else {
     // Bind flow condition token via `iff` to its set of constraints:
     // FC <=> (C1 ^ C2 ^ ...), where Ci are constraints
-    Constraints.insert(&arena().makeEquals(arena().makeAtomRef(Token),
-                                           *ConstraintsIt->second));
+    Constraints.insert(&arena().makeEquals(Token, *ConstraintsIt->second));
   }
 
-  auto DepsIt = FlowConditionDeps.find(Token);
+  auto DepsIt = FlowConditionDeps.find(&Token);
   if (DepsIt != FlowConditionDeps.end()) {
-    for (Atom DepToken : DepsIt->second) {
-      addTransitiveFlowConditionConstraints(DepToken, Constraints,
+    for (AtomicBoolValue *DepToken : DepsIt->second) {
+      addTransitiveFlowConditionConstraints(*DepToken, Constraints,
                                             VisitedTokens);
     }
   }
 }
 
-void DataflowAnalysisContext::dumpFlowCondition(Atom Token,
+void DataflowAnalysisContext::dumpFlowCondition(AtomicBoolValue &Token,
                                                 llvm::raw_ostream &OS) {
-  llvm::SetVector<const Formula *> Constraints;
-  Constraints.insert(&arena().makeAtomRef(Token));
-  llvm::DenseSet<Atom> VisitedTokens;
+  llvm::SetVector<BoolValue *> Constraints;
+  Constraints.insert(&Token);
+  llvm::DenseSet<AtomicBoolValue *> VisitedTokens;
   addTransitiveFlowConditionConstraints(Token, Constraints, VisitedTokens);
 
-  for (const auto *Constraint : Constraints) {
-    Constraint->print(OS);
-    OS << "\n";
-  }
+  llvm::DenseMap<const AtomicBoolValue *, std::string> AtomNames = {
+      {&arena().makeLiteral(false), "False"},
+      {&arena().makeLiteral(true), "True"}};
+  OS << debugString(Constraints.getArrayRef(), AtomNames);
 }
 
 const ControlFlowContext *
diff --git a/clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp b/clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp
index 11bb7da..4a11c09 100644
--- a/clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp
+++ b/clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp
@@ -107,16 +107,15 @@ static Value *mergeDistinctValues(QualType Type, Value &Val1,
     // if (o.has_value())
     //   x = o.value();
     // ```
-    auto &Expr1 = cast<BoolValue>(Val1).formula();
-    auto &Expr2 = cast<BoolValue>(Val2).formula();
-    auto &A = MergedEnv.arena();
-    auto &MergedVal = A.makeAtomRef(A.makeAtom());
-    MergedEnv.addToFlowCondition(
-        A.makeOr(A.makeAnd(A.makeAtomRef(Env1.getFlowConditionToken()),
-                           A.makeEquals(MergedVal, Expr1)),
-                 A.makeAnd(A.makeAtomRef(Env2.getFlowConditionToken()),
-                           A.makeEquals(MergedVal, Expr2))));
-    return &A.makeBoolValue(MergedVal);
+    auto *Expr1 = cast<BoolValue>(&Val1);
+    auto *Expr2 = cast<BoolValue>(&Val2);
+    auto &MergedVal = MergedEnv.makeAtomicBoolValue();
+    MergedEnv.addToFlowCondition(MergedEnv.makeOr(
+        MergedEnv.makeAnd(Env1.getFlowConditionToken(),
+                          MergedEnv.makeIff(MergedVal, *Expr1)),
+        MergedEnv.makeAnd(Env2.getFlowConditionToken(),
+                          MergedEnv.makeIff(MergedVal, *Expr2))));
+    return &MergedVal;
   }
 
   // FIXME: Consider destroying `MergedValue` immediately if `ValueModel::merge`
@@ -270,11 +269,11 @@ void Environment::initFieldsGlobalsAndFuncs(const FunctionDecl *FuncDecl) {
 
 Environment::Environment(DataflowAnalysisContext &DACtx)
     : DACtx(&DACtx),
-      FlowConditionToken(DACtx.arena().makeFlowConditionToken()) {}
+      FlowConditionToken(&DACtx.arena().makeFlowConditionToken()) {}
 
 Environment Environment::fork() const {
   Environment Copy(*this);
-  Copy.FlowConditionToken = DACtx->forkFlowCondition(FlowConditionToken);
+  Copy.FlowConditionToken = &DACtx->forkFlowCondition(*FlowConditionToken);
   return Copy;
 }
 
@@ -588,8 +587,8 @@ Environment Environment::join(const Environment &EnvA, const Environment &EnvB,
 
   // FIXME: update join to detect backedges and simplify the flow condition
   // accordingly.
-  JoinedEnv.FlowConditionToken = EnvA.DACtx->joinFlowConditions(
-      EnvA.FlowConditionToken, EnvB.FlowConditionToken);
+  JoinedEnv.FlowConditionToken = &EnvA.DACtx->joinFlowConditions(
+      *EnvA.FlowConditionToken, *EnvB.FlowConditionToken);
 
   for (auto &Entry : EnvA.LocToVal) {
     const StorageLocation *Loc = Entry.first;
@@ -820,7 +819,7 @@ Value *Environment::createValueUnlessSelfReferential(
     // with integers, and so distinguishing them serves no purpose, but could
     // prevent convergence.
     CreatedValuesCount++;
-    return &arena().create<IntegerValue>();
+    return &DACtx->arena().create<IntegerValue>();
   }
 
   if (Type->isReferenceType() || Type->isPointerType()) {
@@ -838,9 +837,9 @@ Value *Environment::createValueUnlessSelfReferential(
     }
 
     if (Type->isReferenceType())
-      return &arena().create<ReferenceValue>(PointeeLoc);
+      return &DACtx->arena().create<ReferenceValue>(PointeeLoc);
     else
-      return &arena().create<PointerValue>(PointeeLoc);
+      return &DACtx->arena().create<PointerValue>(PointeeLoc);
   }
 
   if (Type->isRecordType()) {
@@ -860,7 +859,7 @@ Value *Environment::createValueUnlessSelfReferential(
       Visited.erase(FieldType.getCanonicalType());
     }
 
-    return &arena().create<StructValue>(std::move(FieldValues));
+    return &DACtx->arena().create<StructValue>(std::move(FieldValues));
   }
 
   return nullptr;
@@ -885,18 +884,12 @@ const StorageLocation &Environment::skip(const StorageLocation &Loc,
   return skip(*const_cast<StorageLocation *>(&Loc), SP);
 }
 
-void Environment::addToFlowCondition(const Formula &Val) {
-  DACtx->addFlowConditionConstraint(FlowConditionToken, Val);
-}
 void Environment::addToFlowCondition(BoolValue &Val) {
-  addToFlowCondition(Val.formula());
+  DACtx->addFlowConditionConstraint(*FlowConditionToken, Val);
 }
 
-bool Environment::flowConditionImplies(const Formula &Val) const {
-  return DACtx->flowConditionImplies(FlowConditionToken, Val);
-}
 bool Environment::flowConditionImplies(BoolValue &Val) const {
-  return flowConditionImplies(Val.formula());
+  return DACtx->flowConditionImplies(*FlowConditionToken, Val);
 }
 
 void Environment::dump(raw_ostream &OS) const {
@@ -916,7 +909,7 @@ void Environment::dump(raw_ostream &OS) const {
   }
 
   OS << "FlowConditionToken:\n";
-  DACtx->dumpFlowCondition(FlowConditionToken, OS);
+  DACtx->dumpFlowCondition(*FlowConditionToken, OS);
 }
 
 void Environment::dump() const {
diff --git a/clang/lib/Analysis/FlowSensitive/DebugSupport.cpp b/clang/lib/Analysis/FlowSensitive/DebugSupport.cpp
index f8a049a..25225ed 100644
--- a/clang/lib/Analysis/FlowSensitive/DebugSupport.cpp
+++ b/clang/lib/Analysis/FlowSensitive/DebugSupport.cpp
@@ -16,12 +16,22 @@
 #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:
@@ -36,19 +46,26 @@ llvm::StringRef debugString(Value::Kind Kind) {
     return "AtomicBool";
   case Value::Kind::TopBool:
     return "TopBool";
-  case Value::Kind::FormulaBool:
-    return "FormulaBool";
+  case Value::Kind::Conjunction:
+    return "Conjunction";
+  case Value::Kind::Disjunction:
+    return "Disjunction";
+  case Value::Kind::Negation:
+    return "Negation";
+  case Value::Kind::Implication:
+    return "Implication";
+  case Value::Kind::Biconditional:
+    return "Biconditional";
   }
   llvm_unreachable("Unhandled value kind");
 }
 
-llvm::raw_ostream &operator<<(llvm::raw_ostream &OS,
-                              Solver::Result::Assignment Assignment) {
+llvm::StringRef debugString(Solver::Result::Assignment Assignment) {
   switch (Assignment) {
   case Solver::Result::Assignment::AssignedFalse:
-    return OS << "False";
+    return "False";
   case Solver::Result::Assignment::AssignedTrue:
-    return OS << "True";
+    return "True";
   }
   llvm_unreachable("Booleans can only be assigned true/false");
 }
@@ -65,16 +82,174 @@ llvm::StringRef debugString(Solver::Result::Status Status) {
   llvm_unreachable("Unhandled SAT check result status");
 }
 
-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";
+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()));
   }
-  return OS;
+
+  /// 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);
 }
 
 } // namespace dataflow
diff --git a/clang/lib/Analysis/FlowSensitive/Formula.cpp b/clang/lib/Analysis/FlowSensitive/Formula.cpp
deleted file mode 100644
index 12f4e25..0000000
--- a/clang/lib/Analysis/FlowSensitive/Formula.cpp
+++ /dev/null
@@ -1,93 +0,0 @@
-//===- 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 {
-
-const 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:
-  case Formula::Literal:
-    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:
-    switch (kind()) {
-    case AtomRef:
-      OS << getAtom();
-      break;
-    case Literal:
-      OS << (literal() ? "true" : "false");
-      break;
-    default:
-      llvm_unreachable("unhandled formula kind");
-    }
-    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/HTMLLogger.cpp b/clang/lib/Analysis/FlowSensitive/HTMLLogger.cpp
index 0c4e838..14293a3 100644
--- a/clang/lib/Analysis/FlowSensitive/HTMLLogger.cpp
+++ b/clang/lib/Analysis/FlowSensitive/HTMLLogger.cpp
@@ -97,7 +97,6 @@ public:
     case Value::Kind::Integer:
     case Value::Kind::TopBool:
     case Value::Kind::AtomicBool:
-    case Value::Kind::FormulaBool:
       break;
     case Value::Kind::Reference:
       JOS.attributeObject(
@@ -112,6 +111,35 @@ public:
         JOS.attributeObject("f:" + Child.first->getNameAsString(),
                             [&] { dump(*Child.second); });
       break;
+    case Value::Kind::Disjunction: {
+      auto &VV = cast<DisjunctionValue>(V);
+      JOS.attributeObject("lhs", [&] { dump(VV.getLeftSubValue()); });
+      JOS.attributeObject("rhs", [&] { dump(VV.getRightSubValue()); });
+      break;
+    }
+    case Value::Kind::Conjunction: {
+      auto &VV = cast<ConjunctionValue>(V);
+      JOS.attributeObject("lhs", [&] { dump(VV.getLeftSubValue()); });
+      JOS.attributeObject("rhs", [&] { dump(VV.getRightSubValue()); });
+      break;
+    }
+    case Value::Kind::Negation: {
+      auto &VV = cast<NegationValue>(V);
+      JOS.attributeObject("not", [&] { dump(VV.getSubVal()); });
+      break;
+    }
+    case Value::Kind::Implication: {
+      auto &VV = cast<ImplicationValue>(V);
+      JOS.attributeObject("if", [&] { dump(VV.getLeftSubValue()); });
+      JOS.attributeObject("then", [&] { dump(VV.getRightSubValue()); });
+      break;
+    }
+    case Value::Kind::Biconditional: {
+      auto &VV = cast<BiconditionalValue>(V);
+      JOS.attributeObject("lhs", [&] { dump(VV.getLeftSubValue()); });
+      JOS.attributeObject("rhs", [&] { dump(VV.getRightSubValue()); });
+      break;
+    }
     }
 
     for (const auto& Prop : V.properties())
@@ -121,12 +149,10 @@ public:
     // Running the SAT solver is expensive, but knowing which booleans are
     // guaranteed true/false here is valuable and hard to determine by hand.
     if (auto *B = llvm::dyn_cast<BoolValue>(&V)) {
-      JOS.attribute("formula", llvm::to_string(B->formula()));
-      JOS.attribute(
-          "truth", Env.flowConditionImplies(B->formula()) ? "true"
-                   : Env.flowConditionImplies(Env.arena().makeNot(B->formula()))
-                       ? "false"
-                       : "unknown");
+      JOS.attribute("truth", Env.flowConditionImplies(*B) ? "true"
+                             : Env.flowConditionImplies(Env.makeNot(*B))
+                                 ? "false"
+                                 : "unknown");
     }
   }
   void dump(const StorageLocation &L) {
diff --git a/clang/lib/Analysis/FlowSensitive/Transfer.cpp b/clang/lib/Analysis/FlowSensitive/Transfer.cpp
index b9a2672..5ad176d 100644
--- a/clang/lib/Analysis/FlowSensitive/Transfer.cpp
+++ b/clang/lib/Analysis/FlowSensitive/Transfer.cpp
@@ -62,12 +62,64 @@ static BoolValue &evaluateBooleanEquality(const Expr &LHS, const Expr &RHS,
   return Env.makeAtomicBoolValue();
 }
 
+// Functionally updates `V` such that any instances of `TopBool` are replaced
+// with fresh atomic bools. Note: This implementation assumes that `B` is a
+// tree; if `B` is a DAG, it will lose any sharing between subvalues that was
+// present in the original .
+static BoolValue &unpackValue(BoolValue &V, Environment &Env);
+
+template <typename Derived, typename M>
+BoolValue &unpackBinaryBoolValue(Environment &Env, BoolValue &B, M build) {
+  auto &V = *cast<Derived>(&B);
+  BoolValue &Left = V.getLeftSubValue();
+  BoolValue &Right = V.getRightSubValue();
+  BoolValue &ULeft = unpackValue(Left, Env);
+  BoolValue &URight = unpackValue(Right, Env);
+
+  if (&ULeft == &Left && &URight == &Right)
+    return V;
+
+  return (Env.*build)(ULeft, URight);
+}
+
 static BoolValue &unpackValue(BoolValue &V, Environment &Env) {
-  if (auto *Top = llvm::dyn_cast<TopBoolValue>(&V)) {
-    auto &A = Env.getDataflowAnalysisContext().arena();
-    return A.makeBoolValue(A.makeAtomRef(Top->getAtom()));
+  switch (V.getKind()) {
+  case Value::Kind::Integer:
+  case Value::Kind::Reference:
+  case Value::Kind::Pointer:
+  case Value::Kind::Struct:
+    llvm_unreachable("BoolValue cannot have any of these kinds.");
+
+  case Value::Kind::AtomicBool:
+    return V;
+
+  case Value::Kind::TopBool:
+    // Unpack `TopBool` into a fresh atomic bool.
+    return Env.makeAtomicBoolValue();
+
+  case Value::Kind::Negation: {
+    auto &N = *cast<NegationValue>(&V);
+    BoolValue &Sub = N.getSubVal();
+    BoolValue &USub = unpackValue(Sub, Env);
+
+    if (&USub == &Sub)
+      return V;
+    return Env.makeNot(USub);
+  }
+  case Value::Kind::Conjunction:
+    return unpackBinaryBoolValue<ConjunctionValue>(Env, V,
+                                                   &Environment::makeAnd);
+  case Value::Kind::Disjunction:
+    return unpackBinaryBoolValue<DisjunctionValue>(Env, V,
+                                                   &Environment::makeOr);
+  case Value::Kind::Implication:
+    return unpackBinaryBoolValue<ImplicationValue>(
+        Env, V, &Environment::makeImplication);
+  case Value::Kind::Biconditional:
+    return unpackBinaryBoolValue<BiconditionalValue>(Env, V,
+                                                     &Environment::makeIff);
   }
-  return V;
+  llvm_unreachable("All reachable cases in switch return");
 }
 
 // Unpacks the value (if any) associated with `E` and updates `E` to the new
diff --git a/clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp b/clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp
index bf48a1f..db2e1d6 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 CNFFormula {
+struct BooleanFormula {
   /// `LargestVar` is equal to the largest positive integer that represents a
   /// variable in the formula.
   const Variable LargestVar;
@@ -121,12 +121,12 @@ struct CNFFormula {
   /// clauses in the formula start from the element at index 1.
   std::vector<ClauseID> NextWatched;
 
-  /// Stores the variable identifier and Atom for atomic booleans in the
-  /// formula.
-  llvm::DenseMap<Variable, Atom> Atomics;
+  /// Stores the variable identifier and value location for atomic booleans in
+  /// the formula.
+  llvm::DenseMap<Variable, AtomicBoolValue *> Atomics;
 
-  explicit CNFFormula(Variable LargestVar,
-                      llvm::DenseMap<Variable, Atom> Atomics)
+  explicit BooleanFormula(Variable LargestVar,
+                          llvm::DenseMap<Variable, AtomicBoolValue *> Atomics)
       : LargestVar(LargestVar), Atomics(std::move(Atomics)) {
     Clauses.push_back(0);
     ClauseStarts.push_back(0);
@@ -144,8 +144,8 @@ struct CNFFormula {
   ///
   ///  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 Formula
-    // and the construction in `buildCNF`.
+    // The literals are guaranteed to be distinct from properties of BoolValue
+    // and the construction in `buildBooleanFormula`.
     assert(L1 != NullLit && L1 != L2 && L1 != L3 &&
            (L2 != L3 || L2 == NullLit));
 
@@ -178,59 +178,98 @@ struct CNFFormula {
 
 /// Converts the conjunction of `Vals` into a formula in conjunctive normal
 /// form where each clause has at least one and at most three literals.
-CNFFormula buildCNF(const llvm::ArrayRef<const Formula *> &Vals) {
+BooleanFormula buildBooleanFormula(const llvm::ArrayRef<BoolValue *> &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-formulas in `Vals`.
+  // of sub-values in `Vals`.
 
-  // 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;
+  // 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;
   Variable NextVar = 1;
   {
-    std::queue<const Formula *> UnprocessedSubVals;
-    for (const Formula *Val : Vals)
+    std::queue<BoolValue *> UnprocessedSubVals;
+    for (BoolValue *Val : Vals)
       UnprocessedSubVals.push(Val);
     while (!UnprocessedSubVals.empty()) {
       Variable Var = NextVar;
-      const Formula *Val = UnprocessedSubVals.front();
+      BoolValue *Val = UnprocessedSubVals.front();
       UnprocessedSubVals.pop();
 
       if (!SubValsToVar.try_emplace(Val, Var).second)
         continue;
       ++NextVar;
 
-      for (const Formula *F : Val->operands())
-        UnprocessedSubVals.push(F);
-      if (Val->kind() == Formula::AtomRef)
-        Atomics[Var] = Val->getAtom();
+      // 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");
+      }
     }
   }
 
-  auto GetVar = [&SubValsToVar](const Formula *Val) {
+  auto GetVar = [&SubValsToVar](const BoolValue *Val) {
     auto ValIt = SubValsToVar.find(Val);
     assert(ValIt != SubValsToVar.end());
     return ValIt->second;
   };
 
-  CNFFormula CNF(NextVar - 1, std::move(Atomics));
+  BooleanFormula Formula(NextVar - 1, std::move(Atomics));
   std::vector<bool> ProcessedSubVals(NextVar, false);
 
-  // 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 a conjunct for each variable that represents a top-level conjunction
+  // value in `Vals`.
+  for (BoolValue *Val : Vals)
+    Formula.addClause(posLit(GetVar(Val)));
 
   // Add conjuncts that represent the mapping between newly-created variables
-  // and their corresponding sub-formulas.
-  std::queue<const Formula *> UnprocessedSubVals;
-  for (const Formula *Val : Vals)
+  // and their corresponding sub-values.
+  std::queue<BoolValue *> UnprocessedSubVals;
+  for (BoolValue *Val : Vals)
     UnprocessedSubVals.push(Val);
   while (!UnprocessedSubVals.empty()) {
-    const Formula *Val = UnprocessedSubVals.front();
+    const BoolValue *Val = UnprocessedSubVals.front();
     UnprocessedSubVals.pop();
     const Variable Var = GetVar(Val);
 
@@ -238,110 +277,117 @@ CNFFormula buildCNF(const llvm::ArrayRef<const Formula *> &Vals) {
       continue;
     ProcessedSubVals[Var] = true;
 
-    switch (Val->kind()) {
-    case Formula::AtomRef:
-      break;
-    case Formula::Literal:
-      CNF.addClause(Val->literal() ? posLit(Var) : negLit(Var));
-      break;
-    case Formula::And: {
-      const Variable LHS = GetVar(Val->operands()[0]);
-      const Variable RHS = GetVar(Val->operands()[1]);
-
-      if (LHS == RHS) {
+    if (auto *C = dyn_cast<ConjunctionValue>(Val)) {
+      const Variable LeftSubVar = GetVar(&C->getLeftSubValue());
+      const Variable RightSubVar = GetVar(&C->getRightSubValue());
+
+      if (LeftSubVar == RightSubVar) {
         // `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.
-        CNF.addClause(negLit(Var), posLit(LHS));
-        CNF.addClause(posLit(Var), negLit(LHS));
+        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());
       } 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.
-        CNF.addClause(negLit(Var), posLit(LHS));
-        CNF.addClause(negLit(Var), posLit(RHS));
-        CNF.addClause(posLit(Var), negLit(LHS), negLit(RHS));
+        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());
       }
-      break;
-    }
-    case Formula::Or: {
-      const Variable LHS = GetVar(Val->operands()[0]);
-      const Variable RHS = GetVar(Val->operands()[1]);
+    } else if (auto *D = dyn_cast<DisjunctionValue>(Val)) {
+      const Variable LeftSubVar = GetVar(&D->getLeftSubValue());
+      const Variable RightSubVar = GetVar(&D->getRightSubValue());
 
-      if (LHS == RHS) {
+      if (LeftSubVar == RightSubVar) {
         // `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.
-        CNF.addClause(negLit(Var), posLit(LHS));
-        CNF.addClause(posLit(Var), negLit(LHS));
+        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());
       } 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.
-        CNF.addClause(negLit(Var), posLit(LHS), posLit(RHS));
-        CNF.addClause(posLit(Var), negLit(LHS));
-        CNF.addClause(posLit(Var), negLit(RHS));
+        // `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());
       }
-      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]);
+    } 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());
 
       // `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.
-      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) {
+      // 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) {
         // `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.
-        CNF.addClause(posLit(Var));
+        Formula.addClause(posLit(Var));
 
         // No need to visit the sub-values of `Val`.
-        continue;
+      } 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());
       }
-      // `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 CNF;
+  return Formula;
 }
 
 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.
-  CNFFormula CNF;
+  BooleanFormula Formula;
 
   /// The search for a satisfying assignment of the variables in `Formula` will
   /// proceed in levels, starting from 1 and going up to `Formula.LargestVar`
@@ -393,10 +439,9 @@ class WatchedLiteralsSolverImpl {
   std::vector<Variable> ActiveVars;
 
 public:
-  explicit WatchedLiteralsSolverImpl(
-      const llvm::ArrayRef<const Formula *> &Vals)
-      : CNF(buildCNF(Vals)), LevelVars(CNF.LargestVar + 1),
-        LevelStates(CNF.LargestVar + 1) {
+  explicit WatchedLiteralsSolverImpl(const llvm::ArrayRef<BoolValue *> &Vals)
+      : Formula(buildBooleanFormula(Vals)), LevelVars(Formula.LargestVar + 1),
+        LevelStates(Formula.LargestVar + 1) {
     assert(!Vals.empty());
 
     // Initialize the state at the root level to a decision so that in
@@ -405,10 +450,10 @@ public:
     LevelStates[0] = State::Decision;
 
     // Initialize all variables as unassigned.
-    VarAssignments.resize(CNF.LargestVar + 1, Assignment::Unassigned);
+    VarAssignments.resize(Formula.LargestVar + 1, Assignment::Unassigned);
 
     // Initialize the active variables.
-    for (Variable Var = CNF.LargestVar; Var != NullVar; --Var) {
+    for (Variable Var = Formula.LargestVar; Var != NullVar; --Var) {
       if (isWatched(posLit(Var)) || isWatched(negLit(Var)))
         ActiveVars.push_back(Var);
     }
@@ -429,7 +474,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 `buildCNF`.
+      // transformations performed by `buildBooleanFormula`.
       assert(activeVarsAreUnassigned());
       assert(activeVarsFormWatchedLiterals());
       assert(unassignedVarsFormingWatchedLiteralsAreActive());
@@ -510,10 +555,12 @@ public:
   }
 
 private:
-  /// 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) {
+  /// 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) {
       // 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.
@@ -549,24 +596,24 @@ private:
     const Literal FalseLit = VarAssignments[Var] == Assignment::AssignedTrue
                                  ? negLit(Var)
                                  : posLit(Var);
-    ClauseID FalseLitWatcher = CNF.WatchedHead[FalseLit];
-    CNF.WatchedHead[FalseLit] = NullClause;
+    ClauseID FalseLitWatcher = Formula.WatchedHead[FalseLit];
+    Formula.WatchedHead[FalseLit] = NullClause;
     while (FalseLitWatcher != NullClause) {
-      const ClauseID NextFalseLitWatcher = CNF.NextWatched[FalseLitWatcher];
+      const ClauseID NextFalseLitWatcher = Formula.NextWatched[FalseLitWatcher];
 
       // Pick the first non-false literal as the new watched literal.
-      const size_t FalseLitWatcherStart = CNF.ClauseStarts[FalseLitWatcher];
+      const size_t FalseLitWatcherStart = Formula.ClauseStarts[FalseLitWatcher];
       size_t NewWatchedLitIdx = FalseLitWatcherStart + 1;
-      while (isCurrentlyFalse(CNF.Clauses[NewWatchedLitIdx]))
+      while (isCurrentlyFalse(Formula.Clauses[NewWatchedLitIdx]))
         ++NewWatchedLitIdx;
-      const Literal NewWatchedLit = CNF.Clauses[NewWatchedLitIdx];
+      const Literal NewWatchedLit = Formula.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.
-      CNF.Clauses[NewWatchedLitIdx] = FalseLit;
-      CNF.Clauses[FalseLitWatcherStart] = NewWatchedLit;
+      Formula.Clauses[NewWatchedLitIdx] = FalseLit;
+      Formula.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.
@@ -574,8 +621,8 @@ private:
           VarAssignments[NewWatchedLitVar] == Assignment::Unassigned)
         ActiveVars.push_back(NewWatchedLitVar);
 
-      CNF.NextWatched[FalseLitWatcher] = CNF.WatchedHead[NewWatchedLit];
-      CNF.WatchedHead[NewWatchedLit] = FalseLitWatcher;
+      Formula.NextWatched[FalseLitWatcher] = Formula.WatchedHead[NewWatchedLit];
+      Formula.WatchedHead[NewWatchedLit] = FalseLitWatcher;
 
       // Go to the next clause that watches `FalseLit`.
       FalseLitWatcher = NextFalseLitWatcher;
@@ -585,15 +632,16 @@ 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 = CNF.WatchedHead[Lit]; LitWatcher != NullClause;
-         LitWatcher = CNF.NextWatched[LitWatcher]) {
-      llvm::ArrayRef<Literal> Clause = CNF.clauseLiterals(LitWatcher);
+    for (ClauseID LitWatcher = Formula.WatchedHead[Lit];
+         LitWatcher != NullClause;
+         LitWatcher = Formula.NextWatched[LitWatcher]) {
+      llvm::ArrayRef<Literal> Clause = Formula.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 `buildCNF`.
+      // due to the transformations performed by `buildBooleanFormula`.
       assert(Clause.front() == Lit);
 
       if (isUnit(Clause))
@@ -617,7 +665,7 @@ private:
 
   /// Returns true if and only if `Lit` is watched by a clause in `Formula`.
   bool isWatched(Literal Lit) const {
-    return CNF.WatchedHead[Lit] != NullClause;
+    return Formula.WatchedHead[Lit] != NullClause;
   }
 
   /// Returns an assignment for an unassigned variable.
@@ -630,8 +678,8 @@ private:
   /// Returns a set of all watched literals.
   llvm::DenseSet<Literal> watchedLiterals() const {
     llvm::DenseSet<Literal> WatchedLiterals;
-    for (Literal Lit = 2; Lit < CNF.WatchedHead.size(); Lit++) {
-      if (CNF.WatchedHead[Lit] == NullClause)
+    for (Literal Lit = 2; Lit < Formula.WatchedHead.size(); Lit++) {
+      if (Formula.WatchedHead[Lit] == NullClause)
         continue;
       WatchedLiterals.insert(Lit);
     }
@@ -671,8 +719,7 @@ private:
   }
 };
 
-Solver::Result
-WatchedLiteralsSolver::solve(llvm::ArrayRef<const Formula *> Vals) {
+Solver::Result WatchedLiteralsSolver::solve(llvm::ArrayRef<BoolValue *> Vals) {
   if (Vals.empty())
     return Solver::Result::Satisfiable({{}});
   auto [Res, Iterations] =