author  wenzelm 
Wed, 08 Oct 2014 11:50:25 +0200  
changeset 58631  41333b45bff9 
parent 58630  71cdb885b3bb 
child 59184  830bb7ddb3ab 
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 

43 
("\"$ISABELLE_CSDP\" " ^ File.shell_path in_path ^ " " ^ File.shell_path out_path) 

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 = 
58631  61 
(writeln o Markup.markup Markup.information) 
62 
("To repeat this proof with a certificate use this command:\n" ^ 

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

58630  64 

65 
fun sos_tac ctxt NONE = 

66 
Sum_of_Squares.sos_tac print_cert 

67 
(Sum_of_Squares.Prover (run_solver ctxt)) ctxt 

68 
 sos_tac ctxt (SOME cert) = 

69 
Sum_of_Squares.sos_tac ignore 

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

71 

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

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

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

77 

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

78 
end 