# HG changeset patch # User blanchet # Date 1334739208 -7200 # Node ID 7fe7c741948927643e72de7d90513e7750d32b9e # Parent 9ad8c4315f9284021dbf72d6dc032727667ad6c1 get rid of minor optimization that caused strange problems and was hard to debug (and apparently saved less than 100 ms on a 30 s run) diff -r 9ad8c4315f92 -r 7fe7c7419489 src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Wed Apr 18 10:53:27 2012 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Wed Apr 18 10:53:28 2012 +0200 @@ -72,7 +72,7 @@ preplay_timeout = preplay_timeout, expect = ""} val problem = {state = state, goal = goal, subgoal = i, subgoal_count = n, - facts = facts, smt_filter = NONE} + facts = facts} val result as {outcome, used_facts, run_time, ...} = prover params (K (K (K ""))) problem in diff -r 9ad8c4315f92 -r 7fe7c7419489 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Wed Apr 18 10:53:27 2012 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Wed Apr 18 10:53:28 2012 +0200 @@ -49,8 +49,7 @@ goal: thm, subgoal: int, subgoal_count: int, - facts: prover_fact list, - smt_filter: (string * stature) SMT_Solver.smt_filter_data option} + facts: prover_fact list} type prover_result = {outcome: failure option, @@ -314,8 +313,7 @@ goal: thm, subgoal: int, subgoal_count: int, - facts: prover_fact list, - smt_filter: (string * stature) SMT_Solver.smt_filter_data option} + facts: prover_fact list} type prover_result = {outcome: failure option, @@ -900,7 +898,7 @@ fun smt_filter_loop ctxt name ({debug, verbose, overlord, max_mono_iters, max_new_mono_instances, timeout, slice, ...} : params) - state i smt_filter = + state i = let val max_slices = if slice then Config.get ctxt smt_max_slices else 1 val repair_context = @@ -944,9 +942,7 @@ val _ = if debug then Output.urgent_message "Invoking SMT solver..." else () val (outcome, used_facts) = - (case (slice, smt_filter) of - (1, SOME head) => head |> apsnd (apsnd repair_context) - | _ => SMT_Solver.smt_filter_preprocess state facts i) + SMT_Solver.smt_filter_preprocess state facts i |> SMT_Solver.smt_filter_apply slice_timeout |> (fn {outcome, used_facts} => (outcome, used_facts)) handle exn => if Exn.is_interrupt exn then @@ -995,15 +991,14 @@ fun run_smt_solver mode name (params as {debug, verbose, preplay_timeout, ...}) minimize_command - ({state, subgoal, subgoal_count, facts, smt_filter, ...} - : prover_problem) = + ({state, subgoal, subgoal_count, facts, ...} : prover_problem) = let val ctxt = Proof.context_of state val num_facts = length facts val facts = facts ~~ (0 upto num_facts - 1) |> map (smt_weighted_fact ctxt num_facts) val {outcome, used_facts = used_pairs, run_time} = - smt_filter_loop ctxt name params state subgoal smt_filter facts + smt_filter_loop ctxt name params state subgoal facts val used_facts = used_pairs |> map fst val outcome = outcome |> Option.map failure_from_smt_failure val (preplay, message, message_tail) = diff -r 9ad8c4315f92 -r 7fe7c7419489 src/HOL/Tools/Sledgehammer/sledgehammer_run.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Wed Apr 18 10:53:27 2012 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Wed Apr 18 10:53:28 2012 +0200 @@ -177,8 +177,8 @@ fun launch_prover (params as {debug, verbose, blocking, max_relevant, slice, timeout, expect, ...}) - mode minimize_command only - {state, goal, subgoal, subgoal_count, facts, smt_filter} name = + mode minimize_command only {state, goal, subgoal, subgoal_count, facts} + name = let val ctxt = Proof.context_of state val hard_timeout = Time.+ (timeout, timeout) @@ -197,8 +197,7 @@ subgoal_count = subgoal_count, facts = ((Sledgehammer_Provers.is_ho_atp ctxt name |> not) ? filter_induction) facts - |> take num_facts, - smt_filter = smt_filter} + |> take num_facts} end fun really_go () = problem @@ -268,14 +267,11 @@ ctxt |> select_smt_solver name |> SMT_Config.solver_class_of |> SMT_Utils.string_of_class -fun dest_SMT_Weighted_Fact (SMT_Weighted_Fact p) = p - | dest_SMT_Weighted_Fact _ = raise Fail "dest_SMT_Weighted_Fact" - val auto_try_max_relevant_divisor = 2 (* FUDGE *) fun run_sledgehammer (params as {debug, verbose, blocking, provers, relevance_thresholds, max_relevant, slice, - timeout, ...}) + ...}) mode i (relevance_override as {only, ...}) minimize_command state = if null provers then error "No prover is set." @@ -303,7 +299,7 @@ val (smts, (ueq_atps, full_atps)) = provers |> List.partition (is_smt_prover ctxt) ||> List.partition (is_unit_equational_atp ctxt) - fun launch_provers state get_facts translate maybe_smt_filter provers = + fun launch_provers state get_facts translate provers = let val facts = get_facts () val num_facts = length facts @@ -311,9 +307,7 @@ |> map (translate num_facts) val problem = {state = state, goal = goal, subgoal = i, subgoal_count = n, - facts = facts, - smt_filter = maybe_smt_filter - (fn () => map_filter (try dest_SMT_Weighted_Fact) facts) i} + facts = facts} val launch = launch_prover params mode minimize_command only in if mode = Auto_Try orelse mode = Try then @@ -377,7 +371,7 @@ else launch_provers state (get_facts label is_appropriate_prop atp_relevance_fudge o K atps) - (K (Untranslated_Fact o fst)) (K (K NONE)) atps + (K (Untranslated_Fact o fst)) atps fun launch_smts accum = if null smts then accum @@ -385,15 +379,10 @@ let val facts = get_facts "SMT solver" NONE smt_relevance_fudge smts val weight = SMT_Weighted_Fact oo weight_smt_fact ctxt - fun smt_filter facts = - (if debug then curry (op o) SOME - else TimeLimit.timeLimit timeout o try) - (SMT_Solver.smt_filter_preprocess state (facts ())) in smts |> map (`(class_of_smt_solver ctxt)) |> AList.group (op =) - |> map (snd #> launch_provers state (K facts) weight smt_filter - #> fst) + |> map (snd #> launch_provers state (K facts) weight #> fst) |> max_outcome_code |> rpair state end val launch_full_atps = launch_atps "ATP" NONE full_atps