From 91d6b2cbbb969655d5ba55c5bc25f2b23f1907d2 Mon Sep 17 00:00:00 2001 From: Andres Notzli Date: Tue, 1 Mar 2016 00:21:10 -0800 Subject: [PATCH] [Z3py] Consistent behavior of eq and ne for FP Before, x == y and x != y were returning inconsistent expressions (i.e. `Not(x == y)` was not the same as `x != y`): >>> x = FP('x', Float32()) >>> y = FP('y', Float32()) >>> (x == y).sexpr() '(= x y)' >>> (x != y).sexpr() '(not (fp.eq x y))' `=` does not have the same semantics as `fp.eq` (e.g. `fp.eq` of +0.0 and -0.0 is true while it is false for `=`). This patch removes the __ne__ method from FPRef, so `x == y` and `x != y` use the inherited operations while fpEQ and fpNEQ can be used to refer to `fp.eq(..)`/`Not(fp.eq(..))`. --- src/api/python/z3.py | 4 ---- 1 file changed, 4 deletions(-) diff --git a/src/api/python/z3.py b/src/api/python/z3.py index 305733aa7..814198d22 100644 --- a/src/api/python/z3.py +++ b/src/api/python/z3.py @@ -8099,10 +8099,6 @@ class FPRef(ExprRef): def __gt__(self, other): return fpGT(self, other, self.ctx) - def __ne__(self, other): - return fpNEQ(self, other, self.ctx) - - def __add__(self, other): """Create the Z3 expression `self + other`.