Python：使用 Z3 数据类型访问数组/列表的第一个元素

Question

在 Python (Collab) 中，我有以下变量 c：

array([x_1 > 1000, y_1 < x_1 + 1], dtype=object)

其中x_1 > 1000 和y_1 < x_1 + 1 是z3 (py) 变量/谓词。我想完全访问它的“第一个元素”：数组/列表[x_1 > 1000, y_1 < x_1 + 1]，但我没有能力。

这些是我所做的尝试：

• c[0] 产生 x_1 > 1000 （当然，c[1] 产生 y_1 < x_1 + 1)。
• a, b = c 再次产生 a 为 x_1 > 1000 和 b 改为 y_1 < x_1 + 1。
• c.0 会产生错误（很明显，c.1 也会产生错误）。

我想访问数组的那个元素的原因是我想以自动方式执行以下 z3 计算：

And([x_1 > 1000, y_1 < x_1 + 1])。所以最好做类似And(c[0])的东西。

这可能是初学者的错误，但我看不到。有什么帮助吗？

---

编辑：

请注意，问And(c[0]) 的问题是我在做And(x_1 > 1000)，而我想执行：And(x_1 > 1000, y_1 < x_1 + 1)（即，显然是And(c[0],c[1])。

Answer 1

最好发布完整的代码段，即那些可以由读者加载和执行而不会填充缺失部分的代码段。否则真的很难复制/理解你正在尝试做什么以及你遇到了什么错误。

我不使用 collab（不确定它是什么），但如果 c 是一个列表，您可以使用 * 表示法将其内容转换为参数。像这样的：

from z3 import *

x_1, y_1 = Ints('x_1 y_1')
c = [x_1 > 1000, y_1 < x_1 + 1]

s = Solver()
s.add(And(*c))
print(s.sexpr())

打印出来：

(declare-fun x_1 () Int)
(declare-fun y_1 () Int)
(assert (and (> x_1 1000) (< y_1 (+ x_1 1))))

无论c 列表中有多少元素，这都会正常工作。请注意，这与z3无关，但它是一个Python习语。

我不确定您的 array 构造；但如果它可以变成一个列表，上面的技巧应该可以工作。这是你要找的吗？