Z3Python 中的散列表达式 [英] Hashing expressions in Z3Python

问题描述

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

It looks like z3 expression has a hash() method but not __hash__(). Is there a reason why not using __hash__() ? This allows the expression to be hashable.

推荐答案

没有理由不叫它__hash__().我称它为 hash() 因为我是 Python 新手.我将在下一个版本 (Z3 4.2) 中添加 __hash__().

There is no reason for not calling it __hash__(). I called it hash() because I'm new to Python. I will add __hash__() in the next release (Z3 4.2).

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

as pointed out in the comments, we also need __eq__ or __cmp__ to be able to use a Z3 object as a key in a Python dictionary. Unfortunately, the __eq__ method (defined at ExprRef) is used to build Z3 expressions. That is, if a and b are referencing Z3 expressions, then a == b returns the Z3 expression object representing the expression a = b. This "feature" is convenient for writing Z3 examples in Python, but it has a nasty side-effect: the Python dictionary class will assume that all Z3 expressions are equal to each other. Actually, it is even worse, since the Python dictionary only invokes the method __eq__ for objects that have the same hashcode. Thus, if we define __hash__() we may have the illusion that is safe to use Z3 expression objects as keys in Python dictionaries. For this reason, I will not include __hash__() in the class AstRef. Users that want to use Z3 expressions as keys in dictionaries may use the following trick:

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)]

这篇关于Z3Python 中的散列表达式的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！