Fix matching of literals in dynamic rules #258
Conversation
|
Codecov ReportAll modified and coverable lines are covered by tests ✅
❗ Your organization needs to install the Codecov GitHub app to enable full functionality. Additional details and impacted files@@ Coverage Diff @@
## ale/3.0 #258 +/- ##
===========================================
- Coverage 81.42% 81.34% -0.09%
===========================================
Files 19 19
Lines 1497 1501 +4
===========================================
+ Hits 1219 1221 +2
- Misses 278 280 +2 ☔ View full report in Codecov by Sentry. |
Benchmark Results
Benchmark PlotsA plot of the benchmark results have been uploaded as an artifact to the workflow run for this PR. |
| @@ -144,15 +144,11 @@ 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) | |||
There was a problem hiding this comment.
This could introduce a hash collision if the hash of some literal value is 0
There was a problem hiding this comment.
True.
Alternative: we could set v_pair_first to a negative or zero value to indicate that this is a literal match, because we do not need the eclassid for literals when we return the hashvalue in v_pair_last.
There was a problem hiding this comment.
Zero value would work I believe
There was a problem hiding this comment.
Tried to change it, but appearently we require the ecid (for literal matches) for this function:
instantiate_enode!(bindings, @nospecialize(g::EGraph), p::PatVar)::Id = v_pair_first(bindings[p.idx])There was a problem hiding this comment.
I think it would be extremly unlikely to produce a hash collision as the number of literals is expected to be small compared to the number of enodes.
There was a problem hiding this comment.
I thought a bit more about the hash collision argument. If we are concerned about hash collisions for literals, then we would need to change the definition of the egraph type, and all handling of literals, as we always just use the hash for literals.
mutable struct EGraph{ExpressionType,Analysis}
...
"Hashcons the constants in the e-graph"
constants::Dict{UInt64,Any}
...
end
| quote | ||
| id = $(Symbol(:σ, addr)) | ||
| eclass = g[id] | ||
| node_idx = $(Symbol(:enode_idx, addr)) - 1 |
There was a problem hiding this comment.
We can probably get rid of the idx thing and just store the hash?
There was a problem hiding this comment.
You mean to track hashes instead of enode_idxs in the pattern matcher?
Seems not straight-forward as the ematcher seems to require the enode_idxs.
There was a problem hiding this comment.
I am thinking about this a bit, and we probably don't need the indexes, but just the hashes. If so, we could also avoid using UInt128 in the buffer and pairing e-class ids with indexes in the buffer. As usual, if an element of the buffer has all bits set to 1 then it's a delimiter between different matches (of many variables). If it has all bits set to 0 then it could simply be discarded and signal eqsat_apply! that the next element is a literal hash and not an e-class ID.
I can experiment and push to a branch :)
The literal_position returned by the ematcher may be invalidated by merging of two eclasses in another rule.
This PR changes the ematcher rules to always return the hash of the enode (even for literals).