flyspeck_needs "../formal_lp/formal_interval/m_verifier.hl";;


let reset_all () =
  Arith_cache.reset_stat();
  Arith_cache.reset_cache();
  Arith_float.reset_stat();
  Arith_float.reset_cache();;


(**************************)
(* Examples *)
let schwefel_poly = expr_to_vector_fun `(x1 - x2 pow 2) pow 2 + (x2 - &1) pow 2 + 
  (x1 - x3 pow 2) pow 2 + (x3 - &1) pow 2`;;
let rd_poly = expr_to_vector_fun `-- x1 + &2 * x2 - x3 - #0.835634534 * x2 * (&1 + x2)`;;
let caprasse_poly = expr_to_vector_fun `-- x1 * x3 pow 3 + &4 * x2 * x3 pow 2 * x4 + 
  &4 * x1 * x3 * x4 pow 2 + &2 * x2 * x4 pow 3 + &4 * x1 * x3 + &4 * x3 pow 2 - 
  &10 * x2 * x4 - &10 * x4 pow 2 + &2`;;
let lv_poly = expr_to_vector_fun `x1 * x2 pow 2 + x1 * x3 pow 2 + x1 * x4 pow 2 - #1.1 * x1 + &1`;;
let butcher_poly = expr_to_vector_fun `x6 * x2 pow 2 + x5 * x3 pow 2 - x1 * x4 pow 2 + x4 pow 2 -
  &1 / &3 * x1 + &4 / &3 * x4`;;
let magnetism_poly = expr_to_vector_fun `x1 pow 2 + &2 * x2 pow 2 + &2 * x3 pow 2 + &2 * x4 pow 2 +
  &2 * x5 pow 2 + &2 * x6 pow 2 + &2 * x7 pow 2 - x1`;;
let heart_poly = expr_to_vector_fun `-- x1 * x6 pow 3 + &3 * x1 * x6 * x7 pow 2 - x3 * x7 pow 3 +
  &3 * x3 * x7 * x6 pow 2 - x2 * x5 pow 3 + &3 * x2 * x5 * x8 pow 2 - x4 * x8 pow 3 + 
  &3 * x4 * x8 * x5 pow 2 - #0.9563453`;;


let schwefel_min = `-- #0.00000000058806` and
    rd_min = `-- #36.7126907` and
    caprasse_min = `-- #3.1801` and
    lv_min = `-- #20.801` and
    butcher_min = `-- #1.44` and
    magnetism_min = `-- #0.25001` and
    heart_min = `-- #1.7435`;;

let schwefel_dom = `[-- &10; -- &10; -- &10]`, `[&10; &10; &10]`;;
let rd_dom = `[-- &5; -- &5; -- &5]`, `[&5; &5; &5]`;;
let caprasse_dom = `[-- #0.5; -- #0.5; -- #0.5; -- #0.5]`, `[#0.5; #0.5; #0.5; #0.5]`;;
let lv_dom = `[-- &2; -- &2; -- &2; -- &2]`, `[&2; &2; &2; &2]`;;
let butcher_dom = `[-- &1; -- #0.1; -- #0.1; -- &1; -- #0.1; -- #0.1]`,
  `[&0; #0.9; #0.5; -- #0.1; -- #0.05; -- #0.03]`;;
let magnetism_dom = `[-- &1; -- &1; -- &1; -- &1; -- &1; -- &1; -- &1]`,
  `[&1; &1; &1; &1; &1; &1; &1]`;;
let heart_dom = `[-- #0.1; #0.4; -- #0.7; -- #0.7; #0.1; -- #0.1; -- #0.3; -- #1.1]`,
  `[#0.4; &1; -- #0.4; #0.4; #0.2; #0.2; #1.1; -- #0.3]`;;



(****************)
let delta_x_poly = 
  let tm = (rand o concl o SPEC_ALL) Sphere.delta_x in
    expr_to_vector_fun tm;;

let delta_y_poly =
  let tm = (rand o concl o SPEC_ALL o REWRITE_RULE[Sphere.delta_x]) Sphere.delta_y in
    expr_to_vector_fun tm;;

let delta_x4_poly =
  let tm = (rand o concl o SPEC_ALL) Sphere.delta_x4 in
    expr_to_vector_fun tm;;


let delta_x4_dom = `[&4;&4;&4;&4;&4;&8]`, `[#6.3504;#6.3504;#6.3504;#6.3504;#6.3504;#25.4016]`;;
let delta_x_dom = `[&4;&4;&4;&4;&4;&4]`, `[#6.3504;#6.3504;#6.3504;#6.3504;#6.3504;#6.3504]`;;
let delta_y_dom = `[&2;&2;&2;&2;&2;&2]`, `[#2.52;#2.52;#2.52;#2.52;#2.52;#2.52]`;;



(***********************************)

let test_verify pp poly_tm min_flag val_tm (xx,zz) eps =
  let total_start = Sys.time() in
  let n = (get_dim o fst o dest_abs) poly_tm in
  let xx1 = convert_to_float_list pp true xx and
      zz1 = convert_to_float_list pp false zz in
  let xx2 = Informal_taylor.convert_to_float_list pp true xx and
      zz2 = Informal_taylor.convert_to_float_list pp false zz in
  let xx_float = map float_of_float_tm (dest_list xx1) and
      zz_float = map float_of_float_tm (dest_list zz1) in
  let eval_fs, tf, ti = mk_verification_functions pp poly_tm min_flag val_tm in
  let certificate = run_test tf xx_float zz_float false 0.0 true true true true eps in
  let c1 = transform_result xx_float zz_float certificate in
  let c1p = Informal_verifier.m_verify_list pp 1 pp ti c1 xx2 zz2 in
  let start = Sys.time() in
  let result = m_p_verify_list n pp eval_fs c1p xx1 zz1 in
  let finish = Sys.time() in
  let _ = report 
    (sprintf "Total time: %f; Verification time: %f" (finish -. total_start) (finish -. start)) in
    result;;


(******)

let pp = 5;;

let n = 2;;
let poly_tm = expr_to_vector_fun `x1 pow 3 + x2`;;

let xx = `[-- &1; &0]` and zz = `[&1; &1]`;;
let xx1 = convert_to_float_list pp true xx and
    zz1 = convert_to_float_list pp false zz;;

let xx_float = map float_of_float_tm (dest_list xx1) and
    zz_float = map float_of_float_tm (dest_list zz1);;

let eval_fs, tf, ti = mk_verification_functions pp poly_tm true `-- #1.1`;;
let certificate = run_test tf xx_float zz_float false 0.0 true false false false 0.0;;
let c1 = transform_result xx_float zz_float certificate;;
(* 5 *)
result_size certificate;;

m_verify_list n pp eval_fs c1 xx1 zz1;;

let c0 = run_test0 tf xx_float zz_float false 0.0 false false false 0.0;;
(* 7 *)
result_size c0;;
m_verify_raw0 n pp eval_fs c0 xx1 zz1;;

test_verify pp poly_tm true `-- &1` (xx,zz) 0.0;;



let domain0 = mk_m_center_domain n pp xx1 zz1;;
let domain1, _ = restrict_domain n 2 true domain0;;
let domain11, domain12 = split_domain n pp 1 domain1;;
let domain111, domain112 = split_domain n pp 1 domain11;;

let eval_taylor =
  match eval_fs with (_, _, _, f) -> f;;

let taylor0 = eval_taylor domain0;;
eval_m_taylor_upper_partial n pp 2 taylor0;;

let taylor111 = eval_taylor domain111;;
eval_m_taylor_upper_bound n pp taylor111;;
let taylor112 = eval_taylor domain112;;
eval_m_taylor_upper_bound n pp taylor112;;

let taylor12 = eval_taylor domain12;;
eval_m_taylor_upper_bound n pp taylor12;;




(****)
(* delta_x4 *)
let pp = 10;;
let n = 6;;
let xx = `[&4;&4;&4;&4;&4;&8]` and
    zz = `[#6.3504;#6.3504;#6.3504;#6.3504;#6.3504;#25.4016]`;;
let xx1 = convert_to_float_list pp true xx and
    zz1 = convert_to_float_list pp false zz;;

let xx_float = map float_of_float_tm (dest_list xx1) and
    zz_float = map float_of_float_tm (dest_list zz1);;


let eval_delta_x4, tf_delta_x4, ti = mk_verification_functions pp delta_x4_poly true `#6.02525`;;
let certificate = run_test tf_delta_x4 xx_float zz_float false 0.0 true true true false 0.0;;
let c1 = transform_result xx_float zz_float certificate;;
(* 1 *)
result_size certificate;;

m_verify_list n pp eval_delta_x4 c1 xx1 zz1;;
m_verify_raw0 n pp eval_delta_x4 certificate xx1 zz1;;


let c0 = run_test0 tf_delta_x4 xx_float zz_float false 0.0 true true false 0.0;;
(* 12 (true false false) 2 (true true false) *)
result_size c0;;
m_verify_raw0 n pp eval_delta_x4 c0 xx1 zz1;;

(* 1.076 *)
test 10 (m_verify_raw0 n pp eval_delta_x4 certificate xx1) zz1;;
(* 0.836 *)
test 10 (m_verify_raw0 n pp eval_delta_x4 c0 xx1) zz1;;



(***)
(* delta_x *)

let pp = 10;;
let n = 6;;
let xx = `[&4;&4;&4;&4;&4;&4]` and
    zz = `[#6.3504;#6.3504;#6.3504;#6.3504;#6.3504;#6.3504]`;;

let xx1 = convert_to_float_list pp true xx and
    zz1 = convert_to_float_list pp false zz;;
let xx_float = map float_of_float_tm (dest_list xx1) and
    zz_float = map float_of_float_tm (dest_list zz1);;

let eval_delta_x, tf_delta_x, ti = mk_verification_functions pp delta_x_poly true `#127.999`;;
let certificate = run_test tf_delta_x xx_float zz_float false 0.0 true true true true 0.0;;
let c1 = transform_result xx_float zz_float certificate;;
(* 1 *)
length c1;;
(* 46 (true false false) 10 (true true false) 10 (true true true) *)
result_size certificate;;
m_verify_raw0 n pp eval_delta_x certificate xx1 zz1;;
m_verify_list n pp eval_delta_x c1 xx1 zz1;;

let c0 = run_test0 tf_delta_x xx_float zz_float false 0.0 true true true 0.0;;
(* 4873 (true false true) 32 (true true true) *)
result_size c0;;
m_verify_raw0 n pp eval_delta_x c0 xx1 zz1;;

(* 10: 65 *)
test 1 (m_verify_raw_old n pp eval_delta_x certificate xx1) zz1;;
(* 10: 38.642
 100 (cached): 0.384
*)
reset_all();;
test 1 (m_verify_raw0 n pp eval_delta_x certificate xx1) zz1;;
(* 10: 40.187; 5.140 (convexity) 3.104 (find_and_replace_all); 3.028 (mixed_partials) *)
reset_all();;
test 1 (m_verify_list n pp eval_delta_x c1 xx1) zz1;;
(* 10: 1.860 *)
test 1 (m_verify_raw0 n pp eval_delta_x c0 xx1) zz1;;
(* 10: 4.228 (2.408, new restrict_domain) *)
test 1 (m_verify_domain_test n pp certificate xx1) zz1;;



(***)
(* delta_y *)
let pp = 10;;
let n = 6;;
let xx = `[&2;&2;&2;&2;&2;&2]` and
    zz = `[#2.52;#2.52;#2.52;#2.52;#2.52;#2.52]`;;

let xx1 = convert_to_float_list pp true xx and
    zz1 = convert_to_float_list 4 false zz;;
let xx2 = Informal_taylor.convert_to_float_list pp true xx and
    zz2 = Informal_taylor.convert_to_float_list 4 false zz;;
let xx_float = map float_of_float_tm (dest_list xx1) and
    zz_float = map float_of_float_tm (dest_list zz1);;

let eval_delta_y, tf_delta_y, ti_delta_y = mk_verification_functions pp delta_y_poly true `#127.999`;;
let certificate = run_test tf_delta_y xx_float zz_float false 0.0 true true true true 0.0;;
let c1 = transform_result xx_float zz_float certificate;;
let c1p = Informal_verifier.m_verify_list pp 1 pp ti_delta_y c1 xx2 zz2;;
(* 17 *)
length c1;;
(* 134 (true true false) 133 (128) (true true true) *)
result_size certificate;;

m_verify_list n pp eval_delta_y c1 xx1 zz1;;
(* 10: 494 *)
test 1 (m_verify_raw n pp eval0_delta_y eval_delta_y certificate xx1) zz1;;

(* 10: 362; 165 (find_and_replace_all); 166.9 (mixed_partials) 300: 75 
*)
reset_all();;
test 1 (m_verify_list n pp eval_delta_y c1 xx1) zz1;;

(* 100:  *)
reset_all();;
test 1 (m_p_verify_list n pp eval_delta_y c1p xx1) zz1;;

let c00 = run_test0 tf_delta_y xx_float zz_float false 0.0 true true true 0.0;;
(* 24671 (true false true) 1785 (1862) (true true true) *)
result_size c00;;
let c0 = transform_result xx_float zz_float c00;;
(* 431 (460) *)
length c0;;

(* 10: 406; 263 (find_and_replace_all) *)
test 1 (m_verify_list n pp eval_delta_y c0 xx1) zz1;;


(***)
let eval_delta_y0, tf_delta_y0 = mk_verification_functions pp delta_y_poly true `&0`;;
let certificate = run_test tf_delta_y0 xx_float zz_float false 0.0 true true true true 0.0;;
result_stat certificate;;
(* 25 (27) *)
result_size certificate;;
let c1 = transform_result xx_float zz_float certificate;;
(* 1 *)
length c1;;
m_verify_list n pp eval_delta_y0 c1 xx1 zz1;;
test 1 (m_verify_list n pp eval_delta_y0 c1 xx1) zz1;;


(***)
let poly1 = `x2 + x3 + x5 + x6 - #7.99 - #0.00385 * delta_y x1 x2 x3 x4 x5 x6 - 
  #2.75 * ((x1 + x4) * #0.5 - sqrt (&8))`;;
let poly_ineq = (expr_to_vector_fun o rand o concl o 
		   REWRITE_CONV[Sphere.delta_y; Sphere.delta_x]) poly1;;

let pp = 10;;
let n = 6;;

let xx = `[sqrt (&8); &2; &2; sqrt (&8); &2; &2]` and
    zz = `[&3; #2.07; #2.07; &4 * #1.26; #2.07; #2.07]`;;

let xx1 = convert_to_float_list pp true xx and
    zz1 = convert_to_float_list pp false zz;;
let xx_float = map float_of_float_tm (dest_list xx1) and
    zz_float = map float_of_float_tm (dest_list zz1);;

let eval_ineq, tf_ineq = mk_verification_functions pp poly_ineq true `&0`;;
let certificate = run_test tf_ineq xx_float zz_float false 0.0 true true true true 0.0;;
(* 51 (true true true) 54 (true false/true false) 439 (false false false) *)
result_size certificate;;
let c1 = transform_result xx_float zz_float certificate;;
(* 30 *)
length c1;;

m_verify_list n pp eval_ineq c1 xx1 zz1;;






(***)
(* schwefel *)
let pp = 12;;
let pp = 4;;
let n = 3;;
let xx = `[-- &10; -- &10; -- &10]` and
    zz = `[&10; &10; &10]`;;

let xx1 = convert_to_float_list pp true xx and
    zz1 = convert_to_float_list pp false zz;;
let xx_float = map float_of_float_tm (dest_list xx1) and
    zz_float = map float_of_float_tm (dest_list zz1);;

let eval_schwefel,tf_schwefel, ti = mk_verification_functions pp schwefel_poly true schwefel_min;;
let certificate = run_test tf_schwefel xx_float zz_float false 0.0 true true true true 0.0;;
result_stat certificate;;

let c1 = transform_result xx_float zz_float certificate;;
(* 641 (661 after eps = 1e-10)*)
length c1;;
(* 1922 (true false false) 1423 (true false true) 1427 (true true true) *)
result_size certificate;;

m_verify_list n pp eval_schwefel c1 xx1 zz1;;

(* 10: 698 (f0_flag: 133) *)
test 1 (m_verify_raw0 n pp eval0_schwefel eval_schwefel certificate xx1) zz1;;
(* 10: 103 (diff2_f: 100) (find_and_replace_all: 91); (mixed_partials: 93); 300: 54 *)
test 1 (m_verify_list n pp eval_schwefel c1 xx1) zz1;;

let c0 = run_test0 tf_schwefel xx_float zz_float false 0.0 true false false 0.0;;
(* 2152 (true false false) *)
result_size c0;;



(***)
(* rd *)

let pp = 12;;
let n = 3;;
let xx = `[-- &5; -- &5; -- &5]` and
    zz = `[&5; &5; &5]`;;

let xx1 = convert_to_float_list pp true xx and
    zz1 = convert_to_float_list pp false zz;;
let xx_float = map float_of_float_tm (dest_list xx1) and
    zz_float = map float_of_float_tm (dest_list zz1);;

let eval_rd, tf_rd = mk_verification_functions pp rd_poly true rd_min;;
let certificate = run_test tf_rd xx_float zz_float false 0.0 true true true 0.0;;
(* 1 *)
result_size certificate;;
m_verify_raw0 n pp eval_rd certificate xx1 zz1;;

(***)
(* caprasse *)

let pp = 8;;
let n = 4;;
let xx = `[-- #0.5; -- #0.5; -- #0.5; -- #0.5]` and
    zz = `[#0.5; #0.5; #0.5; #0.5]`;;

let xx1 = convert_to_float_list pp true xx and
    zz1 = convert_to_float_list pp false zz;;
let xx_float = map float_of_float_tm (dest_list xx1) and
    zz_float = map float_of_float_tm (dest_list zz1);;

let eval_caprasse,tf_caprasse,ti = mk_verification_functions pp caprasse_poly true caprasse_min;;
let certificate = run_test tf_caprasse xx_float zz_float false 0.0 true true true true 0.0;;
let c1 = transform_result xx_float zz_float certificate;;
(* 53 (true false true) 33 (true true true) (41, eps = 1e-10)*)
length c1;;
(* 48 (64, eps = 1e-10) (true true false/true) 80 (true false false) 80 (true false true) *)
result_size certificate;;
m_verify_list n pp eval_caprasse c1 xx1 zz1;;

(* 10: 30.826 (f0_flag: 16.497) (diff2_f: 10.1172, true false false) *)
test 1 (m_verify_raw0 n pp eval_caprasse certificate xx1) zz1;;
(* 10: 6.332 (8.912, eps = 1e-10); 4.848 (find_and_replace_all) *)
test 1 (m_verify_list n pp eval_caprasse c1 xx1) zz1;;

let c00 = run_test0 tf_caprasse xx_float zz_float false 0.0 true true true 0.0;;
(* 128 (true false false) 88 (true true false) *)
result_size c00;;
let c0 = transform_result xx_float zz_float c00;;
(* 69 *)
length c0;;
m_verify_list n pp eval_caprasse c0 xx1 zz1;;

(* 10: 6.652 (true true false) 4.632 (true true true) *)
test 1 (m_verify_list n pp eval_caprasse c0 xx1) zz1;;



(***)
(* lv *)

let pp = 5;;
let n = 4;;
let xx = `[-- &2; -- &2; -- &2; -- &2]` and
    zz = `[&2; &2; &2; &2]`;;

let xx1 = convert_to_float_list pp true xx and
    zz1 = convert_to_float_list pp false zz;;
let xx_float = map float_of_float_tm (dest_list xx1) and
    zz_float = map float_of_float_tm (dest_list zz1);;

let eval_lv, tf_lv = mk_verification_functions pp lv_poly true lv_min;;
let certificate = run_test tf_lv xx_float zz_float false 0.0 true true true 0.0;;
let c1 = transform_result xx_float zz_float certificate;;
(* 1 *)
length c1;;
(* 3 (true true false/true) 11 (true false false) *)
result_size certificate;;
m_verify_list n pp eval_lv c1 xx1 zz1;;

(* 10: 2.688 (f0_flag: 1.216) (df0_flag: 0.564) 0.052 (true true true) *)
test 1 (m_verify_list n pp eval_lv c1 xx1) zz1;;


let c0 = run_test0 tf_lv xx_float zz_float false 0.0 true true false 0.0;;
(* 11 (true false false) 3 (true true false) *)
result_size c0;;

(* 0.06 (true true false) *)
test 1 (m_verify_raw0 n pp eval_lv c0 xx1) zz1;;

(***)
(* butcher *)

let pp = 5;;
let n = 6;;
let xx = `[-- &1; -- #0.1; -- #0.1; -- &1; -- #0.1; -- #0.1]` and
    zz = `[&0; #0.9; #0.5; -- #0.1; -- #0.05; -- #0.03]`;;

let xx1 = convert_to_float_list pp true xx and
    zz1 = convert_to_float_list pp false zz;;
let xx_float = map float_of_float_tm (dest_list xx1) and
    zz_float = map float_of_float_tm (dest_list zz1);;

let eval_butcher, tf_butcher = mk_verification_functions pp butcher_poly true butcher_min;;
let certificate = run_test tf_butcher xx_float zz_float false 0.0 true true false 0.0;;
result_size certificate;;
m_verify_raw0 n pp eval_butcher certificate xx1 zz1;;


(***)
(* magnetism *)

let pp = 8;;
let n = 7;;
let xx = `[-- &1; -- &1; -- &1; -- &1; -- &1; -- &1; -- &1]` and
    zz = `[&1; &1; &1; &1; &1; &1; &1]`;;

let xx1 = convert_to_float_list pp true xx and
    zz1 = convert_to_float_list pp false zz;;
let xx_float = map float_of_float_tm (dest_list xx1) and
    zz_float = map float_of_float_tm (dest_list zz1);;

let eval_magnetism, tf_magnetism, ti = 
  mk_verification_functions pp magnetism_poly true magnetism_min;;
let certificate = run_test tf_magnetism xx_float zz_float false 0.0 true true true true 0.0;;
result_stat certificate;;

let c1 = transform_result xx_float zz_float certificate;;
(* 76 *)
length c1;;
(* 8732 (true false false) 77 (true false/true true) *)
result_size certificate;;

m_verify_list n pp eval_magnetism c1 xx1 zz1;;
(* 10: 7.86 (diff2_f: 5.788) *)
test 1 (m_verify_list n pp eval_magnetism c1 xx1) zz1;;


let c00 = run_test0 tf_magnetism xx_float zz_float false 0.0 true false true 0.0;;
(* 121 (true false true) *)
result_size c00;;
let c0 = transform_result xx_float zz_float c00;;
(* 120 *)
length c0;;
m_verify_list n pp eval_magnetism c0 xx1 zz1;;
(* 10: 13.772 (diff2_f: 9.517) *)
test 1 (m_verify_list n pp eval_magnetism c0 xx1) zz1;;





(***)
(* heart *)

let pp = 10;;
let pp = 4;;
let n = 8;;
let xx = `[-- #0.1; #0.4; -- #0.7; -- #0.7; #0.1; -- #0.1; -- #0.3; -- #1.1]` and
    zz = `[#0.4; &1; -- #0.4; #0.4; #0.2; #0.2; #1.1; -- #0.3]`;;

let xx1 = convert_to_float_list pp true xx and
    zz1 = convert_to_float_list pp false zz;;
let xx_float = map float_of_float_tm (dest_list xx1) and
    zz_float = map float_of_float_tm (dest_list zz1);;

let eval_heart, tf_heart, ti = mk_verification_functions pp heart_poly true heart_min;;
let certificate = run_test tf_heart xx_float zz_float false 0.0 true true true true 1e-10;;
result_stat certificate;;
let c1 = transform_result xx_float zz_float certificate;;
(* 23 *)
length c1;;
(* 42 (true true false) 50 (true false false) 48 (true false true) 37 (true true true) *)
result_size certificate;;
m_verify_list n pp eval_heart c1 xx1 zz1;;

let c00 = run_test0 tf_heart xx_float zz_float false 0.0 true true true 1e-10;;
(* 46 (true true false) 61 (true false false) 45 (true true true) *)
result_size c00;;
let c0 = transform_result xx_float zz_float c00;;
(* 32 *)
length c0;;
m_verify_list n pp eval_heart c0 xx1 zz1;;


(* 10: 109 *)
test 1 (m_verify_raw_old n pp eval_heart certificate xx1) zz1;;

(* 10: 94 (f0_flag: 22.929) (df0_flag: 13.229) *)
test 1 (m_verify_raw0 n pp eval0_heart eval_heart certificate xx1) zz1;;

(* 10: 13.689 (diff2_f: 7.080 (true false true)) 4.868 (true true true) 4.448 (find_and_replace_all) *)
test 1 (m_verify_list n pp eval_heart c1 xx1) zz1;;
(* 10: 4.048 *)
test 1 (m_verify_raw0 n pp eval_heart c00 xx1) zz1;;
(* 10: 4.248 *)
test 1 (m_verify_list n pp eval_heart c0 xx1) zz1;;



(* 10: 13 (10.625, new restrict_domain) (f0_flag: 5.3) (df0_flag: 2.264) *)
test 1 (m_verify_domain_test n pp certificate xx1) zz1;;




(************************************)
(* full time tests *)
(* Bernstein PVS time in parentheses *)

(* 10: 93.717; 89.042 (10.23; 3.18) *)
(* 10 (adaptive p): 93.602; 83.853 *)
test_verify 12 schwefel_poly true schwefel_min schwefel_dom 0.0;;

(* 10: 1.860; 0.024 (3.11; 0.17) *)
test_verify 11 rd_poly true rd_min rd_dom 0.0;;

(* 10: 11.829; 4.856 (11.44; 1.2) *)
reset_all();;
test_verify 8 caprasse_poly true caprasse_min caprasse_dom 0.0;;

(* 10: 2.204; 0.048 (4.75; 0.23) *)
test_verify 5 lv_poly true lv_min lv_dom 0.0;;

(* 10: 4.164; 0.024 (19.83; 0.47)*)
test_verify 5 butcher_poly true butcher_min butcher_dom 0.0;;

(* 10: 11.965; 5.600 (160.44; 82.87) *)
test_verify 8 magnetism_poly true magnetism_min magnetism_dom 0.0;;

(* 10: 23.205; 4.376 (79.68; 26.14) *)
(* 10 (adaptive p): 20.145; 4.288 *)
test_verify 10 heart_poly true heart_min heart_dom 1e-10;;