python - Z3Python でのハッシュ式

Question

z3式にはhash()メソッドがありますが、ないよう__hash__()です。を使用しない理由はあり__hash__()ますか? これにより、式をハッシュ可能にすることができます。

Answer 1

それを呼び出さない理由はありません__hash__()。hash()私はPythonが初めてなので、それを呼び出しました。__hash__()次のリリース (Z3 4.2) で追加します。

編集:コメントで指摘されているように、Z3 オブジェクトを Python 辞書のキーとして使用する必要がある__eq__か__cmp__、使用できるようにする必要があります。残念ながら、__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)]