added 'smt' option to control generation of 'by smt' proofs
authorblanchet
Mon Feb 03 17:13:31 2014 +0100 (2014-02-03 ago)
changeset 552881a4358d14ce2
parent 55287 ffa306239316
child 55289 30d874dc7000
added 'smt' option to control generation of 'by smt' proofs
src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML
src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML
src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML
src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML
src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Mon Feb 03 16:53:58 2014 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Mon Feb 03 17:13:31 2014 +0100
     1.3 @@ -96,6 +96,7 @@
     1.4     ("isar_proofs", "smart"),
     1.5     ("compress_isar", "10"),
     1.6     ("try0_isar", "true"),
     1.7 +   ("smt", "smart"),
     1.8     ("slice", "true"),
     1.9     ("minimize", "smart"),
    1.10     ("preplay_timeout", "2")]
    1.11 @@ -117,7 +118,8 @@
    1.12     ("no_isar_proofs", "isar_proofs"),
    1.13     ("dont_slice", "slice"),
    1.14     ("dont_minimize", "minimize"),
    1.15 -   ("dont_try0_isar", "try0_isar")]
    1.16 +   ("dont_try0_isar", "try0_isar"),
    1.17 +   ("no_smt", "smt")]
    1.18  
    1.19  val params_not_for_minimize =
    1.20    ["blocking", "fact_filter", "max_facts", "fact_thresholds", "slice", "minimize"];
    1.21 @@ -286,6 +288,7 @@
    1.22      val isar_proofs = lookup_option lookup_bool "isar_proofs"
    1.23      val compress_isar = Real.max (1.0, lookup_real "compress_isar")
    1.24      val try0_isar = lookup_bool "try0_isar"
    1.25 +    val smt = lookup_option lookup_bool "smt"
    1.26      val slice = mode <> Auto_Try andalso lookup_bool "slice"
    1.27      val minimize = if mode = Auto_Try then NONE else lookup_option lookup_bool "minimize"
    1.28      val timeout = lookup_time "timeout"
    1.29 @@ -297,8 +300,8 @@
    1.30       uncurried_aliases = uncurried_aliases, learn = learn, fact_filter = fact_filter,
    1.31       max_facts = max_facts, fact_thresholds = fact_thresholds, max_mono_iters = max_mono_iters,
    1.32       max_new_mono_instances = max_new_mono_instances, isar_proofs = isar_proofs,
    1.33 -     compress_isar = compress_isar, try0_isar = try0_isar, slice = slice, minimize = minimize,
    1.34 -     timeout = timeout, preplay_timeout = preplay_timeout, expect = expect}
    1.35 +     compress_isar = compress_isar, try0_isar = try0_isar, smt = smt, slice = slice,
    1.36 +     minimize = minimize, timeout = timeout, preplay_timeout = preplay_timeout, expect = expect}
    1.37    end
    1.38  
    1.39  fun get_params mode = extract_params mode o default_raw_params mode
     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Mon Feb 03 16:53:58 2014 +0100
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Mon Feb 03 17:13:31 2014 +0100
     2.3 @@ -16,8 +16,8 @@
     2.4    val trace : bool Config.T
     2.5  
     2.6    type isar_params =
     2.7 -    bool * (string option * string option) * Time.time * real * bool * bool
     2.8 -      * (term, string) atp_step list * thm
     2.9 +    bool * (string option * string option) * Time.time * real * bool * bool * bool
    2.10 +    * (term, string) atp_step list * thm
    2.11  
    2.12    val proof_text : Proof.context -> bool -> bool option -> (unit -> isar_params) -> int ->
    2.13      one_line_params -> string
    2.14 @@ -108,13 +108,14 @@
    2.15      end
    2.16  
    2.17  type isar_params =
    2.18 -  bool * (string option * string option) * Time.time * real * bool * bool
    2.19 -    * (term, string) atp_step list * thm
    2.20 +  bool * (string option * string option) * Time.time * real * bool * bool * bool
    2.21 +  * (term, string) atp_step list * thm
    2.22  
    2.23  val arith_methods =
    2.24    [Arith_Method, Simp_Method, Auto_Method, Fastforce_Method, Blast_Method, Force_Method,
    2.25     Algebra_Method, Metis_Method (NONE, NONE), Meson_Method]
    2.26 -val datatype_methods = [Simp_Method, Simp_Size_Method]
    2.27 +val datatype_methods =
    2.28 +  [Simp_Method, Simp_Size_Method]
    2.29  val metislike_methods0 =
    2.30    [Metis_Method (NONE, NONE), Simp_Method, Auto_Method, Arith_Method, Blast_Method,
    2.31     Fastforce_Method, Force_Method, Algebra_Method, Meson_Method,
    2.32 @@ -122,19 +123,23 @@
    2.33  val rewrite_methods =
    2.34    [Auto_Method, Simp_Method, Fastforce_Method, Force_Method, Metis_Method (NONE, NONE),
    2.35     Meson_Method]
    2.36 -val skolem_methods = [Metis_Method (NONE, NONE), Blast_Method, Meson_Method]
    2.37 +val skolem_methods =
    2.38 +  [Metis_Method (NONE, NONE), Blast_Method, Meson_Method]
    2.39  
    2.40  fun isar_proof_text ctxt debug isar_proofs isar_params
    2.41      (one_line_params as (_, _, _, _, subgoal, subgoal_count)) =
    2.42    let
    2.43      fun isar_proof_of () =
    2.44        let
    2.45 -        val SOME (verbose, alt_metis_args, preplay_timeout, compress_isar, try0_isar, minimize,
    2.46 +        val SOME (verbose, alt_metis_args, preplay_timeout, compress_isar, try0_isar, smt, minimize,
    2.47            atp_proof, goal) = try isar_params ()
    2.48  
    2.49          val metislike_methods = insert (op =) (Metis_Method alt_metis_args) metislike_methods0
    2.50  
    2.51 -        val massage_meths = not try0_isar ? single o hd
    2.52 +        fun massage_meths (meths as meth :: _) =
    2.53 +          if not try0_isar then [meth]
    2.54 +          else if smt then SMT_Method :: meths
    2.55 +          else meths
    2.56  
    2.57          val (params, _, concl_t) = strip_subgoal goal subgoal ctxt
    2.58          val fixes = map (fn (s, T) => (Binding.name s, SOME T, NoSyn)) params
     3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Mon Feb 03 16:53:58 2014 +0100
     3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Mon Feb 03 17:13:31 2014 +0100
     3.3 @@ -38,6 +38,7 @@
     3.4       isar_proofs : bool option,
     3.5       compress_isar : real,
     3.6       try0_isar : bool,
     3.7 +     smt : bool option,
     3.8       slice : bool,
     3.9       minimize : bool option,
    3.10       timeout : Time.time,
    3.11 @@ -71,7 +72,7 @@
    3.12    val extract_proof_method : params -> proof_method -> string * (string * string list) list
    3.13    val is_proof_method : string -> bool
    3.14    val is_atp : theory -> string -> bool
    3.15 -  val bunch_of_proof_methods : bool -> string -> proof_method list
    3.16 +  val bunch_of_proof_methods : bool -> bool -> string -> proof_method list
    3.17    val is_fact_chained : (('a * stature) * 'b) -> bool
    3.18    val filter_used_facts :
    3.19      bool -> (''a * stature) list -> ((''a * stature) * 'b) list ->
    3.20 @@ -146,6 +147,7 @@
    3.21     isar_proofs : bool option,
    3.22     compress_isar : real,
    3.23     try0_isar : bool,
    3.24 +   smt : bool option,
    3.25     slice : bool,
    3.26     minimize : bool option,
    3.27     timeout : Time.time,
    3.28 @@ -181,19 +183,17 @@
    3.29    | Try => "Sledgehammer (" ^ quote name ^ ") found a proof"
    3.30    | _ => "Try this")
    3.31  
    3.32 -fun bunch_of_proof_methods needs_full_types desperate_lam_trans =
    3.33 -  if needs_full_types then
    3.34 -    [Metis_Method (SOME full_type_enc, NONE),
    3.35 -     Metis_Method (SOME really_full_type_enc, NONE),
    3.36 -     Metis_Method (SOME full_type_enc, SOME desperate_lam_trans),
    3.37 -     Metis_Method (SOME really_full_type_enc, SOME desperate_lam_trans),
    3.38 -     SMT_Method]
    3.39 -  else
    3.40 -    [Metis_Method (NONE, NONE),
    3.41 -     Metis_Method (SOME full_type_enc, NONE),
    3.42 -     Metis_Method (SOME no_typesN, SOME desperate_lam_trans),
    3.43 -     Metis_Method (SOME really_full_type_enc, SOME desperate_lam_trans),
    3.44 -     SMT_Method]
    3.45 +fun bunch_of_proof_methods smt needs_full_types desperate_lam_trans =
    3.46 +  [Metis_Method (SOME full_type_enc, NONE)] @
    3.47 +  (if needs_full_types then
    3.48 +     [Metis_Method (SOME full_type_enc, NONE),
    3.49 +      Metis_Method (SOME really_full_type_enc, NONE),
    3.50 +      Metis_Method (SOME full_type_enc, SOME desperate_lam_trans)]
    3.51 +   else
    3.52 +     [Metis_Method (NONE, NONE),
    3.53 +      Metis_Method (SOME no_typesN, SOME desperate_lam_trans)]) @
    3.54 +  [Metis_Method (SOME really_full_type_enc, SOME desperate_lam_trans)] @
    3.55 +  (if smt then [SMT_Method] else [])
    3.56  
    3.57  fun extract_proof_method ({type_enc, lam_trans, ...} : params)
    3.58        (Metis_Method (type_enc', lam_trans')) =
    3.59 @@ -223,10 +223,9 @@
    3.60  fun filter_used_facts keep_chained used =
    3.61    filter ((member (op =) used o fst) orf (if keep_chained then is_fact_chained else K false))
    3.62  
    3.63 -fun play_one_line_proof mode debug verbose timeout pairs state i preferred meths =
    3.64 +fun play_one_line_proof mode debug verbose timeout pairs state i preferred (meths as meth :: _) =
    3.65    let
    3.66 -    fun get_preferred meths =
    3.67 -      if member (op =) meths preferred then preferred else List.last meths
    3.68 +    fun get_preferred meths = if member (op =) meths preferred then preferred else meth
    3.69    in
    3.70      if timeout = Time.zeroTime then
    3.71        (get_preferred meths, Not_Played)
     4.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Mon Feb 03 16:53:58 2014 +0100
     4.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Mon Feb 03 17:13:31 2014 +0100
     4.3 @@ -132,7 +132,7 @@
     4.4  fun run_atp mode name
     4.5      (params as {debug, verbose, overlord, type_enc, strict, lam_trans, uncurried_aliases,
     4.6         fact_filter, max_facts, max_mono_iters, max_new_mono_instances, isar_proofs, compress_isar,
     4.7 -       try0_isar, slice, minimize, timeout, preplay_timeout, ...})
     4.8 +       try0_isar, smt, slice, minimize, timeout, preplay_timeout, ...})
     4.9      minimize_command
    4.10      ({comment, state, goal, subgoal, subgoal_count, factss, ...} : prover_problem) =
    4.11    let
    4.12 @@ -347,7 +347,7 @@
    4.13            val used_facts = used_facts_in_atp_proof ctxt fact_names atp_proof
    4.14            val needs_full_types = is_typed_helper_used_in_atp_proof atp_proof
    4.15            val meths =
    4.16 -            bunch_of_proof_methods needs_full_types
    4.17 +            bunch_of_proof_methods (smt <> SOME false) needs_full_types
    4.18                (if atp_proof_prefers_lifting atp_proof then liftingN else hide_lamsN)
    4.19          in
    4.20            (used_facts,
    4.21 @@ -372,7 +372,7 @@
    4.22                        |> factify_atp_proof fact_names hyp_ts concl_t
    4.23                    in
    4.24                      (verbose, (metis_type_enc, metis_lam_trans), preplay_timeout, compress_isar,
    4.25 -                     try0_isar, minimize |> the_default true, atp_proof, goal)
    4.26 +                     try0_isar, smt = SOME true, minimize |> the_default true, atp_proof, goal)
    4.27                    end
    4.28                  val one_line_params =
    4.29                    (preplay, proof_banner mode name, used_facts,
     5.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML	Mon Feb 03 16:53:58 2014 +0100
     5.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML	Mon Feb 03 17:13:31 2014 +0100
     5.3 @@ -129,7 +129,7 @@
     5.4  fun print silent f = if silent then () else Output.urgent_message (f ())
     5.5  
     5.6  fun test_facts ({debug, verbose, overlord, spy, provers, max_mono_iters, max_new_mono_instances,
     5.7 -      type_enc, strict, lam_trans, uncurried_aliases, isar_proofs, compress_isar, try0_isar,
     5.8 +      type_enc, strict, lam_trans, uncurried_aliases, isar_proofs, compress_isar, try0_isar, smt,
     5.9        preplay_timeout, ...} : params)
    5.10      silent (prover : prover) timeout i n state goal facts =
    5.11    let
    5.12 @@ -144,7 +144,7 @@
    5.13         uncurried_aliases = uncurried_aliases, learn = false, fact_filter = NONE,
    5.14         max_facts = SOME (length facts), fact_thresholds = (1.01, 1.01),
    5.15         max_mono_iters = max_mono_iters, max_new_mono_instances = max_new_mono_instances,
    5.16 -       isar_proofs = isar_proofs, compress_isar = compress_isar, try0_isar = try0_isar,
    5.17 +       isar_proofs = isar_proofs, compress_isar = compress_isar, try0_isar = try0_isar, smt = smt,
    5.18         slice = false, minimize = SOME false, timeout = timeout, preplay_timeout = preplay_timeout,
    5.19         expect = ""}
    5.20      val problem =
    5.21 @@ -289,7 +289,7 @@
    5.22  fun adjust_proof_method_params override_params
    5.23      ({debug, verbose, overlord, spy, blocking, provers, type_enc, strict, lam_trans,
    5.24        uncurried_aliases, learn, fact_filter, max_facts, fact_thresholds, max_mono_iters,
    5.25 -      max_new_mono_instances, isar_proofs, compress_isar, try0_isar, slice, minimize, timeout,
    5.26 +      max_new_mono_instances, isar_proofs, compress_isar, try0_isar, smt, slice, minimize, timeout,
    5.27        preplay_timeout, expect} : params) =
    5.28    let
    5.29      fun lookup_override name default_value =
    5.30 @@ -305,8 +305,8 @@
    5.31       uncurried_aliases = uncurried_aliases, learn = learn, fact_filter = fact_filter,
    5.32       max_facts = max_facts, fact_thresholds = fact_thresholds, max_mono_iters = max_mono_iters,
    5.33       max_new_mono_instances = max_new_mono_instances, isar_proofs = isar_proofs,
    5.34 -     compress_isar = compress_isar, try0_isar = try0_isar, slice = slice, minimize = minimize,
    5.35 -     timeout = timeout, preplay_timeout = preplay_timeout, expect = expect}
    5.36 +     compress_isar = compress_isar, try0_isar = try0_isar, smt = smt, slice = slice,
    5.37 +     minimize = minimize, timeout = timeout, preplay_timeout = preplay_timeout, expect = expect}
    5.38    end
    5.39  
    5.40  fun maybe_minimize ctxt mode do_learn name (params as {verbose, isar_proofs, minimize, ...})
     6.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML	Mon Feb 03 16:53:58 2014 +0100
     6.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML	Mon Feb 03 17:13:31 2014 +0100
     6.3 @@ -212,8 +212,8 @@
     6.4      do_slice timeout 1 NONE Time.zeroTime
     6.5    end
     6.6  
     6.7 -fun run_smt_solver mode name (params as {debug, verbose, preplay_timeout, ...}) minimize_command
     6.8 -    ({state, goal, subgoal, subgoal_count, factss, ...} : prover_problem) =
     6.9 +fun run_smt_solver mode name (params as {debug, verbose, smt, preplay_timeout, ...})
    6.10 +    minimize_command ({state, goal, subgoal, subgoal_count, factss, ...} : prover_problem) =
    6.11    let
    6.12      val thy = Proof.theory_of state
    6.13      val ctxt = Proof.context_of state
    6.14 @@ -234,7 +234,7 @@
    6.15          NONE =>
    6.16          (Lazy.lazy (fn () =>
    6.17             play_one_line_proof mode debug verbose preplay_timeout used_pairs state subgoal
    6.18 -             SMT_Method (bunch_of_proof_methods false liftingN)),
    6.19 +             SMT_Method (bunch_of_proof_methods (smt <> SOME false) false liftingN)),
    6.20           fn preplay =>
    6.21              let
    6.22                val one_line_params =