Z3 常量和 python 'in' 运算符

Question

我想知道使用 python 内置集类型和 z3 常量的成员测试是否安全。

假设有如下例子：

a = Int('a')
a2 = Int('a')

s = set()
s.add(a)

print(a2 in s)

最后一行 return True，这是我想要的行为（当 name 相同时）。但是，ExpRef 中的 __eq__() 运算符被重新定义为 return 约束 'self == other'，所以我不明白这个 True 来自哪里。当有两个具有不同 name 的常量时，in 运算符可能 return True 会发生吗？

Answer 1

是的，这样做是安全的。它之所以有效，是因为你实际上是在比较这些对象的底层表示（作为 AST），如果你有不同的名称，它们在这个意义上永远不会相等。

但我不得不说这很不正统。为了说明这一点，考虑一下：

from z3 import *

a = Int('a')
b = Int('b')
solver = Solver()
solver.add(a == b)

s = set()
s.add(a)
s.add(b)

print(s)

这将打印 {b, a}，即使我们明确断言 a 和 b 对求解器来说完全相同。这可能会导致混淆。

当然，这很可能正是您想要做的。也就是说，从语法上区分变量，而不考虑它们的值。如果你正在做 "meta" 级别的 z3 编程，我可以看到一些用例，即在它之上构建库，但一般来说，你应该避免在 z3py 中做任何检查对象身份的事情。如果您开始将对象身份和值身份混为一谈，它会变得非常混乱。人们通常需要符号编程中的值同一性，但这同样取决于您的用例。

Answer 2

__eq__ 实际上只是 returns 一个约束，但是 __bool__ 在该约束上 returns 一个布尔值，用于比较两个参数在语法上是否相等。所以基本上 __eq__ 以 a == a2 本身只是创建一个等式约束的方式重载，但在布尔上下文中使用它实际上使它比较 a 和 a2在语法上是相同的。所以两个同名的常量将比较相等，但不同名称的常量则不会。

__hash__ 也使用相同的相等概念定义。所以在集合中使用是安全的（或作为字典中的键）。

Z3 常量和 python 'in' 运算符

Z3 constants and python 'in' operator

z3

z3py