Python-Z3：如何访问 And 的元素

Question

我可以用一个列表来表示连词。例如，让

x_1 = Int('x_1')
the_list = [Not(500 <= x_1), Not(x_1 <= 500), Not(x_1 <= 300)]

phi_1 = And(the_list)

（即phi_1 = And([Not(500 <= x_1), Not(x_1 <= 500), Not(x_1 <= 300)])）

然后，我可以执行the_list[0]，得到Not(500 <= x_1)。

但是，假设我得到了没有列表的连词：

phi_2 = And(Not(500 <= x_1), Not(x_1 <= 500), Not(x_1 <= 300))

如何像访问列表一样访问And 的元素？

Answer 1

使用decl 和arg 调用：

from z3 import *

x_1 = Int('x_1')

phi_2 = And(Not(500 <= x_1), Not(x_1 <= 500), Not(x_1 <= 300))

print(phi_2.decl())
for i in range(phi_2.num_args()):
   print(phi_2.arg(i))

打印出来：

And
Not(x_1 >= 500)
Not(x_1 <= 500)
Not(x_1 <= 300)

decl 返回您正在应用的函数，arg 获取相应的子函数。请注意 z3 如何在内部重新排列您的表达式；它倾向于将变量放在一侧，将常量放在另一侧进行比较，而不改变含义。

请注意，如果您将其应用于不是应用程序的表达式，上述操作将失败。还有一些谓词可以识别您正在处理的节点类型，但它们更适合高级/内部使用。（is_app 是最明显的一个，如果表达式是函数的应用程序，则返回 true论据。）

检查应用程序是否为 AND

如果给定一个表达式并想知道它是否是And 的应用程序，请使用is_and 函数：

print(is_and(phi_2))

为phi_2 的上述定义打印True。有关文档，请参阅 https://z3prover.github.io/api/html/namespacez3py.html#a29dab09fc48e1eaa661cc9366194cb29。您可能需要的许多构造函数都有识别器。如果缺少任何内容，请查看链接文档中is_and 本身的定义，以找出添加新定义的可靠方法。 （即，通过与所有操作的官方枚举进行比较，如下所示：https://z3prover.github.io/api/html/group__capi.html#ga1fe4399e5468621e2a799a680c6667cd）。

为什么与字符串比较不是一个好主意

这有几个原因，最明显的原因是对拼写错误的可维护性、z3 未来打印内容的更改等。但更重要的是，与字符串的比较可能会以下列方式失败：

from z3 import *

MyBadFunction = Function('And', IntSort(), IntSort())
print(str(MyBadFunction(IntVal(1)).decl()) == 'And')

如果你运行它，你会看到它很高兴地打印出True，这不是你想要的。如果您改用is_and，它将正确打印False。因此，永远不要相信任何东西的名称，并始终使用为此目的而定义的内部常量。