# HG changeset patch # User blanchet # Date 1269858111 -7200 # Node ID ab3dfdeb9603708eb182248cec769520dc48da7d # Parent 8256d5a185bd7735155e0a7db41e3fda942ca45c made "theory_const" a Sledgehammer option; by default, it's true for SPASS and false for the others. This eliminates the need for the "spass_no_tc" ATP, which can be obtained by passing "no_theory_const" instead. diff -r 8256d5a185bd -r ab3dfdeb9603 src/HOL/Tools/ATP_Manager/atp_manager.ML --- a/src/HOL/Tools/ATP_Manager/atp_manager.ML Mon Mar 29 12:01:00 2010 +0200 +++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML Mon Mar 29 12:21:51 2010 +0200 @@ -17,6 +17,7 @@ respect_no_atp: bool, relevance_threshold: real, convergence: real, + theory_const: bool option, higher_order: bool option, follow_defs: bool, isar_proof: bool, @@ -57,7 +58,6 @@ (** parameters, problems, results, and provers **) -(* TODO: "theory_const" *) type params = {debug: bool, verbose: bool, @@ -66,6 +66,7 @@ respect_no_atp: bool, relevance_threshold: real, convergence: real, + theory_const: bool option, higher_order: bool option, follow_defs: bool, isar_proof: bool, diff -r 8256d5a185bd -r ab3dfdeb9603 src/HOL/Tools/ATP_Manager/atp_wrapper.ML --- a/src/HOL/Tools/ATP_Manager/atp_wrapper.ML Mon Mar 29 12:01:00 2010 +0200 +++ b/src/HOL/Tools/ATP_Manager/atp_wrapper.ML Mon Mar 29 12:21:51 2010 +0200 @@ -47,7 +47,7 @@ arguments: Time.time -> string, failure_strs: string list, max_new_clauses: int, - add_theory_const: bool, + prefers_theory_const: bool, supports_isar_proofs: bool}; @@ -158,13 +158,14 @@ fun generic_tptp_prover (name, {command, arguments, failure_strs, max_new_clauses, - add_theory_const, supports_isar_proofs}) + prefers_theory_const, supports_isar_proofs}) (params as {respect_no_atp, relevance_threshold, convergence, - higher_order, follow_defs, isar_proof, ...}) timeout = + theory_const, higher_order, follow_defs, isar_proof, ...}) + timeout = generic_prover (get_relevant_facts respect_no_atp relevance_threshold convergence higher_order follow_defs max_new_clauses - add_theory_const) + (the_default prefers_theory_const theory_const)) (prepare_clauses higher_order false) write_tptp_file command (arguments timeout) failure_strs (if supports_isar_proofs andalso isar_proof then structured_isar_proof @@ -186,7 +187,7 @@ failure_strs = ["Satisfiability detected", "Refutation not found", "CANNOT PROVE"], max_new_clauses = 60, - add_theory_const = false, + prefers_theory_const = false, supports_isar_proofs = true} val vampire = tptp_prover "vampire" vampire_config @@ -203,7 +204,7 @@ "SZS status: ResourceOut", "SZS status ResourceOut", "# Cannot determine problem status"], max_new_clauses = 100, - add_theory_const = false, + prefers_theory_const = false, supports_isar_proofs = true} val e = tptp_prover "e" e_config @@ -212,19 +213,20 @@ fun generic_dfg_prover (name, ({command, arguments, failure_strs, max_new_clauses, - add_theory_const, ...} : prover_config)) + prefers_theory_const, ...} : prover_config)) (params as {respect_no_atp, relevance_threshold, convergence, - higher_order, follow_defs, isar_proof, ...}) timeout = + theory_const, higher_order, follow_defs, isar_proof, ...}) + timeout = generic_prover (get_relevant_facts respect_no_atp relevance_threshold convergence higher_order follow_defs max_new_clauses - add_theory_const) + (the_default prefers_theory_const theory_const)) (prepare_clauses higher_order true) write_dfg_file command (arguments timeout) failure_strs (metis_lemma_list true) name params; fun dfg_prover (name, p) = (name, generic_dfg_prover (name, p)); -fun spass_config_for add_theory_const : prover_config = +val spass_config : prover_config = {command = Path.explode "$SPASS_HOME/SPASS", arguments = (fn timeout => "-Auto -SOS=1 -PGiven=0 -PProblem=0 -Splits=0" ^ " -FullRed=0 -DocProof -TimeLimit=" ^ @@ -233,15 +235,10 @@ ["SPASS beiseite: Completion found.", "SPASS beiseite: Ran out of time.", "SPASS beiseite: Maximal number of loops exceeded."], max_new_clauses = 40, - add_theory_const = add_theory_const, - supports_isar_proofs = false}; - -val spass_config = spass_config_for true + prefers_theory_const = true, + supports_isar_proofs = false} val spass = dfg_prover ("spass", spass_config) -val spass_no_tc_config = spass_config_for false -val spass_no_tc = dfg_prover ("spass_no_tc", spass_no_tc_config) - (* remote prover invocation via SystemOnTPTP *) @@ -271,34 +268,29 @@ val remote_failure_strs = ["Remote-script could not extract proof"]; -fun remote_prover_config prover_prefix args max_new_clauses add_theory_const - : prover_config = +fun remote_prover_config prover_prefix args + ({failure_strs, max_new_clauses, prefers_theory_const, ...} + : prover_config) : prover_config = {command = Path.explode "$ISABELLE_ATP_MANAGER/SystemOnTPTP", arguments = (fn timeout => args ^ " -t " ^ string_of_int (Time.toSeconds timeout) ^ " -s " ^ the_system prover_prefix), - failure_strs = remote_failure_strs, + failure_strs = remote_failure_strs @ failure_strs, max_new_clauses = max_new_clauses, - add_theory_const = add_theory_const, + prefers_theory_const = prefers_theory_const, supports_isar_proofs = false} val remote_vampire = tptp_prover "remote_vampire" - (remote_prover_config "Vampire---9" "" - (#max_new_clauses vampire_config) (#add_theory_const vampire_config)) + (remote_prover_config "Vampire---9" "" vampire_config) val remote_e = - tptp_prover "remote_e" - (remote_prover_config "EP---" "" - (#max_new_clauses e_config) (#add_theory_const e_config)) + tptp_prover "remote_e" (remote_prover_config "EP---" "" e_config) val remote_spass = - tptp_prover "remote_spass" - (remote_prover_config "SPASS---" "-x" - (#max_new_clauses spass_config) (#add_theory_const spass_config)) + tptp_prover "remote_spass" (remote_prover_config "SPASS---" "-x" spass_config) -val provers = - [spass, vampire, e, spass_no_tc, remote_vampire, remote_spass, remote_e] +val provers = [spass, vampire, e, remote_vampire, remote_spass, remote_e] val prover_setup = fold add_prover provers val setup = diff -r 8256d5a185bd -r ab3dfdeb9603 src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Mon Mar 29 12:01:00 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Mon Mar 29 12:21:51 2010 +0200 @@ -127,8 +127,8 @@ (*Inserts a dummy "constant" referring to the theory name, so that relevance takes the given theory into account.*) -fun const_prop_of add_theory_const th = - if add_theory_const then +fun const_prop_of theory_const th = + if theory_const then let val name = Context.theory_name (theory_of_thm th) val t = Const (name ^ ". 1", HOLogic.boolT) in t $ prop_of th end @@ -157,7 +157,7 @@ structure CTtab = Table(type key = const_typ list val ord = dict_ord const_typ_ord); -fun count_axiom_consts add_theory_const thy ((thm,_), tab) = +fun count_axiom_consts theory_const thy ((thm,_), tab) = let fun count_const (a, T, tab) = let val (c, cts) = const_with_typ thy (a,T) in (*Two-dimensional table update. Constant maps to types maps to count.*) @@ -170,7 +170,7 @@ count_term_consts (t, count_term_consts (u, tab)) | count_term_consts (Abs(_,_,t), tab) = count_term_consts (t, tab) | count_term_consts (_, tab) = tab - in count_term_consts (const_prop_of add_theory_const thm, tab) end; + in count_term_consts (const_prop_of theory_const thm, tab) end; (**** Actual Filtering Code ****) @@ -202,8 +202,8 @@ let val tab = add_term_consts_typs_rm thy (t, null_const_tab) in Symtab.fold add_expand_pairs tab [] end; -fun pair_consts_typs_axiom add_theory_const thy (p as (thm, _)) = - (p, (consts_typs_of_term thy (const_prop_of add_theory_const thm))); +fun pair_consts_typs_axiom theory_const thy (p as (thm, _)) = + (p, (consts_typs_of_term thy (const_prop_of theory_const thm))); exception ConstFree; fun dest_ConstFree (Const aT) = aT @@ -289,10 +289,10 @@ end; fun relevance_filter ctxt relevance_threshold convergence follow_defs max_new - add_theory_const relevance_override thy axioms goals = + theory_const relevance_override thy axioms goals = if relevance_threshold > 0.0 then let - val const_tab = List.foldl (count_axiom_consts add_theory_const thy) + val const_tab = List.foldl (count_axiom_consts theory_const thy) Symtab.empty axioms val goal_const_tab = get_goal_consts_typs thy goals val _ = @@ -301,8 +301,7 @@ val relevant = relevant_clauses ctxt convergence follow_defs max_new relevance_override thy const_tab relevance_threshold goal_const_tab - (map (pair_consts_typs_axiom add_theory_const thy) - axioms) + (map (pair_consts_typs_axiom theory_const thy) axioms) in trace_msg (fn () => "Total relevant: " ^ Int.toString (length relevant)); relevant @@ -540,7 +539,7 @@ | SOME b => not b fun get_relevant_facts respect_no_atp relevance_threshold convergence - higher_order follow_defs max_new add_theory_const + higher_order follow_defs max_new theory_const relevance_override (ctxt, (chain_ths, th)) goal_cls = let val thy = ProofContext.theory_of ctxt @@ -551,7 +550,7 @@ |> remove_unwanted_clauses in relevance_filter ctxt relevance_threshold convergence follow_defs max_new - add_theory_const relevance_override thy included_cls + theory_const relevance_override thy included_cls (map prop_of goal_cls) end; diff -r 8256d5a185bd -r ab3dfdeb9603 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Mon Mar 29 12:01:00 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Mon Mar 29 12:21:51 2010 +0200 @@ -43,6 +43,7 @@ ("respect_no_atp", "true"), ("relevance_threshold", "50"), ("convergence", "320"), + ("theory_const", "smart"), ("higher_order", "smart"), ("follow_defs", "false"), ("isar_proof", "false"), @@ -53,6 +54,7 @@ ("quiet", "verbose"), ("ignore_no_atp", "respect_no_atp"), ("partial_types", "full_types"), + ("no_theory_const", "theory_const"), ("first_order", "higher_order"), ("dont_follow_defs", "follow_defs"), ("metis_proof", "isar_proof")] @@ -124,6 +126,7 @@ val relevance_threshold = 0.01 * Real.fromInt (lookup_int "relevance_threshold") val convergence = 0.01 * Real.fromInt (lookup_int "convergence") + val theory_const = lookup_bool_option "theory_const" val higher_order = lookup_bool_option "higher_order" val follow_defs = lookup_bool "follow_defs" val isar_proof = lookup_bool "isar_proof" @@ -132,8 +135,9 @@ in {debug = debug, verbose = verbose, atps = atps, full_types = full_types, respect_no_atp = respect_no_atp, relevance_threshold = relevance_threshold, - convergence = convergence, higher_order = higher_order, - follow_defs = follow_defs, isar_proof = isar_proof, timeout = timeout, + convergence = convergence, theory_const = theory_const, + higher_order = higher_order, follow_defs = follow_defs, + isar_proof = isar_proof, timeout = timeout, minimize_timeout = minimize_timeout} end