Hashing expressions in Z3Python

Question

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.

Answer 1

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

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