author | wenzelm |
Thu, 22 Nov 2012 13:21:02 +0100 | |
changeset 50163 | c62ce309dc26 |
parent 45666 | d83797ef0d2d |
child 50450 | 358b6020f8b6 |
permissions | -rw-r--r-- |
41474 | 1 |
(* Title: HOL/Library/Sum_of_Squares/sos_wrapper.ML |
32949
aa6c470a962a
eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents:
32944
diff
changeset
|
2 |
Author: Philipp Meyer, TU Muenchen |
32268
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff
changeset
|
3 |
|
32949
aa6c470a962a
eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents:
32944
diff
changeset
|
4 |
Added functionality for sums of squares, e.g. calling a remote prover. |
32268
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff
changeset
|
5 |
*) |
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff
changeset
|
6 |
|
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff
changeset
|
7 |
signature SOS_WRAPPER = |
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff
changeset
|
8 |
sig |
32332 | 9 |
datatype prover_result = Success | Failure | Error |
32268
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff
changeset
|
10 |
val setup: theory -> theory |
38805 | 11 |
val dest_dir: string Config.T |
12 |
val prover_name: string Config.T |
|
32268
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff
changeset
|
13 |
end |
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff
changeset
|
14 |
|
32949
aa6c470a962a
eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents:
32944
diff
changeset
|
15 |
structure SOS_Wrapper: SOS_WRAPPER = |
32268
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff
changeset
|
16 |
struct |
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff
changeset
|
17 |
|
32332 | 18 |
datatype prover_result = Success | Failure | Error |
32949
aa6c470a962a
eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents:
32944
diff
changeset
|
19 |
|
32332 | 20 |
fun str_of_result Success = "Success" |
21 |
| str_of_result Failure = "Failure" |
|
22 |
| str_of_result Error = "Error" |
|
32268
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff
changeset
|
23 |
|
32949
aa6c470a962a
eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents:
32944
diff
changeset
|
24 |
|
32268
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff
changeset
|
25 |
(*** calling provers ***) |
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff
changeset
|
26 |
|
42616
92715b528e78
added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
wenzelm
parents:
41950
diff
changeset
|
27 |
val dest_dir = Attrib.setup_config_string @{binding sos_dest_dir} (K "") |
32268
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff
changeset
|
28 |
|
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff
changeset
|
29 |
fun filename dir name = |
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff
changeset
|
30 |
let |
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff
changeset
|
31 |
val probfile = Path.basic (name ^ serial_string ()) |
32332 | 32 |
val dir_path = Path.explode dir |
32268
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff
changeset
|
33 |
in |
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff
changeset
|
34 |
if dir = "" then |
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff
changeset
|
35 |
File.tmp_path probfile |
32949
aa6c470a962a
eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents:
32944
diff
changeset
|
36 |
else if File.exists dir_path then |
aa6c470a962a
eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents:
32944
diff
changeset
|
37 |
Path.append dir_path probfile |
aa6c470a962a
eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents:
32944
diff
changeset
|
38 |
else error ("No such directory: " ^ dir) |
32268
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff
changeset
|
39 |
end |
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff
changeset
|
40 |
|
41950
134131d519c0
clarified ISABELLE_CSDP setting (formerly CSDP_EXE);
wenzelm
parents:
41474
diff
changeset
|
41 |
fun run_solver ctxt name exe find_failure input = |
32268
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff
changeset
|
42 |
let |
32949
aa6c470a962a
eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents:
32944
diff
changeset
|
43 |
val _ = warning ("Calling solver: " ^ name) |
32268
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff
changeset
|
44 |
|
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff
changeset
|
45 |
(* create input file *) |
38805 | 46 |
val dir = Config.get ctxt dest_dir |
32949
aa6c470a962a
eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents:
32944
diff
changeset
|
47 |
val input_file = filename dir "sos_in" |
32268
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff
changeset
|
48 |
val _ = File.write input_file input |
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff
changeset
|
49 |
|
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff
changeset
|
50 |
(* call solver *) |
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff
changeset
|
51 |
val output_file = filename dir "sos_out" |
35010
d6e492cea6e4
renamed system/system_out to bash/bash_output -- to emphasized that this is really GNU bash, not some undefined POSIX sh;
wenzelm
parents:
32949
diff
changeset
|
52 |
val (output, rv) = |
43850
7f2cbc713344
moved bash operations to Isabelle_System (cf. Scala version);
wenzelm
parents:
42616
diff
changeset
|
53 |
Isabelle_System.bash_output |
41950
134131d519c0
clarified ISABELLE_CSDP setting (formerly CSDP_EXE);
wenzelm
parents:
41474
diff
changeset
|
54 |
(if File.exists exe then |
134131d519c0
clarified ISABELLE_CSDP setting (formerly CSDP_EXE);
wenzelm
parents:
41474
diff
changeset
|
55 |
space_implode " " (map File.shell_path [exe, input_file, output_file]) |
134131d519c0
clarified ISABELLE_CSDP setting (formerly CSDP_EXE);
wenzelm
parents:
41474
diff
changeset
|
56 |
else error ("Bad executable: " ^ File.platform_path exe)) |
32949
aa6c470a962a
eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents:
32944
diff
changeset
|
57 |
|
aa6c470a962a
eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents:
32944
diff
changeset
|
58 |
(* read and analyze output *) |
32332 | 59 |
val (res, res_msg) = find_failure rv |
60 |
val result = if File.exists output_file then File.read output_file else "" |
|
32268
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff
changeset
|
61 |
|
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff
changeset
|
62 |
(* remove temporary files *) |
32949
aa6c470a962a
eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents:
32944
diff
changeset
|
63 |
val _ = |
aa6c470a962a
eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents:
32944
diff
changeset
|
64 |
if dir = "" then |
aa6c470a962a
eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents:
32944
diff
changeset
|
65 |
(File.rm input_file; if File.exists output_file then File.rm output_file else ()) |
aa6c470a962a
eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents:
32944
diff
changeset
|
66 |
else () |
32268
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff
changeset
|
67 |
|
38805 | 68 |
val _ = |
41474 | 69 |
if Config.get ctxt Sum_of_Squares.trace |
38805 | 70 |
then writeln ("Solver output:\n" ^ output) |
71 |
else () |
|
32268
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff
changeset
|
72 |
|
32949
aa6c470a962a
eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents:
32944
diff
changeset
|
73 |
val _ = warning (str_of_result res ^ ": " ^ res_msg) |
32268
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff
changeset
|
74 |
in |
32949
aa6c470a962a
eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents:
32944
diff
changeset
|
75 |
(case res of |
32332 | 76 |
Success => result |
41474 | 77 |
| Failure => raise Sum_of_Squares.Failure res_msg |
32949
aa6c470a962a
eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents:
32944
diff
changeset
|
78 |
| Error => error ("Prover failed: " ^ res_msg)) |
32268
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff
changeset
|
79 |
end |
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff
changeset
|
80 |
|
32949
aa6c470a962a
eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents:
32944
diff
changeset
|
81 |
|
32268
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff
changeset
|
82 |
(*** various provers ***) |
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff
changeset
|
83 |
|
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff
changeset
|
84 |
(* local csdp client *) |
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff
changeset
|
85 |
|
32332 | 86 |
fun find_csdp_failure rv = |
32268
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff
changeset
|
87 |
case rv of |
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff
changeset
|
88 |
0 => (Success, "SDP solved") |
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff
changeset
|
89 |
| 1 => (Failure, "SDP is primal infeasible") |
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff
changeset
|
90 |
| 2 => (Failure, "SDP is dual infeasible") |
32332 | 91 |
| 3 => (Success, "SDP solved with reduced accuracy") |
92 |
| 4 => (Failure, "Maximum iterations reached") |
|
93 |
| 5 => (Failure, "Stuck at edge of primal feasibility") |
|
94 |
| 6 => (Failure, "Stuck at edge of dual infeasibility") |
|
95 |
| 7 => (Failure, "Lack of progress") |
|
96 |
| 8 => (Failure, "X, Z, or O was singular") |
|
97 |
| 9 => (Failure, "Detected NaN or Inf values") |
|
98 |
| _ => (Error, "return code is " ^ string_of_int rv) |
|
32268
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff
changeset
|
99 |
|
41950
134131d519c0
clarified ISABELLE_CSDP setting (formerly CSDP_EXE);
wenzelm
parents:
41474
diff
changeset
|
100 |
val csdp = (Path.explode "$ISABELLE_CSDP", find_csdp_failure) |
32268
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff
changeset
|
101 |
|
32949
aa6c470a962a
eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents:
32944
diff
changeset
|
102 |
|
32268
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff
changeset
|
103 |
(* remote neos server *) |
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff
changeset
|
104 |
|
32332 | 105 |
fun find_neos_failure rv = |
106 |
case rv of |
|
107 |
20 => (Error, "error submitting job") |
|
32362 | 108 |
| 21 => (Error, "interrupt") |
32332 | 109 |
| _ => find_csdp_failure rv |
32268
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff
changeset
|
110 |
|
41950
134131d519c0
clarified ISABELLE_CSDP setting (formerly CSDP_EXE);
wenzelm
parents:
41474
diff
changeset
|
111 |
val neos_csdp = (Path.explode "$ISABELLE_SUM_OF_SQUARES/neos_csdp_client", find_neos_failure) |
32268
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff
changeset
|
112 |
|
32949
aa6c470a962a
eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents:
32944
diff
changeset
|
113 |
|
aa6c470a962a
eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents:
32944
diff
changeset
|
114 |
(* named provers *) |
aa6c470a962a
eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents:
32944
diff
changeset
|
115 |
|
aa6c470a962a
eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents:
32944
diff
changeset
|
116 |
fun prover "remote_csdp" = neos_csdp |
aa6c470a962a
eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents:
32944
diff
changeset
|
117 |
| prover "csdp" = csdp |
aa6c470a962a
eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents:
32944
diff
changeset
|
118 |
| prover name = error ("Unknown prover: " ^ name) |
32363
a0ea6cd47724
SOS: function to set default prover; output channel changed
Philipp Meyer
parents:
32362
diff
changeset
|
119 |
|
42616
92715b528e78
added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
wenzelm
parents:
41950
diff
changeset
|
120 |
val prover_name = Attrib.setup_config_string @{binding sos_prover_name} (K "remote_csdp") |
32363
a0ea6cd47724
SOS: function to set default prover; output channel changed
Philipp Meyer
parents:
32362
diff
changeset
|
121 |
|
38805 | 122 |
fun call_solver ctxt opt_name = |
32949
aa6c470a962a
eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents:
32944
diff
changeset
|
123 |
let |
38805 | 124 |
val name = the_default (Config.get ctxt prover_name) opt_name |
41950
134131d519c0
clarified ISABELLE_CSDP setting (formerly CSDP_EXE);
wenzelm
parents:
41474
diff
changeset
|
125 |
val (exe, find_failure) = prover name |
134131d519c0
clarified ISABELLE_CSDP setting (formerly CSDP_EXE);
wenzelm
parents:
41474
diff
changeset
|
126 |
in run_solver ctxt name exe find_failure end |
32268
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff
changeset
|
127 |
|
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff
changeset
|
128 |
|
32645
1cc5b24f5a01
sos method generates and uses proof certificates
Philipp Meyer
parents:
32363
diff
changeset
|
129 |
(* certificate output *) |
1cc5b24f5a01
sos method generates and uses proof certificates
Philipp Meyer
parents:
32363
diff
changeset
|
130 |
|
32949
aa6c470a962a
eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents:
32944
diff
changeset
|
131 |
fun output_line cert = |
aa6c470a962a
eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents:
32944
diff
changeset
|
132 |
"To repeat this proof with a certifiate use this command:\n" ^ |
50163
c62ce309dc26
more abstract Sendback operations, with explicit id/exec_id properties;
wenzelm
parents:
45666
diff
changeset
|
133 |
Sendback.markup ("by (sos_cert \"" ^ cert ^ "\")") |
32268
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff
changeset
|
134 |
|
32949
aa6c470a962a
eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents:
32944
diff
changeset
|
135 |
val print_cert = warning o output_line o PositivstellensatzTools.pss_tree_to_cert |
32645
1cc5b24f5a01
sos method generates and uses proof certificates
Philipp Meyer
parents:
32363
diff
changeset
|
136 |
|
32268
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff
changeset
|
137 |
|
32949
aa6c470a962a
eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents:
32944
diff
changeset
|
138 |
(* method setup *) |
32268
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff
changeset
|
139 |
|
41474 | 140 |
fun sos_solver print method = SIMPLE_METHOD' o Sum_of_Squares.sos_tac print method |
32645
1cc5b24f5a01
sos method generates and uses proof certificates
Philipp Meyer
parents:
32363
diff
changeset
|
141 |
|
1cc5b24f5a01
sos method generates and uses proof certificates
Philipp Meyer
parents:
32363
diff
changeset
|
142 |
val setup = |
32949
aa6c470a962a
eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents:
32944
diff
changeset
|
143 |
Method.setup @{binding sos} |
36960
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
35010
diff
changeset
|
144 |
(Scan.lift (Scan.option Parse.xname) |
38805 | 145 |
>> (fn opt_name => fn ctxt => |
146 |
sos_solver print_cert |
|
41474 | 147 |
(Sum_of_Squares.Prover (call_solver ctxt opt_name)) ctxt)) |
32949
aa6c470a962a
eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents:
32944
diff
changeset
|
148 |
"prove universal problems over the reals using sums of squares" #> |
aa6c470a962a
eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents:
32944
diff
changeset
|
149 |
Method.setup @{binding sos_cert} |
36960
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
35010
diff
changeset
|
150 |
(Scan.lift Parse.string |
32949
aa6c470a962a
eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents:
32944
diff
changeset
|
151 |
>> (fn cert => fn ctxt => |
aa6c470a962a
eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents:
32944
diff
changeset
|
152 |
sos_solver ignore |
41474 | 153 |
(Sum_of_Squares.Certificate (PositivstellensatzTools.cert_to_pss_tree ctxt cert)) ctxt)) |
32949
aa6c470a962a
eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents:
32944
diff
changeset
|
154 |
"prove universal problems over the reals using sums of squares with certificates" |
32268
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff
changeset
|
155 |
|
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff
changeset
|
156 |
end |