Z3Py：创建未解释类型的常量列表

Question

我有未解释的排序A

sortA = DeclareSort('A')

和一个函数foo：

foo = Function('foo',sortA,sortA,BoolSort())

现在，我想定义一个类型为A的常量列表。我的尝试是：

X = [ Consts("c_%s" % i,sortA) for i in range(10) ]

但是，这不起作用，因为

s.add(foo(X[0],X[1]))

给出“预期的Z3表达式”错误。我会很感激的帮助:)

Answer 1

Consts创建一个常量list，并且该列表不是Z3表达式（而是Python的Z3表达式列表）。而是按预期使用Const。