z3 - 使用 :pattern usage in SMTLIB v2 input 继续获得 "unknown"结果

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

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

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

问候
卡斯腾

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 32 位，WinXP 32 位，来自安装程序

结果:未知，但给出了一个模型

Z3 4.3.1版本，git checkout 89c1785b73225a1b363c0e485f854613121b70a7，MacOS X，自编译，这是master分支最新版本....

结果:未知，但给出了一个模型

主分支的各种其他结帐，都 <= 4.3.1 产生相同的结果。

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

我刚刚在 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正如预期的那样。