author | wenzelm |
Sun, 20 Sep 2020 20:47:59 +0200 | |
changeset 72278 | 199dc903131b |
parent 71340 | 6d9dd5309b85 |
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 |
|
58631 | 4 |
Wrapper for "sos" proof method. |
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 |
58630 | 9 |
val sos_tac: Proof.context -> string option -> int -> tactic |
32268
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff
changeset
|
10 |
end |
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff
changeset
|
11 |
|
32949
aa6c470a962a
eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents:
32944
diff
changeset
|
12 |
structure SOS_Wrapper: SOS_WRAPPER = |
32268
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff
changeset
|
13 |
struct |
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff
changeset
|
14 |
|
32332 | 15 |
datatype prover_result = Success | Failure | Error |
32949
aa6c470a962a
eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents:
32944
diff
changeset
|
16 |
|
32332 | 17 |
fun str_of_result Success = "Success" |
18 |
| str_of_result Failure = "Failure" |
|
19 |
| str_of_result Error = "Error" |
|
32268
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff
changeset
|
20 |
|
58631 | 21 |
fun get_result rc = |
22 |
(case rc of |
|
58630 | 23 |
0 => (Success, "SDP solved") |
24 |
| 1 => (Failure, "SDP is primal infeasible") |
|
25 |
| 2 => (Failure, "SDP is dual infeasible") |
|
26 |
| 3 => (Success, "SDP solved with reduced accuracy") |
|
27 |
| 4 => (Failure, "Maximum iterations reached") |
|
28 |
| 5 => (Failure, "Stuck at edge of primal feasibility") |
|
29 |
| 6 => (Failure, "Stuck at edge of dual infeasibility") |
|
30 |
| 7 => (Failure, "Lack of progress") |
|
31 |
| 8 => (Failure, "X, Z, or O was singular") |
|
32 |
| 9 => (Failure, "Detected NaN or Inf values") |
|
58631 | 33 |
| _ => (Error, "return code is " ^ string_of_int rc)) |
58630 | 34 |
|
35 |
fun run_solver ctxt input = |
|
58631 | 36 |
Isabelle_System.with_tmp_file "sos_in" "" (fn in_path => |
37 |
Isabelle_System.with_tmp_file "sos_out" "" (fn out_path => |
|
38 |
let |
|
39 |
val _ = File.write in_path input |
|
32268
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff
changeset
|
40 |
|
58631 | 41 |
val (output, rc) = |
42 |
Isabelle_System.bash_output |
|
71340 | 43 |
("\"$ISABELLE_CSDP\" " ^ |
72278 | 44 |
File.bash_platform_path in_path ^ " " ^ |
45 |
File.bash_platform_path out_path); |
|
58631 | 46 |
val _ = Sum_of_Squares.debug_message ctxt (fn () => "Solver output:\n" ^ output) |
32268
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff
changeset
|
47 |
|
58631 | 48 |
val result = if File.exists out_path then File.read out_path else "" |
32268
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff
changeset
|
49 |
|
58631 | 50 |
val (res, res_msg) = get_result rc |
51 |
val _ = Sum_of_Squares.trace_message ctxt (fn () => str_of_result res ^ ": " ^ res_msg) |
|
52 |
in |
|
53 |
(case res of |
|
54 |
Success => result |
|
55 |
| Failure => raise Sum_of_Squares.Failure res_msg |
|
56 |
| Error => error ("Prover failed: " ^ res_msg)) |
|
57 |
end)) |
|
32268
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff
changeset
|
58 |
|
32949
aa6c470a962a
eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents:
32944
diff
changeset
|
59 |
|
aa6c470a962a
eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents:
32944
diff
changeset
|
60 |
(* method setup *) |
32268
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff
changeset
|
61 |
|
58630 | 62 |
fun print_cert cert = |
59184
830bb7ddb3ab
explicit message channels for "state", "information";
wenzelm
parents:
58631
diff
changeset
|
63 |
Output.information |
58631 | 64 |
("To repeat this proof with a certificate use this command:\n" ^ |
63518 | 65 |
Active.sendback_markup_command |
63507 | 66 |
("by (sos \"" ^ Positivstellensatz_Tools.print_cert cert ^ "\")")) |
58630 | 67 |
|
68 |
fun sos_tac ctxt NONE = |
|
69 |
Sum_of_Squares.sos_tac print_cert |
|
70 |
(Sum_of_Squares.Prover (run_solver ctxt)) ctxt |
|
71 |
| sos_tac ctxt (SOME cert) = |
|
72 |
Sum_of_Squares.sos_tac ignore |
|
73 |
(Sum_of_Squares.Certificate (Positivstellensatz_Tools.read_cert ctxt cert)) ctxt |
|
32645
1cc5b24f5a01
sos method generates and uses proof certificates
Philipp Meyer
parents:
32363
diff
changeset
|
74 |
|
58418 | 75 |
val _ = Theory.setup |
69593 | 76 |
(Method.setup \<^binding>\<open>sos\<close> |
58630 | 77 |
(Scan.lift (Scan.option Parse.string) |
78 |
>> (fn arg => fn ctxt => SIMPLE_METHOD' (sos_tac ctxt arg))) |
|
79 |
"prove universal problems over the reals using sums of squares") |
|
32268
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff
changeset
|
80 |
|
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff
changeset
|
81 |
end |