--- a/src/HOL/Library/Sum_of_Squares/sos_wrapper.ML Wed Oct 08 11:09:17 2014 +0200
+++ b/src/HOL/Library/Sum_of_Squares/sos_wrapper.ML Wed Oct 08 11:50:25 2014 +0200
@@ -1,7 +1,7 @@
(* Title: HOL/Library/Sum_of_Squares/sos_wrapper.ML
Author: Philipp Meyer, TU Muenchen
-Added functionality for sums of squares, e.g. calling a remote prover.
+Wrapper for "sos" proof method.
*)
signature SOS_WRAPPER =
@@ -18,12 +18,8 @@
| str_of_result Failure = "Failure"
| str_of_result Error = "Error"
-
-fun filename name =
- File.tmp_path (Path.basic (name ^ serial_string ()))
-
-fun find_failure rv =
- case rv of
+fun get_result rc =
+ (case rc of
0 => (Success, "SDP solved")
| 1 => (Failure, "SDP is primal infeasible")
| 2 => (Failure, "SDP is dual infeasible")
@@ -34,52 +30,37 @@
| 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 exe = Path.explode "$ISABELLE_CSDP"
+ | _ => (Error, "return code is " ^ string_of_int rc))
fun run_solver ctxt input =
- let
- (* create input file *)
- val input_file = filename "sos_in"
- val _ = File.write input_file input
+ Isabelle_System.with_tmp_file "sos_in" "" (fn in_path =>
+ Isabelle_System.with_tmp_file "sos_out" "" (fn out_path =>
+ let
+ val _ = File.write in_path input
- (* call solver *)
- val output_file = filename "sos_out"
- val (output, rv) =
- Isabelle_System.bash_output
- (if File.exists exe then
- space_implode " " (map File.shell_path [exe, input_file, output_file])
- else error ("Bad executable: " ^ File.platform_path exe))
-
- (* read and analyze output *)
- val (res, res_msg) = find_failure rv
- val result = if File.exists output_file then File.read output_file else ""
+ val (output, rc) =
+ Isabelle_System.bash_output
+ ("\"$ISABELLE_CSDP\" " ^ File.shell_path in_path ^ " " ^ File.shell_path out_path)
+ val _ = Sum_of_Squares.debug_message ctxt (fn () => "Solver output:\n" ^ output)
- (* remove temporary files *)
- val _ = File.rm input_file
- val _ = if File.exists output_file then File.rm output_file else ()
+ val result = if File.exists out_path then File.read out_path else ""
- val _ =
- if Config.get ctxt Sum_of_Squares.trace
- then writeln ("Solver output:\n" ^ output)
- else ()
-
- val _ = warning (str_of_result res ^ ": " ^ res_msg)
- in
- (case res of
- Success => result
- | Failure => raise Sum_of_Squares.Failure res_msg
- | Error => error ("Prover failed: " ^ res_msg))
- end
+ val (res, res_msg) = get_result rc
+ val _ = Sum_of_Squares.trace_message ctxt (fn () => str_of_result res ^ ": " ^ res_msg)
+ in
+ (case res of
+ Success => result
+ | Failure => raise Sum_of_Squares.Failure res_msg
+ | Error => error ("Prover failed: " ^ res_msg))
+ end))
(* method setup *)
fun print_cert cert =
- warning
- ("To repeat this proof with a certificate use this proof method:\n" ^
- Active.sendback_markup [] ("(sos \"" ^ Positivstellensatz_Tools.print_cert cert ^ "\")"))
+ (writeln o Markup.markup Markup.information)
+ ("To repeat this proof with a certificate use this command:\n" ^
+ Active.sendback_markup [] ("by (sos \"" ^ Positivstellensatz_Tools.print_cert cert ^ "\")"))
fun sos_tac ctxt NONE =
Sum_of_Squares.sos_tac print_cert
--- a/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML Wed Oct 08 11:09:17 2014 +0200
+++ b/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML Wed Oct 08 11:50:25 2014 +0200
@@ -10,6 +10,9 @@
datatype proof_method = Certificate of RealArith.pss_tree | Prover of string -> string
val sos_tac: (RealArith.pss_tree -> unit) -> proof_method -> Proof.context -> int -> tactic
val trace: bool Config.T
+ val debug: bool Config.T
+ val trace_message: Proof.context -> (unit -> string) -> unit
+ val debug_message: Proof.context -> (unit -> string) -> unit
exception Failure of string;
end
@@ -52,7 +55,13 @@
val pow2 = rat_pow rat_2;
val pow10 = rat_pow rat_10;
+
val trace = Attrib.setup_config_bool @{binding sos_trace} (K false);
+val debug = Attrib.setup_config_bool @{binding sos_debug} (K false);
+
+fun trace_message ctxt msg =
+ if Config.get ctxt trace orelse Config.get ctxt debug then tracing (msg ()) else ();
+fun debug_message ctxt msg = if Config.get ctxt debug then tracing (msg ()) else ();
exception Sanity;
@@ -710,9 +719,7 @@
fun find_rounding d =
let
val _ =
- if Config.get ctxt trace
- then writeln ("Trying rounding with limit "^Rat.string_of_rat d ^ "\n")
- else ()
+ debug_message ctxt (fn () => "Trying rounding with limit "^Rat.string_of_rat d ^ "\n")
val vec = nice_vector d raw_vec
val blockmat =
iter (1, dim vec)
@@ -755,9 +762,10 @@
(* Iterative deepening. *)
-fun deepen f n =
- (writeln ("Searching with depth limit " ^ string_of_int n);
- (f n handle Failure s => (writeln ("failed with message: " ^ s); deepen f (n + 1))));
+fun deepen ctxt f n =
+ (trace_message ctxt (fn () => "Searching with depth limit " ^ string_of_int n);
+ (f n handle Failure s =>
+ (trace_message ctxt (fn () => "failed with message: " ^ s); deepen ctxt f (n + 1))));
(* Map back polynomials and their composites to a positivstellensatz. *)
@@ -839,7 +847,7 @@
(poly_neg(poly_pow pol i))))
(0 upto k)
end
- val (_,i,(cert_ideal,cert_cone)) = deepen tryall 0
+ val (_,i,(cert_ideal,cert_cone)) = deepen ctxt tryall 0
val proofs_ideal =
map2 (fn q => fn (_,ax) => RealArith.Eqmul(q,ax)) cert_ideal eq
val proofs_cone = map cterm_of_sos cert_cone