export-error-bounds-data option

default.cfg

@@ -135,11 +135,16 @@ tmp-date = false
 # {task} is replaced with task's name.
 export-racket =
 
-## If defined then a C file for the ErrorBounds tool is created.
+## If defined then a C file for the search_mpfr(mpfi) tool (from ErrorBounds) is created.
 # The following templates are supported:
 # {task} is replaced with task's name.
 export-error-bounds =
 
+## If defined then a C file for the data_mpfi tool (from ErrorBounds) is created.
+# The following templates are supported:
+# {task} is replaced with task's name.
+export-error-bounds-data =
+
 #**************************
 # Optimization options
 #**************************

fptaylor.ml

@@ -291,6 +291,17 @@ let absolute_errors task tf =
               [out_expr]
           with Not_found -> () in
 
+        let () = try
+          let out_expr = mk_add (mk_mul (mk_float_const (Rounding.get_eps exp)) full_expr)
+                                (mk_float_const total2_i.high) in
+          let name = task.Task.name in
+            Out_error_bounds.generate_data_functions
+              (get_file_formatter "data") task
+              [name, out_expr;
+               name ^ "-total2", mk_float_const total2_i.high;
+               name ^ "-opt-bound", mk_float_const total_i.high]
+          with Not_found -> () in
+
         Log.report `Important "exact bound (exp = %d): %s" exp (bound_info bound);
         Log.report `Important "total2: %s" (bound_info total2_i);
         Log.report `Important "exact total: %s" (bound_info total_i);
@@ -579,6 +590,13 @@ let process_task (task : task) =
       Log.report `Important "Racket export: %s" fname;
       open_file "racket" fname
     end in
+  let () =
+    let data_export = Config.get_string_option "export-error-bounds-data" in
+    if data_export <> "" then begin
+      let fname = Str.global_replace (Str.regexp "{task}") task.Task.name data_export in
+      Log.report `Important "Data (ErrorBounds) export: %s" fname;
+      open_file "data" fname
+    end in
   let () =
     let error_bounds = Config.get_string_option "export-error-bounds" in
     if error_bounds <> "" then begin
@@ -591,6 +609,7 @@ let process_task (task : task) =
     end in
   let result = compute_form { task with constraints = approx_constraints } in
   close_file "racket";
+  close_file "data";
   result
 
 let process_input fname =

out_error_bounds.ml

@@ -47,7 +47,7 @@ let get_expr_name env ?(suffix = "") expr =
   with Not_found ->
     let name, flag =
       match expr with
-      | Const c ->
+      | Const c when Const.is_rat c ->
         let index =
           let n = Const.to_num c in
           try Lib.assoc_eq Num.eq_num n env.constants
@@ -112,6 +112,10 @@ let translate_mpfi env =
     else
       let () =
         match expr with
+        | Const c ->
+          let x = Const.to_interval c in
+          fprintf fmt "  mpfi_interv_d(%s, %.20e, %.20e);@." 
+            name x.Interval.low x.Interval.high
         | U_op (op, arg) -> begin
             let arg_name = translate fmt arg in
             match op with
@@ -278,14 +282,14 @@ let print_init_functions env
 let print_mp_f env fmt ?(mpfi = false) ?(index = 1) expr =
   clear_exprs env;
   env.subexprs_names <- [expr, "r_op"];
-  let mp_type = if mpfi then "mpfi_t" else "mpfr_t" in
-  let args = List.map (fun (_, name) -> mp_type ^ " " ^ name) env.vars in
+  let mp_prefix = if mpfi then "mpfi" else "mpfr" in
+  let args = List.map (fun (_, name) -> mp_prefix ^ "_srcptr " ^ name) env.vars in
   let body, result_name =
     Lib.write_to_string_result 
       (if mpfi then (translate_mpfi env) else (translate_mpfr env))
       expr in
   let f_name = "f_high" ^ (if index <= 1 then "" else string_of_int index) in
-  fprintf fmt "void %s(%s r_op, %a)@.{@." f_name mp_type (print_list ", ") args;
+  fprintf fmt "void %s(%s r_op, %a)@.{@." f_name (mp_prefix ^ "_ptr") (print_list ", ") args;
   fprintf fmt "%s" body;
   if result_name <> "r_op" then begin
     if mpfi then 
@@ -354,7 +358,7 @@ let generate_error_bounds fmt task =
   pp_print_newline fmt ();
   print_single_f env fmt expr
 
-let generate_data_function fmt task named_exprs =
+let generate_data_functions fmt task named_exprs =
   let task_vars, var_bounds =
     let vars = all_active_variables task in
     let bounds = List.map (variable_interval task) vars in
@@ -382,5 +386,5 @@ let generate_data_function fmt task named_exprs =
   fprintf fmt "char *f_names[] = {%a};@." (print_list ", ") expr_names;
   let n = List.length exprs in
   let f_names = 
-    Lib.init_list n (fun i -> "f_high" ^ (if i > 1 then string_of_int i else "")) in
+    Lib.init_list n (fun i -> "f_high" ^ (if i = 0 then "" else string_of_int (i + 1))) in
   fprintf fmt "F_HIGH funcs[] = {%a};@." (print_list ", ") f_names

out_error_bounds.mli

@@ -12,4 +12,4 @@
 
 val generate_error_bounds : Format.formatter -> Task.task -> unit
 
-val generate_data_function : Format.formatter -> Task.task -> (string * Expr.expr) list -> unit
+val generate_data_functions : Format.formatter -> Task.task -> (string * Expr.expr) list -> unit