3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-07 18:05:21 +00:00

[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(..))`.
This commit is contained in:
Andres Notzli 2016-03-01 00:21:10 -08:00
parent 4a15d756d7
commit 91d6b2cbbb

View file

@ -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`.