我正在使用.NET绑定，但假设API是一致的，我希望答案是跨语言 .

我有这个SMT脚本，它确保3d数组的每个元素都被置为等于5 .

(declare-const array0 (Array Int Int))
(assert (= array0 ((as const (Array Int Int)) 5)))

(declare-const array1 (Array Int (Array Int Int)) )
(assert (= array1 ((as const (Array Int (Array Int Int))) array0)))

(declare-const array2 (Array Int (Array Int (Array Int Int))) )
(assert (= array2 ((as const (Array Int (Array Int (Array Int Int)))) array1)))

所以我没有为每个数组使用declare-const，我知道我可以将其压缩如下：

(declare-const array0 (Array Int (Array Int (Array Int Int))) )
(assert (= array0 ((as const (Array Int (Array Int (Array Int Int)))) ((as const (Array Int (Array Int Int))) ((as const (Array Int Int)) 5)))))

但是如何使用API的mkConstArray函数来实现此压缩版本 . 将这些 (as const...) 表达式放在一起的运算符是什么？

z3