smt-libv2-floats-int_via_real.gen 357 Bytes
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13
(* This is a encoding for int/float conversions via reals. *)

theory ieee_float.GenericFloat
  syntax function to_int "(to_int (fp.to_real (fp.roundToIntegral %1 %2)))"
end

theory ieee_float.Float32
  syntax function of_int "((_ to_fp 8 24) %1 (to_real %2))"
end

theory ieee_float.Float64
  syntax function of_int "((_ to_fp 11 53) %1 (to_real %2))"
end