Function fpBVToFP

lean_py/z3/core.py:3486–3487 · view source on GitHub ↗

(a: BitVecRef, sort: FPSortRef, ctx: Context | None = None)

Source from the content-addressed store, hash-verified

3484
3485
3486	def fpBVToFP(a: BitVecRef, sort: FPSortRef, ctx: Context \| None = None) -> FPRef:
3487	return FPRef(AppNode(_AstVar("fpBVToFP"), (a._ast,)), sort, a._vars)
3488
3489
3490	def fpFPToFP(rm: FPRMRef, a: FPRef, sort: FPSortRef, ctx: Context \| None = None) -> FPRef:

test_fpbv_to_fpMethod · 0.90

AppNodeClass · 0.90

FPRefClass · 0.85

test_fpbv_to_fpMethod · 0.72