1.1 --- a/src/HOL/Tools/SMT/smt_solver.ML	Fri Dec 17 12:10:08 2010 +0100
     1.2 +++ b/src/HOL/Tools/SMT/smt_solver.ML	Fri Dec 17 15:30:43 2010 +0100
     1.3 @@ -33,7 +33,7 @@
     1.4    val default_max_relevant: Proof.context -> string -> int
     1.5  
     1.6    (*filter*)
     1.7 -  type 'a smt_filter_head_result = 'a list * (int option * thm) list *
     1.8 +  type 'a smt_filter_head_result = ('a list * (int option * thm) list) *
     1.9      (((int * thm) list * Proof.context) * (int * (int option * thm)) list)
    1.10    val smt_filter_head: Proof.state ->
    1.11      ('a * (int option * thm)) list -> int -> 'a smt_filter_head_result
    1.12 @@ -322,7 +322,7 @@
    1.13  
    1.14  fun mk_result outcome xrules = { outcome = outcome, used_facts = xrules }
    1.15  
    1.16 -type 'a smt_filter_head_result = 'a list * (int option * thm) list *
    1.17 +type 'a smt_filter_head_result = ('a list * (int option * thm) list) *
    1.18    (((int * thm) list * Proof.context) * (int * (int option * thm)) list)
    1.19  
    1.20  fun smt_filter_head st xwrules i =
    1.21 @@ -340,7 +340,7 @@
    1.22  
    1.23      val (xs, wthms) = split_list xwrules
    1.24    in
    1.25 -    (xs, wthms,
    1.26 +    ((xs, wthms),
    1.27       wthms
    1.28       |> map_index I
    1.29       |> append (map (pair ~1 o pair NONE) (Thm.assume cprop :: prems @ facts))
    1.30 @@ -349,7 +349,7 @@
    1.31    end
    1.32  
    1.33  fun smt_filter_tail time_limit run_remote
    1.34 -    (xs, wthms, ((iwthms', ctxt), iwthms)) =
    1.35 +    ((xs, wthms), ((iwthms', ctxt), iwthms)) =
    1.36    let
    1.37      val ctxt = ctxt |> Config.put C.timeout (Time.toReal time_limit)
    1.38      val xrules = xs ~~ map snd wthms

     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Fri Dec 17 12:10:08 2010 +0100
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Fri Dec 17 15:30:43 2010 +0100
     2.3 @@ -64,7 +64,7 @@
     2.4      val {goal, ...} = Proof.goal state
     2.5      val problem =
     2.6        {state = state, goal = goal, subgoal = i, subgoal_count = n,
     2.7 -       facts = facts}
     2.8 +       facts = facts, smt_head = NONE}
     2.9      val result as {outcome, used_facts, ...} = prover params (K "") problem
    2.10    in
    2.11      print silent

     3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Fri Dec 17 12:10:08 2010 +0100
     3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Fri Dec 17 15:30:43 2010 +0100
     3.3 @@ -33,14 +33,16 @@
     3.4    datatype prover_fact =
     3.5      Untranslated_Fact of (string * locality) * thm |
     3.6      ATP_Translated_Fact of
     3.7 -      translated_formula option * ((string * locality) * thm)
     3.8 +      translated_formula option * ((string * locality) * thm) |
     3.9 +    SMT_Weighted_Fact of (string * locality) * (int option * thm)
    3.10  
    3.11    type prover_problem =
    3.12      {state: Proof.state,
    3.13       goal: thm,
    3.14       subgoal: int,
    3.15       subgoal_count: int,
    3.16 -     facts: prover_fact list}
    3.17 +     facts: prover_fact list,
    3.18 +     smt_head: (string * locality) SMT_Solver.smt_filter_head_result option}
    3.19  
    3.20    type prover_result =
    3.21      {outcome: failure option,
    3.22 @@ -56,13 +58,9 @@
    3.23    val smt_iter_time_frac : real Unsynchronized.ref
    3.24    val smt_iter_min_msecs : int Unsynchronized.ref
    3.25    val smt_monomorph_limit : int Unsynchronized.ref
    3.26 -  val smt_weights : bool Unsynchronized.ref
    3.27 -  val smt_min_weight : int Unsynchronized.ref
    3.28 -  val smt_max_weight : int Unsynchronized.ref
    3.29 -  val smt_max_index : int Unsynchronized.ref
    3.30 -  val smt_weight_curve : (int -> int) Unsynchronized.ref
    3.31  
    3.32    val das_Tool : string
    3.33 +  val select_smt_solver : string -> Proof.context -> Proof.context
    3.34    val is_smt_prover : Proof.context -> string -> bool
    3.35    val is_prover_available : Proof.context -> string -> bool
    3.36    val is_prover_installed : Proof.context -> string -> bool
    3.37 @@ -76,6 +74,8 @@
    3.38    val problem_prefix : string Config.T
    3.39    val measure_run_time : bool Config.T
    3.40    val untranslated_fact : prover_fact -> (string * locality) * thm
    3.41 +  val smt_weighted_fact :
    3.42 +    prover_fact -> (string * locality) * (int option * thm)
    3.43    val available_provers : Proof.context -> unit
    3.44    val kill_provers : unit -> unit
    3.45    val running_provers : unit -> unit
    3.46 @@ -102,11 +102,16 @@
    3.47     "Async_Manager". *)
    3.48  val das_Tool = "Sledgehammer"
    3.49  
    3.50 +val unremotify = perhaps (try (unprefix remote_prefix))
    3.51 +
    3.52 +val select_smt_solver =
    3.53 +  Context.proof_map o SMT_Config.select_solver o unremotify
    3.54 +
    3.55  fun is_smt_prover ctxt name =
    3.56    let val smts = SMT_Solver.available_solvers_of ctxt in
    3.57      case try (unprefix remote_prefix) name of
    3.58 -      SOME suffix => member (op =) smts suffix andalso
    3.59 -                     SMT_Solver.is_remotely_available ctxt suffix
    3.60 +      SOME base => member (op =) smts base andalso
    3.61 +                   SMT_Solver.is_remotely_available ctxt base
    3.62      | NONE => member (op =) smts name
    3.63    end
    3.64  
    3.65 @@ -133,8 +138,7 @@
    3.66  fun default_max_relevant_for_prover ctxt name =
    3.67    let val thy = ProofContext.theory_of ctxt in
    3.68      if is_smt_prover ctxt name then
    3.69 -      SMT_Solver.default_max_relevant ctxt
    3.70 -          (perhaps (try (unprefix remote_prefix)) name)
    3.71 +      SMT_Solver.default_max_relevant ctxt (unremotify name)
    3.72      else
    3.73        #default_max_relevant (get_atp thy name)
    3.74    end
    3.75 @@ -146,9 +150,11 @@
    3.76     @{const_name conj}, @{const_name disj}, @{const_name implies},
    3.77     @{const_name HOL.eq}, @{const_name If}, @{const_name Let}]
    3.78  
    3.79 -fun is_built_in_const_for_prover ctxt name (s, T) args =
    3.80 -  if is_smt_prover ctxt name then SMT_Builtin.is_builtin_ext ctxt (s, T) args
    3.81 -  else member (op =) atp_irrelevant_consts s
    3.82 +fun is_built_in_const_for_prover ctxt name =
    3.83 +  if is_smt_prover ctxt name then
    3.84 +    ctxt |> select_smt_solver name |> SMT_Builtin.is_builtin_ext
    3.85 +  else
    3.86 +    K o member (op =) atp_irrelevant_consts o fst
    3.87  
    3.88  (* FUDGE *)
    3.89  val atp_relevance_fudge =
    3.90 @@ -230,14 +236,17 @@
    3.91  
    3.92  datatype prover_fact =
    3.93    Untranslated_Fact of (string * locality) * thm |
    3.94 -  ATP_Translated_Fact of translated_formula option * ((string * locality) * thm)
    3.95 +  ATP_Translated_Fact of
    3.96 +    translated_formula option * ((string * locality) * thm) |
    3.97 +  SMT_Weighted_Fact of (string * locality) * (int option * thm)
    3.98  
    3.99  type prover_problem =
   3.100    {state: Proof.state,
   3.101     goal: thm,
   3.102     subgoal: int,
   3.103     subgoal_count: int,
   3.104 -   facts: prover_fact list}
   3.105 +   facts: prover_fact list,
   3.106 +   smt_head: (string * locality) SMT_Solver.smt_filter_head_result option}
   3.107  
   3.108  type prover_result =
   3.109    {outcome: failure option,
   3.110 @@ -272,8 +281,12 @@
   3.111  
   3.112  fun untranslated_fact (Untranslated_Fact p) = p
   3.113    | untranslated_fact (ATP_Translated_Fact (_, p)) = p
   3.114 -fun atp_translated_fact ctxt (Untranslated_Fact p) = translate_atp_fact ctxt p
   3.115 -  | atp_translated_fact _ (ATP_Translated_Fact q) = q
   3.116 +  | untranslated_fact (SMT_Weighted_Fact (info, (_, th))) = (info, th)
   3.117 +fun atp_translated_fact _ (ATP_Translated_Fact p) = p
   3.118 +  | atp_translated_fact ctxt fact =
   3.119 +    translate_atp_fact ctxt (untranslated_fact fact)
   3.120 +fun smt_weighted_fact (SMT_Weighted_Fact p) = p
   3.121 +  | smt_weighted_fact fact = untranslated_fact fact |> apsnd (pair NONE)
   3.122  
   3.123  fun int_opt_add (SOME m) (SOME n) = SOME (m + n)
   3.124    | int_opt_add _ _ = NONE
   3.125 @@ -471,9 +484,26 @@
   3.126  val smt_iter_min_msecs = Unsynchronized.ref 5000
   3.127  val smt_monomorph_limit = Unsynchronized.ref 4
   3.128  
   3.129 -fun smt_filter_loop ({debug, verbose, timeout, ...} : params) remote state i =
   3.130 +fun smt_filter_loop name ({debug, verbose, overlord, timeout, ...} : params)
   3.131 +                    state i smt_head =
   3.132    let
   3.133      val ctxt = Proof.context_of state
   3.134 +    val (remote, base) =
   3.135 +      case try (unprefix remote_prefix) name of
   3.136 +        SOME base => (true, base)
   3.137 +      | NONE => (false, name)
   3.138 +    val repair_context =
   3.139 +      select_smt_solver base
   3.140 +      #> Config.put SMT_Config.verbose debug
   3.141 +      #> (if overlord then
   3.142 +            Config.put SMT_Config.debug_files
   3.143 +                       (overlord_file_location_for_prover name
   3.144 +                        |> (fn (path, base) => path ^ "/" ^ base))
   3.145 +          else
   3.146 +            I)
   3.147 +      #> Config.put SMT_Config.monomorph_limit (!smt_monomorph_limit)
   3.148 +    val state = state |> Proof.map_context repair_context
   3.149 +
   3.150      fun iter timeout iter_num outcome0 time_so_far facts =
   3.151        let
   3.152          val timer = Timer.startRealTimer ()
   3.153 @@ -498,7 +528,9 @@
   3.154          val _ =
   3.155            if debug then Output.urgent_message "Invoking SMT solver..." else ()
   3.156          val (outcome, used_facts) =
   3.157 -          SMT_Solver.smt_filter_head state facts i
   3.158 +          (case (iter_num, smt_head) of
   3.159 +             (1, SOME head) => head |> apsnd (apfst (apsnd repair_context))
   3.160 +           | _ => SMT_Solver.smt_filter_head state facts i)
   3.161            |> SMT_Solver.smt_filter_tail iter_timeout remote
   3.162            |> (fn {outcome, used_facts} => (outcome, used_facts))
   3.163            handle exn => if Exn.is_interrupt exn then
   3.164 @@ -565,53 +597,14 @@
   3.165              (Config.put Metis_Tactics.verbose debug
   3.166               #> (fn ctxt => Metis_Tactics.metis_tac ctxt ths)) state i
   3.167  
   3.168 -val smt_weights = Unsynchronized.ref true
   3.169 -val smt_weight_min_facts = 20
   3.170 -
   3.171 -(* FUDGE *)
   3.172 -val smt_min_weight = Unsynchronized.ref 0
   3.173 -val smt_max_weight = Unsynchronized.ref 10
   3.174 -val smt_max_index = Unsynchronized.ref 200
   3.175 -val smt_weight_curve = Unsynchronized.ref (fn x : int => x * x)
   3.176 -
   3.177 -fun smt_fact_weight j num_facts =
   3.178 -  if !smt_weights andalso num_facts >= smt_weight_min_facts then
   3.179 -    SOME (!smt_max_weight
   3.180 -          - (!smt_max_weight - !smt_min_weight + 1)
   3.181 -            * !smt_weight_curve (Int.max (0, !smt_max_index - j - 1))
   3.182 -            div !smt_weight_curve (!smt_max_index))
   3.183 -  else
   3.184 -    NONE
   3.185 -
   3.186 -fun run_smt_solver auto name (params as {debug, verbose, overlord, ...})
   3.187 -        minimize_command
   3.188 -        ({state, subgoal, subgoal_count, facts, ...} : prover_problem) =
   3.189 +fun run_smt_solver auto name (params as {debug, verbose, ...}) minimize_command
   3.190 +        ({state, subgoal, subgoal_count, facts, smt_head, ...}
   3.191 +         : prover_problem) =
   3.192    let
   3.193 -    val (remote, suffix) =
   3.194 -      case try (unprefix remote_prefix) name of
   3.195 -        SOME suffix => (true, suffix)
   3.196 -      | NONE => (false, name)
   3.197 -    val repair_context =
   3.198 -      Context.proof_map (SMT_Config.select_solver suffix)
   3.199 -      #> Config.put SMT_Config.verbose debug
   3.200 -      #> (if overlord then
   3.201 -            Config.put SMT_Config.debug_files
   3.202 -                       (overlord_file_location_for_prover name
   3.203 -                        |> (fn (path, base) => path ^ "/" ^ base))
   3.204 -          else
   3.205 -            I)
   3.206 -      #> Config.put SMT_Config.monomorph_limit (!smt_monomorph_limit)
   3.207 -    val state = state |> Proof.map_context repair_context
   3.208 -    val thy = Proof.theory_of state
   3.209 -    val num_facts = length facts
   3.210 -    val facts =
   3.211 -      facts ~~ (0 upto num_facts - 1)
   3.212 -      |> map (fn (fact, j) =>
   3.213 -                 fact |> untranslated_fact
   3.214 -                      |> apsnd (pair (smt_fact_weight j num_facts)
   3.215 -                                o Thm.transfer thy))
   3.216 +    val ctxt = Proof.context_of state
   3.217 +    val facts = facts |> map smt_weighted_fact
   3.218      val {outcome, used_facts, run_time_in_msecs} =
   3.219 -      smt_filter_loop params remote state subgoal facts
   3.220 +      smt_filter_loop name params state subgoal smt_head facts
   3.221      val (chained_lemmas, other_lemmas) = split_used_facts (map fst used_facts)
   3.222      val outcome = outcome |> Option.map failure_from_smt_failure
   3.223      val message =
   3.224 @@ -622,8 +615,10 @@
   3.225              if can_apply_metis debug state subgoal (map snd used_facts) then
   3.226                ("metis", "")
   3.227              else
   3.228 -              ("smt", if suffix = SMT_Config.solver_of @{context} then ""
   3.229 -                      else "smt_solver = " ^ maybe_quote suffix)
   3.230 +              let val base = unremotify name in
   3.231 +                ("smt", if base = SMT_Config.solver_of ctxt then ""
   3.232 +                        else "smt_solver = " ^ maybe_quote base)
   3.233 +              end
   3.234          in
   3.235            try_command_line (proof_banner auto)
   3.236                (apply_on_subgoal settings subgoal subgoal_count ^

     4.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Fri Dec 17 12:10:08 2010 +0100
     4.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Fri Dec 17 15:30:43 2010 +0100
     4.3 @@ -43,7 +43,7 @@
     4.4  
     4.5  fun run_prover (params as {debug, blocking, max_relevant, timeout, expect, ...})
     4.6                 auto minimize_command only
     4.7 -               {state, goal, subgoal, subgoal_count, facts} name =
     4.8 +               {state, goal, subgoal, subgoal_count, facts, smt_head} name =
     4.9    let
    4.10      val ctxt = Proof.context_of state
    4.11      val birth_time = Time.now ()
    4.12 @@ -56,7 +56,8 @@
    4.13      val prover = get_prover ctxt auto name
    4.14      val problem =
    4.15        {state = state, goal = goal, subgoal = subgoal,
    4.16 -       subgoal_count = subgoal_count, facts = take num_facts facts}
    4.17 +       subgoal_count = subgoal_count, facts = take num_facts facts,
    4.18 +       smt_head = smt_head}
    4.19      fun go () =
    4.20        let
    4.21          fun really_go () =
    4.22 @@ -115,6 +116,36 @@
    4.23         (false, state))
    4.24    end
    4.25  
    4.26 +val smt_weights = Unsynchronized.ref true
    4.27 +val smt_weight_min_facts = 20
    4.28 +
    4.29 +(* FUDGE *)
    4.30 +val smt_min_weight = Unsynchronized.ref 0
    4.31 +val smt_max_weight = Unsynchronized.ref 10
    4.32 +val smt_max_index = Unsynchronized.ref 200
    4.33 +val smt_weight_curve = Unsynchronized.ref (fn x : int => x * x)
    4.34 +
    4.35 +fun smt_fact_weight j num_facts =
    4.36 +  if !smt_weights andalso num_facts >= smt_weight_min_facts then
    4.37 +    SOME (!smt_max_weight
    4.38 +          - (!smt_max_weight - !smt_min_weight + 1)
    4.39 +            * !smt_weight_curve (Int.max (0, !smt_max_index - j - 1))
    4.40 +            div !smt_weight_curve (!smt_max_index))
    4.41 +  else
    4.42 +    NONE
    4.43 +
    4.44 +fun weight_smt_fact thy num_facts (fact, j) =
    4.45 +  fact |> apsnd (pair (smt_fact_weight j num_facts) o Thm.transfer thy)
    4.46 +
    4.47 +fun class_of_smt_solver ctxt name =
    4.48 +  ctxt |> select_smt_solver name
    4.49 +       |> SMT_Config.solver_class_of |> SMT_Utils.string_of_class
    4.50 +
    4.51 +(* Makes backtraces more transparent and might be more efficient as well. *)
    4.52 +fun smart_par_list_map _ [] = []
    4.53 +  | smart_par_list_map f [x] = [f x]
    4.54 +  | smart_par_list_map f xs = Par_List.map f xs
    4.55 +
    4.56  (* FUDGE *)
    4.57  val auto_max_relevant_divisor = 2
    4.58  
    4.59 @@ -129,7 +160,10 @@
    4.60    | n =>
    4.61      let
    4.62        val _ = Proof.assert_backward state
    4.63 +      val state =
    4.64 +        state |> Proof.map_context (Config.put SMT_Config.verbose debug)
    4.65        val ctxt = Proof.context_of state
    4.66 +      val thy = ProofContext.theory_of ctxt
    4.67        val {facts = chained_ths, goal, ...} = Proof.goal state
    4.68        val (_, hyp_ts, concl_t) = strip_subgoal goal i
    4.69        val no_dangerous_types = types_dangerous_types type_sys
    4.70 @@ -139,60 +173,83 @@
    4.71                | NONE => ()
    4.72        val _ = if auto then () else Output.urgent_message "Sledgehammering..."
    4.73        val (smts, atps) = provers |> List.partition (is_smt_prover ctxt)
    4.74 -      fun run_provers label no_dangerous_types relevance_fudge maybe_translate
    4.75 -                      provers (res as (success, state)) =
    4.76 +      fun run_provers get_facts translate maybe_smt_head provers
    4.77 +                      (res as (success, state)) =
    4.78          if success orelse null provers then
    4.79            res
    4.80          else
    4.81            let
    4.82 -            val max_max_relevant =
    4.83 -              case max_relevant of
    4.84 -                SOME n => n
    4.85 -              | NONE =>
    4.86 -                0 |> fold (Integer.max o default_max_relevant_for_prover ctxt)
    4.87 -                          provers
    4.88 -                  |> auto ? (fn n => n div auto_max_relevant_divisor)
    4.89 -            val is_built_in_const =
    4.90 -              is_built_in_const_for_prover ctxt (hd provers)
    4.91 -            val facts =
    4.92 -              relevant_facts ctxt no_dangerous_types relevance_thresholds
    4.93 -                             max_max_relevant is_built_in_const relevance_fudge
    4.94 -                             relevance_override chained_ths hyp_ts concl_t
    4.95 -              |> map maybe_translate
    4.96 +            val facts = get_facts ()
    4.97 +            val num_facts = length facts
    4.98 +            val facts = facts ~~ (0 upto num_facts - 1)
    4.99 +                        |> map (translate num_facts)
   4.100              val problem =
   4.101                {state = state, goal = goal, subgoal = i, subgoal_count = n,
   4.102 -               facts = facts}
   4.103 +               facts = facts,
   4.104 +               smt_head = maybe_smt_head (map smt_weighted_fact facts) i}
   4.105              val run_prover = run_prover params auto minimize_command only
   4.106            in
   4.107 -            if debug then
   4.108 -              Output.urgent_message (label ^ plural_s (length provers) ^ ": " ^
   4.109 -                  (if null facts then
   4.110 -                     "Found no relevant facts."
   4.111 -                   else
   4.112 -                     "Including (up to) " ^ string_of_int (length facts) ^
   4.113 -                     " relevant fact" ^ plural_s (length facts) ^ ":\n" ^
   4.114 -                     (facts |> map (fst o fst o untranslated_fact)
   4.115 -                            |> space_implode " ") ^ "."))
   4.116 -            else
   4.117 -              ();
   4.118              if auto then
   4.119                fold (fn prover => fn (true, state) => (true, state)
   4.120                                    | (false, _) => run_prover problem prover)
   4.121                     provers (false, state)
   4.122              else
   4.123                provers
   4.124 -              |> (if blocking andalso length provers > 1 then Par_List.map
   4.125 -                  else map)
   4.126 +              |> (if blocking then smart_par_list_map else map)
   4.127                       (run_prover problem)
   4.128                |> exists fst |> rpair state
   4.129            end
   4.130 +      fun get_facts label no_dangerous_types relevance_fudge provers =
   4.131 +        let
   4.132 +          val max_max_relevant =
   4.133 +            case max_relevant of
   4.134 +              SOME n => n
   4.135 +            | NONE =>
   4.136 +              0 |> fold (Integer.max o default_max_relevant_for_prover ctxt)
   4.137 +                        provers
   4.138 +                |> auto ? (fn n => n div auto_max_relevant_divisor)
   4.139 +          val is_built_in_const =
   4.140 +            is_built_in_const_for_prover ctxt (hd provers)
   4.141 +        in
   4.142 +          relevant_facts ctxt no_dangerous_types relevance_thresholds
   4.143 +                         max_max_relevant is_built_in_const relevance_fudge
   4.144 +                         relevance_override chained_ths hyp_ts concl_t
   4.145 +          |> tap (fn facts =>
   4.146 +                     if debug then
   4.147 +                       label ^ plural_s (length provers) ^ ": " ^
   4.148 +                       (if null facts then
   4.149 +                          "Found no relevant facts."
   4.150 +                        else
   4.151 +                          "Including (up to) " ^ string_of_int (length facts) ^
   4.152 +                          " relevant fact" ^ plural_s (length facts) ^ ":\n" ^
   4.153 +                          (facts |> map (fst o fst) |> space_implode " ") ^ ".")
   4.154 +                       |> Output.urgent_message
   4.155 +                     else
   4.156 +                       ())
   4.157 +        end
   4.158        val run_atps =
   4.159 -        run_provers "ATP" no_dangerous_types atp_relevance_fudge
   4.160 -                    (ATP_Translated_Fact o translate_atp_fact ctxt) atps
   4.161 -      val run_smts =
   4.162 -        run_provers "SMT solver" true smt_relevance_fudge Untranslated_Fact smts
   4.163 +        run_provers
   4.164 +            (get_facts "ATP" no_dangerous_types atp_relevance_fudge o K atps)
   4.165 +            (ATP_Translated_Fact oo K (translate_atp_fact ctxt o fst))
   4.166 +            (K (K NONE)) atps
   4.167 +      fun run_smts (accum as (success, _)) =
   4.168 +        if success orelse null smts then
   4.169 +          accum
   4.170 +        else
   4.171 +          let
   4.172 +            val facts = get_facts "SMT solver" true smt_relevance_fudge smts
   4.173 +            val translate = SMT_Weighted_Fact oo weight_smt_fact thy
   4.174 +            val maybe_smt_head = try o SMT_Solver.smt_filter_head state
   4.175 +          in
   4.176 +            smts |> map (`(class_of_smt_solver ctxt))
   4.177 +                 |> AList.group (op =)
   4.178 +                 |> map (fn (_, smts) => run_provers (K facts) translate
   4.179 +                                                     maybe_smt_head smts accum)
   4.180 +                 |> exists fst |> rpair state
   4.181 +          end
   4.182        fun run_atps_and_smt_solvers () =
   4.183 -        [run_atps, run_smts] |> Par_List.map (fn f => f (false, state) |> K ())
   4.184 +        [run_atps, run_smts]
   4.185 +        |> smart_par_list_map (fn f => f (false, state) |> K ())
   4.186          handle ERROR msg => (Output.urgent_message ("Error: " ^ msg); error msg)
   4.187      in
   4.188        (false, state)