# HG changeset patch # User blanchet # Date 1306068575 -7200 # Node ID cabb3a9478942b2310a6e992020f5bc31a73253f # Parent 7438ee56b89a43a05ad3427fac3589df3d6d4b65 reorganized ATP formats a little bit diff -r 7438ee56b89a -r cabb3a947894 src/HOL/Tools/ATP/atp_problem.ML --- a/src/HOL/Tools/ATP/atp_problem.ML Sat May 21 11:31:59 2011 +0200 +++ b/src/HOL/Tools/ATP/atp_problem.ML Sun May 22 14:49:35 2011 +0200 @@ -15,7 +15,7 @@ AConn of connective * ('a, 'b, 'c) formula list | AAtom of 'c - datatype format = Fof | Tff + datatype format = UEQ | FOF | TFF datatype formula_kind = Axiom | Definition | Lemma | Hypothesis | Conjecture datatype 'a problem_line = Decl of string * 'a * 'a list * 'a | @@ -54,7 +54,7 @@ AConn of connective * ('a, 'b, 'c) formula list | AAtom of 'c -datatype format = Fof | Tff +datatype format = UEQ | FOF | TFF datatype formula_kind = Axiom | Definition | Lemma | Hypothesis | Conjecture datatype 'a problem_line = Decl of string * 'a * 'a list * 'a | @@ -102,9 +102,9 @@ | string_for_connective AIf = "<=" | string_for_connective AIff = "<=>" | string_for_connective ANotIff = "<~>" -fun string_for_bound_var Fof (s, _) = s - | string_for_bound_var Tff (s, ty) = +fun string_for_bound_var TFF (s, ty) = s ^ " : " ^ (ty |> the_default tptp_tff_individual_type) + | string_for_bound_var _ (s, _) = s fun string_for_formula format (AQuant (q, xs, phi)) = "(" ^ string_for_quantifier q ^ "[" ^ commas (map (string_for_bound_var format) xs) ^ "] : " ^ @@ -131,7 +131,7 @@ string_for_symbol_type arg_tys res_ty ^ ").\n" | string_for_problem_line format (Formula (ident, kind, phi, source, useful_info)) = - (case format of Fof => "fof" | Tff => "tff") ^ + (case format of UEQ => "cnf" | FOF => "fof" | TFF => "tff") ^ "(" ^ ident ^ ", " ^ string_for_kind kind ^ ",\n (" ^ string_for_formula format phi ^ ")" ^ (case (source, useful_info) of diff -r 7438ee56b89a -r cabb3a947894 src/HOL/Tools/ATP/atp_systems.ML --- a/src/HOL/Tools/ATP/atp_systems.ML Sat May 21 11:31:59 2011 +0200 +++ b/src/HOL/Tools/ATP/atp_systems.ML Sun May 22 14:49:35 2011 +0200 @@ -218,7 +218,7 @@ (OutOfResources, "SZS status ResourceOut")], conj_sym_kind = Conjecture, (* FIXME: try out Hypothesis *) prem_kind = Conjecture, - formats = [Fof], + formats = [FOF], best_slices = fn ctxt => (* FUDGE *) if effective_e_weight_method ctxt = e_slicesN then @@ -258,7 +258,7 @@ (InternalError, "Please report this error")], conj_sym_kind = Axiom, (* FIXME: try out Hypothesis *) prem_kind = Conjecture, - formats = [Fof], + formats = [FOF], best_slices = fn ctxt => (* FUDGE *) [(0.333, (false, (150, ["mangled_preds_heavy"]))) (* SOS *), @@ -300,7 +300,7 @@ (Interrupted, "Aborted by signal SIGINT")], conj_sym_kind = Conjecture, (* FIXME: try out Hypothesis *) prem_kind = Conjecture, - formats = [Fof], + formats = [FOF], best_slices = fn ctxt => (* FUDGE *) [(0.333, (false, (400, ["mangled_preds_heavy"]))) (* SOS *), @@ -328,7 +328,7 @@ (ProofMissing, "SZS status Unsatisfiable")], conj_sym_kind = Hypothesis, prem_kind = Hypothesis, - formats = [Fof], + formats = [FOF], best_slices = (* FUDGE (FIXME) *) K [(1.0, (false, (250, [])))]} @@ -406,14 +406,14 @@ val remote_z3_atp = remotify_atp z3_atp "Z3" ["2.18"] val remote_tofof_e = remote_atp tofof_eN "ToFoF" ["0.1"] [] (#known_failures e_config) - Axiom Conjecture [Tff] (K (200, ["simple"]) (* FUDGE *)) + Axiom Conjecture [TFF] (K (200, ["simple"]) (* FUDGE *)) val remote_sine_e = - remote_atp sine_eN "SInE" ["0.4"] [] [] Axiom Conjecture [Fof] + remote_atp sine_eN "SInE" ["0.4"] [] [] Axiom Conjecture [FOF] (K (500, ["poly_tags_heavy!", "poly_tags_heavy"]) (* FUDGE *)) val remote_snark = remote_atp snarkN "SNARK" ["20080805r024"] [("refutation.", "end_refutation.")] [] Hypothesis Conjecture - [Tff, Fof] (K (250, ["simple"]) (* FUDGE *)) + [TFF, FOF] (K (250, ["simple"]) (* FUDGE *)) (* Setup *) diff -r 7438ee56b89a -r cabb3a947894 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Sat May 21 11:31:59 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Sun May 22 14:49:35 2011 +0200 @@ -407,14 +407,14 @@ [Preds (Mangled_Monomorphic, Nonmonotonic_Types, Light)] fun adjust_dumb_type_sys formats (Simple_Types level) = - if member (op =) formats Tff then (Tff, Simple_Types level) - else (Fof, Preds (Mangled_Monomorphic, level, Heavy)) + if member (op =) formats TFF then (TFF, Simple_Types level) + else (FOF, Preds (Mangled_Monomorphic, level, Heavy)) | adjust_dumb_type_sys formats type_sys = - (* We could return (Tff, type_sys) in all cases but this would require the + (* We could return (TFF, type_sys) in all cases but this would require the TFF provers to accept problems in which constants are implicitly declared. Today neither SNARK nor ToFoF-E satisfy this criterion. *) - if member (op =) formats Fof then (Fof, type_sys) - else (Tff, Simple_Types All_Types) + if member (op =) formats FOF then (FOF, type_sys) + else (TFF, Simple_Types All_Types) fun determine_format_and_type_sys _ formats (Dumb_Type_Sys type_sys) = adjust_dumb_type_sys formats type_sys | determine_format_and_type_sys best_type_systems formats diff -r 7438ee56b89a -r cabb3a947894 src/HOL/ex/tptp_export.ML --- a/src/HOL/ex/tptp_export.ML Sat May 21 11:31:59 2011 +0200 +++ b/src/HOL/ex/tptp_export.ML Sun May 22 14:49:35 2011 +0200 @@ -114,7 +114,7 @@ infers |> map (apsnd (filter (member (op = o apsnd fst) infers))) val atp_problem = atp_problem |> add_inferences_to_problem infers val ss = - ATP_Problem.tptp_strings_for_atp_problem ATP_Problem.Fof atp_problem + ATP_Problem.tptp_strings_for_atp_problem ATP_Problem.FOF atp_problem val _ = app (File.append path) ss in () end