src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML

   type stature = ATP_Problem_Generate.stature
   type type_enc = ATP_Problem_Generate.type_enc
   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
 
   datatype induction_rules = Include | Exclude | Instantiate
   val induction_rules_of_string : string -> induction_rules option

     {comment : string,
      state : Proof.state,
      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,
      used_from : fact list,
      preferred_methss : proof_method * proof_method list list,
      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
   val overlord_file_location_of_prover : string -> string * string
   val proof_banner : mode -> string -> string
   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
   val repair_monomorph_context : int option -> int -> int option -> int -> Proof.context ->
     Proof.context

   {comment : string,
    state : Proof.state,
    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,
    used_from : fact list,
    preferred_methss : proof_method * proof_method list list,
    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)
 
 fun proof_banner mode prover_name =
   (case mode of

         []
   in
     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 =
   filter ((member (eq_fst (op =)) used o fst) orf
     (if keep_chained then is_fact_chained else K false))