[clang][dataflow] Return a solution from the solver when `Constraints` are `Satisfiable`.

[wyt]

Summary

A truth assignment to atomic boolean values which satisfy Constraints will be returned if found by the solver.
This gives us more information which can be helpful for debugging or constructing warning messages.

[gribozavr2]

clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h

273–278

I'd suggest to revert these edits. Vertical alignment that is not supported by an autoformatter isn't sustainable.

[sgatev]

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

46

A solution consists of true/false assignments for all variables. Having an Unassigned option seems confusing. I suggest defining only two values in this enum and translating WatchedLiteralsSolver's internal representation to Solution right before returning it, in buildValAssignment.

51–58

Let's document these members.

[wyt]

Address comments.

[wyt]

Typo fix.

[wyt]

Make scope resolution consistent (Solver:: instead of WatchedLiteralsSolver::).

[gribozavr2]

clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h

278

[sgatev]

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

79

#include "llvm/ADT/DenseMap.h"

clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp

201

Let's create a local Var variable initialized to NextVar and use that here and below, where NextVar - 1 is currently used.

472–473

[wyt]

Address comments.

[wyt]

Fix comment.

[gribozavr2]

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

67

Please use llvm::Optional, we can't use std::optional in LLVM/Clang code yet.

[wyt]

Replace std::optional with llvm::Optional

[wyt]

Remove decomposing declarations which are not available in llvm.

[dyung]

This change is causing a build failure on the Windows PS4 bot, can you please take a look and revert if you need time to investigate?

https://lab.llvm.org/buildbot/#/builders/216/builds/7026

FAILED: tools/clang/lib/Analysis/FlowSensitive/CMakeFiles/obj.clangAnalysisFlowSensitive.dir/WatchedLiteralsSolver.cpp.obj 
C:\PROGRA~2\MICROS~1\2019\BUILDT~1\VC\Tools\MSVC\1429~1.301\bin\Hostx64\x64\cl.exe  /nologo /TP -DGTEST_HAS_RTTI=0 -DUNICODE -D_CRT_NONSTDC_NO_DEPRECATE -D_CRT_NONSTDC_NO_WARNINGS -D_CRT_SECURE_NO_DEPRECATE -D_CRT_SECURE_NO_WARNINGS -D_GNU_SOURCE -D_HAS_EXCEPTIONS=0 -D_SCL_SECURE_NO_DEPRECATE -D_SCL_SECURE_NO_WARNINGS -D_UNICODE -D__STDC_CONSTANT_MACROS -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -Itools\clang\lib\Analysis\FlowSensitive -IC:\buildbot-root\llvm-clang-x86_64-sie-win\llvm-project\clang\lib\Analysis\FlowSensitive -IC:\buildbot-root\llvm-clang-x86_64-sie-win\llvm-project\clang\include -Itools\clang\include -Iinclude -IC:\buildbot-root\llvm-clang-x86_64-sie-win\llvm-project\llvm\include /DWIN32 /D_WINDOWS   /Zc:inline /Zc:__cplusplus /Oi /bigobj /permissive- /W4 -wd4141 -wd4146 -wd4244 -wd4267 -wd4291 -wd4351 -wd4456 -wd4457 -wd4458 -wd4459 -wd4503 -wd4624 -wd4722 -wd4100 -wd4127 -wd4512 -wd4505 -wd4610 -wd4510 -wd4702 -wd4245 -wd4706 -wd4310 -wd4701 -wd4703 -wd4389 -wd4611 -wd4805 -wd4204 -wd4577 -wd4091 -wd4592 -wd4319 -wd4709 -wd4324 -w14062 -we4238 /Gw /MD /O2 /Ob2  /EHs-c- /GR- -UNDEBUG -std:c++14 /showIncludes /Fotools\clang\lib\Analysis\FlowSensitive\CMakeFiles\obj.clangAnalysisFlowSensitive.dir\WatchedLiteralsSolver.cpp.obj /Fdtools\clang\lib\Analysis\FlowSensitive\CMakeFiles\obj.clangAnalysisFlowSensitive.dir\ /FS -c C:\buildbot-root\llvm-clang-x86_64-sie-win\llvm-project\clang\lib\Analysis\FlowSensitive\WatchedLiteralsSolver.cpp
C:\buildbot-root\llvm-clang-x86_64-sie-win\llvm-project\clang\lib\Analysis\FlowSensitive\WatchedLiteralsSolver.cpp(477): error C2429: language feature 'structured bindings' requires compiler flag '/std:c++17'

clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h

private:
 
   /// Adds all constraints of the flow condition identified by `Token` and all
   /// of its transitive dependencies to `Constraints`. `VisitedTokens` is used
   /// to track tokens of flow conditions that were already visited by recursive
   /// calls.
   void addTransitiveFlowConditionConstraints(
       AtomicBoolValue &Token, llvm::DenseSet<BoolValue *> &Constraints,
       llvm::DenseSet<AtomicBoolValue *> &VisitedTokens);
 
-  /// Returns the result of satisfiability checking on `Constraints`.
-  /// Possible return values are:
-  /// - `Satisfiable`: There exists a satisfying assignment for `Constraints`.
-  /// - `Unsatisfiable`: There is no satisfying assignment for `Constraints`.
-  /// - `TimedOut`: The solver gives up on finding a satisfying assignment.
+  /// Returns the outcome of satisfiability checking on `Constraints`.
+  /// Possible outcomes are:
+  /// - `Satisfiable`: A satisfying assignment exists and is returned.
+  /// - `Unsatisfiable`: A satisfying assignment does not exist.
+  /// - `TimedOut`: The search for a satisfying assignment was not completed.
   Solver::Result querySolver(llvm::DenseSet<BoolValue *> Constraints);
 
   /// Returns true if the solver is able to prove that there is no satisfying
   /// assignment for `Constraints`
   bool isUnsatisfiable(llvm::DenseSet<BoolValue *> Constraints) {
-    return querySolver(std::move(Constraints)) == Solver::Result::Unsatisfiable;
+    return querySolver(std::move(Constraints)).getStatus() ==
+           Solver::Result::Status::Unsatisfiable;
   }
 
   /// Returns a boolean value as a result of substituting `Val` and its sub
   /// values based on entries in `SubstitutionsCache`. Intermediate results are
   /// stored in `SubstitutionsCache` to avoid reprocessing values that have
   /// already been visited.
   BoolValue &substituteBoolValue(
       BoolValue &Val,

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

 //  dataflow analyses.
 //
 //===----------------------------------------------------------------------===//
 
 #ifndef LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_SOLVER_H
 #define LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_SOLVER_H
 
 #include "clang/Analysis/FlowSensitive/Value.h"
+#include "llvm/ADT/DenseMap.h"
 #include "llvm/ADT/DenseSet.h"
+#include "llvm/ADT/Optional.h"
 
 namespace clang {
 namespace dataflow {
 
 /// An interface for a SAT solver that can be used by dataflow analyses.
 class Solver {
 public:
-  enum class Result {
+  struct Result {
+    enum class Status {
       /// Indicates that there exists a satisfying assignment for a boolean
       /// formula.
       Satisfiable,
 
-    /// Indicates that there is no satisfying assignment for a boolean formula.
+      /// Indicates that there is no satisfying assignment for a boolean
+      /// formula.
       Unsatisfiable,
 
-    /// Indicates that the solver gave up trying to find a satisfying assignment
-    /// for a boolean formula.
+      /// Indicates that the solver gave up trying to find a satisfying
+      /// assignment for a boolean formula.
       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) {
+      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 Status; }
+
+    /// Returns a truth assignment to boolean values that satisfies the queried
+    /// boolean formula if available. Otherwise, an empty optional is returned.
+    llvm::Optional<llvm::DenseMap<AtomicBoolValue *, Assignment>>
+    getSolution() const {
+      return Solution;
+    }
+
+  private:
+    Result(
+        enum Status Status,
+        llvm::Optional<llvm::DenseMap<AtomicBoolValue *, Assignment>> Solution)
+        : Status(Status), Solution(std::move(Solution)) {}
+
+    Status Status;
+    llvm::Optional<llvm::DenseMap<AtomicBoolValue *, 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.
-  ///
-  /// FIXME: Consider returning a model in case the conjunction of `Vals` is
-  /// satisfiable so that it can be used to generate warning messages.
   virtual Result solve(llvm::DenseSet<BoolValue *> Vals) = 0;
 };
 
 } // namespace dataflow
 } // namespace clang
 
 #endif // LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_SOLVER_H

clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp

struct BooleanFormula {
   /// 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;
 
-  explicit BooleanFormula(Variable LargestVar) : LargestVar(LargestVar) {
+  /// Stores the variable identifier and value location for atomic booleans in
+  /// the formula.
+  llvm::DenseMap<Variable, AtomicBoolValue *> Atomics;
+
+  explicit BooleanFormula(Variable LargestVar,
+                          llvm::DenseMap<Variable, AtomicBoolValue *> 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
BooleanFormula buildBooleanFormula(const llvm::DenseSet<BoolValue *> &Vals) {
   // The general strategy of the algorithm implemented below is to map each
   // of the sub-values in `Vals` to a unique variable and use these variables in
   // the resulting CNF expression to avoid exponential blow up. The number of
   // literals in the resulting formula is guaranteed to be linear in the number
   // of sub-values 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;
   Variable NextVar = 1;
   {
     std::queue<BoolValue *> UnprocessedSubVals;
     for (BoolValue *Val : Vals)
       UnprocessedSubVals.push(Val);
     while (!UnprocessedSubVals.empty()) {
+      Variable Var = NextVar;
       BoolValue *Val = UnprocessedSubVals.front();
       UnprocessedSubVals.pop();
 
-      if (!SubValsToVar.try_emplace(Val, NextVar).second)
+      if (!SubValsToVar.try_emplace(Val, Var).second)
         continue;
       ++NextVar;
 
       // Visit the sub-values of `Val`.
-      if (auto *C = dyn_cast<ConjunctionValue>(Val)) {
+      switch (Val->getKind()) {
+      case Value::Kind::Conjunction: {
+        auto *C = cast<ConjunctionValue>(Val);
         UnprocessedSubVals.push(&C->getLeftSubValue());
         UnprocessedSubVals.push(&C->getRightSubValue());
-      } else if (auto *D = dyn_cast<DisjunctionValue>(Val)) {
+        break;
+      }
+      case Value::Kind::Disjunction: {
+        auto *D = cast<DisjunctionValue>(Val);
         UnprocessedSubVals.push(&D->getLeftSubValue());
         UnprocessedSubVals.push(&D->getRightSubValue());
-      } else if (auto *N = dyn_cast<NegationValue>(Val)) {
+        break;
+      }
+      case Value::Kind::Negation: {
+        auto *N = cast<NegationValue>(Val);
         UnprocessedSubVals.push(&N->getSubVal());
+        break;
+      }
+      case Value::Kind::AtomicBool: {
+        Atomics[Var] = cast<AtomicBoolValue>(Val);
+        break;
+      }
+      default:
+        llvm_unreachable("buildBooleanFormula: unhandled value kind");
       }
     }
   }
 
   auto GetVar = [&SubValsToVar](const BoolValue *Val) {
     auto ValIt = SubValsToVar.find(Val);
     assert(ValIt != SubValsToVar.end());
     return ValIt->second;
   };
 
-  BooleanFormula Formula(NextVar - 1);
+  BooleanFormula Formula(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 conjuncts that represent the mapping between newly-created variables
while (I < ActiveVars.size()) {
 
         // Backtrack and rewind the `Level` until the most recent non-forced
         // assignment.
         reverseForcedMoves();
 
         // If the root level is reached, then all possible assignments lead to
         // a conflict.
         if (Level == 0)
-          return WatchedLiteralsSolver::Result::Unsatisfiable;
+          return Solver::Result::Unsatisfiable();
 
         // Otherwise, take the other branch at the most recent level where a
         // decision was made.
         LevelStates[Level] = State::Forced;
         const Variable Var = LevelVars[Level];
         VarAssignments[Var] = VarAssignments[Var] == Assignment::AssignedTrue
                                   ? Assignment::AssignedFalse
                                   : Assignment::AssignedTrue;
while (I < ActiveVars.size()) {
 
         // This was the last active variable. Repeat the process from the
         // beginning.
         I = 0;
       } else {
         ++I;
       }
     }
-    return WatchedLiteralsSolver::Result::Satisfiable;
+    return Solver::Result::Satisfiable(buildSolution());
   }
 
 private:
-  // Reverses forced moves until the most recent level where a decision was made
-  // on the assignment of a variable.
+  /// 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 [Var, Val] : Formula.Atomics) {
+      // A variable may have a definite true/false assignment, or it may be
+      // unassigned indicating its truth value does not affect the result of
+      // the formula. Unassigned variables are assigned to true as a default.
+      Solution[Val] = VarAssignments[Var] == Assignment::AssignedFalse
+                          ? Solver::Result::Assignment::AssignedFalse
+                          : Solver::Result::Assignment::AssignedTrue;
+    }
+    return Solution;
+  }
+
+  /// Reverses forced moves until the most recent level where a decision was
+  /// made on the assignment of a variable.
   void reverseForcedMoves() {
     for (; LevelStates[Level] == State::Forced; --Level) {
       const Variable Var = LevelVars[Level];
 
       VarAssignments[Var] = Assignment::Unassigned;
 
       // If the variable that we pass through is watched then we add it to the
       // active variables.
       if (isWatched(posLit(Var)) || isWatched(negLit(Var)))
         ActiveVars.push_back(Var);
     }
   }
 
-  // Updates watched literals that are affected by a variable assignment.
+  /// Updates watched literals that are affected by a variable assignment.
   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);
for (Literal Lit : watchedLiterals()) {
         continue;
       return false;
     }
     return true;
   }
 };
 
 Solver::Result WatchedLiteralsSolver::solve(llvm::DenseSet<BoolValue *> Vals) {
-  return Vals.empty() ? WatchedLiteralsSolver::Result::Satisfiable
+  return Vals.empty() ? Solver::Result::Satisfiable({{}})
                       : WatchedLiteralsSolverImpl(Vals).solve();
 }
 
 } // namespace dataflow
 } // namespace clang

clang/unittests/Analysis/FlowSensitive/SolverTest.cpp

 #include <utility>
 #include <vector>
 
 namespace {
 
 using namespace clang;
 using namespace dataflow;
 
+using testing::_;
+using testing::AnyOf;
+using testing::Optional;
+using testing::Pair;
+using testing::UnorderedElementsAre;
+
 class SolverTest : public ::testing::Test {
 protected:
   // Checks if the conjunction of `Vals` is satisfiable and returns the
   // corresponding result.
   Solver::Result solve(llvm::DenseSet<BoolValue *> Vals) {
     return WatchedLiteralsSolver().solve(std::move(Vals));
   }
 
BoolValue *impl(BoolValue *LeftSubVal, BoolValue *RightSubVal) {
     return disj(neg(LeftSubVal), RightSubVal);
   }
 
   // Creates a boolean biconditional value.
   BoolValue *iff(BoolValue *LeftSubVal, BoolValue *RightSubVal) {
     return conj(impl(LeftSubVal, RightSubVal), impl(RightSubVal, LeftSubVal));
   }
 
+  void expectUnsatisfiable(Solver::Result Result) {
+    EXPECT_EQ(Result.getStatus(), Solver::Result::Status::Unsatisfiable);
+    EXPECT_FALSE(Result.getSolution().has_value());
+  }
+
+  template <typename Matcher>
+  void expectSatisfiable(Solver::Result Result, Matcher Solution) {
+    EXPECT_EQ(Result.getStatus(), Solver::Result::Status::Satisfiable);
+    EXPECT_THAT(Result.getSolution(), Optional(Solution));
+  }
+
 private:
   std::vector<std::unique_ptr<BoolValue>> Vals;
 };
 
 TEST_F(SolverTest, Var) {
   auto X = atom();
 
   // X
-  EXPECT_EQ(solve({X}), Solver::Result::Satisfiable);
+  expectSatisfiable(
+      solve({X}),
+      UnorderedElementsAre(Pair(X, Solver::Result::Assignment::AssignedTrue)));
 }
 
 TEST_F(SolverTest, NegatedVar) {
   auto X = atom();
   auto NotX = neg(X);
 
   // !X
-  EXPECT_EQ(solve({NotX}), Solver::Result::Satisfiable);
+  expectSatisfiable(
+      solve({NotX}),
+      UnorderedElementsAre(Pair(X, Solver::Result::Assignment::AssignedFalse)));
 }
 
 TEST_F(SolverTest, UnitConflict) {
   auto X = atom();
   auto NotX = neg(X);
 
   // X ^ !X
-  EXPECT_EQ(solve({X, NotX}), Solver::Result::Unsatisfiable);
+  expectUnsatisfiable(solve({X, NotX}));
 }
 
 TEST_F(SolverTest, DistinctVars) {
   auto X = atom();
   auto Y = atom();
   auto NotY = neg(Y);
 
   // X ^ !Y
-  EXPECT_EQ(solve({X, NotY}), Solver::Result::Satisfiable);
+  expectSatisfiable(
+      solve({X, NotY}),
+      UnorderedElementsAre(Pair(X, Solver::Result::Assignment::AssignedTrue),
+                           Pair(Y, Solver::Result::Assignment::AssignedFalse)));
 }
 
 TEST_F(SolverTest, DoubleNegation) {
   auto X = atom();
   auto NotX = neg(X);
   auto NotNotX = neg(NotX);
 
   // !!X ^ !X
-  EXPECT_EQ(solve({NotNotX, NotX}), Solver::Result::Unsatisfiable);
+  expectUnsatisfiable(solve({NotNotX, NotX}));
 }
 
 TEST_F(SolverTest, NegatedDisjunction) {
   auto X = atom();
   auto Y = atom();
   auto XOrY = disj(X, Y);
   auto NotXOrY = neg(XOrY);
 
   // !(X v Y) ^ (X v Y)
-  EXPECT_EQ(solve({NotXOrY, XOrY}), Solver::Result::Unsatisfiable);
+  expectUnsatisfiable(solve({NotXOrY, XOrY}));
 }
 
 TEST_F(SolverTest, NegatedConjunction) {
   auto X = atom();
   auto Y = atom();
   auto XAndY = conj(X, Y);
   auto NotXAndY = neg(XAndY);
 
   // !(X ^ Y) ^ (X ^ Y)
-  EXPECT_EQ(solve({NotXAndY, XAndY}), Solver::Result::Unsatisfiable);
+  expectUnsatisfiable(solve({NotXAndY, XAndY}));
 }
 
 TEST_F(SolverTest, DisjunctionSameVars) {
   auto X = atom();
   auto NotX = neg(X);
   auto XOrNotX = disj(X, NotX);
 
   // X v !X
-  EXPECT_EQ(solve({XOrNotX}), Solver::Result::Satisfiable);
+  expectSatisfiable(solve({XOrNotX}), _);
 }
 
 TEST_F(SolverTest, ConjunctionSameVarsConflict) {
   auto X = atom();
   auto NotX = neg(X);
   auto XAndNotX = conj(X, NotX);
 
   // X ^ !X
-  EXPECT_EQ(solve({XAndNotX}), Solver::Result::Unsatisfiable);
+  expectUnsatisfiable(solve({XAndNotX}));
 }
 
 TEST_F(SolverTest, PureVar) {
   auto X = atom();
   auto Y = atom();
   auto NotX = neg(X);
   auto NotXOrY = disj(NotX, Y);
   auto NotY = neg(Y);
   auto NotXOrNotY = disj(NotX, NotY);
 
   // (!X v Y) ^ (!X v !Y)
-  EXPECT_EQ(solve({NotXOrY, NotXOrNotY}), Solver::Result::Satisfiable);
+  expectSatisfiable(
+      solve({NotXOrY, NotXOrNotY}),
+      UnorderedElementsAre(Pair(X, Solver::Result::Assignment::AssignedFalse),
+                           Pair(Y, _)));
 }
 
 TEST_F(SolverTest, MustAssumeVarIsFalse) {
   auto X = atom();
   auto Y = atom();
   auto XOrY = disj(X, Y);
   auto NotX = neg(X);
   auto NotXOrY = disj(NotX, Y);
   auto NotY = neg(Y);
   auto NotXOrNotY = disj(NotX, NotY);
 
   // (X v Y) ^ (!X v Y) ^ (!X v !Y)
-  EXPECT_EQ(solve({XOrY, NotXOrY, NotXOrNotY}), Solver::Result::Satisfiable);
+  expectSatisfiable(
+      solve({XOrY, NotXOrY, NotXOrNotY}),
+      UnorderedElementsAre(Pair(X, Solver::Result::Assignment::AssignedFalse),
+                           Pair(Y, Solver::Result::Assignment::AssignedTrue)));
 }
 
 TEST_F(SolverTest, DeepConflict) {
   auto X = atom();
   auto Y = atom();
   auto XOrY = disj(X, Y);
   auto NotX = neg(X);
   auto NotXOrY = disj(NotX, Y);
   auto NotY = neg(Y);
   auto NotXOrNotY = disj(NotX, NotY);
   auto XOrNotY = disj(X, NotY);
 
   // (X v Y) ^ (!X v Y) ^ (!X v !Y) ^ (X v !Y)
-  EXPECT_EQ(solve({XOrY, NotXOrY, NotXOrNotY, XOrNotY}),
-            Solver::Result::Unsatisfiable);
+  expectUnsatisfiable(solve({XOrY, NotXOrY, NotXOrNotY, XOrNotY}));
 }
 
 TEST_F(SolverTest, IffSameVars) {
   auto X = atom();
   auto XEqX = iff(X, X);
 
   // X <=> X
-  EXPECT_EQ(solve({XEqX}), Solver::Result::Satisfiable);
+  expectSatisfiable(solve({XEqX}), _);
 }
 
 TEST_F(SolverTest, IffDistinctVars) {
   auto X = atom();
   auto Y = atom();
   auto XEqY = iff(X, Y);
 
   // X <=> Y
-  EXPECT_EQ(solve({XEqY}), Solver::Result::Satisfiable);
+  expectSatisfiable(
+      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))));
 }
 
 TEST_F(SolverTest, IffWithUnits) {
   auto X = atom();
   auto Y = atom();
   auto XEqY = iff(X, Y);
 
   // (X <=> Y) ^ X ^ Y
-  EXPECT_EQ(solve({XEqY, X, Y}), Solver::Result::Satisfiable);
+  expectSatisfiable(
+      solve({XEqY, X, Y}),
+      UnorderedElementsAre(Pair(X, Solver::Result::Assignment::AssignedTrue),
+                           Pair(Y, Solver::Result::Assignment::AssignedTrue)));
 }
 
 TEST_F(SolverTest, IffWithUnitsConflict) {
   auto X = atom();
   auto Y = atom();
   auto XEqY = iff(X, Y);
   auto NotY = neg(Y);
 
   // (X <=> Y) ^ X  !Y
-  EXPECT_EQ(solve({XEqY, X, NotY}), Solver::Result::Unsatisfiable);
+  expectUnsatisfiable(solve({XEqY, X, NotY}));
 }
 
 TEST_F(SolverTest, IffTransitiveConflict) {
   auto X = atom();
   auto Y = atom();
   auto Z = atom();
   auto XEqY = iff(X, Y);
   auto YEqZ = iff(Y, Z);
   auto NotX = neg(X);
 
   // (X <=> Y) ^ (Y <=> Z) ^ Z ^ !X
-  EXPECT_EQ(solve({XEqY, YEqZ, Z, NotX}), Solver::Result::Unsatisfiable);
+  expectUnsatisfiable(solve({XEqY, YEqZ, Z, NotX}));
 }
 
 TEST_F(SolverTest, DeMorgan) {
   auto X = atom();
   auto Y = atom();
   auto Z = atom();
   auto W = atom();
 
   // !(X v Y) <=> !X ^ !Y
   auto A = iff(neg(disj(X, Y)), conj(neg(X), neg(Y)));
 
   // !(Z ^ W) <=> !Z v !W
   auto B = iff(neg(conj(Z, W)), disj(neg(Z), neg(W)));
 
   // A ^ B
-  EXPECT_EQ(solve({A, B}), Solver::Result::Satisfiable);
+  expectSatisfiable(solve({A, B}), _);
 }
 
 TEST_F(SolverTest, RespectsAdditionalConstraints) {
   auto X = atom();
   auto Y = atom();
   auto XEqY = iff(X, Y);
   auto NotY = neg(Y);
 
   // (X <=> Y) ^ X ^ !Y
-  EXPECT_EQ(solve({XEqY, X, NotY}), Solver::Result::Unsatisfiable);
+  expectUnsatisfiable(solve({XEqY, X, NotY}));
 }
 
 TEST_F(SolverTest, ImplicationConflict) {
   auto X = atom();
   auto Y = atom();
   auto *XImplY = impl(X, Y);
   auto *XAndNotY = conj(X, neg(Y));
 
   // X => Y ^ X ^ !Y
-  EXPECT_EQ(solve({XImplY, XAndNotY}), Solver::Result::Unsatisfiable);
+  expectUnsatisfiable(solve({XImplY, XAndNotY}));
 }
 
 } // namespace