src/HOL/Library/Sum_of_Squares/sos_wrapper.ML
author wenzelm
Wed, 08 Oct 2014 11:09:17 +0200
changeset 58630 71cdb885b3bb
parent 58629 a6a6cd499d4e
child 58631 41333b45bff9
permissions -rw-r--r--
simplified "sos" method;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
41474
60d091240485 renamed Sum_Of_Squares to Sum_of_Squares;
wenzelm
parents: 38805
diff changeset
     1
(*  Title:      HOL/Library/Sum_of_Squares/sos_wrapper.ML
32949
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
58630
71cdb885b3bb simplified "sos" method;
wenzelm
parents: 58629
diff changeset
     9
  val sos_tac: Proof.context -> string option -> int -> tactic
32268
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    10
end
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    11
32949
aa6c470a962a eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents: 32944
diff changeset
    12
structure SOS_Wrapper: SOS_WRAPPER =
32268
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    13
struct
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    14
32332
bc5cec7b2be6 misc changes to SOS by Philipp Meyer:
wenzelm
parents: 32268
diff changeset
    15
datatype prover_result = Success | Failure | Error
32949
aa6c470a962a eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents: 32944
diff changeset
    16
32332
bc5cec7b2be6 misc changes to SOS by Philipp Meyer:
wenzelm
parents: 32268
diff changeset
    17
fun str_of_result Success = "Success"
bc5cec7b2be6 misc changes to SOS by Philipp Meyer:
wenzelm
parents: 32268
diff changeset
    18
  | str_of_result Failure = "Failure"
bc5cec7b2be6 misc changes to SOS by Philipp Meyer:
wenzelm
parents: 32268
diff changeset
    19
  | str_of_result Error = "Error"
32268
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    20
32949
aa6c470a962a eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents: 32944
diff changeset
    21
58630
71cdb885b3bb simplified "sos" method;
wenzelm
parents: 58629
diff changeset
    22
fun filename name =
71cdb885b3bb simplified "sos" method;
wenzelm
parents: 58629
diff changeset
    23
  File.tmp_path (Path.basic (name ^ serial_string ()))
32268
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    24
58630
71cdb885b3bb simplified "sos" method;
wenzelm
parents: 58629
diff changeset
    25
fun find_failure rv =
71cdb885b3bb simplified "sos" method;
wenzelm
parents: 58629
diff changeset
    26
  case rv of
71cdb885b3bb simplified "sos" method;
wenzelm
parents: 58629
diff changeset
    27
    0 => (Success, "SDP solved")
71cdb885b3bb simplified "sos" method;
wenzelm
parents: 58629
diff changeset
    28
  | 1 => (Failure, "SDP is primal infeasible")
71cdb885b3bb simplified "sos" method;
wenzelm
parents: 58629
diff changeset
    29
  | 2 => (Failure, "SDP is dual infeasible")
71cdb885b3bb simplified "sos" method;
wenzelm
parents: 58629
diff changeset
    30
  | 3 => (Success, "SDP solved with reduced accuracy")
71cdb885b3bb simplified "sos" method;
wenzelm
parents: 58629
diff changeset
    31
  | 4 => (Failure, "Maximum iterations reached")
71cdb885b3bb simplified "sos" method;
wenzelm
parents: 58629
diff changeset
    32
  | 5 => (Failure, "Stuck at edge of primal feasibility")
71cdb885b3bb simplified "sos" method;
wenzelm
parents: 58629
diff changeset
    33
  | 6 => (Failure, "Stuck at edge of dual infeasibility")
71cdb885b3bb simplified "sos" method;
wenzelm
parents: 58629
diff changeset
    34
  | 7 => (Failure, "Lack of progress")
71cdb885b3bb simplified "sos" method;
wenzelm
parents: 58629
diff changeset
    35
  | 8 => (Failure, "X, Z, or O was singular")
71cdb885b3bb simplified "sos" method;
wenzelm
parents: 58629
diff changeset
    36
  | 9 => (Failure, "Detected NaN or Inf values")
71cdb885b3bb simplified "sos" method;
wenzelm
parents: 58629
diff changeset
    37
  | _ => (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
    38
58630
71cdb885b3bb simplified "sos" method;
wenzelm
parents: 58629
diff changeset
    39
val exe = Path.explode "$ISABELLE_CSDP"
71cdb885b3bb simplified "sos" method;
wenzelm
parents: 58629
diff changeset
    40
71cdb885b3bb simplified "sos" method;
wenzelm
parents: 58629
diff changeset
    41
fun run_solver ctxt input =
32268
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    42
  let
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    43
    (* create input file *)
58630
71cdb885b3bb simplified "sos" method;
wenzelm
parents: 58629
diff changeset
    44
    val input_file = filename "sos_in"
32268
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    45
    val _ = File.write input_file input
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    46
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    47
    (* call solver *)
58630
71cdb885b3bb simplified "sos" method;
wenzelm
parents: 58629
diff changeset
    48
    val output_file = filename "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
    49
    val (output, rv) =
43850
7f2cbc713344 moved bash operations to Isabelle_System (cf. Scala version);
wenzelm
parents: 42616
diff changeset
    50
      Isabelle_System.bash_output
41950
134131d519c0 clarified ISABELLE_CSDP setting (formerly CSDP_EXE);
wenzelm
parents: 41474
diff changeset
    51
       (if File.exists exe then
134131d519c0 clarified ISABELLE_CSDP setting (formerly CSDP_EXE);
wenzelm
parents: 41474
diff changeset
    52
          space_implode " " (map File.shell_path [exe, input_file, output_file])
134131d519c0 clarified ISABELLE_CSDP setting (formerly CSDP_EXE);
wenzelm
parents: 41474
diff changeset
    53
        else error ("Bad executable: " ^ File.platform_path exe))
32949
aa6c470a962a eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents: 32944
diff changeset
    54
aa6c470a962a eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents: 32944
diff changeset
    55
    (* read and analyze output *)
32332
bc5cec7b2be6 misc changes to SOS by Philipp Meyer:
wenzelm
parents: 32268
diff changeset
    56
    val (res, res_msg) = find_failure rv
bc5cec7b2be6 misc changes to SOS by Philipp Meyer:
wenzelm
parents: 32268
diff changeset
    57
    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
    58
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    59
    (* remove temporary files *)
58630
71cdb885b3bb simplified "sos" method;
wenzelm
parents: 58629
diff changeset
    60
    val _ = File.rm input_file
71cdb885b3bb simplified "sos" method;
wenzelm
parents: 58629
diff changeset
    61
    val _ = if File.exists output_file then File.rm output_file else ()
32268
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    62
38805
b09d8603f865 Sum_Of_Squares: proper configuration options;
wenzelm
parents: 36960
diff changeset
    63
    val _ =
41474
60d091240485 renamed Sum_Of_Squares to Sum_of_Squares;
wenzelm
parents: 38805
diff changeset
    64
      if Config.get ctxt Sum_of_Squares.trace
38805
b09d8603f865 Sum_Of_Squares: proper configuration options;
wenzelm
parents: 36960
diff changeset
    65
      then writeln ("Solver output:\n" ^ output)
b09d8603f865 Sum_Of_Squares: proper configuration options;
wenzelm
parents: 36960
diff changeset
    66
      else ()
32268
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    67
32949
aa6c470a962a eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents: 32944
diff changeset
    68
    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
    69
  in
32949
aa6c470a962a eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents: 32944
diff changeset
    70
    (case res of
32332
bc5cec7b2be6 misc changes to SOS by Philipp Meyer:
wenzelm
parents: 32268
diff changeset
    71
      Success => result
41474
60d091240485 renamed Sum_Of_Squares to Sum_of_Squares;
wenzelm
parents: 38805
diff changeset
    72
    | Failure => raise Sum_of_Squares.Failure res_msg
32949
aa6c470a962a eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents: 32944
diff changeset
    73
    | Error => error ("Prover failed: " ^ res_msg))
32268
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    74
  end
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
aa6c470a962a eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents: 32944
diff changeset
    77
(* method setup *)
32268
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    78
58630
71cdb885b3bb simplified "sos" method;
wenzelm
parents: 58629
diff changeset
    79
fun print_cert cert =
71cdb885b3bb simplified "sos" method;
wenzelm
parents: 58629
diff changeset
    80
  warning
71cdb885b3bb simplified "sos" method;
wenzelm
parents: 58629
diff changeset
    81
    ("To repeat this proof with a certificate use this proof method:\n" ^
71cdb885b3bb simplified "sos" method;
wenzelm
parents: 58629
diff changeset
    82
      Active.sendback_markup [] ("(sos \"" ^ Positivstellensatz_Tools.print_cert cert ^ "\")"))
71cdb885b3bb simplified "sos" method;
wenzelm
parents: 58629
diff changeset
    83
71cdb885b3bb simplified "sos" method;
wenzelm
parents: 58629
diff changeset
    84
fun sos_tac ctxt NONE =
71cdb885b3bb simplified "sos" method;
wenzelm
parents: 58629
diff changeset
    85
      Sum_of_Squares.sos_tac print_cert
71cdb885b3bb simplified "sos" method;
wenzelm
parents: 58629
diff changeset
    86
        (Sum_of_Squares.Prover (run_solver ctxt)) ctxt
71cdb885b3bb simplified "sos" method;
wenzelm
parents: 58629
diff changeset
    87
  | sos_tac ctxt (SOME cert) =
71cdb885b3bb simplified "sos" method;
wenzelm
parents: 58629
diff changeset
    88
      Sum_of_Squares.sos_tac ignore
71cdb885b3bb simplified "sos" method;
wenzelm
parents: 58629
diff changeset
    89
        (Sum_of_Squares.Certificate (Positivstellensatz_Tools.read_cert ctxt cert)) ctxt
32645
1cc5b24f5a01 sos method generates and uses proof certificates
Philipp Meyer
parents: 32363
diff changeset
    90
58418
a04b242a7a01 clarified SOS tool setup vs. examples;
wenzelm
parents: 56625
diff changeset
    91
val _ = Theory.setup
a04b242a7a01 clarified SOS tool setup vs. examples;
wenzelm
parents: 56625
diff changeset
    92
 (Method.setup @{binding sos}
58630
71cdb885b3bb simplified "sos" method;
wenzelm
parents: 58629
diff changeset
    93
    (Scan.lift (Scan.option Parse.string)
71cdb885b3bb simplified "sos" method;
wenzelm
parents: 58629
diff changeset
    94
      >> (fn arg => fn ctxt => SIMPLE_METHOD' (sos_tac ctxt arg)))
71cdb885b3bb simplified "sos" method;
wenzelm
parents: 58629
diff changeset
    95
    "prove universal problems over the reals using sums of squares")
32268
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    96
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    97
end