--- a/src/HOL/TPTP/atp_export.ML Sat Oct 29 13:15:58 2011 +0200
+++ b/src/HOL/TPTP/atp_export.ML Sat Oct 29 13:15:58 2011 +0200
@@ -115,8 +115,7 @@
val prob_file = File.tmp_path (Path.explode "prob.tptp")
val {exec, arguments, proof_delims, known_failures, ...} =
get_atp thy spassN
- val _ = problem |> tptp_lines_for_atp_problem FOF
- |> File.write_list prob_file
+ val _ = problem |> lines_for_atp_problem FOF |> File.write_list prob_file
val command =
File.shell_path (Path.explode (getenv (fst exec) ^ "/" ^ snd exec)) ^
" " ^ arguments ctxt false "" (seconds 1.0) (K []) ^ " " ^
@@ -189,7 +188,7 @@
val atp_problem =
atp_problem |> add_inferences_to_problem infers
|> order_problem_facts name_ord
- val ss = tptp_lines_for_atp_problem FOF atp_problem
+ val ss = lines_for_atp_problem FOF atp_problem
val _ = app (File.append path) ss
in () end
--- a/src/HOL/Tools/ATP/atp_problem.ML Sat Oct 29 13:15:58 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML Sat Oct 29 13:15:58 2011 +0200
@@ -25,12 +25,14 @@
datatype tptp_polymorphism = TPTP_Monomorphic | TPTP_Polymorphic
datatype tptp_explicitness = TPTP_Implicit | TPTP_Explicit
datatype thf_flavor = THF_Without_Choice | THF_With_Choice
- datatype tptp_format =
+
+ datatype atp_format =
CNF |
CNF_UEQ |
FOF |
TFF of tptp_polymorphism * tptp_explicitness |
- THF of tptp_polymorphism * tptp_explicitness * thf_flavor
+ THF of tptp_polymorphism * tptp_explicitness * thf_flavor |
+ DFG_Sorted
datatype formula_kind = Axiom | Definition | Lemma | Hypothesis | Conjecture
datatype 'a problem_line =
@@ -41,6 +43,11 @@
* (string, string ho_type) ho_term option
type 'a problem = (string * 'a problem_line list) list
+ val isabelle_info_prefix : string
+ val isabelle_info : atp_format -> string -> (string, 'a) ho_term option
+ val introN : string
+ val elimN : string
+ val simpN : string
val tptp_cnf : string
val tptp_fof : string
val tptp_tff : string
@@ -92,9 +99,9 @@
bool option -> (bool option -> 'c -> 'd -> 'd) -> ('a, 'b, 'c) formula
-> 'd -> 'd
val formula_map : ('c -> 'd) -> ('a, 'b, 'c) formula -> ('a, 'b, 'd) formula
- val is_format_thf : tptp_format -> bool
- val is_format_typed : tptp_format -> bool
- val tptp_lines_for_atp_problem : tptp_format -> string problem -> string list
+ val is_format_thf : atp_format -> bool
+ val is_format_typed : atp_format -> bool
+ val lines_for_atp_problem : atp_format -> string problem -> string list
val ensure_cnf_problem :
(string * string) problem -> (string * string) problem
val filter_cnf_ueq_problem :
@@ -134,12 +141,13 @@
datatype tptp_explicitness = TPTP_Implicit | TPTP_Explicit
datatype thf_flavor = THF_Without_Choice | THF_With_Choice
-datatype tptp_format =
+datatype atp_format =
CNF |
CNF_UEQ |
FOF |
TFF of tptp_polymorphism * tptp_explicitness |
- THF of tptp_polymorphism * tptp_explicitness * thf_flavor
+ THF of tptp_polymorphism * tptp_explicitness * thf_flavor |
+ DFG_Sorted
datatype formula_kind = Axiom | Definition | Lemma | Hypothesis | Conjecture
datatype 'a problem_line =
@@ -148,6 +156,21 @@
* (string, string ho_type) ho_term option * (string, string ho_type) ho_term option
type 'a problem = (string * 'a problem_line list) list
+val isabelle_info_prefix = "isabelle_"
+
+(* Currently, only SPASS supports Isabelle metainformation. *)
+fun isabelle_info DFG_Sorted s =
+ SOME (ATerm ("[]", [ATerm (isabelle_info_prefix ^ s, [])]))
+ | isabelle_info _ _ = NONE
+
+val introN = "intro"
+val elimN = "elim"
+val simpN = "simp"
+
+fun is_isabelle_info suffix (SOME (ATerm ("[]", [ATerm (s, [])]))) =
+ s = isabelle_info_prefix ^ suffix
+ | is_isabelle_info _ _ = false
+
(* official TPTP syntax *)
val tptp_cnf = "cnf"
val tptp_fof = "fof"
@@ -186,6 +209,10 @@
fun is_tptp_variable s = Char.isUpper (String.sub (s, 0))
val is_tptp_user_symbol = not o (is_tptp_variable orf is_built_in_tptp_symbol)
+val atype_of_types = AType (`I tptp_type_of_types, [])
+val bool_atype = AType (`I tptp_bool_type, [])
+val individual_atype = AType (`I tptp_individual_type, [])
+
fun raw_polarities_of_conn ANot = (SOME false, NONE)
| raw_polarities_of_conn AAnd = (SOME true, SOME true)
| raw_polarities_of_conn AOr = (SOME true, SOME true)
@@ -228,15 +255,16 @@
| is_format_thf _ = false
fun is_format_typed (TFF _) = true
| is_format_typed (THF _) = true
+ | is_format_typed (DFG_Sorted) = true
| is_format_typed _ = false
-fun string_for_kind Axiom = "axiom"
- | string_for_kind Definition = "definition"
- | string_for_kind Lemma = "lemma"
- | string_for_kind Hypothesis = "hypothesis"
- | string_for_kind Conjecture = "conjecture"
+fun tptp_string_for_kind Axiom = "axiom"
+ | tptp_string_for_kind Definition = "definition"
+ | tptp_string_for_kind Lemma = "lemma"
+ | tptp_string_for_kind Hypothesis = "hypothesis"
+ | tptp_string_for_kind Conjecture = "conjecture"
-fun string_for_app format func args =
+fun tptp_string_for_app format func args =
if is_format_thf format then
"(" ^ space_implode (" " ^ tptp_app ^ " ") (func :: args) ^ ")"
else
@@ -255,17 +283,21 @@
fun str_for_type format ty =
let
- fun str _ (AType (s, [])) = s
+ val dfg = (format = DFG_Sorted)
+ fun str _ (AType (s, [])) =
+ if dfg andalso s = tptp_individual_type then "Top" else s
| str _ (AType (s, tys)) =
let val ss = tys |> map (str false) in
if s = tptp_product_type then
- ss |> space_implode (" " ^ tptp_product_type ^ " ")
- |> length ss > 1 ? enclose "(" ")"
+ ss |> space_implode
+ (if dfg then ", " else " " ^ tptp_product_type ^ " ")
+ |> (not dfg andalso length ss > 1) ? enclose "(" ")"
else
- string_for_app format s ss
+ tptp_string_for_app format s ss
end
| str rhs (AFun (ty1, ty2)) =
- str false ty1 ^ " " ^ tptp_fun_type ^ " " ^ str true ty2
+ (str false ty1 |> dfg ? enclose "(" ")") ^ " " ^
+ (if dfg then "" else tptp_fun_type ^ " ") ^ str true ty2
|> not rhs ? enclose "(" ")"
| str _ (ATyAbs (ss, ty)) =
tptp_pi_binder ^ "[" ^
@@ -274,17 +306,16 @@
in str true ty end
fun string_for_type (format as THF _) ty = str_for_type format ty
- | string_for_type (format as TFF _) ty = str_for_type format (flatten_type ty)
- | string_for_type _ _ = raise Fail "unexpected type in untyped format"
+ | string_for_type format ty = str_for_type format (flatten_type ty)
-fun string_for_quantifier AForall = tptp_forall
- | string_for_quantifier AExists = tptp_exists
+fun tptp_string_for_quantifier AForall = tptp_forall
+ | tptp_string_for_quantifier AExists = tptp_exists
-fun string_for_connective ANot = tptp_not
- | string_for_connective AAnd = tptp_and
- | string_for_connective AOr = tptp_or
- | string_for_connective AImplies = tptp_implies
- | string_for_connective AIff = tptp_iff
+fun tptp_string_for_connective ANot = tptp_not
+ | tptp_string_for_connective AAnd = tptp_and
+ | tptp_string_for_connective AOr = tptp_or
+ | tptp_string_for_connective AImplies = tptp_implies
+ | tptp_string_for_connective AIff = tptp_iff
fun string_for_bound_var format (s, ty) =
s ^
@@ -298,84 +329,193 @@
fun is_format_with_choice (THF (_, _, THF_With_Choice)) = true
| is_format_with_choice _ = false
-fun string_for_term _ (ATerm (s, [])) = s
- | string_for_term format (ATerm (s, ts)) =
+fun tptp_string_for_term _ (ATerm (s, [])) = s
+ | tptp_string_for_term format (ATerm (s, ts)) =
(if s = tptp_empty_list then
(* used for lists in the optional "source" field of a derivation *)
- "[" ^ commas (map (string_for_term format) ts) ^ "]"
+ "[" ^ commas (map (tptp_string_for_term format) ts) ^ "]"
else if is_tptp_equal s then
- space_implode (" " ^ tptp_equal ^ " ") (map (string_for_term format) ts)
+ space_implode (" " ^ tptp_equal ^ " ")
+ (map (tptp_string_for_term format) ts)
|> is_format_thf format ? enclose "(" ")"
else case (s = tptp_ho_forall orelse s = tptp_ho_exists,
s = tptp_choice andalso is_format_with_choice format, ts) of
(true, _, [AAbs ((s', ty), tm)]) =>
(* Use syntactic sugar "!" and "?" instead of "!!" and "??" whenever
possible, to work around LEO-II 1.2.8 parser limitation. *)
- string_for_formula format
+ tptp_string_for_formula format
(AQuant (if s = tptp_ho_forall then AForall else AExists,
[(s', SOME ty)], AAtom tm))
| (_, true, [AAbs ((s', ty), tm)]) =>
(* There is code in "ATP_Translate" to ensure that "Eps" is always
applied to an abstraction. *)
tptp_choice ^ "[" ^ s' ^ " : " ^ string_for_type format ty ^ "]: " ^
- string_for_term format tm ^ ""
+ tptp_string_for_term format tm ^ ""
|> enclose "(" ")"
- | _ => string_for_app format s (map (string_for_term format) ts))
- | string_for_term (format as THF _) (AAbs ((s, ty), tm)) =
+ | _ => tptp_string_for_app format s (map (tptp_string_for_term format) ts))
+ | tptp_string_for_term (format as THF _) (AAbs ((s, ty), tm)) =
"(^[" ^ s ^ " : " ^ string_for_type format ty ^ "]: " ^
- string_for_term format tm ^ ")"
- | string_for_term _ _ = raise Fail "unexpected term in first-order format"
-and string_for_formula format (AQuant (q, xs, phi)) =
- string_for_quantifier q ^
+ tptp_string_for_term format tm ^ ")"
+ | tptp_string_for_term _ _ =
+ raise Fail "unexpected term in first-order format"
+and tptp_string_for_formula format (AQuant (q, xs, phi)) =
+ tptp_string_for_quantifier q ^
"[" ^ commas (map (string_for_bound_var format) xs) ^ "]: " ^
- string_for_formula format phi
+ tptp_string_for_formula format phi
|> enclose "(" ")"
- | string_for_formula format
+ | tptp_string_for_formula format
(AConn (ANot, [AAtom (ATerm ("=" (* tptp_equal *), ts))])) =
space_implode (" " ^ tptp_not_infix ^ tptp_equal ^ " ")
- (map (string_for_term format) ts)
+ (map (tptp_string_for_term format) ts)
|> is_format_thf format ? enclose "(" ")"
- | string_for_formula format (AConn (c, [phi])) =
- string_for_connective c ^ " " ^
- (string_for_formula format phi |> is_format_thf format ? enclose "(" ")")
+ | tptp_string_for_formula format (AConn (c, [phi])) =
+ tptp_string_for_connective c ^ " " ^
+ (tptp_string_for_formula format phi
+ |> is_format_thf format ? enclose "(" ")")
|> enclose "(" ")"
- | string_for_formula format (AConn (c, phis)) =
- space_implode (" " ^ string_for_connective c ^ " ")
- (map (string_for_formula format) phis)
+ | tptp_string_for_formula format (AConn (c, phis)) =
+ space_implode (" " ^ tptp_string_for_connective c ^ " ")
+ (map (tptp_string_for_formula format) phis)
|> enclose "(" ")"
- | string_for_formula format (AAtom tm) = string_for_term format tm
+ | tptp_string_for_formula format (AAtom tm) = tptp_string_for_term format tm
fun the_source (SOME source) = source
| the_source NONE =
ATerm ("inference",
ATerm ("isabelle", []) :: replicate 2 (ATerm ("[]", [])))
-fun string_for_format CNF = tptp_cnf
- | string_for_format CNF_UEQ = tptp_cnf
- | string_for_format FOF = tptp_fof
- | string_for_format (TFF _) = tptp_tff
- | string_for_format (THF _) = tptp_thf
+fun tptp_string_for_format CNF = tptp_cnf
+ | tptp_string_for_format CNF_UEQ = tptp_cnf
+ | tptp_string_for_format FOF = tptp_fof
+ | tptp_string_for_format (TFF _) = tptp_tff
+ | tptp_string_for_format (THF _) = tptp_thf
+ | tptp_string_for_format DFG_Sorted = raise Fail "non-TPTP format"
-fun string_for_problem_line format (Decl (ident, sym, ty)) =
- string_for_format format ^ "(" ^ ident ^ ", type,\n " ^ sym ^ " : " ^
- string_for_type format ty ^ ").\n"
- | string_for_problem_line format (Formula (ident, kind, phi, source, info)) =
- string_for_format format ^ "(" ^ ident ^ ", " ^ string_for_kind kind ^
- ",\n (" ^ string_for_formula format phi ^ ")" ^
+fun tptp_string_for_problem_line format (Decl (ident, sym, ty)) =
+ tptp_string_for_format format ^ "(" ^ ident ^ ", type,\n " ^ sym ^
+ " : " ^ string_for_type format ty ^ ").\n"
+ | tptp_string_for_problem_line format
+ (Formula (ident, kind, phi, source, info)) =
+ tptp_string_for_format format ^ "(" ^ ident ^ ", " ^
+ tptp_string_for_kind kind ^ ",\n (" ^
+ tptp_string_for_formula format phi ^ ")" ^
(case (source, info) of
(NONE, NONE) => ""
- | (SOME tm, NONE) => ", " ^ string_for_term format tm
+ | (SOME tm, NONE) => ", " ^ tptp_string_for_term format tm
| (_, SOME tm) =>
- ", " ^ string_for_term format (the_source source) ^
- ", " ^ string_for_term format tm) ^ ").\n"
-fun tptp_lines_for_atp_problem format problem =
- "% This file was generated by Isabelle (most likely Sledgehammer)\n\
- \% " ^ timestamp () ^ "\n" ::
+ ", " ^ tptp_string_for_term format (the_source source) ^
+ ", " ^ tptp_string_for_term format tm) ^ ").\n"
+
+fun tptp_lines format =
maps (fn (_, []) => []
| (heading, lines) =>
"\n% " ^ heading ^ " (" ^ string_of_int (length lines) ^ ")\n" ::
- map (string_for_problem_line format) lines)
- problem
+ map (tptp_string_for_problem_line format) lines)
+
+fun arity_of_type (AFun (_, ty)) = 1 + arity_of_type ty
+ | arity_of_type _ = 0
+
+fun binder_atypes (AFun (ty1, ty2)) = ty1 :: binder_atypes ty2
+ | binder_atypes _ = []
+
+fun is_function_type (AFun (_, ty)) = is_function_type ty
+ | is_function_type (AType (s, _)) =
+ s <> tptp_type_of_types andalso s <> tptp_bool_type
+ | is_function_type _ = false
+
+fun is_predicate_type (AFun (_, ty)) = is_predicate_type ty
+ | is_predicate_type (AType (s, _)) = (s = tptp_bool_type)
+ | is_predicate_type _ = false
+
+fun dfg_string_for_formula info =
+ let
+ fun str_for_term simp (ATerm (s, tms)) =
+ (if is_tptp_equal s then "equal" |> simp ? suffix ":lr"
+ else if s = tptp_true then "true"
+ else if s = tptp_false then "false"
+ else s) ^
+ (if null tms then ""
+ else "(" ^ commas (map (str_for_term false) tms) ^ ")")
+ | str_for_term _ _ = raise Fail "unexpected term in first-order format"
+ fun str_for_quant AForall = "forall"
+ | str_for_quant AExists = "exists"
+ fun str_for_conn _ ANot = "not"
+ | str_for_conn _ AAnd = "and"
+ | str_for_conn _ AOr = "or"
+ | str_for_conn _ AImplies = "implies"
+ | str_for_conn simp AIff = "equiv" |> simp ? suffix ":lr"
+ fun str_for_formula simp (AQuant (q, xs, phi)) =
+ str_for_quant q ^ "(" ^ "[" ^
+ commas (map (string_for_bound_var DFG_Sorted) xs) ^ "], " ^
+ str_for_formula simp phi ^ ")"
+ | str_for_formula simp (AConn (c, phis)) =
+ str_for_conn simp c ^ "(" ^
+ commas (map (str_for_formula false) phis) ^ ")"
+ | str_for_formula simp (AAtom tm) = str_for_term simp tm
+ in str_for_formula (is_isabelle_info simpN info) end
+
+fun dfg_lines problem =
+ let
+ fun ary sym ty =
+ "(" ^ sym ^ ", " ^ string_of_int (arity_of_type ty) ^ ")"
+ fun fun_typ sym ty =
+ "function(" ^ sym ^ ", " ^ string_for_type DFG_Sorted ty ^ ")."
+ fun pred_typ sym ty =
+ "predicate(" ^
+ commas (sym :: map (string_for_type DFG_Sorted) (binder_atypes ty)) ^ ")."
+ fun formula pred (Formula (ident, kind, phi, _, info)) =
+ if pred kind then
+ SOME ("formula(" ^ dfg_string_for_formula info phi ^ ", " ^ ident ^
+ ").")
+ else
+ NONE
+ | formula _ _ = NONE
+ fun filt f = problem |> map (map_filter f o snd) |> flat
+ val func_aries =
+ filt (fn Decl (_, sym, ty) =>
+ if is_function_type ty then SOME (ary sym ty) else NONE
+ | _ => NONE)
+ |> commas |> enclose "functions [" "]."
+ val pred_aries =
+ filt (fn Decl (_, sym, ty) =>
+ if is_predicate_type ty then SOME (ary sym ty) else NONE
+ | _ => NONE)
+ |> commas |> enclose "predicates [" "]."
+ val sorts =
+ filt (fn Decl (_, sym, AType (s, [])) =>
+ if s = tptp_type_of_types then SOME sym else NONE
+ | _ => NONE)
+ |> commas |> enclose "sorts [" "]."
+ val func_sigs =
+ filt (fn Decl (_, sym, ty) =>
+ if is_function_type ty then SOME (fun_typ sym ty) else NONE
+ | _ => NONE)
+ val pred_sigs =
+ filt (fn Decl (_, sym, ty) =>
+ if is_predicate_type ty then SOME (pred_typ sym ty) else NONE
+ | _ => NONE)
+ val axioms = filt (formula (curry (op <>) Conjecture))
+ val conjs = filt (formula (curry (op =) Conjecture))
+ fun list_of _ [] = []
+ | list_of heading ss =
+ "list_of_" ^ heading ^ ".\n" :: map (suffix "\n") ss @
+ ["end_of_list.\n\n"]
+ in
+ "\nbegin_problem(isabelle).\n\n" ::
+ list_of "descriptions"
+ ["name({**}).", "author({**}).", "status(unknown).",
+ "description({**})."] @
+ list_of "symbols" [func_aries, pred_aries, sorts] @
+ list_of "declarations" (func_sigs @ pred_sigs) @
+ list_of "formulae(axioms)" axioms @
+ list_of "formulae(conjectures)" conjs @
+ ["end_problem.\n"]
+ end
+
+fun lines_for_atp_problem format problem =
+ "% This file was generated by Isabelle (most likely Sledgehammer)\n\
+ \% " ^ timestamp () ^ "\n" ::
+ (if format = DFG_Sorted then dfg_lines else tptp_lines format) problem
(** CNF (Metis) and CNF UEQ (Waldmeister) **)
@@ -467,11 +607,6 @@
(* TFF allows implicit declarations of types, function symbols, and predicate
symbols (with "$i" as the type of individuals), but some provers (e.g.,
SNARK) require explicit declarations. The situation is similar for THF. *)
-
-val atype_of_types = AType (`I tptp_type_of_types, [])
-val bool_atype = AType (`I tptp_bool_type, [])
-val individual_atype = AType (`I tptp_individual_type, [])
-
fun default_type pred_sym =
let
fun typ 0 = if pred_sym then bool_atype else individual_atype
@@ -548,7 +683,12 @@
unreadable "op_1", "op_2", etc., in the problem files. "eq" is reserved to
ensure that "HOL.eq" is correctly mapped to equality (not clear whether this
is still necessary). *)
-val reserved_nice_names = [tptp_old_equal, "op", "eq"]
+val spass_reserved_nice_names =
+ ["forall", "exists", "le", "ls", "ge", "gs", "plus", "minus", "mult", "fract",
+ "equal", "true", "false", "or", "and", "not", "implies", "implied", "equiv",
+ "lr", "def"]
+val reserved_nice_names =
+ [tptp_old_equal, "op", "eq"] @ spass_reserved_nice_names
fun readable_name full_name s =
if s = full_name then
--- a/src/HOL/Tools/ATP/atp_proof.ML Sat Oct 29 13:15:58 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML Sat Oct 29 13:15:58 2011 +0200
@@ -24,8 +24,6 @@
TimedOut |
Inappropriate |
OutOfResources |
- SpassTooOld |
- VampireTooOld |
NoPerl |
NoLibwwwPerl |
MalformedInput |
@@ -81,8 +79,6 @@
TimedOut |
Inappropriate |
OutOfResources |
- SpassTooOld |
- VampireTooOld |
NoPerl |
NoLibwwwPerl |
MalformedInput |
@@ -134,17 +130,6 @@
| string_for_failure Inappropriate =
"The problem lies outside the prover's scope."
| string_for_failure OutOfResources = "The prover ran out of resources."
- | string_for_failure SpassTooOld =
- "Isabelle requires a more recent version of SPASS with support for the \
- \TPTP syntax. To install it, download and extract the package \
- \\"http://isabelle.in.tum.de/dist/contrib/spass-3.7.tar.gz\" and add the \
- \\"spass-3.7\" directory's absolute path to " ^
- Path.print (Path.expand (Path.explode "$ISABELLE_HOME_USER/etc/components")) ^
- " on a line of its own."
- | string_for_failure VampireTooOld =
- "Isabelle requires a more recent version of Vampire. To install it, follow \
- \the instructions from the Sledgehammer manual (\"isabelle doc\
- \ sledgehammer\")."
| string_for_failure NoPerl = "Perl" ^ missing_message_tail
| string_for_failure NoLibwwwPerl =
"The Perl module \"libwww-perl\"" ^ missing_message_tail
--- a/src/HOL/Tools/ATP/atp_systems.ML Sat Oct 29 13:15:58 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML Sat Oct 29 13:15:58 2011 +0200
@@ -7,7 +7,7 @@
signature ATP_SYSTEMS =
sig
- type tptp_format = ATP_Problem.tptp_format
+ type atp_format = ATP_Problem.atp_format
type formula_kind = ATP_Problem.formula_kind
type failure = ATP_Proof.failure
@@ -23,7 +23,7 @@
prem_kind : formula_kind,
best_slices :
Proof.context
- -> (real * (bool * (int * tptp_format * string * string))) list}
+ -> (real * (bool * (int * atp_format * string * string))) list}
val force_sos : bool Config.T
val e_smartN : string
@@ -46,6 +46,7 @@
val satallaxN : string
val snarkN : string
val spassN : string
+ val spass_newN : string
val vampireN : string
val waldmeisterN : string
val z3_tptpN : string
@@ -53,7 +54,7 @@
val remote_atp :
string -> string -> string list -> (string * string) list
-> (failure * string) list -> formula_kind -> formula_kind
- -> (Proof.context -> int * tptp_format * string) -> string * atp_config
+ -> (Proof.context -> int * atp_format * 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
@@ -82,7 +83,7 @@
prem_kind : formula_kind,
best_slices :
Proof.context
- -> (real * (bool * (int * tptp_format * string * string))) list}
+ -> (real * (bool * (int * atp_format * 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
@@ -130,6 +131,7 @@
val satallaxN = "satallax"
val snarkN = "snark"
val spassN = "spass"
+val spass_newN = "spass_new"
val vampireN = "vampire"
val waldmeisterN = "waldmeister"
val z3_tptpN = "z3_tptp"
@@ -315,7 +317,6 @@
(MalformedInput, "Undefined symbol"),
(MalformedInput, "Free Variable"),
(Unprovable, "No formulae and clauses found in input file"),
- (SpassTooOld, "tptp2dfg"),
(InternalError, "Please report this error")],
conj_sym_kind = Hypothesis,
prem_kind = Conjecture,
@@ -329,6 +330,25 @@
val spass = (spassN, spass_config)
+(* Experimental *)
+val spass_new_config : atp_config =
+ {exec = ("SPASS_HOME", "SPASS"),
+ required_execs = [],
+ arguments = #arguments spass_config,
+ proof_delims = #proof_delims spass_config,
+ known_failures = #known_failures spass_config,
+ conj_sym_kind = #conj_sym_kind spass_config,
+ prem_kind = #prem_kind spass_config,
+ best_slices = fn ctxt =>
+ (* FUDGE *)
+ [(0.333, (false, (150, DFG_Sorted, "mono_simple", sosN))) (*,
+ (0.333, (false, (300, DFG_Sorted, "poly_tags??", sosN))),
+ (0.334, (true, (50, DFG_Sorted, "mono_simple", no_sosN)))*)]
+ |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
+ else I)}
+
+val spass_new = (spass_newN, spass_new_config)
+
(* Vampire *)
@@ -359,7 +379,6 @@
(GaveUp, "CANNOT PROVE"),
(Unprovable, "Satisfiability detected"),
(Unprovable, "Termination reason: Satisfiable"),
- (VampireTooOld, "not a valid option"),
(Interrupted, "Aborted by signal SIGINT")],
conj_sym_kind = Conjecture,
prem_kind = Conjecture,
@@ -545,9 +564,9 @@
Synchronized.change systems (fn _ => get_systems ())
val atps =
- [e, leo2, pff, phf, satallax, spass, vampire, z3_tptp, remote_e, remote_leo2,
- remote_satallax, remote_vampire, remote_z3_tptp, remote_e_sine, remote_snark,
- remote_e_tofof, remote_waldmeister]
+ [e, leo2, pff, phf, satallax, spass, spass_new, vampire, z3_tptp, remote_e,
+ remote_leo2, remote_satallax, remote_vampire, remote_z3_tptp, remote_e_sine,
+ remote_snark, remote_e_tofof, remote_waldmeister]
val setup = fold add_atp atps
end;
--- a/src/HOL/Tools/ATP/atp_translate.ML Sat Oct 29 13:15:58 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_translate.ML Sat Oct 29 13:15:58 2011 +0200
@@ -11,7 +11,7 @@
type ('a, 'b) ho_term = ('a, 'b) ATP_Problem.ho_term
type connective = ATP_Problem.connective
type ('a, 'b, 'c) formula = ('a, 'b, 'c) ATP_Problem.formula
- type tptp_format = ATP_Problem.tptp_format
+ type atp_format = ATP_Problem.atp_format
type formula_kind = ATP_Problem.formula_kind
type 'a problem = 'a ATP_Problem.problem
@@ -86,7 +86,7 @@
val is_type_enc_quasi_sound : type_enc -> bool
val is_type_enc_fairly_sound : type_enc -> bool
val type_enc_from_string : soundness -> string -> type_enc
- val adjust_type_enc : tptp_format -> type_enc -> type_enc
+ val adjust_type_enc : atp_format -> type_enc -> type_enc
val mk_aconns :
connective -> ('a, 'b, 'c) formula list -> ('a, 'b, 'c) formula
val unmangled_const : string -> string * (string, 'b) ho_term list
@@ -94,7 +94,7 @@
val helper_table : ((string * bool) * thm list) list
val factsN : string
val prepare_atp_problem :
- Proof.context -> tptp_format -> formula_kind -> formula_kind -> type_enc
+ Proof.context -> atp_format -> formula_kind -> formula_kind -> type_enc
-> bool -> string -> bool -> bool -> term list -> term
-> ((string * locality) * term) list
-> string problem * string Symtab.table * int * int
@@ -123,20 +123,10 @@
val lambdasN = "lambdas"
val smartN = "smart"
-val generate_info = false (* experimental *)
-
-fun isabelle_info s =
- if generate_info then SOME (ATerm ("[]", [ATerm ("isabelle_" ^ s, [])]))
- else NONE
-
-val introN = "intro"
-val elimN = "elim"
-val simpN = "simp"
-
(* TFF1 is still in development, and it is still unclear whether symbols will be
allowed to have types like "$tType > $o" (i.e., "![A : $tType] : $o"), with
- "dummy" type variables. *)
-val avoid_first_order_dummy_type_vars = true
+ ghost type variables. *)
+val avoid_first_order_ghost_type_vars = true
val bound_var_prefix = "B_"
val all_bound_var_prefix = "BA_"
@@ -313,7 +303,7 @@
tvar_prefix ^ (ascii_of_indexname (unprefix "'" x, i))
fun make_fixed_type_var x = tfree_prefix ^ (ascii_of (unprefix "'" x))
-(* "HOL.eq" and Choice are mapped to the ATP's equivalents *)
+(* "HOL.eq" and choice are mapped to the ATP's equivalents *)
local
val choice_const = (fst o dest_Const o HOLogic.choice_const) Term.dummyT
fun default c = const_prefix ^ lookup_const c
@@ -650,6 +640,8 @@
| adjust_type_enc (THF _) type_enc = type_enc
| adjust_type_enc (TFF (TPTP_Monomorphic, _)) (Simple_Types (_, _, level)) =
Simple_Types (First_Order, Mangled_Monomorphic, level)
+ | adjust_type_enc DFG_Sorted (Simple_Types (_, _, level)) =
+ Simple_Types (First_Order, Mangled_Monomorphic, level)
| adjust_type_enc (TFF _) (Simple_Types (_, poly, level)) =
Simple_Types (First_Order, poly, level)
| adjust_type_enc format (Simple_Types (_, poly, level)) =
@@ -755,7 +747,7 @@
AAtom (ATerm (class, arg ::
(case type_enc of
Simple_Types (First_Order, Polymorphic, _) =>
- if avoid_first_order_dummy_type_vars then [ATerm (TYPE_name, [arg])]
+ if avoid_first_order_ghost_type_vars then [ATerm (TYPE_name, [arg])]
else []
| _ => [])))
fun formulas_for_types type_enc add_sorts_on_typ Ts =
@@ -1545,7 +1537,7 @@
val type_tag = `(make_fixed_const NONE) type_tag_name
-fun type_tag_idempotence_fact type_enc =
+fun type_tag_idempotence_fact format type_enc =
let
fun var s = ATerm (`I s, [])
fun tag tm = ATerm (type_tag, [var "A", tm])
@@ -1553,7 +1545,7 @@
in
Formula (type_tag_idempotence_helper_name, Axiom,
eq_formula type_enc [] false (tag tagged_var) tagged_var,
- isabelle_info simpN, NONE)
+ isabelle_info format simpN, NONE)
end
fun should_specialize_helper type_enc t =
@@ -1833,32 +1825,34 @@
|> close_formula_universally type_enc,
NONE,
case locality of
- Intro => isabelle_info introN
- | Elim => isabelle_info elimN
- | Simp => isabelle_info simpN
+ Intro => isabelle_info format introN
+ | Elim => isabelle_info format elimN
+ | Simp => isabelle_info format simpN
| _ => NONE)
|> Formula
-fun formula_line_for_class_rel_clause type_enc
+fun formula_line_for_class_rel_clause format type_enc
({name, subclass, superclass, ...} : class_rel_clause) =
let val ty_arg = ATerm (tvar_a_name, []) in
Formula (class_rel_clause_prefix ^ ascii_of name, Axiom,
AConn (AImplies,
[type_class_formula type_enc subclass ty_arg,
type_class_formula type_enc superclass ty_arg])
- |> close_formula_universally type_enc, isabelle_info introN, NONE)
+ |> close_formula_universally type_enc,
+ isabelle_info format introN, NONE)
end
fun formula_from_arity_atom type_enc (class, t, args) =
ATerm (t, map (fn arg => ATerm (arg, [])) args)
|> type_class_formula type_enc class
-fun formula_line_for_arity_clause type_enc
+fun formula_line_for_arity_clause format type_enc
({name, prem_atoms, concl_atom, ...} : arity_clause) =
Formula (arity_clause_prefix ^ name, Axiom,
mk_ahorn (map (formula_from_arity_atom type_enc) prem_atoms)
(formula_from_arity_atom type_enc concl_atom)
- |> close_formula_universally type_enc, isabelle_info introN, NONE)
+ |> close_formula_universally type_enc,
+ isabelle_info format introN, NONE)
fun formula_line_for_conjecture ctxt format mono type_enc
({name, kind, iformula, atomic_types, ...} : translated_formula) =
@@ -1883,7 +1877,7 @@
fun decl_line_for_class order s =
let val name as (s, _) = `make_type_class s in
Decl (sym_decl_prefix ^ s, name,
- if order = First_Order andalso avoid_first_order_dummy_type_vars then
+ if order = First_Order andalso avoid_first_order_ghost_type_vars then
ATyAbs ([tvar_a_name], AFun (a_itself_atype, bool_atype))
else
AFun (atype_of_types, bool_atype))
@@ -2059,7 +2053,7 @@
(K (K (K (K (K (K true)))))) (SOME true)
|> bound_tvars type_enc (atyps_of T)
|> close_formula_universally type_enc,
- isabelle_info introN, NONE)
+ isabelle_info format introN, NONE)
fun formula_line_for_tags_mono_type ctxt format mono type_enc T =
let val x_var = ATerm (`make_bound_var "X", []) in
@@ -2069,7 +2063,7 @@
eq_formula type_enc (atyps_of T) false
(tag_with_type ctxt format mono type_enc NONE T x_var)
x_var,
- isabelle_info simpN, NONE)
+ isabelle_info format simpN, NONE)
end
fun problem_lines_for_mono_types ctxt format mono type_enc Ts =
@@ -2143,7 +2137,7 @@
|> n > 1 ? bound_tvars type_enc (atyps_of T)
|> close_formula_universally type_enc
|> maybe_negate,
- isabelle_info introN, NONE)
+ isabelle_info format introN, NONE)
end
fun formula_lines_for_tags_sym_decl ctxt format conj_sym_kind mono type_enc n s
@@ -2179,7 +2173,7 @@
in
cons (Formula (ident_base ^ "_res", kind,
eq (tag_with res_T (cst bounds)) (cst tagged_bounds),
- isabelle_info simpN, NONE))
+ isabelle_info format simpN, NONE))
end
else
I
@@ -2191,7 +2185,7 @@
cons (Formula (ident_base ^ "_arg" ^ string_of_int (k + 1), kind,
eq (cst (bounds1 @ tag_with arg_T bound :: bounds2))
(cst bounds),
- isabelle_info simpN, NONE))
+ isabelle_info format simpN, NONE))
| _ => raise Fail "expected nonempty tail"
else
I
@@ -2343,7 +2337,7 @@
|> map (formula_line_for_fact ctxt format helper_prefix I false true mono
type_enc)
|> (if needs_type_tag_idempotence ctxt type_enc then
- cons (type_tag_idempotence_fact type_enc)
+ cons (type_tag_idempotence_fact format type_enc)
else
I)
(* Reordering these might confuse the proof reconstruction code or the SPASS
@@ -2355,8 +2349,10 @@
(not exporter) (not exporter) mono type_enc)
(0 upto length facts - 1 ~~ facts)),
(class_relsN,
- map (formula_line_for_class_rel_clause type_enc) class_rel_clauses),
- (aritiesN, map (formula_line_for_arity_clause type_enc) arity_clauses),
+ map (formula_line_for_class_rel_clause format type_enc)
+ class_rel_clauses),
+ (aritiesN,
+ map (formula_line_for_arity_clause format type_enc) arity_clauses),
(helpersN, helper_lines),
(conjsN,
map (formula_line_for_conjecture ctxt format mono type_enc) conjs),
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Sat Oct 29 13:15:58 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Sat Oct 29 13:15:58 2011 +0200
@@ -799,28 +799,28 @@
is_that_fact thm
end)
-fun meta_equify (@{const Trueprop}
- $ (Const (@{const_name HOL.eq}, Type (_, [T, _])) $ t1 $ t2)) =
- Const (@{const_name "=="}, T --> T --> @{typ prop}) $ t1 $ t2
- | meta_equify t = t
-
-val normalize_simp_prop =
- meta_equify
- #> map_aterms (fn Var ((s, _), T) => Var ((s, 0), T) | t => t)
+val crude_zero_vars =
+ map_aterms (fn Var ((s, _), T) => Var ((s, 0), T) | t => t)
#> map_types (map_type_tvar (fn ((s, _), S) => TVar ((s, 0), S)))
fun clasimpset_rule_table_of ctxt =
let
- fun add loc g f = fold (Termtab.update o rpair loc o g o prop_of o f)
- val {safeIs, safeEs, hazIs, hazEs, ...} = ctxt |> claset_of |> Classical.rep_cs
+ val thy = Proof_Context.theory_of ctxt
+ val atomize = HOLogic.mk_Trueprop o Object_Logic.atomize_term thy
+ fun add loc g f =
+ fold (Termtab.update o rpair loc o g o crude_zero_vars o prop_of o f)
+ val {safeIs, safeEs, hazIs, hazEs, ...} =
+ ctxt |> claset_of |> Classical.rep_cs
val intros = Item_Net.content safeIs @ Item_Net.content hazIs
- val elims = map Classical.classical_rule (Item_Net.content safeEs @ Item_Net.content hazEs)
+ val elims =
+ Item_Net.content safeEs @ Item_Net.content hazEs
+ |> map Classical.classical_rule
val simps = ctxt |> simpset_of |> dest_ss |> #simps
in
Termtab.empty |> add Intro I I intros
|> add Elim I I elims
|> add Simp I snd simps
- |> add Simp normalize_simp_prop snd simps
+ |> add Simp atomize snd simps
end
fun all_facts ctxt ho_atp reserved exporter add_ths chained_ths =
@@ -833,17 +833,20 @@
fun is_assum th = exists (fn ct => prop_of th aconv term_of ct) assms
val is_chained = member Thm.eq_thm_prop chained_ths
val clasimpset_table = clasimpset_rule_table_of ctxt
- fun locality_of_theorem global (name: string) th =
- if String.isSubstring ".induct" name orelse(*FIXME: use structured name*)
+ fun locality_of_theorem global name th =
+ if String.isSubstring ".induct" name orelse (*FIXME: use structured name*)
String.isSubstring ".inducts" name then
- Induction
+ Induction
else if is_chained th then
Chained
else if global then
case Termtab.lookup clasimpset_table (prop_of th) of
SOME loc => loc
| NONE => General
- else if is_assum th then Assum else Local
+ else if is_assum th then
+ Assum
+ else
+ Local
fun is_good_unnamed_local th =
not (Thm.has_name_hint th) andalso
forall (fn (_, ths) => not (member Thm.eq_thm_prop ths th)) named_locals
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Sat Oct 29 13:15:58 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Sat Oct 29 13:15:58 2011 +0200
@@ -659,11 +659,9 @@
arguments ctxt full_proof extra slice_timeout weights ^ " " ^
File.shell_path prob_file
val command = "TIMEFORMAT='%3R'; { time " ^ core ^ " ; } 2>&1"
- val _ =
- atp_problem
- |> tptp_lines_for_atp_problem format
- |> cons ("% " ^ command ^ "\n")
- |> File.write_list prob_file
+ val _ = atp_problem |> lines_for_atp_problem format
+ |> cons ("% " ^ command ^ "\n")
+ |> File.write_list prob_file
val conjecture_shape =
conjecture_offset + 1
upto conjecture_offset + length hyp_ts + 1