src/HOL/Library/Sum_Of_Squares/sos_wrapper.ML
author wenzelm
Tue Sep 29 16:24:36 2009 +0200 (2009-09-29)
changeset 32740 9dd0a2f83429
parent 32646 962b4354ed90
child 32944 ecc0705174c2
permissions -rw-r--r--
explicit indication of Unsynchronized.ref;
     1 (* Title:      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 
    10   datatype prover_result = Success | Failure | Error
    11 
    12   val setup: theory -> theory
    13   val destdir: string Unsynchronized.ref
    14   val get_prover_name: unit -> string
    15   val set_prover_name: string -> unit
    16 end
    17 
    18 structure SosWrapper : SOS_WRAPPER=
    19 struct
    20 
    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"
    25 
    26 (*** output control ***)
    27 
    28 fun debug s = if ! Sos.debugging then Output.writeln s else ()
    29 val write = Output.warning
    30 
    31 (*** calling provers ***)
    32 
    33 val destdir = Unsynchronized.ref ""
    34 
    35 fun filename dir name =
    36   let
    37     val probfile = Path.basic (name ^ serial_string ())
    38     val dir_path = Path.explode dir
    39   in
    40     if dir = "" then
    41       File.tmp_path probfile
    42     else
    43       if File.exists dir_path then
    44         Path.append dir_path probfile
    45       else
    46         error ("No such directory: " ^ dir)
    47   end
    48 
    49 fun run_solver name cmd find_failure input =
    50   let
    51     val _ = write ("Calling solver: " ^ name)
    52 
    53     (* create input file *)
    54     val dir = ! destdir
    55     val input_file = filename dir "sos_in" 
    56     val _ = File.write input_file input
    57 
    58     (* call solver *)
    59     val output_file = filename dir "sos_out"
    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))
    64  
    65     (* read and analysize output *)
    66     val (res, res_msg) = find_failure rv
    67     val result = if File.exists output_file then File.read output_file else ""
    68 
    69     (* remove temporary files *)
    70     val _ = if dir = "" then
    71         (File.rm input_file ; if File.exists output_file then File.rm output_file else ())
    72         else ()
    73 
    74     val _ = debug ("Solver output:\n" ^ output)
    75 
    76     val _ = write (str_of_result res ^ ": " ^ res_msg)
    77   in
    78     case res of
    79       Success => result
    80     | Failure => raise Sos.Failure res_msg
    81     | Error => error ("Prover failed: " ^ res_msg)
    82   end
    83 
    84 (*** various provers ***)
    85 
    86 (* local csdp client *)
    87 
    88 fun find_csdp_failure rv =
    89   case rv of
    90     0 => (Success, "SDP solved")
    91   | 1 => (Failure, "SDP is primal infeasible")
    92   | 2 => (Failure, "SDP is dual infeasible")
    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)
   101 
   102 val csdp = ("$CSDP_EXE", find_csdp_failure)
   103 
   104 (* remote neos server *)
   105 
   106 fun find_neos_failure rv =
   107   case rv of
   108     20 => (Error, "error submitting job")
   109   | 21 => (Error, "interrupt")
   110   |  _ => find_csdp_failure rv
   111 
   112 val neos_csdp = ("$ISABELLE_SUM_OF_SQUARES/neos_csdp_client", find_neos_failure)
   113 
   114 (* default prover *)
   115 
   116 val prover_name = Unsynchronized.ref "remote_csdp"
   117 
   118 fun get_prover_name () = CRITICAL (fn () => ! prover_name);
   119 fun set_prover_name str = CRITICAL (fn () => prover_name := str);
   120 
   121 (* save provers in table *)
   122 
   123 val provers =
   124      Symtab.make [("remote_csdp", neos_csdp),("csdp", csdp)]
   125 
   126 fun get_prover name =
   127   case Symtab.lookup provers name of
   128     SOME prover => prover
   129   | NONE => error ("unknown prover: " ^ name)
   130 
   131 fun call_solver name_option =
   132   let
   133     val name = the_default (get_prover_name()) name_option
   134     val (cmd, find_failure) = get_prover name
   135   in
   136     run_solver name (Path.explode cmd) find_failure
   137   end
   138 
   139 (* certificate output *)
   140 
   141 fun output_line cert = "To repeat this proof with a certifiate use this command:\n" ^
   142         (Markup.markup Markup.sendback) ("by (sos_cert \"" ^ cert ^ "\")")
   143 
   144 val print_cert = Output.writeln o output_line o PositivstellensatzTools.pss_tree_to_cert
   145 
   146 (* setup tactic *)
   147 
   148 fun parse_cert (input as (ctxt, _)) = 
   149   (Scan.lift OuterParse.string >>
   150     PositivstellensatzTools.cert_to_pss_tree (Context.proof_of ctxt)) input
   151 
   152 fun sos_solver print method = (SIMPLE_METHOD' o (Sos.sos_tac print method)) 
   153 
   154 val sos_method =
   155    Scan.lift (Scan.option OuterParse.xname) >> (fn n => Sos.Prover (call_solver n)) >>
   156    sos_solver print_cert
   157 
   158 val sos_cert_method =
   159   parse_cert >> Sos.Certificate >> sos_solver ignore
   160 
   161 val setup =
   162      Method.setup @{binding sos} sos_method
   163      "Prove universal problems over the reals using sums of squares"
   164   #> Method.setup @{binding sos_cert} sos_cert_method
   165      "Prove universal problems over the reals using sums of squares with certificates"
   166 
   167 end