================
@@ -2001,3 +1932,260 @@ 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 (unsigned I = 0, S = Mapping->size(); I < S; ++I) {
+ SemaRef.getASTContext()
+ .getCanonicalTemplateArgument((*Mapping)[I].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
+ std::sort(C.begin(), C.end());
+ C.erase(std::unique(C.begin(), C.end()), 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 <ransform : Left) {
+ for (const auto &RTransform : Right) {
+ Clause Combined;
+ Combined.reserve(LTransform.size() + RTransform.size());
+ std::copy(LTransform.begin(), LTransform.end(),
+ std::back_inserter(Combined));
+ std::copy(RTransform.begin(), RTransform.end(),
+ std::back_inserter(Combined));
+ Add(std::move(Combined));
+ }
+ }
+ return Res;
+}
+
+void SubsumptionChecker::AddUniqueClauseToFormula(Formula &F, Clause C) {
+ for (auto &Other : F) {
+ if (llvm::equal(C, Other))
+ return;
+ }
+ F.push_back(C);
+}
+
+std::optional<bool> SubsumptionChecker::Subsumes(NamedDecl *DP,
+ ArrayRef<const Expr *> P,
+ NamedDecl *DQ,
+ ArrayRef<const Expr *> Q) {
+ const NormalizedConstraint *PNormalized =
+ getNormalizedAssociatedConstraints(SemaRef, DP, P);
+ if (!PNormalized)
+ return std::nullopt;
+
+ const NormalizedConstraint *QNormalized =
+ getNormalizedAssociatedConstraints(SemaRef, DQ, Q);
+ if (!QNormalized)
+ return std::nullopt;
+
+ return Subsumes(PNormalized, QNormalized);
+}
+
+bool SubsumptionChecker::Subsumes(const NormalizedConstraint *P,
+ const NormalizedConstraint *Q) {
+
+ DNFFormula DNFP = DNF(*P);
+ CNFFormula CNFQ = CNF(*Q);
+ return Subsumes(DNFP, CNFQ);
+}
+
+bool SubsumptionChecker::Subsumes(const DNFFormula &PDNF,
+ const CNFFormula &QCNF) {
+ for (const auto &Pi : PDNF) {
+ for (const auto &Qj : QCNF) {
+ // C++ [temp.constr.order] p2
+ // - [...] a disjunctive clause Pi subsumes a conjunctive clause Qj if
+ // and only if there exists an atomic constraint Pia in Pi for which
+ // there exists an atomic constraint, Qjb, in Qj such that Pia
+ // subsumes Qjb.
+ if (!DNFSubsumes(Pi, Qj))
+ return false;
+ }
+ }
+ return true;
+}
+
+bool SubsumptionChecker::DNFSubsumes(const Clause &P, const Clause &Q) {
+
+ return llvm::any_of(P, [&](Literal LP) {
+ return llvm::any_of(Q, [this, LP](Literal LQ) { return Subsumes(LP, LQ);
});
+ });
+}
+
+bool SubsumptionChecker::Subsumes(const FoldExpandedConstraint *A,
+ const FoldExpandedConstraint *B) {
+ std::pair<const FoldExpandedConstraint *, const FoldExpandedConstraint *>
Key{
+ A, B};
+
+ auto It = FoldSubsumptionCache.find(Key);
+ if (It == FoldSubsumptionCache.end()) {
+ // C++ [temp.constr.order]
+ // a fold expanded constraint A subsumes another fold expanded
+ // constraint B if they are compatible for subsumption, have the same
+ // fold-operator, and the constraint of A subsumes that of B.
+ bool DoesSubsume =
+ A->Kind == B->Kind &&
+ FoldExpandedConstraint::AreCompatibleForSubsumption(*A, *B) &&
+ Subsumes(&A->Constraint, &B->Constraint);
+ It = FoldSubsumptionCache.try_emplace(std::move(Key), DoesSubsume).first;
+ }
----------------
MagentaTreehouse wrote:
I think this repeated map lookup can be avoided without the need for
`with_result_of`:
```suggestion
auto [It, Inserted] = FoldSubsumptionCache.try_emplace({A, B});
if (Inserted) {
// C++ [temp.constr.order]
// a fold expanded constraint A subsumes another fold expanded
// constraint B if they are compatible for subsumption, have the same
// fold-operator, and the constraint of A subsumes that of B.
bool DoesSubsume =
A->Kind == B->Kind &&
FoldExpandedConstraint::AreCompatibleForSubsumption(*A, *B) &&
Subsumes(&A->Constraint, &B->Constraint);
It->second = DoesSubsume;
}
```
https://github.com/llvm/llvm-project/pull/132849
_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
