Z3 Seq Int 中的最大元素

Question

我正在尝试编写一个在 Seq Int 上运行的 max 函数。它应该return具有最大值的索引。这是我拥有的：

(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（就像它应该的那样）。我在这里错过了什么吗？有没有办法正确定义最大值？

Answer 1

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

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

(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)

如果你运行这个，它成功地说：

sat

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

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 答案，我也不会指望求解器的响应。

长话短说 递归需要归纳，如果这是您的规范所要求的，请使用理解归纳的工具。 Isabelle、HOL、Coq、Agda、Lean；仅举几例。有很多选择。并且大多数这些工具都会在后台自动调用 z3（或其他 SMT 求解器）以根据需要（或根据用户的指导）建立属性；这样你就可以两全其美了。

Z3 Seq Int 中的最大元素

max element in Z3 Seq Int

max

z3

seq