[Question]: How can I get used lemmas about formula after solving?

[hagozaebii]

Hello,

When using the -st option in Z3, the statistics provided are relatively high-level and lack detailed information about the solving process. For example, while Z3 reports stats like memory usage, number of propagations, and conflicts like:

(qfnra-tactic start)
(simplifier :num-exprs 115 :num-asts 384 :time 0.00 :before-memory 17.86 :after-memory 17.86)
(propagate-values :num-exprs 102 :num-asts 363 :time 0.00 :before-memory 17.86 :after-memory 17.86)
(qfnra-nlsat-tactic)
(simplifier :num-exprs 102 :num-asts 363 :time 0.00 :before-memory 19.31 :after-memory 19.31)
(nnf :num-exprs 102 :num-asts 363 :time 0.00 :before-memory 19.31 :after-memory 19.31)
(simplifier :num-exprs 102 :num-asts 363 :time 0.00 :before-memory 19.31 :after-memory 19.31)
(purify-arith :num-exprs 102 :num-asts 363 :time 0.00 :before-memory 19.31 :after-memory 19.31)
(simplifier :num-exprs 102 :num-asts 363 :time 0.00 :before-memory 19.31 :after-memory 19.31)
(propagate-values :num-exprs 102 :num-asts 363 :time 0.00 :before-memory 19.31 :after-memory 19.31)
(solve-eqs :num-exprs 100 :num-asts 363 :time 0.00 :before-memory 19.31 :after-memory 19.31)
(:solve-eqs-elim-vars 1
 :solve-eqs-steps     1)
(elim-uncnstr :num-exprs 100 :num-asts 363 :time 0.00 :before-memory 19.31 :after-memory 19.31)
(elim-term-ite :num-exprs 100 :num-asts 363 :time 0.00 :before-memory 19.31 :after-memory 19.31)
(nnf :num-exprs 100 :num-asts 363 :time 0.00 :before-memory 19.31 :after-memory 19.31)
(simplifier :num-exprs 100 :num-asts 363 :time 0.00 :before-memory 19.31 :after-memory 19.31)
(purify-arith :num-exprs 100 :num-asts 363 :time 0.00 :before-memory 19.31 :after-memory 19.31)
(simplifier :num-exprs 100 :num-asts 363 :time 0.00 :before-memory 19.31 :after-memory 19.31)
(factor :num-exprs 85 :num-asts 377 :time 0.00 :before-memory 19.31 :after-memory 19.31)
(solve-eqs :num-exprs 85 :num-asts 377 :time 0.00 :before-memory 19.31 :after-memory 19.31)
(nnf :num-exprs 85 :num-asts 377 :time 0.00 :before-memory 19.31 :after-memory 19.31)
(simplifier :num-exprs 85 :num-asts 383 :time 0.00 :before-memory 19.31 :after-memory 19.31)
(purify-arith :num-exprs 85 :num-asts 379 :time 0.00 :before-memory 19.31 :after-memory 19.31)
(simplifier :num-exprs 85 :num-asts 379 :time 0.00 :before-memory 19.31 :after-memory 19.31)
(simplifier :num-exprs 85 :num-asts 379 :time 0.00 :before-memory 19.31 :after-memory 19.31)
(tseitin-cnf :num-exprs 88 :num-asts 382 :time 0.00 :before-memory 19.31 :after-memory 19.31)
(simplifier :num-exprs 88 :num-asts 382 :time 0.00 :before-memory 19.31 :after-memory 19.31)
v5 v2 + v10 v2 - 2 v8 v2 - v5 + v8 = 0
(nlsat :conflicts 1 :decisions 0 :propagations 17 :clauses 21 :learned 1)
(nlsat :num-exprs 0 :num-asts 364 :time 0.00 :before-memory 19.31 :after-memory 19.41)
(qfnra-tactic done)
sat
(:max-memory          19.40
 :memory              19.40
 :nlsat-conflicts     1
 :nlsat-propagations  26
 :nlsat-restarts      1
 :nlsat-stages        15
 :num-allocs          123678
 :rlimit-count        2933
 :solve-eqs-elim-vars 1
 :solve-eqs-steps     1
 :time                0.01
 :total-time          0.02)

However, I want to know lemmas used during solving and rewrite rules or transformations applied to the formula.
For example, cvc5 provides very granular statistics with the --stats-internal option, such as the number of terms processed, the individual rewrite steps applied, and even specific inference types and their counts (e.g., ARITH_CONF_EQ, ARITH_SPLIT_DEQ) like:

resource::steps::inference-id = { ARITH_CONF_EQ: 2, ARITH_CONF_LOWER: 3, ARITH_CONF_SIMPLEX: 2, ARITH_CONF_UPPER: 11, ARITH_NL_COMPARISON: 5, ARITH_NL_SIGN: 35, ARITH_ROW_IMPL: 3, ARITH_SPLIT_DEQ: 14, ARITH_UNATE: 1, EXTT_SIMPLIFY: 12 }
resource::steps::resource = { ArithNlCoveringStep: 10, ArithPivotStep: 31, CnfStep: 132, DecisionStep: 319, LemmaStep: 45, PreprocessStep: 8, RewriteStep: 7916, SatConflictStep: 321, TheoryCheckStep: 449 }

Is there any way to extract similarly detailed statistics from Z3?

Thank you for your help!