Skip to content

Commit

Permalink
Add protection against using non-rebuilt egraphs
Browse files Browse the repository at this point in the history
  • Loading branch information
mwillsey committed Sep 27, 2021
1 parent afbd482 commit b4257e8
Show file tree
Hide file tree
Showing 2 changed files with 16 additions and 0 deletions.
15 changes: 15 additions & 0 deletions src/egraph.rs
Original file line number Diff line number Diff line change
Expand Up @@ -72,6 +72,13 @@ pub struct EGraph<L: Language, N: Analysis<L>> {
#[cfg_attr(feature = "serde-1", serde(skip))]
#[cfg_attr(feature = "serde-1", serde(default = "default_classes_by_op"))]
pub(crate) classes_by_op: HashMap<std::mem::Discriminant<L>, HashSet<Id>>,
/// Whether or not reading operation are allowed on this e-graph.
/// Mutating operations will set this to `false`, and
/// [`EGraph::rebuild`] will set it to true.
/// Reading operations require this to be `true`.
/// Only manually set it if you know what you're doing.
#[cfg_attr(feature = "serde-1", serde(skip))]
pub clean: bool,
}

#[cfg(feature = "serde-1")]
Expand Down Expand Up @@ -103,6 +110,7 @@ impl<L: Language, N: Analysis<L>> EGraph<L, N> {
to_union: Default::default(),
classes: Default::default(),
unionfind: Default::default(),
clean: false,
explain: None,
pending: Default::default(),
memo: Default::default(),
Expand Down Expand Up @@ -408,6 +416,8 @@ impl<L: Language, N: Analysis<L>> EGraph<L, N> {
assert!(self.memo.insert(enode, id).is_none());

N::modify(self, id);

self.clean = false;
id
})
}
Expand Down Expand Up @@ -470,6 +480,7 @@ impl<L: Language, N: Analysis<L>> EGraph<L, N> {
subst: &Subst,
rule_name: impl Into<Symbol>,
) -> bool {
self.clean = false;
if let Some(explain) = &mut self.explain {
if self.unionfind.find_mut(id1) == self.unionfind.find_mut(id2) {
false
Expand Down Expand Up @@ -504,6 +515,7 @@ impl<L: Language, N: Analysis<L>> EGraph<L, N> {
/// You must call [`rebuild`](EGraph::rebuild) to observe any effect.
///
pub fn union(&mut self, id1: Id, id2: Id) -> bool {
self.clean = false;
if self.explain.is_some() {
panic!("Use union_instantiations when explanation mode is enabled.");
}
Expand Down Expand Up @@ -757,6 +769,8 @@ impl<L: Language, N: Analysis<L>> EGraph<L, N> {
/// invariants before any query operations, otherwise the results
/// may be stale or incorrect.
///
/// This will set [`EGraph::clean`] to `true`.
///
/// # Example
/// ```
/// use egg::{*, SymbolLang as S};
Expand Down Expand Up @@ -808,6 +822,7 @@ impl<L: Language, N: Analysis<L>> EGraph<L, N> {
);

debug_assert!(self.check_memo());
self.clean = true;
n_unions
}

Expand Down
1 change: 1 addition & 0 deletions src/machine.rs
Original file line number Diff line number Diff line change
Expand Up @@ -307,6 +307,7 @@ impl<L: Language> Program<L> {
{
let mut machine = Machine::default();

assert!(egraph.clean, "Tried to search a dirty e-graph!");
assert_eq!(machine.reg.len(), 0);
for expr in &self.ground_terms {
if let Some(id) = egraph.lookup_expr(&expr.clone()) {
Expand Down

0 comments on commit b4257e8

Please sign in to comment.