Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Remove Existence Explanations #333

Open
wants to merge 2 commits into
base: main
Choose a base branch
from
Open

Remove Existence Explanations #333

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
121d98a
remove existence explanations
oflatt Aug 20, 2024
c318a94
Merge branch 'main' into oflatt-remove-existence-proofs
oflatt Aug 31, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions CHANGELOG.md
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,7 @@
# Changes

## [Unreleased] - ReleaseDate
- Removed existence explanations from egg (the `explain_existance` function). This feature was buggy and not well supported. Supporting it fully required many changes, and it is incompatible with analysis. See #332 for more details.
- Change the API of `make` to have mutable access to the e-graph for some [advanced uses cases](https://github.com/egraphs-good/egg/pull/277).
- Fix an e-matching performance regression introduced in [this commit](https://github.com/egraphs-good/egg/commit/ae8af8815231e4aba1b78962f8c07ce837ee1c0e#diff-1d06da761111802c793c6e5ca704bfa0d6336d0becf87fddff02d81548a838ab).
- Use `quanta` instead of `instant` crate to provide timing information. This can provide a huge speedup if you have lots of rules, since it avoids some syscalls.
Expand Down
89 changes: 10 additions & 79 deletions src/egraph.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -493,43 +493,6 @@ impl<L: Language, N: Analysis<L>> EGraph<L, N> {
}
}

/// When explanations are enabled, this function
/// produces an [`Explanation`] describing how the given expression came
/// to be in the egraph.
///
/// The [`Explanation`] begins with some expression that was added directly
/// into the egraph and ends with the given `expr`.
/// Note that this function can be called again to explain any intermediate terms
/// used in the output [`Explanation`].
pub fn explain_existance(&mut self, expr: &RecExpr<L>) -> Explanation<L> {
let id = self.add_expr_uncanonical(expr);
self.explain_existance_id(id)
}

/// Equivalent to calling [`explain_existance`](EGraph::explain_existance)`(`[`id_to_expr`](EGraph::id_to_expr)`(id))`
/// but more efficient
fn explain_existance_id(&mut self, id: Id) -> Explanation<L> {
if let Some(explain) = &mut self.explain {
explain.with_nodes(&self.nodes).explain_existance(id)
} else {
panic!("Use runner.with_explanations_enabled() or egraph.with_explanations_enabled() before running to get explanations.")
}
}

/// Return an [`Explanation`] for why a pattern appears in the egraph.
pub fn explain_existance_pattern(
&mut self,
pattern: &PatternAst<L>,
subst: &Subst,
) -> Explanation<L> {
let id = self.add_instantiation_noncanonical(pattern, subst);
if let Some(explain) = &mut self.explain {
explain.with_nodes(&self.nodes).explain_existance(id)
} else {
panic!("Use runner.with_explanations_enabled() or egraph.with_explanations_enabled() before running to get explanations.")
}
}

/// Get an explanation for why an expression matches a pattern.
pub fn explain_matches(
&mut self,
Expand Down Expand Up @@ -858,14 +821,6 @@ impl<L: Language, N: Analysis<L>> EGraph<L, N> {
} else {
new_node_q.push(false);
}
if let Some(explain) = &mut self.explain {
node.for_each(|child| {
// Set the existance reason for new nodes to their parent node.
if new_node_q[usize::from(child)] {
explain.set_existance_reason(new_ids[usize::from(child)], next_id);
}
});
}
new_ids.push(next_id);
}
*new_ids.last().unwrap()
Expand Down Expand Up @@ -905,13 +860,6 @@ impl<L: Language, N: Analysis<L>> EGraph<L, N> {
new_node_q.push(false);
}

if let Some(explain) = &mut self.explain {
node.for_each(|child| {
if new_node_q[usize::from(child)] {
explain.set_existance_reason(new_ids[usize::from(child)], next_id);
}
});
}
new_ids.push(next_id);
}
}
Expand Down Expand Up @@ -1046,11 +994,11 @@ impl<L: Language, N: Analysis<L>> EGraph<L, N> {
*existing_explain
} else {
let new_id = self.unionfind.make_set();
explain.add(original.clone(), new_id, new_id);
explain.add(original.clone(), new_id);
debug_assert_eq!(Id::from(self.nodes.len()), new_id);
self.nodes.push(original);
self.unionfind.union(id, new_id);
explain.union(existing_id, new_id, Justification::Congruence, true);
explain.union(existing_id, new_id, Justification::Congruence);
new_id
}
} else {
Expand All @@ -1059,7 +1007,7 @@ impl<L: Language, N: Analysis<L>> EGraph<L, N> {
} else {
let id = self.make_new_eclass(enode, original.clone());
if let Some(explain) = self.explain.as_mut() {
explain.add(original, id, id);
explain.add(original, id);
}

// now that we updated explanations, run the analysis for the new eclass
Expand Down Expand Up @@ -1139,16 +1087,9 @@ impl<L: Language, N: Analysis<L>> EGraph<L, N> {
rule_name: impl Into<Symbol>,
) -> (Id, bool) {
let id1 = self.add_instantiation_noncanonical(from_pat, subst);
let size_before = self.unionfind.size();
let id2 = self.add_instantiation_noncanonical(to_pat, subst);
let rhs_new = self.unionfind.size() > size_before;

let did_union = self.perform_union(
id1,
id2,
Some(Justification::Rule(rule_name.into())),
rhs_new,
);
let did_union = self.perform_union(id1, id2, Some(Justification::Rule(rule_name.into())));
(self.find(id1), did_union)
}

Expand All @@ -1158,7 +1099,7 @@ impl<L: Language, N: Analysis<L>> EGraph<L, N> {
/// `Id`s returned by functions like [`add_uncanonical`](EGraph::add_uncanonical) is important
/// to control explanations
pub fn union_trusted(&mut self, from: Id, to: Id, reason: impl Into<Symbol>) -> bool {
self.perform_union(from, to, Some(Justification::Rule(reason.into())), false)
self.perform_union(from, to, Some(Justification::Rule(reason.into())))
}

/// Unions two eclasses given their ids.
Expand All @@ -1181,17 +1122,11 @@ impl<L: Language, N: Analysis<L>> EGraph<L, N> {
let caller = std::panic::Location::caller();
self.union_trusted(id1, id2, caller.to_string())
} else {
self.perform_union(id1, id2, None, false)
self.perform_union(id1, id2, None)
}
}

fn perform_union(
&mut self,
enode_id1: Id,
enode_id2: Id,
rule: Option<Justification>,
any_new_rhs: bool,
) -> bool {
fn perform_union(&mut self, enode_id1: Id, enode_id2: Id, rule: Option<Justification>) -> bool {
N::pre_union(self, enode_id1, enode_id2, &rule);

self.clean = false;
Expand All @@ -1213,7 +1148,7 @@ impl<L: Language, N: Analysis<L>> EGraph<L, N> {
}

if let Some(explain) = &mut self.explain {
explain.union(enode_id1, enode_id2, rule.unwrap(), any_new_rhs);
explain.union(enode_id1, enode_id2, rule.unwrap());
}

// make id1 the new root
Expand Down Expand Up @@ -1388,12 +1323,8 @@ impl<L: Language, N: Analysis<L>> EGraph<L, N> {
let mut node = self.nodes[usize::from(class)].clone();
node.update_children(|id| self.find_mut(id));
if let Some(memo_class) = self.memo.insert(node, class) {
let did_something = self.perform_union(
memo_class,
class,
Some(Justification::Congruence),
false,
);
let did_something =
self.perform_union(memo_class, class, Some(Justification::Congruence));
n_unions += did_something as usize;
}
}
Expand Down
135 changes: 2 additions & 133 deletions src/explain.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -46,12 +46,6 @@ struct ExplainNode {
// neighbors includes parent connections
neighbors: Vec<Connection>,
parent_connection: Connection,
// it was inserted because of:
// 1) it's parent is inserted (points to parent enode)
// 2) a rewrite instantiated it (points to adjacent enode)
// 3) it was inserted directly (points to itself)
// if 1 is true but it's also adjacent (2) then either works and it picks 2
existance_node: Id,
}

#[derive(Debug, Clone)]
Expand Down Expand Up @@ -916,11 +910,7 @@ impl<L: Language> Explain<L> {
}
}

pub(crate) fn set_existance_reason(&mut self, node: Id, existance_node: Id) {
self.explainfind[usize::from(node)].existance_node = existance_node;
}

pub(crate) fn add(&mut self, node: L, set: Id, existance_node: Id) -> Id {
pub(crate) fn add(&mut self, node: L, set: Id) -> Id {
assert_eq!(self.explainfind.len(), usize::from(set));
self.uncanon_memo.insert(node, set);
self.explainfind.push(ExplainNode {
Expand All @@ -931,7 +921,6 @@ impl<L: Language> Explain<L> {
next: set,
current: set,
},
existance_node,
});
set
}
Expand Down Expand Up @@ -988,19 +977,10 @@ impl<L: Language> Explain<L> {
.insert((node2, node1), (BigUint::one(), node1));
}

pub(crate) fn union(
&mut self,
node1: Id,
node2: Id,
justification: Justification,
new_rhs: bool,
) {
pub(crate) fn union(&mut self, node1: Id, node2: Id, justification: Justification) {
if let Justification::Congruence = justification {
// assert!(self.node(node1).matches(self.node(node2)));
}
if new_rhs {
self.set_existance_reason(node2, node1)
}

self.make_leader(node1);
self.explainfind[usize::from(node1)].parent_connection.next = node2;
Expand Down Expand Up @@ -1105,21 +1085,6 @@ impl<'x, L: Language> ExplainNodes<'x, L> {
for i in 0..self.explainfind.len() {
let explain_node = &self.explainfind[i];

// check that explanation reasons never form a cycle
let mut existance = i;
let mut seen_existance: HashSet<usize> = Default::default();
loop {
seen_existance.insert(existance);
let next = usize::from(self.explainfind[existance].existance_node);
if existance == next {
break;
}
existance = next;
if seen_existance.contains(&existance) {
panic!("Cycle in existance!");
}
}

if explain_node.parent_connection.next != Id::from(i) {
let mut current_explanation = self.node_to_flat_explanation(Id::from(i));
let mut next_explanation =
Expand Down Expand Up @@ -1161,17 +1126,6 @@ impl<'x, L: Language> ExplainNodes<'x, L> {
Explanation::new(self.explain_enodes(left, right, &mut cache, &mut enode_cache, false))
}

pub(crate) fn explain_existance(&mut self, left: Id) -> Explanation<L> {
let mut cache = Default::default();
let mut enode_cache = Default::default();
Explanation::new(self.explain_enode_existance(
left,
self.node_to_explanation(left, &mut enode_cache),
&mut cache,
&mut enode_cache,
))
}

fn common_ancestor(&self, mut left: Id, mut right: Id) -> Id {
let mut seen_left: HashSet<Id> = Default::default();
let mut seen_right: HashSet<Id> = Default::default();
Expand Down Expand Up @@ -1257,62 +1211,6 @@ impl<'x, L: Language> ExplainNodes<'x, L> {
(left_connections, right_connections)
}

fn explain_enode_existance(
&self,
node: Id,
rest_of_proof: Rc<TreeTerm<L>>,
cache: &mut ExplainCache<L>,
enode_cache: &mut NodeExplanationCache<L>,
) -> TreeExplanation<L> {
let graphnode = &self.explainfind[usize::from(node)];
let existance = graphnode.existance_node;
let existance_node = &self.explainfind[usize::from(existance)];
// case 1)
if existance == node {
return vec![self.node_to_explanation(node, enode_cache), rest_of_proof];
}

// case 2)
if graphnode.parent_connection.next == existance
|| existance_node.parent_connection.next == node
{
let mut connection = if graphnode.parent_connection.next == existance {
graphnode.parent_connection.clone()
} else {
existance_node.parent_connection.clone()
};

if graphnode.parent_connection.next == existance {
connection.is_rewrite_forward = !connection.is_rewrite_forward;
std::mem::swap(&mut connection.next, &mut connection.current);
}

let adj = self.explain_adjacent(connection, cache, enode_cache, false);
let mut exp = self.explain_enode_existance(existance, adj, cache, enode_cache);
exp.push(rest_of_proof);
return exp;
}

// case 3)
let mut new_rest_of_proof = (*self.node_to_explanation(existance, enode_cache)).clone();
let mut index_of_child = 0;
let mut found = false;
self.node(existance).for_each(|child| {
if found {
return;
}
if child == node {
found = true;
} else {
index_of_child += 1;
}
});
assert!(found);
new_rest_of_proof.child_proofs[index_of_child].push(rest_of_proof);

self.explain_enode_existance(existance, Rc::new(new_rest_of_proof), cache, enode_cache)
}

fn explain_enodes(
&self,
left: Id,
Expand Down Expand Up @@ -2050,35 +1948,6 @@ mod tests {

egraph.dot().to_dot("target/foo.dot").unwrap();
}

#[test]
fn simple_explain_exists() {
//! Same as previous test, but now I want to make a rewrite add some term and see it exists in
//! more then one step
use crate::SymbolLang;
init_logger();

let rws: Vec<Rewrite<SymbolLang, ()>> =
[rewrite!("makeb"; "a" => "b"), rewrite!("makec"; "b" => "c")].to_vec();
let mut egraph = Runner::default()
.with_explanations_enabled()
.without_explanation_length_optimization()
.with_expr(&"a".parse().unwrap())
.run(&rws)
.egraph;
egraph.rebuild();
let _a: Symbol = "a".parse().unwrap();
let _b: Symbol = "b".parse().unwrap();
let _c: Symbol = "c".parse().unwrap();
let mut exp = egraph.explain_existance(&"c".parse().unwrap());
println!("{:?}", exp.make_flat_explanation());
assert_eq!(
exp.make_flat_explanation().len(),
3,
"Expected 3 steps, got {:?}",
exp.make_flat_explanation()
);
}
}

#[test]
Expand Down
14 changes: 0 additions & 14 deletions src/run.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -489,20 +489,6 @@ where
self.egraph.explain_equivalence(left, right)
}

/// Calls [`EGraph::explain_existance`](EGraph::explain_existance()).
pub fn explain_existance(&mut self, expr: &RecExpr<L>) -> Explanation<L> {
self.egraph.explain_existance(expr)
}

/// Calls [EGraph::explain_existance_pattern`](EGraph::explain_existance_pattern()).
pub fn explain_existance_pattern(
&mut self,
pattern: &PatternAst<L>,
subst: &Subst,
) -> Explanation<L> {
self.egraph.explain_existance_pattern(pattern, subst)
}

/// Get an explanation for why an expression matches a pattern.
pub fn explain_matches(
&mut self,
Expand Down
Loading