-
-
Notifications
You must be signed in to change notification settings - Fork 45
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Merge pull request #169 from JuliaSymbolics/ale/debugging
Add debugging and GraphViz visualization utilities
- Loading branch information
Showing
12 changed files
with
413 additions
and
58 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Loading
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,41 @@ | ||
| # Visualizing E-Graphs | ||
|
|
||
| You can visualize e-graphs in VSCode by using [GraphViz.jl]() | ||
|
|
||
| All you need to do is to install GraphViz.jl and to evaluate an e-graph after including the extra script: | ||
|
|
||
| ```julia | ||
| using GraphViz | ||
|
|
||
| include(dirname(pathof(Metatheory)) * "/extras/graphviz.jl") | ||
|
|
||
| algebra_rules = @theory a b c begin | ||
| a * (b * c) == (a * b) * c | ||
| a + (b + c) == (a + b) + c | ||
|
|
||
| a + b == b + a | ||
| a * (b + c) == (a * b) + (a * c) | ||
| (a + b) * c == (a * c) + (b * c) | ||
|
|
||
| -a == -1 * a | ||
| a - b == a + -b | ||
| 1 * a == a | ||
|
|
||
| 0 * a --> 0 | ||
| a + 0 --> a | ||
|
|
||
| a::Number * b == b * a::Number | ||
| a::Number * b::Number => a * b | ||
| a::Number + b::Number => a + b | ||
| end; | ||
|
|
||
| ex = :(a - a) | ||
| g = EGraph(ex) | ||
| params = SaturationParams(; timeout = 2) | ||
| saturate!(g, algebra_rules, params) | ||
| g | ||
| ``` | ||
|
|
||
| And you will see a nice e-graph drawing in the Julia Plots VSCode panel: | ||
|
|
||
|  |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,96 @@ | ||
| using GraphViz | ||
| using Metatheory | ||
| using TermInterface | ||
|
|
||
| function render_egraph!(io::IO, g::EGraph) | ||
| print( | ||
| io, | ||
| """digraph { | ||
| compound=true | ||
| clusterrank=local | ||
| remincross=false | ||
| ranksep=0.9 | ||
| """, | ||
| ) | ||
| for (_, eclass) in g.classes | ||
| render_eclass!(io, g, eclass) | ||
| end | ||
| println(io, "\n}\n") | ||
| end | ||
|
|
||
| function render_eclass!(io::IO, g::EGraph, eclass::EClass) | ||
| print( | ||
| io, | ||
| """ subgraph cluster_$(eclass.id) { | ||
| style="dotted,rounded"; | ||
| rank=same; | ||
| label="#$(eclass.id). Smallest: $(extract!(g, astsize; root=eclass.id))" | ||
| fontcolor = gray | ||
| fontsize = 8 | ||
| """, | ||
| ) | ||
|
|
||
| # if g.root == find(g, eclass.id) | ||
| # println(io, " penwidth=2") | ||
| # end | ||
|
|
||
| for (i, node) in enumerate(eclass.nodes) | ||
| render_enode_node!(io, g, eclass.id, i, node) | ||
| end | ||
| print(io, "\n }\n") | ||
|
|
||
| for (i, node) in enumerate(eclass.nodes) | ||
| render_enode_edges!(io, g, eclass.id, i, node) | ||
| end | ||
| println(io) | ||
| end | ||
|
|
||
|
|
||
| function render_enode_node!(io::IO, g::EGraph, eclass_id, i::Int, node::AbstractENode) | ||
| label = operation(node) | ||
| # (mr, style) = if node in diff && get(report.cause, node, missing) !== missing | ||
| # pair = get(report.cause, node, missing) | ||
| # split(split("$(pair[1].rule) ", "=>")[1], "-->")[1], " color=\"red\"" | ||
| # else | ||
| # " ", "" | ||
| # end | ||
| # sg *= " $id.$os [label=<$label<br /><font point-size=\"8\" color=\"gray\">$mr</font>> $style];" | ||
| println(io, " $eclass_id.$i [label=<$label> shape=box style=rounded]") | ||
| end | ||
|
|
||
| render_enode_edges!(::IO, ::EGraph, eclass_id, i, ::ENodeLiteral) = nothing | ||
|
|
||
| function render_enode_edges!(io::IO, g::EGraph, eclass_id, i, node::ENodeTerm) | ||
| len = length(arguments(node)) | ||
| for (ite, child) in enumerate(arguments(node)) | ||
| cluster_id = find(g, child) | ||
| # The limitation of graphviz is that it cannot point to the eclass outer frame, | ||
| # so when pointing to the same e-class, the next best thing is to point to the same e-node. | ||
| target_id = "$cluster_id" * (cluster_id == eclass_id ? ".$i" : ".1") | ||
|
|
||
| # In order from left to right, if there are more than 3 children, label the order. | ||
| dir = if len == 2 | ||
| ite == 1 ? ":sw" : ":se" | ||
| elseif len == 3 | ||
| ite == 1 ? ":sw" : (ite == 2 ? ":s" : ":se") | ||
| else | ||
| "" | ||
| end | ||
|
|
||
| linelabel = len > 3 ? " label=$ite" : " " | ||
| println(io, " $eclass_id.$i$dir -> $target_id [arrowsize=0.5 lhead=cluster_$cluster_id $linelabel]") | ||
| end | ||
| end | ||
|
|
||
| function Base.convert(::Type{GraphViz.Graph}, g::EGraph)::GraphViz.Graph | ||
| io = IOBuffer() | ||
| render_egraph!(io, g) | ||
| gs = String(take!(io)) | ||
| g = GraphViz.Graph(gs) | ||
| GraphViz.layout!(g; engine = "dot") | ||
| g | ||
| end | ||
|
|
||
| function Base.show(io::IO, mime::MIME"image/svg+xml", g::EGraph) | ||
| show(io, mime, convert(GraphViz.Graph, g)) | ||
| end |
Oops, something went wrong.