# HG changeset patch # User blanchet # Date 1271332186 -7200 # Node ID c1a35be8e4762f065fad18bdb5eb526c62b4b927 # Parent e8db171b86432960fbf1f08b9debcea947039ea6 make Sledgehammer's output more debugging friendly diff -r e8db171b8643 -r c1a35be8e476 src/HOL/Tools/ATP_Manager/atp_manager.ML --- 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 diff -r e8db171b8643 -r c1a35be8e476 src/HOL/Tools/ATP_Manager/atp_wrapper.ML --- 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)); diff -r e8db171b8643 -r c1a35be8e476 src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML --- 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; diff -r e8db171b8643 -r c1a35be8e476 src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML --- 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 +