search

viperproject / axiom-profiler-2

The axiom profiler for exploring and visualizing SMT solver quantifier instantiations (made via E-matching).
https://viperproject.github.io/axiom-profiler-2/
16 stars 3 forks source link

Helper binary for extracting axiom dependencies #50

Closed JonasAlaif closed 5 months ago

JonasAlaif commented 5 months ago

Duplicate of https://github.com/viperproject/axiom-profiler-2/pull/45, I just don't have permissions to push to your fork. @Gopiandcode could you enable this in the future :)

JonasAlaif commented 5 months ago

Responding to the PR: this looks great! I will pull this into the main crate

kiranandcode commented 5 months ago

ah, whoops, my bad!! will enable that in the future, can't believe I missed that lol!

JonasAlaif commented 5 months ago

@Gopiandcode I've made some changes, let me know if everything still works for you or if I broke something. The main change is that I keep around the InstIdx for much longer instead of using RawNodeIndex (the missing link is that one can go from the former to the latter using the InstIdx as IndexesInstGraph trait). I also switched to petgraph::Dfs which requires some not very nice EdgeFiltered and Reversed adaptors but still nicer than doing the dfs manually imo

kiranandcode commented 5 months ago

Ooh, yep, this looks good! Lemme try it out!

kiranandcode commented 5 months ago

Awesome, tried it out! Works great!