Predicates not working in egraph

[vitrun]

Predicates work in classical term rewriting, however, fail in equality saturation.

julia> t = [@rule ~x::iseven + ~y --> ~x * ~y]
1-element Vector{RewriteRule}:
 ~(x::iseven) + ~y --> ~x * ~y

julia> Chain(t)(:(2+3))
:(2 * 3)

julia> g = EGraph(:(2+3))
EGraph(IntDisjointSet{Int64}([-1, -1, -1], ...

julia> saturate!(g, t)
ERROR: MethodError: no method matching iseven(::EGraph, ::EClass)
Stacktrace:
  [1] (::Metatheory.EGraphs.Machine)(instr::CheckPredicate, pc::Int64)
    @ Metatheory.EGraphs ~/Work/julia/Metatheory.jl/src/EGraphs/ematch.jl:141
  [2] next(m::Metatheory.EGraphs.Machine, pc::Int64)

[vitrun]

Not quite sure, but is it related with #83?

[overshiki]

Hi @vitrun
One way to do this is to use type predicates combining a where statement:

t = [@rule ~x::Int + ~y::Int --> ~x * ~y where iseven(~x)]

See also #117 for more details

[vitrun]

@overshiki Thanks very much. I should have checked the closed issues.

[vitrun]

@overshiki I experimented and got the following results. The where statement seems not working with symbolic rules. Is it what you expect?

t = [@rule ~x::Int + ~y::Int --> ~x * ~y where {iseven(~x)}]  # egraph wrong
# t = [@rule a b a::Int + b::Int --> 1 where {iseven(a)}]  # egraph wrong

# t = [@rule ~x::Int + ~y::Int => iseven(~x) ? ~x * ~y : nothing]  # ok
# t = [@rule ~x::Int + ~y::Int => ~x * ~y where {iseven(~x)}]  #  invalid variable expression in "where"
# t = [@rule a b a::Int + b::Int => 1 where {iseven(a)}]  # ok
g = EGraph(:(2 + 3))
saturate!(g, t)

[overshiki]

Hi @vitrun
It should be

t = [@rule ~x::Int + ~y::Int --> ~x * ~y where iseven(~x)]

not

t = [@rule ~x::Int + ~y::Int --> ~x * ~y where {iseven(~x)}]

The where statement here is actually not the normal julia statement when declaring a parametric type(in which way you do x::T where {T}), but a DSL in Metatheory.jl, since it is inside a macro call.

[vitrun]

Hi @overshiki , I've tried your version. The where statement becomes part of the RHS. That's what I mean by 'egraph wrong'.

t = [@rule ~x::Int + ~y::Int --> ~x * ~y where iseven(~x)]

Check the visualized graph (ignore the red circle and grey lines):

[overshiki]

Hi @vitrun
This is what I didn't expect! Maybe I'm wrong about the statement.

Could you also try the dynamic version? see if it would make a difference:

t = [@rule x y x::Int + y::Int => :($x * $y) where iseven(x)]

[vitrun]

t = [@rule x y x::Int + y::Int => :($x * $y) where iseven(x)]

It works as expected! Thanks again.

[0x0f0f0f]

Hi @overshiki , I've tried your version. The where statement becomes part of the RHS. That's what I mean by 'egraph wrong'.

t = [@rule ~x::Int + ~y::Int --> ~x * ~y where iseven(~x)]

Check the visualized graph (ignore the red circle and grey lines):

How did you visualize the e-graph?

[vitrun]

@0x0f0f0f I use GraphViz.jl. It's a quick hack and may have bugs

[aabouman]

@0x0f0f0f I use GraphViz.jl. It's a quick hack and may have bugs

Would you mind sharing your code to visualize the EGraphs? I was about to implement the same thing and would love to use it as a starting point

[0x0f0f0f]

@0x0f0f0f I use GraphViz.jl. It's a quick hack and may have bugs

This is interesting. It would be cool to have an extra package to do so. See #41

[vitrun]

@aabouman check https://gist.github.com/vitrun/29aeeb0601419e977c0dfb8db2b00401

[0x0f0f0f]

cc @vitrun see pull request above