Added smt (verit) to Sledgehammer's proof preplay.
Tuned preplay multithreading.

--- a/CONTRIBUTORS	Thu Oct 29 18:23:29 2020 +0000
+++ b/CONTRIBUTORS	Thu Oct 29 16:07:41 2020 +0100
@@ -6,6 +6,9 @@
 Contributions to this Isabelle version
 --------------------------------------
 
+* October 2020: Jasmin Blanchette, Martin Desharnais, Mathias Fleury
+  Use veriT in proof preplay in Sledgehammer.
+
 * October 2020: Mathias Fleury
   Updated proof reconstruction for the SMT solver veriT in the smt method.
 

--- a/NEWS	Thu Oct 29 18:23:29 2020 +0000
+++ b/NEWS	Thu Oct 29 16:07:41 2020 +0100
@@ -166,6 +166,10 @@
 are in working order again, as opposed to outputting "GaveUp" on nearly
 all problems.
 
+* Sledgehammer:
+  - Use veriT in proof preplay.
+  - Take adventage of more cores in proof preplay.
+
 
 *** FOL ***
 

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Thu Oct 29 18:23:29 2020 +0000
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Thu Oct 29 16:07:41 2020 +0100
@@ -160,7 +160,7 @@
 
             fun massage_methods (meths as meth :: _) =
               if not try0 then [meth]
-              else if smt_proofs then SMT_Method :: meths
+              else if smt_proofs then SMT_Method SMT_Default :: meths
               else meths
 
             val (params, _, concl_t) = strip_subgoal goal subgoal ctxt

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML	Thu Oct 29 18:23:29 2020 +0000
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML	Thu Oct 29 16:07:41 2020 +0100
@@ -57,13 +57,15 @@
           else
             let val y = f timeout x in
               (case get_time y of
-                SOME time => next_timeout := time
+                SOME time => next_timeout := time_min (time, !next_timeout)
               | _ => ());
               SOME y
             end
         end
     in
-      map_filter I (Par_List.map apply_f xs)
+      chop_groups (Multithreading.max_threads ()) xs
+      |> map (map_filter I o Par_List.map apply_f)
+      |> flat
     end
 
 fun enrich_context_with_local_facts proof ctxt =

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML	Thu Oct 29 18:23:29 2020 +0000
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML	Thu Oct 29 16:07:41 2020 +0100
@@ -9,10 +9,14 @@
 sig
   type stature = ATP_Problem_Generate.stature
 
+  datatype SMT_backend =
+    SMT_Default |
+    SMT_Verit of string
+
   datatype proof_method =
     Metis_Method of string option * string option |
     Meson_Method |
-    SMT_Method |
+    SMT_Method of SMT_backend |
     SATx_Method |
     Blast_Method |
     Simp_Method |
@@ -48,10 +52,14 @@
 open ATP_Problem_Generate
 open ATP_Proof_Reconstruct
 
+datatype SMT_backend =
+  SMT_Default |
+  SMT_Verit of string
+
 datatype proof_method =
   Metis_Method of string option * string option |
   Meson_Method |
-  SMT_Method |
+  SMT_Method of SMT_backend |
   SATx_Method |
   Blast_Method |
   Simp_Method |
@@ -73,7 +81,7 @@
 
 fun is_proof_method_direct (Metis_Method _) = true
   | is_proof_method_direct Meson_Method = true
-  | is_proof_method_direct SMT_Method = true
+  | is_proof_method_direct (SMT_Method _) = true
   | is_proof_method_direct Simp_Method = true
   | is_proof_method_direct _ = false
 
@@ -93,7 +101,9 @@
       | Metis_Method (type_enc_opt, lam_trans_opt) =>
         "metis (" ^ commas (map_filter I [type_enc_opt, lam_trans_opt]) ^ ")"
       | Meson_Method => "meson"
-      | SMT_Method => "smt"
+      | SMT_Method SMT_Default => "smt"
+      | SMT_Method (SMT_Verit strategy) =>
+        "smt (" ^ commas ("verit" :: (if strategy = "default" then [] else [strategy])) ^ ")"
       | SATx_Method => "satx"
       | Blast_Method => "blast"
       | Simp_Method => if null ss then "simp" else "simp add:"
@@ -109,34 +119,41 @@
   end
 
 fun tac_of_proof_method ctxt (local_facts, global_facts) meth =
-  (case meth of
-    Metis_Method (type_enc_opt, lam_trans_opt) =>
-    let
-      val ctxt = ctxt
-        |> Config.put Metis_Tactic.verbose false
-        |> Config.put Metis_Tactic.trace false
-    in
-      SELECT_GOAL (Metis_Tactic.metis_method ((Option.map single type_enc_opt, lam_trans_opt),
-        global_facts) ctxt local_facts)
-    end
-  | SMT_Method => SMT_Solver.smt_tac ctxt (local_facts @ global_facts)
-  | _ =>
-    Method.insert_tac ctxt local_facts THEN'
+  let
+    fun tac_of_metis (type_enc_opt, lam_trans_opt) =
+      let
+        val ctxt = ctxt
+          |> Config.put Metis_Tactic.verbose false
+          |> Config.put Metis_Tactic.trace false
+      in
+        SELECT_GOAL (Metis_Tactic.metis_method ((Option.map single type_enc_opt, lam_trans_opt),
+          global_facts) ctxt local_facts)
+      end
+
+    fun tac_of_smt SMT_Default = SMT_Solver.smt_tac
+      | tac_of_smt (SMT_Verit strategy) = Verit_Proof.verit_tac_stgy strategy
+  in
     (case meth of
-      Meson_Method => Meson_Tactic.meson_general_tac ctxt global_facts
-    | Simp_Method => Simplifier.asm_full_simp_tac (ctxt addsimps global_facts)
+      Metis_Method options => tac_of_metis options
+    | SMT_Method backend => tac_of_smt backend ctxt (local_facts @ global_facts)
     | _ =>
-      Method.insert_tac ctxt global_facts THEN'
+      Method.insert_tac ctxt local_facts THEN'
       (case meth of
-        SATx_Method => SAT.satx_tac ctxt
-      | Blast_Method => blast_tac ctxt
-      | Auto_Method => SELECT_GOAL (Clasimp.auto_tac ctxt)
-      | Fastforce_Method => Clasimp.fast_force_tac ctxt
-      | Force_Method => Clasimp.force_tac ctxt
-      | Moura_Method => moura_tac ctxt
-      | Linarith_Method => Lin_Arith.tac ctxt
-      | Presburger_Method => Cooper.tac true [] [] ctxt
-      | Algebra_Method => Groebner.algebra_tac [] [] ctxt)))
+        Meson_Method => Meson_Tactic.meson_general_tac ctxt global_facts
+      | Simp_Method => Simplifier.asm_full_simp_tac (ctxt addsimps global_facts)
+      | _ =>
+        Method.insert_tac ctxt global_facts THEN'
+        (case meth of
+          SATx_Method => SAT.satx_tac ctxt
+        | Blast_Method => blast_tac ctxt
+        | Auto_Method => SELECT_GOAL (Clasimp.auto_tac ctxt)
+        | Fastforce_Method => Clasimp.fast_force_tac ctxt
+        | Force_Method => Clasimp.force_tac ctxt
+        | Moura_Method => moura_tac ctxt
+        | Linarith_Method => Lin_Arith.tac ctxt
+        | Presburger_Method => Cooper.tac true [] [] ctxt
+        | Algebra_Method => Groebner.algebra_tac [] [] ctxt)))
+  end
 
 fun string_of_play_outcome (Played time) = string_of_ext_time (false, time)
   | string_of_play_outcome (Play_Timed_Out time) =
@@ -158,7 +175,7 @@
   | apply_on_subgoal i n = "prefer " ^ string_of_int i ^ " " ^ apply_on_subgoal 1 n
 
 (* FIXME *)
-fun proof_method_command ctxt meth i n used_chaineds _(*num_chained*) extras =
+fun proof_method_command meth i n used_chaineds _(*num_chained*) extras =
   let
     val (indirect_ss, direct_ss) =
       if is_proof_method_direct meth then
@@ -177,11 +194,11 @@
     (s |> s <> "" ? enclose " (" ")")
   end
 
-fun one_line_proof_text ctxt num_chained
+fun one_line_proof_text _ num_chained
     ((used_facts, (meth, play)), banner, subgoal, subgoal_count) =
   let val (chained, extra) = List.partition (fn (_, (sc, _)) => sc = Chained) used_facts in
     map fst extra
-    |> proof_method_command ctxt meth subgoal subgoal_count (map fst chained) num_chained
+    |> proof_method_command meth subgoal subgoal_count (map fst chained) num_chained
     |> (if play = Play_Failed then prefix "One-line proof reconstruction failed: "
         else try_command_line banner play)
   end

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Thu Oct 29 18:23:29 2020 +0000
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Thu Oct 29 16:07:41 2020 +0100
@@ -67,7 +67,8 @@
   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 : bool -> bool -> bool -> string -> proof_method list list
+  val bunches_of_proof_methods : Proof.context -> bool -> bool -> bool -> string ->
+    proof_method list 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
@@ -155,23 +156,35 @@
   | Try => "Sledgehammer (" ^ quote name ^ ") found a proof"
   | _ => "Try this")
 
-fun bunches_of_proof_methods try0 smt_proofs needs_full_types desperate_lam_trans =
-  (if try0 then
-    [[Simp_Method, Auto_Method, Blast_Method, Linarith_Method],
-     [Meson_Method, Fastforce_Method, Force_Method, Presburger_Method]]
-   else
-     []) @
-  [[Metis_Method (if needs_full_types then SOME full_typesN else NONE, NONE)],
-   (if needs_full_types then
-      [Metis_Method (NONE, NONE),
-       Metis_Method (SOME really_full_type_enc, NONE),
-       Metis_Method (SOME full_typesN, SOME desperate_lam_trans),
-       Metis_Method (SOME really_full_type_enc, SOME desperate_lam_trans)]
-    else
-      [Metis_Method (SOME full_typesN, NONE),
-       Metis_Method (SOME no_typesN, SOME desperate_lam_trans),
-       Metis_Method (SOME really_full_type_enc, SOME desperate_lam_trans)])] @
-  (if smt_proofs then [[SMT_Method]] else [])
+fun bunches_of_proof_methods ctxt try0 smt_proofs needs_full_types desperate_lam_trans =
+  let
+    val try0_methodss =
+      if try0 then
+        [[Simp_Method, Auto_Method, Blast_Method, Linarith_Method, Meson_Method,
+          Metis_Method (NONE, NONE), Fastforce_Method, Force_Method, Presburger_Method]]
+      else
+        []
+
+    val metis_methods =
+      (if try0 then [] else [Metis_Method (NONE, NONE)]) @
+      Metis_Method (SOME full_typesN, NONE) ::
+      Metis_Method (SOME really_full_type_enc, SOME desperate_lam_trans) ::
+      (if needs_full_types then
+         [Metis_Method (SOME really_full_type_enc, NONE),
+          Metis_Method (SOME full_typesN, SOME desperate_lam_trans)]
+       else
+         [Metis_Method (SOME no_typesN, SOME desperate_lam_trans)])
+
+    val smt_methodss =
+      if smt_proofs then
+        [SMT_Method SMT_Default ::
+         map (fn strategy => SMT_Method (SMT_Verit strategy))
+           (Verit_Proof.all_veriT_stgies (Context.Proof ctxt))]
+      else
+        []
+  in
+    try0_methodss @ [metis_methods] @ smt_methodss
+  end
 
 fun is_fact_chained ((_, (sc, _)), _) = sc = Chained
 

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Thu Oct 29 18:23:29 2020 +0000
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Thu Oct 29 16:07:41 2020 +0100
@@ -360,7 +360,7 @@
           val needs_full_types = is_typed_helper_used_in_atp_proof atp_proof
           val preferred_methss =
             (Metis_Method (NONE, NONE),
-             bunches_of_proof_methods try0 smt_proofs needs_full_types
+             bunches_of_proof_methods ctxt try0 smt_proofs needs_full_types
               (if atp_proof_prefers_lifting atp_proof then liftingN else hide_lamsN))
         in
           (used_facts, preferred_methss,

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML	Thu Oct 29 18:23:29 2020 +0000
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML	Thu Oct 29 16:07:41 2020 +0100
@@ -200,11 +200,14 @@
         NONE =>
         let
           val _ = found_proof ();
-          val preferred_methss =
-            (if smt_proofs then SMT_Method else Metis_Method (NONE, NONE),
-             bunches_of_proof_methods try0 smt_proofs false liftingN)
+          val preferred =
+            if smt_proofs then
+              SMT_Method (if name = "verit" then SMT_Verit "default" else SMT_Default)
+            else
+              Metis_Method (NONE, NONE);
+          val methss = bunches_of_proof_methods ctxt try0 smt_proofs false liftingN;
         in
-          (preferred_methss,
+          ((preferred, methss),
            fn preplay =>
              let
                val _ = if verbose then writeln "Generating proof text..." else ()

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Thu Oct 29 18:23:29 2020 +0000
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Thu Oct 29 16:07:41 2020 +0100
@@ -14,6 +14,7 @@
   val simplify_spaces : string -> string
   val with_cleanup : ('a -> unit) -> ('a -> 'b) -> 'a -> 'b
   val time_mult : real -> Time.time -> Time.time
+  val time_min : Time.time * Time.time -> Time.time
   val parse_bool_option : bool -> string -> string -> bool option
   val parse_time : string -> string -> Time.time
   val subgoal_count : Proof.state -> int
@@ -49,6 +50,7 @@
   |> Exn.release
 
 fun time_mult k t = Time.fromMilliseconds (Real.ceil (k * Real.fromInt (Time.toMilliseconds t)))
+fun time_min (x, y) = if x < y then x else y
 
 fun parse_bool_option option name s =
   (case s of