feature wish: improve the reporting of the number of steps taken

[claudemarche]

Currently, to get the number of steps taken by Alt-Ergo (using the Dolmen frontend) one has to parse the SMT comment of the form

; File \".*\", line [0-9]+, characters [0-9]+-[0-9]+:.*(\\([0-9]+.?[0-9]*\\) steps)

which indeed comes before the answer unsat or unknown. There should be a better way to get this info, e.g. by issuing a command of the form

(get-info :steps-taken)

after the (check-sat) query, and get back an answer of a standardized form, e.g.

resource::steps = ...

(moreover, this should be documented)

Thanks!

[bclement-ocp]

This information was added in #863 (not part of release 2.5) to the response of the standards (get-info :all-statistics):

(
 :timer-Arrays 0.000001000
 :timer-CC 0.000001000
 :timer-Records 0.000000000
 :timer-Expr 0.000000000
 :timer-Simplex 0.000000000
 :timer-Triggers 0.000000000
 :timer-Arith 0.000005000
 :timer-Typing 0.000000000
 :timer-None 0.000017000
 :timer-Match 0.000001000
 :timer-UF 0.000002000
 :timer-Sum 0.000001000
 :timer-Ite 0.000000000
 :timer-AC 0.000000000
 :timer-Sat 0.000005000
 :steps 3)

However, this currently requires enabling profiling (which should not be necessary, as it induces overhead and the information is there already), and further the --profiling option was broken by the switch to ppx_deriving_enum in #863 (the max_ty_function and max_ty_module were the length, they are now the last value, and so the arrays are too small by one element).

We should fix those two issues and document the format of (get-info :all-statistics).