1 (* Multivariate polynomial inequalities *)
2 (* Examples are taken from the paper:
3 César Muñoz and Anthony Narkawicz,
4 Formalization of a Representation of Bernstein Polynomials and Applications to Global Optimization,
5 Journal of Automated Reasoning, DOI: 10.1007/s10817-012-9256-3
6 http://shemesh.larc.nasa.gov/people/cam/Bernstein/ *)
9 (* Set up the loading path:
10 load_path := "path to the formal_ineqs directory" :: !load_path;;
13 (* Change default arithmetic options before loading other libraries *)
14 (* (arithmetic options cannot be changed later) *)
15 needs "arith_options.hl";;
17 (* Set the base of natural number arithmetic to 200 *)
18 Arith_options.base := 200;;
20 (* Load all verification libraries *)
21 (* Note: the verification library loads Multivariate/realanalysis.ml,
22 so it is recommended to use a checkpointed version of HOL Light
23 with preloaded realanalysis.ml *)
24 needs "verifier/m_verifier_main.hl";;
27 Set the level of info/debug printing:
28 0 - no info/debug printing
29 1 - report important steps (default)
32 needs "verifier_options.hl";;
33 Verifier_options.info_print_level := 1;;
35 (* Open the main verification module *)
36 open M_verifier_main;;
42 let schwefel_poly = `(x1 - x2 pow 2) pow 2 + (x2 - &1) pow 2 +
43 (x1 - x3 pow 2) pow 2 + (x3 - &1) pow 2` and
45 rd_poly = `-- x1 + &2 * x2 - x3 - #0.835634534 * x2 * (&1 + x2)` and
47 caprasse_poly = `-- x1 * x3 pow 3 + &4 * x2 * x3 pow 2 * x4 +
48 &4 * x1 * x3 * x4 pow 2 + &2 * x2 * x4 pow 3 + &4 * x1 * x3 + &4 * x3 pow 2 -
49 &10 * x2 * x4 - &10 * x4 pow 2 + &2` and
51 lv_poly = `x1 * x2 pow 2 + x1 * x3 pow 2 + x1 * x4 pow 2 - #1.1 * x1 + &1` and
53 butcher_poly = `x6 * x2 pow 2 + x5 * x3 pow 2 - x1 * x4 pow 2 + x4 pow 2 -
54 &1 / &3 * x1 + &4 / &3 * x4` and
56 magnetism_poly = `x1 pow 2 + &2 * x2 pow 2 + &2 * x3 pow 2 + &2 * x4 pow 2 +
57 &2 * x5 pow 2 + &2 * x6 pow 2 + &2 * x7 pow 2 - x1` and
59 heart_poly = `-- x1 * x6 pow 3 + &3 * x1 * x6 * x7 pow 2 - x3 * x7 pow 3 +
60 &3 * x3 * x7 * x6 pow 2 - x2 * x5 pow 3 + &3 * x2 * x5 * x8 pow 2 - x4 * x8 pow 3 +
61 &3 * x4 * x8 * x5 pow 2 - #0.9563453`;;
64 let schwefel_min = `-- #0.00000000058806` and
65 rd_min = `-- #36.7126907` and
66 caprasse_min = `-- #3.1801` and
67 lv_min = `-- #20.801` and
68 butcher_min = `-- #1.44` and
69 magnetism_min = `-- #0.25001` and
70 heart_min = `-- #1.7435`;;
73 let schwefel_dom = `[-- &10; -- &10; -- &10]`, `[&10; &10; &10]` and
74 rd_dom = `[-- &5; -- &5; -- &5]`, `[&5; &5; &5]` and
75 caprasse_dom = `[-- #0.5; -- #0.5; -- #0.5; -- #0.5]`, `[#0.5; #0.5; #0.5; #0.5]` and
76 lv_dom = `[-- &2; -- &2; -- &2; -- &2]`, `[&2; &2; &2; &2]` and
77 butcher_dom = `[-- &1; -- #0.1; -- #0.1; -- &1; -- #0.1; -- #0.1]`,
78 `[&0; #0.9; #0.5; -- #0.1; -- #0.05; -- #0.03]` and
79 magnetism_dom = `[-- &1; -- &1; -- &1; -- &1; -- &1; -- &1; -- &1]`,
80 `[&1; &1; &1; &1; &1; &1; &1]` and
81 heart_dom = `[-- #0.1; #0.4; -- #0.7; -- #0.7; #0.1; -- #0.1; -- #0.3; -- #1.1]`,
82 `[#0.4; &1; -- #0.4; #0.4; #0.2; #0.2; #1.1; -- #0.3]`;;
85 let mk_poly_ineq poly_tm min_tm dom =
86 let n = length (frees poly_tm) in
87 let xs = map (fun i -> "x"^string_of_int i) (1--n) in
88 let ineq_tm = mk_binop `(<):real->real->bool` min_tm poly_tm in
89 let ineq2_tm = M_verifier_main.mk_ineq ineq_tm xs dom in
92 (* Create all inequalities *)
100 mk_poly_ineq schwefel_poly schwefel_min schwefel_dom,
101 mk_poly_ineq rd_poly rd_min rd_dom,
102 mk_poly_ineq caprasse_poly caprasse_min caprasse_dom,
103 mk_poly_ineq lv_poly lv_min lv_dom,
104 mk_poly_ineq butcher_poly butcher_min butcher_dom,
105 mk_poly_ineq magnetism_poly magnetism_min magnetism_dom,
106 mk_poly_ineq heart_poly heart_min heart_dom;;
111 let test_schwefel () =
112 verify_ineq default_params 5 schwefel_ineq;;
115 verify_ineq default_params 5 rd_ineq;;
117 let test_caprasse () =
118 verify_ineq default_params 5 caprasse_ineq;;
121 verify_ineq default_params 5 lv_ineq;;
123 let test_butcher () =
124 verify_ineq default_params 5 butcher_ineq;;
126 let test_magnetism () =
127 verify_ineq default_params 5 magnetism_ineq;;
130 verify_ineq {default_params with eps = 1e-10} 5 heart_ineq;;
134 [test_schwefel(); test_rd(); test_caprasse(); test_lv();
135 test_butcher(); test_magnetism(); test_heart()];;
138 map fst (run_tests());;