author  wenzelm 
Sat, 06 Feb 2010 14:50:55 +0100  
changeset 35010  d6e492cea6e4 
parent 32949  aa6c470a962a 
child 36960  01594f816e3a 
permissions  rwrr 
32949
aa6c470a962a
eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents:
32944
diff
changeset

1 
(* Title: HOL/Library/Sum_Of_Squares/sos_wrapper.ML 
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 
32740  11 
val destdir: string Unsynchronized.ref 
32949
aa6c470a962a
eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents:
32944
diff
changeset

12 
val prover_name: string Unsynchronized.ref 
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 
(*** output control ***) 
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff
changeset

26 

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

27 
fun debug s = if ! Sum_Of_Squares.debugging then writeln s else () 
aa6c470a962a
eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents:
32944
diff
changeset

28 

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

29 

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

30 
(*** calling provers ***) 
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff
changeset

31 

32740  32 
val destdir = Unsynchronized.ref "" 
32268
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff
changeset

33 

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

34 
fun filename dir name = 
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff
changeset

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

36 
val probfile = Path.basic (name ^ serial_string ()) 
32332  37 
val dir_path = Path.explode dir 
32268
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff
changeset

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

39 
if dir = "" then 
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff
changeset

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

41 
else if File.exists dir_path then 
aa6c470a962a
eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents:
32944
diff
changeset

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

43 
else error ("No such directory: " ^ dir) 
32268
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff
changeset

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

45 

32332  46 
fun run_solver name cmd find_failure input = 
32268
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff
changeset

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

48 
val _ = warning ("Calling solver: " ^ name) 
32268
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 
(* create input file *) 
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff
changeset

51 
val dir = ! destdir 
32949
aa6c470a962a
eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents:
32944
diff
changeset

52 
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

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

54 

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

55 
(* call solver *) 
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff
changeset

56 
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

57 
val (output, rv) = 
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

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

59 
(if File.exists cmd then 
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

60 
space_implode " " 
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

61 
[File.shell_path cmd, File.shell_path input_file, File.shell_path output_file] 
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

62 
else error ("Bad executable: " ^ File.platform_path cmd)) 
32949
aa6c470a962a
eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents:
32944
diff
changeset

63 

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

64 
(* read and analyze output *) 
32332  65 
val (res, res_msg) = find_failure rv 
66 
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

67 

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

68 
(* remove temporary files *) 
32949
aa6c470a962a
eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents:
32944
diff
changeset

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

70 
if dir = "" then 
aa6c470a962a
eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents:
32944
diff
changeset

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

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

73 

32332  74 
val _ = debug ("Solver output:\n" ^ output) 
32268
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 
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

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

78 
(case res of 
32332  79 
Success => result 
32949
aa6c470a962a
eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents:
32944
diff
changeset

80 
 Failure => raise Sum_Of_Squares.Failure res_msg 
aa6c470a962a
eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents:
32944
diff
changeset

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

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

83 

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

84 

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

85 
(*** various provers ***) 
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff
changeset

86 

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

87 
(* local csdp client *) 
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff
changeset

88 

32332  89 
fun find_csdp_failure rv = 
32268
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff
changeset

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

91 
0 => (Success, "SDP solved") 
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff
changeset

92 
 1 => (Failure, "SDP is primal infeasible") 
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff
changeset

93 
 2 => (Failure, "SDP is dual infeasible") 
32332  94 
 3 => (Success, "SDP solved with reduced accuracy") 
95 
 4 => (Failure, "Maximum iterations reached") 

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

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

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

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

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

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

102 

32332  103 
val csdp = ("$CSDP_EXE", find_csdp_failure) 
32268
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff
changeset

104 

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

105 

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

106 
(* remote neos server *) 
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff
changeset

107 

32332  108 
fun find_neos_failure rv = 
109 
case rv of 

110 
20 => (Error, "error submitting job") 

32362  111 
 21 => (Error, "interrupt") 
32332  112 
 _ => find_csdp_failure rv 
32268
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff
changeset

113 

32332  114 
val neos_csdp = ("$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

115 

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

116 

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

117 
(* named provers *) 
aa6c470a962a
eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents:
32944
diff
changeset

118 

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

119 
fun prover "remote_csdp" = neos_csdp 
aa6c470a962a
eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents:
32944
diff
changeset

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

121 
 prover name = error ("Unknown prover: " ^ name) 
32363
a0ea6cd47724
SOS: function to set default prover; output channel changed
Philipp Meyer
parents:
32362
diff
changeset

122 

32740  123 
val prover_name = Unsynchronized.ref "remote_csdp" 
32363
a0ea6cd47724
SOS: function to set default prover; output channel changed
Philipp Meyer
parents:
32362
diff
changeset

124 

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

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

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

127 
val name = the_default (! prover_name) opt_name 
aa6c470a962a
eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents:
32944
diff
changeset

128 
val (cmd, find_failure) = prover name 
aa6c470a962a
eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents:
32944
diff
changeset

129 
in run_solver name (Path.explode cmd) find_failure end 
32268
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff
changeset

130 

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

131 

32645
1cc5b24f5a01
sos method generates and uses proof certificates
Philipp Meyer
parents:
32363
diff
changeset

132 
(* certificate output *) 
1cc5b24f5a01
sos method generates and uses proof certificates
Philipp Meyer
parents:
32363
diff
changeset

133 

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

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

135 
"To repeat this proof with a certifiate use this command:\n" ^ 
aa6c470a962a
eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents:
32944
diff
changeset

136 
Markup.markup Markup.sendback ("by (sos_cert \"" ^ cert ^ "\")") 
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 
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

139 

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

140 

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

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

142 

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

143 
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

144 

1cc5b24f5a01
sos method generates and uses proof certificates
Philipp Meyer
parents:
32363
diff
changeset

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

146 
Method.setup @{binding sos} 
aa6c470a962a
eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents:
32944
diff
changeset

147 
(Scan.lift (Scan.option OuterParse.xname) 
aa6c470a962a
eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents:
32944
diff
changeset

148 
>> (sos_solver print_cert o Sum_Of_Squares.Prover o call_solver)) 
aa6c470a962a
eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents:
32944
diff
changeset

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

150 
Method.setup @{binding sos_cert} 
aa6c470a962a
eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents:
32944
diff
changeset

151 
(Scan.lift OuterParse.string 
aa6c470a962a
eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents:
32944
diff
changeset

152 
>> (fn cert => fn ctxt => 
aa6c470a962a
eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents:
32944
diff
changeset

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

154 
(Sum_Of_Squares.Certificate (PositivstellensatzTools.cert_to_pss_tree ctxt cert)) ctxt)) 
aa6c470a962a
eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents:
32944
diff
changeset

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

156 

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

157 
end 