mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 18:31:49 +00:00
Code Activity

Merge pull request #486 from 4tXJ7f/patch-1

Browse source 
[Z3py] Add examples for fpToFP
This commit is contained in:
Christoph M. Wintersteiger 2016-03-07 11:31:12 +00:00
parent eccf03aaac d6ece7e8a5
commit 4423447029
1 changed files with 25 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -8944,7 +8944,31 @@ def fpFP(sgn, exp, sig, ctx=None):
return FPRef(Z3_mk_fpa_fp(ctx.ref(), sgn.ast, exp.ast, sig.ast), ctx)
def fpToFP(a1, a2=None, a3=None, ctx=None):
"""Create a Z3 floating-point conversion expression from other terms."""
"""Create a Z3 floating-point conversion expression from other term sorts
to floating-point.
From a bit-vector term in IEEE 754-2008 format:
>>> x = FPVal(1.0, Float32())
>>> x_bv = fpToIEEEBV(x)
>>> simplify(fpToFP(x_bv, Float32()))
1
From a floating-point term with different precision:
>>> x = FPVal(1.0, Float32())
>>> x_db = fpToFP(RNE(), x, Float64())
>>> x_db.sort()
FPSort(11, 53)
From a real term:
>>> x_r = RealVal(1.5)
>>> simplify(fpToFP(RNE(), x_r, Float32()))
1.5
From a signed bit-vector term:
>>> x_signed = BitVecVal(-5, BitVecSort(32))
>>> simplify(fpToFP(RNE(), x_signed, Float32()))
-1.25*(2**2)
"""
ctx = _get_ctx(ctx)
if is_bv(a1) and is_fp_sort(a2):
return FPRef(Z3_mk_fpa_to_fp_bv(ctx.ref(), a1.ast, a2.ast), ctx)