--- a/src/HOL/TPTP/atp_problem_import.ML Mon Jul 06 10:47:30 2020 +0000
+++ b/src/HOL/TPTP/atp_problem_import.ML Mon Jul 06 16:52:48 2020 +0200
@@ -8,15 +8,14 @@
signature ATP_PROBLEM_IMPORT =
sig
val read_tptp_file : theory -> (string * term -> 'a) -> string ->
- 'a list * ('a list * 'a list) * Proof.context
+ 'a list * ('a list * 'a list) * local_theory
val nitpick_tptp_file : theory -> int -> string -> unit
val refute_tptp_file : theory -> int -> string -> unit
val can_tac : Proof.context -> (Proof.context -> tactic) -> term -> bool
val SOLVE_TIMEOUT : int -> string -> tactic -> tactic
- val atp_tac : Proof.context -> int -> (string * string) list -> int -> term list -> string ->
+ val atp_tac : local_theory -> 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 smt_solver_tac : string -> local_theory -> int -> tactic
val make_conj : term list * term list -> term list -> term
val sledgehammer_tptp_file : theory -> int -> string -> unit
val isabelle_tptp_file : theory -> int -> string -> unit
@@ -73,14 +72,14 @@
fun nitpick_tptp_file thy timeout file_name =
let
- val (conjs, (defs, nondefs), ctxt) = read_tptp_file thy snd file_name
- val thy = Proof_Context.theory_of ctxt
+ val (conjs, (defs, nondefs), lthy) = read_tptp_file thy snd file_name
+ val thy = Proof_Context.theory_of lthy
val (defs, pseudo_defs) = defs
- |> map (ATP_Util.abs_extensionalize_term ctxt #> aptrueprop (hol_open_form I))
+ |> map (ATP_Util.abs_extensionalize_term lthy #> aptrueprop (hol_open_form I))
|> List.partition (is_legitimate_tptp_def o perhaps (try HOLogic.dest_Trueprop)
o ATP_Util.unextensionalize_def)
val nondefs = pseudo_defs @ nondefs
- val state = Proof.init ctxt
+ val state = Proof.init lthy
val params =
[("card", "1-100"),
("box", "false"),
@@ -118,12 +117,12 @@
else
"GaveUp")
|> writeln
- val (conjs, (defs, nondefs), ctxt) = read_tptp_file thy snd file_name
+ val (conjs, (defs, nondefs), lthy) = read_tptp_file thy snd file_name
val params =
[("maxtime", string_of_int timeout),
("maxvars", "100000")]
in
- Refute.refute_term ctxt params (defs @ nondefs)
+ Refute.refute_term lthy params (defs @ nondefs)
(case conjs of conj :: _ => conj | [] => \<^prop>\<open>True\<close>)
|> print_szs_of_outcome (not (null conjs))
end
@@ -146,7 +145,7 @@
| SOME st' => (writeln ("SUCCESS: " ^ name); Seq.single st'))
end
-fun nitpick_finite_oracle_tac ctxt timeout i th =
+fun nitpick_finite_oracle_tac lthy timeout i th =
let
fun is_safe (Type (\<^type_name>\<open>fun\<close>, Ts)) = forall is_safe Ts
| is_safe \<^typ>\<open>prop\<close> = true
@@ -159,8 +158,8 @@
Seq.empty
else
let
- val thy = Proof_Context.theory_of ctxt
- val state = Proof.init ctxt
+ val thy = Proof_Context.theory_of lthy
+ val state = Proof.init lthy
val params =
[("box", "false"),
("max_threads", "1"),
@@ -177,22 +176,22 @@
val (outcome, _) =
Nitpick.pick_nits_in_term state params Nitpick.Normal i n step subst [] [] conj
in
- if outcome = "none" then ALLGOALS (Skip_Proof.cheat_tac ctxt) th else Seq.empty
+ if outcome = "none" then ALLGOALS (Skip_Proof.cheat_tac lthy) th else Seq.empty
end
end
-fun atp_tac ctxt completeness override_params timeout assms prover =
+fun atp_tac lthy completeness override_params timeout assms prover =
let
- val thy = Proof_Context.theory_of ctxt
+ val thy = Proof_Context.theory_of lthy
val assm_ths0 = map (Skip_Proof.make_thm thy) assms
- val ((assm_name, _), ctxt) = ctxt
+ val ((assm_name, _), lthy) = lthy
|> Config.put Sledgehammer_Prover_ATP.atp_completish (if completeness > 0 then 3 else 0)
|> Local_Theory.note ((\<^binding>\<open>thms\<close>, []), 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
+ Sledgehammer_Tactics.sledgehammer_as_oracle_tac lthy
([("debug", if debug then "true" else "false"),
("overlord", if overlord then "true" else "false"),
("provers", prover),
@@ -205,13 +204,13 @@
{add = ref_of_assms :: map ref_of [ext, @{thm someI}], del = [], only = true} []
end
-fun sledgehammer_tac demo ctxt timeout assms i =
+fun sledgehammer_tac demo lthy 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) assms prover i)
+ (atp_tac lthy completeness [] (mult * timeout div frac) assms prover i)
in
slice 2 0 ATP_Proof.spassN
ORELSE slice 2 0 ATP_Proof.vampireN
@@ -229,36 +228,27 @@
no_tac)
end
-fun smt_solver_tac solver ctxt =
+fun smt_solver_tac solver lthy =
let
- val ctxt = ctxt |> Context.proof_map (SMT_Config.select_solver solver)
- in SMT_Solver.smt_tac ctxt [] end
+ val lthy = lthy |> Context.proof_map (SMT_Config.select_solver solver)
+ in SMT_Solver.smt_tac lthy [] end
-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)
+fun auto_etc_tac lthy timeout assms i =
+ SOLVE_TIMEOUT (timeout div 20) "nitpick" (nitpick_finite_oracle_tac lthy (timeout div 20) i)
+ ORELSE SOLVE_TIMEOUT (timeout div 10) "simp" (asm_full_simp_tac lthy i)
+ ORELSE SOLVE_TIMEOUT (timeout div 10) "blast" (blast_tac lthy i)
ORELSE SOLVE_TIMEOUT (timeout div 5) "auto+spass"
- (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) "cvc4" (smt_solver_tac "cvc4" 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) "meson" (Meson.meson_tac ctxt [] i)
- ORELSE SOLVE_TIMEOUT (timeout div 10) "fastforce" (fast_force_tac ctxt i)
+ (auto_tac lthy THEN ALLGOALS (atp_tac lthy 0 [] (timeout div 5) assms ATP_Proof.spassN))
+ ORELSE SOLVE_TIMEOUT (timeout div 10) "fast" (fast_tac lthy i)
+ ORELSE SOLVE_TIMEOUT (timeout div 20) "z3" (smt_solver_tac "z3" lthy i)
+ ORELSE SOLVE_TIMEOUT (timeout div 20) "cvc4" (smt_solver_tac "cvc4" lthy i)
+ ORELSE SOLVE_TIMEOUT (timeout div 20) "best" (best_tac lthy i)
+ ORELSE SOLVE_TIMEOUT (timeout div 10) "force" (force_tac lthy i)
+ ORELSE SOLVE_TIMEOUT (timeout div 10) "meson" (Meson.meson_tac lthy [] i)
+ ORELSE SOLVE_TIMEOUT (timeout div 10) "fastforce" (fast_force_tac lthy i)
fun problem_const_prefix thy = Context.theory_name thy ^ Long_Name.separator
-(* Isabelle's standard automatic tactics ("auto", etc.) are more eager to
- unfold "definitions" of free variables than of constants (cf. PUZ107^5). *)
-fun freeze_problem_consts thy =
- let val is_problem_const = String.isPrefix (problem_const_prefix thy) in
- map_aterms
- (fn t as Const (s, T) => if is_problem_const s then Free (Long_Name.base_name s, T) else t
- | t => t)
- end
-
fun make_conj (defs, nondefs) conjs =
Logic.list_implies (rev defs @ rev nondefs, case conjs of conj :: _ => conj | [] => \<^prop>\<open>False\<close>)
@@ -271,27 +261,27 @@
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 (conjs, assms, lthy) = read_tptp_file thy snd file_name
val conj = make_conj ([], []) conjs
val assms = op @ assms
in
- can_tac ctxt (fn ctxt => sledgehammer_tac true ctxt timeout assms 1) conj
+ can_tac lthy (fn lthy => sledgehammer_tac true lthy 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 (conjs, assms, lthy) = read_tptp_file thy snd file_name
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 (fn ctxt => auto_etc_tac ctxt (timeout div 2) assms 1) full_conj orelse
- can_tac ctxt (fn ctxt => sledgehammer_tac demo ctxt (timeout div 2) assms 1) conj orelse
- can_tac ctxt (fn ctxt => SOLVE_TIMEOUT timeout (last_hope_atp ^ "(*)")
- (atp_tac ctxt last_hope_completeness [] timeout assms last_hope_atp 1)) full_conj)
+ (can_tac lthy (fn lthy => auto_etc_tac lthy (timeout div 2) assms 1) full_conj orelse
+ can_tac lthy (fn lthy => sledgehammer_tac demo lthy (timeout div 2) assms 1) conj orelse
+ can_tac lthy (fn lthy => SOLVE_TIMEOUT timeout (last_hope_atp ^ "(*)")
+ (atp_tac lthy last_hope_completeness [] timeout assms last_hope_atp 1)) full_conj)
|> print_szs_of_success conjs
end
@@ -303,7 +293,7 @@
fun translate_tptp_file thy format_str file_name =
let
- val (conjs, (defs, nondefs), ctxt) = read_tptp_file thy I file_name
+ val (conjs, (defs, nondefs), lthy) = read_tptp_file thy I file_name
val conj = make_conj ([], []) (map snd conjs)
val (format, type_enc, lam_trans) =
@@ -322,11 +312,11 @@
map (apfst (rpair (Global, Non_Rec_Def))) defs @
map (apfst (rpair (Global, General))) nondefs
val (atp_problem, _, _, _) =
- generate_atp_problem ctxt generate_info format Hypothesis (type_enc_of_string Strict type_enc)
+ generate_atp_problem lthy generate_info format Hypothesis (type_enc_of_string Strict type_enc)
Translator
lam_trans uncurried_aliases readable_names presimp [] conj facts
- val ord = effective_term_order ctxt spassN
+ val ord = effective_term_order lthy spassN
val ord_info = K []
val lines = lines_of_atp_problem format ord ord_info atp_problem
in