src/HOL/Library/Sum_Of_Squares/sos_wrapper.ML
author wenzelm
Mon, 17 May 2010 23:54:15 +0200
changeset 36960 01594f816e3a
parent 35010 d6e492cea6e4
child 38805 b09d8603f865
permissions -rw-r--r--
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax; eliminated old-style structure aliases K = Keyword, P = Parse;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
32949
aa6c470a962a eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents: 32944
diff changeset
     1
(*  Title:      HOL/Library/Sum_Of_Squares/sos_wrapper.ML
aa6c470a962a eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents: 32944
diff changeset
     2
    Author:     Philipp Meyer, TU Muenchen
32268
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
     3
32949
aa6c470a962a eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents: 32944
diff changeset
     4
Added functionality for sums of squares, e.g. calling a remote prover.
32268
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
32332
bc5cec7b2be6 misc changes to SOS by Philipp Meyer:
wenzelm
parents: 32268
diff changeset
     9
  datatype prover_result = Success | Failure | Error
32268
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    10
  val setup: theory -> theory
32740
9dd0a2f83429 explicit indication of Unsynchronized.ref;
wenzelm
parents: 32646
diff changeset
    11
  val destdir: string Unsynchronized.ref
32949
aa6c470a962a eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents: 32944
diff changeset
    12
  val prover_name: string Unsynchronized.ref
32268
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    13
end
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    14
32949
aa6c470a962a eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents: 32944
diff changeset
    15
structure SOS_Wrapper: SOS_WRAPPER =
32268
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    16
struct
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    17
32332
bc5cec7b2be6 misc changes to SOS by Philipp Meyer:
wenzelm
parents: 32268
diff changeset
    18
datatype prover_result = Success | Failure | Error
32949
aa6c470a962a eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents: 32944
diff changeset
    19
32332
bc5cec7b2be6 misc changes to SOS by Philipp Meyer:
wenzelm
parents: 32268
diff changeset
    20
fun str_of_result Success = "Success"
bc5cec7b2be6 misc changes to SOS by Philipp Meyer:
wenzelm
parents: 32268
diff changeset
    21
  | str_of_result Failure = "Failure"
bc5cec7b2be6 misc changes to SOS by Philipp Meyer:
wenzelm
parents: 32268
diff changeset
    22
  | str_of_result Error = "Error"
32268
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    23
32949
aa6c470a962a eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents: 32944
diff changeset
    24
32268
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
32949
aa6c470a962a eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents: 32944
diff changeset
    27
fun debug s = if ! Sum_Of_Squares.debugging then writeln s else ()
aa6c470a962a eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents: 32944
diff changeset
    28
32268
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    29
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    30
(*** calling provers ***)
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    31
32740
9dd0a2f83429 explicit indication of Unsynchronized.ref;
wenzelm
parents: 32646
diff changeset
    32
val destdir = Unsynchronized.ref ""
32268
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    33
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    34
fun filename dir name =
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    35
  let
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    36
    val probfile = Path.basic (name ^ serial_string ())
32332
bc5cec7b2be6 misc changes to SOS by Philipp Meyer:
wenzelm
parents: 32268
diff changeset
    37
    val dir_path = Path.explode dir
32268
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
32949
aa6c470a962a eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents: 32944
diff changeset
    41
    else if File.exists dir_path then
aa6c470a962a eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents: 32944
diff changeset
    42
      Path.append dir_path probfile
aa6c470a962a eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents: 32944
diff changeset
    43
    else error ("No such directory: " ^ dir)
32268
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    44
  end
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    45
32332
bc5cec7b2be6 misc changes to SOS by Philipp Meyer:
wenzelm
parents: 32268
diff changeset
    46
fun run_solver name cmd find_failure input =
32268
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    47
  let
32949
aa6c470a962a eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents: 32944
diff changeset
    48
    val _ = warning ("Calling solver: " ^ name)
32268
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    49
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    50
    (* create input file *)
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    51
    val dir = ! destdir
32949
aa6c470a962a eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents: 32944
diff changeset
    52
    val input_file = filename dir "sos_in"
32268
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    53
    val _ = File.write input_file input
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    54
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    55
    (* call solver *)
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    56
    val output_file = filename dir "sos_out"
35010
d6e492cea6e4 renamed system/system_out to bash/bash_output -- to emphasized that this is really GNU bash, not some undefined POSIX sh;
wenzelm
parents: 32949
diff changeset
    57
    val (output, rv) =
d6e492cea6e4 renamed system/system_out to bash/bash_output -- to emphasized that this is really GNU bash, not some undefined POSIX sh;
wenzelm
parents: 32949
diff changeset
    58
      bash_output
d6e492cea6e4 renamed system/system_out to bash/bash_output -- to emphasized that this is really GNU bash, not some undefined POSIX sh;
wenzelm
parents: 32949
diff changeset
    59
       (if File.exists cmd then
d6e492cea6e4 renamed system/system_out to bash/bash_output -- to emphasized that this is really GNU bash, not some undefined POSIX sh;
wenzelm
parents: 32949
diff changeset
    60
          space_implode " "
d6e492cea6e4 renamed system/system_out to bash/bash_output -- to emphasized that this is really GNU bash, not some undefined POSIX sh;
wenzelm
parents: 32949
diff changeset
    61
            [File.shell_path cmd, File.shell_path input_file, File.shell_path output_file]
d6e492cea6e4 renamed system/system_out to bash/bash_output -- to emphasized that this is really GNU bash, not some undefined POSIX sh;
wenzelm
parents: 32949
diff changeset
    62
        else error ("Bad executable: " ^ File.platform_path cmd))
32949
aa6c470a962a eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents: 32944
diff changeset
    63
aa6c470a962a eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents: 32944
diff changeset
    64
    (* read and analyze output *)
32332
bc5cec7b2be6 misc changes to SOS by Philipp Meyer:
wenzelm
parents: 32268
diff changeset
    65
    val (res, res_msg) = find_failure rv
bc5cec7b2be6 misc changes to SOS by Philipp Meyer:
wenzelm
parents: 32268
diff changeset
    66
    val result = if File.exists output_file then File.read output_file else ""
32268
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
    (* remove temporary files *)
32949
aa6c470a962a eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents: 32944
diff changeset
    69
    val _ =
aa6c470a962a eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents: 32944
diff changeset
    70
      if dir = "" then
aa6c470a962a eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents: 32944
diff changeset
    71
        (File.rm input_file; if File.exists output_file then File.rm output_file else ())
aa6c470a962a eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents: 32944
diff changeset
    72
      else ()
32268
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    73
32332
bc5cec7b2be6 misc changes to SOS by Philipp Meyer:
wenzelm
parents: 32268
diff changeset
    74
    val _ = debug ("Solver output:\n" ^ output)
32268
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    75
32949
aa6c470a962a eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents: 32944
diff changeset
    76
    val _ = warning (str_of_result res ^ ": " ^ res_msg)
32268
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    77
  in
32949
aa6c470a962a eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents: 32944
diff changeset
    78
    (case res of
32332
bc5cec7b2be6 misc changes to SOS by Philipp Meyer:
wenzelm
parents: 32268
diff changeset
    79
      Success => result
32949
aa6c470a962a eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents: 32944
diff changeset
    80
    | Failure => raise Sum_Of_Squares.Failure res_msg
aa6c470a962a eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents: 32944
diff changeset
    81
    | Error => error ("Prover failed: " ^ res_msg))
32268
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    82
  end
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    83
32949
aa6c470a962a eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents: 32944
diff changeset
    84
32268
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    85
(*** various provers ***)
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
(* local csdp client *)
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    88
32332
bc5cec7b2be6 misc changes to SOS by Philipp Meyer:
wenzelm
parents: 32268
diff changeset
    89
fun find_csdp_failure rv =
32268
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    90
  case rv of
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    91
    0 => (Success, "SDP solved")
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    92
  | 1 => (Failure, "SDP is primal infeasible")
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    93
  | 2 => (Failure, "SDP is dual infeasible")
32332
bc5cec7b2be6 misc changes to SOS by Philipp Meyer:
wenzelm
parents: 32268
diff changeset
    94
  | 3 => (Success, "SDP solved with reduced accuracy")
bc5cec7b2be6 misc changes to SOS by Philipp Meyer:
wenzelm
parents: 32268
diff changeset
    95
  | 4 => (Failure, "Maximum iterations reached")
bc5cec7b2be6 misc changes to SOS by Philipp Meyer:
wenzelm
parents: 32268
diff changeset
    96
  | 5 => (Failure, "Stuck at edge of primal feasibility")
bc5cec7b2be6 misc changes to SOS by Philipp Meyer:
wenzelm
parents: 32268
diff changeset
    97
  | 6 => (Failure, "Stuck at edge of dual infeasibility")
bc5cec7b2be6 misc changes to SOS by Philipp Meyer:
wenzelm
parents: 32268
diff changeset
    98
  | 7 => (Failure, "Lack of progress")
bc5cec7b2be6 misc changes to SOS by Philipp Meyer:
wenzelm
parents: 32268
diff changeset
    99
  | 8 => (Failure, "X, Z, or O was singular")
bc5cec7b2be6 misc changes to SOS by Philipp Meyer:
wenzelm
parents: 32268
diff changeset
   100
  | 9 => (Failure, "Detected NaN or Inf values")
bc5cec7b2be6 misc changes to SOS by Philipp Meyer:
wenzelm
parents: 32268
diff changeset
   101
  | _ => (Error, "return code is " ^ string_of_int rv)
32268
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
   102
32332
bc5cec7b2be6 misc changes to SOS by Philipp Meyer:
wenzelm
parents: 32268
diff changeset
   103
val csdp = ("$CSDP_EXE", find_csdp_failure)
32268
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
   104
32949
aa6c470a962a eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents: 32944
diff changeset
   105
32268
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
   106
(* remote neos server *)
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
   107
32332
bc5cec7b2be6 misc changes to SOS by Philipp Meyer:
wenzelm
parents: 32268
diff changeset
   108
fun find_neos_failure rv =
bc5cec7b2be6 misc changes to SOS by Philipp Meyer:
wenzelm
parents: 32268
diff changeset
   109
  case rv of
bc5cec7b2be6 misc changes to SOS by Philipp Meyer:
wenzelm
parents: 32268
diff changeset
   110
    20 => (Error, "error submitting job")
32362
c0c640d86b4e interrupt handler for neos csdp client
Philipp Meyer
parents: 32332
diff changeset
   111
  | 21 => (Error, "interrupt")
32332
bc5cec7b2be6 misc changes to SOS by Philipp Meyer:
wenzelm
parents: 32268
diff changeset
   112
  |  _ => find_csdp_failure rv
32268
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
   113
32332
bc5cec7b2be6 misc changes to SOS by Philipp Meyer:
wenzelm
parents: 32268
diff changeset
   114
val neos_csdp = ("$ISABELLE_SUM_OF_SQUARES/neos_csdp_client", find_neos_failure)
32268
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
   115
32949
aa6c470a962a eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents: 32944
diff changeset
   116
aa6c470a962a eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents: 32944
diff changeset
   117
(* named provers *)
aa6c470a962a eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents: 32944
diff changeset
   118
aa6c470a962a eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents: 32944
diff changeset
   119
fun prover "remote_csdp" = neos_csdp
aa6c470a962a eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents: 32944
diff changeset
   120
  | prover "csdp" = csdp
aa6c470a962a eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents: 32944
diff changeset
   121
  | prover name = error ("Unknown prover: " ^ name)
32363
a0ea6cd47724 SOS: function to set default prover; output channel changed
Philipp Meyer
parents: 32362
diff changeset
   122
32740
9dd0a2f83429 explicit indication of Unsynchronized.ref;
wenzelm
parents: 32646
diff changeset
   123
val prover_name = Unsynchronized.ref "remote_csdp"
32363
a0ea6cd47724 SOS: function to set default prover; output channel changed
Philipp Meyer
parents: 32362
diff changeset
   124
32949
aa6c470a962a eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents: 32944
diff changeset
   125
fun call_solver opt_name =
aa6c470a962a eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents: 32944
diff changeset
   126
  let
aa6c470a962a eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents: 32944
diff changeset
   127
    val name = the_default (! prover_name) opt_name
aa6c470a962a eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents: 32944
diff changeset
   128
    val (cmd, find_failure) = prover name
aa6c470a962a eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents: 32944
diff changeset
   129
  in run_solver name (Path.explode cmd) find_failure end
32268
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
   130
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
   131
32645
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents: 32363
diff changeset
   132
(* certificate output *)
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents: 32363
diff changeset
   133
32949
aa6c470a962a eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents: 32944
diff changeset
   134
fun output_line cert =
aa6c470a962a eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents: 32944
diff changeset
   135
  "To repeat this proof with a certifiate use this command:\n" ^
aa6c470a962a eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents: 32944
diff changeset
   136
    Markup.markup Markup.sendback ("by (sos_cert \"" ^ cert ^ "\")")
32268
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
   137
32949
aa6c470a962a eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents: 32944
diff changeset
   138
val print_cert = warning o output_line o PositivstellensatzTools.pss_tree_to_cert
32645
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents: 32363
diff changeset
   139
32268
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
   140
32949
aa6c470a962a eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents: 32944
diff changeset
   141
(* method setup *)
32268
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
   142
32949
aa6c470a962a eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents: 32944
diff changeset
   143
fun sos_solver print method = SIMPLE_METHOD' o Sum_Of_Squares.sos_tac print method
32645
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents: 32363
diff changeset
   144
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents: 32363
diff changeset
   145
val setup =
32949
aa6c470a962a eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents: 32944
diff changeset
   146
  Method.setup @{binding sos}
36960
01594f816e3a prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents: 35010
diff changeset
   147
    (Scan.lift (Scan.option Parse.xname)
32949
aa6c470a962a eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents: 32944
diff changeset
   148
      >> (sos_solver print_cert o Sum_Of_Squares.Prover o call_solver))
aa6c470a962a eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents: 32944
diff changeset
   149
    "prove universal problems over the reals using sums of squares" #>
aa6c470a962a eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents: 32944
diff changeset
   150
  Method.setup @{binding sos_cert}
36960
01594f816e3a prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents: 35010
diff changeset
   151
    (Scan.lift Parse.string
32949
aa6c470a962a eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents: 32944
diff changeset
   152
      >> (fn cert => fn ctxt =>
aa6c470a962a eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents: 32944
diff changeset
   153
        sos_solver ignore
aa6c470a962a eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents: 32944
diff changeset
   154
          (Sum_Of_Squares.Certificate (PositivstellensatzTools.cert_to_pss_tree ctxt cert)) ctxt))
aa6c470a962a eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents: 32944
diff changeset
   155
    "prove universal problems over the reals using sums of squares with certificates"
32268
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
   156
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
   157
end