Skip to content


Switch branches/tags

Name already in use

A tag already exists with the provided branch name. Many Git commands accept both tag and branch names, so creating this branch may cause unexpected behavior. Are you sure you want to create this branch?


Failed to load latest commit information.
Latest commit message
Commit time

ruler logo Ruler

This project is under active development and not yet stable. If you are looking for the version of Ruler from Nandi et al's Rewrite Rule Inference Using Equality Saturation, please use this branch

Ruler is a framework that uses equality saturation to automatically infer small, expressive rulesets for a domain.


Ruler is implemented in Rust. You can install Rust here. To build Ruler, type cargo build --release. This should take a few minutes.


To install Ruler, 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.


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.
    • is the main entrypoint and defines some auxiliary data types.
    • 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.)
    • 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, $W_1$ and $W_2$ and a string, $s$; for each term in $W_2$ that contains $s$, it “plugs” in the values in $W_1$ and generates a new workload which is a cross product of all the new plugged terms.
    • contains an implementation of s-expressions.
    • defines a rewrite rule.
    • contains the Ruleset data type. Rulesets are implemented as an IndexMap of Equality. There are several operations over Rulesets that can be used to combine, compose, and refine rulesets. For example, Ruleset::cvec_match extracts a set of equalities from an egraph via cvec-matching; Ruleset::minimize can be used to eliminate redundant rules from a ruleset; Ruleset::derive tests the proving power of one ruleset compared to another.
    • defines the Filter data type which can be used to filter workloads. and define data types that are used in Filter.
    • has some small helper functions.


See here for documentation on OOPSLA artifacts.

Extending Ruler to Support New Domains

Ruler's goal is to support rewrite inference for new domains, given a grammar, an interpreter, and a validation technique. To understand how to add support for a new domain, you can look at the domains in the tests directory. Note that some domains are experimental and not reported in the paper, but they all provide examples of how you can add support for new domains.