wneuper/isa: comparison src/HOL/Tools/ATP/atp

equal deleted inserted replaced

-:3e4889375781
+:b342cd125533
 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 list * string))) list}
+Proof.context -> (real * (bool * (int * string * string))) list}
 val e_smartN : string
 val e_autoN : string
 val e_fun_weightN : string
 val e_sym_offset_weightN : string
 val z3_atpN : string
 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 list) -> string * atp_config
+-> (Proof.context -> int * 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
 val is_atp_installed : theory -> string -> bool
 val refresh_systems_on_tptp : unit -> unit
 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 list * string))) list}
+Proof.context -> (real * (bool * (int * 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
-time available given to the slice; these should add up to 1.0. The "bool"
+time available given to the slice and should add up to 1.0. The "bool"
 component indicates whether the slice's strategy is complete; the "int", the
-preferred number of facts to pass; the "string list", the preferred type
+preferred number of facts to pass; the first "string", the preferred type
-systems, which should be of the form [sound] or [unsound, sound], where
+system; the second "string", extra information to the prover (e.g., SOS or no
-"sound" is a sound type system and "unsound" is an unsound one.
+SOS).
 The last slice should be the most "normal" one, because it will get all the
-time available if the other slices fail early and also because it is used for
+time available if the other slices fail early and also because it is used if
-remote provers and if slicing is disabled. *)
+slicing is disabled (e.g., by the minimizer). *)
 val known_perl_failures =
 [(CantConnect, "HTTP error"),
 (NoPerl, "env: perl"),
 (NoLibwwwPerl, "Can't locate HTTP")]
 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.333, (true, (500, "mangled_tags?", e_fun_weightN))),
-(0.334, (true, (50, ["mangled_preds?"], e_fun_weightN))),
+(0.334, (true, (50, "mangled_preds?", e_fun_weightN))),
-(0.333, (true, (1000, ["mangled_tags?"], e_sym_offset_weightN)))]
+(0.333, (true, (1000, "mangled_tags?", e_sym_offset_weightN)))]
 else
-[(1.0, (true, (500, ["mangled_tags?"], method)))]
+[(1.0, (true, (500, "mangled_tags?", method)))]
 end}
 val e = (eN, e_config)
 (* The "-VarWeight=3" option helps the higher-order problems, probably by
 counteracting the presence of "hAPP". *)
 val spass_config : atp_config =
 {exec = ("ISABELLE_ATP", "scripts/spass"),
 required_execs = [("SPASS_HOME", "SPASS"), ("SPASS_HOME", "tptp2dfg")],
-arguments = fn ctxt => fn _ => fn sos => fn timeout => fn _ =>
+arguments = fn _ => fn _ => fn sos => fn timeout => fn _ =>
 ("-Auto -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof \
 \-VarWeight=3 -TimeLimit=" ^ string_of_int (to_secs timeout))
 |> sos = sosN ? prefix "-SOS=1 ",
 proof_delims = [("Here is a proof", "Formulae used in the proof")],
 known_failures =
 conj_sym_kind = Hypothesis,
 prem_kind = Conjecture,
 formats = [FOF],
 best_slices = fn ctxt =>
 (* FUDGE *)
-[(0.333, (false, (150, ["mangled_tags"], sosN))),
+[(0.333, (false, (150, "mangled_tags", sosN))),
-(0.333, (false, (300, ["poly_tags?"], sosN))),
+(0.333, (false, (300, "poly_tags?", sosN))),
-(0.334, (true, (50, ["mangled_tags?"], no_sosN)))]
+(0.334, (true, (50, "mangled_tags?", no_sosN)))]
 |> (if Config.get ctxt spass_force_sos then hd #> apfst (K 1.0) #> single
 else I)}
 val spass = (spassN, spass_config)
 Attrib.setup_config_bool @{binding atp_vampire_force_sos} (K false)
 val vampire_config : atp_config =
 {exec = ("VAMPIRE_HOME", "vampire"),
 required_execs = [],
-arguments = fn ctxt => fn _ => fn sos => fn timeout => fn _ =>
+arguments = fn _ => fn _ => fn sos => fn timeout => fn _ =>
 "--proof tptp --mode casc -t " ^ string_of_int (to_secs timeout) ^
 " --thanks \"Andrei and Krystof\" --input_file"
 |> sos = sosN ? prefix "--sos on ",
 proof_delims =
 [("=========== Refutation ==========",
 conj_sym_kind = Conjecture,
 prem_kind = Conjecture,
 formats = [FOF],
 best_slices = fn ctxt =>
 (* FUDGE *)
-[(0.333, (false, (150, ["poly_preds"], sosN))),
+[(0.333, (false, (150, "poly_preds", sosN))),
-(0.334, (true, (50, ["mangled_preds?"], no_sosN))),
+(0.334, (true, (50, "mangled_preds?", no_sosN))),
-(0.333, (false, (500, ["mangled_tags?"], sosN)))]
+(0.333, (false, (500, "mangled_tags?", sosN)))]
 |> (if Config.get ctxt vampire_force_sos then hd #> apfst (K 1.0) #> single
 else I)}
 val vampire = (vampireN, vampire_config)
 conj_sym_kind = Hypothesis,
 prem_kind = Hypothesis,
 formats = [FOF],
 best_slices =
 (* FUDGE (FIXME) *)
-K [(1.0, (false, (250, [], "")))]}
+K [(1.0, (false, (250, "mangled_preds?", "")))]}
 val z3_atp = (z3_atpN, z3_atp_config)
 (* Remote ATP invocation via SystemOnTPTP *)
 (Inappropriate, "says Inappropriate")],
 conj_sym_kind = conj_sym_kind,
 prem_kind = prem_kind,
 formats = formats,
 best_slices = fn ctxt =>
-let val (max_relevant, type_syss) = best_slice ctxt in
+let val (max_relevant, type_sys) = best_slice ctxt in
-[(1.0, (false, (max_relevant, type_syss, "")))]
+[(1.0, (false, (max_relevant, type_sys, "")))]
 end}
 fun remotify_config system_name system_versions best_slice
 ({proof_delims, known_failures, conj_sym_kind, prem_kind, formats, ...}
 : atp_config) : atp_config =
 (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, "mangled_tags?") (* FUDGE *))
 val remote_vampire =
 remotify_atp vampire "Vampire" ["0.6", "9.0", "1.0"]
-(K (200, ["mangled_preds?"]) (* FUDGE *))
+(K (200, "mangled_preds?") (* FUDGE *))
 val remote_z3_atp =
-remotify_atp z3_atp "Z3" ["2.18"] (K (250, ["mangled_preds?"]) (* FUDGE *))
+remotify_atp z3_atp "Z3" ["2.18"] (K (250, "mangled_preds?") (* FUDGE *))
 val remote_leo2 =
 remote_atp leo2N "LEO-II" ["1.2.6"] [] [] Axiom Hypothesis [THF]
-(K (100, ["simple"]) (* FUDGE *))
+(K (100, "simple") (* FUDGE *))
 val remote_satallax =
 remote_atp satallaxN "Satallax" ["2.0"] [] [] Axiom Hypothesis [THF]
-(K (64, ["simple"]) (* FUDGE *))
+(K (64, "simple") (* FUDGE *))
 val remote_sine_e =
-remote_atp sine_eN "SInE" ["0.4"] [] (#known_failures e_config)
+remote_atp sine_eN "SInE" ["0.4"] [] (#known_failures e_config) Axiom
-Axiom Conjecture [FOF]
+Conjecture [FOF] (K (500, "mangled_preds?") (* FUDGE *))
-(K (500, ["mangled_preds?"]) (* FUDGE *))
 val remote_snark =
 remote_atp snarkN "SNARK" ["20080805r029", "20080805r024"]
 [("refutation.", "end_refutation.")] [] Hypothesis Hypothesis
-[TFF, FOF] (K (100, ["simple"]) (* FUDGE *))
+[TFF, FOF] (K (100, "simple") (* FUDGE *))
 val remote_tofof_e =
 remote_atp tofof_eN "ToFoF" ["0.1"] [] (#known_failures e_config)
-Axiom Hypothesis [TFF] (K (150, ["simple"]) (* FUDGE *))
+Axiom Hypothesis [TFF] (K (150, "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 *))
+(K (50, "mangled_tags?") (* FUDGE *))
 (* Setup *)
 fun add_atp (name, config) thy =
 Data.map (Symtab.update_new (name, (config, stamp ()))) thy

changeset 44431	b342cd125533
parent 44429	dda3e38cc351
child 44437	cfb2077cb2db