Skip to content
Merged
Changes from 1 commit
Commits
Show all changes
30 commits
Select commit Hold shift + click to select a range
2816884
add test case
dcreager Oct 21, 2025
e111e4e
add BDD graph display
dcreager Oct 17, 2025
0e26c7c
simplify individual clauses for display
dcreager Oct 17, 2025
db63d2a
don't simplify until time to display
dcreager Oct 17, 2025
c334ba6
simplify individual clauses last
dcreager Oct 17, 2025
dc76a71
normalize bounds
dcreager Oct 15, 2025
2a85ed6
order typevars near each other
dcreager Oct 16, 2025
ddb4ca4
clean up implies
dcreager Oct 21, 2025
8be58fc
clippy
dcreager Oct 21, 2025
86047f5
fix implies
dcreager Oct 21, 2025
671582a
remove implications first I guess?
dcreager Oct 21, 2025
be43f6c
dead_code not unused
dcreager Oct 21, 2025
a392d59
add normalization test
dcreager Oct 21, 2025
90460a8
mdformat
dcreager Oct 21, 2025
550c485
Apply suggestion from @AlexWaygood
dcreager Oct 21, 2025
f7ce95c
doc implies
dcreager Oct 21, 2025
dd674c6
def _ -> f
dcreager Oct 21, 2025
4920258
ordering comment
dcreager Oct 21, 2025
9fbec28
document display_graph
dcreager Oct 21, 2025
362a1a2
doc implies 2
dcreager Oct 21, 2025
ae00c34
move bdd ordering into a struct
dcreager Oct 21, 2025
ad54fc3
clippy!!1!!!1
dcreager Oct 21, 2025
c3520f5
typo
dcreager Oct 21, 2025
21f75eb
simplify constraint ordering
dcreager Oct 21, 2025
33816d6
render → display
dcreager Oct 21, 2025
5c1e038
Update crates/ty_python_semantic/src/types/constraints.rs
dcreager Oct 22, 2025
c5ff1fa
Update crates/ty_python_semantic/src/types/constraints.rs
dcreager Oct 22, 2025
9391e42
ordering method
dcreager Oct 22, 2025
86072f4
add snapshot test for graph output
dcreager Oct 22, 2025
2e4332e
clippy
dcreager Oct 22, 2025
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
89 changes: 33 additions & 56 deletions crates/ty_python_semantic/src/types/constraints.rs
Original file line number Diff line number Diff line change
Expand Up @@ -316,6 +316,22 @@ impl<'db> ConstrainedTypeVar<'db> {
&& other.upper(db).is_subtype_of(db, self.upper(db))
}

/// Defines the ordering of the variables in a constraint set BDD.
///
/// If we only care about _correctness_, we can choose any ordering that we want, as long as
/// it's consistent. However, different orderings can have very different _performance_
/// characteristics. Many BDD libraries attempt to reorder variables on the fly while building
/// and working with BDDs. We don't do that, but we have tried to make some simple choices that
/// have clear wins.
///
/// In particular, we compare the _typevars_ of each constraint first, so that all constraints
/// for a single typevar are guaranteed to be adjacent in the BDD structure. There are several
/// simplifications that we perform that operate on constraints with the same typevar, and this
/// ensures that we can find all candidate simplifications more easily.
fn ordering(self, db: &'db dyn Db) -> impl Ord {
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Clever :)

(self.typevar(db), self.as_id())
}

/// Returns whether this constraint implies another — i.e., whether every type that
/// satisfies this constraint also satisfies `other`.
///
Expand Down Expand Up @@ -393,42 +409,6 @@ impl<'db> ConstrainedTypeVar<'db> {
}
}

/// Defines the ordering of the variables in a constraint set BDD.
///
/// If we only care about _correctness_, we can choose any ordering that we want, as long as it's
/// consistent. However, different orderings can have very different _performance_ characteristics.
/// Many BDD libraries attempt to reorder variables on the fly while building and working with
/// BDDs. We don't do that, but we have tried to make some simple choices that have clear wins.
///
/// In particular, we compare the _typevars_ of each constraint first, so that all constraints for
/// a single typevar are guaranteed to be adjacent in the BDD structure. There are several
/// simplifications that we perform that operate on constraints with the same typevar, and this
/// ensures that we can find all candidate simplifications more easily.
#[derive(Clone, Copy)]
struct ConstraintOrdering<'db>(&'db dyn Db, ConstrainedTypeVar<'db>);

impl<'db> PartialEq<ConstrainedTypeVar<'db>> for ConstraintOrdering<'db> {
fn eq(&self, other_constraint: &ConstrainedTypeVar<'db>) -> bool {
let ConstraintOrdering(_, self_constraint) = *self;
self_constraint == *other_constraint
}
}

impl<'db> PartialOrd<ConstrainedTypeVar<'db>> for ConstraintOrdering<'db> {
fn partial_cmp(&self, other_constraint: &ConstrainedTypeVar<'db>) -> Option<Ordering> {
let ConstraintOrdering(db, self_constraint) = *self;
if self_constraint == *other_constraint {
return Some(Ordering::Equal);
}
Some(
self_constraint
.typevar(db)
.cmp(&other_constraint.typevar(db))
.then_with(|| self_constraint.as_id().cmp(&other_constraint.as_id())),
)
}
}

/// A BDD node.
///
/// The "variables" of a constraint set BDD are individual constraints, represented by an interned
Expand All @@ -442,8 +422,8 @@ impl<'db> PartialOrd<ConstrainedTypeVar<'db>> for ConstraintOrdering<'db> {
/// that point at the same node.
///
/// 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. [`ConstraintOrdering`] defines the variable ordering that
/// we use for constraint set BDDs.
/// visits variables in the same order. [`ConstrainedTypeVar::ordering`] defines the variable
/// ordering that we use for constraint set BDDs.
#[derive(Clone, Copy, Debug, Eq, Hash, PartialEq, get_size2::GetSize, salsa::Update)]
enum Node<'db> {
AlwaysFalse,
Expand All @@ -460,11 +440,11 @@ impl<'db> Node<'db> {
if_false: Node<'db>,
) -> Self {
debug_assert!((if_true.root_constraint(db)).is_none_or(|root_constraint| {
ConstraintOrdering(db, root_constraint) > constraint
root_constraint.ordering(db) > constraint.ordering(db)
}));
debug_assert!(
(if_false.root_constraint(db)).is_none_or(|root_constraint| {
ConstraintOrdering(db, root_constraint) > constraint
root_constraint.ordering(db) > constraint.ordering(db)
})
);
if if_true == if_false {
Expand Down Expand Up @@ -925,80 +905,77 @@ impl<'db> InteriorNode<'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 ConstraintOrdering(db, self_constraint).partial_cmp(&other_constraint) {
Some(Ordering::Equal) => Node::new(
match (self_constraint.ordering(db)).cmp(&other_constraint.ordering(db)) {
Ordering::Equal => Node::new(
db,
self_constraint,
self.if_true(db).or(db, other.if_true(db)),
self.if_false(db).or(db, other.if_false(db)),
),
Some(Ordering::Less) => Node::new(
Ordering::Less => Node::new(
db,
self_constraint,
self.if_true(db).or(db, Node::Interior(other)),
self.if_false(db).or(db, Node::Interior(other)),
),
Some(Ordering::Greater) => Node::new(
Ordering::Greater => Node::new(
db,
other_constraint,
Node::Interior(self).or(db, other.if_true(db)),
Node::Interior(self).or(db, other.if_false(db)),
),
None => unreachable!("constraints should always be comparable"),
}
}

#[salsa::tracked(heap_size=ruff_memory_usage::heap_size)]
fn and(self, db: &'db dyn Db, other: Self) -> Node<'db> {
let self_constraint = self.constraint(db);
let other_constraint = other.constraint(db);
match ConstraintOrdering(db, self_constraint).partial_cmp(&other_constraint) {
Some(Ordering::Equal) => Node::new(
match (self_constraint.ordering(db)).cmp(&other_constraint.ordering(db)) {
Ordering::Equal => Node::new(
db,
self_constraint,
self.if_true(db).and(db, other.if_true(db)),
self.if_false(db).and(db, other.if_false(db)),
),
Some(Ordering::Less) => Node::new(
Ordering::Less => Node::new(
db,
self_constraint,
self.if_true(db).and(db, Node::Interior(other)),
self.if_false(db).and(db, Node::Interior(other)),
),
Some(Ordering::Greater) => Node::new(
Ordering::Greater => Node::new(
db,
other_constraint,
Node::Interior(self).and(db, other.if_true(db)),
Node::Interior(self).and(db, other.if_false(db)),
),
None => unreachable!("constraints should always be comparable"),
}
}

#[salsa::tracked(heap_size=ruff_memory_usage::heap_size)]
fn iff(self, db: &'db dyn Db, other: Self) -> Node<'db> {
let self_constraint = self.constraint(db);
let other_constraint = other.constraint(db);
match ConstraintOrdering(db, self_constraint).partial_cmp(&other_constraint) {
Some(Ordering::Equal) => Node::new(
match (self_constraint.ordering(db)).cmp(&other_constraint.ordering(db)) {
Ordering::Equal => Node::new(
db,
self_constraint,
self.if_true(db).iff(db, other.if_true(db)),
self.if_false(db).iff(db, other.if_false(db)),
),
Some(Ordering::Less) => Node::new(
Ordering::Less => Node::new(
db,
self_constraint,
self.if_true(db).iff(db, Node::Interior(other)),
self.if_false(db).iff(db, Node::Interior(other)),
),
Some(Ordering::Greater) => Node::new(
Ordering::Greater => Node::new(
db,
other_constraint,
Node::Interior(self).iff(db, other.if_true(db)),
Node::Interior(self).iff(db, other.if_false(db)),
),
None => unreachable!("constraints should always be comparable"),
}
}

Expand All @@ -1012,7 +989,7 @@ impl<'db> InteriorNode<'db> {
// point in the BDD where the assignment can no longer affect the result,
// and we can return early.
let self_constraint = self.constraint(db);
if ConstraintOrdering(db, assignment.constraint()) < self_constraint {
if assignment.constraint().ordering(db) < self_constraint.ordering(db) {
return (Node::Interior(self), false);
}

Expand Down
Loading