author  Philipp Meyer 
Mon, 10 Aug 2009 13:53:42 +0200  
changeset 32363  a0ea6cd47724 
parent 32362  c0c640d86b4e 
child 32645  1cc5b24f5a01 
permissions  rwrr 
32268
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff
changeset

1 
(* Title: sos_wrapper.ML 
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff
changeset

2 
Author: Philipp Meyer, TU Muenchen 
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff
changeset

3 

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

4 
Added functionality for sums of squares, e.g. calling a remote prover 
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 
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff
changeset

9 

32332  10 
datatype prover_result = Success  Failure  Error 
32268
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff
changeset

11 

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

12 
val setup: theory > theory 
32332  13 
val destdir: string ref 
32363
a0ea6cd47724
SOS: function to set default prover; output channel changed
Philipp Meyer
parents:
32362
diff
changeset

14 
val get_prover_name: unit > string 
a0ea6cd47724
SOS: function to set default prover; output channel changed
Philipp Meyer
parents:
32362
diff
changeset

15 
val set_prover_name: string > unit 
32268
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff
changeset

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

17 

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

18 
structure SosWrapper : SOS_WRAPPER= 
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff
changeset

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

20 

32332  21 
datatype prover_result = Success  Failure  Error 
22 
fun str_of_result Success = "Success" 

23 
 str_of_result Failure = "Failure" 

24 
 str_of_result Error = "Error" 

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

25 

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

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

27 

32332  28 
fun debug s = if ! Sos.debugging then Output.writeln s else () 
32363
a0ea6cd47724
SOS: function to set default prover; output channel changed
Philipp Meyer
parents:
32362
diff
changeset

29 
val write = Output.warning 
32268
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff
changeset

30 

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

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

32 

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

33 
val destdir = ref "" 
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff
changeset

34 

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

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

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

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

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

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

41 
File.tmp_path probfile 
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff
changeset

42 
else 
32332  43 
if File.exists dir_path then 
44 
Path.append dir_path probfile 

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

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

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

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

48 

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

50 
let 
32332  51 
val _ = write ("Calling solver: " ^ name) 
32268
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff
changeset

52 

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

53 
(* create input file *) 
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff
changeset

54 
val dir = ! destdir 
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff
changeset

55 
val input_file = filename dir "sos_in" 
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff
changeset

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

57 

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

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

59 
val output_file = filename dir "sos_out" 
32332  60 
val (output, rv) = system_out ( 
61 
if File.exists cmd then space_implode " " 

62 
[File.shell_path cmd, File.platform_path input_file, File.platform_path output_file] 

63 
else error ("Bad executable: " ^ File.shell_path cmd)) 

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

64 

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

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

68 

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

69 
(* remove temporary files *) 
32332  70 
val _ = if dir = "" then 
71 
(File.rm input_file ; if File.exists output_file then File.rm output_file else ()) 

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 

32332  76 
val _ = write (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 
32332  78 
case res of 
79 
Success => result 

80 
 Failure => raise Sos.Failure res_msg 

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 

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

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

85 

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

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

87 

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

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

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

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

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

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

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

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

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

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

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

101 

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

103 

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

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

105 

32332  106 
fun find_neos_failure rv = 
107 
case rv of 

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

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

111 

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

113 

32363
a0ea6cd47724
SOS: function to set default prover; output channel changed
Philipp Meyer
parents:
32362
diff
changeset

114 
(* default prover *) 
a0ea6cd47724
SOS: function to set default prover; output channel changed
Philipp Meyer
parents:
32362
diff
changeset

115 

a0ea6cd47724
SOS: function to set default prover; output channel changed
Philipp Meyer
parents:
32362
diff
changeset

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

117 

a0ea6cd47724
SOS: function to set default prover; output channel changed
Philipp Meyer
parents:
32362
diff
changeset

118 
fun get_prover_name () = CRITICAL (fn () => ! prover_name); 
a0ea6cd47724
SOS: function to set default prover; output channel changed
Philipp Meyer
parents:
32362
diff
changeset

119 
fun set_prover_name str = CRITICAL (fn () => prover_name := str); 
a0ea6cd47724
SOS: function to set default prover; output channel changed
Philipp Meyer
parents:
32362
diff
changeset

120 

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

121 
(* save provers in table *) 
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff
changeset

122 

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

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

124 
Symtab.make [("remote_csdp", neos_csdp),("csdp", csdp)] 
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff
changeset

125 

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

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

127 
case Symtab.lookup provers name of 
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff
changeset

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

129 
 NONE => error ("unknown prover: " ^ name) 
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff
changeset

130 

32363
a0ea6cd47724
SOS: function to set default prover; output channel changed
Philipp Meyer
parents:
32362
diff
changeset

131 
fun call_solver name_option = 
32332  132 
let 
32363
a0ea6cd47724
SOS: function to set default prover; output channel changed
Philipp Meyer
parents:
32362
diff
changeset

133 
val name = the_default (get_prover_name()) name_option 
32332  134 
val (cmd, find_failure) = get_prover name 
135 
in 

136 
run_solver name (Path.explode cmd) find_failure 

137 
end 

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

138 

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

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

140 

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

141 
fun sos_solver name = (SIMPLE_METHOD' o (Sos.sos_tac (call_solver name))) 
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff
changeset

142 

32363
a0ea6cd47724
SOS: function to set default prover; output channel changed
Philipp Meyer
parents:
32362
diff
changeset

143 
val sos_method = Scan.option (Scan.lift OuterParse.xname) >> sos_solver 
32268
d50f0cb67578
Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff
changeset

144 

32332  145 
val setup = Method.setup @{binding sos} sos_method 
146 
"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

147 

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

148 
end 