diff --git a/crates/oxidd-core/src/lib.rs b/crates/oxidd-core/src/lib.rs index f35f818..c0cf652 100644 --- a/crates/oxidd-core/src/lib.rs +++ b/crates/oxidd-core/src/lib.rs @@ -230,6 +230,10 @@ pub trait InnerNode: Sized + Eq + Hash + DropWith { /// number and want to get the level number. fn check_level(&self, check: impl FnOnce(LevelNo) -> bool) -> bool; + /// Panics if the node types stores a level and the node's level is not + /// `level` + fn assert_level_matches(&self, level: LevelNo); + /// Get the children of this node as an iterator #[must_use] fn children(&self) -> Self::ChildrenIter<'_>; @@ -293,7 +297,8 @@ pub type AtomicLevelNo = std::sync::atomic::AtomicU32; /// 1. A node in a [`LevelView`] with level number L has level number L (i.e. /// `self.level()` returns L). /// 2. [`InnerNode::check_level()`] with a check `c` must return -/// `c(self.level())`. +/// `c(self.level())`. Similarly, [`InnerNode::assert_level_matches()`] must +/// panic if the level does not match. /// /// These conditions are crucial to enable concurrent level swaps as part of /// reordering (see the `oxidd-reorder` crate): The algorithm iterates over the diff --git a/crates/oxidd-manager-index/src/manager.rs b/crates/oxidd-manager-index/src/manager.rs index a6856bf..3fcfb54 100644 --- a/crates/oxidd-manager-index/src/manager.rs +++ b/crates/oxidd-manager-index/src/manager.rs @@ -1004,7 +1004,7 @@ where Ok(e2) } - #[inline] + #[inline(always)] fn level(&self, no: LevelNo) -> Self::LevelView<'_> { LevelView { store: self.store(), @@ -1486,19 +1486,13 @@ where // No need to check if the node referenced by `edge` is stored in // `self.store` due to lifetime restrictions. let nodes = &self.store.inner_nodes; - nodes.inner_node(&edge).check_level(|level| { - assert_eq!(level, self.level, "node level does not match"); - true - }); + nodes.inner_node(&edge).assert_level_matches(self.level); self.set.insert(nodes, edge) } #[inline(always)] fn get_or_insert(&mut self, node: N) -> AllocResult> { - node.check_level(|level| { - assert_eq!(level, self.level, "node level does not match"); - true - }); + node.assert_level_matches(self.level); // No need to check if the children of `node` are stored in `self.store` // due to lifetime restrictions. self.set.get_or_insert( @@ -1605,19 +1599,13 @@ where // No need to check if the node referenced by `edge` is stored in // `self.store` due to lifetime restrictions. let nodes = &self.store.inner_nodes; - nodes.inner_node(&edge).check_level(|level| { - assert_eq!(level, self.level, "node level does not match"); - true - }); + nodes.inner_node(&edge).assert_level_matches(self.level); self.set.insert(nodes, edge) } #[inline(always)] fn get_or_insert(&mut self, node: N) -> AllocResult> { - node.check_level(|level| { - assert_eq!(level, self.level, "node level does not match"); - true - }); + node.assert_level_matches(self.level); // No need to check if the children of `node` are stored in `self.store` // due to lifetime restrictions. self.set.get_or_insert( diff --git a/crates/oxidd-manager-index/src/node/fixed_arity.rs b/crates/oxidd-manager-index/src/node/fixed_arity.rs index 01a733d..f779b29 100644 --- a/crates/oxidd-manager-index/src/node/fixed_arity.rs +++ b/crates/oxidd-manager-index/src/node/fixed_arity.rs @@ -140,6 +140,15 @@ impl<'id, ET: Tag, const ARITY: usize> InnerNode> fn check_level(&self, check: impl FnOnce(LevelNo) -> bool) -> bool { check(self.level.load(Relaxed)) } + #[inline(always)] + #[track_caller] + fn assert_level_matches(&self, level: LevelNo) { + assert_eq!( + self.level.load(Relaxed), + level, + "the level number does not match" + ); + } #[inline(always)] fn children(&self) -> Self::ChildrenIter<'_> { diff --git a/crates/oxidd-manager-pointer/src/manager.rs b/crates/oxidd-manager-pointer/src/manager.rs index ba3b9ef..d2b738e 100644 --- a/crates/oxidd-manager-pointer/src/manager.rs +++ b/crates/oxidd-manager-pointer/src/manager.rs @@ -674,10 +674,7 @@ where let level_no = self.unique_table.len() as LevelNo; assert!(level_no < LevelNo::MAX, "too many levels"); let node = f(level_no); - node.check_level(|l| { - assert_eq!(l, level_no, "node level does not match"); - true - }); + node.assert_level_matches(level_no); let [e1, e2] = add_node(self.store(), node)?; @@ -690,7 +687,7 @@ where Ok(e2) } - #[inline] + #[inline(always)] fn level(&self, no: LevelNo) -> Self::LevelView<'_> { LevelView { store: self.store(), @@ -1282,19 +1279,13 @@ where 0, "can only insert untagged edges pointing to inner nodes" ); - unsafe { edge.inner_node_unchecked() }.check_level(|l| { - assert_eq!(l, self.level, "node level does not match"); - true - }); + unsafe { edge.inner_node_unchecked() }.assert_level_matches(self.level); self.set.insert(edge) } #[inline(always)] fn get_or_insert(&mut self, node: N) -> AllocResult> { - node.check_level(|l| { - assert_eq!(l, self.level, "node level does not match"); - true - }); + node.assert_level_matches(self.level); // No need to check if the children of `node` are stored in `self.store` // due to lifetime restrictions. LevelViewSet::get_or_insert(&mut *self.set, node, |node| add_node(self.store, node)) @@ -1399,19 +1390,13 @@ where 0, "can only insert untagged edges pointing to inner nodes" ); - unsafe { edge.inner_node_unchecked() }.check_level(|l| { - assert_eq!(l, self.level, "node level does not match"); - true - }); + unsafe { edge.inner_node_unchecked() }.assert_level_matches(self.level); self.set.insert(edge) } #[inline(always)] fn get_or_insert(&mut self, node: N) -> AllocResult> { - node.check_level(|l| { - assert_eq!(l, self.level, "node level does not match"); - true - }); + node.assert_level_matches(self.level); // No need to check if the children of `node` are stored in `self.store` // due to lifetime restrictions. self.set diff --git a/crates/oxidd-manager-pointer/src/node/fixed_arity.rs b/crates/oxidd-manager-pointer/src/node/fixed_arity.rs index 6f2624f..d78ad8c 100644 --- a/crates/oxidd-manager-pointer/src/node/fixed_arity.rs +++ b/crates/oxidd-manager-pointer/src/node/fixed_arity.rs @@ -150,6 +150,15 @@ impl<'id, ET: Tag, const TAG_BITS: u32, const ARITY: usize> fn check_level(&self, check: impl FnOnce(LevelNo) -> bool) -> bool { check(self.level.load(Relaxed)) } + #[inline(always)] + #[track_caller] + fn assert_level_matches(&self, level: LevelNo) { + assert_eq!( + self.level.load(Relaxed), + level, + "the level number does not match" + ); + } #[inline(always)] fn children(&self) -> Self::ChildrenIter<'_> { diff --git a/crates/oxidd-rules-bdd/src/complement_edge/mod.rs b/crates/oxidd-rules-bdd/src/complement_edge/mod.rs index 2b26f7c..30e6771 100644 --- a/crates/oxidd-rules-bdd/src/complement_edge/mod.rs +++ b/crates/oxidd-rules-bdd/src/complement_edge/mod.rs @@ -209,16 +209,32 @@ fn reduce( level: LevelNo, t: M::Edge, e: M::Edge, - _op: BCDDOp, + op: BCDDOp, ) -> AllocResult where M: Manager, { - let tmp = >::reduce(manager, level, [t, e]); - if let ReducedOrNew::Reduced(..) = &tmp { - stat!(reduced _op); + // We do not use `DiagramRules::reduce()` here, as the iterator is + // apparently not fully optimized away. + if t == e { + stat!(reduced op); + manager.drop_edge(e); + return Ok(t); } - tmp.then_insert(manager, level) + + let tt = t.tag(); + let (node, tag) = if tt == EdgeTag::Complemented { + let et = e.tag(); + let node = M::InnerNode::new( + level, + [t.with_tag_owned(EdgeTag::None), e.with_tag_owned(!et)], + ); + (node, EdgeTag::Complemented) + } else { + (M::InnerNode::new(level, [t, e]), EdgeTag::None) + }; + + Ok(oxidd_core::LevelView::get_or_insert(&mut manager.level(level), node)?.with_tag_owned(tag)) } // --- Terminal Type ----------------------------------------------------------- diff --git a/crates/oxidd-rules-bdd/src/simple/mod.rs b/crates/oxidd-rules-bdd/src/simple/mod.rs index d9812cf..73e23a6 100644 --- a/crates/oxidd-rules-bdd/src/simple/mod.rs +++ b/crates/oxidd-rules-bdd/src/simple/mod.rs @@ -59,21 +59,21 @@ impl> DiagramRules for BDDRules { /// Apply the reduction rules, creating a node in `manager` if necessary #[inline(always)] -fn reduce( - manager: &M, - level: LevelNo, - t: M::Edge, - e: M::Edge, - _op: BDDOp, -) -> AllocResult +fn reduce(manager: &M, level: LevelNo, t: M::Edge, e: M::Edge, op: BDDOp) -> AllocResult where M: Manager, { - let tmp = >::reduce(manager, level, [t, e]); - if let ReducedOrNew::Reduced(..) = &tmp { - stat!(reduced _op); + // We do not use `DiagramRules::reduce()` here, as the iterator is + // apparently not fully optimized away. + if t == e { + stat!(reduced op); + manager.drop_edge(e); + return Ok(t); } - tmp.then_insert(manager, level) + oxidd_core::LevelView::get_or_insert( + &mut manager.level(level), + M::InnerNode::new(level, [t, e]), + ) } /// Collect the two children of a binary node diff --git a/crates/oxidd-rules-zbdd/src/lib.rs b/crates/oxidd-rules-zbdd/src/lib.rs index 721d050..bfc9fff 100644 --- a/crates/oxidd-rules-zbdd/src/lib.rs +++ b/crates/oxidd-rules-zbdd/src/lib.rs @@ -71,12 +71,17 @@ fn reduce( where M: Manager, { - let _ = op; - let tmp = >::reduce(manager, level, [hi, lo]); - if let ReducedOrNew::Reduced(..) = &tmp { + // We do not use `DiagramRules::reduce()` here, as the iterator is + // apparently not fully optimized away. + if manager.get_node(&hi).is_terminal(&ZBDDTerminal::Empty) { stat!(reduced op); + manager.drop_edge(hi); + return Ok(lo); } - tmp.then_insert(manager, level) + oxidd_core::LevelView::get_or_insert( + &mut manager.level(level), + M::InnerNode::new(level, [hi, lo]), + ) } #[inline(always)] diff --git a/crates/oxidd-test-utils/src/edge.rs b/crates/oxidd-test-utils/src/edge.rs index 182e62f..deab0f8 100644 --- a/crates/oxidd-test-utils/src/edge.rs +++ b/crates/oxidd-test-utils/src/edge.rs @@ -326,6 +326,7 @@ impl InnerNode for DummyNode { fn check_level(&self, _check: impl FnOnce(LevelNo) -> bool) -> bool { true } + fn assert_level_matches(&self, _level: LevelNo) {} fn children(&self) -> Self::ChildrenIter<'_> { std::iter::empty() diff --git a/crates/oxidd/tests/boolean_function.rs b/crates/oxidd/tests/boolean_function.rs index 69370a0..5b66f29 100644 --- a/crates/oxidd/tests/boolean_function.rs +++ b/crates/oxidd/tests/boolean_function.rs @@ -709,10 +709,10 @@ impl<'a, B: BooleanFunction> TestAllBooleanFunctions<'a, B> { let mut choice_requested = 0u32; let cube = f.pick_cube([], |manager, edge, level| { - assert!(manager + manager .get_node(edge) .unwrap_inner() - .check_level(|l| l == level)); + .assert_level_matches(level); if choice_requested & (1 << level) != 0 { panic!("choice requested twice for x{level}"); } else { @@ -723,10 +723,10 @@ impl<'a, B: BooleanFunction> TestAllBooleanFunctions<'a, B> { let mut choice_requested_sym = 0u32; let dd_cube = f .pick_cube_dd(|manager, edge, level| { - assert!(manager + manager .get_node(edge) .unwrap_inner() - .check_level(|l| l == level)); + .assert_level_matches(level); if choice_requested_sym & (1 << level) != 0 { panic!("choice requested twice for x{level}"); } else {