SMT profiling information to report through F*

[nikswamy]

The --print_z3_statistics option now shows more output about the SMT context, hypotheses that were used etc., along with many other Z3 statistics. See #1632

We also expect a PR soon from @wintersteiger and Adrian Rebola-Pardo that surfaces smt.qi.profile information back to the F* user.

What else could we show regarding Z3 statistics?

One idea we are discussing is to show the result of differential profiling, e.g., the results of qprofdiff surfaced via an F* option.

What else? @wintersteiger @parno et al.

[jaybosamiya]

For z3 stats, it would be nice to have the "converted back to F*" z3 rlimits.

[arpj-rebola]

This is the kind of output our branch is generating. Each set of queries generates a report when Z3 is killed (this limitation cannot be bypassed, although Z3 can be killed for every query, and the checked queries can be restricted with the "admit" options). The report contains quantifier IDs, number of instantiations, and origins (including module, source file and lines).

[edit: fixed file] ulib.zip

[wintersteiger]

Neither Windows nor 7-Zip are able to open that .zip file. Could you check what's wrong there?

[wintersteiger]

Ah! It's not a .zip file at all, it's just plain text.

[arpj-rebola]

Fixed - don't know what happened.

[R1kM]

From what was presented this morning, a list of the used facts is generated for each proof with the current settings.

It would be great if this could be saved somewhere, and accessible even if the proof in the future does not succeed. My usecase would be, "I have this proof that previously succeeded with this set of facts and is now failing. This proof is now timing out. A first fix could be setting "using_facts_from" to this set of facts to reduce my context, and make my proof more stable".

This could for instance be saved in the hints file. I would only see that used for debug purposes.

[parno]

Having lots of detailed info available is great, but I think it's also helpful to have a few high-level aggregates easily accessible as well. For example, a summary of how much time was spent in F* vs. Z3, and what percentage of Z3's rlimit was spent on, say, e-matching and quantifiers vs. arithmetic would be helpful. It seems easier for users to develop intuition about "normal" results of such aggregates, and hence easier to notice anomalies.

[nikswamy]

Please also see #1684

[wintersteiger]

@parno that information is not available; the z3 statistics are in terms of numbers of operations without any relation to time or rlimit. To get that sort of information, we would have to generate a complete log with timing information for each step, i.e. this would be huge and slow, and we'd have to implement profiling in Z3 first. (Also, it's usually the search that takes time, while an e-matching step (like quantifier instantiation) is cheap, because it only creates and adds a new term. So, whatever happens later is very hard to relate to a particular instance, etc.)

The first step towards making all these numbers understandable is to simply add the units in the output, to make it clear what kind of numbers we're looking at.