arrays - 使用量词在 Z3 中重写代码

Question

伙计们

我正在使用 Microsft Z3 编写模型，我需要向其中添加以下断言：

(declare-const line (Array Int Int))

(assert (and (> (select line 1) 0) (< (select line 1) 4)))
(assert (and (> (select line 2) 0) (< (select line 2) 4)))
(assert (and (> (select line 3) 0) (< (select line 3) 4)))

如您所见，我要说明的是，我的 3 长度数组（称为line）只能包含 [1..3] 中的元素。这段代码完美地工作，但是，我希望能够使用量词只用一行代码做出这些断言。我试过了：

(assert (forall ((i Int)) (=> (and (> i 0) (< i 4)) (and (> (select line i) 0) (< (select line i) 4)))))

我虽然会工作......但在执行之后，Z3 返回了 unsat，这在以前版本的代码中没有发生。

为什么会这样？

这可能吗？