src/HOL/Tools/ATP/atp_systems.ML
changeset 47032 73cdeed236c0
parent 47031 26dd49368db6
child 47033 baa9dc39ee51
     1.1 --- a/src/HOL/Tools/ATP/atp_systems.ML	Tue Mar 20 00:44:30 2012 +0100
     1.2 +++ b/src/HOL/Tools/ATP/atp_systems.ML	Tue Mar 20 00:44:30 2012 +0100
     1.3 @@ -26,11 +26,12 @@
     1.4         Proof.context -> (real * (bool * (slice_spec * string))) list}
     1.5  
     1.6    val force_sos : bool Config.T
     1.7 +  val term_order : string Config.T
     1.8    val e_smartN : string
     1.9    val e_autoN : string
    1.10    val e_fun_weightN : string
    1.11    val e_sym_offset_weightN : string
    1.12 -  val e_selection_weight_method : string Config.T
    1.13 +  val e_selection_heuristic : string Config.T
    1.14    val e_default_fun_weight : real Config.T
    1.15    val e_fun_weight_base : real Config.T
    1.16    val e_fun_weight_span : real Config.T
    1.17 @@ -161,6 +162,16 @@
    1.18  
    1.19  val force_sos = Attrib.setup_config_bool @{binding atp_force_sos} (K false)
    1.20  
    1.21 +val smartN = "smart"
    1.22 +val kboN = "kbo"
    1.23 +val lpoN = "lpo"
    1.24 +val weightsN = "_weights"
    1.25 +val precsN = "_precs"
    1.26 +val lrN = "_lr" (* SPASS-specific *)
    1.27 +
    1.28 +val term_order =
    1.29 +  Attrib.setup_config_string @{binding atp_term_order} (K smartN)
    1.30 +
    1.31  
    1.32  (* Alt-Ergo *)
    1.33  
    1.34 @@ -200,8 +211,8 @@
    1.35  val e_fun_weightN = "fun_weight"
    1.36  val e_sym_offset_weightN = "sym_offset_weight"
    1.37  
    1.38 -val e_selection_weight_method =
    1.39 -  Attrib.setup_config_string @{binding atp_e_selection_weight_method} (K e_smartN)
    1.40 +val e_selection_heuristic =
    1.41 +  Attrib.setup_config_string @{binding atp_e_selection_heuristic} (K e_smartN)
    1.42  (* FUDGE *)
    1.43  val e_default_fun_weight =
    1.44    Attrib.setup_config_real @{binding atp_e_default_fun_weight} (K 20.0)
    1.45 @@ -216,15 +227,15 @@
    1.46  val e_sym_offs_weight_span =
    1.47    Attrib.setup_config_real @{binding atp_e_sym_offs_weight_span} (K 60.0)
    1.48  
    1.49 -fun e_selection_weight_method_case method fw sow =
    1.50 +fun e_selection_heuristic_case method fw sow =
    1.51    if method = e_fun_weightN then fw
    1.52    else if method = e_sym_offset_weightN then sow
    1.53    else raise Fail ("unexpected " ^ quote method)
    1.54  
    1.55  fun scaled_e_selection_weight ctxt method w =
    1.56 -  w * Config.get ctxt (e_selection_weight_method_case method
    1.57 +  w * Config.get ctxt (e_selection_heuristic_case method
    1.58                             e_fun_weight_span e_sym_offs_weight_span)
    1.59 -  + Config.get ctxt (e_selection_weight_method_case method
    1.60 +  + Config.get ctxt (e_selection_heuristic_case method
    1.61                           e_fun_weight_base e_sym_offs_weight_base)
    1.62    |> Real.ceil |> signed_string_of_int
    1.63  
    1.64 @@ -237,10 +248,9 @@
    1.65      \--destructive-er-aggressive --destructive-er --presat-simplify \
    1.66      \--prefer-initial-clauses -tKBO6 -winvfreqrank -c1 -Ginvfreqconjmax -F1 \
    1.67      \--delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred \
    1.68 -    \-H'(4*" ^
    1.69 -    e_selection_weight_method_case method "FunWeight" "SymOffsetWeight" ^
    1.70 +    \-H'(4*" ^ e_selection_heuristic_case method "FunWeight" "SymOffsetWeight" ^
    1.71      "(SimulateSOS, " ^
    1.72 -    (e_selection_weight_method_case method
    1.73 +    (e_selection_heuristic_case method
    1.74           e_default_fun_weight e_default_sym_offs_weight
    1.75       |> Config.get ctxt |> Real.ceil |> signed_string_of_int) ^
    1.76      ",20,1.5,1.5,1" ^
    1.77 @@ -252,9 +262,8 @@
    1.78      \1.5,1.5,1),1*Clauseweight(PreferProcessed,1,1,1),1*\
    1.79      \FIFOWeight(PreferProcessed))'"
    1.80  
    1.81 -fun effective_e_selection_weight_method ctxt =
    1.82 -  if is_old_e_version () then e_autoN
    1.83 -  else Config.get ctxt e_selection_weight_method
    1.84 +fun effective_e_selection_heuristic ctxt =
    1.85 +  if is_old_e_version () then e_autoN else Config.get ctxt e_selection_heuristic
    1.86  
    1.87  val e_config : atp_config =
    1.88    {exec = ("E_HOME", "eproof"),
    1.89 @@ -273,7 +282,7 @@
    1.90     conj_sym_kind = Hypothesis,
    1.91     prem_kind = Conjecture,
    1.92     best_slices = fn ctxt =>
    1.93 -     let val method = effective_e_selection_weight_method ctxt in
    1.94 +     let val method = effective_e_selection_heuristic ctxt in
    1.95         (* FUDGE *)
    1.96         if method = e_smartN then
    1.97           [(0.333, (true, ((500, FOF, "mono_tags??", combsN, false), e_fun_weightN))),