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 文献中是众所周知的 "statistics"，例如 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

Z3统计意义

Z3 statistics meaning

statistics

z3