only keep smallest minimizations

This commit is contained in:
Douglas Creager 2025-09-29 16:56:23 -04:00
parent 69d60cb5d8
commit 07dbe2d8cf
1 changed files with 23 additions and 1 deletions

View File

@ -431,6 +431,15 @@ impl<'db> Node<'db> {
}
}
/// 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 clauses describing all of the variable assignments that cause this BDD to evaluate
/// to `true`. (This translates the boolean function that this BDD represents into DNF form.)
fn satisfied_clauses(self, db: &'db dyn Db) -> SatisfiedClauses<'db> {
@ -506,6 +515,14 @@ struct InteriorNode<'db> {
// The Salsa heap is tracked separately.
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)
}
}
/// An "underspecified" BDD node.
///
/// This is just like a BDD [`Node`], but with an additional
@ -1472,7 +1489,12 @@ impl<'db> PossiblySpecifiedInteriorNode<'db> {
minimizations.push(Node::new(db, constraint, *if_true, *if_false));
}
}
// XXX: keep smallest
let minimum_size = minimizations
.iter()
.map(|node| node.interior_node_count(db))
.min()
.unwrap_or_default();
minimizations.retain(|node| node.interior_node_count(db) == minimum_size);
minimizations.into_boxed_slice()
}
}