1 (* Title: HOL/Library/Sum_Of_Squares/sos_wrapper.ML |
|
2 Author: Philipp Meyer, TU Muenchen |
|
3 |
|
4 Added functionality for sums of squares, e.g. calling a remote prover. |
|
5 *) |
|
6 |
|
7 signature SOS_WRAPPER = |
|
8 sig |
|
9 datatype prover_result = Success | Failure | Error |
|
10 val setup: theory -> theory |
|
11 val dest_dir: string Config.T |
|
12 val prover_name: string Config.T |
|
13 end |
|
14 |
|
15 structure SOS_Wrapper: SOS_WRAPPER = |
|
16 struct |
|
17 |
|
18 datatype prover_result = Success | Failure | Error |
|
19 |
|
20 fun str_of_result Success = "Success" |
|
21 | str_of_result Failure = "Failure" |
|
22 | str_of_result Error = "Error" |
|
23 |
|
24 |
|
25 (*** calling provers ***) |
|
26 |
|
27 val (dest_dir, setup_dest_dir) = Attrib.config_string "sos_dest_dir" (K "") |
|
28 |
|
29 fun filename dir name = |
|
30 let |
|
31 val probfile = Path.basic (name ^ serial_string ()) |
|
32 val dir_path = Path.explode dir |
|
33 in |
|
34 if dir = "" then |
|
35 File.tmp_path probfile |
|
36 else if File.exists dir_path then |
|
37 Path.append dir_path probfile |
|
38 else error ("No such directory: " ^ dir) |
|
39 end |
|
40 |
|
41 fun run_solver ctxt name cmd find_failure input = |
|
42 let |
|
43 val _ = warning ("Calling solver: " ^ name) |
|
44 |
|
45 (* create input file *) |
|
46 val dir = Config.get ctxt dest_dir |
|
47 val input_file = filename dir "sos_in" |
|
48 val _ = File.write input_file input |
|
49 |
|
50 (* call solver *) |
|
51 val output_file = filename dir "sos_out" |
|
52 val (output, rv) = |
|
53 bash_output |
|
54 (if File.exists cmd then |
|
55 space_implode " " |
|
56 [File.shell_path cmd, File.shell_path input_file, File.shell_path output_file] |
|
57 else error ("Bad executable: " ^ File.platform_path cmd)) |
|
58 |
|
59 (* read and analyze output *) |
|
60 val (res, res_msg) = find_failure rv |
|
61 val result = if File.exists output_file then File.read output_file else "" |
|
62 |
|
63 (* remove temporary files *) |
|
64 val _ = |
|
65 if dir = "" then |
|
66 (File.rm input_file; if File.exists output_file then File.rm output_file else ()) |
|
67 else () |
|
68 |
|
69 val _ = |
|
70 if Config.get ctxt Sum_Of_Squares.trace |
|
71 then writeln ("Solver output:\n" ^ output) |
|
72 else () |
|
73 |
|
74 val _ = warning (str_of_result res ^ ": " ^ res_msg) |
|
75 in |
|
76 (case res of |
|
77 Success => result |
|
78 | Failure => raise Sum_Of_Squares.Failure res_msg |
|
79 | Error => error ("Prover failed: " ^ res_msg)) |
|
80 end |
|
81 |
|
82 |
|
83 (*** various provers ***) |
|
84 |
|
85 (* local csdp client *) |
|
86 |
|
87 fun find_csdp_failure rv = |
|
88 case rv of |
|
89 0 => (Success, "SDP solved") |
|
90 | 1 => (Failure, "SDP is primal infeasible") |
|
91 | 2 => (Failure, "SDP is dual infeasible") |
|
92 | 3 => (Success, "SDP solved with reduced accuracy") |
|
93 | 4 => (Failure, "Maximum iterations reached") |
|
94 | 5 => (Failure, "Stuck at edge of primal feasibility") |
|
95 | 6 => (Failure, "Stuck at edge of dual infeasibility") |
|
96 | 7 => (Failure, "Lack of progress") |
|
97 | 8 => (Failure, "X, Z, or O was singular") |
|
98 | 9 => (Failure, "Detected NaN or Inf values") |
|
99 | _ => (Error, "return code is " ^ string_of_int rv) |
|
100 |
|
101 val csdp = ("$CSDP_EXE", find_csdp_failure) |
|
102 |
|
103 |
|
104 (* remote neos server *) |
|
105 |
|
106 fun find_neos_failure rv = |
|
107 case rv of |
|
108 20 => (Error, "error submitting job") |
|
109 | 21 => (Error, "interrupt") |
|
110 | _ => find_csdp_failure rv |
|
111 |
|
112 val neos_csdp = ("$ISABELLE_SUM_OF_SQUARES/neos_csdp_client", find_neos_failure) |
|
113 |
|
114 |
|
115 (* named provers *) |
|
116 |
|
117 fun prover "remote_csdp" = neos_csdp |
|
118 | prover "csdp" = csdp |
|
119 | prover name = error ("Unknown prover: " ^ name) |
|
120 |
|
121 val (prover_name, setup_prover_name) = Attrib.config_string "sos_prover_name" (K "remote_csdp") |
|
122 |
|
123 fun call_solver ctxt opt_name = |
|
124 let |
|
125 val name = the_default (Config.get ctxt prover_name) opt_name |
|
126 val (cmd, find_failure) = prover name |
|
127 in run_solver ctxt name (Path.explode cmd) find_failure end |
|
128 |
|
129 |
|
130 (* certificate output *) |
|
131 |
|
132 fun output_line cert = |
|
133 "To repeat this proof with a certifiate use this command:\n" ^ |
|
134 Markup.markup Markup.sendback ("by (sos_cert \"" ^ cert ^ "\")") |
|
135 |
|
136 val print_cert = warning o output_line o PositivstellensatzTools.pss_tree_to_cert |
|
137 |
|
138 |
|
139 (* method setup *) |
|
140 |
|
141 fun sos_solver print method = SIMPLE_METHOD' o Sum_Of_Squares.sos_tac print method |
|
142 |
|
143 val setup = |
|
144 setup_dest_dir #> |
|
145 setup_prover_name #> |
|
146 Method.setup @{binding sos} |
|
147 (Scan.lift (Scan.option Parse.xname) |
|
148 >> (fn opt_name => fn ctxt => |
|
149 sos_solver print_cert |
|
150 (Sum_Of_Squares.Prover (call_solver ctxt opt_name)) ctxt)) |
|
151 "prove universal problems over the reals using sums of squares" #> |
|
152 Method.setup @{binding sos_cert} |
|
153 (Scan.lift Parse.string |
|
154 >> (fn cert => fn ctxt => |
|
155 sos_solver ignore |
|
156 (Sum_Of_Squares.Certificate (PositivstellensatzTools.cert_to_pss_tree ctxt cert)) ctxt)) |
|
157 "prove universal problems over the reals using sums of squares with certificates" |
|
158 |
|
159 end |
|