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