# HG changeset patch # User blanchet # Date 1282144145 -7200 # Node ID b03f8fe043ec1a7a3e5440ddf8e9061e220ebbc2 # Parent 6a5b104f92cb0bf703acf715332f4899eaa7dcf0 added "max_relevant_per_iter" option to Sledgehammer diff -r 6a5b104f92cb -r b03f8fe043ec src/HOL/Tools/ATP/atp_systems.ML --- a/src/HOL/Tools/ATP/atp_systems.ML Wed Aug 18 16:42:37 2010 +0200 +++ b/src/HOL/Tools/ATP/atp_systems.ML Wed Aug 18 17:09:05 2010 +0200 @@ -18,8 +18,8 @@ arguments: bool -> Time.time -> string, proof_delims: (string * string) list, known_failures: (failure * string) list, - max_new_relevant_facts_per_iter: int, - prefers_theory_relevant: bool, + default_max_relevant_per_iter: int, + default_theory_relevant: bool, explicit_forall: bool} val string_for_failure : failure -> string @@ -49,8 +49,8 @@ arguments: bool -> Time.time -> string, proof_delims: (string * string) list, known_failures: (failure * string) list, - max_new_relevant_facts_per_iter: int, - prefers_theory_relevant: bool, + default_max_relevant_per_iter: int, + default_theory_relevant: bool, explicit_forall: bool} val missing_message_tail = @@ -144,8 +144,8 @@ "# Cannot determine problem status within resource limit"), (OutOfResources, "SZS status: ResourceOut"), (OutOfResources, "SZS status ResourceOut")], - max_new_relevant_facts_per_iter = 50 (* FIXME *), - prefers_theory_relevant = false, + default_max_relevant_per_iter = 50 (* FIXME *), + default_theory_relevant = false, explicit_forall = false} val e = ("e", e_config) @@ -171,8 +171,8 @@ (MalformedInput, "Undefined symbol"), (MalformedInput, "Free Variable"), (SpassTooOld, "tptp2dfg")], - max_new_relevant_facts_per_iter = 35 (* FIXME *), - prefers_theory_relevant = true, + default_max_relevant_per_iter = 35 (* FIXME *), + default_theory_relevant = true, explicit_forall = true} val spass = ("spass", spass_config) @@ -198,8 +198,8 @@ (Unprovable, "Satisfiability detected"), (OutOfResources, "Refutation not found"), (VampireTooOld, "not a valid option")], - max_new_relevant_facts_per_iter = 45 (* FIXME *), - prefers_theory_relevant = false, + default_max_relevant_per_iter = 45 (* FIXME *), + default_theory_relevant = false, explicit_forall = false} val vampire = ("vampire", vampire_config) @@ -220,9 +220,10 @@ fun refresh_systems_on_tptp () = Synchronized.change systems (fn _ => get_systems ()) -fun get_system prefix = Synchronized.change_result systems (fn systems => - (if null systems then get_systems () else systems) - |> `(find_first (String.isPrefix prefix))); +fun get_system prefix = + Synchronized.change_result systems + (fn systems => (if null systems then get_systems () else systems) + |> `(find_first (String.isPrefix prefix))) fun the_system prefix = (case get_system prefix of @@ -230,8 +231,8 @@ | SOME sys => sys); fun remote_config atp_prefix - ({proof_delims, known_failures, max_new_relevant_facts_per_iter, - prefers_theory_relevant, ...} : prover_config) : prover_config = + ({proof_delims, known_failures, default_max_relevant_per_iter, + default_theory_relevant, ...} : prover_config) : prover_config = {exec = ("ISABELLE_ATP", "scripts/remote_atp"), required_execs = [], arguments = fn _ => fn timeout => @@ -241,8 +242,8 @@ known_failures = known_failures @ known_perl_failures @ [(TimedOut, "says Timeout")], - max_new_relevant_facts_per_iter = max_new_relevant_facts_per_iter, - prefers_theory_relevant = prefers_theory_relevant, + default_max_relevant_per_iter = default_max_relevant_per_iter, + default_theory_relevant = default_theory_relevant, explicit_forall = true} val remote_name = prefix "remote_" diff -r 6a5b104f92cb -r b03f8fe043ec src/HOL/Tools/Sledgehammer/sledgehammer.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Wed Aug 18 16:42:37 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Wed Aug 18 17:09:05 2010 +0200 @@ -20,6 +20,7 @@ explicit_apply: bool, relevance_threshold: real, relevance_convergence: real, + max_relevant_per_iter: int option, theory_relevant: bool option, defs_relevant: bool, isar_proof: bool, @@ -89,6 +90,7 @@ explicit_apply: bool, relevance_threshold: real, relevance_convergence: real, + max_relevant_per_iter: int option, theory_relevant: bool option, defs_relevant: bool, isar_proof: bool, @@ -208,10 +210,11 @@ fun prover_fun atp_name {exec, required_execs, arguments, proof_delims, known_failures, - max_new_relevant_facts_per_iter, prefers_theory_relevant, + default_max_relevant_per_iter, default_theory_relevant, explicit_forall} ({debug, verbose, overlord, full_types, explicit_apply, - relevance_threshold, relevance_convergence, theory_relevant, + relevance_threshold, relevance_convergence, + max_relevant_per_iter, theory_relevant, defs_relevant, isar_proof, isar_shrink_factor, timeout, ...} : params) minimize_command ({subgoal, goal, relevance_override, axioms} : problem) = @@ -231,8 +234,10 @@ (print_d (fn () => "Selecting relevant facts for " ^ quote atp_name ^ "."); relevant_facts full_types relevance_threshold relevance_convergence - defs_relevant max_new_relevant_facts_per_iter - (the_default prefers_theory_relevant theory_relevant) + defs_relevant + (the_default default_max_relevant_per_iter + max_relevant_per_iter) + (the_default default_theory_relevant theory_relevant) relevance_override goal hyp_ts concl_t |> tap ((fn n => print_v (fn () => "Selected " ^ string_of_int n ^ " fact" ^ plural_s n ^ diff -r 6a5b104f92cb -r b03f8fe043ec src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimize.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimize.ML Wed Aug 18 16:42:37 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimize.ML Wed Aug 18 17:09:05 2010 +0200 @@ -43,9 +43,9 @@ end fun test_theorems ({debug, verbose, overlord, atps, full_types, - relevance_threshold, relevance_convergence, theory_relevant, - defs_relevant, isar_proof, isar_shrink_factor, - ...} : params) + relevance_threshold, relevance_convergence, + defs_relevant, isar_proof, isar_shrink_factor, ...} + : params) (prover : prover) explicit_apply timeout subgoal state name_thms_pairs = let @@ -56,9 +56,10 @@ full_types = full_types, explicit_apply = explicit_apply, relevance_threshold = relevance_threshold, relevance_convergence = relevance_convergence, - theory_relevant = theory_relevant, defs_relevant = defs_relevant, - isar_proof = isar_proof, isar_shrink_factor = isar_shrink_factor, - timeout = timeout, minimize_timeout = timeout} + max_relevant_per_iter = NONE, theory_relevant = NONE, + defs_relevant = defs_relevant, isar_proof = isar_proof, + isar_shrink_factor = isar_shrink_factor, timeout = timeout, + minimize_timeout = timeout} val axioms = maps (fn (n, ths) => map (pair n) ths) name_thms_pairs val {context = ctxt, facts, goal} = Proof.goal state val problem = @@ -98,10 +99,8 @@ fun minimize_theorems {atps = [], ...} _ _ _ _ = error "No ATP is set." | minimize_theorems - (params as {debug, verbose, overlord, atps as atp :: _, full_types, - relevance_threshold, relevance_convergence, theory_relevant, - defs_relevant, isar_proof, isar_shrink_factor, - minimize_timeout, ...}) + (params as {debug, atps = atp :: _, full_types, isar_proof, + isar_shrink_factor, minimize_timeout, ...}) i n state name_thms_pairs = let val thy = Proof.theory_of state diff -r 6a5b104f92cb -r b03f8fe043ec src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Aug 18 16:42:37 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Aug 18 17:09:05 2010 +0200 @@ -69,6 +69,7 @@ ("explicit_apply", "false"), ("relevance_threshold", "50"), ("relevance_convergence", "320"), + ("max_relevant_per_iter", "smart"), ("theory_relevant", "smart"), ("defs_relevant", "false"), ("isar_proof", "false"), @@ -158,6 +159,10 @@ SOME n => n | NONE => error ("Parameter " ^ quote name ^ " must be assigned an integer value.") + fun lookup_int_option name = + case lookup name of + SOME "smart" => NONE + | _ => SOME (lookup_int name) val debug = lookup_bool "debug" val verbose = debug orelse lookup_bool "verbose" val overlord = lookup_bool "overlord" @@ -168,6 +173,7 @@ 0.01 * Real.fromInt (lookup_int "relevance_threshold") val relevance_convergence = 0.01 * Real.fromInt (lookup_int "relevance_convergence") + val max_relevant_per_iter = lookup_int_option "max_relevant_per_iter" val theory_relevant = lookup_bool_option "theory_relevant" val defs_relevant = lookup_bool "defs_relevant" val isar_proof = lookup_bool "isar_proof" @@ -179,6 +185,7 @@ full_types = full_types, explicit_apply = explicit_apply, relevance_threshold = relevance_threshold, relevance_convergence = relevance_convergence, + max_relevant_per_iter = max_relevant_per_iter, theory_relevant = theory_relevant, defs_relevant = defs_relevant, isar_proof = isar_proof, isar_shrink_factor = isar_shrink_factor, timeout = timeout, minimize_timeout = minimize_timeout} diff -r 6a5b104f92cb -r b03f8fe043ec src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML Wed Aug 18 16:42:37 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML Wed Aug 18 17:09:05 2010 +0200 @@ -420,8 +420,8 @@ type instantiations). If false, the constant always receives all of its arguments and is used as a predicate. *) fun is_predicate NONE s = - s = "equal" orelse String.isPrefix type_const_prefix s orelse - String.isPrefix class_prefix s + s = "equal" orelse s = "$false" orelse s = "$true" orelse + String.isPrefix type_const_prefix s orelse String.isPrefix class_prefix s | is_predicate (SOME the_const_tab) s = case Symtab.lookup the_const_tab s of SOME {min_arity, max_arity, sub_level} =>