From 781109597c61aeade2bdd7fb3bfcf4428bcb70c0 Mon Sep 17 00:00:00 2001 From: Gabriel Kronberger Date: Tue, 10 Sep 2024 12:42:19 +0200 Subject: [PATCH 1/9] Fix operation --- test/integration/stream_fusion.jl | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/test/integration/stream_fusion.jl b/test/integration/stream_fusion.jl index 5b24d3e7..b119c069 100644 --- a/test/integration/stream_fusion.jl +++ b/test/integration/stream_fusion.jl @@ -49,7 +49,7 @@ fold_theory = @theory x y z begin x::Number * y::Number => x * y x::Number + y::Number => x + y x::Number / y::Number => x / y - x::Number - y::Number => x / y + x::Number - y::Number => x - y # etc... end From 8cc9c880170725855ae0b1e95b0656b9d08346bc Mon Sep 17 00:00:00 2001 From: Gabriel Kronberger Date: Tue, 10 Sep 2024 12:45:25 +0200 Subject: [PATCH 2/9] Add missing modify call after updating eclass analysis --- src/EGraphs/egraph.jl | 1 + 1 file changed, 1 insertion(+) diff --git a/src/EGraphs/egraph.jl b/src/EGraphs/egraph.jl index 5937ddad..40b51259 100644 --- a/src/EGraphs/egraph.jl +++ b/src/EGraphs/egraph.jl @@ -361,6 +361,7 @@ function Base.union!( ) g.classes[id_1] = new_eclass + modify!(g, new_eclass) return true end From 26530750c41d8be0cd51fc75306ed9800df4b78b Mon Sep 17 00:00:00 2001 From: Gabriel Kronberger Date: Tue, 10 Sep 2024 12:50:31 +0200 Subject: [PATCH 3/9] Only update eclass analysis if the new analysis != nothing --- src/EGraphs/egraph.jl | 25 +++++++++++++------------ 1 file changed, 13 insertions(+), 12 deletions(-) diff --git a/src/EGraphs/egraph.jl b/src/EGraphs/egraph.jl index 40b51259..93954eda 100644 --- a/src/EGraphs/egraph.jl +++ b/src/EGraphs/egraph.jl @@ -426,21 +426,22 @@ function process_unions!(g::EGraph{ExpressionType,AnalysisType})::Int where {Exp eclass = g.classes[eclass_id_key] node_data = make(g, node) - if !isnothing(eclass.data) - joined_data = join(eclass.data, node_data) - - if joined_data != eclass.data - g.classes[eclass_id_key] = EClass{AnalysisType}(eclass_id, eclass.nodes, eclass.parents, joined_data) - # eclass.data = joined_data + if !isnothing(node_data) + if !isnothing(eclass.data) + joined_data = join(eclass.data, node_data) + + if joined_data != eclass.data + g.classes[eclass_id_key] = EClass{AnalysisType}(eclass_id, eclass.nodes, eclass.parents, joined_data) + # eclass.data = joined_data + modify!(g, eclass) + append!(g.analysis_pending, eclass.parents) + end + else + g.classes[eclass_id_key] = EClass{AnalysisType}(eclass_id, eclass.nodes, eclass.parents, node_data) + # eclass.data = node_data modify!(g, eclass) - append!(g.analysis_pending, eclass.parents) end - else - g.classes[eclass_id_key] = EClass{AnalysisType}(eclass_id, eclass.nodes, eclass.parents, node_data) - # eclass.data = node_data - modify!(g, eclass) end - end end n_unions From 4cb1dc642eff87e681b704bde739ccb9a682ed48 Mon Sep 17 00:00:00 2001 From: Gabriel Kronberger Date: Tue, 10 Sep 2024 12:52:01 +0200 Subject: [PATCH 4/9] Queue update of parents when analysis of eclass is updated (even when it was nothing) --- src/EGraphs/egraph.jl | 1 + 1 file changed, 1 insertion(+) diff --git a/src/EGraphs/egraph.jl b/src/EGraphs/egraph.jl index 93954eda..a4f0e5f3 100644 --- a/src/EGraphs/egraph.jl +++ b/src/EGraphs/egraph.jl @@ -440,6 +440,7 @@ function process_unions!(g::EGraph{ExpressionType,AnalysisType})::Int where {Exp g.classes[eclass_id_key] = EClass{AnalysisType}(eclass_id, eclass.nodes, eclass.parents, node_data) # eclass.data = node_data modify!(g, eclass) + append!(g.analysis_pending, eclass.parents) end end end From cd064e67d5b06045aaef350b43acef6ed48b7375 Mon Sep 17 00:00:00 2001 From: Gabriel Kronberger Date: Tue, 10 Sep 2024 12:56:54 +0200 Subject: [PATCH 5/9] Move statement into bidirection conditional as it is only required for bidirectional rules --- src/EGraphs/saturation.jl | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/EGraphs/saturation.jl b/src/EGraphs/saturation.jl index 41b2702f..fcc3555f 100644 --- a/src/EGraphs/saturation.jl +++ b/src/EGraphs/saturation.jl @@ -86,9 +86,8 @@ function eqsat_search!( @debug "$rule is banned" continue end - ids_left = cached_ids(g, rule.left) - ids_right = is_bidirectional(rule) ? cached_ids(g, rule.right) : UNDEF_ID_VEC + ids_left = cached_ids(g, rule.left) for i in ids_left cansearch(scheduler, rule_idx, i) || continue n_matches += rule.ematcher_left!(g, rule_idx, i, rule.stack, ematch_buffer) @@ -96,6 +95,7 @@ function eqsat_search!( end if is_bidirectional(rule) + ids_right = cached_ids(g, rule.right) for i in ids_right cansearch(scheduler, rule_idx, i) || continue n_matches += rule.ematcher_right!(g, rule_idx, i, rule.stack, ematch_buffer) From f8d82ebf57f84bfce7b6c502582791d29d0acf44 Mon Sep 17 00:00:00 2001 From: Gabriel Kronberger Date: Tue, 10 Sep 2024 12:59:29 +0200 Subject: [PATCH 6/9] Fix access to ematch buffer elements --- src/utils.jl | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/utils.jl b/src/utils.jl index 2e03b08d..377132e5 100644 --- a/src/utils.jl +++ b/src/utils.jl @@ -36,7 +36,7 @@ function buffer_readable(g, limit, ematch_buffer) k = length(ematch_buffer) while k > limit - delimiter = ematch_buffer[k] + delimiter = ematch_buffer.v[k] @assert delimiter == 0xffffffffffffffffffffffffffffffff n = k - 1 @@ -44,19 +44,19 @@ function buffer_readable(g, limit, ematch_buffer) n_elems = 0 for i in n:-1:1 n_elems += 1 - if ematch_buffer[i] == 0xffffffffffffffffffffffffffffffff + if ematch_buffer.v[i] == 0xffffffffffffffffffffffffffffffff n_elems -= 1 next_delimiter_idx = i break end end - match_info = ematch_buffer[next_delimiter_idx + 1] + match_info = ematch_buffer.v[next_delimiter_idx + 1] id = v_pair_first(match_info) rule_idx = reinterpret(Int, v_pair_last(match_info)) rule_idx = abs(rule_idx) - bindings = @view ematch_buffer[(next_delimiter_idx + 2):n] + bindings = @view ematch_buffer.v[(next_delimiter_idx + 2):n] print("$id E-Classes: ", map(x -> reinterpret(Int, v_pair_first(x)), bindings)) print(" Nodes: ", map(x -> reinterpret(Int, v_pair_last(x)), bindings), "\n") From a252b32ee0f2f75ae55138385c735b4f4d52e338 Mon Sep 17 00:00:00 2001 From: Gabriel Kronberger Date: Wed, 25 Sep 2024 10:19:05 +0200 Subject: [PATCH 7/9] Add a test case for dynamic rule predicates with where (mentioned in docs, but no test case yet) --- test/egraphs/ematch.jl | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/test/egraphs/ematch.jl b/test/egraphs/ematch.jl index d2c5fb6d..045baea3 100644 --- a/test/egraphs/ematch.jl +++ b/test/egraphs/ematch.jl @@ -289,6 +289,18 @@ end @test test_equality(some_theory, :(a * b * 0), 0) end +@testset "Dynamic rule predicates in EMatcher" begin + some_theory = @theory begin + ~a * ~b => 0 where (iszero(a) || iszero(b)) + ~a * ~b --> ~b * ~a + end + + g = EGraph(:(2 * 3)) + saturate!(g, some_theory) + + @test true == areequal(g, some_theory, :(a * b * 0), 0) +end + @testset "Inequalities" begin failme = @theory p begin p != !p From bce5fa33f66a1edf795afe1564eb21338d526ae4 Mon Sep 17 00:00:00 2001 From: Gabriel Kronberger Date: Wed, 25 Sep 2024 10:27:45 +0200 Subject: [PATCH 8/9] Bugfix for new test case --- test/egraphs/ematch.jl | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/test/egraphs/ematch.jl b/test/egraphs/ematch.jl index 045baea3..8b51c748 100644 --- a/test/egraphs/ematch.jl +++ b/test/egraphs/ematch.jl @@ -290,12 +290,16 @@ end end @testset "Dynamic rule predicates in EMatcher" begin + g = EGraph(:(2 * 3)) + zero_id = addexpr!(g, 0) + some_theory = @theory begin ~a * ~b => 0 where (iszero(a) || iszero(b)) ~a * ~b --> ~b * ~a end - g = EGraph(:(2 * 3)) + Base.iszero(ec::EClass) = in_same_class(g, zero_id, ec.id) + saturate!(g, some_theory) @test true == areequal(g, some_theory, :(a * b * 0), 0) From 3373cb649516729c824c1ae5ad319e909c3cfb30 Mon Sep 17 00:00:00 2001 From: Gabriel Kronberger Date: Wed, 25 Sep 2024 10:37:48 +0200 Subject: [PATCH 9/9] Another fix required.. --- test/egraphs/ematch.jl | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/test/egraphs/ematch.jl b/test/egraphs/ematch.jl index 8b51c748..414c7439 100644 --- a/test/egraphs/ematch.jl +++ b/test/egraphs/ematch.jl @@ -302,7 +302,7 @@ end saturate!(g, some_theory) - @test true == areequal(g, some_theory, :(a * b * 0), 0) + @test test_equality(some_theory, :(a * b * 0), 0) end @testset "Inequalities" begin