JuliaSymbolics / Metatheory.jl

Makes Julia reason with equations. General purpose metaprogramming, symbolic computation and algebraic equational reasoning library for the Julia programming language: E-Graphs & equality saturation, term rewriting and more.
https://juliasymbolics.github.io/Metatheory.jl/dev/
MIT License
362 stars 47 forks source link

`astsize_inv` cost function #64

Open gpeairs opened 3 years ago

gpeairs commented 3 years ago

I think there's a bug in astsize_inv, since -1 * astsize(n, g, an) means within astsize you're adding the arguments' inverted cost to the usual positive 1+arity for the current node. I don't 100% understand how everything works yet, but I think it should be

function astsize_inv(n::ENode, g::EGraph, an::Type{<:AbstractAnalysis})
    cost = -(1 + arity(n)) # minus sign here is the only difference vs astsize
    for id ∈ n.args
        eclass = geteclass(g, id)
        !hasdata(eclass, an) && (cost += Inf; break)
        cost += last(getdata(eclass, an))
    end
    return cost
end

This seems to fix test_boson.jl, if I understand correctly what it was meant to do (also adding a rule):

boson = @theory begin :c * :cdag => :cdag * :c + 1 end

distr_assoc = distrib(:*, :+) ∪ associativity(:*)

ident_comm = @theory begin
    1 * x => x * 1
end

ident = @theory begin
    1 * x => x
end

function boson_expand(ex, timeout=9)
    params = SaturationParams(timeout=timeout)
    G = EGraph(ex)
    saturate!(G, boson ∪ distr_assoc ∪ ident_comm, params)
    ex = extract!(G, astsize_inv)
    G = EGraph(ex)
    saturate!(G, distr_assoc ∪ ident, params)
    ex = extract!(G, astsize)
    return ex
end

e1 = :(c * c * cdag * cdag)
boson_expand(e1)
:((cdag * (((cdag * c + 1) + 1) * c) + (cdag * c + 1)) + (cdag * c + 1))
0x0f0f0f commented 3 years ago

Thanks!