Commit 7b90b156 authored by Nikita Zyuzin's avatar Nikita Zyuzin

Use Daisy_compute and fail FMA for eval_exp_float

parent 72e60f72
......@@ -1980,6 +1980,7 @@ Proof.
intros mIsJoin e1_real e2_real e3_real eval_real e1_float e2_float e3_float eval_float
subexpr_ok valid_error valid_e1 valid_e2 valid_e3 absenv_e1 absenv_e2 absenv_e3 absenv_fma
err1_bounded err2_bounded err3_bounded.
Daisy_compute; try congruence; type_conv; subst.
eapply Rle_trans.
eapply (fma_abs_err_bounded e1 e2 e3); eauto.
unfold validErrorbound in valid_error.
......
......@@ -47,7 +47,7 @@ Fixpoint eval_exp_float (e:exp (binary_float 53 1024)) (E:nat -> option fl64):=
end
| Fma e1 e2 e3 =>
match eval_exp_float e1 E, eval_exp_float e2 E, eval_exp_float e3 E with
| Some f1, Some f2, Some f3 => Some (b64_plus dmode f1 (b64_mult dmode f2 f3))
(* | Some f1, Some f2, Some f3 => Some (b64_plus dmode f1 (b64_mult dmode f2 f3)) *)
| _, _, _ => None
end
| _ => None
......
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