--- a/src/HOL/Tools/ATP/atp_proof.ML Tue Feb 22 21:34:12 2022 +0100
+++ b/src/HOL/Tools/ATP/atp_proof.ML Tue Feb 22 21:34:29 2022 +0100
@@ -563,20 +563,20 @@
(if full then parse_hol_formula || skip_term >> K dummy_phi else skip_term >> K dummy_phi)
-- parse_tstp_extra_arguments --| $$ ")"
--| $$ "."
- >> (fn (((num, role), phi), src) =>
+ >> (fn (((num, role0), phi), src) =>
let
- val role' = role_of_tptp_string role
- val ((name, phi), rule, deps) =
+ val role = role_of_tptp_string role0
+ val (name, phi, role', rule, deps) =
(case src of
SOME (File_Source (_, SOME s)) =>
- if role' = Definition then
- (((num, map fst (find_formula_in_problem phi problem)), phi), "", [])
+ if role = Definition then
+ ((num, map fst (find_formula_in_problem phi problem)), phi, role, "", [])
else
- (((num, [s]), phi), "", [])
- | SOME (Inference_Source (rule, deps)) => (((num, []), phi), rule, deps)
- | SOME (Introduced_Source rule) => (((num, []), phi), rule, [])
- | SOME Define_Source => (((num, []), phi), zipperposition_define_rule, [])
- | _ => (((num, [num]), phi), "", []))
+ ((num, [s]), phi, role, "", [])
+ | SOME (Inference_Source (rule, deps)) => ((num, []), phi, role, rule, deps)
+ | SOME (Introduced_Source rule) => ((num, []), phi, Definition, rule, [])
+ | SOME Define_Source => ((num, []), phi, Definition, zipperposition_define_rule, [])
+ | _ => ((num, [num]), phi, role, "", []))
in
[(name, role', phi, rule, map (rpair []) deps)]
end)
@@ -607,8 +607,8 @@
| SOME (File_Source _) =>
(((num, map fst (find_formula_in_problem phi problem)), phi), role, "", [])
| SOME (Inference_Source (rule, deps)) => (((num, []), phi), role, rule, deps)
- | SOME (Introduced_Source rule) => (((num, []), phi), Lemma, rule, [])
- | SOME Define_Source => (((num, []), phi), Lemma, zipperposition_define_rule, [])
+ | SOME (Introduced_Source rule) => (((num, []), phi), Definition, rule, [])
+ | SOME Define_Source => (((num, []), phi), Definition, zipperposition_define_rule, [])
| _ => (((num, [num]), phi), role, "", []))
fun mk_step () = (name, role', phi, rule, map (rpair []) deps)
--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Tue Feb 22 21:34:12 2022 +0100
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Tue Feb 22 21:34:29 2022 +0100
@@ -782,7 +782,7 @@
else ([], Hypothesis, close_form (nth hyp_ts j))
| _ =>
(case resolve_facts facts (num :: ss) of
- [] => (ss, if role = Lemma then Lemma else Plain, t)
+ [] => (ss, if member (op =) [Definition, Lemma] role then role else Plain, t)
| facts => (map fst facts, Axiom, t)))
in
((num, ss'), role', t', rule, deps)
--- a/src/HOL/Tools/ATP/atp_util.ML Tue Feb 22 21:34:12 2022 +0100
+++ b/src/HOL/Tools/ATP/atp_util.ML Tue Feb 22 21:34:29 2022 +0100
@@ -409,8 +409,9 @@
val long = Thm.get_name_hint th
val short = Long_Name.base_name long
in
- if Thm.eq_thm_prop (th, singleton (Attrib.eval_thms ctxt) (Facts.named short, [])) then short
- else long
+ (case try (singleton (Attrib.eval_thms ctxt)) (Facts.named short, []) of
+ SOME th' => if Thm.eq_thm_prop (th, th') then short else long
+ | _ => long)
end
val map_prod = Ctr_Sugar_Util.map_prod
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Tue Feb 22 21:34:12 2022 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Tue Feb 22 21:34:29 2022 +0100
@@ -59,15 +59,15 @@
val z3_th_lemma_rule_prefix = Z3_Proof.string_of_rule (Z3_Proof.Th_Lemma "")
val zipperposition_cnf_rule = "cnf"
-val skolemize_rules =
+val symbol_introduction_rules =
[e_definition_rule, e_skolemize_rule, leo2_extcnf_forall_neg_rule, satallax_skolemize_rule,
spass_skolemize_rule, vampire_skolemisation_rule, z3_skolemize_rule,
- zipperposition_cnf_rule] @ veriT_skolemize_rules
+ zipperposition_cnf_rule, zipperposition_define_rule] @ veriT_skolemize_rules
fun is_ext_rule rule = (rule = leo2_extcnf_equal_neg_rule)
val is_maybe_ext_rule = is_ext_rule orf String.isPrefix satallax_tab_rule_prefix
-val is_skolemize_rule = member (op =) skolemize_rules
+val is_symbol_introduction_rule = member (op =) symbol_introduction_rules
fun is_arith_rule rule =
String.isPrefix z3_th_lemma_rule_prefix rule orelse rule = veriT_simp_arith_rule orelse
rule = veriT_la_generic_rule
@@ -89,7 +89,8 @@
line :: lines
else if t aconv \<^prop>\<open>True\<close> then
map (replace_dependencies_in_line (name, [])) lines
- else if role = Lemma orelse role = Hypothesis orelse is_arith_rule rule then
+ else if role = Definition orelse role = Lemma orelse role = Hypothesis
+ orelse is_arith_rule rule then
line :: lines
else if role = Axiom then
lines (* axioms (facts) need no proof lines *)
@@ -113,15 +114,16 @@
fun looks_boring () = t aconv \<^prop>\<open>False\<close> orelse length deps < 2
- fun is_skolemizing_line (_, _, _, rule', deps') =
- is_skolemize_rule rule' andalso member (op =) deps' name
+ fun is_symbol_introduction_line (_, _, _, rule', deps') =
+ is_symbol_introduction_rule rule' andalso member (op =) deps' name
- fun is_before_skolemize_rule () = exists is_skolemizing_line lines
+ fun is_before_symbol_introduction_rule () = exists is_symbol_introduction_line lines
in
if is_duplicate orelse
- (role = Plain andalso not (is_skolemize_rule rule) andalso
+ (role = Plain andalso not (is_symbol_introduction_rule rule) andalso
not (is_ext_rule rule) andalso not (is_arith_rule rule) andalso
- not (null lines) andalso looks_boring () andalso not (is_before_skolemize_rule ())) then
+ not (null lines) andalso looks_boring () andalso
+ not (is_before_symbol_introduction_rule ())) then
add_lines_pass2 res (map (replace_dependencies_in_line (name, deps)) lines)
else
add_lines_pass2 (line :: res) lines
@@ -174,7 +176,8 @@
| SOME n => n)
fun is_fixed ctxt = Variable.is_declared ctxt orf Name.is_skolem
- fun skolems_of ctxt t = Term.add_frees t [] |> filter_out (is_fixed ctxt o fst) |> rev
+ fun introduced_symbols_of ctxt t =
+ Term.add_frees t [] |> filter_out (is_fixed ctxt o fst) |> rev
fun get_role keep_role ((num, _), role, t, rule, _) =
if keep_role role then SOME ((raw_label_of_num num, t), rule) else NONE
@@ -201,14 +204,14 @@
fun add_lemma ((label, goal), rule) ctxt =
let
- val (skos, proof_methods) =
- (if is_skolemize_rule rule then (skolems_of ctxt goal, skolem_methods)
+ val (obtains, proof_methods) =
+ (if is_symbol_introduction_rule rule then (introduced_symbols_of ctxt goal, skolem_methods)
else if is_arith_rule rule then ([], arith_methods)
else ([], rewrite_methods))
||> massage_methods
val prove = Prove {
qualifiers = [],
- obtains = skos,
+ obtains = obtains,
label = label,
goal = goal,
subproofs = [],
@@ -216,11 +219,12 @@
proof_methods = proof_methods,
comment = ""}
in
- (prove, ctxt |> not (null skos) ? (Variable.add_fixes (map fst skos) #> snd))
+ (prove, ctxt |> not (null obtains) ? (Variable.add_fixes (map fst obtains) #> snd))
end
val (lems, _) =
- fold_map add_lemma (map_filter (get_role (curry (op =) Lemma)) atp_proof) ctxt
+ fold_map add_lemma (map_filter (get_role (member (op =) [Definition, Lemma]))
+ atp_proof) ctxt
val bot = #1 (List.last atp_proof)
@@ -326,14 +330,14 @@
val l = label_of_clause c
val t = prop_of_clause c
val rule = rule_of_clause_id id
- val skolem = is_skolemize_rule rule
+ val introduces_symbols = is_symbol_introduction_rule rule
val deps = ([], [])
|> fold add_fact_of_dependency gamma
|> is_maybe_ext_rule rule ? add_global_fact [short_thm_name ctxt ext]
|> sort_facts
val meths =
- (if skolem then skolem_methods
+ (if introduces_symbols then skolem_methods
else if is_arith_rule rule then arith_methods
else systematic_methods')
|> massage_methods
@@ -352,10 +356,10 @@
if is_clause_tainted c then
(case gamma of
[g] =>
- if skolem andalso is_clause_tainted g andalso not (null accum) then
+ if introduces_symbols andalso is_clause_tainted g andalso not (null accum) then
let
- val skos = skolems_of ctxt (prop_of_clause g)
- val subproof = Proof {fixes = skos, assumptions = [], steps = rev accum}
+ val fixes = introduced_symbols_of ctxt (prop_of_clause g)
+ val subproof = Proof {fixes = fixes, assumptions = [], steps = rev accum}
in
isar_steps outer (SOME l) [prove [subproof] ([], [])] infs
end
@@ -364,8 +368,8 @@
| _ => steps_of_rest (prove [] deps))
else
steps_of_rest
- (if skolem then
- (case skolems_of ctxt t of
+ (if introduces_symbols then
+ (case introduced_symbols_of ctxt t of
[] => prove [] deps
| skos => Prove {
qualifiers = [],
@@ -453,7 +457,8 @@
(do_preplay ? keep_fastest_method_of_isar_step (!preplay_data)
#> minimize ? minimize_isar_step_dependencies ctxt preplay_data)
|> tap (trace_isar_proof "Minimized")
- |> `(preplay_outcome_of_isar_proof (!preplay_data))
+ |> `(if do_preplay then preplay_outcome_of_isar_proof (!preplay_data)
+ else K (Play_Timed_Out Time.zeroTime))
||> (comment_isar_proof comment_of
#> chain_isar_proof
#> kill_useless_labels_in_isar_proof
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML Tue Feb 22 21:34:12 2022 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML Tue Feb 22 21:34:29 2022 +0100
@@ -166,8 +166,12 @@
play_outcome
end
-fun preplay_isar_step_for_method ctxt chained timeout meth =
- try (raw_preplay_step_for_method ctxt chained timeout meth) #> the_default Play_Failed
+fun preplay_isar_step_for_method ctxt chained timeout meth step =
+ if timeout = Time.zeroTime then
+ Play_Timed_Out Time.zeroTime
+ else
+ try (raw_preplay_step_for_method ctxt chained timeout meth) step
+ |> the_default Play_Failed
val min_preplay_timeout = seconds 0.002
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML Tue Feb 22 21:34:12 2022 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML Tue Feb 22 21:34:29 2022 +0100
@@ -75,12 +75,16 @@
val run_timeout = slice_timeout slices timeout
val (higher_order, nat_as_int) =
(case type_enc of
- SOME s => (String.isSubstring "native_higher" s, String.isSubstring "arith" s)
- | NONE => (false, false))
+ SOME s => (SOME (String.isSubstring "native_higher" s), SOME (String.isSubstring "arith" s))
+ | NONE => (NONE, NONE))
fun repair_context ctxt = ctxt
|> Context.proof_map (SMT_Config.select_solver name)
- |> Config.put SMT_Config.higher_order higher_order
- |> Config.put SMT_Config.nat_as_int nat_as_int
+ |> (case higher_order of
+ SOME higher_order => Config.put SMT_Config.higher_order higher_order
+ | NONE => I)
+ |> (case nat_as_int of
+ SOME nat_as_int => Config.put SMT_Config.nat_as_int nat_as_int
+ | NONE => I)
|> (if overlord then
Config.put SMT_Config.debug_files
(overlord_file_location_of_prover name |> (fn (path, name) => path ^ "/" ^ name))