MCPcopy Create free account
hub / github.com/BasisResearch/lean.py / RNE

Function RNE

lean_py/z3/core.py:3305–3306  ·  view source on GitHub ↗
(ctx: Context | None = None)

Source from the content-addressed store, hash-verified

3303
3304
3305def RNE(ctx: Context | None = None) -> FPRMRef:
3306 return RoundNearestTiesToEven(ctx)
3307
3308
3309def RoundNearestTiesToAway(ctx: Context | None = None) -> FPRMRef:

Callers 15

test_rounding_modesMethod · 0.90
test_fp_addMethod · 0.90
test_fp_subMethod · 0.90
test_fp_mulMethod · 0.90
test_fp_divMethod · 0.90
test_fp_sqrtMethod · 0.90
test_fp_fmaMethod · 0.90
test_fp_to_sbvMethod · 0.90
test_fp_to_ubvMethod · 0.90
test_fp_to_fpMethod · 0.90
test_fp_fp_to_fpMethod · 0.90
test_fp_real_to_fpMethod · 0.90

Calls 1

RoundNearestTiesToEvenFunction · 0.85

Tested by 15

test_rounding_modesMethod · 0.72
test_fp_addMethod · 0.72
test_fp_subMethod · 0.72
test_fp_mulMethod · 0.72
test_fp_divMethod · 0.72
test_fp_sqrtMethod · 0.72
test_fp_fmaMethod · 0.72
test_fp_to_sbvMethod · 0.72
test_fp_to_ubvMethod · 0.72
test_fp_to_fpMethod · 0.72
test_fp_fp_to_fpMethod · 0.72
test_fp_real_to_fpMethod · 0.72