4

在 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 以这种方式表示模型检查问题。

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

任何关于这个问题的想法都非常受欢迎！

问候卡斯滕

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

根据 mhs 的评论进行编辑：

4.3.2版本（不稳定）似乎出现了拿不到模型的问题。我对不同版本进行了一些故障排除：

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

有趣的？

4

2 回答 2

0

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

  • 在. (push)_ (check-sat)这是一个小技巧，它迫使投资组合求解器选择产生“候选模型”的求解器。

补充说明：

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

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

于 2013-04-06T17:03:02.027 回答
0

我刚刚在 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预期的结果。

于 2013-04-04T08:43:31.483 回答