[all-commits] [llvm/llvm-project] ae54f4: [Clang] Improve subsumption. (#132849)

[cor3ntin via All-commits]

  Branch: refs/heads/main
  Home:   https://github.com/llvm/llvm-project
  Commit: ae54f476f7d856682976f08622ee70880318a1b1
      https://github.com/llvm/llvm-project/commit/ae54f476f7d856682976f08622ee70880318a1b1
  Author: cor3ntin <corentinjabot at gmail.com>
  Date:   2025-03-27 (Thu, 27 Mar 2025)

  Changed paths:
    M clang/docs/ReleaseNotes.rst
    M clang/include/clang/Sema/SemaConcept.h
    M clang/lib/Sema/SemaConcept.cpp
    A clang/test/SemaCXX/concepts-subsumption.cpp

  Log Message:
  -----------
  [Clang] Improve subsumption. (#132849)

The main goal of this patch is to improve the
performance of concept subsumption by

- Making sure literal (atomic) clauses are de-duplicated (Whether 2
atomic constraint is established during the initial normal form
production).
 - Eagerly removing duplicated clauses.

This should minimize the risks of exponentially large formulas that can
be produced by a naive {C,D}NF transformation.

While at it, I restructured that part of the code to be a bit clearer.

Subsumption of fold expanded constraint is also cached.

---

Note that removing duplicated clauses seems to be necessary and
sufficient to have acceptable performance on anything that could be
construed as reasonable code.

Ultimately, the number of clauses is always going to be fairly small
(but $2^{fairly\ small}$ is quickly *fairly large*..).

I went too far in the rabbit hole of Tseitin transformations etc, which
was much faster but would then require to check satisfiabiliy to
establish subsumption between some constraints (although it was good
enough to pass all but ones of our tests...).

It doesn't help that the C++ standard has a very specific definition of
subsumption that is really more of an implication...

While that sort of musing is fascinating, it was ultimately a fool's
errand, at least until such time that there is more motivation for a SAT
solver in clang (clang-tidy can after all use z3!).

Here be dragons.

Fixes #122581



To unsubscribe from these emails, change your notification settings at https://github.com/llvm/llvm-project/settings/notifications