Function fpToSBV

lean_py/z3/core.py:3462–3465

(rm: FPRMRef, a: FPRef, sort: BitVecSortRef, ctx: Context | None = None)

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


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