Skip to content

Commit

Permalink
merge
Browse files Browse the repository at this point in the history
  • Loading branch information
smjleo committed Jul 12, 2024
2 parents 12cc1ee + dae3050 commit 019e013
Show file tree
Hide file tree
Showing 46 changed files with 7,526 additions and 2,731 deletions.
32 changes: 18 additions & 14 deletions .github/workflows/build.yml
Original file line number Diff line number Diff line change
@@ -1,24 +1,28 @@
name: Build and Test

on: [push, pull_request]

jobs:
build:

runs-on: ubuntu-latest

test:
runs-on: ubuntu-20.04
steps:
- uses: actions/checkout@v1
- uses: actions/checkout@v2
- name: Cache cargo bin
uses: actions/cache@v1
uses: actions/cache@v2
with:
path: ~/.cargo/bin
key: ${{ runner.os }}-cargo-bin
- name: Install cargo web
run: which cargo-web || cargo install cargo-web
- name: Install cbc
run: sudo apt-get install coinor-libcbc-dev
- name: Test
run: make test
nits:
runs-on: ubuntu-20.04
steps:
- uses: actions/checkout@v2
- name: Install cargo deadlinks
run: which cargo-deadlinks || cargo install cargo-deadlinks
- name: Install graphviz
run: sudo apt-get update && sudo apt-get install graphviz
- name: Build and Test
run: make
run: |
curl -L -o ~/.cargo/bin/cargo-deadlinks https://github.com/deadlinks/cargo-deadlinks/releases/download/0.4.2/deadlinks-linux
chmod +x ~/.cargo/bin/cargo-deadlinks
cargo deadlinks --version
- name: Nits
run: make nits
23 changes: 23 additions & 0 deletions .github/workflows/docs.yml
Original file line number Diff line number Diff line change
@@ -0,0 +1,23 @@
name: Publish Docs
on:
push:
branches:
- main
jobs:
docs:
runs-on: ubuntu-latest
steps:
- uses: actions/checkout@v2
with:
persist-credentials: false
- name: Build Docs
run: |
cargo doc --no-deps --all-features
touch target/doc/.nojekyll # prevent jekyll from running
- name: Deploy 🚀
uses: JamesIves/[email protected]
with:
GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
BRANCH: gh-pages # The branch the action should deploy to.
FOLDER: target/doc # The folder the action should deploy.
CLEAN: true # Automatically remove deleted files from the deploy branch
7 changes: 6 additions & 1 deletion .gitignore
Original file line number Diff line number Diff line change
Expand Up @@ -10,4 +10,9 @@ egg/data/
default.nix

# other stuff
TODO.md
TODO.md
flamegraph.svg
perf.data*
*.bench
.vscode/settings.json
out.csv
169 changes: 150 additions & 19 deletions CHANGELOG.md
Original file line number Diff line number Diff line change
@@ -1,8 +1,129 @@
# Changes

<!-- next-header -->

## [Unreleased] - ReleaseDate
- 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.

## [0.9.5] - 2023-06-29
- Fixed a few edge cases in proof size optimization that caused egg to crash.

## [0.9.4] - 2023-05-23
- [#253] Improved rebuilding algorithm using a queue.
- [#259] Fixed another overflow bug in proof size optimization.
- Various typo fixes (Thanks @nlewycky)

## [0.9.3] - 2023-02-06

### Added
- [#215](https://github.com/egraphs-good/egg/pull/215) Added a better intersection algorithms on two egraphs based on "Join Algorithms for the Theory of Uninterpreted Functions". The old intersection algorithm was not complete on the terms in both egraphs, but the new one is. Unfortunately, the new algorithm is quadratic.

### Changed
- [#230](https://github.com/egraphs-good/egg/pull/230) Fixed a performance bug in `get_string_with_let` that caused printing let-bound proofs to be extremely inefficient.


## [0.9.2] - 2022-12-15

### Added

- [#210](https://github.com/egraphs-good/egg/pull/210) Fix crashes in proof generation due to proof size calculations overflowing.

## [0.9.1] - 2022-09-22

### Added

- [#186](https://github.com/egraphs-good/egg/pull/186) Added proof minimization (enabled by default), a greedy algorithm to find smaller proofs
- with and `without_explanation_length_optimization` for turning this on and off
- `copy_without_unions` for copying an egraph but without any equality information
- `id_to_expr` for getting an expression corresponding to a particular enode's id
- [#197](https://github.com/egraphs-good/egg/pull/197) Added `search_with_limit`, so that matching also stops when it hits scheduling limits.

### Changed

- Changed the `pre_union` hook to support explanations
- now provides the `Id` of the two specific enodes that are merged, not canonical ids.
- It also provides the reason for the merge in the form of a `Justification`.

## [0.9.0] - 2022-06-12

### Added
- Added a way to update analysis data and have it propagate through the e-graph

### Changed
- Improved documentation
- Updated dependencies
- `union` is now allowed when explanations are on

## [0.8.1] - 2022-05-04

### Changed
- Improved documentation for features.

## [0.8.0] - 2022-04-28

### Added
- ([#128](https://github.com/egraphs-good/egg/pull/128)) Add an ILP-based extractor.
- ([#168](https://github.com/egraphs-good/egg/pull/168)) Added MultiPatterns.

### Changed
- ([#165](https://github.com/egraphs-good/egg/pull/165)) Unions now happen "instantly", restoring the pre-0.7 behavior.
- The tested MSRV is now 1.60.0.
- Several small documentation enhancements.
- ([#162](https://github.com/egraphs-good/egg/pull/162), [#163](https://github.com/egraphs-good/egg/pull/163))
Extracted the `Symbol` logic into the [`symbol_table`](https://crates.io/crates/symbol_table) crate.

## [0.7.1] - 2021-12-14

This patch fixes a pretty bad e-matching bug introduced in 0.7.0. Please upgrade!

### Fixed
- (#143) Non-linear patterns e-match correctly again
- (#141) Loosen requirement on FromOp::Error

## [0.7.0] - 2021-11-23

It's a been a long time since a release!
There's a lot in this one, hopefully I can cut releases more frequently in the future,
because there are definitely more features coming :)

### Added
- The egraph now has an `EGraph::with_explanations_enabled` mode that allows for
explaining why two terms are equivalent in the egraph.
In explanations mode, all unions must be done through `union_instantiations` in order
to justify the union.
Calling `explain_equivalence` returns an `Explanation`
which has both a `FlatExplanation` form and a
`TreeExplanation` form.
See #115 and #119 for more details.
- The `BackoffScheduler` is now more flexible.
- `EGraph::pre_union` allows inspection of unions, which can be useful for debugging.
- The dot printer is now more flexible.

### Changed

- `Analysis::merge` now gets a `&mut self`, so it can store data on the `Analysis` itself.
- `Analysis::merge` has a different signature.
- Pattern compilation and execution is faster, especially when there are ground terms involved.
- All unions are now delayed until rebuilding, so `EGraph::rebuild` be called to observe effects.
- The `apply_one` function on appliers *now needs to perform unions*.
- The congruence closure algorithm now keeps the egraph congruent before
doing any analysis (calling `make`). It does this by interleaving rebuilding
and doing analysis.
- `EGraph::add_expr` now proceeds linearly through the given `RecExpr`, which
should be faster and include _all_ e-nodes from the expression.
- `Rewrite` now has public `searcher` and `applier` fields and no `long_name`.
- ([#61](https://github.com/egraphs-good/egg/pull/61))
Rebuilding is much improved!
The new algorithm's congruence closure part is closer to
[Downey, Sethi, Tarjan](https://dl.acm.org/doi/pdf/10.1145/322217.322228),
and the analysis data propagation is more precise with respect to merging.
Overall, the algorithm is simpler, easier to reason about, and more than twice as fast!
- ([#86](https://github.com/egraphs-good/egg/pull/86))
`Language::display_op` has been removed. Languages should implement `Display`
to display the operator instead. `define_language!` now implements `Display`
accordingly.
- `Language::from_op_str` has been replaced by a new `FromOp` trait.
`define_language!` implements this trait automatically.

## [0.6.0] - 2020-07-16

Expand All @@ -26,7 +147,7 @@
- Rewrite creation will now fail if the searcher doesn't bind the right variables.
- The `rewrite!` macro supports bidirectional rewrites now.
- `define_language!` now supports variable numbers of children with `Box<[Id]>`.

### Fixed
- The `rewrite!` macro builds conditional rewrites in the correct order now.

Expand All @@ -50,14 +171,14 @@
as per-eclass data.
- **Fix:**
An eclass's metadata will now get updated by
congruence.
([commit](https://github.com/mwillsey/egg/commit/0de75c9c9b0a80adb67fb78cc98cce3da383621a))
congruence.
([commit](https://github.com/egraphs-good/egg/commit/0de75c9c9b0a80adb67fb78cc98cce3da383621a))
- The `BackoffScheduler` will now fast-forward if all rules are banned.
([commit](https://github.com/mwillsey/egg/commit/dd172ef77279e28448d0bf8147e0171a8175228d))
([commit](https://github.com/egraphs-good/egg/commit/dd172ef77279e28448d0bf8147e0171a8175228d))
- Improve benchmark reporting
([commit](https://github.com/mwillsey/egg/commit/ca2ea5e239feda7eb6971942e119075f55f869ab))
- The egraph now skips irrelevant eclasses while searching for a ~40% search speed up.
([PR](https://github.com/mwillsey/egg/pull/21))
([commit](https://github.com/egraphs-good/egg/commit/ca2ea5e239feda7eb6971942e119075f55f869ab))
- The egraph now skips irrelevant eclasses while searching for a ~40% search speed up.
([PR](https://github.com/egraphs-good/egg/pull/21))

## [0.3.0] - 2020-02-27

Expand Down Expand Up @@ -121,13 +242,23 @@ But hopefully things will be a little more stable from here on out
since the API is a lot nicer.

<!-- next-url -->
[Unreleased]: https://github.com/mwillsey/egg/compare/v0.6.0...HEAD
[0.6.0]: https://github.com/mwillsey/egg/compare/v0.5.0...v0.6.0
[0.5.0]: https://github.com/mwillsey/egg/compare/v0.4.1...v0.5.0
[0.4.1]: https://github.com/mwillsey/egg/compare/v0.4.0...v0.4.1
[0.4.0]: https://github.com/mwillsey/egg/compare/v0.3.0...v0.4.0
[0.3.0]: https://github.com/mwillsey/egg/compare/v0.2.0...v0.3.0
[0.2.0]: https://github.com/mwillsey/egg/compare/v0.1.2...v0.2.0
[0.1.2]: https://github.com/mwillsey/egg/compare/v0.1.1...v0.1.2
[0.1.1]: https://github.com/mwillsey/egg/compare/v0.1.0...v0.1.1
[0.1.0]: https://github.com/mwillsey/egg/tree/v0.1.0
[Unreleased]: https://github.com/egraphs-good/egg/compare/v0.9.5...HEAD
[0.9.5]: https://github.com/egraphs-good/egg/compare/v0.9.4...v0.9.5
[0.9.4]: https://github.com/egraphs-good/egg/compare/v0.9.3...v0.9.4
[0.9.3]: https://github.com/egraphs-good/egg/compare/v0.9.2...v0.9.3
[0.9.2]: https://github.com/egraphs-good/egg/compare/v0.9.1...v0.9.2
[0.9.1]: https://github.com/egraphs-good/egg/compare/v0.9.0...v0.9.1
[0.9.0]: https://github.com/egraphs-good/egg/compare/v0.8.1...v0.9.0
[0.8.1]: https://github.com/egraphs-good/egg/compare/v0.8.0...v0.8.1
[0.8.0]: https://github.com/egraphs-good/egg/compare/v0.7.1...v0.8.0
[0.7.1]: https://github.com/egraphs-good/egg/compare/v0.7.0...v0.7.1
[0.7.0]: https://github.com/egraphs-good/egg/compare/v0.6.0...v0.7.0
[0.6.0]: https://github.com/egraphs-good/egg/compare/v0.5.0...v0.6.0
[0.5.0]: https://github.com/egraphs-good/egg/compare/v0.4.1...v0.5.0
[0.4.1]: https://github.com/egraphs-good/egg/compare/v0.4.0...v0.4.1
[0.4.0]: https://github.com/egraphs-good/egg/compare/v0.3.0...v0.4.0
[0.3.0]: https://github.com/egraphs-good/egg/compare/v0.2.0...v0.3.0
[0.2.0]: https://github.com/egraphs-good/egg/compare/v0.1.2...v0.2.0
[0.1.2]: https://github.com/egraphs-good/egg/compare/v0.1.1...v0.1.2
[0.1.1]: https://github.com/egraphs-good/egg/compare/v0.1.0...v0.1.1
[0.1.0]: https://github.com/egraphs-good/egg/tree/v0.1.0
73 changes: 47 additions & 26 deletions Cargo.toml
Original file line number Diff line number Diff line change
@@ -1,39 +1,60 @@
[package]
name = "egg"
version = "0.6.1-dev"
authors = ["Max Willsey <[email protected]>"]
edition = "2018"
categories = ["data-structures"]
description = "An implementation of egraphs"
repository = "https://github.com/mwillsey/egg"
readme = "README.md"
license = "MIT"
edition = "2018"
keywords = ["e-graphs"]
categories = ["data-structures"]
license = "MIT"
name = "egg"
readme = "README.md"
repository = "https://github.com/egraphs-good/egg"
version = "0.9.5"

[dependencies]
symbolic_expressions = "5"
log = "0.4"
smallvec = "1"
indexmap = "1"
instant = "0.1"
once_cell = "1"
env_logger = { version = "0.9.0", default-features = false }
fxhash = "0.2.1"
hashbrown = "0.12.1"
indexmap = "1.8.1"
quanta = "0.12"
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"
num-bigint = "0.4"
num-traits = "0.2"

# for the lp feature
coin_cbc = { version = "0.1.6", optional = true }

# for the serde-1 feature
serde = { version = "1", features = ["derive"], optional = true }
serde = { version = "1.0.137", features = ["derive"], optional = true }
vectorize = { version = "0.2.0", optional = true }

# for the reports feature
serde_json = { version = "1", optional = true }
serde_json = { version = "1.0.81", optional = true }
saturating = "0.1.0"

[dev-dependencies]
env_logger = {version = "0.7", default-features = false}
ordered-float = "1"
ordered-float = "3.0.0"

[features]
upward-merging = []
stdweb = [ "instant/stdweb" ]
serde-1 = [ "serde", "indexmap/serde-1" ]
reports = [ "serde-1", "serde_json" ]

[workspace]
members = [
".",
"web-demo",
# forces the use of indexmaps over hashmaps
deterministic = []
lp = ["coin_cbc"]
reports = ["serde-1", "serde_json"]
serde-1 = [
"serde",
"indexmap/serde-1",
"hashbrown/serde",
"symbol_table/serde",
"vectorize",
]
wasm-bindgen = []

# private features for testing
test-explanations = []

[package.metadata.docs.rs]
all-features = true
rustdoc-args = ["--cfg", "docsrs"]
Loading

0 comments on commit 019e013

Please sign in to comment.