python - Z3Python 中的散列表达式

Question

看起来 z3 表达式有一个hash()方法，但没有__hash__()。有理由不使用__hash__()吗？这允许表达式是可散列的。

Answer 1

没有理由不调用它__hash__()。我之所以叫它是hash()因为我是 Python 新手。我将__hash__()在下一个版本（Z3 4.2）中添加。

编辑：正如评论中所指出的，我们还需要__eq__或__cmp__能够使用 Z3 对象作为 Python 字典中的键。不幸的是，该__eq__方法（定义于ExprRef）用于构建 Z3 表达式。也就是说，如果a和b正在引用 Z3 表达式，则a == b返回表示表达式的 Z3 表达式对象a = b。这个“特性”便于用 Python 编写 Z3 示例，但它有一个讨厌的副作用：Python 字典类将假定所有 Z3 表达式彼此相等。实际上，情况更糟，因为 Python 字典只调用__eq__具有相同哈希码的对象的方法。因此，如果我们定义__hash__()我们可能有这样的错觉，即使用 Z3 表达式对象作为 Python 字典中的键是安全的。出于这个原因，我不会包括__hash__()在课堂AstRef上。想要在字典中使用 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)]