Z3 Forall阵列 - 编程之家

如何解决Z3 Forall阵列

Z3提供了一个未知的简单问题：

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

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

这是引起问题的原因，因为我要解决的问题类别更像是

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

单独否定所有人的问题并不相同，因此无法在此处完成。有什么方法可以让Z3遇到这种问题，从而得出un / sat结果？

解决方法

SMT求解器总是带有量词的问题，特别是如果它们涉及数组和交替量词（如您的示例）时，尤其如此。您基本上拥有mat["A","B"] <- 7。 Z3或任何其他SMT求解器将很难处理这类问题。

当您像在exits u. forall y. P(u,y)位于顶层或与forall嵌套的情况下那样进行量化断言时，逻辑将变为半确定的。 Z3使用MBQI（基于模型的量化器实例化）来启发式地解决此类问题，但这样做常常会失败。问题不仅仅在于z3不能胜任：没有针对此类问题的决策程序，而z3尽其所能。

您可以尝试为此类问题提供量词模式以帮助z3，但我认为没有简单的方法可以将其应用于您的问题。（当您具有未解释的函数和量化的公理时，将应用量词模式。请参见https://rise4fun.com/z3/tutorialcontent/guide#h28）。因此，我认为它不会为您服务。即使这样做，模式也很难编程，并且对于规范中可能看起来无害的更改也不可靠。

如果要处理这样的量词，那么SMT求解器可能不太适合。研究诸如Lean，Isabelle，Coq等的半自动定理证明者，它们旨在以更加严格的方式处理量词。当然，您失去了完全的自动化功能，但是其中大多数工具都可以使用SMT求解器来释放“足够简单”的子目标。这样，您仍然可以手动执行“繁重”操作，但是大多数子目标由z3自动处理。（特别是对于精益而言，请参见此处：https://leanprover.github.io/）

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

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

运行上面的代码，您将得到unsat作为答案。

对于第二个程序，别名答案可能对您有用。