# HG changeset patch # User blanchet # Date 1271772276 -7200 # Node ID 61159615a0c5351d2611cbd2df0d48a4161d2498 # Parent 77abfa526524a0b903a20d42f08df46d63287e98 added "explicit_apply" option to Sledgehammer, to control whether an explicit apply function should be used as much or as little as possible (replaces a previous global variable) diff -r 77abfa526524 -r 61159615a0c5 src/HOL/Tools/ATP_Manager/atp_manager.ML --- a/src/HOL/Tools/ATP_Manager/atp_manager.ML Tue Apr 20 14:39:42 2010 +0200 +++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML Tue Apr 20 16:04:36 2010 +0200 @@ -15,6 +15,7 @@ overlord: bool, atps: string list, full_types: bool, + explicit_apply: bool, respect_no_atp: bool, relevance_threshold: real, convergence: real, @@ -69,6 +70,7 @@ overlord: bool, atps: string list, full_types: bool, + explicit_apply: bool, respect_no_atp: bool, relevance_threshold: real, convergence: real, diff -r 77abfa526524 -r 61159615a0c5 src/HOL/Tools/ATP_Manager/atp_wrapper.ML --- a/src/HOL/Tools/ATP_Manager/atp_wrapper.ML Tue Apr 20 14:39:42 2010 +0200 +++ b/src/HOL/Tools/ATP_Manager/atp_wrapper.ML Tue Apr 20 16:04:36 2010 +0200 @@ -67,7 +67,7 @@ | (failure :: _) => SOME failure fun generic_prover overlord get_facts prepare write_file cmd args failure_strs - proof_text name ({debug, full_types, ...} : params) + proof_text name ({debug, full_types, explicit_apply, ...} : params) ({subgoal, goal, relevance_override, axiom_clauses, filtered_clauses} : problem) = let @@ -128,7 +128,7 @@ if Config.get ctxt measure_runtime then split_time s else (s, 0) fun run_on probfile = if File.exists cmd then - write_file full_types probfile clauses + write_file full_types explicit_apply probfile clauses |> pair (apfst split_time' (bash_output (cmd_line probfile))) else error ("Bad executable: " ^ Path.implode cmd ^ "."); diff -r 77abfa526524 -r 61159615a0c5 src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML Tue Apr 20 14:39:42 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML Tue Apr 20 16:04:36 2010 +0200 @@ -34,10 +34,10 @@ val get_helper_clauses : bool -> theory -> bool -> hol_clause list * (thm * (axiom_name * hol_clause_id)) list * string list -> hol_clause list - val write_tptp_file : bool -> bool -> Path.T -> + val write_tptp_file : bool -> bool -> bool -> Path.T -> hol_clause list * hol_clause list * hol_clause list * hol_clause list * classrel_clause list * arity_clause list -> unit - val write_dfg_file : bool -> Path.T -> + val write_dfg_file : bool -> bool -> Path.T -> hol_clause list * hol_clause list * hol_clause list * hol_clause list * classrel_clause list * arity_clause list -> unit end @@ -50,19 +50,19 @@ open Sledgehammer_Fact_Preprocessor (* Parameter "full_types" below indicates that full type information is to be -exported *) + exported. -(* If true, each function will be directly applied to as many arguments as - possible, avoiding use of the "apply" operator. Use of hBOOL is also - minimized. *) -val minimize_applies = true; + If "explicit_apply" is false, each function will be directly applied to as + many arguments as possible, avoiding use of the "apply" operator. Use of + hBOOL is also minimized. +*) fun min_arity_of const_min_arity c = the_default 0 (Symtab.lookup const_min_arity c); (*True if the constant ever appears outside of the top-level position in literals. If false, the constant always receives all of its arguments and is used as a predicate.*) -fun needs_hBOOL const_needs_hBOOL c = - not minimize_applies orelse +fun needs_hBOOL explicit_apply const_needs_hBOOL c = + explicit_apply orelse the_default false (Symtab.lookup const_needs_hBOOL c); @@ -211,9 +211,10 @@ val type_wrapper = "ti"; -fun head_needs_hBOOL const_needs_hBOOL (CombConst((c, _), _, _)) = - needs_hBOOL const_needs_hBOOL c - | head_needs_hBOOL _ _ = true; +fun head_needs_hBOOL explicit_apply const_needs_hBOOL + (CombConst ((c, _), _, _)) = + needs_hBOOL explicit_apply const_needs_hBOOL c + | head_needs_hBOOL _ _ _ = true fun wrap_type full_types (s, ty) pool = if full_types then @@ -223,8 +224,11 @@ else (s, pool) -fun wrap_type_if full_types cnh (head, s, tp) = - if head_needs_hBOOL cnh head then wrap_type full_types (s, tp) else pair s +fun wrap_type_if full_types explicit_apply cnh (head, s, tp) = + if head_needs_hBOOL explicit_apply cnh head then + wrap_type full_types (s, tp) + else + pair s fun apply ss = "hAPP" ^ paren_pack ss; @@ -252,18 +256,22 @@ | string_of_application _ _ (CombVar (name, _), args) pool = nice_name name pool |>> (fn s => string_apply (s, args)) -fun string_of_combterm (params as (full_types, cma, cnh)) t pool = +fun string_of_combterm (params as (full_types, explicit_apply, cma, cnh)) t + pool = let val (head, args) = strip_combterm_comb t val (ss, pool) = pool_map (string_of_combterm params) args pool val (s, pool) = string_of_application full_types cma (head, ss) pool - in wrap_type_if full_types cnh (head, s, type_of_combterm t) pool end + in + wrap_type_if full_types explicit_apply cnh (head, s, type_of_combterm t) + pool + end (*Boolean-valued terms are here converted to literals.*) fun boolify params c = string_of_combterm params c #>> prefix "hBOOL" o paren_pack o single -fun string_of_predicate (params as (_, _, cnh)) t = +fun string_of_predicate (params as (_, explicit_apply, _, cnh)) t = case t of (CombApp (CombApp (CombConst (("equal", _), _, _), t1), t2)) => (* DFG only: new TPTP prefers infix equality *) @@ -272,7 +280,8 @@ | _ => case #1 (strip_combterm_comb t) of CombConst ((s, _), _, _) => - (if needs_hBOOL cnh s then boolify else string_of_combterm) params t + (if needs_hBOOL explicit_apply cnh s then boolify else string_of_combterm) + params t | _ => boolify params t @@ -342,8 +351,8 @@ fun add_types tvars = fold add_fol_type_funcs tvars -fun add_decls (full_types, cma, cnh) (CombConst ((c, _), _, tvars)) - (funcs, preds) = +fun add_decls (full_types, explicit_apply, cma, cnh) + (CombConst ((c, _), _, tvars)) (funcs, preds) = if c = "equal" then (add_types tvars funcs, preds) else @@ -351,8 +360,10 @@ val ntys = if not full_types then length tvars else 0 val addit = Symtab.update(c, arity+ntys) in - if needs_hBOOL cnh c then (add_types tvars (addit funcs), preds) - else (add_types tvars funcs, addit preds) + if needs_hBOOL explicit_apply cnh c then + (add_types tvars (addit funcs), preds) + else + (add_types tvars funcs, addit preds) end | add_decls _ (CombVar (_, ctp)) (funcs, preds) = (add_fol_type_funcs ctp funcs, preds) @@ -458,18 +469,23 @@ (const_min_arity, const_needs_hBOOL) = fold count_constants_lit literals (const_min_arity, const_needs_hBOOL); -fun display_arity const_needs_hBOOL (c,n) = +fun display_arity explicit_apply const_needs_hBOOL (c,n) = trace_msg (fn () => "Constant: " ^ c ^ " arity:\t" ^ Int.toString n ^ - (if needs_hBOOL const_needs_hBOOL c then " needs hBOOL" else "")); + (if needs_hBOOL explicit_apply const_needs_hBOOL c then + " needs hBOOL" + else + "")) -fun count_constants (conjectures, _, extra_clauses, helper_clauses, _, _) = - if minimize_applies then +fun count_constants explicit_apply + (conjectures, _, extra_clauses, helper_clauses, _, _) = + if not explicit_apply then let val (const_min_arity, const_needs_hBOOL) = fold count_constants_clause conjectures (Symtab.empty, Symtab.empty) |> fold count_constants_clause extra_clauses |> fold count_constants_clause helper_clauses - val _ = List.app (display_arity const_needs_hBOOL) (Symtab.dest (const_min_arity)) + val _ = List.app (display_arity explicit_apply const_needs_hBOOL) + (Symtab.dest (const_min_arity)) in (const_min_arity, const_needs_hBOOL) end else (Symtab.empty, Symtab.empty); @@ -479,15 +495,15 @@ (* TPTP format *) -fun write_tptp_file readable_names full_types file clauses = +fun write_tptp_file readable_names full_types explicit_apply file clauses = let fun section _ [] = [] | section name ss = "\n% " ^ name ^ plural_s (length ss) ^ "\n" :: ss val pool = empty_name_pool readable_names val (conjectures, axclauses, _, helper_clauses, classrel_clauses, arity_clauses) = clauses - val (cma, cnh) = count_constants clauses - val params = (full_types, cma, cnh) + val (cma, cnh) = count_constants explicit_apply clauses + val params = (full_types, explicit_apply, cma, cnh) val ((conjecture_clss, tfree_litss), pool) = pool_map (tptp_clause params) conjectures pool |>> ListPair.unzip val tfree_clss = map tptp_tfree_clause (fold (union (op =)) tfree_litss []) @@ -511,7 +527,7 @@ (* DFG format *) -fun write_dfg_file full_types file clauses = +fun write_dfg_file full_types explicit_apply file clauses = let (* Some of the helper functions below are not name-pool-aware. However, there's no point in adding name pool support if the DFG format is on its @@ -519,8 +535,8 @@ val pool = NONE val (conjectures, axclauses, _, helper_clauses, classrel_clauses, arity_clauses) = clauses - val (cma, cnh) = count_constants clauses - val params = (full_types, cma, cnh) + val (cma, cnh) = count_constants explicit_apply clauses + val params = (full_types, explicit_apply, cma, cnh) val ((conjecture_clss, tfree_litss), pool) = pool_map (dfg_clause params) conjectures pool |>> ListPair.unzip and probname = Path.implode (Path.base file) diff -r 77abfa526524 -r 61159615a0c5 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Tue Apr 20 14:39:42 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Tue Apr 20 16:04:36 2010 +0200 @@ -41,6 +41,7 @@ [("debug", "false"), ("verbose", "false"), ("overlord", "false"), + ("explicit_apply", "false"), ("respect_no_atp", "true"), ("relevance_threshold", "50"), ("convergence", "320"), @@ -58,6 +59,7 @@ [("no_debug", "debug"), ("quiet", "verbose"), ("no_overlord", "overlord"), + ("implicit_apply", "explicit_apply"), ("ignore_no_atp", "respect_no_atp"), ("partial_types", "full_types"), ("theory_irrelevant", "theory_relevant"), @@ -146,6 +148,7 @@ val overlord = lookup_bool "overlord" val atps = lookup_string "atps" |> space_explode " " val full_types = lookup_bool "full_types" + val explicit_apply = lookup_bool "explicit_apply" val respect_no_atp = lookup_bool "respect_no_atp" val relevance_threshold = 0.01 * Real.fromInt (lookup_int "relevance_threshold") @@ -160,11 +163,12 @@ val minimize_timeout = lookup_time "minimize_timeout" in {debug = debug, verbose = verbose, overlord = overlord, atps = atps, - full_types = full_types, respect_no_atp = respect_no_atp, - relevance_threshold = relevance_threshold, convergence = convergence, - theory_relevant = theory_relevant, higher_order = higher_order, - follow_defs = follow_defs, isar_proof = isar_proof, modulus = modulus, - sorts = sorts, timeout = timeout, minimize_timeout = minimize_timeout} + full_types = full_types, explicit_apply = explicit_apply, + respect_no_atp = respect_no_atp, relevance_threshold = relevance_threshold, + convergence = convergence, theory_relevant = theory_relevant, + higher_order = higher_order, follow_defs = follow_defs, + isar_proof = isar_proof, modulus = modulus, sorts = sorts, + timeout = timeout, minimize_timeout = minimize_timeout} end fun get_params thy = extract_params thy (default_raw_params thy)