author  wenzelm 
Wed, 08 Mar 2017 10:50:59 +0100  
changeset 65151  a7394aa4d21c 
parent 63518  ae8fd6fe63a1 
child 69593  3dda49e08b9d 
permissions  rwrr 
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 

62549
9498623b27f0
File.bash_string operations in ML as in Scala  exclusively for GNU bash, not perl and not user output;
wenzelm
parents:
59184
diff
changeset

43 
("\"$ISABELLE_CSDP\" " ^ File.bash_path in_path ^ " " ^ File.bash_path out_path) 
58631  44 
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

45 

58631  46 
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

47 

58631  48 
val (res, res_msg) = get_result rc 
49 
val _ = Sum_of_Squares.trace_message ctxt (fn () => str_of_result res ^ ": " ^ res_msg) 

50 
in 

51 
(case res of 

52 
Success => result 

53 
 Failure => raise Sum_of_Squares.Failure res_msg 

54 
 Error => error ("Prover failed: " ^ res_msg)) 

55 
end)) 

32268
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff
changeset

56 

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 
(* method setup *) 
32268
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff
changeset

59 

58630  60 
fun print_cert cert = 
59184
830bb7ddb3ab
explicit message channels for "state", "information";
wenzelm
parents:
58631
diff
changeset

61 
Output.information 
58631  62 
("To repeat this proof with a certificate use this command:\n" ^ 
63518  63 
Active.sendback_markup_command 
63507  64 
("by (sos \"" ^ Positivstellensatz_Tools.print_cert cert ^ "\")")) 
58630  65 

66 
fun sos_tac ctxt NONE = 

67 
Sum_of_Squares.sos_tac print_cert 

68 
(Sum_of_Squares.Prover (run_solver ctxt)) ctxt 

69 
 sos_tac ctxt (SOME cert) = 

70 
Sum_of_Squares.sos_tac ignore 

71 
(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

72 

58418  73 
val _ = Theory.setup 
74 
(Method.setup @{binding sos} 

58630  75 
(Scan.lift (Scan.option Parse.string) 
76 
>> (fn arg => fn ctxt => SIMPLE_METHOD' (sos_tac ctxt arg))) 

77 
"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

78 

d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff
changeset

79 
end 