1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Library/Sum_Of_Squares/sos_wrapper.ML	Thu Aug 06 19:51:59 2009 +0200
     1.3 @@ -0,0 +1,140 @@
     1.4 +(* Title:      sos_wrapper.ML
     1.5 +   Author:     Philipp Meyer, TU Muenchen
     1.6 +
     1.7 +Added functionality for sums of squares, e.g. calling a remote prover
     1.8 +*)
     1.9 +
    1.10 +signature SOS_WRAPPER =
    1.11 +sig
    1.12 +
    1.13 +  datatype prover_result = Success | Failure | Error
    1.14 +
    1.15 +  val setup: theory -> theory
    1.16 +  val destdir: string ref
    1.17 +end
    1.18 +
    1.19 +structure SosWrapper : SOS_WRAPPER=
    1.20 +struct
    1.21 +
    1.22 +datatype prover_result = Success | Failure | Error
    1.23 +fun str_of_result Success = "Success"
    1.24 +  | str_of_result Failure = "Failure"
    1.25 +  | str_of_result Error = "Error"
    1.26 +
    1.27 +(*** output control ***)
    1.28 +
    1.29 +fun debug s = if ! Sos.debugging then Output.writeln s else ()
    1.30 +val write = Output.priority
    1.31 +
    1.32 +(*** calling provers ***)
    1.33 +
    1.34 +val destdir = ref ""
    1.35 +
    1.36 +fun filename dir name =
    1.37 +  let
    1.38 +    val probfile = Path.basic (name ^ serial_string ())
    1.39 +    val dir_path = Path.explode dir
    1.40 +  in
    1.41 +    if dir = "" then
    1.42 +      File.tmp_path probfile
    1.43 +    else
    1.44 +      if File.exists dir_path then
    1.45 +        Path.append dir_path probfile
    1.46 +      else
    1.47 +        error ("No such directory: " ^ dir)
    1.48 +  end
    1.49 +
    1.50 +fun run_solver name cmd find_failure input =
    1.51 +  let
    1.52 +    val _ = write ("Calling solver: " ^ name)
    1.53 +
    1.54 +    (* create input file *)
    1.55 +    val dir = ! destdir
    1.56 +    val input_file = filename dir "sos_in" 
    1.57 +    val _ = File.write input_file input
    1.58 +
    1.59 +    (* call solver *)
    1.60 +    val output_file = filename dir "sos_out"
    1.61 +    val (output, rv) = system_out (
    1.62 +      if File.exists cmd then space_implode " "
    1.63 +        [File.shell_path cmd, File.platform_path input_file, File.platform_path output_file]
    1.64 +      else error ("Bad executable: " ^ File.shell_path cmd))
    1.65 + 
    1.66 +    (* read and analysize output *)
    1.67 +    val (res, res_msg) = find_failure rv
    1.68 +    val result = if File.exists output_file then File.read output_file else ""
    1.69 +
    1.70 +    (* remove temporary files *)
    1.71 +    val _ = if dir = "" then
    1.72 +        (File.rm input_file ; if File.exists output_file then File.rm output_file else ())
    1.73 +        else ()
    1.74 +
    1.75 +    val _ = debug ("Solver output:\n" ^ output)
    1.76 +
    1.77 +    val _ = write (str_of_result res ^ ": " ^ res_msg)
    1.78 +  in
    1.79 +    case res of
    1.80 +      Success => result
    1.81 +    | Failure => raise Sos.Failure res_msg
    1.82 +    | Error => error ("Prover failed: " ^ res_msg)
    1.83 +  end
    1.84 +
    1.85 +(*** various provers ***)
    1.86 +
    1.87 +(* local csdp client *)
    1.88 +
    1.89 +fun find_csdp_failure rv =
    1.90 +  case rv of
    1.91 +    0 => (Success, "SDP solved")
    1.92 +  | 1 => (Failure, "SDP is primal infeasible")
    1.93 +  | 2 => (Failure, "SDP is dual infeasible")
    1.94 +  | 3 => (Success, "SDP solved with reduced accuracy")
    1.95 +  | 4 => (Failure, "Maximum iterations reached")
    1.96 +  | 5 => (Failure, "Stuck at edge of primal feasibility")
    1.97 +  | 6 => (Failure, "Stuck at edge of dual infeasibility")
    1.98 +  | 7 => (Failure, "Lack of progress")
    1.99 +  | 8 => (Failure, "X, Z, or O was singular")
   1.100 +  | 9 => (Failure, "Detected NaN or Inf values")
   1.101 +  | _ => (Error, "return code is " ^ string_of_int rv)
   1.102 +
   1.103 +val csdp = ("$CSDP_EXE", find_csdp_failure)
   1.104 +
   1.105 +(* remote neos server *)
   1.106 +
   1.107 +fun find_neos_failure rv =
   1.108 +  case rv of
   1.109 +    20 => (Error, "error submitting job")
   1.110 +  | 21 => (Error, "no solution")
   1.111 +  |  _ => find_csdp_failure rv
   1.112 +
   1.113 +val neos_csdp = ("$ISABELLE_SUM_OF_SQUARES/neos_csdp_client", find_neos_failure)
   1.114 +
   1.115 +(* save provers in table *)
   1.116 +
   1.117 +val provers =
   1.118 +     Symtab.make [("remote_csdp", neos_csdp),("csdp", csdp)]
   1.119 +
   1.120 +fun get_prover name =
   1.121 +  case Symtab.lookup provers name of
   1.122 +    SOME prover => prover
   1.123 +  | NONE => error ("unknown prover: " ^ name)
   1.124 +
   1.125 +fun call_solver name =
   1.126 +  let
   1.127 +    val (cmd, find_failure) = get_prover name
   1.128 +  in
   1.129 +    run_solver name (Path.explode cmd) find_failure
   1.130 +  end
   1.131 +
   1.132 +(* setup tactic *)
   1.133 +
   1.134 +val def_solver = "remote_csdp"
   1.135 +
   1.136 +fun sos_solver name = (SIMPLE_METHOD' o (Sos.sos_tac (call_solver name))) 
   1.137 +
   1.138 +val sos_method = Scan.optional (Scan.lift OuterParse.xname) def_solver >> sos_solver
   1.139 +
   1.140 +val setup = Method.setup @{binding sos} sos_method
   1.141 +  "Prove universal problems over the reals using sums of squares"
   1.142 +
   1.143 +end