src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
changeset 35866 513074557e06
parent 35830 d4c4f88f6432
child 35867 16279c4c7a33
     1.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Fri Mar 19 13:02:18 2010 +0100
     1.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Fri Mar 19 15:07:44 2010 +0100
     1.3 @@ -42,8 +42,7 @@
     1.4  
     1.5  datatype min_data = MinData of {
     1.6    succs: int,
     1.7 -  ab_ratios: int,
     1.8 -  it_ratios: int
     1.9 +  ab_ratios: int
    1.10    }
    1.11  
    1.12  fun make_sh_data
    1.13 @@ -51,8 +50,8 @@
    1.14    ShData{calls=calls, success=success, lemmas=lemmas, max_lems=max_lems,
    1.15           time_isa=time_isa, time_atp=time_atp, time_atp_fail=time_atp_fail}
    1.16  
    1.17 -fun make_min_data (succs, ab_ratios, it_ratios) =
    1.18 -  MinData{succs=succs, ab_ratios=ab_ratios, it_ratios=it_ratios}
    1.19 +fun make_min_data (succs, ab_ratios) =
    1.20 +  MinData{succs=succs, ab_ratios=ab_ratios}
    1.21  
    1.22  fun make_me_data (calls,success,proofs,time,timeout,lemmas,posns) =
    1.23    MeData{calls=calls, success=success, proofs=proofs, time=time,
    1.24 @@ -66,8 +65,7 @@
    1.25    time_atp, time_atp_fail}) = (calls, success, lemmas, max_lems, time_isa,
    1.26    time_atp, time_atp_fail)
    1.27  
    1.28 -fun tuple_of_min_data (MinData {succs, ab_ratios, it_ratios}) =
    1.29 -  (succs, ab_ratios, it_ratios)
    1.30 +fun tuple_of_min_data (MinData {succs, ab_ratios}) = (succs, ab_ratios)
    1.31  
    1.32  fun tuple_of_me_data (MeData {calls, success, proofs, time, timeout, lemmas,
    1.33    posns}) = (calls, success, proofs, time, timeout, lemmas, posns)
    1.34 @@ -147,13 +145,10 @@
    1.35      => (calls,success,lemmas,max_lems,time_isa,time_atp,time_atp_fail + t))
    1.36  
    1.37  val inc_min_succs = map_min_data
    1.38 -  (fn (succs,ab_ratios,it_ratios) => (succs+1, ab_ratios, it_ratios))
    1.39 +  (fn (succs,ab_ratios) => (succs+1, ab_ratios))
    1.40  
    1.41  fun inc_min_ab_ratios r = map_min_data
    1.42 -  (fn (succs, ab_ratios, it_ratios) => (succs, ab_ratios+r, it_ratios))
    1.43 -
    1.44 -fun inc_min_it_ratios r = map_min_data
    1.45 -  (fn (succs, ab_ratios, it_ratios) => (succs, ab_ratios, it_ratios+r))
    1.46 +  (fn (succs, ab_ratios) => (succs, ab_ratios+r))
    1.47  
    1.48  val inc_metis_calls = map_me_data
    1.49    (fn (calls,success,proofs,time,timeout,lemmas,posns)
    1.50 @@ -234,10 +229,9 @@
    1.51    else ()
    1.52   )
    1.53  
    1.54 -fun log_min_data log (succs, ab_ratios, it_ratios) =
    1.55 +fun log_min_data log (succs, ab_ratios) =
    1.56    (log ("Number of successful minimizations: " ^ string_of_int succs);
    1.57 -   log ("After/before ratios: " ^ string_of_int ab_ratios);
    1.58 -   log ("Iterations ratios: " ^ string_of_int it_ratios)
    1.59 +   log ("After/before ratios: " ^ string_of_int ab_ratios)
    1.60    )
    1.61  
    1.62  in
    1.63 @@ -380,9 +374,10 @@
    1.64  
    1.65  fun run_minimize args named_thms id ({pre=st, log, ...}: Mirabelle.run_args) =
    1.66    let
    1.67 +    open ATP_Minimal
    1.68      val n0 = length (these (!named_thms))
    1.69      val (prover_name, prover) = get_atp (Proof.theory_of st) args
    1.70 -    val minimize = ATP_Minimal.minimalize prover prover_name
    1.71 +    val minimize = minimize_theorems linear_minimize prover prover_name
    1.72      val timeout =
    1.73        AList.lookup (op =) args minimize_timeoutK
    1.74        |> Option.map (fst o read_int o explode)
    1.75 @@ -393,7 +388,6 @@
    1.76        (SOME (named_thms',its), msg) =>
    1.77          (change_data id inc_min_succs;
    1.78           change_data id (inc_min_ab_ratios ((100 * length named_thms') div n0));
    1.79 -         change_data id (inc_min_it_ratios ((100*its) div n0));
    1.80           if length named_thms' = n0
    1.81           then log (minimize_tag id ^ "already minimal")
    1.82           else (named_thms := SOME named_thms';