--- 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
--- 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
--- 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))