--- a/src/HOL/TPTP/ATP_Problem_Import.thy Fri Apr 27 22:58:29 2012 +0200
+++ b/src/HOL/TPTP/ATP_Problem_Import.thy Fri Apr 27 23:17:58 2012 +0200
@@ -3,6 +3,7 @@
*)
header {* ATP Problem Importer *}
+
theory ATP_Problem_Import
imports Complex_Main TPTP_Interpret
uses "sledgehammer_tactics.ML"
--- a/src/HOL/TPTP/atp_problem_import.ML Fri Apr 27 22:58:29 2012 +0200
+++ b/src/HOL/TPTP/atp_problem_import.ML Fri Apr 27 23:17:58 2012 +0200
@@ -69,7 +69,6 @@
val params =
[("card", "1\<emdash>100"),
("box", "false"),
- ("sat_solver", "smart"),
("max_threads", "1"),
("batch_size", "5"),
("falsify", if null conjs then "false" else "true"),
@@ -134,13 +133,47 @@
| SOME st' => (Output.urgent_message ("SUCCESS: " ^ name); Seq.single st')
end
+fun nitpick_finite_oracle_tac ctxt timeout i th =
+ let
+ fun is_safe (Type (@{type_name fun}, Ts)) = forall is_safe Ts
+ | is_safe @{typ prop} = true
+ | is_safe @{typ bool} = true
+ | is_safe _ = false
+ val conj = Thm.term_of (Thm.cprem_of th i)
+ in
+ if exists_type (not o is_safe) conj then
+ Seq.empty
+ else
+ let
+ val thy = Proof_Context.theory_of ctxt
+ val state = Proof.init ctxt
+ val params =
+ [("box", "false"),
+ ("max_threads", "1"),
+ ("verbose", "true"),
+ ("debug", if debug then "true" else "false"),
+ ("overlord", if overlord then "true" else "false"),
+ ("max_potential", "0"),
+ ("timeout", string_of_int timeout)]
+ |> Nitpick_Isar.default_params thy
+ val i = 1
+ val n = 1
+ val step = 0
+ val subst = []
+ val (outcome, _) =
+ Nitpick.pick_nits_in_term state params Nitpick.Normal i n step subst
+ [] [] conj
+ in if outcome = "none" then Skip_Proof.cheat_tac thy th else Seq.empty end
+ end
+
fun atp_tac ctxt override_params timeout prover =
Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt
([("debug", if debug then "true" else "false"),
("overlord", if overlord then "true" else "false"),
("provers", prover),
("timeout", string_of_int timeout)] @ override_params)
- {add = [], del = [], only = true}
+ {add = [(Facts.named (Thm.derivation_name ext), [])],
+ del = [], only = true}
fun sledgehammer_tac ctxt timeout i =
let
@@ -156,17 +189,20 @@
end
fun auto_etc_tac ctxt timeout i =
- SOLVE_TIMEOUT (timeout div 10) "simp" (asm_full_simp_tac (simpset_of ctxt) i)
+ SOLVE_TIMEOUT (timeout div 20) "nitpick"
+ (nitpick_finite_oracle_tac ctxt (timeout div 20) i)
+ ORELSE SOLVE_TIMEOUT (timeout div 10) "simp"
+ (asm_full_simp_tac (simpset_of ctxt) i)
ORELSE SOLVE_TIMEOUT (timeout div 10) "blast" (blast_tac ctxt i)
ORELSE SOLVE_TIMEOUT (timeout div 5) "auto+spass"
(auto_tac ctxt
THEN ALLGOALS (atp_tac ctxt [] (timeout div 5) ATP_Systems.spassN))
ORELSE SOLVE_TIMEOUT (timeout div 5) "smt" (SMT_Solver.smt_tac ctxt [] i)
- ORELSE SOLVE_TIMEOUT (timeout div 10) "fast" (fast_tac ctxt i)
- ORELSE SOLVE_TIMEOUT (timeout div 10) "best" (best_tac ctxt i)
+ ORELSE SOLVE_TIMEOUT (timeout div 20) "fast" (fast_tac ctxt i)
+ ORELSE SOLVE_TIMEOUT (timeout div 20) "best" (best_tac ctxt i)
ORELSE SOLVE_TIMEOUT (timeout div 10) "force" (force_tac ctxt i)
- ORELSE SOLVE_TIMEOUT (timeout div 10) "arith" (Arith_Data.arith_tac ctxt i)
- ORELSE SOLVE_TIMEOUT timeout "fastforce" (fast_force_tac ctxt i)
+ ORELSE SOLVE_TIMEOUT (timeout div 20) "arith" (Arith_Data.arith_tac ctxt i)
+ ORELSE SOLVE_TIMEOUT (timeout div 10) "fastforce" (fast_force_tac ctxt i)
fun problem_const_prefix thy = Context.theory_name thy ^ Long_Name.separator
@@ -207,8 +243,8 @@
read_tptp_file thy (freeze_problem_consts thy) file_name
val conj = make_conj assms conjs
in
- (can_tac ctxt (sledgehammer_tac ctxt (timeout div 2) 1) conj orelse
- can_tac ctxt (auto_etc_tac ctxt (timeout div 2) 1) conj orelse
+ (can_tac ctxt (auto_etc_tac ctxt (timeout div 2) 1) conj orelse
+ can_tac ctxt (sledgehammer_tac ctxt (timeout div 2) 1) conj orelse
can_tac ctxt (atp_tac ctxt [] timeout ATP_Systems.satallaxN 1) conj)
|> print_szs_from_success conjs
end
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML Fri Apr 27 22:58:29 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Fri Apr 27 23:17:58 2012 +0200
@@ -1681,7 +1681,7 @@
level_of_type_enc type_enc <> No_Types andalso
not (null (Term.hidden_polymorphism t))
-fun helper_facts_for_sym ctxt format type_enc (s, {types, ...} : sym_info) =
+fun add_helper_facts_for_sym ctxt format type_enc (s, {types, ...} : sym_info) =
case unprefix_and_unascii const_prefix s of
SOME mangled_s =>
let
@@ -1705,20 +1705,20 @@
val make_facts = map_filter (make_fact ctxt format type_enc false)
val fairly_sound = is_type_enc_fairly_sound type_enc
in
- helper_table
- |> maps (fn ((helper_s, needs_fairly_sound), ths) =>
- if helper_s <> unmangled_s orelse
- (needs_fairly_sound andalso not fairly_sound) then
- []
- else
- ths ~~ (1 upto length ths)
- |> maps (dub_and_inst needs_fairly_sound)
- |> make_facts)
+ fold (fn ((helper_s, needs_fairly_sound), ths) =>
+ if helper_s <> unmangled_s orelse
+ (needs_fairly_sound andalso not fairly_sound) then
+ I
+ else
+ ths ~~ (1 upto length ths)
+ |> maps (dub_and_inst needs_fairly_sound)
+ |> make_facts
+ |> union (op = o pairself #iformula))
+ helper_table
end
- | NONE => []
+ | NONE => I
fun helper_facts_for_sym_table ctxt format type_enc sym_tab =
- Symtab.fold_rev (append o helper_facts_for_sym ctxt format type_enc) sym_tab
- []
+ Symtab.fold_rev (add_helper_facts_for_sym ctxt format type_enc) sym_tab []
(***************************************************************)
(* Type Classes Present in the Axiom or Conjecture Clauses *)