Construct FP from sign/exponent/significand BitVecs.
(sgn: BitVecRef, exp: BitVecRef, sig: BitVecRef, ctx: Context | None = None)
| 3550 | |
| 3551 | |
| 3552 | def fpFP(sgn: BitVecRef, exp: BitVecRef, sig: BitVecRef, ctx: Context | None = None) -> FPRef: |
| 3553 | """Construct FP from sign/exponent/significand BitVecs.""" |
| 3554 | exp_sort = exp._sort |
| 3555 | sig_sort = sig._sort |
| 3556 | ebits = exp_sort._width if isinstance(exp_sort, BitVecSortRef) else 11 |
| 3557 | sbits = (sig_sort._width if isinstance(sig_sort, BitVecSortRef) else 52) + 1 |
| 3558 | sort = FPSort(ebits, sbits) |
| 3559 | merged: frozenset[tuple[str, ASTSort]] = frozenset().union(sgn._vars, exp._vars, sig._vars) |
| 3560 | return FPRef(AppNode(_AstVar("fpFP"), (sgn._ast, exp._ast, sig._ast)), sort, merged) |
| 3561 | |
| 3562 | |
| 3563 | def fpToFPUnsigned(rm: FPRMRef, a: ExprRef, sort: FPSortRef, ctx: Context | None = None) -> FPRef: |