Z3统计意义答案

【问题标题】：Z3 statistics meaningZ3统计意义
【发布时间】：2019-11-18 02:06:33
【问题描述】：

我想知道是否有人可以告诉我以下 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)

谢谢。

【问题讨论】：

标签： statistics z3

【解决方案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

【讨论】：