EGraph saturation does not run its iterations

[Roger-luo]

Hi @0x0f0f0f ! I finally got time to work on the EGraph for circuit idea, so I'm trying to test on a very simple expr as following, but the saturate! doesn't seem to run as I expected, I'm wondering if you know how to fix it? I'm guess I'm not overloading the TermInterface properly, but not sure what happened exactly

the following code implements one simple operation Contract, which should be exactly the same as * (same as @commutative_monoid without identity), but saturate only gives me an egraph with 1 eclass and 1 node, and changing => to == doesn't help

using Metatheory
using TermInterface

abstract type TExpr end

struct Tensor <: TExpr
    id::Int
end

struct Contract <: TExpr
    left
    right
end

TermInterface.istree(::TExpr) = true
TermInterface.exprhead(::TExpr) = :call

TermInterface.operation(::Tensor) = :Tensor
TermInterface.operation(::Contract) = :Contract

TermInterface.arguments(x::Contract) = [x.left, x.right]
TermInterface.arguments(x::Tensor) = [x.id]

function TermInterface.similarterm(x::Type{Contract}, head, args; metadata=nothing)
    @assert head == :call && args[1] == :Contract
    return Contract(args[2:end]...)
end

function TermInterface.similarterm(x::Type{Tensor}, head, args; metadata=nothing)
    @assert head == :call && args[1] == :Tensor
    return Tensor(args[2:end]...)
end

t = @theory A B C begin
    Contract(A, B) => Contract(B, A)
    Contract(Contract(A, B), C) => Contract(A, Contract(B, C))
    Contract(A, Contract(B, C)) => Contract(Contract(A, B), C)
end

T = Contract(Contract(Tensor(1), Tensor(2)), Tensor(3))
G = EGraph(T)

# this only runs one iteration unlike *
saturate!(G, t)

and I'm expecting it to get a similar result as

t = @theory A B C begin
    A * B == B * A
    (A * B) * C == A * (B * C)
    A * (B * C) == (A * B) * C
end

G = EGraph(:((A * B) * C))
saturate!(G, t)

[0x0f0f0f]

There are some breaking changes undergoing similarterm and TermInterface.

[0x0f0f0f]

Let's keep in touch on Zulip :P

#101

[0x0f0f0f]

@Roger-luo can we close this?

[Roger-luo]

yes, thanks!