Module narrowing_constraints 

Narrowing constraints

When building a semantic index for a file, we associate each binding with a narrowing constraint, which constrains the type of the binding’s place. A binding can be associated with a different narrowing constraint at different points in a file. See the use_def module for more details.

A narrowing constraint is a boolean formula over predicates such as isinstance(x, A). Internally, we store these formulas in a ternary decision diagram (TDD). Each interior node has three outgoing edges:

• if_true applies when the predicate is true.
• if_false applies when the predicate is false.
• if_uncertain applies either way.

Despite its name, if_uncertain does not mean that the predicate’s value is unknown. It is a “don’t care” edge: the formula on that edge does not depend on the predicate. A node represents this formula:

if_uncertain OR (predicate AND if_true) OR (NOT predicate AND if_false)

The extra edge keeps repeated unions small. For example, A OR B can store A once on B’s if_uncertain edge instead of copying A into both of B’s other edges.

We also absorb redundant cofactors when constructing TDD nodes. This is especially useful for the continuation of a large if/elif chain. Each branch has narrowing constraints of the form A, NOT A AND B, NOT A AND NOT B AND C, and so on. The continuation combines those branch constraints with OR. The negative part of each branch constraint is redundant in that union because it is already covered by the earlier positive branches. These negative prefixes are cofactors of the earlier positive alternatives and can be absorbed. For example, A OR (NOT A AND B) simplifies to A OR B.

Structs

InteriorNode

NarrowingConstraints

NarrowingConstraintsBuilder

ScopedNarrowingConstraint

The ID of a narrowing formula within one scope.

Enums

ConstraintKey