Z3Python中的哈希表达式

Question

看起来z3表达式有一个hash()方法，但没有__hash__()。有没有理由不使用__hash__()？这使得表达式可以散列。在

Answer 1

没有理由不调用它__hash__()。我把它命名为hash()，因为我是Python新手。我将在下一个版本（z34.2）中添加__hash__()。在

编辑：正如评论中所指出的，我们还需要__eq__或{}来使用Z3对象作为Python字典中的键。不幸的是，__eq__方法（定义在ExprRef）被用来构建Z3表达式。也就是说，如果a和b引用Z3表达式，那么a == b返回表示表达式a = b的Z3表达式对象。这个“特性”对于用Python编写Z3示例很方便，但是它有一个令人讨厌的副作用：Python字典类将假定所有Z3表达式彼此相等。实际上，情况更糟，因为Python字典只为具有相同hashcode的对象调用__eq__方法。因此，如果我们定义__hash__()，我们可能会有一种错觉，即在Python字典中使用Z3表达式对象作为键是安全的。因此，我将不在类AstRef中包含__hash__()。 想要在字典中使用Z3表达式作为键的用户可以使用以下技巧：

from z3 import *

class AstRefKey:
    def __init__(self, n):
        self.n = n
    def __hash__(self):
        return self.n.hash()
    def __eq__(self, other):
        return self.n.eq(other.n)

def askey(n):
    assert isinstance(n, AstRef)
    return AstRefKey(n)


x = Int('x')
y = Int('y')
d = {}
d[askey(x)] = 10
d[askey(y)] = 20
d[askey(x + y)] = 30
print d[askey(x)]
print d[askey(y)]
print d[askey(x + y)]
n = simplify(x + 1 + y - 1)
print d[askey(n)]