9

我将创建一个具有固定大小的数组并用一些值对其进行初始化。

例如，以下 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 中是否有一些实用程序可以对其进行建模？

4

2 回答 2

15

Z3 支持数组理论，但通常用于编码无界数组或非常大的数组。大，我的意思是公式中的数组访问（即选择）的数量远小于数组的实际大小。我们应该问自己：“我们真的需要数组来建模/解决问题 X 吗？”。对于您示例中的固定大小数组，我们可以为每个数组位置使用不同的变量。示例：a0for a[0]，a1fora[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

于 2012-06-17T06:37:07.993 回答
1

我同意莱昂纳多的回答，尤其是数组旨在模拟大输入范围。没有真正的方法来定义固定大小的数组（除非您使用有限输入排序，例如BitVecSort(3)）。

由于 Z3Py (Python) 示例被删除，我想添加我自己的解决方案。此函数指定一系列数组条目，从起始地址开始。（断言存储在一个Solver对象中。）

def assert_array(solver, array, start_index, data):
    for offset in range(len(data)):
        solver.add(array[start_index + offset] == data[offset])

请注意，这是SMT 2.0 中array[idx]的 Z3Py 等效项。(select array idx)问题中的数组可以这样建模：

s = Solver()
a = Array('a', IntSort(), IntSort())
data = [10, 23, 27, 12, 19, 31, 41, 7]
assert_array(s, a, 0, data)

print s
#[a[0] == 10,
# a[1] == 23,
# a[2] == 27,
# a[3] == 12,
# a[4] == 19,
# a[5] == 31,
# a[6] == 41,
# a[7] == 7]
于 2018-10-09T11:51:40.380 回答