author blanchet Sun, 01 May 2011 18:37:25 +0200 changeset 42577 78414ec6fa4e parent 42576 a8a80a2a34be child 42578 1eaf4d437d4c
made the format (TFF or FOF) of the TPTP problem a global argument of the problem again and have the ATPs report which formats they support
```--- a/src/HOL/Tools/ATP/atp_problem.ML	Sun May 01 18:37:25 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML	Sun May 01 18:37:25 2011 +0200
@@ -15,20 +15,21 @@
AConn of connective * ('a, 'b, 'c) formula list |
AAtom of 'c

-  datatype logic = Fof | Tff
+  datatype format = Fof | Tff
datatype formula_kind = Axiom | Definition | Lemma | Hypothesis | Conjecture
datatype 'a problem_line =
Decl of string * 'a * 'a list * 'a |
-    Formula of logic * string * formula_kind * ('a, 'a, 'a fo_term) formula
+    Formula of string * formula_kind * ('a, 'a, 'a fo_term) formula
* string fo_term option * string fo_term option
type 'a problem = (string * 'a problem_line list) list

+  val mk_anot : ('a, 'b, 'c) formula -> ('a, 'b, 'c) formula
val timestamp : unit -> string
val hashw : word * word -> word
val hashw_string : string * word -> word
val is_atp_variable : string -> bool
val tptp_strings_for_atp_problem :
-    bool -> (string * string problem_line list) list -> string list
+    formula_kind -> format -> string problem -> string list
val nice_atp_problem :
bool -> ('a * (string * string) problem_line list) list
-> ('a * string problem_line list) list
@@ -48,11 +49,13 @@
AConn of connective * ('a, 'b, 'c) formula list |
AAtom of 'c

-datatype logic = Fof | Tff
+fun mk_anot phi = AConn (ANot, [phi])
+
+datatype format = Fof | Tff
datatype formula_kind = Axiom | Definition | Lemma | Hypothesis | Conjecture
datatype 'a problem_line =
Decl of string * 'a * 'a list * 'a |
-  Formula of logic * string * formula_kind * ('a, 'a, 'a fo_term) formula
+  Formula of string * formula_kind * ('a, 'a, 'a fo_term) formula
* string fo_term option * string fo_term option
type 'a problem = (string * 'a problem_line list) list

@@ -108,19 +111,19 @@
| string_for_symbol_type arg_tys res_ty =
string_for_symbol_type ["(" ^ space_implode " * " arg_tys ^ ")"] res_ty

-fun string_for_problem_line _ (Decl (ident, sym, arg_tys, res_ty)) =
+fun string_for_problem_line _ _ (Decl (ident, sym, arg_tys, res_ty)) =
"tff(" ^ ident ^ ", type,\n    " ^ sym ^ " : " ^
string_for_symbol_type arg_tys res_ty ^ ").\n"
-  | string_for_problem_line use_conjecture_for_hypotheses
-        (Formula (logic, ident, kind, phi, source, useful_info)) =
+  | string_for_problem_line hypothesis_kind format
+                            (Formula (ident, kind, phi, source, useful_info)) =
let
val (kind, phi) =
-        if kind = Hypothesis andalso use_conjecture_for_hypotheses then
-          (Conjecture, AConn (ANot, [phi]))
+        if kind = Hypothesis then
+          (hypothesis_kind, phi |> hypothesis_kind = Conjecture ? mk_anot)
else
(kind, phi)
in
-      (case logic of Fof => "fof" | Tff => "tff") ^
+      (case format of Fof => "fof" | Tff => "tff") ^
"(" ^ ident ^ ", " ^ string_for_kind kind ^ ",\n    (" ^
string_for_formula phi ^ ")" ^
(case (source, useful_info) of
@@ -130,13 +133,13 @@
", " ^ string_for_term (source |> the_default (ATerm ("[]", []))) ^
", " ^ string_for_term tm) ^ ").\n"
end
-fun tptp_strings_for_atp_problem use_conjecture_for_hypotheses problem =
+fun tptp_strings_for_atp_problem hypothesis_kind format problem =
"% This file was generated by Isabelle (most likely Sledgehammer)\n\
\% " ^ timestamp () ^ "\n" ::
maps (fn (_, []) => []
"\n% " ^ heading ^ " (" ^ string_of_int (length lines) ^ ")\n" ::
-           map (string_for_problem_line use_conjecture_for_hypotheses) lines)
+           map (string_for_problem_line hypothesis_kind format) lines)
problem

fun is_atp_variable s = Char.isUpper (String.sub (s, 0))
@@ -221,9 +224,9 @@
##>> pool_map nice_name arg_tys
##>> nice_name res_ty
#>> (fn ((sym, arg_tys), res_ty) => Decl (ident, sym, arg_tys, res_ty))
-  | nice_problem_line (Formula (logic, ident, kind, phi, source, useful_info)) =
+  | nice_problem_line (Formula (ident, kind, phi, source, useful_info)) =
nice_formula phi
-    #>> (fn phi => Formula (logic, ident, kind, phi, source, useful_info))
+    #>> (fn phi => Formula (ident, kind, phi, source, useful_info))
fun nice_problem problem =
pool_map nice_problem_line lines #>> pair heading) problem```
```--- a/src/HOL/Tools/ATP/atp_systems.ML	Sun May 01 18:37:25 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Sun May 01 18:37:25 2011 +0200
@@ -7,6 +7,8 @@

signature ATP_SYSTEMS =
sig
+  type format = ATP_Problem.format
+  type formula_kind = ATP_Problem.formula_kind
type failure = ATP_Proof.failure

type atp_config =
@@ -16,7 +18,8 @@
slices: unit -> (real * (bool * int)) list,
proof_delims: (string * string) list,
known_failures: (failure * string) list,
-     use_conjecture_for_hypotheses: bool}
+     hypothesis_kind: formula_kind,
+     formats: format list}

datatype e_weight_method =
E_Slices | E_Auto | E_Fun_Weight | E_Sym_Offset_Weight
@@ -40,7 +43,8 @@
val remote_prefix : string
val remote_atp :
string -> string -> string list -> (string * string) list
-    -> (failure * string) list -> (unit -> int) -> bool -> string * atp_config
+    -> (failure * string) list -> (unit -> int) -> formula_kind -> format list
+    -> string * atp_config
val add_atp : string * atp_config -> theory -> theory
val get_atp : theory -> string -> atp_config
val supported_atps : theory -> string list
@@ -52,6 +56,7 @@
structure ATP_Systems : ATP_SYSTEMS =
struct

+open ATP_Problem
open ATP_Proof

(* ATP configuration *)
@@ -63,7 +68,8 @@
slices: unit -> (real * (bool * int)) list,
proof_delims: (string * string) list,
known_failures: (failure * string) list,
-   use_conjecture_for_hypotheses: bool}
+   hypothesis_kind: formula_kind,
+   formats: format list}

val known_perl_failures =
[(CantConnect, "HTTP error"),
@@ -188,7 +194,8 @@
"# Cannot determine problem status within resource limit"),
(OutOfResources, "SZS status: ResourceOut"),
(OutOfResources, "SZS status ResourceOut")],
-   use_conjecture_for_hypotheses = true}
+   hypothesis_kind = Conjecture,
+   formats = [Fof]}

val e = (eN, e_config)

@@ -216,7 +223,8 @@
(MalformedInput, "Free Variable"),
(SpassTooOld, "tptp2dfg"),
-   use_conjecture_for_hypotheses = true}
+   hypothesis_kind = Conjecture,
+   formats = [Fof]}

val spass = (spassN, spass_config)

@@ -249,7 +257,8 @@
(Unprovable, "Termination reason: Satisfiable"),
(VampireTooOld, "not a valid option"),
(Interrupted, "Aborted by signal SIGINT")],
-   use_conjecture_for_hypotheses = true}
+   hypothesis_kind = Conjecture,
+   formats = [Fof]}

val vampire = (vampireN, vampire_config)

@@ -269,7 +278,8 @@
(IncompleteUnprovable, "SZS status Satisfiable"),
(ProofMissing, "\nunsat"),
(ProofMissing, "SZS status Unsatisfiable")],
-   use_conjecture_for_hypotheses = false}
+   hypothesis_kind = Hypothesis,
+   formats = [Fof]}

val z3_atp = (z3_atpN, z3_atp_config)

@@ -307,8 +317,7 @@
val max_remote_secs = 240 (* give Geoff Sutcliffe's servers a break *)

fun remote_config system_name system_versions proof_delims known_failures
-                  default_max_relevant use_conjecture_for_hypotheses
-                  : atp_config =
+                  default_max_relevant hypothesis_kind formats : atp_config =
{exec = ("ISABELLE_ATP", "scripts/remote_atp"),
required_execs = [],
arguments = fn _ => fn timeout => fn _ =>
@@ -320,21 +329,22 @@
known_failures @ known_perl_failures @
[(IncompleteUnprovable, "says Unknown"),
(TimedOut, "says Timeout")],
-   use_conjecture_for_hypotheses = use_conjecture_for_hypotheses}
+   hypothesis_kind = hypothesis_kind,
+   formats = formats}

fun int_average f xs = fold (Integer.add o f) xs 0 div length xs

fun remotify_config system_name system_versions
-        ({proof_delims, slices, known_failures, use_conjecture_for_hypotheses,
-          ...} : atp_config) : atp_config =
+                    ({proof_delims, slices, known_failures, hypothesis_kind,
+                      formats, ...} : atp_config) : atp_config =
remote_config system_name system_versions proof_delims known_failures
-                (int_average (snd o snd) o slices) use_conjecture_for_hypotheses
+                (int_average (snd o snd) o slices) hypothesis_kind formats

fun remote_atp name system_name system_versions proof_delims known_failures
-               default_max_relevant use_conjecture_for_hypotheses =
+               default_max_relevant hypothesis_kind formats =
(remote_prefix ^ name,
remote_config system_name system_versions proof_delims known_failures
-                 default_max_relevant use_conjecture_for_hypotheses)
+                 default_max_relevant hypothesis_kind formats)
fun remotify_atp (name, config) system_name system_versions =
(remote_prefix ^ name, remotify_config system_name system_versions config)

@@ -343,12 +353,13 @@
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)
-             (K 200 (* FUDGE *)) true
+             (K 200 (* FUDGE *)) Conjecture [Tff]
val remote_sine_e =
-  remote_atp sine_eN "SInE" ["0.4"] [] [] (K 500 (* FUDGE *)) true
+  remote_atp sine_eN "SInE" ["0.4"] [] [] (K 500 (* FUDGE *)) Conjecture [Fof]
val remote_snark =
remote_atp snarkN "SNARK" ["20080805r024"]
-             [("refutation.", "end_refutation.")] [] (K 250 (* FUDGE *)) true
+             [("refutation.", "end_refutation.")] [] (K 250 (* FUDGE *))
+             Conjecture [Tff, Fof]

(* Setup *)
```
```--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Sun May 01 18:37:25 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Sun May 01 18:37:25 2011 +0200
@@ -156,7 +156,6 @@
|> filter (fn TyLitVar _ => kind <> Conjecture
| TyLitFree _ => kind = Conjecture)

-fun mk_anot phi = AConn (ANot, [phi])
fun mk_aconn c phi1 phi2 = AConn (c, [phi1, phi2])
fun mk_aconns c phis =
let val (phis', phi') = split_last phis in
@@ -532,7 +531,7 @@
fun var s = ATerm (`I s, [])
fun tag tm = ATerm (`I type_tag_name, [var "X", tm])
in
-    Formula (Fof, helper_prefix ^ ascii_of "ti_ti", Axiom,
+    Formula (helper_prefix ^ ascii_of "ti_ti", Axiom,
AAtom (ATerm (`I "equal", [tag (tag (var "Y")), tag (var "Y")]))
|> close_formula_universally, NONE, NONE)
end
@@ -690,22 +689,18 @@
(close_combformula_universally combformula))
|> close_formula_universally

-fun logic_for_type_sys Many_Typed = Tff
-  | logic_for_type_sys _ = Fof
-
(* Each fact is given a unique fact number to avoid name clashes (e.g., because
of monomorphization). The TPTP explicitly forbids name clashes, and some of
the remote provers might care. *)
fun formula_line_for_fact ctxt prefix type_sys
(j, formula as {name, kind, ...}) =
-  Formula (logic_for_type_sys type_sys,
-           prefix ^ string_of_int j ^ "_" ^ ascii_of name, kind,
+  Formula (prefix ^ string_of_int j ^ "_" ^ ascii_of name, kind,
formula_for_fact ctxt type_sys formula, NONE, NONE)

fun formula_line_for_class_rel_clause (ClassRelClause {name, subclass,
superclass, ...}) =
let val ty_arg = ATerm (`I "T", []) in
-    Formula (Fof, class_rel_clause_prefix ^ ascii_of name, Axiom,
+    Formula (class_rel_clause_prefix ^ ascii_of name, Axiom,
AConn (AImplies, [AAtom (ATerm (subclass, [ty_arg])),
AAtom (ATerm (superclass, [ty_arg]))])
|> close_formula_universally, NONE, NONE)
@@ -718,7 +713,7 @@

fun formula_line_for_arity_clause (ArityClause {name, conclLit, premLits,
...}) =
-  Formula (Fof, arity_clause_prefix ^ ascii_of name, Axiom,
+  Formula (arity_clause_prefix ^ ascii_of name, Axiom,
mk_ahorn (map (formula_from_fo_literal o apfst not
o fo_literal_from_arity_literal) premLits)
(formula_from_fo_literal
@@ -727,7 +722,7 @@

fun formula_line_for_conjecture ctxt type_sys
({name, kind, combformula, ...} : translated_formula) =
-  Formula (logic_for_type_sys type_sys, conjecture_prefix ^ name, kind,
+  Formula (conjecture_prefix ^ name, kind,
formula_from_combformula ctxt type_sys
(close_combformula_universally combformula)
|> close_formula_universally, NONE, NONE)
@@ -737,7 +732,7 @@
|> map fo_literal_from_type_literal

fun formula_line_for_free_type j lit =
-  Formula (Fof, tfree_prefix ^ string_of_int j, Hypothesis,
+  Formula (tfree_prefix ^ string_of_int j, Hypothesis,
formula_from_fo_literal lit, NONE, NONE)
fun formula_lines_for_free_types type_sys facts =
let
@@ -803,7 +798,7 @@
val freshener =
case type_sys of Args _ => string_of_int j ^ "_" | _ => ""
in
-      Formula (Fof, sym_decl_prefix ^ freshener ^ "_" ^ ascii_of s, Axiom,
+      Formula (sym_decl_prefix ^ freshener ^ "_" ^ ascii_of s, Axiom,
CombConst ((s, s'), T, T_args)
|> fold (curry (CombApp o swap)) bound_tms
|> type_pred_combatom type_sys res_T
@@ -837,7 +832,7 @@

fun add_tff_types_in_problem_line (Decl (_, _, arg_Ts, res_T)) =
union (op =) (res_T :: arg_Ts)
-  | add_tff_types_in_problem_line (Formula (_, _, _, phi, _, _)) =
+  | add_tff_types_in_problem_line (Formula (_, _, phi, _, _)) =

fun tff_types_in_problem problem =
@@ -914,7 +909,7 @@
fun add_term_weights weight (ATerm (s, tms)) =
(not (is_atp_variable s) andalso s <> "equal") ? Symtab.default (s, weight)
-fun add_problem_line_weights weight (Formula (_, _, _, phi, _, _)) =
+fun add_problem_line_weights weight (Formula (_, _, phi, _, _)) =
| add_problem_line_weights _ _ = I
```
```--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Sun May 01 18:37:25 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Sun May 01 18:37:25 2011 +0200
@@ -340,7 +340,7 @@

fun run_atp auto name
({exec, required_execs, arguments, slices, proof_delims, known_failures,
-          use_conjecture_for_hypotheses, ...} : atp_config)
+          hypothesis_kind, ...} : atp_config)
({debug, verbose, overlord, type_sys, max_relevant, monomorphize,
monomorphize_limit, explicit_apply, isar_proof, isar_shrink_factor,
slicing, timeout, ...} : params)
@@ -348,6 +348,7 @@
let
val thy = Proof.theory_of state
val ctxt = Proof.context_of state
+    val format = if type_sys = Many_Typed then Tff else Fof
val (_, hyp_ts, concl_t) = strip_subgoal goal subgoal
val (dest_dir, problem_prefix) =
if overlord then overlord_file_location_for_prover name
@@ -452,7 +453,7 @@
"exec " ^ core) ^ " 2>&1"
val _ =
atp_problem
-                  |> tptp_strings_for_atp_problem use_conjecture_for_hypotheses
+                  |> tptp_strings_for_atp_problem hypothesis_kind format
|> cons ("% " ^ command ^ "\n")
|> File.write_list prob_file
val conjecture_shape =```