Metatheory incorrectly merges e-classes?

[MrVPlusOne]

Hi,

I was trying to figure out why my program synthesizer was producing non-deterministic results when using MT to prune equivalent programs. So far I haven't been able to reproduce the non-deterministic behavior using a minimal working example yet, but I ended up encountering an even stranger behavior, which I'm reporting here.

First, let's define a simple function to enumerate arithmetic expressions up until a given size constraint.

using BenchmarkTools
using Metatheory
using Metatheory.Library

"""
Enumerate arithmatic expressions up until a given size
"""
function all_expressions(size)
    size_map = Dict{Int, Vector{Any}}()
    size_map[0] = []
    size_map[1] = [:a, :b, :c, 1, 0]

    ast_size(::Symbol) = 1
    ast_size(e::Expr) = sum(ast_size, e.args)

    function rec(size)
        get!(size_map, size) do
            exs = []
            for left in 1:size-2
                right = size-1-left
                for (a, b) in Iterators.product(rec(left), rec(right))
                    append!(exs, Expr(:call, op, a, b) for op in [:+, :-, :*, :/])
                end
            end
            exs
        end
    end

    rec.(1:size)
    (s -> size_map[s]).(1:size) |> Iterators.flatten |> collect
end

We can test this with size=5, which produces 4105 terms.

julia> display(all_expressions(5))
4105-element Vector{Any}:
  :a
  :b
  :c
 1
 0
  :(a + a)
  :(a - a)
  :(a * a)
  :(a / a)
  :(b + a)
 ⋮
  :((0 - 0) / 0)
  :(0 * 0 + 0)
  :(0 * 0 - 0)
  :((0 * 0) * 0)
  :((0 * 0) / 0)
  :(0 / 0 + 0)
  :(0 / 0 - 0)
  :((0 / 0) * 0)
  :((0 / 0) / 0)

Now let's define a simple pruning example, which calls equality saturation on the enumerated terms and records the simplest expression in each equivalence class. It also prints out the number of e-classes in the e-graph.

function rewrite_example(size, rules; threaded=true, timeout=2)
    g = EGraph()
    # use SimpleScheduler to ensure that all rules are applied
    params = SaturationParams(;
       scheduler = Metatheory.Schedulers.SimpleScheduler,
       timeout, eclasslimit=0, enodelimit=0, matchlimit=0,
       threaded,
    )
    exps = all_expressions(size)
    # map each expression to its original eclass id.
    exp_map = Dict(map(exps) do e
        eclass, enode = addexpr!(g, e)
        e => eclass.id
    end)

    saturate!(g, rules, params)

    @show g.numclasses

    # use this to record the simplest expression in each eclass
    club = Dict{EClassId, Any}()
    pruned = []

    for e in exps
        e_class = Metatheory.find(g, exp_map[e])
        if !haskey(club, e_class)
            club[e_class] = e
        else
            push!(pruned, (pruned=e, by=club[e_class]))
        end
    end
    (; club, pruned)
end

Now, calling this with a simple set of rules seems to be giving reasonable results.

simple_rules = commutative_monoid(:(*), 1) ∪ commutative_monoid(:(+), 0)
rewrite_example(5, simple_rules)

Which prints out g.numclasses = 1999.

However, if we add these 3 more rules

# now this is problamtic
more_rules = @theory begin
    (a * b) + (a * c) => a * (b + c)

    (a / a) => 1

    a / b => a * reciprocal(b)
end
club, pruned = rewrite_example(5, simple_rules ∪ more_rules)
display(values(club))
display(pruned)

Now it produces nonsensical results:

g.numclasses = 10
ValueIterator for a Dict{Int64, Any} with 5 entries. Values:
  :(a - (a - a))
  :(a / (a - a))
  :(a - a)
  :a
  :((a - a) - a)
4100-element Vector{Any}:
 (pruned = :b, by = :a)
 (pruned = :c, by = :a)
 (pruned = 1, by = :a)
 (pruned = 0, by = :a)
 (pruned = :(a + a), by = :a)
 (pruned = :(a * a), by = :a)
 (pruned = :(a / a), by = :a)
 (pruned = :(b + a), by = :a)
 (pruned = :(b - a), by = :(a - a))
 (pruned = :(b * a), by = :a)
 ⋮
 (pruned = :((0 - 0) / 0), by = :(a - a))
 (pruned = :(0 * 0 + 0), by = :a)
 (pruned = :(0 * 0 - 0), by = :(a - a))
 (pruned = :((0 * 0) * 0), by = :a)
 (pruned = :((0 * 0) / 0), by = :a)
 (pruned = :(0 / 0 + 0), by = :a)
 (pruned = :(0 / 0 - 0), by = :(a - a))
 (pruned = :((0 / 0) * 0), by = :a)
 (pruned = :((0 / 0) / 0), by = :a)

Somehow adding these 3 rules caused only 10 e-classes left in the final e-graph. (This happens regardless of whether threaded=true or false.) I also noticed that in the final kept expressions, :(a - a) is kept as the simplest expression in its e-class as opposed to 0 (I also see this behavior a lot in my synthesizer.)

Any idea what might be causing this? Thanks!

[0x0f0f0f]

Hi Jiayi, what version of MT are you using? I will try to replicate when I'm back at my computer.

[0x0f0f0f]

First thing I see that you are not adding any specific rule about the - operator. Metatheory.jl does not implicitly handle the relationship between + and -. They are just treated as purely syntactic symbols. The commutative_monoid utility functions just creates a bunch of rules (you can print them out to see them in detail)

[MrVPlusOne]

Hi Alessandro,

I'm using the version right before the latest update on master (the one that adds Rewriters into the dependency). I tried to also test this with the latest version, but it looks like Rewriters is not on the General Registry yet so Pkg could not resolve a valid version.

[0x0f0f0f]

Rewriters should be on the general registry now but it's not yet used by the egraphs module

[MrVPlusOne]

First thing I see that you are not adding any specific rule about the - operator. Metatheory.jl does not implicitly handle the relationship between + and -. They are just treated as purely syntactic symbols. The commutative_monoid utility functions just creates a bunch of rules (you can print them out to see them in detail)

Ah, you are right! Adding the rule a - a => 0 does fix that problem, but unfortunately, now all the expressions are merged into a single class:

julia> more_rules = @theory begin
           a - a => 0

           (a * b) + (a * c) => a * (b + c)

           (a / a) => 1

           a / b => a * reciprocal(b)
       end
       club, pruned = rewrite_example(5, simple_rules ∪ more_rules, threaded=false)
       display(values(club))
       display(pruned)
g.numclasses = 6
ValueIterator for a Dict{Int64, Any} with 1 entry. Values:
  :a
4104-element Vector{Any}:
 (pruned = :b, by = :a)
 (pruned = :c, by = :a)
 (pruned = 1, by = :a)
 (pruned = 0, by = :a)
 (pruned = :(a + a), by = :a)
 (pruned = :(a - a), by = :a)
 (pruned = :(a * a), by = :a)
 (pruned = :(a / a), by = :a)
 (pruned = :(b + a), by = :a)
 (pruned = :(b - a), by = :a)
 ⋮
 (pruned = :((0 - 0) / 0), by = :a)
 (pruned = :(0 * 0 + 0), by = :a)
 (pruned = :(0 * 0 - 0), by = :a)
 (pruned = :((0 * 0) * 0), by = :a)
 (pruned = :((0 * 0) / 0), by = :a)
 (pruned = :(0 / 0 + 0), by = :a)
 (pruned = :(0 / 0 - 0), by = :a)
 (pruned = :((0 / 0) * 0), by = :a)
 (pruned = :((0 / 0) / 0), by = :a)

[0x0f0f0f]

That seems like a serious problem. I hope it is caused by a wrong return in a top-level exposed API function. What happens if you display(egraph.classes)?

[MrVPlusOne]

classes seems to be consistent with numclasses:

g.numclasses = 6
Classes: 
Dict{Int64, Metatheory.EGraphs.EClass} with 6 entries:
  6    => EClass 6 ([ENode{Symbol}(+)])
  10   => EClass 10 ([ENode{Symbol}(*)])
  4636 => EClass 4636 ([ENode{Expr}(call 6 4636 2004), ENode{Expr}(call 6 2004 4636), ENode{Expr}(call 10 4636 4636), ENode{Int64}(1), ENode{Expr}(c…
  12   => EClass 12 ([ENode{Symbol}(/)])
  5105 => EClass 5105 ([ENode{Symbol}(reciprocal)])
  8    => EClass 8 ([ENode{Symbol}(-)])

[0x0f0f0f]

I agree that this result is mostly nonsensical and that has to be fixed ASAP. Could you help me out investigating/debugging while I'm not home? Tomorrow I will have only a few hours to take a look.

[0x0f0f0f]

Can you try syncing to latest commit on master and delete your Manifest.toml and re-resolve?

[0x0f0f0f]

A first step for debugging could also be printing the matches and merges to see what is going on, for example trying to look what causes 1 to be set equal to :a . What happens if you build n different egraphs and simplify one at a time?

[MrVPlusOne]

I agree that this result is mostly nonsensical and that has to be fixed ASAP. Could you help me out investigating/debugging while I'm not home? Tomorrow I will have only a few hours to take a look.

Sure, I'll try the steps you mentioned.

for example trying to look what causes 1 to be set equal to :a

What would be the best way to track these merges? BTW, I was actually trying to implement some utilities to generate a series of rewrites as proofs of equivalence (which I later realized you have also tried this before), but that turned to be quite involved and I haven't got a satisfying result yet. I think I have finally figured out an algorithm that might actually work, but I haven't got the time to try that out yet, and I'm also not sure how bad the resulting proofs would look (it might produce very long and redundant rewrite steps).

[MrVPlusOne]

Can you try syncing to latest commit on master and delete your Manifest.toml and re-resolve?

(Metatheory) pkg> resolve
ERROR: expected package `Rewriters [1df27592]` to be registered

Looks like Rewrites is still not registered. Which link did you use to download it locally?

[0x0f0f0f]

I released the package myself on registry. Are you sure your local copy of the registry is up to date? I had to remove it by hand and re-download it a few days ago.

[0x0f0f0f]

for example trying to look what causes 1 to be set equal to :a

What would be the best way to track these merges?

print the merges in src/Egraphs/saturation/apply.jl

[0x0f0f0f]

that's how i (naively) debugged those issues

[MrVPlusOne]

for example trying to look what causes 1 to be set equal to :a

What would be the best way to track these merges?

print the merges in src/Egraphs/saturation/apply.jl

Hmm... that sounds challenging for large graphs like this one, but I can certainly give it a try. The annoying thing is, I haven't been able to reproduce this bug on smaller graphs yet. If I change the maximal AST size from 5 to 3, then it no longer merges everything into one class. If I delete any of the 3 additional rules, it also stops happening. This seems to suggest that it requires the AST to be deep enough to happen, which probably has something to do with the distributive rule.

[MrVPlusOne]

I released the package myself on registry. Are you sure your local copy of the registry is up to date? I had to remove it by hand and re-download it a few days ago.

Updating the registry did help, but now it's printing this error:

Any quick fix for this?

[MrVPlusOne]

Sorry accidentally hit the close issue button.

[MrVPlusOne]

Any quick fix for this?

Ok never mind. Deleting the manifest solved the issue. :)

[0x0f0f0f]

for example trying to look what causes 1 to be set equal to :a

What would be the best way to track these merges?

print the merges in src/Egraphs/saturation/apply.jl

Hmm... that sounds challenging for large graphs like this one, but I can certainly give it a try. The annoying thing is, I haven't been able to reproduce this bug on smaller graphs yet. If I change the maximal AST size from 5 to 3, then it no longer merges everything into one class. If I delete any of the 3 additional rules, it also stops happening. This seems to suggest that it requires the AST to be deep enough to happen, which probably has something to do with the distributive rule.

This is just super weird. Might be useful to do a Chtulhu.jl madness descent and a debug with breakpoints printing what is going on in the function call parameters inside saturation. Only issue is that this thing is huge to debug and might take ages. I can try to summon @philzook58. Phil if you have any insight or idea about what might cause this it would be of great help.

[0x0f0f0f]

What happens if the depth is set to 4? What about if you just fill the egraph with a slice of the total input exprs? Is there any cutoff number of input expressions where this happens? Can we find any other cutoff number (num of eclasses, num of enodes etc...) that might suggest the source of this issue?

[MrVPlusOne]

What happens if the depth is set to 4?

In this particular case, since I'm only building binary expressions, ast_size=4 would be equivalent to ast_size=3.

What about if you just fill the egraph with a slice of the total input exprs? Is there any cutoff number of input expressions where this happens? Can we find any other cutoff number (num of eclasses, num of enodes etc...) that might suggest the source of this issue?

Yeah, I can try to further reduce the egraph size. Maybe it's easier to see what's going on if we can make this happen in a smaller graph.

I'm pasting the entire example below so that you can also locally test it on your side.

using BenchmarkTools
using Metatheory
using Metatheory.Library

"""
Enumerate arithmatic expressions up until a given size
"""
function all_expressions(size)
    size_map = Dict{Int, Vector{Any}}()
    size_map[0] = []
    size_map[1] = [:a, :b, :c, 1, 0]

    ast_size(::Symbol) = 1
    ast_size(e::Expr) = sum(ast_size, e.args)

    function rec(size)
        get!(size_map, size) do
            exs = []
            for left in 1:size-2
                right = size-1-left
                for (a, b) in Iterators.product(rec(left), rec(right))
                    append!(exs, Expr(:call, op, a, b) for op in [:+, :-, :*, :/])
                end
            end
            exs
        end
    end

    rec.(1:size)
    (s -> size_map[s]).(1:size) |> Iterators.flatten |> collect
end

function rewrite_example(size, rules; threaded=true, timeout=2)
    g = EGraph()
    # use SimpleScheduler to ensure that all rules are applied
    params = SaturationParams(;
       scheduler = Metatheory.Schedulers.SimpleScheduler,
       timeout, eclasslimit=0, enodelimit=0, matchlimit=0,
       threaded,
    )
    exps = all_expressions(size)
    # map each expression to its original eclass id.
    exp_map = Dict(map(exps) do e
        eclass, enode = addexpr!(g, e)
        e => eclass.id
    end)

    saturate!(g, rules, params)

    @show g.numclasses
    # println("Classes: ")
    # display(g.classes)

    # use this to record the simplest expression in each eclass
    club = Dict{EClassId, Any}()
    pruned = []

    for e in exps
        e_class = Metatheory.find(g, exp_map[e])
        if !haskey(club, e_class)
            club[e_class] = e
        else
            push!(pruned, (pruned=e, by=club[e_class]))
        end
    end
    (; club, pruned)
end
##

display(all_expressions(5))

simple_rules = commutative_monoid(:(*), 1) ∪ commutative_monoid(:(+), 0)
rewrite_example(5, simple_rules)

# now this is problamtic
more_rules = @theory begin
    a - a => 0

    (a * b) + (a * c) => a * (b + c)

    (a / a) => 1

    # a / b => a * reciprocal(b)
end
club, pruned = rewrite_example(5, simple_rules ∪ more_rules, threaded=false)
display(values(club))
display(pruned)
##

[0x0f0f0f]

Another simpler idea to see what is going on might be printing the egraph classes with display before and after each equality saturation step that might affect the merges to understand if it is happening in application (because of wrong matches?) or in rebuilding because of a more fundamental bug (hope not)

[0x0f0f0f]

Thanks. Will try tomorrow!!

[MrVPlusOne]

Thanks. Will try tomorrow!!

Thanks for the help! I actually also need to head out now, but I may be able to work on this later tonight. BTW, do you think using an egraph analysis can help in this case? Maybe I can start by adding an inequality assertion?

[0x0f0f0f]

yep good idea equalities stop the saturation eagerly when detected

[MrVPlusOne]

I have managed to reproduce the problem using a smaller egraph. We can actually get rid of the variables :a, :b, :c and only use 1 and 0 to cause the same behavior. This reduces the number of expressions from 4100 to 274.

I also added a temporary check on the egraph by adding a graph_check::Function field to EGraph and call it in eqsat_step! and eqsat_apply! (immediately after each rule application), like shown below

in eqsat_step!

    g.graph_check("Before apply (iter=$curr_iter)")  # added this
    @timeit report.to "Apply" eqsat_apply!(g, matches, report, params)

    # union!(match_hist, matches)

    if report.reason === nothing && cansaturate(scheduler) && isempty(g.dirty)
        report.reason = Saturated()
    end
    @timeit report.to "Rebuild" rebuild!(g)
    g.graph_check("After rebuild (iter=$curr_iter)")  #  added this

in eqsat_apply

        halt_reason = rule(g, match)
        g.graph_check((; match))   # added this
        if (halt_reason !== nothing)
            rep.reason = halt_reason
            return 
        end 

Then, using the following updated example code

using BenchmarkTools
using Metatheory
using Metatheory.Library

"""
Enumerate arithmatic expressions up until a given size
"""
function all_expressions(size)
    size_map = Dict{Int, Vector{Any}}()
    size_map[0] = []
    size_map[1] = [0, 1]

    ast_size(::Symbol) = 1
    ast_size(e::Expr) = sum(ast_size, e.args)

    function rec(size)
        get!(size_map, size) do
            exs = []
            for left in 1:size-2
                right = size-1-left
                for (a, b) in Iterators.product(rec(left), rec(right))
                    append!(exs, Expr(:call, op, a, b) for op in [:+, :-, :*, :/])
                end
            end
            exs
        end
    end

    rec.(1:size)
    (s -> size_map[s]).(1:size) |> Iterators.flatten |> collect
end

function rewrite_example(exps, rules; 
        check_noteq::Union{Nothing, Tuple{EClassId, EClassId}}=nothing, 
        threaded=true, timeout=2)
    g = EGraph()
    # use SimpleScheduler to ensure that all rules are applied
    params = SaturationParams(;
       scheduler = Metatheory.Schedulers.SimpleScheduler,
       timeout, eclasslimit=0, enodelimit=0, matchlimit=0,
       threaded,
    )
    # map each expression to its original eclass id.
    exp_map = Dict(map(exps) do e
        eclass, enode = addexpr!(g, e)
        e => eclass.id
    end)

    # this checks if the two given expressions are equal and will throw an error and print out some graph info if they do.
    function graph_check(info)
        if check_noteq !== nothing
            e1, e2 = check_noteq
            i1, i2 = exp_map[e1], exp_map[e2]
            if find(g, i1) == find(g, i2) 
                classes = sort(collect(pairs(g.classes)), by=x->x[1])
                classes_str = join(classes, "\n")
                @error "$e1 equaled to $e2" info
                println("All classes: ")
                println(classes_str)
                error("graph check failed.")
            end
        end
    end
    g.graph_check = graph_check

    saturate!(g, rules, params)

    @show g.numclasses

    # use this to record the simplest expression in each eclass
    club = Dict{EClassId, Any}()
    pruned = []

    for e in exps
        e_class = Metatheory.find(g, exp_map[e])
        if !haskey(club, e_class)
            club[e_class] = e
        else
            push!(pruned, (pruned=e, by=club[e_class]))
        end
    end
    (; club, pruned)
end
##

display(all_expressions(5))

# this is ok
simple_rules = commutative_monoid(:(*), 1) ∪ commutative_monoid(:(+), 0)
rewrite_example(all_expressions(5), simple_rules)

# now this is problamtic
more_rules = @theory begin
    a - a => 0

    (a * b) + (a * c) => a * (b + c)

    (a / a) => 1

    a / b => a * reciprocal(b)
end

club, pruned = rewrite_example(all_expressions(5), simple_rules ∪ more_rules, 
    threaded=false, timeout=2, check_noteq=(1, 0))
display(values(club))
display(pruned)

I can detect that 1 becomes equal to 0 immediately after a rule application of a/b => a*reciprocal(b), the error is shown below:

┌ Error: 1 equaled to 0
│   info = (match = Metatheory.EGraphs.Match(a / b => a * reciprocal(b), a * reciprocal(b), Metatheory.EGraphs.Sub(ENode{Expr}(call 9 177 289), [177, 289], Union{Nothing, Metatheory.EGraphs.ENode}[nothing, nothing]), 360),)
└ @ Main.Playground ~/.julia/dev/SEDL/scripts/metatheory_bug.jl:59
All classes: 
3 => EClass 3 ([ENode{Symbol}(+)])
5 => EClass 5 ([ENode{Symbol}(-)])
7 => EClass 7 ([ENode{Symbol}(*)])
9 => EClass 9 ([ENode{Symbol}(/)])
40 => EClass 40 ([ENode{Expr}(call 5 289 177)])
44 => EClass 44 ([ENode{Expr}(call 5 249 177)])
64 => EClass 64 ([ENode{Expr}(call 5 289 69)])
65 => EClass 65 ([ENode{Expr}(call 7 289 69), ENode{Expr}(call 7 69 289), ENode{Expr}(call 7 65 249), ENode{Expr}(call 7 249 65)])
68 => EClass 68 ([ENode{Expr}(call 5 249 69)])
... more omitted ...

But the EGraph is still not very readable to me, and this only shows the egraph immediately after applying the rule, it might be helpful to also show its state before the application, which can probably be achieved by copying the classes immediately before each rule application. Anyway, I'm pasting my progress here, and hopefully, it can help you pinpoint the root cause.

[0x0f0f0f]

From @yihozhang

Yihong Zhang, [08.09.21 06:35]
Actually, I'm not too surprised that it generates very few e-classes, because the rule a / a => 1 is not arithmetically sound if a equals 0, and this rule can interacts with other rules

Yihong Zhang, [08.09.21 06:36]
I'm having a hard time giving a concrete trace of how it goes wrong, but I suspect it's the case (one could probably verify that in egg it will produce something similar)

Yihong Zhang, [08.09.21 06:41]
Okay here is an example

Yihong Zhang, [08.09.21 06:41]
First we have
0/0=1
0/0=0*reciprocal(0)
1/0=1*reciprocal(0)

Yihong Zhang, [08.09.21 06:42]
0/0+1/0 = 0*reciprocal(0) + 1*reciprocal(0)
        = (0+1)*reciprocal(0)
        = 1*reciprocal(0) 
        = 1/0

Yihong Zhang, [08.09.21 06:43]
Because 0/0=1, we proved something like 1+a=a

Yihong Zhang, [08.09.21 06:45]
And you can have many other weird things happening following this line of reasoning, and at the end of the day arithmetics fails :)

[0x0f0f0f]

Removing the a / a => 1 rule seems to solve this :)

[0x0f0f0f]

more_rules = @theory begin
    a - a => 0

    (a * b) + (a * c) => a * (b + c)

    (a / a) |> begin 
        b, n = addexpr!(_egraph, 0)
        if in_same_class(_egraph, a, b)
            return _lhs_expr
        else 
            return 1
        end
    end

    a / b => a * reciprocal(b)
end

Does this solve the issue? A predicate system should be added in the near future to do things like:

notzero(g::EGraph, x::EClass) = !in_same_class(first(addexpr!(g, 0)), x)
notzero(x) = (x != zero(x))

a / a::notzero => 1

See https://github.com/JuliaSymbolics/SymbolicUtils.jl/issues/355

[0x0f0f0f]

In the original example i now get 2419 pruned expressions and 1686 expressions in club. :)

[MrVPlusOne]

Thanks so much for looking into this! After reading @yihozhang's explanation, it all makes sense now! I didn't expect 0 is so tricky to deal with (and it also breaks the physical unit type system that I was using :( )

I'm not 100% sure the new solution completely fixes the problem, though. Looks like it's saying that we will not apply a/a=>1 only if we have already proved a == 0. What happens if we haven't proved e==0 for some big expression e? Does this mean that we could still incorrectly apply this rule to e/e when, say, e=a+b+c*0-b-a and the e-graph does not know e will become 0 in later iterations? Do we need to somehow change to rule to 'only apply when we can prove a != 0', like using an e-graph analysis?

[0x0f0f0f]

Yes, using an egraph analysis may be the way to go. The other simpler solution is breaking the saturation down in many subsequent steps (building n egraphs for n steps), each one with a different theory of rules in order to give some sort of "ordering". This way you could apply all the rules that prove that things are equal to zero first, and then you could apply all the rules that need the guarantee that some things must be (not) equal to zero. Closing ;)

[MrVPlusOne]

Hi @yihozhang,

By any chance you can construct an example to explain why these rules could cause two distinct variables like :a and :b to become equal? I'm trying to gain a deeper intuition on why this failed and figure out a way to prevent this type of error in the future. And I think the example you gave only proves something like 1+a/0=a/0, which if you think about it, actually can make some sense (e.g., when a!=0, both the LHS and RHS becomes Inf). I still couldn't see how this type of error can cause all expressions to be merged into a single e-class, as happened in my first example where there are also 3 variables?

[yihozhang]

Hey @MrVPlusOne, in general, I think if the background theory is not sound, any false claim can be proved. In this case, since we proved 1+0/0=0/0 (by substituting a for 0) and 0/0=1, we proved 1+1=1, so (1+1)*a=1*a by congruence, thus a+a=a, and so is a+a+...+a=a.

[MrVPlusOne]

Thanks for the explaination, @yihozhang! I get it that in logic, if we can prove a contradiction, we can use it to prove anything. Altough I was not sure how often this would happen in equality saturation. It feels like it's going to be really hard to completely avoid unsound rules without significantly reducing the number of applicable simplifications? I wonder what's the standard way to deal with this type of situation in e-graph based approaches? Maybe I can try to add some concrete examples as additional checks like they did in http://arxiv.org/abs/2108.10436?