Commit 880a3855 authored by Guillaume Melquiond's avatar Guillaume Melquiond
Browse files

Add symbols from real.FromInt to Gappa output.

This makes bench/valid/intreal.why pass with Gappa.
parent 7d4ea8e1
......@@ -133,6 +133,12 @@ theory real.Truncate
end
theory real.FromInt
syntax logic from_int "%1"
end
theory floating_point.Single
prelude "@rnd_ieee32_ne=float<ieee_32,ne>;"
......
......@@ -88,6 +88,7 @@ let get_info =
let real_truncate = find_real_truncate "truncate" in
let real_floor = find_real_truncate "floor" in
let real_ceil = find_real_truncate "ceil" in
let real_from_int = find_th env "real" "FromInt" "from_int" in
let find_rounding_theory = find_th env "floating_point" "Rounding" in
let round_ne = find_rounding_theory "NearestTiesToEven" in
let round_zr = find_rounding_theory "ToZero" in
......@@ -112,6 +113,7 @@ let get_info =
real_le; real_ge; real_lt; real_gt;
real_abs; real_sqrt ;
real_truncate; real_floor; real_ceil;
real_from_int;
!round_single; !round_double;
] Sls.empty
in
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment