egglog

这是论文 "Better Together: Unifying Datalog and Equality Saturation"（《更好的结合：统一 Datalog 和等价饱和》）所附工具 egglog 的仓库 (ACM DL, arXiv)。

如果您使用这项工作，请使用 此引用。

另请参阅 Python 绑定，它提供了一些额外的文档：https://egglog-python.readthedocs.io/

聊天

这里有关于 egglog 的 Zulip 聊天：https://egraphs.zulipchat.com/#narrow/stream/375765-egglog

先决条件与编译

apt-get install make cargo
cargo install cargo-nextest
make all

使用方法

cargo run [-f fact-path] [-naive] [--to-json] [--to-dot] [--to-svg] <files.egg>

或直接

cargo run

用于交互式解释器。

• --to-dot 命令将在程序末尾保存一个 graphviz dot 文件，将 .egg 扩展名替换为 .dot。
• --to-svg（需要安装 Graphviz），将在程序末尾保存一个 graphviz svg 文件，将 .egg 扩展名替换为 .svg。

社区扩展

• @hatoo 维护了一个 egglog-language 扩展，在 VS Code 中（只需在 VS Code 中搜索 "egglog" 即可）。
• @segeljakt 使用 tree-sitter 维护了一个 Neovim 插件，用于 egglog。

开发

要运行测试，请使用 make test。

文档

要查看文档，请运行 cargo doc --open。

待办事项：将以下文档迁移到 cargo doc

排序：i64

支持以下原语的64位整数

+ - * / %           ; arithmetic
& | ^ << >> not-i64 ; bit-wise operations
< > <= >=           ; comparisons
min max log2
to-f64
to-string

排序：f64

支持以下原语的64位浮点数

+ - * / %           ; arithmetic
< > <= >=           ; comparisons
min max neg
to-i64
to-string

排序：map

从键类型到值类型的映射，支持以下原语

empty
insert
get
not-contains
contains
set-union
set-diff
set-intersect
map-remove

排序：rational

具有64位精度（分子和分母）的分数（有理数），支持以下原语

+ - * /         ; arithmetic
min max neg abs floor ceil round
rational        ; construct from a numerator and denominator
numer denom     ; get numerator and denominator
pow log sqrt
< > <= >=       ; comparisons

这些原语仅在结果本身是纯有理数时定义。

排序：string

使用双引号获取引号："Foo "" Bar" 是 Foo " Bar。没有定义原语。