--- a/src/HOL/TPTP/ATP_Problem_Import.thy Thu Aug 07 12:17:41 2014 +0200
+++ b/src/HOL/TPTP/ATP_Problem_Import.thy Thu Aug 07 12:17:41 2014 +0200
@@ -5,10 +5,7 @@
header {* ATP Problem Importer *}
theory ATP_Problem_Import
-imports
- Complex_Main
- TPTP_Interpret
- "~~/src/HOL/Library/Refute"
+imports Complex_Main TPTP_Interpret "~~/src/HOL/Library/Refute"
begin
ML_file "sledgehammer_tactics.ML"
@@ -24,8 +21,7 @@
ML_file "atp_problem_import.ML"
(*
-ML {* ATP_Problem_Import.isabelle_tptp_file @{theory} 50
- "$TPTP/Problems/PUZ/PUZ107^5.p" *}
+ML {* ATP_Problem_Import.isabelle_tptp_file @{theory} 50 "$TPTP/Problems/PUZ/PUZ107^5.p" *}
*)
end
--- a/src/HOL/TPTP/atp_problem_import.ML Thu Aug 07 12:17:41 2014 +0200
+++ b/src/HOL/TPTP/atp_problem_import.ML Thu Aug 07 12:17:41 2014 +0200
@@ -13,7 +13,8 @@
val refute_tptp_file : theory -> int -> string -> unit
val can_tac : Proof.context -> tactic -> term -> bool
val SOLVE_TIMEOUT : int -> string -> tactic -> tactic
- val atp_tac : Proof.context -> int -> (string * string) list -> int -> string -> int -> tactic
+ val atp_tac : Proof.context -> int -> (string * string) list -> int -> term list -> string ->
+ int -> tactic
val smt_solver_tac : string -> Proof.context -> int -> tactic
val freeze_problem_consts : theory -> term -> term
val make_conj : term list * term list -> term list -> term
@@ -56,7 +57,7 @@
in
(map (get_prop I) conjs,
pairself (map (get_prop Logic.varify_global)) defs_and_nondefs,
- Proof_Context.init_global thy)
+ Named_Target.theory_init thy)
end
@@ -181,10 +182,16 @@
end
end
-fun atp_tac ctxt completeness override_params timeout prover =
+fun atp_tac ctxt completeness override_params timeout assms prover =
let
- val ctxt = ctxt |> Config.put Sledgehammer_Prover_ATP.atp_completish (completeness > 0)
+ val thy = Proof_Context.theory_of ctxt
+ val assm_ths0 = map (Skip_Proof.make_thm thy) assms
+ val ((assm_name, _), ctxt) = ctxt
+ |> Config.put Sledgehammer_Prover_ATP.atp_completish (completeness > 0)
+ |> Local_Theory.note ((@{binding thms}, []), assm_ths0)
+
fun ref_of th = (Facts.named (Thm.derivation_name th), [])
+ val ref_of_assms = (Facts.named assm_name, [])
in
Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt
([("debug", if debug then "true" else "false"),
@@ -196,16 +203,16 @@
else
[]) @
override_params)
- {add = map ref_of [ext, @{thm someI}], del = [], only = true}
+ {add = ref_of_assms :: map ref_of [ext, @{thm someI}], del = [], only = true} []
end
-fun sledgehammer_tac demo ctxt timeout i =
+fun sledgehammer_tac demo ctxt timeout assms i =
let
val frac = if demo then 16 else 12
fun slice mult completeness prover =
SOLVE_TIMEOUT (mult * timeout div frac)
(prover ^ (if completeness > 0 then "(" ^ string_of_int completeness ^ ")" else ""))
- (atp_tac ctxt completeness [] (mult * timeout div frac) prover i)
+ (atp_tac ctxt completeness [] (mult * timeout div frac) assms prover i)
in
slice 2 0 ATP_Proof.spassN
ORELSE slice 2 0 ATP_Proof.vampireN
@@ -228,12 +235,12 @@
val ctxt = ctxt |> Context.proof_map (SMT_Config.select_solver solver)
in SMT_Solver.smt_tac ctxt [] end
-fun auto_etc_tac ctxt timeout i =
+fun auto_etc_tac ctxt timeout assms 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 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 0 [] (timeout div 5) ATP_Proof.spassN))
+ (auto_tac ctxt THEN ALLGOALS (atp_tac ctxt 0 [] (timeout div 5) assms ATP_Proof.spassN))
ORELSE SOLVE_TIMEOUT (timeout div 10) "fast" (fast_tac ctxt i)
ORELSE SOLVE_TIMEOUT (timeout div 20) "z3" (smt_solver_tac "z3" ctxt i)
ORELSE SOLVE_TIMEOUT (timeout div 20) "cvc3" (smt_solver_tac "cvc3" ctxt i)
@@ -266,23 +273,26 @@
fun sledgehammer_tptp_file thy timeout file_name =
let
val (conjs, assms, ctxt) = read_tptp_file thy (freeze_problem_consts thy o snd) file_name
- val conj = make_conj assms conjs
+ val conj = make_conj ([], []) conjs
+ val assms = op @ assms
in
- can_tac ctxt (sledgehammer_tac true ctxt timeout 1) conj
+ can_tac ctxt (sledgehammer_tac true ctxt timeout assms 1) conj
|> print_szs_of_success conjs
end
fun generic_isabelle_tptp_file demo thy timeout file_name =
let
val (conjs, assms, ctxt) = read_tptp_file thy (freeze_problem_consts thy o snd) file_name
- val conj = make_conj assms conjs
+ val conj = make_conj ([], []) conjs
+ val full_conj = make_conj assms conjs
+ val assms = op @ assms
val (last_hope_atp, last_hope_completeness) =
if demo then (ATP_Proof.satallaxN, 0) else (ATP_Proof.vampireN, 2)
in
- (can_tac ctxt (auto_etc_tac ctxt (timeout div 2) 1) conj orelse
- can_tac ctxt (sledgehammer_tac demo ctxt (timeout div 2) 1) conj orelse
+ (can_tac ctxt (auto_etc_tac ctxt (timeout div 2) assms 1) full_conj orelse
+ can_tac ctxt (sledgehammer_tac demo ctxt (timeout div 2) assms 1) conj orelse
can_tac ctxt (SOLVE_TIMEOUT timeout (last_hope_atp ^ "(*)")
- (atp_tac ctxt last_hope_completeness [] timeout last_hope_atp 1)) conj)
+ (atp_tac ctxt last_hope_completeness [] timeout assms last_hope_atp 1)) full_conj)
|> print_szs_of_success conjs
end
--- a/src/HOL/TPTP/sledgehammer_tactics.ML Thu Aug 07 12:17:41 2014 +0200
+++ b/src/HOL/TPTP/sledgehammer_tactics.ML Thu Aug 07 12:17:41 2014 +0200
@@ -10,9 +10,9 @@
type fact_override = Sledgehammer_Fact.fact_override
val sledgehammer_with_metis_tac : Proof.context -> (string * string) list -> fact_override ->
- int -> tactic
+ thm list -> int -> tactic
val sledgehammer_as_oracle_tac : Proof.context -> (string * string) list -> fact_override ->
- int -> tactic
+ thm list -> int -> tactic
end;
structure Sledgehammer_Tactics : SLEDGEHAMMER_TACTICS =
@@ -26,7 +26,7 @@
open Sledgehammer_MaSh
open Sledgehammer_Commands
-fun run_prover override_params fact_override i n ctxt goal =
+fun run_prover override_params fact_override chained i n ctxt goal =
let
val thy = Proof_Context.theory_of ctxt
val mode = Normal
@@ -39,10 +39,9 @@
val reserved = reserved_isar_keyword_table ()
val css_table = clasimpset_rule_table_of ctxt
val facts =
- nearly_all_facts ctxt ho_atp fact_override reserved css_table [] hyp_ts concl_t
- |> relevant_facts ctxt params name
- (the_default default_max_facts max_facts) fact_override hyp_ts
- concl_t
+ nearly_all_facts ctxt ho_atp fact_override reserved css_table chained hyp_ts concl_t
+ |> relevant_facts ctxt params name (the_default default_max_facts max_facts) fact_override
+ hyp_ts concl_t
|> hd |> snd
val problem =
{comment = "", state = Proof.init ctxt, goal = goal, subgoal = i, subgoal_count = n,
@@ -54,22 +53,24 @@
handle ERROR message => (warning ("Error: " ^ message ^ "\n"); NONE)
end
-fun sledgehammer_with_metis_tac ctxt override_params fact_override i th =
+fun sledgehammer_with_metis_tac ctxt override_params fact_override chained i th =
let val override_params = override_params @ [("preplay_timeout", "0")] in
- case run_prover override_params fact_override i i ctxt th of
+ (case run_prover override_params fact_override chained i i ctxt th of
SOME facts =>
Metis_Tactic.metis_tac [] ATP_Problem_Generate.combs_or_liftingN ctxt
- (maps (thms_of_name ctxt) facts) i th
- | NONE => Seq.empty
+ (maps (thms_of_name ctxt) facts) i th
+ | NONE => Seq.empty)
end
-fun sledgehammer_as_oracle_tac ctxt override_params fact_override i th =
+fun sledgehammer_as_oracle_tac ctxt override_params fact_override chained i th =
let
val override_params =
override_params @
[("preplay_timeout", "0"),
("minimize", "false")]
- val xs = run_prover override_params fact_override i i ctxt th
- in if is_some xs then ALLGOALS Skip_Proof.cheat_tac th else Seq.empty end
+ val xs = run_prover override_params fact_override chained i i ctxt th
+ in
+ if is_some xs then ALLGOALS Skip_Proof.cheat_tac th else Seq.empty
+ end
end;