From 192f807db00bd2c53720dad12b99f95120c621a5 Mon Sep 17 00:00:00 2001 From: Matthew Wang Date: Tue, 18 Jul 2023 14:24:37 -0400 Subject: [PATCH 1/4] Draft: sized get or insert (does not compile right now) --- src/backing_store/bump_table.rs | 102 ++++++++++++++++++++++++++- src/backing_store/mod.rs | 4 ++ src/builder/decision_nnf/semantic.rs | 14 ++-- src/repr/bdd.rs | 7 ++ 4 files changed, 121 insertions(+), 6 deletions(-) diff --git a/src/backing_store/bump_table.rs b/src/backing_store/bump_table.rs index 6fa6b5ef..e3a83d49 100644 --- a/src/backing_store/bump_table.rs +++ b/src/backing_store/bump_table.rs @@ -1,7 +1,10 @@ //! A unique table based on a bump allocator and robin-hood hashing //! this is the primary unique table for storing all nodes -use crate::{backing_store::UniqueTable, util::*}; +use crate::{ + backing_store::{AbstractlySized, UniqueTable}, + util::*, +}; use bumpalo::Bump; use rustc_hash::FxHasher; use std::{ @@ -248,6 +251,103 @@ impl<'a, T: Eq + Hash + Clone> BackedRobinhoodTable<'a, T> { } } +impl<'a, T: Eq + Hash + Clone + AbstractlySized> BackedRobinhoodTable<'a, T> { + pub fn sized_get_or_insert_by_hash( + &'a mut self, + hash: u64, + elem: T, + equality_by_hash: bool, + ) -> &'a T { + if (self.len + 1) as f64 > (self.cap as f64 * LOAD_FACTOR) { + self.grow(); + } + + // the current index into the array + let mut pos: usize = (hash as usize) % self.cap; + // the distance this item is from its desired location + let mut psl = 0; + + loop { + if self.is_occupied(pos) { + let cur_itm = self.tbl[pos].clone(); + // first check the hashes to see if these elements could + // possibly be equal; if they are, check if the items are + // equal and return the found pointer if so + if hash == cur_itm.hash { + println!("collision"); + let found: &T = cur_itm.ptr.unwrap(); + if equality_by_hash || *found == elem { + let diff = (elem.abstract_size() as i64) + - (cur_itm.ptr.unwrap().abstract_size() as i64); + if diff != 0 { + println!("size difference (g); delta: {}", diff); + } + self.hits += 1; + return found; + } + } + + // not equal; begin probing + if cur_itm.psl < psl { + // elem is not in the table; insert it at pos and propagate + // the item that is currently here + self.propagate(cur_itm, pos); + let ptr = self.alloc.alloc(elem); + let entry = HashTableElement::new(ptr, hash, psl); + self.len += 1; + self.tbl[pos] = entry; + return ptr; + } + psl += 1; + pos = (pos + 1) % self.cap; // wrap to the beginning of the array + } else { + // this element is unique, so place it in the current spot + let ptr = self.alloc.alloc(elem); + let entry = HashTableElement::new(ptr, hash, psl); + self.len += 1; + self.tbl[pos] = entry; + return ptr; + } + } + } + + pub fn sized_get_by_hash(&'a mut self, hash: u64, elem: T) -> Option<&'a T> { + // the current index into the array + let mut pos: usize = (hash as usize) % self.cap; + // the distance this item is from its desired location + let mut psl = 0; + + loop { + if self.is_occupied(pos) { + let cur_itm = self.tbl[pos].clone(); + if hash == cur_itm.hash { + self.hits += 1; + + let diff = (elem.abstract_size() as i64) + - (cur_itm.ptr.unwrap().abstract_size() as i64); + if diff != 0 { + println!("size difference (g); delta: {}", diff); + } + if diff < 0 { + println!("smaller element found ... replacing"); + let ptr = self.alloc.alloc(elem); + self.tbl[pos] = HashTableElement::new(ptr, hash, psl); + } + return cur_itm.ptr; + } + + if cur_itm.psl < psl { + return None; + } + psl += 1; + pos = (pos + 1) % self.cap; + } else { + return None; + } + } + } +} + impl<'a, T: Hash + Eq + Clone> Default for BackedRobinhoodTable<'a, T> { fn default() -> Self { Self::new() diff --git a/src/backing_store/mod.rs b/src/backing_store/mod.rs index 59551fc2..48dc3edd 100644 --- a/src/backing_store/mod.rs +++ b/src/backing_store/mod.rs @@ -9,3 +9,7 @@ pub trait UniqueTable<'a, T: Eq + Hash> { /// use a hash to allocate space in table, but use strict equality for probing/checking fn get_or_insert(&'a mut self, item: T) -> &'a T; } + +pub trait AbstractlySized { + fn abstract_size(&self) -> usize; +} diff --git a/src/builder/decision_nnf/semantic.rs b/src/builder/decision_nnf/semantic.rs index 2dc9a8e0..07393f9c 100644 --- a/src/builder/decision_nnf/semantic.rs +++ b/src/builder/decision_nnf/semantic.rs @@ -31,7 +31,7 @@ impl<'a, const P: u128> DecisionNNFBuilder<'a> for SemanticDecisionNNFBuilder<'a fn get_or_insert(&'a self, bdd: BddNode<'a>) -> BddPtr<'a> { let semantic_hash = bdd.semantic_hash(&self.order, &self.map); - if let Some(bdd) = self.check_cached_hash_and_neg(semantic_hash) { + if let Some(bdd) = self.check_cached_hash_and_neg(semantic_hash, bdd) { return bdd; } @@ -45,7 +45,7 @@ impl<'a, const P: u128> DecisionNNFBuilder<'a> for SemanticDecisionNNFBuilder<'a unsafe { let tbl = &mut *self.compute_table.as_ptr(); - BddPtr::Reg(tbl.get_or_insert_by_hash(hash, bdd, true)) + BddPtr::Reg(tbl.sized_get_or_insert_by_hash(hash, bdd, true)) } } @@ -80,14 +80,18 @@ impl<'a, const P: u128> SemanticDecisionNNFBuilder<'a, P> { } } - fn check_cached_hash_and_neg(&self, semantic_hash: FiniteField

) -> Option { + fn check_cached_hash_and_neg( + &'a self, + semantic_hash: FiniteField

, + bdd: &'a BddNode<'a>, + ) -> Option { // check regular hash let mut hasher = FxHasher::default(); semantic_hash.value().hash(&mut hasher); let hash = hasher.finish(); unsafe { let tbl = &mut *self.compute_table.as_ptr(); - if let Some(bdd) = tbl.get_by_hash(hash) { + if let Some(bdd) = tbl.sized_get_by_hash(hash, bdd) { return Some(BddPtr::Reg(bdd)); } } @@ -99,7 +103,7 @@ impl<'a, const P: u128> SemanticDecisionNNFBuilder<'a, P> { let hash = hasher.finish(); unsafe { let tbl = &mut *self.compute_table.as_ptr(); - if let Some(bdd) = tbl.get_by_hash(hash) { + if let Some(bdd) = tbl.sized_get_by_hash(hash, bdd) { return Some(BddPtr::Compl(bdd)); } } diff --git a/src/repr/bdd.rs b/src/repr/bdd.rs index a49fba97..37406d36 100644 --- a/src/repr/bdd.rs +++ b/src/repr/bdd.rs @@ -1,6 +1,7 @@ //! Binary decision diagram representation use crate::{ + backing_store::AbstractlySized, repr::ddnnf::{DDNNFPtr, DDNNF}, repr::model::PartialModel, repr::var_label::{Literal, VarLabel, VarSet}, @@ -1121,3 +1122,9 @@ impl<'a> Ord for BddNode<'a> { self.partial_cmp(other).unwrap() } } + +impl<'a> AbstractlySized for BddNode<'a> { + fn abstract_size(&self) -> usize { + BddPtr::Reg(self).count_nodes() + } +} From 5808bebcf926f47bccb92c69e455f4b291f98537 Mon Sep 17 00:00:00 2001 From: Matthew Wang Date: Wed, 19 Jul 2023 17:09:21 -0400 Subject: [PATCH 2/4] Slightly working post-hoc compression --- examples/semantic_top_down_experiment.rs | 44 ++++++++++++++++++++++++ src/backing_store/bump_table.rs | 9 +++-- src/builder/decision_nnf/semantic.rs | 19 ++++++++-- src/repr/bdd.rs | 6 ++-- 4 files changed, 68 insertions(+), 10 deletions(-) diff --git a/examples/semantic_top_down_experiment.rs b/examples/semantic_top_down_experiment.rs index 59affed4..21e7d8dc 100644 --- a/examples/semantic_top_down_experiment.rs +++ b/examples/semantic_top_down_experiment.rs @@ -73,6 +73,8 @@ fn compare_sem_and_std(cnf: &Cnf, order: &VarOrder) -> (usize, usize) { let sem_nodes = sem_dnnf.count_nodes(); let std_nodes = std_dnnf.count_nodes(); + println!("==="); + println!( "sem/std size ratio: {:.4}x ({} / {})", (sem_nodes as f64 / std_nodes as f64), @@ -92,9 +94,51 @@ fn compare_sem_and_std(cnf: &Cnf, order: &VarOrder) -> (usize, usize) { std_time ); + println!("===\nRebuilding..."); + let rebuilt = rebuild_and_compare(&sem_builder, &sem_dnnf); + let rebuilt_nodes: usize = rebuilt.count_nodes(); + println!("FINAL STATS"); + println!( + "rebuilt/sem size ratio: {:.4}x ({} / {})", + (rebuilt_nodes as f64 / sem_nodes as f64), + rebuilt_nodes, + sem_nodes + ); + + if diff_by_wmc(cnf.num_vars(), order, std_dnnf, rebuilt) > 0.0001 { + println!( + "error on rebuild {}\n std bdd: {}\nsem bdd: {}", + cnf, + std_dnnf.to_string_debug(), + rebuilt.to_string_debug() + ); + } + (sem_nodes, std_nodes) } +fn rebuild_and_compare<'a, const P: u128>( + builder: &'a SemanticDecisionNNFBuilder<'a, P>, + dnnf: &BddPtr<'a>, +) -> BddPtr<'a> { + println!("\nRebuilding..."); + let og_nodes = dnnf.count_nodes(); + let rebuilt = builder.rebuild(*dnnf); + let rebuilt_nodes = rebuilt.count_nodes(); + println!( + "rebuilt/sem size ratio: {:.4}x ({} / {})", + (rebuilt_nodes as f64 / og_nodes as f64), + rebuilt_nodes, + og_nodes + ); + + if og_nodes != rebuilt_nodes { + return rebuild_and_compare(builder, &rebuilt); + } + + rebuilt +} + struct RandomVarOrders { vars: u64, total: usize, diff --git a/src/backing_store/bump_table.rs b/src/backing_store/bump_table.rs index e3a83d49..51b03977 100644 --- a/src/backing_store/bump_table.rs +++ b/src/backing_store/bump_table.rs @@ -280,7 +280,7 @@ impl<'a, T: Eq + Hash + Clone + AbstractlySized> BackedRobinhoodTable<'a, T> { let diff = (elem.abstract_size() as i64) - (cur_itm.ptr.unwrap().abstract_size() as i64); if diff != 0 { - println!("size difference (g); delta: {}", diff); + println!("size difference (g/i); delta: {}", diff); } self.hits += 1; return found; @@ -325,13 +325,12 @@ impl<'a, T: Eq + Hash + Clone + AbstractlySized> BackedRobinhoodTable<'a, T> { let diff = (elem.abstract_size() as i64) - (cur_itm.ptr.unwrap().abstract_size() as i64); - if diff != 0 { - println!("size difference (g); delta: {}", diff); - } + if diff < 0 { - println!("smaller element found ... replacing"); + println!("smaller element found (diff: {}) ... replacing", diff); let ptr = self.alloc.alloc(elem); self.tbl[pos] = HashTableElement::new(ptr, hash, psl); + return Some(ptr); } return cur_itm.ptr; } diff --git a/src/builder/decision_nnf/semantic.rs b/src/builder/decision_nnf/semantic.rs index 07393f9c..3a9d2284 100644 --- a/src/builder/decision_nnf/semantic.rs +++ b/src/builder/decision_nnf/semantic.rs @@ -31,7 +31,7 @@ impl<'a, const P: u128> DecisionNNFBuilder<'a> for SemanticDecisionNNFBuilder<'a fn get_or_insert(&'a self, bdd: BddNode<'a>) -> BddPtr<'a> { let semantic_hash = bdd.semantic_hash(&self.order, &self.map); - if let Some(bdd) = self.check_cached_hash_and_neg(semantic_hash, bdd) { + if let Some(bdd) = self.check_cached_hash_and_neg(semantic_hash, bdd.clone()) { return bdd; } @@ -80,10 +80,23 @@ impl<'a, const P: u128> SemanticDecisionNNFBuilder<'a, P> { } } + pub fn rebuild(&'a self, bdd: BddPtr) -> BddPtr { + match bdd { + BddPtr::PtrTrue => BddPtr::PtrTrue, + BddPtr::PtrFalse => BddPtr::PtrFalse, + BddPtr::Reg(node) => { + let new_node = + BddNode::new(node.var, self.rebuild(node.low), self.rebuild(node.high)); + self.get_or_insert(new_node) + } + BddPtr::Compl(node) => self.rebuild(BddPtr::Reg(node)).neg(), + } + } + fn check_cached_hash_and_neg( &'a self, semantic_hash: FiniteField

, - bdd: &'a BddNode<'a>, + bdd: BddNode<'a>, ) -> Option { // check regular hash let mut hasher = FxHasher::default(); @@ -91,7 +104,7 @@ impl<'a, const P: u128> SemanticDecisionNNFBuilder<'a, P> { let hash = hasher.finish(); unsafe { let tbl = &mut *self.compute_table.as_ptr(); - if let Some(bdd) = tbl.sized_get_by_hash(hash, bdd) { + if let Some(bdd) = tbl.sized_get_by_hash(hash, bdd.clone()) { return Some(BddPtr::Reg(bdd)); } } diff --git a/src/repr/bdd.rs b/src/repr/bdd.rs index 37406d36..82ea2d0e 100644 --- a/src/repr/bdd.rs +++ b/src/repr/bdd.rs @@ -326,14 +326,15 @@ impl<'a> BddPtr<'a> { } /// Gets the scratch value stored in `&self` - /// - /// Panics if not node. pub fn get_scratch(&self) -> Option { match self { Compl(n) | Reg(n) => { if self.is_scratch_cleared() { return None; } + if n.data.borrow().is_none() { + return None; + } // println!("dereferencing {:?}", n.data.as_ptr()); n.data .borrow() @@ -369,6 +370,7 @@ impl<'a> BddPtr<'a> { // return true; match self { Compl(n) | Reg(n) => n.data.borrow().is_none(), + // && n.low.is_scratch_cleared() && n.high.is_scratch_cleared(), PtrTrue => true, PtrFalse => true, } From 57e89f1cf209da4d3d4154d76a2a192d7948f7d3 Mon Sep 17 00:00:00 2001 From: Matthew Wang Date: Thu, 20 Jul 2023 11:42:59 -0400 Subject: [PATCH 3/4] Hm, this still doesn't work --- examples/semantic_top_down_experiment.rs | 25 ++++++++++----------- src/backing_store/bump_table.rs | 11 +++++++--- src/builder/decision_nnf/semantic.rs | 28 +++++++++++++++++++++++- 3 files changed, 47 insertions(+), 17 deletions(-) diff --git a/examples/semantic_top_down_experiment.rs b/examples/semantic_top_down_experiment.rs index 21e7d8dc..b0720c59 100644 --- a/examples/semantic_top_down_experiment.rs +++ b/examples/semantic_top_down_experiment.rs @@ -73,8 +73,11 @@ fn compare_sem_and_std(cnf: &Cnf, order: &VarOrder) -> (usize, usize) { let sem_nodes = sem_dnnf.count_nodes(); let std_nodes = std_dnnf.count_nodes(); - println!("==="); + println!("===\nRebuilding sem..."); + let rebuilt_sem = rebuild_and_compare(&sem_builder, &sem_dnnf); + let rebuilt_sem_nodes: usize = rebuilt_sem.count_nodes(); + println!("\n\n===FINAL STATS==="); println!( "sem/std size ratio: {:.4}x ({} / {})", (sem_nodes as f64 / std_nodes as f64), @@ -93,28 +96,24 @@ fn compare_sem_and_std(cnf: &Cnf, order: &VarOrder) -> (usize, usize) { sem_time, std_time ); - - println!("===\nRebuilding..."); - let rebuilt = rebuild_and_compare(&sem_builder, &sem_dnnf); - let rebuilt_nodes: usize = rebuilt.count_nodes(); - println!("FINAL STATS"); + println!("==="); println!( - "rebuilt/sem size ratio: {:.4}x ({} / {})", - (rebuilt_nodes as f64 / sem_nodes as f64), - rebuilt_nodes, + "sem rebuilt/sem size ratio: {:.4}x ({} / {})", + (rebuilt_sem_nodes as f64 / sem_nodes as f64), + rebuilt_sem_nodes, sem_nodes ); - if diff_by_wmc(cnf.num_vars(), order, std_dnnf, rebuilt) > 0.0001 { + if diff_by_wmc(cnf.num_vars(), order, std_dnnf, rebuilt_sem) > 0.0001 { println!( - "error on rebuild {}\n std bdd: {}\nsem bdd: {}", + "error on sem rebuild {}\n std bdd: {}\nsem bdd: {}", cnf, std_dnnf.to_string_debug(), - rebuilt.to_string_debug() + rebuilt_sem.to_string_debug() ); } - (sem_nodes, std_nodes) + (rebuilt_sem_nodes, std_nodes) } fn rebuild_and_compare<'a, const P: u128>( diff --git a/src/backing_store/bump_table.rs b/src/backing_store/bump_table.rs index 51b03977..94dd30f7 100644 --- a/src/backing_store/bump_table.rs +++ b/src/backing_store/bump_table.rs @@ -323,11 +323,16 @@ impl<'a, T: Eq + Hash + Clone + AbstractlySized> BackedRobinhoodTable<'a, T> { if hash == cur_itm.hash { self.hits += 1; - let diff = (elem.abstract_size() as i64) - - (cur_itm.ptr.unwrap().abstract_size() as i64); + let e = elem.abstract_size() as i64; + let c = cur_itm.ptr.unwrap().abstract_size() as i64; + + let diff = e - c; if diff < 0 { - println!("smaller element found (diff: {}) ... replacing", diff); + println!( + "replacing table elem (diff: {}; new: {}; old {})", + diff, e, c + ); let ptr = self.alloc.alloc(elem); self.tbl[pos] = HashTableElement::new(ptr, hash, psl); return Some(ptr); diff --git a/src/builder/decision_nnf/semantic.rs b/src/builder/decision_nnf/semantic.rs index 3a9d2284..af07dc40 100644 --- a/src/builder/decision_nnf/semantic.rs +++ b/src/builder/decision_nnf/semantic.rs @@ -41,6 +41,8 @@ impl<'a, const P: u128> DecisionNNFBuilder<'a> for SemanticDecisionNNFBuilder<'a .value() .hash(&mut hasher); hasher.finish() + + // bdd.semantic_hash(&self.order, &self.map).value() as u64 }; unsafe { @@ -80,11 +82,31 @@ impl<'a, const P: u128> SemanticDecisionNNFBuilder<'a, P> { } } - pub fn rebuild(&'a self, bdd: BddPtr) -> BddPtr { + pub fn rebuild(&'a self, bdd: BddPtr<'a>) -> BddPtr<'a> { match bdd { BddPtr::PtrTrue => BddPtr::PtrTrue, BddPtr::PtrFalse => BddPtr::PtrFalse, BddPtr::Reg(node) => { + // let semantic_hash = bdd.semantic_hash(&self.order, &self.map); + + // if let Some(bdd) = self.check_cached_hash_and_neg(semantic_hash, BddNode::new(node.var, node.low, node.high)) { + // match bdd { + // BddPtr::PtrTrue => return BddPtr::PtrTrue, + // BddPtr::PtrFalse => return BddPtr::PtrFalse, + // BddPtr::Reg(node) => { + // let new_node = + // BddNode::new(node.var, self.rebuild(node.low), self.rebuild(node.high)); + // return self.get_or_insert(new_node) + // } + // BddPtr::Compl(node) => { + // let new_node = + // BddNode::new(node.var, self.rebuild(node.low), self.rebuild(node.high)); + // return self.get_or_insert(new_node).neg() + // } + // } + // } + // panic!("unreachable"); + let new_node = BddNode::new(node.var, self.rebuild(node.low), self.rebuild(node.high)); self.get_or_insert(new_node) @@ -102,6 +124,8 @@ impl<'a, const P: u128> SemanticDecisionNNFBuilder<'a, P> { let mut hasher = FxHasher::default(); semantic_hash.value().hash(&mut hasher); let hash = hasher.finish(); + // let hash = semantic_hash.value() as u64; + unsafe { let tbl = &mut *self.compute_table.as_ptr(); if let Some(bdd) = tbl.sized_get_by_hash(hash, bdd.clone()) { @@ -114,6 +138,8 @@ impl<'a, const P: u128> SemanticDecisionNNFBuilder<'a, P> { let mut hasher = FxHasher::default(); semantic_hash.value().hash(&mut hasher); let hash = hasher.finish(); + // let hash = semantic_hash.value() as u64; + unsafe { let tbl = &mut *self.compute_table.as_ptr(); if let Some(bdd) = tbl.sized_get_by_hash(hash, bdd) { From 2787e31b91521dc24686b6b07f16e45fa7964694 Mon Sep 17 00:00:00 2001 From: Matthew Wang Date: Sat, 22 Jul 2023 16:44:03 -0400 Subject: [PATCH 4/4] Cleanup --- src/builder/decision_nnf/semantic.rs | 34 ++++------------------------ src/repr/bdd.rs | 1 - 2 files changed, 5 insertions(+), 30 deletions(-) diff --git a/src/builder/decision_nnf/semantic.rs b/src/builder/decision_nnf/semantic.rs index d8c40bcd..0ef14886 100644 --- a/src/builder/decision_nnf/semantic.rs +++ b/src/builder/decision_nnf/semantic.rs @@ -41,8 +41,6 @@ impl<'a, const P: u128> DecisionNNFBuilder<'a> for SemanticDecisionNNFBuilder<'a .value() .hash(&mut hasher); hasher.finish() - - // bdd.semantic_hash(&self.order, &self.map).value() as u64 }; unsafe { @@ -86,31 +84,11 @@ impl<'a, const P: u128> SemanticDecisionNNFBuilder<'a, P> { match bdd { BddPtr::PtrTrue => BddPtr::PtrTrue, BddPtr::PtrFalse => BddPtr::PtrFalse, - BddPtr::Reg(node) => { - // let semantic_hash = bdd.semantic_hash(&self.order, &self.map); - - // if let Some(bdd) = self.check_cached_hash_and_neg(semantic_hash, BddNode::new(node.var, node.low, node.high)) { - // match bdd { - // BddPtr::PtrTrue => return BddPtr::PtrTrue, - // BddPtr::PtrFalse => return BddPtr::PtrFalse, - // BddPtr::Reg(node) => { - // let new_node = - // BddNode::new(node.var, self.rebuild(node.low), self.rebuild(node.high)); - // return self.get_or_insert(new_node) - // } - // BddPtr::Compl(node) => { - // let new_node = - // BddNode::new(node.var, self.rebuild(node.low), self.rebuild(node.high)); - // return self.get_or_insert(new_node).neg() - // } - // } - // } - // panic!("unreachable"); - - let new_node = - BddNode::new(node.var, self.rebuild(node.low), self.rebuild(node.high)); - self.get_or_insert(new_node) - } + BddPtr::Reg(node) => self.get_or_insert(BddNode::new( + node.var, + self.rebuild(node.low), + self.rebuild(node.high), + )), BddPtr::Compl(node) => self.rebuild(BddPtr::Reg(node)).neg(), } } @@ -124,7 +102,6 @@ impl<'a, const P: u128> SemanticDecisionNNFBuilder<'a, P> { let mut hasher = FxHasher::default(); semantic_hash.value().hash(&mut hasher); let hash = hasher.finish(); - // let hash = semantic_hash.value() as u64; unsafe { let tbl = &mut *self.compute_table.as_ptr(); @@ -138,7 +115,6 @@ impl<'a, const P: u128> SemanticDecisionNNFBuilder<'a, P> { let mut hasher = FxHasher::default(); semantic_hash.value().hash(&mut hasher); let hash = hasher.finish(); - // let hash = semantic_hash.value() as u64; unsafe { let tbl = &mut *self.compute_table.as_ptr(); diff --git a/src/repr/bdd.rs b/src/repr/bdd.rs index 3aba0159..92dc2768 100644 --- a/src/repr/bdd.rs +++ b/src/repr/bdd.rs @@ -370,7 +370,6 @@ impl<'a> BddPtr<'a> { // return true; match self { Compl(n) | Reg(n) => n.data.borrow().is_none(), - // && n.low.is_scratch_cleared() && n.high.is_scratch_cleared(), PtrTrue => true, PtrFalse => true, }