Z3 将数组的默认值设置为零

Question

我正在尝试求解数组表达式的模型，其中数组的默认值等于 0。

例如，我正在尝试解决这个例子，但我一直得到未知的结果

(declare-const arr (Array Int Int))
(declare-const arr2 (Array Int Int))
(declare-const a Int)
(declare-const b Int)

(assert (forall ((x Int)) (= (select arr x) 0)))

(assert (> a 0))
(assert (<= a 10))

(assert (= arr2 (store arr a 1337)))

(assert (> b 0))
(assert (<= b 10))


(assert (= (select arr2 b) 0))

(check-sat)
(get-model)

Answer 1

Patrick 关于不使用量词的建议很正确！他们会让你的生活更艰难。但是，您很幸运，因为 z3 为您的用例支持常量数组，这很常见。语法是：

(assert (= arr ((as const (Array Int Int)) 0)))

这确保 arr 的所有条目都为 0；不需要量化，z3 内部处理得很好。

因此，您的基准将是：

(declare-const arr (Array Int Int))
(declare-const arr2 (Array Int Int))
(declare-const a Int)
(declare-const b Int)

(assert (= arr ((as const (Array Int Int)) 0)))

(assert (> a 0))
(assert (<= a 10))

(assert (= arr2 (store arr a 1337)))

(assert (> b 0))
(assert (<= b 10))


(assert (= (select arr2 b) 0))

(check-sat)
(get-model)

很快就解决了。这样就可以让整个数组以0开头，修改自己感兴趣的范围；它可以像往常一样取决于变量，不需要提前知道。

Z3 将数组的默认值设置为零

Z3 set default value of array to zero

z3