Z3 无法为带有量词和模式的简单公式找到令人满意的分配

Question

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

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

(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 层）。但是我可以忍受这个限制以避免匹配循环。

代码的"bug"是我错误地初始化了一个变量，这最终导致了最后一个断言中的错误组件(= 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 作为比较，它立即显示 "unknown"。所以我的问题似乎不是 Z3 特有的。
公式显然可以满足。 (= 1 (fib 0)) 是 false，因此整个最后的断言自动为真。 (>= n 0)也很容易满足

Answer 1

我不是 Z3 专家，但也许我可以提供一些启示。

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

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

提供了两个定义

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

我将如何处理这个问题

你现在正在做的是一个很好的技巧，它允许 Z3 根据需要扩展 fib 定义以证明问题 unsat。但是它不适合模型查找器，因为你间接引入了一个递归定义。

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

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

您可能想阅读有关 k 归纳法的内容，我建议您大致了解一下。

Z3 无法为带有量词和模式的简单公式找到令人满意的分配

Z3 unable to find satisfying assignment for simple formula with quantifiers and patterns

formal-verification

smt

z3