DOCSEARCHbyAlgolia
Submit Docs

egglog

repository·main·Indexed 21 days ago

https://github.com/egraphs-good/egglog

A next-generation equality saturation engine that combines equality saturation with Datalog for high-performance program transformations and reasoning. It provides a Rust library and CLI with REPL and standard modes, supporting parallel execution via rayon and WebAssembly compilation via wasm-pack.

Tokens
36.7K
Snippets
128
Records
164
Agent score
73%

What's inside egglog

  1. Configure parallelism in egglog

    main

    Egglog uses rayon's global thread pool for parallelism.

    • CLI Users: Use the -j flag. Setting -j 0 uses the maximum inferred parallelism of the system.
    • Library Users: Control the level of parallelism by configuring rayon's num_threads in your own code.

  2. Install egglog from source

    main

    To install the core egglog engine from the repository, ensure you have Cargo installed, then clone the repository and install the path-based dependency.

    Note: This installs the core engine. For a more feature-rich experience, consider egglog-experimental.

    git clone git@github.com:egraphs-good/egglog.git
cargo install --path=egglog

  3. Extract terms from an e-graph

    main

    To retrieve an extracted term from an e-graph back into your application, follow these steps:

    1. Bind the term: In your egglog program, use a let binding to assign a global name to the term you want to extract (e.g., (let $root ...)).
    2. Resolve the name: Use EGraph::eval_expr to resolve that global name to its (sort, Value) representation.
    3. Perform extraction:
      • For the default cost model, use EGraph::extract_value.
      • For custom cost models, use EGraph::extract_value_with_cost_model or implement the extract::CostModel trait.

    The extract module contains the complete API for extraction operations.

    // Conceptual workflow in egglog
// (let $root (some_expression))

// In Rust:
// 1. EGraph::eval_expr("$root") -> (sort, Value)
// 2. EGraph::extract_value(value) -> ExtractedTerm

  4. Build egglog to WebAssembly

    main

    This package provides an example of how to compile egglog to WebAssembly (Wasm) for use in web environments. The build process is based on the wasm-bindgen pattern for building without a bundler.

    To build and test the WebAssembly implementation, ensure you have wasm-pack installed and use the provided Makefile.

    cargo install wasm-pack
make test

  5. Generate code coverage reports

    main

    To generate local code coverage reports, use cargo-llvm-cov and the provided Makefile target.

    1. Install cargo-llvm-cov.
    2. Run make coverage to generate an lcov.info report using nextest.
    3. (Optional) Use the Coverage Gutters VS Code extension to visualize coverage directly in your editor.
    cargo install cargo-llvm-cov
make coverage

  6. Profile egglog performance with samply

    main

    To debug performance issues, you can use samply. Follow these steps to build a profiling build with debug symbols and record a trace:

    1. Install samply via cargo.
    2. Build the project using the profiling profile.
    3. Record the execution of an .egg file.

    To reduce noise from stdout during profiling, you can set RUST_LOG=error and use the --no-messages flag if supported.

    # 1. Install samply
cargo install --locked samply

# 2. Build a profile build which includes debug symbols
cargo build --profile profiling

# 3. Run the egglog file and profile
samply record ./target/profiling/egglog tests/extract-vec-bench.egg

# [Optional] Run without logging/printing to reduce stdout noise
env RUST_LOG=error samply record ./target/profiling/egglog --no-messages tests/extract-vec-bench.egg

  7. How to use egglog from Rust

    main

    While egglog is a standalone language, you can integrate it into Rust applications. The recommended workflow is to write your sorts, functions, and rules as an egglog program and execute them using EGraph::parse_and_run_program.

    Use the following patterns to decide which API to use:

    • Standard Workflow: Write egglog code and use EGraph::parse_and_run_program.
    • Direct Manipulation: Use EGraph::update only when you must perform reads/writes from Rust (e.g., integrating with existing Rust data structures).
    • Rust-based Rules: For rules where the Right-Hand Side (RHS) requires Rust logic, use prelude::rust_rule or prelude::rust_rule_full.
    • Custom Functions: To define new functions callable from egglog expressions, define a custom Primitive and register it using EGraph::add_*_primitive. The add_primitive! macro is available for common pure native functions.

  8. Use Term and TermDag for efficient term manipulation

    main

    egglog uses a TermDag (Directed Acyclic Graph) to represent terms. Instead of using recursive tree structures, terms are represented by a TermId (a usize) that points into a TermDag. This approach provides automatic hashconsing, meaning identical terms are deduplicated and share the same TermId, which enables efficient structural equality checks and memory savings.

    Key Types

    • TermId: A type alias for usize used to reference terms.
    • Term: An enum representing the structure of a term: Lit(Literal), Var(String), or App(String, Vec<TermId>).
    • TermDag: A hashconsing arena that manages the storage and deduplication of Terms.
    • OrdTerm<'a>: A wrapper for TermId that allows ordering terms based on their AST structure rather than their insertion order in the DAG. This is useful for using terms as keys in ordered collections like BTreeMap or BTreeSet.
    // Example of creating terms within a TermDag
let mut td = TermDag::default();
let x = td.var("x".into());
let y = td.var("y".into());
let lit = td.lit(7.into());
let app = td.app("f".into(), vec![x, lit]);

  9. Implement a custom CostModel

    main

    To customize how egglog calculates the cost of extracted terms, implement the CostModel<C> trait.

    Requirements for the cost type C:

    • Must satisfy Ord + Eq + Clone + Debug.
    • Must implement the Cost trait.
    • To avoid cycles in extracted terms, the cost model should ideally guarantee that a term has a no-smaller cost than its subterms. If a term can have a lower cost than its subterms, the extractor will still terminate as long as there are no negative cost cycles, but you must ensure the resulting extracted terms are acyclic.

    Key Methods to Implement:

    • fold: Calculates the total cost of a term using the head cost and the costs of its children.
    • enode_cost: Returns the cost of an enode (excluding children).
    • container_cost (optional): Defines how to combine costs of elements within a container. Defaults to the combine operation of the cost type.
    • base_value_cost (optional): Defines the cost of primitive values. Defaults to C::unit().
    impl CostModel<MyCostType> for MyCustomCostModel {
    fn fold(&self, head: &str, children_cost: &[MyCostType], head_cost: MyCostType) -> MyCostType {
        // Custom logic
    }

    fn enode_cost(&self, egraph: &EGraph, func: &Function, enode: &Enode<'_>) -> MyCostType {
        // Custom logic
    }
}

  10. Understand the Sort trait in egglog

    main

    In egglog, a Sort (or type) defines the domain of values allowed in the e-graph. Sorts are user-extensible, meaning you can implement this trait to define custom types.

    Key characteristics of a Sort:

    • Naming: Every sort has a unique name via name().
    • Backend Integration: Sorts map to backend-specific column types via column_ty() (using ColumnTy).
    • Container Sorts: Some sorts are containers (e.g., sets, vectors) that hold other sorts. These can be identified via is_container_sort(). Container sorts provide access to their elements through inner_sorts() and inner_values().
    • Equality: is_eq_sort() identifies sorts that represent equality (like EqSort).
    • Value Representation: Non-equality sorts typically return a TypeId via value_type() to identify the underlying data type.

  11. Configure egglog Run Modes

    main

    The --mode flag controls how the egglog engine handles output and interaction. Use these modes to adjust verbosity or enable interactive sessions.

    Available Modes:

    • normal: Standard execution mode.
    • desugar: Shows the desugared egglog code (useful for inspecting how high-level commands are translated).
    • interactive: Enables interactive REPL behavior (adds (done) or (error) markers).
    • no-messages: Suppresses all messages/output from the engine.
    eglog --mode desugar my_program.egg

  12. Define rules and rewrites

    main

    Rules are the core mechanism for equality saturation in egglog. They match facts in the database and perform actions.

    Rule Syntax

    A rule matches a list of facts (the body) and executes a list of actions (the head). Matches are performed modulo equality.

    (rule ((body_fact1) (body_fact2)) ((action1) (action2)))

    Rewrite Syntax

    rewrite is syntactic sugar for a rule that unions the left-hand side (LHS) with the right-hand side (RHS).

    (rewrite <lhs> <rhs>)

    Rewrite Options

    • :when (<conditions>): The rewrite only applies if the specified conditions are met.
    • :subsume: Causes the LHS to be subsumed after matching, meaning it can no longer be matched in a rule but can still be checked against.
    • bi-rewrite: Generates two rules, one for each direction (LHS $\to$ RHS and RHS $\to$ LHS).

    Examples

    // Standard rewrite
(rewrite (Add a b) (Add b a))

// Rewrite with condition
(rewrite (Add a b) (Add b a) :when ((= a (Num 0))))

// Rewrite with subsumption
(rewrite (Mul a 2) (bitshift-left a 1) :subsume)

// Bidirectional rewrite
(bi-rewrite (Mul (Var x) (Num 0)) (Var x))
    (rule ((edge x y)) ((path x y)))
(rewrite (Add a b) (Add b a))
(bi-rewrite (Mul (Var x) (Num 0)) (Var x))