needs "../formal_lp/formal_interval/m_taylor_arith2.hl";;
needs "../formal_lp/formal_interval/m_verifier.hl";;
needs "../formal_lp/arith/informal/informal_m_verifier.hl";;



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


let dest_int int =
  let f1, f2 = Informal_interval.dest_interval int in
    Informal_float.dest_float f1, Informal_float.dest_float f2;;

let dest_f = Informal_float.dest_float;;

let dest_dom dom =
  map dest_f dom.Informal_taylor.lo,
  map dest_f dom.Informal_taylor.hi,
  map dest_f dom.Informal_taylor.y,
  map dest_f dom.Informal_taylor.w;;

let dest_ti ti =
  dest_int ti.Informal_taylor.f, 
  map dest_int ti.Informal_taylor.df, 
  map (map dest_int) ti.Informal_taylor.ddf;;



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

(* dummy functions *)

let eval_d0 i pp t1 t2 = failwith "eval_d0";;
let eval_dd0 i j pp t1 t2 = failwith "eval_dd0";;
let eval_0 pp t1 t2 = failwith "eval_0";;
let eval_diff2 t1 t2 = failwith "eval_diff2";;


(******************************)
(* real tests *)

let n = 6;;
let pp = 15;;
let pp = 8;;

(* delta_y *)
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;;

(* delta_y4 *)
let delta_y4_poly =
  let tm = (rand o concl o SPECL[`y1*y1`; `y2*y2`; `y3*y3`; `y4*y4`; `y5*y5`; `y6*y6`]) Sphere.delta_x4 in
    expr_to_vector_fun tm;;

(* 4 * y1 * delta_y *)
let four_y1_delta_y_poly = 
  let x_var, tm = dest_abs delta_y_poly in
    mk_abs (x_var, mk_binop mul_op_real `&4` (mk_binop mul_op_real `(x:real^6)$1 * x$1` tm));;

(* - delta_y4 *)
let neg_delta_y4_poly =
  let x_var, tm = dest_abs delta_y4_poly in
    mk_abs (x_var, mk_comb (neg_op_real, tm));;


let eval_neg_delta_y4, tf_neg_delta_y4, ti_neg_delta_y4 = 
  mk_verification_functions pp neg_delta_y4_poly false `&0`;;

let eval_4y1_delta_y, tf_4y1_delta_y, ti_4y1_delta_y = 
  mk_verification_functions pp four_y1_delta_y_poly false `&0`;;

let eval_pi2, tf_pi2, ti_pi2 = 
  mk_verification_functions pp `\x:real^6. pi / &2` false `&0`;;


let eval_pi2_plus, tf_pi2_plus, ti_pi2_plus = 
  mk_verification_functions pp `\x:real^6. pi / &2 - #1.893` false `&0`;;


(* dih_y *)
open Univariate;;

let tf_dih_y_hi =
  let denom = Uni_compose (uinv, Uni_compose (usqrt, tf_4y1_delta_y)) in
    Plus (tf_pi2_plus, Uni_compose (uatan, Product (tf_neg_delta_y4, denom)));;

let eval_dih_y_hi p_lin p_second th =
  let inv, atn, sqrt, ( * ), ( + ) = 
    eval_m_taylor_inv2 n p_lin p_second, eval_m_taylor_atn2 n p_lin p_second, 
    eval_m_taylor_sqrt2 n p_lin p_second, eval_m_taylor_mul2 n p_lin p_second, 
    eval_m_taylor_add2 n p_lin p_second in
  let poly1 = eval_4y1_delta_y.taylor p_lin p_second th and
      poly2 = eval_neg_delta_y4.taylor p_lin p_second th and
      pi2 = eval_pi2_plus.taylor p_lin p_second th in
    pi2 + atn (poly2 * inv (sqrt (poly1)));;


let ti_dih_y_hi p_lin p_second th =
  let inv, atn, sqrt, ( * ), ( + ) = 
    Informal_taylor.eval_m_taylor_inv p_lin p_second, Informal_taylor.eval_m_taylor_atn p_lin p_second, 
    Informal_taylor.eval_m_taylor_sqrt p_lin p_second, Informal_taylor.eval_m_taylor_mul p_lin p_second, 
    Informal_taylor.eval_m_taylor_add p_lin p_second in
  let poly1 = ti_4y1_delta_y.Informal_verifier.taylor p_lin p_second th and
      poly2 = ti_neg_delta_y4.Informal_verifier.taylor p_lin p_second th and
      pi2 = ti_pi2_plus.Informal_verifier.taylor p_lin p_second th in
    pi2 + atn (poly2 * inv (sqrt (poly1)));;


let eval_taylor =
  {taylor = eval_dih_y_hi; f = eval_0; df = eval_d0; ddf = eval_dd0; diff2_f = eval_diff2};;

let ti = 
  {Informal_verifier.taylor = ti_dih_y_hi;
  Informal_verifier.f = eval_0;
  Informal_verifier.df = eval_d0;
  Informal_verifier.ddf = eval_dd0};;



(************)
(* Small domain *)
let xx_s = `[&2; &2; &2; &2; &2; &2]` and
    zz_s = `[#2.1; #2.1; #2.1; #2.1; #2.1; #2.1]`;;

(* domain *)
let domain_th =
  let xx1_s = convert_to_float_list pp true xx_s and
      zz1_s = convert_to_float_list pp false zz_s in
    mk_m_center_domain n pp xx1_s zz1_s;;

let dom =
  let xx2_s = Informal_taylor.convert_to_float_list pp true xx_s and
      zz2_s = Informal_taylor.convert_to_float_list pp false zz_s in
    Informal_taylor.mk_m_center_domain pp xx2_s zz2_s;;
  

	
(* 10: 9.121 (pp = 15) *)
(* 300: 5.5 (pp = 8) *)
(* 100 (cached, float_cached, pp = 8): 2.68 *)
(* 100 (optimization): 1.732 *)
(* 200 (m_taylor_arith2): 1.428 *)
reset_all();;
test 1 (eval_dih_y_hi pp pp) domain_th;;
(* 100: 1.668 *)
(* 200 (optimization): 0.580 *)
(* 200 (m_taylor_arith2): 0.328 *)
test 1 (eval_dih_y_hi pp pp) domain_th;;
(* 100: 0.088 *)

test 1 (ti_dih_y_hi pp pp) dom;;


Arith_cache.print_stat();;
Arith_float.print_stat();;

(***)

let th1 = eval_4y1_delta_y.taylor pp pp domain_th;;
let th2 = eval_neg_delta_y4.taylor pp pp domain_th;;
let pi2_th = eval_pi2_plus.taylor pp pp domain_th;;

let r1 = eval_m_taylor_sqrt2 n pp pp th1;;
let r2 = eval_m_taylor_inv2 n pp pp r1;;
let r3 = eval_m_taylor_mul2 n pp pp th2 r2;;
let r4 = eval_m_taylor_atn2 n pp pp r3;;
let r5 = eval_m_taylor_add2 n pp pp pi2_th r4;;

reset_all();;

(* 100: 0.264 (second: 0.084) *)
test 1 (eval_4y1_delta_y.taylor pp pp) domain_th;;
(* 100: 0.032 (second: 0.020) *)
test 1 (eval_neg_delta_y4.taylor pp pp) domain_th;;
(* 100: 0.000 (second: 0.000) *)
test 1 (eval_pi2_plus.taylor pp pp) domain_th;;

(* 100: 0.356 (second: 0.168); 0.300 (0.116) *)
test 1 (eval_m_taylor_sqrt n pp pp) th1;;
(* 200: 0.220 (second: 0.048) *)
test 1 (eval_m_taylor_sqrt2 n pp pp) th1;;

(* 100: 0.412 (second: 0.188); 0.316 (0.104) *)
test 1 (eval_m_taylor_inv n pp pp) r1;;
(* 200: 0.264 (second: 0.056) *)
test 1 (eval_m_taylor_inv2 n pp pp) r1;;

(* 100: 0.384 (second: 0.212); 0.316 (0.140) *)
test 1 (eval_m_taylor_mul n pp pp th2) r2;;
(* 200: 0.244 (second: 0.092) *)
test 1 (eval_m_taylor_mul2 n pp pp th2) r2;;

(* 100: 0.616 (second: 0.272); build2: 0.504 (0.132) *)
test 1 (eval_m_taylor_atn n pp pp) r3;;
(* 200: 0.436 (second: 0.060) *)
test 1 (eval_m_taylor_atn2 n pp pp) r3;;

(* 100: 0.096 (second: 0.072); 0.072 (0.052) *)
test 1 (eval_m_taylor_add n pp pp pi2_th) r4;;
(* 200: 0.032 (second: 0.024) *)
test 1 (eval_m_taylor_add2 n pp pp pi2_th) r4;;



(***)
let xx = `[&2; &2; &2; &2; &2; &2]` and
    zz = `[#2.52; #2.52; #2.52; #2.52; #2.52; #2.52]`;;

let xx_s = `[&2; &2; &2; &2; &2; &2]` and
    zz_s = `[#2.52; #2.1; #2.1; #2.1; #2.1; #2.1]`;;

let xx_s2 = `[&2; &2; &2; &2; &2; &2]` and
    zz_s2 = `[#2.52; #2.2; #2.2; #2.2; #2.2; #2.2]`;;


let pp0 = 3;;
let pp0 = 5;;
let xx1 = convert_to_float_list pp0 true xx and
    zz1 = convert_to_float_list pp0 false zz and
    xx1_s = convert_to_float_list pp0 true xx_s and
    zz1_s = convert_to_float_list pp0 false zz_s and
    xx1_s2 = convert_to_float_list pp0 true xx_s2 and
    zz1_s2 = convert_to_float_list pp0 false zz_s2;;

let xx2 = Informal_taylor.convert_to_float_list pp0 true xx and
    zz2 = Informal_taylor.convert_to_float_list pp0 false zz and
    xx2_s = Informal_taylor.convert_to_float_list pp0 true xx_s and
    zz2_s = Informal_taylor.convert_to_float_list pp0 false zz_s and
    xx2_s2 = Informal_taylor.convert_to_float_list pp0 true xx_s2 and
    zz2_s2 = Informal_taylor.convert_to_float_list pp0 false zz_s2;;


let xx_float, zz_float, xx_s_float, zz_s_float, xx_s2_float, zz_s2_float =
  let pad = replicate 0.0 (8 - length (dest_list xx1)) in
    map float_of_float_tm (dest_list xx1) @ pad,
    map float_of_float_tm (dest_list zz1) @ pad,
    map float_of_float_tm (dest_list xx1_s) @ pad,
    map float_of_float_tm (dest_list zz1_s) @ pad,
    map float_of_float_tm (dest_list xx1_s2) @ pad,
    map float_of_float_tm (dest_list zz1_s2) @ pad;;



(***)


let c_dih_y_s = run_test tf_dih_y_hi xx_s_float zz_s_float false 0.0 true false true false 0.0;;
let c_dih_y_s2 = run_test tf_dih_y_hi xx_s2_float zz_s2_float false 0.0 true false true false 0.0;;
let c_dih_y0 = run_test tf_dih_y_hi xx_float zz_float false 0.0 true false false false 0.0;;

(* pass = 4 *)
result_stat c_dih_y_s;;
(* pass = 63 *)
result_stat c_dih_y_s2;;
(* pass = 4294, mono = 10 *)
result_stat c_dih_y0;;

let p_split = pp and
    p_min = 1 and
    p_max = pp;;

let cp_s = Informal_verifier.m_verify_raw0 p_split p_min p_max ti c_dih_y_s xx2_s zz2_s;;
let cp_s2 = Informal_verifier.m_verify_raw0 p_split p_min p_max ti c_dih_y_s2 xx2_s2 zz2_s2;;


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

reset_all();;

(* 10 (pp = 15): 38.418 *)
(* 300 (pp = 8): 22.289 *)
(* 100 (cached, float_cached, pp = 8): 12.229; 9.372 (MY_BETA_RULE); 8.028 (build2) *)
(* 200 (m_taylor_arith2) : 6.548 *)
let _ =
  let start = Sys.time() in
  let result = m_verify_raw0 n pp eval_taylor c_dih_y_s xx1_s zz1_s in
  let finish = Sys.time() in
  let _ = report 
    (sprintf "Verification time: %f" (finish -. start)) in
    result;;

Arith_cache.print_stat();;
Arith_float.print_stat();;


(* 100 (cached, float_cached, pp = 8): 8.025; 5.116 (MY_BETA_RULE); 3.700 (build2) *)
(* 200 (m_taylor_arith2): 2.496 *)
reset_all();;
let _ =
  let start = Sys.time() in
  let result = m_p_verify_raw0 n p_split eval_taylor cp_s xx1_s zz1_s in
  let finish = Sys.time() in
  let _ = report 
    (sprintf "Verification time: %f" (finish -. start)) in
    result;;

(* stats *)
result_p_stat false cp_s2;;

(* 100 (cached, float_cached, pp = adaptive): 129.788; 87.729 (MY_BETA_RULE); 64.884 (build2) *)
(* (pp = 8: 233.80) *)
(* 200: 63.984 (build2) *)
(* 200 (m_taylor_arith2): 43.927 *)
reset_all();;

let _ =
  let start = Sys.time() in
  let result = m_p_verify_raw0 n p_split eval_taylor cp_s2 xx1_s2 zz1_s2 in
  let finish = Sys.time() in
  let _ = report 
    (sprintf "Verification time: %f" (finish -. start)) in
    result;;

(*****************)
let cp = Informal_verifier.m_verify_raw0 p_split p_min p_max ti c_dih_y0 xx2 zz2;;
result_p_stat false cp;;

(* 100: 9105 (was 15202)*)
(* 200 (build2): 4242 *)
(* 200 (m_taylor_arith2): 3121 *)
(* 200 (mixed_partials): 2880 *)
reset_all();;
let _ =
  let start = Sys.time() in
  let result = m_p_verify_raw0 n p_split eval_taylor cp xx1 zz1 in
  let finish = Sys.time() in
  let _ = report 
    (sprintf "Verification time: %f" (finish -. start)) in
    result;;





(**************************************)
(* 3318775219 *)

let tf_dih_y =
  let denom = Uni_compose (uinv, Uni_compose (usqrt, tf_4y1_delta_y)) in
    Plus (tf_pi2, Uni_compose (uatan, Product (tf_neg_delta_y4, denom)));;

let eval_dih_y p_lin p_second th =
  let inv, atn, sqrt, ( * ), ( + ) = 
    eval_m_taylor_inv2 n p_lin p_second, eval_m_taylor_atn2 n p_lin p_second, 
    eval_m_taylor_sqrt2 n p_lin p_second, eval_m_taylor_mul2 n p_lin p_second, 
    eval_m_taylor_add2 n p_lin p_second in
  let poly1 = eval_4y1_delta_y.taylor p_lin p_second th and
      poly2 = eval_neg_delta_y4.taylor p_lin p_second th and
      pi2 = eval_pi2.taylor p_lin p_second th in
    pi2 + atn (poly2 * inv (sqrt (poly1)));;


let ti_dih_y p_lin p_second th =
  let inv, atn, sqrt, ( * ), ( + ) = 
    Informal_taylor.eval_m_taylor_inv p_lin p_second, Informal_taylor.eval_m_taylor_atn p_lin p_second, 
    Informal_taylor.eval_m_taylor_sqrt p_lin p_second, Informal_taylor.eval_m_taylor_mul p_lin p_second, 
    Informal_taylor.eval_m_taylor_add p_lin p_second in
  let poly1 = ti_4y1_delta_y.Informal_verifier.taylor p_lin p_second th and
      poly2 = ti_neg_delta_y4.Informal_verifier.taylor p_lin p_second th and
      pi2 = ti_pi2.Informal_verifier.taylor p_lin p_second th in
    pi2 + atn (poly2 * inv (sqrt (poly1)));;


(* - #1.629 +  
  (#0.414 * (y2 + y3 + y5 + y6 - #8.0)) -
  (#0.763 * (y4 - #2.52)) - 
  (#0.315 * (y1 - #2.0)) *)
let neg_poly3318 = expr_to_vector_fun `-- (-- #1.629 +  
  (#0.414 * (y2 + y3 + y5 + y6 - #8.0)) -
  (#0.763 * (y4 - #2.52)) - 
  (#0.315 * (y1 - #2.0)))`;;

let eval_poly3318, tf_poly3318, ti_poly3318 =
  mk_verification_functions pp neg_poly3318 false `&0`;;


let tf_3318 =
  let dih = tf_dih_y in
  let poly = tf_poly3318 in
    Plus (poly, Scale (dih, mk_interval (-1.0, -1.0)));;
    

let eval_3318 p_lin p_second th =
  let ( - ) = eval_m_taylor_sub2 n p_lin p_second in
  let dih = eval_dih_y p_lin p_second th and
      poly = eval_poly3318.taylor p_lin p_second th in
    poly - dih;;

let ti_3318 p_lin p_second th =
  let ( - ) = Informal_taylor.eval_m_taylor_sub p_lin p_second in
  let dih = ti_dih_y p_lin p_second th and
      poly = ti_poly3318.Informal_verifier.taylor p_lin p_second th in
    poly - dih;;


let eval_taylor =
  {taylor = eval_3318; f = eval_0; df = eval_d0; ddf = eval_dd0; diff2_f = eval_diff2};;

let ti = 
  {Informal_verifier.taylor = ti_3318;
  Informal_verifier.f = eval_0;
  Informal_verifier.df = eval_d0;
  Informal_verifier.ddf = eval_dd0};;


(* domain *)
let xx = `[&2; &2; &2; #2.52; &2; &2]` and
    zz = `[#2.52; #2.52; #2.52; sqrt(&8); #2.52; #2.52]`;;

let xx_s = `[&2; &2; &2; #2.52; &2; &2]` and
    zz_s = `[#2.52; #2.1; #2.1; sqrt(&8); #2.1; #2.1]`;;

let pp0 = 3;;
let xx1 = convert_to_float_list pp0 true xx and
    zz1 = convert_to_float_list pp0 false zz and
    xx1_s = convert_to_float_list pp0 true xx_s and
    zz1_s = convert_to_float_list pp0 false zz_s;;

let xx2 = Informal_taylor.convert_to_float_list pp0 true xx and
    zz2 = Informal_taylor.convert_to_float_list pp0 false zz and
    xx2_s = Informal_taylor.convert_to_float_list pp0 true xx_s and
    zz2_s = Informal_taylor.convert_to_float_list pp0 false zz_s;;

let xx_float, zz_float, xx_s_float, zz_s_float =
  let pad = replicate 0.0 (8 - length (dest_list xx1)) in
    map float_of_float_tm (dest_list xx1) @ pad,
    map float_of_float_tm (dest_list zz1) @ pad,
    map float_of_float_tm (dest_list xx1_s) @ pad,
    map float_of_float_tm (dest_list zz1_s) @ pad;;


(* certificates *)

let c_s = run_test tf_3318 xx_s_float zz_s_float false 0.0 true false false false 0.0;;
let c0 = run_test tf_3318 xx_float zz_float false 0.0 true false false false 0.0;;
let c_test = run_test tf_3318 xx_float zz_float false 0.0 true true true true 0.0;;

(* pass = 355, mono = 21 *)
result_stat c_s;;
(* pass = 16165, mono = 1036 *)
result_stat c0;;
(* pass = 15924 (raw = 1), mono = 796, pass_mono = 240 *)
result_stat c_test;;

let p_split = pp and
    p_min = 1 and
    p_max = pp;;

let cp_s = Informal_verifier.m_verify_raw0 p_split p_min p_max ti c_s xx2_s zz2_s;;
let cp0 = Informal_verifier.m_verify_raw0 p_split p_min p_max ti c0 xx2 zz2;;


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

reset_all();;

(* 200 (m_taylor_arith2): 282.7 *)
let _ =
  let start = Sys.time() in
  let result = m_p_verify_raw0 n p_split eval_taylor cp_s xx1_s zz1_s in
  let finish = Sys.time() in
  let _ = report 
    (sprintf "Verification time: %f" (finish -. start)) in
    result;;


reset_all();;

(* 200 (m_taylor_arith2): 14175.2 *)
let _ =
  let start = Sys.time() in
  let result = m_p_verify_raw0 n p_split eval_taylor cp0 xx1 zz1 in
  let finish = Sys.time() in
  let _ = report 
    (sprintf "Verification time: %f" (finish -. start)) in
    result;;


(**************************************)
(* 9922699028 *)


(* #1.6294 -  
  (#0.2213 * (y2 + y3 + y5 + y6 - #8.0)) +
  (#0.913 * (y4 - #2.52)) + 
  (#0.728 * (y1 - #2.0)) *)
let neg_poly9922 = expr_to_vector_fun `-- (#1.6294 -  
  (#0.2213 * (y2 + y3 + y5 + y6 - #8.0)) +
  (#0.913 * (y4 - #2.52)) + 
  (#0.728 * (y1 - #2.0)))`;;

let eval_poly9922, tf_poly9922, ti_poly9922 =
  mk_verification_functions pp neg_poly9922 false `&0`;;



let tf_9922 =
  let dih = tf_dih_y in
  let poly = tf_poly9922 in
    Plus (dih, poly);;
    

let eval_9922 p_lin p_second th =
  let ( + ) = eval_m_taylor_add2 n p_lin p_second in
  let dih = eval_dih_y p_lin p_second th and
      poly = eval_poly9922.taylor p_lin p_second th in
    dih + poly;;

let ti_9922 p_lin p_second th =
  let ( + ) = Informal_taylor.eval_m_taylor_add p_lin p_second in
  let dih = ti_dih_y p_lin p_second th and
      poly = ti_poly9922.Informal_verifier.taylor p_lin p_second th in
    dih + poly;;


let eval_taylor =
  {taylor = eval_9922; f = eval_0; df = eval_d0; ddf = eval_dd0; diff2_f = eval_diff2};;

let ti = 
  {Informal_verifier.taylor = ti_9922;
  Informal_verifier.f = eval_0;
  Informal_verifier.df = eval_d0;
  Informal_verifier.ddf = eval_dd0};;


(* domain *)
let xx = `[&2; &2; &2; #2.52; &2; &2]` and
    zz = `[#2.52; #2.52; #2.52; sqrt(&8); #2.52; #2.52]`;;

let xx_s = `[&2; &2; &2; #2.52; &2; &2]` and
    zz_s = `[#2.52; #2.1; #2.1; sqrt(&8); #2.1; #2.1]`;;

let pp0 = 3;;
let xx1 = convert_to_float_list pp0 true xx and
    zz1 = convert_to_float_list pp0 false zz and
    xx1_s = convert_to_float_list pp0 true xx_s and
    zz1_s = convert_to_float_list pp0 false zz_s;;

let xx2 = Informal_taylor.convert_to_float_list pp0 true xx and
    zz2 = Informal_taylor.convert_to_float_list pp0 false zz and
    xx2_s = Informal_taylor.convert_to_float_list pp0 true xx_s and
    zz2_s = Informal_taylor.convert_to_float_list pp0 false zz_s;;

let xx_float, zz_float, xx_s_float, zz_s_float =
  let pad = replicate 0.0 (8 - length (dest_list xx1)) in
    map float_of_float_tm (dest_list xx1) @ pad,
    map float_of_float_tm (dest_list zz1) @ pad,
    map float_of_float_tm (dest_list xx1_s) @ pad,
    map float_of_float_tm (dest_list zz1_s) @ pad;;


(* certificates *)

let c_s = run_test tf_9922 xx_s_float zz_s_float false 0.0 true false false false 0.0;;
let c0 = run_test tf_9922 xx_float zz_float false 0.0 true false false false 0.0;;
let c_test = run_test tf_9922 xx_float zz_float false 0.0 true true true true 0.0;;

(* pass = 179, mono = 26 *)
result_stat c_s;;
(* pass = 6322, mono = 235 *)
result_stat c0;;
(* pass = 6307 (raw = 5), mono = 220, pass_mono = 15 *)
result_stat c_test;;

let p_split = pp and
    p_min = 1 and
    p_max = pp;;

let cp_s = Informal_verifier.m_verify_raw0 p_split p_min p_max ti c_s xx2_s zz2_s;;
let cp0 = Informal_verifier.m_verify_raw0 p_split p_min p_max ti c0 xx2 zz2;;


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

reset_all();;

(* 200 (m_taylor_arith2): 157.2 *)
let _ =
  let start = Sys.time() in
  let result = m_p_verify_raw0 n p_split eval_taylor cp_s xx1_s zz1_s in
  let finish = Sys.time() in
  let _ = report 
    (sprintf "Verification time: %f" (finish -. start)) in
    result;;


reset_all();;

(* 200 (m_taylor_arith2): 5039.6  *)
let _ =
  let start = Sys.time() in
  let result = m_p_verify_raw0 n p_split eval_taylor cp0 xx1 zz1 in
  let finish = Sys.time() in
  let _ = report 
    (sprintf "Verification time: %f" (finish -. start)) in
    result;;