allow each prover to specify its own formula kind for symbols occurring in the conjecture
--- a/src/HOL/Tools/ATP/atp_problem.ML Fri May 06 13:34:59 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML Fri May 06 13:34:59 2011 +0200
@@ -23,13 +23,11 @@
* 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 :
- formula_kind -> format -> string problem -> string list
+ val tptp_strings_for_atp_problem : format -> string problem -> string list
val nice_atp_problem :
bool -> ('a * (string * string) problem_line list) list
-> ('a * string problem_line list) list
@@ -49,8 +47,6 @@
AConn of connective * ('a, 'b, 'c) formula list |
AAtom of 'c
-fun mk_anot phi = AConn (ANot, [phi])
-
datatype format = Fof | Tff
datatype formula_kind = Axiom | Definition | Lemma | Hypothesis | Conjecture
datatype 'a problem_line =
@@ -114,35 +110,27 @@
val default_source =
ATerm ("inference", ATerm ("isabelle", []) :: replicate 2 (ATerm ("[]", [])))
-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 hypothesis_kind format
+ | string_for_problem_line format
(Formula (ident, kind, phi, source, useful_info)) =
- let
- val (kind, phi) =
- if kind = Hypothesis then
- (hypothesis_kind, phi |> hypothesis_kind = Conjecture ? mk_anot)
- else
- (kind, phi)
- in
- (case format of Fof => "fof" | Tff => "tff") ^
- "(" ^ ident ^ ", " ^ string_for_kind kind ^ ",\n (" ^
- string_for_formula phi ^ ")" ^
- (case (source, useful_info) of
- (NONE, NONE) => ""
- | (SOME tm, NONE) => ", " ^ string_for_term tm
- | (_, SOME tm) =>
- ", " ^ string_for_term (source |> the_default default_source) ^
- ", " ^ string_for_term tm) ^ ").\n"
- end
-fun tptp_strings_for_atp_problem hypothesis_kind format problem =
+ (case format of Fof => "fof" | Tff => "tff") ^
+ "(" ^ ident ^ ", " ^ string_for_kind kind ^ ",\n (" ^
+ string_for_formula phi ^ ")" ^
+ (case (source, useful_info) of
+ (NONE, NONE) => ""
+ | (SOME tm, NONE) => ", " ^ string_for_term tm
+ | (_, SOME tm) =>
+ ", " ^ string_for_term (source |> the_default default_source) ^
+ ", " ^ string_for_term tm) ^ ").\n"
+fun tptp_strings_for_atp_problem format problem =
"% This file was generated by Isabelle (most likely Sledgehammer)\n\
\% " ^ timestamp () ^ "\n" ::
maps (fn (_, []) => []
| (heading, lines) =>
"\n% " ^ heading ^ " (" ^ string_of_int (length lines) ^ ")\n" ::
- map (string_for_problem_line hypothesis_kind format) lines)
+ map (string_for_problem_line format) lines)
problem
fun is_atp_variable s = Char.isUpper (String.sub (s, 0))
--- a/src/HOL/Tools/ATP/atp_systems.ML Fri May 06 13:34:59 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML Fri May 06 13:34:59 2011 +0200
@@ -19,7 +19,8 @@
-> string,
proof_delims : (string * string) list,
known_failures : (failure * string) list,
- hypothesis_kind : formula_kind,
+ conj_sym_kind : formula_kind,
+ prem_kind : formula_kind,
formats : format list,
best_slices : Proof.context -> (real * (bool * int)) list,
best_type_systems : string list}
@@ -41,7 +42,7 @@
val remote_prefix : string
val remote_atp :
string -> string -> string list -> (string * string) list
- -> (failure * string) list -> formula_kind -> format list
+ -> (failure * string) list -> formula_kind -> formula_kind -> format list
-> (Proof.context -> int) -> string list -> string * atp_config
val add_atp : string * atp_config -> theory -> theory
val get_atp : theory -> string -> atp_config
@@ -67,7 +68,8 @@
-> string,
proof_delims : (string * string) list,
known_failures : (failure * string) list,
- hypothesis_kind : formula_kind,
+ conj_sym_kind : formula_kind,
+ prem_kind : formula_kind,
formats : format list,
best_slices : Proof.context -> (real * (bool * int)) list,
best_type_systems : string list}
@@ -201,7 +203,8 @@
"# Cannot determine problem status within resource limit"),
(OutOfResources, "SZS status: ResourceOut"),
(OutOfResources, "SZS status ResourceOut")],
- hypothesis_kind = Conjecture,
+ conj_sym_kind = Conjecture, (* FIXME: try out Hypothesis *)
+ prem_kind = Conjecture,
formats = [Fof],
best_slices = fn ctxt =>
if effective_e_weight_method ctxt = e_slicesN then
@@ -239,7 +242,8 @@
(MalformedInput, "Free Variable"),
(SpassTooOld, "tptp2dfg"),
(InternalError, "Please report this error")],
- hypothesis_kind = Conjecture,
+ conj_sym_kind = Axiom, (* FIXME: try out Hypothesis *)
+ prem_kind = Conjecture,
formats = [Fof],
best_slices =
K [(0.66667, (false, 150 (* FUDGE *))) (* with SOS *),
@@ -276,7 +280,8 @@
(Unprovable, "Termination reason: Satisfiable"),
(VampireTooOld, "not a valid option"),
(Interrupted, "Aborted by signal SIGINT")],
- hypothesis_kind = Conjecture,
+ conj_sym_kind = Conjecture, (* FIXME: try out Hypothesis *)
+ prem_kind = Conjecture,
formats = [Fof],
best_slices =
K [(0.66667, (false, 450 (* FUDGE *))) (* with SOS *),
@@ -301,7 +306,8 @@
(IncompleteUnprovable, "SZS status Satisfiable"),
(ProofMissing, "\nunsat"),
(ProofMissing, "SZS status Unsatisfiable")],
- hypothesis_kind = Hypothesis,
+ conj_sym_kind = Hypothesis,
+ prem_kind = Hypothesis,
formats = [Fof],
best_slices = K [(1.0, (false, 250 (* FUDGE *)))],
best_type_systems = [] (* FIXME *)}
@@ -342,8 +348,8 @@
val max_remote_secs = 240 (* give Geoff Sutcliffe's servers a break *)
fun remote_config system_name system_versions proof_delims known_failures
- hypothesis_kind formats best_max_relevant best_type_systems
- : atp_config =
+ conj_sym_kind prem_kind formats best_max_relevant
+ best_type_systems : atp_config =
{exec = ("ISABELLE_ATP", "scripts/remote_atp"),
required_execs = [],
arguments = fn _ => fn _ => fn timeout => fn _ =>
@@ -355,7 +361,8 @@
[(IncompleteUnprovable, "says Unknown"),
(IncompleteUnprovable, "says GaveUp"),
(TimedOut, "says Timeout")],
- hypothesis_kind = hypothesis_kind,
+ conj_sym_kind = conj_sym_kind,
+ prem_kind = prem_kind,
formats = formats,
best_slices = fn ctxt => [(1.0, (false, best_max_relevant ctxt))],
best_type_systems = best_type_systems}
@@ -363,18 +370,18 @@
fun int_average f xs = fold (Integer.add o f) xs 0 div length xs
fun remotify_config system_name system_versions
- ({proof_delims, known_failures, hypothesis_kind, formats,
- best_slices, best_type_systems, ...} : atp_config)
- : atp_config =
+ ({proof_delims, known_failures, conj_sym_kind, prem_kind, formats,
+ best_slices, best_type_systems, ...} : atp_config) : atp_config =
remote_config system_name system_versions proof_delims known_failures
- hypothesis_kind formats (int_average (snd o snd) o best_slices)
- best_type_systems
+ conj_sym_kind prem_kind formats
+ (int_average (snd o snd) o best_slices) best_type_systems
fun remote_atp name system_name system_versions proof_delims known_failures
- hypothesis_kind formats best_max_relevant best_type_systems =
+ conj_sym_kind prem_kind formats best_max_relevant best_type_systems =
(remote_prefix ^ name,
remote_config system_name system_versions proof_delims known_failures
- hypothesis_kind formats best_max_relevant best_type_systems)
+ conj_sym_kind prem_kind formats best_max_relevant
+ best_type_systems)
fun remotify_atp (name, config) system_name system_versions =
(remote_prefix ^ name, remotify_config system_name system_versions config)
@@ -383,14 +390,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)
- Conjecture [Tff] (K 200 (* FUDGE *)) ["simple"]
+ Axiom Conjecture [Tff] (K 200 (* FUDGE *)) ["simple"]
val remote_sine_e =
- remote_atp sine_eN "SInE" ["0.4"] [] [] Conjecture [Fof] (K 500 (* FUDGE *))
- ["args", "preds", "tags"]
+ remote_atp sine_eN "SInE" ["0.4"] [] [] Axiom Conjecture [Fof]
+ (K 500 (* FUDGE *)) ["args", "preds", "tags"]
val remote_snark =
remote_atp snarkN "SNARK" ["20080805r024"]
- [("refutation.", "end_refutation.")] [] Conjecture [Tff, Fof]
- (K 250 (* FUDGE *)) ["simple"]
+ [("refutation.", "end_refutation.")] [] Hypothesis Conjecture
+ [Tff, Fof] (K 250 (* FUDGE *)) ["simple"]
(* Setup *)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Fri May 06 13:34:59 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Fri May 06 13:34:59 2011 +0200
@@ -9,6 +9,7 @@
signature SLEDGEHAMMER_ATP_TRANSLATE =
sig
type 'a fo_term = 'a ATP_Problem.fo_term
+ type formula_kind = ATP_Problem.formula_kind
type 'a problem = 'a ATP_Problem.problem
type locality = Sledgehammer_Filter.locality
@@ -41,7 +42,8 @@
Proof.context -> bool -> (string * locality) * thm
-> translated_formula option * ((string * locality) * thm)
val prepare_atp_problem :
- Proof.context -> type_system -> bool -> term list -> term
+ Proof.context -> formula_kind -> formula_kind -> type_system -> bool
+ -> term list -> term
-> (translated_formula option * ((string * 'a) * thm)) list
-> string problem * string Symtab.table * int * int
* (string * 'a) list vector
@@ -215,6 +217,7 @@
|> 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
@@ -452,10 +455,21 @@
NONE
| (_, formula) => SOME formula
-fun make_conjecture ctxt ts =
+fun make_conjecture ctxt prem_kind ts =
let val last = length ts - 1 in
- map2 (fn j => make_formula ctxt true true (string_of_int j) Chained
- (if j = last then Conjecture else Hypothesis))
+ map2 (fn j => fn t =>
+ let
+ val (kind, maybe_negate) =
+ if j = last then
+ (Conjecture, I)
+ else
+ (prem_kind,
+ if prem_kind = Conjecture then update_combformula mk_anot
+ else I)
+ in
+ make_formula ctxt true true (string_of_int j) Chained kind t
+ |> maybe_negate
+ end)
(0 upto last) ts
end
@@ -750,7 +764,7 @@
fun translate_atp_fact ctxt keep_trivial =
`(make_fact ctxt keep_trivial true true o apsnd prop_of)
-fun translate_formulas ctxt type_sys hyp_ts concl_t rich_facts =
+fun translate_formulas ctxt prem_kind type_sys hyp_ts concl_t rich_facts =
let
val thy = Proof_Context.theory_of ctxt
val fact_ts = map (prop_of o snd o snd) rich_facts
@@ -767,7 +781,7 @@
val subs = tfree_classes_of_terms all_ts
val supers = tvar_classes_of_terms all_ts
val tycons = type_consts_of_terms thy all_ts
- val conjs = make_conjecture ctxt (hyp_ts @ [concl_t])
+ val conjs = make_conjecture ctxt prem_kind (hyp_ts @ [concl_t])
val (supers', arity_clauses) =
if level_of_type_sys type_sys = No_Types then ([], [])
else make_arity_clauses thy tycons supers
@@ -985,9 +999,12 @@
fun is_polymorphic_type T = fold_atyps (fn TVar _ => K true | _ => I) T false
-fun formula_line_for_sym_decl ctxt nonmono_Ts type_sys n s j
+fun formula_line_for_sym_decl ctxt conj_sym_kind nonmono_Ts type_sys n s j
(s', T_args, T, _, ary, in_conj) =
let
+ val (kind, maybe_negate) =
+ if in_conj then (conj_sym_kind, conj_sym_kind = Conjecture ? mk_anot)
+ else (Axiom, I)
val (arg_Ts, res_T) = n_ary_strip_type ary T
val bound_names =
1 upto length arg_Ts |> map (`I o make_bound_var o string_of_int)
@@ -998,18 +1015,19 @@
else NONE)
in
Formula (sym_decl_prefix ^ s ^
- (if n > 1 then "_" ^ string_of_int j else ""),
- if in_conj then Hypothesis else Axiom,
+ (if n > 1 then "_" ^ string_of_int j else ""), kind,
CombConst ((s, s'), T, T_args)
|> fold (curry (CombApp o swap)) bound_tms
|> type_pred_combatom ctxt nonmono_Ts type_sys res_T
|> mk_aquant AForall (bound_names ~~ bound_Ts)
|> formula_from_combformula ctxt nonmono_Ts type_sys
- |> close_formula_universally,
+ |> close_formula_universally
+ |> maybe_negate,
NONE, NONE)
end
-fun problem_lines_for_sym_decls ctxt nonmono_Ts type_sys (s, decls) =
+fun problem_lines_for_sym_decls ctxt conj_sym_kind nonmono_Ts type_sys
+ (s, decls) =
case type_sys of
Simple _ => map (decl_line_for_sym s) decls
| _ =>
@@ -1030,13 +1048,15 @@
decls |> filter (should_predicate_on_type ctxt nonmono_Ts type_sys
o result_type_of_decl)
in
- map2 (formula_line_for_sym_decl ctxt nonmono_Ts type_sys n s)
- (0 upto length decls - 1) decls
+ (0 upto length decls - 1, decls)
+ |-> map2 (formula_line_for_sym_decl ctxt conj_sym_kind nonmono_Ts type_sys
+ n s)
end
-fun problem_lines_for_sym_decl_table ctxt nonmono_Ts type_sys sym_decl_tab =
- Symtab.fold_rev (append o problem_lines_for_sym_decls ctxt nonmono_Ts
- type_sys)
+fun problem_lines_for_sym_decl_table ctxt conj_sym_kind nonmono_Ts type_sys
+ sym_decl_tab =
+ Symtab.fold_rev (append o problem_lines_for_sym_decls ctxt conj_sym_kind
+ nonmono_Ts type_sys)
sym_decl_tab []
fun add_tff_types_in_formula (AQuant (_, xs, phi)) =
@@ -1070,10 +1090,11 @@
if heading = needle then j
else offset_of_heading_in_problem needle problem (j + length lines)
-fun prepare_atp_problem ctxt type_sys explicit_apply hyp_ts concl_t facts =
+fun prepare_atp_problem ctxt conj_sym_kind prem_kind type_sys explicit_apply
+ hyp_ts concl_t facts =
let
val (fact_names, (conjs, facts, class_rel_clauses, arity_clauses)) =
- translate_formulas ctxt type_sys hyp_ts concl_t facts
+ translate_formulas ctxt prem_kind type_sys hyp_ts concl_t facts
val sym_tab = conjs @ facts |> sym_table_for_facts explicit_apply
val nonmono_Ts =
[] |> fold (add_nonmonotonic_types_for_facts ctxt type_sys) [facts, conjs]
@@ -1085,7 +1106,7 @@
val sym_decl_lines =
(conjs, facts) (* FIXME: what if "True_or_False" is among helpers? *)
|> sym_decl_table_for_facts type_sys repaired_sym_tab
- |> problem_lines_for_sym_decl_table ctxt nonmono_Ts type_sys
+ |> problem_lines_for_sym_decl_table ctxt conj_sym_kind nonmono_Ts type_sys
(* Reordering these might confuse the proof reconstruction code or the SPASS
Flotter hack. *)
val problem =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Fri May 06 13:34:59 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Fri May 06 13:34:59 2011 +0200
@@ -364,8 +364,8 @@
fun run_atp auto name
({exec, required_execs, arguments, proof_delims, known_failures,
- hypothesis_kind, formats, best_slices, best_type_systems, ...}
- : atp_config)
+ conj_sym_kind, prem_kind, formats, best_slices, best_type_systems,
+ ...} : atp_config)
({debug, verbose, overlord, type_sys, max_relevant, monomorphize_limit,
explicit_apply, isar_proof, isar_shrink_factor, slicing, timeout, ...}
: params)
@@ -470,8 +470,8 @@
()
val (atp_problem, pool, conjecture_offset, facts_offset,
fact_names) =
- prepare_atp_problem ctxt type_sys explicit_apply hyp_ts
- concl_t facts
+ prepare_atp_problem ctxt conj_sym_kind prem_kind type_sys
+ explicit_apply hyp_ts concl_t facts
fun weights () = atp_problem_weights atp_problem
val core =
File.shell_path command ^ " " ^
@@ -484,7 +484,7 @@
"exec " ^ core) ^ " 2>&1"
val _ =
atp_problem
- |> tptp_strings_for_atp_problem hypothesis_kind format
+ |> tptp_strings_for_atp_problem format
|> cons ("% " ^ command ^ "\n")
|> File.write_list prob_file
val conjecture_shape =
--- a/src/HOL/ex/tptp_export.ML Fri May 06 13:34:59 2011 +0200
+++ b/src/HOL/ex/tptp_export.ML Fri May 06 13:34:59 2011 +0200
@@ -104,8 +104,8 @@
else Sledgehammer_ATP_Translate.Const_Arg_Types)
val explicit_apply = false
val (atp_problem, _, _, _, _) =
- Sledgehammer_ATP_Translate.prepare_atp_problem ctxt type_sys
- explicit_apply [] @{prop False} facts
+ Sledgehammer_ATP_Translate.prepare_atp_problem ctxt ATP_Problem.Axiom
+ ATP_Problem.Axiom type_sys explicit_apply [] @{prop False} facts
val infers =
facts0 |> map (fn (_, (_, th)) =>
(fact_name_of (Thm.get_name_hint th),
@@ -114,8 +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.Hypothesis
- 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