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 returns 您正在应用的函数，arg 获取相应的子项。请注意 z3 如何在内部重新排列您的表达式；它倾向于在比较中把变量放在一边，常量放在另一边，而不改变意思。

请注意，如果将其应用于不是应用程序的表达式，上述操作将会失败。还有一些谓词可以识别您正在处理的节点类型，但它们更适合 advanced/internal 使用。（is_app 是最明显的，如果表达式是函数对参数的应用。）

检查应用程序是否为 AND

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

print(is_and(phi_2))

为上述 phi_2 的定义打印 True。参见 https://z3prover.github.io/api/html/namespacez3py.html#a29dab09fc48e1eaa661cc9366194cb29 for documentation. There are recognizers for many of the constructors you might need. And if any is missing, look at the definition of is_and itself in the linked documentation to find out the robust way of adding new ones. (i.e., by comparing to the official enumeration of all operations, as given by: 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。因此，永远不要相信任何东西的名称，并始终使用为此目的定义的内部常量。

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

Python-Z3: How can I access the elements of an And

python

list

first-order-logic

z3

z3py

检查应用程序是否为 AND

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