# HG changeset patch
# User blanchet
# Date 1306485007 -7200
# Node ID 5f8d74d3b297dc56da430e50d59f5aea97a01414
# Parent  a14cf580a5a54d85f4d43cbe40d127817b2aa16e
added syntax for specifying Metis timeout (currently used only by SMT solvers)

diff -r a14cf580a5a5 -r 5f8d74d3b297 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri May 27 10:30:07 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri May 27 10:30:07 2011 +0200
@@ -87,7 +87,8 @@
    ("explicit_apply", "false"),
    ("isar_proof", "false"),
    ("isar_shrink_factor", "1"),
-   ("slicing", "true")]
+   ("slicing", "true"),
+   ("metis_timeout", "5")]
 
 val alias_params =
   [("prover", "provers"),
@@ -105,7 +106,8 @@
 
 val params_for_minimize =
   ["debug", "verbose", "overlord", "type_sys", "full_types", "max_mono_iters",
-   "max_new_mono_instances", "isar_proof", "isar_shrink_factor", "timeout"]
+   "max_new_mono_instances", "isar_proof", "isar_shrink_factor", "timeout",
+   "metis_timeout"]
 
 val property_dependent_params = ["provers", "full_types", "timeout"]
 
@@ -275,6 +277,8 @@
     val isar_shrink_factor = Int.max (1, lookup_int "isar_shrink_factor")
     val slicing = not auto andalso lookup_bool "slicing"
     val timeout = (if auto then NONE else lookup_time "timeout") |> the_timeout
+    val metis_timeout =
+      if auto then Time.zeroTime else lookup_time "metis_timeout" |> the_timeout
     val expect = lookup_string "expect"
   in
     {debug = debug, verbose = verbose, overlord = overlord, blocking = blocking,
@@ -283,7 +287,7 @@
      max_new_mono_instances = max_new_mono_instances, type_sys = type_sys,
      explicit_apply = explicit_apply, isar_proof = isar_proof,
      isar_shrink_factor = isar_shrink_factor, slicing = slicing,
-     timeout = timeout, expect = expect}
+     timeout = timeout, metis_timeout = metis_timeout, expect = expect}
   end
 
 fun get_params auto ctxt = extract_params auto (default_raw_params ctxt)
diff -r a14cf580a5a5 -r 5f8d74d3b297 src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Fri May 27 10:30:07 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Fri May 27 10:30:07 2011 +0200
@@ -44,7 +44,7 @@
 
 fun test_facts ({debug, verbose, overlord, provers, max_mono_iters,
                  max_new_mono_instances, type_sys, isar_proof,
-                 isar_shrink_factor, ...} : params)
+                 isar_shrink_factor, metis_timeout, ...} : params)
         explicit_apply_opt silent (prover : prover) timeout i n state facts =
   let
     val ctxt = Proof.context_of state
@@ -70,7 +70,7 @@
        max_mono_iters = max_mono_iters,
        max_new_mono_instances = max_new_mono_instances, isar_proof = isar_proof,
        isar_shrink_factor = isar_shrink_factor, slicing = false,
-       timeout = timeout, expect = ""}
+       timeout = timeout, metis_timeout = metis_timeout, expect = ""}
     val facts =
       facts |> maps (fn (n, ths) => ths |> map (Untranslated_Fact o pair n))
     val problem =
diff -r a14cf580a5a5 -r 5f8d74d3b297 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Fri May 27 10:30:07 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Fri May 27 10:30:07 2011 +0200
@@ -35,6 +35,7 @@
      isar_shrink_factor: int,
      slicing: bool,
      timeout: Time.time,
+     metis_timeout: Time.time,
      expect: string}
 
   datatype prover_fact =
@@ -278,6 +279,7 @@
    isar_shrink_factor: int,
    slicing: bool,
    timeout: Time.time,
+   metis_timeout: Time.time,
    expect: string}
 
 datatype prover_fact =
@@ -879,17 +881,15 @@
     | _ => false
   end
 
-val smt_metis_timeout = seconds 1.0
+fun can_apply_metis debug timeout ths =
+  can_apply timeout (Config.put Metis_Tactics.verbose debug
+                     #> (fn ctxt => Metis_Tactics.metis_tac ctxt ths))
 
-fun can_apply_metis debug state i ths =
-  can_apply smt_metis_timeout
-            (Config.put Metis_Tactics.verbose debug
-             #> (fn ctxt => Metis_Tactics.metis_tac ctxt ths)) state i
-
-fun run_smt_solver auto name (params as {debug, verbose, blocking, ...})
-                   minimize_command
-                   ({state, subgoal, subgoal_count, facts, smt_filter, ...}
-                    : prover_problem) =
+fun run_smt_solver auto name
+        (params as {debug, verbose, blocking, metis_timeout, ...})
+        minimize_command
+        ({state, subgoal, subgoal_count, facts, smt_filter, ...}
+         : prover_problem) =
   let
     val ctxt = Proof.context_of state
     val num_facts = length facts
@@ -904,7 +904,8 @@
         NONE =>
         let
           val (method, settings) =
-            if can_apply_metis debug state subgoal (map snd used_facts) then
+            if can_apply_metis debug metis_timeout (map snd used_facts) state
+                               subgoal then
               ("metis", "")
             else
               ("smt", if name = SMT_Solver.solver_name_of ctxt then ""