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

Documentation on how to view Quantifier Instantiations #27

Closed kiranandcode closed 5 months ago

kiranandcode commented 5 months ago

Hihi! Sorry if this isn't the right place to ask this? feel free to close if so!

I'm running the axiom profiler on some logs, and I'd like to view the concrete instantiations of an quantified axiom that z3 tried in its proof search.

Is there a place in the UI to view this? I tried looking at the documentation, but I couldn't find anything.

oskari1 commented 5 months ago

The nodes in the represented graph correspond to instantiations of quantified assertions and you can click on them to view the information associated with each instantiation. Do you want to view specific user-specified quantified assertions? In that case, we are planning to work on a feature which goes in that direction.

kiranandcode commented 5 months ago

Ah I see, thanks for clarifying! Yes, that makes sense.

JonasAlaif commented 5 months ago

@Gopiandcode just to clarify, all nodes of the same colour correspond to the same quantifier. Quantifiers can be identified by name if they had a :qid NAME in the .smt2 file given to z3. In the current version, it's a bit tricky to figure out which name matches to which colour, but you can try using the "Show quant _" operation in the left sidebar (it takes the name of the quantifier and shows all nodes associated with it). Once https://github.com/viperproject/axiom-profiler-2/pull/28 lands, you will be able to search for and iterate through the nodes of named quantifier. If you run into any other problems, please open more issues :)