tuning
authorblanchet
Fri Oct 22 18:31:45 2010 +0200 (2010-10-22)
changeset 40114acb75271cdce
parent 40113 1f61f0826e8a
child 40115 e5ed638e49b0
tuning
src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
src/HOL/Tools/Sledgehammer/sledgehammer.ML
src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML
src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML
     1.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Fri Oct 22 18:24:10 2010 +0200
     1.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Fri Oct 22 18:31:45 2010 +0200
     1.3 @@ -364,7 +364,7 @@
     1.4      val problem =
     1.5        {state = st', goal = goal, subgoal = i,
     1.6         subgoal_count = Sledgehammer_Util.subgoal_count st,
     1.7 -       axioms = axioms |> map Sledgehammer.Unprepared, only = true}
     1.8 +       axioms = axioms |> map Sledgehammer.Untranslated, only = true}
     1.9      val time_limit =
    1.10        (case hard_timeout of
    1.11          NONE => I
     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Fri Oct 22 18:24:10 2010 +0200
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Fri Oct 22 18:31:45 2010 +0200
     2.3 @@ -12,7 +12,7 @@
     2.4    type locality = Sledgehammer_Filter.locality
     2.5    type relevance_fudge = Sledgehammer_Filter.relevance_fudge
     2.6    type relevance_override = Sledgehammer_Filter.relevance_override
     2.7 -  type prepared_formula = Sledgehammer_ATP_Translate.prepared_formula
     2.8 +  type translated_formula = Sledgehammer_ATP_Translate.translated_formula
     2.9    type minimize_command = Sledgehammer_ATP_Reconstruct.minimize_command
    2.10  
    2.11    type params =
    2.12 @@ -31,8 +31,8 @@
    2.13       expect: string}
    2.14  
    2.15    datatype axiom =
    2.16 -    Unprepared of (string * locality) * thm |
    2.17 -    Prepared of term * ((string * locality) * prepared_formula) option
    2.18 +    Untranslated of (string * locality) * thm |
    2.19 +    Translated of term * ((string * locality) * translated_formula) option
    2.20  
    2.21    type prover_problem =
    2.22      {state: Proof.state,
    2.23 @@ -195,8 +195,8 @@
    2.24     expect: string}
    2.25  
    2.26  datatype axiom =
    2.27 -  Unprepared of (string * locality) * thm |
    2.28 -  Prepared of term * ((string * locality) * prepared_formula) option
    2.29 +  Untranslated of (string * locality) * thm |
    2.30 +  Translated of term * ((string * locality) * translated_formula) option
    2.31  
    2.32  type prover_problem =
    2.33    {state: Proof.state,
    2.34 @@ -250,10 +250,10 @@
    2.35  
    2.36  (* generic TPTP-based ATPs *)
    2.37  
    2.38 -fun dest_Unprepared (Unprepared p) = p
    2.39 -  | dest_Unprepared (Prepared _) = raise Fail "dest_Unprepared"
    2.40 -fun prepared_axiom ctxt (Unprepared p) = prepare_axiom ctxt p
    2.41 -  | prepared_axiom _ (Prepared p) = p
    2.42 +fun dest_Untranslated (Untranslated p) = p
    2.43 +  | dest_Untranslated (Translated _) = raise Fail "dest_Untranslated"
    2.44 +fun translated_axiom ctxt (Untranslated p) = translate_axiom ctxt p
    2.45 +  | translated_axiom _ (Translated p) = p
    2.46  
    2.47  fun int_option_add (SOME m) (SOME n) = SOME (m + n)
    2.48    | int_option_add _ _ = NONE
    2.49 @@ -275,7 +275,7 @@
    2.50      val (_, hyp_ts, concl_t) = strip_subgoal goal subgoal
    2.51      val axioms =
    2.52        axioms |> not only ? take (the_default default_max_relevant max_relevant)
    2.53 -             |> map (prepared_axiom ctxt)
    2.54 +             |> map (translated_axiom ctxt)
    2.55      val dest_dir = if overlord then getenv "ISABELLE_HOME_USER"
    2.56                     else Config.get ctxt dest_dir
    2.57      val problem_prefix = Config.get ctxt problem_prefix
    2.58 @@ -418,7 +418,7 @@
    2.59    let
    2.60      val {outcome, used_axioms, run_time_in_msecs} =
    2.61        saschas_run_smt_solver remote timeout state
    2.62 -                             (map_filter (try dest_Unprepared) axioms) subgoal
    2.63 +                             (map_filter (try dest_Untranslated) axioms) subgoal
    2.64      val message =
    2.65        if outcome = NONE then
    2.66          try_command_line (proof_banner false)
    2.67 @@ -507,8 +507,8 @@
    2.68        val _ = () |> not blocking ? kill_provers
    2.69        val _ = if auto then () else priority "Sledgehammering..."
    2.70        val (smts, atps) = provers |> List.partition is_smt_prover
    2.71 -      fun run_provers full_types irrelevant_consts relevance_fudge maybe_prepare
    2.72 -                      provers (res as (success, state)) =
    2.73 +      fun run_provers full_types irrelevant_consts relevance_fudge
    2.74 +                      maybe_translate provers (res as (success, state)) =
    2.75          if success orelse null provers then
    2.76            res
    2.77          else
    2.78 @@ -524,7 +524,7 @@
    2.79                relevant_facts ctxt full_types relevance_thresholds
    2.80                               max_max_relevant irrelevant_consts relevance_fudge
    2.81                               relevance_override chained_ths hyp_ts concl_t
    2.82 -              |> map maybe_prepare
    2.83 +              |> map maybe_translate
    2.84              val problem =
    2.85                {state = state, goal = goal, subgoal = i, subgoal_count = n,
    2.86                 axioms = axioms, only = only}
    2.87 @@ -541,9 +541,9 @@
    2.88            end
    2.89        val run_atps =
    2.90          run_provers full_types atp_irrelevant_consts atp_relevance_fudge
    2.91 -                    (Prepared o prepare_axiom ctxt) atps
    2.92 +                    (Translated o translate_axiom ctxt) atps
    2.93        val run_smts =
    2.94 -        run_provers true smt_irrelevant_consts smt_relevance_fudge Unprepared
    2.95 +        run_provers true smt_irrelevant_consts smt_relevance_fudge Untranslated
    2.96                      smts
    2.97        fun run_atps_and_smt_solvers () =
    2.98          [run_atps, run_smts] |> Par_List.map (fn f => f (false, state) |> K ())
     3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML	Fri Oct 22 18:24:10 2010 +0200
     3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML	Fri Oct 22 18:31:45 2010 +0200
     3.3 @@ -1,4 +1,4 @@
     3.4 -(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
     3.5 +(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML
     3.6      Author:     Lawrence C. Paulson, Cambridge University Computer Laboratory
     3.7      Author:     Claire Quigley, Cambridge University Computer Laboratory
     3.8      Author:     Jasmin Blanchette, TU Muenchen
     4.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Fri Oct 22 18:24:10 2010 +0200
     4.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Fri Oct 22 18:31:45 2010 +0200
     4.3 @@ -1,4 +1,4 @@
     4.4 -(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_translate.ML
     4.5 +(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
     4.6      Author:     Fabian Immler, TU Muenchen
     4.7      Author:     Makarius
     4.8      Author:     Jasmin Blanchette, TU Muenchen
     4.9 @@ -9,16 +9,16 @@
    4.10  signature SLEDGEHAMMER_ATP_TRANSLATE =
    4.11  sig
    4.12    type 'a problem = 'a ATP_Problem.problem
    4.13 -  type prepared_formula
    4.14 +  type translated_formula
    4.15  
    4.16    val axiom_prefix : string
    4.17    val conjecture_prefix : string
    4.18 -  val prepare_axiom :
    4.19 +  val translate_axiom :
    4.20      Proof.context -> (string * 'a) * thm
    4.21 -    -> term * ((string * 'a) * prepared_formula) option
    4.22 +    -> term * ((string * 'a) * translated_formula) option
    4.23    val prepare_atp_problem :
    4.24      Proof.context -> bool -> bool -> bool -> bool -> term list -> term
    4.25 -    -> (term * ((string * 'a) * prepared_formula) option) list
    4.26 +    -> (term * ((string * 'a) * translated_formula) option) list
    4.27      -> string problem * string Symtab.table * int * (string * 'a) list vector
    4.28  end;
    4.29  
    4.30 @@ -39,7 +39,7 @@
    4.31  (* Freshness almost guaranteed! *)
    4.32  val sledgehammer_weak_prefix = "Sledgehammer:"
    4.33  
    4.34 -type prepared_formula =
    4.35 +type translated_formula =
    4.36    {name: string,
    4.37     kind: kind,
    4.38     combformula: (name, combterm) formula,
    4.39 @@ -214,7 +214,7 @@
    4.40  fun count_combformula (AQuant (_, _, phi)) = count_combformula phi
    4.41    | count_combformula (AConn (_, phis)) = fold count_combformula phis
    4.42    | count_combformula (AAtom tm) = count_combterm tm
    4.43 -fun count_prepared_formula ({combformula, ...} : prepared_formula) =
    4.44 +fun count_translated_formula ({combformula, ...} : translated_formula) =
    4.45    count_combformula combformula
    4.46  
    4.47  val optional_helpers =
    4.48 @@ -235,7 +235,7 @@
    4.49  fun get_helper_facts ctxt is_FO full_types conjectures axioms =
    4.50    let
    4.51      val ct =
    4.52 -      fold (fold count_prepared_formula) [conjectures, axioms] init_counters
    4.53 +      fold (fold count_translated_formula) [conjectures, axioms] init_counters
    4.54      fun is_needed c = the (Symtab.lookup ct c) > 0
    4.55      fun baptize th = ((Thm.get_name_hint th, false), th)
    4.56    in
    4.57 @@ -247,12 +247,12 @@
    4.58      |> map_filter (Option.map snd o make_axiom ctxt false)
    4.59    end
    4.60  
    4.61 -fun prepare_axiom ctxt (ax as (_, th)) = (prop_of th, make_axiom ctxt true ax)
    4.62 +fun translate_axiom ctxt (ax as (_, th)) = (prop_of th, make_axiom ctxt true ax)
    4.63  
    4.64 -fun prepare_formulas ctxt full_types hyp_ts concl_t axioms =
    4.65 +fun translate_formulas ctxt full_types hyp_ts concl_t axioms =
    4.66    let
    4.67      val thy = ProofContext.theory_of ctxt
    4.68 -    val (axiom_ts, prepared_axioms) = ListPair.unzip axioms
    4.69 +    val (axiom_ts, translated_axioms) = ListPair.unzip axioms
    4.70      (* Remove existing axioms from the conjecture, as this can dramatically
    4.71         boost an ATP's performance (for some reason). *)
    4.72      val hyp_ts = hyp_ts |> filter_out (member (op aconv) axiom_ts)
    4.73 @@ -263,7 +263,7 @@
    4.74      val tycons = type_consts_of_terms thy (goal_t :: axiom_ts)
    4.75      (* TFrees in the conjecture; TVars in the axioms *)
    4.76      val conjectures = make_conjecture ctxt (hyp_ts @ [concl_t])
    4.77 -    val (axiom_names, axioms) = ListPair.unzip (map_filter I prepared_axioms)
    4.78 +    val (axiom_names, axioms) = ListPair.unzip (map_filter I translated_axioms)
    4.79      val helper_facts = get_helper_facts ctxt is_FO full_types conjectures axioms
    4.80      val (supers', arity_clauses) = make_arity_clauses thy tycons supers
    4.81      val class_rel_clauses = make_class_rel_clauses thy subs supers'
    4.82 @@ -323,7 +323,7 @@
    4.83    in aux end
    4.84  
    4.85  fun formula_for_axiom full_types
    4.86 -                      ({combformula, ctypes_sorts, ...} : prepared_formula) =
    4.87 +                      ({combformula, ctypes_sorts, ...} : translated_formula) =
    4.88    mk_ahorn (map (formula_for_fo_literal o fo_literal_for_type_literal)
    4.89                  (type_literals_for_types ctypes_sorts))
    4.90             (formula_for_combformula full_types combformula)
    4.91 @@ -353,11 +353,12 @@
    4.92                       (fo_literal_for_arity_literal conclLit)))
    4.93  
    4.94  fun problem_line_for_conjecture full_types
    4.95 -                           ({name, kind, combformula, ...} : prepared_formula) =
    4.96 +        ({name, kind, combformula, ...} : translated_formula) =
    4.97    Fof (conjecture_prefix ^ name, kind,
    4.98         formula_for_combformula full_types combformula)
    4.99  
   4.100 -fun free_type_literals_for_conjecture ({ctypes_sorts, ...} : prepared_formula) =
   4.101 +fun free_type_literals_for_conjecture
   4.102 +        ({ctypes_sorts, ...} : translated_formula) =
   4.103    map fo_literal_for_type_literal (type_literals_for_types ctypes_sorts)
   4.104  
   4.105  fun problem_line_for_free_type j lit =
   4.106 @@ -501,7 +502,7 @@
   4.107      val thy = ProofContext.theory_of ctxt
   4.108      val (axiom_names, (conjectures, axioms, helper_facts, class_rel_clauses,
   4.109                         arity_clauses)) =
   4.110 -      prepare_formulas ctxt full_types hyp_ts concl_t axioms
   4.111 +      translate_formulas ctxt full_types hyp_ts concl_t axioms
   4.112      val axiom_lines = map (problem_line_for_fact axiom_prefix full_types) axioms
   4.113      val helper_lines =
   4.114        map (problem_line_for_fact helper_prefix full_types) helper_facts
     5.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Fri Oct 22 18:24:10 2010 +0200
     5.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Fri Oct 22 18:31:45 2010 +0200
     5.3 @@ -55,7 +55,7 @@
     5.4         max_relevant = NONE, isar_proof = isar_proof,
     5.5         isar_shrink_factor = isar_shrink_factor, timeout = timeout, expect = ""}
     5.6      val axioms =
     5.7 -      axioms |> maps (fn (n, ths) => ths |> map (Unprepared o pair n))
     5.8 +      axioms |> maps (fn (n, ths) => ths |> map (Untranslated o pair n))
     5.9      val {goal, ...} = Proof.goal state
    5.10      val problem =
    5.11        {state = state, goal = goal, subgoal = i, subgoal_count = n,