Z3统计意义

Question

我想知道是否有人能告诉我以下Z3统计数字是什么意思。

(:add-rows        2
 :arith-conflicts 1
 :assert-lower    2
 :assert-upper    1
 :conflicts       1
 :max-memory      0.43
 :memory          0.43
 :mk-bool-var     4
 :num-allocs      6961
 :num-checks      1
 :pivots          2
 :rlimit-count    115
 :time            0.00)

谢谢。

Answer 1

我不相信这些统计数据的意义已经有了很好的记录。如果你想详细研究源代码的话，最好的方法就是仔细阅读源代码。你可以从这里开始：https://github.com/Z3Prover/z3/blob/ca498e20d17457b4baa32578a94923cf8e3e105c/src/smt/theory_lra.cpp#L3527-L3554

其中一些是众所周知的SMT-文献中的“统计数据”，比如conflicts. (本质上衡量了求解者不得不回溯多少次)。其他的则完全是特定的解决方法，比如mk-bool-var。

SMTLib本身指定了一些统计数据；请参阅http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2017-07-18.pdf的3.9.2节，但是实际意义主要留给实现，并且可能因求解器而异。

如果您对某个特定的问题感到好奇，我建议直接在z3 github：https://github.com/Z3Prover/z3上询问。