diff --git a/crates/ty_python_semantic/src/types/constraints.rs b/crates/ty_python_semantic/src/types/constraints.rs
index 3288fabb4ac6e..bb2bf8af24780 100644
--- a/crates/ty_python_semantic/src/types/constraints.rs
+++ b/crates/ty_python_semantic/src/types/constraints.rs
@@ -71,7 +71,7 @@ use std::cmp::Ordering;
 use std::fmt::Display;
 use std::ops::Range;
 
-use itertools::Itertools;
+use itertools::{Either, Itertools};
 use rustc_hash::{FxHashMap, FxHashSet};
 use salsa::plumbing::AsId;
 use smallvec::SmallVec;
@@ -147,8 +147,16 @@ where
         db: &'db dyn Db,
         mut f: impl FnMut(T) -> ConstraintSet<'db>,
     ) -> ConstraintSet<'db> {
-        let node = Node::distributed_or(db, self.map(|element| f(element).node));
-        ConstraintSet { node }
+        let mut support = Support::Empty;
+        let node = Node::distributed_or(
+            db,
+            self.map(|element| {
+                let element = f(element);
+                support = support.union(db, element.support);
+                element.node
+            }),
+        );
+        ConstraintSet { node, support }
     }
 
     fn when_all<'db>(
@@ -156,8 +164,16 @@ where
         db: &'db dyn Db,
         mut f: impl FnMut(T) -> ConstraintSet<'db>,
     ) -> ConstraintSet<'db> {
-        let node = Node::distributed_and(db, self.map(|element| f(element).node));
-        ConstraintSet { node }
+        let mut support = Support::Empty;
+        let node = Node::distributed_and(
+            db,
+            self.map(|element| {
+                let element = f(element);
+                support = support.union(db, element.support);
+                element.node
+            }),
+        );
+        ConstraintSet { node, support }
     }
 }
 
@@ -175,21 +191,35 @@ where
 pub struct ConstraintSet<'db> {
     /// The BDD representing this constraint set
     node: Node<'db>,
+    /// The set of constraints explicitly added to this constraint set.
+    support: Support<'db>,
 }
 
 impl<'db> ConstraintSet<'db> {
     fn never() -> Self {
         Self {
             node: Node::AlwaysFalse,
+            support: Support::Empty,
         }
     }
 
     fn always() -> Self {
         Self {
             node: Node::AlwaysTrue,
+            support: Support::Empty,
         }
     }
 
+    fn with_support(db: &'db dyn Db, node: Node<'db>, support: Support<'db>) -> Self {
+        // The support should only contain constraints that participate in making a constraint set
+        // satisfiable.
+        let node = node.prune_impossible_paths(db, support);
+        if node == Node::AlwaysFalse {
+            return Self::never();
+        }
+        Self { node, support }
+    }
+
     /// Returns a constraint set that constraints a typevar to a particular range of types.
     pub(crate) fn constrain_typevar(
         db: &'db dyn Db,
@@ -197,19 +227,20 @@ impl<'db> ConstraintSet<'db> {
         lower: Type<'db>,
         upper: Type<'db>,
     ) -> Self {
-        Self {
-            node: ConstrainedTypeVar::new_node(db, typevar, lower, upper),
-        }
+        let mut support = FxOrderSet::default();
+        let node =
+            ConstrainedTypeVar::new_node_with_support(db, &mut support, typevar, lower, upper);
+        Self::with_support(db, node, Support::new(db, support))
     }
 
     /// Returns whether this constraint set never holds
     pub(crate) fn is_never_satisfied(self, db: &'db dyn Db) -> bool {
-        self.node.is_never_satisfied(db)
+        self.node.is_never_satisfied(db, self.support)
     }
 
     /// Returns whether this constraint set always holds
     pub(crate) fn is_always_satisfied(self, db: &'db dyn Db) -> bool {
-        self.node.is_always_satisfied(db)
+        self.node.is_always_satisfied(db, self.support)
     }
 
     /// Returns whether this constraint set contains any cycles between typevars. If it does, then
@@ -281,7 +312,7 @@ impl<'db> ConstraintSet<'db> {
             BoundTypeVarIdentity<'db>,
             FxHashSet<BoundTypeVarIdentity<'db>>,
         > = FxHashMap::default();
-        self.node.for_each_constraint(db, &mut |constraint, _| {
+        self.node.for_each_constraint(db, &mut |constraint| {
             let visitor = CollectReachability::default();
             visitor.visit_type(db, constraint.lower(db));
             visitor.visit_type(db, constraint.upper(db));
@@ -315,9 +346,26 @@ impl<'db> ConstraintSet<'db> {
         lhs: Type<'db>,
         rhs: Type<'db>,
     ) -> Self {
-        Self {
-            node: self.node.implies_subtype_of(db, lhs, rhs),
-        }
+        let mut support = FxOrderSet::default();
+        match (lhs, rhs) {
+            (Type::TypeVar(bound_typevar), _) => ConstrainedTypeVar::new_node_with_support(
+                db,
+                &mut support,
+                bound_typevar,
+                Type::Never,
+                rhs.bottom_materialization(db),
+            ),
+            (_, Type::TypeVar(bound_typevar)) => ConstrainedTypeVar::new_node_with_support(
+                db,
+                &mut support,
+                bound_typevar,
+                lhs.top_materialization(db),
+                Type::object(),
+            ),
+            _ => panic!("at least one type should be a typevar"),
+        };
+        let support = self.support.union(db, Support::new(db, support));
+        Self::with_support(db, self.node.implies_subtype_of(db, lhs, rhs), support)
     }
 
     /// Returns whether this constraint set is satisfied by all of the typevars that it mentions.
@@ -339,52 +387,46 @@ impl<'db> ConstraintSet<'db> {
         db: &'db dyn Db,
         inferable: InferableTypeVars<'_, 'db>,
     ) -> bool {
-        self.node.satisfied_by_all_typevars(db, inferable)
+        self.node
+            .satisfied_by_all_typevars(db, inferable, self.support)
     }
 
     pub(crate) fn limit_to_valid_specializations(self, db: &'db dyn Db) -> Self {
-        let mut result = self.node;
+        let mut result = self;
         let mut seen = FxHashSet::default();
-        self.node.for_each_constraint(db, &mut |constraint, _| {
+        self.node.for_each_constraint(db, &mut |constraint| {
             let bound_typevar = constraint.typevar(db);
             if seen.insert(bound_typevar) {
-                result = result.and_with_offset(db, bound_typevar.valid_specializations(db));
+                result = result.and(db, || bound_typevar.valid_specializations(db));
             }
         });
-        Self { node: result }
+        result
     }
 
     /// Updates this constraint set to hold the union of itself and another constraint set.
-    ///
-    /// In the result, `self` will appear before `other` according to the `source_order` of the BDD
-    /// nodes.
     pub(crate) fn union(&mut self, db: &'db dyn Db, other: Self) -> Self {
-        self.node = self.node.or_with_offset(db, other.node);
+        let support = self.support.union(db, other.support);
+        let node = self.node.or(db, other.node);
+        *self = Self::with_support(db, node, support);
         *self
     }
 
     /// Updates this constraint set to hold the intersection of itself and another constraint set.
-    ///
-    /// In the result, `self` will appear before `other` according to the `source_order` of the BDD
-    /// nodes.
     pub(crate) fn intersect(&mut self, db: &'db dyn Db, other: Self) -> Self {
-        self.node = self.node.and_with_offset(db, other.node);
+        let support = self.support.union(db, other.support);
+        let node = self.node.and(db, other.node);
+        *self = Self::with_support(db, node, support);
         *self
     }
 
     /// Returns the negation of this constraint set.
     pub(crate) fn negate(self, db: &'db dyn Db) -> Self {
-        Self {
-            node: self.node.negate(db),
-        }
+        Self::with_support(db, self.node.negate(db), self.support)
     }
 
     /// Returns the intersection of this constraint set and another. The other constraint set is
     /// provided as a thunk, to implement short-circuiting: the thunk is not forced if the
     /// constraint set is already saturated.
-    ///
-    /// In the result, `self` will appear before `other` according to the `source_order` of the BDD
-    /// nodes.
     pub(crate) fn and(mut self, db: &'db dyn Db, other: impl FnOnce() -> Self) -> Self {
         if !self.is_never_satisfied(db) {
             self.intersect(db, other());
@@ -395,9 +437,6 @@ impl<'db> ConstraintSet<'db> {
     /// Returns the union of this constraint set and another. The other constraint set is provided
     /// as a thunk, to implement short-circuiting: the thunk is not forced if the constraint set is
     /// already saturated.
-    ///
-    /// In the result, `self` will appear before `other` according to the `source_order` of the BDD
-    /// nodes.
     pub(crate) fn or(mut self, db: &'db dyn Db, other: impl FnOnce() -> Self) -> Self {
         if !self.is_always_satisfied(db) {
             self.union(db, other());
@@ -406,21 +445,15 @@ impl<'db> ConstraintSet<'db> {
     }
 
     /// Returns a constraint set encoding that this constraint set implies another.
-    ///
-    /// In the result, `self` will appear before `other` according to the `source_order` of the BDD
-    /// nodes.
     pub(crate) fn implies(self, db: &'db dyn Db, other: impl FnOnce() -> Self) -> Self {
         self.negate(db).or(db, other)
     }
 
     /// Returns a constraint set encoding that this constraint set is equivalent to another.
-    ///
-    /// In the result, `self` will appear before `other` according to the `source_order` of the BDD
-    /// nodes.
     pub(crate) fn iff(self, db: &'db dyn Db, other: Self) -> Self {
-        ConstraintSet {
-            node: self.node.iff_with_offset(db, other.node),
-        }
+        let support = self.support.union(db, other.support);
+        let node = self.node.iff(db, other.node);
+        Self::with_support(db, node, support)
     }
 
     /// Reduces the set of inferable typevars for this constraint set. You provide an iterator of
@@ -433,12 +466,37 @@ impl<'db> ConstraintSet<'db> {
         db: &'db dyn Db,
         to_remove: impl IntoIterator<Item = BoundTypeVarIdentity<'db>>,
     ) -> Self {
-        let node = self.node.exists(db, to_remove);
-        Self { node }
+        let to_remove: Vec<_> = to_remove.into_iter().collect();
+        let node = self
+            .node
+            .exists(db, to_remove.iter().copied(), self.support);
+        let to_remove_set: FxHashSet<_> = to_remove.into_iter().collect();
+        let mentions_removed = |ty: Type<'db>| match ty {
+            Type::TypeVar(bound_typevar) => to_remove_set.contains(&bound_typevar.identity(db)),
+            _ => false,
+        };
+        let support_constraints: FxOrderSet<_> = self
+            .support
+            .iter(db)
+            .filter(|constraint| {
+                let identity = constraint.typevar(db).identity(db);
+                if to_remove_set.contains(&identity) {
+                    return false;
+                }
+                if any_over_type(db, constraint.lower(db), &mentions_removed, false) {
+                    return false;
+                }
+                if any_over_type(db, constraint.upper(db), &mentions_removed, false) {
+                    return false;
+                }
+                true
+            })
+            .collect();
+        Self::with_support(db, node, Support::new(db, support_constraints))
     }
 
     pub(crate) fn for_each_path(self, db: &'db dyn Db, f: impl FnMut(&PathAssignments<'db>)) {
-        self.node.for_each_path(db, f);
+        self.node.for_each_path(db, self.support, f);
     }
 
     pub(crate) fn range(
@@ -467,6 +525,58 @@ impl From<bool> for ConstraintSet<'_> {
     }
 }
 
+/// The set of constraints explicitly added to a constraint set.
+#[derive(Clone, Copy, Debug, Eq, Hash, PartialEq, get_size2::GetSize, salsa::Update)]
+enum Support<'db> {
+    Empty,
+    Constraints(SupportInner<'db>),
+}
+
+impl<'db> Support<'db> {
+    fn new(db: &'db dyn Db, constraints: FxOrderSet<ConstrainedTypeVar<'db>>) -> Self {
+        if constraints.is_empty() {
+            return Support::Empty;
+        }
+        Support::Constraints(SupportInner::new(db, constraints))
+    }
+
+    fn iter(self, db: &'db dyn Db) -> impl Iterator<Item = ConstrainedTypeVar<'db>> + 'db {
+        match self {
+            Support::Empty => Either::Left(std::iter::empty()),
+            Support::Constraints(inner) => Either::Right(inner.constraints(db).iter().copied()),
+        }
+    }
+
+    fn union(self, db: &'db dyn Db, other: Self) -> Self {
+        match (self, other) {
+            (Support::Empty, Support::Empty) => Support::Empty,
+            (one @ Support::Constraints(_), Support::Empty)
+            | (Support::Empty, one @ Support::Constraints(_)) => one,
+            (Support::Constraints(self_inner), Support::Constraints(other_inner)) => {
+                let constraints: FxOrderSet<_> = self_inner
+                    .constraints(db)
+                    .union(other_inner.constraints(db))
+                    .copied()
+                    .collect();
+                Support::Constraints(SupportInner::new(db, constraints))
+            }
+        }
+    }
+
+    fn path_assignments(self, db: &'db dyn Db, node: Node<'db>) -> PathAssignments<'db> {
+        PathAssignments::new(db, self, node)
+    }
+}
+
+#[salsa::interned(debug, heap_size=ruff_memory_usage::heap_size)]
+struct SupportInner<'db> {
+    #[returns(ref)]
+    constraints: FxOrderSet<ConstrainedTypeVar<'db>>,
+}
+
+// The Salsa heap is tracked separately.
+impl get_size2::GetSize for SupportInner<'_> {}
+
 impl<'db> BoundTypeVarInstance<'db> {
     /// Returns whether this typevar can be the lower or upper bound of another typevar in a
     /// constraint set.
@@ -515,6 +625,17 @@ impl<'db> ConstrainedTypeVar<'db> {
     fn new_node(
         db: &'db dyn Db,
         typevar: BoundTypeVarInstance<'db>,
+        lower: Type<'db>,
+        upper: Type<'db>,
+    ) -> Node<'db> {
+        let mut support = FxOrderSet::default();
+        Self::new_node_with_support(db, &mut support, typevar, lower, upper)
+    }
+
+    fn new_node_with_support(
+        db: &'db dyn Db,
+        support: &mut FxOrderSet<ConstrainedTypeVar<'db>>,
+        typevar: BoundTypeVarInstance<'db>,
         mut lower: Type<'db>,
         mut upper: Type<'db>,
     ) -> Node<'db> {
@@ -529,9 +650,15 @@ impl<'db> ConstrainedTypeVar<'db> {
         if let Type::Union(lower_union) = lower {
             let mut result = Node::AlwaysTrue;
             for lower_element in lower_union.elements(db) {
-                result = result.and_with_offset(
+                result = result.and(
                     db,
-                    ConstrainedTypeVar::new_node(db, typevar, *lower_element, upper),
+                    ConstrainedTypeVar::new_node_with_support(
+                        db,
+                        support,
+                        typevar,
+                        *lower_element,
+                        upper,
+                    ),
                 );
             }
             return result;
@@ -544,15 +671,27 @@ impl<'db> ConstrainedTypeVar<'db> {
         {
             let mut result = Node::AlwaysTrue;
             for upper_element in upper_intersection.iter_positive(db) {
-                result = result.and_with_offset(
+                result = result.and(
                     db,
-                    ConstrainedTypeVar::new_node(db, typevar, lower, upper_element),
+                    ConstrainedTypeVar::new_node_with_support(
+                        db,
+                        support,
+                        typevar,
+                        lower,
+                        upper_element,
+                    ),
                 );
             }
             for upper_element in upper_intersection.iter_negative(db) {
-                result = result.and_with_offset(
+                result = result.and(
                     db,
-                    ConstrainedTypeVar::new_node(db, typevar, lower, upper_element.negate(db)),
+                    ConstrainedTypeVar::new_node_with_support(
+                        db,
+                        support,
+                        typevar,
+                        lower,
+                        upper_element.negate(db),
+                    ),
                 );
             }
             return result;
@@ -582,12 +721,9 @@ impl<'db> ConstrainedTypeVar<'db> {
                     })
                 }) =>
             {
-                return Node::new_constraint(
-                    db,
-                    ConstrainedTypeVar::new(db, typevar, Type::Never, Type::object()),
-                    1,
-                )
-                .negate(db);
+                let constraint = ConstrainedTypeVar::new(db, typevar, Type::Never, Type::object());
+                support.insert(constraint);
+                return Node::new_constraint(db, constraint).negate(db);
             }
             _ => {}
         }
@@ -629,46 +765,41 @@ impl<'db> ConstrainedTypeVar<'db> {
                 } else {
                     (typevar, lower)
                 };
-                Node::new_constraint(
+                let constraint = ConstrainedTypeVar::new(
                     db,
-                    ConstrainedTypeVar::new(
-                        db,
-                        typevar,
-                        Type::TypeVar(bound),
-                        Type::TypeVar(bound),
-                    ),
-                    1,
-                )
+                    typevar,
+                    Type::TypeVar(bound),
+                    Type::TypeVar(bound),
+                );
+                support.insert(constraint);
+                Node::new_constraint(db, constraint)
             }
 
             // L ≤ T ≤ U == ([L] ≤ T) && (T ≤ [U])
             (Type::TypeVar(lower), Type::TypeVar(upper))
                 if typevar.can_be_bound_for(db, lower) && typevar.can_be_bound_for(db, upper) =>
             {
-                let lower = Node::new_constraint(
-                    db,
-                    ConstrainedTypeVar::new(db, lower, Type::Never, Type::TypeVar(typevar)),
-                    1,
-                );
-                let upper = Node::new_constraint(
-                    db,
-                    ConstrainedTypeVar::new(db, upper, Type::TypeVar(typevar), Type::object()),
-                    1,
-                );
+                let lower_constraint =
+                    ConstrainedTypeVar::new(db, lower, Type::Never, Type::TypeVar(typevar));
+                let upper_constraint =
+                    ConstrainedTypeVar::new(db, upper, Type::TypeVar(typevar), Type::object());
+                support.insert(lower_constraint);
+                support.insert(upper_constraint);
+                let lower = Node::new_constraint(db, lower_constraint);
+                let upper = Node::new_constraint(db, upper_constraint);
                 lower.and(db, upper)
             }
 
             // L ≤ T ≤ U == ([L] ≤ T) && ([T] ≤ U)
             (Type::TypeVar(lower), _) if typevar.can_be_bound_for(db, lower) => {
-                let lower = Node::new_constraint(
-                    db,
-                    ConstrainedTypeVar::new(db, lower, Type::Never, Type::TypeVar(typevar)),
-                    1,
-                );
+                let lower_constraint =
+                    ConstrainedTypeVar::new(db, lower, Type::Never, Type::TypeVar(typevar));
+                support.insert(lower_constraint);
+                let lower = Node::new_constraint(db, lower_constraint);
                 let upper = if upper.is_object() {
                     Node::AlwaysTrue
                 } else {
-                    Self::new_node(db, typevar, Type::Never, upper)
+                    Self::new_node_with_support(db, support, typevar, Type::Never, upper)
                 };
                 lower.and(db, upper)
             }
@@ -678,17 +809,20 @@ impl<'db> ConstrainedTypeVar<'db> {
                 let lower = if lower.is_never() {
                     Node::AlwaysTrue
                 } else {
-                    Self::new_node(db, typevar, lower, Type::object())
+                    Self::new_node_with_support(db, support, typevar, lower, Type::object())
                 };
-                let upper = Node::new_constraint(
-                    db,
-                    ConstrainedTypeVar::new(db, upper, Type::TypeVar(typevar), Type::object()),
-                    1,
-                );
+                let upper_constraint =
+                    ConstrainedTypeVar::new(db, upper, Type::TypeVar(typevar), Type::object());
+                support.insert(upper_constraint);
+                let upper = Node::new_constraint(db, upper_constraint);
                 lower.and(db, upper)
             }
 
-            _ => Node::new_constraint(db, ConstrainedTypeVar::new(db, typevar, lower, upper), 1),
+            _ => {
+                let constraint = ConstrainedTypeVar::new(db, typevar, lower, upper);
+                support.insert(constraint);
+                Node::new_constraint(db, constraint)
+            }
         }
     }
 
@@ -862,22 +996,13 @@ impl<'db> ConstrainedTypeVar<'db> {
 /// Terminal nodes (`false` and `true`) have their own dedicated enum variants. The
 /// [`Interior`][InteriorNode] variant represents interior nodes.
 ///
-/// BDD nodes are _quasi-reduced_, which means that there are no duplicate nodes (which we handle
-/// via Salsa interning). Unlike the typical BDD representation, which is (fully) reduced, we do
-/// allow redundant nodes, with `if_true` and `if_false` edges that point at the same node. That
-/// means that our BDDs "remember" all of the individual constraints that they were created with.
+/// BDD nodes are fully reduced and contain no duplicate nodes (which we handle via Salsa
+/// interning). We track the constraints that were explicitly added to a constraint set separately,
+/// so the BDD itself can be fully reduced without losing that information.
 ///
 /// BDD nodes are also _ordered_, meaning that every path from the root of a BDD to a terminal node
 /// visits variables in the same order. [`ConstrainedTypeVar::ordering`] defines the variable
 /// ordering that we use for constraint set BDDs.
-///
-/// In addition to this BDD variable ordering, we also track a `source_order` for each individual
-/// constraint. This records the order in which constraints are added to the constraint set, which
-/// typically tracks when they appear in the underlying Python source code. This provides an
-/// ordering that is stable across multiple runs, for consistent test and diagnostic output. (We
-/// cannot use this ordering as our BDD variable ordering, since we calculate it from already
-/// constructed BDDs, and we need the BDD variable ordering to be fixed and available before
-/// construction starts.)
 #[derive(Clone, Copy, Debug, Eq, Hash, PartialEq, get_size2::GetSize, salsa::Update)]
 enum Node<'db> {
     AlwaysFalse,
@@ -886,13 +1011,12 @@ enum Node<'db> {
 }
 
 impl<'db> Node<'db> {
-    /// Creates a new BDD node, ensuring that it is quasi-reduced.
+    /// Creates a new BDD node, ensuring that it is fully reduced.
     fn new(
         db: &'db dyn Db,
         constraint: ConstrainedTypeVar<'db>,
         if_true: Node<'db>,
         if_false: Node<'db>,
-        source_order: usize,
     ) -> Self {
         debug_assert!((if_true.root_constraint(db)).is_none_or(|root_constraint| {
             root_constraint.ordering(db) > constraint.ordering(db)
@@ -902,63 +1026,39 @@ impl<'db> Node<'db> {
                 root_constraint.ordering(db) > constraint.ordering(db)
             })
         );
-        if if_true == Node::AlwaysFalse && if_false == Node::AlwaysFalse {
-            return Node::AlwaysFalse;
+        if if_true == if_false {
+            return if_true;
         }
-        let max_source_order = source_order
-            .max(if_true.max_source_order(db))
-            .max(if_false.max_source_order(db));
-        Self::Interior(InteriorNode::new(
-            db,
-            constraint,
-            if_true,
-            if_false,
-            source_order,
-            max_source_order,
-        ))
+        Self::Interior(InteriorNode::new(db, constraint, if_true, if_false))
     }
 
     /// Creates a new BDD node for an individual constraint. (The BDD will evaluate to `true` when
     /// the constraint holds, and to `false` when it does not.)
-    fn new_constraint(
-        db: &'db dyn Db,
-        constraint: ConstrainedTypeVar<'db>,
-        source_order: usize,
-    ) -> Self {
+    fn new_constraint(db: &'db dyn Db, constraint: ConstrainedTypeVar<'db>) -> Self {
         Self::Interior(InteriorNode::new(
             db,
             constraint,
             Node::AlwaysTrue,
             Node::AlwaysFalse,
-            source_order,
-            source_order,
         ))
     }
 
     /// Creates a new BDD node for a positive or negative individual constraint. (For a positive
     /// constraint, this returns the same BDD node as [`new_constraint`][Self::new_constraint]. For
     /// a negative constraint, it returns the negation of that BDD node.)
-    fn new_satisfied_constraint(
-        db: &'db dyn Db,
-        constraint: ConstraintAssignment<'db>,
-        source_order: usize,
-    ) -> Self {
+    fn new_satisfied_constraint(db: &'db dyn Db, constraint: ConstraintAssignment<'db>) -> Self {
         match constraint {
             ConstraintAssignment::Positive(constraint) => Self::Interior(InteriorNode::new(
                 db,
                 constraint,
                 Node::AlwaysTrue,
                 Node::AlwaysFalse,
-                source_order,
-                source_order,
             )),
             ConstraintAssignment::Negative(constraint) => Self::Interior(InteriorNode::new(
                 db,
                 constraint,
                 Node::AlwaysFalse,
                 Node::AlwaysTrue,
-                source_order,
-                source_order,
             )),
         }
     }
@@ -972,71 +1072,109 @@ impl<'db> Node<'db> {
         }
     }
 
-    fn max_source_order(self, db: &'db dyn Db) -> usize {
-        match self {
-            Node::Interior(interior) => interior.max_source_order(db),
-            Node::AlwaysTrue | Node::AlwaysFalse => 0,
-        }
-    }
-
-    /// Returns a copy of this BDD node with all `source_order`s adjusted by the given amount.
-    fn with_adjusted_source_order(self, db: &'db dyn Db, delta: usize) -> Self {
-        if delta == 0 {
-            return self;
-        }
+    fn prune_impossible_paths(self, db: &'db dyn Db, support: Support<'db>) -> Self {
         match self {
-            Node::AlwaysTrue => Node::AlwaysTrue,
-            Node::AlwaysFalse => Node::AlwaysFalse,
-            Node::Interior(interior) => Node::new(
-                db,
-                interior.constraint(db),
-                interior.if_true(db).with_adjusted_source_order(db, delta),
-                interior.if_false(db).with_adjusted_source_order(db, delta),
-                interior.source_order(db) + delta,
-            ),
+            Node::AlwaysTrue | Node::AlwaysFalse => self,
+            Node::Interior(_) => {
+                let mut path = support.path_assignments(db, self);
+                self.prune_impossible_paths_inner(db, &mut path)
+            }
         }
     }
 
-    fn for_each_path(self, db: &'db dyn Db, mut f: impl FnMut(&PathAssignments<'db>)) {
+    fn prune_impossible_paths_inner(
+        self,
+        db: &'db dyn Db,
+        path: &mut PathAssignments<'db>,
+    ) -> Self {
         match self {
-            Node::AlwaysTrue => {}
-            Node::AlwaysFalse => {}
+            Node::AlwaysTrue | Node::AlwaysFalse => self,
             Node::Interior(interior) => {
-                let mut path = interior.path_assignments(db);
-                self.for_each_path_inner(db, &mut f, &mut path);
+                let constraint = interior.constraint(db);
+                let if_true = path
+                    .walk_edge(db, constraint.when_true(), |path, _| {
+                        interior.if_true(db).prune_impossible_paths_inner(db, path)
+                    })
+                    .unwrap_or(Node::AlwaysFalse);
+                let if_false = path
+                    .walk_edge(db, constraint.when_false(), |path, _| {
+                        interior.if_false(db).prune_impossible_paths_inner(db, path)
+                    })
+                    .unwrap_or(Node::AlwaysFalse);
+                Node::new(db, constraint, if_true, if_false)
             }
         }
     }
 
+    fn for_each_path(
+        self,
+        db: &'db dyn Db,
+        support: Support<'db>,
+        mut f: impl FnMut(&PathAssignments<'db>),
+    ) {
+        let mut present = FxHashSet::default();
+        self.for_each_constraint(db, &mut |constraint| {
+            present.insert(constraint);
+        });
+        let missing = support
+            .iter(db)
+            .filter(|constraint| !present.contains(constraint))
+            .collect::<Vec<_>>();
+        let mut path = support.path_assignments(db, self);
+        self.for_each_path_inner(db, &missing, &mut f, &mut path);
+    }
+
     fn for_each_path_inner(
         self,
         db: &'db dyn Db,
+        missing: &[ConstrainedTypeVar<'db>],
         f: &mut dyn FnMut(&PathAssignments<'db>),
         path: &mut PathAssignments<'db>,
     ) {
         match self {
-            Node::AlwaysTrue => f(path),
+            Node::AlwaysTrue => Self::for_each_path_with_missing(db, missing, f, path),
             Node::AlwaysFalse => {}
             Node::Interior(interior) => {
                 let constraint = interior.constraint(db);
-                let source_order = interior.source_order(db);
-                path.walk_edge(db, constraint.when_true(), source_order, |path, _| {
-                    interior.if_true(db).for_each_path_inner(db, f, path);
+                path.walk_edge(db, constraint.when_true(), |path, _| {
+                    interior
+                        .if_true(db)
+                        .for_each_path_inner(db, missing, f, path);
                 });
-                path.walk_edge(db, constraint.when_false(), source_order, |path, _| {
-                    interior.if_false(db).for_each_path_inner(db, f, path);
+                path.walk_edge(db, constraint.when_false(), |path, _| {
+                    interior
+                        .if_false(db)
+                        .for_each_path_inner(db, missing, f, path);
                 });
             }
         }
     }
 
+    fn for_each_path_with_missing(
+        db: &'db dyn Db,
+        missing: &[ConstrainedTypeVar<'db>],
+        f: &mut dyn FnMut(&PathAssignments<'db>),
+        path: &mut PathAssignments<'db>,
+    ) {
+        if let Some((constraint, rest)) = missing.split_first() {
+            path.walk_edge(db, constraint.when_true(), |path, _| {
+                Self::for_each_path_with_missing(db, rest, f, path);
+            });
+            path.walk_edge(db, constraint.when_false(), |path, _| {
+                Self::for_each_path_with_missing(db, rest, f, path);
+            });
+        } else {
+            f(path);
+        }
+    }
+
     /// Returns whether this BDD represent the constant function `true`.
-    fn is_always_satisfied(self, db: &'db dyn Db) -> bool {
+    fn is_always_satisfied(self, db: &'db dyn Db, support: Support<'db>) -> bool {
         match self {
             Node::AlwaysTrue => true,
             Node::AlwaysFalse => false,
-            Node::Interior(interior) => {
-                let mut path = interior.path_assignments(db);
+            Node::Interior(_) => {
+                let mut path = support.path_assignments(db, self);
                 self.is_always_satisfied_inner(db, &mut path)
             }
         }
@@ -1051,9 +1189,8 @@ impl<'db> Node<'db> {
                 // from it) causes the if_true edge to become impossible. We want to ignore
                 // impossible paths, and so we treat them as passing the "always satisfied" check.
                 let constraint = interior.constraint(db);
-                let source_order = interior.source_order(db);
                 let true_always_satisfied = path
-                    .walk_edge(db, constraint.when_true(), source_order, |path, _| {
+                    .walk_edge(db, constraint.when_true(), |path, _| {
                         interior.if_true(db).is_always_satisfied_inner(db, path)
                     })
                     .unwrap_or(true);
@@ -1062,7 +1199,7 @@ impl<'db> Node<'db> {
                 }
 
                 // Ditto for the if_false branch
-                path.walk_edge(db, constraint.when_false(), source_order, |path, _| {
+                path.walk_edge(db, constraint.when_false(), |path, _| {
                     interior.if_false(db).is_always_satisfied_inner(db, path)
                 })
                 .unwrap_or(true)
@@ -1071,12 +1208,12 @@ impl<'db> Node<'db> {
     }
 
     /// Returns whether this BDD represent the constant function `false`.
-    fn is_never_satisfied(self, db: &'db dyn Db) -> bool {
+    fn is_never_satisfied(self, db: &'db dyn Db, support: Support<'db>) -> bool {
         match self {
             Node::AlwaysTrue => false,
             Node::AlwaysFalse => true,
-            Node::Interior(interior) => {
-                let mut path = interior.path_assignments(db);
+            Node::Interior(_) => {
+                let mut path = support.path_assignments(db, self);
                 self.is_never_satisfied_inner(db, &mut path)
             }
         }
@@ -1091,9 +1228,8 @@ impl<'db> Node<'db> {
                 // from it) causes the if_true edge to become impossible. We want to ignore
                 // impossible paths, and so we treat them as passing the "never satisfied" check.
                 let constraint = interior.constraint(db);
-                let source_order = interior.source_order(db);
                 let true_never_satisfied = path
-                    .walk_edge(db, constraint.when_true(), source_order, |path, _| {
+                    .walk_edge(db, constraint.when_true(), |path, _| {
                         interior.if_true(db).is_never_satisfied_inner(db, path)
                     })
                     .unwrap_or(true);
@@ -1102,7 +1238,7 @@ impl<'db> Node<'db> {
                 }
 
                 // Ditto for the if_false branch
-                path.walk_edge(db, constraint.when_false(), source_order, |path, _| {
+                path.walk_edge(db, constraint.when_false(), |path, _| {
                     interior.if_false(db).is_never_satisfied_inner(db, path)
                 })
                 .unwrap_or(true)
@@ -1119,47 +1255,13 @@ impl<'db> Node<'db> {
         }
     }
 
-    /// Returns the `or` or union of two BDDs.
-    ///
-    /// In the result, `self` will appear before `other` according to the `source_order` of the BDD
-    /// nodes.
-    fn or_with_offset(self, db: &'db dyn Db, other: Self) -> Self {
-        // To ensure that `self` appears before `other` in `source_order`, we add the maximum
-        // `source_order` of the lhs to all of the `source_order`s in the rhs.
-        //
-        // TODO: If we store `other_offset` as a new field on InteriorNode, we might be able to
-        // avoid all of the extra work in the calls to with_adjusted_source_order, and apply the
-        // adjustment lazily when walking a BDD tree. (ditto below in the other _with_offset
-        // methods)
-        let other_offset = self.max_source_order(db);
-        self.or_inner(db, other, other_offset)
-    }
-
     fn or(self, db: &'db dyn Db, other: Self) -> Self {
-        self.or_inner(db, other, 0)
-    }
-
-    fn or_inner(self, db: &'db dyn Db, other: Self, other_offset: usize) -> Self {
         match (self, other) {
-            (Node::AlwaysTrue, Node::AlwaysTrue) => Node::AlwaysTrue,
-            (Node::AlwaysTrue, Node::Interior(other_interior)) => Node::new(
-                db,
-                other_interior.constraint(db),
-                Node::AlwaysTrue,
-                Node::AlwaysTrue,
-                other_interior.source_order(db) + other_offset,
-            ),
-            (Node::Interior(self_interior), Node::AlwaysTrue) => Node::new(
-                db,
-                self_interior.constraint(db),
-                Node::AlwaysTrue,
-                Node::AlwaysTrue,
-                self_interior.source_order(db),
-            ),
-            (Node::AlwaysFalse, _) => other.with_adjusted_source_order(db, other_offset),
+            (Node::AlwaysTrue, _) | (_, Node::AlwaysTrue) => Node::AlwaysTrue,
+            (Node::AlwaysFalse, _) => other,
             (_, Node::AlwaysFalse) => self,
             (Node::Interior(self_interior), Node::Interior(other_interior)) => {
-                self_interior.or(db, other_interior, other_offset)
+                self_interior.or(db, other_interior)
             }
         }
     }
@@ -1243,61 +1345,21 @@ impl<'db> Node<'db> {
     }
 
     fn distributed_or(db: &'db dyn Db, nodes: impl Iterator<Item = Node<'db>>) -> Self {
-        Self::tree_fold(
-            db,
-            nodes,
-            Node::AlwaysFalse,
-            Node::AlwaysTrue,
-            Self::or_with_offset,
-        )
+        Self::tree_fold(db, nodes, Node::AlwaysFalse, Node::AlwaysTrue, Self::or)
     }
 
     fn distributed_and(db: &'db dyn Db, nodes: impl Iterator<Item = Node<'db>>) -> Self {
-        Self::tree_fold(
-            db,
-            nodes,
-            Node::AlwaysTrue,
-            Node::AlwaysFalse,
-            Self::and_with_offset,
-        )
+        Self::tree_fold(db, nodes, Node::AlwaysTrue, Node::AlwaysFalse, Self::and)
     }
 
     /// Returns the `and` or intersection of two BDDs.
-    ///
-    /// In the result, `self` will appear before `other` according to the `source_order` of the BDD
-    /// nodes.
-    fn and_with_offset(self, db: &'db dyn Db, other: Self) -> Self {
-        // To ensure that `self` appears before `other` in `source_order`, we add the maximum
-        // `source_order` of the lhs to all of the `source_order`s in the rhs.
-        let other_offset = self.max_source_order(db);
-        self.and_inner(db, other, other_offset)
-    }
-
     fn and(self, db: &'db dyn Db, other: Self) -> Self {
-        self.and_inner(db, other, 0)
-    }
-
-    fn and_inner(self, db: &'db dyn Db, other: Self, other_offset: usize) -> Self {
         match (self, other) {
-            (Node::AlwaysFalse, Node::AlwaysFalse) => Node::AlwaysFalse,
-            (Node::AlwaysFalse, Node::Interior(other_interior)) => Node::new(
-                db,
-                other_interior.constraint(db),
-                Node::AlwaysFalse,
-                Node::AlwaysFalse,
-                other_interior.source_order(db) + other_offset,
-            ),
-            (Node::Interior(self_interior), Node::AlwaysFalse) => Node::new(
-                db,
-                self_interior.constraint(db),
-                Node::AlwaysFalse,
-                Node::AlwaysFalse,
-                self_interior.source_order(db),
-            ),
-            (Node::AlwaysTrue, _) => other.with_adjusted_source_order(db, other_offset),
+            (Node::AlwaysFalse, _) | (_, Node::AlwaysFalse) => Node::AlwaysFalse,
+            (Node::AlwaysTrue, _) => other,
             (_, Node::AlwaysTrue) => self,
             (Node::Interior(self_interior), Node::Interior(other_interior)) => {
-                self_interior.and(db, other_interior, other_offset)
+                self_interior.and(db, other_interior)
             }
         }
     }
@@ -1307,23 +1369,7 @@ impl<'db> Node<'db> {
         self.negate(db).or(db, other)
     }
 
-    /// Returns a new BDD that evaluates to `true` when both input BDDs evaluate to the same
-    /// result.
-    ///
-    /// In the result, `self` will appear before `other` according to the `source_order` of the BDD
-    /// nodes.
-    fn iff_with_offset(self, db: &'db dyn Db, other: Self) -> Self {
-        // To ensure that `self` appears before `other` in `source_order`, we add the maximum
-        // `source_order` of the lhs to all of the `source_order`s in the rhs.
-        let other_offset = self.max_source_order(db);
-        self.iff_inner(db, other, other_offset)
-    }
-
     fn iff(self, db: &'db dyn Db, other: Self) -> Self {
-        self.iff_inner(db, other, 0)
-    }
-
-    fn iff_inner(self, db: &'db dyn Db, other: Self, other_offset: usize) -> Self {
         match (self, other) {
             (Node::AlwaysFalse, Node::AlwaysFalse) | (Node::AlwaysTrue, Node::AlwaysTrue) => {
                 Node::AlwaysTrue
@@ -1334,18 +1380,16 @@ impl<'db> Node<'db> {
             (Node::AlwaysTrue | Node::AlwaysFalse, Node::Interior(interior)) => Node::new(
                 db,
                 interior.constraint(db),
-                self.iff_inner(db, interior.if_true(db), other_offset),
-                self.iff_inner(db, interior.if_false(db), other_offset),
-                interior.source_order(db) + other_offset,
+                self.iff(db, interior.if_true(db)),
+                self.iff(db, interior.if_false(db)),
             ),
             (Node::Interior(interior), Node::AlwaysTrue | Node::AlwaysFalse) => Node::new(
                 db,
                 interior.constraint(db),
-                interior.if_true(db).iff_inner(db, other, other_offset),
-                interior.if_false(db).iff_inner(db, other, other_offset),
-                interior.source_order(db),
+                interior.if_true(db).iff(db, other),
+                interior.if_false(db).iff(db, other),
             ),
-            (Node::Interior(a), Node::Interior(b)) => a.iff(db, b, other_offset),
+            (Node::Interior(a), Node::Interior(b)) => a.iff(db, b),
         }
     }
 
@@ -1388,6 +1432,7 @@ impl<'db> Node<'db> {
         self,
         db: &'db dyn Db,
         inferable: InferableTypeVars<'_, 'db>,
+        support: Support<'db>,
     ) -> bool {
         match self {
             Node::AlwaysTrue => return true,
@@ -1396,22 +1441,30 @@ impl<'db> Node<'db> {
         }
 
         let mut typevars = FxHashSet::default();
-        self.for_each_constraint(db, &mut |constraint, _| {
+        self.for_each_constraint(db, &mut |constraint| {
             typevars.insert(constraint.typevar(db));
         });
 
         // Returns if some specialization satisfies this constraint set.
-        let some_specialization_satisfies = move |specializations: Node<'db>| {
-            let when_satisfied = specializations.implies(db, self).and(db, specializations);
-            !when_satisfied.is_never_satisfied(db)
+        let some_specialization_satisfies = move |specializations: ConstraintSet<'db>| {
+            let when_satisfied = specializations
+                .node
+                .implies(db, self)
+                .and(db, specializations.node);
+            let combined_support = support.union(db, specializations.support);
+            !when_satisfied.is_never_satisfied(db, combined_support)
         };
 
         // Returns if all specializations satisfy this constraint set.
-        let all_specializations_satisfy = move |specializations: Node<'db>| {
-            let when_satisfied = specializations.implies(db, self).and(db, specializations);
+        let all_specializations_satisfy = move |specializations: ConstraintSet<'db>| {
+            let when_satisfied = specializations
+                .node
+                .implies(db, self)
+                .and(db, specializations.node);
+            let combined_support = support.union(db, specializations.support);
             when_satisfied
-                .iff(db, specializations)
-                .is_always_satisfied(db)
+                .iff(db, specializations.node)
+                .is_always_satisfied(db, combined_support)
         };
 
         for typevar in typevars {
@@ -1457,29 +1510,40 @@ impl<'db> Node<'db> {
         self,
         db: &'db dyn Db,
         bound_typevars: impl IntoIterator<Item = BoundTypeVarIdentity<'db>>,
+        support: Support<'db>,
     ) -> Self {
         bound_typevars
             .into_iter()
             .fold(self, |abstracted, bound_typevar| {
-                abstracted.exists_one(db, bound_typevar)
+                abstracted.exists_one(db, bound_typevar, support)
             })
     }
 
-    fn exists_one(self, db: &'db dyn Db, bound_typevar: BoundTypeVarIdentity<'db>) -> Self {
+    fn exists_one(
+        self,
+        db: &'db dyn Db,
+        bound_typevar: BoundTypeVarIdentity<'db>,
+        support: Support<'db>,
+    ) -> Self {
         match self {
             Node::AlwaysTrue => Node::AlwaysTrue,
             Node::AlwaysFalse => Node::AlwaysFalse,
-            Node::Interior(interior) => interior.exists_one(db, bound_typevar),
+            Node::Interior(interior) => interior.exists_one(db, bound_typevar, support),
         }
     }
 
     /// Returns a new BDD that is the _existential abstraction_ of `self` for a set of typevars.
     /// All typevars _other_ than the one given will be removed and abstracted away.
-    fn retain_one(self, db: &'db dyn Db, bound_typevar: BoundTypeVarIdentity<'db>) -> Self {
+    fn retain_one(
+        self,
+        db: &'db dyn Db,
+        bound_typevar: BoundTypeVarIdentity<'db>,
+        support: Support<'db>,
+    ) -> Self {
         match self {
             Node::AlwaysTrue => Node::AlwaysTrue,
             Node::AlwaysFalse => Node::AlwaysFalse,
-            Node::Interior(interior) => interior.retain_one(db, bound_typevar),
+            Node::Interior(interior) => interior.retain_one(db, bound_typevar, support),
         }
     }
 
@@ -1512,85 +1576,44 @@ impl<'db> Node<'db> {
         self,
         db: &'db dyn Db,
         bound_typevar: BoundTypeVarIdentity<'db>,
+        support: Support<'db>,
         mut f: impl FnMut(Option<&[RepresentativeBounds<'db>]>),
     ) {
-        self.retain_one(db, bound_typevar)
-            .find_representative_types_inner(db, &mut Vec::default(), &mut f);
-    }
-
-    fn find_representative_types_inner(
-        self,
-        db: &'db dyn Db,
-        current_bounds: &mut Vec<RepresentativeBounds<'db>>,
-        f: &mut dyn FnMut(Option<&[RepresentativeBounds<'db>]>),
-    ) {
-        match self {
-            Node::AlwaysTrue => {
-                // If we reach the `true` terminal, the path we've been following represents one
-                // representative type.
-                if current_bounds.is_empty() {
-                    f(None);
-                    return;
-                }
-
-                // If `lower ≰ upper`, then this path somehow represents in invalid specialization.
-                // That should have been removed from the BDD domain as part of the simplification
-                // process. (Here we are just checking assignability, so we don't need to construct
-                // the lower and upper bounds in a consistent order.)
-                debug_assert!({
-                    let greatest_lower_bound = UnionType::from_elements(
-                        db,
-                        current_bounds.iter().map(|bounds| bounds.lower),
-                    );
-                    let least_upper_bound = IntersectionType::from_elements(
-                        db,
-                        current_bounds.iter().map(|bounds| bounds.upper),
-                    );
-                    greatest_lower_bound.is_constraint_set_assignable_to(db, least_upper_bound)
-                });
-
-                // We've been tracking the lower and upper bound that the types for this path must
-                // satisfy. Pass those bounds along and let the caller choose a representative type
-                // from within that range.
-                f(Some(current_bounds));
+        let retained = self.retain_one(db, bound_typevar, support);
+        let support = support
+            .iter(db)
+            .filter(|constraint| constraint.typevar(db).identity(db) == bound_typevar)
+            .collect();
+        let support = Support::new(db, support);
+        retained.for_each_path(db, support, |path| {
+            let mut bounds: Vec<_> = path
+                .positive_constraints()
+                .map(|(constraint, source_order)| {
+                    RepresentativeBounds::new(
+                        constraint.lower(db),
+                        constraint.upper(db),
+                        source_order,
+                    )
+                })
+                .collect();
+            if bounds.is_empty() {
+                f(None);
+                return;
             }
 
-            Node::AlwaysFalse => {
-                // If we reach the `false` terminal, the path we've been following represents an
-                // invalid specialization, so we skip it.
+            // If `lower ≰ upper`, then this path represents an invalid specialization and should
+            // be skipped.
+            let greatest_lower_bound =
+                UnionType::from_elements(db, bounds.iter().map(|bounds| bounds.lower));
+            let least_upper_bound =
+                IntersectionType::from_elements(db, bounds.iter().map(|bounds| bounds.upper));
+            if !greatest_lower_bound.is_constraint_set_assignable_to(db, least_upper_bound) {
+                return;
             }
 
-            Node::Interior(interior) => {
-                let reset_point = current_bounds.len();
-
-                // For an interior node, there are two outgoing paths: one for the `if_true`
-                // branch, and one for the `if_false` branch.
-                //
-                // For the `if_true` branch, this node's constraint places additional restrictions
-                // on the types that satisfy the current path through the BDD. So we intersect the
-                // current glb/lub with the constraint's bounds to get the new glb/lub for the
-                // recursive call.
-                current_bounds.push(RepresentativeBounds::from_interior_node(db, interior));
-                interior
-                    .if_true(db)
-                    .find_representative_types_inner(db, current_bounds, f);
-                current_bounds.truncate(reset_point);
-
-                // For the `if_false` branch, then the types that satisfy the current path through
-                // the BDD do _not_ satisfy the node's constraint. Because we used `retain_one` to
-                // abstract the BDD to a single typevar, we don't need to worry about how that
-                // negative constraint affects the lower/upper bound that we're tracking. The
-                // abstraction process will have compared the negative constraint with all of the
-                // other constraints in the BDD, and added new interior nodes to handle the
-                // combination of those constraints. So we can recurse down the `if_false` branch
-                // without updating the lower/upper bounds, relying on the other constraints along
-                // the path to incorporate that negative "hole" in the set of valid types for this
-                // path.
-                interior
-                    .if_false(db)
-                    .find_representative_types_inner(db, current_bounds, f);
-            }
-        }
+            bounds.sort_by_key(|bounds| bounds.source_order);
+            f(Some(&bounds));
+        });
     }
 
     /// Returns a new BDD that returns the same results as `self`, but with some inputs fixed to
@@ -1629,9 +1652,7 @@ impl<'db> Node<'db> {
         self,
         db: &'db dyn Db,
         left: ConstraintAssignment<'db>,
-        left_source_order: usize,
         right: ConstraintAssignment<'db>,
-        right_source_order: usize,
         replacement: Node<'db>,
     ) -> Self {
         // We perform a Shannon expansion to find out what the input BDD evaluates to when:
@@ -1665,8 +1686,8 @@ impl<'db> Node<'db> {
         //     false
         //
         //  (Note that the `else` branch shouldn't be reachable, but we have to provide something!)
-        let left_node = Node::new_satisfied_constraint(db, left, left_source_order);
-        let right_node = Node::new_satisfied_constraint(db, right, right_source_order);
+        let left_node = Node::new_satisfied_constraint(db, left);
+        let right_node = Node::new_satisfied_constraint(db, right);
         let right_result = right_node.ite(db, Node::AlwaysFalse, when_left_but_not_right);
         let left_result = left_node.ite(db, right_result, when_not_left);
         let result = replacement.ite(db, when_left_and_right, left_result);
@@ -1689,9 +1710,7 @@ impl<'db> Node<'db> {
         self,
         db: &'db dyn Db,
         left: ConstraintAssignment<'db>,
-        left_source_order: usize,
         right: ConstraintAssignment<'db>,
-        right_source_order: usize,
         replacement: Node<'db>,
     ) -> Self {
         // We perform a Shannon expansion to find out what the input BDD evaluates to when:
@@ -1731,8 +1750,8 @@ impl<'db> Node<'db> {
         // Lastly, verify that the result is consistent with the input. (It must produce the same
         // results when `left ∨ right`.) If it doesn't, the substitution isn't valid, and we should
         // return the original BDD unmodified.
-        let left_node = Node::new_satisfied_constraint(db, left, left_source_order);
-        let right_node = Node::new_satisfied_constraint(db, right, right_source_order);
+        let left_node = Node::new_satisfied_constraint(db, left);
+        let right_node = Node::new_satisfied_constraint(db, right);
         let validity = replacement.iff(db, left_node.or(db, right_node));
         let constrained_original = self.and(db, validity);
         let constrained_replacement = result.and(db, validity);
@@ -1747,15 +1766,11 @@ impl<'db> Node<'db> {
     /// constraint can appear multiple times in different paths from the root; we do not
     /// deduplicate those constraints, and will instead invoke the callback each time we encounter
     /// the constraint.)
-    fn for_each_constraint(
-        self,
-        db: &'db dyn Db,
-        f: &mut dyn FnMut(ConstrainedTypeVar<'db>, usize),
-    ) {
+    fn for_each_constraint(self, db: &'db dyn Db, f: &mut dyn FnMut(ConstrainedTypeVar<'db>)) {
         let Node::Interior(interior) = self else {
             return;
         };
-        f(interior.constraint(db), interior.source_order(db));
+        f(interior.constraint(db));
         interior.if_true(db).for_each_constraint(db, f);
         interior.if_false(db).for_each_constraint(db, f);
     }
@@ -1891,13 +1906,7 @@ impl<'db> Node<'db> {
                     if !is_new {
                         return write!(f, "<{index}> SHARED");
                     }
-                    write!(
-                        f,
-                        "<{index}> {} {}/{}",
-                        interior.constraint(db).display(db),
-                        interior.source_order(db),
-                        interior.max_source_order(db),
-                    )?;
+                    write!(f, "<{index}> {}", interior.constraint(db).display(db))?;
                     // Calling display_graph recursively here causes rustc to claim that the
                     // expect(unused) up above is unfulfilled!
                     write!(f, "\n{prefix}┡━₁ ",)?;
@@ -1944,11 +1953,7 @@ struct RepresentativeBounds<'db> {
 }
 
 impl<'db> RepresentativeBounds<'db> {
-    fn from_interior_node(db: &'db dyn Db, interior: InteriorNode<'db>) -> Self {
-        let constraint = interior.constraint(db);
-        let lower = constraint.lower(db);
-        let upper = constraint.upper(db);
-        let source_order = interior.source_order(db);
+    fn new(lower: Type<'db>, upper: Type<'db>, source_order: usize) -> Self {
         Self {
             lower,
             upper,
@@ -1963,16 +1968,6 @@ struct InteriorNode<'db> {
     constraint: ConstrainedTypeVar<'db>,
     if_true: Node<'db>,
     if_false: Node<'db>,
-
-    /// Represents the order in which this node's constraint was added to the containing constraint
-    /// set, relative to all of the other constraints in the set. This starts off at 1 for a simple
-    /// single-constraint set (e.g. created with [`Node::new_constraint`] or
-    /// [`Node::new_satisfied_constraint`]). It will get incremented, if needed, as that simple BDD
-    /// is combined into larger BDDs.
-    source_order: usize,
-
-    /// The maximum `source_order` across this node and all of its descendants.
-    max_source_order: usize,
 }
 
 // The Salsa heap is tracked separately.
@@ -1987,112 +1982,95 @@ impl<'db> InteriorNode<'db> {
             self.constraint(db),
             self.if_true(db).negate(db),
             self.if_false(db).negate(db),
-            self.source_order(db),
         )
     }
 
     #[salsa::tracked(heap_size=ruff_memory_usage::heap_size)]
-    fn or(self, db: &'db dyn Db, other: Self, other_offset: usize) -> Node<'db> {
+    fn or(self, db: &'db dyn Db, other: Self) -> Node<'db> {
         let self_constraint = self.constraint(db);
         let other_constraint = other.constraint(db);
         match (self_constraint.ordering(db)).cmp(&other_constraint.ordering(db)) {
             Ordering::Equal => Node::new(
                 db,
                 self_constraint,
-                self.if_true(db)
-                    .or_inner(db, other.if_true(db), other_offset),
-                self.if_false(db)
-                    .or_inner(db, other.if_false(db), other_offset),
-                self.source_order(db),
+                self.if_true(db).or(db, other.if_true(db)),
+                self.if_false(db).or(db, other.if_false(db)),
             ),
             Ordering::Less => Node::new(
                 db,
                 self_constraint,
-                self.if_true(db)
-                    .or_inner(db, Node::Interior(other), other_offset),
-                self.if_false(db)
-                    .or_inner(db, Node::Interior(other), other_offset),
-                self.source_order(db),
+                self.if_true(db).or(db, Node::Interior(other)),
+                self.if_false(db).or(db, Node::Interior(other)),
             ),
             Ordering::Greater => Node::new(
                 db,
                 other_constraint,
-                Node::Interior(self).or_inner(db, other.if_true(db), other_offset),
-                Node::Interior(self).or_inner(db, other.if_false(db), other_offset),
-                other.source_order(db) + other_offset,
+                Node::Interior(self).or(db, other.if_true(db)),
+                Node::Interior(self).or(db, other.if_false(db)),
             ),
         }
     }
 
     #[salsa::tracked(heap_size=ruff_memory_usage::heap_size)]
-    fn and(self, db: &'db dyn Db, other: Self, other_offset: usize) -> Node<'db> {
+    fn and(self, db: &'db dyn Db, other: Self) -> Node<'db> {
         let self_constraint = self.constraint(db);
         let other_constraint = other.constraint(db);
         match (self_constraint.ordering(db)).cmp(&other_constraint.ordering(db)) {
             Ordering::Equal => Node::new(
                 db,
                 self_constraint,
-                self.if_true(db)
-                    .and_inner(db, other.if_true(db), other_offset),
-                self.if_false(db)
-                    .and_inner(db, other.if_false(db), other_offset),
-                self.source_order(db),
+                self.if_true(db).and(db, other.if_true(db)),
+                self.if_false(db).and(db, other.if_false(db)),
             ),
             Ordering::Less => Node::new(
                 db,
                 self_constraint,
-                self.if_true(db)
-                    .and_inner(db, Node::Interior(other), other_offset),
-                self.if_false(db)
-                    .and_inner(db, Node::Interior(other), other_offset),
-                self.source_order(db),
+                self.if_true(db).and(db, Node::Interior(other)),
+                self.if_false(db).and(db, Node::Interior(other)),
             ),
             Ordering::Greater => Node::new(
                 db,
                 other_constraint,
-                Node::Interior(self).and_inner(db, other.if_true(db), other_offset),
-                Node::Interior(self).and_inner(db, other.if_false(db), other_offset),
-                other.source_order(db) + other_offset,
+                Node::Interior(self).and(db, other.if_true(db)),
+                Node::Interior(self).and(db, other.if_false(db)),
             ),
         }
     }
 
     #[salsa::tracked(heap_size=ruff_memory_usage::heap_size)]
-    fn iff(self, db: &'db dyn Db, other: Self, other_offset: usize) -> Node<'db> {
+    fn iff(self, db: &'db dyn Db, other: Self) -> Node<'db> {
         let self_constraint = self.constraint(db);
         let other_constraint = other.constraint(db);
         match (self_constraint.ordering(db)).cmp(&other_constraint.ordering(db)) {
             Ordering::Equal => Node::new(
                 db,
                 self_constraint,
-                self.if_true(db)
-                    .iff_inner(db, other.if_true(db), other_offset),
-                self.if_false(db)
-                    .iff_inner(db, other.if_false(db), other_offset),
-                self.source_order(db),
+                self.if_true(db).iff(db, other.if_true(db)),
+                self.if_false(db).iff(db, other.if_false(db)),
             ),
             Ordering::Less => Node::new(
                 db,
                 self_constraint,
-                self.if_true(db)
-                    .iff_inner(db, Node::Interior(other), other_offset),
-                self.if_false(db)
-                    .iff_inner(db, Node::Interior(other), other_offset),
-                self.source_order(db),
+                self.if_true(db).iff(db, Node::Interior(other)),
+                self.if_false(db).iff(db, Node::Interior(other)),
             ),
             Ordering::Greater => Node::new(
                 db,
                 other_constraint,
-                Node::Interior(self).iff_inner(db, other.if_true(db), other_offset),
-                Node::Interior(self).iff_inner(db, other.if_false(db), other_offset),
-                other.source_order(db) + other_offset,
+                Node::Interior(self).iff(db, other.if_true(db)),
+                Node::Interior(self).iff(db, other.if_false(db)),
             ),
         }
     }
 
     #[salsa::tracked(heap_size=ruff_memory_usage::heap_size)]
-    fn exists_one(self, db: &'db dyn Db, bound_typevar: BoundTypeVarIdentity<'db>) -> Node<'db> {
-        let mut path = self.path_assignments(db);
+    fn exists_one(
+        self,
+        db: &'db dyn Db,
+        bound_typevar: BoundTypeVarIdentity<'db>,
+        support: Support<'db>,
+    ) -> Node<'db> {
+        let mut path = support.path_assignments(db, Node::Interior(self));
         let mentions_typevar = |ty: Type<'db>| match ty {
             Type::TypeVar(haystack) => haystack.identity(db) == bound_typevar,
             _ => false,
@@ -2123,8 +2101,13 @@ impl<'db> InteriorNode<'db> {
     }
 
     #[salsa::tracked(heap_size=ruff_memory_usage::heap_size)]
-    fn retain_one(self, db: &'db dyn Db, bound_typevar: BoundTypeVarIdentity<'db>) -> Node<'db> {
-        let mut path = self.path_assignments(db);
+    fn retain_one(
+        self,
+        db: &'db dyn Db,
+        bound_typevar: BoundTypeVarIdentity<'db>,
+        support: Support<'db>,
+    ) -> Node<'db> {
+        let mut path = support.path_assignments(db, Node::Interior(self));
         self.abstract_one_inner(
             db,
             // Remove any node that constrains some other typevar than `bound_typevar`, and any
@@ -2151,7 +2134,6 @@ impl<'db> InteriorNode<'db> {
         path: &mut PathAssignments<'db>,
     ) -> Node<'db> {
         let self_constraint = self.constraint(db);
-        let self_source_order = self.source_order(db);
         if should_remove(self_constraint) {
             // If we should remove constraints involving this typevar, then we replace this node
             // with the OR of its if_false/if_true edges. That is, the result is true if there's
@@ -2159,88 +2141,57 @@ impl<'db> InteriorNode<'db> {
             //
             // We also have to check if there are any derived facts that depend on the constraint
             // we're about to remove. If so, we need to "remember" them by AND-ing them in with the
-            // corresponding branch. We currently reuse the `source_order` of the constraint being
-            // removed when we add these derived facts.
-            //
-            // TODO: This might not be stable enough, if we add more than one derived fact for this
-            // constraint. If we still see inconsistent test output, we might need a more complex
-            // way of tracking source order for derived facts.
-            let self_source_order = self.source_order(db);
+            // corresponding branch.
             let if_true = path
-                .walk_edge(
-                    db,
-                    self_constraint.when_true(),
-                    self_source_order,
-                    |path, new_range| {
-                        let branch = self.if_true(db).abstract_one_inner(db, should_remove, path);
-                        path.assignments[new_range]
-                            .iter()
-                            .filter(|(assignment, _)| {
-                                // Don't add back any derived facts if they are ones that we would have
-                                // removed!
-                                !should_remove(assignment.constraint())
-                            })
-                            .fold(branch, |branch, (assignment, source_order)| {
-                                branch.and(
-                                    db,
-                                    Node::new_satisfied_constraint(db, *assignment, *source_order),
-                                )
-                            })
-                    },
-                )
+                .walk_edge(db, self_constraint.when_true(), |path, new_range| {
+                    let branch = self.if_true(db).abstract_one_inner(db, should_remove, path);
+                    path.assignments[new_range]
+                        .iter()
+                        .filter(|(assignment, _)| {
+                            // Don't add back any derived facts if they are ones that we would have
+                            // removed!
+                            !should_remove(assignment.constraint())
+                        })
+                        .fold(branch, |branch, (assignment, _)| {
+                            branch.and(db, Node::new_satisfied_constraint(db, *assignment))
+                        })
+                })
                 .unwrap_or(Node::AlwaysFalse);
             let if_false = path
-                .walk_edge(
-                    db,
-                    self_constraint.when_false(),
-                    self_source_order,
-                    |path, new_range| {
-                        let branch = self
-                            .if_false(db)
-                            .abstract_one_inner(db, should_remove, path);
-                        path.assignments[new_range]
-                            .iter()
-                            .filter(|(assignment, _)| {
-                                // Don't add back any derived facts if they are ones that we would have
-                                // removed!
-                                !should_remove(assignment.constraint())
-                            })
-                            .fold(branch, |branch, (assignment, source_order)| {
-                                branch.and(
-                                    db,
-                                    Node::new_satisfied_constraint(db, *assignment, *source_order),
-                                )
-                            })
-                    },
-                )
+                .walk_edge(db, self_constraint.when_false(), |path, new_range| {
+                    let branch = self
+                        .if_false(db)
+                        .abstract_one_inner(db, should_remove, path);
+                    path.assignments[new_range]
+                        .iter()
+                        .filter(|(assignment, _)| {
+                            // Don't add back any derived facts if they are ones that we would have
+                            // removed!
+                            !should_remove(assignment.constraint())
+                        })
+                        .fold(branch, |branch, (assignment, _)| {
+                            branch.and(db, Node::new_satisfied_constraint(db, *assignment))
+                        })
+                })
                 .unwrap_or(Node::AlwaysFalse);
             if_true.or(db, if_false)
         } else {
             // Otherwise, we abstract the if_false/if_true edges recursively.
             let if_true = path
-                .walk_edge(
-                    db,
-                    self_constraint.when_true(),
-                    self_source_order,
-                    |path, _| self.if_true(db).abstract_one_inner(db, should_remove, path),
-                )
+                .walk_edge(db, self_constraint.when_true(), |path, _| {
+                    self.if_true(db).abstract_one_inner(db, should_remove, path)
+                })
                 .unwrap_or(Node::AlwaysFalse);
             let if_false = path
-                .walk_edge(
-                    db,
-                    self_constraint.when_false(),
-                    self_source_order,
-                    |path, _| {
-                        self.if_false(db)
-                            .abstract_one_inner(db, should_remove, path)
-                    },
-                )
+                .walk_edge(db, self_constraint.when_false(), |path, _| {
+                    self.if_false(db)
+                        .abstract_one_inner(db, should_remove, path)
+                })
                 .unwrap_or(Node::AlwaysFalse);
             // NB: We cannot use `Node::new` here, because the recursive calls might introduce new
             // derived constraints into the result, and those constraints might appear before this
             // one in the BDD ordering.
-            Node::new_constraint(db, self_constraint, self.source_order(db))
-                .ite(db, if_true, if_false)
+            Node::new_constraint(db, self_constraint).ite(db, if_true, if_false)
         }
     }
 
@@ -2268,32 +2219,12 @@ impl<'db> InteriorNode<'db> {
             let (if_true, found_in_true) = self.if_true(db).restrict_one(db, assignment);
             let (if_false, found_in_false) = self.if_false(db).restrict_one(db, assignment);
             (
-                Node::new(
-                    db,
-                    self_constraint,
-                    if_true,
-                    if_false,
-                    self.source_order(db),
-                ),
+                Node::new(db, self_constraint, if_true, if_false),
                 found_in_true || found_in_false,
             )
         }
     }
 
-    fn path_assignments(self, db: &'db dyn Db) -> PathAssignments<'db> {
-        // Sort the constraints in this BDD by their `source_order`s before adding them to the
-        // sequent map. This ensures that constraints appear in the sequent map in a stable order.
-        // The constraints mentioned in a BDD should all have distinct `source_order`s, so an
-        // unstable sort is fine.
-        let mut constraints: SmallVec<[_; 8]> = SmallVec::new();
-        Node::Interior(self).for_each_constraint(db, &mut |constraint, source_order| {
-            constraints.push((constraint, source_order));
-        });
-        constraints.sort_unstable_by_key(|(_, source_order)| *source_order);
-
-        PathAssignments::new(constraints.into_iter().map(|(constraint, _)| constraint))
-    }
-
     /// Returns a simplified version of a BDD.
     ///
     /// This is calculated by looking at the relationships that exist between the constraints that
@@ -2317,26 +2248,17 @@ impl<'db> InteriorNode<'db> {
         // visit queue with all pairs of those constraints. (We use "combinations" because we don't
         // need to compare a constraint against itself, and because ordering doesn't matter.)
         let mut seen_constraints = FxHashSet::default();
-        let mut source_orders = FxHashMap::default();
-        Node::Interior(self).for_each_constraint(db, &mut |constraint, source_order| {
+        Node::Interior(self).for_each_constraint(db, &mut |constraint| {
             seen_constraints.insert(constraint);
-            source_orders.insert(constraint, source_order);
         });
         let mut to_visit: Vec<(_, _)> = (seen_constraints.iter().copied())
             .tuple_combinations()
             .collect();
 
         // Repeatedly pop constraint pairs off of the visit queue, checking whether each pair can
-        // be simplified. If we add any derived constraints, we will place them at the end in
-        // source order. (We do not have any test cases that depend on constraint sets being
-        // displayed in a consistent ordering, so we don't need to be clever in assigning these
-        // `source_order`s.)
+        // be simplified.
         let mut simplified = Node::Interior(self);
-        let mut next_source_order = self.max_source_order(db) + 1;
         while let Some((left_constraint, right_constraint)) = to_visit.pop() {
-            let left_source_order = source_orders[&left_constraint];
-            let right_source_order = source_orders[&right_constraint];
-
             // If the constraints refer to different typevars, the only simplifications we can make
             // are of the form `S ≤ T ∧ T ≤ int → S ≤ int`.
             let left_typevar = left_constraint.typevar(db);
@@ -2402,18 +2324,11 @@ impl<'db> InteriorNode<'db> {
                 if seen_constraints.contains(&new_constraint) {
                     continue;
                 }
-                let new_node = Node::new_constraint(db, new_constraint, next_source_order);
-                next_source_order += 1;
-                let positive_left_node = Node::new_satisfied_constraint(
-                    db,
-                    left_constraint.when_true(),
-                    left_source_order,
-                );
-                let positive_right_node = Node::new_satisfied_constraint(
-                    db,
-                    right_constraint.when_true(),
-                    right_source_order,
-                );
+                let new_node = Node::new_constraint(db, new_constraint);
+                let positive_left_node =
+                    Node::new_satisfied_constraint(db, left_constraint.when_true());
+                let positive_right_node =
+                    Node::new_satisfied_constraint(db, right_constraint.when_true());
                 let lhs = positive_left_node.and(db, positive_right_node);
                 let intersection = new_node.ite(db, lhs, Node::AlwaysFalse);
                 simplified = simplified.and(db, intersection);
@@ -2436,47 +2351,23 @@ impl<'db> InteriorNode<'db> {
             // Containment: The range of one constraint might completely contain the range of the
             // other. If so, there are several potential simplifications.
             let larger_smaller = if left_constraint.implies(db, right_constraint) {
-                Some((
-                    right_constraint,
-                    right_source_order,
-                    left_constraint,
-                    left_source_order,
-                ))
+                Some((right_constraint, left_constraint))
             } else if right_constraint.implies(db, left_constraint) {
-                Some((
-                    left_constraint,
-                    left_source_order,
-                    right_constraint,
-                    right_source_order,
-                ))
+                Some((left_constraint, right_constraint))
             } else {
                 None
             };
-            if let Some((
-                larger_constraint,
-                larger_source_order,
-                smaller_constraint,
-                smaller_source_order,
-            )) = larger_smaller
-            {
-                let positive_larger_node = Node::new_satisfied_constraint(
-                    db,
-                    larger_constraint.when_true(),
-                    larger_source_order,
-                );
-                let negative_larger_node = Node::new_satisfied_constraint(
-                    db,
-                    larger_constraint.when_false(),
-                    larger_source_order,
-                );
+            if let Some((larger_constraint, smaller_constraint)) = larger_smaller {
+                let positive_larger_node =
+                    Node::new_satisfied_constraint(db, larger_constraint.when_true());
+                let negative_larger_node =
+                    Node::new_satisfied_constraint(db, larger_constraint.when_false());
 
                 // larger ∨ smaller = larger
                 simplified = simplified.substitute_union(
                     db,
                     larger_constraint.when_true(),
-                    larger_source_order,
                     smaller_constraint.when_true(),
-                    smaller_source_order,
                     positive_larger_node,
                 );
 
@@ -2484,9 +2375,7 @@ impl<'db> InteriorNode<'db> {
                 simplified = simplified.substitute_intersection(
                     db,
                     larger_constraint.when_false(),
-                    larger_source_order,
                     smaller_constraint.when_false(),
-                    smaller_source_order,
                     negative_larger_node,
                 );
 
@@ -2495,9 +2384,7 @@ impl<'db> InteriorNode<'db> {
                 simplified = simplified.substitute_intersection(
                     db,
                     larger_constraint.when_false(),
-                    larger_source_order,
                     smaller_constraint.when_true(),
-                    smaller_source_order,
                     Node::AlwaysFalse,
                 );
 
@@ -2506,9 +2393,7 @@ impl<'db> InteriorNode<'db> {
                 simplified = simplified.substitute_union(
                     db,
                     larger_constraint.when_true(),
-                    larger_source_order,
                     smaller_constraint.when_false(),
-                    smaller_source_order,
                     Node::AlwaysTrue,
                 );
             }
@@ -2524,54 +2409,32 @@ impl<'db> InteriorNode<'db> {
                     // represent that intersection. We also need to add the new constraint to our
                     // seen set and (if we haven't already seen it) to the to-visit queue.
                     if seen_constraints.insert(intersection_constraint) {
-                        source_orders.insert(intersection_constraint, next_source_order);
                         to_visit.extend(
                             (seen_constraints.iter().copied())
                                 .filter(|seen| *seen != intersection_constraint)
                                 .map(|seen| (seen, intersection_constraint)),
                         );
                     }
-                    let positive_intersection_node = Node::new_satisfied_constraint(
-                        db,
-                        intersection_constraint.when_true(),
-                        next_source_order,
-                    );
-                    let negative_intersection_node = Node::new_satisfied_constraint(
-                        db,
-                        intersection_constraint.when_false(),
-                        next_source_order,
-                    );
-                    next_source_order += 1;
+                    let positive_intersection_node =
+                        Node::new_satisfied_constraint(db, intersection_constraint.when_true());
+                    let negative_intersection_node =
+                        Node::new_satisfied_constraint(db, intersection_constraint.when_false());
 
-                    let positive_left_node = Node::new_satisfied_constraint(
-                        db,
-                        left_constraint.when_true(),
-                        left_source_order,
-                    );
-                    let negative_left_node = Node::new_satisfied_constraint(
-                        db,
-                        left_constraint.when_false(),
-                        left_source_order,
-                    );
+                    let positive_left_node =
+                        Node::new_satisfied_constraint(db, left_constraint.when_true());
+                    let negative_left_node =
+                        Node::new_satisfied_constraint(db, left_constraint.when_false());
 
-                    let positive_right_node = Node::new_satisfied_constraint(
-                        db,
-                        right_constraint.when_true(),
-                        right_source_order,
-                    );
-                    let negative_right_node = Node::new_satisfied_constraint(
-                        db,
-                        right_constraint.when_false(),
-                        right_source_order,
-                    );
+                    let positive_right_node =
+                        Node::new_satisfied_constraint(db, right_constraint.when_true());
+                    let negative_right_node =
+                        Node::new_satisfied_constraint(db, right_constraint.when_false());
 
                     // left ∧ right = intersection
                     simplified = simplified.substitute_intersection(
                         db,
                         left_constraint.when_true(),
-                        left_source_order,
                         right_constraint.when_true(),
-                        right_source_order,
                         positive_intersection_node,
                     );
 
@@ -2579,9 +2442,7 @@ impl<'db> InteriorNode<'db> {
                     simplified = simplified.substitute_union(
                         db,
                         left_constraint.when_false(),
-                        left_source_order,
                         right_constraint.when_false(),
-                        right_source_order,
                         negative_intersection_node,
                     );
 
@@ -2591,9 +2452,7 @@ impl<'db> InteriorNode<'db> {
                     simplified = simplified.substitute_intersection(
                         db,
                         left_constraint.when_true(),
-                        left_source_order,
                         right_constraint.when_false(),
-                        right_source_order,
                         positive_left_node.and(db, negative_intersection_node),
                     );
 
@@ -2602,9 +2461,7 @@ impl<'db> InteriorNode<'db> {
                     simplified = simplified.substitute_intersection(
                         db,
                         left_constraint.when_false(),
-                        left_source_order,
                         right_constraint.when_true(),
-                        right_source_order,
                         positive_right_node.and(db, negative_intersection_node),
                     );
 
@@ -2614,9 +2471,7 @@ impl<'db> InteriorNode<'db> {
                     simplified = simplified.substitute_union(
                         db,
                         left_constraint.when_true(),
-                        left_source_order,
                         right_constraint.when_false(),
-                        right_source_order,
                         negative_right_node.or(db, positive_intersection_node),
                     );
 
@@ -2625,9 +2480,7 @@ impl<'db> InteriorNode<'db> {
                     simplified = simplified.substitute_union(
                         db,
                         left_constraint.when_false(),
-                        left_source_order,
                         right_constraint.when_true(),
-                        right_source_order,
                         negative_left_node.or(db, positive_intersection_node),
                     );
                 }
@@ -2640,24 +2493,16 @@ impl<'db> InteriorNode<'db> {
                     // All of the below hold because we just proved that the intersection of left
                     // and right is empty.
 
-                    let positive_left_node = Node::new_satisfied_constraint(
-                        db,
-                        left_constraint.when_true(),
-                        left_source_order,
-                    );
-                    let positive_right_node = Node::new_satisfied_constraint(
-                        db,
-                        right_constraint.when_true(),
-                        right_source_order,
-                    );
+                    let positive_left_node =
+                        Node::new_satisfied_constraint(db, left_constraint.when_true());
+                    let positive_right_node =
+                        Node::new_satisfied_constraint(db, right_constraint.when_true());
 
                     // left ∧ right = false
                     simplified = simplified.substitute_intersection(
                         db,
                         left_constraint.when_true(),
-                        left_source_order,
                         right_constraint.when_true(),
-                        right_source_order,
                         Node::AlwaysFalse,
                     );
 
@@ -2665,9 +2510,7 @@ impl<'db> InteriorNode<'db> {
                     simplified = simplified.substitute_union(
                         db,
                         left_constraint.when_false(),
-                        left_source_order,
                         right_constraint.when_false(),
-                        right_source_order,
                         Node::AlwaysTrue,
                     );
 
@@ -2676,9 +2519,7 @@ impl<'db> InteriorNode<'db> {
                     simplified = simplified.substitute_intersection(
                         db,
                         left_constraint.when_true(),
-                        left_source_order,
                         right_constraint.when_false(),
-                        right_source_order,
                         positive_left_node,
                     );
 
@@ -2687,9 +2528,7 @@ impl<'db> InteriorNode<'db> {
                     simplified = simplified.substitute_intersection(
                         db,
                         left_constraint.when_false(),
-                        left_source_order,
                         right_constraint.when_true(),
-                        right_source_order,
                         positive_right_node,
                     );
                 }
@@ -3408,11 +3247,15 @@ pub(crate) struct PathAssignments<'db> {
 }
 
 impl<'db> PathAssignments<'db> {
-    fn new(constraints: impl IntoIterator<Item = ConstrainedTypeVar<'db>>) -> Self {
-        let discovered = constraints
-            .into_iter()
+    fn new(db: &'db dyn Db, support: Support<'db>, node: Node<'db>) -> Self {
+        let mut discovered: FxIndexMap<_, _> = support
+            .iter(db)
             .map(|constraint| (constraint, false))
             .collect();
+        node.for_each_constraint(db, &mut |constraint| {
+            discovered.insert(constraint, false);
+        });
+
         Self {
             map: SequentMap::default(),
             assignments: FxIndexMap::default(),
@@ -3446,7 +3289,6 @@ impl<'db> PathAssignments<'db> {
         &mut self,
         db: &'db dyn Db,
         assignment: ConstraintAssignment<'db>,
-        source_order: usize,
         f: impl FnOnce(&mut Self, Range<usize>) -> R,
     ) -> Option<R> {
         // Record a snapshot of the assignments that we already knew held — both so that we can
@@ -3464,6 +3306,11 @@ impl<'db> PathAssignments<'db> {
             edge = %assignment.display(db),
             "walk edge",
         );
+        let source_order = self
+            .discovered
+            .get_index_of(&assignment.constraint())
+            .map(|index| index + 1)
+            .unwrap_or(0);
         let found_conflict = self.add_assignment(db, assignment, source_order);
         let result = if found_conflict.is_err() {
             // If that results in the path now being impossible due to a contradiction, return
@@ -3539,6 +3386,11 @@ impl<'db> PathAssignments<'db> {
         assignment: ConstraintAssignment<'db>,
         source_order: usize,
     ) -> Result<(), PathAssignmentConflict> {
+        let source_order = self
+            .discovered
+            .get_index_of(&assignment.constraint())
+            .map(|index| index + 1)
+            .unwrap_or(source_order);
         // First add this assignment. If it causes a conflict, return that as an error. If we've
         // already know this assignment holds, just return.
         if self.assignments.contains_key(&assignment.negated()) {
@@ -3863,7 +3715,7 @@ impl<'db> BoundTypeVarInstance<'db> {
     /// Returns the valid specializations of a typevar. This is used when checking a constraint set
     /// when this typevar is in inferable position, where we only need _some_ specialization to
     /// satisfy the constraint set.
-    fn valid_specializations(self, db: &'db dyn Db) -> Node<'db> {
+    fn valid_specializations(self, db: &'db dyn Db) -> ConstraintSet<'db> {
         // For gradual upper bounds and constraints, we are free to choose any materialization that
         // makes the check succeed. In inferable positions, it is most helpful to choose a
         // materialization that is as permissive as possible, since that maximizes the number of
@@ -3875,20 +3727,24 @@ impl<'db> BoundTypeVarInstance<'db> {
         // that _some_ valid specialization satisfies the constraint set, it's correct for us to
         // return the range of valid materializations that we can choose from.
         match self.typevar(db).bound_or_constraints(db) {
-            None => Node::AlwaysTrue,
+            None => ConstraintSet::from(true),
             Some(TypeVarBoundOrConstraints::UpperBound(bound)) => {
                 let bound = bound.top_materialization(db);
-                ConstrainedTypeVar::new_node(db, self, Type::Never, bound)
+                ConstraintSet::constrain_typevar(db, self, Type::Never, bound)
             }
             Some(TypeVarBoundOrConstraints::Constraints(constraints)) => {
-                let mut specializations = Node::AlwaysFalse;
+                let mut specializations = ConstraintSet::from(false);
                 for constraint in constraints.elements(db) {
                     let constraint_lower = constraint.bottom_materialization(db);
                     let constraint_upper = constraint.top_materialization(db);
-                    specializations = specializations.or_with_offset(
-                        db,
-                        ConstrainedTypeVar::new_node(db, self, constraint_lower, constraint_upper),
-                    );
+                    specializations = specializations.or(db, || {
+                        ConstraintSet::constrain_typevar(
+                            db,
+                            self,
+                            constraint_lower,
+                            constraint_upper,
+                        )
+                    });
                 }
                 specializations
             }
@@ -3908,32 +3764,38 @@ impl<'db> BoundTypeVarInstance<'db> {
     /// specifies the required specializations, and the iterator will be empty. For a constrained
     /// typevar, the primary result will include the fully static constraints, and the iterator
     /// will include an entry for each non-fully-static constraint.
-    fn required_specializations(self, db: &'db dyn Db) -> (Node<'db>, Vec<Node<'db>>) {
+    fn required_specializations(
+        self,
+        db: &'db dyn Db,
+    ) -> (ConstraintSet<'db>, Vec<ConstraintSet<'db>>) {
         // For upper bounds and constraints, we are free to choose any materialization that makes
         // the check succeed. In non-inferable positions, it is most helpful to choose a
         // materialization that is as restrictive as possible, since that minimizes the number of
         // valid specializations that must satisfy the check. We therefore take the bottom
         // materialization of the bound or constraints.
         match self.typevar(db).bound_or_constraints(db) {
-            None => (Node::AlwaysTrue, Vec::new()),
+            None => (ConstraintSet::from(true), Vec::new()),
             Some(TypeVarBoundOrConstraints::UpperBound(bound)) => {
                 let bound = bound.bottom_materialization(db);
                 (
-                    ConstrainedTypeVar::new_node(db, self, Type::Never, bound),
+                    ConstraintSet::constrain_typevar(db, self, Type::Never, bound),
                     Vec::new(),
                 )
             }
             Some(TypeVarBoundOrConstraints::Constraints(constraints)) => {
-                let mut non_gradual_constraints = Node::AlwaysFalse;
+                let mut non_gradual_constraints = ConstraintSet::from(false);
                 let mut gradual_constraints = Vec::new();
                 for constraint in constraints.elements(db) {
                     let constraint_lower = constraint.bottom_materialization(db);
                     let constraint_upper = constraint.top_materialization(db);
-                    let constraint =
-                        ConstrainedTypeVar::new_node(db, self, constraint_lower, constraint_upper);
+                    let constraint = ConstraintSet::constrain_typevar(
+                        db,
+                        self,
+                        constraint_lower,
+                        constraint_upper,
+                    );
                     if constraint_lower == constraint_upper {
-                        non_gradual_constraints =
-                            non_gradual_constraints.or_with_offset(db, constraint);
+                        non_gradual_constraints = non_gradual_constraints.or(db, || constraint);
                     } else {
                         gradual_constraints.push(constraint);
                     }
@@ -3973,110 +3835,114 @@ impl<'db> GenericContext<'db> {
         // each typevar.
         let abstracted = self
             .variables(db)
-            .fold(Node::AlwaysTrue, |constraints, bound_typevar| {
-                constraints.and_with_offset(db, bound_typevar.valid_specializations(db))
-            })
-            .and_with_offset(db, constraints.node);
+            .when_all(db, |bound_typevar| bound_typevar.valid_specializations(db))
+            .and(db, || constraints);
         tracing::trace!(
             target: "ty_python_semantic::types::constraints::specialize_constrained",
-            valid = %abstracted.display(db),
+            valid = %abstracted.node.display(db),
             "limited to valid specializations",
         );
 
         // Then we find all of the "representative types" for each typevar in the constraint set.
         let mut error_occurred = false;
         let mut representatives = Vec::new();
-        let types =
-            self.variables(db).map(|bound_typevar| {
-                // Each representative type represents one of the ways that the typevar can satisfy the
-                // constraint, expressed as a lower/upper bound on the types that the typevar can
-                // specialize to.
-                //
-                // If there are multiple paths in the BDD, they technically represent independent
-                // possible specializations. If there's a type that satisfies all of them, we will
-                // return that as the specialization. If not, then the constraint set is ambiguous.
-                // (This happens most often with constrained typevars.) We could in the future turn
-                // _each_ of the paths into separate specializations, but it's not clear what we would
-                // do with that, so instead we just report the ambiguity as a specialization failure.
-                let mut unconstrained = false;
-                let identity = bound_typevar.identity(db);
+        let types = self.variables(db).map(|bound_typevar| {
+            // Each representative type represents one of the ways that the typevar can satisfy the
+            // constraint, expressed as a lower/upper bound on the types that the typevar can
+            // specialize to.
+            //
+            // If there are multiple paths in the BDD, they technically represent independent
+            // possible specializations. If there's a type that satisfies all of them, we will
+            // return that as the specialization. If not, then the constraint set is ambiguous.
+            // (This happens most often with constrained typevars.) We could in the future turn
+            // _each_ of the paths into separate specializations, but it's not clear what we would
+            // do with that, so instead we just report the ambiguity as a specialization failure.
+            let mut unconstrained = false;
+            let identity = bound_typevar.identity(db);
+            tracing::trace!(
+                target: "ty_python_semantic::types::constraints::specialize_constrained",
+                bound_typevar = %identity.display(db),
+                abstracted = %abstracted.node.retain_one(
+                    db,
+                    identity,
+                    abstracted.support,
+                ).display(db),
+                "find specialization for typevar",
+            );
+            representatives.clear();
+            abstracted.node.find_representative_types(
+                db,
+                identity,
+                abstracted.support,
+                |representative| match representative {
+                    Some(representative) => {
+                        representatives.extend_from_slice(representative);
+                    }
+                    None => {
+                        unconstrained = true;
+                    }
+                },
+            );
+
+            // The BDD is satisfiable, but the typevar is unconstrained, then we use `None` to tell
+            // specialize_recursive to fall back on the typevar's default.
+            if unconstrained {
                 tracing::trace!(
                     target: "ty_python_semantic::types::constraints::specialize_constrained",
                     bound_typevar = %identity.display(db),
-                    abstracted = %abstracted.retain_one(db, identity).display(db),
-                    "find specialization for typevar",
+                    "typevar is unconstrained",
                 );
-                representatives.clear();
-                abstracted.find_representative_types(db, identity, |representative| {
-                    match representative {
-                        Some(representative) => {
-                            representatives.extend_from_slice(representative);
-                        }
-                        None => {
-                            unconstrained = true;
-                        }
-                    }
-                });
-
-                // The BDD is satisfiable, but the typevar is unconstrained, then we use `None` to tell
-                // specialize_recursive to fall back on the typevar's default.
-                if unconstrained {
-                    tracing::trace!(
-                        target: "ty_python_semantic::types::constraints::specialize_constrained",
-                        bound_typevar = %identity.display(db),
-                        "typevar is unconstrained",
-                    );
-                    return None;
-                }
-
-                // If there are no satisfiable paths in the BDD, then there is no valid specialization
-                // for this constraint set.
-                if representatives.is_empty() {
-                    // TODO: Construct a useful error here
-                    tracing::trace!(
-                        target: "ty_python_semantic::types::constraints::specialize_constrained",
-                        bound_typevar = %identity.display(db),
-                        "typevar cannot be satisfied",
-                    );
-                    error_occurred = true;
-                    return None;
-                }
+                return None;
+            }
 
-                // Before constructing the final lower and upper bound, sort the constraints by
-                // their source order. This should give us a consistently ordered specialization,
-                // regardless of the variable ordering of the original BDD.
-                representatives.sort_unstable_by_key(|bounds| bounds.source_order);
-                let greatest_lower_bound =
-                    UnionType::from_elements(db, representatives.iter().map(|bounds| bounds.lower));
-                let least_upper_bound = IntersectionType::from_elements(
-                    db,
-                    representatives.iter().map(|bounds| bounds.upper),
+            // If there are no satisfiable paths in the BDD, then there is no valid specialization
+            // for this constraint set.
+            if representatives.is_empty() {
+                // TODO: Construct a useful error here
+                tracing::trace!(
+                    target: "ty_python_semantic::types::constraints::specialize_constrained",
+                    bound_typevar = %identity.display(db),
+                    "typevar cannot be satisfied",
                 );
+                error_occurred = true;
+                return None;
+            }
 
-                // If `lower ≰ upper`, then there is no type that satisfies all of the paths in the
-                // BDD. That's an ambiguous specialization, as described above.
-                if !greatest_lower_bound.is_constraint_set_assignable_to(db, least_upper_bound) {
-                    tracing::trace!(
-                        target: "ty_python_semantic::types::constraints::specialize_constrained",
-                        bound_typevar = %identity.display(db),
-                        greatest_lower_bound = %greatest_lower_bound.display(db),
-                        least_upper_bound = %least_upper_bound.display(db),
-                        "typevar bounds are incompatible",
-                    );
-                    error_occurred = true;
-                    return None;
-                }
+            // Before constructing the final lower and upper bound, sort the constraints by
+            // their source order. This should give us a consistently ordered specialization,
+            // regardless of the variable ordering of the original BDD.
+            representatives.sort_unstable_by_key(|bounds| bounds.source_order);
+            let greatest_lower_bound =
+                UnionType::from_elements(db, representatives.iter().map(|bounds| bounds.lower));
+            let least_upper_bound = IntersectionType::from_elements(
+                db,
+                representatives.iter().map(|bounds| bounds.upper),
+            );
 
-                // Of all of the types that satisfy all of the paths in the BDD, we choose the
-                // "largest" one (i.e., "closest to `object`") as the specialization.
+            // If `lower ≰ upper`, then there is no type that satisfies all of the paths in the
+            // BDD. That's an ambiguous specialization, as described above.
+            if !greatest_lower_bound.is_constraint_set_assignable_to(db, least_upper_bound) {
                 tracing::trace!(
                     target: "ty_python_semantic::types::constraints::specialize_constrained",
                     bound_typevar = %identity.display(db),
-                    specialization = %least_upper_bound.display(db),
-                    "found specialization for typevar",
+                    greatest_lower_bound = %greatest_lower_bound.display(db),
+                    least_upper_bound = %least_upper_bound.display(db),
+                    "typevar bounds are incompatible",
                 );
-                Some(least_upper_bound)
-            });
+                error_occurred = true;
+                return None;
+            }
+
+            // Of all of the types that satisfy all of the paths in the BDD, we choose the
+            // "largest" one (i.e., "closest to `object`") as the specialization.
+            tracing::trace!(
+                target: "ty_python_semantic::types::constraints::specialize_constrained",
+                bound_typevar = %identity.display(db),
+                specialization = %least_upper_bound.display(db),
+                "found specialization for typevar",
+            );
+            Some(least_upper_bound)
+        });
 
         let specialization = self.specialize_recursive(db, types);
         if error_occurred {
@@ -4100,18 +3966,14 @@ mod tests {
     #[test]
     fn test_display_graph_output() {
         let expected = indoc! {r#"
-            <0> (U = bool) 2/4
-            ┡━₁ <1> (U = str) 1/4
-            │   ┡━₁ <2> (T = bool) 4/4
-            │   │   ┡━₁ <3> (T = str) 3/3
-            │   │   │   ┡━₁ always
-            │   │   │   └─₀ always
-            │   │   └─₀ <4> (T = str) 3/3
-            │   │       ┡━₁ always
-            │   │       └─₀ never
-            │   └─₀ <2> SHARED
-            └─₀ <5> (U = str) 1/4
-                ┡━₁ <2> SHARED
+            <0> (U = bool)
+            ┡━₁ <1> (T = bool)
+            │   ┡━₁ always
+            │   └─₀ <2> (T = str)
+            │       ┡━₁ always
+            │       └─₀ never
+            └─₀ <3> (U = str)
+                ┡━₁ <1> SHARED
                 └─₀ never
         "#}
         .trim_end();
@@ -4127,8 +3989,7 @@ mod tests {
         let t_bool = ConstraintSet::range(&db, bool_type, t, bool_type);
         let u_str = ConstraintSet::range(&db, str_type, u, str_type);
         let u_bool = ConstraintSet::range(&db, bool_type, u, bool_type);
-        // Construct this in a different order than above to make the source_orders more
-        // interesting.
+        // Construct this in a different order than above to make the ordering more interesting.
         let constraints = (u_str.or(&db, || u_bool)).and(&db, || t_str.or(&db, || t_bool));
         let actual = constraints.node.display_graph(&db, &"").to_string();
         assert_eq!(actual, expected);
diff --git a/scripts/uv.lock b/scripts/uv.lock
new file mode 100644
index 0000000000000..a66b3968f5abc
--- /dev/null
+++ b/scripts/uv.lock
@@ -0,0 +1,131 @@
+version = 1
+revision = 3
+requires-python = ">=3.12"
+
+[[package]]
+name = "colorama"
+version = "0.4.6"
+source = { registry = "https://pypi.org/simple" }
+sdist = { url = "https://files.pythonhosted.org/packages/d8/53/6f443c9a4a8358a93a6792e2acffb9d9d5cb0a5cfd8802644b7b1c9a02e4/colorama-0.4.6.tar.gz", hash = "sha256:08695f5cb7ed6e0531a20572697297273c47b8cae5a63ffc6d6ed5c201be6e44", size = 27697, upload-time = "2022-10-25T02:36:22.414Z" }
+wheels = [
+    { url = "https://files.pythonhosted.org/packages/d1/d6/3965ed04c63042e047cb6a3e6ed1a63a35087b6a609aa3a15ed8ac56c221/colorama-0.4.6-py2.py3-none-any.whl", hash = "sha256:4f1d9991f5acc0ca119f9d443620b77f9d6b33703e51011c16baf57afb285fc6", size = 25335, upload-time = "2022-10-25T02:36:20.889Z" },
+]
+
+[[package]]
+name = "markdown-it-py"
+version = "4.0.0"
+source = { registry = "https://pypi.org/simple" }
+dependencies = [
+    { name = "mdurl" },
+]
+sdist = { url = "https://files.pythonhosted.org/packages/5b/f5/4ec618ed16cc4f8fb3b701563655a69816155e79e24a17b651541804721d/markdown_it_py-4.0.0.tar.gz", hash = "sha256:cb0a2b4aa34f932c007117b194e945bd74e0ec24133ceb5bac59009cda1cb9f3", size = 73070, upload-time = "2025-08-11T12:57:52.854Z" }
+wheels = [
+    { url = "https://files.pythonhosted.org/packages/94/54/e7d793b573f298e1c9013b8c4dade17d481164aa517d1d7148619c2cedbf/markdown_it_py-4.0.0-py3-none-any.whl", hash = "sha256:87327c59b172c5011896038353a81343b6754500a08cd7a4973bb48c6d578147", size = 87321, upload-time = "2025-08-11T12:57:51.923Z" },
+]
+
+[[package]]
+name = "mdformat"
+version = "1.0.0"
+source = { registry = "https://pypi.org/simple" }
+dependencies = [
+    { name = "markdown-it-py" },
+]
+sdist = { url = "https://files.pythonhosted.org/packages/3f/05/32b5e14b192b0a8a309f32232c580aefedd9d06017cb8fe8fce34bec654c/mdformat-1.0.0.tar.gz", hash = "sha256:4954045fcae797c29f86d4ad879e43bb151fa55dbaf74ac6eaeacf1d45bb3928", size = 56953, upload-time = "2025-10-16T12:05:03.695Z" }
+wheels = [
+    { url = "https://files.pythonhosted.org/packages/54/9a/8fe71b95985ca7a4001effbcc58e5a07a1f2a2884203f74dcf48a3b08315/mdformat-1.0.0-py3-none-any.whl", hash = "sha256:bca015d65a1d063a02e885a91daee303057bc7829c2cd37b2075a50dbb65944b", size = 53288, upload-time = "2025-10-16T12:05:02.607Z" },
+]
+
+[[package]]
+name = "mdurl"
+version = "0.1.2"
+source = { registry = "https://pypi.org/simple" }
+sdist = { url = "https://files.pythonhosted.org/packages/d6/54/cfe61301667036ec958cb99bd3efefba235e65cdeb9c84d24a8293ba1d90/mdurl-0.1.2.tar.gz", hash = "sha256:bb413d29f5eea38f31dd4754dd7377d4465116fb207585f97bf925588687c1ba", size = 8729, upload-time = "2022-08-14T12:40:10.846Z" }
+wheels = [
+    { url = "https://files.pythonhosted.org/packages/b3/38/89ba8ad64ae25be8de66a6d463314cf1eb366222074cfda9ee839c56a4b4/mdurl-0.1.2-py3-none-any.whl", hash = "sha256:84008a41e51615a49fc9966191ff91509e3c40b939176e643fd50a5c2196b8f8", size = 9979, upload-time = "2022-08-14T12:40:09.779Z" },
+]
+
+[[package]]
+name = "pyyaml"
+version = "6.0.3"
+source = { registry = "https://pypi.org/simple" }
+sdist = { url = "https://files.pythonhosted.org/packages/05/8e/961c0007c59b8dd7729d542c61a4d537767a59645b82a0b521206e1e25c2/pyyaml-6.0.3.tar.gz", hash = "sha256:d76623373421df22fb4cf8817020cbb7ef15c725b9d5e45f17e189bfc384190f", size = 130960, upload-time = "2025-09-25T21:33:16.546Z" }
+wheels = [
+    { url = "https://files.pythonhosted.org/packages/d1/33/422b98d2195232ca1826284a76852ad5a86fe23e31b009c9886b2d0fb8b2/pyyaml-6.0.3-cp312-cp312-macosx_10_13_x86_64.whl", hash = "sha256:7f047e29dcae44602496db43be01ad42fc6f1cc0d8cd6c83d342306c32270196", size = 182063, upload-time = "2025-09-25T21:32:11.445Z" },
+    { url = "https://files.pythonhosted.org/packages/89/a0/6cf41a19a1f2f3feab0e9c0b74134aa2ce6849093d5517a0c550fe37a648/pyyaml-6.0.3-cp312-cp312-macosx_11_0_arm64.whl", hash = "sha256:fc09d0aa354569bc501d4e787133afc08552722d3ab34836a80547331bb5d4a0", size = 173973, upload-time = "2025-09-25T21:32:12.492Z" },
+    { url = "https://files.pythonhosted.org/packages/ed/23/7a778b6bd0b9a8039df8b1b1d80e2e2ad78aa04171592c8a5c43a56a6af4/pyyaml-6.0.3-cp312-cp312-manylinux2014_aarch64.manylinux_2_17_aarch64.manylinux_2_28_aarch64.whl", hash = "sha256:9149cad251584d5fb4981be1ecde53a1ca46c891a79788c0df828d2f166bda28", size = 775116, upload-time = "2025-09-25T21:32:13.652Z" },
+    { url = "https://files.pythonhosted.org/packages/65/30/d7353c338e12baef4ecc1b09e877c1970bd3382789c159b4f89d6a70dc09/pyyaml-6.0.3-cp312-cp312-manylinux2014_s390x.manylinux_2_17_s390x.manylinux_2_28_s390x.whl", hash = "sha256:5fdec68f91a0c6739b380c83b951e2c72ac0197ace422360e6d5a959d8d97b2c", size = 844011, upload-time = "2025-09-25T21:32:15.21Z" },
+    { url = "https://files.pythonhosted.org/packages/8b/9d/b3589d3877982d4f2329302ef98a8026e7f4443c765c46cfecc8858c6b4b/pyyaml-6.0.3-cp312-cp312-manylinux2014_x86_64.manylinux_2_17_x86_64.manylinux_2_28_x86_64.whl", hash = "sha256:ba1cc08a7ccde2d2ec775841541641e4548226580ab850948cbfda66a1befcdc", size = 807870, upload-time = "2025-09-25T21:32:16.431Z" },
+    { url = "https://files.pythonhosted.org/packages/05/c0/b3be26a015601b822b97d9149ff8cb5ead58c66f981e04fedf4e762f4bd4/pyyaml-6.0.3-cp312-cp312-musllinux_1_2_aarch64.whl", hash = "sha256:8dc52c23056b9ddd46818a57b78404882310fb473d63f17b07d5c40421e47f8e", size = 761089, upload-time = "2025-09-25T21:32:17.56Z" },
+    { url = "https://files.pythonhosted.org/packages/be/8e/98435a21d1d4b46590d5459a22d88128103f8da4c2d4cb8f14f2a96504e1/pyyaml-6.0.3-cp312-cp312-musllinux_1_2_x86_64.whl", hash = "sha256:41715c910c881bc081f1e8872880d3c650acf13dfa8214bad49ed4cede7c34ea", size = 790181, upload-time = "2025-09-25T21:32:18.834Z" },
+    { url = "https://files.pythonhosted.org/packages/74/93/7baea19427dcfbe1e5a372d81473250b379f04b1bd3c4c5ff825e2327202/pyyaml-6.0.3-cp312-cp312-win32.whl", hash = "sha256:96b533f0e99f6579b3d4d4995707cf36df9100d67e0c8303a0c55b27b5f99bc5", size = 137658, upload-time = "2025-09-25T21:32:20.209Z" },
+    { url = "https://files.pythonhosted.org/packages/86/bf/899e81e4cce32febab4fb42bb97dcdf66bc135272882d1987881a4b519e9/pyyaml-6.0.3-cp312-cp312-win_amd64.whl", hash = "sha256:5fcd34e47f6e0b794d17de1b4ff496c00986e1c83f7ab2fb8fcfe9616ff7477b", size = 154003, upload-time = "2025-09-25T21:32:21.167Z" },
+    { url = "https://files.pythonhosted.org/packages/1a/08/67bd04656199bbb51dbed1439b7f27601dfb576fb864099c7ef0c3e55531/pyyaml-6.0.3-cp312-cp312-win_arm64.whl", hash = "sha256:64386e5e707d03a7e172c0701abfb7e10f0fb753ee1d773128192742712a98fd", size = 140344, upload-time = "2025-09-25T21:32:22.617Z" },
+    { url = "https://files.pythonhosted.org/packages/d1/11/0fd08f8192109f7169db964b5707a2f1e8b745d4e239b784a5a1dd80d1db/pyyaml-6.0.3-cp313-cp313-macosx_10_13_x86_64.whl", hash = "sha256:8da9669d359f02c0b91ccc01cac4a67f16afec0dac22c2ad09f46bee0697eba8", size = 181669, upload-time = "2025-09-25T21:32:23.673Z" },
+    { url = "https://files.pythonhosted.org/packages/b1/16/95309993f1d3748cd644e02e38b75d50cbc0d9561d21f390a76242ce073f/pyyaml-6.0.3-cp313-cp313-macosx_11_0_arm64.whl", hash = "sha256:2283a07e2c21a2aa78d9c4442724ec1eb15f5e42a723b99cb3d822d48f5f7ad1", size = 173252, upload-time = "2025-09-25T21:32:25.149Z" },
+    { url = "https://files.pythonhosted.org/packages/50/31/b20f376d3f810b9b2371e72ef5adb33879b25edb7a6d072cb7ca0c486398/pyyaml-6.0.3-cp313-cp313-manylinux2014_aarch64.manylinux_2_17_aarch64.manylinux_2_28_aarch64.whl", hash = "sha256:ee2922902c45ae8ccada2c5b501ab86c36525b883eff4255313a253a3160861c", size = 767081, upload-time = "2025-09-25T21:32:26.575Z" },
+    { url = "https://files.pythonhosted.org/packages/49/1e/a55ca81e949270d5d4432fbbd19dfea5321eda7c41a849d443dc92fd1ff7/pyyaml-6.0.3-cp313-cp313-manylinux2014_s390x.manylinux_2_17_s390x.manylinux_2_28_s390x.whl", hash = "sha256:a33284e20b78bd4a18c8c2282d549d10bc8408a2a7ff57653c0cf0b9be0afce5", size = 841159, upload-time = "2025-09-25T21:32:27.727Z" },
+    { url = "https://files.pythonhosted.org/packages/74/27/e5b8f34d02d9995b80abcef563ea1f8b56d20134d8f4e5e81733b1feceb2/pyyaml-6.0.3-cp313-cp313-manylinux2014_x86_64.manylinux_2_17_x86_64.manylinux_2_28_x86_64.whl", hash = "sha256:0f29edc409a6392443abf94b9cf89ce99889a1dd5376d94316ae5145dfedd5d6", size = 801626, upload-time = "2025-09-25T21:32:28.878Z" },
+    { url = "https://files.pythonhosted.org/packages/f9/11/ba845c23988798f40e52ba45f34849aa8a1f2d4af4b798588010792ebad6/pyyaml-6.0.3-cp313-cp313-musllinux_1_2_aarch64.whl", hash = "sha256:f7057c9a337546edc7973c0d3ba84ddcdf0daa14533c2065749c9075001090e6", size = 753613, upload-time = "2025-09-25T21:32:30.178Z" },
+    { url = "https://files.pythonhosted.org/packages/3d/e0/7966e1a7bfc0a45bf0a7fb6b98ea03fc9b8d84fa7f2229e9659680b69ee3/pyyaml-6.0.3-cp313-cp313-musllinux_1_2_x86_64.whl", hash = "sha256:eda16858a3cab07b80edaf74336ece1f986ba330fdb8ee0d6c0d68fe82bc96be", size = 794115, upload-time = "2025-09-25T21:32:31.353Z" },
+    { url = "https://files.pythonhosted.org/packages/de/94/980b50a6531b3019e45ddeada0626d45fa85cbe22300844a7983285bed3b/pyyaml-6.0.3-cp313-cp313-win32.whl", hash = "sha256:d0eae10f8159e8fdad514efdc92d74fd8d682c933a6dd088030f3834bc8e6b26", size = 137427, upload-time = "2025-09-25T21:32:32.58Z" },
+    { url = "https://files.pythonhosted.org/packages/97/c9/39d5b874e8b28845e4ec2202b5da735d0199dbe5b8fb85f91398814a9a46/pyyaml-6.0.3-cp313-cp313-win_amd64.whl", hash = "sha256:79005a0d97d5ddabfeeea4cf676af11e647e41d81c9a7722a193022accdb6b7c", size = 154090, upload-time = "2025-09-25T21:32:33.659Z" },
+    { url = "https://files.pythonhosted.org/packages/73/e8/2bdf3ca2090f68bb3d75b44da7bbc71843b19c9f2b9cb9b0f4ab7a5a4329/pyyaml-6.0.3-cp313-cp313-win_arm64.whl", hash = "sha256:5498cd1645aa724a7c71c8f378eb29ebe23da2fc0d7a08071d89469bf1d2defb", size = 140246, upload-time = "2025-09-25T21:32:34.663Z" },
+    { url = "https://files.pythonhosted.org/packages/9d/8c/f4bd7f6465179953d3ac9bc44ac1a8a3e6122cf8ada906b4f96c60172d43/pyyaml-6.0.3-cp314-cp314-macosx_10_13_x86_64.whl", hash = "sha256:8d1fab6bb153a416f9aeb4b8763bc0f22a5586065f86f7664fc23339fc1c1fac", size = 181814, upload-time = "2025-09-25T21:32:35.712Z" },
+    { url = "https://files.pythonhosted.org/packages/bd/9c/4d95bb87eb2063d20db7b60faa3840c1b18025517ae857371c4dd55a6b3a/pyyaml-6.0.3-cp314-cp314-macosx_11_0_arm64.whl", hash = "sha256:34d5fcd24b8445fadc33f9cf348c1047101756fd760b4dacb5c3e99755703310", size = 173809, upload-time = "2025-09-25T21:32:36.789Z" },
+    { url = "https://files.pythonhosted.org/packages/92/b5/47e807c2623074914e29dabd16cbbdd4bf5e9b2db9f8090fa64411fc5382/pyyaml-6.0.3-cp314-cp314-manylinux2014_aarch64.manylinux_2_17_aarch64.manylinux_2_28_aarch64.whl", hash = "sha256:501a031947e3a9025ed4405a168e6ef5ae3126c59f90ce0cd6f2bfc477be31b7", size = 766454, upload-time = "2025-09-25T21:32:37.966Z" },
+    { url = "https://files.pythonhosted.org/packages/02/9e/e5e9b168be58564121efb3de6859c452fccde0ab093d8438905899a3a483/pyyaml-6.0.3-cp314-cp314-manylinux2014_s390x.manylinux_2_17_s390x.manylinux_2_28_s390x.whl", hash = "sha256:b3bc83488de33889877a0f2543ade9f70c67d66d9ebb4ac959502e12de895788", size = 836355, upload-time = "2025-09-25T21:32:39.178Z" },
+    { url = "https://files.pythonhosted.org/packages/88/f9/16491d7ed2a919954993e48aa941b200f38040928474c9e85ea9e64222c3/pyyaml-6.0.3-cp314-cp314-manylinux2014_x86_64.manylinux_2_17_x86_64.manylinux_2_28_x86_64.whl", hash = "sha256:c458b6d084f9b935061bc36216e8a69a7e293a2f1e68bf956dcd9e6cbcd143f5", size = 794175, upload-time = "2025-09-25T21:32:40.865Z" },
+    { url = "https://files.pythonhosted.org/packages/dd/3f/5989debef34dc6397317802b527dbbafb2b4760878a53d4166579111411e/pyyaml-6.0.3-cp314-cp314-musllinux_1_2_aarch64.whl", hash = "sha256:7c6610def4f163542a622a73fb39f534f8c101d690126992300bf3207eab9764", size = 755228, upload-time = "2025-09-25T21:32:42.084Z" },
+    { url = "https://files.pythonhosted.org/packages/d7/ce/af88a49043cd2e265be63d083fc75b27b6ed062f5f9fd6cdc223ad62f03e/pyyaml-6.0.3-cp314-cp314-musllinux_1_2_x86_64.whl", hash = "sha256:5190d403f121660ce8d1d2c1bb2ef1bd05b5f68533fc5c2ea899bd15f4399b35", size = 789194, upload-time = "2025-09-25T21:32:43.362Z" },
+    { url = "https://files.pythonhosted.org/packages/23/20/bb6982b26a40bb43951265ba29d4c246ef0ff59c9fdcdf0ed04e0687de4d/pyyaml-6.0.3-cp314-cp314-win_amd64.whl", hash = "sha256:4a2e8cebe2ff6ab7d1050ecd59c25d4c8bd7e6f400f5f82b96557ac0abafd0ac", size = 156429, upload-time = "2025-09-25T21:32:57.844Z" },
+    { url = "https://files.pythonhosted.org/packages/f4/f4/a4541072bb9422c8a883ab55255f918fa378ecf083f5b85e87fc2b4eda1b/pyyaml-6.0.3-cp314-cp314-win_arm64.whl", hash = "sha256:93dda82c9c22deb0a405ea4dc5f2d0cda384168e466364dec6255b293923b2f3", size = 143912, upload-time = "2025-09-25T21:32:59.247Z" },
+    { url = "https://files.pythonhosted.org/packages/7c/f9/07dd09ae774e4616edf6cda684ee78f97777bdd15847253637a6f052a62f/pyyaml-6.0.3-cp314-cp314t-macosx_10_13_x86_64.whl", hash = "sha256:02893d100e99e03eda1c8fd5c441d8c60103fd175728e23e431db1b589cf5ab3", size = 189108, upload-time = "2025-09-25T21:32:44.377Z" },
+    { url = "https://files.pythonhosted.org/packages/4e/78/8d08c9fb7ce09ad8c38ad533c1191cf27f7ae1effe5bb9400a46d9437fcf/pyyaml-6.0.3-cp314-cp314t-macosx_11_0_arm64.whl", hash = "sha256:c1ff362665ae507275af2853520967820d9124984e0f7466736aea23d8611fba", size = 183641, upload-time = "2025-09-25T21:32:45.407Z" },
+    { url = "https://files.pythonhosted.org/packages/7b/5b/3babb19104a46945cf816d047db2788bcaf8c94527a805610b0289a01c6b/pyyaml-6.0.3-cp314-cp314t-manylinux2014_aarch64.manylinux_2_17_aarch64.manylinux_2_28_aarch64.whl", hash = "sha256:6adc77889b628398debc7b65c073bcb99c4a0237b248cacaf3fe8a557563ef6c", size = 831901, upload-time = "2025-09-25T21:32:48.83Z" },
+    { url = "https://files.pythonhosted.org/packages/8b/cc/dff0684d8dc44da4d22a13f35f073d558c268780ce3c6ba1b87055bb0b87/pyyaml-6.0.3-cp314-cp314t-manylinux2014_s390x.manylinux_2_17_s390x.manylinux_2_28_s390x.whl", hash = "sha256:a80cb027f6b349846a3bf6d73b5e95e782175e52f22108cfa17876aaeff93702", size = 861132, upload-time = "2025-09-25T21:32:50.149Z" },
+    { url = "https://files.pythonhosted.org/packages/b1/5e/f77dc6b9036943e285ba76b49e118d9ea929885becb0a29ba8a7c75e29fe/pyyaml-6.0.3-cp314-cp314t-manylinux2014_x86_64.manylinux_2_17_x86_64.manylinux_2_28_x86_64.whl", hash = "sha256:00c4bdeba853cc34e7dd471f16b4114f4162dc03e6b7afcc2128711f0eca823c", size = 839261, upload-time = "2025-09-25T21:32:51.808Z" },
+    { url = "https://files.pythonhosted.org/packages/ce/88/a9db1376aa2a228197c58b37302f284b5617f56a5d959fd1763fb1675ce6/pyyaml-6.0.3-cp314-cp314t-musllinux_1_2_aarch64.whl", hash = "sha256:66e1674c3ef6f541c35191caae2d429b967b99e02040f5ba928632d9a7f0f065", size = 805272, upload-time = "2025-09-25T21:32:52.941Z" },
+    { url = "https://files.pythonhosted.org/packages/da/92/1446574745d74df0c92e6aa4a7b0b3130706a4142b2d1a5869f2eaa423c6/pyyaml-6.0.3-cp314-cp314t-musllinux_1_2_x86_64.whl", hash = "sha256:16249ee61e95f858e83976573de0f5b2893b3677ba71c9dd36b9cf8be9ac6d65", size = 829923, upload-time = "2025-09-25T21:32:54.537Z" },
+    { url = "https://files.pythonhosted.org/packages/f0/7a/1c7270340330e575b92f397352af856a8c06f230aa3e76f86b39d01b416a/pyyaml-6.0.3-cp314-cp314t-win_amd64.whl", hash = "sha256:4ad1906908f2f5ae4e5a8ddfce73c320c2a1429ec52eafd27138b7f1cbe341c9", size = 174062, upload-time = "2025-09-25T21:32:55.767Z" },
+    { url = "https://files.pythonhosted.org/packages/f1/12/de94a39c2ef588c7e6455cfbe7343d3b2dc9d6b6b2f40c4c6565744c873d/pyyaml-6.0.3-cp314-cp314t-win_arm64.whl", hash = "sha256:ebc55a14a21cb14062aa4162f906cd962b28e2e9ea38f9b4391244cd8de4ae0b", size = 149341, upload-time = "2025-09-25T21:32:56.828Z" },
+]
+
+[[package]]
+name = "scripts"
+version = "0.0.1"
+source = { virtual = "." }
+dependencies = [
+    { name = "mdformat" },
+    { name = "pyyaml" },
+    { name = "stdlibs" },
+    { name = "tqdm" },
+]
+
+[package.metadata]
+requires-dist = [
+    { name = "mdformat" },
+    { name = "pyyaml" },
+    { name = "stdlibs" },
+    { name = "tqdm" },
+]
+
+[[package]]
+name = "stdlibs"
+version = "2025.10.28"
+source = { registry = "https://pypi.org/simple" }
+sdist = { url = "https://files.pythonhosted.org/packages/e4/83/ac15c4a3c059725dcb5f5d76270b986808cc12d2d7d417ee540d37609e46/stdlibs-2025.10.28.tar.gz", hash = "sha256:18db81f45f7783ddf86b80771e061782c70e2f4a8642843b3c80b42cd774b24f", size = 20108, upload-time = "2025-10-28T22:14:42.308Z" }
+wheels = [
+    { url = "https://files.pythonhosted.org/packages/65/de/5fcc806280950b9535d3892c7f1f3477efc4c2f8624ae6c0b2c3baf9a339/stdlibs-2025.10.28-py3-none-any.whl", hash = "sha256:fc25a3608c417c7fecec06736a2671adaceafc9f20c3f536d967e894a998afea", size = 59232, upload-time = "2025-10-28T22:14:40.799Z" },
+]
+
+[[package]]
+name = "tqdm"
+version = "4.67.1"
+source = { registry = "https://pypi.org/simple" }
+dependencies = [
+    { name = "colorama", marker = "sys_platform == 'win32'" },
+]
+sdist = { url = "https://files.pythonhosted.org/packages/a8/4b/29b4ef32e036bb34e4ab51796dd745cdba7ed47ad142a9f4a1eb8e0c744d/tqdm-4.67.1.tar.gz", hash = "sha256:f8aef9c52c08c13a65f30ea34f4e5aac3fd1a34959879d7e59e63027286627f2", size = 169737, upload-time = "2024-11-24T20:12:22.481Z" }
+wheels = [
+    { url = "https://files.pythonhosted.org/packages/d0/30/dc54f88dd4a2b5dc8a0279bdd7270e735851848b762aeb1c1184ed1f6b14/tqdm-4.67.1-py3-none-any.whl", hash = "sha256:26445eca388f82e72884e0d580d5464cd801a3ea01e63e5601bdff9ba6a48de2", size = 78540, upload-time = "2024-11-24T20:12:19.698Z" },
+]