[ty] Refactor constraint traversal and cache satisfiability checks (astral-sh#29492)

This PR extracts some refactoring changes out of astral-sh#29027 so they can be
reviewed separately. This should be entirely behavioral neutral.

The changes:

- There is now a clear separation between "atomic" constraints and
non-atomic constraints. There aren't actually any non-atomic constraints
yet, but astral-sh#29027 will add existential nodes as a non-atomic constraint.
The defining characteristic is that an atomic constraint is one that is
an actual assignment to a typevar; it is what `PathAssignments` builds
up as it walks a BDD, and is what can live as an antecedent or
consequent in a `SequentMap`.

- We've extracted the logic for persisting a `ConstraintSet` into an
`OwnedConstraintSet`, moving it into a standalone file and structuring
it better via a helper type and some finer grained methods.

- Removed some code sharing in `SolutionWalker` that was actually
leading to more complex code. `visit_node` and
`node_is_satisfiable_on_path` no longer use a shared helper, since the
two uses had many differences, which required overridable hook points.
The shared part was much smaller, so it's simpler to just copy/paste
that part.

- That makes it easier to add caching of `node_is_satisfiable_on_path`,
similar to the caching we already had for `visit_node`.

Author: dcreager

crates/ruff_benchmark/benches/ty_constraint_set.rs

@@ -651,6 +651,31 @@ fn benchmark_pydantic_core_schema_dict(criterion: &mut Criterion) {
     });
 }
 
+/// Repeated unions share source-order subtrees even after the TDD stops growing. Persisting each
+/// result must not expand those shared subtrees into exponentially many copies.
+fn benchmark_shared_source_order_compaction(criterion: &mut Criterion) {
+    setup_rayon();
+
+    let mut code = String::from(
+        "from ty_extensions._internal import ConstraintSet\n\ndef repeated[T]() -> None:\n    c0 = ConstraintSet.lower_bound(int, T)\n    c1 = ConstraintSet.lower_bound(str, T)\n",
+    );
+    for i in 2..26 {
+        writeln!(&mut code, "    c{i} = c{} | c{}", i - 2, i - 1).ok();
+    }
+
+    criterion.bench_function("ty_micro[shared_source_order_compaction]", |b| {
+        b.iter_batched_ref(
+            || setup_micro_case(&code),
+            |case| {
+                let Case { db } = case;
+                let result = db.check();
+                assert_eq!(result.len(), 0);
+            },
+            BatchSize::SmallInput,
+        );
+    });
+}
+
 criterion_group!(
     constraint_set,
     benchmark_typevar_mapping_large_accumulation,
@@ -667,5 +692,6 @@ criterion_group!(
     benchmark_many_invariant_typevars,
     benchmark_mixed_many_invariant_typevars,
     benchmark_pydantic_core_schema_dict,
+    benchmark_shared_source_order_compaction,
 );
 criterion_main!(constraint_set);

crates/ty_python_semantic/resources/mdtest/regression/constraint_set_ordering.md

@@ -561,3 +561,50 @@ def high_fanout[
     # revealed: None
     reveal_type(impossible.solutions_for(R11, inferable=inferable))
 ```
+
+## Satisfiability checks exceeding the traversal budget
+
+Independent alternatives can produce too many paths to check within the computation budget. An
+incomplete check returns `bool`, without claiming either literal result. This applies both to
+checking that a constraint set never holds and to checking that its negation always holds. Orderings
+that reach the contradiction early can instead prove the result within the budget.
+
+```py
+from ty_extensions._internal import ConstraintSet
+
+def bounded[A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, X]() -> None:
+    # (A = int ∨ A = str) ∧ … ∧ (R = int ∨ R = str)
+    choices = (
+        (ConstraintSet.equality(A, int) | ConstraintSet.equality(A, str))
+        & (ConstraintSet.equality(B, int) | ConstraintSet.equality(B, str))
+        & (ConstraintSet.equality(C, int) | ConstraintSet.equality(C, str))
+        & (ConstraintSet.equality(D, int) | ConstraintSet.equality(D, str))
+        & (ConstraintSet.equality(E, int) | ConstraintSet.equality(E, str))
+        & (ConstraintSet.equality(F, int) | ConstraintSet.equality(F, str))
+        & (ConstraintSet.equality(G, int) | ConstraintSet.equality(G, str))
+        & (ConstraintSet.equality(H, int) | ConstraintSet.equality(H, str))
+        & (ConstraintSet.equality(I, int) | ConstraintSet.equality(I, str))
+        & (ConstraintSet.equality(J, int) | ConstraintSet.equality(J, str))
+        & (ConstraintSet.equality(K, int) | ConstraintSet.equality(K, str))
+        & (ConstraintSet.equality(L, int) | ConstraintSet.equality(L, str))
+        & (ConstraintSet.equality(M, int) | ConstraintSet.equality(M, str))
+        & (ConstraintSet.equality(N, int) | ConstraintSet.equality(N, str))
+        & (ConstraintSet.equality(O, int) | ConstraintSet.equality(O, str))
+        & (ConstraintSet.equality(P, int) | ConstraintSet.equality(P, str))
+        & (ConstraintSet.equality(Q, int) | ConstraintSet.equality(Q, str))
+        & (ConstraintSet.equality(R, int) | ConstraintSet.equality(R, str))
+    )
+    # Every combination of choices eventually encounters X = int ∧ X = str.
+    impossible = ConstraintSet.equality(X, int) & ConstraintSet.equality(X, str) & choices
+    # TODO: sometimes: revealed Literal[True]
+    # revealed: bool
+    reveal_type(impossible.is_never_satisfied(inferable=tuple[A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, X]))
+
+    # TODO: sometimes: revealed Literal[True]
+    # revealed: bool
+    reveal_type((~impossible).is_always_satisfied(inferable=tuple[A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, X]))
+
+    # Finding one witness for the choices alone does not require exploring every combination.
+    # revealed: Literal[False]
+    reveal_type(choices.is_never_satisfied(inferable=tuple[A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R]))
+```

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

@@ -1113,6 +1113,32 @@ def f[S, T, U]():
     ...
 ```
 
+## Repeated combinations preserve the first occurrence
+
+Combining previously constructed constraint sets can repeat the same constraints many times. The
+first occurrence still determines binding order, even when later combinations reverse that order.
+
+```py
+from ty_extensions._internal import ConstraintSet
+
+def repeated[T, U]() -> None:
+    c0 = ConstraintSet.equality(T, int)
+    c1 = ConstraintSet.equality(U, str)
+    c2 = c0 & c1
+    c3 = c1 & c2
+    c4 = c2 & c3
+    c5 = c3 & c4
+    c6 = c4 & c5
+    c7 = c5 & c6
+    c8 = c6 & c7
+    c9 = c7 & c8
+
+    # revealed: tuple[Solution[T=int, U=str]]
+    reveal_type(c8.solutions(inferable=tuple[T, U]))
+    # revealed: tuple[Solution[U=str, T=int]]
+    reveal_type(c9.solutions(inferable=tuple[T, U]))
+```
+
 ## Other simplifications
 
 ### Ordering of intersection and union elements
@@ -1342,6 +1368,50 @@ def declared_bound[T: str]() -> None:
     static_assert(constraint.solutions(inferable=tuple[T]) is None)
 ```
 
+## Satisfiability checks exceeding the traversal budget
+
+Independent alternatives can produce too many paths to check within the computation budget. An
+incomplete check returns `bool`, without claiming either literal result. This applies both to
+checking that a constraint set never holds and to checking that its negation always holds.
+
+```py
+from ty_extensions._internal import ConstraintSet
+
+def bounded[A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, X]() -> None:
+    # (A = int ∨ A = str) ∧ … ∧ (R = int ∨ R = str)
+    choices = (
+        (ConstraintSet.equality(A, int) | ConstraintSet.equality(A, str))
+        & (ConstraintSet.equality(B, int) | ConstraintSet.equality(B, str))
+        & (ConstraintSet.equality(C, int) | ConstraintSet.equality(C, str))
+        & (ConstraintSet.equality(D, int) | ConstraintSet.equality(D, str))
+        & (ConstraintSet.equality(E, int) | ConstraintSet.equality(E, str))
+        & (ConstraintSet.equality(F, int) | ConstraintSet.equality(F, str))
+        & (ConstraintSet.equality(G, int) | ConstraintSet.equality(G, str))
+        & (ConstraintSet.equality(H, int) | ConstraintSet.equality(H, str))
+        & (ConstraintSet.equality(I, int) | ConstraintSet.equality(I, str))
+        & (ConstraintSet.equality(J, int) | ConstraintSet.equality(J, str))
+        & (ConstraintSet.equality(K, int) | ConstraintSet.equality(K, str))
+        & (ConstraintSet.equality(L, int) | ConstraintSet.equality(L, str))
+        & (ConstraintSet.equality(M, int) | ConstraintSet.equality(M, str))
+        & (ConstraintSet.equality(N, int) | ConstraintSet.equality(N, str))
+        & (ConstraintSet.equality(O, int) | ConstraintSet.equality(O, str))
+        & (ConstraintSet.equality(P, int) | ConstraintSet.equality(P, str))
+        & (ConstraintSet.equality(Q, int) | ConstraintSet.equality(Q, str))
+        & (ConstraintSet.equality(R, int) | ConstraintSet.equality(R, str))
+    )
+    # Every combination of choices eventually encounters X = int ∧ X = str.
+    impossible = ConstraintSet.equality(X, int) & ConstraintSet.equality(X, str) & choices
+    # revealed: bool
+    reveal_type(impossible.is_never_satisfied(inferable=tuple[A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, X]))
+
+    # revealed: bool
+    reveal_type((~impossible).is_always_satisfied(inferable=tuple[A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, X]))
+
+    # Finding one witness for the choices alone does not require exploring every combination.
+    # revealed: Literal[False]
+    reveal_type(choices.is_never_satisfied(inferable=tuple[A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R]))
+```
+
 ## Solutions with inferable and non-inferable typevars
 
 Solution extraction receives the type variables that it is allowed to infer. Other type variables

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

@@ -3230,12 +3230,15 @@ impl<'db> Bindings<'db> {
                                 method,
                                 KnownBoundMethodType::ConstraintSetIsAlwaysSatisfied(_)
                             ) {
-                                set.is_always_satisfied(db, env, inferable)
+                                set.is_always_satisfied_bounded(db, env, inferable)
                             } else {
-                                set.is_never_satisfied(db, env, inferable)
+                                set.is_never_satisfied_bounded(db, env, inferable)
                             }
                         });
-                        overload.set_return_type(Type::bool_literal(result));
+                        overload.set_return_type(result.map_or_else(
+                            || KnownClass::Bool.to_instance(db, env),
+                            Type::bool_literal,
+                        ));
                     }
 
                     Type::KnownBoundMethod(KnownBoundMethodType::ConstraintSetSolutions(