使用 SMTLIB v2 输入中的 :pattern 用法不断获得“未知”结果

Question

在 Z3 中使用 SMTLIBv2 输入格式和模式时遇到问题：我不断收到以下输入的结果“未知”：

(declare-datatypes () ((L L0 L1)))
(declare-fun path () (List L))
(declare-fun checkTransition ((List L)) Bool)

(define-fun isCons ((p (List L))) Bool
    (not (= p nil))
)

; configuration options for :pattern, taken from the Z3 tutorial
(set-option :auto-config false) ; disable automatic self configuration
(set-option :smt.mbqi false)    ; disable model-based quantifier instantiation

(assert (isCons path))
(assert (isCons (tail path)))
(assert (= nil (tail (tail path))))
(assert (= L0 (head path)))             ; initial state constraint

(assert
    (forall ((p (List L)))
    (!
        (implies
            (and    (isCons p)
                    (isCons (tail p)))
            (and    (=  L0  (head p))           ; transition from L0
                    (=  L1  (head (tail p)))))  ; to L1
    :pattern ((checkTransition p))
    )
    )
)
(assert (checkTransition path))

(check-sat)
(get-model)

我使用一个列表来表示通过转换系统的可能路径。在这种情况下，转换系统仅由状态 L0 和 L1 组成，它们通过从 L0 到 L1 的转换链接。通过断言语句，我将路径限制为以 L0 开头且长度为 2 的路径。 我希望将路径（L0（cons（L1（cons nil））））作为模型。

我已经尝试将其归结为一个仍然显示问题的最小示例，从而产生上面的代码。 我想使用该模式对“路径”进行递归检查，以确保列表中的每两个连续节点都符合某些（转换）约束。检查连续 cons 用作此递归检查的停止条件。尽管在上面的示例中我通过 checkTransition 删除了递归检查，但它仍然不起作用。整个想法可以追溯到 Milicevic 和 Kugler 的一篇文章，他们在文章中使用 Z3 2.0 和 .net API 以这种方式表示模型检查问题。

我知道模式实例化会导致结果“未知”，但我想知道为什么它已经发生在这样一个简单的 (?) 示例中。我是否以错误的方式使用模式来实现量词支持？

欢迎任何关于这个问题的想法！

问候 卡斯滕

附： 我在 MacOS X (10.8.3) 上使用 Z3 版本 4.3.2 提到的文章：Milicevic, A. & Kugler, H.，2011。使用 SMT 和列表理论进行模型检查。 NASA 形式方法，第 282-297 页。

基于 mhs 的 cmets 进行编辑：

从 4.3.2 版本开始出现无法获取模型的问题（不稳定）。 我对不同版本进行了一些故障排除：

• Z3 4.3.0 32bit，WinXP 32bit，来自安装程序
  • 结果：未知，但给出了一个模型
• Z3版本4.3.1，git checkout 89c1785b73225a1b363c0e485f854613121b70a7，MacOS X，自编译，这是master分支最新版本....
  • 结果：未知，但给出了一个模型
• master 分支的各种其他检查，所有
• Z3 版本 4.3.2，夜间构建 z3-4.3.2.197b2e8ddb91-x64-osx-10.8.2，MacOS X...
  • 结果：未知，没有给出模型
• Z3 版本 4.3.2，夜间构建 z3-4.3.2.96f4606a7f2d-x64-osx-10.8.2，MacOS X...
  • 结果：未知，没有给出模型

有趣吗？

Answer 1

Z3 有很多求解器。当结果为unknown 时，并非每个求解器都会生成“候选模型”。 默认求解器是自动选择要使用的求解器的投资组合。投资组合求解器在 unstable (working-in-progress) 分支中进行了修改。使用 unstable 分支编译夜间构建。我将添加一个命令来指定在执行(check-sat) 时执行的求解器。因此，如果我们对unknown 结果的“候选模型”感兴趣，我们可以指定一个生成它们的求解器。同时，您可以使用以下解决方法：

• 在(check-sat) 之前添加(push) 命令。这是一个小技巧，它迫使投资组合求解器选择生成“候选模型”的求解器。

补充说明：

• Z3 v4.3.2 尚未发布。这就是为什么问题中的每晚构建都附加了 git 哈希 197b2e8ddb91 和 96f4606a7f2d 的原因。这些哈希码标识了用于构建它们的精确 git 提交。

• 如果我们删除命令(set-option :smt.mbqi false)，Z3 将使用mbqi 模块并成功显示断言为unsat。

Answer 2

我刚刚在 Win 7 x64 上的 Z3 4.3.0 上尝试了您的示例，我得到了结果

unknown

(model 
  (define-fun path () (List L)
    (insert L0 (insert L1 nil)))

  (define-fun checkTransition ((x!1 (List L))) Bool
    (ite (= x!1 (insert L0 (insert L1 nil))) true
      true))
)

这不正是你期待的path 的模型吗？

我假设您收到 unknown 是因为您的问题未明确说明，但我无法指出具体问题。如果你给 Z3 一些反驳的东西，例如通过附加

(assert (not (= L1 (head (tail path)))))
(check-sat)

添加到您的代码，然后您将按预期获得unsat。