# HG changeset patch
# User blanchet
# Date 1391444011 -3600
# Node ID 1a4358d14ce252cb8c90a6f9e2bf4d28654c696d
# Parent  ffa30623931696c9566a35b080eebb7acc24af78
added 'smt' option to control generation of 'by smt' proofs

diff -r ffa306239316 -r 1a4358d14ce2 src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Mon Feb 03 16:53:58 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Mon Feb 03 17:13:31 2014 +0100
@@ -96,6 +96,7 @@
    ("isar_proofs", "smart"),
    ("compress_isar", "10"),
    ("try0_isar", "true"),
+   ("smt", "smart"),
    ("slice", "true"),
    ("minimize", "smart"),
    ("preplay_timeout", "2")]
@@ -117,7 +118,8 @@
    ("no_isar_proofs", "isar_proofs"),
    ("dont_slice", "slice"),
    ("dont_minimize", "minimize"),
-   ("dont_try0_isar", "try0_isar")]
+   ("dont_try0_isar", "try0_isar"),
+   ("no_smt", "smt")]
 
 val params_not_for_minimize =
   ["blocking", "fact_filter", "max_facts", "fact_thresholds", "slice", "minimize"];
@@ -286,6 +288,7 @@
     val isar_proofs = lookup_option lookup_bool "isar_proofs"
     val compress_isar = Real.max (1.0, lookup_real "compress_isar")
     val try0_isar = lookup_bool "try0_isar"
+    val smt = lookup_option lookup_bool "smt"
     val slice = mode <> Auto_Try andalso lookup_bool "slice"
     val minimize = if mode = Auto_Try then NONE else lookup_option lookup_bool "minimize"
     val timeout = lookup_time "timeout"
@@ -297,8 +300,8 @@
      uncurried_aliases = uncurried_aliases, learn = learn, fact_filter = fact_filter,
      max_facts = max_facts, fact_thresholds = fact_thresholds, max_mono_iters = max_mono_iters,
      max_new_mono_instances = max_new_mono_instances, isar_proofs = isar_proofs,
-     compress_isar = compress_isar, try0_isar = try0_isar, slice = slice, minimize = minimize,
-     timeout = timeout, preplay_timeout = preplay_timeout, expect = expect}
+     compress_isar = compress_isar, try0_isar = try0_isar, smt = smt, slice = slice,
+     minimize = minimize, timeout = timeout, preplay_timeout = preplay_timeout, expect = expect}
   end
 
 fun get_params mode = extract_params mode o default_raw_params mode
diff -r ffa306239316 -r 1a4358d14ce2 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Mon Feb 03 16:53:58 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Mon Feb 03 17:13:31 2014 +0100
@@ -16,8 +16,8 @@
   val trace : bool Config.T
 
   type isar_params =
-    bool * (string option * string option) * Time.time * real * bool * bool
-      * (term, string) atp_step list * thm
+    bool * (string option * string option) * Time.time * real * bool * bool * bool
+    * (term, string) atp_step list * thm
 
   val proof_text : Proof.context -> bool -> bool option -> (unit -> isar_params) -> int ->
     one_line_params -> string
@@ -108,13 +108,14 @@
     end
 
 type isar_params =
-  bool * (string option * string option) * Time.time * real * bool * bool
-    * (term, string) atp_step list * thm
+  bool * (string option * string option) * Time.time * real * bool * bool * bool
+  * (term, string) atp_step list * thm
 
 val arith_methods =
   [Arith_Method, Simp_Method, Auto_Method, Fastforce_Method, Blast_Method, Force_Method,
    Algebra_Method, Metis_Method (NONE, NONE), Meson_Method]
-val datatype_methods = [Simp_Method, Simp_Size_Method]
+val datatype_methods =
+  [Simp_Method, Simp_Size_Method]
 val metislike_methods0 =
   [Metis_Method (NONE, NONE), Simp_Method, Auto_Method, Arith_Method, Blast_Method,
    Fastforce_Method, Force_Method, Algebra_Method, Meson_Method,
@@ -122,19 +123,23 @@
 val rewrite_methods =
   [Auto_Method, Simp_Method, Fastforce_Method, Force_Method, Metis_Method (NONE, NONE),
    Meson_Method]
-val skolem_methods = [Metis_Method (NONE, NONE), Blast_Method, Meson_Method]
+val skolem_methods =
+  [Metis_Method (NONE, NONE), Blast_Method, Meson_Method]
 
 fun isar_proof_text ctxt debug isar_proofs isar_params
     (one_line_params as (_, _, _, _, subgoal, subgoal_count)) =
   let
     fun isar_proof_of () =
       let
-        val SOME (verbose, alt_metis_args, preplay_timeout, compress_isar, try0_isar, minimize,
+        val SOME (verbose, alt_metis_args, preplay_timeout, compress_isar, try0_isar, smt, minimize,
           atp_proof, goal) = try isar_params ()
 
         val metislike_methods = insert (op =) (Metis_Method alt_metis_args) metislike_methods0
 
-        val massage_meths = not try0_isar ? single o hd
+        fun massage_meths (meths as meth :: _) =
+          if not try0_isar then [meth]
+          else if smt then SMT_Method :: meths
+          else meths
 
         val (params, _, concl_t) = strip_subgoal goal subgoal ctxt
         val fixes = map (fn (s, T) => (Binding.name s, SOME T, NoSyn)) params
diff -r ffa306239316 -r 1a4358d14ce2 src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Mon Feb 03 16:53:58 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Mon Feb 03 17:13:31 2014 +0100
@@ -38,6 +38,7 @@
      isar_proofs : bool option,
      compress_isar : real,
      try0_isar : bool,
+     smt : bool option,
      slice : bool,
      minimize : bool option,
      timeout : Time.time,
@@ -71,7 +72,7 @@
   val extract_proof_method : params -> proof_method -> string * (string * string list) list
   val is_proof_method : string -> bool
   val is_atp : theory -> string -> bool
-  val bunch_of_proof_methods : bool -> string -> proof_method list
+  val bunch_of_proof_methods : bool -> bool -> string -> proof_method list
   val is_fact_chained : (('a * stature) * 'b) -> bool
   val filter_used_facts :
     bool -> (''a * stature) list -> ((''a * stature) * 'b) list ->
@@ -146,6 +147,7 @@
    isar_proofs : bool option,
    compress_isar : real,
    try0_isar : bool,
+   smt : bool option,
    slice : bool,
    minimize : bool option,
    timeout : Time.time,
@@ -181,19 +183,17 @@
   | Try => "Sledgehammer (" ^ quote name ^ ") found a proof"
   | _ => "Try this")
 
-fun bunch_of_proof_methods needs_full_types desperate_lam_trans =
-  if needs_full_types then
-    [Metis_Method (SOME full_type_enc, NONE),
-     Metis_Method (SOME really_full_type_enc, NONE),
-     Metis_Method (SOME full_type_enc, SOME desperate_lam_trans),
-     Metis_Method (SOME really_full_type_enc, SOME desperate_lam_trans),
-     SMT_Method]
-  else
-    [Metis_Method (NONE, NONE),
-     Metis_Method (SOME full_type_enc, NONE),
-     Metis_Method (SOME no_typesN, SOME desperate_lam_trans),
-     Metis_Method (SOME really_full_type_enc, SOME desperate_lam_trans),
-     SMT_Method]
+fun bunch_of_proof_methods smt needs_full_types desperate_lam_trans =
+  [Metis_Method (SOME full_type_enc, NONE)] @
+  (if needs_full_types then
+     [Metis_Method (SOME full_type_enc, NONE),
+      Metis_Method (SOME really_full_type_enc, NONE),
+      Metis_Method (SOME full_type_enc, SOME desperate_lam_trans)]
+   else
+     [Metis_Method (NONE, NONE),
+      Metis_Method (SOME no_typesN, SOME desperate_lam_trans)]) @
+  [Metis_Method (SOME really_full_type_enc, SOME desperate_lam_trans)] @
+  (if smt then [SMT_Method] else [])
 
 fun extract_proof_method ({type_enc, lam_trans, ...} : params)
       (Metis_Method (type_enc', lam_trans')) =
@@ -223,10 +223,9 @@
 fun filter_used_facts keep_chained used =
   filter ((member (op =) used o fst) orf (if keep_chained then is_fact_chained else K false))
 
-fun play_one_line_proof mode debug verbose timeout pairs state i preferred meths =
+fun play_one_line_proof mode debug verbose timeout pairs state i preferred (meths as meth :: _) =
   let
-    fun get_preferred meths =
-      if member (op =) meths preferred then preferred else List.last meths
+    fun get_preferred meths = if member (op =) meths preferred then preferred else meth
   in
     if timeout = Time.zeroTime then
       (get_preferred meths, Not_Played)
diff -r ffa306239316 -r 1a4358d14ce2 src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Mon Feb 03 16:53:58 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Mon Feb 03 17:13:31 2014 +0100
@@ -132,7 +132,7 @@
 fun run_atp mode name
     (params as {debug, verbose, overlord, type_enc, strict, lam_trans, uncurried_aliases,
        fact_filter, max_facts, max_mono_iters, max_new_mono_instances, isar_proofs, compress_isar,
-       try0_isar, slice, minimize, timeout, preplay_timeout, ...})
+       try0_isar, smt, slice, minimize, timeout, preplay_timeout, ...})
     minimize_command
     ({comment, state, goal, subgoal, subgoal_count, factss, ...} : prover_problem) =
   let
@@ -347,7 +347,7 @@
           val used_facts = used_facts_in_atp_proof ctxt fact_names atp_proof
           val needs_full_types = is_typed_helper_used_in_atp_proof atp_proof
           val meths =
-            bunch_of_proof_methods needs_full_types
+            bunch_of_proof_methods (smt <> SOME false) needs_full_types
               (if atp_proof_prefers_lifting atp_proof then liftingN else hide_lamsN)
         in
           (used_facts,
@@ -372,7 +372,7 @@
                       |> factify_atp_proof fact_names hyp_ts concl_t
                   in
                     (verbose, (metis_type_enc, metis_lam_trans), preplay_timeout, compress_isar,
-                     try0_isar, minimize |> the_default true, atp_proof, goal)
+                     try0_isar, smt = SOME true, minimize |> the_default true, atp_proof, goal)
                   end
                 val one_line_params =
                   (preplay, proof_banner mode name, used_facts,
diff -r ffa306239316 -r 1a4358d14ce2 src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML	Mon Feb 03 16:53:58 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML	Mon Feb 03 17:13:31 2014 +0100
@@ -129,7 +129,7 @@
 fun print silent f = if silent then () else Output.urgent_message (f ())
 
 fun test_facts ({debug, verbose, overlord, spy, provers, max_mono_iters, max_new_mono_instances,
-      type_enc, strict, lam_trans, uncurried_aliases, isar_proofs, compress_isar, try0_isar,
+      type_enc, strict, lam_trans, uncurried_aliases, isar_proofs, compress_isar, try0_isar, smt,
       preplay_timeout, ...} : params)
     silent (prover : prover) timeout i n state goal facts =
   let
@@ -144,7 +144,7 @@
        uncurried_aliases = uncurried_aliases, learn = false, fact_filter = NONE,
        max_facts = SOME (length facts), fact_thresholds = (1.01, 1.01),
        max_mono_iters = max_mono_iters, max_new_mono_instances = max_new_mono_instances,
-       isar_proofs = isar_proofs, compress_isar = compress_isar, try0_isar = try0_isar,
+       isar_proofs = isar_proofs, compress_isar = compress_isar, try0_isar = try0_isar, smt = smt,
        slice = false, minimize = SOME false, timeout = timeout, preplay_timeout = preplay_timeout,
        expect = ""}
     val problem =
@@ -289,7 +289,7 @@
 fun adjust_proof_method_params override_params
     ({debug, verbose, overlord, spy, blocking, provers, type_enc, strict, lam_trans,
       uncurried_aliases, learn, fact_filter, max_facts, fact_thresholds, max_mono_iters,
-      max_new_mono_instances, isar_proofs, compress_isar, try0_isar, slice, minimize, timeout,
+      max_new_mono_instances, isar_proofs, compress_isar, try0_isar, smt, slice, minimize, timeout,
       preplay_timeout, expect} : params) =
   let
     fun lookup_override name default_value =
@@ -305,8 +305,8 @@
      uncurried_aliases = uncurried_aliases, learn = learn, fact_filter = fact_filter,
      max_facts = max_facts, fact_thresholds = fact_thresholds, max_mono_iters = max_mono_iters,
      max_new_mono_instances = max_new_mono_instances, isar_proofs = isar_proofs,
-     compress_isar = compress_isar, try0_isar = try0_isar, slice = slice, minimize = minimize,
-     timeout = timeout, preplay_timeout = preplay_timeout, expect = expect}
+     compress_isar = compress_isar, try0_isar = try0_isar, smt = smt, slice = slice,
+     minimize = minimize, timeout = timeout, preplay_timeout = preplay_timeout, expect = expect}
   end
 
 fun maybe_minimize ctxt mode do_learn name (params as {verbose, isar_proofs, minimize, ...})
diff -r ffa306239316 -r 1a4358d14ce2 src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML	Mon Feb 03 16:53:58 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML	Mon Feb 03 17:13:31 2014 +0100
@@ -212,8 +212,8 @@
     do_slice timeout 1 NONE Time.zeroTime
   end
 
-fun run_smt_solver mode name (params as {debug, verbose, preplay_timeout, ...}) minimize_command
-    ({state, goal, subgoal, subgoal_count, factss, ...} : prover_problem) =
+fun run_smt_solver mode name (params as {debug, verbose, smt, preplay_timeout, ...})
+    minimize_command ({state, goal, subgoal, subgoal_count, factss, ...} : prover_problem) =
   let
     val thy = Proof.theory_of state
     val ctxt = Proof.context_of state
@@ -234,7 +234,7 @@
         NONE =>
         (Lazy.lazy (fn () =>
            play_one_line_proof mode debug verbose preplay_timeout used_pairs state subgoal
-             SMT_Method (bunch_of_proof_methods false liftingN)),
+             SMT_Method (bunch_of_proof_methods (smt <> SOME false) false liftingN)),
          fn preplay =>
             let
               val one_line_params =