implemented general slicing for ATPs, especially E 1.2w and above
authorblanchet
Thu Apr 21 18:39:22 2011 +0200 (2011-04-21)
changeset 42443724e612ba248
parent 42442 036142bd0302
child 42444 8e5438dc70bb
implemented general slicing for ATPs, especially E 1.2w and above
doc-src/Sledgehammer/sledgehammer.tex
src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML
src/HOL/Tools/ATP/atp_systems.ML
src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML
src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
src/HOL/Tools/Sledgehammer/sledgehammer_run.ML
src/HOL/ex/sledgehammer_tactics.ML
     1.1 --- a/doc-src/Sledgehammer/sledgehammer.tex	Thu Apr 21 18:39:22 2011 +0200
     1.2 +++ b/doc-src/Sledgehammer/sledgehammer.tex	Thu Apr 21 18:39:22 2011 +0200
     1.3 @@ -356,7 +356,8 @@
     1.4  General. For automatic runs, only the first prover set using \textit{provers}
     1.5  (\S\ref{mode-of-operation}) is considered, \textit{verbose}
     1.6  (\S\ref{output-format}) and \textit{debug} (\S\ref{output-format}) are disabled,
     1.7 -fewer facts are passed to the prover, and \textit{timeout}
     1.8 +fewer facts are passed to the prover, \textit{slicing}
     1.9 +(\S\ref{mode-of-operation}) is disabled, and \textit{timeout}
    1.10  (\S\ref{mode-of-operation}) is superseded by the ``Auto Tools Time Limit'' in
    1.11  Proof General's ``Isabelle'' menu. Sledgehammer's output is also more concise.
    1.12  
    1.13 @@ -508,6 +509,21 @@
    1.14  the putative theorem manually while Sledgehammer looks for a proof, but it can
    1.15  also be more confusing.
    1.16  
    1.17 +\optrue{slicing}{no\_slicing}
    1.18 +Specifies whether the time allocated to a prover should be sliced into several
    1.19 +segments, each of which has its own set of possibly prover-dependent options.
    1.20 +For SPASS and Vampire, the first slice tries the fast-but-incomplete
    1.21 +set-of-support (SOS) strategy, whereas the second slice runs without it. For E,
    1.22 +up to three slices are defined, with different weighted search strategies and
    1.23 +number of facts. For SMT solvers, several slices are tried with the same options
    1.24 +but fewer and fewer facts. According to benchmarks with a timeout of 30 seconds,
    1.25 +slicing is a valuable optimization, and you should probably leave it enabled
    1.26 +unless you are conducting experiments. However, this option is implicitly
    1.27 +disabled for (short) automatic runs.
    1.28 +
    1.29 +\nopagebreak
    1.30 +{\small See also \textit{verbose} (\S\ref{output-format}).}
    1.31 +
    1.32  \opfalse{overlord}{no\_overlord}
    1.33  Specifies whether Sledgehammer should put its temporary files in
    1.34  \texttt{\$ISA\-BELLE\_\allowbreak HOME\_\allowbreak USER}, which is useful for
     2.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Thu Apr 21 18:39:22 2011 +0200
     2.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Thu Apr 21 18:39:22 2011 +0200
     2.3 @@ -317,13 +317,13 @@
     2.4  fun change_data id f = (Unsynchronized.change data (AList.map_entry (op =) id f); ())
     2.5  
     2.6  
     2.7 -fun get_prover ctxt args =
     2.8 +fun get_prover ctxt slicing args =
     2.9    let
    2.10      fun default_prover_name () =
    2.11        hd (#provers (Sledgehammer_Isar.default_params ctxt []))
    2.12        handle Empty => error "No ATP available."
    2.13      fun get_prover name =
    2.14 -      (name, Sledgehammer_Run.get_minimizing_prover ctxt false name)
    2.15 +      (name, Sledgehammer_Run.get_minimizing_prover ctxt false slicing name)
    2.16    in
    2.17      (case AList.lookup (op =) args proverK of
    2.18        SOME name => get_prover name
    2.19 @@ -362,14 +362,15 @@
    2.20        st |> Proof.map_context
    2.21                  (change_dir dir
    2.22                   #> Config.put Sledgehammer_Provers.measure_run_time true)
    2.23 -    val params as {type_sys, relevance_thresholds, max_relevant, ...} =
    2.24 +    val params as {type_sys, relevance_thresholds, max_relevant, slicing, ...} =
    2.25        Sledgehammer_Isar.default_params ctxt
    2.26            [("verbose", "true"),
    2.27             ("type_sys", type_sys),
    2.28             ("max_relevant", max_relevant),
    2.29             ("timeout", string_of_int timeout)]
    2.30      val default_max_relevant =
    2.31 -      Sledgehammer_Provers.default_max_relevant_for_prover ctxt prover_name
    2.32 +      Sledgehammer_Provers.default_max_relevant_for_prover ctxt slicing
    2.33 +        prover_name
    2.34      val is_built_in_const =
    2.35        Sledgehammer_Provers.is_built_in_const_for_prover ctxt prover_name
    2.36      val relevance_fudge =
    2.37 @@ -428,7 +429,7 @@
    2.38      val triv_str = if trivial then "[T] " else ""
    2.39      val _ = change_data id inc_sh_calls
    2.40      val _ = if trivial then () else change_data id inc_sh_nontriv_calls
    2.41 -    val (prover_name, prover) = get_prover (Proof.context_of st) args
    2.42 +    val (prover_name, prover) = get_prover (Proof.context_of st) true args
    2.43      val type_sys = AList.lookup (op =) args type_sysK |> the_default "smart"
    2.44      val max_relevant = AList.lookup (op =) args max_relevantK |> the_default "smart"
    2.45      val dir = AList.lookup (op =) args keepK
    2.46 @@ -472,7 +473,7 @@
    2.47    let
    2.48      val ctxt = Proof.context_of st
    2.49      val n0 = length (these (!named_thms))
    2.50 -    val (prover_name, _) = get_prover ctxt args
    2.51 +    val (prover_name, _) = get_prover ctxt false args
    2.52      val type_sys = AList.lookup (op =) args type_sysK |> the_default "smart"
    2.53      val timeout =
    2.54        AList.lookup (op =) args minimize_timeoutK
     3.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML	Thu Apr 21 18:39:22 2011 +0200
     3.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML	Thu Apr 21 18:39:22 2011 +0200
     3.3 @@ -112,16 +112,17 @@
     3.4           val {context = ctxt, facts, goal} = Proof.goal pre
     3.5           val prover = AList.lookup (op =) args "prover"
     3.6                        |> the_default default_prover
     3.7 +         val {relevance_thresholds, type_sys, max_relevant, slicing, ...} =
     3.8 +           Sledgehammer_Isar.default_params ctxt args
     3.9           val default_max_relevant =
    3.10 -           Sledgehammer_Provers.default_max_relevant_for_prover ctxt prover
    3.11 +           Sledgehammer_Provers.default_max_relevant_for_prover ctxt slicing
    3.12 +                                                                prover
    3.13          val is_built_in_const =
    3.14            Sledgehammer_Provers.is_built_in_const_for_prover ctxt default_prover
    3.15           val relevance_fudge =
    3.16             extract_relevance_fudge args
    3.17                 (Sledgehammer_Provers.relevance_fudge_for_prover ctxt prover)
    3.18           val relevance_override = {add = [], del = [], only = false}
    3.19 -         val {relevance_thresholds, type_sys, max_relevant, ...} =
    3.20 -           Sledgehammer_Isar.default_params ctxt args
    3.21           val subgoal = 1
    3.22           val (_, hyp_ts, concl_t) = Sledgehammer_Util.strip_subgoal goal subgoal
    3.23           val no_dangerous_types =
     4.1 --- a/src/HOL/Tools/ATP/atp_systems.ML	Thu Apr 21 18:39:22 2011 +0200
     4.2 +++ b/src/HOL/Tools/ATP/atp_systems.ML	Thu Apr 21 18:39:22 2011 +0200
     4.3 @@ -12,15 +12,15 @@
     4.4    type atp_config =
     4.5      {exec: string * string,
     4.6       required_execs: (string * string) list,
     4.7 -     arguments: bool -> Time.time -> (unit -> (string * real) list) -> string,
     4.8 -     has_incomplete_mode: bool,
     4.9 +     arguments: int -> Time.time -> (unit -> (string * real) list) -> string,
    4.10 +     slices: unit -> (real * (bool * int)) list,
    4.11       proof_delims: (string * string) list,
    4.12       known_failures: (failure * string) list,
    4.13 -     default_max_relevant: int,
    4.14       explicit_forall: bool,
    4.15       use_conjecture_for_hypotheses: bool}
    4.16  
    4.17 -  datatype e_weight_method = E_Auto | E_Fun_Weight | E_Sym_Offset_Weight
    4.18 +  datatype e_weight_method =
    4.19 +    E_Slices | E_Auto | E_Fun_Weight | E_Sym_Offset_Weight
    4.20  
    4.21    (* for experimentation purposes -- do not use in production code *)
    4.22    val e_weight_method : e_weight_method Unsynchronized.ref
    4.23 @@ -40,7 +40,7 @@
    4.24    val remote_prefix : string
    4.25    val remote_atp :
    4.26      string -> string -> string list -> (string * string) list
    4.27 -    -> (failure * string) list -> int -> bool -> string * atp_config
    4.28 +    -> (failure * string) list -> (unit -> int) -> bool -> string * atp_config
    4.29    val add_atp : string * atp_config -> theory -> theory
    4.30    val get_atp : theory -> string -> atp_config
    4.31    val supported_atps : theory -> string list
    4.32 @@ -59,11 +59,10 @@
    4.33  type atp_config =
    4.34    {exec: string * string,
    4.35     required_execs: (string * string) list,
    4.36 -   arguments: bool -> Time.time -> (unit -> (string * real) list) -> string,
    4.37 -   has_incomplete_mode: bool,
    4.38 +   arguments: int -> Time.time -> (unit -> (string * real) list) -> string,
    4.39 +   slices: unit -> (real * (bool * int)) list,
    4.40     proof_delims: (string * string) list,
    4.41     known_failures: (failure * string) list,
    4.42 -   default_max_relevant: int,
    4.43     explicit_forall: bool,
    4.44     use_conjecture_for_hypotheses: bool}
    4.45  
    4.46 @@ -106,9 +105,10 @@
    4.47  val tstp_proof_delims =
    4.48    ("# SZS output start CNFRefutation.", "# SZS output end CNFRefutation")
    4.49  
    4.50 -datatype e_weight_method = E_Auto | E_Fun_Weight | E_Sym_Offset_Weight
    4.51 +datatype e_weight_method =
    4.52 +  E_Slices | E_Auto | E_Fun_Weight | E_Sym_Offset_Weight
    4.53  
    4.54 -val e_weight_method = Unsynchronized.ref E_Fun_Weight
    4.55 +val e_weight_method = Unsynchronized.ref E_Slices
    4.56  (* FUDGE *)
    4.57  val e_default_fun_weight = Unsynchronized.ref 20.0
    4.58  val e_fun_weight_base = Unsynchronized.ref 0.0
    4.59 @@ -117,44 +117,67 @@
    4.60  val e_sym_offs_weight_base = Unsynchronized.ref ~20.0
    4.61  val e_sym_offs_weight_span = Unsynchronized.ref 60.0
    4.62  
    4.63 -fun e_weight_method_case fw sow =
    4.64 -  case !e_weight_method of
    4.65 +fun e_weight_method_case method fw sow =
    4.66 +  case method of
    4.67      E_Auto => raise Fail "Unexpected \"E_Auto\""
    4.68    | E_Fun_Weight => fw
    4.69    | E_Sym_Offset_Weight => sow
    4.70  
    4.71 -fun scaled_e_weight w =
    4.72 -  e_weight_method_case (!e_fun_weight_base) (!e_sym_offs_weight_base)
    4.73 -  + w * e_weight_method_case (!e_fun_weight_span) (!e_sym_offs_weight_span)
    4.74 +fun scaled_e_weight method w =
    4.75 +  w * e_weight_method_case method (!e_fun_weight_span) (!e_sym_offs_weight_span)
    4.76 +  + e_weight_method_case method (!e_fun_weight_base) (!e_sym_offs_weight_base)
    4.77    |> Real.ceil |> signed_string_of_int
    4.78  
    4.79 -fun e_weight_arguments weights =
    4.80 -  if !e_weight_method = E_Auto orelse
    4.81 -     string_ord (getenv "E_VERSION", "1.2w") = LESS then
    4.82 +fun e_weight_arguments method weights =
    4.83 +  if method = E_Auto then
    4.84      "-xAutoDev"
    4.85    else
    4.86      "--split-clauses=4 --split-reuse-defs --simul-paramod --forward-context-sr \
    4.87      \--destructive-er-aggressive --destructive-er --presat-simplify \
    4.88      \--prefer-initial-clauses -tKBO6 -winvfreqrank -c1 -Ginvfreqconjmax -F1 \
    4.89      \--delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred \
    4.90 -    \-H'(4*" ^ e_weight_method_case "FunWeight" "SymOffsetWeight" ^
    4.91 +    \-H'(4*" ^ e_weight_method_case method "FunWeight" "SymOffsetWeight" ^
    4.92      "(SimulateSOS, " ^
    4.93 -    (e_weight_method_case (!e_default_fun_weight) (!e_default_sym_offs_weight)
    4.94 +    (e_weight_method_case method (!e_default_fun_weight)
    4.95 +                                 (!e_default_sym_offs_weight)
    4.96       |> Real.ceil |> signed_string_of_int) ^
    4.97      ",20,1.5,1.5,1" ^
    4.98 -    (weights () |> map (fn (s, w) => "," ^ s ^ ":" ^ scaled_e_weight w)
    4.99 +    (weights () |> map (fn (s, w) => "," ^ s ^ ":" ^ scaled_e_weight method w)
   4.100                  |> implode) ^
   4.101      "),3*ConjectureGeneralSymbolWeight(PreferNonGoals,200,100,200,50,50,1,100,\
   4.102      \1.5,1.5,1),1*Clauseweight(PreferProcessed,1,1,1),1*\
   4.103      \FIFOWeight(PreferProcessed))'"
   4.104  
   4.105 +fun is_old_e_version () = (string_ord (getenv "E_VERSION", "1.2w") = LESS)
   4.106 +
   4.107 +fun effective_e_weight_method () =
   4.108 +  if is_old_e_version () then E_Auto else !e_weight_method
   4.109 +
   4.110 +(* The order here must correspond to the order in "e_config" below. *)
   4.111 +fun method_for_slice slice =
   4.112 +  case effective_e_weight_method () of
   4.113 +    E_Slices => (case slice of
   4.114 +                   0 => E_Sym_Offset_Weight
   4.115 +                 | 1 => E_Auto
   4.116 +                 | 2 => E_Fun_Weight
   4.117 +                 | _ => raise Fail "no such slice")
   4.118 +  | method => method
   4.119 +
   4.120  val e_config : atp_config =
   4.121    {exec = ("E_HOME", "eproof"),
   4.122     required_execs = [],
   4.123 -   arguments = fn _ => fn timeout => fn weights =>
   4.124 -     "--tstp-in --tstp-out -l5 " ^ e_weight_arguments weights ^ " -tAutoDev \
   4.125 -     \--silent --cpu-limit=" ^ string_of_int (to_secs (e_bonus ()) timeout),
   4.126 -   has_incomplete_mode = false,
   4.127 +   arguments = fn slice => fn timeout => fn weights =>
   4.128 +     "--tstp-in --tstp-out -l5 " ^
   4.129 +     e_weight_arguments (method_for_slice slice) weights ^
   4.130 +     " -tAutoDev --silent --cpu-limit=" ^
   4.131 +     string_of_int (to_secs (e_bonus ()) timeout),
   4.132 +   slices = fn () =>
   4.133 +     if effective_e_weight_method () = E_Slices then
   4.134 +       [(0.33333, (true, 100 (* FUDGE *))) (* E_Sym_Offset_Weight *),
   4.135 +        (0.33333, (true, 1000 (* FUDGE *))) (* E_Auto *),
   4.136 +        (0.33334, (true, 200 (* FUDGE *))) (* E_Fun_Weight *)]
   4.137 +     else
   4.138 +       [(1.0, (true, 250 (* FUDGE *)))],
   4.139     proof_delims = [tstp_proof_delims],
   4.140     known_failures =
   4.141       [(Unprovable, "SZS status: CounterSatisfiable"),
   4.142 @@ -165,7 +188,6 @@
   4.143         "# Cannot determine problem status within resource limit"),
   4.144        (OutOfResources, "SZS status: ResourceOut"),
   4.145        (OutOfResources, "SZS status ResourceOut")],
   4.146 -   default_max_relevant = 250 (* FUDGE *),
   4.147     explicit_forall = false,
   4.148     use_conjecture_for_hypotheses = true}
   4.149  
   4.150 @@ -179,11 +201,12 @@
   4.151  val spass_config : atp_config =
   4.152    {exec = ("ISABELLE_ATP", "scripts/spass"),
   4.153     required_execs = [("SPASS_HOME", "SPASS"), ("SPASS_HOME", "tptp2dfg")],
   4.154 -   arguments = fn complete => fn timeout => fn _ =>
   4.155 +   arguments = fn slice => fn timeout => fn _ =>
   4.156       ("-Auto -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof \
   4.157        \-VarWeight=3 -TimeLimit=" ^ string_of_int (to_secs 0 timeout))
   4.158 -     |> not complete ? prefix "-SOS=1 ",
   4.159 -   has_incomplete_mode = true,
   4.160 +     |> slice = 0 ? prefix "-SOS=1 ",
   4.161 +   slices = K [(0.66667, (false, 150 (* FUDGE *))) (* with SOS *),
   4.162 +               (0.33333, (true, 150 (* FUDGE *))) (* without SOS *)],
   4.163     proof_delims = [("Here is a proof", "Formulae used in the proof")],
   4.164     known_failures =
   4.165       known_perl_failures @
   4.166 @@ -194,7 +217,6 @@
   4.167        (MalformedInput, "Free Variable"),
   4.168        (SpassTooOld, "tptp2dfg"),
   4.169        (InternalError, "Please report this error")],
   4.170 -   default_max_relevant = 150 (* FUDGE *),
   4.171     explicit_forall = true,
   4.172     use_conjecture_for_hypotheses = true}
   4.173  
   4.174 @@ -206,12 +228,13 @@
   4.175  val vampire_config : atp_config =
   4.176    {exec = ("VAMPIRE_HOME", "vampire"),
   4.177     required_execs = [],
   4.178 -   arguments = fn complete => fn timeout => fn _ =>
   4.179 +   arguments = fn slice => fn timeout => fn _ =>
   4.180       (* This would work too but it's less tested: "--proof tptp " ^ *)
   4.181       "--mode casc -t " ^ string_of_int (to_secs 0 timeout) ^
   4.182       " --thanks \"Andrei and Krystof\" --input_file"
   4.183 -     |> not complete ? prefix "--sos on ",
   4.184 -   has_incomplete_mode = true,
   4.185 +     |> slice = 0 ? prefix "--sos on ",
   4.186 +   slices = K [(0.66667, (false, 450 (* FUDGE *))) (* with SOS *),
   4.187 +               (0.33333, (true, 450 (* FUDGE *))) (* without SOS *)],
   4.188     proof_delims =
   4.189       [("=========== Refutation ==========",
   4.190         "======= End of refutation ======="),
   4.191 @@ -227,7 +250,6 @@
   4.192        (Unprovable, "Termination reason: Satisfiable"),
   4.193        (VampireTooOld, "not a valid option"),
   4.194        (Interrupted, "Aborted by signal SIGINT")],
   4.195 -   default_max_relevant = 450 (* FUDGE *),
   4.196     explicit_forall = false,
   4.197     use_conjecture_for_hypotheses = true}
   4.198  
   4.199 @@ -241,13 +263,14 @@
   4.200     required_execs = [],
   4.201     arguments = fn _ => fn timeout => fn _ =>
   4.202       "MBQI=true -p -t:" ^ string_of_int (to_secs 0 timeout),
   4.203 -   has_incomplete_mode = false,
   4.204 +   slices = K [(1.0, (false, 250 (* FUDGE *)))],
   4.205     proof_delims = [],
   4.206     known_failures =
   4.207       [(Unprovable, "\nsat"),
   4.208        (IncompleteUnprovable, "\nunknown"),
   4.209 -      (ProofMissing, "\nunsat")],
   4.210 -   default_max_relevant = 225 (* FUDGE *),
   4.211 +      (IncompleteUnprovable, "SZS status Satisfiable"),
   4.212 +      (ProofMissing, "\nunsat"),
   4.213 +      (ProofMissing, "SZS status Unsatisfiable")],
   4.214     explicit_forall = true,
   4.215     use_conjecture_for_hypotheses = false}
   4.216  
   4.217 @@ -293,20 +316,21 @@
   4.218     arguments = fn _ => fn timeout => fn _ =>
   4.219       " -t " ^ string_of_int (Int.min (max_remote_secs, (to_secs 0 timeout)))
   4.220       ^ " -s " ^ the_system system_name system_versions,
   4.221 -   has_incomplete_mode = false,
   4.222 +   slices = fn () => [(1.0, (false, default_max_relevant ()))],
   4.223     proof_delims = insert (op =) tstp_proof_delims proof_delims,
   4.224     known_failures =
   4.225       known_failures @ known_perl_failures @
   4.226       [(TimedOut, "says Timeout")],
   4.227 -   default_max_relevant = default_max_relevant,
   4.228     explicit_forall = true,
   4.229     use_conjecture_for_hypotheses = use_conjecture_for_hypotheses}
   4.230  
   4.231 +fun int_average f xs = fold (Integer.add o f) xs 0 div length xs
   4.232 +
   4.233  fun remotify_config system_name system_versions
   4.234 -        ({proof_delims, known_failures, default_max_relevant,
   4.235 -          use_conjecture_for_hypotheses, ...} : atp_config) : atp_config =
   4.236 +        ({proof_delims, slices, known_failures, use_conjecture_for_hypotheses,
   4.237 +          ...} : atp_config) : atp_config =
   4.238    remote_config system_name system_versions proof_delims known_failures
   4.239 -                default_max_relevant use_conjecture_for_hypotheses
   4.240 +                (int_average (snd o snd) o slices) use_conjecture_for_hypotheses
   4.241  
   4.242  fun remote_atp name system_name system_versions proof_delims known_failures
   4.243                 default_max_relevant use_conjecture_for_hypotheses =
   4.244 @@ -318,17 +342,13 @@
   4.245  
   4.246  val remote_e = remotify_atp e "EP" ["1.0", "1.1", "1.2"]
   4.247  val remote_vampire = remotify_atp vampire "Vampire" ["0.6", "9.0", "1.0"]
   4.248 -val remote_z3_atp =
   4.249 -  remote_atp z3_atpN "Z3---" ["2.18"] []
   4.250 -             [(IncompleteUnprovable, "SZS status Satisfiable"),
   4.251 -              (ProofMissing, "SZS status Unsatisfiable")]
   4.252 -             225 (* FUDGE *) false
   4.253 +val remote_z3_atp = remotify_atp z3_atp "Z3---" ["2.18"]
   4.254  val remote_sine_e =
   4.255    remote_atp sine_eN "SInE" [] [] [(IncompleteUnprovable, "says Unknown")]
   4.256 -             500 (* FUDGE *) true
   4.257 +             (K 500 (* FUDGE *)) true
   4.258  val remote_snark =
   4.259    remote_atp snarkN "SNARK---" [] [("refutation.", "end_refutation.")] []
   4.260 -             250 (* FUDGE *) true
   4.261 +             (K 250 (* FUDGE *)) true
   4.262  
   4.263  (* Setup *)
   4.264  
     5.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Thu Apr 21 18:39:22 2011 +0200
     5.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Thu Apr 21 18:39:22 2011 +0200
     5.3 @@ -86,7 +86,8 @@
     5.4     ("type_sys", "smart"),
     5.5     ("explicit_apply", "false"),
     5.6     ("isar_proof", "false"),
     5.7 -   ("isar_shrink_factor", "1")]
     5.8 +   ("isar_shrink_factor", "1"),
     5.9 +   ("slicing", "true")]
    5.10  
    5.11  val alias_params =
    5.12    [("prover", "provers"),
    5.13 @@ -100,7 +101,8 @@
    5.14     ("dont_monomorphize", "monomorphize"),
    5.15     ("partial_types", "full_types"),
    5.16     ("implicit_apply", "explicit_apply"),
    5.17 -   ("no_isar_proof", "isar_proof")]
    5.18 +   ("no_isar_proof", "isar_proof"),
    5.19 +   ("no_slicing", "slicing")]
    5.20  
    5.21  val params_for_minimize =
    5.22    ["debug", "verbose", "overlord", "type_sys", "full_types", "isar_proof",
    5.23 @@ -252,6 +254,7 @@
    5.24      val explicit_apply = lookup_bool "explicit_apply"
    5.25      val isar_proof = lookup_bool "isar_proof"
    5.26      val isar_shrink_factor = Int.max (1, lookup_int "isar_shrink_factor")
    5.27 +    val slicing = lookup_bool "slicing"
    5.28      val timeout = (if auto then NONE else lookup_time "timeout") |> the_timeout
    5.29      val expect = lookup_string "expect"
    5.30    in
    5.31 @@ -260,8 +263,8 @@
    5.32       max_relevant = max_relevant, monomorphize = monomorphize,
    5.33       monomorphize_limit = monomorphize_limit, type_sys = type_sys,
    5.34       explicit_apply = explicit_apply, isar_proof = isar_proof,
    5.35 -     isar_shrink_factor = isar_shrink_factor, timeout = timeout,
    5.36 -     expect = expect}
    5.37 +     isar_shrink_factor = isar_shrink_factor, slicing = slicing,
    5.38 +     timeout = timeout, expect = expect}
    5.39    end
    5.40  
    5.41  fun get_params auto ctxt = extract_params auto (default_raw_params ctxt)
    5.42 @@ -300,7 +303,7 @@
    5.43    in
    5.44      if subcommand = runN then
    5.45        let val i = the_default 1 opt_i in
    5.46 -        run_sledgehammer (get_params false ctxt override_params) false i
    5.47 +        run_sledgehammer (get_params false ctxt override_params) false true i
    5.48                           relevance_override (minimize_command override_params i)
    5.49                           state
    5.50          |> K ()
    5.51 @@ -373,8 +376,8 @@
    5.52  
    5.53  fun auto_sledgehammer state =
    5.54    let val ctxt = Proof.context_of state in
    5.55 -    run_sledgehammer (get_params true ctxt []) true 1 no_relevance_override
    5.56 -                     (minimize_command [] 1) state
    5.57 +    run_sledgehammer (get_params true ctxt []) true false 1
    5.58 +                     no_relevance_override (minimize_command [] 1) state
    5.59    end
    5.60  
    5.61  val setup = Auto_Tools.register_tool (auto, auto_sledgehammer)
     6.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Thu Apr 21 18:39:22 2011 +0200
     6.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Thu Apr 21 18:39:22 2011 +0200
     6.3 @@ -67,7 +67,7 @@
     6.4         relevance_thresholds = (1.01, 1.01), max_relevant = NONE,
     6.5         monomorphize = false, monomorphize_limit = monomorphize_limit,
     6.6         isar_proof = isar_proof, isar_shrink_factor = isar_shrink_factor,
     6.7 -       timeout = timeout, expect = ""}
     6.8 +       slicing = false, timeout = timeout, expect = ""}
     6.9      val facts =
    6.10        facts |> maps (fn (n, ths) => ths |> map (Untranslated_Fact o pair n))
    6.11      val problem =
    6.12 @@ -147,7 +147,7 @@
    6.13                     silent i n state facts =
    6.14    let
    6.15      val ctxt = Proof.context_of state
    6.16 -    val prover = get_prover ctxt false prover_name
    6.17 +    val prover = get_prover ctxt false false prover_name
    6.18      val msecs = Time.toMilliseconds timeout
    6.19      val _ = print silent (fn () => "Sledgehammer minimize: " ^
    6.20                                     quote prover_name ^ ".")
     7.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu Apr 21 18:39:22 2011 +0200
     7.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu Apr 21 18:39:22 2011 +0200
     7.3 @@ -29,6 +29,7 @@
     7.4       explicit_apply: bool,
     7.5       isar_proof: bool,
     7.6       isar_shrink_factor: int,
     7.7 +     slicing: bool,
     7.8       timeout: Time.time,
     7.9       expect: string}
    7.10  
    7.11 @@ -55,8 +56,6 @@
    7.12    type prover = params -> minimize_command -> prover_problem -> prover_result
    7.13  
    7.14    (* for experimentation purposes -- do not use in production code *)
    7.15 -  val atp_run_twice_threshold : int Unsynchronized.ref
    7.16 -  val atp_first_iter_time_frac : real Unsynchronized.ref
    7.17    val smt_triggers : bool Unsynchronized.ref
    7.18    val smt_weights : bool Unsynchronized.ref
    7.19    val smt_weight_min_facts : int Unsynchronized.ref
    7.20 @@ -64,17 +63,17 @@
    7.21    val smt_max_weight : int Unsynchronized.ref
    7.22    val smt_max_weight_index : int Unsynchronized.ref
    7.23    val smt_weight_curve : (int -> int) Unsynchronized.ref
    7.24 -  val smt_max_iters : int Unsynchronized.ref
    7.25 -  val smt_iter_fact_frac : real Unsynchronized.ref
    7.26 -  val smt_iter_time_frac : real Unsynchronized.ref
    7.27 -  val smt_iter_min_msecs : int Unsynchronized.ref
    7.28 +  val smt_max_slices : int Unsynchronized.ref
    7.29 +  val smt_slice_fact_frac : real Unsynchronized.ref
    7.30 +  val smt_slice_time_frac : real Unsynchronized.ref
    7.31 +  val smt_slice_min_secs : int Unsynchronized.ref
    7.32  
    7.33    val das_Tool : string
    7.34    val select_smt_solver : string -> Proof.context -> Proof.context
    7.35    val is_smt_prover : Proof.context -> string -> bool
    7.36    val is_prover_supported : Proof.context -> string -> bool
    7.37    val is_prover_installed : Proof.context -> string -> bool
    7.38 -  val default_max_relevant_for_prover : Proof.context -> string -> int
    7.39 +  val default_max_relevant_for_prover : Proof.context -> bool -> string -> int
    7.40    val is_built_in_const_for_prover :
    7.41      Proof.context -> string -> string * typ -> term list -> bool * term list
    7.42    val atp_relevance_fudge : relevance_fudge
    7.43 @@ -94,7 +93,7 @@
    7.44    val kill_provers : unit -> unit
    7.45    val running_provers : unit -> unit
    7.46    val messages : int option -> unit
    7.47 -  val get_prover : Proof.context -> bool -> string -> prover
    7.48 +  val get_prover : Proof.context -> bool -> bool -> string -> prover
    7.49    val setup : theory -> theory
    7.50  end;
    7.51  
    7.52 @@ -130,12 +129,17 @@
    7.53  fun is_prover_installed ctxt =
    7.54    is_smt_prover ctxt orf is_atp_installed (Proof_Context.theory_of ctxt)
    7.55  
    7.56 -fun default_max_relevant_for_prover ctxt name =
    7.57 +fun get_slices slicing slices =
    7.58 +  (0 upto length slices - 1) ~~ slices
    7.59 +  |> not slicing ? (List.last #> single)
    7.60 +
    7.61 +fun default_max_relevant_for_prover ctxt slicing name =
    7.62    let val thy = Proof_Context.theory_of ctxt in
    7.63      if is_smt_prover ctxt name then
    7.64        SMT_Solver.default_max_relevant ctxt name
    7.65      else
    7.66 -      #default_max_relevant (get_atp thy name)
    7.67 +      fold (Integer.max o snd o snd o snd)
    7.68 +           (get_slices slicing (#slices (get_atp thy name) ())) 0
    7.69    end
    7.70  
    7.71  (* These are either simplified away by "Meson.presimplify" (most of the time) or
    7.72 @@ -238,6 +242,7 @@
    7.73     explicit_apply: bool,
    7.74     isar_proof: bool,
    7.75     isar_shrink_factor: int,
    7.76 +   slicing: bool,
    7.77     timeout: Time.time,
    7.78     expect: string}
    7.79  
    7.80 @@ -325,25 +330,22 @@
    7.81  fun int_opt_add (SOME m) (SOME n) = SOME (m + n)
    7.82    | int_opt_add _ _ = NONE
    7.83  
    7.84 -val atp_run_twice_threshold = Unsynchronized.ref 50
    7.85 -val atp_first_iter_time_frac = Unsynchronized.ref 0.67
    7.86 -
    7.87  (* Important messages are important but not so important that users want to see
    7.88     them each time. *)
    7.89 -val important_message_keep_factor = 0.1
    7.90 +val atp_important_message_keep_factor = 0.1
    7.91  
    7.92 -fun run_atp auto name
    7.93 -        ({exec, required_execs, arguments, has_incomplete_mode, proof_delims,
    7.94 -          known_failures, explicit_forall, use_conjecture_for_hypotheses, ...}
    7.95 -          : atp_config)
    7.96 -        ({debug, verbose, overlord, monomorphize, monomorphize_limit, type_sys,
    7.97 -          explicit_apply, isar_proof, isar_shrink_factor, timeout, ...}
    7.98 -         : params)
    7.99 +fun run_atp auto may_slice name
   7.100 +        ({exec, required_execs, arguments, slices, proof_delims, known_failures,
   7.101 +          explicit_forall, use_conjecture_for_hypotheses, ...} : atp_config)
   7.102 +        ({debug, verbose, overlord, max_relevant, monomorphize,
   7.103 +          monomorphize_limit, type_sys, explicit_apply, isar_proof,
   7.104 +          isar_shrink_factor, slicing, timeout, ...} : params)
   7.105          minimize_command ({state, goal, subgoal, facts, ...} : prover_problem) =
   7.106    let
   7.107      val thy = Proof.theory_of state
   7.108      val ctxt = Proof.context_of state
   7.109      val (_, hyp_ts, concl_t) = strip_subgoal goal subgoal
   7.110 +    val slicing = may_slice andalso slicing
   7.111      fun monomorphize_facts facts =
   7.112        let
   7.113          val repair_context =
   7.114 @@ -400,27 +402,55 @@
   7.115          if File.exists command then
   7.116            let
   7.117              val readable_names = debug andalso overlord
   7.118 -            val (atp_problem, pool, conjecture_offset, fact_names) =
   7.119 -              prepare_atp_problem ctxt readable_names explicit_forall type_sys
   7.120 -                                  explicit_apply hyp_ts concl_t facts
   7.121 -            val ss = tptp_strings_for_atp_problem use_conjecture_for_hypotheses
   7.122 -                                                  atp_problem
   7.123 -            val _ = File.write_list prob_file ss
   7.124 -            val conjecture_shape =
   7.125 -              conjecture_offset + 1 upto conjecture_offset + length hyp_ts + 1
   7.126 -              |> map single
   7.127 -            fun run complete timeout =
   7.128 +            (* If slicing is disabled, we expand the last slice to fill the
   7.129 +               entire time available. *)
   7.130 +            val actual_slices = get_slices slicing (slices ())
   7.131 +            val num_actual_slices = length actual_slices
   7.132 +            fun run_slice (slice, (time_frac, (complete, default_max_relevant)))
   7.133 +                          time_left =
   7.134                let
   7.135 +                val num_facts =
   7.136 +                  length facts |> is_none max_relevant
   7.137 +                                  ? Integer.min default_max_relevant
   7.138 +                val real_ms = Real.fromInt o Time.toMilliseconds
   7.139 +                val slice_timeout =
   7.140 +                  ((real_ms time_left
   7.141 +                    |> (if slice < num_actual_slices - 1 then
   7.142 +                          curry Real.min (time_frac * real_ms timeout)
   7.143 +                        else
   7.144 +                          I))
   7.145 +                   * 0.001) |> seconds
   7.146 +                val _ =
   7.147 +                  if verbose then
   7.148 +                    "ATP slice " ^ string_of_int (slice + 1) ^ " with " ^
   7.149 +                    string_of_int num_facts ^ " fact" ^ plural_s num_facts ^
   7.150 +                    " for " ^ string_from_time slice_timeout ^ "..."
   7.151 +                    |> Output.urgent_message
   7.152 +                  else
   7.153 +                    ()
   7.154 +                val (atp_problem, pool, conjecture_offset, fact_names) =
   7.155 +                  prepare_atp_problem ctxt readable_names explicit_forall
   7.156 +                                      type_sys explicit_apply hyp_ts concl_t
   7.157 +                                      (facts |> take num_facts)
   7.158                  fun weights () = atp_problem_weights atp_problem
   7.159                  val core =
   7.160                    File.shell_path command ^ " " ^
   7.161 -                  arguments complete timeout weights ^ " " ^
   7.162 +                  arguments slice slice_timeout weights ^ " " ^
   7.163                    File.shell_path prob_file
   7.164                  val command =
   7.165                    (if measure_run_time then
   7.166                       "TIMEFORMAT='%3R'; { time " ^ core ^ " ; }"
   7.167                     else
   7.168                       "exec " ^ core) ^ " 2>&1"
   7.169 +                val _ =
   7.170 +                  atp_problem
   7.171 +                  |> tptp_strings_for_atp_problem use_conjecture_for_hypotheses
   7.172 +                  |> cons ("% " ^ command ^ "\n")
   7.173 +                  |> File.write_list prob_file
   7.174 +                val conjecture_shape =
   7.175 +                  conjecture_offset + 1
   7.176 +                    upto conjecture_offset + length hyp_ts + 1
   7.177 +                  |> map single
   7.178                  val ((output, msecs), res_code) =
   7.179                    bash_output command
   7.180                    |>> (if overlord then
   7.181 @@ -431,26 +461,22 @@
   7.182                  val (tstplike_proof, outcome) =
   7.183                    extract_tstplike_proof_and_outcome debug verbose complete
   7.184                        res_code proof_delims known_failures output
   7.185 -              in (output, msecs, tstplike_proof, outcome) end
   7.186 -            val run_twice =
   7.187 -              has_incomplete_mode andalso not auto andalso
   7.188 -              length facts >= !atp_run_twice_threshold
   7.189 +              in
   7.190 +                ((pool, conjecture_shape, fact_names),
   7.191 +                 (output, msecs, tstplike_proof, outcome))
   7.192 +              end
   7.193              val timer = Timer.startRealTimer ()
   7.194 -            val result =
   7.195 -              run (not run_twice)
   7.196 -                 (if run_twice then
   7.197 -                    seconds (0.001 * !atp_first_iter_time_frac
   7.198 -                             * Real.fromInt (Time.toMilliseconds timeout))
   7.199 -                  else
   7.200 -                    timeout)
   7.201 -              |> run_twice
   7.202 -                 ? (fn (_, msecs0, _, SOME _) =>
   7.203 -                       run true (Time.- (timeout, Timer.checkRealTimer timer))
   7.204 -                       |> (fn (output, msecs, tstplike_proof, outcome) =>
   7.205 -                              (output, int_opt_add msecs0 msecs, tstplike_proof,
   7.206 -                               outcome))
   7.207 -                     | result => result)
   7.208 -          in ((pool, conjecture_shape, fact_names), result) end
   7.209 +            fun maybe_run_slice slice (_, (_, msecs0, _, SOME _)) =
   7.210 +                run_slice slice (Time.- (timeout, Timer.checkRealTimer timer))
   7.211 +                |> (fn (stuff, (output, msecs, tstplike_proof, outcome)) =>
   7.212 +                       (stuff, (output, int_opt_add msecs0 msecs,
   7.213 +                                tstplike_proof, outcome)))
   7.214 +              | maybe_run_slice _ result = result
   7.215 +          in
   7.216 +            ((Symtab.empty, [], Vector.fromList []),
   7.217 +             ("", SOME 0, "", SOME InternalError))
   7.218 +            |> fold maybe_run_slice actual_slices
   7.219 +          end
   7.220          else
   7.221            error ("Bad executable: " ^ Path.print command ^ ".")
   7.222  
   7.223 @@ -469,7 +495,7 @@
   7.224      val (conjecture_shape, fact_names) =
   7.225        repair_conjecture_shape_and_fact_names output conjecture_shape fact_names
   7.226      val important_message =
   7.227 -      if not auto andalso random () <= important_message_keep_factor then
   7.228 +      if not auto andalso random () <= atp_important_message_keep_factor then
   7.229          extract_important_message output
   7.230        else
   7.231          ""
   7.232 @@ -535,16 +561,19 @@
   7.233      UnknownError msg
   7.234  
   7.235  (* FUDGE *)
   7.236 -val smt_max_iters = Unsynchronized.ref 8
   7.237 -val smt_iter_fact_frac = Unsynchronized.ref 0.5
   7.238 -val smt_iter_time_frac = Unsynchronized.ref 0.5
   7.239 -val smt_iter_min_msecs = Unsynchronized.ref 5000
   7.240 +val smt_max_slices = Unsynchronized.ref 8
   7.241 +val smt_slice_fact_frac = Unsynchronized.ref 0.5
   7.242 +val smt_slice_time_frac = Unsynchronized.ref 0.5
   7.243 +val smt_slice_min_secs = Unsynchronized.ref 5
   7.244  
   7.245 -fun smt_filter_loop name ({debug, verbose, overlord, monomorphize_limit,
   7.246 -                           timeout, ...} : params)
   7.247 +fun smt_filter_loop may_slice name
   7.248 +                    ({debug, verbose, overlord, monomorphize_limit, timeout,
   7.249 +                      slicing, ...} : params)
   7.250                      state i smt_filter =
   7.251    let
   7.252      val ctxt = Proof.context_of state
   7.253 +    val slicing = may_slice andalso slicing
   7.254 +    val max_slices = if slicing then !smt_max_slices else 1
   7.255      val repair_context =
   7.256        select_smt_solver name
   7.257        #> Config.put SMT_Config.verbose debug
   7.258 @@ -559,23 +588,24 @@
   7.259        #> Config.put SMT_Config.monomorph_limit monomorphize_limit
   7.260      val state = state |> Proof.map_context repair_context
   7.261  
   7.262 -    fun iter timeout iter_num outcome0 time_so_far facts =
   7.263 +    fun do_slice timeout slice outcome0 time_so_far facts =
   7.264        let
   7.265          val timer = Timer.startRealTimer ()
   7.266          val ms = timeout |> Time.toMilliseconds
   7.267 -        val iter_timeout =
   7.268 -          if iter_num < !smt_max_iters then
   7.269 +        val slice_timeout =
   7.270 +          if slice < max_slices then
   7.271              Int.min (ms,
   7.272 -                Int.max (!smt_iter_min_msecs,
   7.273 -                    Real.ceil (!smt_iter_time_frac * Real.fromInt ms)))
   7.274 +                Int.max (1000 * !smt_slice_min_secs,
   7.275 +                    Real.ceil (!smt_slice_time_frac * Real.fromInt ms)))
   7.276              |> Time.fromMilliseconds
   7.277            else
   7.278              timeout
   7.279          val num_facts = length facts
   7.280          val _ =
   7.281            if verbose then
   7.282 -            "SMT iteration with " ^ string_of_int num_facts ^ " fact" ^
   7.283 -            plural_s num_facts ^ " for " ^ string_from_time iter_timeout ^ "..."
   7.284 +            "SMT slice with " ^ string_of_int num_facts ^ " fact" ^
   7.285 +            plural_s num_facts ^ " for " ^ string_from_time slice_timeout ^
   7.286 +            "..."
   7.287              |> Output.urgent_message
   7.288            else
   7.289              ()
   7.290 @@ -583,10 +613,10 @@
   7.291          val _ =
   7.292            if debug then Output.urgent_message "Invoking SMT solver..." else ()
   7.293          val (outcome, used_facts) =
   7.294 -          (case (iter_num, smt_filter) of
   7.295 +          (case (slice, smt_filter) of
   7.296               (1, SOME head) => head |> apsnd (apsnd repair_context)
   7.297             | _ => SMT_Solver.smt_filter_preprocess state facts i)
   7.298 -          |> SMT_Solver.smt_filter_apply iter_timeout
   7.299 +          |> SMT_Solver.smt_filter_apply slice_timeout
   7.300            |> (fn {outcome, used_facts} => (outcome, used_facts))
   7.301            handle exn => if Exn.is_interrupt exn then
   7.302                            reraise exn
   7.303 @@ -608,7 +638,7 @@
   7.304            case outcome of
   7.305              NONE => false
   7.306            | SOME (SMT_Failure.Counterexample _) => false
   7.307 -          | SOME SMT_Failure.Time_Out => iter_timeout <> timeout
   7.308 +          | SOME SMT_Failure.Time_Out => slice_timeout <> timeout
   7.309            | SOME (SMT_Failure.Abnormal_Termination code) =>
   7.310              (if verbose then
   7.311                 "The SMT solver invoked with " ^ string_of_int num_facts ^
   7.312 @@ -622,17 +652,19 @@
   7.313            | SOME (SMT_Failure.Other_Failure _) => true
   7.314          val timeout = Time.- (timeout, Timer.checkRealTimer timer)
   7.315        in
   7.316 -        if too_many_facts_perhaps andalso iter_num < !smt_max_iters andalso
   7.317 +        if too_many_facts_perhaps andalso slice < max_slices andalso
   7.318             num_facts > 0 andalso Time.> (timeout, Time.zeroTime) then
   7.319            let
   7.320 -            val n = Real.ceil (!smt_iter_fact_frac * Real.fromInt num_facts)
   7.321 -          in iter timeout (iter_num + 1) outcome0 time_so_far (take n facts) end
   7.322 +            val n = Real.ceil (!smt_slice_fact_frac * Real.fromInt num_facts)
   7.323 +          in
   7.324 +            do_slice timeout (slice + 1) outcome0 time_so_far (take n facts)
   7.325 +          end
   7.326          else
   7.327            {outcome = if is_none outcome then NONE else the outcome0,
   7.328             used_facts = used_facts,
   7.329             run_time_in_msecs = SOME (Time.toMilliseconds time_so_far)}
   7.330        end
   7.331 -  in iter timeout 1 NONE Time.zeroTime end
   7.332 +  in do_slice timeout 1 NONE Time.zeroTime end
   7.333  
   7.334  (* taken from "Mirabelle" and generalized *)
   7.335  fun can_apply timeout tac state i =
   7.336 @@ -652,9 +684,10 @@
   7.337              (Config.put Metis_Tactics.verbose debug
   7.338               #> (fn ctxt => Metis_Tactics.metis_tac ctxt ths)) state i
   7.339  
   7.340 -fun run_smt_solver auto name (params as {debug, verbose, ...}) minimize_command
   7.341 -        ({state, subgoal, subgoal_count, facts, smt_filter, ...}
   7.342 -         : prover_problem) =
   7.343 +fun run_smt_solver auto may_slice name (params as {debug, verbose, ...})
   7.344 +                   minimize_command
   7.345 +                   ({state, subgoal, subgoal_count, facts, smt_filter, ...}
   7.346 +                    : prover_problem) =
   7.347    let
   7.348      val ctxt = Proof.context_of state
   7.349      val thy = Proof.theory_of state
   7.350 @@ -662,7 +695,7 @@
   7.351      val facts = facts ~~ (0 upto num_facts - 1)
   7.352                  |> map (smt_weighted_fact thy num_facts)
   7.353      val {outcome, used_facts, run_time_in_msecs} =
   7.354 -      smt_filter_loop name params state subgoal smt_filter facts
   7.355 +      smt_filter_loop may_slice name params state subgoal smt_filter facts
   7.356      val (chained_lemmas, other_lemmas) = split_used_facts (map fst used_facts)
   7.357      val outcome = outcome |> Option.map failure_from_smt_failure
   7.358      val message =
   7.359 @@ -694,12 +727,12 @@
   7.360       run_time_in_msecs = run_time_in_msecs, message = message}
   7.361    end
   7.362  
   7.363 -fun get_prover ctxt auto name =
   7.364 +fun get_prover ctxt auto may_slice name =
   7.365    let val thy = Proof_Context.theory_of ctxt in
   7.366      if is_smt_prover ctxt name then
   7.367 -      run_smt_solver auto name
   7.368 +      run_smt_solver auto may_slice name
   7.369      else if member (op =) (supported_atps thy) name then
   7.370 -      run_atp auto name (get_atp thy name)
   7.371 +      run_atp auto may_slice name (get_atp thy name)
   7.372      else
   7.373        error ("No such prover: " ^ name ^ ".")
   7.374    end
     8.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Thu Apr 21 18:39:22 2011 +0200
     8.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Thu Apr 21 18:39:22 2011 +0200
     8.3 @@ -14,10 +14,10 @@
     8.4    type prover = Sledgehammer_Provers.prover
     8.5  
     8.6    val auto_minimize_min_facts : int Unsynchronized.ref
     8.7 -  val get_minimizing_prover : Proof.context -> bool -> string -> prover
     8.8 +  val get_minimizing_prover : Proof.context -> bool -> bool -> string -> prover
     8.9    val run_sledgehammer :
    8.10 -    params -> bool -> int -> relevance_override -> (string -> minimize_command)
    8.11 -    -> Proof.state -> bool * Proof.state
    8.12 +    params -> bool -> bool -> int -> relevance_override
    8.13 +    -> (string -> minimize_command) -> Proof.state -> bool * Proof.state
    8.14  end;
    8.15  
    8.16  structure Sledgehammer_Run : SLEDGEHAMMER_RUN =
    8.17 @@ -44,10 +44,10 @@
    8.18  
    8.19  val auto_minimize_min_facts = Unsynchronized.ref (!binary_min_facts)
    8.20  
    8.21 -fun get_minimizing_prover ctxt auto name
    8.22 +fun get_minimizing_prover ctxt auto may_slice name
    8.23          (params as {debug, verbose, explicit_apply, ...}) minimize_command
    8.24          (problem as {state, subgoal, subgoal_count, facts, ...}) =
    8.25 -  get_prover ctxt auto name params minimize_command problem
    8.26 +  get_prover ctxt auto may_slice name params minimize_command problem
    8.27    |> (fn result as {outcome, used_facts, run_time_in_msecs, message} =>
    8.28           if is_some outcome then
    8.29             result
    8.30 @@ -83,16 +83,18 @@
    8.31               | NONE => result
    8.32             end)
    8.33  
    8.34 -fun launch_prover
    8.35 -        (params as {debug, blocking, max_relevant, timeout, expect, ...})
    8.36 -        auto minimize_command only
    8.37 +fun launch_prover (params as {debug, blocking, max_relevant, slicing, timeout,
    8.38 +                              expect, ...})
    8.39 +        auto may_slice minimize_command only
    8.40          {state, goal, subgoal, subgoal_count, facts, smt_filter} name =
    8.41    let
    8.42      val ctxt = Proof.context_of state
    8.43 +    val slicing = may_slice andalso slicing
    8.44      val birth_time = Time.now ()
    8.45      val death_time = Time.+ (birth_time, timeout)
    8.46      val max_relevant =
    8.47 -      the_default (default_max_relevant_for_prover ctxt name) max_relevant
    8.48 +      max_relevant
    8.49 +      |> the_default (default_max_relevant_for_prover ctxt slicing name)
    8.50      val num_facts = length facts |> not only ? Integer.min max_relevant
    8.51      val desc =
    8.52        prover_description ctxt params name num_facts subgoal subgoal_count goal
    8.53 @@ -102,7 +104,8 @@
    8.54         smt_filter = smt_filter}
    8.55      fun really_go () =
    8.56        problem
    8.57 -      |> get_minimizing_prover ctxt auto name params (minimize_command name)
    8.58 +      |> get_minimizing_prover ctxt auto may_slice name params
    8.59 +                               (minimize_command name)
    8.60        |> (fn {outcome, message, ...} =>
    8.61               (if is_some outcome then "none" else "some" (* sic *), message))
    8.62      fun go () =
    8.63 @@ -166,9 +169,9 @@
    8.64  
    8.65  fun run_sledgehammer (params as {debug, blocking, provers, monomorphize,
    8.66                                   type_sys, relevance_thresholds, max_relevant,
    8.67 -                                 timeout, ...})
    8.68 -                     auto i (relevance_override as {only, ...}) minimize_command
    8.69 -                     state =
    8.70 +                                 slicing, timeout, ...})
    8.71 +                     auto may_slice i (relevance_override as {only, ...})
    8.72 +                     minimize_command state =
    8.73    if null provers then
    8.74      error "No prover is set."
    8.75    else case subgoal_count state of
    8.76 @@ -181,6 +184,7 @@
    8.77          state |> Proof.map_context (Config.put SMT_Config.verbose debug)
    8.78        val ctxt = Proof.context_of state
    8.79        val thy = Proof_Context.theory_of ctxt
    8.80 +      val slicing = may_slice andalso slicing
    8.81        val {facts = chained_ths, goal, ...} = Proof.goal state
    8.82        val (_, hyp_ts, concl_t) = strip_subgoal goal i
    8.83        val no_dangerous_types = types_dangerous_types type_sys
    8.84 @@ -201,7 +205,7 @@
    8.85               facts = facts,
    8.86               smt_filter = maybe_smt_filter
    8.87                    (fn () => map_filter (try dest_SMT_Weighted_Fact) facts) i}
    8.88 -          val launch = launch_prover params auto minimize_command only
    8.89 +          val launch = launch_prover params auto may_slice minimize_command only
    8.90          in
    8.91            if auto then
    8.92              fold (fn prover => fn (true, state) => (true, state)
    8.93 @@ -218,7 +222,8 @@
    8.94              case max_relevant of
    8.95                SOME n => n
    8.96              | NONE =>
    8.97 -              0 |> fold (Integer.max o default_max_relevant_for_prover ctxt)
    8.98 +              0 |> fold (Integer.max
    8.99 +                         o default_max_relevant_for_prover ctxt slicing)
   8.100                          provers
   8.101                  |> auto ? (fn n => n div auto_max_relevant_divisor)
   8.102            val is_built_in_const =
     9.1 --- a/src/HOL/ex/sledgehammer_tactics.ML	Thu Apr 21 18:39:22 2011 +0200
     9.2 +++ b/src/HOL/ex/sledgehammer_tactics.ML	Thu Apr 21 18:39:22 2011 +0200
     9.3 @@ -18,14 +18,14 @@
     9.4  fun run_atp force_full_types timeout i n ctxt goal name =
     9.5    let
     9.6      val chained_ths = [] (* a tactic has no chained ths *)
     9.7 -    val params as {type_sys, relevance_thresholds, max_relevant, ...} =
     9.8 +    val params as {type_sys, relevance_thresholds, max_relevant, slicing, ...} =
     9.9        ((if force_full_types then [("full_types", "true")] else [])
    9.10         @ [("timeout", string_of_int (Time.toSeconds timeout))])
    9.11         (* @ [("overlord", "true")] *)
    9.12        |> Sledgehammer_Isar.default_params ctxt
    9.13 -    val prover = Sledgehammer_Provers.get_prover ctxt false name
    9.14 +    val prover = Sledgehammer_Provers.get_prover ctxt false true name
    9.15      val default_max_relevant =
    9.16 -      Sledgehammer_Provers.default_max_relevant_for_prover ctxt name
    9.17 +      Sledgehammer_Provers.default_max_relevant_for_prover ctxt slicing name
    9.18      val is_built_in_const =
    9.19        Sledgehammer_Provers.is_built_in_const_for_prover ctxt name
    9.20      val relevance_fudge =