# HG changeset patch # User blanchet # Date 1594047168 -7200 # Node ID 3e08311ada8ec8209d01e3ba45901b1073002dc0 # Parent 379d0c207c291a6efafd0c57f0332290879cdafb removed 'freeze_problem_consts' hack in TPTP tools, which wasn't compatible with post-2016 reforms to local theories diff -r 379d0c207c29 -r 3e08311ada8e NEWS --- a/NEWS Mon Jul 06 10:47:30 2020 +0000 +++ b/NEWS Mon Jul 06 16:52:48 2020 +0200 @@ -81,6 +81,10 @@ into theories Misc_lsb, Misc_msb and Misc_set_bit respectively. INCOMPATIBILITY. +* Session HOL-TPTP: The "tptp_isabelle" and "tptp_sledgehammer" +commands are in working order again, as opposed to outputting +"GaveUp" on nearly all problems. + * Simproc defined_all and rewrite rule subst_all perform more aggressive substitution with variables from assumptions. INCOMPATIBILITY, use something like diff -r 379d0c207c29 -r 3e08311ada8e src/HOL/TPTP/ATP_Problem_Import.thy --- a/src/HOL/TPTP/ATP_Problem_Import.thy Mon Jul 06 10:47:30 2020 +0000 +++ b/src/HOL/TPTP/ATP_Problem_Import.thy Mon Jul 06 16:52:48 2020 +0200 @@ -5,7 +5,7 @@ section \ATP Problem Importer\ theory ATP_Problem_Import -imports Complex_Main TPTP_Interpret "HOL-Library.Refute" + imports Complex_Main TPTP_Interpret "HOL-Library.Refute" begin ML_file \sledgehammer_tactics.ML\ diff -r 379d0c207c29 -r 3e08311ada8e src/HOL/TPTP/atp_problem_import.ML --- 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>\True\) |> 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>\fun\, Ts)) = forall is_safe Ts | is_safe \<^typ>\prop\ = 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>\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 + 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>\False\) @@ -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