# HG changeset patch
# User blanchet
# Date 1411979979 -7200
# Node ID d919cde2569147f8e47361a715019e8dbfa1e285
# Parent  4d00caa0e4d742b8c8d05f14c5f184a1e583ff15
added options to Mirabelle

diff -r 4d00caa0e4d7 -r d919cde25691 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Mon Sep 29 10:39:39 2014 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Mon Sep 29 10:39:39 2014 +0200
@@ -23,6 +23,7 @@
 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)*)
@@ -316,7 +317,7 @@
 
 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)
@@ -325,9 +326,16 @@
 (* 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
@@ -349,8 +357,8 @@
 
 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
@@ -375,7 +383,7 @@
                   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),
@@ -386,6 +394,7 @@
            ("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)
@@ -471,6 +480,7 @@
     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
@@ -479,8 +489,8 @@
     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) =>
@@ -559,8 +569,12 @@
           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