Enumo is a domain-specific language for programmable theory exploration. It uses equality saturation to infer small, expressive rulesets for a domain.

Publications

• (OOPSLA 2023) A. Pal, B. Saiki, R. Tjoa, C. Richey, A. Zhu, O. Flatt, M. Willsey, Z. Tatlock, C. Nandi, Equality Saturation Theory Exploration à la Carte

• (OOPSLA 2021, Distinguished Paper Award) C. Nandi, M. Willsey, A. Zhu, Y. Wang, B. Saiki, A. Anderson, A. Schulz, D. Grossman, Z. Tatlock, Rewrite Rule Inference Using Equality Saturation. *

* This paper is based on an older version of this repository. If you are looking for the code associated with this paper, please use this branch.

Getting Started

Enumo is implemented in Rust. To install Enumo, the following dependencies must be installed:

• Rust
• libz3

If libz3 is not offered on your system, you can edit Cargo.toml in this directory by changing the dependency z3 = xxx to z3 = {version=xxx, features = ["static-link-z3"]}. This will statically link to a built copy of z3 instead of dynamically linking, but the build process will take considerably longer. It is recommended that you install libz3 if possible.

To build Enumo, type cargo build --release. This should take a few minutes.

Run cargo doc --open to build and open the documentation in a browser.

cargo test will run all the tests, including tests that find rules for a handful of example domains. See the tests directory for examples of how to set up a domain, construct workloads, and find rules.

Project Layout

• The source code resides in the src directory.
  • lib.rs is the main entrypoint and defines some auxiliary data types.
  • language.rs defines the SynthLanguage trait, which must be implemented in order to use the Ruler DSL to find rules for a domain. There are two main things that must be implemented: an interpreter and a rule validator. (In the case of rule lifting, the interpreter is not needed.)
  • workload.rs contains the Workload data type. Workloads evaluate to a list of terms (s-expressions). Workloads can be constructed directly from a list of s-expressions (Workload::Set), combined (Workload::Append), refined with a filter (Workload::Filter), or composed via plugs (Workload::Plug). Plug is a novel operation for generating workloads from smaller workloads. It takes two workloads,