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

Question

我正在学习 Z3 解算器。我对数组和相关条件有疑问。特别是，我必须创建 Z3py 代码来解决以下 if 条件：

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

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

myAccounts 是整数列表，是列表 totalAccounts 的子集。要通过的条件是 cnt > 10 取决于 length of myAccounts list.

我想我需要将 myAccounts 表示为 Z3 的数组，并使用函数 Store.

复制 totalAccounts 中的值

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()，因此该数组具有一个任意整数值的元素。请注意，这与编程语言中数组的通常处理方式不同，在编程语言中您通常会得到数组的 "length"。您可以在此处阅读有关 SMTLib 数组的更多信息：http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2017-07-18.pdf（尤其是第 39 页。）

为了对数组长度的任何概念进行建模，人们通常会在单独的符号变量中对其进行跟踪，并且无论何时表达属性，通常都会参考该变量来完成。准确询问您要解决的问题会让您走得更远。

您可能还想查看 Z3 指南（https://rise4fun.com/z3/tutorial/guide), which also has a section on arrays. Stack-overflow also has similar questions regarding array usage in z3py, here's one example answer, relevant to the current context:

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

Solve using Z3 solver a condition with a length of an arbitrary size array

python

solver

z3

z3py