Skip to content

Commit 3982507

Browse files
added the type squashing optimization
1 parent 1760197 commit 3982507

File tree

2 files changed

+14
-11
lines changed

2 files changed

+14
-11
lines changed

src/distance/graph.rs

Lines changed: 11 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -388,9 +388,10 @@ impl<L: Label> EGraph<L> {
388388
costs: &C,
389389
progress_bar: ProgressBar,
390390
) -> Option<(TreeNode<L>, usize)> {
391-
let ref_size = reference.size();
392-
let ref_euler = EulerString::new(reference);
393-
let ref_pp = PreprocessedTree::new(reference);
391+
let ref_squashed = reference.to_owned().squash_types();
392+
let ref_size = ref_squashed.size();
393+
let ref_euler = EulerString::new(&ref_squashed);
394+
let ref_pp = PreprocessedTree::new(&ref_squashed);
394395
let running_best = AtomicUsize::new(usize::MAX);
395396

396397
self.choice_iter(max_revisits)
@@ -420,10 +421,10 @@ impl<L: Label> EGraph<L> {
420421
costs: &C,
421422
quiet: bool,
422423
) -> (Option<(TreeNode<L>, usize)>, ExtractionStats) {
423-
let ref_size = reference.size();
424-
let ref_euler = EulerString::new(reference);
425-
let ref_pp = PreprocessedTree::new(reference);
426-
424+
let ref_squashed = reference.to_owned().squash_types();
425+
let ref_size = ref_squashed.size();
426+
let ref_euler = EulerString::new(&ref_squashed);
427+
let ref_pp = PreprocessedTree::new(&ref_squashed);
427428
let running_best = AtomicUsize::new(usize::MAX);
428429

429430
let progress = self.progress_bar(max_revisits, quiet);
@@ -465,7 +466,9 @@ impl<L: Label> EGraph<L> {
465466
running_best: &AtomicUsize,
466467
costs: &C,
467468
) -> (Option<(TreeNode<L>, usize)>, ExtractionStats) {
468-
let tree = self.tree_from_choices(self.root(), choices, true);
469+
let tree = self
470+
.tree_from_choices(self.root(), choices, true)
471+
.squash_types();
469472
let best = running_best.load(Ordering::Relaxed);
470473

471474
// Fast pruning: size difference is a lower bound on edit distance

src/distance/tree.rs

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -124,18 +124,18 @@ impl<L: Label> TreeNode<L> {
124124
/// trades height and node number vs child number
125125
#[allow(clippy::missing_panics_doc)]
126126
#[must_use]
127-
pub fn flattify_type(mut self) -> Self {
127+
pub fn squash_types(mut self) -> Self {
128128
if self.label().is_type_of() {
129129
let mut child_iter = self.children.into_iter();
130-
let mut expr_tree = child_iter.next().unwrap().flattify_type();
130+
let mut expr_tree = child_iter.next().unwrap().squash_types();
131131
let type_tree = child_iter.next().unwrap();
132132
expr_tree.children.push(type_tree);
133133
expr_tree
134134
} else {
135135
self.children = self
136136
.children
137137
.into_iter()
138-
.map(|c| c.flattify_type())
138+
.map(|c| c.squash_types())
139139
.collect();
140140
self
141141
}

0 commit comments

Comments
 (0)