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 ...