Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
Generate Egg programs from Metatheory.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

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.

@0x0f0f0f

This comment has been minimized.

Copy link

@0x0f0f0f 0x0f0f0f commented Mar 7, 2021

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
    (truefalse)      =>   true
    (falsetrue)      =>   true
    (truetrue)       =>   true
    (falsefalse)     =>   false
    (truetrue)       =>   true
    (falsetrue)      =>   false
    (truefalse)      =>   false
    (falsefalse)     =>   false
    ¬(true)             =>   false
    ¬(false)            =>   true
end

theory = or_alg  and_alg  comb  negt  impl  fold


query = :(¬(((¬p ∨ q) ∧ (¬r ∨ s)) ∧ (p ∨ r)) ∨ (q ∨ s))
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment