Merged Python API changes.

src/api/python/z3.py

@@ -999,6 +999,8 @@ def is_expr(a):
     >>> x = Int('x')
     >>> is_expr(ForAll(x, x >= 0))
     True
+    >>> is_expr(FPVal(1.0))
+    True
     """
     return isinstance(a, ExprRef)
 
@@ -7912,6 +7914,30 @@ def _dflt_rm(ctx=None):
 def _dflt_fps(ctx=None):
     return get_default_fp_sort(ctx)
 
+def _coerce_fp_expr_list(alist, ctx):
+    first_fp_sort = None
+    for a in alist:
+        if is_fp(a):
+            if first_fp_sort == None:
+                first_fp_sort = a.sort()
+            elif first_fp_sort == a.sort():
+                pass # OK, same as before
+            else:
+                # we saw at least 2 different float sorts; something will
+                # throw a sort mismatch later, for now assume None.
+                first_fp_sort = None
+                break
+            
+    r = []
+    for i in range(len(alist)):
+        a = alist[i]
+        if (isinstance(a, str) and a.contains('2**(') and a.endswith(')')) or _is_int(a) or isinstance(a, float) or isinstance(a, bool):
+            r.append(FPVal(a, None, first_fp_sort, ctx))
+        else:
+            r.append(a)
+    return _coerce_expr_list(r, ctx)
+
+
 ### FP Sorts
     
 class FPSortRef(SortRef):
@@ -8076,8 +8102,8 @@ class FPRef(ExprRef):
         >>> (x + y).sort()
         FPSort(8, 24)
         """
-        a, b = z3._coerce_exprs(self, other)
+        [a, b] = _coerce_fp_expr_list([self, other], self.ctx)
-        return fpAdd(_dflt_rm(), self, other)
+        return fpAdd(_dflt_rm(), a, b, self.ctx)
 
     def __radd__(self, other):
         """Create the Z3 expression `other + self`.
@@ -8086,8 +8112,8 @@ class FPRef(ExprRef):
         >>> 10 + x
         1.25*(2**3) + x
         """
-        a, b = _coerce_exprs(self, other)
+        [a, b] = _coerce_fp_expr_list([other, self], self.ctx)
-        return fpAdd(_dflt_rm(), other, self)
+        return fpAdd(_dflt_rm(), a, b, self.ctx)
 
     def __sub__(self, other):
         """Create the Z3 expression `self - other`.
@@ -8099,8 +8125,8 @@ class FPRef(ExprRef):
         >>> (x - y).sort()
         FPSort(8, 24)
         """
-        a, b = z3._coerce_exprs(self, other)
+        [a, b] = _coerce_fp_expr_list([self, other], self.ctx)
-        return fpSub(_dflt_rm(), self, other)
+        return fpSub(_dflt_rm(), a, b, self.ctx)
 
     def __rsub__(self, other):
         """Create the Z3 expression `other - self`.
@@ -8109,9 +8135,9 @@ class FPRef(ExprRef):
         >>> 10 - x
         1.25*(2**3) - x
         """
-        a, b = _coerce_exprs(self, other)
+        [a, b] = _coerce_fp_expr_list([other, self], self.ctx)
-        return fpSub(_dflt_rm(), other, self)
+        return fpSub(_dflt_rm(), a, b, self.ctx)
-
+      
     def __mul__(self, other):
         """Create the Z3 expression `self * other`.
         
@@ -8124,8 +8150,8 @@ class FPRef(ExprRef):
         >>> 10 * y
         1.25*(2**3) * y
         """
-        a, b = z3._coerce_exprs(self, other)
+        [a, b] = _coerce_fp_expr_list([self, other], self.ctx)
-        return fpMul(_dflt_rm(), self, other)
+        return fpMul(_dflt_rm(), a, b, self.ctx)
 
     def __rmul__(self, other):
         """Create the Z3 expression `other * self`.
@@ -8137,8 +8163,8 @@ class FPRef(ExprRef):
         >>> x * 10
         x * 1.25*(2**3)
         """
-        a, b = _coerce_exprs(self, other)
+        [a, b] = _coerce_fp_expr_list([other, self], self.ctx)
-        return fpMul(_dflt_rm(), other, self)
+        return fpMul(_dflt_rm(), a, b, self.ctx)
 
     def __pos__(self):
         """Create the Z3 expression `+self`."""
@@ -8147,14 +8173,43 @@ class FPRef(ExprRef):
     def __neg__(self):
         """Create the Z3 expression `-self`."""
         return FPRef(fpNeg(self))
+    
+    def __div__(self, other):
+        """Create the Z3 expression `self / other`.
+        
+        >>> x = FP('x', FPSort(8, 24))
+        >>> y = FP('y', FPSort(8, 24))
+        >>> x / y
+        x / y
+        >>> (x / y).sort()
+        FPSort(8, 24)
+        >>> 10 / y
+        1.25*(2**3) / y
+        """
+        [a, b] = _coerce_fp_expr_list([self, other], self.ctx)
+        return fpDiv(_dflt_rm(), a, b, self.ctx)
 
-    def __truediv__(self, other):
+    def __rdiv__(self, other):
-        """Create the Z3 expression division `self / other`."""
+        """Create the Z3 expression `other / self`.
-        return self.__div__(other)
+        
+        >>> x = FP('x', FPSort(8, 24))
+        >>> y = FP('y', FPSort(8, 24))
+        >>> x / y
+        x / y
+        >>> x / 10
+        x / 1.25*(2**3)
+        """
+        [a, b] = _coerce_fp_expr_list([other, self], self.ctx)
+        return fpDiv(_dflt_rm(), a, b, self.ctx)
 
-    def __rtruediv__(self, other):
+    if not sys.version < '3':
-        """Create the Z3 expression division `other / self`."""
+        def __truediv__(self, other):
-        return self.__rdiv__(other)
+            """Create the Z3 expression division `self / other`."""
+            return self.__div__(other)
+        
+        def __rtruediv__(self, other):
+            """Create the Z3 expression division `other / self`."""
+            return self.__rdiv__(other)        
 
     def __mod__(self, other):
         """Create the Z3 expression mod `self % other`."""
@@ -8384,31 +8439,60 @@ def _to_float_str(val, exp=0):
 
 
 def fpNaN(s):
+    """Create a Z3 floating-point NaN term.
+
+    >>> s = FPSort(8, 24)
+    >>> set_fpa_pretty(True)
+    >>> fpNaN(s)
+    NaN
+    >>> pb = get_fpa_pretty()
+    >>> set_fpa_pretty(False)
+    >>> fpNaN(s)
+    fpNaN(FPSort(8, 24))
+    >>> set_fpa_pretty(pb)
+    """
     _z3_assert(isinstance(s, FPSortRef), "sort mismatch")
     return FPNumRef(Z3_mk_fpa_nan(s.ctx_ref(), s.ast), s.ctx)
 
 def fpPlusInfinity(s):
+    """Create a Z3 floating-point +oo term.
+
+    >>> s = FPSort(8, 24)
+    >>> pb = get_fpa_pretty()
+    >>> set_fpa_pretty(True)
+    >>> fpPlusInfinity(s)
+    +oo
+    >>> set_fpa_pretty(False)
+    >>> fpPlusInfinity(s)
+    fpPlusInfinity(FPSort(8, 24))
+    >>> set_fpa_pretty(pb)
+    """
     _z3_assert(isinstance(s, FPSortRef), "sort mismatch")
     return FPNumRef(Z3_mk_fpa_inf(s.ctx_ref(), s.ast, False), s.ctx)
 
 def fpMinusInfinity(s):
+    """Create a Z3 floating-point -oo term."""
     _z3_assert(isinstance(s, FPSortRef), "sort mismatch")
     return FPNumRef(Z3_mk_fpa_inf(s.ctx_ref(), s.ast, True), s.ctx)
 
 def fpInfinity(s, negative):
+    """Create a Z3 floating-point +oo or -oo term."""
     _z3_assert(isinstance(s, FPSortRef), "sort mismatch")
     _z3_assert(isinstance(negative, bool), "expected Boolean flag")
     return FPNumRef(Z3_mk_fpa_inf(s.ctx_ref(), s.ast, negative), s.ctx)
 
 def fpPlusZero(s):
+    """Create a Z3 floating-point +0.0 term."""
     _z3_assert(isinstance(s, FPSortRef), "sort mismatch")
     return FPNumRef(Z3_mk_fpa_zero(s.ctx_ref(), s.ast, False), s.ctx)
 
 def fpMinusZero(s):
+    """Create a Z3 floating-point -0.0 term."""
     _z3_assert(isinstance(s, FPSortRef), "sort mismatch")
     return FPNumRef(Z3_mk_fpa_zero(s.ctx_ref(), s.ast, True), s.ctx)
 
 def fpZero(s, negative):
+    """Create a Z3 floating-point +0.0 or -0.0 term."""
     _z3_assert(isinstance(s, FPSortRef), "sort mismatch")
     _z3_assert(isinstance(negative, bool), "expected Boolean flag")
     return FPNumRef(Z3_mk_fpa_zero(s.ctx_ref(), s.ast, negative), s.ctx)
@@ -8456,8 +8540,8 @@ def FP(name, fpsort, ctx=None):
     >>> x2 = FP('x', word)
     >>> eq(x, x2)
     True
-    """ 
+    """
-    if isinstance(fpsort, FPSortRef):
+    if isinstance(fpsort, FPSortRef) and ctx is None:
         ctx = fpsort.ctx
     else:
         ctx = _get_ctx(ctx)
@@ -8481,7 +8565,7 @@ def FPs(names, fpsort, ctx=None):
         names = names.split(" ")
     return [FP(name, fpsort, ctx) for name in names]
 
-def fpAbs(a):
+def fpAbs(a, ctx=None):
     """Create a Z3 floating-point absolute value expression.
 
     >>> s = FPSort(8, 24)
@@ -8499,18 +8583,11 @@ def fpAbs(a):
     >>> fpAbs(x).sort()
     FPSort(8, 24)
     """
-    ctx = None
+    ctx = _get_ctx(ctx)
-    if not is_expr(a):
+    [a] = _coerce_fp_expr_list([a], ctx)
-        ctx =_get_ctx(ctx)
+    return FPRef(Z3_mk_fpa_abs(ctx.ref(), a.as_ast()), ctx)
-        s = get_default_fp_sort(ctx)
-        a = FPVal(a, s)
-    else:
-        ctx = a.ctx
-    if __debug__:     
-        _z3_assert(is_fp(a), "First argument must be Z3 floating-point expression")
-    return FPRef(Z3_mk_fpa_abs(a.ctx_ref(), a.as_ast()), a.ctx)
 
-def fpNeg(a):
+def fpNeg(a, ctx=None):
     """Create a Z3 floating-point addition expression.
 
     >>> s = FPSort(8, 24)
@@ -8521,18 +8598,63 @@ def fpNeg(a):
     >>> fpNeg(x).sort()
     FPSort(8, 24)
     """
-    ctx = None
+    ctx = _get_ctx(ctx)
-    if not is_expr(a):
+    [a] = _coerce_fp_expr_list([a], ctx)
-        ctx =_get_ctx(ctx)
+    return FPRef(Z3_mk_fpa_neg(ctx.ref(), a.as_ast()), ctx) 
-        s = get_default_fp_sort(ctx)
-        a = FPVal(a, s)
-    else:
-        ctx = a.ctx
-    if __debug__:        
-        _z3_assert(is_fp(a), "First argument must be Z3 floating-point expression")
-    return FPRef(Z3_mk_fpa_neg(a.ctx_ref(), a.as_ast()), a.ctx)
 
-def fpAdd(rm, a, b):
+def _mk_fp_unary(f, rm, a, ctx):
+    ctx = _get_ctx(ctx)
+    [a] = _coerce_fp_expr_list([a], ctx)
+    if __debug__:
+        _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression")
+        _z3_assert(is_fp(a), "Second argument must be a Z3 floating-point expression")
+    return FPRef(f(ctx.ref(), rm.as_ast(), a.as_ast()), ctx)
+
+def _mk_fp_unary_norm(f, a, ctx):
+    ctx = _get_ctx(ctx)
+    [a] = _coerce_fp_expr_list([a], ctx)
+    if __debug__:
+        _z3_assert(is_fp(a), "First argument must be a Z3 floating-point expression")
+    return FPRef(f(ctx.ref(), a.as_ast()), ctx)
+
+def _mk_fp_unary_pred(f, a, ctx):
+    ctx = _get_ctx(ctx)
+    [a] = _coerce_fp_expr_list([a], ctx)
+    if __debug__:
+        _z3_assert(is_fp(a) or is_fp(b), "Second or third argument must be a Z3 floating-point expression")
+    return BoolRef(f(ctx.ref(), a.as_ast()), ctx)
+
+def _mk_fp_bin(f, rm, a, b, ctx):
+    ctx = _get_ctx(ctx)
+    [a, b] = _coerce_fp_expr_list([a, b], ctx)
+    if __debug__:
+        _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression")
+        _z3_assert(is_fp(a) or is_fp(b), "Second or third argument must be a Z3 floating-point expression")
+    return FPRef(f(ctx.ref(), rm.as_ast(), a.as_ast(), b.as_ast()), ctx)
+
+def _mk_fp_bin_norm(f, a, b, ctx):
+    ctx = _get_ctx(ctx)
+    [a, b] = _coerce_fp_expr_list([a, b], ctx)
+    if __debug__:
+        _z3_assert(is_fp(a) or is_fp(b), "First or second argument must be a Z3 floating-point expression")
+    return FPRef(f(ctx.ref(), a.as_ast(), b.as_ast()), ctx)
+
+def _mk_fp_bin_pred(f, a, b, ctx):
+    ctx = _get_ctx(ctx)
+    [a, b] = _coerce_fp_expr_list([a, b], ctx)
+    if __debug__:
+        _z3_assert(is_fp(a) or is_fp(b), "Second or third argument must be a Z3 floating-point expression")
+    return BoolRef(f(ctx.ref(), a.as_ast(), b.as_ast()), ctx)
+
+def _mk_fp_tern(f, rm, a, b, c, ctx):
+    ctx = _get_ctx(ctx)
+    [a, b, c] = _coerce_fp_expr_list([a, b, c], ctx)
+    if __debug__:
+        _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression")
+        _z3_assert(is_fp(a) or is_fp(b) or is_fp(c), "At least one of the arguments must be a Z3 floating-point expression")
+    return FPRef(f(ctx.ref(), rm.as_ast(), a.as_ast(), b.as_ast(), c.as_ast()), ctx)
+
+def fpAdd(rm, a, b, ctx=None):
     """Create a Z3 floating-point addition expression.
 
     >>> s = FPSort(8, 24)
@@ -8541,16 +8663,14 @@ def fpAdd(rm, a, b):
     >>> y = FP('y', s)
     >>> fpAdd(rm, x, y)
     fpAdd(RNE(), x, y)
+    >>> fpAdd(RTZ(), x, y) # default rounding mode is RTZ
+    x + y
     >>> fpAdd(rm, x, y).sort()
     FPSort(8, 24)
     """
-    if __debug__:
+    return _mk_fp_bin(Z3_mk_fpa_add, rm, a, b, ctx)
-        _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression")
+    
-        _z3_assert(is_fp(a) or is_fp(b), "Second or third argument must be a Z3 floating-point expression")
+def fpSub(rm, a, b, ctx=None):
-    a, b = _coerce_exprs(a, b)
-    return FPRef(Z3_mk_fpa_add(rm.ctx_ref(), rm.as_ast(), a.as_ast(), b.as_ast()), rm.ctx)
-
-def fpSub(rm, a, b):
     """Create a Z3 floating-point subtraction expression.
 
     >>> s = FPSort(8, 24)
@@ -8562,13 +8682,9 @@ def fpSub(rm, a, b):
     >>> fpSub(rm, x, y).sort()
     FPSort(8, 24)
     """
-    if __debug__:
+    return _mk_fp_bin(Z3_mk_fpa_sub, rm, a, b, ctx)
-        _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression")
-        _z3_assert(is_fp(a) or is_fp(b), "Second or third argument must be a Z3 floating-point expression")
-    a, b = _coerce_exprs(a, b)
-    return FPRef(Z3_mk_fpa_sub(rm.ctx_ref(), rm.as_ast(), a.as_ast(), b.as_ast()), rm.ctx)
 
-def fpMul(rm, a, b):
+def fpMul(rm, a, b, ctx=None):
     """Create a Z3 floating-point multiplication expression.
 
     >>> s = FPSort(8, 24)
@@ -8580,13 +8696,9 @@ def fpMul(rm, a, b):
     >>> fpMul(rm, x, y).sort()
     FPSort(8, 24)
     """
-    if __debug__:
+    return _mk_fp_bin(Z3_mk_fpa_mul, rm, a, b, ctx)
-        _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression")
+    
-        _z3_assert(is_fp(a) or is_fp(b), "Second or third argument must be a Z3 floating-point expression")
+def fpDiv(rm, a, b, ctx=None):
-    a, b = _coerce_exprs(a, b)
-    return FPRef(Z3_mk_fpa_mul(rm.ctx_ref(), rm.as_ast(), a.as_ast(), b.as_ast()), rm.ctx)
-
-def fpDiv(rm, a, b):
     """Create a Z3 floating-point divison expression.
 
     >>> s = FPSort(8, 24)
@@ -8598,13 +8710,9 @@ def fpDiv(rm, a, b):
     >>> fpDiv(rm, x, y).sort()
     FPSort(8, 24)
     """
-    if __debug__:
+    return _mk_fp_bin(Z3_mk_fpa_div, rm, a, b, ctx)
-        _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression")
-        _z3_assert(is_fp(a) or is_fp(b), "Second or third argument must be a Z3 floating-point expression")
-    a, b = _coerce_exprs(a, b)
-    return FPRef(Z3_mk_fpa_div(rm.ctx_ref(), rm.as_ast(), a.as_ast(), b.as_ast()), rm.ctx)
 
-def fpRem(a, b):
+def fpRem(a, b, ctx=None):
     """Create a Z3 floating-point remainder expression.
 
     >>> s = FPSort(8, 24)
@@ -8615,12 +8723,9 @@ def fpRem(a, b):
     >>> fpRem(x, y).sort()
     FPSort(8, 24)
     """
-    if __debug__:        
+    return _mk_fp_bin_norm(Z3_mk_fpa_rem, a, b, ctx)
-        _z3_assert(is_fp(a) or is_fp(b), "Second or third argument must be a Z3 floating-point expression")
-    a, b = _coerce_exprs(a, b)
-    return FPRef(Z3_mk_fpa_rem(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
 
-def fpMin(a, b):
+def fpMin(a, b, ctx=None):
     """Create a Z3 floating-point minimium expression.
 
     >>> s = FPSort(8, 24)
@@ -8632,12 +8737,9 @@ def fpMin(a, b):
     >>> fpMin(x, y).sort()
     FPSort(8, 24)
     """
-    if __debug__:        
+    return _mk_fp_bin_norm(Z3_mk_fpa_min, a, b, ctx)
-        _z3_assert(is_fp(a) or is_fp(b), "Second or third argument must be a Z3 floating-point expression")
-    a, b = _coerce_exprs(a, b)
-    return FPRef(Z3_mk_fpa_min(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
 
-def fpMax(a, b):
+def fpMax(a, b, ctx=None):
     """Create a Z3 floating-point maximum expression.
 
     >>> s = FPSort(8, 24)
@@ -8649,104 +8751,75 @@ def fpMax(a, b):
     >>> fpMax(x, y).sort()
     FPSort(8, 24)
     """
-    if __debug__:        
+    return _mk_fp_bin_norm(Z3_mk_fpa_max, a, b, ctx)
-        _z3_assert(is_fp(a) or is_fp(b), "Second or third argument must be a Z3 floating-point expression")
-    a, b = _coerce_exprs(a, b)
-    return FPRef(Z3_mk_fpa_max(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
 
-def fpFMA(rm, a, b, c):
+def fpFMA(rm, a, b, c, ctx=None):
     """Create a Z3 floating-point fused multiply-add expression.
     """
-    if __debug__:
+    return _mk_fp_tern(Z3_mk_fpa_fma, rm, a, b, c, ctx)
-        _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression")
-        _z3_assert(is_fp(a) or is_fp(b) or is_fp(c), "Second, third, or fourth argument must be a Z3 floating-point expression")
-    a, b, c = _coerce_expr_list([a, b, c])
-    return FPRef(Z3_mk_fpa_fma(rm.ctx_ref(), rm.as_ast(), a.as_ast(), b.as_ast(), c.as_ast()), rm.ctx)    
 
-def fpSqrt(rm, a):
+def fpSqrt(rm, a, ctx=None):
     """Create a Z3 floating-point square root expression.
     """
-    ctx = None
+    return _mk_fp_unary(Z3_mk_fpa_sqrt, rm, a, ctx)
-    if not is_expr(a):
-        ctx =_get_ctx(ctx)
-        s = get_default_fp_sort(ctx)
-        a = FPVal(a, s)
-    else:
-        ctx = a.ctx
-    if __debug__:
-        _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression")
-        _z3_assert(is_fp(a), "Second argument must be a Z3 floating-point expressions")
-    return FPRef(Z3_mk_fpa_sqrt(rm.ctx_ref(), rm.as_ast(), a.as_ast()), rm.ctx)    
 
-def fpRoundToIntegral(rm, a):
+def fpRoundToIntegral(rm, a, ctx=None):
     """Create a Z3 floating-point roundToIntegral expression.
     """
-    ctx = None
+    return _mk_fp_unary(Z3_mk_fpa_round_to_integral, rm, a, ctx)
-    if not is_expr(a):
-        ctx =_get_ctx(ctx)
-        s = get_default_fp_sort(ctx)
-        a = FPVal(a, s)
-    else:
-        ctx = a.ctx
-    if __debug__:
-        _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression")
-        _z3_assert(is_fp(a), "Second argument must be a Z3 floating-point expressions")
-    return FPRef(Z3_mk_fpa_round_to_integral(rm.ctx_ref(), rm.as_ast(), a.as_ast()), rm.ctx)    
 
-def fpIsNaN(a):
+def fpIsNaN(a, ctx=None):
     """Create a Z3 floating-point isNaN expression.
-    """
-    if __debug__:        
-        _z3_assert(is_fp(a), "Argument must be Z3 floating-point expressions")
-    return FPRef(Z3_mk_fpa_is_nan(a.ctx_ref(), a.as_ast()), a.ctx) 
 
-def fpIsInfinite(a):
+    >>> s = FPSort(8, 24)
+    >>> x = FP('x', s)
+    >>> y = FP('y', s)
+    >>> fpIsNaN(x)
+    fpIsNaN(x)
+    """
+    return _mk_fp_unary_norm(Z3_mk_fpa_is_nan, a, ctx)
+
+def fpIsInf(a, ctx=None):
     """Create a Z3 floating-point isInfinite expression.
-    """
-    if __debug__:        
-        _z3_assert(is_fp(a), "Argument must be Z3 floating-point expressions")
-    return FPRef(Z3_mk_fpa_is_infinite(a.ctx_ref(), a.as_ast()), a.ctx) 
 
-def fpIsZero(a):
+    >>> s = FPSort(8, 24)
+    >>> x = FP('x', s)
+    >>> fpIsInf(x)
+    fpIsInf(x)
+    """
+    return _mk_fp_unary_norm(Z3_mk_fpa_is_infinite, a, ctx)
+
+def fpIsZero(a, ctx=None):
     """Create a Z3 floating-point isZero expression.
     """
-    if __debug__:        
+    return _mk_fp_unary_norm(Z3_mk_fpa_is_zero, a, ctx)
-        _z3_assert(is_fp(a), "Argument must be Z3 floating-point expressions")
-    return FPRef(Z3_mk_fpa_is_zero(a.ctx_ref(), a.as_ast()), a.ctx) 
 
-def fpIsNormal(a):
+def fpIsNormal(a, ctx=None):
     """Create a Z3 floating-point isNormal expression.
     """
-    if __debug__:        
+    return _mk_fp_unary_norm(Z3_mk_fpa_is_normal, a, ctx)
-        _z3_assert(is_fp(a), "Argument must be Z3 floating-point expressions")
-    return FPRef(Z3_mk_fpa_is_normal(a.ctx_ref(), a.as_ast()), a.ctx) 
 
-def fpIsSubnormal(a):
+def fpIsSubnormal(a, ctx=None):
     """Create a Z3 floating-point isSubnormal expression.
     """
-    if __debug__:        
+    return _mk_fp_unary_norm(Z3_mk_fpa_is_subnormal, a, ctx)
-        _z3_assert(is_fp(a), "Argument must be Z3 floating-point expressions")
-    return FPRef(Z3_mk_fpa_is_subnormal(a.ctx_ref(), a.as_ast()), a.ctx) 
 
-def fpIsNegative(a):
+def fpIsNegative(a, ctx=None):
     """Create a Z3 floating-point isNegative expression.
     """
-    if __debug__:        
+    return _mk_fp_unary_norm(Z3_mk_fpa_is_negative, a, ctx)
-        _z3_assert(is_fp(a), "Argument must be Z3 floating-point expressions")
-    return FPRef(Z3_mk_fpa_is_negative(a.ctx_ref(), a.as_ast()), a.ctx) 
 
-def fpIsPositive(a):
+def fpIsPositive(a, ctx=None):
     """Create a Z3 floating-point isPositive expression.
     """
-    if __debug__:        
+    return _mk_fp_unary_norm(Z3_mk_fpa_is_positive, a, ctx)
-        _z3_assert(is_fp(a), "Argument must be Z3 floating-point expressions")
     return FPRef(Z3_mk_fpa_is_positive(a.ctx_ref(), a.as_ast()), a.ctx) 
 
 def _check_fp_args(a, b):
     if __debug__:
         _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):
+def fpLT(a, b, ctx=None):
     """Create the Z3 floating-point expression `other <= self`.
     
     >>> x, y = FPs('x y', FPSort(8, 24))
@@ -8755,11 +8828,9 @@ def fpLT(a, b):
     >>> (x <= y).sexpr()
     '(fp.leq x y)'
     """
-    _check_fp_args(a, b)
+    return _mk_fp_bin_pred(Z3_mk_fpa_lt, a, b, ctx)
-    a, b = _coerce_exprs(a, b)
-    return BoolRef(Z3_mk_fpa_lt(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
 
-def fpLEQ(a, b):
+def fpLEQ(a, b, ctx=None):
     """Create the Z3 floating-point expression `other <= self`.
     
     >>> x, y = FPs('x y', FPSort(8, 24))
@@ -8768,11 +8839,9 @@ def fpLEQ(a, b):
     >>> (x <= y).sexpr()
     '(fp.leq x y)'
     """
-    _check_fp_args(a, b)
+    return _mk_fp_bin_pred(Z3_mk_fpa_leq, a, b, ctx)
-    a, b = _coerce_exprs(a, b)
-    return BoolRef(Z3_mk_fpa_leq(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
 
-def fpGT(a, b):
+def fpGT(a, b, ctx=None):
     """Create the Z3 floating-point expression `other <= self`.
     
     >>> x, y = FPs('x y', FPSort(8, 24))
@@ -8781,12 +8850,9 @@ def fpGT(a, b):
     >>> (x > y).sexpr()
     '(fp.gt x y)'
     """
-    _check_fp_args(a, b)
+    return _mk_fp_bin_pred(Z3_mk_fpa_gt, a, b, ctx)
-    a, b = _coerce_exprs(a, b)
-    return BoolRef(Z3_mk_fpa_gt(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
 
-
+def fpGEQ(a, b, ctx=None):
-def fpGEQ(a, b):
     """Create the Z3 floating-point expression `other <= self`.
     
     >>> x, y = FPs('x y', FPSort(8, 24))
@@ -8797,11 +8863,9 @@ def fpGEQ(a, b):
     >>> (x >= y).sexpr()
     '(fp.geq x y)'
     """
-    _check_fp_args(a, b)
+    return _mk_fp_bin_pred(Z3_mk_fpa_geq, a, b, ctx)
-    a, b = _coerce_exprs(a, b)
-    return BoolRef(Z3_mk_fpa_geq(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
 
-def fpEQ(a, b):
+def fpEQ(a, b, ctx=None):
     """Create the Z3 floating-point expression `other <= self`.
     
     >>> x, y = FPs('x y', FPSort(8, 24))
@@ -8810,11 +8874,9 @@ def fpEQ(a, b):
     >>> fpEQ(x, y).sexpr()
     '(fp.eq x y)'
     """
-    _check_fp_args(a, b)
+    return _mk_fp_bin_pred(Z3_mk_fpa_eq, a, b, ctx)
-    a, b = _coerce_exprs(a, b)
-    return BoolRef(Z3_mk_fpa_eq(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
 
-def fpNEQ(a, b):
+def fpNEQ(a, b, ctx=None):
     """Create the Z3 floating-point expression `other <= self`.
     
     >>> x, y = FPs('x y', FPSort(8, 24))
@@ -8823,18 +8885,26 @@ def fpNEQ(a, b):
     >>> (x != y).sexpr()
     '(not (fp.eq x y))'
     """
-    _check_fp_args(a, b)
+    return Not(fpEQ(a, b, ctx))
-    a, b = _coerce_exprs(a, b)
-    return Not(BoolRef(Z3_mk_fpa_eq(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx), a.ctx)
-
-
 
 def fpFP(sgn, exp, sig):
-    """Create the Z3 floating-point value `fpFP(sgn, sig, exp)` from the three bit-vectorssgn, sig, and exp."""    
+    """Create the Z3 floating-point value `fpFP(sgn, sig, exp)` from the three bit-vectors sgn, sig, and exp.
+
+    >>> s = FPSort(11, 53)
+    >>> x = fpFP(BitVecVal(1, 1), BitVecVal(0, 11), BitVecVal(0, 52))
+    >>> print(x)
+    fpFP(1, 0, 0)
+    >>> slvr = Solver()
+    >>> slvr.add(fpEQ(x, fpMinusZero(s)))
+    >>> slvr.check()
+    sat
+    >>> slvr.model()
+    [x = 1]
+    """
     _z3_assert(is_bv(sgn) and is_bv(exp) and is_bv(sig), "sort mismatch")
     _z3_assert(sgn.sort().size() == 1, "sort mismatch")
-    return FPRef(Z3_mk_fpa_fp(sgn.ctx_ref(), sgn.ast, exp.ast, sig.ast), sgn.ctx)
+    _z3_assert(sgn.ctx == exp.ctx == sig.ctx, "sort mismatch")
-    
+    return FPRef(Z3_mk_fpa_fp(sgn.ctx.ref(), sgn.ast, exp.ast, sig.ast), sgn.ctx)
 
 def fpToFP(a1, a2=None, a3=None):
     """Create a Z3 floating-point conversion expression from other terms."""
@@ -8849,7 +8919,7 @@ def fpToFP(a1, a2=None, a3=None):
     else:
         raise Z3Exception("Unsupported combination of arguments for conversion to floating-point term.")
 
-def fpToFPUnsigned(rm, x, s):
+def fpToFPUnsigned(rm, x, s, ctx=None):
     """Create a Z3 floating-point conversion expression, from unsigned bit-vector to floating-point expression."""
     if __debug__:
         _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression")
@@ -8857,7 +8927,7 @@ def fpToFPUnsigned(rm, x, s):
         _z3_assert(is_fp_sort(s), "Third argument must be Z3 floating-point sort")
     return FPRef(Z3_mk_fpa_to_fp_unsigned(rm.ctx_ref(), rm.ast, x.ast, s.ast), rm.ctx)
 
-def fpToSBV(rm, x, s):
+def fpToSBV(rm, x, s, ctx=None):
     """Create a Z3 floating-point conversion expression, from floating-point expression to signed bit-vector.
 
     >>> x = FP('x', FPSort(8, 24))

src/api/python/z3printer.py

@@ -68,8 +68,8 @@ _z3_op_to_fpa_normal_str = {
     Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN : 'RoundNearestTiesToEven()', Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY : 'RoundNearestTiesToAway()',
     Z3_OP_FPA_RM_TOWARD_POSITIVE : 'RoundTowardPositive()', Z3_OP_FPA_RM_TOWARD_NEGATIVE : 'RoundTowardNegative()',
     Z3_OP_FPA_RM_TOWARD_ZERO : 'RoundTowardZero()',
-    Z3_OP_FPA_PLUS_INF : '+oo', Z3_OP_FPA_MINUS_INF : '-oo',
+    Z3_OP_FPA_PLUS_INF : 'fpPlusInfinity', Z3_OP_FPA_MINUS_INF : 'fpMinusInfinity',
-    Z3_OP_FPA_NAN : 'NaN', Z3_OP_FPA_PLUS_ZERO : 'PZero', Z3_OP_FPA_MINUS_ZERO : 'NZero',
+    Z3_OP_FPA_NAN : 'fpNaN', Z3_OP_FPA_PLUS_ZERO : 'fpPZero', Z3_OP_FPA_MINUS_ZERO : 'fpNZero',
     Z3_OP_FPA_ADD : 'fpAdd', Z3_OP_FPA_SUB : 'fpSub', Z3_OP_FPA_NEG : 'fpNeg', Z3_OP_FPA_MUL : 'fpMul',
     Z3_OP_FPA_DIV : 'fpDiv', Z3_OP_FPA_REM : 'fpRem', Z3_OP_FPA_ABS : 'fpAbs',
     Z3_OP_FPA_MIN : 'fpMin', Z3_OP_FPA_MAX : 'fpMax',
@@ -588,14 +588,24 @@ class Formatter:
 
     def pp_fp_value(self, a):
         z3._z3_assert(isinstance(a, z3.FPNumRef), 'type mismatch')
-        if not self.fpa_pretty:            
+        if not self.fpa_pretty:
+            r = []
             if (a.isNaN()):
-                return to_format('NaN')
+                r.append(to_format(_z3_op_to_fpa_normal_str[Z3_OP_FPA_NAN]))
+                r.append(to_format('('))
+                r.append(to_format(a.sort()))
+                r.append(to_format(')'))
+                return compose(r)
             elif (a.isInf()):
                 if (a.isNegative()):
-                    return to_format('-oo')
+                    r.append(to_format(_z3_op_to_fpa_normal_str[Z3_OP_FPA_MINUS_INF]))
                 else:
-                    return to_format('+oo')
+                    r.append(to_format(_z3_op_to_fpa_normal_str[Z3_OP_FPA_PLUS_INF]))                
+                r.append(to_format('('))
+                r.append(to_format(a.sort()))
+                r.append(to_format(')'))
+                return compose(r)
+
             elif (a.isZero()):
                 if (a.isNegative()):
                     return to_format('-zero')
@@ -1195,6 +1205,10 @@ def set_fpa_pretty(flag=True):
 
 set_fpa_pretty(True)
 
+def get_fpa_pretty():
+    global Formatter
+    return _Formatter.fpa_pretty
+
 def in_html_mode():
     return isinstance(_Formatter, HTMLFormatter)