--- a/src/HOL/Tools/ATP/atp_problem.ML Sun May 22 14:50:32 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML Sun May 22 14:51:01 2011 +0200
@@ -15,7 +15,7 @@
AConn of connective * ('a, 'b, 'c) formula list |
AAtom of 'c
- datatype format = UEQ | FOF | TFF
+ datatype format = CNF_UEQ | FOF | TFF
datatype formula_kind = Axiom | Definition | Lemma | Hypothesis | Conjecture
datatype 'a problem_line =
Decl of string * 'a * 'a list * 'a |
@@ -23,18 +23,20 @@
* string fo_term option * string fo_term option
type 'a problem = (string * 'a problem_line list) list
-(* official TPTP syntax *)
+ (* official TPTP syntax *)
val tptp_special_prefix : string
val tptp_false : string
val tptp_true : string
val tptp_tff_type_of_types : string
val tptp_tff_bool_type : string
val tptp_tff_individual_type : string
+ val is_atp_variable : string -> bool
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 : format -> string problem -> string list
+ val filter_cnf_ueq_problem :
+ (string * string) problem -> (string * string) problem
val nice_atp_problem :
bool -> ('a * (string * string) problem_line list) list
-> ('a * string problem_line list) list
@@ -54,7 +56,7 @@
AConn of connective * ('a, 'b, 'c) formula list |
AAtom of 'c
-datatype format = UEQ | FOF | TFF
+datatype format = CNF_UEQ | FOF | TFF
datatype formula_kind = Axiom | Definition | Lemma | Hypothesis | Conjecture
datatype 'a problem_line =
Decl of string * 'a * 'a list * 'a |
@@ -70,6 +72,8 @@
val tptp_tff_bool_type = "$o"
val tptp_tff_individual_type = "$i"
+fun is_atp_variable s = Char.isUpper (String.sub (s, 0))
+
val timestamp = Date.fmt "%Y-%m-%d %H:%M:%S" o Date.fromTimeLocal o Time.now
(* This hash function is recommended in Compilers: Principles, Techniques, and
@@ -129,12 +133,11 @@
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 format
- (Formula (ident, kind, phi, source, useful_info)) =
- (case format of UEQ => "cnf" | FOF => "fof" | TFF => "tff") ^
+ | string_for_problem_line format (Formula (ident, kind, phi, source, info)) =
+ (case format of CNF_UEQ => "cnf" | FOF => "fof" | TFF => "tff") ^
"(" ^ ident ^ ", " ^ string_for_kind kind ^ ",\n (" ^
string_for_formula format phi ^ ")" ^
- (case (source, useful_info) of
+ (case (source, info) of
(NONE, NONE) => ""
| (SOME tm, NONE) => ", " ^ string_for_term tm
| (_, SOME tm) =>
@@ -149,7 +152,37 @@
map (string_for_problem_line format) lines)
problem
-fun is_atp_variable s = Char.isUpper (String.sub (s, 0))
+
+(** CNF UEQ (Waldmeister) **)
+
+exception LOST_CONJECTURE of unit
+
+fun is_problem_line_negated (Formula (_, _, AConn (ANot, _), _, _)) = true
+ | is_problem_line_negated _ = false
+
+fun is_problem_line_cnf_ueq
+ (Formula (_, _, AAtom (ATerm (("equal", _), _)), _, _)) = true
+ | is_problem_line_cnf_ueq _ = false
+
+fun open_formula (AQuant (AForall, _, phi)) = open_formula phi
+ | open_formula phi = phi
+fun open_non_conjecture_line (line as Formula (_, Conjecture, _, _, _)) = line
+ | open_non_conjecture_line (Formula (ident, kind, phi, source, info)) =
+ Formula (ident, kind, open_formula phi, source, info)
+ | open_non_conjecture_line line = line
+
+fun negate_conjecture_line (Formula (ident, Conjecture, phi, source, info)) =
+ Formula (ident, Hypothesis, AConn (ANot, [phi]), source, info)
+ | negate_conjecture_line line = line
+
+val filter_cnf_ueq_problem =
+ map (apsnd (map open_non_conjecture_line
+ #> filter is_problem_line_cnf_ueq
+ #> map negate_conjecture_line))
+ #> (fn problem =>
+ let
+ val conjs = problem |> maps snd |> filter is_problem_line_negated
+ in if length conjs = 1 then problem else [] end)
(** Nice names **)
@@ -178,14 +211,15 @@
problem files. "equal" is reserved by some ATPs. "eq" is reserved to ensure
that "HOL.eq" is correctly mapped to equality. *)
val reserved_nice_names = ["op", "equal", "eq"]
+
fun readable_name full_name s =
if s = full_name then
s
else
s |> no_qualifiers
|> Name.desymbolize (Char.isUpper (String.sub (full_name, 0)))
- (* SNARK doesn't like sort (type) names that end with digits. We make
- an effort to avoid this here. *)
+ (* SNARK 20080805r024 doesn't like sort (type) names that end with
+ digits. We make an effort to avoid this here. *)
|> (fn s => if Char.isDigit (String.sub (s, size s - 1)) then s ^ "_"
else s)
|> (fn s =>
@@ -209,7 +243,8 @@
val nice_prefix = readable_name full_name desired_name
fun add j =
let
- (* The trailing "_" is for SNARK (cf. comment above). *)
+ (* The trailing "_" is for SNARK 20080805r024 (see comment
+ above). *)
val nice_name =
nice_prefix ^ (if j = 0 then "" else "_" ^ string_of_int j ^ "_")
in
@@ -240,9 +275,8 @@
##>> 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 (ident, kind, phi, source, useful_info)) =
- nice_formula phi
- #>> (fn phi => Formula (ident, kind, phi, source, useful_info))
+ | nice_problem_line (Formula (ident, kind, phi, source, info)) =
+ nice_formula phi #>> (fn phi => Formula (ident, kind, phi, source, info))
fun nice_problem problem =
pool_map (fn (heading, lines) =>
pool_map nice_problem_line lines #>> pair heading) problem
--- a/src/HOL/Tools/ATP/atp_systems.ML Sun May 22 14:50:32 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML Sun May 22 14:51:01 2011 +0200
@@ -413,7 +413,7 @@
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"]
+ remote_atp snarkN "SNARK" ["20080805r029", "20080805r024"]
[("refutation.", "end_refutation.")] [] Hypothesis Conjecture
[TFF, FOF] (K (250, ["simple"]) (* FUDGE *))
val remote_waldmeister =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Sun May 22 14:50:32 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Sun May 22 14:51:01 2011 +0200
@@ -9,6 +9,7 @@
signature SLEDGEHAMMER_ATP_TRANSLATE =
sig
type 'a fo_term = 'a ATP_Problem.fo_term
+ type format = ATP_Problem.format
type formula_kind = ATP_Problem.formula_kind
type 'a problem = 'a ATP_Problem.problem
type locality = Sledgehammer_Filter.locality
@@ -44,8 +45,8 @@
Proof.context -> bool -> (string * locality) * thm
-> translated_formula option * ((string * locality) * thm)
val prepare_atp_problem :
- Proof.context -> formula_kind -> formula_kind -> type_system -> bool
- -> term list -> term
+ Proof.context -> format -> 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 * int list * int Symtab.table
@@ -908,8 +909,8 @@
| Simp => simp_info
| _ => NONE)
-fun formula_line_for_class_rel_clause (ClassRelClause {name, subclass,
- superclass, ...}) =
+fun formula_line_for_class_rel_clause
+ (ClassRelClause {name, subclass, superclass, ...}) =
let val ty_arg = ATerm (`I "T", []) in
Formula (class_rel_clause_prefix ^ ascii_of name, Axiom,
AConn (AImplies, [AAtom (ATerm (subclass, [ty_arg])),
@@ -922,8 +923,8 @@
| fo_literal_from_arity_literal (TVarLit (c, sort)) =
(false, ATerm (c, [ATerm (sort, [])]))
-fun formula_line_for_arity_clause (ArityClause {name, prem_lits, concl_lits,
- ...}) =
+fun formula_line_for_arity_clause
+ (ArityClause {name, prem_lits, concl_lits, ...}) =
Formula (arity_clause_prefix ^ ascii_of name, Axiom,
mk_ahorn (map (formula_from_fo_literal o apfst not
o fo_literal_from_arity_literal) prem_lits)
@@ -935,8 +936,8 @@
({name, kind, combformula, ...} : translated_formula) =
Formula (conjecture_prefix ^ name, kind,
formula_from_combformula ctxt nonmono_Ts type_sys
- is_var_nonmonotonic_in_formula false
- (close_combformula_universally combformula)
+ is_var_nonmonotonic_in_formula false
+ (close_combformula_universally combformula)
|> close_formula_universally, NONE, NONE)
fun free_type_literals type_sys ({atomic_types, ...} : translated_formula) =
@@ -1183,6 +1184,11 @@
level = Nonmonotonic_Types orelse level = Finite_Types
| should_add_ti_ti_helper _ = false
+fun offset_of_heading_in_problem _ [] j = j
+ | offset_of_heading_in_problem needle ((heading, lines) :: problem) j =
+ if heading = needle then j
+ else offset_of_heading_in_problem needle problem (j + length lines)
+
val type_declsN = "Types"
val sym_declsN = "Symbol types"
val factsN = "Relevant facts"
@@ -1192,13 +1198,8 @@
val conjsN = "Conjectures"
val free_typesN = "Type variables"
-fun offset_of_heading_in_problem _ [] j = j
- | offset_of_heading_in_problem needle ((heading, lines) :: problem) j =
- if heading = needle then j
- else offset_of_heading_in_problem needle problem (j + length lines)
-
-fun prepare_atp_problem ctxt conj_sym_kind prem_kind type_sys explicit_apply
- hyp_ts concl_t facts =
+fun prepare_atp_problem ctxt format 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 prem_kind type_sys hyp_ts concl_t facts
@@ -1223,7 +1224,10 @@
val helper_lines =
map (formula_line_for_fact ctxt helper_prefix lavish_nonmono_Ts type_sys)
(0 upto length helpers - 1 ~~ helpers)
- |> should_add_ti_ti_helper type_sys ? cons (ti_ti_helper_fact ())
+ |> (if should_add_ti_ti_helper type_sys then
+ cons (ti_ti_helper_fact ())
+ else
+ I)
(* Reordering these might confuse the proof reconstruction code or the SPASS
Flotter hack. *)
val problem =
@@ -1243,6 +1247,8 @@
cons (type_declsN,
map decl_line_for_tff_type (tff_types_in_problem problem))
| _ => I)
+ val problem =
+ problem |> (if format = CNF_UEQ then filter_cnf_ueq_problem else I)
val (problem, pool) =
problem |> nice_atp_problem (Config.get ctxt readable_names)
val helpers_offset = offset_of_heading_in_problem helpersN problem 0
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Sun May 22 14:50:32 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Sun May 22 14:51:01 2011 +0200
@@ -413,8 +413,15 @@
(* 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 if member (op =) formats CNF_UEQ then
+ (CNF_UEQ, case type_sys of
+ Tags _ => type_sys
+ | _ => Preds (polymorphism_of_type_sys type_sys,
+ Const_Arg_Types, Light))
+ 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
@@ -535,8 +542,8 @@
()
val (atp_problem, pool, conjecture_offset, facts_offset,
fact_names, typed_helpers, sym_tab) =
- prepare_atp_problem ctxt conj_sym_kind prem_kind type_sys
- explicit_apply hyp_ts concl_t facts
+ prepare_atp_problem ctxt format 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 ^ " " ^
--- a/src/HOL/ex/tptp_export.ML Sun May 22 14:50:32 2011 +0200
+++ b/src/HOL/ex/tptp_export.ML Sun May 22 14:51:01 2011 +0200
@@ -104,8 +104,9 @@
Sledgehammer_ATP_Translate.Heavy)
val explicit_apply = false
val (atp_problem, _, _, _, _, _, _) =
- Sledgehammer_ATP_Translate.prepare_atp_problem ctxt ATP_Problem.Axiom
- ATP_Problem.Axiom type_sys explicit_apply [] @{prop False} facts
+ Sledgehammer_ATP_Translate.prepare_atp_problem ctxt ATP_Problem.FOF
+ 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),