Z3 Forall阵列 [英] Z3 Forall with array

问题描述

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

Z3 provides unknown for the simple problem:

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

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

I've found that it becomes sat if negate the forall, but this seems like a particularly simple thing to be unable to solve.

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

This is causing issues because the class of problems I want to solve are more like,

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

单单否定所有人的情况不一样的问题，因此无法在此处完成。有什么方法可以给Z3带来这种问题，以得到un / sat结果？

Where negating the forall alone is not the same problem, so that cannot be done here. Is there some way to pose this style of problem to Z3 to get an un/sat result?

推荐答案

总是存在量词的问题SMT求解器存在问题，尤其是像您的示例中那样涉及数组和交替量词时。您实际上有个出口u。永远P（u，y）。 Z3或任何其他SMT求解器将很难处理此类问题。

Problems with quantifiers are always problematic with SMT solvers, especially if they involve arrays and alternating quantifiers like in your example. You essentially have exits u. forall y. P(u, y). Z3, or any other SMT solver, will have hard time dealing with these sorts of problems.

当您像量化断言那样执行 forall 位于顶层或与存在嵌套，逻辑变得半可决定。 Z3使用MBQI（基于模型的量化器实例化）试探性地解决了此类问题，但这样做常常会失败。问题不仅仅在于z3不能胜任：没有针对此类问题的决策程序，而z3尽其所能。

When you have a quantified assertion like you do where you have forall's either at the top-level or nested with exists, the logic becomes semi-decidable. Z3 uses MBQI (model-based quantifier instantiation) to heuristically solve such problems, but it more often than not fails to do so. The issue isn't merely that z3 is not capable: There's no decision procedure for such problems, and z3 does its best.

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

You can try giving quantifier patterns for such problems to help z3, but I don't see an easy way to apply that in your problem. (Quantifier patterns apply when you have uninterpreted functions and quantified axioms. See https://rise4fun.com/z3/tutorialcontent/guide#h28). So, I don't think it'll work for you. Even if it did, patterns are very finicky to program with, and not robust with respect to changes in your specification that might otherwise look innocuous.

如果要处理这样的量词，那么SMT求解器可能不是一个很好的选择。研究诸如Lean，Isabelle，Coq等的半自动定理证明者，它们旨在以更加严格的方式处理量词。当然，您失去了完全的自动化，但是这些工具中的大多数可以使用SMT求解器来释放容易的子目标。足够。这样，您仍然可以进行重载操作。手动，但大多数子目标由z3自动处理。 （特别是在精益的情况下，请参见此处： https://leanprover.github.io/ ）

If you're dealing with such quantifiers, SMT solvers are probably just not a good fit. Look into semi-automated theorem provers such as Lean, Isabelle, Coq, etc., which are designed to deal with quantifiers in a much more disciplined way. Of course, you lose full automation, but most of these tools can use an SMT solver to discharge subgoals that are "easy" enough. That way, you still do the "heavy-lifting" manually, but most subgoals are automatically handled by z3. (Especially in the case of Lean, see here: https://leanprover.github.io/)

这篇关于Z3 Forall阵列的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！