Yield all larger expressions?

[THinnerichs]

Hey there,

Given an initial expression, I want to iterate over equivalent, larger expressions.

comm_monoid = @commutative_monoid (*) 1;
t = @theory a b c begin
  a + 0 --> a
  a --> a + 0
  a + b --> b + a
end
t = comm_monoid ∪ t

g = EGraph(:(x+1))
saturate!(g, t)
extract!(g, astsize)

This returns the EClasses

julia> g.classes
Dict{Int64, EClass} with 3 entries:
  4 => EClass 4 ([ENode(call, +, Expr, [2, 1]), ENode(call, +, Expr, [1, 2])], NamedTuple())
  2 => EClass 2 ([1], NamedTuple())
  1 => EClass 1 ([x], NamedTuple())

1. Now (even though non-sensical in this example), I want to generate bigger expressions using, e.g., a --> a+0. How can I do that?
2. The e-graph only considers operations that were already in the original expression, i.e., +, but ignores all rules w.r.t. multiplication here, e.g. 1*x + 1.
3. Is there an existing implementation for iterating expressions of an e-graph?

[gkronber]

With the ale/3.0 branch the following (saturated) egraph is produced.

julia> g
EGraph{Expr, Nothing} with 4 e-classes:
  1 => [x, %1 + %4, %4 + %1]
  2 => [1, %2 + %4, %4 + %2]
  3 => [%1 + %2, %3 + %4, %2 + %1, %4 + %3]
  4 => [0, %4 + %4]

Note the cycle for example for eclass 4. The egraph is a compact representation of all possible expressions. Metatheory does not provide a way to enumerate all possible expressions from the egraph, but you could implement your own using e.g. breadth-first search starting with a root node.