src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML

 val max_factsK = "max_facts" (*=NUM: max. relevant clauses to use*)
 val max_relevantK = "max_relevant" (*=NUM: max. relevant clauses to use*)
 val max_callsK = "max_calls" (*=NUM: max. no. of calls to sledgehammer*)
 val preplay_timeoutK = "preplay_timeout" (*=TIME: timeout for finding reconstructed proof*)
 val isar_proofsK = "isar_proofs" (*: enable Isar proof generation*)
+val smt_proofsK = "smt_proofs" (*: enable SMT proof generation*)
 val minimizeK = "minimize" (*: instruct sledgehammer to run its minimizer*)
 
 val check_trivialK = "check_trivial" (*: check if goals are "trivial" (false by default)*)
 val fact_filterK = "fact_filter" (*=STRING: fact filter*)
 val type_encK = "type_enc" (*=STRING: type encoding scheme*)

     Sledgehammer_Prover_Minimize.get_minimizing_prover ctxt Sledgehammer_Prover.Normal learn name
   end
 
 type stature = ATP_Problem_Generate.stature
 
-fun good_line s =
+fun is_good_line s =
   (String.isSubstring " ms)" s orelse String.isSubstring " s)" s)
   andalso not (String.isSubstring "(> " s)
   andalso not (String.isSubstring ", > " s)
   andalso not (String.isSubstring "may fail" s)
 
 (* Fragile hack *)
 fun proof_method_from_msg args msg =
   (case AList.lookup (op =) args proof_methodK of
-    SOME name => name
+    SOME name =>
+    if name = "smart" then
+      if exists is_good_line (split_lines msg) then
+        "none"
+      else
+        "fail"
+    else
+      name
   | NONE =>
-    if exists good_line (split_lines msg) then
+    if exists is_good_line (split_lines msg) then
       "none" (* trust the preplayed proof *)
     else if String.isSubstring "metis (" msg then
       msg |> Substring.full
           |> Substring.position "metis ("
           |> snd |> Substring.position ")"

   SH_FAIL of int * int |
   SH_ERROR
 
 fun run_sh prover_name fact_filter type_enc strict max_facts slice
       lam_trans uncurried_aliases e_selection_heuristic term_order force_sos
-      hard_timeout timeout preplay_timeout isar_proofsLST minimizeLST
-      max_new_mono_instancesLST max_mono_itersLST dir pos st =
+      hard_timeout timeout preplay_timeout isar_proofsLST smt_proofsLST
+      minimizeLST max_new_mono_instancesLST max_mono_itersLST dir pos st =
   let
     val thy = Proof.theory_of st
     val {context = ctxt, facts = chained_ths, goal} = Proof.goal st
     val i = 1
     fun set_file_name (SOME dir) =

                   term_order |> the_default I)
             #> (Option.map (Config.put ATP_Systems.force_sos)
                   force_sos |> the_default I))
     val params as {max_facts, minimize, preplay_timeout, ...} =
       Sledgehammer_Commands.default_params thy
-         ([("verbose", "true"),
+         ([(* ("verbose", "true"), *)
            ("fact_filter", fact_filter),
            ("type_enc", type_enc),
            ("strict", strict),
            ("lam_trans", lam_trans |> the_default lam_trans_default),
            ("uncurried_aliases", uncurried_aliases |> the_default uncurried_aliases_default),
            ("max_facts", max_facts),
            ("slice", slice),
            ("timeout", string_of_int timeout),
            ("preplay_timeout", preplay_timeout)]
           |> isar_proofsLST
+          |> smt_proofsLST
           |> minimizeLST (*don't confuse the two minimization flags*)
           |> max_new_mono_instancesLST
           |> max_mono_itersLST)
     val default_max_facts =
       Sledgehammer_Prover_Minimize.default_max_facts_of_prover ctxt prover_name

     (* always use a hard timeout, but give some slack so that the automatic
        minimizer has a chance to do its magic *)
     val preplay_timeout = AList.lookup (op =) args preplay_timeoutK
       |> the_default preplay_timeout_default
     val isar_proofsLST = available_parameter args isar_proofsK "isar_proofs"
+    val smt_proofsLST = available_parameter args smt_proofsK "smt_proofs"
     val minimizeLST = available_parameter args minimizeK "minimize"
     val max_new_mono_instancesLST =
       available_parameter args max_new_mono_instancesK max_new_mono_instancesK
     val max_mono_itersLST = available_parameter args max_mono_itersK max_mono_itersK
     val hard_timeout = SOME (4 * timeout)
     val (msg, result) =
       run_sh prover_name fact_filter type_enc strict max_facts slice lam_trans
         uncurried_aliases e_selection_heuristic term_order force_sos
-        hard_timeout timeout preplay_timeout isar_proofsLST minimizeLST
-        max_new_mono_instancesLST max_mono_itersLST dir pos st
+        hard_timeout timeout preplay_timeout isar_proofsLST smt_proofsLST
+        minimizeLST max_new_mono_instancesLST max_mono_itersLST dir pos st
   in
     (case result of
       SH_OK (time_isa, time_prover, names) =>
         let
           fun get_thms (name, stature) =

               |>> the_default [ATP_Proof_Reconstruct.partial_typesN]
               ||> the_default ATP_Proof_Reconstruct.default_metis_lam_trans
           in Metis_Tactic.metis_tac type_encs lam_trans ctxt thms end
         else if !meth = "metis" then
           Metis_Tactic.metis_tac [] ATP_Proof_Reconstruct.default_metis_lam_trans ctxt thms
+        else if !meth = "none" then
+          K all_tac
+        else if !meth = "fail" then
+          K no_tac
         else
-          K all_tac
+          (warning ("Unknown method " ^ quote (!meth)); K no_tac)
       end
     fun apply_method named_thms =
       Mirabelle.can_apply timeout (do_method named_thms) st
 
     fun with_time (false, t) = "failed (" ^ string_of_int t ^ ")"