我想知道是否有人可以告诉我以下 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)
谢谢。
我不相信这些统计数据的含义是有据可查的。如果您想详细研究它们，最好的办法是实际通读源代码。你可以从这里开始：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
本文收集自互联网，转载请注明来源。
如有侵权，请联系 [email protected] 删除。
我来说两句