1

莱昂纳多：感谢您的快速回复！非常感激。

如果我将以下脚本提供给 Z3：

(set-option :MBQI true)
(set-option :produce-models true)
(declare-fun s1 ((_ BitVec 16)) (_ BitVec 16))
(assert (forall ((s0 (_ BitVec 16))) (bvuge s0 (s1 s0))))
(check-sat)
(get-model)
(eval (s1 #x0000))

Z3 成功构建了模型，其中s1给出了恒等函数。但是，对 eval 的调用会导致 Z3 超时。我需要设置一个特定的选项吗？

另外，我注意到如果我删除该行：

(set-option :MBQI true)

然后 Z3 回应unknown。由于 QBVF 是可判定的，所以我需要设置一个选项有点令人惊讶。是不是我们应该true在所有 QBVF 问题中设置 MBQI，还是这个实例有什么特别之处？

谢谢..

4

1 回答 1

1

Z3有几个处理量词的引擎：E-matching、MBQI、叠加等。虽然QBVF是一个可判定的分片，但只有MBQI引擎才能判定。E-matching 模块仅在显示公式不可满足时有效。对于可满足的实例，它总是会失败（返回未知）。叠加模块在纯（无理论）一阶逻辑公式中有效。

在 Z3 的某些版本中，默认不启用 MBQI 模块，因为它非常昂贵。一些应用程序，例如 VCC 和 Spec#，使用非常复杂的量化公式，这些公式不在 MBQI 可以支持的任何可判定片段中。因此，MBQI 模块只是这些应用程序的开销。在 Z3 3.1（可在 Z3 网站下载）中，默认启用 MBQI。

在即将发布的 Z3 3.2 中，将正式支持逻辑 UFBV。UFBV 是 QBVF 的 SMT-LIB 名称。因此，您将能够使用(set-logic UFBV)并且 Z3 将自动针对此逻辑进行自我配置。

关于eval命令，这是一个错误，我会修复它。该修复程序将在 Z3 3.2 中提供。

于 2011-09-09T18:32:34.723 回答