21 个版本

0.9.5 2023 年 6 月 29 日
0.9.3 2023 年 2 月 6 日
0.9.2 2022 年 12 月 15 日
0.9.1 2022 年 9 月 23 日
0.0.2 2019 年 5 月 21 日

#89 in 数据结构

Download history 6173/week @ 2024-04-22 5137/week @ 2024-04-29 5841/week @ 2024-05-06 9869/week @ 2024-05-13 9691/week @ 2024-05-20 10730/week @ 2024-05-27 9117/week @ 2024-06-03 13858/week @ 2024-06-10 14363/week @ 2024-06-17 14911/week @ 2024-06-24 8325/week @ 2024-07-01 13042/week @ 2024-07-08 13620/week @ 2024-07-15 16301/week @ 2024-07-22 16522/week @ 2024-07-29 13353/week @ 2024-08-05

60,974 每月下载量
用于 8 软件包(5 个直接使用)

MIT 许可证

350KB
6K SLoC

egg 标志 egg: egraphs good

Crates.io Released Docs.rs Main branch docs Zulip

还可以查看基于 Datalog 的基于语言的、增量执行和可组合分析的替代方法 egglog 系统。请参阅 论文网络演示

你在使用 egg 吗?请使用以下 BibTeX 引用,并将你的项目添加到 egg 网站

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

查看 网络演示 以快速进行 e-graph 操作!

使用 egg

egg 添加到您的 Cargo.toml,如下所示

[dependencies]
egg = "0.9.5"

如果您正在衡量性能,请确保使用 --release 进行编译!

开发

它是用 Rust 编写的。通常,您会使用 rustup 安装 Rust。

运行 cargo doc --open 来构建并在浏览器中打开文档。

在提交/推送之前,请确保运行 make,它会运行 CI 将要运行的所有测试和 lint(包括那些在功能标志下)。由于 lp 功能,此要求 cbc 解算器。

测试

运行 cargo test 将运行测试。一些测试可能会超时;如果发生这种情况,请尝试运行 cargo test --release

tests 目录中有几个有趣的测试。

  • prop.rs 实现了命题逻辑并证明了几个简单的定理。
  • math.rs 实现了实数运算,并附带一些符号微分。
  • lambda.rs 实现了一个小的lambda演算,使用 egg 作为部分评估器。

基准测试

要获取每个测试运行时间的简单csv文件,请设置环境变量 EGG_BENCH_CSV,以便为每个测试添加一行到csv文件中。

示例

EGG_BENCH_CSV=math.csv cargo test --test math --release -- --nocapture --test --test-threads=1

依赖项

~1.7–4MB
~74K SLoC