--- 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
--- 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 *)
--- 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
--- 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