From 2f106a44421dd82e55b57b2f1b15a9dbc4f145ba Mon Sep 17 00:00:00 2001 From: Thomas Koehler Date: Tue, 2 May 2023 20:30:40 +0200 Subject: [PATCH] Use a unique queue for pending analyses (#253) * Use a unique queue for pending analyses * implement (De)Serialize for UniqueQueue * fix serialize nit test * cargo fmt --------- Co-authored-by: thomas --- src/egraph.rs | 2 +- src/util.rs | 61 +++++++++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 62 insertions(+), 1 deletion(-) diff --git a/src/egraph.rs b/src/egraph.rs index 3ce31e26..22956348 100644 --- a/src/egraph.rs +++ b/src/egraph.rs @@ -65,7 +65,7 @@ pub struct EGraph> { /// Nodes which need to be processed for rebuilding. The `Id` is the `Id` of the enode, /// not the canonical id of the eclass. pending: Vec<(L, Id)>, - analysis_pending: IndexSet<(L, Id)>, + analysis_pending: UniqueQueue<(L, Id)>, #[cfg_attr( feature = "serde-1", serde(bound( diff --git a/src/util.rs b/src/util.rs index b1ffc880..0e9051ee 100644 --- a/src/util.rs +++ b/src/util.rs @@ -3,6 +3,9 @@ use symbolic_expressions::Sexp; use fmt::{Debug, Display, Formatter}; +#[cfg(feature = "serde-1")] +use ::serde::{Deserialize, Serialize}; + #[allow(unused_imports)] use crate::*; @@ -111,3 +114,61 @@ impl Debug for DisplayAsDebug { Display::fmt(&self.0, f) } } + +/** A data structure to maintain a queue of unique elements. + +Notably, insert/pop operations have O(1) expected amortized runtime complexity. +*/ +#[derive(Clone)] +#[cfg_attr(feature = "serde-1", derive(Serialize, Deserialize))] +pub(crate) struct UniqueQueue +where + T: Eq + std::hash::Hash + Clone, +{ + set: hashbrown::HashSet, + queue: std::collections::VecDeque, +} + +impl Default for UniqueQueue +where + T: Eq + std::hash::Hash + Clone, +{ + fn default() -> Self { + UniqueQueue { + set: hashbrown::HashSet::default(), + queue: std::collections::VecDeque::new(), + } + } +} + +impl UniqueQueue +where + T: Eq + std::hash::Hash + Clone, +{ + pub fn insert(&mut self, t: T) { + if self.set.insert(t.clone()) { + self.queue.push_back(t); + } + } + + pub fn extend(&mut self, iter: I) + where + I: IntoIterator, + { + for t in iter.into_iter() { + self.insert(t); + } + } + + pub fn pop(&mut self) -> Option { + let res = self.queue.pop_front(); + res.as_ref().map(|t| self.set.remove(t)); + res + } + + pub fn is_empty(&self) -> bool { + let r = self.queue.is_empty(); + debug_assert_eq!(r, self.set.is_empty()); + r + } +}