# HG changeset patch # User blanchet # Date 1328792657 -3600 # Node ID c862760145716e13387782d29979849f57fe42b1 # Parent 1e07620d724c057ca01e89ee5100f349711f6fcb improved KBO weights -- beware of explicit applications diff -r 1e07620d724c -r c86276014571 src/HOL/Tools/ATP/atp_problem.ML --- a/src/HOL/Tools/ATP/atp_problem.ML Thu Feb 09 12:57:59 2012 +0100 +++ b/src/HOL/Tools/ATP/atp_problem.ML Thu Feb 09 14:04:17 2012 +0100 @@ -754,7 +754,8 @@ fun avoid_clash_with_dfg_keywords s = let val n = String.size s in - if n < 2 orelse String.isSubstring "_" s then + if n < 2 orelse (n = 2 andalso String.sub (s, 0) = String.sub (s, 1)) orelse + String.isSubstring "_" s then s else String.substring (s, 0, n - 1) ^ diff -r 1e07620d724c -r c86276014571 src/HOL/Tools/ATP/atp_problem_generate.ML --- a/src/HOL/Tools/ATP/atp_problem_generate.ML Thu Feb 09 12:57:59 2012 +0100 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Thu Feb 09 14:04:17 2012 +0100 @@ -2706,14 +2706,27 @@ val use_topo_for_kbo = false (* experimental *) val default_kbo_weight = 1 +fun have_head_rolling (ATerm (s, args)) = + (* ugly hack: may make innocent victims *) + if String.isPrefix app_op_name s andalso length args = 2 then + have_head_rolling (hd args) ||> append (tl args) + else + (s, args) + | have_head_rolling _ = ("", []) + 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) + fun add_eq_deps (ATerm (s, [lhs as _, rhs])) = + if is_tptp_equal s then + let val (head, rest) = have_head_rolling lhs in + fold (add_term_deps head) (rhs :: rest) + end + else + I | add_eq_deps _ = I fun add_line_deps _ (Decl (_, s, ty)) = is_function_type ty ? Graph.default_node (s, ())