debug

crates/ty_python_semantic/src/types/constraints.rs

@@ -471,6 +471,15 @@ impl<'db> Node<'db> {
         matches!(self, Node::AlwaysFalse)
     }
 
+    /// Returns the number of internal nodes in this BDD. This is a decent proxy for the complexity
+    /// of the function that the BDD represents.
+    fn interior_node_count(self, db: &'db dyn Db) -> usize {
+        match self {
+            Node::AlwaysTrue | Node::AlwaysFalse => 0,
+            Node::Interior(interior) => interior.interior_node_count(db),
+        }
+    }
+
     /// Returns the negation of this BDD.
     fn negate(self, db: &'db dyn Db) -> Self {
         match self {
@@ -574,6 +583,58 @@ impl<'db> Node<'db> {
         }
     }
 
+    /// Returns the minimization of this BDD given a particular set of inputs that you don't care
+    /// about. The result BDD's output is undefined for all of the inputs in the `do_not_care` set,
+    /// but it will agree with this BDD for all other inputs.
+    ///
+    /// The `do_not_care` set typically encodes impossible situations in the input space. For a
+    /// specific example involving constraint sets, this lets us model two constraints that are
+    /// disjoint, whose intersection is empty. It is not possible for both constraints to be true,
+    /// and so any input with both of the corresponding BDD variables set is invalid. For those
+    /// invalid inputs, it doesn't matter which output the BDD produces. Of all of the possible
+    /// BDDs that produce correct results for the _valid_ inputs, we want the smallest one.
+    ///
+    /// We currently use a brute-force algorithm to calculate the minimization, which should be
+    /// fine for the sizes of BDDs and don't-care sets that we work with.
+    fn minimize(self, db: &'db dyn Db, do_not_care: Node<'db>) -> Self {
+        eprintln!("==> minimize    {}", self.display(db));
+        eprintln!("    relative to {}", do_not_care.display(db));
+        self.minimizations(db, do_not_care)
+            .as_slice()
+            .iter()
+            .copied()
+            .next()
+            .expect("all BDDs should have a minimization")
+    }
+
+    /// Returns all of the minimizations of this BDD that have the same size as the smallest
+    /// minimization.
+    fn minimizations(self, db: &'db dyn Db, do_not_care: Node<'db>) -> Minimized<'db, 'db> {
+        eprintln!(" -> minimizations {}", self.display(db));
+        eprintln!(" -> relative to   {}", do_not_care.display(db));
+        match (self, do_not_care) {
+            // If we never care about this node, then its minimization can evaluate to any result.
+            (_, Node::AlwaysTrue) => {
+                eprintln!(" -> minimizations of {}", self.display(db));
+                eprintln!("    always");
+                eprintln!("    never");
+                Minimized::OwnedTwo([Node::AlwaysTrue, Node::AlwaysFalse])
+            }
+            // If we always care about this node, then its minimization should behave the same as
+            // the node itself.
+            (_, Node::AlwaysFalse) => {
+                eprintln!(" -> minimizations of {}", self.display(db));
+                eprintln!("    {}", self.display(db));
+                Minimized::OwnedOne(self)
+            }
+            // If we sometimes care about this node, we need to recurse down, finding the
+            // minimizations of each side and combining them back together.
+            (_, Node::Interior(do_not_care)) => {
+                Minimized::Borrowed(do_not_care.minimizations_of(db, self))
+            }
+        }
+    }
+
     /// Returns a new BDD with any occurrence of `left ∧ right` replaced with `replacement`.
     fn substitute_intersection(
         self,
@@ -786,6 +847,11 @@ impl get_size2::GetSize for InteriorNode<'_> {}
 
 #[salsa::tracked]
 impl<'db> InteriorNode<'db> {
+    #[salsa::tracked(heap_size=ruff_memory_usage::heap_size)]
+    fn interior_node_count(self, db: &'db dyn Db) -> usize {
+        1 + self.if_true(db).interior_node_count(db) + self.if_false(db).interior_node_count(db)
+    }
+
     #[salsa::tracked(heap_size=ruff_memory_usage::heap_size)]
     fn negate(self, db: &'db dyn Db) -> Node<'db> {
         Node::new(
@@ -904,6 +970,55 @@ impl<'db> InteriorNode<'db> {
         }
     }
 
+    #[salsa::tracked(returns(deref), heap_size=ruff_memory_usage::heap_size)]
+    fn minimizations_of(self, db: &'db dyn Db, node: Node<'db>) -> Box<[Node<'db>]> {
+        let do_not_care = self;
+        let do_not_care_constraint = do_not_care.constraint(db);
+        let (constraint, true_minimized, false_minimized) = match node {
+            Node::AlwaysTrue | Node::AlwaysFalse => (
+                do_not_care_constraint,
+                node.minimizations(db, do_not_care.if_true(db)),
+                node.minimizations(db, do_not_care.if_false(db)),
+            ),
+            Node::Interior(node) => {
+                let node_constraint = node.constraint(db);
+                match node_constraint.cmp(&do_not_care_constraint) {
+                    Ordering::Equal => (
+                        node_constraint,
+                        (node.if_true(db)).minimizations(db, do_not_care.if_true(db)),
+                        (node.if_false(db)).minimizations(db, do_not_care.if_false(db)),
+                    ),
+                    Ordering::Less => (
+                        node_constraint,
+                        (node.if_true(db)).minimizations(db, Node::Interior(do_not_care)),
+                        (node.if_false(db)).minimizations(db, Node::Interior(do_not_care)),
+                    ),
+                    Ordering::Greater => (
+                        do_not_care_constraint,
+                        Node::Interior(node).minimizations(db, do_not_care.if_true(db)),
+                        Node::Interior(node).minimizations(db, do_not_care.if_false(db)),
+                    ),
+                }
+            }
+        };
+
+        eprintln!(" -> minimizations of {}", node.display(db));
+        let mut result = Vec::new();
+        for if_true in true_minimized.as_slice() {
+            for if_false in false_minimized.as_slice() {
+                let x = Node::new(db, constraint, *if_true, *if_false);
+                eprintln!("    {} {}", x.interior_node_count(db), x.display(db));
+                result.push(x);
+            }
+        }
+        let minimum_size = (result.iter())
+            .map(|node| node.interior_node_count(db))
+            .min()
+            .expect("minimizing should never produce an empty BDD");
+        result.retain(|node| node.interior_node_count(db) == minimum_size);
+        result.into_boxed_slice()
+    }
+
     #[salsa::tracked(heap_size=ruff_memory_usage::heap_size)]
     fn simplify(self, db: &'db dyn Db) -> Node<'db> {
         // To simplify a non-terminal BDD, we find all pairs of constraints that are mentioned in
@@ -951,12 +1066,18 @@ impl<'db> InteriorNode<'db> {
                 None
             };
             if let Some((larger_constraint, smaller_constraint)) = larger_smaller {
+                let larger_node = Node::new_satisfied_constraint(db, larger_constraint.when_true());
+                let smaller_node =
+                    Node::new_satisfied_constraint(db, smaller_constraint.when_true());
+                let not_larger_node =
+                    Node::new_satisfied_constraint(db, larger_constraint.when_false());
+
                 // larger ∨ smaller = larger
                 simplified = simplified.substitute_union(
                     db,
                     larger_constraint.when_true(),
                     smaller_constraint.when_true(),
-                    Node::new_satisfied_constraint(db, larger_constraint.when_true()),
+                    larger_node,
                 );
 
                 // ¬larger ∧ ¬smaller = ¬larger
@@ -964,26 +1085,12 @@ impl<'db> InteriorNode<'db> {
                     db,
                     larger_constraint.when_false(),
                     smaller_constraint.when_false(),
-                    Node::new_satisfied_constraint(db, larger_constraint.when_false()),
+                    not_larger_node,
                 );
 
                 // smaller ∧ ¬larger = false
                 // (¬larger removes everything that's present in smaller)
-                simplified = simplified.substitute_intersection(
-                    db,
-                    larger_constraint.when_false(),
-                    smaller_constraint.when_true(),
-                    Node::AlwaysFalse,
-                );
-
-                // larger ∨ ¬smaller = true
-                // (larger fills in everything that's missing in ¬smaller)
-                simplified = simplified.substitute_union(
-                    db,
-                    larger_constraint.when_true(),
-                    smaller_constraint.when_false(),
-                    Node::AlwaysTrue,
-                );
+                simplified = simplified.minimize(db, smaller_node.and(db, not_larger_node));
             }
 
             // There are some simplifications we can make when the intersection of the two
@@ -1070,19 +1177,10 @@ impl<'db> InteriorNode<'db> {
                     // and right is empty.
 
                     // left ∧ right = false
-                    simplified = simplified.substitute_intersection(
+                    simplified = simplified.minimize(
                         db,
-                        left_constraint.when_true(),
-                        right_constraint.when_true(),
-                        Node::AlwaysFalse,
-                    );
-
-                    // ¬left ∨ ¬right = true
-                    simplified = simplified.substitute_union(
-                        db,
-                        left_constraint.when_false(),
-                        right_constraint.when_false(),
-                        Node::AlwaysTrue,
+                        Node::new_constraint(db, left_constraint)
+                            .and(db, Node::new_constraint(db, right_constraint)),
                     );
 
                     // left ∧ ¬right = left
@@ -1110,6 +1208,23 @@ impl<'db> InteriorNode<'db> {
     }
 }
 
+#[derive(Clone, Debug, Eq, Hash, PartialEq)]
+enum Minimized<'a, 'db> {
+    OwnedOne(Node<'db>),
+    OwnedTwo([Node<'db>; 2]),
+    Borrowed(&'a [Node<'db>]),
+}
+
+impl<'a, 'db> Minimized<'a, 'db> {
+    fn as_slice(&'a self) -> &'a [Node<'db>] {
+        match self {
+            Minimized::OwnedOne(owned) => std::slice::from_ref(owned),
+            Minimized::OwnedTwo(owned) => owned,
+            Minimized::Borrowed(borrowed) => borrowed,
+        }
+    }
+}
+
 /// An assignment of one BDD variable to either `true` or `false`. (When evaluating a BDD, we
 /// must provide an assignment for each variable present in the BDD.)
 #[derive(Clone, Copy, Debug, Eq, Hash, PartialEq)]