SMTLib2指令(get-info all-statistics)显示多个数字，例如
num. conflicts: 4
num. propagations: 0 (binary: 0)
num. qa. inst: 23
为了测试不同的公理化和编码，我想知道这些数字中的哪一个适合宣布一个Z3运行比另一个运行更好/更有效。
从名字中猜测，我想说的是num. qa. inst-数量化实例化的数量-是一个很好的指标（低=更好），但是其他指标呢？
给定一个使用 Z3 实数编码的问题，Z3 /smt2 /st产生的哪些统计数据可能有助于判断实数引擎是否“有问题/做了很多工作”？
就我而言，我有两个几乎等效的问题编码，都使用实数。然而，编码中的“小”差异在运行时产生了很大差异，即编码 A 需要 2:30 分钟，编码 B 需要 13 分钟。Z3的统计数据显示，conflicts和quant-instantiations大多是等价的，但其他人都没有，例如grobner，pivots和nonlinear-horner。
两种不同的统计数据可作为gist 使用。
编辑（以解决 Leo 的评论）：
两个版本生成的 SMT2 编码约为 30k 行，并且使用实数的断言散布在整个代码中。的主要区别在于编码乙使用大量尚未得以实时类型的常量从范围0.0到1.0由不等式，例如有界0.0 < r1 < 1.0或0.0 < r3 < 0.75 - r1 - r2，而在编码许多这些尚未得以常数已经从相同的范围置换为固定真实值，例如，0.1或0.75 - 0.01。两种编码都使用非线性实数算术，例如r1 * (1.0 - r2).
来自两种编码的一些随机示例可作为要点。如上所述，所有出现的变量都是未指定的实数。
PS：是否为固定实数值引入别名，例如，
(define-sort $Perms () Real)
(declare-const …我在Z3中得到以下统计信息.
(:added-eqs 24529
:binary-propagations 43837
:bv-bit2core 7115
:bv-conflicts 156
:bv-diseqs 10395
:bv-dynamic-diseqs 10028
:bv->core-eq 10401
:conflicts 409
:decisions 4840
:del-clause 84926
:final-checks 2
:max-generation 4
:memory 5.69
:minimized-lits 467
:mk-clause 88358
:propagations 90195
:quant-instantiations 3388
:restarts 3
:time 0.83)
我想知道每个结果行使用的指标.
你能帮助我吗？