author  wenzelm 
Wed, 08 Oct 2014 11:09:17 +0200  
changeset 58630  71cdb885b3bb 
parent 58629  a6a6cd499d4e 
child 58631  41333b45bff9 
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 

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

32949
aa6c470a962a
eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents:
32944
diff
changeset

21 

58630  22 
fun filename name = 
23 
File.tmp_path (Path.basic (name ^ serial_string ())) 

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

24 

58630  25 
fun find_failure rv = 
26 
case rv of 

27 
0 => (Success, "SDP solved") 

28 
 1 => (Failure, "SDP is primal infeasible") 

29 
 2 => (Failure, "SDP is dual infeasible") 

30 
 3 => (Success, "SDP solved with reduced accuracy") 

31 
 4 => (Failure, "Maximum iterations reached") 

32 
 5 => (Failure, "Stuck at edge of primal feasibility") 

33 
 6 => (Failure, "Stuck at edge of dual infeasibility") 

34 
 7 => (Failure, "Lack of progress") 

35 
 8 => (Failure, "X, Z, or O was singular") 

36 
 9 => (Failure, "Detected NaN or Inf values") 

37 
 _ => (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

38 

58630  39 
val exe = Path.explode "$ISABELLE_CSDP" 
40 

41 
fun run_solver ctxt input = 

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

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

43 
(* create input file *) 
58630  44 
val input_file = filename "sos_in" 
32268
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff
changeset

45 
val _ = File.write input_file input 
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff
changeset

46 

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

47 
(* call solver *) 
58630  48 
val output_file = filename "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

49 
val (output, rv) = 
43850
7f2cbc713344
moved bash operations to Isabelle_System (cf. Scala version);
wenzelm
parents:
42616
diff
changeset

50 
Isabelle_System.bash_output 
41950
134131d519c0
clarified ISABELLE_CSDP setting (formerly CSDP_EXE);
wenzelm
parents:
41474
diff
changeset

51 
(if File.exists exe then 
134131d519c0
clarified ISABELLE_CSDP setting (formerly CSDP_EXE);
wenzelm
parents:
41474
diff
changeset

52 
space_implode " " (map File.shell_path [exe, input_file, output_file]) 
134131d519c0
clarified ISABELLE_CSDP setting (formerly CSDP_EXE);
wenzelm
parents:
41474
diff
changeset

53 
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

54 

aa6c470a962a
eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents:
32944
diff
changeset

55 
(* read and analyze output *) 
32332  56 
val (res, res_msg) = find_failure rv 
57 
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

58 

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

59 
(* remove temporary files *) 
58630  60 
val _ = File.rm input_file 
61 
val _ = if File.exists output_file then File.rm output_file else () 

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

62 

38805  63 
val _ = 
41474  64 
if Config.get ctxt Sum_of_Squares.trace 
38805  65 
then writeln ("Solver output:\n" ^ output) 
66 
else () 

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

67 

32949
aa6c470a962a
eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents:
32944
diff
changeset

68 
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

69 
in 
32949
aa6c470a962a
eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents:
32944
diff
changeset

70 
(case res of 
32332  71 
Success => result 
41474  72 
 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

73 
 Error => error ("Prover failed: " ^ res_msg)) 
32268
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff
changeset

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

75 

32949
aa6c470a962a
eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents:
32944
diff
changeset

76 

aa6c470a962a
eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents:
32944
diff
changeset

77 
(* method setup *) 
32268
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff
changeset

78 

58630  79 
fun print_cert cert = 
80 
warning 

81 
("To repeat this proof with a certificate use this proof method:\n" ^ 

82 
Active.sendback_markup [] ("(sos \"" ^ Positivstellensatz_Tools.print_cert cert ^ "\")")) 

83 

84 
fun sos_tac ctxt NONE = 

85 
Sum_of_Squares.sos_tac print_cert 

86 
(Sum_of_Squares.Prover (run_solver ctxt)) ctxt 

87 
 sos_tac ctxt (SOME cert) = 

88 
Sum_of_Squares.sos_tac ignore 

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

90 

58418  91 
val _ = Theory.setup 
92 
(Method.setup @{binding sos} 

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

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

96 

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

97 
end 