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.

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

Push Pop API #300

Draft
wants to merge 21 commits into
base: main
Choose a base branch
from
Draft
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
21 commits
Select commit Hold shift + click to select a range
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
9 changes: 6 additions & 3 deletions Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -2,23 +2,24 @@
authors = ["Max Willsey <[email protected]>"]
categories = ["data-structures"]
description = "An implementation of egraphs"
edition = "2018"
edition = "2021"
keywords = ["e-graphs"]
license = "MIT"
name = "egg"
readme = "README.md"
repository = "https://github.com/egraphs-good/egg"
version = "0.9.5"
rust-version = "1.63.0"

[dependencies]
env_logger = { version = "0.9.0", default-features = false }
fxhash = "0.2.1"
hashbrown = "0.12.1"
hashbrown = { version = "0.14.3", default-features = false, features = ["inline-more"] }
indexmap = "1.8.1"
instant = "0.1.12"
log = "0.4.17"
smallvec = { version = "1.8.0", features = ["union", "const_generics"] }
symbol_table = { version = "0.2.0", features = ["global"] }
symbol_table = { version = "0.3.0", features = ["global"] }
symbolic_expressions = "5.0.3"
thiserror = "1.0.31"

Expand Down Expand Up @@ -49,9 +50,11 @@ serde-1 = [
"vectorize",
]
wasm-bindgen = ["instant/wasm-bindgen"]
push-pop-alt = []

# private features for testing
test-explanations = []
test-push-pop = ["deterministic"]

[package.metadata.docs.rs]
all-features = true
Expand Down
2 changes: 2 additions & 0 deletions Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -6,6 +6,8 @@ test:
cargo test --release --features=lp
# don't run examples in proof-production mode
cargo test --release --features "test-explanations"
cargo test --release --features "test-push-pop" --features "test-explanations"
cargo test --release --features "test-push-pop" --features "push-pop-alt"


.PHONY: nits
Expand Down
2 changes: 1 addition & 1 deletion rust-toolchain
Original file line number Diff line number Diff line change
@@ -1 +1 @@
1.60
1.63
36 changes: 18 additions & 18 deletions src/dot.rs
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
/*!
EGraph visualization with [GraphViz]

Use the [`Dot`] struct to visualize an [`EGraph`]
Use the [`Dot`] struct to visualize an [`EGraph`](crate::EGraph)

[GraphViz]: https://graphviz.gitlab.io/
!*/
Expand All @@ -11,13 +11,13 @@ use std::fmt::{self, Debug, Display, Formatter};
use std::io::{Error, ErrorKind, Result, Write};
use std::path::Path;

use crate::{egraph::EGraph, Analysis, Language};
use crate::{raw::EGraphResidual, Language};

/**
A wrapper for an [`EGraph`] that can output [GraphViz] for
A wrapper for an [`EGraphResidual`] that can output [GraphViz] for
visualization.

The [`EGraph::dot`](EGraph::dot()) method creates `Dot`s.
The [`EGraphResidual::dot`] method creates `Dot`s.

# Example

Expand Down Expand Up @@ -50,19 +50,18 @@ instead of to its own eclass.

[GraphViz]: https://graphviz.gitlab.io/
**/
pub struct Dot<'a, L: Language, N: Analysis<L>> {
pub(crate) egraph: &'a EGraph<L, N>,
pub struct Dot<'a, L: Language> {
pub(crate) egraph: &'a EGraphResidual<L>,
/// A list of strings to be output top part of the dot file.
pub config: Vec<String>,
/// Whether or not to anchor the edges in the output.
/// True by default.
pub use_anchors: bool,
}

impl<'a, L, N> Dot<'a, L, N>
impl<'a, L> Dot<'a, L>
where
L: Language + Display,
N: Analysis<L>,
{
/// Writes the `Dot` to a .dot file with the given filename.
/// Does _not_ require a `dot` binary.
Expand Down Expand Up @@ -170,16 +169,15 @@ where
}
}

impl<'a, L: Language, N: Analysis<L>> Debug for Dot<'a, L, N> {
impl<'a, L: Language> Debug for Dot<'a, L> {
fn fmt(&self, f: &mut Formatter) -> fmt::Result {
f.debug_tuple("Dot").field(self.egraph).finish()
}
}

impl<'a, L, N> Display for Dot<'a, L, N>
impl<'a, L> Display for Dot<'a, L>
where
L: Language + Display,
N: Analysis<L>,
{
fn fmt(&self, f: &mut Formatter) -> fmt::Result {
writeln!(f, "digraph egraph {{")?;
Expand All @@ -192,37 +190,39 @@ where
writeln!(f, " {}", line)?;
}

let classes = self.egraph.generate_class_nodes();

// define all the nodes, clustered by eclass
for class in self.egraph.classes() {
writeln!(f, " subgraph cluster_{} {{", class.id)?;
for (&id, class) in &classes {
writeln!(f, " subgraph cluster_{} {{", id)?;
writeln!(f, " style=dotted")?;
for (i, node) in class.iter().enumerate() {
writeln!(f, " {}.{}[label = \"{}\"]", class.id, i, node)?;
writeln!(f, " {}.{}[label = \"{}\"]", id, i, node)?;
}
writeln!(f, " }}")?;
}

for class in self.egraph.classes() {
for (&id, class) in &classes {
for (i_in_class, node) in class.iter().enumerate() {
let mut arg_i = 0;
node.try_for_each(|child| {
// write the edge to the child, but clip it to the eclass with lhead
let (anchor, label) = self.edge(arg_i, node.len());
let child_leader = self.egraph.find(child);

if child_leader == class.id {
if child_leader == id {
writeln!(
f,
// {}.0 to pick an arbitrary node in the cluster
" {}.{}{} -> {}.{}:n [lhead = cluster_{}, {}]",
class.id, i_in_class, anchor, class.id, i_in_class, class.id, label
id, i_in_class, anchor, id, i_in_class, id, label
)?;
} else {
writeln!(
f,
// {}.0 to pick an arbitrary node in the cluster
" {}.{}{} -> {}.0 [lhead = cluster_{}, {}]",
class.id, i_in_class, anchor, child, child_leader, label
id, i_in_class, anchor, child, child_leader, label
)?;
}
arg_i += 1;
Expand Down
29 changes: 16 additions & 13 deletions src/eclass.rs
Original file line number Diff line number Diff line change
@@ -1,33 +1,41 @@
use std::fmt::Debug;
use std::fmt::{Debug, Formatter};
use std::iter::ExactSizeIterator;

use crate::*;

/// An equivalence class of enodes.
/// The additional data required to turn a [`raw::RawEClass`] into a [`EClass`]
#[non_exhaustive]
#[derive(Debug, Clone)]
#[derive(Clone)]
#[cfg_attr(feature = "serde-1", derive(serde::Serialize, serde::Deserialize))]
pub struct EClass<L, D> {
/// This eclass's id.
pub id: Id,
pub struct EClassData<L, D> {
/// The equivalent enodes in this equivalence class.
pub nodes: Vec<L>,
/// The analysis data associated with this eclass.
///
/// Modifying this field will _not_ cause changes to propagate through the e-graph.
/// Prefer [`EGraph::set_analysis_data`] instead.
pub data: D,
/// The parent enodes and their original Ids.
pub(crate) parents: Vec<(L, Id)>,
}

impl<L: Language, D: Debug> Debug for EClassData<L, D> {
fn fmt(&self, f: &mut Formatter<'_>) -> std::fmt::Result {
let mut nodes = self.nodes.clone();
nodes.sort();
write!(f, "({:?}): {:?}", self.data, nodes)
}
}

/// An equivalence class of enodes
pub type EClass<L, D> = raw::RawEClass<EClassData<L, D>>;

impl<L, D> EClass<L, D> {
/// Returns `true` if the `eclass` is empty.
pub fn is_empty(&self) -> bool {
self.nodes.is_empty()
}

/// Returns the number of enodes in this eclass.
#[allow(clippy::len_without_is_empty)] // https://github.com/rust-lang/rust-clippy/issues/11165
pub fn len(&self) -> usize {
self.nodes.len()
}
Expand All @@ -36,11 +44,6 @@ impl<L, D> EClass<L, D> {
pub fn iter(&self) -> impl ExactSizeIterator<Item = &L> {
self.nodes.iter()
}

/// Iterates over the parent enodes of this eclass.
pub fn parents(&self) -> impl ExactSizeIterator<Item = (&L, Id)> {
self.parents.iter().map(|(node, id)| (node, *id))
}
}

impl<L: Language, D> EClass<L, D> {
Expand Down
Loading