z3 - 我怎么知道z3中有多少值有一个数组？

Question

我正在使用 Z3py，但是当我定义一个数组时

array = Array('array', IntSort(), IntSort())

我不知道如何知道数组有多少个值。

标签： z3z3py

Answer 1

Z3（和 SMT）中的数组是无限大小的。参见，例如，创建一个固定大小的数组并初始化它