[red-knot] Use ternary decision diagrams (TDDs) for visibility constraints (#15861)

We now use ternary decision diagrams (TDDs) to represent visibility
constraints. A TDD is just like a BDD ([_binary_ decision
diagram](https://en.wikipedia.org/wiki/Binary_decision_diagram)), but
with "ambiguous" as an additional allowed value. Unlike the previous
representation, TDDs are strongly normalizing, so equivalent ternary
formulas are represented by exactly the same graph node, and can be
compared for equality in constant time.

We currently have a slight 1-3% performance regression with this in
place, according to local testing. However, we also have a _5× increase_
in performance for pathological cases, since we can now remove the
recursion limit when we evaluate visibility constraints.

As follow-on work, we are now closer to being able to remove the
`simplify_visibility_constraint` calls in the semantic index builder. In
the vast majority of cases, we now see (for instance) that the
visibility constraint after an `if` statement, for bindings of symbols
that weren't rebound in any branch, simplifies back to `true`. But there
are still some cases we generate constraints that are cyclic. With
fixed-point cycle support in salsa, or with some careful analysis of the
still-failing cases, we might be able to remove those.
This commit is contained in:
Douglas Creager
2025-02-04 14:32:11 -05:00
committed by GitHub
parent 6bb32355ef
commit 444b055cec
4 changed files with 383 additions and 191 deletions

View File

@@ -1509,37 +1509,6 @@ if True:
from module import symbol
```
## Known limitations
We currently have a limitation in the complexity (depth) of the visibility constraints that are
supported. This is to avoid pathological cases that would require us to recurse deeply.
```py
x = 1
False or False or False or False or \
False or False or False or False or \
False or False or False or False or \
False or False or False or False or \
False or False or False or False or \
False or False or (x := 2) # fmt: skip
# This still works fine:
reveal_type(x) # revealed: Literal[2]
y = 1
False or False or False or False or \
False or False or False or False or \
False or False or False or False or \
False or False or False or False or \
False or False or False or False or \
False or False or False or (y := 2) # fmt: skip
# TODO: This should ideally be `Literal[2]` as well:
reveal_type(y) # revealed: Literal[1, 2]
```
## Unsupported features
We do not support full unreachable code analysis yet. We also raise diagnostics from