[clang] [Clang] Improve subsumption. (PR #132849)

[Aaron Ballman via cfe-commits]

================
@@ -2001,3 +1932,258 @@ NormalizedConstraint::getFoldExpandedConstraint() const {
          "getFoldExpandedConstraint called on non-fold-expanded constraint.");
   return cast<FoldExpandedConstraint *>(Constraint);
 }
+
+//
+//
+// ------------------------ Subsumption -----------------------------------
+//
+//
+
+template <> struct llvm::DenseMapInfo<llvm::FoldingSetNodeID> {
+
+  static FoldingSetNodeID getEmptyKey() {
+    FoldingSetNodeID ID;
+    ID.AddInteger(std::numeric_limits<unsigned>::max());
+    return ID;
+  }
+
+  static FoldingSetNodeID getTombstoneKey() {
+    FoldingSetNodeID ID;
+    for (unsigned I = 0; I < sizeof(ID) / sizeof(unsigned); ++I) {
+      ID.AddInteger(std::numeric_limits<unsigned>::max());
+    }
+    return ID;
+  }
+
+  static unsigned getHashValue(const FoldingSetNodeID &Val) {
+    return Val.ComputeHash();
+  }
+
+  static bool isEqual(const FoldingSetNodeID &LHS,
+                      const FoldingSetNodeID &RHS) {
+    return LHS == RHS;
+  }
+};
+
+SubsumptionChecker::SubsumptionChecker(Sema &SemaRef,
+                                       SubsumptionCallable Callable)
+    : SemaRef(SemaRef), Callable(Callable), NextID(1) {}
+
+uint16_t SubsumptionChecker::getNewLiteralId() {
+  assert((unsigned(NextID) + 1 < std::numeric_limits<uint16_t>::max()) &&
+         "too many constraints!");
+  return NextID++;
+}
+
+auto SubsumptionChecker::find(AtomicConstraint *Ori) -> Literal {
+  auto &Elems = AtomicMap[Ori->ConstraintExpr];
+  // C++ [temp.constr.order] p2
+  //   - an atomic constraint A subsumes another atomic constraint B
+  //     if and only if the A and B are identical [...]
+  //
+  // C++ [temp.constr.atomic] p2
+  //   Two atomic constraints are identical if they are formed from the
+  //   same expression and the targets of the parameter mappings are
+  //   equivalent according to the rules for expressions [...]
+
+  // Because subsumption of atomic constraints is an identity
+  // relationship that does not require further analysis
+  // We cache the results such that if an atomic constraint literal
+  // subsumes another, their literal will be the same
+
+  llvm::FoldingSetNodeID ID;
+  const auto &Mapping = Ori->ParameterMapping;
+  ID.AddBoolean(Mapping.has_value());
+  if (Mapping) {
+    for (const TemplateArgumentLoc &TAL : *Mapping) {
+      SemaRef.getASTContext()
+          .getCanonicalTemplateArgument(TAL.getArgument())
+          .Profile(ID, SemaRef.getASTContext());
+    }
+  }
+  auto It = Elems.find(ID);
+  if (It == Elems.end()) {
+    It =
+        Elems
+            .insert({ID, MappedAtomicConstraint{Ori, Literal{getNewLiteralId(),
+                                                             Literal::Atomic}}})
+            .first;
+    ReverseMap[It->second.ID.Value] = Ori;
+  }
+  return It->getSecond().ID;
+}
+
+auto SubsumptionChecker::find(FoldExpandedConstraint *Ori) -> Literal {
+  auto &Elems = FoldMap[Ori->Pattern];
+
+  FoldExpendedConstraintKey K;
+  K.Kind = Ori->Kind;
+
+  auto It = llvm::find_if(Elems, [&K](const FoldExpendedConstraintKey &Other) {
+    return K.Kind == Other.Kind;
+  });
+  if (It == Elems.end()) {
+    K.ID = {getNewLiteralId(), Literal::FoldExpanded};
+    It = Elems.insert(Elems.end(), std::move(K));
+    ReverseMap[It->ID.Value] = Ori;
+  }
+  return It->ID;
+}
+
+auto SubsumptionChecker::CNF(const NormalizedConstraint &C) -> CNFFormula {
+  return SubsumptionChecker::Normalize<CNFFormula>(C);
+}
+auto SubsumptionChecker::DNF(const NormalizedConstraint &C) -> DNFFormula {
+  return SubsumptionChecker::Normalize<DNFFormula>(C);
+}
+
+///
+/// \brief SubsumptionChecker::Normalize
+///
+/// Normalize a formula to Conjunctive Normal Form or
+/// Disjunctive normal form.
+///
+/// Each Atomic (and Fold Expanded) constraint gets represented by
+/// a single id to reduce space.
+///
+/// To minimize risks of exponential blow up, if two atomic
+/// constraints subsumes each other (same constraint and mapping),
+/// they are represented by the same literal.
+///
+template <typename FormulaType>
+FormulaType SubsumptionChecker::Normalize(const NormalizedConstraint &NC) {
+  FormulaType Res;
+
+  auto Add = [&, this](Clause C) {
+    // Sort each clause and remove duplicates for faster comparisons
+    llvm::sort(C);
+    C.erase(llvm::unique(C), C.end());
+    AddUniqueClauseToFormula(Res, std::move(C));
+  };
+
+  if (NC.isAtomic())
+    return {{find(NC.getAtomicConstraint())}};
+
+  if (NC.isFoldExpanded())
+    return {{find(NC.getFoldExpandedConstraint())}};
+
+  FormulaType Left, Right;
+  SemaRef.runWithSufficientStackSpace(SourceLocation(), [&] {
+    Left = Normalize<FormulaType>(NC.getLHS());
+    Right = Normalize<FormulaType>(NC.getRHS());
+  });
+
+  if (NC.getCompoundKind() == FormulaType::Kind) {
+    Res = std::move(Left);
+    Res.reserve(Left.size() + Right.size());
+    std::for_each(std::make_move_iterator(Right.begin()),
+                  std::make_move_iterator(Right.end()), Add);
+    return Res;
+  }
+
+  Res.reserve(Left.size() * Right.size());
+  for (const auto &LTransform : Left) {
+    for (const auto &RTransform : Right) {
+      Clause Combined;
+      Combined.reserve(LTransform.size() + RTransform.size());
+      llvm::copy(LTransform, std::back_inserter(Combined));
+      llvm::copy(RTransform, std::back_inserter(Combined));
+      Add(std::move(Combined));
+    }
+  }
+  return Res;
+}
+
+void SubsumptionChecker::AddUniqueClauseToFormula(Formula &F, Clause C) {
+  for (auto &Other : F) {
----------------
AaronBallman wrote:

Could this be better handled via a set interface that keeps the elements unique as opposed to walking the elements each time?

https://github.com/llvm/llvm-project/pull/132849