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

Fix parsing issues and a performance issue #12

Closed JonasAlaif closed 7 months ago

JonasAlaif commented 7 months ago

It turns out that the logfile can contain multiline entries, e.g. in the z3 v4.8.7 one sent here at line 15716 there is the entry

[assign] #7690 clause p49 (not p50)
  (and (not (= $allocated val)) (not (= $allocated init)) (not (= $allocated rel)) (not (= $allocated acq)) (not (= val init)) (not (= val rel)) (not (= val acq)) (not (= init rel)) (not (= init acq)) (not (= rel acq))) 
  (not (distinct $allocated val init rel acq))

These are now handeled.

JonasAlaif commented 7 months ago

@oskari1 please note the fix here: this little change reduces my overall time (from opening the file to viewing a graph) from 13s to 3s. You have to be very careful to not run O(n^2) operations with such big graphs.