# HG changeset patch
# User wenzelm
# Date 1298045119 -3600
# Node ID 7eb9eac392b698d0de3064b8d05f489da87d3d00
# Parent  22d23da89aa518a90e202f55d559dc3af3b62c14# Parent  a68f503805ed9a97598c602e4e4b4ce8753d4df1
merged

diff -r a68f503805ed -r 7eb9eac392b6 src/HOL/Tools/Nitpick/nitpick.ML
--- a/src/HOL/Tools/Nitpick/nitpick.ML	Fri Feb 18 17:03:30 2011 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick.ML	Fri Feb 18 17:05:19 2011 +0100
@@ -981,15 +981,15 @@
   in (outcome_code, !state_ref) end
 
 (* Give the inner timeout a chance. *)
-val timeout_bonus = seconds 0.25
+val timeout_bonus = seconds 1.0
 
 fun pick_nits_in_term state (params as {debug, timeout, expect, ...}) auto i n
                       step subst assm_ts orig_t =
-  let val warning_m = if auto then K () else warning in
+  let val print_m = if auto then K () else Output.urgent_message in
     if getenv "KODKODI" = "" then
       (* The "expect" argument is deliberately ignored if Kodkodi is missing so
          that the "Nitpick_Examples" can be processed on any machine. *)
-      (warning_m (Pretty.string_of (plazy install_kodkodi_message));
+      (print_m (Pretty.string_of (plazy install_kodkodi_message));
        ("no_kodkodi", state))
     else
       let
@@ -1001,12 +1001,14 @@
               (pick_them_nits_in_term deadline state params auto i n step subst
                                       assm_ts) orig_t
           handle TOO_LARGE (_, details) =>
-                 (warning ("Limit reached: " ^ details ^ "."); unknown_outcome)
+                 (print_m ("Limit reached: " ^ details ^ "."); unknown_outcome)
                | TOO_SMALL (_, details) =>
-                 (warning ("Limit reached: " ^ details ^ "."); unknown_outcome)
+                 (print_m ("Limit reached: " ^ details ^ "."); unknown_outcome)
                | Kodkod.SYNTAX (_, details) =>
-                 (warning ("Ill-formed Kodkodi output: " ^ details ^ ".");
+                 (print_m ("Malformed Kodkodi output: " ^ details ^ ".");
                   unknown_outcome)
+               | TimeLimit.TimeOut =>
+                 (print_m "Nitpick ran out of time."; unknown_outcome)
       in
         if expect = "" orelse outcome_code = expect then outcome
         else error ("Unexpected outcome: " ^ quote outcome_code ^ ".")
diff -r a68f503805ed -r 7eb9eac392b6 src/HOL/Tools/SMT/smt_setup_solvers.ML
--- a/src/HOL/Tools/SMT/smt_setup_solvers.ML	Fri Feb 18 17:03:30 2011 +0100
+++ b/src/HOL/Tools/SMT/smt_setup_solvers.ML	Fri Feb 18 17:05:19 2011 +0100
@@ -62,7 +62,7 @@
     avail = make_avail is_remote "CVC3",
     command = make_command is_remote "CVC3",
     options = cvc3_options,
-    default_max_relevant = 250,
+    default_max_relevant = 200,
     supports_filter = false,
     outcome =
       on_first_line (outcome_of "Unsatisfiable." "Satisfiable." "Unknown."),
@@ -86,7 +86,7 @@
   options = (fn ctxt => [
     "--rand-seed=" ^ string_of_int (Config.get ctxt SMT_Config.random_seed),
     "--smtlib"]),
-  default_max_relevant = 275,
+  default_max_relevant = 200,
   supports_filter = false,
   outcome = on_first_line (outcome_of "unsat" "sat" "unknown"),
   cex_parser = NONE,
@@ -131,7 +131,7 @@
     avail = make_avail is_remote "Z3",
     command = z3_make_command is_remote "Z3",
     options = z3_options,
-    default_max_relevant = 225,
+    default_max_relevant = 250,
     supports_filter = true,
     outcome = z3_on_last_line,
     cex_parser = SOME Z3_Model.parse_counterex,
diff -r a68f503805ed -r 7eb9eac392b6 src/HOL/Tools/Sledgehammer/sledgehammer_run.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Fri Feb 18 17:03:30 2011 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Fri Feb 18 17:05:19 2011 +0100
@@ -175,6 +175,7 @@
   | n =>
     let
       val _ = Proof.assert_backward state
+      val print = if auto then K () else Output.urgent_message
       val state =
         state |> Proof.map_context (Config.put SMT_Config.verbose debug)
       val ctxt = Proof.context_of state
@@ -186,7 +187,7 @@
       val _ = case find_first (not o is_prover_supported ctxt) provers of
                 SOME name => error ("No such prover: " ^ name ^ ".")
               | NONE => ()
-      val _ = if auto then () else Output.urgent_message "Sledgehammering..."
+      val _ = print "Sledgehammering..."
       val (smts, atps) = provers |> List.partition (is_smt_prover ctxt)
       fun launch_provers state get_facts translate maybe_smt_filter provers =
         let
@@ -234,7 +235,7 @@
                           "Including (up to) " ^ string_of_int (length facts) ^
                           " relevant fact" ^ plural_s (length facts) ^ ":\n" ^
                           (facts |> map (fst o fst) |> space_implode " ") ^ ".")
-                       |> Output.urgent_message
+                       |> print
                      else
                        ())
         end
@@ -265,11 +266,13 @@
       fun launch_atps_and_smt_solvers () =
         [launch_atps, launch_smts]
         |> smart_par_list_map (fn f => f (false, state) |> K ())
-        handle ERROR msg => (Output.urgent_message ("Error: " ^ msg); error msg)
+        handle ERROR msg => (print ("Error: " ^ msg); error msg)
     in
       (false, state)
       |> (if blocking then launch_atps #> not auto ? launch_smts
           else (fn p => Future.fork (tap launch_atps_and_smt_solvers) |> K p))
+      handle TimeLimit.TimeOut =>
+             (print "Sledgehammer ran out of time."; (false, state))
     end
 
 end;