src/HOL/Library/Sum_of_Squares/sos_wrapper.ML
author wenzelm
Thu Jul 18 20:53:22 2013 +0200 (2013-07-18 ago)
changeset 52697 6fb98a20c349
parent 50450 358b6020f8b6
child 56625 54505623a8ef
permissions -rw-r--r--
explicit padding on command boundary for "auto" generated sendback -- do not replace the corresponding goal command, but append to it;
wenzelm@41474
     1
(*  Title:      HOL/Library/Sum_of_Squares/sos_wrapper.ML
wenzelm@32949
     2
    Author:     Philipp Meyer, TU Muenchen
Philipp@32268
     3
wenzelm@32949
     4
Added functionality for sums of squares, e.g. calling a remote prover.
Philipp@32268
     5
*)
Philipp@32268
     6
Philipp@32268
     7
signature SOS_WRAPPER =
Philipp@32268
     8
sig
wenzelm@32332
     9
  datatype prover_result = Success | Failure | Error
Philipp@32268
    10
  val setup: theory -> theory
wenzelm@38805
    11
  val dest_dir: string Config.T
wenzelm@38805
    12
  val prover_name: string Config.T
Philipp@32268
    13
end
Philipp@32268
    14
wenzelm@32949
    15
structure SOS_Wrapper: SOS_WRAPPER =
Philipp@32268
    16
struct
Philipp@32268
    17
wenzelm@32332
    18
datatype prover_result = Success | Failure | Error
wenzelm@32949
    19
wenzelm@32332
    20
fun str_of_result Success = "Success"
wenzelm@32332
    21
  | str_of_result Failure = "Failure"
wenzelm@32332
    22
  | str_of_result Error = "Error"
Philipp@32268
    23
wenzelm@32949
    24
Philipp@32268
    25
(*** calling provers ***)
Philipp@32268
    26
wenzelm@42616
    27
val dest_dir = Attrib.setup_config_string @{binding sos_dest_dir} (K "")
Philipp@32268
    28
Philipp@32268
    29
fun filename dir name =
Philipp@32268
    30
  let
Philipp@32268
    31
    val probfile = Path.basic (name ^ serial_string ())
wenzelm@32332
    32
    val dir_path = Path.explode dir
Philipp@32268
    33
  in
Philipp@32268
    34
    if dir = "" then
Philipp@32268
    35
      File.tmp_path probfile
wenzelm@32949
    36
    else if File.exists dir_path then
wenzelm@32949
    37
      Path.append dir_path probfile
wenzelm@32949
    38
    else error ("No such directory: " ^ dir)
Philipp@32268
    39
  end
Philipp@32268
    40
wenzelm@41950
    41
fun run_solver ctxt name exe find_failure input =
Philipp@32268
    42
  let
wenzelm@32949
    43
    val _ = warning ("Calling solver: " ^ name)
Philipp@32268
    44
Philipp@32268
    45
    (* create input file *)
wenzelm@38805
    46
    val dir = Config.get ctxt dest_dir
wenzelm@32949
    47
    val input_file = filename dir "sos_in"
Philipp@32268
    48
    val _ = File.write input_file input
Philipp@32268
    49
Philipp@32268
    50
    (* call solver *)
Philipp@32268
    51
    val output_file = filename dir "sos_out"
wenzelm@35010
    52
    val (output, rv) =
wenzelm@43850
    53
      Isabelle_System.bash_output
wenzelm@41950
    54
       (if File.exists exe then
wenzelm@41950
    55
          space_implode " " (map File.shell_path [exe, input_file, output_file])
wenzelm@41950
    56
        else error ("Bad executable: " ^ File.platform_path exe))
wenzelm@32949
    57
wenzelm@32949
    58
    (* read and analyze output *)
wenzelm@32332
    59
    val (res, res_msg) = find_failure rv
wenzelm@32332
    60
    val result = if File.exists output_file then File.read output_file else ""
Philipp@32268
    61
Philipp@32268
    62
    (* remove temporary files *)
wenzelm@32949
    63
    val _ =
wenzelm@32949
    64
      if dir = "" then
wenzelm@32949
    65
        (File.rm input_file; if File.exists output_file then File.rm output_file else ())
wenzelm@32949
    66
      else ()
Philipp@32268
    67
wenzelm@38805
    68
    val _ =
wenzelm@41474
    69
      if Config.get ctxt Sum_of_Squares.trace
wenzelm@38805
    70
      then writeln ("Solver output:\n" ^ output)
wenzelm@38805
    71
      else ()
Philipp@32268
    72
wenzelm@32949
    73
    val _ = warning (str_of_result res ^ ": " ^ res_msg)
Philipp@32268
    74
  in
wenzelm@32949
    75
    (case res of
wenzelm@32332
    76
      Success => result
wenzelm@41474
    77
    | Failure => raise Sum_of_Squares.Failure res_msg
wenzelm@32949
    78
    | Error => error ("Prover failed: " ^ res_msg))
Philipp@32268
    79
  end
Philipp@32268
    80
wenzelm@32949
    81
Philipp@32268
    82
(*** various provers ***)
Philipp@32268
    83
Philipp@32268
    84
(* local csdp client *)
Philipp@32268
    85
wenzelm@32332
    86
fun find_csdp_failure rv =
Philipp@32268
    87
  case rv of
Philipp@32268
    88
    0 => (Success, "SDP solved")
Philipp@32268
    89
  | 1 => (Failure, "SDP is primal infeasible")
Philipp@32268
    90
  | 2 => (Failure, "SDP is dual infeasible")
wenzelm@32332
    91
  | 3 => (Success, "SDP solved with reduced accuracy")
wenzelm@32332
    92
  | 4 => (Failure, "Maximum iterations reached")
wenzelm@32332
    93
  | 5 => (Failure, "Stuck at edge of primal feasibility")
wenzelm@32332
    94
  | 6 => (Failure, "Stuck at edge of dual infeasibility")
wenzelm@32332
    95
  | 7 => (Failure, "Lack of progress")
wenzelm@32332
    96
  | 8 => (Failure, "X, Z, or O was singular")
wenzelm@32332
    97
  | 9 => (Failure, "Detected NaN or Inf values")
wenzelm@32332
    98
  | _ => (Error, "return code is " ^ string_of_int rv)
Philipp@32268
    99
wenzelm@41950
   100
val csdp = (Path.explode "$ISABELLE_CSDP", find_csdp_failure)
Philipp@32268
   101
wenzelm@32949
   102
Philipp@32268
   103
(* remote neos server *)
Philipp@32268
   104
wenzelm@32332
   105
fun find_neos_failure rv =
wenzelm@32332
   106
  case rv of
wenzelm@32332
   107
    20 => (Error, "error submitting job")
Philipp@32362
   108
  | 21 => (Error, "interrupt")
wenzelm@32332
   109
  |  _ => find_csdp_failure rv
Philipp@32268
   110
wenzelm@41950
   111
val neos_csdp = (Path.explode "$ISABELLE_SUM_OF_SQUARES/neos_csdp_client", find_neos_failure)
Philipp@32268
   112
wenzelm@32949
   113
wenzelm@32949
   114
(* named provers *)
wenzelm@32949
   115
wenzelm@32949
   116
fun prover "remote_csdp" = neos_csdp
wenzelm@32949
   117
  | prover "csdp" = csdp
wenzelm@32949
   118
  | prover name = error ("Unknown prover: " ^ name)
Philipp@32363
   119
wenzelm@42616
   120
val prover_name = Attrib.setup_config_string @{binding sos_prover_name} (K "remote_csdp")
Philipp@32363
   121
wenzelm@38805
   122
fun call_solver ctxt opt_name =
wenzelm@32949
   123
  let
wenzelm@38805
   124
    val name = the_default (Config.get ctxt prover_name) opt_name
wenzelm@41950
   125
    val (exe, find_failure) = prover name
wenzelm@41950
   126
  in run_solver ctxt name exe find_failure end
Philipp@32268
   127
Philipp@32268
   128
Philipp@32645
   129
(* certificate output *)
Philipp@32645
   130
wenzelm@32949
   131
fun output_line cert =
wenzelm@32949
   132
  "To repeat this proof with a certifiate use this command:\n" ^
wenzelm@52697
   133
    Active.sendback_markup [] ("by (sos_cert \"" ^ cert ^ "\")")
Philipp@32268
   134
wenzelm@32949
   135
val print_cert = warning o output_line o PositivstellensatzTools.pss_tree_to_cert
Philipp@32645
   136
Philipp@32268
   137
wenzelm@32949
   138
(* method setup *)
Philipp@32268
   139
wenzelm@41474
   140
fun sos_solver print method = SIMPLE_METHOD' o Sum_of_Squares.sos_tac print method
Philipp@32645
   141
Philipp@32645
   142
val setup =
wenzelm@32949
   143
  Method.setup @{binding sos}
wenzelm@36960
   144
    (Scan.lift (Scan.option Parse.xname)
wenzelm@38805
   145
      >> (fn opt_name => fn ctxt =>
wenzelm@38805
   146
        sos_solver print_cert
wenzelm@41474
   147
          (Sum_of_Squares.Prover (call_solver ctxt opt_name)) ctxt))
wenzelm@32949
   148
    "prove universal problems over the reals using sums of squares" #>
wenzelm@32949
   149
  Method.setup @{binding sos_cert}
wenzelm@36960
   150
    (Scan.lift Parse.string
wenzelm@32949
   151
      >> (fn cert => fn ctxt =>
wenzelm@32949
   152
        sos_solver ignore
wenzelm@41474
   153
          (Sum_of_Squares.Certificate (PositivstellensatzTools.cert_to_pss_tree ctxt cert)) ctxt))
wenzelm@32949
   154
    "prove universal problems over the reals using sums of squares with certificates"
Philipp@32268
   155
Philipp@32268
   156
end