# HG changeset patch
# User blanchet
# Date 1643641763 -3600
# Node ID f741d55a81e5ed7dc87f0cd07daaa3100439b364
# Parent  114eb0af123dde4dd219a5f25d84233efacdf518
thread slices through

diff -r 114eb0af123d -r f741d55a81e5 src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Mon Jan 31 16:09:23 2022 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Mon Jan 31 16:09:23 2022 +0100
@@ -137,31 +137,20 @@
         (used_facts |> filter_out (fn (_, (sc, _)) => sc = Chained), (meth, play)))
 
 fun launch_prover (params as {verbose, spy, max_facts, induction_rules, ...}) mode only learn
-    ({comment, state, goal, subgoal, subgoal_count, facts, found_proof} : prover_problem) name =
+    (problem as {state, subgoal, factss, ...} : prover_problem) slice name =
   let
     val ctxt = Proof.context_of state
 
     val _ = spying spy (fn () => (state, subgoal, name, "Launched"))
-    val max_facts = max_facts |> the_default (default_max_facts_of_prover ctxt name)
-    val num_facts = length (snd facts) |> not only ? Integer.min max_facts
     val induction_rules = the_default Exclude induction_rules
 
-    val problem =
-      {comment = comment, state = state, goal = goal, subgoal = subgoal,
-       subgoal_count = subgoal_count,
-       facts = facts
-         (* We take "num_facts" because "facts" contains the maximum of all called provers. *)
-         |> apsnd (take num_facts o maybe_filter_out_induction_rules induction_rules),
-       found_proof = found_proof}
-
     fun print_used_facts used_facts used_from =
       tag_list 1 used_from
       |> map (fn (j, fact) => fact |> apsnd (K j))
       |> filter_used_facts false used_facts
       |> map (fn ((name, _), j) => name ^ "@" ^ string_of_int j)
       |> commas
-      |> prefix ("Fact" ^ plural_s num_facts ^ " in " ^ name ^
-        " proof (of " ^ string_of_int num_facts ^ "): ")
+      |> prefix ("Facts in " ^ name ^ " proof: ")
       |> writeln
 
     fun spying_str_of_res ({outcome = NONE, used_facts, used_from, ...} : prover_result) =
@@ -185,19 +174,18 @@
             end
 
           val filter_infos =
-            map filter_info [("actual", used_from), facts]
+            map filter_info (("actual", used_from) :: factss)
             |> AList.group (op =)
             |> map (fn (indices, fact_filters) => commas fact_filters ^ ": " ^ indices)
         in
-          "Success: Found proof with " ^ string_of_int num_used_facts ^ " of " ^
-          string_of_int num_facts ^ " fact" ^ plural_s num_facts ^
+          "Success: Found proof with " ^ string_of_int num_used_facts ^ " fact" ^
+          plural_s num_used_facts ^
           (if num_used_facts = 0 then "" else ": " ^ commas filter_infos)
         end
       | spying_str_of_res {outcome = SOME failure, ...} =
         "Failure: " ^ string_of_atp_failure failure
  in
-  problem
-  |> get_minimizing_prover ctxt mode learn name params
+  get_minimizing_prover ctxt mode learn name params problem slice
   |> verbose ? tap (fn {outcome = NONE, used_facts as _ :: _, used_from, ...} =>
       print_used_facts used_facts used_from
     | _ => ())
@@ -235,13 +223,13 @@
   end
 
 fun launch_prover_and_preplay (params as {debug, timeout, expect, ...}) mode writeln_result only
-    learn (problem as {state, subgoal, ...}) prover_name =
+    learn (problem as {state, subgoal, ...}) slice prover_name =
   let
     val ctxt = Proof.context_of state
     val hard_timeout = Time.scale 5.0 timeout
 
     fun really_go () =
-      launch_prover params mode only learn problem prover_name
+      launch_prover params mode only learn problem slice prover_name
       |> preplay_prover_result params state subgoal
 
     fun go () =
@@ -342,23 +330,22 @@
 
         fun launch_provers () =
           let
-            val facts = hd (get_factss provers) (* temporary *)
             val problem =
               {comment = "", state = state, goal = goal, subgoal = i, subgoal_count = n,
-               facts = facts, found_proof = found_proof}
+               factss = get_factss provers, found_proof = found_proof}
             val learn = mash_learn_proof ctxt params (Thm.prop_of goal)
             val launch = launch_prover_and_preplay params mode writeln_result only learn
           in
             if mode = Auto_Try then
               (SH_Unknown, "")
               |> fold (fn prover =>
-                fn accum as (SH_Some _, _) => accum
-                 | _ => launch problem prover)
+                  fn accum as (SH_Some _, _) => accum
+                    | _ => launch problem (get_default_slice ctxt prover) prover)
                 provers
             else
               (learn chained_thms;
                provers
-               |> Par_List.map (launch problem)
+               |> Par_List.map (fn prover => launch problem (get_default_slice ctxt prover) prover)
                |> max_outcome)
           end
       in
diff -r 114eb0af123d -r f741d55a81e5 src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML	Mon Jan 31 16:09:23 2022 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML	Mon Jan 31 16:09:23 2022 +0100
@@ -12,7 +12,7 @@
   type atp_formula_role = ATP_Problem.atp_formula_role
   type atp_failure = ATP_Proof.atp_failure
 
-  type atp_slice_spec = (int * string) * atp_format * string * string * bool * string
+  type atp_slice = (int * string) * atp_format * string * string * bool * string
   type atp_config =
     {exec : string list * string list,
      arguments : Proof.context -> bool -> string -> Time.time -> Path.T ->
@@ -20,7 +20,7 @@
      proof_delims : (string * string) list,
      known_failures : (atp_failure * string) list,
      prem_role : atp_formula_role,
-     best_slices : Proof.context -> atp_slice_spec list,
+     best_slices : Proof.context -> atp_slice list,
      best_max_mono_iters : int,
      best_max_new_mono_instances : int}
 
@@ -46,7 +46,7 @@
   val spass_H2SOS : string
   val isabelle_scala_function: string list * string list
   val remote_atp : string -> string -> string list -> (string * string) list ->
-    (atp_failure * string) list -> atp_formula_role -> (Proof.context -> atp_slice_spec) ->
+    (atp_failure * string) list -> atp_formula_role -> (Proof.context -> atp_slice) ->
     string * (unit -> atp_config)
   val add_atp : string * (unit -> atp_config) -> theory -> theory
   val get_atp : theory -> string -> (unit -> atp_config)
@@ -76,7 +76,7 @@
 val default_max_mono_iters = 3 (* FUDGE *)
 val default_max_new_mono_instances = 100 (* FUDGE *)
 
-type atp_slice_spec = (int * string) * atp_format * string * string * bool * string
+type atp_slice = (int * string) * atp_format * string * string * bool * string
 
 type atp_config =
   {exec : string list * string list,
@@ -85,7 +85,7 @@
    proof_delims : (string * string) list,
    known_failures : (atp_failure * string) list,
    prem_role : atp_formula_role,
-   best_slices : Proof.context -> atp_slice_spec list,
+   best_slices : Proof.context -> atp_slice list,
    best_max_mono_iters : int,
    best_max_new_mono_instances : int}
 
diff -r 114eb0af123d -r f741d55a81e5 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Mon Jan 31 16:09:23 2022 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Mon Jan 31 16:09:23 2022 +0100
@@ -868,9 +868,10 @@
   let
     val problem =
       {comment = "Goal: " ^ goal_name, state = Proof.init ctxt, goal = goal, subgoal = 1,
-       subgoal_count = 1, facts = ("", facts), found_proof = K ()}
+       subgoal_count = 1, factss = [("", facts)], found_proof = K ()}
+    val slice = get_default_slice ctxt prover
   in
-    get_minimizing_prover ctxt MaSh (K ()) prover params problem
+    get_minimizing_prover ctxt MaSh (K ()) prover params problem slice
   end
 
 val bad_types = [\<^type_name>\<open>prop\<close>, \<^type_name>\<open>bool\<close>, \<^type_name>\<open>fun\<close>]
diff -r 114eb0af123d -r f741d55a81e5 src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Mon Jan 31 16:09:23 2022 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Mon Jan 31 16:09:23 2022 +0100
@@ -14,6 +14,7 @@
   type fact = Sledgehammer_Fact.fact
   type proof_method = Sledgehammer_Proof_Methods.proof_method
   type play_outcome = Sledgehammer_Proof_Methods.play_outcome
+  type atp_slice = Sledgehammer_ATP_Systems.atp_slice
 
   datatype mode = Auto_Try | Try | Normal | Minimize | MaSh
 
@@ -58,9 +59,13 @@
      goal : thm,
      subgoal : int,
      subgoal_count : int,
-     facts : string * fact list,
+     factss : (string * fact list) list,
      found_proof : string -> unit}
 
+  datatype prover_slice =
+    ATP_Slice of atp_slice
+  | SMT_Slice of int * string
+
   type prover_result =
     {outcome : atp_failure option,
      used_facts : (string * stature) list,
@@ -69,7 +74,7 @@
      run_time : Time.time,
      message : (unit -> (string * stature) list * (proof_method * play_outcome)) -> string}
 
-  type prover = params -> prover_problem -> prover_result
+  type prover = params -> prover_problem -> prover_slice -> prover_result
 
   val SledgehammerN : string
   val str_of_mode : mode -> string
@@ -78,6 +83,7 @@
   val is_atp : theory -> string -> bool
   val bunches_of_proof_methods : Proof.context -> bool -> bool -> bool -> string ->
     proof_method list list
+  val get_facts_of_filter : string -> (string * fact list) list -> fact list
   val is_fact_chained : (('a * stature) * 'b) -> bool
   val filter_used_facts : bool -> (''a * stature) list -> ((''a * stature) * 'b) list ->
     ((''a * stature) * 'b) list
@@ -190,9 +196,13 @@
    goal : thm,
    subgoal : int,
    subgoal_count : int,
-   facts : string * fact list,
+   factss : (string * fact list) list,
    found_proof : string -> unit}
 
+datatype prover_slice =
+  ATP_Slice of atp_slice
+| SMT_Slice of int * string
+
 type prover_result =
   {outcome : atp_failure option,
    used_facts : (string * stature) list,
@@ -201,7 +211,7 @@
    run_time : Time.time,
    message : (unit -> (string * stature) list * (proof_method * play_outcome)) -> string}
 
-type prover = params -> prover_problem -> prover_result
+type prover = params -> prover_problem -> prover_slice -> prover_result
 
 fun overlord_file_location_of_prover prover = (getenv "ISABELLE_HOME_USER", "prob_" ^ prover)
 
@@ -240,6 +250,11 @@
     try0_methodss @ [metis_methods] @ smt_methodss
   end
 
+fun get_facts_of_filter fact_filter factss =
+  (case AList.lookup (op =) factss fact_filter of
+    SOME facts => facts
+  | NONE => snd (hd factss))
+
 fun is_fact_chained ((_, (sc, _)), _) = sc = Chained
 
 fun filter_used_facts keep_chained used =
diff -r 114eb0af123d -r f741d55a81e5 src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Mon Jan 31 16:09:23 2022 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Mon Jan 31 16:09:23 2022 +0100
@@ -103,15 +103,19 @@
 val atp_important_message_keep_quotient = 25
 
 fun run_atp mode name
-    ({debug, verbose, overlord, type_enc, strict, lam_trans, uncurried_aliases, max_facts,
-      max_mono_iters, max_new_mono_instances, isar_proofs, compress, try0, smt_proofs, minimize,
-      slices, timeout, preplay_timeout, spy, ...} : params)
-    ({comment, state, goal, subgoal, subgoal_count, facts, found_proof} : prover_problem) =
+    ({debug, verbose, overlord, type_enc, strict, lam_trans, uncurried_aliases, fact_filter,
+      max_facts, max_mono_iters, max_new_mono_instances, isar_proofs, compress, try0, smt_proofs,
+      minimize, slices, timeout, preplay_timeout, spy, ...} : params)
+    ({comment, state, goal, subgoal, subgoal_count, factss, found_proof} : prover_problem)
+    slice =
   let
     val thy = Proof.theory_of state
     val ctxt = Proof.context_of state
 
-    val {exec, arguments, proof_delims, known_failures, prem_role, best_slices, best_max_mono_iters,
+    val ATP_Slice ((best_max_facts, best_fact_filter), format, best_type_enc, best_lam_trans,
+      best_uncurried_aliases, extra) = slice
+
+    val {exec, arguments, proof_delims, known_failures, prem_role, best_max_mono_iters,
       best_max_new_mono_instances, ...} = get_atp thy name ()
 
     val full_proofs = isar_proofs |> the_default (mode = Minimize)
@@ -158,10 +162,6 @@
 
     fun run () =
       let
-        val ((best_max_facts, _), format, best_type_enc, best_lam_trans, best_uncurried_aliases,
-            extra) =
-          List.last (best_slices ctxt)
-
         fun monomorphize_facts facts =
           let
             val ctxt =
@@ -183,7 +183,8 @@
             |> maps (fn (name, rths) => map (pair name o zero_var_indexes o snd) rths)
           end
 
-        val facts = snd facts
+        val effective_fact_filter = fact_filter |> the_default best_fact_filter
+        val facts = get_facts_of_filter effective_fact_filter factss
         val num_facts =
           (case max_facts of
             NONE => best_max_facts
diff -r 114eb0af123d -r f741d55a81e5 src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML	Mon Jan 31 16:09:23 2022 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML	Mon Jan 31 16:09:23 2022 +0100
@@ -13,11 +13,13 @@
   type mode = Sledgehammer_Prover.mode
   type params = Sledgehammer_Prover.params
   type prover = Sledgehammer_Prover.prover
+  type prover_slice = Sledgehammer_Prover.prover_slice
 
   val is_prover_supported : Proof.context -> string -> bool
   val is_prover_installed : Proof.context -> string -> bool
   val default_max_facts_of_prover : Proof.context -> string -> int
   val get_prover : Proof.context -> mode -> string -> prover
+  val get_default_slice : Proof.context -> string -> prover_slice
 
   val binary_min_facts : int Config.T
   val minimize_facts : (thm list -> unit) -> string -> params -> bool -> int -> int ->
@@ -68,6 +70,16 @@
     else error ("No such prover: " ^ name)
   end
 
+fun get_default_slice ctxt name =
+  let val thy = Proof_Context.theory_of ctxt in
+    if is_atp thy name then
+      ATP_Slice (List.last (#best_slices (get_atp thy name ()) ctxt))
+    else if is_smt_prover ctxt name then
+      SMT_Slice (SMT_Solver.default_max_relevant ctxt name, "")
+    else
+      error ("No such prover: " ^ name)
+  end
+
 (* wrapper for calling external prover *)
 
 fun n_facts names =
@@ -81,7 +93,7 @@
 fun test_facts ({debug, verbose, overlord, spy, provers, max_mono_iters, max_new_mono_instances,
       type_enc, strict, lam_trans, uncurried_aliases, isar_proofs, compress, try0, smt_proofs,
       minimize, preplay_timeout, induction_rules, ...} : params)
-    silent (prover : prover) timeout i n state goal facts =
+    slice silent (prover : prover) timeout i n state goal facts =
   let
     val _ = print silent (fn () => "Testing " ^ n_facts (map fst facts) ^
       (if verbose then " (timeout: " ^ string_of_time timeout ^ ")" else "") ^ "...")
@@ -98,10 +110,10 @@
        slices = 1, timeout = timeout, preplay_timeout = preplay_timeout, expect = ""}
     val problem =
       {comment = "", state = state, goal = goal, subgoal = i, subgoal_count = n,
-       facts = ("", facts), found_proof = K ()}
+       factss = [("", facts)], found_proof = K ()}
     val result0 as {outcome = outcome0, used_facts, used_from, preferred_methss, run_time,
         message} =
-      prover params problem
+      prover params problem slice
     val result as {outcome, ...} =
       if is_none outcome0 andalso
          forall (member (fn ((s, _), ((s', _), _)) => s = s') used_from) used_facts then
@@ -201,10 +213,11 @@
   let
     val ctxt = Proof.context_of state
     val prover = get_prover ctxt Minimize prover_name
+    val slice = get_default_slice ctxt prover_name
     val (chained, non_chained) = List.partition is_fact_chained facts
 
     fun test timeout non_chained =
-      test_facts params silent prover timeout i n state goal (chained @ non_chained)
+      test_facts params slice silent prover timeout i n state goal (chained @ non_chained)
   in
     (print silent (fn () => "Sledgehammer minimizer: " ^ prover_name);
      (case test timeout non_chained of
@@ -258,8 +271,8 @@
       | NONE => result)
     end
 
-fun get_minimizing_prover ctxt mode do_learn name params problem =
-  get_prover ctxt mode name params problem
+fun get_minimizing_prover ctxt mode do_learn name params problem slice =
+  get_prover ctxt mode name params problem slice
   |> maybe_minimize mode do_learn name params problem
 
 end;
diff -r 114eb0af123d -r f741d55a81e5 src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML	Mon Jan 31 16:09:23 2022 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML	Mon Jan 31 16:09:23 2022 +0100
@@ -109,13 +109,17 @@
     {outcome = outcome, filter_result = filter_result, used_from = facts, run_time = run_time}
   end
 
-fun run_smt_solver mode name (params as {debug, verbose, isar_proofs, compress, try0,
+fun run_smt_solver mode name (params as {debug, verbose, fact_filter, isar_proofs, compress, try0,
       smt_proofs, minimize, preplay_timeout, ...})
-    ({state, goal, subgoal, subgoal_count, facts, found_proof, ...} : prover_problem) =
+    ({state, goal, subgoal, subgoal_count, factss, found_proof, ...} : prover_problem)
+    slice =
   let
     val ctxt = Proof.context_of state
 
-    val facts = snd facts
+    val SMT_Slice (best_max_facts, best_fact_filter) = slice
+
+    val effective_fact_filter = fact_filter |> the_default best_fact_filter
+    val facts = get_facts_of_filter effective_fact_filter factss
 
     val {outcome, filter_result = {fact_ids, atp_proof, ...}, used_from, run_time} =
       smt_filter name params state goal subgoal facts
diff -r 114eb0af123d -r f741d55a81e5 src/HOL/Tools/Sledgehammer/sledgehammer_tactics.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_tactics.ML	Mon Jan 31 16:09:23 2022 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_tactics.ML	Mon Jan 31 16:09:23 2022 +0100
@@ -45,9 +45,10 @@
       |> hd |> snd
     val problem =
       {comment = "", state = Proof.init ctxt, goal = goal, subgoal = i, subgoal_count = n,
-       facts = ("", facts), found_proof = K ()}
+       factss = [("", facts)], found_proof = K ()}
+    val slice = get_default_slice ctxt name
   in
-    (case prover params problem of
+    (case prover params problem slice of
       {outcome = NONE, used_facts, ...} => used_facts |> map fst |> SOME
     | _ => NONE)
     handle ERROR message => (warning ("Error: " ^ message ^ "\n"); NONE)