Consolidate options and output for z3 insights

[msprotz]

We currently have three options that do slightly different things: --hint_info, --query_statsand--print_z3_statistics`.

First request is: consolidate these three options into a single one. If some options are inferior (because they provide less output), remove them. I they have to remain because of tooling (e.g. python parsing of build logs), remove them from fstar --help and update the wiki.

edit: second half is a duplicate of #1681

Second request is: the output currently is something along those lines:

[F* info] (<input>(320,29-320,32))  Query-stats (Negotiation.__proj__ServerHelloRetryRequest__item__hrr, 1) succeeded in 267 milliseconds with fuel 2 and ifuel 1 and rlimit 2723280 statistics={mk-bool-var=58980 del-clause=35680 lazy-quant-instantiations=240 num-checks=6 conflicts=171 binary-propagations=108 propagations=105831 arith-assert-upper=6 arith-assert-lower=17 decisions=3361 datatype-occurs-check=216 rlimit-count=2248924 quant-instantiations=7963 mk-clause=50981 memory=70.52 arith-pivots=46 max-generation=12 arith-add-rows=20 time=0.25 num-allocs=1967325 datatype-accessor-ax=26 max-memory=73.00 final-checks=12 arith-eq-adapter=8 added-eqs=11736}

per discussions at the all-hands (and writing it down here so that it doesn't get lost), it'd be good to summarize the values above by:

• printing rlimit values in terms of F* rlimit (i.e. divided by the magic number we use)
• separating all of this into time spent into arithmetic vs. time spent in quantifiers vs. time spent in the rest

Thanks,

Jonathan

[nikswamy]

Can we fold this into 1681 and close?

[msprotz]

Thanks. I've removed the second half but left the first half which is the request to consolidate options into a single one.