--- a/src/HOL/TPTP/atp_theory_export.ML Thu Feb 09 09:36:30 2012 +0100
+++ b/src/HOL/TPTP/atp_theory_export.ML Thu Feb 09 12:57:59 2012 +0100
@@ -117,7 +117,8 @@
val prob_file = File.tmp_path (Path.explode "prob.tptp")
val {exec, arguments, proof_delims, known_failures, ...} =
get_atp thy (case format of DFG _ => spassN | _ => eN)
- val _ = problem |> lines_for_atp_problem format |> File.write_list prob_file
+ val _ = problem |> lines_for_atp_problem format (K [])
+ |> File.write_list prob_file
val command =
File.shell_path (Path.explode (getenv (fst exec) ^ "/" ^ snd exec)) ^
" " ^ arguments ctxt false "" (seconds 1.0) (K []) ^ " " ^
@@ -212,7 +213,7 @@
atp_problem
|> (case format of DFG _ => I | _ => add_inferences_to_problem infers)
|> order_problem_facts name_ord
- val ss = lines_for_atp_problem format atp_problem
+ val ss = lines_for_atp_problem format (K []) atp_problem
val _ = app (File.append path) ss
in () end
--- a/src/HOL/Tools/ATP/atp_problem.ML Thu Feb 09 09:36:30 2012 +0100
+++ b/src/HOL/Tools/ATP/atp_problem.ML Thu Feb 09 12:57:59 2012 +0100
@@ -76,6 +76,8 @@
val tptp_empty_list : string
val isabelle_info_prefix : string
val isabelle_info : atp_format -> string -> int -> (string, 'a) ho_term list
+ val extract_isabelle_status : (string, 'a) ho_term list -> string option
+ val extract_isabelle_rank : (string, 'a) ho_term list -> int
val introN : string
val elimN : string
val simpN : string
@@ -83,6 +85,7 @@
val rankN : string
val minimum_rank : int
val default_rank : int
+ val default_kbo_weight : int
val is_tptp_equal : string -> bool
val is_built_in_tptp_symbol : string -> bool
val is_tptp_variable : string -> bool
@@ -104,9 +107,12 @@
bool option -> (bool option -> 'c -> 'd -> 'd) -> ('a, 'b, 'c) formula
-> 'd -> 'd
val formula_map : ('c -> 'd) -> ('a, 'b, 'c) formula -> ('a, 'b, 'd) formula
+ val is_function_type : string ho_type -> bool
+ val is_predicate_type : string ho_type -> bool
val is_format_higher_order : atp_format -> bool
val is_format_typed : atp_format -> bool
- val lines_for_atp_problem : atp_format -> string problem -> string list
+ val lines_for_atp_problem :
+ atp_format -> (unit -> (string * int) list) -> string problem -> string list
val ensure_cnf_problem :
(string * string) problem -> (string * string) problem
val filter_cnf_ueq_problem :
@@ -205,6 +211,7 @@
val minimum_rank = 0
val default_rank = 1000
+val default_kbo_weight = 1
(* Currently, only newer versions of SPASS, with sorted DFG format support, can
process Isabelle metainformation. *)
@@ -273,6 +280,16 @@
| formula_map f (AConn (c, phis)) = AConn (c, map (formula_map f) phis)
| formula_map f (AAtom tm) = AAtom (f tm)
+fun is_function_type (AFun (_, ty)) = is_function_type ty
+ | is_function_type (AType (s, _)) =
+ s <> tptp_type_of_types andalso s <> tptp_bool_type
+ | is_function_type _ = false
+fun is_predicate_type (AFun (_, ty)) = is_predicate_type ty
+ | is_predicate_type (AType (s, _)) = (s = tptp_bool_type)
+ | is_predicate_type _ = false
+fun is_nontrivial_predicate_type (AFun (_, ty)) = is_predicate_type ty
+ | is_nontrivial_predicate_type _ = false
+
fun is_format_higher_order (THF _) = true
| is_format_higher_order _ = false
fun is_format_typed (TFF _) = true
@@ -443,17 +460,6 @@
fun binder_atypes (AFun (ty1, ty2)) = ty1 :: binder_atypes ty2
| binder_atypes _ = []
-fun is_function_type (AFun (_, ty)) = is_function_type ty
- | is_function_type (AType (s, _)) =
- s <> tptp_type_of_types andalso s <> tptp_bool_type
- | is_function_type _ = false
-
-fun is_predicate_type (AFun (_, ty)) = is_predicate_type ty
- | is_predicate_type (AType (s, _)) = (s = tptp_bool_type)
- | is_predicate_type _ = false
-fun is_nontrivial_predicate_type (AFun (_, ty)) = is_predicate_type ty
- | is_nontrivial_predicate_type _ = false
-
fun dfg_string_for_formula flavor info =
let
fun suffix_tag top_level s =
@@ -490,12 +496,12 @@
| str_for_formula top_level (AAtom tm) = str_for_term top_level tm
in str_for_formula true end
-fun dfg_lines flavor problem =
+fun dfg_lines flavor kbo_weights problem =
let
val sorted = (flavor = DFG_Sorted)
val format = DFG flavor
- fun ary sym ty =
- "(" ^ sym ^ ", " ^ string_of_int (arity_of_type ty) ^ ")"
+ fun spair (sym, k) = "(" ^ sym ^ ", " ^ string_of_int k ^ ")"
+ fun ary sym = curry spair sym o arity_of_type
fun fun_typ sym ty =
"function(" ^ sym ^ ", " ^ string_for_type format ty ^ ")."
fun pred_typ sym ty =
@@ -527,7 +533,11 @@
if s = tptp_type_of_types then SOME sym else NONE
| _ => NONE) @ [[dfg_individual_type]]
|> flat |> commas |> enclose "sorts [" "]."
- val syms = [func_aries, pred_aries] @ (if sorted then [sorts ()] else [])
+ fun do_kbo_weights () =
+ kbo_weights () |> map spair |> commas |> enclose "weights [" "]."
+ val syms =
+ [func_aries] @ (if sorted then [do_kbo_weights ()] else []) @
+ [pred_aries] @ (if sorted then [sorts ()] else [])
fun func_sigs () =
filt (fn Decl (_, sym, ty) =>
if is_function_type ty then SOME (fun_typ sym ty) else NONE
@@ -560,11 +570,11 @@
["end_problem.\n"]
end
-fun lines_for_atp_problem format problem =
+fun lines_for_atp_problem format kbo_weights problem =
"% This file was generated by Isabelle (most likely Sledgehammer)\n\
\% " ^ timestamp () ^ "\n" ::
(case format of
- DFG flavor => dfg_lines flavor
+ DFG flavor => dfg_lines flavor kbo_weights
| _ => tptp_lines format) problem
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML Thu Feb 09 09:36:30 2012 +0100
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Thu Feb 09 12:57:59 2012 +0100
@@ -107,7 +107,8 @@
-> ((string * stature) * term) list
-> string problem * string Symtab.table * (string * stature) list vector
* (string * term) list * int Symtab.table
- val atp_problem_weights : string problem -> (string * real) list
+ val atp_problem_relevance_weights : string problem -> (string * real) list
+ val atp_problem_kbo_weights : string problem -> (string * int) list
end;
structure ATP_Problem_Generate : ATP_PROBLEM_GENERATE =
@@ -2665,42 +2666,80 @@
val fact_max_weight = 1.0
val type_info_default_weight = 0.8
-fun add_term_weights weight (ATerm (s, tms)) =
- is_tptp_user_symbol s ? Symtab.default (s, weight)
- #> fold (add_term_weights weight) tms
- | add_term_weights weight (AAbs (_, tm)) = add_term_weights weight tm
-fun add_problem_line_weights weight (Formula (_, _, phi, _, _)) =
- formula_fold NONE (K (add_term_weights weight)) phi
- | add_problem_line_weights _ _ = I
-
-fun add_conjectures_weights [] = I
- | add_conjectures_weights conjs =
- let val (hyps, conj) = split_last conjs in
- add_problem_line_weights conj_weight conj
- #> fold (add_problem_line_weights hyp_weight) hyps
- end
-
-fun add_facts_weights facts =
+(* Weights are from 0.0 (most important) to 1.0 (least important). *)
+fun atp_problem_relevance_weights problem =
let
- val num_facts = length facts
- fun weight_of j =
- fact_min_weight + (fact_max_weight - fact_min_weight) * Real.fromInt j
- / Real.fromInt num_facts
+ fun add_term_weights weight (ATerm (s, tms)) =
+ is_tptp_user_symbol s ? Symtab.default (s, weight)
+ #> fold (add_term_weights weight) tms
+ | add_term_weights weight (AAbs (_, tm)) = add_term_weights weight tm
+ fun add_line_weights weight (Formula (_, _, phi, _, _)) =
+ formula_fold NONE (K (add_term_weights weight)) phi
+ | add_line_weights _ _ = I
+ fun add_conjectures_weights [] = I
+ | add_conjectures_weights conjs =
+ let val (hyps, conj) = split_last conjs in
+ add_line_weights conj_weight conj
+ #> fold (add_line_weights hyp_weight) hyps
+ end
+ fun add_facts_weights facts =
+ let
+ val num_facts = length facts
+ fun weight_of j =
+ fact_min_weight + (fact_max_weight - fact_min_weight) * Real.fromInt j
+ / Real.fromInt num_facts
+ in
+ map weight_of (0 upto num_facts - 1) ~~ facts
+ |> fold (uncurry add_line_weights)
+ end
+ val get = these o AList.lookup (op =) problem
in
- map weight_of (0 upto num_facts - 1) ~~ facts
- |> fold (uncurry add_problem_line_weights)
- end
-
-(* Weights are from 0.0 (most important) to 1.0 (least important). *)
-fun atp_problem_weights problem =
- let val get = these o AList.lookup (op =) problem in
Symtab.empty
|> add_conjectures_weights (get free_typesN @ get conjsN)
|> add_facts_weights (get factsN)
- |> fold (fold (add_problem_line_weights type_info_default_weight) o get)
+ |> fold (fold (add_line_weights type_info_default_weight) o get)
[explicit_declsN, class_relsN, aritiesN]
|> Symtab.dest
|> sort (prod_ord Real.compare string_ord o pairself swap)
end
+val use_topo_for_kbo = false (* experimental *)
+val default_kbo_weight = 1
+
+fun atp_problem_kbo_weights problem =
+ let
+ fun add_term_deps head (ATerm (s, args)) =
+ is_tptp_user_symbol s ? perhaps (try (Graph.add_edge_acyclic (s, head)))
+ #> fold (add_term_deps head) args
+ | add_term_deps head (AAbs (_, tm)) = add_term_deps head tm
+ fun add_eq_deps (ATerm (s, [ATerm (head, args as _ :: _), rhs])) =
+ is_tptp_equal s ? fold (add_term_deps head) (rhs :: args)
+ | add_eq_deps _ = I
+ fun add_line_deps _ (Decl (_, s, ty)) =
+ is_function_type ty ? Graph.default_node (s, ())
+ | add_line_deps status (Formula (_, _, phi, _, info)) =
+ if extract_isabelle_status info = SOME status then
+ formula_fold NONE (K add_eq_deps) phi
+ else
+ I
+ val graph =
+ Graph.empty |> fold (fold (add_line_deps spec_eqN) o snd) problem
+ |> fold (fold (add_line_deps simpN) o snd) problem
+ fun next_weight w = w + w
+ fun add_weights _ [] = I
+ | add_weights weight syms =
+ fold (AList.update (op =) o rpair weight) syms
+ #> add_weights (next_weight weight)
+ (fold (union (op =) o Graph.immediate_succs graph) syms [])
+ in
+ if use_topo_for_kbo then
+ let val topo = graph |> Graph.topological_order in
+ topo ~~ (1 upto length topo)
+ end
+ else
+ [] |> add_weights 1 (Graph.minimals graph)
+ |> sort (int_ord o pairself snd)
+ end
+ |> filter_out (fn (_, weight) => weight = default_kbo_weight)
+
end;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Thu Feb 09 09:36:30 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Thu Feb 09 12:57:59 2012 +0100
@@ -709,17 +709,19 @@
|> prepare_atp_problem ctxt format conj_sym_kind prem_kind
type_enc false lam_trans uncurried_aliases
readable_names true hyp_ts concl_t
- fun weights () = atp_problem_weights atp_problem
+ fun rel_weights () = atp_problem_relevance_weights atp_problem
+ fun kbo_weights () = atp_problem_kbo_weights atp_problem
val full_proof = debug orelse isar_proof
val command =
File.shell_path command ^ " " ^
- arguments ctxt full_proof extra slice_timeout weights ^ " " ^
- File.shell_path prob_file
+ arguments ctxt full_proof extra slice_timeout rel_weights ^
+ " " ^ File.shell_path prob_file
|> enclose "TIMEFORMAT='%3R'; { time " " ; } 2>&1"
val _ =
- atp_problem |> lines_for_atp_problem format
- |> cons ("% " ^ command ^ "\n")
- |> File.write_list prob_file
+ atp_problem
+ |> lines_for_atp_problem format kbo_weights
+ |> cons ("% " ^ command ^ "\n")
+ |> File.write_list prob_file
val ((output, run_time), (atp_proof, outcome)) =
TimeLimit.timeLimit generous_slice_timeout
Isabelle_System.bash_output command