FPA Python API cleanup.

src/api/python/z3.py

@@ -8077,19 +8077,19 @@ class FPRef(ExprRef):
         return Z3_ast_to_string(self.ctx_ref(), self.as_ast())
 
     def __le__(self, other):
-        return fpLEQ(self, other)
+        return fpLEQ(self, other, self.ctx)
 
     def __lt__(self, other):
-        return fpLT(self, other)
+        return fpLT(self, other, self.ctx)
 
     def __ge__(self, other):
-        return fpGEQ(self, other)
+        return fpGEQ(self, other, self.ctx)
 
     def __gt__(self, other):
-        return fpGT(self, other)
+        return fpGT(self, other, self.ctx)
 
     def __ne__(self, other):
-        return fpNEQ(self, other)
+        return fpNEQ(self, other, self.ctx)
 
 
     def __add__(self, other):
@@ -8359,13 +8359,6 @@ class FPNumRef(FPRef):
         s = Z3_fpa_get_numeral_string(self.ctx.ref(), self.as_ast())
         return ("FPVal(%s, %s)" % (s, FPSortRef(self.sort()).as_string()))
 
-
-def _to_fpnum(num, ctx=None):
-    if isinstance(num, FPNum):
-        return num
-    else:
-        return FPNum(num, ctx)
-
 def is_fp(a):
     """Return `True` if `a` is a Z3 floating-point expression.
 
@@ -8887,35 +8880,45 @@ def fpNEQ(a, b, ctx=None):
     """
     return Not(fpEQ(a, b, ctx))
 
-def fpFP(sgn, exp, sig):
+def fpFP(sgn, exp, sig, ctx=None):
     """Create the Z3 floating-point value `fpFP(sgn, sig, exp)` from the three bit-vectors sgn, sig, and exp.
 
-    >>> s = FPSort(11, 53)
+    >>> s = FPSort(8, 24)
-    >>> x = fpFP(BitVecVal(1, 1), BitVecVal(0, 11), BitVecVal(0, 52))
+    >>> x = fpFP(BitVecVal(1, 1), BitVecVal(2**7-1, 8), BitVecVal(2**22, 23))
     >>> print(x)
-    fpFP(1, 0, 0)
+    fpFP(1, 127, 4194304)
+    >>> xv = FPVal(-1.5, s)
+    >>> print(xv)
+    -1.5
     >>> slvr = Solver()
-    >>> slvr.add(fpEQ(x, fpMinusZero(s)))
+    >>> slvr.add(fpEQ(x, xv))
     >>> slvr.check()
     sat
-    >>> slvr.model()
+    >>> xv = FPVal(+1.5, s)
-    [x = 1]
+    >>> print(xv)
+    1.5
+    >>> slvr = Solver()
+    >>> slvr.add(fpEQ(x, xv))
+    >>> slvr.check()
+    unsat
     """
     _z3_assert(is_bv(sgn) and is_bv(exp) and is_bv(sig), "sort mismatch")
     _z3_assert(sgn.sort().size() == 1, "sort mismatch")
-    _z3_assert(sgn.ctx == exp.ctx == sig.ctx, "sort mismatch")
+    ctx = _get_ctx(ctx)
-    return FPRef(Z3_mk_fpa_fp(sgn.ctx.ref(), sgn.ast, exp.ast, sig.ast), sgn.ctx)
+    _z3_assert(ctx == sgn.ctx == exp.ctx == sig.ctx, "context mismatch")
+    return FPRef(Z3_mk_fpa_fp(ctx.ref(), sgn.ast, exp.ast, sig.ast), ctx)
 
-def fpToFP(a1, a2=None, a3=None):
+def fpToFP(a1, a2=None, a3=None, ctx=None):
     """Create a Z3 floating-point conversion expression from other terms."""
+    ctx = _get_ctx(ctx)
     if is_bv(a1) and is_fp_sort(a2):
-        return FPRef(Z3_mk_fpa_to_fp_bv(a1.ctx_ref(), a1.ast, a2.ast), a1.ctx)
+        return FPRef(Z3_mk_fpa_to_fp_bv(ctx.ref(), a1.ast, a2.ast), ctx)
     elif is_fprm(a1) and is_fp(a2) and is_fp_sort(a3):
-        return FPRef(Z3_mk_fpa_to_fp_float(a1.ctx_ref(), a1.ast, a2.ast, a3.ast), a1.ctx)
+        return FPRef(Z3_mk_fpa_to_fp_float(ctx.ref(), a1.ast, a2.ast, a3.ast), ctx)
     elif is_fprm(a1) and is_real(a2) and is_fp_sort(a3):
-        return FPRef(Z3_mk_fpa_to_fp_real(a1.ctx_ref(), a1.ast, a2.ast, a3.ast), a1.ctx)
+        return FPRef(Z3_mk_fpa_to_fp_real(ctx.ref(), a1.ast, a2.ast, a3.ast), ctx)
     elif is_fprm(a1) and is_bv(a2) and is_fp_sort(a3):
-        return FPRef(Z3_mk_fpa_to_fp_signed(a1.ctx_ref(), a1.ast, a2.ast, a3.ast), a1.ctx)
+        return FPRef(Z3_mk_fpa_to_fp_signed(ctx.ref(), a1.ast, a2.ast, a3.ast), ctx)
     else:
         raise Z3Exception("Unsupported combination of arguments for conversion to floating-point term.")
 
@@ -8925,7 +8928,8 @@ def fpToFPUnsigned(rm, x, s, ctx=None):
         _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression")
         _z3_assert(is_bv(x), "Second argument must be a Z3 bit-vector expression")
         _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)
+    ctx = _get_ctx(ctx)
+    return FPRef(Z3_mk_fpa_to_fp_unsigned(ctx.ref(), rm.ast, x.ast, s.ast), ctx)
 
 def fpToSBV(rm, x, s, ctx=None):
     """Create a Z3 floating-point conversion expression, from floating-point expression to signed bit-vector.
@@ -8945,9 +8949,10 @@ def fpToSBV(rm, x, s, ctx=None):
         _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression")
         _z3_assert(is_fp(x), "Second argument must be a Z3 floating-point expression")
         _z3_assert(is_bv_sort(s), "Third argument must be Z3 bit-vector sort")
-    return BitVecRef(Z3_mk_fpa_to_sbv(rm.ctx_ref(), rm.ast, x.ast, s.size()), rm.ctx)
+    ctx = _get_ctx(ctx)
+    return BitVecRef(Z3_mk_fpa_to_sbv(ctx.ref(), rm.ast, x.ast, s.size()), ctx)
 
-def fpToUBV(rm, x, s):
+def fpToUBV(rm, x, s, ctx=None):
     """Create a Z3 floating-point conversion expression, from floating-point expression to unsigned bit-vector.
 
     >>> x = FP('x', FPSort(8, 24))
@@ -8965,9 +8970,10 @@ def fpToUBV(rm, x, s):
         _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression")
         _z3_assert(is_fp(x), "Second argument must be a Z3 floating-point expression")
         _z3_assert(is_bv_sort(s), "Third argument must be Z3 bit-vector sort")
-    return BitVecRef(Z3_mk_fpa_to_ubv(rm.ctx_ref(), rm.ast, x.ast, s.size()), rm.ctx)
+    ctx = _get_ctx(ctx)
+    return BitVecRef(Z3_mk_fpa_to_ubv(ctx.ref(), rm.ast, x.ast, s.size()), ctx)
 
-def fpToReal(x):
+def fpToReal(x, ctx=None):
     """Create a Z3 floating-point conversion expression, from floating-point expression to real.
 
     >>> x = FP('x', FPSort(8, 24))
@@ -8983,9 +8989,10 @@ def fpToReal(x):
     """
     if __debug__:
         _z3_assert(is_fp(x), "First argument must be a Z3 floating-point expression")
-    return ArithRef(Z3_mk_fpa_to_real(x.ctx_ref(), x.ast), x.ctx)
+    ctx = _get_ctx(ctx)
+    return ArithRef(Z3_mk_fpa_to_real(ctx.ref(), x.ast), ctx)
 
-def fpToIEEEBV(x):
+def fpToIEEEBV(x, ctx=None):
     """\brief Conversion of a floating-point term into a bit-vector term in IEEE 754-2008 format.
 
     The size of the resulting bit-vector is automatically determined.
@@ -9007,7 +9014,8 @@ def fpToIEEEBV(x):
     """
     if __debug__:
         _z3_assert(is_fp(x), "First argument must be a Z3 floating-point expression")
-    return BitVecRef(Z3_mk_fpa_to_ieee_bv(x.ctx_ref(), x.ast), x.ctx)
+    ctx = _get_ctx(ctx)
+    return BitVecRef(Z3_mk_fpa_to_ieee_bv(ctx.ref(), x.ast), ctx)