more weight attribute tuning
authorblanchet
Tue Mar 20 00:44:30 2012 +0100 (2012-03-20)
changeset 4703273cdeed236c0
parent 47031 26dd49368db6
child 47033 baa9dc39ee51
more weight attribute tuning
src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
src/HOL/Tools/ATP/atp_problem_generate.ML
src/HOL/Tools/ATP/atp_systems.ML
     1.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Tue Mar 20 00:44:30 2012 +0100
     1.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Tue Mar 20 00:44:30 2012 +0100
     1.3 @@ -13,7 +13,7 @@
     1.4  val sliceK = "slice"
     1.5  val lam_transK = "lam_trans"
     1.6  val uncurried_aliasesK = "uncurried_aliases"
     1.7 -val e_selection_weight_methodK = "e_selection_weight_method"
     1.8 +val e_selection_heuristicK = "e_selection_heuristic"
     1.9  val force_sosK = "force_sos"
    1.10  val max_relevantK = "max_relevant"
    1.11  val max_callsK = "max_calls"
    1.12 @@ -376,7 +376,7 @@
    1.13    SH_ERROR
    1.14  
    1.15  fun run_sh prover_name prover type_enc strict max_relevant slice lam_trans
    1.16 -        uncurried_aliases e_selection_weight_method force_sos hard_timeout
    1.17 +        uncurried_aliases e_selection_heuristic force_sos hard_timeout
    1.18          timeout preplay_timeout sh_minimizeLST max_new_mono_instancesLST
    1.19          max_mono_itersLST dir pos st =
    1.20    let
    1.21 @@ -394,8 +394,8 @@
    1.22        st
    1.23        |> Proof.map_context
    1.24             (set_file_name dir
    1.25 -            #> (Option.map (Config.put ATP_Systems.e_selection_weight_method)
    1.26 -                  e_selection_weight_method |> the_default I)
    1.27 +            #> (Option.map (Config.put ATP_Systems.e_selection_heuristic)
    1.28 +                  e_selection_heuristic |> the_default I)
    1.29              #> (Option.map (Config.put ATP_Systems.force_sos)
    1.30                    force_sos |> the_default I))
    1.31      val params as {relevance_thresholds, max_relevant, slice, ...} =
    1.32 @@ -492,7 +492,7 @@
    1.33      val slice = AList.lookup (op =) args sliceK |> the_default "true"
    1.34      val lam_trans = AList.lookup (op =) args lam_transK
    1.35      val uncurried_aliases = AList.lookup (op =) args uncurried_aliasesK
    1.36 -    val e_selection_weight_method = AList.lookup (op =) args e_selection_weight_methodK
    1.37 +    val e_selection_heuristic = AList.lookup (op =) args e_selection_heuristicK
    1.38      val force_sos = AList.lookup (op =) args force_sosK
    1.39        |> Option.map (curry (op <>) "false")
    1.40      val dir = AList.lookup (op =) args keepK
    1.41 @@ -508,7 +508,7 @@
    1.42      val hard_timeout = SOME (2 * timeout)
    1.43      val (msg, result) =
    1.44        run_sh prover_name prover type_enc strict max_relevant slice lam_trans
    1.45 -        uncurried_aliases e_selection_weight_method force_sos hard_timeout
    1.46 +        uncurried_aliases e_selection_heuristic force_sos hard_timeout
    1.47          timeout preplay_timeout sh_minimizeLST max_new_mono_instancesLST
    1.48          max_mono_itersLST dir pos st
    1.49    in
     2.1 --- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Tue Mar 20 00:44:30 2012 +0100
     2.2 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Tue Mar 20 00:44:30 2012 +0100
     2.3 @@ -2746,13 +2746,13 @@
     2.4      |> sort (prod_ord Real.compare string_ord o pairself swap)
     2.5    end
     2.6  
     2.7 -fun have_head_rolling (ATerm (s, args)) =
     2.8 -    (* ugly hack: may make innocent victims *)
     2.9 +fun make_head_roll (ATerm (s, args)) =
    2.10 +    (* ugly hack: may make innocent victims (collateral damage) *)
    2.11      if String.isPrefix app_op_name s andalso length args = 2 then
    2.12 -      have_head_rolling (hd args) ||> append (tl args)
    2.13 +      make_head_roll (hd args) ||> append (tl args)
    2.14      else
    2.15        (s, args)
    2.16 -  | have_head_rolling _ = ("", [])
    2.17 +  | make_head_roll _ = ("", [])
    2.18  
    2.19  val max_term_order_weight = 2147483647
    2.20  
    2.21 @@ -2764,7 +2764,7 @@
    2.22        | add_term_deps head (AAbs (_, tm)) = add_term_deps head tm
    2.23      fun add_eq_deps (ATerm (s, [lhs as _, rhs])) =
    2.24          if is_tptp_equal s then
    2.25 -          let val (head, rest) = have_head_rolling lhs in
    2.26 +          let val (head, rest) = make_head_roll lhs in
    2.27              fold (add_term_deps head) (rhs :: rest)
    2.28            end
    2.29          else
     3.1 --- a/src/HOL/Tools/ATP/atp_systems.ML	Tue Mar 20 00:44:30 2012 +0100
     3.2 +++ b/src/HOL/Tools/ATP/atp_systems.ML	Tue Mar 20 00:44:30 2012 +0100
     3.3 @@ -26,11 +26,12 @@
     3.4         Proof.context -> (real * (bool * (slice_spec * string))) list}
     3.5  
     3.6    val force_sos : bool Config.T
     3.7 +  val term_order : string Config.T
     3.8    val e_smartN : string
     3.9    val e_autoN : string
    3.10    val e_fun_weightN : string
    3.11    val e_sym_offset_weightN : string
    3.12 -  val e_selection_weight_method : string Config.T
    3.13 +  val e_selection_heuristic : string Config.T
    3.14    val e_default_fun_weight : real Config.T
    3.15    val e_fun_weight_base : real Config.T
    3.16    val e_fun_weight_span : real Config.T
    3.17 @@ -161,6 +162,16 @@
    3.18  
    3.19  val force_sos = Attrib.setup_config_bool @{binding atp_force_sos} (K false)
    3.20  
    3.21 +val smartN = "smart"
    3.22 +val kboN = "kbo"
    3.23 +val lpoN = "lpo"
    3.24 +val weightsN = "_weights"
    3.25 +val precsN = "_precs"
    3.26 +val lrN = "_lr" (* SPASS-specific *)
    3.27 +
    3.28 +val term_order =
    3.29 +  Attrib.setup_config_string @{binding atp_term_order} (K smartN)
    3.30 +
    3.31  
    3.32  (* Alt-Ergo *)
    3.33  
    3.34 @@ -200,8 +211,8 @@
    3.35  val e_fun_weightN = "fun_weight"
    3.36  val e_sym_offset_weightN = "sym_offset_weight"
    3.37  
    3.38 -val e_selection_weight_method =
    3.39 -  Attrib.setup_config_string @{binding atp_e_selection_weight_method} (K e_smartN)
    3.40 +val e_selection_heuristic =
    3.41 +  Attrib.setup_config_string @{binding atp_e_selection_heuristic} (K e_smartN)
    3.42  (* FUDGE *)
    3.43  val e_default_fun_weight =
    3.44    Attrib.setup_config_real @{binding atp_e_default_fun_weight} (K 20.0)
    3.45 @@ -216,15 +227,15 @@
    3.46  val e_sym_offs_weight_span =
    3.47    Attrib.setup_config_real @{binding atp_e_sym_offs_weight_span} (K 60.0)
    3.48  
    3.49 -fun e_selection_weight_method_case method fw sow =
    3.50 +fun e_selection_heuristic_case method fw sow =
    3.51    if method = e_fun_weightN then fw
    3.52    else if method = e_sym_offset_weightN then sow
    3.53    else raise Fail ("unexpected " ^ quote method)
    3.54  
    3.55  fun scaled_e_selection_weight ctxt method w =
    3.56 -  w * Config.get ctxt (e_selection_weight_method_case method
    3.57 +  w * Config.get ctxt (e_selection_heuristic_case method
    3.58                             e_fun_weight_span e_sym_offs_weight_span)
    3.59 -  + Config.get ctxt (e_selection_weight_method_case method
    3.60 +  + Config.get ctxt (e_selection_heuristic_case method
    3.61                           e_fun_weight_base e_sym_offs_weight_base)
    3.62    |> Real.ceil |> signed_string_of_int
    3.63  
    3.64 @@ -237,10 +248,9 @@
    3.65      \--destructive-er-aggressive --destructive-er --presat-simplify \
    3.66      \--prefer-initial-clauses -tKBO6 -winvfreqrank -c1 -Ginvfreqconjmax -F1 \
    3.67      \--delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred \
    3.68 -    \-H'(4*" ^
    3.69 -    e_selection_weight_method_case method "FunWeight" "SymOffsetWeight" ^
    3.70 +    \-H'(4*" ^ e_selection_heuristic_case method "FunWeight" "SymOffsetWeight" ^
    3.71      "(SimulateSOS, " ^
    3.72 -    (e_selection_weight_method_case method
    3.73 +    (e_selection_heuristic_case method
    3.74           e_default_fun_weight e_default_sym_offs_weight
    3.75       |> Config.get ctxt |> Real.ceil |> signed_string_of_int) ^
    3.76      ",20,1.5,1.5,1" ^
    3.77 @@ -252,9 +262,8 @@
    3.78      \1.5,1.5,1),1*Clauseweight(PreferProcessed,1,1,1),1*\
    3.79      \FIFOWeight(PreferProcessed))'"
    3.80  
    3.81 -fun effective_e_selection_weight_method ctxt =
    3.82 -  if is_old_e_version () then e_autoN
    3.83 -  else Config.get ctxt e_selection_weight_method
    3.84 +fun effective_e_selection_heuristic ctxt =
    3.85 +  if is_old_e_version () then e_autoN else Config.get ctxt e_selection_heuristic
    3.86  
    3.87  val e_config : atp_config =
    3.88    {exec = ("E_HOME", "eproof"),
    3.89 @@ -273,7 +282,7 @@
    3.90     conj_sym_kind = Hypothesis,
    3.91     prem_kind = Conjecture,
    3.92     best_slices = fn ctxt =>
    3.93 -     let val method = effective_e_selection_weight_method ctxt in
    3.94 +     let val method = effective_e_selection_heuristic ctxt in
    3.95         (* FUDGE *)
    3.96         if method = e_smartN then
    3.97           [(0.333, (true, ((500, FOF, "mono_tags??", combsN, false), e_fun_weightN))),