创建一个固定大小的数组并初始化它 [英] Create an array with fixed size and initialize it
问题描述
我将创建一个固定大小的数组并用一些值对其进行初始化.
I'm going to create an array with fixed size and initialize it with some values.
例如以下 C++ 代码:
For example, the following C++ code:
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 中是否有一些实用程序可以对其进行建模?
Are there some utilities in Z3 to model it?
推荐答案
Z3 支持数组理论，但通常用于编码无界数组，或非常大的数组.大，我的意思是公式中数组访问(即选择)的数量比数组的实际大小小得多.我们应该问自己:我们真的需要数组来建模/解决问题 X 吗?".对于像您的示例中那样的固定大小数组，我们可以为每个数组位置使用不同的变量.例如:a0 for a[0]，a1 for a[1]，等等.当然，如果我们不使用理论，那么对诸如 a[i] 之类的数组访问进行编码必须编码为一个大 if-then-else 项，例如
Z3 supports the array theory, but is usually used to encode unbounded arrays, or arrays that are very big. By big, I mean the number of array accesses (i.e., selects) in your formula is much smaller than the actual size of the array. We should ask ourselves : "do we really need arrays for modeling/solving problem X?". For fixed size arrays like in your example, we can use a different variable for every array position. Example: a0 for a[0], a1 for a[1], etc. Of course, if we do not use theories, then encoding an array access such as a[i] must be encoded as a big if-then-else term such as
(ite (= i 0) a0 (ite (= i 1) a1 ...))
如果数组大小已知并且很小，那么这通常是对问题进行编码的最有效方法.
If the array size is known and small, then this is usually the most efficient approach for encoding a problem.
另一方面，如果您决定使用数组理论，则可以将问题中的初始化编码为:
On the other hand, if you decide to use the array theory, you can encode the initialization in your question as:
(declare-const a (Array Int Int))
(assert (= (select a 0) 10))
...
(assert (= (select a 7) 7))
以下是以 SMT 2.0 格式编码的整个示例:
Here is the whole example encoded in SMT 2.0 format:
请注意对这个数组的更新进行编码.比如C语句a[3] = 5，我们必须创建一个新的数组变量来表示这个赋值后的数组.最紧凑的方式是使用 store 表达式:
Note that to encode an update on this array. For example, the C statement a[3] = 5, we must create a new array variable representing the array after this assignment. The most compact way uses the store expression:
(declare-const a1 (Array Int Int))
(assert (= a1 (store a 3 5)))
这是更新的完整示例.
您也可以考虑 Python/C++/.Net API.它们使我们能够以更紧凑的方式对像您这样的示例进行编码.这个想法是实现对常用模式(如数组初始化)进行编码的函数.这是您在 Python 中的数组初始化示例:
You may also consider the Python/C++/.Net APIs. They allow us to encode examples like yours in a much more compact way. The idea is to implement functions that encode commonly used patterns such as array initialization. Here is your array initialization example in Python:
这篇关于创建一个固定大小的数组并初始化它的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！
