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.
--- 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,
--- 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 =
--- 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;
--- 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