diff --git a/clang/include/clang/Analysis/FlowSensitive/SimplifyConstraints.h b/clang/include/clang/Analysis/FlowSensitive/SimplifyConstraints.h
new file mode 100644
index 0000000000000..fadb3caf0a4c8
--- /dev/null
+++ b/clang/include/clang/Analysis/FlowSensitive/SimplifyConstraints.h
@@ -0,0 +1,49 @@
+//===-- SimplifyConstraints.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_SIMPLIFYCONSTRAINTS_H
+#define LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_SIMPLIFYCONSTRAINTS_H
+
+#include "clang/Analysis/FlowSensitive/Arena.h"
+#include "clang/Analysis/FlowSensitive/Formula.h"
+#include "llvm/ADT/SetVector.h"
+
+namespace clang {
+namespace dataflow {
+
+/// Information on the way a set of constraints was simplified.
+struct SimplifyConstraintsInfo {
+  /// List of equivalence classes of atoms. For each equivalence class, the
+  /// original constraints imply that all atoms in it must be equivalent.
+  /// Simplification replaces all occurrences of atoms in an equivalence class
+  /// with a single representative atom from the class.
+  /// Does not contain equivalence classes with just one member or atoms
+  /// contained in `TrueAtoms` or `FalseAtoms`.
+  llvm::SmallVector<llvm::SmallVector<Atom>> EquivalentAtoms;
+  /// Atoms that the original constraints imply must be true.
+  /// Simplification replaces all occurrences of these atoms by a true literal
+  /// (which may enable additional simplifications).
+  llvm::SmallVector<Atom> TrueAtoms;
+  /// Atoms that the original constraints imply must be false.
+  /// Simplification replaces all occurrences of these atoms by a false literal
+  /// (which may enable additional simplifications).
+  llvm::SmallVector<Atom> FalseAtoms;
+};
+
+/// Simplifies a set of constraints (implicitly connected by "and") in a way
+/// that does not change satisfiability of the constraints. This does _not_ mean
+/// that the set of solutions is the same before and after simplification.
+/// `Info`, if non-null, will be populated with information about the
+/// simplifications that were made to the formula (e.g. to display to the user).
+void simplifyConstraints(llvm::SetVector<const Formula *> &Constraints,
+                         Arena &arena, SimplifyConstraintsInfo *Info = nullptr);
+
+} // namespace dataflow
+} // namespace clang
+
+#endif // LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_SIMPLIFYCONSTRAINTS_H
diff --git a/clang/lib/Analysis/FlowSensitive/CMakeLists.txt b/clang/lib/Analysis/FlowSensitive/CMakeLists.txt
index 3394c9f0299e4..5af4ecfc9efa5 100644
--- a/clang/lib/Analysis/FlowSensitive/CMakeLists.txt
+++ b/clang/lib/Analysis/FlowSensitive/CMakeLists.txt
@@ -7,6 +7,7 @@ add_clang_library(clangAnalysisFlowSensitive
   HTMLLogger.cpp
   Logger.cpp
   RecordOps.cpp
+  SimplifyConstraints.cpp
   Transfer.cpp
   TypeErasedDataflowAnalysis.cpp
   Value.cpp
diff --git a/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp b/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
index 40de6cdf3a69e..9c15c8756e9dc 100644
--- a/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
+++ b/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
@@ -17,6 +17,7 @@
 #include "clang/Analysis/FlowSensitive/DebugSupport.h"
 #include "clang/Analysis/FlowSensitive/Formula.h"
 #include "clang/Analysis/FlowSensitive/Logger.h"
+#include "clang/Analysis/FlowSensitive/SimplifyConstraints.h"
 #include "clang/Analysis/FlowSensitive/Value.h"
 #include "llvm/ADT/SetOperations.h"
 #include "llvm/ADT/SetVector.h"
@@ -205,13 +206,50 @@ void DataflowAnalysisContext::addTransitiveFlowConditionConstraints(
   }
 }
 
+static void printAtomList(const llvm::SmallVector<Atom> &Atoms,
+                          llvm::raw_ostream &OS) {
+  OS << "(";
+  for (size_t i = 0; i < Atoms.size(); ++i) {
+    OS << Atoms[i];
+    if (i + 1 < Atoms.size())
+      OS << ", ";
+  }
+  OS << ")\n";
+}
+
 void DataflowAnalysisContext::dumpFlowCondition(Atom Token,
                                                 llvm::raw_ostream &OS) {
   llvm::SetVector<const Formula *> Constraints;
   Constraints.insert(&arena().makeAtomRef(Token));
   addTransitiveFlowConditionConstraints(Token, Constraints);
 
-  for (const auto *Constraint : Constraints) {
+  OS << "Flow condition token: " << Token << "\n";
+  SimplifyConstraintsInfo Info;
+  llvm::SetVector<const Formula *> OriginalConstraints = Constraints;
+  simplifyConstraints(Constraints, arena(), &Info);
+  if (!Constraints.empty()) {
+    OS << "Constraints:\n";
+    for (const auto *Constraint : Constraints) {
+      Constraint->print(OS);
+      OS << "\n";
+    }
+  }
+  if (!Info.TrueAtoms.empty()) {
+    OS << "True atoms: ";
+    printAtomList(Info.TrueAtoms, OS);
+  }
+  if (!Info.FalseAtoms.empty()) {
+    OS << "False atoms: ";
+    printAtomList(Info.FalseAtoms, OS);
+  }
+  if (!Info.EquivalentAtoms.empty()) {
+    OS << "Equivalent atoms:\n";
+    for (const llvm::SmallVector<Atom> Class : Info.EquivalentAtoms)
+      printAtomList(Class, OS);
+  }
+
+  OS << "\nFlow condition constraints before simplification:\n";
+  for (const auto *Constraint : OriginalConstraints) {
     Constraint->print(OS);
     OS << "\n";
   }
diff --git a/clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp b/clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp
index cf1e9eb7b1fd7..2b000eb7b3708 100644
--- a/clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp
+++ b/clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp
@@ -961,7 +961,7 @@ void Environment::dump(raw_ostream &OS) const {
     OS << "  [" << L << ", " << V << ": " << *V << "]\n";
   }
 
-  OS << "FlowConditionToken:\n";
+  OS << "\n";
   DACtx->dumpFlowCondition(FlowConditionToken, OS);
 }
 
diff --git a/clang/lib/Analysis/FlowSensitive/SimplifyConstraints.cpp b/clang/lib/Analysis/FlowSensitive/SimplifyConstraints.cpp
new file mode 100644
index 0000000000000..decb928f218a8
--- /dev/null
+++ b/clang/lib/Analysis/FlowSensitive/SimplifyConstraints.cpp
@@ -0,0 +1,179 @@
+//===-- SimplifyConstraints.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/SimplifyConstraints.h"
+#include "llvm/ADT/EquivalenceClasses.h"
+
+namespace clang {
+namespace dataflow {
+
+// Substitutes all occurrences of a given atom in `F` by a given formula and
+// returns the resulting formula.
+static const Formula &
+substitute(const Formula &F,
+           const llvm::DenseMap<Atom, const Formula *> &Substitutions,
+           Arena &arena) {
+  switch (F.kind()) {
+  case Formula::AtomRef:
+    if (auto iter = Substitutions.find(F.getAtom());
+        iter != Substitutions.end())
+      return *iter->second;
+    return F;
+  case Formula::Literal:
+    return F;
+  case Formula::Not:
+    return arena.makeNot(substitute(*F.operands()[0], Substitutions, arena));
+  case Formula::And:
+    return arena.makeAnd(substitute(*F.operands()[0], Substitutions, arena),
+                         substitute(*F.operands()[1], Substitutions, arena));
+  case Formula::Or:
+    return arena.makeOr(substitute(*F.operands()[0], Substitutions, arena),
+                        substitute(*F.operands()[1], Substitutions, arena));
+  case Formula::Implies:
+    return arena.makeImplies(
+        substitute(*F.operands()[0], Substitutions, arena),
+        substitute(*F.operands()[1], Substitutions, arena));
+  case Formula::Equal:
+    return arena.makeEquals(substitute(*F.operands()[0], Substitutions, arena),
+                            substitute(*F.operands()[1], Substitutions, arena));
+  }
+}
+
+// Returns the result of replacing atoms in `Atoms` with the leader of their
+// equivalence class in `EquivalentAtoms`.
+// Atoms that don't have an equivalence class in `EquivalentAtoms` are inserted
+// into it as single-member equivalence classes.
+static llvm::DenseSet<Atom>
+projectToLeaders(const llvm::DenseSet<Atom> &Atoms,
+                 llvm::EquivalenceClasses<Atom> &EquivalentAtoms) {
+  llvm::DenseSet<Atom> Result;
+
+  for (Atom Atom : Atoms)
+    Result.insert(EquivalentAtoms.getOrInsertLeaderValue(Atom));
+
+  return Result;
+}
+
+// Returns the atoms in the equivalence class for the leader identified by
+// `LeaderIt`.
+static llvm::SmallVector<Atom>
+atomsInEquivalenceClass(const llvm::EquivalenceClasses<Atom> &EquivalentAtoms,
+                        llvm::EquivalenceClasses<Atom>::iterator LeaderIt) {
+  llvm::SmallVector<Atom> Result;
+  for (auto MemberIt = EquivalentAtoms.member_begin(LeaderIt);
+       MemberIt != EquivalentAtoms.member_end(); ++MemberIt)
+    Result.push_back(*MemberIt);
+  return Result;
+}
+
+void simplifyConstraints(llvm::SetVector<const Formula *> &Constraints,
+                         Arena &arena, SimplifyConstraintsInfo *Info) {
+  auto contradiction = [&]() {
+    Constraints.clear();
+    Constraints.insert(&arena.makeLiteral(false));
+  };
+
+  llvm::EquivalenceClasses<Atom> EquivalentAtoms;
+  llvm::DenseSet<Atom> TrueAtoms;
+  llvm::DenseSet<Atom> FalseAtoms;
+
+  while (true) {
+    for (const auto *Constraint : Constraints) {
+      switch (Constraint->kind()) {
+      case Formula::AtomRef:
+        TrueAtoms.insert(Constraint->getAtom());
+        break;
+      case Formula::Not:
+        if (Constraint->operands()[0]->kind() == Formula::AtomRef)
+          FalseAtoms.insert(Constraint->operands()[0]->getAtom());
+        break;
+      case Formula::Equal: {
+        ArrayRef<const Formula *> operands = Constraint->operands();
+        if (operands[0]->kind() == Formula::AtomRef &&
+            operands[1]->kind() == Formula::AtomRef) {
+          EquivalentAtoms.unionSets(operands[0]->getAtom(),
+                                    operands[1]->getAtom());
+        }
+        break;
+      }
+      default:
+        break;
+      }
+    }
+
+    TrueAtoms = projectToLeaders(TrueAtoms, EquivalentAtoms);
+    FalseAtoms = projectToLeaders(FalseAtoms, EquivalentAtoms);
+
+    llvm::DenseMap<Atom, const Formula *> Substitutions;
+    for (auto It = EquivalentAtoms.begin(); It != EquivalentAtoms.end(); ++It) {
+      Atom TheAtom = It->getData();
+      Atom Leader = EquivalentAtoms.getLeaderValue(TheAtom);
+      if (TrueAtoms.contains(Leader)) {
+        if (FalseAtoms.contains(Leader)) {
+          contradiction();
+          return;
+        }
+        Substitutions.insert({TheAtom, &arena.makeLiteral(true)});
+      } else if (FalseAtoms.contains(Leader)) {
+        Substitutions.insert({TheAtom, &arena.makeLiteral(false)});
+      } else if (TheAtom != Leader) {
+        Substitutions.insert({TheAtom, &arena.makeAtomRef(Leader)});
+      }
+    }
+
+    llvm::SetVector<const Formula *> NewConstraints;
+    for (const auto *Constraint : Constraints) {
+      const Formula &NewConstraint =
+          substitute(*Constraint, Substitutions, arena);
+      if (&NewConstraint == &arena.makeLiteral(true))
+        continue;
+      if (&NewConstraint == &arena.makeLiteral(false)) {
+        contradiction();
+        return;
+      }
+      if (NewConstraint.kind() == Formula::And) {
+        NewConstraints.insert(NewConstraint.operands()[0]);
+        NewConstraints.insert(NewConstraint.operands()[1]);
+        continue;
+      }
+      NewConstraints.insert(&NewConstraint);
+    }
+
+    if (NewConstraints == Constraints)
+      break;
+    Constraints = std::move(NewConstraints);
+  }
+
+  if (Info) {
+    for (auto It = EquivalentAtoms.begin(), End = EquivalentAtoms.end();
+         It != End; ++It) {
+      if (!It->isLeader())
+        continue;
+      Atom At = *EquivalentAtoms.findLeader(It);
+      if (TrueAtoms.contains(At) || FalseAtoms.contains(At))
+        continue;
+      llvm::SmallVector<Atom> Atoms =
+          atomsInEquivalenceClass(EquivalentAtoms, It);
+      if (Atoms.size() == 1)
+        continue;
+      std::sort(Atoms.begin(), Atoms.end());
+      Info->EquivalentAtoms.push_back(std::move(Atoms));
+    }
+    for (Atom At : TrueAtoms)
+      Info->TrueAtoms.append(atomsInEquivalenceClass(
+          EquivalentAtoms, EquivalentAtoms.findValue(At)));
+    std::sort(Info->TrueAtoms.begin(), Info->TrueAtoms.end());
+    for (Atom At : FalseAtoms)
+      Info->FalseAtoms.append(atomsInEquivalenceClass(
+          EquivalentAtoms, EquivalentAtoms.findValue(At)));
+    std::sort(Info->FalseAtoms.begin(), Info->FalseAtoms.end());
+  }
+}
+
+} // namespace dataflow
+} // namespace clang
diff --git a/clang/unittests/Analysis/FlowSensitive/CMakeLists.txt b/clang/unittests/Analysis/FlowSensitive/CMakeLists.txt
index a9c07d930cdd0..94160d949637c 100644
--- a/clang/unittests/Analysis/FlowSensitive/CMakeLists.txt
+++ b/clang/unittests/Analysis/FlowSensitive/CMakeLists.txt
@@ -17,6 +17,7 @@ add_clang_unittest(ClangAnalysisFlowSensitiveTests
   MultiVarConstantPropagationTest.cpp
   RecordOpsTest.cpp
   SignAnalysisTest.cpp
+  SimplifyConstraintsTest.cpp
   SingleVarConstantPropagationTest.cpp
   SolverTest.cpp
   TestingSupport.cpp
diff --git a/clang/unittests/Analysis/FlowSensitive/SimplifyConstraintsTest.cpp b/clang/unittests/Analysis/FlowSensitive/SimplifyConstraintsTest.cpp
new file mode 100644
index 0000000000000..1f34ae076d5ed
--- /dev/null
+++ b/clang/unittests/Analysis/FlowSensitive/SimplifyConstraintsTest.cpp
@@ -0,0 +1,177 @@
+//===- unittests/Analysis/FlowSensitive/SimplifyConstraintsTest.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/SimplifyConstraints.h"
+#include "TestingSupport.h"
+#include "clang/Analysis/FlowSensitive/Arena.h"
+#include "gmock/gmock.h"
+#include "gtest/gtest.h"
+
+namespace {
+
+using namespace clang;
+using namespace dataflow;
+
+using ::testing::ElementsAre;
+using ::testing::IsEmpty;
+
+class SimplifyConstraintsTest : public ::testing::Test {
+protected:
+  llvm::SetVector<const Formula *> parse(StringRef Lines) {
+    std::vector<const Formula *> formulas = test::parseFormulas(A, Lines);
+    llvm::SetVector<const Formula *> Constraints(formulas.begin(),
+                                                 formulas.end());
+    return Constraints;
+  }
+
+  llvm::SetVector<const Formula *> simplify(StringRef Lines,
+                                            SimplifyConstraintsInfo &Info) {
+    llvm::SetVector<const Formula *> Constraints = parse(Lines);
+    simplifyConstraints(Constraints, A, &Info);
+    return Constraints;
+  }
+
+  Arena A;
+};
+
+void printConstraints(const llvm::SetVector<const Formula *> &Constraints,
+                      raw_ostream &OS) {
+  if (Constraints.empty()) {
+    OS << "empty";
+    return;
+  }
+  for (const auto *Constraint : Constraints) {
+    Constraint->print(OS);
+    OS << "\n";
+  }
+}
+
+std::string
+constraintsToString(const llvm::SetVector<const Formula *> &Constraints) {
+  std::string Str;
+  llvm::raw_string_ostream OS(Str);
+  printConstraints(Constraints, OS);
+  return Str;
+}
+
+MATCHER_P(EqualsConstraints, Constraints,
+          "constraints are: " + constraintsToString(Constraints)) {
+  if (arg == Constraints)
+    return true;
+
+  if (result_listener->stream()) {
+    llvm::raw_os_ostream OS(*result_listener->stream());
+    OS << "constraints are: ";
+    printConstraints(arg, OS);
+  }
+  return false;
+}
+
+TEST_F(SimplifyConstraintsTest, TriviallySatisfiable) {
+  SimplifyConstraintsInfo Info;
+  EXPECT_THAT(simplify(R"(
+     V0
+  )",
+                       Info),
+              EqualsConstraints(parse("")));
+  EXPECT_THAT(Info.EquivalentAtoms, IsEmpty());
+  EXPECT_THAT(Info.TrueAtoms, ElementsAre(Atom(0)));
+  EXPECT_THAT(Info.FalseAtoms, IsEmpty());
+}
+
+TEST_F(SimplifyConstraintsTest, SimpleContradiction) {
+  SimplifyConstraintsInfo Info;
+  EXPECT_THAT(simplify(R"(
+     V0
+     !V0
+  )",
+                       Info),
+              EqualsConstraints(parse("false")));
+  EXPECT_THAT(Info.EquivalentAtoms, IsEmpty());
+  EXPECT_THAT(Info.TrueAtoms, IsEmpty());
+  EXPECT_THAT(Info.FalseAtoms, IsEmpty());
+}
+
+TEST_F(SimplifyConstraintsTest, ContradictionThroughEquivalence) {
+  SimplifyConstraintsInfo Info;
+  EXPECT_THAT(simplify(R"(
+     (V0 = V1)
+     V0
+     !V1
+  )",
+                       Info),
+              EqualsConstraints(parse("false")));
+  EXPECT_THAT(Info.EquivalentAtoms, IsEmpty());
+  EXPECT_THAT(Info.TrueAtoms, IsEmpty());
+  EXPECT_THAT(Info.FalseAtoms, IsEmpty());
+}
+
+TEST_F(SimplifyConstraintsTest, EquivalenceChain) {
+  SimplifyConstraintsInfo Info;
+  EXPECT_THAT(simplify(R"(
+     (V0 | V3)
+     (V1 = V2)
+     (V2 = V3)
+  )",
+                       Info),
+              EqualsConstraints(parse("(V0 | V1)")));
+  EXPECT_THAT(Info.EquivalentAtoms,
+              ElementsAre(ElementsAre(Atom(1), Atom(2), Atom(3))));
+  EXPECT_THAT(Info.TrueAtoms, IsEmpty());
+  EXPECT_THAT(Info.FalseAtoms, IsEmpty());
+}
+
+TEST_F(SimplifyConstraintsTest, TrueAndFalseAtomsSimplifyOtherExpressions) {
+  SimplifyConstraintsInfo Info;
+  EXPECT_THAT(simplify(R"(
+    V0
+    !V1
+    (V0 & (V2 => V3))
+    (V1 | (V4 => V5))
+  )",
+                       Info),
+              EqualsConstraints(parse(R"(
+    (V2 => V3)
+    (V4 => V5)
+  )")));
+  EXPECT_THAT(Info.EquivalentAtoms, IsEmpty());
+  EXPECT_THAT(Info.TrueAtoms, ElementsAre(Atom(0)));
+  EXPECT_THAT(Info.FalseAtoms, ElementsAre(Atom(1)));
+}
+
+TEST_F(SimplifyConstraintsTest, TrueAtomUnlocksEquivalenceChain) {
+  SimplifyConstraintsInfo Info;
+  EXPECT_THAT(simplify(R"(
+     V0
+     (V0 & (V1 = V2))
+     (V0 & (V2 = V3))
+  )",
+                       Info),
+              EqualsConstraints(parse("")));
+  EXPECT_THAT(Info.EquivalentAtoms,
+              ElementsAre(ElementsAre(Atom(1), Atom(2), Atom(3))));
+  EXPECT_THAT(Info.TrueAtoms, ElementsAre(Atom(0)));
+  EXPECT_THAT(Info.FalseAtoms, IsEmpty());
+}
+
+TEST_F(SimplifyConstraintsTest, TopLevelAndSplitIntoMultipleConstraints) {
+  SimplifyConstraintsInfo Info;
+  EXPECT_THAT(simplify(R"(
+     ((V0 => V1) & (V2 => V3))
+  )",
+                       Info),
+              EqualsConstraints(parse(R"(
+    (V0 => V1)
+    (V2 => V3)
+  )")));
+  EXPECT_THAT(Info.EquivalentAtoms, IsEmpty());
+  EXPECT_THAT(Info.TrueAtoms, IsEmpty());
+  EXPECT_THAT(Info.FalseAtoms, IsEmpty());
+}
+
+} // namespace
diff --git a/llvm/utils/gn/secondary/clang/lib/Analysis/FlowSensitive/BUILD.gn b/llvm/utils/gn/secondary/clang/lib/Analysis/FlowSensitive/BUILD.gn
index 60b5e0b449763..e69567c2d9c65 100644
--- a/llvm/utils/gn/secondary/clang/lib/Analysis/FlowSensitive/BUILD.gn
+++ b/llvm/utils/gn/secondary/clang/lib/Analysis/FlowSensitive/BUILD.gn
@@ -32,6 +32,7 @@ static_library("FlowSensitive") {
     "HTMLLogger.cpp",
     "Logger.cpp",
     "RecordOps.cpp",
+    "SimplifyConstraints.cpp",
     "Transfer.cpp",
     "TypeErasedDataflowAnalysis.cpp",
     "Value.cpp",
diff --git a/llvm/utils/gn/secondary/clang/unittests/Analysis/FlowSensitive/BUILD.gn b/llvm/utils/gn/secondary/clang/unittests/Analysis/FlowSensitive/BUILD.gn
index 2fe4fe854c576..df5b4587bf1c1 100644
--- a/llvm/utils/gn/secondary/clang/unittests/Analysis/FlowSensitive/BUILD.gn
+++ b/llvm/utils/gn/secondary/clang/unittests/Analysis/FlowSensitive/BUILD.gn
@@ -31,6 +31,7 @@ unittest("ClangAnalysisFlowSensitiveTests") {
     "MultiVarConstantPropagationTest.cpp",
     "RecordOpsTest.cpp",
     "SignAnalysisTest.cpp",
+    "SimplifyConstraintsTest.cpp",
     "SingleVarConstantPropagationTest.cpp",
     "SolverTest.cpp",
     "TestingSupport.cpp",