Хеширование выражений в 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, Эта "особенность" удобна для написания примеров Z3 на Python, но имеет неприятный побочный эффект: класс словаря 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)]