Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add debugging and GraphViz visualization utilities #169

Merged
merged 13 commits into from
Oct 22, 2023
Merged
Changes from 1 commit
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Next Next commit
add debug statements
  • Loading branch information
a committed Oct 20, 2023
commit db4228492e3c89f74b46aefed94f21fad8715760
2 changes: 1 addition & 1 deletion src/EGraphs/EGraphs.jl
Original file line number Diff line number Diff line change
@@ -6,7 +6,7 @@ using DataStructures
using TermInterface
using TimerOutputs
using Metatheory:
alwaystrue, cleanast, binarize, @log, DEFAULT_BUFFER_SIZE, BUFFER, BUFFER_LOCK, MERGES_BUF, MERGES_BUF_LOCK, Bindings
alwaystrue, cleanast, binarize, DEFAULT_BUFFER_SIZE, BUFFER, BUFFER_LOCK, MERGES_BUF, MERGES_BUF_LOCK, Bindings
using Metatheory.Patterns
using Metatheory.Rules
using Metatheory.EMatchCompiler
8 changes: 0 additions & 8 deletions src/EGraphs/egraph.jl
Original file line number Diff line number Diff line change
@@ -294,8 +294,6 @@ end
Inserts an e-node in an [`EGraph`](@ref)
"""
function add!(g::EGraph, n::AbstractENode)::EClassId
@debug("adding ", n)

n = canonicalize(g, n)
haskey(g.memo, n) && return g.memo[n]

@@ -378,9 +376,6 @@ function Base.merge!(g::EGraph, a::EClassId, b::EClassId)::EClassId

id_a == id_b && return id_a
to = union!(g.uf, id_a, id_b)

@debug "merging" id_a id_b

from = (to == id_a) ? id_b : id_a

push!(g.dirty, to)
@@ -432,15 +427,13 @@ function repair!(g::EGraph, id::EClassId)
id = find(g, id)
ecdata = g[id]
ecdata.id = id
@debug "repairing " id

new_parents = (length(ecdata.parents) > 30 ? OrderedDict : LittleDict){AbstractENode,EClassId}()

for (p_enode, p_eclass) in ecdata.parents
p_enode = canonicalize!(g, p_enode)
# deduplicate parents
if haskey(new_parents, p_enode)
@debug "merging classes" p_eclass (new_parents[p_enode])
merge!(g, p_eclass, new_parents[p_enode])
end
n_id = find(g, p_eclass)
@@ -449,7 +442,6 @@ function repair!(g::EGraph, id::EClassId)
end

ecdata.parents = collect(new_parents)
@debug "updated parents " id g.parents[id]

# ecdata.nodes = map(n -> canonicalize(g.uf, n), ecdata.nodes)

23 changes: 10 additions & 13 deletions src/EGraphs/saturation.jl
Original file line number Diff line number Diff line change
@@ -71,7 +71,6 @@ Base.@kwdef mutable struct SaturationParams
schedulerparams::Tuple = ()
threaded::Bool = false
timer::Bool = true
printiter::Bool = false
end

# function cached_ids(g::EGraph, p::PatTerm)# ::Vector{Int64}
@@ -124,17 +123,20 @@ function eqsat_search!(
empty!(BUFFER[])
end

@debug "SEARCHING"
for (rule_idx, rule) in enumerate(theory)
@timeit report.to string(rule_idx) begin
# don't apply banned rules
if !cansearch(scheduler, rule)
@debug "$rule is banned"
continue
end
ids = cached_ids(g, rule.left)
rule isa BidirRule && (ids = ids ∪ cached_ids(g, rule.right))
for i in ids
n_matches += rule.ematcher!(g, rule_idx, i)
end
n_matches > 0 && @debug "$rule produced $n_matches matches"
inform!(scheduler, rule, n_matches)
end
end
@@ -180,7 +182,7 @@ function apply_rule!(bindings::Bindings, g::EGraph, rule::UnequalRule, id::EClas
other_id = instantiate_enode!(bindings, g, pat_to_inst)

if find(g, id) == find(g, other_id)
@log "Contradiction!" rule
@debug "$rule produced a contradiction!"
return :contradiction
end
nothing
@@ -215,10 +217,12 @@ function eqsat_apply!(g::EGraph, theory::Vector{<:AbstractRule}, rep::Saturation
i = 0
@assert isempty(MERGES_BUF[])

@debug "APPLYING $(length(BUFFER[])) matches"

lock(BUFFER_LOCK) do
while !isempty(BUFFER[])
if reached(g, params.goal)
@log "Goal reached"
@debug "Goal reached"
rep.reason = :goalreached
return
end
@@ -249,10 +253,6 @@ function eqsat_apply!(g::EGraph, theory::Vector{<:AbstractRule}, rep::Saturation
end



import ..@log


"""
Core algorithm of the library: the equality saturation step.
"""
@@ -276,6 +276,8 @@ function eqsat_step!(
end
@timeit report.to "Rebuild" rebuild!(g)

@debug smallest_expr = extract!(g, astsize)

return report
end

@@ -297,7 +299,7 @@ function saturate!(g::EGraph, theory::Vector{<:AbstractRule}, params = Saturatio
while true
curr_iter += 1

params.printiter && @info("iteration ", curr_iter)
@debug "================ EQSAT ITERATION $curr_iter ================"

report = eqsat_step!(g, theory, curr_iter, sched, params, report)

@@ -328,7 +330,6 @@ function saturate!(g::EGraph, theory::Vector{<:AbstractRule}, params = Saturatio
end
end
report.iterations = curr_iter
@log report

return report
end
@@ -339,13 +340,9 @@ function areequal(theory::Vector, exprs...; params = SaturationParams())
end

function areequal(g::EGraph, t::Vector{<:AbstractRule}, exprs...; params = SaturationParams())
@log "Checking equality for " exprs
if length(exprs) == 1
return true
end
# rebuild!(G)

@log "starting saturation"

n = length(exprs)
ids = map(Base.Fix1(addexpr!, g), collect(exprs))
6 changes: 0 additions & 6 deletions src/Metatheory.jl
Original file line number Diff line number Diff line change
@@ -24,12 +24,6 @@ using Base.Meta
using Reexport
using TermInterface

macro log(args...)
quote
haskey(ENV, "MT_DEBUG") && @info($(args...))
end |> esc
end

@inline alwaystrue(x) = true

function lookup_pat end