# HG changeset patch # User blanchet # Date 1277460949 -7200 # Node ID 08fc6b026b018c5eb43993da4999858afcd7a366 # Parent a92a7f45ca28a3e7567affda0e64f4d66dea0761# Parent 6034aac6514382caecbd1da2b39945e2ec4ec6ae merged diff -r a92a7f45ca28 -r 08fc6b026b01 src/HOL/Predicate.thy --- a/src/HOL/Predicate.thy Fri Jun 25 07:19:21 2010 +0200 +++ b/src/HOL/Predicate.thy Fri Jun 25 12:15:49 2010 +0200 @@ -645,7 +645,7 @@ lemma "f () = False \ f () = True" by simp -lemma closure_of_bool_cases: +lemma closure_of_bool_cases [no_atp]: assumes "(f :: unit \ bool) = (%u. False) \ P f" assumes "f = (%u. True) \ P f" shows "P f" diff -r a92a7f45ca28 -r 08fc6b026b01 src/HOL/Tools/ATP_Manager/atp_systems.ML --- a/src/HOL/Tools/ATP_Manager/atp_systems.ML Fri Jun 25 07:19:21 2010 +0200 +++ b/src/HOL/Tools/ATP_Manager/atp_systems.ML Fri Jun 25 12:15:49 2010 +0200 @@ -223,7 +223,7 @@ val conjecture_shape = shape_of_clauses (conjecture_offset + 1) goal_clss val result = do_run false - |> (fn (_, msecs0, _, SOME IncompleteUnprovable) => + |> (fn (_, msecs0, _, SOME _) => do_run true |> (fn (output, msecs, proof, outcome) => (output, msecs0 + msecs, proof, outcome)) @@ -298,9 +298,11 @@ val spass_config : prover_config = {home_var = "SPASS_HOME", executable = "SPASS", + (* "div 2" accounts for the fact that SPASS is often run twice. *) arguments = fn complete => fn timeout => ("-TPTP -Auto -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof \ - \-VarWeight=3 -TimeLimit=" ^ string_of_int (to_generous_secs timeout)) + \-VarWeight=3 -TimeLimit=" ^ + string_of_int (to_generous_secs timeout div 2)) |> not complete ? prefix "-SOS=1 ", proof_delims = [("Here is a proof", "Formulae used in the proof")], known_failures = diff -r a92a7f45ca28 -r 08fc6b026b01 src/HOL/Tools/Sledgehammer/metis_tactics.ML --- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML Fri Jun 25 07:19:21 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML Fri Jun 25 12:15:49 2010 +0200 @@ -446,13 +446,15 @@ of 1, and the use of RSN would increase this typically to 3. Instantiations of those Vars could then fail. See comment on mk_var.*) fun resolve_inc_tyvars(tha,i,thb) = - let val tha = Drule.incr_type_indexes (1 + Thm.maxidx_of thb) tha + let + val tha = Drule.incr_type_indexes (1 + Thm.maxidx_of thb) tha val ths = Seq.list_of (Thm.bicompose false (false,tha,nprems_of tha) i thb) in case distinct Thm.eq_thm ths of [th] => th | _ => raise THM ("resolve_inc_tyvars: unique result expected", i, [tha,thb]) - end; + end + handle TERM (msg, _) => raise METIS ("resolve_inc_tyvars", msg) fun resolve_inf ctxt mode skolem_somes thpairs atm th1 th2 = let diff -r a92a7f45ca28 -r 08fc6b026b01 src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Fri Jun 25 07:19:21 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Fri Jun 25 12:15:49 2010 +0200 @@ -88,10 +88,11 @@ Symtab.map_default (c, [ctyps]) (fn [] => [] | ctypss => insert (op =) ctyps ctypss) -val fresh_sko_prefix = "Sledgehammer.Skox." +val fresh_prefix = "Sledgehammer.Fresh." val flip = Option.map not +val boring_natural_consts = [@{const_name If}] (* Including equality in this list might be expected to stop rules like subset_antisym from being chosen, but for some reason filtering works better with them listed. The logical signs All, Ex, &, and --> are omitted for CNF @@ -113,12 +114,15 @@ | Free x => add_const_type_to_table (const_with_typ thy x) | (t as Const (@{const_name skolem_id}, _)) $ _ => do_term t | t1 $ t2 => do_term t1 #> do_term t2 - | Abs (_, _, t) => do_term t + | Abs (_, _, t) => + (* Abstractions lead to combinators, so we add a penalty for them. *) + add_const_type_to_table (gensym fresh_prefix, []) + #> do_term t | _ => I fun do_quantifier sweet_pos pos body_t = do_formula pos body_t #> (if pos = SOME sweet_pos then I - else add_const_type_to_table (gensym fresh_sko_prefix, [])) + else add_const_type_to_table (gensym fresh_prefix, [])) and do_equality T t1 t2 = fold (if T = @{typ bool} orelse T = @{typ prop} then do_formula NONE else do_term) [t1, t2] @@ -148,7 +152,8 @@ in Symtab.empty |> (if !use_natural_form then - fold (do_formula pos) ts + fold (Symtab.update o rpair []) boring_natural_consts + #> fold (do_formula pos) ts else fold (Symtab.update o rpair []) boring_cnf_consts #> fold do_term ts) @@ -361,9 +366,15 @@ val const_tab = fold (count_axiom_consts theory_relevant thy) axioms Symtab.empty val goal_const_tab = get_consts_typs thy (SOME true) goals + val relevance_threshold = + if !use_natural_form then 0.9 * relevance_threshold (* experimental *) + else relevance_threshold val _ = trace_msg (fn () => "Initial constants: " ^ - commas (Symtab.keys goal_const_tab)) + commas (goal_const_tab + |> Symtab.dest + |> filter (curry (op <>) [] o snd) + |> map fst)) val relevant = relevant_clauses ctxt relevance_convergence defs_relevant max_new relevance_override const_tab relevance_threshold @@ -609,7 +620,7 @@ fun count_literal (Literal (_, t)) = count_combterm t fun count_clause (HOLClause {literals, ...}) = fold count_literal literals -val raw_cnf_rules_pairs = map (fn (name, thm) => (thm, ((name, 0), thm))) +fun raw_cnf_rules_pairs ps = map (fn (name, thm) => (thm, ((name, 0), thm))) ps fun cnf_helper_thms thy raw = map (`Thm.get_name_hint) #> (if raw then raw_cnf_rules_pairs else cnf_rules_pairs thy)