Z3 Forall 带阵列答案

【问题标题】：Z3 Forall with arrayZ3 Forall 带阵列
【发布时间】：2020-12-15 15:43:51
【问题描述】：

Z3 为简单问题提供未知数：

(assert
(forall ((y (Array Int Int)))
   (= (select y 1) 0))
 )
(check-sat)

我发现如果否定forall就会变成sat，但这似乎是一件特别简单的事情无法解决。

这会导致问题，因为我要解决的问题类别更像是，

(declare-fun u () Int)
(assert
 (forall ((y (Array Int Int)) )
     (=> 
        (= u 0) (<= (select y 1) 0))
 )
)
(check-sat)

单独否定 forall 不是同一个问题，所以这里不能这样做。有什么方法可以向 Z3 提出这种类型的问题以获得 un/sat 结果？

【问题讨论】：

标签： arrays z3 quantifiers

【解决方案1】：

有一个额外的右（右）括号，需要删除。另外，在 forall 语句之前添加 assert。

(assert ( forall ( (y (Array Int Int) ) ) 
   (= (select y 1) 0) 
))
(check-sat)

运行上面的代码，你应该得到 unsat 作为答案。

对于第二个程序，别名的回答可能对你有用。

【讨论】：

rise4fun.com/Z3/FKO1b 来自在线求解器，结果未知。
我在终端上运行了它。我不知道，为什么会显示 - 在其网站上未知。
不管怎样，你的问题中多了一个右括号，需要去掉。

【解决方案2】：

量词问题对于 SMT 求解器总是有问题，尤其是当它们涉及数组和交替量词时，例如您的示例。你基本上有exits u. forall y. P(u, y)。 Z3 或任何其他 SMT 求解器将很难处理这类问题。

当你有一个量化的断言时，就像你在顶层有forall 或者嵌套在exists 中一样，逻辑就变成了半可判定的。 Z3 使用 MBQI（基于模型的量词实例化）来启发式地解决此类问题，但它往往不能这样做。问题不仅仅在于 z3 没有能力：没有针对此类问题的决策程序，而 z3 已尽力而为。

您可以尝试为此类问题提供量词模式以帮助 z3，但我没有看到将其应用于您的问题的简单方法。（当你有未解释的函数和量化的公理时，量词模式适用。见https://rise4fun.com/z3/tutorialcontent/guide#h28）。所以，我不认为它会为你工作。即使这样做了，模式编程也非常挑剔，并且对于您的规范中可能看起来无害的更改并不健壮。

如果您正在处理此类量词，则 SMT 求解器可能不太适合。研究半自动定理证明器，例如 Lean、Isabelle、Coq 等，它们旨在以更规范的方式处理量词。当然，您会失去完全自动化，但这些工具中的大多数都可以使用 SMT 求解器来实现足够“简单”的子目标。这样，您仍然可以手动执行“繁重的工作”，但大多数子目标都由 z3 自动处理。（特别是在精益的情况下，请参见此处：https://leanprover.github.io/）

【讨论】：