From eec4e2ed11e848fd2bc3c6d9587ff7b16ba42090 Mon Sep 17 00:00:00 2001 From: Douglas Creager Date: Fri, 17 Oct 2025 09:04:40 -0400 Subject: [PATCH] add impossible terminal --- .../src/types/constraints.rs | 47 ++++++++++++++----- 1 file changed, 35 insertions(+), 12 deletions(-) diff --git a/crates/ty_python_semantic/src/types/constraints.rs b/crates/ty_python_semantic/src/types/constraints.rs index 6de20c09d9..e7c0920dcd 100644 --- a/crates/ty_python_semantic/src/types/constraints.rs +++ b/crates/ty_python_semantic/src/types/constraints.rs @@ -409,6 +409,7 @@ impl<'db> ConstrainedTypeVar<'db> { enum Node<'db> { AlwaysFalse, AlwaysTrue, + Impossible, Interior(InteriorNode<'db>), } @@ -464,11 +465,22 @@ impl<'db> Node<'db> { matches!(self, Node::AlwaysFalse) } + /// Given a BDD that evaluates to `false` for some conditions, returns a new BDD where those + /// conditions are `impossible`. + fn impossible(self, db: &'db dyn Db) -> Self { + match self { + Node::AlwaysTrue => Node::AlwaysTrue, + Node::AlwaysFalse | Node::Impossible => Node::Impossible, + Node::Interior(interior) => interior.impossible(db), + } + } + /// Returns the negation of this BDD. fn negate(self, db: &'db dyn Db) -> Self { match self { Node::AlwaysTrue => Node::AlwaysFalse, Node::AlwaysFalse => Node::AlwaysTrue, + Node::Impossible => Node::Impossible, Node::Interior(interior) => interior.negate(db), } } @@ -476,6 +488,7 @@ impl<'db> Node<'db> { /// Returns the `or` or union of two BDDs. fn or(self, db: &'db dyn Db, other: Self) -> Self { match (self, other) { + (Node::Impossible, _) | (_, Node::Impossible) => Node::Impossible, (Node::AlwaysTrue, _) | (_, Node::AlwaysTrue) => Node::AlwaysTrue, (Node::AlwaysFalse, other) | (other, Node::AlwaysFalse) => other, (Node::Interior(a), Node::Interior(b)) => { @@ -489,6 +502,7 @@ impl<'db> Node<'db> { /// Returns the `and` or intersection of two BDDs. fn and(self, db: &'db dyn Db, other: Self) -> Self { match (self, other) { + (Node::Impossible, _) | (_, Node::Impossible) => Node::Impossible, (Node::AlwaysFalse, _) | (_, Node::AlwaysFalse) => Node::AlwaysFalse, (Node::AlwaysTrue, other) | (other, Node::AlwaysTrue) => other, (Node::Interior(a), Node::Interior(b)) => { @@ -502,6 +516,7 @@ impl<'db> Node<'db> { /// Returns the `xor` of two BDDs. fn xor(self, db: &'db dyn Db, other: Self) -> Self { match (self, other) { + (Node::Impossible, _) | (_, Node::Impossible) => Node::Impossible, (Node::AlwaysFalse, other) | (other, Node::AlwaysFalse) => other, (Node::AlwaysTrue, Node::AlwaysTrue) => Node::AlwaysFalse, (Node::AlwaysTrue, Node::Interior(interior)) @@ -518,6 +533,7 @@ impl<'db> Node<'db> { /// result. fn iff(self, db: &'db dyn Db, other: Self) -> Self { match (self, other) { + (Node::Impossible, _) | (_, Node::Impossible) => Node::Impossible, (Node::AlwaysFalse, Node::AlwaysFalse) | (Node::AlwaysTrue, Node::AlwaysTrue) => { Node::AlwaysTrue } @@ -578,6 +594,7 @@ impl<'db> Node<'db> { match self { Node::AlwaysTrue => (Node::AlwaysTrue, false), Node::AlwaysFalse => (Node::AlwaysFalse, false), + Node::Impossible => (Node::Impossible, false), Node::Interior(interior) => interior.restrict_one(db, assignment), } } @@ -603,14 +620,8 @@ impl<'db> Node<'db> { /// so we don't need to care what the BDD evaluates to when `T ≤ bool ∧ T ≰ int`, since that is /// not a valid combination of constraints. fn simplify(self, db: &'db dyn Db) -> Self { - // TODO: Simplifying to `false` for invalid assignments is correct, but means that our - // display output is not always as compact as it could be. Ideally, we would map impossible - // inputs to a new "don't care" terminal, and update our `Display` impl to display the - // smallest formula, choosing arbitrarily whether each "don't care" is true or false. Since - // that doesn't effect _correctness_, just the rendering in our test cases, I've punted on - // that for now. match self { - Node::AlwaysTrue | Node::AlwaysFalse => self, + Node::AlwaysTrue | Node::AlwaysFalse | Node::Impossible => self, Node::Interior(interior) => interior.simplify(db), } } @@ -626,7 +637,7 @@ impl<'db> Node<'db> { impl<'db> Searcher<'db> { fn visit_node(&mut self, db: &'db dyn Db, node: Node<'db>) { match node { - Node::AlwaysFalse => {} + Node::AlwaysFalse | Node::Impossible => {} Node::AlwaysTrue => self.clauses.push(self.current_clause.clone()), Node::Interior(interior) => { let interior_constraint = interior.constraint(db); @@ -665,6 +676,7 @@ impl<'db> Node<'db> { match self.node { Node::AlwaysTrue => f.write_str("always"), Node::AlwaysFalse => f.write_str("never"), + Node::Impossible => f.write_str("impossible"), Node::Interior(_) => { let mut clauses = self.node.satisfied_clauses(self.db); clauses.simplify(self.db); @@ -706,6 +718,7 @@ impl<'db> Node<'db> { match self.node { Node::AlwaysTrue => write!(f, "always"), Node::AlwaysFalse => write!(f, "never"), + Node::Impossible => write!(f, "impossible"), Node::Interior(interior) => { interior.constraint(self.db).display(self.db).fmt(f)?; write!( @@ -751,6 +764,16 @@ impl get_size2::GetSize for InteriorNode<'_> {} #[salsa::tracked] impl<'db> InteriorNode<'db> { + #[salsa::tracked(heap_size=ruff_memory_usage::heap_size)] + fn impossible(self, db: &'db dyn Db) -> Node<'db> { + Node::new( + db, + self.constraint(db), + self.if_true(db).impossible(db), + self.if_false(db).impossible(db), + ) + } + #[salsa::tracked(heap_size=ruff_memory_usage::heap_size)] fn negate(self, db: &'db dyn Db) -> Node<'db> { Node::new( @@ -920,11 +943,11 @@ impl<'db> InteriorNode<'db> { if left.implies(db, right) { // left → right = ¬left ∨ right let implication = left_constraint.negate(db).or(db, right_constraint); - domain = domain.and(db, implication); + domain = domain.and(db, implication.impossible(db)); } else if right.implies(db, left) { // right → left = ¬right ∨ left let implication = right_constraint.negate(db).or(db, left_constraint); - domain = domain.and(db, implication); + domain = domain.and(db, implication.impossible(db)); } match left.intersect(db, right) { @@ -939,7 +962,7 @@ impl<'db> InteriorNode<'db> { let implication = (left_constraint.negate(db)) .or(db, right_constraint.negate(db)) .or(db, intersection_constraint); - domain = domain.and(db, implication); + domain = domain.and(db, implication.impossible(db)); // But we also want to perform some replacements: // - `left ∧ right` becomes `intersection` @@ -974,7 +997,7 @@ impl<'db> InteriorNode<'db> { let no_conflict = left_constraint .negate(db) .or(db, right_constraint.negate(db)); - domain = domain.and(db, no_conflict); + domain = domain.and(db, no_conflict.impossible(db)); } } }