tuning
authorblanchet
Mon May 02 22:52:15 2011 +0200 (2011-05-02)
changeset 42642f5b4b9d4acda
parent 42641 2cd4e6463842
child 42643 c7b71b55099b
tuning
src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML
src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
src/HOL/Tools/Sledgehammer/sledgehammer_run.ML
src/HOL/ex/sledgehammer_tactics.ML
src/HOL/ex/tptp_export.ML
     1.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Mon May 02 22:52:15 2011 +0200
     1.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Mon May 02 22:52:15 2011 +0200
     1.3 @@ -362,7 +362,7 @@
     1.4        st |> Proof.map_context
     1.5                  (change_dir dir
     1.6                   #> Config.put Sledgehammer_Provers.measure_run_time true)
     1.7 -    val params as {type_sys, relevance_thresholds, max_relevant, slicing, ...} =
     1.8 +    val params as {relevance_thresholds, max_relevant, slicing, ...} =
     1.9        Sledgehammer_Isar.default_params ctxt
    1.10            [("verbose", "true"),
    1.11             ("type_sys", type_sys),
     2.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML	Mon May 02 22:52:15 2011 +0200
     2.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML	Mon May 02 22:52:15 2011 +0200
     2.3 @@ -112,7 +112,7 @@
     2.4           val {context = ctxt, facts, goal} = Proof.goal pre
     2.5           val prover = AList.lookup (op =) args "prover"
     2.6                        |> the_default default_prover
     2.7 -         val {relevance_thresholds, type_sys, max_relevant, slicing, ...} =
     2.8 +         val {relevance_thresholds, max_relevant, slicing, ...} =
     2.9             Sledgehammer_Isar.default_params ctxt args
    2.10           val default_max_relevant =
    2.11             Sledgehammer_Provers.default_max_relevant_for_prover ctxt slicing
     3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Mon May 02 22:52:15 2011 +0200
     3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Mon May 02 22:52:15 2011 +0200
     3.3 @@ -642,7 +642,6 @@
     3.4                             timeout, slicing, ...} : params)
     3.5                      state i smt_filter =
     3.6    let
     3.7 -    val ctxt = Proof.context_of state
     3.8      val max_slices = if slicing then !smt_max_slices else 1
     3.9      val repair_context =
    3.10        select_smt_solver name
     4.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Mon May 02 22:52:15 2011 +0200
     4.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Mon May 02 22:52:15 2011 +0200
     4.3 @@ -164,9 +164,8 @@
     4.4  
     4.5  val auto_max_relevant_divisor = 2 (* FUDGE *)
     4.6  
     4.7 -fun run_sledgehammer (params as {debug, blocking, provers, type_sys,
     4.8 -                                 relevance_thresholds, max_relevant, slicing,
     4.9 -                                 timeout, ...})
    4.10 +fun run_sledgehammer (params as {debug, blocking, provers, relevance_thresholds,
    4.11 +                                 max_relevant, slicing, timeout, ...})
    4.12          auto i (relevance_override as {only, ...}) minimize_command state =
    4.13    if null provers then
    4.14      error "No prover is set."
     5.1 --- a/src/HOL/ex/sledgehammer_tactics.ML	Mon May 02 22:52:15 2011 +0200
     5.2 +++ b/src/HOL/ex/sledgehammer_tactics.ML	Mon May 02 22:52:15 2011 +0200
     5.3 @@ -18,7 +18,7 @@
     5.4  fun run_atp force_full_types timeout i n ctxt goal name =
     5.5    let
     5.6      val chained_ths = [] (* a tactic has no chained ths *)
     5.7 -    val params as {type_sys, relevance_thresholds, max_relevant, slicing, ...} =
     5.8 +    val params as {relevance_thresholds, max_relevant, slicing, ...} =
     5.9        ((if force_full_types then [("full_types", "true")] else [])
    5.10         @ [("timeout", string_of_int (Time.toSeconds timeout))])
    5.11         (* @ [("overlord", "true")] *)
     6.1 --- a/src/HOL/ex/tptp_export.ML	Mon May 02 22:52:15 2011 +0200
     6.2 +++ b/src/HOL/ex/tptp_export.ML	Mon May 02 22:52:15 2011 +0200
     6.3 @@ -23,7 +23,7 @@
     6.4  
     6.5  fun facts_of thy =
     6.6    Sledgehammer_Filter.all_facts (ProofContext.init_global thy) Symtab.empty
     6.7 -      true Sledgehammer_Provers.atp_relevance_fudge [] []
     6.8 +                                true [] []
     6.9  
    6.10  fun fold_body_thms f =
    6.11    let