diff --git a/src/api/python/z3.py b/src/api/python/z3.py index f5b2a1e6e..c17c19b82 100644 --- a/src/api/python/z3.py +++ b/src/api/python/z3.py @@ -285,6 +285,9 @@ class AstRef(Z3PPObject): def __repr__(self): return obj_to_string(self) + def __eq__(self, other): + return self.eq(other) + def __hash__(self): return self.hash() @@ -531,6 +534,10 @@ class SortRef(AstRef): """ return not Z3_is_eq_sort(self.ctx_ref(), self.ast, other.ast) + def __hash__(self): + """ Hash code. """ + ASTRef.__hash__(self) + def is_sort(s): """Return `True` if `s` is a Z3 sort. @@ -793,6 +800,10 @@ class ExprRef(AstRef): a, b = _coerce_exprs(self, other) return BoolRef(Z3_mk_eq(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx) + def __hash__(self): + """ Hash code. """ + ASTRef.__hash__(self) + def __ne__(self, other): """Return a Z3 expression that represents the constraint `self != other`.