mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-12 17:06:14 +00:00
Code Activity

Fix documentation for floating-point comparisons

Browse source
This commit is contained in:
Andres Nötzli 2016-02-29 19:12:14 -08:00
parent 7ac5e67538
commit c9269c1983
1 changed files with 5 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

12
src/api/python/z3.py
View file

@ -8824,7 +8824,7 @@ def _check_fp_args(a, b):
_z3_assert(is_fp(a) or is_fp(b), "At least one of the arguments must be a Z3 floating-point expression") _z3_assert(is_fp(a) or is_fp(b), "At least one of the arguments must be a Z3 floating-point expression")
def fpLT(a, b, ctx=None): def fpLT(a, b, ctx=None):
"""Create the Z3 floating-point expression `other <= self`. """Create the Z3 floating-point expression `other < self`.
>>> x, y = FPs('x y', FPSort(8, 24)) >>> x, y = FPs('x y', FPSort(8, 24))
>>> fpLT(x, y) >>> fpLT(x, y)
@ -8846,7 +8846,7 @@ def fpLEQ(a, b, ctx=None):
return _mk_fp_bin_pred(Z3_mk_fpa_leq, a, b, ctx) return _mk_fp_bin_pred(Z3_mk_fpa_leq, a, b, ctx)
def fpGT(a, b, ctx=None): def fpGT(a, b, ctx=None):
"""Create the Z3 floating-point expression `other <= self`. """Create the Z3 floating-point expression `other > self`.
>>> x, y = FPs('x y', FPSort(8, 24)) >>> x, y = FPs('x y', FPSort(8, 24))
>>> fpGT(x, y) >>> fpGT(x, y)
@ -8857,11 +8857,9 @@ def fpGT(a, b, ctx=None):
return _mk_fp_bin_pred(Z3_mk_fpa_gt, a, b, ctx) return _mk_fp_bin_pred(Z3_mk_fpa_gt, a, b, ctx)
def fpGEQ(a, b, ctx=None): def fpGEQ(a, b, ctx=None):
"""Create the Z3 floating-point expression `other <= self`. """Create the Z3 floating-point expression `other >= self`.
>>> x, y = FPs('x y', FPSort(8, 24)) >>> x, y = FPs('x y', FPSort(8, 24))
>>> x + y
x + y
>>> fpGEQ(x, y) >>> fpGEQ(x, y)
x >= y x >= y
>>> (x >= y).sexpr() >>> (x >= y).sexpr()
@ -8870,7 +8868,7 @@ def fpGEQ(a, b, ctx=None):
return _mk_fp_bin_pred(Z3_mk_fpa_geq, a, b, ctx) return _mk_fp_bin_pred(Z3_mk_fpa_geq, a, b, ctx)
def fpEQ(a, b, ctx=None): def fpEQ(a, b, ctx=None):
"""Create the Z3 floating-point expression `other <= self`. """Create the Z3 floating-point expression `fpEQ(other, self)`.
>>> x, y = FPs('x y', FPSort(8, 24)) >>> x, y = FPs('x y', FPSort(8, 24))
>>> fpEQ(x, y) >>> fpEQ(x, y)
@ -8881,7 +8879,7 @@ def fpEQ(a, b, ctx=None):
return _mk_fp_bin_pred(Z3_mk_fpa_eq, a, b, ctx) return _mk_fp_bin_pred(Z3_mk_fpa_eq, a, b, ctx)
def fpNEQ(a, b, ctx=None): def fpNEQ(a, b, ctx=None):
"""Create the Z3 floating-point expression `other <= self`. """Create the Z3 floating-point expression `Not(fpEQ(other, self))`.
>>> x, y = FPs('x y', FPSort(8, 24)) >>> x, y = FPs('x y', FPSort(8, 24))
>>> fpNEQ(x, y) >>> fpNEQ(x, y)