| 3472 | |
| 3473 | |
| 3474 | def fpToFP(rm: Any, a: Any, sort: FPSortRef | None = None, ctx: Context | None = None) -> FPRef: |
| 3475 | if sort is None: |
| 3476 | sort = Float64() |
| 3477 | merged: frozenset[tuple[str, ASTSort]] = frozenset() |
| 3478 | args_ast: list[ASTNode] = [] |
| 3479 | for x in (rm, a): |
| 3480 | if isinstance(x, ExprRef): |
| 3481 | merged = merged | x._vars |
| 3482 | args_ast.append(x._ast) |
| 3483 | return FPRef(AppNode(_AstVar("fpToFP"), tuple(args_ast)), sort, merged) |
| 3484 | |
| 3485 | |
| 3486 | def fpBVToFP(a: BitVecRef, sort: FPSortRef, ctx: Context | None = None) -> FPRef: |