我目前正在Z3之上为我的编程语言编写一个自动验证程序，这是一个有趣的项目，我正试图用它来证明使用循环的fibonacci实现等同于递归实现。
如果输入程序是正确的，也就是说，它为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)
注意，这两个量词表示fibonacci的递归定义。我的一个朋友告诉我这个避免匹配循环的技巧：我没有将fib定义为递归函数，而是引入了另一个函数fakeFib，我没有提供它的定义，我在fib的递归定义中使用了它。此外，我告诉验证器它们是相等的，但那个量词只得到fib的模式，而不是fakeFib的模式。由于限制性的模式，它是不完整的，也就是说，它只能证明程序的正确性，只要看一级递归就足以证明它（但它可以很容易地扩展到k级）。但为了避免匹配循环，我可以接受这种限制。
代码的"错误"是我错误地初始化了一个变量，这最终导致了最后一个断言中的错误组件(= 1 (fib 0))。对于正确的程序，它将是(= 0 (fib 0))。
一些观察：
- 如果我用
(= 0 (fib 0))替换(= 1 (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，因此整个最后断言自动为真。CCD_ 11也很容易满足
我不是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归纳法的书，我建议你或多或少就是这样。