Function fpRealToFP

lean_py/z3/core.py:3494–3499

(rm: FPRMRef, a: ArithRef, sort: FPSortRef, ctx: Context | None = None)

def fpRealToFP(rm: FPRMRef, a: ArithRef, sort: FPSortRef, ctx: Context | None = None) -> FPRef:
    return FPRef(
        AppNode(_AstVar("fpRealToFP"), (rm._ast, a._ast)),
        sort,
        _merge(rm._vars, a._vars),
    )


def fpSignedToFP(rm: FPRMRef, a: ExprRef, sort: FPSortRef, ctx: Context | None = None) -> FPRef: