# HG changeset patch # User immler # Date 1387270330 -3600 # Node ID 5e8bdb42078c393f8653b29fec8ff61fc61c3d2a # Parent 4876fb408c0d0985c8f0bd0eb07c9f79ea48e621# Parent bddb91fb8e374a78261f994d1203629e8f39928c merged diff -r 4876fb408c0d -r 5e8bdb42078c src/HOL/Tools/ATP/atp_problem_generate.ML --- a/src/HOL/Tools/ATP/atp_problem_generate.ML Mon Dec 16 17:08:22 2013 +0100 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Tue Dec 17 09:52:10 2013 +0100 @@ -1958,6 +1958,10 @@ end in List.partition (curry (op =) Definition o #role) #>> reorder [] #> op @ end +fun s_not_prop (@{const Trueprop} $ t) = @{const Trueprop} $ s_not t + | s_not_prop (@{const "==>"} $ t $ @{prop False}) = t + | s_not_prop t = @{const "==>"} $ t $ @{prop False} + fun translate_formulas ctxt prem_role format type_enc lam_trans presimp hyp_ts concl_t facts = let diff -r 4876fb408c0d -r 5e8bdb42078c src/HOL/Tools/ATP/atp_proof.ML --- a/src/HOL/Tools/ATP/atp_proof.ML Mon Dec 16 17:08:22 2013 +0100 +++ b/src/HOL/Tools/ATP/atp_proof.ML Tue Dec 17 09:52:10 2013 +0100 @@ -231,8 +231,7 @@ val dummy_phi = AAtom (ATerm (("", []), [])) val dummy_inference = Inference_Source ("", []) -(* "skip_term" is there to cope with Waldmeister nonsense such as - "theory(equality)". *) +(* "skip_term" is there to cope with Waldmeister nonsense such as "theory(equality)". *) fun parse_dependency x = (parse_inference_source >> snd || scan_general_id --| skip_term >> single) x @@ -469,8 +468,7 @@ (* Syntax: core(,[,...,]). *) fun parse_z3_tptp_line x = (scan_general_id --| $$ "," --| $$ "[" -- parse_dependencies --| $$ "]" - >> (fn (name, names) => - (("", name :: names), Unknown, dummy_phi, z3_tptp_coreN, []))) x + >> (fn (name, names) => (("", name :: names), Unknown, dummy_phi, z3_tptp_coreN, []))) x (* Syntax: *) fun parse_satallax_line x = diff -r 4876fb408c0d -r 5e8bdb42078c src/HOL/Tools/ATP/atp_proof_reconstruct.ML --- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Mon Dec 16 17:08:22 2013 +0100 +++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Tue Dec 17 09:52:10 2013 +0100 @@ -11,9 +11,11 @@ type ('a, 'b) atp_term = ('a, 'b) ATP_Problem.atp_term type ('a, 'b, 'c, 'd) atp_formula = ('a, 'b, 'c, 'd) ATP_Problem.atp_formula type stature = ATP_Problem_Generate.stature + type atp_step_name = ATP_Proof.atp_step_name type ('a, 'b) atp_step = ('a, 'b) ATP_Proof.atp_step type 'a atp_proof = 'a ATP_Proof.atp_proof + val spass_skolemize_rule : string val metisN : string val full_typesN : string val partial_typesN : string @@ -25,6 +27,7 @@ val full_type_encs : string list val partial_type_encs : string list val default_metis_lam_trans : string + val metis_call : string -> string -> string val forall_of : term -> term -> term val exists_of : term -> term -> term @@ -40,8 +43,11 @@ 'a atp_proof -> string list option val lam_trans_of_atp_proof : string atp_proof -> string -> string val is_typed_helper_used_in_atp_proof : string atp_proof -> bool + val replace_dependencies_in_line : atp_step_name * atp_step_name list -> ('a, 'b) atp_step -> + ('a, 'b) atp_step val termify_atp_proof : Proof.context -> string Symtab.table -> (string * term) list -> int Symtab.table -> string atp_proof -> (term, string) atp_step list + val introduce_spass_skolem : (term, string) atp_step list -> (term, string) atp_step list val factify_atp_proof : (string * 'a) list vector -> term list -> term -> (term, string) atp_step list -> (term, string) atp_step list end; @@ -54,6 +60,9 @@ open ATP_Proof open ATP_Problem_Generate +val spass_input_rule = "Inp" +val spass_skolemize_rule = "__Sko" (* arbitrary *) + val metisN = "metis" val full_typesN = "full_types" @@ -174,6 +183,7 @@ fun loose_aconv (Free (s, _), Free (s', _)) = s = s' | loose_aconv (t, t') = t aconv t' +val spass_skolem_prefix = "sk" (* "skc" or "skf" *) val vampire_skolem_prefix = "sK" (* First-order translation. No types are known for variables. "HOLogic.typeT" @@ -268,9 +278,10 @@ [(s, ())] |> Variable.variant_frees ctxt [] |> hd |> fst val term_ts = map (do_term [] NONE) us - (* Vampire (2.6) passes arguments to Skolem functions in reverse - order *) - |> String.isPrefix vampire_skolem_prefix s ? rev + (* SPASS (3.8ds) and Vampire (2.6) pass arguments to Skolem functions in reverse + order, which is incompatible with the new Metis skolemizer. *) + |> exists (fn pre => String.isPrefix pre s) + [spass_skolem_prefix, vampire_skolem_prefix] ? rev val ts = term_ts @ extra_ts val T = case opt_T of @@ -334,9 +345,8 @@ | AQuant (q, (s, _) :: xs, phi') => do_formula pos (AQuant (q, xs, phi')) (* FIXME: TFF *) - #>> quantify_over_var - (case q of AForall => forall_of | AExists => exists_of) - (s |> textual ? repair_var_name) + #>> quantify_over_var (case q of AForall => forall_of | AExists => exists_of) + (s |> textual ? repair_var_name) | AConn (ANot, [phi']) => do_formula (not pos) phi' #>> s_not | AConn (c, [phi1, phi2]) => do_formula (pos |> c = AImplies ? not) phi1 @@ -452,6 +462,10 @@ fun is_typed_helper_used_in_atp_proof atp_proof = is_axiom_used_in_proof is_typed_helper_name atp_proof +fun replace_one_dependency (old, new) dep = if is_same_atp_step dep old then new else [dep] +fun replace_dependencies_in_line old_new (name, role, t, rule, deps) = + (name, role, t, rule, fold (union (op =) o replace_one_dependency old_new) deps []) + fun repair_name "$true" = "c_True" | repair_name "$false" = "c_False" | repair_name "$$e" = tptp_equal (* seen in Vampire proofs *) @@ -529,6 +543,58 @@ #> map (termify_line ctxt lifted sym_tab) #> repair_waldmeister_endgame +fun introduce_spass_skolem [] = [] + | introduce_spass_skolem (proof as (_, _, _, rule1, _) :: _) = + if rule1 = spass_input_rule then + let + fun add_sko (Free (s, _)) = String.isPrefix spass_skolem_prefix s ? insert (op =) s + | add_sko _ = I + + (* union-find would be faster *) + fun add_cycle _ [] = I + | add_cycle name ss = + fold (fn s => Graph.default_node (s, ())) ss + #> fold Graph.add_edge (ss ~~ tl ss @ [hd ss]) + + val (input_steps, other_steps) = List.partition (null o #5) proof + + 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 + + fun step_name_of_group skos = (implode skos, []) + fun in_group group = member (op =) group o hd + fun group_of sko = the (find_first (fn group => in_group group sko) groups) + + fun new_step group (skoss_steps : ('a * (term, 'b) atp_step) list) = + let + val t = + skoss_steps + |> map (snd #> #3 #> HOLogic.dest_Trueprop) + |> Library.foldr1 s_conj + |> HOLogic.mk_Trueprop + val deps = map (snd #> #1) skoss_steps + in + (step_name_of_group group, Plain, t, spass_skolemize_rule, deps) + end + + val sko_steps = + map (fn group => new_step group (filter (in_group group o fst) skoss_input_steps)) groups + + val old_news = + map (fn (skos, (name, _, _, _, _)) => (name, [step_name_of_group (group_of skos)])) + skoss_input_steps + val repair_deps = fold replace_dependencies_in_line old_news + in + input_steps @ sko_steps @ map repair_deps other_steps + end + else + proof + fun factify_atp_proof fact_names hyp_ts concl_t atp_proof = let fun factify_step ((num, ss), role, t, rule, deps) = @@ -550,7 +616,8 @@ fun repair_dep (num, ss) = (num, the_default ss (AList.lookup (op =) names num)) fun repair_deps (name, role, t, rule, deps) = (name, role, t, rule, map repair_dep deps) - - in map repair_deps atp_proof end + in + map repair_deps atp_proof + end end; diff -r 4876fb408c0d -r 5e8bdb42078c src/HOL/Tools/ATP/atp_util.ML --- a/src/HOL/Tools/ATP/atp_util.ML Mon Dec 16 17:08:22 2013 +0100 +++ b/src/HOL/Tools/ATP/atp_util.ML Tue Dec 17 09:52:10 2013 +0100 @@ -36,7 +36,6 @@ val s_disj : term * term -> term val s_imp : term * term -> term val s_iff : term * term -> term - val s_not_prop : term -> term val close_form : term -> term val hol_close_form_prefix : string val hol_close_form : term -> term @@ -308,10 +307,6 @@ | s_iff (t1, @{const False}) = s_not t1 | s_iff (t1, t2) = HOLogic.eq_const HOLogic.boolT $ t1 $ t2 -fun s_not_prop (@{const Trueprop} $ t) = @{const Trueprop} $ s_not t - | s_not_prop (@{const "==>"} $ t $ @{prop False}) = t - | s_not_prop t = @{const "==>"} $ t $ @{prop False} - fun close_form t = fold (fn ((s, i), T) => fn t' => Logic.all_const T $ Abs (s, T, abstract_over (Var ((s, i), T), t'))) diff -r 4876fb408c0d -r 5e8bdb42078c src/HOL/Tools/Sledgehammer/sledgehammer_print.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_print.ML Mon Dec 16 17:08:22 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_print.ML Tue Dec 17 09:52:10 2013 +0100 @@ -82,8 +82,7 @@ |> pairself (sort_distinct (string_ord o pairself fst)) fun one_line_proof_text num_chained - (preplay, banner, used_facts, minimize_command, subgoal, - subgoal_count) = + (preplay, banner, used_facts, minimize_command, subgoal, subgoal_count) = let val (chained, extra) = split_used_facts used_facts val (failed, reconstr, ext_time) = @@ -91,10 +90,9 @@ Played (reconstr, time) => (false, reconstr, (SOME (false, time))) | Trust_Playable (reconstr, time) => (false, reconstr, - case time of + (case time of NONE => NONE - | SOME time => - if time = Time.zeroTime then NONE else SOME (true, time)) + | SOME time => if time = Time.zeroTime then NONE else SOME (true, time))) | Failed_to_Play reconstr => (true, reconstr, NONE) val try_line = ([], map fst extra) @@ -105,9 +103,9 @@ \solve this.)" else try_command_line banner ext_time) - in try_line ^ minimize_line minimize_command (map fst (extra @ chained)) end - - + in + try_line ^ minimize_line minimize_command (map fst (extra @ chained)) + end (** detailed Isar proofs **) diff -r 4876fb408c0d -r 5e8bdb42078c src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Mon Dec 16 17:08:22 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Tue Dec 17 09:52:10 2013 +0100 @@ -394,8 +394,7 @@ fun is_fact_chained ((_, (sc, _)), _) = sc = Chained fun filter_used_facts keep_chained used = - filter ((member (op =) used o fst) orf - (if keep_chained then is_fact_chained else K false)) + filter ((member (op =) used o fst) orf (if keep_chained then is_fact_chained else K false)) fun play_one_line_proof mode debug verbose timeout pairs state i preferred reconstrs = @@ -847,6 +846,7 @@ val atp_proof = atp_proof |> termify_atp_proof ctxt pool lifted sym_tab + |> introduce_spass_skolem |> factify_atp_proof fact_names hyp_ts concl_t in (debug, verbose, metis_type_enc, metis_lam_trans, preplay_timeout, diff -r 4876fb408c0d -r 5e8bdb42078c src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Mon Dec 16 17:08:22 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Tue Dec 17 09:52:10 2013 +0100 @@ -7,6 +7,7 @@ signature SLEDGEHAMMER_RECONSTRUCT = sig + type atp_step_name = ATP_Proof.atp_step_name type ('a, 'b) atp_step = ('a, 'b) ATP_Proof.atp_step type 'a atp_proof = 'a ATP_Proof.atp_proof type stature = ATP_Problem_Generate.stature @@ -46,19 +47,16 @@ open String_Redirect -val e_skolemize_rule = "skolemize" +val e_skolemize_rules = ["skolemize", "shift_quantors"] val vampire_skolemisation_rule = "skolemisation" (* TODO: Use "Z3_Proof.string_of_rule" once it is moved to Isabelle *) -val z3_apply_def_rule = "apply-def" -val z3_hypothesis_rule = "hypothesis" -val z3_intro_def_rule = "intro-def" -val z3_lemma_rule = "lemma" val z3_skolemize_rule = "sk" val z3_th_lemma_rule = "th-lemma" -val is_skolemize_rule = - member (op =) [e_skolemize_rule, vampire_skolemisation_rule, z3_skolemize_rule] +val skolemize_rules = + e_skolemize_rules @ [spass_skolemize_rule, vampire_skolemisation_rule, z3_skolemize_rule] +val is_skolemize_rule = member (op =) skolemize_rules val is_arith_rule = String.isPrefix z3_th_lemma_rule fun raw_label_of_num num = (num, 0) @@ -69,69 +67,14 @@ fun add_fact_of_dependencies [(_, ss as _ :: _)] = apsnd (union (op =) ss) | add_fact_of_dependencies names = apfst (insert (op =) (label_of_clause names)) -fun replace_one_dependency (old, new) dep = - if is_same_atp_step dep old then new else [dep] -fun replace_dependencies_in_line p (name, role, t, rule, deps) = - (name, role, t, rule, fold (union (op =) o replace_one_dependency p) deps []) - -fun inline_z3_defs _ [] = [] - | inline_z3_defs defs ((line as (name, role, t, rule, deps)) :: lines) = - if rule = z3_intro_def_rule then - let val def = t |> HOLogic.dest_Trueprop |> HOLogic.dest_eq |> swap in - inline_z3_defs (insert (op =) def defs) - (map (replace_dependencies_in_line (name, [])) lines) - end - else if rule = z3_apply_def_rule then - inline_z3_defs defs (map (replace_dependencies_in_line (name, [])) lines) - else - (name, role, Term.subst_atomic defs t, rule, deps) :: inline_z3_defs defs lines - -fun alist_cons_list eq (k, v) = AList.map_default eq (k, []) (cons v) - -fun add_z3_hypotheses [] = I - | add_z3_hypotheses hyps = - HOLogic.dest_Trueprop - #> curry s_imp (Library.foldr1 s_conj (map HOLogic.dest_Trueprop hyps)) - #> HOLogic.mk_Trueprop - -fun inline_z3_hypotheses _ _ [] = [] - | inline_z3_hypotheses hyp_names hyps ((name, role, t, rule, deps) :: lines) = - if rule = z3_hypothesis_rule then - inline_z3_hypotheses (name :: hyp_names) (alist_cons_list (op =) (t, name) hyps) lines - else - let val deps' = subtract (op =) hyp_names deps in - if rule = z3_lemma_rule then - (name, role, t, rule, deps') :: inline_z3_hypotheses hyp_names hyps lines - else - let - val add_hyps = filter_out (null o inter (op =) deps o snd) hyps - val t' = add_z3_hypotheses (map fst add_hyps) t - val deps' = subtract (op =) hyp_names deps - val hyps' = fold (AList.update (op =) o apsnd (insert (op =) name)) add_hyps hyps - in - (name, role, t', rule, deps') :: inline_z3_hypotheses hyp_names hyps' lines - end - end - -fun simplify_prop (@{const Not} $ t) = s_not (simplify_prop t) - | simplify_prop (@{const conj} $ t $ u) = s_conj (simplify_prop t, simplify_prop u) - | simplify_prop (@{const disj} $ t $ u) = s_disj (simplify_prop t, simplify_prop u) - | simplify_prop (@{const implies} $ t $ u) = s_imp (simplify_prop t, simplify_prop u) - | simplify_prop (@{const HOL.eq (bool)} $ t $ u) = s_iff (simplify_prop t, simplify_prop u) - | simplify_prop (t $ u) = simplify_prop t $ simplify_prop u - | simplify_prop (Abs (s, T, t)) = Abs (s, T, simplify_prop t) - | simplify_prop t = t - -fun simplify_line (name, role, t, rule, deps) = (name, role, simplify_prop t, rule, deps) - (* No "real" literals means only type information (tfree_tcs, clsrel, or clsarity). *) fun is_only_type_information t = t aconv @{prop True} (* 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 = - (* No dependencies: lemma (for Z3), fact, conjecture, or (for Vampire) - internal facts or definitions. *) + (* 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 role = Hypothesis orelse is_arith_rule rule then line :: lines @@ -150,8 +93,8 @@ and delete_dependency name lines = fold_rev add_line_pass2 (map (replace_dependencies_in_line (name, [])) lines) [] -fun add_line_pass3 res [] = rev res - | add_line_pass3 res ((name as (_, ss), role, t, rule, deps) :: lines) = +fun add_lines_pass3 res [] = rev res + | add_lines_pass3 res ((name as (_, ss), 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 @@ -159,9 +102,9 @@ andalso length deps >= 2 andalso (* don't keep next to last line, which usually results in a trivial step *) not (can the_single lines)) then - add_line_pass3 ((name, role, simplify_prop t, rule, deps) :: res) lines + add_lines_pass3 ((name, role, t, rule, deps) :: res) lines else - add_line_pass3 res (map (replace_dependencies_in_line (name, deps)) lines) + add_lines_pass3 res (map (replace_dependencies_in_line (name, deps)) lines) val add_labels_of_proof = steps_of_proof @@ -283,12 +226,9 @@ let val atp_proof = atp_proof - |> inline_z3_defs [] - |> map simplify_line - |> inline_z3_hypotheses [] [] |> rpair [] |-> fold_rev add_line_pass1 |> rpair [] |-> fold_rev add_line_pass2 - |> add_line_pass3 [] + |> add_lines_pass3 [] val conjs = map_filter (fn (name, role, _, _, _) => @@ -324,8 +264,10 @@ |> fold (fn (name as (s, _), role, t, rule, _) => Symtab.update_new (s, (rule, t |> (if is_clause_tainted [name] then - role <> Conjecture ? s_not_prop + HOLogic.dest_Trueprop + #> role <> Conjecture ? s_not #> fold exists_of (map Var (Term.add_vars t [])) + #> HOLogic.mk_Trueprop else I)))) atp_proof diff -r 4876fb408c0d -r 5e8bdb42078c src/HOL/Tools/Sledgehammer/sledgehammer_reconstructor.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstructor.ML Mon Dec 16 17:08:22 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstructor.ML Tue Dec 17 09:52:10 2013 +0100 @@ -19,9 +19,7 @@ Failed_to_Play of reconstructor type minimize_command = string list -> string - - type one_line_params = - play * string * (string * stature) list * minimize_command * int * int + type one_line_params = play * string * (string * stature) list * minimize_command * int * int val smtN : string end; @@ -41,9 +39,7 @@ Failed_to_Play of reconstructor type minimize_command = string list -> string - -type one_line_params = - play * string * (string * stature) list * minimize_command * int * int +type one_line_params = play * string * (string * stature) list * minimize_command * int * int val smtN = "smt" diff -r 4876fb408c0d -r 5e8bdb42078c src/HOL/Tools/Sledgehammer/sledgehammer_run.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Mon Dec 16 17:08:22 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Tue Dec 17 09:52:10 2013 +0100 @@ -108,13 +108,17 @@ tag_list 1 facts |> map (fn (j, fact) => fact |> apsnd (K j)) |> filter_used_facts false used_facts + |> distinct (eq_fst (op =)) |> map (prefix "@" o string_of_int o snd) fun filter_info (fact_filter, facts) = let val indices = find_indices facts - val unknowns = replicate (num_used_facts - length indices) "?" - in (commas (indices @ unknowns), fact_filter) end + (* "Int.max" is there for robustness -- it shouldn't be necessary *) + val unknowns = replicate (Int.max (0, num_used_facts - length indices)) "?" + in + (commas (indices @ unknowns), fact_filter) + end val filter_infos = map filter_info (("actual", used_from) :: factss)