(* Title:      sos_wrapper.ML

   Author:     Philipp Meyer, TU Muenchen

Added functionality for sums of squares, e.g. calling a remote prover

*)

signature SOS_WRAPPER =

sig

  datatype prover_result = Success | Failure | Error

  val setup: theory -> theory

  val destdir: string ref

end

structure SosWrapper : SOS_WRAPPER=

struct

datatype prover_result = Success | Failure | Error

fun str_of_result Success = "Success"

  | str_of_result Failure = "Failure"

  | str_of_result Error = "Error"

(*** output control ***)

fun debug s = if ! Sos.debugging then Output.writeln s else ()

val write = Output.priority

(*** calling provers ***)

val destdir = ref ""

fun filename dir name =

  let

    val probfile = Path.basic (name ^ serial_string ())

    val dir_path = Path.explode dir

  in

    if dir = "" then

      File.tmp_path probfile

    else

      if File.exists dir_path then

        Path.append dir_path probfile

      else

        error ("No such directory: " ^ dir)

  end

fun run_solver name cmd find_failure input =

  let

    val _ = write ("Calling solver: " ^ name)

    (* create input file *)

    val dir = ! destdir

    val input_file = filename dir "sos_in" 

    val _ = File.write input_file input

    (* call solver *)

    val output_file = filename dir "sos_out"

    val (output, rv) = system_out (

      if File.exists cmd then space_implode " "

        [File.shell_path cmd, File.platform_path input_file, File.platform_path output_file]

      else error ("Bad executable: " ^ File.shell_path cmd))

    (* read and analysize output *)

    val (res, res_msg) = find_failure rv

    val result = if File.exists output_file then File.read output_file else ""

    (* remove temporary files *)

    val _ = if dir = "" then

        (File.rm input_file ; if File.exists output_file then File.rm output_file else ())

        else ()

    val _ = debug ("Solver output:\n" ^ output)

    val _ = write (str_of_result res ^ ": " ^ res_msg)

  in

    case res of

      Success => result

    | Failure => raise Sos.Failure res_msg

    | Error => error ("Prover failed: " ^ res_msg)

  end

(*** various provers ***)

(* local csdp client *)

fun find_csdp_failure rv =

  case rv of

    0 => (Success, "SDP solved")

  | 1 => (Failure, "SDP is primal infeasible")

  | 2 => (Failure, "SDP is dual infeasible")

  | 3 => (Success, "SDP solved with reduced accuracy")

  | 4 => (Failure, "Maximum iterations reached")

  | 5 => (Failure, "Stuck at edge of primal feasibility")

  | 6 => (Failure, "Stuck at edge of dual infeasibility")

  | 7 => (Failure, "Lack of progress")

  | 8 => (Failure, "X, Z, or O was singular")

  | 9 => (Failure, "Detected NaN or Inf values")

  | _ => (Error, "return code is " ^ string_of_int rv)

val csdp = ("$CSDP_EXE", find_csdp_failure)

(* remote neos server *)

fun find_neos_failure rv =

  case rv of

    20 => (Error, "error submitting job")

  | 21 => (Error, "no solution")

  |  _ => find_csdp_failure rv

val neos_csdp = ("$ISABELLE_SUM_OF_SQUARES/neos_csdp_client", find_neos_failure)

(* save provers in table *)

val provers =

     Symtab.make [("remote_csdp", neos_csdp),("csdp", csdp)]

fun get_prover name =

  case Symtab.lookup provers name of

    SOME prover => prover

  | NONE => error ("unknown prover: " ^ name)

fun call_solver name =

  let

    val (cmd, find_failure) = get_prover name

  in

    run_solver name (Path.explode cmd) find_failure

  end

(* setup tactic *)

val def_solver = "remote_csdp"

fun sos_solver name = (SIMPLE_METHOD' o (Sos.sos_tac (call_solver name))) 

val sos_method = Scan.optional (Scan.lift OuterParse.xname) def_solver >> sos_solver

val setup = Method.setup @{binding sos} sos_method

  "Prove universal problems over the reals using sums of squares"

end