Z3 Seq Int 中的最大元素 [英] max element in Z3 Seq Int

问题描述

我正在尝试编写一个对 Seq Int 进行操作的 max 函数.它应该返回具有最大值的索引.这是我所拥有的:

I'm trying to write a max function that operates on Seq Int. It should return the index with maximal value. Here is what I have:

(declare-fun max ((Seq Int)) Int)
(assert (forall ((A (Seq Int)))
    (=>
        (> (seq.len A) 0)
        (and
            (<= 0 (max A))
            (<  (max A) (seq.len A))
            (forall ((i Int))
                (=>
                    (and
                        (<= 0 i)
                        (<  i (seq.len A)))
                    (<= (seq.nth A i) (seq.nth A (max A))))))))
)

 (assert (= (max (seq.++ (seq.unit 8) (seq.unit 3))) 0))
;(assert (= (max (seq.++ (seq.unit 8) (seq.unit 3))) 1))

(check-sat)

当我这样运行时，Z3 卡住.如果我改用注释行，Z3 会立即回答 unsat(就像它应该的那样).我在这里错过了什么吗?有没有办法正确定义最大值?

When I run it like this, Z3 gets stuck. If I use the commented line instead, Z3 immediately answers unsat (like it should). Am I missing something here? Is there a way to define max properly?

推荐答案

这种量化的问题并不适合 z3.(或任何其他 SMT 求解器.)要证明此类递归谓词的属性，您需要归纳.传统的 SMT 求解器没有归纳能力.

This sort of quantified problems are just not a good match for z3. (Or any other SMT solver.) To prove properties of such recursive predicates, you need induction. Traditional SMT solvers have no induction capabilities.

话虽如此，您可以通过将量化断言分开来帮助 z3，如下所示:

Having said that, you can help z3 by making your quantified assertions separated out, like this:

(declare-fun max ((Seq Int)) Int)
(assert (forall ((A (Seq Int))) (=> (> (seq.len A) 0) (<= 0 (max A)))))
(assert (forall ((A (Seq Int))) (=> (> (seq.len A) 0) (< (max A) (seq.len A)))))
(assert (forall ((A (Seq Int)) (i Int)) (=> (and (> (seq.len A) 0) (<= 0 i) (< i (seq.len A)))
                        (<= (seq.nth A i) (seq.nth A (max A))))))

(assert (= (max (seq.++ (seq.unit 8) (seq.unit 3))) 0))
;(assert (= (max (seq.++ (seq.unit 8) (seq.unit 3))) 1))

(check-sat)

如果你运行这个，它会成功说:

If you run this, it succesfully says:

sat

虽然这是正确的，但不要误以为您已经完全指定了 max 应该如何工作，否则 z3 可以处理所有此类问题.也就是说，让我们添加 (get-model) 看看它说了什么:

While this is correct, don't be fooled into thinking you've completely specified how max should work or z3 can handle all such problems. To wit, let's add (get-model) and see what it says:

sat
(model
  (define-fun max ((x!0 (Seq Int))) Int
    (ite (= x!0 (seq.++ (seq.unit 7718) (seq.++ (seq.unit 15) (seq.unit 7719))))
      2
      0))
)

哦，看，它只是找到了对 max 的解释，它甚至不满足您给出的量化公理.看起来这是一个 z3 错误，应该报告.但故事的寓意是一样的:序列逻辑和量词是一个软肋，即使你得到一个 sat 答案，我也不会指望求解器的响应.

Oh look, it simply found an interpretation of max that doesn't even satisfy the quantified axioms you've given. Looks like this is a z3 bug and should probably be reported. But the moral of the story is the same: Sequence logic and quantifiers are a soft spot, and I wouldn't count on the solver response even if you got a sat answer.

长话短说 递归需要归纳，如果这就是您的规范要求，请使用理解归纳的工具.伊莎贝尔、HOL、Coq、Agda、精益；仅举几例.有很多选择.并且大多数这些工具会自动调用 z3(或其他 SMT 求解器)以根据需要(或根据用户的指导)以任何方式建立属性；所以你拥有两全其美的优势.

Long story short Recursion requires induction, and if that's what your specification requires, use a tool that understands induction. Isabelle, HOL, Coq, Agda, Lean; to name a few. There are many choices. And most of those tools automatically call z3 (or other SMT solvers) under the hood to establish properties as necessary (or as guided by the user) anyhow; so you have the best of both worlds.

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