Generate Egg programs from Metatheory.jl

gen_egg.jl

using Pkg
Pkg.activate("metatheory")
Pkg.add(url="https://github.com/0x0f0f0f/Metatheory.jl.git")
using Metatheory
using Metatheory.EGraphs

to_sexpr_pattern(e::QuoteNode) = e.value
to_sexpr_pattern(e::Symbol) = "?$e" 
function to_sexpr_pattern(e::Expr)
    @assert e.head == :call
    e1 = join([e.args[1] ;  to_sexpr_pattern.(e.args[2:end])], ' ')
    "($e1)"
end

to_sexpr(e::Symbol) = e
to_sexpr(e::Expr) = "($(join(to_sexpr.(e.args),' ')))"

function eggify(rules)
    egg_rules = []
    for rule in rules
        l = to_sexpr_pattern(rule.left)
        r = to_sexpr_pattern(rule.right)
        if rule.mode == :rewrite
            push!(egg_rules,"\tvec![rw!( \"$(rule.expr)\" ; \"$l\" => \"$r\" )]")
        elseif rule.mode == :equational
            push!(egg_rules,"\trw!( \"$(rule.expr)\" ; \"$l\" <=> \"$r\" )")
        else
            println("Unsupported Rewrite Mode")
            @assert false
        end
        
    end
    return join(egg_rules, ",\n")
end
##########################################
# REPLACE WITH YOUR THEORY AND QUERY HERE

theory = @theory begin
    :a * b => :a
    a * b == b * a
end

query = :(a * (b * c))

###########################################

G = EGraph( query )
@time saturate!(G, theory)
extractor = addanalysis!(G, ExtractionAnalysis, astsize)
ex = extract!(G, extractor)
println( "Best found: $ex")

rust_code = 
"""
use egg::{*, rewrite as rw};
//use std::time::Duration;

fn main() {
    let rules : &[Rewrite<SymbolLang, ()>] = &vec![
    $(eggify(theory))
    ].concat();
    
    let start = "$(to_sexpr(query))".parse().unwrap();
    let runner = Runner::default().with_expr(&start)
        // More options here https://docs.rs/egg/0.6.0/egg/struct.Runner.html
        //.with_iter_limit(10)
        //.with_node_limit(1_000_000)
        //.with_time_limit(Duration::new(30,0))
        .run(rules);
    runner.print_report();
    let mut extractor = Extractor::new(&runner.egraph, AstSize);
    let (best_cost, best_expr) = extractor.find_best(runner.roots[0]);
    println!("best cost: {}, best expr {}", best_cost, best_expr);
}
"""
open("src/main.rs", "w") do f
    write(f, rust_code)
end

Instructions.md

This is a simple script to convert Metatheory.jl https://github.com/0x0f0f0f/Metatheory.jl theories into an Egg https://egraphs-good.github.io/ query for comparison.

Get a rust toolchain https://rustup.rs/

Make a new project

cargo new my_project
cd my_project

Add egg as a dependency to the Cargo.toml. Add the last line shown here.

[package]
name = "autoegg"
version = "0.1.0"
authors = ["Philip Zucker <philzook58@gmail.com>"]
edition = "2018"

# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html

[dependencies]
egg = "0.6.0"

Copy and paste the Julia script in the project folder. Replace the example theory and query with yours in the script Run it

julia gen_egg.jl

Now you can run it in Egg

cargo run --release

Profit.

thread 'main' panicked at 'called `Result::unwrap()` on an `Err` value: "Rewrite p ∧ ¬p => false refers to unbound var ?false"', src/main.rs:23:10
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace

I've added the line
to_sexpr_pattern(e::Bool) = "?$e"

My theory

or_alg = @theory begin
    ((p ∨ q) ∨ r)       ==  (p ∨ (q ∨ r))
    (p ∨ q)             ==  (q ∨ p)
    (p ∨ p)             =>  p
    (p ∨ true)          =>  true
    (p ∨ false)         =>  p
end

and_alg = @theory begin
    ((p ∧ q) ∧ r)       ==  (p ∧ (q ∧ r))
    (p ∧ q)             ==  (q ∧ p)
    (p ∧ p)             =>  p
    (p ∧ true)          =>  p
    (p ∧ false)         =>  false
end

comb = @theory begin
    # DeMorgan
    ¬(p ∨ q)            ==  (¬p ∧ ¬q)
    ¬(p ∧ q)            ==  (¬p ∨ ¬q)
    # distrib
    (p ∧ (q ∨ r))       ==  ((p ∧ q) ∨ (p ∧ r))
    (p ∨ (q ∧ r))       ==  ((p ∨ q) ∧ (p ∨ r))
    # absorb
    (p ∧ (p ∨ q))       =>  p
    (p ∨ (p ∧ q))       =>  p
    # complement
    (p ∧ (¬p ∨ q))      =>  p ∧ q
    (p ∨ (¬p ∧ q))      =>  p ∨ q
end

negt = @theory begin
    (p ∧ ¬p)            =>  false
    (p ∨ ¬(p))          =>  true
    ¬(¬p)               ==  p
end

impl = @theory begin
    (p == ¬p)           =>  false
    (p == p)            =>  true
    (p == q)            =>  (¬p ∨ q) ∧ (¬q ∨ p)
    (p => q)            =>  (¬p ∨ q)
end

fold = @theory begin
    (true == false)     =>   false
    (false == true)     =>   false
    (true == true)      =>   true
    (false == false)    =>   true
    (true ∨ false)      =>   true
    (false ∨ true)      =>   true
    (true ∨ true)       =>   true
    (false ∨ false)     =>   false
    (true ∧ true)       =>   true
    (false ∧ true)      =>   false
    (true ∧ false)      =>   false
    (false ∧ false)     =>   false
    ¬(true)             =>   false
    ¬(false)            =>   true
end

theory = or_alg ∪ and_alg ∪ comb ∪ negt ∪ impl ∪ fold


query = :(¬(((¬p ∨ q) ∧ (¬r ∨ s)) ∧ (p ∨ r)) ∨ (q ∨ s))