Repository navigation

[WIP] Float encoding equivalence - #8990

Draft

tautschnig wants to merge 30 commits into

diffblue:developfrom

tautschnig:float-encoding-equivalence

Draft

[WIP] Float encoding equivalence#8990
tautschnig wants to merge 30 commits into
diffblue:developfrom
tautschnig:float-encoding-equivalence

Commits on Apr 27, 2026
- Add plan for float_utilst vs float_bvt equivalence checking
  
  tautschnig
  and
  kiro-agent
  committed
  bd69c33
- Remove dead #if 0 block in boolbv_mod.cpp
  
  tautschnig
  and
  kiro-agent
  committed
  159607c
- Introduce ID_floatbv_mod to distinguish fmod from IEEE remainder
  
  tautschnig
  and
  kiro-agent
  committed
  bce38a7
- Use __CPROVER_fmod and __CPROVER_remainder built-ins in C library
  
  tautschnig
  and
  kiro-agent
  committed
  47e4af8
- Fix float_utilst::rem crash and distinguish fmod from remainder
  
  tautschnig
  and
  kiro-agent
  committed
  7364a99
- Add fmod and remainder support to SMT2 and float_bvt back-ends
  
  tautschnig
  and
  kiro-agent
  committed
  5e51e61
- Update fmod/fmodf/fmodl regression tests
  
  tautschnig
  and
  kiro-agent
  committed
  b268567
- Update remainder/remainderf/remainderl regression tests
  
  tautschnig
  and
  kiro-agent
  committed
  4356883
- Add remainderf edge case test
  
  tautschnig
  and
  kiro-agent
  committed
  be27ba3
- Add remainderf tie-break test
  
  tautschnig
  and
  kiro-agent
  committed
  b5ae236
- Add Java fmod regression test (farith2)
  
  tautschnig
  and
  kiro-agent
  committed
  832e8fd
- Add fp.rem regression tests (Z3#2381, Z3#8414)
  
  tautschnig
  and
  kiro-agent
  committed
  027c513
- Use FMA for IEEE remainder correction in float_utilst
  
  tautschnig
  and
  kiro-agent
  committed
  48a7c98
- Add _Float16 variants of fmod/remainder/fma built-ins
  
  tautschnig
  and
  kiro-agent
  committed
  3c6f25d
- Add Coq proof and documentation for FMA-based remainder
  
  tautschnig
  and
  kiro-agent
  committed
  98bc4dc
- Add HOL Light proofs for FMA-based remainder algorithm
  
  tautschnig
  and
  kiro-agent
  committed
  d65b63f
- Add proof verification CI and _Float16 property tests
  
  tautschnig
  and
  kiro-agent
  committed
  e5bb869
- Use conditional subtract for IEEE remainder correction
  
  tautschnig
  and
  kiro-agent
  committed
  1663dad
- Fix float_utilst::rem infinity bug in correction step
  
  tautschnig
  and
  kiro-agent
  committed
  4fd0129
- Fix ROUND_TO_AWAY rounding decision in float_bvt
  
  tautschnig
  and
  kiro-agent
  committed
  abad050
- Fix division exponent overflow and overflow-to-inf ROUND_TO_AWAY
  
  tautschnig
  and
  kiro-agent
  committed
  5d86072
- Fix FMA sign handling in float_bvt for infinity and zero results
  
  tautschnig
  and
  kiro-agent
  committed
  ca51a97
- Fix float-to-integer conversion for wide destination types
  
  tautschnig
  and
  kiro-agent
  committed
  ed8e244
Commits on Apr 28, 2026
- Fix subnormal division precision loss in float_utilst and float_bvt
  
  tautschnig
  and
  kiro-agent
  committed
  690dbdd
- Add is_finite, is_plus_inf, is_minus_inf to float encodings
  
  tautschnig
  and
  kiro-agent
  committed
  04db3a4
- Add round_to_integral to float_bvt, rewrite in float_utilst
  
  tautschnig
  and
  kiro-agent
  committed
  924b99d
- Rewrite float_bvt::mod/rem with exact integer significand arithmetic
  
  tautschnig
  and
  kiro-agent
  committed
  93fcab5
- Fix x86 extended precision support across all layers
  
  tautschnig
  and
  kiro-agent
  committed
  b3044d7
- Remove unused is_plus_inf and is_minus_inf
  
  tautschnig
  and
  kiro-agent
  committed
  282178f
- Add equivalence tests and extended random tests
  
  tautschnig
  and
  kiro-agent
  committed
  d016029

Commits

Commits on Apr 27, 2026

Commits on Apr 28, 2026