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/
8 stars 3 forks source link

Equality nodes with cg and lit #19

Closed oskari1 closed 3 months ago

oskari1 commented 5 months ago

The basic idea is that I initially add all nodes for the equalities corresponding to [eq-expl] with lit or cg in the log. The code in inst_graph.rs should document the procedure pretty well.

Note: I've removed the functionality of detecting matching loops for now since the latest matching-loop-graph-2 branch anyways uses a completely different approach.