创建一个固定大小的数组并初始化它

Question

我将创建一个固定大小的数组,并用一些值初始化它.

例如,以下C++代码:

a[0] = 10;
a[1] = 23;
a[2] = 27;
a[3] = 12;
a[4] = 19;
a[5] = 31;
a[6] = 41;
a[7] = 7;

Z3中是否有一些实用程序可以对其进行建模？

Answer 1

Z3支持数组理论,但通常用于编码无界数组或非常大的数组.大,我的意思是公式中的数组访问次数(即选择)远小于数组的实际大小.我们应该问自己:"我们真的需要数组来建模/解决问题X吗？".对于像示例中的固定大小数组,我们可以为每个数组位置使用不同的变量.示例:a0for a[0],a1for a[1]等.当然,如果我们不使用理论,那么编码一个数组访问,例如a[i]必须编码为一个大的if-then-else术语,如

(ite (= i 0) a0 (ite (= i 1) a1 ...))

如果数组大小已知且很小,那么这通常是编码问题的最有效方法.

另一方面,如果您决定使用数组理论,则可以将问题中的初始化编码为:

(declare-const a (Array Int Int))
(assert (= (select a 0) 10))
...
(assert (= (select a 7) 7))

以下是以SMT 2.0格式编码的整个示例:

http://rise4fun.com/Z3/iwo

请注意,要对此阵列进行更新编码.例如,在C语句中a[3] = 5,我们必须在此赋值后创建一个表示数组的新数组变量.最紧凑的方式使用store表达式:

(declare-const a1 (Array Int Int))
(assert (= a1 (store a 3 5)))

以下是更新的完整示例.

http://rise4fun.com/Z3/Kpln

您还可以考虑Python/C++/.Net API.它们允许我们以更紧凑的方式编码像你这样的例子.我们的想法是实现编码常用模式的函数,例如数组初始化.这是Python中的数组初始化示例:

http://rise4fun.com/Z3Py/AAD