move negate

This commit is contained in:
Douglas Creager 2025-09-29 15:34:22 -04:00
parent 8a314f252d
commit c55c400281
1 changed files with 16 additions and 38 deletions

View File

@ -441,15 +441,6 @@ impl<'db> Node<'db> {
matches!(self, Node::AlwaysFalse) matches!(self, Node::AlwaysFalse)
} }
/// 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::Interior(interior) => interior.negate(db),
}
}
/// Returns the `or` or union of two BDDs. /// Returns the `or` or union of two BDDs.
fn or(self, db: &'db dyn Db, other: Self) -> Self { fn or(self, db: &'db dyn Db, other: Self) -> Self {
match (self, other) { match (self, other) {
@ -506,13 +497,6 @@ impl<'db> Node<'db> {
} }
} }
/// Returns the `if-then-else` of three BDDs: when `self` evaluates to `true`, it returns what
/// `then_node` evaluates to; otherwise it returns what `else_node` evaluates to.
fn ite(self, db: &'db dyn Db, then_node: Self, else_node: Self) -> Self {
self.and(db, then_node)
.or(db, self.negate(db).and(db, else_node))
}
/// Returns clauses describing all of the variable assignments that cause this BDD to evaluate /// 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.) /// to `true`. (This translates the boolean function that this BDD represents into DNF form.)
fn satisfied_clauses(self, db: &'db dyn Db) -> SatisfiedClauses<'db> { fn satisfied_clauses(self, db: &'db dyn Db) -> SatisfiedClauses<'db> {
@ -590,16 +574,6 @@ impl get_size2::GetSize for InteriorNode<'_> {}
#[salsa::tracked] #[salsa::tracked]
impl<'db> InteriorNode<'db> { impl<'db> InteriorNode<'db> {
#[salsa::tracked(heap_size=ruff_memory_usage::heap_size)]
fn negate(self, db: &'db dyn Db) -> Node<'db> {
Node::new(
db,
self.constraint(db),
self.if_true(db).negate(db),
self.if_false(db).negate(db),
)
}
#[salsa::tracked(heap_size=ruff_memory_usage::heap_size)] #[salsa::tracked(heap_size=ruff_memory_usage::heap_size)]
fn or(self, db: &'db dyn Db, other: Self) -> Node<'db> { fn or(self, db: &'db dyn Db, other: Self) -> Node<'db> {
let self_constraint = self.constraint(db); let self_constraint = self.constraint(db);
@ -816,8 +790,12 @@ impl<'db> UnderspecifiedNode<'db> {
UnderspecifiedNode::AlwaysTrue => UnderspecifiedNode::AlwaysFalse, UnderspecifiedNode::AlwaysTrue => UnderspecifiedNode::AlwaysFalse,
UnderspecifiedNode::AlwaysFalse => UnderspecifiedNode::AlwaysTrue, UnderspecifiedNode::AlwaysFalse => UnderspecifiedNode::AlwaysTrue,
UnderspecifiedNode::Impossible => UnderspecifiedNode::Impossible, UnderspecifiedNode::Impossible => UnderspecifiedNode::Impossible,
UnderspecifiedNode::Interior(interior) => interior.negate(db), UnderspecifiedNode::FullySpecified(interior) => {
UnderspecifiedNode::FullySpecified(interior) => interior.negate(db).into(), PossiblySpecifiedInteriorNode::from(interior).negate(db)
}
UnderspecifiedNode::Interior(interior) => {
PossiblySpecifiedInteriorNode::from(interior).negate(db)
}
} }
} }
@ -1195,16 +1173,6 @@ impl<'db> UnderspecifiedInteriorNode<'db> {
} }
} }
#[salsa::tracked(heap_size=ruff_memory_usage::heap_size)]
fn negate(self, db: &'db dyn Db) -> UnderspecifiedNode<'db> {
UnderspecifiedNode::new(
db,
self.constraint(db),
self.if_true(db).negate(db),
self.if_false(db).negate(db),
)
}
#[salsa::tracked(heap_size=ruff_memory_usage::heap_size)] #[salsa::tracked(heap_size=ruff_memory_usage::heap_size)]
fn or(self, db: &'db dyn Db, other: UnderspecifiedNode<'db>) -> UnderspecifiedNode<'db> { fn or(self, db: &'db dyn Db, other: UnderspecifiedNode<'db>) -> UnderspecifiedNode<'db> {
match self.cmp_constraints(db, other) { match self.cmp_constraints(db, other) {
@ -1331,6 +1299,16 @@ impl<'db> PossiblySpecifiedInteriorNode<'db> {
} }
} }
#[salsa::tracked(heap_size=ruff_memory_usage::heap_size)]
fn negate(self, db: &'db dyn Db) -> UnderspecifiedNode<'db> {
UnderspecifiedNode::new(
db,
self.constraint(db),
self.if_true(db).negate(db),
self.if_false(db).negate(db),
)
}
#[salsa::tracked(heap_size=ruff_memory_usage::heap_size)] #[salsa::tracked(heap_size=ruff_memory_usage::heap_size)]
fn restrict_one( fn restrict_one(
self, self,