z3 - 我如何获得 k 其中 k 来自 F_k for pdr in muz？

Question

我在 Z3 中使用 muZ，它有这个新的通用 PDR。我想知道如何获得有关 PDR 算法的一些数据。PDR 算法的不变量如下：

I => F_0
F_i => F_{i+1} for 0 <= i < k
F_i => P for 0 <= i <= k
F_i /\ T => F'_{i + 1}

我对终止时的 k 值非常感兴趣。这个统计数据是否可用？如果我在查询中启用 :print-statistics true ，我看不到它：

(query (p x) :print-statistics true)

Answer 1

统计功能目前并没有详细说明 PDR（它应该并感谢您指出这一点）。此时，您可以通过以详细模式运行它来获取更多信息。它将迭代计数打印到 stderr 流。

例如：

z3.exe bakery.smt2 /v:1
Entering level 1
Entering level 2
Entering level 3
Entering level 4
Entering level 5
Entering level 6
.... followed by inductive assertions ...