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

Reusing equality explanations #22

Closed oskari1 closed 2 months ago

oskari1 commented 3 months ago

When opening cg_sort.log with the AP and filtering out all descendants of node i12, we can see in the screenshot below, that the equality node f(i) = f(inc(inc(inc(i)))) blames three nodes, namely f(i) = f(inc(i)), f(inc(i)) = f(inc(inc(i))), and f(inc(inc(i))) = f(inc(inc(inc(i)))), so it does not correctly compute the "shortest path" in the e-graph.

image