mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
Merge branch 'master' of https://github.com/Z3Prover/z3
This commit is contained in:
commit
3b6eef05c9
|
@ -8824,13 +8824,13 @@ 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)
|
||||
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)
|
||||
|
||||
|
@ -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)
|
||||
|
|
Loading…
Reference in a new issue