# HG changeset patch # User blanchet # Date 1280408035 -7200 # Node ID cc44e887246c481b807eb8149af7fe322ab03852 # Parent e2aac207d13b8c58070ab29c3883b2ea995fc347 avoid "clause" and "cnf" terminology where it no longer makes sense diff -r e2aac207d13b -r cc44e887246c src/HOL/Tools/Sledgehammer/sledgehammer.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Thu Jul 29 14:42:09 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Thu Jul 29 14:53:55 2010 +0200 @@ -171,12 +171,12 @@ AConn (AImplies, [fold (mk_aconn AAnd) phis phi, psi]) (* ### FIXME: reintroduce -fun make_clause_table xs = +fun make_formula_table xs = fold (Termtab.update o `(prop_of o snd)) xs Termtab.empty -(* Remove existing axiom clauses from the conjecture clauses, as this can +(* Remove existing axioms from the conjecture, as this can dramatically boost an ATP's performance (for some reason). *) -fun subtract_cls ax_clauses = - filter_out (Termtab.defined (make_clause_table ax_clauses) o prop_of) +fun subtract_cls axioms = + filter_out (Termtab.defined (make_formula_table axioms) o prop_of) *) fun combformula_for_prop thy = @@ -277,8 +277,8 @@ Axiom => HOLogic.true_const | Conjecture => HOLogic.false_const -(* making axiom and conjecture clauses *) -fun make_clause ctxt (formula_name, kind, t) = +(* making axiom and conjecture formulas *) +fun make_formula ctxt (formula_name, kind, t) = let val thy = ProofContext.theory_of ctxt (* ### FIXME: perform other transformations previously done by @@ -293,13 +293,13 @@ kind = kind, ctypes_sorts = ctypes_sorts} end -fun make_axiom_clause ctxt (name, th) = - (name, make_clause ctxt (name, Axiom, prop_of th)) -fun make_conjecture_clauses ctxt ts = - map2 (fn j => fn t => make_clause ctxt (Int.toString j, Conjecture, t)) +fun make_axiom ctxt (name, th) = + (name, make_formula ctxt (name, Axiom, prop_of th)) +fun make_conjectures ctxt ts = + map2 (fn j => fn t => make_formula ctxt (Int.toString j, Conjecture, t)) (0 upto length ts - 1) ts -(** Helper clauses **) +(** Helper facts **) fun count_combterm (CombConst ((s, _), _, _)) = Symtab.map_entry s (Integer.add 1) @@ -324,24 +324,24 @@ Symtab.make (maps (maps (map (rpair 0) o fst)) [optional_helpers, optional_typed_helpers]) -fun get_helper_clauses ctxt is_FO full_types conjectures axclauses = +fun get_helper_facts ctxt is_FO full_types conjectures axioms = let - val ct = fold (fold count_fol_formula) [conjectures, axclauses] - init_counters + val ct = fold (fold count_fol_formula) [conjectures, axioms] init_counters fun is_needed c = the (Symtab.lookup ct c) > 0 - val cnfs = - (optional_helpers - |> full_types ? append optional_typed_helpers - |> maps (fn (ss, ths) => - if exists is_needed ss then map (`Thm.get_name_hint) ths - else [])) @ - (if is_FO then [] else map (`Thm.get_name_hint) mandatory_helpers) - in map (snd o make_axiom_clause ctxt) cnfs end + in + (optional_helpers + |> full_types ? append optional_typed_helpers + |> maps (fn (ss, ths) => + if exists is_needed ss then map (`Thm.get_name_hint) ths + else [])) @ + (if is_FO then [] else map (`Thm.get_name_hint) mandatory_helpers) + |> map (snd o make_axiom ctxt) + end fun s_not (@{const Not} $ t) = t | s_not t = @{const Not} $ t -fun prepare_clauses ctxt full_types hyp_ts concl_t axcls = +fun prepare_formulas ctxt full_types hyp_ts concl_t axcls = let val thy = ProofContext.theory_of ctxt val goal_t = Logic.list_implies (hyp_ts, concl_t) @@ -350,19 +350,18 @@ val subs = tfree_classes_of_terms [goal_t] val supers = tvar_classes_of_terms axtms val tycons = type_consts_of_terms thy (goal_t :: axtms) - (* TFrees in conjecture clauses; TVars in axiom clauses *) + (* TFrees in the conjecture; TVars in the axioms *) val conjectures = map (s_not o HOLogic.dest_Trueprop) hyp_ts @ - [HOLogic.dest_Trueprop concl_t] - |> make_conjecture_clauses ctxt - val (clnames, axioms) = ListPair.unzip (map (make_axiom_clause ctxt) axcls) - val helper_clauses = - get_helper_clauses ctxt is_FO full_types conjectures axioms + [HOLogic.dest_Trueprop concl_t] + |> make_conjectures ctxt + val (clnames, axioms) = ListPair.unzip (map (make_axiom ctxt) axcls) + val helper_facts = get_helper_facts ctxt is_FO full_types conjectures axioms val (supers', arity_clauses) = make_arity_clauses thy tycons supers val class_rel_clauses = make_class_rel_clauses thy subs supers' in (Vector.fromList clnames, - (conjectures, axioms, helper_clauses, class_rel_clauses, arity_clauses)) + (conjectures, axioms, helper_facts, class_rel_clauses, arity_clauses)) end fun wrap_type ty t = ATerm ((type_wrapper_name, type_wrapper_name), [ty, t]) @@ -585,14 +584,14 @@ (const_table_for_problem explicit_apply problem) problem fun write_tptp_file thy readable_names explicit_forall full_types explicit_apply - file (conjectures, axioms, helper_clauses, - class_rel_clauses, arity_clauses) = + file (conjectures, axioms, helper_facts, class_rel_clauses, + arity_clauses) = let val axiom_lines = map (problem_line_for_axiom full_types) axioms val class_rel_lines = map problem_line_for_class_rel_clause class_rel_clauses val arity_lines = map problem_line_for_arity_clause arity_clauses - val helper_lines = map (problem_line_for_axiom full_types) helper_clauses + val helper_lines = map (problem_line_for_axiom full_types) helper_facts val conjecture_lines = map (problem_line_for_conjecture full_types) conjectures val tfree_lines = problem_lines_for_free_types conjectures @@ -675,7 +674,6 @@ minimize_command timeout ({subgoal, goal, relevance_override, axioms} : problem) = let - (* get clauses and prepare them for writing *) val (ctxt, (_, th)) = goal; val thy = ProofContext.theory_of ctxt (* ### FIXME: (1) preprocessing for "if" etc. *) @@ -688,8 +686,8 @@ max_new_relevant_facts_per_iter (the_default prefers_theory_relevant theory_relevant) relevance_override goal hyp_ts concl_t - val (internal_thm_names, clauses) = - prepare_clauses ctxt full_types hyp_ts concl_t the_axioms + val (internal_thm_names, formulas) = + prepare_formulas ctxt full_types hyp_ts concl_t the_axioms (* path to unique problem file *) val the_dest_dir = if overlord then getenv "ISABELLE_HOME_USER" @@ -757,7 +755,7 @@ val readable_names = debug andalso overlord val (pool, conjecture_offset) = write_tptp_file thy readable_names explicit_forall full_types - explicit_apply probfile clauses + explicit_apply probfile formulas val conjecture_shape = conjecture_offset + 1 upto conjecture_offset + length hyp_ts + 1 |> map single diff -r e2aac207d13b -r cc44e887246c src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Thu Jul 29 14:42:09 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Thu Jul 29 14:53:55 2010 +0200 @@ -88,18 +88,8 @@ (fn [] => [] | ctypss => insert (op =) ctyps ctypss) 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 - 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 @@ -213,11 +203,8 @@ (the (Symtab.lookup const_tab c) handle Option.Option => raise Fail ("Const: " ^ c)) 0 -(*A surprising number of theorems contain only a few significant constants. - These include all induction rules, and other general theorems. Filtering - theorems in clause form reveals these complexities in the form of Skolem - functions. If we were instead to filter theorems in their natural form, - some other method of measuring theorem complexity would become necessary.*) +(* A surprising number of theorems contain only a few significant constants. + These include all induction rules, and other general theorems. *) (* "log" seems best in practice. A constant function of one ignores the constant frequencies. *) @@ -228,8 +215,8 @@ (*Relevant constants are weighted according to frequency, but irrelevant constants are simply counted. Otherwise, Skolem functions, - which are rare, would harm a clause's chances of being picked.*) -fun clause_weight const_tab gctyps consts_typs = + which are rare, would harm a formula's chances of being picked.*) +fun formula_weight const_tab gctyps consts_typs = let val rel = filter (uni_mem gctyps) consts_typs val rel_weight = fold (curry Real.+ o ct_weight const_tab) rel 0.0 in @@ -270,13 +257,13 @@ | _ => false end; -type annotated_cnf_thm = (string * thm) * (string * const_typ list) list +type annotated_thm = (string * thm) * (string * const_typ list) list (*For a reverse sort, putting the largest values first.*) fun compare_pairs ((_, w1), (_, w2)) = Real.compare (w2, w1) -(*Limit the number of new clauses, to prevent runaway acceptance.*) -fun take_best max_new (newpairs : (annotated_cnf_thm * real) list) = +(* Limit the number of new facts, to prevent runaway acceptance. *) +fun take_best max_new (newpairs : (annotated_thm * real) list) = let val nnew = length newpairs in if nnew <= max_new then (map #1 newpairs, []) @@ -294,8 +281,8 @@ end end; -fun relevant_clauses ctxt relevance_convergence defs_relevant max_new - ({add, del, ...} : relevance_override) const_tab = +fun relevant_facts ctxt relevance_convergence defs_relevant max_new + ({add, del, ...} : relevance_override) const_tab = let val thy = ProofContext.theory_of ctxt val add_thms = maps (ProofContext.get_fact ctxt) add @@ -323,7 +310,7 @@ val weight = if member Thm.eq_thm add_thms th then 1.0 else if member Thm.eq_thm del_thms th then 0.0 - else clause_weight const_tab rel_const_tab consts_typs + else formula_weight const_tab rel_const_tab consts_typs in if weight >= threshold orelse (defs_relevant andalso defines thy th rel_const_tab) then @@ -335,7 +322,7 @@ relevant (newrels, ax :: rejects) axs end in - trace_msg (fn () => "relevant_clauses, current threshold: " ^ + trace_msg (fn () => "relevant_facts, current threshold: " ^ Real.toString threshold); relevant ([], []) end @@ -361,11 +348,11 @@ |> filter (curry (op <>) [] o snd) |> map fst)) val relevant = - relevant_clauses ctxt relevance_convergence defs_relevant max_new - relevance_override const_tab relevance_threshold - goal_const_tab - (map (pair_consts_typs_axiom theory_relevant thy) - axioms) + relevant_facts ctxt relevance_convergence defs_relevant max_new + relevance_override const_tab relevance_threshold + goal_const_tab + (map (pair_consts_typs_axiom theory_relevant thy) + axioms) in trace_msg (fn () => "Total relevant: " ^ Int.toString (length relevant)); relevant @@ -387,11 +374,9 @@ String.isSuffix "_def" a orelse String.isSuffix "_defs" a end; -fun make_clause_table xs = +fun make_fact_table xs = fold (Termtab.update o `(prop_of o snd)) xs Termtab.empty - -fun make_unique xs = - Termtab.fold (cons o snd) (make_clause_table xs) [] +fun make_unique xs = Termtab.fold (cons o snd) (make_fact_table xs) [] (* FIXME: put other record thms here, or declare as "no_atp" *) val multi_base_blacklist = @@ -427,8 +412,7 @@ | apply_depth _ = 0 fun is_formula_too_complex t = - apply_depth t > max_apply_depth orelse Meson.too_many_clauses NONE t orelse - formula_has_too_many_lambdas [] t + apply_depth t > max_apply_depth orelse formula_has_too_many_lambdas [] t val exists_sledgehammer_const = exists_Const (fn (s, _) => String.isPrefix sledgehammer_prefix s) @@ -512,12 +496,13 @@ (* ATP invocation methods setup *) (***************************************************************) -(**** Predicates to detect unwanted clauses (prolific or likely to cause +(**** Predicates to detect unwanted facts (prolific or likely to cause unsoundness) ****) (** Too general means, positive equality literal with a variable X as one operand, when X does not occur properly in the other operand. This rules out clearly - inconsistent clauses such as V=a|V=b, though it by no means guarantees soundness. **) + inconsistent facts such as V = a | V = b, though it by no means guarantees + soundness. **) fun var_occurs_in_term ix = let @@ -532,6 +517,7 @@ (*Unwanted equalities include (1) those between a variable that does not properly occur in the second operand, (2) those between a variable and a record, since these seem to be prolific "cases" thms + (* FIXME: still a problem? *) *) fun too_general_eqterms (Var (ix,T), t) = not (var_occurs_in_term ix t) orelse is_record_type T @@ -544,14 +530,14 @@ fun has_typed_var tycons = exists_subterm (fn Var (_, Type (a, _)) => member (op =) tycons a | _ => false); -(* Clauses are forbidden to contain variables of these types. The typical reason +(* Facts are forbidden to contain variables of these types. The typical reason is that they lead to unsoundness. Note that "unit" satisfies numerous - equations like "?x = ()". The resulting clause will have no type constraint, + equations like "?x = ()". The resulting clauses will have no type constraint, yielding false proofs. Even "bool" leads to many unsound proofs, though only for higher-order problems. *) val dangerous_types = [@{type_name unit}, @{type_name bool}]; -(* Clauses containing variables of type "unit" or "bool" or of the form +(* Facts containing variables of type "unit" or "bool" or of the form "?x = A | ?x = B | ?x = C" are likely to lead to unsound proofs if types are omitted. *) fun is_dangerous_term _ @{prop True} = true diff -r e2aac207d13b -r cc44e887246c src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Thu Jul 29 14:42:09 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Thu Jul 29 14:53:55 2010 +0200 @@ -67,10 +67,10 @@ fun mk_aconn c (phi1, phi2) = AConn (c, [phi1, phi2]) fun index_in_shape x = find_index (exists (curry (op =) x)) -fun is_axiom_clause_number thm_names num = +fun is_axiom_number thm_names num = num > 0 andalso num <= Vector.length thm_names andalso Vector.sub (thm_names, num - 1) <> "" -fun is_conjecture_clause_number conjecture_shape num = +fun is_conjecture_number conjecture_shape num = index_in_shape num conjecture_shape >= 0 fun negate_term (Const (@{const_name All}, T) $ Abs (s, T', t')) = @@ -281,7 +281,7 @@ (SOME b, [T]) => (pos, b, T) | _ => raise FO_TERM [u] -(** Accumulate type constraints in a clause: negative type literals **) +(** Accumulate type constraints in a formula: negative type literals **) fun add_var (key, z) = Vartab.map_default (key, []) (cons z) fun add_type_constraint (false, cl, TFree (a ,_)) = add_var ((a, ~1), cl) | add_type_constraint (false, cl, TVar (ix, _)) = add_var (ix, cl) @@ -407,8 +407,8 @@ | frees as (_, free_T) :: _ => Abs (free_s, free_T, fold (curry abstract_over) (map Free frees) body_t) -(* Interpret a list of syntax trees as a clause, extracting sort constraints - as they appear in the formula. *) +(* Interpret an ATP formula as a HOL term, extracting sort constraints as they + appear in the formula. *) fun prop_from_formula thy full_types tfrees phi = let fun do_formula pos phi = @@ -484,13 +484,13 @@ | replace_deps_in_line p (Inference (num, t, deps)) = Inference (num, t, fold (union (op =) o replace_one_dep p) deps []) -(*Discard axioms; consolidate adjacent lines that prove the same clause, since they differ - only in type information.*) +(* Discard axioms; consolidate adjacent lines that prove the same formula, since + they differ only in type information.*) fun add_line _ _ (line as Definition _) lines = line :: lines | add_line conjecture_shape thm_names (Inference (num, t, [])) lines = - (* No dependencies: axiom, conjecture clause, or internal axioms or - definitions (Vampire). *) - if is_axiom_clause_number thm_names num then + (* No dependencies: axiom, conjecture, or (for Vampire) internal axioms or + definitions. *) + if is_axiom_number thm_names num then (* Axioms are not proof lines. *) if is_only_type_information t then map (replace_deps_in_line (num, [])) lines @@ -499,7 +499,7 @@ (_, []) => lines (*no repetition of proof line*) | (pre, Inference (num', _, _) :: post) => pre @ map (replace_deps_in_line (num', [num])) post - else if is_conjecture_clause_number conjecture_shape num then + else if is_conjecture_number conjecture_shape num then Inference (num, t, []) :: lines else map (replace_deps_in_line (num, [])) lines @@ -539,8 +539,8 @@ | add_desired_line isar_shrink_factor conjecture_shape thm_names frees (Inference (num, t, deps)) (j, lines) = (j + 1, - if is_axiom_clause_number thm_names num orelse - is_conjecture_clause_number conjecture_shape num orelse + if is_axiom_number thm_names num orelse + is_conjecture_number conjecture_shape num orelse (not (is_only_type_information t) andalso null (Term.add_tvars t []) andalso not (exists_subterm (is_bad_free frees) t) andalso @@ -562,10 +562,8 @@ let fun axiom_name num = let val j = Int.fromString num |> the_default ~1 in - if is_axiom_clause_number thm_names j then - SOME (Vector.sub (thm_names, j - 1)) - else - NONE + if is_axiom_number thm_names j then SOME (Vector.sub (thm_names, j - 1)) + else NONE end val tokens_of = String.tokens (fn c => not (Char.isAlphaNum c) andalso c <> #"_") @@ -655,7 +653,7 @@ | smart_case_split proofs facts = CaseSplit (proofs, facts) fun add_fact_from_dep thm_names num = - if is_axiom_clause_number thm_names num then + if is_axiom_number thm_names num then apsnd (insert (op =) (Vector.sub (thm_names, num - 1))) else apfst (insert (op =) (raw_prefix, num))