# HG changeset patch # User blanchet # Date 1387381814 -3600 # Node ID 565f9af86d67b0735681074da172d265d6eca450 # Parent 287e569eebb2d219e6dfd02fe9c6601c09eefa2c tuning diff -r 287e569eebb2 -r 565f9af86d67 src/HOL/Tools/ATP/atp_proof.ML --- a/src/HOL/Tools/ATP/atp_proof.ML Wed Dec 18 16:50:14 2013 +0100 +++ b/src/HOL/Tools/ATP/atp_proof.ML Wed Dec 18 16:50:14 2013 +0100 @@ -220,15 +220,18 @@ val skip_term = let fun skip _ accum [] = (accum, []) - | skip 0 accum (ss as "," :: _) = (accum, ss) - | skip 0 accum (ss as ")" :: _) = (accum, ss) - | skip 0 accum (ss as "]" :: _) = (accum, ss) - | skip n accum ((s as "(") :: ss) = skip (n + 1) (s :: accum) ss - | skip n accum ((s as "[") :: ss) = skip (n + 1) (s :: accum) ss - | skip n accum ((s as "]") :: ss) = skip (n - 1) (s :: accum) ss - | skip n accum ((s as ")") :: ss) = skip (n - 1) (s :: accum) ss - | skip n accum (s :: ss) = skip n (s :: accum) ss - in skip 0 [] #>> (rev #> implode) end + | skip n accum (s :: ss) = + if s = "," andalso n = 0 then + (accum, ss) + else if member (op =) [")", "]", ">", "}"] s then + if n = 0 then (accum, ss) else skip (n - 1) (s :: accum) ss + else if member (op =) ["(", "[", "<", "{"] s then + skip (n + 1) (s :: accum) ss + else + skip n (s :: accum) ss + in + skip 0 [] #>> (rev #> implode) + end datatype source = File_Source of string * string option | @@ -261,21 +264,17 @@ || scan_general_id >> (fn s => Inference_Source ("", [s])) (* for E *) || skip_term >> K dummy_inference) x -fun list_app (f, args) = - fold (fn arg => fn f => ATerm ((tptp_app, []), [f, arg])) args f +fun list_app (f, args) = fold (fn arg => fn f => ATerm ((tptp_app, []), [f, arg])) args f (* We currently ignore TFF and THF types. *) -fun parse_type_stuff x = - Scan.repeat (($$ tptp_has_type || $$ tptp_fun_type) |-- parse_arg) x +fun parse_type_stuff x = Scan.repeat (($$ tptp_has_type || $$ tptp_fun_type) |-- parse_arg) x and parse_arg x = ($$ "(" |-- parse_term --| $$ ")" --| parse_type_stuff || scan_general_id --| parse_type_stuff -- Scan.optional ($$ "(" |-- parse_terms --| $$ ")") [] >> (ATerm o apfst (rpair []))) x -and parse_term x = - (parse_arg -- Scan.repeat ($$ tptp_app |-- parse_arg) >> list_app) x -and parse_terms x = - (parse_term ::: Scan.repeat ($$ "," |-- parse_term)) x +and parse_term x = (parse_arg -- Scan.repeat ($$ tptp_app |-- parse_arg) >> list_app) x +and parse_terms x = (parse_term ::: Scan.repeat ($$ "," |-- parse_term)) x fun parse_atom x = (parse_term -- Scan.option (Scan.option ($$ tptp_not_infix) --| $$ tptp_equal @@ -311,9 +310,7 @@ and parse_quantified_formula x = (($$ tptp_forall >> K AForall || $$ tptp_exists >> K AExists) --| $$ "[" -- parse_terms --| $$ "]" --| $$ ":" -- parse_literal - >> (fn ((q, ts), phi) => - (* We ignore TFF and THF types for now. *) - AQuant (q, map (fn ATerm ((s, []), _) => (s, NONE)) ts, phi))) x + >> (fn ((q, ts), phi) => AQuant (q, map (fn ATerm ((s, []), _) => (s, NONE)) ts, phi))) x val parse_tstp_extra_arguments = Scan.optional ($$ "," |-- parse_source --| Scan.option ($$ "," |-- skip_term)) @@ -351,9 +348,9 @@ c1 = c2 andalso length phis1 = length phis2 andalso forall (uncurry (is_same_formula comm subst)) (phis1 ~~ phis2) | is_same_formula comm subst - (AAtom (tm1 as ATerm (("equal", []), [tm11, tm12]))) (AAtom tm2) = + (AAtom (tm1 as ATerm (("equal", tys), [tm11, tm12]))) (AAtom tm2) = is_same_term subst tm1 tm2 orelse - (comm andalso is_same_term subst (ATerm (("equal", []), [tm12, tm11])) tm2) + (comm andalso is_same_term subst (ATerm (("equal", tys), [tm12, tm11])) tm2) | is_same_formula _ subst (AAtom tm1) (AAtom tm2) = is_same_term subst tm1 tm2 | is_same_formula _ _ _ _ = false @@ -361,11 +358,13 @@ if is_same_formula true [] phi phi' then SOME (ident, phi') else NONE | matching_formula_line_identifier _ _ = NONE -fun find_formula_in_problem problem phi = - problem |> maps snd |> map_filter (matching_formula_line_identifier phi) - |> try (single o hd) |> the_default [] +fun find_formula_in_problem phi = + maps snd + #> map_filter (matching_formula_line_identifier phi) + #> try (single o hd) + #> the_default [] -fun commute_eq (AAtom (ATerm ((s, []), tms))) = AAtom (ATerm ((s, []), rev tms)) +fun commute_eq (AAtom (ATerm ((s, tys), tms))) = AAtom (ATerm ((s, tys), rev tms)) | commute_eq _ = raise Fail "expected equation" fun role_of_tptp_string "axiom" = Axiom @@ -392,7 +391,7 @@ (case deps of File_Source (_, SOME s) => (if s = waldmeister_conjecture_name then - (case find_formula_in_problem problem (mk_anot phi) of + (case find_formula_in_problem (mk_anot phi) problem of (* Waldmeister hack: Get the original orientation of the equation to avoid confusing Isar. *) [(s, phi')] => @@ -404,16 +403,14 @@ phi), "", []) | File_Source _ => - (((num, phi |> find_formula_in_problem problem |> map fst), - phi), "", []) + (((num, map fst (find_formula_in_problem phi problem)), phi), "", []) | Inference_Source (rule, deps) => (((num, []), phi), rule, deps)) - fun mk_step () = - (name, role_of_tptp_string role, phi, rule, map (rpair []) deps) + fun mk_step () = (name, role_of_tptp_string role, phi, rule, map (rpair []) deps) in (case role_of_tptp_string role of Definition => (case phi of - AAtom (ATerm (("equal", []), _)) => + AAtom (ATerm (("equal", _), _)) => (* Vampire's equality proxy axiom *) (name, Definition, phi, rule, map (rpair []) deps) | _ => mk_step ()) diff -r 287e569eebb2 -r 565f9af86d67 src/HOL/Tools/ATP/atp_proof_reconstruct.ML --- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Wed Dec 18 16:50:14 2013 +0100 +++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Wed Dec 18 16:50:14 2013 +0100 @@ -536,8 +536,8 @@ | add_sko _ = I (* union-find would be faster *) - fun add_cycle _ [] = I - | add_cycle name ss = + fun add_cycle [] = I + | add_cycle ss = fold (fn s => Graph.default_node (s, ())) ss #> fold Graph.add_edge (ss ~~ tl ss @ [hd ss]) @@ -545,11 +545,7 @@ val skoss = map (fn (_, _, t, _, _) => Term.fold_aterms add_sko t []) input_steps val skoss_input_steps = filter_out (null o fst) (skoss ~~ input_steps) - - val groups = - Graph.empty - |> fold (fn (skos, (name, _, _, _, _)) => add_cycle name skos) skoss_input_steps - |> Graph.strong_conn + val groups = Graph.strong_conn (fold add_cycle skoss Graph.empty) fun step_name_of_group skos = (implode skos, []) fun in_group group = member (op =) group o hd @@ -582,7 +578,7 @@ fun factify_atp_proof fact_names hyp_ts concl_t atp_proof = let - fun factify_step ((num, ss), role, t, rule, deps) = + fun factify_step ((num, ss), _, t, rule, deps) = let val (ss', role', t') = (case resolve_conjecture ss of diff -r 287e569eebb2 -r 565f9af86d67 src/HOL/Tools/ATP/atp_proof_redirect.ML --- a/src/HOL/Tools/ATP/atp_proof_redirect.ML Wed Dec 18 16:50:14 2013 +0100 +++ b/src/HOL/Tools/ATP/atp_proof_redirect.ML Wed Dec 18 16:50:14 2013 +0100 @@ -68,7 +68,6 @@ val atom_eq = is_equal o Atom.ord val clause_ord = dict_ord Atom.ord -val clause_eq = is_equal o clause_ord fun direct_sequent_ord seqp = prod_ord clause_ord clause_ord (pairself snd seqp) fun direct_sequent_eq seqp = is_equal (direct_sequent_ord seqp) diff -r 287e569eebb2 -r 565f9af86d67 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Wed Dec 18 16:50:14 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Wed Dec 18 16:50:14 2013 +0100 @@ -679,8 +679,8 @@ fun strs_of_type_arg (T as Type (s, _)) = massage_long_name s :: (if generalize_goal andalso in_goal then strs_of_sort (sort_of_type alg T) else []) - | strs_of_type_arg (TFree (s, S)) = strs_of_sort S - | strs_of_type_arg (TVar (s, S)) = strs_of_sort S + | strs_of_type_arg (TFree (_, S)) = strs_of_sort S + | strs_of_type_arg (TVar (_, S)) = strs_of_sort S val typargss = these (try (Sign.const_typargs thy) x) diff -r 287e569eebb2 -r 565f9af86d67 src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML Wed Dec 18 16:50:14 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML Wed Dec 18 16:50:14 2013 +0100 @@ -123,7 +123,7 @@ (* main function for preplaying Isar steps; may throw exceptions *) fun preplay_raw _ _ _ _ _ (Let _) = zero_preplay_time | preplay_raw debug type_enc lam_trans ctxt timeout - (step as Prove (_, xs, _, t, subproofs, (fact_names, (meth :: _) :: _))) = + (Prove (_, xs, _, t, subproofs, (fact_names, (meth :: _) :: _))) = let val goal = (case xs of diff -r 287e569eebb2 -r 565f9af86d67 src/HOL/Tools/Sledgehammer/sledgehammer_print.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_print.ML Wed Dec 18 16:50:14 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_print.ML Wed Dec 18 16:50:14 2013 +0100 @@ -238,7 +238,7 @@ #> add_suffix " = " #> add_term t2 #> add_suffix "\n" - | add_step ind (step as Prove (qs, xs, l, t, subproofs, (facts, (meth :: _) :: _))) = + | add_step ind (Prove (qs, xs, l, t, subproofs, (facts, (meth :: _) :: _))) = add_step_pre ind qs subproofs #> (case xs of [] => add_suffix (of_have qs (length subproofs) ^ " ") diff -r 287e569eebb2 -r 565f9af86d67 src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Wed Dec 18 16:50:14 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Wed Dec 18 16:50:14 2013 +0100 @@ -72,7 +72,7 @@ (* Discard facts; consolidate adjacent lines that prove the same formula, since they differ only in type information. *) -fun add_line_pass1 (line as (name as (_, ss), role, t, rule, [])) lines = +fun add_line_pass1 (line as (name, role, t, rule, [])) lines = (* No dependencies: lemma (for Z3), fact, conjecture, or (for Vampire) internal facts or definitions. *) if role = Lemma orelse role = Conjecture orelse role = Negated_Conjecture orelse @@ -94,7 +94,7 @@ fold_rev add_line_pass2 (map (replace_dependencies_in_line (name, [])) lines) [] fun add_lines_pass3 res [] = rev res - | add_lines_pass3 res ((name as (_, ss), role, t, rule, deps) :: lines) = + | add_lines_pass3 res ((name, role, t, rule, deps) :: lines) = if role <> Plain orelse is_skolemize_rule rule orelse is_arith_rule rule orelse (* the last line must be kept *) null lines orelse @@ -208,7 +208,7 @@ atp_proof, goal) (one_line_params as (_, _, _, _, subgoal, subgoal_count)) = let - val (params, hyp_ts, concl_t) = strip_subgoal goal subgoal ctxt + val (params, _, concl_t) = strip_subgoal goal subgoal ctxt val (_, ctxt) = params |> map (fn (s, T) => (Binding.name s, SOME T, NoSyn)) diff -r 287e569eebb2 -r 565f9af86d67 src/HOL/Tools/Sledgehammer/sledgehammer_run.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Wed Dec 18 16:50:14 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Wed Dec 18 16:50:14 2013 +0100 @@ -65,8 +65,7 @@ (if blocking then "." else "\n" ^ Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i)))) -fun launch_prover (params as {debug, verbose, spy, blocking, max_facts, slice, - timeout, expect, ...}) +fun launch_prover (params as {debug, verbose, spy, blocking, max_facts, timeout, expect, ...}) mode output_result minimize_command only learn {comment, state, goal, subgoal, subgoal_count, factss as (_, facts) :: _} name = let @@ -221,8 +220,8 @@ |> map (fn (filter, facts) => quote filter ^ ": " ^ string_of_facts facts) |> space_implode "\n\n" -fun run_sledgehammer (params as {debug, verbose, spy, blocking, provers, max_facts, slice, ...}) - mode output_result i (fact_override as {only, ...}) minimize_command state = +fun run_sledgehammer (params as {debug, verbose, spy, blocking, provers, max_facts, ...}) mode + output_result i (fact_override as {only, ...}) minimize_command state = if null provers then error "No prover is set." else case subgoal_count state of @@ -250,12 +249,10 @@ val _ = print "Sledgehammering..." val _ = spying spy (fn () => (state, i, "***", "Starting " ^ @{make_string} mode ^ " mode")) - val (ueq_atps, full_provers) = List.partition (is_unit_equational_atp ctxt) provers - val spying_str_of_factss = commas o map (fn (filter, facts) => filter ^ ": " ^ string_of_int (length facts)) - fun get_factss label is_appropriate_prop provers = + fun get_factss provers = let val max_max_facts = case max_facts of @@ -263,28 +260,19 @@ | NONE => 0 |> fold (Integer.max o default_max_facts_of_prover ctxt) provers |> mode = Auto_Try ? (fn n => n div auto_try_max_facts_divisor) - val _ = spying spy (fn () => (state, i, label ^ "s", + val _ = spying spy (fn () => (state, i, "All", "Filtering " ^ string_of_int (length all_facts) ^ " facts")); in all_facts - |> (case is_appropriate_prop of - SOME is_app => filter (is_app o prop_of o snd) - | NONE => I) |> relevant_facts ctxt params (hd provers) max_max_facts fact_override hyp_ts concl_t - |> tap (fn factss => - if verbose then - label ^ plural_s (length provers) ^ ": " ^ - string_of_factss factss - |> print - else - ()) + |> tap (fn factss => if verbose then print (string_of_factss factss) else ()) |> spy ? tap (fn factss => spying spy (fn () => - (state, i, label ^ "s", "Selected facts: " ^ spying_str_of_factss factss))) + (state, i, "All", "Selected facts: " ^ spying_str_of_factss factss))) end - fun launch_provers state label is_appropriate_prop provers = + fun launch_provers state = let - val factss = get_factss label is_appropriate_prop provers + val factss = get_factss provers val problem = {comment = "", state = state, goal = goal, subgoal = i, subgoal_count = n, factss = factss} @@ -303,35 +291,11 @@ |> max_outcome_code |> rpair state end - fun maybe_launch_provers label is_appropriate_prop provers_to_launch accum = - if null provers_to_launch then - accum - else if is_some is_appropriate_prop andalso - not (the is_appropriate_prop concl_t) then - (if verbose orelse length provers_to_launch = length provers then - "Goal outside the scope of " ^ - space_implode " " (serial_commas "and" (map quote provers_to_launch)) ^ "." - |> Output.urgent_message - else - (); - accum) - else - launch_provers state label is_appropriate_prop provers_to_launch - - val launch_full_provers = maybe_launch_provers "ATP/SMT" NONE full_provers - val launch_ueq_atps = maybe_launch_provers "Unit-equational provers" (SOME is_unit_equality) ueq_atps - - fun launch_atps_and_smt_solvers p = - [launch_full_provers, launch_ueq_atps] - |> Par_List.map (fn f => fst (f p)) - handle ERROR msg => (print ("Error: " ^ msg); error msg) - fun maybe f (accum as (outcome_code, _)) = accum |> (mode = Normal orelse outcome_code <> someN) ? f in - (unknownN, state) - |> (if blocking then launch_full_provers - else (fn p => (Future.fork (tap (fn () => launch_full_provers p)); p))) + (if blocking then launch_provers state + else (Future.fork (tap (fn () => launch_provers state)); (unknownN, state))) handle TimeLimit.TimeOut => (print "Sledgehammer ran out of time."; (unknownN, state)) end |> `(fn (outcome_code, _) => outcome_code = someN)