Skip to content

Commit

Permalink
Bugfix: ematcher now returns hash of constants instead of index of en…
Browse files Browse the repository at this point in the history 
…ode in class when using type predicates in dynamic rules.
  • Loading branch information
@gkronber
gkronber committed Oct 6, 2024
1 parent 72ff196 commit 7dd5848
Show file tree
Hide file tree
Showing 2 changed files with 14 additions and 6 deletions.
8 changes: 3 additions & 5 deletions src/EGraphs/saturation.jl
View file
Original file line number Diff line number Diff line change
Expand Up @@ -144,14 +144,12 @@ end
Instantiate argument for dynamic rule application in e-graph
"""
function instantiate_actual_param!(bindings, g::EGraph, i)
const_hash = v_pair_last(bindings[i])
const_hash == 0 || return get_constant(g, const_hash)

ecid = v_pair_first(bindings[i])
literal_position = reinterpret(Int, v_pair_last(bindings[i]))
ecid <= 0 && error("unbound pattern variable")
eclass = g[ecid]
if literal_position > 0
@assert !v_isexpr(eclass[literal_position])
return get_constant(g, v_head(eclass[literal_position]))
end
return eclass
end

Expand Down
12 changes: 11 additions & 1 deletion src/ematch_compiler.jl
View file
Original file line number Diff line number Diff line change
Expand Up @@ -326,7 +326,17 @@ end

function yield_expr(patvar_to_addr, direction)
push_exprs = [
:(push!(ematch_buffer, v_pair($(Symbol(:σ, addr)), reinterpret(UInt64, $(Symbol(:enode_idx, addr)) - 1)))) for
quote
id = $(Symbol(:σ, addr))
eclass = g[id]
node_idx = $(Symbol(:enode_idx, addr)) - 1
if node_idx == 0
push!(ematch_buffer, v_pair(id, reinterpret(UInt64, 0)))
else
n = eclass.nodes[node_idx]
push!(ematch_buffer, v_pair(id, v_head(n)))
end
end for
addr in patvar_to_addr
]
quote
Expand Down

4 comments on commit 7dd5848

@olynch
Copy link
Collaborator

@olynch olynch commented on 7dd5848 Oct 11, 2024

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This looks reasonable to me and this looks like it solves the issue, but I guess the larger issue is that we need documentation for exactly what the UInt128s pushed to the ematch_buffer are supposed to represent? This is what caused the issue in the first place, because I think different bits of code were making slightly different assumptions.

@gkronber
Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yes, it is potentially confusing.
I have the feeling that this could be the cause for failing tests in CAS and lambda_theory

@0x0f0f0f
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Is there a PR for this? @gkronber

@gkronber
Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Not sure what you mean. There is one remaining failing test for CAS.
This change is included in #249 . If necessary I can prepare the changes for ematch_compiler in a separate branch.

Please sign in to comment.