# HG changeset patch # User blanchet # Date 1314103459 -7200 # Node ID cabd06b69c1813e342ebdab48810d9b486e18e58 # Parent ce6cd1b2344b1931e3d0d555a119153bf7dbbca1 added formats to the slice and use TFF for remote Vampire diff -r ce6cd1b2344b -r cabd06b69c18 src/HOL/Tools/ATP/atp_systems.ML --- a/src/HOL/Tools/ATP/atp_systems.ML Tue Aug 23 07:14:09 2011 +0200 +++ b/src/HOL/Tools/ATP/atp_systems.ML Tue Aug 23 14:44:19 2011 +0200 @@ -21,9 +21,8 @@ known_failures : (failure * string) list, conj_sym_kind : formula_kind, prem_kind : formula_kind, - formats : format list, best_slices : - Proof.context -> (real * (bool * (int * string * string))) list} + Proof.context -> (real * (bool * (int * format * string * string))) list} val force_sos : bool Config.T val e_smartN : string @@ -50,8 +49,8 @@ val remote_prefix : string val remote_atp : string -> string -> string list -> (string * string) list - -> (failure * string) list -> formula_kind -> formula_kind -> format list - -> (Proof.context -> int * string) -> string * atp_config + -> (failure * string) list -> formula_kind -> formula_kind + -> (Proof.context -> int * format * string) -> string * atp_config val add_atp : string * atp_config -> theory -> theory val get_atp : theory -> string -> atp_config val supported_atps : theory -> string list @@ -78,9 +77,8 @@ known_failures : (failure * string) list, conj_sym_kind : formula_kind, prem_kind : formula_kind, - formats : format list, best_slices : - Proof.context -> (real * (bool * (int * string * string))) list} + Proof.context -> (real * (bool * (int * format * string * string))) list} (* "best_slices" must be found empirically, taking a wholistic approach since the ATPs are run in parallel. The "real" components give the faction of the @@ -214,16 +212,15 @@ (OutOfResources, "SZS status ResourceOut")], conj_sym_kind = Hypothesis, prem_kind = Conjecture, - formats = [FOF], best_slices = fn ctxt => let val method = effective_e_weight_method ctxt in (* FUDGE *) if method = e_smartN then - [(0.333, (true, (500, "mangled_tags?", e_fun_weightN))), - (0.334, (true, (50, "mangled_guards?", e_fun_weightN))), - (0.333, (true, (1000, "mangled_tags?", e_sym_offset_weightN)))] + [(0.333, (true, (500, FOF, "mangled_tags?", e_fun_weightN))), + (0.334, (true, (50, FOF, "mangled_guards?", e_fun_weightN))), + (0.333, (true, (1000, FOF, "mangled_tags?", e_sym_offset_weightN)))] else - [(1.0, (true, (500, "mangled_tags?", method)))] + [(1.0, (true, (500, FOF, "mangled_tags?", method)))] end} val e = (eN, e_config) @@ -242,11 +239,10 @@ known_failures = [], conj_sym_kind = Axiom, prem_kind = Hypothesis, - formats = [THF Without_Choice, FOF], best_slices = fn ctxt => (* FUDGE *) - [(0.667, (false, (150, "simple_higher", sosN))), - (0.333, (true, (50, "simple_higher", no_sosN)))] + [(0.667, (false, (150, THF Without_Choice, "simple_higher", sosN))), + (0.333, (true, (50, THF Without_Choice, "simple_higher", no_sosN)))] |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single else I)} @@ -265,8 +261,8 @@ known_failures = [(ProofMissing, "SZS status Theorem")], conj_sym_kind = Axiom, prem_kind = Hypothesis, - formats = [THF With_Choice], - best_slices = K [(1.0, (true, (100, "simple_higher", "")))] (* FUDGE *)} + best_slices = + K [(1.0, (true, (100, THF With_Choice, "simple_higher", "")))] (* FUDGE *)} val satallax = (satallaxN, satallax_config) @@ -295,12 +291,11 @@ (InternalError, "Please report this error")], conj_sym_kind = Hypothesis, prem_kind = Conjecture, - formats = [FOF], best_slices = fn ctxt => (* FUDGE *) - [(0.333, (false, (150, "mangled_tags", sosN))), - (0.333, (false, (300, "poly_tags?", sosN))), - (0.334, (true, (50, "mangled_tags?", no_sosN)))] + [(0.333, (false, (150, FOF, "mangled_tags", sosN))), + (0.333, (false, (300, FOF, "poly_tags?", sosN))), + (0.334, (true, (50, FOF, "mangled_tags?", no_sosN)))] |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single else I)} @@ -333,12 +328,11 @@ (Interrupted, "Aborted by signal SIGINT")], conj_sym_kind = Conjecture, prem_kind = Conjecture, - formats = [FOF], best_slices = fn ctxt => (* FUDGE *) - [(0.333, (false, (150, "poly_guards", sosN))), - (0.334, (true, (50, "mangled_guards?", no_sosN))), - (0.333, (false, (500, "mangled_tags?", sosN)))] + [(0.333, (false, (150, TFF, "poly_guards", sosN))), + (0.334, (true, (50, TFF, "mangled_guards?", no_sosN))), + (0.333, (false, (500, TFF, "mangled_tags?", sosN)))] |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single else I)} @@ -361,13 +355,12 @@ (ProofMissing, "SZS status Unsatisfiable")], conj_sym_kind = Hypothesis, prem_kind = Hypothesis, - formats = [FOF], best_slices = (* FUDGE (FIXME) *) - K [(0.5, (false, (250, "mangled_guards?", ""))), - (0.25, (false, (125, "mangled_guards?", ""))), - (0.125, (false, (62, "mangled_guards?", ""))), - (0.125, (false, (31, "mangled_guards?", "")))]} + K [(0.5, (false, (250, FOF, "mangled_guards?", ""))), + (0.25, (false, (125, FOF, "mangled_guards?", ""))), + (0.125, (false, (62, FOF, "mangled_guards?", ""))), + (0.125, (false, (31, FOF, "mangled_guards?", "")))]} val z3_atp = (z3_atpN, z3_atp_config) @@ -407,7 +400,7 @@ val max_remote_secs = 240 (* give Geoff Sutcliffe's servers a break *) fun remote_config system_name system_versions proof_delims known_failures - conj_sym_kind prem_kind formats best_slice : atp_config = + conj_sym_kind prem_kind best_slice : atp_config = {exec = ("ISABELLE_ATP", "scripts/remote_atp"), required_execs = [], arguments = fn _ => fn _ => fn _ => fn timeout => fn _ => @@ -425,58 +418,58 @@ (Inappropriate, "says Inappropriate")], conj_sym_kind = conj_sym_kind, prem_kind = prem_kind, - formats = formats, best_slices = fn ctxt => - let val (max_relevant, type_enc) = best_slice ctxt in - [(1.0, (false, (max_relevant, type_enc, "")))] + let val (max_relevant, format, type_enc) = best_slice ctxt in + [(1.0, (false, (max_relevant, format, type_enc, "")))] end} fun remotify_config system_name system_versions best_slice - ({proof_delims, known_failures, conj_sym_kind, prem_kind, formats, ...} + ({proof_delims, known_failures, conj_sym_kind, prem_kind, ...} : atp_config) : atp_config = remote_config system_name system_versions proof_delims known_failures - conj_sym_kind prem_kind formats best_slice + conj_sym_kind prem_kind best_slice fun remote_atp name system_name system_versions proof_delims known_failures - conj_sym_kind prem_kind formats best_slice = + conj_sym_kind prem_kind best_slice = (remote_prefix ^ name, remote_config system_name system_versions proof_delims known_failures - conj_sym_kind prem_kind formats best_slice) + conj_sym_kind prem_kind best_slice) fun remotify_atp (name, config) system_name system_versions best_slice = (remote_prefix ^ name, remotify_config system_name system_versions best_slice config) val remote_e = remotify_atp e "EP" ["1.0", "1.1", "1.2"] - (K (750, "mangled_tags?") (* FUDGE *)) + (K (750, FOF, "mangled_tags?") (* FUDGE *)) val remote_leo2 = remotify_atp leo2 "LEO-II" ["1.2.8", "1.2.6"] - (K (100, "simple_higher") (* FUDGE *)) + (K (100, THF Without_Choice, "simple_higher") (* FUDGE *)) val remote_satallax = remotify_atp satallax "Satallax" ["2.1", "2.0", "2"] - (K (100, "simple_higher") (* FUDGE *)) + (K (100, THF With_Choice, "simple_higher") (* FUDGE *)) val remote_vampire = - remotify_atp vampire "Vampire" ["0.6", "9.0", "1.0"] - (K (200, "mangled_guards?") (* FUDGE *)) + remotify_atp vampire "Vampire" ["1.8"] + (K (200, TFF, "mangled_guards?") (* FUDGE *)) val remote_z3_atp = - remotify_atp z3_atp "Z3" ["2.18"] (K (250, "mangled_guards?") (* FUDGE *)) + remotify_atp z3_atp "Z3" ["2.18"] + (K (250, FOF, "mangled_guards?") (* FUDGE *)) val remote_e_sine = remote_atp e_sineN "SInE" ["0.4"] [] (#known_failures e_config) Axiom - Conjecture [FOF] (K (500, "mangled_guards?") (* FUDGE *)) + Conjecture (K (500, FOF, "mangled_guards?") (* FUDGE *)) val remote_snark = remote_atp snarkN "SNARK" ["20080805r029", "20080805r024"] [("refutation.", "end_refutation.")] [] Hypothesis Hypothesis - [TFF, FOF] (K (100, "simple") (* FUDGE *)) + (K (100, TFF, "simple") (* FUDGE *)) val remote_e_tofof = remote_atp e_tofofN "ToFoF" ["0.1"] [] (#known_failures e_config) - Axiom Hypothesis [TFF] (K (150, "simple") (* FUDGE *)) + Axiom Hypothesis (K (150, TFF, "simple") (* FUDGE *)) val remote_waldmeister = remote_atp waldmeisterN "Waldmeister" ["710"] [("#START OF PROOF", "Proved Goals:")] [(OutOfResources, "Too many function symbols"), (Crashed, "Unrecoverable Segmentation Fault")] - Hypothesis Hypothesis [CNF_UEQ] - (K (50, "mangled_tags?") (* FUDGE *)) + Hypothesis Hypothesis + (K (50, CNF_UEQ, "mangled_tags?") (* FUDGE *)) (* Setup *) diff -r ce6cd1b2344b -r cabd06b69c18 src/HOL/Tools/ATP/atp_translate.ML --- a/src/HOL/Tools/ATP/atp_translate.ML Tue Aug 23 07:14:09 2011 +0200 +++ b/src/HOL/Tools/ATP/atp_translate.ML Tue Aug 23 14:44:19 2011 +0200 @@ -90,7 +90,7 @@ val level_of_type_enc : type_enc -> type_level val is_type_enc_quasi_sound : type_enc -> bool val is_type_enc_fairly_sound : type_enc -> bool - val choose_format : format list -> type_enc -> format * type_enc + val adjust_type_enc : format -> type_enc -> type_enc val mk_aconns : connective -> ('a, 'b, 'c) formula list -> ('a, 'b, 'c) formula val unmangled_const : string -> string * (string, 'b) ho_term list @@ -611,23 +611,14 @@ | is_type_level_monotonicity_based Fin_Nonmono_Types = true | is_type_level_monotonicity_based _ = false -fun choose_format formats (Simple_Types (order, level)) = - (case find_first is_format_thf formats of - SOME format => (format, Simple_Types (order, level)) - | NONE => - if member (op =) formats TFF then - (TFF, Simple_Types (First_Order, level)) - else - choose_format formats (Guards (Mangled_Monomorphic, level, Uniform))) - | choose_format formats type_enc = - (case hd formats of - CNF_UEQ => - (CNF_UEQ, case type_enc of - Guards stuff => - (if is_type_enc_fairly_sound type_enc then Tags else Guards) - stuff - | _ => type_enc) - | format => (format, type_enc)) +fun adjust_type_enc (THF _) type_enc = type_enc + | adjust_type_enc TFF (Simple_Types (Higher_Order, level)) = + Simple_Types (First_Order, level) + | adjust_type_enc format (Simple_Types (_, level)) = + adjust_type_enc format (Guards (Mangled_Monomorphic, level, Uniform)) + | adjust_type_enc CNF_UEQ (type_enc as Guards stuff) = + (if is_type_enc_fairly_sound type_enc then Tags else Guards) stuff + | adjust_type_enc _ type_enc = type_enc fun lift_lambdas ctxt type_enc = map (close_form o Envir.eta_contract) #> rpair ctxt @@ -2087,7 +2078,7 @@ fun prepare_atp_problem ctxt format conj_sym_kind prem_kind type_enc exporter lambda_trans readable_names preproc hyp_ts concl_t facts = let - val (format, type_enc) = choose_format [format] type_enc + val type_enc = type_enc |> adjust_type_enc format val lambda_trans = if lambda_trans = smartN then if is_type_enc_higher_order type_enc then lambdasN else combinatorsN diff -r ce6cd1b2344b -r cabd06b69c18 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Tue Aug 23 07:14:09 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Tue Aug 23 14:44:19 2011 +0200 @@ -154,7 +154,9 @@ fun is_unit_equational_atp ctxt name = let val thy = Proof_Context.theory_of ctxt in case try (get_atp thy) name of - SOME {formats, ...} => member (op =) formats CNF_UEQ + SOME {best_slices, ...} => + exists (fn (_, (_, (_, format, _, _))) => format = CNF_UEQ) + (best_slices ctxt) | NONE => false end @@ -512,10 +514,10 @@ them each time. *) val atp_important_message_keep_quotient = 10 -fun choose_format_and_type_enc soundness best_type_enc formats = +fun choose_type_enc soundness best_type_enc format = the_default best_type_enc #> type_enc_from_string soundness - #> choose_format formats + #> adjust_type_enc format val metis_minimize_max_time = seconds 2.0 @@ -540,7 +542,7 @@ fun run_atp mode name ({exec, required_execs, arguments, proof_delims, known_failures, - conj_sym_kind, prem_kind, formats, best_slices, ...} : atp_config) + conj_sym_kind, prem_kind, best_slices, ...} : atp_config) ({debug, verbose, overlord, type_enc, sound, max_relevant, max_mono_iters, max_new_mono_instances, isar_proof, isar_shrink_factor, slicing, timeout, preplay_timeout, ...} : params) @@ -609,7 +611,8 @@ |> maps (fn (name, rths) => map (pair name o snd) rths) end fun run_slice (slice, (time_frac, (complete, - (best_max_relevant, best_type_enc, extra)))) + (best_max_relevant, format, best_type_enc, + extra)))) time_left = let val num_facts = @@ -623,9 +626,8 @@ Sound else Unsound - val (format, type_enc) = - choose_format_and_type_enc soundness best_type_enc formats - type_enc + val type_enc = + type_enc |> choose_type_enc soundness best_type_enc format val fairly_sound = is_type_enc_fairly_sound type_enc val facts = facts |> map untranslated_fact