--- a/src/HOL/Tools/ATP_Manager/atp_manager.ML Wed Apr 14 21:22:48 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML Thu Apr 15 13:49:46 2010 +0200
@@ -223,7 +223,7 @@
do
(Synchronized.timed_access global_state (SOME o time_limit o #timeout_heap) action
|> these
- |> List.app (unregister "Interrupted (reached timeout)");
+ |> List.app (unregister "Timed out.");
print_new_messages ();
(*give threads some time to respond to interrupt*)
OS.Process.sleep min_wait_time)
@@ -325,7 +325,7 @@
fun start_prover (params as {timeout, ...}) birth_time death_time i
relevance_override proof_state name =
(case get_prover (Proof.theory_of proof_state) name of
- NONE => warning ("Unknown ATP: " ^ quote name)
+ NONE => warning ("Unknown ATP: " ^ quote name ^ ".")
| SOME prover =>
let
val {context = ctxt, facts, goal} = Proof.goal proof_state;
@@ -357,7 +357,10 @@
let
val birth_time = Time.now ()
val death_time = Time.+ (birth_time, timeout)
- val _ = kill_atps () (* RACE w.r.t. other invocations of Sledgehammer *)
+ val _ =
+ (* RACE w.r.t. other invocations of Sledgehammer *)
+ if null (#active (Synchronized.value global_state)) then ()
+ else (kill_atps (); priority "Killed active Sledgehammer threads.")
val _ = priority "Sledgehammering..."
val _ = List.app (start_prover params birth_time death_time i
relevance_override proof_state) atps
--- a/src/HOL/Tools/ATP_Manager/atp_wrapper.ML Wed Apr 14 21:22:48 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_wrapper.ML Thu Apr 15 13:49:46 2010 +0200
@@ -129,9 +129,10 @@
if File.exists cmd then
write full_types probfile clauses
|> pair (apfst split_time' (bash_output (cmd_line probfile)))
- else error ("Bad executable: " ^ Path.implode cmd);
+ else error ("Bad executable: " ^ Path.implode cmd ^ ".");
- (* if problemfile has not been exported, delete problemfile; otherwise export proof, too *)
+ (* If the problem file has not been exported, remove it; otherwise, export
+ the proof file too. *)
fun cleanup probfile = if destdir' = "" then try File.rm probfile else NONE;
fun export probfile (((proof, _), _), _) =
if destdir' = "" then ()
@@ -140,12 +141,12 @@
val (((proof, atp_run_time_in_msecs), rc), conj_pos) =
with_path cleanup export run_on (prob_pathname subgoal);
- (* check for success and print out some information on failure *)
+ (* Check for success and print out some information on failure. *)
val failure = find_failure failure_strs proof;
val success = rc = 0 andalso is_none failure;
val (message, relevant_thm_names) =
- if is_some failure then ("External prover failed.", [])
- else if rc <> 0 then ("External prover failed: " ^ proof, [])
+ if is_some failure then ("ATP failed to find a proof.", [])
+ else if rc <> 0 then ("ATP error: " ^ proof ^ ".", [])
else
(produce_answer name (proof, internal_thm_names, conj_pos, ctxt, th,
subgoal));
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML Wed Apr 14 21:22:48 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML Thu Apr 15 13:49:46 2010 +0200
@@ -495,22 +495,24 @@
(**** Produce TPTP files ****)
-(*Attach sign in TPTP syntax: false means negate.*)
fun tptp_sign true s = s
| tptp_sign false s = "~ " ^ s
-fun tptp_of_typeLit pos (LTVar (s,ty)) = tptp_sign pos (s ^ "(" ^ ty ^ ")")
- | tptp_of_typeLit pos (LTFree (s,ty)) = tptp_sign pos (s ^ "(" ^ ty ^ ")");
+fun tptp_of_typeLit pos (LTVar (s, ty)) = tptp_sign pos (s ^ "(" ^ ty ^ ")")
+ | tptp_of_typeLit pos (LTFree (s, ty)) = tptp_sign pos (s ^ "(" ^ ty ^ ")")
+
+fun tptp_cnf name kind formula =
+ "cnf(" ^ name ^ ", " ^ kind ^ ",\n " ^ formula ^ ").\n"
-fun gen_tptp_cls (cls_id,ax_name,Axiom,lits,tylits) =
- "cnf(" ^ string_of_clausename (cls_id,ax_name) ^ ",axiom," ^
- tptp_pack (tylits@lits) ^ ").\n"
- | gen_tptp_cls (cls_id,ax_name,Conjecture,lits,_) =
- "cnf(" ^ string_of_clausename (cls_id,ax_name) ^ ",negated_conjecture," ^
- tptp_pack lits ^ ").\n";
+fun gen_tptp_cls (cls_id, ax_name, Axiom, lits, tylits) =
+ tptp_cnf (string_of_clausename (cls_id, ax_name)) "axiom"
+ (tptp_pack (tylits @ lits))
+ | gen_tptp_cls (cls_id, ax_name, Conjecture, lits, _) =
+ tptp_cnf (string_of_clausename (cls_id, ax_name)) "negated_conjecture"
+ (tptp_pack lits)
fun tptp_tfree_clause tfree_lit =
- "cnf(" ^ "tfree_tcs," ^ "negated_conjecture" ^ "," ^ tptp_pack[tfree_lit] ^ ").\n";
+ tptp_cnf "tfree_tcs" "negated_conjecture" (tptp_pack [tfree_lit])
fun tptp_of_arLit (TConsLit (c,t,args)) =
tptp_sign true (make_type_class c ^ "(" ^ t ^ paren_pack args ^ ")")
@@ -518,14 +520,14 @@
tptp_sign false (make_type_class c ^ "(" ^ str ^ ")")
fun tptp_arity_clause (ArityClause{axiom_name,conclLit,premLits,...}) =
- "cnf(" ^ string_of_ar axiom_name ^ ",axiom," ^
- tptp_pack (map tptp_of_arLit (conclLit :: premLits)) ^ ").\n";
+ tptp_cnf (string_of_ar axiom_name) "axiom"
+ (tptp_pack (map tptp_of_arLit (conclLit :: premLits)))
fun tptp_classrelLits sub sup =
let val tvar = "(T)"
in tptp_pack [tptp_sign false (sub^tvar), tptp_sign true (sup^tvar)] end;
fun tptp_classrel_clause (ClassrelClause {axiom_name,subclass,superclass,...}) =
- "cnf(" ^ axiom_name ^ ",axiom," ^ tptp_classrelLits subclass superclass ^ ").\n"
+ tptp_cnf axiom_name "axiom" (tptp_classrelLits subclass superclass)
end;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML Wed Apr 14 21:22:48 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML Thu Apr 15 13:49:46 2010 +0200
@@ -45,6 +45,7 @@
structure Sledgehammer_HOL_Clause : SLEDGEHAMMER_HOL_CLAUSE =
struct
+open Sledgehammer_Util
open Sledgehammer_FOL_Clause
open Sledgehammer_Fact_Preprocessor
@@ -453,20 +454,26 @@
fun write_tptp_file full_types file clauses =
let
+ fun section _ [] = []
+ | section name ss = "\n% " ^ name ^ plural_s (length ss) ^ "\n" :: ss
val (conjectures, axclauses, _, helper_clauses,
classrel_clauses, arity_clauses) = clauses
val (cma, cnh) = count_constants clauses
val params = (full_types, cma, cnh)
val (tptp_clss,tfree_litss) = ListPair.unzip (map (clause2tptp params) conjectures)
val tfree_clss = map tptp_tfree_clause (List.foldl (uncurry (union (op =))) [] tfree_litss)
+ val timestamp = Date.fmt "%Y-%m-%d %H:%M:%S" (Date.fromTimeLocal (Time.now ()))
val _ =
File.write_list file (
- map (#1 o (clause2tptp params)) axclauses @
- tfree_clss @
- tptp_clss @
- map tptp_classrel_clause classrel_clauses @
- map tptp_arity_clause arity_clauses @
- map (#1 o (clause2tptp params)) helper_clauses)
+ "% This file was generated by Isabelle (most likely Sledgehammer)\n" ^
+ "% " ^ timestamp ^ "\n" ::
+ section "Relevant fact" (map (#1 o (clause2tptp params)) axclauses) @
+ section "Type variable" tfree_clss @
+ section "Class relationship"
+ (map tptp_classrel_clause classrel_clauses) @
+ section "Arity declaration" (map tptp_arity_clause arity_clauses) @
+ section "Helper fact" (map (#1 o (clause2tptp params)) helper_clauses) @
+ section "Conjecture" tptp_clss)
in (length axclauses + 1, length tfree_clss + length tptp_clss)
end;
@@ -492,17 +499,17 @@
string_of_descrip probname ::
string_of_symbols (string_of_funcs funcs)
(string_of_preds (cl_preds @ ty_preds)) ::
- "list_of_clauses(axioms,cnf).\n" ::
+ "list_of_clauses(axioms, cnf).\n" ::
axstrs @
map dfg_classrel_clause classrel_clauses @
map dfg_arity_clause arity_clauses @
helper_clauses_strs @
- ["end_of_list.\n\nlist_of_clauses(conjectures,cnf).\n"] @
+ ["end_of_list.\n\nlist_of_clauses(conjectures, cnf).\n"] @
tfree_clss @
dfg_clss @
["end_of_list.\n\n",
(*VarWeight=3 helps the HO problems, probably by counteracting the presence of hAPP*)
- "list_of_settings(SPASS).\n{*\nset_flag(VarWeight,3).\n*}\nend_of_list.\n\n",
+ "list_of_settings(SPASS).\n{*\nset_flag(VarWeight, 3).\n*}\nend_of_list.\n\n",
"end_problem.\n"])
in (length axclauses + length classrel_clauses + length arity_clauses +