(* 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> (K "")
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 "prob")
val atp_completish = Attrib.setup_config_int \<^binding>\<open>sledgehammer_atp_completish\<close> (K 0)
(* In addition to being easier to read, readable names are often much shorter, especially if types
are mangled in names. This makes a difference for some provers (e.g., E). For these reason, short
names are enabled by default. *)
val atp_full_names = Attrib.setup_config_bool \<^binding>\<open>sledgehammer_atp_full_names\<close> (K false)
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 properly
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 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, timeout,
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 f = fn _ =>
if exec = isabelle_scala_function then
let val {output, ...} = SystemOnTPTP.run_system_encoded args
in output end
else
let val res = Isabelle_System.bash_process (Bash.script command |> Bash.redirect)
in Process_Result.out res end
(* 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_candidates,
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 =>
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 one_line_params = (preplay (), 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;