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

Merge branch 'master' of https://github.com/Z3Prover/z3

Browse source
This commit is contained in:
Nikolaj Bjorner 2016-03-01 22:31:53 -08:00
parent a25336a899 1e86175c03
commit 1a081936ac
1 changed files with 37 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -48,6 +48,7 @@ from z3printer import *
from fractions import Fraction
import sys
import io
import math
if sys.version < '3':
def _is_int(v):
@ -8409,11 +8410,24 @@ def FPSort(ebits, sbits, ctx=None):
def _to_float_str(val, exp=0):
if isinstance(val, float):
v = val.as_integer_ratio()
num = v[0]
den = v[1]
rvs = str(num) + '/' + str(den)
res = rvs + 'p' + _to_int_str(exp)
if math.isnan(val):
res = "NaN"
elif val == 0.0:
sone = math.copysign(1.0, val)
if sone < 0.0:
return "-0.0"
else:
return "+0.0"
elif val == float("+inf"):
res = "+oo"
elif val == float("-inf"):
res = "-oo"
else:
v = val.as_integer_ratio()
num = v[0]
den = v[1]
rvs = str(num) + '/' + str(den)
res = rvs + 'p' + _to_int_str(exp)
elif isinstance(val, bool):
if val:
res = "1.0"
@ -8511,6 +8525,12 @@ def FPVal(sig, exp=None, fps=None, ctx=None):
>>> v = FPVal(-2.25, FPSort(8, 24))
>>> v
-1.125*(2**1)
>>> v = FPVal(-0.0, FPSort(8, 24))
-0.0
>>> v = FPVal(0.0, FPSort(8, 24))
+0.0
>>> v = FPVal(+0.0, FPSort(8, 24))
+0.0
"""
ctx = _get_ctx(ctx)
if is_fp_sort(exp):
@ -8522,7 +8542,18 @@ def FPVal(sig, exp=None, fps=None, ctx=None):
if exp == None:
exp = 0
val = _to_float_str(sig)
return FPNumRef(Z3_mk_numeral(ctx.ref(), val, fps.ast), ctx)
if val == "NaN" or val == "nan":
return fpNaN(fps)
elif val == "-0.0":
return fpMinusZero(fps)
elif val == "0.0" or val == "+0.0":
return fpPlusZero(fps)
elif val == "+oo" or val == "+inf" or val == "+Inf":
return fpPlusInfinity(fps)
elif val == "-oo" or val == "-inf" or val == "-Inf":
return fpMinusInfinity(fps)
else:
return FPNumRef(Z3_mk_numeral(ctx.ref(), val, fps.ast), ctx)
def FP(name, fpsort, ctx=None):
"""Return a floating-point constant named `name`.