# HG changeset patch # User blanchet # Date 1277311430 -7200 # Node ID 8e56d1ccf1895a1a27623867a49cb3b635a6d7c5 # Parent 9fc2ae73c5caaac219d284743f7a64585a9ea5be improve the new "natural formula" fact filter diff -r 9fc2ae73c5ca -r 8e56d1ccf189 src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Wed Jun 23 16:28:12 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Wed Jun 23 18:43:50 2010 +0200 @@ -88,42 +88,70 @@ Symtab.map_default (c, [ctyps]) (fn [] => [] | ctypss => insert (op =) ctyps ctypss) -val fresh_Ex_prefix = "Sledgehammer.Ex." +val fresh_sko_prefix = "Sledgehammer.Skox." + +val flip = Option.map not -fun get_goal_consts_typs thy goals = +(* 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 + because any remaining occurrences must be within comprehensions. *) +val boring_cnf_consts = + [@{const_name Trueprop}, @{const_name "==>"}, @{const_name all}, + @{const_name "=="}, @{const_name "op |"}, @{const_name Not}, + @{const_name "op ="}] + +fun get_consts_typs thy pos ts = let - val use_natural_form = !use_natural_form (* Free variables are included, as well as constants, to handle locales. "skolem_id" is included to increase the complexity of theorems containing Skolem functions. In non-CNF form, "Ex" is included but each occurrence is considered fresh, to simulate the effect of Skolemization. *) - fun aux (Const (x as (s, _))) = - (if s = @{const_name Ex} andalso use_natural_form then - (gensym fresh_Ex_prefix, []) - else - (const_with_typ thy x)) - |> add_const_type_to_table - | aux (Free x) = add_const_type_to_table (const_with_typ thy x) - | aux ((t as Const (@{const_name skolem_id}, _)) $ _) = aux t - | aux (t $ u) = aux t #> aux u - | aux (Abs (_, _, t)) = aux t - | aux _ = I - (* 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 - because any remaining occurrences must be within comprehensions. *) - val standard_consts = - [@{const_name Trueprop}, @{const_name "==>"}, @{const_name all}, - @{const_name "=="}, @{const_name "op |"}, @{const_name Not}, - @{const_name "op ="}] @ - (if use_natural_form then - [@{const_name All}, @{const_name Ex}, @{const_name "op &"}, - @{const_name "op -->"}] - else - []) + fun do_term t = + case t of + Const x => add_const_type_to_table (const_with_typ thy x) + | 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 + | _ => 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, [])) + and do_equality T t1 t2 = + fold (if T = @{typ bool} orelse T = @{typ prop} then do_formula NONE + else do_term) [t1, t2] + and do_formula pos t = + case t of + Const (@{const_name all}, _) $ Abs (_, _, body_t) => + do_quantifier false pos body_t + | @{const "==>"} $ t1 $ t2 => + do_formula (flip pos) t1 #> do_formula pos t2 + | Const (@{const_name "=="}, Type (_, [T, _])) $ t1 $ t2 => + do_equality T t1 t2 + | @{const Trueprop} $ t1 => do_formula pos t1 + | @{const Not} $ t1 => do_formula (flip pos) t1 + | Const (@{const_name All}, _) $ Abs (_, _, body_t) => + do_quantifier false pos body_t + | Const (@{const_name Ex}, _) $ Abs (_, _, body_t) => + do_quantifier true pos body_t + | @{const "op &"} $ t1 $ t2 => fold (do_formula pos) [t1, t2] + | @{const "op |"} $ t1 $ t2 => fold (do_formula pos) [t1, t2] + | @{const "op -->"} $ t1 $ t2 => + do_formula (flip pos) t1 #> do_formula pos t2 + | Const (@{const_name "op ="}, Type (_, [T, _])) $ t1 $ t2 => + do_equality T t1 t2 + | (t0 as Const (_, @{typ bool})) $ t1 => + do_term t0 #> do_formula pos t1 (* theory constant *) + | _ => do_term t in - Symtab.empty |> fold (Symtab.update o rpair []) standard_consts - |> fold aux goals + Symtab.empty + |> (if !use_natural_form then + fold (do_formula pos) ts + else + fold (Symtab.update o rpair []) boring_cnf_consts + #> fold do_term ts) end (*Inserts a dummy "constant" referring to the theory name, so that relevance @@ -217,7 +245,7 @@ fun add_expand_pairs (x,ys) xys = List.foldl (fn (y,acc) => (x,y)::acc) xys ys; fun consts_typs_of_term thy t = - Symtab.fold add_expand_pairs (get_goal_consts_typs thy [t]) [] + Symtab.fold add_expand_pairs (get_consts_typs thy (SOME false) [t]) [] fun pair_consts_typs_axiom theory_relevant thy axiom = (axiom, axiom |> appropriate_prop_of theory_relevant @@ -306,9 +334,11 @@ if weight >= threshold orelse (defs_relevant andalso defines thy (#1 clsthm) rel_const_tab) then - (trace_msg (fn () => name ^ " clause " ^ Int.toString n ^ - " passes: " ^ Real.toString weight); - relevant ((ax, weight) :: newrels, rejects) axs) + (trace_msg (fn () => + name ^ " clause " ^ Int.toString n ^ + " passes: " ^ Real.toString weight + (* ^ " consts: " ^ commas (map fst consts_typs) *)); + relevant ((ax, weight) :: newrels, rejects) axs) else relevant (newrels, ax :: rejects) axs end @@ -326,7 +356,7 @@ let val const_tab = fold (count_axiom_consts theory_relevant thy) axioms Symtab.empty - val goal_const_tab = get_goal_consts_typs thy goals + val goal_const_tab = get_consts_typs thy (SOME true) goals val _ = trace_msg (fn () => "Initial constants: " ^ commas (Symtab.keys goal_const_tab))