# HG changeset patch # User wenzelm # Date 1307564029 -7200 # Node ID e77baf329f483f94121d7a4734a3a12109698a5c # Parent 755e3d5ea3f2d6a1e5840b1798d361b485d16e35# Parent acc680ab62048e2f8a87d9cec454d17eb90c692c merged diff -r acc680ab6204 -r e77baf329f48 src/HOL/Tools/ATP/atp_problem.ML --- a/src/HOL/Tools/ATP/atp_problem.ML Wed Jun 08 22:06:05 2011 +0200 +++ b/src/HOL/Tools/ATP/atp_problem.ML Wed Jun 08 22:13:49 2011 +0200 @@ -351,9 +351,8 @@ val (n, phis) = phi |> try (clausify_formula true) |> these |> `length in map2 (fn phi => fn j => - Formula (ident ^ - (if n > 1 then "_cls" ^ string_of_int j else ""), - kind, phi, source, info)) + Formula (ident ^ replicate_string (j - 1) "x", kind, phi, source, + info)) phis (1 upto n) end | clausify_formula_line _ = [] diff -r acc680ab6204 -r e77baf329f48 src/HOL/Tools/ATP/atp_reconstruct.ML --- a/src/HOL/Tools/ATP/atp_reconstruct.ML Wed Jun 08 22:06:05 2011 +0200 +++ b/src/HOL/Tools/ATP/atp_reconstruct.ML Wed Jun 08 22:13:49 2011 +0200 @@ -225,25 +225,26 @@ | add_fact _ _ _ _ _ = I fun used_facts_in_atp_proof ctxt type_sys facts_offset fact_names atp_proof = - if null atp_proof then Vector.foldl (op @) [] fact_names + if null atp_proof then Vector.foldl (uncurry (union (op =))) [] fact_names else fold (add_fact ctxt type_sys facts_offset fact_names) atp_proof [] -fun is_conjecture_referred_to_in_proof conjecture_shape = +fun is_conjecture_used_in_proof conjecture_shape = exists (fn Inference (name, _, []) => is_conjecture conjecture_shape name | _ => false) -fun used_facts_in_unsound_atp_proof ctxt type_sys conjecture_shape facts_offset +fun used_facts_in_unsound_atp_proof _ _ _ _ _ [] = NONE + | used_facts_in_unsound_atp_proof ctxt type_sys conjecture_shape facts_offset fact_names atp_proof = - let - val used_facts = - used_facts_in_atp_proof ctxt type_sys facts_offset fact_names atp_proof - in - if forall (is_locality_global o snd) used_facts andalso - not (is_conjecture_referred_to_in_proof conjecture_shape atp_proof) then - SOME (map fst used_facts) - else - NONE - end + let + val used_facts = + used_facts_in_atp_proof ctxt type_sys facts_offset fact_names atp_proof + in + if forall (is_locality_global o snd) used_facts andalso + not (is_conjecture_used_in_proof conjecture_shape atp_proof) then + SOME (map fst used_facts) + else + NONE + end fun uses_typed_helpers typed_helpers = exists (fn Inference (name, _, []) => is_typed_helper typed_helpers name diff -r acc680ab6204 -r e77baf329f48 src/HOL/Tools/ATP/atp_systems.ML --- a/src/HOL/Tools/ATP/atp_systems.ML Wed Jun 08 22:06:05 2011 +0200 +++ b/src/HOL/Tools/ATP/atp_systems.ML Wed Jun 08 22:13:49 2011 +0200 @@ -432,7 +432,7 @@ [(OutOfResources, "Too many function symbols"), (Crashed, "Unrecoverable Segmentation Fault")] Hypothesis Hypothesis [CNF_UEQ] - (K (50, ["poly_args"]) (* FUDGE *)) + (K (50, ["mangled_args", "mangled_tags?"]) (* FUDGE *)) (* Setup *) diff -r acc680ab6204 -r e77baf329f48 src/HOL/Tools/ATP/atp_translate.ML --- a/src/HOL/Tools/ATP/atp_translate.ML Wed Jun 08 22:06:05 2011 +0200 +++ b/src/HOL/Tools/ATP/atp_translate.ML Wed Jun 08 22:13:49 2011 +0200 @@ -625,7 +625,7 @@ CNF_UEQ => (CNF_UEQ, case type_sys of Preds stuff => - (if is_type_sys_fairly_sound type_sys then Preds else Tags) + (if is_type_sys_fairly_sound type_sys then Tags else Preds) stuff | _ => type_sys) | format => (format, type_sys)) @@ -975,16 +975,15 @@ atomic_types = atomic_types} end -fun make_fact ctxt format type_sys keep_trivial eq_as_iff preproc presimp_consts +fun make_fact ctxt format type_sys eq_as_iff preproc presimp_consts ((name, loc), t) = let val thy = Proof_Context.theory_of ctxt in - case (keep_trivial, - t |> preproc ? preprocess_prop ctxt presimp_consts Axiom - |> make_formula thy format type_sys eq_as_iff name loc Axiom) of - (false, - formula as {combformula = AAtom (CombConst ((s, _), _, _)), ...}) => + case t |> preproc ? preprocess_prop ctxt presimp_consts Axiom + |> make_formula thy format type_sys (eq_as_iff andalso format <> CNF) + name loc Axiom of + formula as {combformula = AAtom (CombConst ((s, _), _, _)), ...} => if s = tptp_true then NONE else SOME formula - | (_, formula) => SOME formula + | formula => SOME formula end fun make_conjecture ctxt format prem_kind type_sys preproc presimp_consts ts = @@ -1005,7 +1004,7 @@ t |> preproc ? (preprocess_prop ctxt presimp_consts kind #> freeze_term) |> make_formula thy format type_sys (format <> CNF) - (string_of_int j) General kind + (string_of_int j) Local kind |> maybe_negate end) (0 upto last) ts @@ -1354,7 +1353,7 @@ | _ => I) end) val make_facts = - map_filter (make_fact ctxt format type_sys false false false []) + map_filter (make_fact ctxt format type_sys false false []) val fairly_sound = is_type_sys_fairly_sound type_sys in helper_table @@ -1417,8 +1416,7 @@ val thy = Proof_Context.theory_of ctxt val fact_ts = facts |> map snd val presimp_consts = Meson.presimplified_consts ctxt - val make_fact = - make_fact ctxt format type_sys false true true presimp_consts + val make_fact = make_fact ctxt format type_sys true preproc presimp_consts val (facts, fact_names) = facts |> map (fn (name, t) => (name, t) |> make_fact |> rpair name) |> map_filter (try (apfst the)) @@ -1648,21 +1646,22 @@ (* This inference is described in section 2.3 of Claessen et al.'s "Sorting it out with monotonicity" paper presented at CADE 2011. *) -fun add_combterm_nonmonotonic_types _ _ (SOME false) _ = I - | add_combterm_nonmonotonic_types ctxt level _ +fun add_combterm_nonmonotonic_types _ _ _ (SOME false) _ = I + | add_combterm_nonmonotonic_types ctxt level locality _ (CombApp (CombApp (CombConst ((s, _), Type (_, [T, _]), _), tm1), tm2)) = (is_tptp_equal s andalso exists is_var_or_bound_var [tm1, tm2] andalso (case level of Nonmonotonic_Types => + not (is_locality_global locality) orelse not (is_type_surely_infinite ctxt known_infinite_types T) | Finite_Types => is_type_surely_finite ctxt T | _ => true)) ? insert_type ctxt I (deep_freeze_type T) - | add_combterm_nonmonotonic_types _ _ _ _ = I -fun add_fact_nonmonotonic_types ctxt level ({kind, combformula, ...} + | add_combterm_nonmonotonic_types _ _ _ _ _ = I +fun add_fact_nonmonotonic_types ctxt level ({kind, locality, combformula, ...} : translated_formula) = formula_fold (SOME (kind <> Conjecture)) - (add_combterm_nonmonotonic_types ctxt level) combformula + (add_combterm_nonmonotonic_types ctxt level locality) combformula fun nonmonotonic_types_for_facts ctxt type_sys facts = let val level = level_of_type_sys type_sys in if level = Nonmonotonic_Types orelse level = Finite_Types then diff -r acc680ab6204 -r e77baf329f48 src/HOL/Tools/Metis/metis_reconstruct.ML --- a/src/HOL/Tools/Metis/metis_reconstruct.ML Wed Jun 08 22:06:05 2011 +0200 +++ b/src/HOL/Tools/Metis/metis_reconstruct.ML Wed Jun 08 22:13:49 2011 +0200 @@ -230,7 +230,8 @@ (* Match untyped terms. *) fun untyped_aconv (Const (a, _), Const(b, _)) = (a = b) | untyped_aconv (Free (a, _), Free (b, _)) = (a = b) - | untyped_aconv (Var ((a, _), _), Var ((b, _), _)) = (a = b) + | untyped_aconv (Var ((a, _), _), Var ((b, _), _)) = + (a = b) (* ignore variable numbers *) | untyped_aconv (Bound i, Bound j) = (i = j) | untyped_aconv (Abs (_, _, t), Abs (_, _, u)) = untyped_aconv (t, u) | untyped_aconv (t1 $ t2, u1 $ u2) = diff -r acc680ab6204 -r e77baf329f48 src/HOL/Tools/Metis/metis_translate.ML --- a/src/HOL/Tools/Metis/metis_translate.ML Wed Jun 08 22:06:05 2011 +0200 +++ b/src/HOL/Tools/Metis/metis_translate.ML Wed Jun 08 22:13:49 2011 +0200 @@ -145,6 +145,8 @@ if ident = type_tag_idempotence_helper_name orelse String.isPrefix lightweight_tags_sym_formula_prefix ident then Isa_Reflexive_or_Trivial |> some + else if String.isPrefix conjecture_prefix ident then + NONE else if String.isPrefix helper_prefix ident then case (String.isSuffix typed_helper_suffix ident, space_explode "_" ident) of @@ -155,12 +157,11 @@ |> prepare_helper |> Isa_Raw |> some | _ => raise Fail ("malformed helper identifier " ^ quote ident) - else case try (unprefix conjecture_prefix) ident of + else case try (unprefix fact_prefix) ident of SOME s => - let val j = the (Int.fromString s) in - if j = length clauses then NONE - else Meson.make_meta_clause (nth clauses j) |> Isa_Raw |> some - end + let + val j = s |> space_explode "_" |> List.last |> Int.fromString |> the + in Meson.make_meta_clause (snd (nth clauses j)) |> Isa_Raw |> some end | NONE => TrueI |> Isa_Raw |> some end | metis_axiom_from_atp _ _ = raise Fail "not CNF -- expected formula" @@ -169,31 +170,40 @@ fun prepare_metis_problem ctxt type_sys conj_clauses fact_clauses = let val type_sys = type_sys_from_string type_sys + val (conj_clauses, fact_clauses) = + if polymorphism_of_type_sys type_sys = Polymorphic then + (conj_clauses, fact_clauses) + else + conj_clauses @ fact_clauses + |> map (pair 0) + |> rpair ctxt + |-> Monomorph.monomorph atp_schematic_consts_of + |> fst |> chop (length conj_clauses) + |> pairself (maps (map (zero_var_indexes o snd))) + val num_conjs = length conj_clauses val clauses = - conj_clauses @ fact_clauses - |> (if polymorphism_of_type_sys type_sys = Polymorphic then - I - else - map (pair 0) - #> rpair ctxt - #-> Monomorph.monomorph atp_schematic_consts_of - #> fst #> maps (map (zero_var_indexes o snd))) + map2 (fn j => pair (Int.toString j, Local)) + (0 upto num_conjs - 1) conj_clauses @ + (* "General" below isn't quite correct; the fact could be local. *) + map2 (fn j => pair (Int.toString (num_conjs + j), General)) + (0 upto length fact_clauses - 1) fact_clauses val (old_skolems, props) = - fold_rev (fn clause => fn (old_skolems, props) => - clause |> prop_of |> Logic.strip_imp_concl - |> conceal_old_skolem_terms (length clauses) - old_skolems - ||> (fn prop => prop :: props)) - clauses ([], []) -(* -val _ = tracing ("PROPS:\n" ^ cat_lines (map (Syntax.string_of_term ctxt) props)) -*) + fold_rev (fn (name, th) => fn (old_skolems, props) => + th |> prop_of |> Logic.strip_imp_concl + |> conceal_old_skolem_terms (length clauses) old_skolems + ||> (fn prop => (name, prop) :: props)) + clauses ([], []) + (* + val _ = + tracing ("PROPS:\n" ^ cat_lines (map (Syntax.string_of_term ctxt) props)) + *) val (atp_problem, _, _, _, _, _, sym_tab) = - prepare_atp_problem ctxt CNF Hypothesis Axiom type_sys false false props - @{prop False} [] -(* -val _ = tracing ("ATP PROBLEM: " ^ cat_lines (tptp_lines_for_atp_problem CNF atp_problem)) -*) + prepare_atp_problem ctxt CNF Hypothesis Axiom type_sys false false [] + @{prop False} props + (* + val _ = tracing ("ATP PROBLEM: " ^ + cat_lines (tptp_lines_for_atp_problem CNF atp_problem)) + *) (* "rev" is for compatibility *) val axioms = atp_problem |> maps (map_filter (metis_axiom_from_atp clauses) o snd) diff -r acc680ab6204 -r e77baf329f48 src/HOL/Tools/Sledgehammer/sledgehammer_run.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Wed Jun 08 22:06:05 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Wed Jun 08 22:13:49 2011 +0200 @@ -19,7 +19,7 @@ val timeoutN : string val unknownN : string val auto_minimize_min_facts : int Config.T - val auto_minimize_max_seconds : real Config.T + val auto_minimize_max_time : real Config.T val get_minimizing_prover : Proof.context -> mode -> string -> prover val run_sledgehammer : params -> mode -> int -> relevance_override -> (string -> minimize_command) @@ -69,15 +69,15 @@ val auto_minimize_min_facts = Attrib.setup_config_int @{binding sledgehammer_auto_minimize_min_facts} (fn generic => Config.get_generic generic binary_min_facts) -val auto_minimize_max_seconds = - Attrib.setup_config_real @{binding sledgehammer_auto_minimize_max_seconds} +val auto_minimize_max_time = + Attrib.setup_config_real @{binding sledgehammer_auto_minimize_max_time} (K 5.0) fun minimize ctxt mode name (params as {debug, verbose, isar_proof, ...}) ({state, subgoal, subgoal_count, facts, ...} : prover_problem) (result as {outcome, used_facts, run_time_in_msecs, preplay, message, message_tail} : prover_result) = - if is_some outcome then + if is_some outcome orelse null used_facts then result else let @@ -90,7 +90,7 @@ let fun can_min_fast_enough msecs = 0.001 * Real.fromInt ((num_facts + 2) * msecs) - <= Config.get ctxt auto_minimize_max_seconds + <= Config.get ctxt auto_minimize_max_time val prover_fast_enough = run_time_in_msecs |> Option.map can_min_fast_enough |> the_default false