使用 Z3 求解器求解长度为任意大小数组的条件

Question

我正在学习 Z3 求解器。我有一个关于数组和相关条件的问题。特别是，我必须创建 Z3py 代码来解决以下 if 条件：

totalAccounts = [ 1, 2, 3, 4, 5 ]    

def (myAccounts):
   cnt = len(myAccounts)
   if (cnt > 10) doSomething()

myAccounts是一个整数列表，是列表的子集totalAccounts。通过的条件cnt > 10取决于列表的长度myAccounts。

我想我需要表示为 Z3 的数组并使用函数myAccounts复制其中的值。totalAccountsStore

MYACCOUNTS = Array ('MYACCOUNTS', IntSort(), IntSort())
I = Int('I')
i = 0
for elem in totalAccounts:
  MYACCOUNTS = Store(MYACCOUNTS, i, elem)
  i = i + 1

但我不知道如何在创建添加到求解器的条件时表示此类数组的长度：

solver = Solver()
solver.add( ??? > 10 )

我做对了吗？

Answer 1

SMTLib 数组（以及 z3 和 z3py 数组）按其整个域类型进行索引。在您的示例中，索引类型为Int()，因此数组具有任何整数值的元素。请注意，这与编程语言中对数组的通常处理不同，在编程语言中，您通常会获得数组的“长度”。您可以在此处阅读有关 SMTLib 数组的更多信息：http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2017-07-18.pdf（特别是第 39 页。）

为了对数组长度的任何概念进行建模，通常在一个单独的符号变量中跟踪它，并且每当表达属性时，通常都会引用该变量来完成。准确地询问你想要解决的问题会让你走得更远。

您可能还想查看 Z3 指南 ( https://rise4fun.com/z3/tutorial/guide )，其中也有关于数组的部分。Stack-overflow 也有关于 z3py 中数组使用的类似问题，这是一个与当前上下文相关的示例答案：/sf/answers/1662041531/