[dataflow] Add dedicated representation of boolean formulas

[sammccall]

Summary

This is the first step in untangling the two current jobs of BoolValue.

Desired end-state:

• BoolValue will model C++ booleans e.g. held in StorageLocations. this includes describing uncertainty (e.g. "top" is a Value concern)
• Formula describes analysis-level assertions in terms of SAT atoms.

These can still be linked together: a BoolValue may have a corresponding
SAT atom which is constrained by formulas.

Done in this patch:

BoolValue is left intact, Formula is just the input type to the
SAT solver, and we build formulas as needed to invoke the solver.

Incidental changes to debug string printing:

• variables renamed from B0 etc to V0 etc B0 collides with the names of basic blocks, which is confusing when debugging flow conditions.
• debug printing of formulas (Formula and Atom) uses operator<< rather than debugString(), so works with gtest. Therefore moved out of DebugSupport.h
• Did the same to Solver::Result, and some helper changes to SolverTest, so that we get useful messages on unit test failures
• formulas are now printed as infix expressions on one line, rather than wrapped/indented S-exprs. My experience is that this is easier to scan FCs for small examples, and large ones are unreadable either way.
• most of the several debugString() functions for constraints/results are unused, so removed them rather than updating tests. Inlined the one that was actually used into its callsite.

[sammccall]

update tests

[sammccall]

updating description

[sammccall]

more tests

[sammccall]

remove dead comment

[sammccall]

clean up

[sammccall]

Splitting out Formula from BoolValue is a pretty big change... I've tried to keep this patch a manageable size by really just using Formula for interacting with the SAT solver and some printing, but this means we're maintaining BoolValues and Formulas in parallel for now. Best to take a look at Formula.h, then look ahead to D153469 to see how we can eliminate the BoolValue subclasses, stop using Values as flow conditions in DataflowAnalysisContext, etc.

Would be very happy to hear high-level feedback/concerns first.
(I do know there's a bunch of places where words in comments/variable names should likely change - I thought making all these up front may make this very noisy to review)

[mboehme]

High-level comment: I like the separation of concerns that this introduces.

Would you like me to review https://reviews.llvm.org/D153469 or should we wait for this patch to converge first?

clang/include/clang/Analysis/FlowSensitive/Formula.h

23

Put this right above the class definition below? (This is just needed for the alignas(Formula *), right?)

39

Is this important to state? (It's an implementation detail of Atom, essentially?)

48

Do you need the alignas because the pointers to operands are stored as trailing objects? Can you add a short comment to that effect?

72

Is this technically legal? (I've taken a look, but the definition of similar types makes my eyes glaze over.)

Why not use TrailingObjects instead? (I'm not really familiar with TrailingObjects, so there may be good reasons against it -- just asking because it seems like an obvious existing mechanism that could be used here.)

83

This looks like an "internal" API -- it's really only intended for use by Arena, right?

Maybe add a comment indicating that it's not intended to be used directly?

105

Why not give this type Atom?

clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp

219

Now that we've added Formula, it's pretty confusing that we also have BooleanFormula.

I assume this is one of the renamings that you want to get to later? I guess BooleanFormula becomes something like CnfFormula (would like to do 3CnfFormula, but you can't start with a digit... :( )

[sammccall]

Would you like me to review https://reviews.llvm.org/D153469 or should we wait for this patch to converge first?

Similarly it'd be great to get high-level feedback there: whether the design of FormulaBoolValue is right, whether the changes to use Atom/Formula more pervasively seem sensible etc.
For the details, probably better to wait until this one is stable to avoid churn...

Thanks!

clang/include/clang/Analysis/FlowSensitive/Formula.h

72

Is this technically legal?

Yeah, it's OK: similar types etc is not relevant because these pointers are not pointing to objects of different types: there's an object of type Formula at one address that has a lifetime that begins at the constructor (but it's trivially destructible and never destroyed), and then objects of type Formula* at higher addresses - these don't overlap, and are both part of the chunks of memory provided by malloc.

Why not use TrailingObjects instead?

TrailingObjects is complicated and ugly - it *can* work for this, but I don't think it's actually easier to understand. (Do a code search for "this + 1" in LLVM - this is often done "by hand" instead of with TrailingObjects for simple cases like this one).

e.g. here we have a little magic in create() and a little in operands(). TrailingObjects equally needs ~2 pieces of magic, they're *slightly* less scary, but they also don't relate directly to the memory layout, and I don't think you can have a meaningful understanding of what this is for without also thinking about the memory layout.

TrailingObjects shines when the pointer arithmetic gets complicated, though...

105

I don't think it should always be Atom, even when it's used

see D153485 where I add a "Literal" formula and use value to distinguish true/false

clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp

219

Agree this is an unfortunate conflict and we should probably rename this local one.
(Just because it's more important that the public type gets the good name)

CNFFormula or just CNF SGTM.
I'll leave this open and do it as a followup if that's OK, the patch is noisy as is.

[mboehme]

In D153366#4441758, @sammccall wrote:

Would you like me to review https://reviews.llvm.org/D153469 or should we wait for this patch to converge first?

Similarly it'd be great to get high-level feedback there: whether the design of FormulaBoolValue is right, whether the changes to use Atom/Formula more pervasively seem sensible etc.
For the details, probably better to wait until this one is stable to avoid churn...

Thanks!

Will do!

clang/include/clang/Analysis/FlowSensitive/Formula.h

72

Is this technically legal?

Yeah, it's OK: similar types etc is not relevant because these pointers are not pointing to objects of different types: there's an object of type Formula at one address that has a lifetime that begins at the constructor (but it's trivially destructible and never destroyed), and then objects of type Formula* at higher addresses - these don't overlap, and are both part of the chunks of memory provided by malloc.

Thanks for the explanation!

Is it worth putting a (condensed) version of this in a comment, or is this well-known enough that it's not worth it?

Why not use TrailingObjects instead?

TrailingObjects is complicated and ugly - it *can* work for this, but I don't think it's actually easier to understand. (Do a code search for "this + 1" in LLVM - this is often done "by hand" instead of with TrailingObjects for simple cases like this one).

e.g. here we have a little magic in create() and a little in operands(). TrailingObjects equally needs ~2 pieces of magic, they're *slightly* less scary, but they also don't relate directly to the memory layout, and I don't think you can have a meaningful understanding of what this is for without also thinking about the memory layout.

TrailingObjects shines when the pointer arithmetic gets complicated, though...

Again, thanks for the explanation. I don't have any experience with TrailingObjects except for using classes that are implemented using it, so thanks for filling me in.

105

Ah, I understand now.

Maybe add a comment somewhere to explain this distinction? (If it had me scratching my head, it might do so for others too.)

clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp

219

Yes, please do leave it open. This should happen later, just wanted to clarify that that's the plan.

[sammccall]

address Martin's review comments

[sammccall]

BTW, since this is a substantial API/concept change, I'll wait on approval from all of @mboehme, @xazax.hun, @gribozavr2 - if you don't plan to review just LMK.
(Not in a hurry, just wanted to mention so we don't deadlock :-)

clang/include/clang/Analysis/FlowSensitive/Formula.h

72

Is it worth putting a (condensed) version of this in a comment, or is this well-known enough that it's not worth it?

I've added a few lines inside create() - putting this in the class comment is just distracting I think.

83

Done. We could friend Arena, but it's not actually a really specialized or dangerous API, so I think a comment is cleaner.

clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp

219

In fact there are only a handful of references to this class name, and it's pretty confusing, so I've done the rename to CNFFormula. I think this actually makes the purpose of this class much clearer!

(I did also update some comments here were "value" was being used in a way that's now misleading)

[sammccall]

rebase, primarily on the SAT-inputs-are-ordered change (SetVector etc)

clarify that Formula::print output is supposed to be reliably stable.
This is useful for testing downstream analyses: having a representation of
formulas that can outlive the DataAnalysisContext makes tests more ergonomic.

Change Formula::print back to using a map of atom names instead of a delegate
print function. The extra flexibility is not useful, and it's awkward to use.

[gribozavr2]

clang/include/clang/Analysis/FlowSensitive/Formula.h

28

34

47

For consistency with the printed representation of the formula.

70

Should it be called getAsAtom() or castAsAtom() ? For uniformity with other names in Clang and LLVM.

130–131

'inline' should be unnecessary here.

clang/include/clang/Analysis/FlowSensitive/Solver.h

73–74

clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp

137

clang/unittests/Analysis/FlowSensitive/SolverTest.cpp

92

While you're refactoring this test, could you add 'using' decls for AssignedTrue and AssignedFalse at the top of the file?

clang/unittests/Analysis/FlowSensitive/TestingSupport.h

475

I'd say either "creates a fresh..." or "returns a reference to..." (although pedantically, it returns a pointer)

485–487

499–500

Similarly, drop "value" from the rest of the comments above.

[sammccall]

clang/include/clang/Analysis/FlowSensitive/Formula.h

70

This isn't quite a cast - the distinction between a variable's identity and a reference to it is real.
renamed to getAtom()

[uabelho]

Failed Tests (6):
  Clang-Unit :: Analysis/FlowSensitive/./ClangAnalysisFlowSensitiveTests/BoolValueDebugStringTest/ComplexBooleanWithSomeNames
  Clang-Unit :: Analysis/FlowSensitive/./ClangAnalysisFlowSensitiveTests/BoolValueDebugStringTest/Conjunction
  Clang-Unit :: Analysis/FlowSensitive/./ClangAnalysisFlowSensitiveTests/BoolValueDebugStringTest/Disjunction
  Clang-Unit :: Analysis/FlowSensitive/./ClangAnalysisFlowSensitiveTests/BoolValueDebugStringTest/Iff
  Clang-Unit :: Analysis/FlowSensitive/./ClangAnalysisFlowSensitiveTests/BoolValueDebugStringTest/Implication
  Clang-Unit :: Analysis/FlowSensitive/./ClangAnalysisFlowSensitiveTests/BoolValueDebugStringTest/NestedBoolean

https://lab.llvm.org/buildbot/#/builders/139/builds/44269

[thakis]

Looks like this breaks tests on windows: http://45.33.8.238/win/80815/step_7.txt

Please take a look etc

[TWeaver]

Hello and good afternoon from the UK,

I believe this change has introduced test failures on the following buildbot:

https://lab.llvm.org/buildbot/#/builders/139/builds/44269

are you able to take a look see?

Much appreciated,
Tom W

[TWeaver]

My apologies but I've had to revert this change for now until the author can address the buildbot failures.

[sammccall]

In D153366#4471320, @TWeaver wrote:

My apologies but I've had to revert this change for now until the author can address the buildbot failures.

Thanks for the revert, and sorry for the disruption - I expected to be around to keep an eye on this, but was away.

[TWeaver]

In D153366#4471460, @sammccall wrote:

In D153366#4471320, @TWeaver wrote:

My apologies but I've had to revert this change for now until the author can address the buildbot failures.

Thanks for the revert, and sorry for the disruption - I expected to be around to keep an eye on this, but was away.

No worries Sam, thanks for understanding! Good luck on the fix, let me know if you need any help 👍

clang/include/clang/Analysis/FlowSensitive/Arena.h

 //===-- Arena.h -------------------------------*- C++ -------------------*-===//
 //
 // Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
 // See https://llvm.org/LICENSE.txt for license information.
 // SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
 //
 //===----------------------------------------------------------------------===//
 #ifndef LLVM_CLANG_ANALYSIS_FLOWSENSITIVE__ARENA_H
 #define LLVM_CLANG_ANALYSIS_FLOWSENSITIVE__ARENA_H
 
+#include "clang/Analysis/FlowSensitive/Formula.h"
 #include "clang/Analysis/FlowSensitive/StorageLocation.h"
 #include "clang/Analysis/FlowSensitive/Value.h"
 #include <vector>
 
 namespace clang::dataflow {
 
 /// The Arena owns the objects that model data within an analysis.
 /// For example, `Value` and `StorageLocation`.
public:
   /// Creates a fresh flow condition and returns a token that identifies it. The
   /// token can be used to perform various operations on the flow condition such
   /// as adding constraints to it, forking it, joining it with another flow
   /// condition, or checking implications.
   AtomicBoolValue &makeFlowConditionToken() {
     return create<AtomicBoolValue>();
   }
 
+  /// Gets the boolean formula equivalent of a BoolValue.
+  /// Each unique Top values is translated to an Atom.
+  /// TODO: migrate to storing Formula directly in Values instead.
+  const Formula &getFormula(const BoolValue &);
+
+  /// Returns a new atomic boolean variable, distinct from any other.
+  Atom makeAtom() { return static_cast<Atom>(NextAtom++); };
+
 private:
+  llvm::BumpPtrAllocator Alloc;
+
   // Storage for the state of a program.
   std::vector<std::unique_ptr<StorageLocation>> Locs;
   std::vector<std::unique_ptr<Value>> Vals;
 
   // Indices that are used to avoid recreating the same integer literals and
   // composite boolean values.
   llvm::DenseMap<llvm::APInt, IntegerValue *> IntegerLiterals;
   llvm::DenseMap<std::pair<BoolValue *, BoolValue *>, ConjunctionValue *>
       ConjunctionVals;
   llvm::DenseMap<std::pair<BoolValue *, BoolValue *>, DisjunctionValue *>
       DisjunctionVals;
   llvm::DenseMap<BoolValue *, NegationValue *> NegationVals;
   llvm::DenseMap<std::pair<BoolValue *, BoolValue *>, ImplicationValue *>
       ImplicationVals;
   llvm::DenseMap<std::pair<BoolValue *, BoolValue *>, BiconditionalValue *>
       BiconditionalVals;
 
+  llvm::DenseMap<const BoolValue *, const Formula *> ValToFormula;
+  unsigned NextAtom = 0;
+
   AtomicBoolValue &TrueVal;
   AtomicBoolValue &FalseVal;
 };
 
 } // namespace clang::dataflow
 
 #endif // LLVM_CLANG_ANALYSIS_FLOWSENSITIVE__ARENA_H

clang/include/clang/Analysis/FlowSensitive/DebugSupport.h

 #ifndef LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_DEBUGSUPPORT_H_
 #define LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_DEBUGSUPPORT_H_
 
 #include <string>
 #include <vector>
 
 #include "clang/Analysis/FlowSensitive/Solver.h"
 #include "clang/Analysis/FlowSensitive/Value.h"
-#include "llvm/ADT/DenseMap.h"
 #include "llvm/ADT/StringRef.h"
 
 namespace clang {
 namespace dataflow {
 
 /// Returns a string representation of a value kind.
 llvm::StringRef debugString(Value::Kind Kind);
 
-/// Returns a string representation of a boolean assignment to true or false.
-llvm::StringRef debugString(Solver::Result::Assignment Assignment);
-
 /// Returns a string representation of the result status of a SAT check.
 llvm::StringRef debugString(Solver::Result::Status Status);
 
-/// Returns a string representation for the boolean value `B`.
-///
-/// Atomic booleans appearing in the boolean value `B` are assigned to labels
-/// either specified in `AtomNames` or created by default rules as B0, B1, ...
-///
-/// Requirements:
-///
-///   Names assigned to atoms should not be repeated in `AtomNames`.
-std::string debugString(
-    const BoolValue &B,
-    llvm::DenseMap<const AtomicBoolValue *, std::string> AtomNames = {{}});
-
-/// Returns a string representation for `Constraints` - a collection of boolean
-/// formulas.
-///
-/// Atomic booleans appearing in the boolean value `Constraints` are assigned to
-/// labels either specified in `AtomNames` or created by default rules as B0,
-/// B1, ...
-///
-/// Requirements:
-///
-///   Names assigned to atoms should not be repeated in `AtomNames`.
-std::string debugString(
-    const llvm::ArrayRef<BoolValue *> Constraints,
-    llvm::DenseMap<const AtomicBoolValue *, std::string> AtomNames = {{}});
-
-/// Returns a string representation for `Constraints` - a collection of boolean
-/// formulas and the `Result` of satisfiability checking.
-///
-/// Atomic booleans appearing in `Constraints` and `Result` are assigned to
-/// labels either specified in `AtomNames` or created by default rules as B0,
-/// B1, ...
-///
-/// Requirements:
-///
-///   Names assigned to atoms should not be repeated in `AtomNames`.
-std::string debugString(
-    ArrayRef<BoolValue *> Constraints, const Solver::Result &Result,
-    llvm::DenseMap<const AtomicBoolValue *, std::string> AtomNames = {{}});
-
 } // namespace dataflow
 } // namespace clang
 
 #endif // LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_DEBUGSUPPORT_H_

clang/include/clang/Analysis/FlowSensitive/Formula.h

+//===- Formula.h - Boolean formulas -----------------------------*- C++ -*-===//
+//
+// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
+// See https://llvm.org/LICENSE.txt for license information.
+// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+//
+//===----------------------------------------------------------------------===//
+
+#ifndef LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_FORMULA_H
+#define LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_FORMULA_H
+
+#include "clang/Basic/LLVM.h"
+#include "llvm/ADT/ArrayRef.h"
+#include "llvm/ADT/DenseMap.h"
+#include "llvm/ADT/DenseMapInfo.h"
+#include "llvm/ADT/STLFunctionalExtras.h"
+#include "llvm/Support/Allocator.h"
+#include "llvm/Support/raw_ostream.h"
+#include <cassert>
+#include <string>
+#include <type_traits>
+
+namespace clang::dataflow {
+
+/// Identifies an atomic boolean variable such as "V1".
+///
+/// This often represents an assertion that is interesting to the analysis but
+/// cannot immediately be proven true or false. For example:
+/// - V1 may mean "the program reaches this point",
+/// - V2 may mean "the parameter was null"
+///
+/// We can use these variables in formulas to describe relationships we know
+/// to be true: "if the parameter was null, the program reaches this point".
+/// We also express hypotheses as formulas, and use a SAT solver to check
+/// whether they are consistent with the known facts.
+enum class Atom : unsigned {};
+
+/// A boolean expression such as "true" or "V1 & !V2".
+/// Expressions may refer to boolean atomic variables. These should take a
+/// consistent true/false value across the set of formulas being considered.
+///
+/// (Formulas are always expressions in terms of boolean variables rather than
+/// e.g. integers because our underlying model is SAT rather than e.g. SMT).
+///
+/// Simple formulas such as "true" and "V1" are self-contained.
+/// Compound formulas connect other formulas, e.g. "(V1 & V2) || V3" is an 'or'
+/// formula, with pointers to its operands "(V1 & V2)" and "V3" stored as
+/// trailing objects.
+/// For this reason, Formulas are Arena-allocated and over-aligned.
+class Formula;
+class alignas(const Formula *) Formula {
+public:
+  enum Kind : unsigned {
+    /// A reference to an atomic boolean variable.
+    /// We name these e.g. "V3", where 3 == atom identity == Value.
+    AtomRef,
+    // FIXME: add const true/false rather than modeling them as variables
+
+    Not, /// True if its only operand is false
+
+    // These kinds connect two operands LHS and RHS
+    And,     /// True if LHS and RHS are both true
+    Or,      /// True if either LHS or RHS is true
+    Implies, /// True if LHS is false or RHS is true
+    Equal,   /// True if LHS and RHS have the same truth value
+  };
+  Kind kind() const { return FormulaKind; }
+
+  Atom getAtom() const {
+    assert(kind() == AtomRef);
+    return static_cast<Atom>(Value);
+  }
+
+  ArrayRef<const Formula *> operands() const {
+    return ArrayRef(reinterpret_cast<Formula *const *>(this + 1),
+                    numOperands(kind()));
+  }
+
+  using AtomNames = llvm::DenseMap<Atom, std::string>;
+  // Produce a stable human-readable representation of this formula.
+  // For example: (V3 | !(V1 & V2))
+  // If AtomNames is provided, these override the default V0, V1... names.
+  void print(llvm::raw_ostream &OS, const AtomNames * = nullptr) const;
+
+  // Allocate Formulas using Arena rather than calling this function directly.
+  static Formula &create(llvm::BumpPtrAllocator &Alloc, Kind K,
+                         ArrayRef<const Formula *> Operands,
+                         unsigned Value = 0);
+
+private:
+  Formula() = default;
+  Formula(const Formula &) = delete;
+  Formula &operator=(const Formula &) = delete;
+
+  static unsigned numOperands(Kind K) {
+    switch (K) {
+    case AtomRef:
+      return 0;
+    case Not:
+      return 1;
+    case And:
+    case Or:
+    case Implies:
+    case Equal:
+      return 2;
+    }
+  }
+
+  Kind FormulaKind;
+  // Some kinds of formula have scalar values, e.g. AtomRef's atom number.
+  unsigned Value;
+};
+
+// The default names of atoms are V0, V1 etc in order of creation.
+inline llvm::raw_ostream &operator<<(llvm::raw_ostream &OS, Atom A) {
+  return OS << 'V' << static_cast<unsigned>(A);
+}
+inline llvm::raw_ostream &operator<<(llvm::raw_ostream &OS, const Formula &F) {
+  F.print(OS);
+  return OS;
+}
+
+} // namespace clang::dataflow
+namespace llvm {
+template <> struct DenseMapInfo<clang::dataflow::Atom> {
+  using Atom = clang::dataflow::Atom;
+  using Underlying = std::underlying_type_t<Atom>;
+
+  static inline Atom getEmptyKey() { return Atom(Underlying(-1)); }
+  static inline Atom getTombstoneKey() { return Atom(Underlying(-2)); }
+  static unsigned getHashValue(const Atom &Val) {
+    return DenseMapInfo<Underlying>::getHashValue(Underlying(Val));
+  }
+  static bool isEqual(const Atom &LHS, const Atom &RHS) { return LHS == RHS; }
+};
+} // namespace llvm
+#endif

clang/include/clang/Analysis/FlowSensitive/Solver.h

 //===- Solver.h -------------------------------------------------*- 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
 //
 //===----------------------------------------------------------------------===//
 //
 //  This file defines an interface for a SAT solver that can be used by
 //  dataflow analyses.
 //
 //===----------------------------------------------------------------------===//
 
 #ifndef LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_SOLVER_H
 #define LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_SOLVER_H
 
-#include "clang/Analysis/FlowSensitive/Value.h"
+#include "clang/Analysis/FlowSensitive/Formula.h"
 #include "clang/Basic/LLVM.h"
 #include "llvm/ADT/ArrayRef.h"
 #include "llvm/ADT/DenseMap.h"
-#include "llvm/ADT/DenseSet.h"
-#include "llvm/Support/Compiler.h"
 #include <optional>
 #include <vector>
 
 namespace clang {
 namespace dataflow {
 
 /// An interface for a SAT solver that can be used by dataflow analyses.
 class Solver {
enum class Status {
       TimedOut,
     };
 
     /// A boolean value is set to true or false in a truth assignment.
     enum class Assignment : uint8_t { AssignedFalse = 0, AssignedTrue = 1 };
 
     /// Constructs a result indicating that the queried boolean formula is
     /// satisfiable. The result will hold a solution found by the solver.
-    static Result
-    Satisfiable(llvm::DenseMap<AtomicBoolValue *, Assignment> Solution) {
+    static Result Satisfiable(llvm::DenseMap<Atom, Assignment> Solution) {
       return Result(Status::Satisfiable, std::move(Solution));
     }
 
     /// Constructs a result indicating that the queried boolean formula is
     /// unsatisfiable.
     static Result Unsatisfiable() { return Result(Status::Unsatisfiable, {}); }
 
     /// Constructs a result indicating that satisfiability checking on the
     /// queried boolean formula was not completed.
     static Result TimedOut() { return Result(Status::TimedOut, {}); }
 
     /// Returns the status of satisfiability checking on the queried boolean
     /// formula.
     Status getStatus() const { return SATCheckStatus; }
 
     /// Returns a truth assignment to boolean values that satisfies the queried
     /// boolean formula if available. Otherwise, an empty optional is returned.
-    std::optional<llvm::DenseMap<AtomicBoolValue *, Assignment>>
-    getSolution() const {
+    std::optional<llvm::DenseMap<Atom, Assignment>> getSolution() const {
       return Solution;
     }
 
   private:
-    Result(
-        enum Status SATCheckStatus,
-        std::optional<llvm::DenseMap<AtomicBoolValue *, Assignment>> Solution)
+    Result(Status SATCheckStatus,
+           std::optional<llvm::DenseMap<Atom, Assignment>> Solution)
         : SATCheckStatus(SATCheckStatus), Solution(std::move(Solution)) {}
 
     Status SATCheckStatus;
-    std::optional<llvm::DenseMap<AtomicBoolValue *, Assignment>> Solution;
+    std::optional<llvm::DenseMap<Atom, Assignment>> Solution;
   };
 
   virtual ~Solver() = default;
 
   /// Checks if the conjunction of `Vals` is satisfiable and returns the
   /// corresponding result.
   ///
   /// Requirements:
   ///
   ///  All elements in `Vals` must not be null.
-  virtual Result solve(llvm::ArrayRef<BoolValue *> Vals) = 0;
-
-  LLVM_DEPRECATED("Pass ArrayRef for determinism", "")
-  virtual Result solve(llvm::DenseSet<BoolValue *> Vals) {
-    return solve(ArrayRef(std::vector<BoolValue *>(Vals.begin(), Vals.end())));
-  }
+  virtual Result solve(llvm::ArrayRef<const Formula *> Vals) = 0;
 };
 
+llvm::raw_ostream &operator<<(llvm::raw_ostream &, const Solver::Result &);
+llvm::raw_ostream &operator<<(llvm::raw_ostream &, Solver::Result::Assignment);
+
 } // namespace dataflow
 } // namespace clang
 
 #endif // LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_SOLVER_H

clang/include/clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h

 //===- WatchedLiteralsSolver.h ----------------------------------*- 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
 //
 //===----------------------------------------------------------------------===//
 //
 //  This file defines a SAT solver implementation that can be used by dataflow
 //  analyses.
 //
 //===----------------------------------------------------------------------===//
 
 #ifndef LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_WATCHEDLITERALSSOLVER_H
 #define LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_WATCHEDLITERALSSOLVER_H
 
+#include "clang/Analysis/FlowSensitive/Formula.h"
 #include "clang/Analysis/FlowSensitive/Solver.h"
-#include "clang/Analysis/FlowSensitive/Value.h"
 #include "llvm/ADT/ArrayRef.h"
 #include <limits>
 
 namespace clang {
 namespace dataflow {
 
 /// A SAT solver that is an implementation of Algorithm D from Knuth's The Art
 /// of Computer Programming Volume 4: Satisfiability, Fascicle 6. It is based on
public:
 
   // `Work` specifies a computational limit on the solver. Units of "work"
   // roughly correspond to attempts to assign a value to a single
   // variable. Since the algorithm is exponential in the number of variables,
   // this is the most direct (abstract) unit to target.
   explicit WatchedLiteralsSolver(std::int64_t WorkLimit)
       : MaxIterations(WorkLimit) {}
 
-  Result solve(llvm::ArrayRef<BoolValue *> Vals) override;
+  Result solve(llvm::ArrayRef<const Formula *> Vals) override;
 };
 
 } // namespace dataflow
 } // namespace clang
 
 #endif // LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_WATCHEDLITERALSSOLVER_H

clang/lib/Analysis/FlowSensitive/Arena.cpp

 IntegerValue &Arena::makeIntLiteral(llvm::APInt Value) {
   auto [It, Inserted] = IntegerLiterals.try_emplace(Value, nullptr);
 
   if (Inserted)
     It->second = &create<IntegerValue>();
   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

clang/lib/Analysis/FlowSensitive/CMakeLists.txt

 add_clang_library(clangAnalysisFlowSensitive
   Arena.cpp
   ControlFlowContext.cpp
   DataflowAnalysisContext.cpp
   DataflowEnvironment.cpp
+  Formula.cpp
   HTMLLogger.cpp
   Logger.cpp
   RecordOps.cpp
   Transfer.cpp
   TypeErasedDataflowAnalysis.cpp
   Value.cpp
   WatchedLiteralsSolver.cpp
   DebugSupport.cpp

clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp

 //  encompass the state of a program and stores context that is used during
 //  dataflow analysis.
 //
 //===----------------------------------------------------------------------===//
 
 #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"
 #include "llvm/ADT/SetVector.h"
 #include "llvm/Support/CommandLine.h"
 #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,
     llvm::cl::desc("Emit log of dataflow analysis. With no arg, writes textual "
                    "log to stderr. With an arg, writes HTML logs under the "
                    "specified directory (one per analyzed function)."));
 
 namespace clang {
addFlowConditionConstraint(
       Token, arena().makeOr(FirstToken, SecondToken));
   return Token;
 }
 
 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,
                                                    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
for (AtomicBoolValue *DepToken : DepsIt->second) {
       addTransitiveFlowConditionConstraints(*DepToken, Constraints,
                                             VisitedTokens);
     }
   }
 }
 
 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 *
 DataflowAnalysisContext::getControlFlowContext(const FunctionDecl *F) {
   // Canonicalize the key:
   F = F->getDefinition();
   if (F == nullptr)
     return nullptr;

clang/lib/Analysis/FlowSensitive/DebugSupport.cpp

 //
 //===----------------------------------------------------------------------===//
 
 #include <utility>
 
 #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:
     return "Integer";
   case Value::Kind::Reference:
     return "Reference";
   case Value::Kind::Pointer:
     return "Pointer";
llvm::StringRef debugString(Value::Kind Kind) {
   case Value::Kind::Implication:
     return "Implication";
   case Value::Kind::Biconditional:
     return "Biconditional";
   }
   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");
 }
 
 llvm::StringRef debugString(Solver::Result::Status Status) {
   switch (Status) {
   case Solver::Result::Status::Satisfiable:
     return "Satisfiable";
   case Solver::Result::Status::Unsatisfiable:
     return "Unsatisfiable";
   case Solver::Result::Status::TimedOut:
     return "TimedOut";
   }
   llvm_unreachable("Unhandled SAT check result status");
 }
 
-namespace {
-
-class DebugStringGenerator {
-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()));
-  }
-
-  /// 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);
+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";
+  return OS;
 }
 
 } // namespace dataflow
 } // namespace clang

clang/lib/Analysis/FlowSensitive/Formula.cpp

+//===- 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

clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp

 //===----------------------------------------------------------------------===//
 
 #include <cassert>
 #include <cstdint>
 #include <iterator>
 #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"
 #include "llvm/ADT/DenseSet.h"
 #include "llvm/ADT/STLExtras.h"
 
 namespace clang {
 namespace dataflow {

 /// Clause identifiers are represented as positive integers.
 using ClauseID = uint32_t;
 
 /// A null clause identifier is used as a placeholder in various data structures
 /// and algorithms.
 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;
 
   /// Literals of all clauses in the formula.
   ///
   /// The element at index 0 stands for the literal in the null clause. It is
   /// set to 0 and isn't used. Literals of clauses in the formula start from the
struct CNFFormula {
   /// Maps clause identifiers (elements of the vector) to identifiers of other
   /// clauses that watch the same literals, forming a set of linked lists.
   ///
   /// The element at index 0 stands for the identifier of the clause that
   /// follows the null clause. It is set to 0 and isn't used. Identifiers of
   /// 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);
     NextWatched.push_back(0);
     const size_t NumLiterals = 2 * LargestVar + 1;
     WatchedHead.resize(NumLiterals + 1, 0);
   }
 
   /// Adds the `L1 v L2 v L3` clause to the formula. If `L2` or `L3` are
   /// `NullLit` they are respectively omitted from the clause.
   ///
   /// Requirements:
   ///
   ///  `L1` must not be `NullLit`.
   ///
   ///  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));
 
     const ClauseID C = ClauseStarts.size();
     const size_t S = Clauses.size();
     ClauseStarts.push_back(S);
 
     Clauses.push_back(L1);
struct CNFFormula {
   /// Returns the literals of clause `C`.
   llvm::ArrayRef<Literal> clauseLiterals(ClauseID C) const {
     return llvm::ArrayRef<Literal>(&Clauses[ClauseStarts[C]], clauseSize(C));
   }
 };
 
 /// 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);
 
     if (ProcessedSubVals[Var])
       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());
-      }
-    } else if (auto *D = dyn_cast<DisjunctionValue>(Val)) {
-      const Variable LeftSubVar = GetVar(&D->getLeftSubValue());
-      const Variable RightSubVar = GetVar(&D->getRightSubValue());
+        CNF.addClause(negLit(Var), posLit(LHS));
+        CNF.addClause(negLit(Var), posLit(RHS));
+        CNF.addClause(posLit(Var), negLit(LHS), negLit(RHS));
+      }
+      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));
+      break;
+    }
+    case Formula::Not: {
+      const Variable Operand = GetVar(Val->operands()[0]);
 
-      // 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 <=> !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());
+      // 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 (LeftSubVar == RightSubVar) {
+      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 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`
   /// (inclusive). The current level is stored in `Level`. At each level the
   /// solver will assign a value to an unassigned variable. If this leads to a
   /// consistent partial assignment, `Level` will be incremented. Otherwise, if
   /// it results in a conflict, the solver will backtrack by decrementing
   /// `Level` until it reaches the most recent level where a decision was made.
class WatchedLiteralsSolverImpl {
   /// element at index 1.
   std::vector<Assignment> VarAssignments;
 
   /// A set of unassigned variables that appear in watched literals in
   /// `Formula`. The vector is guaranteed to contain unique elements.
   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
     // `reverseForcedMoves` we don't have to check that `Level >= 0` on each
     // iteration.
     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);
     }
   }
 
   // Returns the `Result` and the number of iterations "remaining" from
   // `MaxIterations` (that is, `MaxIterations` - iterations in this call).
   std::pair<Solver::Result, std::int64_t> solve(std::int64_t MaxIterations) && {
     size_t I = 0;
     while (I < ActiveVars.size()) {
       if (MaxIterations == 0)
         return std::make_pair(Solver::Result::TimedOut(), 0);
       --MaxIterations;
 
       // Assert that the following invariants hold:
       // 1. All active variables are unassigned.
       // 2. All active variables form watched literals.
       // 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());
 
       const Variable ActiveVar = ActiveVars[I];
 
       // Look for unit clauses that contain the active variable.
       const bool unitPosLit = watchedByUnitClause(posLit(ActiveVar));
while (I < ActiveVars.size()) {
       } else {
         ++I;
       }
     }
     return std::make_pair(Solver::Result::Satisfiable(buildSolution()), MaxIterations);
   }
 
 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.
       Solution[Atomic.second] =
           VarAssignments[Atomic.first] == Assignment::AssignedFalse
               ? Solver::Result::Assignment::AssignedFalse
               : Solver::Result::Assignment::AssignedTrue;
     }
private:
   void updateWatchedLiterals() {
     const Variable Var = LevelVars[Level];
 
     // Update the watched literals of clauses that currently watch the literal
     // that falsifies `Var`.
     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.
       if (!isWatched(NewWatchedLit) && !isWatched(notLit(NewWatchedLit)) &&
           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;
     }
   }
 
   /// 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))
         return true;
     }
     return false;
   }
 
   /// Returns true if and only if `Clause` is a unit clause.
   bool isUnit(llvm::ArrayRef<Literal> Clause) const {
     return llvm::all_of(Clause.drop_front(),
                         [this](Literal L) { return isCurrentlyFalse(L); });
   }
 
   /// Returns true if and only if `Lit` evaluates to `false` in the current
   /// partial assignment.
   bool isCurrentlyFalse(Literal Lit) const {
     return static_cast<int8_t>(VarAssignments[var(Lit)]) ==
            static_cast<int8_t>(Lit & 1);
   }
 
   /// 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.
   Assignment decideAssignment(Variable Var) const {
     return !isWatched(posLit(Var)) || isWatched(negLit(Var))
                ? Assignment::AssignedFalse
                : Assignment::AssignedTrue;
   }
 
   /// 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);
     }
     return WatchedLiterals;
   }
 
   /// Returns true if and only if all active variables are unassigned.
   bool activeVarsAreUnassigned() const {
for (Literal Lit : watchedLiterals()) {
       if (ActiveVarsSet.contains(Var))
         continue;
       return false;
     }
     return true;
   }
 };
 
-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] =
       WatchedLiteralsSolverImpl(Vals).solve(MaxIterations);
   MaxIterations = Iterations;
   return Res;
 }
 
 } // namespace dataflow
 } // namespace clang

clang/unittests/Analysis/FlowSensitive/ArenaTest.cpp

 //===- ArenaTest.cpp ------------------------------------------------------===//
 //
 // 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/Arena.h"
+#include "llvm/Support/ScopedPrinter.h"
 #include "gmock/gmock.h"
 #include "gtest/gtest.h"
 
 namespace clang::dataflow {
 namespace {
 
 class ArenaTest : public ::testing::Test {
 protected:
TEST_F(ArenaTest, GetOrCreateIffReturnsSameExprOnSubsequentCalls) {
   auto &YIffX = A.makeEquals(Y, X);
   EXPECT_EQ(&XIffY1, &YIffX);
 
   auto &Z = A.create<AtomicBoolValue>();
   auto &XIffZ = A.makeEquals(X, Z);
   EXPECT_NE(&XIffY1, &XIffZ);
 }
 
+TEST_F(ArenaTest, ValueToFormula) {
+  auto &X = A.create<AtomicBoolValue>();
+  auto &Y = A.create<AtomicBoolValue>();
+  auto &XIffY = A.makeEquals(X, Y);
+  auto &XOrNotY = A.makeOr(X, A.makeNot(Y));
+  auto &Implies = A.makeImplies(XIffY, XOrNotY);
+
+  EXPECT_EQ(llvm::to_string(A.getFormula(Implies)),
+            "((V0 = V1) => (V0 | !V1))");
+}
+
+TEST_F(ArenaTest, ValueToFormulaCached) {
+  auto &X = A.create<AtomicBoolValue>();
+  auto &Y = A.create<AtomicBoolValue>();
+  auto &XIffY = A.makeEquals(X, Y);
+
+  auto &Formula1 = A.getFormula(XIffY);
+  auto &Formula2 = A.getFormula(XIffY);
+  EXPECT_EQ(&Formula1, &Formula2);
+}
+
 } // namespace
 } // namespace clang::dataflow

clang/unittests/Analysis/FlowSensitive/DebugSupportTest.cpp

 //===- unittests/Analysis/FlowSensitive/DebugSupportTest.cpp --------------===//
 //
 // 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/DebugSupport.h"
 #include "TestingSupport.h"
-#include "clang/Analysis/FlowSensitive/Value.h"
-#include "clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h"
+#include "clang/Analysis/FlowSensitive/Formula.h"
+#include "llvm/Support/ScopedPrinter.h"
+#include "llvm/Support/raw_ostream.h"
 #include "gmock/gmock.h"
 #include "gtest/gtest.h"
 
 namespace {
 
 using namespace clang;
 using namespace dataflow;
 
 using test::ConstraintContext;
 using testing::StrEq;
 
 TEST(BoolValueDebugStringTest, AtomicBoolean) {
-  // B0
   ConstraintContext Ctx;
   auto B = Ctx.atom();
 
-  auto Expected = R"(B0)";
-  EXPECT_THAT(debugString(*B), StrEq(Expected));
-}
-
-TEST(BoolValueDebugStringTest, Top) {
-  ConstraintContext Ctx;
-  auto B = Ctx.top();
-
-  auto Expected = R"(top)";
-  EXPECT_THAT(debugString(*B), StrEq(Expected));
+  auto Expected = "V0";
+  EXPECT_THAT(llvm::to_string(*B), StrEq(Expected));
 }
 
 TEST(BoolValueDebugStringTest, Negation) {
-  // !B0
   ConstraintContext Ctx;
   auto B = Ctx.neg(Ctx.atom());
 
-  auto Expected = R"((not
-    B0))";
-  EXPECT_THAT(debugString(*B), StrEq(Expected));
+  auto Expected = "!V0";
+  EXPECT_THAT(llvm::to_string(*B), StrEq(Expected));
 }
 
 TEST(BoolValueDebugStringTest, Conjunction) {
-  // B0 ^ B1
   ConstraintContext Ctx;
   auto B = Ctx.conj(Ctx.atom(), Ctx.atom());
 
-  auto Expected = R"((and
-    B0
-    B1))";
-  EXPECT_THAT(debugString(*B), StrEq(Expected));
+  auto Expected = "(V0 & V1)";
+  EXPECT_THAT(llvm::to_string(*B), StrEq(Expected));
 }
 
 TEST(BoolValueDebugStringTest, Disjunction) {
-  // B0 v B1
   ConstraintContext Ctx;
   auto B = Ctx.disj(Ctx.atom(), Ctx.atom());
 
-  auto Expected = R"((or
-    B0
-    B1))";
-  EXPECT_THAT(debugString(*B), StrEq(Expected));
+  auto Expected = "(V0 | V1)";
+  EXPECT_THAT(llvm::to_string(*B), StrEq(Expected));
 }
 
 TEST(BoolValueDebugStringTest, Implication) {
-  // B0 => B1
   ConstraintContext Ctx;
   auto B = Ctx.impl(Ctx.atom(), Ctx.atom());
 
-  auto Expected = R"((=>
-    B0
-    B1))";
-  EXPECT_THAT(debugString(*B), StrEq(Expected));
+  auto Expected = "(V0 => V1)";
+  EXPECT_THAT(llvm::to_string(*B), StrEq(Expected));
 }
 
 TEST(BoolValueDebugStringTest, Iff) {
-  // B0 <=> B1
   ConstraintContext Ctx;
   auto B = Ctx.iff(Ctx.atom(), Ctx.atom());
 
-  auto Expected = R"((=
-    B0
-    B1))";
-  EXPECT_THAT(debugString(*B), StrEq(Expected));
+  auto Expected = "(V0 = V1)";
+  EXPECT_THAT(llvm::to_string(*B), StrEq(Expected));
 }
 
 TEST(BoolValueDebugStringTest, Xor) {
-  // (B0 ^ !B1) V (!B0 ^ B1)
   ConstraintContext Ctx;
   auto B0 = Ctx.atom();
   auto B1 = Ctx.atom();
   auto B = Ctx.disj(Ctx.conj(B0, Ctx.neg(B1)), Ctx.conj(Ctx.neg(B0), B1));
 
-  auto Expected = R"((or
-    (and
-        B0
-        (not
-            B1))
-    (and
-        (not
-            B0)
-        B1)))";
-  EXPECT_THAT(debugString(*B), StrEq(Expected));
+  auto Expected = "((V0 & !V1) | (!V0 & V1))";
+  EXPECT_THAT(llvm::to_string(*B), StrEq(Expected));
 }
 
 TEST(BoolValueDebugStringTest, NestedBoolean) {
-  // B0 ^ (B1 v (B2 ^ (B3 v B4)))
   ConstraintContext Ctx;
   auto B = Ctx.conj(
       Ctx.atom(),
       Ctx.disj(Ctx.atom(),
                Ctx.conj(Ctx.atom(), Ctx.disj(Ctx.atom(), Ctx.atom()))));
 
-  auto Expected = R"((and
-    B0
-    (or
-        B1
-        (and
-            B2
-            (or
-                B3
-                B4)))))";
-  EXPECT_THAT(debugString(*B), StrEq(Expected));
-}
-
-TEST(BoolValueDebugStringTest, AtomicBooleanWithName) {
-  // True
-  ConstraintContext Ctx;
-  auto True = cast<AtomicBoolValue>(Ctx.atom());
-  auto B = True;
-
-  auto Expected = R"(True)";
-  EXPECT_THAT(debugString(*B, {{True, "True"}}), StrEq(Expected));
-}
-
-TEST(BoolValueDebugStringTest, ComplexBooleanWithNames) {
-  // (Cond ^ Then ^ !Else) v (!Cond ^ !Then ^ Else)
-  ConstraintContext Ctx;
-  auto Cond = cast<AtomicBoolValue>(Ctx.atom());
-  auto Then = cast<AtomicBoolValue>(Ctx.atom());
-  auto Else = cast<AtomicBoolValue>(Ctx.atom());
-  auto B = Ctx.disj(Ctx.conj(Cond, Ctx.conj(Then, Ctx.neg(Else))),
-                    Ctx.conj(Ctx.neg(Cond), Ctx.conj(Ctx.neg(Then), Else)));
-
-  auto Expected = R"((or
-    (and
-        Cond
-        (and
-            Then
-            (not
-                Else)))
-    (and
-        (not
-            Cond)
-        (and
-            (not
-                Then)
-            Else))))";
-  EXPECT_THAT(debugString(*B, {{Cond, "Cond"}, {Then, "Then"}, {Else, "Else"}}),
-              StrEq(Expected));
+  auto Expected = "(V0 & (V1 | (V2 & (V3 | V4))))";
+  EXPECT_THAT(llvm::to_string(*B), StrEq(Expected));
 }
 
 TEST(BoolValueDebugStringTest, ComplexBooleanWithSomeNames) {
-  // (False && B0) v (True v B1)
   ConstraintContext Ctx;
-  auto True = cast<AtomicBoolValue>(Ctx.atom());
-  auto False = cast<AtomicBoolValue>(Ctx.atom());
+  auto True = Ctx.atom();
+  auto False = Ctx.atom();
+  Formula::AtomNames Names;
+  Names[True->getAtom()] = "true";
+  Names[False->getAtom()] = "false";
   auto B = Ctx.disj(Ctx.conj(False, Ctx.atom()), Ctx.disj(True, Ctx.atom()));
 
-  auto Expected = R"((or
-    (and
-        False
-        B0)
-    (or
-        True
-        B1)))";
-  EXPECT_THAT(debugString(*B, {{True, "True"}, {False, "False"}}),
-              StrEq(Expected));
-}
-
-TEST(ConstraintSetDebugStringTest, Empty) {
-  llvm::ArrayRef<BoolValue *> Constraints;
-  EXPECT_THAT(debugString(Constraints), StrEq(""));
-}
-
-TEST(ConstraintSetDebugStringTest, Simple) {
-  ConstraintContext Ctx;
-  std::vector<BoolValue *> Constraints;
-  auto X = cast<AtomicBoolValue>(Ctx.atom());
-  auto Y = cast<AtomicBoolValue>(Ctx.atom());
-  Constraints.push_back(Ctx.disj(X, Y));
-  Constraints.push_back(Ctx.disj(X, Ctx.neg(Y)));
-
-  auto Expected = R"((or
-    X
-    Y)
-(or
-    X
-    (not
-        Y))
-)";
-  EXPECT_THAT(debugString(Constraints, {{X, "X"}, {Y, "Y"}}),
-              StrEq(Expected));
-}
-
-Solver::Result CheckSAT(std::vector<BoolValue *> Constraints) {
-  return WatchedLiteralsSolver().solve(std::move(Constraints));
-}
-
-TEST(SATCheckDebugStringTest, AtomicBoolean) {
-  // B0
-  ConstraintContext Ctx;
-  std::vector<BoolValue *> Constraints({Ctx.atom()});
-  auto Result = CheckSAT(Constraints);
-
-  auto Expected = R"(
-Constraints
-------------
-B0
-------------
-Satisfiable.
-
-B0 = True
-)";
-  EXPECT_THAT(debugString(Constraints, Result), StrEq(Expected));
-}
-
-TEST(SATCheckDebugStringTest, AtomicBooleanAndNegation) {
-  // B0, !B0
-  ConstraintContext Ctx;
-  auto B0 = Ctx.atom();
-  std::vector<BoolValue *> Constraints({B0, Ctx.neg(B0)});
-  auto Result = CheckSAT(Constraints);
-
-  auto Expected = R"(
-Constraints
-------------
-B0
-
-(not
-    B0)
-------------
-Unsatisfiable.
-
-)";
-  EXPECT_THAT(debugString(Constraints, Result), StrEq(Expected));
-}
-
-TEST(SATCheckDebugStringTest, MultipleAtomicBooleans) {
-  // B0, B1
-  ConstraintContext Ctx;
-  std::vector<BoolValue *> Constraints({Ctx.atom(), Ctx.atom()});
-  auto Result = CheckSAT(Constraints);
-
-  auto Expected = R"(
-Constraints
-------------
-B0
-
-B1
-------------
-Satisfiable.
-
-B0 = True
-B1 = True
-)";
-  EXPECT_THAT(debugString(Constraints, Result), StrEq(Expected));
-}
-
-TEST(SATCheckDebugStringTest, Implication) {
-  // B0, B0 => B1
-  ConstraintContext Ctx;
-  auto B0 = Ctx.atom();
-  auto B1 = Ctx.atom();
-  auto Impl = Ctx.disj(Ctx.neg(B0), B1);
-  std::vector<BoolValue *> Constraints({B0, Impl});
-  auto Result = CheckSAT(Constraints);
-
-  auto Expected = R"(
-Constraints
-------------
-B0
-
-(or
-    (not
-        B0)
-    B1)
-------------
-Satisfiable.
-
-B0 = True
-B1 = True
-)";
-  EXPECT_THAT(debugString(Constraints, Result), StrEq(Expected));
-}
-
-TEST(SATCheckDebugStringTest, Iff) {
-  // B0, B0 <=> B1
-  ConstraintContext Ctx;
-  auto B0 = Ctx.atom();
-  auto B1 = Ctx.atom();
-  auto Iff = Ctx.conj(Ctx.disj(Ctx.neg(B0), B1), Ctx.disj(B0, Ctx.neg(B1)));
-  std::vector<BoolValue *> Constraints({B0, Iff});
-  auto Result = CheckSAT(Constraints);
-
-  auto Expected = R"(
-Constraints
-------------
-B0
-
-(and
-    (or
-        (not
-            B0)
-        B1)
-    (or
-        B0
-        (not
-            B1)))
-------------
-Satisfiable.
-
-B0 = True
-B1 = True
-)";
-  EXPECT_THAT(debugString(Constraints, Result), StrEq(Expected));
+  auto Expected = R"(((false & V2) | (true | V3)))";
+  std::string Actual;
+  llvm::raw_string_ostream OS(Actual);
+  B->print(OS, &Names);
+  EXPECT_THAT(Actual, StrEq(Expected));
 }
 
-TEST(SATCheckDebugStringTest, Xor) {
-  // B0, XOR(B0, B1)
-  ConstraintContext Ctx;
-  auto B0 = Ctx.atom();
-  auto B1 = Ctx.atom();
-  auto XOR = Ctx.disj(Ctx.conj(B0, Ctx.neg(B1)), Ctx.conj(Ctx.neg(B0), B1));
-  std::vector<BoolValue *> Constraints({B0, XOR});
-  auto Result = CheckSAT(Constraints);
-
-  auto Expected = R"(
-Constraints
-------------
-B0
-
-(or
-    (and
-        B0
-        (not
-            B1))
-    (and
-        (not
-            B0)
-        B1))
-------------
-Satisfiable.
-
-B0 = True
-B1 = False
-)";
-  EXPECT_THAT(debugString(Constraints, Result), StrEq(Expected));
-}
-
-TEST(SATCheckDebugStringTest, ComplexBooleanWithNames) {
-  // Cond, (Cond ^ Then ^ !Else) v (!Cond ^ !Then ^ Else)
-  ConstraintContext Ctx;
-  auto Cond = cast<AtomicBoolValue>(Ctx.atom());
-  auto Then = cast<AtomicBoolValue>(Ctx.atom());
-  auto Else = cast<AtomicBoolValue>(Ctx.atom());
-  auto B = Ctx.disj(Ctx.conj(Cond, Ctx.conj(Then, Ctx.neg(Else))),
-                    Ctx.conj(Ctx.neg(Cond), Ctx.conj(Ctx.neg(Then), Else)));
-  std::vector<BoolValue *> Constraints({Cond, B});
-  auto Result = CheckSAT(Constraints);
-
-  auto Expected = R"(
-Constraints
-------------
-Cond
-
-(or
-    (and
-        Cond
-        (and
-            Then
-            (not
-                Else)))
-    (and
-        (not
-            Cond)
-        (and
-            (not
-                Then)
-            Else)))
-------------
-Satisfiable.
-
-Cond = True
-Else = False
-Then = True
-)";
-  EXPECT_THAT(debugString(Constraints, Result,
-                          {{Cond, "Cond"}, {Then, "Then"}, {Else, "Else"}}),
-              StrEq(Expected));
-}
-
-TEST(SATCheckDebugStringTest, ComplexBooleanWithLongNames) {
-  // ThisIntEqZero, !IntsAreEq, ThisIntEqZero ^ OtherIntEqZero => IntsAreEq
-  ConstraintContext Ctx;
-  auto IntsAreEq = cast<AtomicBoolValue>(Ctx.atom());
-  auto ThisIntEqZero = cast<AtomicBoolValue>(Ctx.atom());
-  auto OtherIntEqZero = cast<AtomicBoolValue>(Ctx.atom());
-  auto BothZeroImpliesEQ =
-      Ctx.disj(Ctx.neg(Ctx.conj(ThisIntEqZero, OtherIntEqZero)), IntsAreEq);
-  std::vector<BoolValue *> Constraints(
-      {ThisIntEqZero, Ctx.neg(IntsAreEq), BothZeroImpliesEQ});
-  auto Result = CheckSAT(Constraints);
-
-  auto Expected = R"(
-Constraints
-------------
-ThisIntEqZero
-
-(not
-    IntsAreEq)
-
-(or
-    (not
-        (and
-            ThisIntEqZero
-            OtherIntEqZero))
-    IntsAreEq)
-------------
-Satisfiable.
-
-IntsAreEq      = False
-OtherIntEqZero = False
-ThisIntEqZero  = True
-)";
-  EXPECT_THAT(debugString(Constraints, Result,
-                          {{IntsAreEq, "IntsAreEq"},
-                           {ThisIntEqZero, "ThisIntEqZero"},
-                           {OtherIntEqZero, "OtherIntEqZero"}}),
-              StrEq(Expected));
-}
 } // namespace

clang/unittests/Analysis/FlowSensitive/SolverTest.cpp

 //===- unittests/Analysis/FlowSensitive/SolverTest.cpp --------------------===//
 //
 // 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 <utility>
 
 #include "TestingSupport.h"
+#include "clang/Analysis/FlowSensitive/Formula.h"
 #include "clang/Analysis/FlowSensitive/Solver.h"
-#include "clang/Analysis/FlowSensitive/Value.h"
 #include "clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h"
+#include "llvm/ADT/ArrayRef.h"
 #include "gmock/gmock.h"
 #include "gtest/gtest.h"
 
 namespace {
 
 using namespace clang;
 using namespace dataflow;
 
 using test::ConstraintContext;
 using testing::_;
 using testing::AnyOf;
-using testing::IsEmpty;
-using testing::Optional;
 using testing::Pair;
 using testing::UnorderedElementsAre;
 
+constexpr auto AssignedTrue = Solver::Result::Assignment::AssignedTrue;
+constexpr auto AssignedFalse = Solver::Result::Assignment::AssignedFalse;
+
 // Checks if the conjunction of `Vals` is satisfiable and returns the
 // corresponding result.
-Solver::Result solve(llvm::ArrayRef<BoolValue *> Vals) {
+Solver::Result solve(llvm::ArrayRef<const Formula *> Vals) {
   return WatchedLiteralsSolver().solve(Vals);
 }
 
-void expectUnsatisfiable(Solver::Result Result) {
-  EXPECT_EQ(Result.getStatus(), Solver::Result::Status::Unsatisfiable);
-  EXPECT_FALSE(Result.getSolution().has_value());
+MATCHER(unsat, "") {
+  return arg.getStatus() == Solver::Result::Status::Unsatisfiable;
 }
-
-template <typename Matcher>
-void expectSatisfiable(Solver::Result Result, Matcher Solution) {
-  EXPECT_EQ(Result.getStatus(), Solver::Result::Status::Satisfiable);
-  EXPECT_THAT(Result.getSolution(), Optional(Solution));
+MATCHER_P(sat, SolutionMatcher,
+          "is satisfiable, where solution " +
+              (testing::DescribeMatcher<
+                  llvm::DenseMap<Atom, Solver::Result::Assignment>>(
+                  SolutionMatcher))) {
+  if (arg.getStatus() != Solver::Result::Status::Satisfiable)
+    return false;
+  auto Solution = *arg.getSolution();
+  return testing::ExplainMatchResult(SolutionMatcher, Solution,
+                                     result_listener);
 }
 
 TEST(SolverTest, Var) {
   ConstraintContext Ctx;
   auto X = Ctx.atom();
 
   // X
-  expectSatisfiable(
-      solve({X}),
-      UnorderedElementsAre(Pair(X, Solver::Result::Assignment::AssignedTrue)));
+  EXPECT_THAT(solve({X}),
+              sat(UnorderedElementsAre(Pair(X->getAtom(), AssignedTrue))));
 }
 
 TEST(SolverTest, NegatedVar) {
   ConstraintContext Ctx;
   auto X = Ctx.atom();
   auto NotX = Ctx.neg(X);
 
   // !X
-  expectSatisfiable(
-      solve({NotX}),
-      UnorderedElementsAre(Pair(X, Solver::Result::Assignment::AssignedFalse)));
+  EXPECT_THAT(solve({NotX}),
+              sat(UnorderedElementsAre(Pair(X->getAtom(), AssignedFalse))));
 }
 
 TEST(SolverTest, UnitConflict) {
   ConstraintContext Ctx;
   auto X = Ctx.atom();
   auto NotX = Ctx.neg(X);
 
   // X ^ !X
-  expectUnsatisfiable(solve({X, NotX}));
+  EXPECT_THAT(solve({X, NotX}), unsat());
 }
 
 TEST(SolverTest, DistinctVars) {
   ConstraintContext Ctx;
   auto X = Ctx.atom();
   auto Y = Ctx.atom();
   auto NotY = Ctx.neg(Y);
 
   // X ^ !Y
-  expectSatisfiable(
-      solve({X, NotY}),
-      UnorderedElementsAre(Pair(X, Solver::Result::Assignment::AssignedTrue),
-                           Pair(Y, Solver::Result::Assignment::AssignedFalse)));
-}
-
-TEST(SolverTest, Top) {
-  ConstraintContext Ctx;
-  auto X = Ctx.top();
-
-  // X. Since Top is anonymous, we do not get any results in the solution.
-  expectSatisfiable(solve({X}), IsEmpty());
-}
-
-TEST(SolverTest, NegatedTop) {
-  ConstraintContext Ctx;
-  auto X = Ctx.top();
-
-  // !X
-  expectSatisfiable(solve({Ctx.neg(X)}), IsEmpty());
-}
-
-TEST(SolverTest, DistinctTops) {
-  ConstraintContext Ctx;
-  auto X = Ctx.top();
-  auto Y = Ctx.top();
-  auto NotY = Ctx.neg(Y);
-
-  // X ^ !Y
-  expectSatisfiable(solve({X, NotY}), IsEmpty());
+  EXPECT_THAT(solve({X, NotY}),
+              sat(UnorderedElementsAre(Pair(X->getAtom(), AssignedTrue),
+                                       Pair(Y->getAtom(), AssignedFalse))));
 }
 
 TEST(SolverTest, DoubleNegation) {
   ConstraintContext Ctx;
   auto X = Ctx.atom();
   auto NotX = Ctx.neg(X);
   auto NotNotX = Ctx.neg(NotX);
 
   // !!X ^ !X
-  expectUnsatisfiable(solve({NotNotX, NotX}));
+  EXPECT_THAT(solve({NotNotX, NotX}), unsat());
 }
 
 TEST(SolverTest, NegatedDisjunction) {
   ConstraintContext Ctx;
   auto X = Ctx.atom();
   auto Y = Ctx.atom();
   auto XOrY = Ctx.disj(X, Y);
   auto NotXOrY = Ctx.neg(XOrY);
 
   // !(X v Y) ^ (X v Y)
-  expectUnsatisfiable(solve({NotXOrY, XOrY}));
+  EXPECT_THAT(solve({NotXOrY, XOrY}), unsat());
 }
 
 TEST(SolverTest, NegatedConjunction) {
   ConstraintContext Ctx;
   auto X = Ctx.atom();
   auto Y = Ctx.atom();
   auto XAndY = Ctx.conj(X, Y);
   auto NotXAndY = Ctx.neg(XAndY);
 
   // !(X ^ Y) ^ (X ^ Y)
-  expectUnsatisfiable(solve({NotXAndY, XAndY}));
+  EXPECT_THAT(solve({NotXAndY, XAndY}), unsat());
 }
 
 TEST(SolverTest, DisjunctionSameVarWithNegation) {
   ConstraintContext Ctx;
   auto X = Ctx.atom();
   auto NotX = Ctx.neg(X);
   auto XOrNotX = Ctx.disj(X, NotX);
 
   // X v !X
-  expectSatisfiable(solve({XOrNotX}), _);
+  EXPECT_THAT(solve({XOrNotX}), sat(_));
 }
 
 TEST(SolverTest, DisjunctionSameVar) {
   ConstraintContext Ctx;
   auto X = Ctx.atom();
   auto XOrX = Ctx.disj(X, X);
 
   // X v X
-  expectSatisfiable(solve({XOrX}), _);
+  EXPECT_THAT(solve({XOrX}), sat(_));
 }
 
 TEST(SolverTest, ConjunctionSameVarsConflict) {
   ConstraintContext Ctx;
   auto X = Ctx.atom();
   auto NotX = Ctx.neg(X);
   auto XAndNotX = Ctx.conj(X, NotX);
 
   // X ^ !X
-  expectUnsatisfiable(solve({XAndNotX}));
+  EXPECT_THAT(solve({XAndNotX}), unsat());
 }
 
 TEST(SolverTest, ConjunctionSameVar) {
   ConstraintContext Ctx;
   auto X = Ctx.atom();
   auto XAndX = Ctx.conj(X, X);
 
   // X ^ X
-  expectSatisfiable(solve({XAndX}), _);
+  EXPECT_THAT(solve({XAndX}), sat(_));
 }
 
 TEST(SolverTest, PureVar) {
   ConstraintContext Ctx;
   auto X = Ctx.atom();
   auto Y = Ctx.atom();
   auto NotX = Ctx.neg(X);
   auto NotXOrY = Ctx.disj(NotX, Y);
   auto NotY = Ctx.neg(Y);
   auto NotXOrNotY = Ctx.disj(NotX, NotY);
 
   // (!X v Y) ^ (!X v !Y)
-  expectSatisfiable(
-      solve({NotXOrY, NotXOrNotY}),
-      UnorderedElementsAre(Pair(X, Solver::Result::Assignment::AssignedFalse),
-                           Pair(Y, _)));
+  EXPECT_THAT(solve({NotXOrY, NotXOrNotY}),
+              sat(UnorderedElementsAre(Pair(X->getAtom(), AssignedFalse),
+                                       Pair(Y->getAtom(), _))));
 }
 
 TEST(SolverTest, MustAssumeVarIsFalse) {
   ConstraintContext Ctx;
   auto X = Ctx.atom();
   auto Y = Ctx.atom();
   auto XOrY = Ctx.disj(X, Y);
   auto NotX = Ctx.neg(X);
   auto NotXOrY = Ctx.disj(NotX, Y);
   auto NotY = Ctx.neg(Y);
   auto NotXOrNotY = Ctx.disj(NotX, NotY);
 
   // (X v Y) ^ (!X v Y) ^ (!X v !Y)
-  expectSatisfiable(
-      solve({XOrY, NotXOrY, NotXOrNotY}),
-      UnorderedElementsAre(Pair(X, Solver::Result::Assignment::AssignedFalse),
-                           Pair(Y, Solver::Result::Assignment::AssignedTrue)));
+  EXPECT_THAT(solve({XOrY, NotXOrY, NotXOrNotY}),
+              sat(UnorderedElementsAre(Pair(X->getAtom(), AssignedFalse),
+                                       Pair(Y->getAtom(), AssignedTrue))));
 }
 
 TEST(SolverTest, DeepConflict) {
   ConstraintContext Ctx;
   auto X = Ctx.atom();
   auto Y = Ctx.atom();
   auto XOrY = Ctx.disj(X, Y);
   auto NotX = Ctx.neg(X);
   auto NotXOrY = Ctx.disj(NotX, Y);
   auto NotY = Ctx.neg(Y);
   auto NotXOrNotY = Ctx.disj(NotX, NotY);
   auto XOrNotY = Ctx.disj(X, NotY);
 
   // (X v Y) ^ (!X v Y) ^ (!X v !Y) ^ (X v !Y)
-  expectUnsatisfiable(solve({XOrY, NotXOrY, NotXOrNotY, XOrNotY}));
+  EXPECT_THAT(solve({XOrY, NotXOrY, NotXOrNotY, XOrNotY}), unsat());
 }
 
 TEST(SolverTest, IffIsEquivalentToDNF) {
   ConstraintContext Ctx;
   auto X = Ctx.atom();
   auto Y = Ctx.atom();
   auto NotX = Ctx.neg(X);
   auto NotY = Ctx.neg(Y);
   auto XIffY = Ctx.iff(X, Y);
   auto XIffYDNF = Ctx.disj(Ctx.conj(X, Y), Ctx.conj(NotX, NotY));
   auto NotEquivalent = Ctx.neg(Ctx.iff(XIffY, XIffYDNF));
 
   // !((X <=> Y) <=> ((X ^ Y) v (!X ^ !Y)))
-  expectUnsatisfiable(solve({NotEquivalent}));
+  EXPECT_THAT(solve({NotEquivalent}), unsat());
 }
 
 TEST(SolverTest, IffSameVars) {
   ConstraintContext Ctx;
   auto X = Ctx.atom();
   auto XEqX = Ctx.iff(X, X);
 
   // X <=> X
-  expectSatisfiable(solve({XEqX}), _);
+  EXPECT_THAT(solve({XEqX}), sat(_));
 }
 
 TEST(SolverTest, IffDistinctVars) {
   ConstraintContext Ctx;
   auto X = Ctx.atom();
   auto Y = Ctx.atom();
   auto XEqY = Ctx.iff(X, Y);
 
   // X <=> Y
-  expectSatisfiable(
+  EXPECT_THAT(
       solve({XEqY}),
-      AnyOf(UnorderedElementsAre(
-                Pair(X, Solver::Result::Assignment::AssignedTrue),
-                Pair(Y, Solver::Result::Assignment::AssignedTrue)),
-            UnorderedElementsAre(
-                Pair(X, Solver::Result::Assignment::AssignedFalse),
-                Pair(Y, Solver::Result::Assignment::AssignedFalse))));
+      sat(AnyOf(UnorderedElementsAre(Pair(X->getAtom(), AssignedTrue),
+                                     Pair(Y->getAtom(), AssignedTrue)),
+                UnorderedElementsAre(Pair(X->getAtom(), AssignedFalse),
+                                     Pair(Y->getAtom(), AssignedFalse)))));
 }
 
 TEST(SolverTest, IffWithUnits) {
   ConstraintContext Ctx;
   auto X = Ctx.atom();
   auto Y = Ctx.atom();
   auto XEqY = Ctx.iff(X, Y);
 
   // (X <=> Y) ^ X ^ Y
-  expectSatisfiable(
-      solve({XEqY, X, Y}),
-      UnorderedElementsAre(Pair(X, Solver::Result::Assignment::AssignedTrue),
-                           Pair(Y, Solver::Result::Assignment::AssignedTrue)));
+  EXPECT_THAT(solve({XEqY, X, Y}),
+              sat(UnorderedElementsAre(Pair(X->getAtom(), AssignedTrue),
+                                       Pair(Y->getAtom(), AssignedTrue))));
 }
 
 TEST(SolverTest, IffWithUnitsConflict) {
   ConstraintContext Ctx;
   auto X = Ctx.atom();
   auto Y = Ctx.atom();
   auto XEqY = Ctx.iff(X, Y);
   auto NotY = Ctx.neg(Y);
 
   // (X <=> Y) ^ X  !Y
-  expectUnsatisfiable(solve({XEqY, X, NotY}));
+  EXPECT_THAT(solve({XEqY, X, NotY}), unsat());
 }
 
 TEST(SolverTest, IffTransitiveConflict) {
   ConstraintContext Ctx;
   auto X = Ctx.atom();
   auto Y = Ctx.atom();
   auto Z = Ctx.atom();
   auto XEqY = Ctx.iff(X, Y);
   auto YEqZ = Ctx.iff(Y, Z);
   auto NotX = Ctx.neg(X);
 
   // (X <=> Y) ^ (Y <=> Z) ^ Z ^ !X
-  expectUnsatisfiable(solve({XEqY, YEqZ, Z, NotX}));
+  EXPECT_THAT(solve({XEqY, YEqZ, Z, NotX}), unsat());
 }
 
 TEST(SolverTest, DeMorgan) {
   ConstraintContext Ctx;
   auto X = Ctx.atom();
   auto Y = Ctx.atom();
   auto Z = Ctx.atom();
   auto W = Ctx.atom();
 
   // !(X v Y) <=> !X ^ !Y
   auto A = Ctx.iff(Ctx.neg(Ctx.disj(X, Y)), Ctx.conj(Ctx.neg(X), Ctx.neg(Y)));
 
   // !(Z ^ W) <=> !Z v !W
   auto B = Ctx.iff(Ctx.neg(Ctx.conj(Z, W)), Ctx.disj(Ctx.neg(Z), Ctx.neg(W)));
 
   // A ^ B
-  expectSatisfiable(solve({A, B}), _);
+  EXPECT_THAT(solve({A, B}), sat(_));
 }
 
 TEST(SolverTest, RespectsAdditionalConstraints) {
   ConstraintContext Ctx;
   auto X = Ctx.atom();
   auto Y = Ctx.atom();
   auto XEqY = Ctx.iff(X, Y);
   auto NotY = Ctx.neg(Y);
 
   // (X <=> Y) ^ X ^ !Y
-  expectUnsatisfiable(solve({XEqY, X, NotY}));
+  EXPECT_THAT(solve({XEqY, X, NotY}), unsat());
 }
 
 TEST(SolverTest, ImplicationIsEquivalentToDNF) {
   ConstraintContext Ctx;
   auto X = Ctx.atom();
   auto Y = Ctx.atom();
   auto XImpliesY = Ctx.impl(X, Y);
   auto XImpliesYDNF = Ctx.disj(Ctx.neg(X), Y);
   auto NotEquivalent = Ctx.neg(Ctx.iff(XImpliesY, XImpliesYDNF));
 
   // !((X => Y) <=> (!X v Y))
-  expectUnsatisfiable(solve({NotEquivalent}));
+  EXPECT_THAT(solve({NotEquivalent}), unsat());
 }
 
 TEST(SolverTest, ImplicationConflict) {
   ConstraintContext Ctx;
   auto X = Ctx.atom();
   auto Y = Ctx.atom();
   auto *XImplY = Ctx.impl(X, Y);
   auto *XAndNotY = Ctx.conj(X, Ctx.neg(Y));
 
   // X => Y ^ X ^ !Y
-  expectUnsatisfiable(solve({XImplY, XAndNotY}));
+  EXPECT_THAT(solve({XImplY, XAndNotY}), unsat());
 }
 
 TEST(SolverTest, LowTimeoutResultsInTimedOut) {
   WatchedLiteralsSolver solver(10);
   ConstraintContext Ctx;
   auto X = Ctx.atom();
   auto Y = Ctx.atom();
   auto Z = Ctx.atom();

clang/unittests/Analysis/FlowSensitive/TestingSupport.h

 #include "clang/Basic/LLVM.h"
 #include "clang/Serialization/PCHContainerOperations.h"
 #include "clang/Tooling/ArgumentsAdjusters.h"
 #include "clang/Tooling/Tooling.h"
 #include "llvm/ADT/ArrayRef.h"
 #include "llvm/ADT/DenseMap.h"
 #include "llvm/ADT/StringMap.h"
 #include "llvm/ADT/StringRef.h"
+#include "llvm/Support/Allocator.h"
 #include "llvm/Support/Errc.h"
 #include "llvm/Support/Error.h"
 #include "llvm/Testing/Annotations/Annotations.h"
 
 namespace clang {
 namespace dataflow {
 
 // Requires a `<<` operator for the `Lattice` type.
ValueT &getValueForDecl(ASTContext &ASTCtx, const Environment &Env,
                         llvm::StringRef Name) {
   const ValueDecl *VD = findValueDecl(ASTCtx, Name);
   assert(VD != nullptr);
   return *cast<ValueT>(Env.getValue(*VD));
 }
 
 /// Creates and owns constraints which are boolean values.
 class ConstraintContext {
-public:
-  // Creates an atomic boolean value.
-  BoolValue *atom() {
-    Vals.push_back(std::make_unique<AtomicBoolValue>());
-    return Vals.back().get();
-  }
+  unsigned NextAtom = 0;
+  llvm::BumpPtrAllocator A;
 
-  // Creates an instance of the Top boolean value.
-  BoolValue *top() {
-    Vals.push_back(std::make_unique<TopBoolValue>());
-    return Vals.back().get();
+  const Formula *make(Formula::Kind K,
+                      llvm::ArrayRef<const Formula *> Operands) {
+    return &Formula::create(A, K, Operands);
   }
 
-  // Creates a boolean conjunction value.
-  BoolValue *conj(BoolValue *LeftSubVal, BoolValue *RightSubVal) {
-    Vals.push_back(
-        std::make_unique<ConjunctionValue>(*LeftSubVal, *RightSubVal));
-    return Vals.back().get();
+public:
+  // Returns a reference to a fresh atomic variable.
+  const Formula *atom() {
+    return &Formula::create(A, Formula::AtomRef, {}, NextAtom++);
   }
 
-  // Creates a boolean disjunction value.
-  BoolValue *disj(BoolValue *LeftSubVal, BoolValue *RightSubVal) {
-    Vals.push_back(
-        std::make_unique<DisjunctionValue>(*LeftSubVal, *RightSubVal));
-    return Vals.back().get();
+  // Creates a boolean conjunction.
+  const Formula *conj(const Formula *LHS, const Formula *RHS) {
+    return make(Formula::And, {LHS, RHS});
   }
 
-  // Creates a boolean negation value.
-  BoolValue *neg(BoolValue *SubVal) {
-    Vals.push_back(std::make_unique<NegationValue>(*SubVal));
-    return Vals.back().get();
+  // Creates a boolean disjunction.
+  const Formula *disj(const Formula *LHS, const Formula *RHS) {
+    return make(Formula::Or, {LHS, RHS});
   }
 
-  // Creates a boolean implication value.
-  BoolValue *impl(BoolValue *LeftSubVal, BoolValue *RightSubVal) {
-    Vals.push_back(
-        std::make_unique<ImplicationValue>(*LeftSubVal, *RightSubVal));
-    return Vals.back().get();
+  // Creates a boolean negation.
+  const Formula *neg(const Formula *Operand) {
+    return make(Formula::Not, {Operand});
   }
 
-  // Creates a boolean biconditional value.
-  BoolValue *iff(BoolValue *LeftSubVal, BoolValue *RightSubVal) {
-    Vals.push_back(
-        std::make_unique<BiconditionalValue>(*LeftSubVal, *RightSubVal));
-    return Vals.back().get();
+  // Creates a boolean implication.
+  const Formula *impl(const Formula *LHS, const Formula *RHS) {
+    return make(Formula::Implies, {LHS, RHS});
   }
 
-private:
-  std::vector<std::unique_ptr<BoolValue>> Vals;
+  // Creates a boolean biconditional.
+  const Formula *iff(const Formula *LHS, const Formula *RHS) {
+    return make(Formula::Equal, {LHS, RHS});
+  }
 };
 
 } // namespace test
 } // namespace dataflow
 } // namespace clang
 
 #endif // LLVM_CLANG_ANALYSIS_FLOW_SENSITIVE_TESTING_SUPPORT_H_