diff --git a/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h b/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
--- a/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
+++ b/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
@@ -17,6 +17,7 @@
 
 #include "clang/AST/Decl.h"
 #include "clang/AST/Expr.h"
+#include "clang/Analysis/FlowSensitive/Solver.h"
 #include "clang/Analysis/FlowSensitive/StorageLocation.h"
 #include "clang/Analysis/FlowSensitive/Value.h"
 #include "llvm/ADT/DenseMap.h"
@@ -33,9 +34,19 @@
 /// is used during dataflow analysis.
 class DataflowAnalysisContext {
 public:
-  DataflowAnalysisContext()
-      : TrueVal(takeOwnership(std::make_unique<AtomicBoolValue>())),
-        FalseVal(takeOwnership(std::make_unique<AtomicBoolValue>())) {}
+  /// Constructs a dataflow analysis context.
+  ///
+  /// Requirements:
+  ///
+  ///  `S` must not be null.
+  DataflowAnalysisContext(std::unique_ptr<Solver> S)
+      : S(std::move(S)), TrueVal(createAtomicBoolValue()),
+        FalseVal(createAtomicBoolValue()) {
+    assert(this->S != nullptr);
+  }
+
+  /// Returns the SAT solver instance that is available in this context.
+  Solver &getSolver() const { return *S; }
 
   /// Takes ownership of `Loc` and returns a reference to it.
   ///
@@ -119,7 +130,30 @@
     return Value ? TrueVal : FalseVal;
   }
 
+  /// Creates an atomic boolean value.
+  AtomicBoolValue &createAtomicBoolValue() {
+    return takeOwnership(std::make_unique<AtomicBoolValue>());
+  }
+
+  /// Returns a boolean value that represents the conjunction of `LHS` and
+  /// `RHS`. Subsequent calls with the same arguments, regardless of their
+  /// order, will return the same result. If the given boolean values represent
+  /// the same value, the result will be the value itself.
+  BoolValue &getOrCreateConjunctionValue(BoolValue &LHS, BoolValue &RHS);
+
+  /// Returns a boolean value that represents the disjunction of `LHS` and
+  /// `RHS`. Subsequent calls with the same arguments, regardless of their
+  /// order, will return the same result. If the given boolean values represent
+  /// the same value, the result will be the value itself.
+  BoolValue &getOrCreateDisjunctionValue(BoolValue &LHS, BoolValue &RHS);
+
+  /// Returns a boolean value that represents the negation of `Val`. Subsequent
+  /// calls with the same argument will return the same result.
+  BoolValue &getOrCreateNegationValue(BoolValue &Val);
+
 private:
+  std::unique_ptr<Solver> S;
+
   // Storage for the state of a program.
   std::vector<std::unique_ptr<StorageLocation>> Locs;
   std::vector<std::unique_ptr<Value>> Vals;
@@ -134,9 +168,16 @@
 
   StorageLocation *ThisPointeeLoc = nullptr;
 
-  // FIXME: Add support for boolean expressions.
   AtomicBoolValue &TrueVal;
   AtomicBoolValue &FalseVal;
+
+  // Indices that are used to avoid recreating the same composite boolean
+  // values.
+  llvm::DenseMap<std::pair<BoolValue *, BoolValue *>, ConjunctionValue *>
+      ConjunctionVals;
+  llvm::DenseMap<std::pair<BoolValue *, BoolValue *>, DisjunctionValue *>
+      DisjunctionVals;
+  llvm::DenseMap<BoolValue *, NegationValue *> NegationVals;
 };
 
 } // namespace dataflow
diff --git a/clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h b/clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h
--- a/clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h
+++ b/clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h
@@ -235,6 +235,56 @@
     return DACtx->getBoolLiteralValue(Value);
   }
 
+  /// Returns an atomic boolean value.
+  BoolValue &makeAtomicBoolValue() { return DACtx->createAtomicBoolValue(); }
+
+  /// Returns a boolean value that represents the conjunction of `LHS` and
+  /// `RHS`. Subsequent calls with the same arguments, regardless of their
+  /// order, will return the same result. If the given boolean values represent
+  /// the same value, the result will be the value itself.
+  BoolValue &makeAnd(BoolValue &LHS, BoolValue &RHS) {
+    return DACtx->getOrCreateConjunctionValue(LHS, RHS);
+  }
+
+  /// Returns a boolean value that represents the disjunction of `LHS` and
+  /// `RHS`. Subsequent calls with the same arguments, regardless of their
+  /// order, will return the same result. If the given boolean values represent
+  /// the same value, the result will be the value itself.
+  BoolValue &makeOr(BoolValue &LHS, BoolValue &RHS) {
+    return DACtx->getOrCreateDisjunctionValue(LHS, RHS);
+  }
+
+  /// Returns a boolean value that represents the negation of `Val`. Subsequent
+  /// calls with the same argument will return the same result.
+  BoolValue &makeNot(BoolValue &Val) {
+    return DACtx->getOrCreateNegationValue(Val);
+  }
+
+  /// Returns a boolean value represents `LHS` => `RHS`. Subsequent calls with
+  /// the same arguments, regardless of their order, will return the same
+  /// result. If the given boolean values represent the same value, the result
+  /// will be a value that represents the true boolean literal.
+  BoolValue &makeImplication(BoolValue &LHS, BoolValue &RHS) {
+    return &LHS == &RHS ? getBoolLiteralValue(true) : makeOr(makeNot(LHS), RHS);
+  }
+
+  /// Returns a boolean value represents `LHS` <=> `RHS`. Subsequent calls with
+  /// the same arguments, regardless of their order, will return the same
+  /// result. If the given boolean values represent the same value, the result
+  /// will be a value that represents the true boolean literal.
+  BoolValue &makeIff(BoolValue &LHS, BoolValue &RHS) {
+    return &LHS == &RHS
+               ? getBoolLiteralValue(true)
+               : makeAnd(makeImplication(LHS, RHS), makeImplication(RHS, LHS));
+  }
+
+  /// Adds `Val` to the set of clauses that constitute the flow condition.
+  void addToFlowCondition(BoolValue &Val);
+
+  /// Returns true if and only if the clauses that constitute the flow condition
+  /// imply that `Val` is true.
+  bool flowConditionImplies(BoolValue &Val);
+
 private:
   /// Creates a value appropriate for `Type`, if `Type` is supported, otherwise
   /// return null.
@@ -272,7 +322,7 @@
                  std::pair<StructValue *, const ValueDecl *>>
       MemberLocToStruct;
 
-  // FIXME: Add flow condition constraints.
+  llvm::DenseSet<BoolValue *> FlowConditionConstraints;
 };
 
 } // namespace dataflow
diff --git a/clang/lib/Analysis/FlowSensitive/CMakeLists.txt b/clang/lib/Analysis/FlowSensitive/CMakeLists.txt
--- a/clang/lib/Analysis/FlowSensitive/CMakeLists.txt
+++ b/clang/lib/Analysis/FlowSensitive/CMakeLists.txt
@@ -1,5 +1,6 @@
 add_clang_library(clangAnalysisFlowSensitive
   ControlFlowContext.cpp
+  DataflowAnalysisContext.cpp
   DataflowEnvironment.cpp
   Transfer.cpp
   TypeErasedDataflowAnalysis.cpp
diff --git a/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp b/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
new file mode 100644
--- /dev/null
+++ b/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
@@ -0,0 +1,68 @@
+//===-- DataflowAnalysisContext.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
+//
+//===----------------------------------------------------------------------===//
+//
+//  This file defines a DataflowAnalysisContext class that owns objects that
+//  encompass the state of a program and stores context that is used during
+//  dataflow analysis.
+//
+//===----------------------------------------------------------------------===//
+
+#include "clang/Analysis/FlowSensitive/DataflowAnalysisContext.h"
+#include "clang/Analysis/FlowSensitive/Value.h"
+#include <cassert>
+#include <memory>
+#include <utility>
+
+namespace clang {
+namespace dataflow {
+
+static std::pair<BoolValue *, BoolValue *>
+makeCanonicalBoolValuePair(BoolValue &LHS, BoolValue &RHS) {
+  auto Res = std::make_pair(&LHS, &RHS);
+  if (&RHS < &LHS)
+    std::swap(Res.first, Res.second);
+  return Res;
+}
+
+BoolValue &
+DataflowAnalysisContext::getOrCreateConjunctionValue(BoolValue &LHS,
+                                                     BoolValue &RHS) {
+  if (&LHS == &RHS)
+    return LHS;
+
+  auto Res = ConjunctionVals.try_emplace(makeCanonicalBoolValuePair(LHS, RHS),
+                                         nullptr);
+  if (Res.second)
+    Res.first->second =
+        &takeOwnership(std::make_unique<ConjunctionValue>(LHS, RHS));
+  return *Res.first->second;
+}
+
+BoolValue &
+DataflowAnalysisContext::getOrCreateDisjunctionValue(BoolValue &LHS,
+                                                     BoolValue &RHS) {
+  if (&LHS == &RHS)
+    return LHS;
+
+  auto Res = DisjunctionVals.try_emplace(makeCanonicalBoolValuePair(LHS, RHS),
+                                         nullptr);
+  if (Res.second)
+    Res.first->second =
+        &takeOwnership(std::make_unique<DisjunctionValue>(LHS, RHS));
+  return *Res.first->second;
+}
+
+BoolValue &DataflowAnalysisContext::getOrCreateNegationValue(BoolValue &Val) {
+  auto Res = NegationVals.try_emplace(&Val, nullptr);
+  if (Res.second)
+    Res.first->second = &takeOwnership(std::make_unique<NegationValue>(Val));
+  return *Res.first->second;
+}
+
+} // namespace dataflow
+} // namespace clang
diff --git a/clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp b/clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp
--- a/clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp
+++ b/clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp
@@ -453,5 +453,24 @@
   return skip(*const_cast<StorageLocation *>(&Loc), SP);
 }
 
+void Environment::addToFlowCondition(BoolValue &Val) {
+  FlowConditionConstraints.insert(&Val);
+}
+
+bool Environment::flowConditionImplies(BoolValue &Val) {
+  // Returns true if and only if truth assignment of the flow condition implies
+  // that `Val` is also true. We prove whether or not this property holds by
+  // reducing the problem to satisfiability checking. In other words, we attempt
+  // to show that assuming `Val` is false makes the constraints induced by the
+  // flow condition unsatisfiable.
+  llvm::DenseSet<BoolValue *> Constraints = {
+      &makeNot(Val), &getBoolLiteralValue(true),
+      &makeNot(getBoolLiteralValue(false))};
+  Constraints.insert(FlowConditionConstraints.begin(),
+                     FlowConditionConstraints.end());
+  return DACtx->getSolver().solve(std::move(Constraints)) ==
+         Solver::Result::Unsatisfiable;
+}
+
 } // namespace dataflow
 } // namespace clang
diff --git a/clang/unittests/Analysis/FlowSensitive/CMakeLists.txt b/clang/unittests/Analysis/FlowSensitive/CMakeLists.txt
--- a/clang/unittests/Analysis/FlowSensitive/CMakeLists.txt
+++ b/clang/unittests/Analysis/FlowSensitive/CMakeLists.txt
@@ -4,6 +4,8 @@
   )
 
 add_clang_unittest(ClangAnalysisFlowSensitiveTests
+  DataflowAnalysisContextTest.cpp
+  DataflowEnvironmentTest.cpp
   MapLatticeTest.cpp
   MultiVarConstantPropagationTest.cpp
   SingleVarConstantPropagationTest.cpp
diff --git a/clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp b/clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp
new file mode 100644
--- /dev/null
+++ b/clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp
@@ -0,0 +1,93 @@
+//===- unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.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/DataflowAnalysisContext.h"
+#include "clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h"
+#include "gmock/gmock.h"
+#include "gtest/gtest.h"
+#include <memory>
+
+namespace {
+
+using namespace clang;
+using namespace dataflow;
+
+class DataflowAnalysisContextTest : public ::testing::Test {
+protected:
+  DataflowAnalysisContextTest()
+      : Context(std::make_unique<WatchedLiteralsSolver>()) {}
+
+  DataflowAnalysisContext Context;
+};
+
+TEST_F(DataflowAnalysisContextTest,
+       CreateAtomicBoolValueReturnsDistinctValues) {
+  auto &X = Context.createAtomicBoolValue();
+  auto &Y = Context.createAtomicBoolValue();
+  EXPECT_NE(&X, &Y);
+}
+
+TEST_F(DataflowAnalysisContextTest,
+       GetOrCreateConjunctionValueReturnsSameExprGivenSameArgs) {
+  auto &X = Context.createAtomicBoolValue();
+  auto &XAndX = Context.getOrCreateConjunctionValue(X, X);
+  EXPECT_EQ(&XAndX, &X);
+}
+
+TEST_F(DataflowAnalysisContextTest,
+       GetOrCreateConjunctionValueReturnsSameExprOnSubsequentCalls) {
+  auto &X = Context.createAtomicBoolValue();
+  auto &Y = Context.createAtomicBoolValue();
+  auto &XAndY1 = Context.getOrCreateConjunctionValue(X, Y);
+  auto &XAndY2 = Context.getOrCreateConjunctionValue(X, Y);
+  EXPECT_EQ(&XAndY1, &XAndY2);
+
+  auto &YAndX = Context.getOrCreateConjunctionValue(Y, X);
+  EXPECT_EQ(&XAndY1, &YAndX);
+
+  auto &Z = Context.createAtomicBoolValue();
+  auto &XAndZ = Context.getOrCreateConjunctionValue(X, Z);
+  EXPECT_NE(&XAndY1, &XAndZ);
+}
+
+TEST_F(DataflowAnalysisContextTest,
+       GetOrCreateDisjunctionValueReturnsSameExprGivenSameArgs) {
+  auto &X = Context.createAtomicBoolValue();
+  auto &XOrX = Context.getOrCreateDisjunctionValue(X, X);
+  EXPECT_EQ(&XOrX, &X);
+}
+
+TEST_F(DataflowAnalysisContextTest,
+       GetOrCreateDisjunctionValueReturnsSameExprOnSubsequentCalls) {
+  auto &X = Context.createAtomicBoolValue();
+  auto &Y = Context.createAtomicBoolValue();
+  auto &XOrY1 = Context.getOrCreateDisjunctionValue(X, Y);
+  auto &XOrY2 = Context.getOrCreateDisjunctionValue(X, Y);
+  EXPECT_EQ(&XOrY1, &XOrY2);
+
+  auto &YOrX = Context.getOrCreateDisjunctionValue(Y, X);
+  EXPECT_EQ(&XOrY1, &YOrX);
+
+  auto &Z = Context.createAtomicBoolValue();
+  auto &XOrZ = Context.getOrCreateDisjunctionValue(X, Z);
+  EXPECT_NE(&XOrY1, &XOrZ);
+}
+
+TEST_F(DataflowAnalysisContextTest,
+       GetOrCreateNegationValueReturnsSameExprOnSubsequentCalls) {
+  auto &X = Context.createAtomicBoolValue();
+  auto &NotX1 = Context.getOrCreateNegationValue(X);
+  auto &NotX2 = Context.getOrCreateNegationValue(X);
+  EXPECT_EQ(&NotX1, &NotX2);
+
+  auto &Y = Context.createAtomicBoolValue();
+  auto &NotY = Context.getOrCreateNegationValue(Y);
+  EXPECT_NE(&NotX1, &NotY);
+}
+
+} // namespace
diff --git a/clang/unittests/Analysis/FlowSensitive/DataflowEnvironmentTest.cpp b/clang/unittests/Analysis/FlowSensitive/DataflowEnvironmentTest.cpp
new file mode 100644
--- /dev/null
+++ b/clang/unittests/Analysis/FlowSensitive/DataflowEnvironmentTest.cpp
@@ -0,0 +1,57 @@
+//===- unittests/Analysis/FlowSensitive/DataflowEnvironmentTest.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/DataflowEnvironment.h"
+#include "clang/Analysis/FlowSensitive/DataflowAnalysisContext.h"
+#include "clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h"
+#include "gmock/gmock.h"
+#include "gtest/gtest.h"
+#include <memory>
+
+namespace {
+
+using namespace clang;
+using namespace dataflow;
+
+class EnvironmentTest : public ::testing::Test {
+  DataflowAnalysisContext Context;
+
+protected:
+  EnvironmentTest()
+      : Context(std::make_unique<WatchedLiteralsSolver>()), Env(Context) {}
+
+  Environment Env;
+};
+
+TEST_F(EnvironmentTest, MakeImplicationReturnsTrueGivenSameArgs) {
+  auto &X = Env.makeAtomicBoolValue();
+  auto &XEqX = Env.makeImplication(X, X);
+  EXPECT_EQ(&XEqX, &Env.getBoolLiteralValue(true));
+}
+
+TEST_F(EnvironmentTest, MakeIffReturnsTrueGivenSameArgs) {
+  auto &X = Env.makeAtomicBoolValue();
+  auto &XEqX = Env.makeIff(X, X);
+  EXPECT_EQ(&XEqX, &Env.getBoolLiteralValue(true));
+}
+
+TEST_F(EnvironmentTest, FlowCondition) {
+  EXPECT_TRUE(Env.flowConditionImplies(Env.getBoolLiteralValue(true)));
+  EXPECT_FALSE(Env.flowConditionImplies(Env.getBoolLiteralValue(false)));
+
+  auto &X = Env.makeAtomicBoolValue();
+  EXPECT_FALSE(Env.flowConditionImplies(X));
+
+  Env.addToFlowCondition(X);
+  EXPECT_TRUE(Env.flowConditionImplies(X));
+
+  auto &NotX = Env.makeNot(X);
+  EXPECT_FALSE(Env.flowConditionImplies(NotX));
+}
+
+} // namespace
diff --git a/clang/unittests/Analysis/FlowSensitive/TestingSupport.h b/clang/unittests/Analysis/FlowSensitive/TestingSupport.h
--- a/clang/unittests/Analysis/FlowSensitive/TestingSupport.h
+++ b/clang/unittests/Analysis/FlowSensitive/TestingSupport.h
@@ -23,6 +23,7 @@
 #include "clang/Analysis/FlowSensitive/ControlFlowContext.h"
 #include "clang/Analysis/FlowSensitive/DataflowAnalysis.h"
 #include "clang/Analysis/FlowSensitive/DataflowEnvironment.h"
+#include "clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h"
 #include "clang/Basic/LLVM.h"
 #include "clang/Serialization/PCHContainerOperations.h"
 #include "clang/Tooling/ArgumentsAdjusters.h"
@@ -104,7 +105,7 @@
   if (!CFCtx)
     return CFCtx.takeError();
 
-  DataflowAnalysisContext DACtx;
+  DataflowAnalysisContext DACtx(std::make_unique<WatchedLiteralsSolver>());
   Environment Env(DACtx, *F);
   auto Analysis = MakeAnalysis(Context, Env);
 
diff --git a/clang/unittests/Analysis/FlowSensitive/TypeErasedDataflowAnalysisTest.cpp b/clang/unittests/Analysis/FlowSensitive/TypeErasedDataflowAnalysisTest.cpp
--- a/clang/unittests/Analysis/FlowSensitive/TypeErasedDataflowAnalysisTest.cpp
+++ b/clang/unittests/Analysis/FlowSensitive/TypeErasedDataflowAnalysisTest.cpp
@@ -18,6 +18,7 @@
 #include "clang/Analysis/FlowSensitive/DataflowEnvironment.h"
 #include "clang/Analysis/FlowSensitive/DataflowLattice.h"
 #include "clang/Analysis/FlowSensitive/Value.h"
+#include "clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h"
 #include "clang/Tooling/Tooling.h"
 #include "llvm/ADT/Optional.h"
 #include "llvm/ADT/STLExtras.h"
@@ -68,7 +69,7 @@
       ControlFlowContext::build(nullptr, Body, &AST->getASTContext()));
 
   AnalysisT Analysis = MakeAnalysis(AST->getASTContext());
-  DataflowAnalysisContext DACtx;
+  DataflowAnalysisContext DACtx(std::make_unique<WatchedLiteralsSolver>());
   Environment Env(DACtx);
 
   return runDataflowAnalysis(CFCtx, Analysis, Env);