src/HOL/Library/Sum_of_Squares/sos_wrapper.ML
author wenzelm
Wed, 08 Mar 2017 10:50:59 +0100
changeset 65151 a7394aa4d21c
parent 63518 ae8fd6fe63a1
child 69593 3dda49e08b9d
permissions -rw-r--r--
tuned proofs;
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
58631
41333b45bff9 clarified messages depending on options;
wenzelm
parents: 58630
diff changeset
     4
Wrapper for "sos" proof method.
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
58631
41333b45bff9 clarified messages depending on options;
wenzelm
parents: 58630
diff changeset
    21
fun get_result rc =
41333b45bff9 clarified messages depending on options;
wenzelm
parents: 58630
diff changeset
    22
  (case rc of
58630
71cdb885b3bb simplified "sos" method;
wenzelm
parents: 58629
diff changeset
    23
    0 => (Success, "SDP solved")
71cdb885b3bb simplified "sos" method;
wenzelm
parents: 58629
diff changeset
    24
  | 1 => (Failure, "SDP is primal infeasible")
71cdb885b3bb simplified "sos" method;
wenzelm
parents: 58629
diff changeset
    25
  | 2 => (Failure, "SDP is dual infeasible")
71cdb885b3bb simplified "sos" method;
wenzelm
parents: 58629
diff changeset
    26
  | 3 => (Success, "SDP solved with reduced accuracy")
71cdb885b3bb simplified "sos" method;
wenzelm
parents: 58629
diff changeset
    27
  | 4 => (Failure, "Maximum iterations reached")
71cdb885b3bb simplified "sos" method;
wenzelm
parents: 58629
diff changeset
    28
  | 5 => (Failure, "Stuck at edge of primal feasibility")
71cdb885b3bb simplified "sos" method;
wenzelm
parents: 58629
diff changeset
    29
  | 6 => (Failure, "Stuck at edge of dual infeasibility")
71cdb885b3bb simplified "sos" method;
wenzelm
parents: 58629
diff changeset
    30
  | 7 => (Failure, "Lack of progress")
71cdb885b3bb simplified "sos" method;
wenzelm
parents: 58629
diff changeset
    31
  | 8 => (Failure, "X, Z, or O was singular")
71cdb885b3bb simplified "sos" method;
wenzelm
parents: 58629
diff changeset
    32
  | 9 => (Failure, "Detected NaN or Inf values")
58631
41333b45bff9 clarified messages depending on options;
wenzelm
parents: 58630
diff changeset
    33
  | _ => (Error, "return code is " ^ string_of_int rc))
58630
71cdb885b3bb simplified "sos" method;
wenzelm
parents: 58629
diff changeset
    34
71cdb885b3bb simplified "sos" method;
wenzelm
parents: 58629
diff changeset
    35
fun run_solver ctxt input =
58631
41333b45bff9 clarified messages depending on options;
wenzelm
parents: 58630
diff changeset
    36
  Isabelle_System.with_tmp_file "sos_in" "" (fn in_path =>
41333b45bff9 clarified messages depending on options;
wenzelm
parents: 58630
diff changeset
    37
    Isabelle_System.with_tmp_file "sos_out" "" (fn out_path =>
41333b45bff9 clarified messages depending on options;
wenzelm
parents: 58630
diff changeset
    38
      let
41333b45bff9 clarified messages depending on options;
wenzelm
parents: 58630
diff changeset
    39
        val _ = File.write in_path input
32268
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    40
58631
41333b45bff9 clarified messages depending on options;
wenzelm
parents: 58630
diff changeset
    41
        val (output, rc) =
41333b45bff9 clarified messages depending on options;
wenzelm
parents: 58630
diff changeset
    42
          Isabelle_System.bash_output
62549
9498623b27f0 File.bash_string operations in ML as in Scala -- exclusively for GNU bash, not perl and not user output;
wenzelm
parents: 59184
diff changeset
    43
            ("\"$ISABELLE_CSDP\" " ^ File.bash_path in_path ^ " " ^ File.bash_path out_path)
58631
41333b45bff9 clarified messages depending on options;
wenzelm
parents: 58630
diff changeset
    44
        val _ = Sum_of_Squares.debug_message ctxt (fn () => "Solver output:\n" ^ output)
32268
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    45
58631
41333b45bff9 clarified messages depending on options;
wenzelm
parents: 58630
diff changeset
    46
        val result = if File.exists out_path then File.read out_path else ""
32268
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    47
58631
41333b45bff9 clarified messages depending on options;
wenzelm
parents: 58630
diff changeset
    48
        val (res, res_msg) = get_result rc
41333b45bff9 clarified messages depending on options;
wenzelm
parents: 58630
diff changeset
    49
        val _ = Sum_of_Squares.trace_message ctxt (fn () => str_of_result res ^ ": " ^ res_msg)
41333b45bff9 clarified messages depending on options;
wenzelm
parents: 58630
diff changeset
    50
      in
41333b45bff9 clarified messages depending on options;
wenzelm
parents: 58630
diff changeset
    51
        (case res of
41333b45bff9 clarified messages depending on options;
wenzelm
parents: 58630
diff changeset
    52
          Success => result
41333b45bff9 clarified messages depending on options;
wenzelm
parents: 58630
diff changeset
    53
        | Failure => raise Sum_of_Squares.Failure res_msg
41333b45bff9 clarified messages depending on options;
wenzelm
parents: 58630
diff changeset
    54
        | Error => error ("Prover failed: " ^ res_msg))
41333b45bff9 clarified messages depending on options;
wenzelm
parents: 58630
diff changeset
    55
      end))
32268
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    56
32949
aa6c470a962a eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents: 32944
diff changeset
    57
aa6c470a962a eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents: 32944
diff changeset
    58
(* method setup *)
32268
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    59
58630
71cdb885b3bb simplified "sos" method;
wenzelm
parents: 58629
diff changeset
    60
fun print_cert cert =
59184
830bb7ddb3ab explicit message channels for "state", "information";
wenzelm
parents: 58631
diff changeset
    61
  Output.information
58631
41333b45bff9 clarified messages depending on options;
wenzelm
parents: 58630
diff changeset
    62
    ("To repeat this proof with a certificate use this command:\n" ^
63518
ae8fd6fe63a1 tuned signature;
wenzelm
parents: 63507
diff changeset
    63
      Active.sendback_markup_command
63507
79122bdd4404 clarified markup;
wenzelm
parents: 62549
diff changeset
    64
        ("by (sos \"" ^ Positivstellensatz_Tools.print_cert cert ^ "\")"))
58630
71cdb885b3bb simplified "sos" method;
wenzelm
parents: 58629
diff changeset
    65
71cdb885b3bb simplified "sos" method;
wenzelm
parents: 58629
diff changeset
    66
fun sos_tac ctxt NONE =
71cdb885b3bb simplified "sos" method;
wenzelm
parents: 58629
diff changeset
    67
      Sum_of_Squares.sos_tac print_cert
71cdb885b3bb simplified "sos" method;
wenzelm
parents: 58629
diff changeset
    68
        (Sum_of_Squares.Prover (run_solver ctxt)) ctxt
71cdb885b3bb simplified "sos" method;
wenzelm
parents: 58629
diff changeset
    69
  | sos_tac ctxt (SOME cert) =
71cdb885b3bb simplified "sos" method;
wenzelm
parents: 58629
diff changeset
    70
      Sum_of_Squares.sos_tac ignore
71cdb885b3bb simplified "sos" method;
wenzelm
parents: 58629
diff changeset
    71
        (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
    72
58418
a04b242a7a01 clarified SOS tool setup vs. examples;
wenzelm
parents: 56625
diff changeset
    73
val _ = Theory.setup
a04b242a7a01 clarified SOS tool setup vs. examples;
wenzelm
parents: 56625
diff changeset
    74
 (Method.setup @{binding sos}
58630
71cdb885b3bb simplified "sos" method;
wenzelm
parents: 58629
diff changeset
    75
    (Scan.lift (Scan.option Parse.string)
71cdb885b3bb simplified "sos" method;
wenzelm
parents: 58629
diff changeset
    76
      >> (fn arg => fn ctxt => SIMPLE_METHOD' (sos_tac ctxt arg)))
71cdb885b3bb simplified "sos" method;
wenzelm
parents: 58629
diff changeset
    77
    "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
    78
d50f0cb67578 Functionality for sum of squares to call a remote csdp prover
Philipp Meyer
parents:
diff changeset
    79
end