From 4f5a2e432d3c4df17c37ec2c083abf55b8e13911 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Mon, 14 Dec 2015 16:27:39 +0000 Subject: [PATCH 1/2] For for Python 3.x __eq__/__hash__. Fixes #377. --- src/api/python/z3.py | 11 +++++++++++ 1 file changed, 11 insertions(+) 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`. From e652b7d2c73a3105aff7d845aef0ad4f1daf578d Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Mon, 14 Dec 2015 16:31:10 +0000 Subject: [PATCH 2/2] Follow-up fix for #377. --- src/api/python/z3.py | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/api/python/z3.py b/src/api/python/z3.py index c17c19b82..864a92846 100644 --- a/src/api/python/z3.py +++ b/src/api/python/z3.py @@ -536,7 +536,7 @@ class SortRef(AstRef): def __hash__(self): """ Hash code. """ - ASTRef.__hash__(self) + AstRef.__hash__(self) def is_sort(s): """Return `True` if `s` is a Z3 sort. @@ -802,7 +802,7 @@ class ExprRef(AstRef): def __hash__(self): """ Hash code. """ - ASTRef.__hash__(self) + AstRef.__hash__(self) def __ne__(self, other): """Return a Z3 expression that represents the constraint `self != other`.