Repository: astral-sh/ruff
File: crates/ty_python_semantic/src/types/constraints.rs (Rust)

Code before:
        }
    }
}

/// A collection of _sequents_ that describe how the constraints mentioned in a BDD relate to each
/// other. These are used in several BDD operations that need to know about "derived facts" even if
/// they are not mentioned in the BDD directly. These operations involve walking one or more paths
/// from the root node to a terminal node. Each sequent describes paths that are invalid (which are
/// pruned from the search), and new constraints that we can assume to be true even if we haven't
/// seen them directly.
///
/// We support several kinds of sequent:
///
/// - `¬C₁ → false`: This indicates that `C₁` is always true. Any path that assumes it is false is
///   impossible and can be pruned.
///
/// - `C₁ ∧ C₂ → false`: This indicates that `C₁` and `C₂` are disjoint: it is not possible for
///   both to hold. Any path that assumes both is impossible and can be pruned.
///
/// - `C₁ ∧ C₂ → D`: This indicates that the intersection of `C₁` and `C₂` can be simplified to
///   `D`. Any path that assumes both `C₁` and `C₂` hold, but assumes `D` does _not_, is impossible
///   and can be pruned.
///
/// - `C → D`: This indicates that `C` on its own is enough to imply `D`. Any path that assumes `C`
///   holds but `D` does _not_ is impossible and can be pruned.
#[derive(Debug, Default, Eq, PartialEq, get_size2::GetSize, salsa::Update)]
struct SequentMap<'db> {
    /// Sequents of the form `¬C₁ → false`
    single_tautologies: FxHashSet<ConstrainedTypeVar<'db>>,
    /// Sequents of the form `C₁ ∧ C₂ → false`
    pair_impossibilities: FxHashSet<(ConstrainedTypeVar<'db>, ConstrainedTypeVar<'db>)>,
    /// Sequents of the form `C₁ ∧ C₂ → D`
    pair_implications: FxHashMap<
        (ConstrainedTypeVar<'db>, ConstrainedTypeVar<'db>),
        FxHashSet<ConstrainedTypeVar<'db>>,
    >,
    /// Sequents of the form `C → D`
    single_implications: FxHashMap<ConstrainedTypeVar<'db>, FxHashSet<ConstrainedTypeVar<'db>>>,
    /// Constraints that we have already processed
    processed: FxHashSet<ConstrainedTypeVar<'db>>,
    /// Constraints that enqueued to be processed
    enqueued: Vec<ConstrainedTypeVar<'db>>,
}

impl<'db> SequentMap<'db> {
    fn add(&mut self, db: &'db dyn Db, constraint: ConstrainedTypeVar<'db>) {
        self.enqueue_constraint(constraint);

        while let Some(constraint) = self.enqueued.pop() {
            // If we've already processed this constraint, we can skip it.
            if !self.processed.insert(constraint) {

Review comment (suggestion):
Mostly just curiosity: is there an important reason why we frame this as `¬C₁ → false` rather than `C₁ → true`? Are these different in some way? The prose here suggests not.

Code after:
                        constraint.display(self.db).fmt(f)
                    }
                    ConstraintAssignment::Negative(constraint) => {
                        constraint.display_negated(self.db).fmt(f)
                    }
                }
            }
        }

        DisplayConstraintAssignment {
            constraint: self,
            db,
        }
    }
}

/// A collection of _sequents_ that describe how the constraints mentioned in a BDD relate to each
/// other. These are used in several BDD operations that need to know about "derived facts" even if
/// they are not mentioned in the BDD directly. These operations involve walking one or more paths
/// from the root node to a terminal node. Each sequent describes paths that are invalid (which are
/// pruned from the search), and new constraints that we can assume to be true even if we haven't
/// seen them directly.
///
/// We support several kinds of sequent:
///
/// - `¬C₁ → false`: This indicates that `C₁` is always true. Any path that assumes it is false is
///   impossible and can be pruned.
///
/// - `C₁ ∧ C₂ → false`: This indicates that `C₁` and `C₂` are disjoint: it is not possible for
///   both to hold. Any path that assumes both is impossible and can be pruned.
///
/// - `C₁ ∧ C₂ → D`: This indicates that the intersection of `C₁` and `C₂` can be simplified to
///   `D`. Any path that assumes both `C₁` and `C₂` hold, but assumes `D` does _not_, is impossible
///   and can be pruned.
///
/// - `C → D`: This indicates that `C` on its own is enough to imply `D`. Any path that assumes `C`
///   holds but `D` does _not_ is impossible and can be pruned.
#[derive(Debug, Default, Eq, PartialEq, get_size2::GetSize, salsa::Update)]
struct SequentMap<'db> {
    /// Sequents of the form `¬C₁ → false`
    single_tautologies: FxHashSet<ConstrainedTypeVar<'db>>,
    /// Sequents of the form `C₁ ∧ C₂ → false`
    pair_impossibilities: FxHashSet<(ConstrainedTypeVar<'db>, ConstrainedTypeVar<'db>)>,
    /// Sequents of the form `C₁ ∧ C₂ → D`
    pair_implications: FxHashMap<
        (ConstrainedTypeVar<'db>, ConstrainedTypeVar<'db>),
        FxHashSet<ConstrainedTypeVar<'db>>,
    >,
    /// Sequents of the form `C → D`
    single_implications: FxHashMap<ConstrainedTypeVar<'db>, FxHashSet<ConstrainedTypeVar<'db>>>,
    /// Constraints that we have already processed