Question regarding false and 0 in E-graphs

[ViciousDoormat]

Hello,

The following rewrite rules and E-graph saturation process:

t = @theory a begin
  false --> 0 ≥ 1
end

g = EGraph{Expr, Nothing}(:(false))
saturate!(g, t)
println(g)

result in the following E-graph:

EGraph{Expr, Nothing} with 2 e-classes:
  1 => [0, %1 ≥ %2]
  2 => [1]

As you can see, it puts 0 and false in the same class. This makes sense because in julia 0 == false returns true.
However, is there a way to make sure 0 and false do not end up in the same class?
I tried adding the type Bool to false, but when I do that, it just does not apply the rule anymore.

[0x0f0f0f]

You can wrap it in a custom struct, without implementing any TermInterface method. It should treat it as a different constant

[ViciousDoormat]

Do you mean something like:

struct BoolWrapper
  value::Bool
end

t = @theory a begin
  BoolWrapper(false) --> 0 ≥ 1
end

g = EGraph{Expr, Nothing}(:(BoolWrapper(false)))
saturate!(g, t)
println(g)

This results in:

EGraph{Expr, Nothing} with 3 e-classes:
  1 => [0]
  3 => [1]
  4 => [%1 ≥ %3, BoolWrapper(%1)]

It still sees 0 and false as the same thing, but does see BoolWrapper(false) as what I want false to be.

However, I could just as well define my own symbol :not_true instead of BoolWrapper(false) in this case, which is also basically my current solution.

[ViciousDoormat]

Just an idea:
My assumption as to why this happens is because in Julia false == 0. I do not know where exactly in MT during the saturation process this is relevant, but could it be possible to make MT use comparisons based on === for certain rules, as false === 0 returns false?

[0x0f0f0f]

Just an idea:
My assumption as to why this happens is because in Julia false == 0. I do not know where exactly in MT during the saturation process this is relevant, but could it be possible to make MT use comparisons based on === for certain rules, as false === 0 returns false?

That would be possible, but a bit more challenging. Let me look into it

[gkronber]

@0x0f0f0f the problem in the saturation process is mainly this:

julia> hash(false)
0x77cfa1eef01bca90

julia> hash(0)
0x77cfa1eef01bca90