Expression Hashing in Z3Python

Question

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

Answer 1

There is no reason not to call him __hash__(). I named it hash()because I am new to Python. I will add __hash__()in the next version (Z3 4.2).

EDIT: as pointed out in the comments, we also need __eq__or __cmp__to use the Z3 object as a key in the Python dictionary. Unfortunately, the method __eq__(defined in ExprRef) is used to create Z3 expressions. That is, if athey brefer to expressions Z3, then a == breturns an object of expression Z3 representing the expression a = b. This "function" is convenient for writing Z3 examples in Python, but it has an unpleasant side effect: the Python dictionary class will assume that all Z3 expressions are equal to each other. This is actually even worse, since the Python dictionary only calls a method __eq__for objects that have the same hash code. So, if we define__hash__(), we may have an 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 who want to use Z3 expressions as keys in dictionaries can 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)]