【发布时间】：2020-01-14 10:05:53
【问题描述】：
我正在使用 Z3py，但是当我定义一个数组时
array = Array('array', IntSort(), IntSort())
我不知道如何知道数组有多少个值。
【问题讨论】：
-
尝试使用内置的
len(array)函数，如果这不起作用，请尝试查看哪些属性可用于数组对象，dir(array)
【发布时间】：2020-01-14 10:05:53
【问题描述】：
Z3（和 SMT）中的数组是无限大小的。例如，请参阅Create an array with fixed size and initialize it
【讨论】：
-
感谢您的回复，但如果我定义了 5 个“数组”实例，我如何知道存在 5 个实例？例如
array[0] = ... ,array[1] = ... , array[2] = ..., array[3] = ... , array[4] = ...那么，如果我使用 int i = 5 之类的值，如果数组的实例数为 5 或更少，我如何与 i 进行比较？ -
正如 Christoph 所提到的，将为每个整数元素定义一个从
IntSort到IntSort的数组。 （从这个意义上说，它更像是一个函数。）所以，问“5 或更少”是没有意义的。答案是，它总是大于 5：每个整数值都有一个元素。不要将它与 C 或 Java 等语言中的数组混为一谈。