小编e.e*_*ann的帖子

我正在学习 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 )

我做对了吗？