如何将x-d列表转换为数组？

Question

从其他问题中，我知道如何将一维列表转换为数组。里面的“Store”功能可以完成这个。但是，我想得到一个通用的方法来完成这项工作。

这是一个解释我的问题的例子：

i, j = Ints('i j')
VG = [[0, 0, 0], [0, 0, 0], [0, 0, 0], [0, 0, 0], [0, 0, 0], [0, 0, 0], [0, 0, 0], [0, 0, 0], [0, 0, 0]]
A = Array('A',IntSort(),ArraySort(IntSort(), IntSort()))

我需要使数组 A 等于列表 VG，因为我将添加一些如下约束：

s = Solver()
s.add(FORALL([i,j],Implies(And(i>=0, i<9, j>=0, j<3), A[i][j]>=0)))

如果我使用列表 L 来执行此操作：

s.add(FORALL([i,j],Implies(And(i>=0, i<9, j>=0, j<3), VG[i][j]>=0)))

z3 报告以下错误消息：

s.add(ForAll([i,j],Implies(And(i>=0, i<9, j>=0, j<3), VG[i][j]>=0)))
                                                          ~~^^^
TypeError: list indices must be integers or slices, not ArithRef

我在Stack Overflow上搜索了有关此错误消息的信息，比如这个Error with quantifier in Z3Py，所以我想用这个方法来解决我的问题。但是当列表的维度更多时，这个方法似乎不起作用。

我不知道列表有多少维，也不知道数组中每个维的大小。我所拥有的只是一个列表，就像上面的“VG”一样，我需要获得一些约束的结果，例如“VG[i][j]>0”，那么如何解决呢？还有更好的方法吗？

Answer 1

简短回答：如果您事先不知道输入数组的尺寸，则无法使用 SMTLib 数组。 SMTLib 数组具有显式声明的常量维度：它们覆盖声明类型的整个范围；他们不会根据您的输入“调整”其大小。

但是你正在使用 z3py 编程；所以你需要做的是根据输入列表的形状动态声明你的数组。一般来说，这可能很容易出错，因为您编写的每个表达式都必须考虑这种可变性；但这是使用内部数据结构处理此类问题的唯一方法。 （另一种方法可能是声明您自己的数据类型；但这本身可能会变得相当麻烦。）

作为概念验证，以下内容将在假设下起作用：

• 输入的每个元素都具有完全相同的形状
• 输入中没有空列表作为元素

from z3 import *

# Assumes:
#    1. each element of the input has the exact same shape
#    2. There are no empty lists
# Otherwise, you can't map it to SMTLib anyhow; unless you
# make some further assumptions.
def smtType (a):
    if type(a) != list:
        return IntSort()
    else:
        return ArraySort(IntSort(), smtType(a[0]))

一些测试：

print(smtType([0]))
print(smtType([[0]]))
print(smtType([[[0]]]))
print(smtType([[[[0]]]]))

打印：

Array(Int, Int)
Array(Int, Array(Int, Int))
Array(Int, Array(Int, Array(Int, Int)))
Array(Int, Array(Int, Array(Int, Array(Int, Int))))

您可以使用此方法来跟踪“维度”并相应地编写代码。不幸的是，这并不是很容易，但是在强类型 SMTLib 理论中没有其他方法可以对此进行编码。