src/HOL/Library/sos_wrapper.ML
author Philipp Meyer
Fri, 24 Jul 2009 13:56:02 +0200
changeset 32268 d50f0cb67578
permissions -rw-r--r--
Functionality for sum of squares to call a remote csdp prover
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
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
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    10
  datatype prover_result = Success | PartialSuccess | Failure | Error
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    11
  type prover = string * (int -> string -> prover_result * string)
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    12
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    13
  val setup: theory -> theory
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    14
end
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    15
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    16
structure SosWrapper : SOS_WRAPPER=
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    17
struct
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    18
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    19
datatype prover_result = Success | PartialSuccess | Failure | Error
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    20
type prover =
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    21
  string *                           (* command name *)
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    22
  (int -> string ->prover_result * string)   (* function to find failure from return value and output *)
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    23
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    24
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
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    27
fun debug s = Output.debug (fn () => s)
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    28
val answer = Output.priority
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    29
val write = Output.writeln
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 ())
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
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    41
    else
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    42
      if File.exists (Path.explode dir) then
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    43
        Path.append  (Path.explode dir) probfile
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    44
      else
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    45
        error ("No such directory: " ^ dir)
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    46
  end
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    47
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    48
fun is_success Success = true
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    49
  | is_success PartialSuccess = true
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    50
  | is_success _ = false
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    51
fun str_of_status Success = "Success"
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    52
  | str_of_status PartialSuccess = "Partial Success"
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    53
  | str_of_status Failure= "Failure"
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    54
  | str_of_status Error= "Error"
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    55
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    56
fun run_solver name (cmd, find_failure) input =
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    57
  let
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    58
    val _ = answer ("Calling solver: " ^ name)
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    59
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    60
    (* create input file *)
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    61
    val dir = ! destdir
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    62
    val input_file = filename dir "sos_in" 
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    63
    val _ = File.write input_file input
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
    val _ = debug "Solver input:"
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    66
    val _ = debug input
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
    (* call solver *)
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    69
    val output_file = filename dir "sos_out"
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    70
    val (output, rv) = system_out (cmd ^ " " ^ (Path.implode input_file) ^
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    71
                         " " ^ (Path.implode output_file))
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    72
 
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    73
    (* read and analysize output *)
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    74
    val (res, res_msg) = find_failure rv output
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    75
    val result = if is_success res then File.read output_file else ""
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    76
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    77
    (* remove temporary files *)
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    78
    val _ = if dir = "" then (File.rm input_file ; if File.exists output_file then File.rm output_file else ()) else ()
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    79
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    80
    val _ = debug "Solver output:"
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    81
    val _ = debug output
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    82
    val _ = debug "Solver result:"
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    83
    val _ = debug result
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    84
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    85
    val _ = answer (str_of_status res ^ ": " ^ res_msg)
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
  in
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    88
    if is_success res then
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    89
      result
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    90
    else
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    91
      error ("Prover failed: " ^ res_msg)
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    92
  end
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    93
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    94
(*** various provers ***)
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    95
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    96
(* local csdp client *)
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    97
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    98
fun find_csdp_run_failure rv _ =
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    99
  case rv of
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
   100
    0 => (Success, "SDP solved")
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
   101
  | 1 => (Failure, "SDP is primal infeasible")
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
   102
  | 2 => (Failure, "SDP is dual infeasible")
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
   103
  | 3 => (PartialSuccess, "SDP solved with reduced accuracy")
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
   104
  | _ => (Failure, "return code is " ^ string_of_int rv)
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
   105
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
   106
val csdp = ("csdp", find_csdp_run_failure)
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
   107
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
   108
(* remote neos server *)
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
   109
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
   110
fun find_neos_failure rv output =
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
   111
  if rv = 2 then (Failure, "no solution") else
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
   112
  if rv <> 0 then (Error, "return code is " ^ string_of_int rv) else
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
   113
  let
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
   114
    fun find_success str =
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
   115
      if String.isPrefix "Success: " str then
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
   116
        SOME (Success, unprefix "Success: " str)
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
   117
      else if String.isPrefix "Partial Success: " str then
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
   118
        SOME (PartialSuccess, unprefix "Partial Success: " str)
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
   119
      else if String.isPrefix "Failure: " str then
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
   120
        SOME (Failure, unprefix "Failure: " str)
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
   121
      else
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
   122
        NONE 
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
   123
    val exit_line = get_first find_success (split_lines output)
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
   124
  in
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
   125
    case exit_line of
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
   126
      SOME (status, msg) =>
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
   127
        if String.isPrefix "SDP solved" msg then
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
   128
          (status, msg)
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
   129
        else (Failure, msg)
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
   130
    | NONE => (Failure, "no success")
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
   131
  end
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
   132
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
   133
val neos_csdp = ("$ISABELLE_HOME/lib/scripts/neos/NeosCSDPClient.py", find_neos_failure)
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
   134
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
   135
(* save provers in table *)
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
   136
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
   137
val provers =
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
   138
     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
   139
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
   140
fun get_prover name =
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
   141
  case Symtab.lookup provers name of
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
   142
    SOME prover => prover
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
   143
  | NONE => error ("unknown prover: " ^ name)
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
   144
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
   145
fun call_solver name =
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
   146
    run_solver name (get_prover name)
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
(* setup tactic *)
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
   149
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
   150
val def_solver = "remote_csdp"
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
   151
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
   152
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
   153
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
   154
val sos_method = Scan.optional (Scan.lift OuterParse.xname) def_solver >> sos_solver
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
   155
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
   156
val setup = Method.setup @{binding sos} sos_method "Prove universal problems over the reals using sums of squares"
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
   157
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
   158
end