Serious egraphs pattern matcher bug

[0x0f0f0f]

How to reproduce on latest master commit:

testt = @theory begin
    a + b       ==  b + a
    a + (b + c) ==  (a + b) + c
    d - d       => 0
    a + -b      => a - b
    a - b       => a + (-b)
end

ex = :((a + d) + -d)
g = EGraph(ex)
saturate!(g, testt)
# ERROR: unbound pattern variable b in rule Rule(:(a + -b => a - b))

[0x0f0f0f]

The pattern matcher does not produce a substitution for pattern variable b. Only substitution for pattern variable a is produced.

[0x0f0f0f]

Not related to binary operators or parser:

testt = @theory begin
    foo(a, b)           ==  foo(b, a)
    foo(a, foo(b, c))   ==  foo(foo(a, b), c)
    bar(d, d)           =>  0
    foo(a, bar(b))      =>  bar(a, b)
    bar(a, b)           =>  foo(a, bar(b))
end

ex = :(foo(foo(a, d), bar(d)))
g = EGraph(ex)
saturate!(g, testt)
extract!(g, astsize)

Still errors

[thautwarm]

https://github.com/0x0f0f0f/Metatheory.jl/blob/d6a7aa0783f1b2c6650c45211d6ae875b2333e09/src/EGraphs/ematch.jl#L102

You try to match -b with [- 2 2], and you just accept the results at https://github.com/0x0f0f0f/Metatheory.jl/blob/d6a7aa0783f1b2c6650c45211d6ae875b2333e09/src/EGraphs/ematch.jl#L28

As a result, you fail at getting bound of b in that substitution.

I'd suggest performing the following change:

https://github.com/0x0f0f0f/Metatheory.jl/blob/master/src/EGraphs/ematch.jl#L102

=>

(ariety(n) > 0) && n.head == gethead(t) && length(getargs(t)) == length(n.args) || continue

[0x0f0f0f]

THANKS!