python - 使用 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 的长度列表。

我想我需要代表myAccounts作为 Z3 的数组并复制 totalAccounts 中的值使用函数Store对其进行.

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 中数组使用的类似问题，这是一个与当前上下文相关的示例答案:https://stackoverflow.com/a/23743450/936310