From c6c84dd59a0823921422c1b7b0e4f023eb91a5e3 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 29 Feb 2016 17:04:26 -0800 Subject: [PATCH 1/2] update documentation help to be inline with fpLT. Issue #465 Signed-off-by: Nikolaj Bjorner --- 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 9f3b0a1b9..3a8800f1d 100644 --- a/src/api/python/z3.py +++ b/src/api/python/z3.py @@ -8829,8 +8829,8 @@ def fpLT(a, b, ctx=None): >>> x, y = FPs('x y', FPSort(8, 24)) >>> fpLT(x, y) x < y - >>> (x <= y).sexpr() - '(fp.leq x y)' + >>> (x < y).sexpr() + '(fp.lt x y)' """ return _mk_fp_bin_pred(Z3_mk_fpa_lt, a, b, ctx) From c9269c198382375fe923a3a52ca405578d403d91 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Andres=20N=C3=B6tzli?= Date: Mon, 29 Feb 2016 19:12:14 -0800 Subject: [PATCH 2/2] Fix documentation for floating-point comparisons --- src/api/python/z3.py | 12 +++++------- 1 file changed, 5 insertions(+), 7 deletions(-) diff --git a/src/api/python/z3.py b/src/api/python/z3.py index 3a8800f1d..305733aa7 100644 --- a/src/api/python/z3.py +++ b/src/api/python/z3.py @@ -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") 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)) >>> 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) 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)) >>> 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) 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 - x + y >>> fpGEQ(x, y) x >= y >>> (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) 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)) >>> 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) 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)) >>> fpNEQ(x, y)