| Quellcodebibliothek Statistik Leitseite products/sources/formale Sprachen/Isabelle/HOL/Tools/Sledgehammer/ (Beweissystem Isabelle Version 2025-1©) Datei vom 16.11.2025 mit Größe 18 kB |
|
Quelle sledgehammer_prover_atp.ML Sprache: SML |
|||||||||
|
(* Title: HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML
Author: Fabian Immler, TU Muenchen Author: Makarius Author: Jasmin Blanchette, TU Muenchen ATPs as Sledgehammer provers. *) signature SLEDGEHAMMER_PROVER_ATP = sig type mode = Sledgehammer_Prover.mode type prover = Sledgehammer_Prover.prover val atp_problem_dest_dir : string Config.T val atp_proof_dest_dir : string Config.T val atp_problem_prefix : string Config.T val atp_completish : int Config.T val atp_full_names : bool Config.T val run_atp : mode -> string -> prover end; structure Sledgehammer_Prover_ATP : SLEDGEHAMMER_PROVER_ATP = struct open ATP_Util open ATP_Problem open ATP_Problem_Generate open ATP_Proof open ATP_Proof_Reconstruct open Sledgehammer_Util open Sledgehammer_Proof_Methods open Sledgehammer_Isar open Sledgehammer_ATP_Systems open Sledgehammer_Prover (* Empty string means create files in Isabelle's temporary files directory. *) val atp_problem_dest_dir = Attrib.setup_config_string \<^binding>\<open>sledgehammer_atp_problem_dest_dir\<close> ( val atp_proof_dest_dir = Attrib.setup_config_string \<^binding>\<open>sledgehammer_atp_proof_dest_dir\<close> (K " val atp_problem_prefix = Attrib.setup_config_string \<^binding>\<open>sledgehammer_atp_problem_prefix\<close> (K " val atp_completish = Attrib.setup_config_int \<^binding>\<open>sledgehammer_atp_completi (* In addition to being easier to read, readable names are often much shorter, especially if typ are mangled in names. This makes a difference for some provers (e.g., E). For these reason, shor names are enabled by default. *) val atp_full_names = Attrib.setup_config_bool \<^binding>\<open>sledgehammer_atp_full_na fun choose_type_enc strictness format good_type_enc = type_enc_of_string strictness good_type_enc |> adjust_type_enc format fun has_bound_or_var_of_type pred = exists_subterm (fn Var (_, T as Type _) => pred T | Abs (_, T as Type _, _) => pred T | _ => false) (* Unwanted equalities are those between a (bound or schematic) variable that does not properl occur in the second operand. *) val is_exhaustive_finite = let fun is_bad_equal (Var z) t = not (exists_subterm (fn Var z' => z = z' | _ => false) t) | is_bad_equal (Bound j) t = not (loose_bvar1 (t, j)) | is_bad_equal _ _ = false fun do_equals t1 t2 = is_bad_equal t1 t2 orelse is_bad_equal t2 t1 fun do_formula pos t = (case (pos, t) of (_, \<^Const_>\<open>Trueprop for t1\<close>) => do_formula pos t1 | (true, Const (\<^const_name>\<open>Pure.all\<close>, _) $ Abs (_, _, t')) => do_formula pos t | (true, Const (\<^const_name>\<open>All\<close>, _) $ Abs (_, _, t')) => do_formula pos t' | (false, Const (\<^const_name>\<open>Ex\<close>, _) $ Abs (_, _, t')) => do_formula pos t' | (_, \<^Const_>\<open>Pure.imp for t1 t2\<close>) => do_formula (not pos) t1 andalso (t2 = \<^prop>\<open>False\<close> orelse do_formula pos t2) | (_, \<^Const_>\<open>implies for t1 t2\<close>) => do_formula (not pos) t1 andalso (t2 = \<^Const>\<open>False\<close> orelse do_formula pos t2) | (_, \<^Const_>\<open>Not for t1\<close>) => do_formula (not pos) t1 | (true, \<^Const_>\<open>disj for t1 t2\<close>) => forall (do_formula pos) [t1, t2] | (false, \<^Const_>\<open>conj for t1 t2\<close>) => forall (do_formula pos) [t1, t2] | (true, Const (\<^const_name>\<open>HOL.eq\<close>, _) $ t1 $ t2) => do_equals t1 t2 | (true, Const (\<^const_name>\<open>Pure.eq\<close>, _) $ t1 $ t2) => do_equals t1 t2 | _ => false) in do_formula true end (* Facts containing variables of finite types such as "unit" or "bool" or of the form "ALL x. x = A | x = B | x = C" are likely to lead to untypable proofs for unsound type encodings. *) fun is_dangerous_prop ctxt = transform_elim_prop #> (has_bound_or_var_of_type (is_type_surely_finite ctxt) orf is_exhaustive_finite) val mono_max_privileged_facts = 10 fun suffix_of_mode Auto_Try = "_try" | suffix_of_mode Try = "_try" | suffix_of_mode Normal = "" | suffix_of_mode MaSh = "" | suffix_of_mode Minimize = "_min" fun tptp_logic_of_atp_format CNF = "CNF" | tptp_logic_of_atp_format CNF_UEQ = "CNF" | tptp_logic_of_atp_format FOF = "FOF" | tptp_logic_of_atp_format (TFF (Monomorphic, Without_FOOL)) = "TF0" | tptp_logic_of_atp_format (TFF (Polymorphic, Without_FOOL)) = "TF1" | tptp_logic_of_atp_format (TFF (Monomorphic, With_FOOL _)) = "TX0" | tptp_logic_of_atp_format (TFF (Polymorphic, With_FOOL _)) = "TX1" | tptp_logic_of_atp_format (THF (Monomorphic, _, _)) = "TH0" | tptp_logic_of_atp_format (THF (Polymorphic, _, _)) = "TH1" | tptp_logic_of_atp_format (DFG _) = "DFG" fun run_atp mode name ({debug, verbose, overlord, abduce = abduce_max_candidates, strict, max_mono_iters, max_new_mono_instances, isar_proofs, compress, try0, smt_proofs, minimize, slices, time preplay_timeout, spy, ...} : params) ({comment, state, goal, subgoal, subgoal_count, factss, has_already_found_something, found_something, memoize_fun_call} : prover_problem) slice = let val (basic_slice as (slice_size, abduce, _, _, _), ATP_Slice (good_format, good_type_enc, good_lam_trans, good_uncurried_aliases, extra) slice val facts = facts_of_basic_slice basic_slice factss val thy = Proof.theory_of state val ctxt = Proof.context_of state val {exec, arguments, proof_delims, known_failures, prem_role, generate_isabelle_info, good_max_mono_iters, good_max_new_mono_instances, ...} = get_atp thy name () val full_proofs = isar_proofs |> the_default (mode = Minimize) val local_name = perhaps (try (unprefix remote_prefix)) name val completish = Config.get ctxt atp_completish val atp_mode = if completish > 0 then Sledgehammer_Completish completish else Sledgehammer val (_, hyp_ts, concl_t) = strip_subgoal goal subgoal ctxt val (problem_dest_dir, proof_dest_dir, problem_prefix) = if overlord then overlord_file_location_of_prover name |> (fn (dir, prefix) => (dir, dir, prefix)) else (Config.get ctxt atp_problem_dest_dir, Config.get ctxt atp_proof_dest_dir, Config.get ctxt atp_problem_prefix) val (problem_file_name, proof_file_name) = let val base_name = problem_prefix ^ (if overlord then "" else serial_string ()) ^ suffix_of_mode mode ^ "_" ^ string_of_int subgoal in (base_name, suffix "_proof" base_name) |> apply2 Path.basic |> apply2 (Path.ext "p") end val prob_path = if problem_dest_dir = "" then File.tmp_path problem_file_name else let val problem_dest_dir_path = Path.explode problem_dest_dir in if File.is_dir problem_dest_dir_path then problem_dest_dir_path + problem_file_name else error ("No such directory: " ^ quote problem_dest_dir) end val executable = (case find_first (fn var => getenv var <> "") (fst exec) of SOME var => let val pref = getenv var ^ "/" val paths = map (Path.explode o prefix pref) (if ML_System.platform_is_windows then map (suffix ".exe") (snd exec) @ snd exec else snd exec); in (case find_first File.exists paths of SOME path => path | NONE => error ("Bad executable: " ^ Path.print (hd paths))) end | NONE => error ("The environment variable " ^ quote (List.last (fst exec)) ^ " is not set") fun run () = let fun monomorphize_facts facts = let val ctxt = ctxt |> repair_monomorph_context max_mono_iters good_max_mono_iters max_new_mono_instances good_max_new_mono_instances (* pseudo-theorem involving the same constants as the subgoal *) val subgoal_th = Logic.list_implies (hyp_ts, concl_t) |> Skip_Proof.make_thm thy val rths = facts |> chop mono_max_privileged_facts |>> map (pair 1 o snd) ||> map (pair 2 o snd) |> op @ |> cons (0, subgoal_th) in Monomorph.monomorph atp_schematic_consts_of ctxt rths |> tl |> curry ListPair.zip (map fst facts) |> maps (fn (name, rths) => map (pair name o zero_var_indexes o snd) rths) end val strictness = if strict then Strict else Non_Strict val type_enc = choose_type_enc strictness good_format good_type_enc val run_timeout = slice_timeout slice_size slices timeout val generous_run_timeout = if mode = MaSh then one_day else if abduce then run_timeout + seconds 5.0 else run_timeout val ({elapsed, ...}, atp_problem_data as (atp_problem, _, _, _)) = Timing.timing (fn () => let val readable_names = not (Config.get ctxt atp_full_names) in facts |> not (is_type_enc_sound type_enc) ? filter_out (is_dangerous_prop ctxt o Thm.prop_of o snd) |> not (is_type_enc_polymorphic type_enc) ? monomorphize_facts |> map (apsnd Thm.prop_of) |> generate_atp_problem ctxt generate_isabelle_info good_format prem_role type_enc atp_mode good_lam_trans good_uncurried_aliases readable_names true hyp_ts concl_t end) () val () = spying spy (fn () => (state, subgoal, name, "Generating ATP problem in " ^ string_of_int (Time.toMilliseconds elapsed) ^ " ms")) val make_args = arguments abduce full_proofs extra run_timeout fun make_command args = implode_space (File.bash_path executable :: args) val args = make_args prob_path val command = make_command args val lines_of_atp_problem = lines_of_atp_problem good_format (fn () => atp_problem_term_order_info atp_problem) atp_problem val () = lines_of_atp_problem |> (exec <> isabelle_scala_function) ? cons ("% " ^ command ^ "\n" ^ (if comment = "" then "" else "% " ^ comment ^ "\n")) |> File.write_list prob_path fun run_command () = let val sledgehammer_persistent_data_dir = Options.default_string \<^system_option>\<open>sledgehammer_persistent_data_dir\<close> val env = if sledgehammer_persistent_data_dir = "" then [] else let val tptp_logic = tptp_logic_of_atp_format good_format val thy_long_name = Context.theory_long_name thy val session_name = Long_Name.qualifier thy_long_name val dir = Path.expand (Path.explode sledgehammer_persistent_data_dir + Path.explode (name ^ "-" ^ session_name) + Path.explode tptp_logic) in [("SLH_PERSISTENT_DATA_DIR", Path.implode dir)] end val f = fn _ => if exec = isabelle_scala_function then let val {output, ...} = SystemOnTPTP.run_system_encoded args in output end else Bash.script command |> Bash.putenv env |> Bash.redirect |> Isabelle_System.bash_process |> Process_Result.out (* Hackish: The following lines try to make the TPTP problem and command line more deterministic and constant. *) val hackish_lines = drop 2 lines_of_atp_problem val hackish_command = make_command (make_args (Path.basic "fake_prob_path.p")) val arg = cat_lines (hackish_command :: hackish_lines) in Timing.timing (memoize_fun_call f) arg end val local_name = name |> perhaps (try (unprefix remote_prefix)) val ((output, run_time), ((atp_proof, tstplike_proof), outcome)) = let val ({elapsed, ...}, output) = Timeout.apply generous_run_timeout run_command () val output = if overlord then prefix ("% " ^ command ^ "\n% " ^ timestamp () ^ "\n") output else output val output2 = extract_tstplike_proof_and_outcome verbose proof_delims known_failures output |>> `(atp_proof_of_tstplike_proof false local_name atp_problem) handle UNRECOGNIZED_ATP_PROOF () => (([], ""), SOME ProofUnparsable) in ((output, elapsed), output2) end handle Timeout.TIMEOUT _ => (("", run_timeout), (([], ""), SOME TimedOut)) | ERROR msg => (("", Time.zeroTime), (([], ""), SOME (UnknownError msg))) val atp_abduce_candidates = if abduce andalso outcome <> NONE andalso not (has_already_found_something ()) then atp_abduce_candidates_of_output local_name atp_problem output else [] val () = spying spy (fn () => (state, subgoal, name, "Running command in " ^ string_of_int (Time.toMilliseconds run_time) ^ " ms")) val outcome = (case outcome of NONE => (found_something name; NONE) | _ => outcome) in (atp_problem_data, (output, run_time, facts, atp_problem, tstplike_proof, atp_proof, atp_abduce_candidate outcome), (good_format, type_enc)) end (* If the problem file has not been exported, remove it; otherwise, export the proof file too. *) fun clean_up () = if problem_dest_dir = "" then (try File.rm prob_path; ()) else () fun export (_, (output, _, _, _, _, _, _, _), _) = if proof_dest_dir = "" then Output.system_message "don't export proof" else let val proof_dest_dir_path = Path.explode proof_dest_dir in if File.is_dir proof_dest_dir_path then File.write (proof_dest_dir_path + proof_file_name) output else error ("No such directory: " ^ quote proof_dest_dir) end val ((_, pool, lifted, sym_tab), (_, run_time, used_from, atp_problem, tstplike_proof, atp_proof, atp_abduce_candidates, outcome), (format, type_enc)) = \<^try>\<open>run () finally clean_up ()\<close> |> tap export val (outcome, used_facts, preferred_methss, message) = (case outcome of NONE => let val used_facts = sort_by fst (used_facts_in_atp_proof ctxt (map fst used_from) atp_proof) val _ = if mode = Normal andalso not (is_conjecture_used_in_proof atp_proof) andalso not (Logic.get_goal (Thm.prop_of goal) subgoal aconv @{prop False}) then warning ("Derived \"False\" from these facts alone: " ^ implode_space (map fst used_facts)) else () val needs_full_types = is_typed_helper_used_in_atp_proof atp_proof val needs_lam_defs = good_lam_trans = keep_lamsN orelse is_lam_def_used_in_atp_proof atp_proof val preferred = Metis_Method (NONE, NONE, []) val preferred_methss = (preferred, if try0 then bunches_of_proof_methods ctxt smt_proofs needs_full_types needs_lam_defs else bunches_of_metis_methods ctxt needs_full_types needs_lam_defs) in (NONE, used_facts, preferred_methss, fn preplay_outcome => let val _ = if verbose then writeln "Generating proof text..." else () fun isar_params () = let val full_atp_proof = atp_proof_of_tstplike_proof true (perhaps (try (unprefix remote_prefix)) name) atp_problem tstplike_proof val metis_type_enc = if is_typed_helper_used_in_atp_proof full_atp_proof then SOME full_typesN else NONE val metis_lam_trans = if atp_proof_prefers_lifting full_atp_proof then SOME liftingN else NONE val full_atp_proof = full_atp_proof |> termify_atp_proof ctxt name format type_enc pool lifted sym_tab |> local_name = spassN ? introduce_spass_skolems |> local_name = zipperpositionN ? regroup_zipperposition_skolems |> factify_atp_proof (map fst used_from) hyp_ts concl_t in (verbose, (metis_type_enc, metis_lam_trans, []), preplay_timeout, compress, try0, minimize, full_atp_proof, goal) end val preplay_result = preplay_outcome |> the_default (map (apfst Pretty.str) used_facts, (preferred, Play_Timed_Out Time.zeroTime)) val one_line_params = (preplay_result, proof_banner mode name, subgoal, subgoal_count) val num_chained = length (#facts (Proof.goal state)) in proof_text ctxt debug isar_proofs smt_proofs isar_params num_chained one_line_params end) end | SOME failure => let val max_abduce_candidates_factor = 3 (* FUDGE *) val max_abduce_candidates = the_default default_abduce_max_candidates abduce_max_candidates val abduce_candidates = atp_abduce_candidates |> map (termify_atp_abduce_candidate ctxt name format type_enc pool lifted sym_tab) |> top_abduce_candidates (max_abduce_candidates * max_abduce_candidates_factor) |> sort_propositions_by_provability ctxt |> take max_abduce_candidates in if null abduce_candidates then (SOME failure, [], (Auto_Method (* dummy *), []), fn _ => string_of_atp_failure failure) else (NONE, [], (Auto_Method (* dummy *), []), fn _ => abduce_text ctxt abduce_candidates) end) in {outcome = outcome, used_facts = used_facts, used_from = used_from, preferred_methss = preferred_methss, run_time = run_time, message = message} end end; ¤ Dauer der Verarbeitung: 0.17 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28