Visitar URL original
[ty] Check for unsatisfiable bodies before existentially quantifying … · astral-sh/ruff@734d75a · GitHub
Skip to content

Commit 734d75a

Browse files
dcreagerdcreager
authored
[ty] Check for unsatisfiable bodies before existentially quantifying (#29504)
When we existentially quantify a BDD, we calculate `∃X . B` for some set of typevars `X` and some BDD `B`. If the BDD is never satisfiable, this is equivalent to `∃X . false`, which can be further simplified to `false`. We expect this to be performance neutral at the moment, since `reduce_inferable` will already simplify the resulting quantified BDD down to `false` in most cases. We've extracted it for separate review out of #29027, where is has a much more pronounced impact, since it prevents us from creating existential nodes that we have to repeatedly walk through during solution extraction.
1 parent b0f9526 commit 734d75a

11 files changed

Lines changed: 264 additions & 0 deletions

File tree

‎crates/ruff_benchmark/benches/ty_constraint_set.rs‎

Lines changed: 39 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -102,6 +102,44 @@ def combine[T](first: T, second: T, third: T) -> T:
102102
});
103103
}
104104

105+
/// Quantify both satisfiable and contradictory bodies containing free variables. The satisfiable
106+
/// case measures the cost of checking for contradictions when projection still has work to do.
107+
fn benchmark_constraint_quantification(criterion: &mut Criterion) {
108+
const NUM_FUNCTIONS: usize = 128;
109+
110+
setup_rayon();
111+
112+
for (name, lower, upper, negation) in [
113+
("satisfiable", "A", "A", ""),
114+
("unsatisfiable", "int", "tuple[A, B]", "not "),
115+
] {
116+
let mut code = "from ty_extensions import static_assert\n\
117+
from ty_extensions._internal import ConstraintSet\n\n"
118+
.to_string();
119+
for i in 0..NUM_FUNCTIONS {
120+
writeln!(
121+
&mut code,
122+
"def check{i}[X, A, B]() -> None:
123+
body = ConstraintSet.lower_bound({lower}, X) & ConstraintSet.upper_bound(X, {upper})
124+
static_assert({negation}body.exists(tuple[X]))
125+
"
126+
)
127+
.ok();
128+
}
129+
130+
criterion.bench_function(
131+
&format!("ty_micro[constraint_quantification/{name}]"),
132+
|b| {
133+
b.iter_batched_ref(
134+
|| setup_micro_case(&code),
135+
|Case { db }| assert_eq!(db.check().len(), 0),
136+
BatchSize::SmallInput,
137+
);
138+
},
139+
);
140+
}
141+
}
142+
105143
/// Benchmarks solving many union-bearing upper bounds while inferring a generic call.
106144
///
107145
/// Each callable argument places a distinct union upper bound on `T` through callable-parameter
@@ -680,6 +718,7 @@ criterion_group!(
680718
constraint_set,
681719
benchmark_typevar_mapping_large_accumulation,
682720
benchmark_typevar_mapping_small_accumulations,
721+
benchmark_constraint_quantification,
683722
benchmark_factored_upper_bounds,
684723
benchmark_many_upper_bound_callbacks,
685724
benchmark_pandas_tdd,

‎crates/ty_python_semantic/resources/mdtest/type_properties/constraints.md‎

Lines changed: 34 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1368,6 +1368,40 @@ def declared_bound[T: str]() -> None:
13681368
static_assert(constraint.solutions(inferable=tuple[T]) is None)
13691369
```
13701370

1371+
## Trivial satisfiability checks
1372+
1373+
The trivial satisfiability checks only recognize the true and false terminal BDDs.
1374+
1375+
```py
1376+
from ty_extensions import static_assert
1377+
from ty_extensions._internal import ConstraintSet
1378+
1379+
static_assert(ConstraintSet.always().is_trivially_always_satisfied())
1380+
static_assert(not ConstraintSet.always().is_trivially_never_satisfied())
1381+
static_assert(ConstraintSet.never().is_trivially_never_satisfied())
1382+
static_assert(not ConstraintSet.never().is_trivially_always_satisfied())
1383+
1384+
def bounded[T]() -> None:
1385+
constraint = ConstraintSet.equality(T, int)
1386+
static_assert(not constraint.is_trivially_always_satisfied())
1387+
static_assert(not constraint.is_trivially_never_satisfied())
1388+
```
1389+
1390+
Semantic contradictions and tautologies need not be represented as terminal BDDs.
1391+
1392+
```py
1393+
def nonterminal[T]() -> None:
1394+
# T = int ∧ T = str
1395+
impossible = ConstraintSet.equality(T, int) & ConstraintSet.equality(T, str)
1396+
static_assert(impossible.is_never_satisfied(inferable=tuple[T]))
1397+
static_assert(not impossible.is_trivially_never_satisfied())
1398+
1399+
# ¬(T = int ∧ T = str)
1400+
tautology = ~impossible
1401+
static_assert(tautology.is_always_satisfied(inferable=tuple[T]))
1402+
static_assert(not tautology.is_trivially_always_satisfied())
1403+
```
1404+
13711405
## Satisfiability checks exceeding the traversal budget
13721406

13731407
Independent alternatives can produce too many paths to check within the computation budget. An

‎crates/ty_python_semantic/resources/mdtest/type_properties/quantification.md‎

Lines changed: 69 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -309,3 +309,72 @@ def alternation[X: (int, str), Y: (int, str)]() -> None:
309309
missing_str = int_only.exists(tuple[X]).for_all(tuple[Y])
310310
static_assert(not missing_str)
311311
```
312+
313+
## Unsatisfiable bodies with free variables
314+
315+
No type `X` can be both a supertype of `int` and a subtype of `tuple[A, B]`, regardless of what
316+
types `A` and `B` are specialized to. As an optimization, when quantifying over `X` we detect that
317+
"eagerly", and reduce the constraint set to the "always false" terminal BDD, instead of evaluating
318+
the satisfiability of the body each time we solve.
319+
320+
```py
321+
from ty_extensions import static_assert
322+
from ty_extensions._internal import ConstraintSet
323+
324+
def impossible[X, A, B]() -> None:
325+
body = ConstraintSet.lower_bound(int, X) & ConstraintSet.upper_bound(X, tuple[A, B])
326+
# ∃X. int ≤ X ≤ tuple[A, B]
327+
impossible = body.exists(tuple[X])
328+
# Note that this constraint set is not just never satisfied; it reduces specifically
329+
# to the `false` terminal.
330+
static_assert(impossible.is_trivially_never_satisfied())
331+
```
332+
333+
## Satisfiability depends on free variables
334+
335+
There is an `X` satisfying `A ≤ X ≤ int` when `A` is `int`, but not when `A` is `str`. When we
336+
quantify over `X`, the resulting constraint set must preserve that distinction.
337+
338+
```py
339+
from ty_extensions._internal import ConstraintSet
340+
341+
def possible[X, A]() -> None:
342+
body = ConstraintSet.lower_bound(A, X) & ConstraintSet.upper_bound(X, int)
343+
# ∃X. A ≤ X ≤ int
344+
quantified = body.exists(tuple[X])
345+
346+
# (∃X. A ≤ X ≤ int) ∧ A = int
347+
valid = quantified & ConstraintSet.equality(A, int)
348+
# revealed: tuple[Solution[A=int]]
349+
reveal_type(valid.solutions(inferable=tuple[A]))
350+
351+
# (∃X. A ≤ X ≤ int) ∧ A = str
352+
invalid = quantified & ConstraintSet.equality(A, str)
353+
# revealed: None
354+
reveal_type(invalid.solutions(inferable=tuple[A]))
355+
```
356+
357+
## Negated inner quantification with free variables
358+
359+
An inner existential can hold for some choices of a free variable and fail for others. Its negation
360+
must preserve the choices for which it fails when an enclosing existential is evaluated.
361+
362+
```py
363+
from ty_extensions._internal import ConstraintSet
364+
365+
def nested[X, Y, A]() -> None:
366+
# ∃X. X = int ∧ X = A
367+
inner = (ConstraintSet.equality(X, int) & ConstraintSet.equality(X, A)).exists(tuple[X])
368+
# ∃Y. ¬(∃X. X = int ∧ X = A) ∧ Y = str
369+
outer = (~inner & ConstraintSet.equality(Y, str)).exists(tuple[Y])
370+
371+
# (∃Y. ¬(∃X. X = int ∧ X = A) ∧ Y = str) ∧ A = str
372+
valid = outer & ConstraintSet.equality(A, str)
373+
# revealed: tuple[Solution[A=str]]
374+
reveal_type(valid.solutions(inferable=tuple[A]))
375+
376+
# (∃Y. ¬(∃X. X = int ∧ X = A) ∧ Y = str) ∧ A = int
377+
invalid = outer & ConstraintSet.equality(A, int)
378+
# revealed: None
379+
reveal_type(invalid.solutions(inferable=tuple[A]))
380+
```

‎crates/ty_python_semantic/src/types.rs‎

Lines changed: 22 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -6265,6 +6265,22 @@ impl<'db> Type<'db> {
62656265
))
62666266
.into()
62676267
}
6268+
Type::KnownInstance(KnownInstanceType::ConstraintSet(tracked))
6269+
if name == "is_trivially_always_satisfied" =>
6270+
{
6271+
Place::bound(Type::KnownBoundMethod(
6272+
KnownBoundMethodType::ConstraintSetIsTriviallyAlwaysSatisfied(tracked),
6273+
))
6274+
.into()
6275+
}
6276+
Type::KnownInstance(KnownInstanceType::ConstraintSet(tracked))
6277+
if name == "is_trivially_never_satisfied" =>
6278+
{
6279+
Place::bound(Type::KnownBoundMethod(
6280+
KnownBoundMethodType::ConstraintSetIsTriviallyNeverSatisfied(tracked),
6281+
))
6282+
.into()
6283+
}
62686284
Type::KnownInstance(KnownInstanceType::ConstraintSet(tracked))
62696285
if name == "with_detailed_display" =>
62706286
{
@@ -9499,6 +9515,8 @@ impl<'db> Type<'db> {
94999515
| KnownBoundMethodType::ConstraintSetSolutions(_)
95009516
| KnownBoundMethodType::ConstraintSetIsAlwaysSatisfied(_)
95019517
| KnownBoundMethodType::ConstraintSetIsNeverSatisfied(_)
9518+
| KnownBoundMethodType::ConstraintSetIsTriviallyAlwaysSatisfied(_)
9519+
| KnownBoundMethodType::ConstraintSetIsTriviallyNeverSatisfied(_)
95029520
| KnownBoundMethodType::ConstraintSetWithDetailedDisplay(_)
95039521
)
95049522
) {
@@ -9957,6 +9975,8 @@ impl<'db> Type<'db> {
99579975
| KnownBoundMethodType::ConstraintSetSolutions(_)
99589976
| KnownBoundMethodType::ConstraintSetIsAlwaysSatisfied(_)
99599977
| KnownBoundMethodType::ConstraintSetIsNeverSatisfied(_)
9978+
| KnownBoundMethodType::ConstraintSetIsTriviallyAlwaysSatisfied(_)
9979+
| KnownBoundMethodType::ConstraintSetIsTriviallyNeverSatisfied(_)
99609980
| KnownBoundMethodType::ConstraintSetWithDetailedDisplay(_),
99619981
)
99629982
| Type::DataclassDecorator(_)
@@ -10324,6 +10344,8 @@ impl<'db> Type<'db> {
1032410344
| KnownBoundMethodType::ConstraintSetSolutions(_)
1032510345
| KnownBoundMethodType::ConstraintSetIsAlwaysSatisfied(_)
1032610346
| KnownBoundMethodType::ConstraintSetIsNeverSatisfied(_)
10347+
| KnownBoundMethodType::ConstraintSetIsTriviallyAlwaysSatisfied(_)
10348+
| KnownBoundMethodType::ConstraintSetIsTriviallyNeverSatisfied(_)
1032710349
| KnownBoundMethodType::ConstraintSetWithDetailedDisplay(_),
1032810350
)
1032910351
| Type::DataclassDecorator(_)

‎crates/ty_python_semantic/src/types/call/bind.rs‎

Lines changed: 21 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -3241,6 +3241,27 @@ impl<'db> Bindings<'db> {
32413241
));
32423242
}
32433243

3244+
Type::KnownBoundMethod(
3245+
method @ (KnownBoundMethodType::ConstraintSetIsTriviallyAlwaysSatisfied(
3246+
tracked,
3247+
)
3248+
| KnownBoundMethodType::ConstraintSetIsTriviallyNeverSatisfied(
3249+
tracked,
3250+
)),
3251+
) => {
3252+
let result = tracked.constraints(db).query(|_builder, set| {
3253+
if matches!(
3254+
method,
3255+
KnownBoundMethodType::ConstraintSetIsTriviallyAlwaysSatisfied(_)
3256+
) {
3257+
set.is_trivially_always_satisfied()
3258+
} else {
3259+
set.is_trivially_never_satisfied()
3260+
}
3261+
});
3262+
overload.set_return_type(Type::bool_literal(result));
3263+
}
3264+
32443265
Type::KnownBoundMethod(KnownBoundMethodType::ConstraintSetSolutions(
32453266
tracked,
32463267
)) => {

‎crates/ty_python_semantic/src/types/constraints.rs‎

Lines changed: 23 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -802,6 +802,29 @@ impl<'db, 'c> ConstraintSet<'db, 'c> {
802802
return self;
803803
}
804804
let mut storage = builder.storage.borrow_mut();
805+
// A quantified body is false if no assignment to its locals or free variables can
806+
// satisfy it.
807+
if let Some(support) = storage.node_support(self.node)
808+
&& support.is_complete()
809+
{
810+
let inferable =
811+
TypeVarSet::from_typevars(db, support.iter().map(|id| storage.typevar_data(id)));
812+
let budget = SolutionBudget::default();
813+
let limits = BoundedSolutionLimits {
814+
remaining_paths: budget.paths,
815+
remaining_visits: budget.visits,
816+
};
817+
if let ControlFlow::Continue(true) = self.node.is_never_satisfied_with_limits(
818+
db,
819+
env,
820+
&mut storage,
821+
inferable,
822+
self.source_order,
823+
limits,
824+
) {
825+
return Self::never(builder);
826+
}
827+
}
805828
let (node, derived_source_order) =
806829
self.node
807830
.exists(db, env, &mut storage, to_remove, self.source_order);

‎crates/ty_python_semantic/src/types/display.rs‎

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1578,6 +1578,16 @@ impl<'db> FmtDetailed<'db> for DisplayRepresentation<'_, 'db> {
15781578
KnownBoundMethodType::ConstraintSetWithDetailedDisplay(_) => {
15791579
return f.write_str("bound method `ConstraintSet.with_detailed_display`");
15801580
}
1581+
KnownBoundMethodType::ConstraintSetIsTriviallyAlwaysSatisfied(_) => {
1582+
return f.write_str(
1583+
"bound method `ConstraintSet.is_trivially_always_satisfied`",
1584+
);
1585+
}
1586+
KnownBoundMethodType::ConstraintSetIsTriviallyNeverSatisfied(_) => {
1587+
return f.write_str(
1588+
"bound method `ConstraintSet.is_trivially_never_satisfied`",
1589+
);
1590+
}
15811591
};
15821592

15831593
f.write_char('<')?;

‎crates/ty_python_semantic/src/types/infer/comparisons.rs‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -393,6 +393,8 @@ impl<'db> Type<'db> {
393393
| KnownBoundMethodType::ConstraintSetSolutions(_)
394394
| KnownBoundMethodType::ConstraintSetIsAlwaysSatisfied(_)
395395
| KnownBoundMethodType::ConstraintSetIsNeverSatisfied(_)
396+
| KnownBoundMethodType::ConstraintSetIsTriviallyAlwaysSatisfied(_)
397+
| KnownBoundMethodType::ConstraintSetIsTriviallyNeverSatisfied(_)
396398
| KnownBoundMethodType::ConstraintSetWithDetailedDisplay(_) => {
397399
(method, NegativeRetention::Stable)
398400
}

‎crates/ty_python_semantic/src/types/method.rs‎

Lines changed: 28 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -410,6 +410,8 @@ pub enum KnownBoundMethodType<'db> {
410410
ConstraintSetSolutions(InternedConstraintSet<'db>),
411411
ConstraintSetIsAlwaysSatisfied(InternedConstraintSet<'db>),
412412
ConstraintSetIsNeverSatisfied(InternedConstraintSet<'db>),
413+
ConstraintSetIsTriviallyAlwaysSatisfied(InternedConstraintSet<'db>),
414+
ConstraintSetIsTriviallyNeverSatisfied(InternedConstraintSet<'db>),
413415
ConstraintSetWithDetailedDisplay(InternedConstraintSet<'db>),
414416
}
415417

@@ -455,6 +457,8 @@ pub(super) fn walk_method_wrapper_type<'db, V: visitor::TypeVisitor<'db> + ?Size
455457
| KnownBoundMethodType::ConstraintSetSolutions(_)
456458
| KnownBoundMethodType::ConstraintSetIsAlwaysSatisfied(_)
457459
| KnownBoundMethodType::ConstraintSetIsNeverSatisfied(_)
460+
| KnownBoundMethodType::ConstraintSetIsTriviallyAlwaysSatisfied(_)
461+
| KnownBoundMethodType::ConstraintSetIsTriviallyNeverSatisfied(_)
458462
| KnownBoundMethodType::ConstraintSetWithDetailedDisplay(_) => {}
459463
}
460464
}
@@ -519,6 +523,8 @@ impl<'db> KnownBoundMethodType<'db> {
519523
| KnownBoundMethodType::ConstraintSetSolutions(_)
520524
| KnownBoundMethodType::ConstraintSetIsAlwaysSatisfied(_)
521525
| KnownBoundMethodType::ConstraintSetIsNeverSatisfied(_)
526+
| KnownBoundMethodType::ConstraintSetIsTriviallyAlwaysSatisfied(_)
527+
| KnownBoundMethodType::ConstraintSetIsTriviallyNeverSatisfied(_)
522528
| KnownBoundMethodType::ConstraintSetWithDetailedDisplay(_) => Some(self),
523529
}
524530
}
@@ -547,6 +553,8 @@ impl<'db> KnownBoundMethodType<'db> {
547553
| KnownBoundMethodType::ConstraintSetSolutions(_)
548554
| KnownBoundMethodType::ConstraintSetIsAlwaysSatisfied(_)
549555
| KnownBoundMethodType::ConstraintSetIsNeverSatisfied(_)
556+
| KnownBoundMethodType::ConstraintSetIsTriviallyAlwaysSatisfied(_)
557+
| KnownBoundMethodType::ConstraintSetIsTriviallyNeverSatisfied(_)
550558
| KnownBoundMethodType::ConstraintSetWithDetailedDisplay(_) => {
551559
KnownClass::ConstraintSet
552560
}
@@ -834,6 +842,14 @@ impl<'db> KnownBoundMethodType<'db> {
834842
)))
835843
}
836844

845+
KnownBoundMethodType::ConstraintSetIsTriviallyAlwaysSatisfied(_)
846+
| KnownBoundMethodType::ConstraintSetIsTriviallyNeverSatisfied(_) => {
847+
Either::Right(std::iter::once(Signature::new(
848+
Parameters::empty(),
849+
KnownClass::Bool.to_instance(db, env),
850+
)))
851+
}
852+
837853
KnownBoundMethodType::ConstraintSetWithDetailedDisplay(_) => {
838854
Either::Right(std::iter::once(Signature::new(
839855
Parameters::empty(),
@@ -945,6 +961,14 @@ impl<'c, 'db> TypeRelationChecker<'_, 'c, 'db> {
945961
KnownBoundMethodType::ConstraintSetIsNeverSatisfied(_),
946962
KnownBoundMethodType::ConstraintSetIsNeverSatisfied(_),
947963
)
964+
| (
965+
KnownBoundMethodType::ConstraintSetIsTriviallyAlwaysSatisfied(_),
966+
KnownBoundMethodType::ConstraintSetIsTriviallyAlwaysSatisfied(_),
967+
)
968+
| (
969+
KnownBoundMethodType::ConstraintSetIsTriviallyNeverSatisfied(_),
970+
KnownBoundMethodType::ConstraintSetIsTriviallyNeverSatisfied(_),
971+
)
948972
| (
949973
KnownBoundMethodType::ConstraintSetWithDetailedDisplay(_),
950974
KnownBoundMethodType::ConstraintSetWithDetailedDisplay(_),
@@ -972,6 +996,8 @@ impl<'c, 'db> TypeRelationChecker<'_, 'c, 'db> {
972996
| KnownBoundMethodType::ConstraintSetSolutions(_)
973997
| KnownBoundMethodType::ConstraintSetIsAlwaysSatisfied(_)
974998
| KnownBoundMethodType::ConstraintSetIsNeverSatisfied(_)
999+
| KnownBoundMethodType::ConstraintSetIsTriviallyAlwaysSatisfied(_)
1000+
| KnownBoundMethodType::ConstraintSetIsTriviallyNeverSatisfied(_)
9751001
| KnownBoundMethodType::ConstraintSetWithDetailedDisplay(_),
9761002
KnownBoundMethodType::FunctionTypeDunderGet(_)
9771003
| KnownBoundMethodType::DunderCall(_)
@@ -994,6 +1020,8 @@ impl<'c, 'db> TypeRelationChecker<'_, 'c, 'db> {
9941020
| KnownBoundMethodType::ConstraintSetSolutions(_)
9951021
| KnownBoundMethodType::ConstraintSetIsAlwaysSatisfied(_)
9961022
| KnownBoundMethodType::ConstraintSetIsNeverSatisfied(_)
1023+
| KnownBoundMethodType::ConstraintSetIsTriviallyAlwaysSatisfied(_)
1024+
| KnownBoundMethodType::ConstraintSetIsTriviallyNeverSatisfied(_)
9971025
| KnownBoundMethodType::ConstraintSetWithDetailedDisplay(_),
9981026
) => self.never(),
9991027
}

‎crates/ty_python_semantic/src/types/relation.rs‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -276,6 +276,8 @@ impl<'db> Type<'db> {
276276
| KnownBoundMethodType::ConstraintSetSolutions(_)
277277
| KnownBoundMethodType::ConstraintSetIsAlwaysSatisfied(_)
278278
| KnownBoundMethodType::ConstraintSetIsNeverSatisfied(_)
279+
| KnownBoundMethodType::ConstraintSetIsTriviallyAlwaysSatisfied(_)
280+
| KnownBoundMethodType::ConstraintSetIsTriviallyNeverSatisfied(_)
279281
| KnownBoundMethodType::ConstraintSetWithDetailedDisplay(_),
280282
)
281283
| Type::DataclassDecorator(_)

0 commit comments

Comments
 (0)