2

我目前正在 Z3 之上为我的编程语言编写一个自动验证器，作为一个有趣的项目，我试图用它来证明使用循环的斐波那契实现等同于递归。

如果输入程序正确，它似乎可以工作，即它为 Z3 生成合理的输入，而 Z3 说它不能满足，这意味着在我的上下文中，程序是正确的。但是当我更改了一个变量初始化并因此导致程序不正确时，我的验证器提出了以下 Z3 公式，这对我来说似乎并不太复杂，但 Z3 说“未知”。

(set-option :smt.auto-config false)
(set-option :smt.mbqi false)
(declare-fun fib (Int) Int)
(declare-fun fakeFib (Int) Int)
(declare-fun n () Int)
(assert (forall ((n Int))
   (! (= (fib n)
         (ite (= n 0) 0
            (ite (= n 1) 1
               (+ (fakeFib (- n 1)) (fakeFib (- n 2))))))
      :pattern ((fib n)))))
(assert (forall ((n Int))
   (! (= (fib n) (fakeFib n)) :pattern ((fib n)))))
(assert (>= n 0))
(assert (not (and (<= 0 n) (= 1 (fib 1)) (= 1 (fib 0)))))
(check-sat)

请注意，这两个量词表示斐波那契的递归定义。我的一个朋友告诉我这个技巧来避免匹配循环：我没有将 fib 定义为递归函数，而是引入了另一个我没有提供定义的函数 fakeFib，我在 fib 的递归定义中使用了该函数。另外，我告诉验证者它们是相等的，但是量词只得到 fib 的模式，而不是 fakeFib 的模式。由于模式的限制，它是不完整的，即，它只能证明程序的正确性，只要看一层递归就足以证明它（但它可以很容易地扩展到 k 层）。但我可以忍受这个限制，以避免匹配循环。

代码的“错误”是我错误地初始化了一个变量，这最终导致(= 1 (fib 0))最后一个断言中的组件不正确。对于正确的程序，它将是(= 0 (fib 0)).

一些观察：

  • 如果我替换(= 1 (fib 0))为(= 0 (fib 0))，那么 Z3 立即发现它无法满足。
  • 以前，我没有选项(set-option :smt.auto-config false)和(set-option :smt.mbqi false)设置，然后它在我的机器上耗尽内存并且在rise4fun 上超时。
  • 似乎对有类似问题的人有用的设置(set-option :smt.macro-finder true)对我不起作用。我猜这是因为我有两个量词，fib而不仅仅是一个。
  • 我尝试使用 cvc4 作为比较，它立即说“未知”。所以我的问题似乎不是 Z3 特有的。
  • 该公式显然是可满足的。(= 1 (fib 0))是false，因此整个最后一个断言自动为真。(>= n 0)也很容易满足。
4

1 回答 1

2

我不是 Z3 专家，但也许我可以解释一下。

通过禁用 MBQI，您将禁用 Z3 为量化公式生成模型的能力，因此我猜当 Z3 无法找到证明您的问题不可满足的方法时，它会迅速将其报告为unknown.

请注意，您的问题的模型需要满足四个断言，而不仅仅是最后两个断言。正如您指出的那样，Z3 不能像宏一样消除您的第一个断言，因为您为fib n.

如果你启用 MBQI，你会看到 Z3 试图找到一个模型，并且在它上面消耗了相当多的内存！我认为这是因为满足您的规范的唯一方法需要构建递归函数fib，Z3 不支持的功能。

我将如何处理这个

你现在正在做的是一个很好的技巧，它允许 Z3fib尽可能多地扩展定义以证明一个问题unsat。但它不能很好地与模型查找器配合使用，因为您间接引入了递归定义。

因此，如果 Z3 报告，unsat那么您就知道您的程序是正确的。如果它报告unknown，您必须开始一个迭代过程。在此之前，您删除第二个断言(= (fib n) (fakeFib n))以防止构建模型的无限循环。

  1. 在每次迭代中，您提供 的 k 展开fib，其中fib(k+1)根据 抽象fakeFib。你可以不fakeFib n加约束，或者你可以对其施加轻微的约束（例如必须是一个正整数），而不添加递归。
  2. 如果 Z3 报告unsat，那么您的程序是正确的。
  3. 如果 Z3 报告sat，您必须检查返回的模型是否与fib. 如果它是一致的，那么你有一个反例。如果不一致，则增加k并转到步骤 1。

您可能想阅读有关 k-induction 的内容，我建议您或多或少是这样。

于 2015-11-16T21:36:04.947 回答