Function fpToReal

lean_py/z3/core.py:3458–3459

(a: FPRef, ctx: Context | None = None)

# FP conversions
def fpToReal(a: FPRef, ctx: Context | None = None) -> ArithRef:
    return ArithRef(AppNode(_AstVar("fpToReal"), (a._ast,)), RealSort(), a._vars)


def fpToSBV(rm: FPRMRef, a: FPRef, sort: BitVecSortRef, ctx: Context | None = None) -> BitVecRef: