继续“未知"结果与 :pattern 在 SMTLIB v2 输入中的使用 [英] Keep getting "unknown" result with :pattern usage in SMTLIB v2 input

问题描述

我在 Z3 中使用 SMTLIBv2 输入格式和模式时遇到问题:我一直使用以下输入获得结果未知":

I'm encountering a problem when using the SMTLIBv2 input format and patterns with Z3: I keep getting the result "unknown" with the following input:

(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)))) 作为模型.

I use a list to represent the possible paths through a transition system. The transition system in this case consists only of states L0 and L1 which are linked by a transition from L0 to L1. By assert statements I limit the paths to such that start with L0 and are of length 2. I expect to get as a model the path (L0 (cons (L1 (cons nil)))).

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

I already tried to boil it down to a minimal example that still shows the problem, resulting in the code above. I want to use the pattern to implement a recursive check on 'path', to ensure that each two consecutive nodes in the list comply with some (transition) constraint. The check for consecutive cons is used as a stopping condition for this recursive check. Although in the example above I removed the recursive check via checkTransition, it still does not work. The whole idea goes back to an article by Milicevic and Kugler in which they use Z3 2.0 and the .net API to represent a Model Checking problem in such a way.

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

I'm aware that pattern instantiation can lead to the result "unknown", but I was wondering why it already happens with such a simple (?) example. Am I using the pattern in a wrong way to achieve quantifier support?

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

Any ideas on this problem are more than welcome!

问候卡斯腾

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

P.S.: I use Z3 version 4.3.2 on MacOS X (10.8.3) The mentioned article: Milicevic, A. & Kugler, H., 2011. Model checking using SMT and theory of lists. NASA Formal Methods, pp.282–297.

根据 mhs 的评论进行

获取不到模型的问题好像是从4.3.2版本开始出现的(不稳定).我对不同版本进行了一些故障排除:

The problem of not getting a model seems to occur from version 4.3.2 (unstable). I did some troubleshooting with different versions:

• Z3 4.3.0 32 位，WinXP 32 位，来自安装程序
  • 结果:未知，但给出了模型
  • 结果:未知，但给出了模型
  • 结果:未知，没有模型
  • 结果:未知，没有模型

  有趣吗?

  推荐答案

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

  Z3 has many solvers. Not every solver produces a "candidate model" when the result is unknown. The default solver is a portfolio that automatically selects the solver to be used. The portfolio solver was modified in the unstable (working-in-progress) branch. The nightly builds are compiled using the unstable branch. I will add a command to specify the solver that is executed when (check-sat) is executed. Thus, if we are interested in "candidate models" for unknown results, we can specify a solver that produces them. In the meantime, you can use the following workaround:

  • 在(check-sat)之前添加一个(push)命令.这是一个小技巧，它迫使投资组合求解器选择生成候选模型"的求解器.
  • Add a (push) command before (check-sat). This is a little hack that forces the portfolio solver to select a solver that produces "candidate models".

  补充说明:

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

  • Z3 v4.3.2 was not released yet. This is why the nightly builds in the question have the git hashes 197b2e8ddb91 and 96f4606a7f2d attached to them. These hash codes identify the precise git commits used to build them.

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

  If we remove the command (set-option :smt.mbqi false), Z3 will use the mbqi module and will successfully show the assertions to be unsat.

  这篇关于继续“未知"结果与 :pattern 在 SMTLIB v2 输入中的使用的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！