Become a (more) independent fork

Cargo.toml

@@ -2,25 +2,25 @@
 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"
-indexmap = "1.8.1"
-instant = "0.1.12"
+hashbrown = { version = "0.14.3", default-features = false, features = ["inline-more"] }
+indexmap = { version = "1.8.1", optional = true }
+instant = { version = "0.1.12" , optional = true}
 log = "0.4.17"
 smallvec = { version = "1.8.0", features = ["union", "const_generics"] }
-symbol_table = { version = "0.2.0", features = ["global"] }
-symbolic_expressions = "5.0.3"
-thiserror = "1.0.31"
+symbol_table = { version = "0.3.0", features = ["global"], optional = true }
+symbolic_expressions = { version = "5.0.3", optional = true }
+thiserror = { version = "1.0.31" , optional = true }
 
 # for the lp feature
 coin_cbc = { version = "0.1.6", optional = true }
@@ -35,10 +35,12 @@ saturating = "0.1.0"
 
 [dev-dependencies]
 ordered-float = "3.0.0"
+env_logger = { version = "0.9.0", default-features = false }
 
 [features]
 # forces the use of indexmaps over hashmaps
-deterministic = []
+deterministic = ["indexmap"]
+egg_compat = ["indexmap", "instant", "symbol_table", "symbolic_expressions", "thiserror"]
 lp = ["coin_cbc"]
 reports = ["serde-1", "serde_json"]
 serde-1 = [
@@ -49,9 +51,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

Makefile

@@ -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

README.md

@@ -1,88 +1,5 @@
-# <img src="doc/egg.svg" alt="egg logo" height="40" align="left"> egg: egraphs good
-
-[![Crates.io](https://img.shields.io/crates/v/egg.svg)](https://crates.io/crates/egg)
-[![Released Docs.rs](https://img.shields.io/crates/v/egg?color=blue&label=docs)](https://docs.rs/egg/)
-[![Main branch docs](https://img.shields.io/badge/docs-main-blue)](https://egraphs-good.github.io/egg/egg/)
-[![Zulip](https://img.shields.io/badge/zulip-join%20chat-blue)](https://egraphs.zulipchat.com)
-
-Also check out the [egglog](https://github.com/egraphs-good/egglog) 
- system that provides an alternative approach to 
- equality saturation based on Datalog.
-It features a language-based design, incremental execution, and composable analyses.
-See also the [paper](//mwillsey.com/papers/egglog) and the [web demo](https://egraphs-good.github.io/egglog).
-
-Are you using egg?
-Please cite using the BibTeX below and
- add your project to the `egg`
- [website](https://github.com/egraphs-good/egraphs-good.github.io)!
-
-<details class="bibtex">
-    <summary>BibTeX</summary>
-    <code><pre>@article{2021-egg,
-  author = {Willsey, Max and Nandi, Chandrakana and Wang, Yisu Remy and Flatt, Oliver and Tatlock, Zachary and Panchekha, Pavel},
-  title = {egg: Fast and Extensible Equality Saturation},
-  year = {2021},
-  issue_date = {January 2021},
-  publisher = {Association for Computing Machinery},
-  address = {New York, NY, USA},
-  volume = {5},
-  number = {POPL},
-  url = {https://doi.org/10.1145/3434304},
-  doi = {10.1145/3434304},
-  abstract = {An e-graph efficiently represents a congruence relation over many expressions. Although they were originally developed in the late 1970s for use in automated theorem provers, a more recent technique known as equality saturation repurposes e-graphs to implement state-of-the-art, rewrite-driven compiler optimizations and program synthesizers. However, e-graphs remain unspecialized for this newer use case. Equality saturation workloads exhibit distinct characteristics and often require ad-hoc e-graph extensions to incorporate transformations beyond purely syntactic rewrites.  This work contributes two techniques that make e-graphs fast and extensible, specializing them to equality saturation. A new amortized invariant restoration technique called rebuilding takes advantage of equality saturation's distinct workload, providing asymptotic speedups over current techniques in practice. A general mechanism called e-class analyses integrates domain-specific analyses into the e-graph, reducing the need for ad hoc manipulation.  We implemented these techniques in a new open-source library called egg. Our case studies on three previously published applications of equality saturation highlight how egg's performance and flexibility enable state-of-the-art results across diverse domains.},
-  journal = {Proc. ACM Program. Lang.},
-  month = jan,
-  articleno = {23},
-  numpages = {29},
-  keywords = {equality saturation, e-graphs}
-}
-</pre></code>
-</details>
-
-Check out the [web demo](https://egraphs-good.github.io/egg-web-demo) for some quick e-graph action!
-
-## Using egg
-
-Add `egg` to your `Cargo.toml` like this:
-```toml
-[dependencies]
-egg = "0.9.5"
-```
-
-Make sure to compile with `--release` if you are measuring performance!
-
-## Developing
-
-It's written in [Rust](https://www.rust-lang.org/).
-Typically, you install Rust using [`rustup`](https://www.rust-lang.org/tools/install).
-
-Run `cargo doc --open` to build and open the documentation in a browser.
-
-Before committing/pushing, make sure to run `make`, 
- which runs all the tests and lints that CI will (including those under feature flags).
-This requires the [`cbc`](https://projects.coin-or.org/Cbc) solver
- due to the `lp` feature.
-
-### Tests
-
-Running `cargo test` will run the tests.
-Some tests may time out; try `cargo test --release` if that happens.
-
-There are a couple interesting tests in the `tests` directory:
-
-- `prop.rs` implements propositional logic and proves some simple
-  theorems.
-- `math.rs` implements real arithmetic, with a little bit of symbolic differentiation.
-- `lambda.rs` implements a small lambda calculus, using `egg` as a partial evaluator.
-
-
-### Benchmarking
-
-To get a simple csv of the runtime of each test, you set the environment variable
-`EGG_BENCH_CSV` to something to append a row per test to a csv.
-
-Example:
-```bash
-EGG_BENCH_CSV=math.csv cargo test --test math --release -- --nocapture --test --test-threads=1
-```
+This is a fork of [egg](https://github.com/egraphs-good/egg) primarily designed for
+[bat_egg_smt](https://github.com/dewert99/bat_egg_smt) (a toy QF_UF smt solver). It is still
+mostly compatible with the original version of egg when using the "egg_compat" feature
+(enabled by default).
 

rust-toolchain

@@ -1 +1 @@
-1.60
+1.63

src/dot.rs

@@ -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/
 !*/
@@ -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, raw::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
 
@@ -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.
@@ -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 {{")?;
@@ -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;

src/eclass.rs

@@ -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()
     }
@@ -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> {