make Sledgehammer's output more debugging friendly
authorblanchet
Thu Apr 15 13:49:46 2010 +0200 (2010-04-15)
changeset 36167c1a35be8e476
parent 36144 e8db171b8643
child 36168 0a6ed065683d
make Sledgehammer's output more debugging friendly
src/HOL/Tools/ATP_Manager/atp_manager.ML
src/HOL/Tools/ATP_Manager/atp_wrapper.ML
src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML
src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML
     1.1 --- a/src/HOL/Tools/ATP_Manager/atp_manager.ML	Wed Apr 14 21:22:48 2010 +0200
     1.2 +++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML	Thu Apr 15 13:49:46 2010 +0200
     1.3 @@ -223,7 +223,7 @@
     1.4          do
     1.5            (Synchronized.timed_access global_state (SOME o time_limit o #timeout_heap) action
     1.6              |> these
     1.7 -            |> List.app (unregister "Interrupted (reached timeout)");
     1.8 +            |> List.app (unregister "Timed out.");
     1.9              print_new_messages ();
    1.10              (*give threads some time to respond to interrupt*)
    1.11              OS.Process.sleep min_wait_time)
    1.12 @@ -325,7 +325,7 @@
    1.13  fun start_prover (params as {timeout, ...}) birth_time death_time i
    1.14                   relevance_override proof_state name =
    1.15    (case get_prover (Proof.theory_of proof_state) name of
    1.16 -    NONE => warning ("Unknown ATP: " ^ quote name)
    1.17 +    NONE => warning ("Unknown ATP: " ^ quote name ^ ".")
    1.18    | SOME prover =>
    1.19        let
    1.20          val {context = ctxt, facts, goal} = Proof.goal proof_state;
    1.21 @@ -357,7 +357,10 @@
    1.22    let
    1.23      val birth_time = Time.now ()
    1.24      val death_time = Time.+ (birth_time, timeout)
    1.25 -    val _ = kill_atps () (* RACE w.r.t. other invocations of Sledgehammer *)
    1.26 +    val _ =
    1.27 +      (* RACE w.r.t. other invocations of Sledgehammer *)
    1.28 +      if null (#active (Synchronized.value global_state)) then ()
    1.29 +      else (kill_atps (); priority "Killed active Sledgehammer threads.")
    1.30      val _ = priority "Sledgehammering..."
    1.31      val _ = List.app (start_prover params birth_time death_time i
    1.32                                     relevance_override proof_state) atps
     2.1 --- a/src/HOL/Tools/ATP_Manager/atp_wrapper.ML	Wed Apr 14 21:22:48 2010 +0200
     2.2 +++ b/src/HOL/Tools/ATP_Manager/atp_wrapper.ML	Thu Apr 15 13:49:46 2010 +0200
     2.3 @@ -129,9 +129,10 @@
     2.4        if File.exists cmd then
     2.5          write full_types probfile clauses
     2.6          |> pair (apfst split_time' (bash_output (cmd_line probfile)))
     2.7 -      else error ("Bad executable: " ^ Path.implode cmd);
     2.8 +      else error ("Bad executable: " ^ Path.implode cmd ^ ".");
     2.9  
    2.10 -    (* if problemfile has not been exported, delete problemfile; otherwise export proof, too *)
    2.11 +    (* If the problem file has not been exported, remove it; otherwise, export
    2.12 +       the proof file too. *)
    2.13      fun cleanup probfile = if destdir' = "" then try File.rm probfile else NONE;
    2.14      fun export probfile (((proof, _), _), _) =
    2.15        if destdir' = "" then ()
    2.16 @@ -140,12 +141,12 @@
    2.17      val (((proof, atp_run_time_in_msecs), rc), conj_pos) =
    2.18        with_path cleanup export run_on (prob_pathname subgoal);
    2.19  
    2.20 -    (* check for success and print out some information on failure *)
    2.21 +    (* Check for success and print out some information on failure. *)
    2.22      val failure = find_failure failure_strs proof;
    2.23      val success = rc = 0 andalso is_none failure;
    2.24      val (message, relevant_thm_names) =
    2.25 -      if is_some failure then ("External prover failed.", [])
    2.26 -      else if rc <> 0 then ("External prover failed: " ^ proof, [])
    2.27 +      if is_some failure then ("ATP failed to find a proof.", [])
    2.28 +      else if rc <> 0 then ("ATP error: " ^ proof ^ ".", [])
    2.29        else
    2.30          (produce_answer name (proof, internal_thm_names, conj_pos, ctxt, th,
    2.31                                subgoal));
     3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML	Wed Apr 14 21:22:48 2010 +0200
     3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML	Thu Apr 15 13:49:46 2010 +0200
     3.3 @@ -495,22 +495,24 @@
     3.4  
     3.5  (**** Produce TPTP files ****)
     3.6  
     3.7 -(*Attach sign in TPTP syntax: false means negate.*)
     3.8  fun tptp_sign true s = s
     3.9    | tptp_sign false s = "~ " ^ s
    3.10  
    3.11 -fun tptp_of_typeLit pos (LTVar (s,ty))  = tptp_sign pos (s ^ "(" ^ ty ^ ")")
    3.12 -  | tptp_of_typeLit pos (LTFree (s,ty)) = tptp_sign pos  (s ^ "(" ^ ty ^ ")");
    3.13 +fun tptp_of_typeLit pos (LTVar (s, ty))  = tptp_sign pos (s ^ "(" ^ ty ^ ")")
    3.14 +  | tptp_of_typeLit pos (LTFree (s, ty)) = tptp_sign pos (s ^ "(" ^ ty ^ ")")
    3.15 +
    3.16 +fun tptp_cnf name kind formula =
    3.17 +  "cnf(" ^ name ^ ", " ^ kind ^ ",\n    " ^ formula ^ ").\n"
    3.18  
    3.19 -fun gen_tptp_cls (cls_id,ax_name,Axiom,lits,tylits) =
    3.20 -      "cnf(" ^ string_of_clausename (cls_id,ax_name) ^ ",axiom," ^ 
    3.21 -               tptp_pack (tylits@lits) ^ ").\n"
    3.22 -  | gen_tptp_cls (cls_id,ax_name,Conjecture,lits,_) =
    3.23 -      "cnf(" ^ string_of_clausename (cls_id,ax_name) ^ ",negated_conjecture," ^ 
    3.24 -               tptp_pack lits ^ ").\n";
    3.25 +fun gen_tptp_cls (cls_id, ax_name, Axiom, lits, tylits) =
    3.26 +      tptp_cnf (string_of_clausename (cls_id, ax_name)) "axiom"
    3.27 +               (tptp_pack (tylits @ lits))
    3.28 +  | gen_tptp_cls (cls_id, ax_name, Conjecture, lits, _) =
    3.29 +      tptp_cnf (string_of_clausename (cls_id, ax_name)) "negated_conjecture"
    3.30 +               (tptp_pack lits)
    3.31  
    3.32  fun tptp_tfree_clause tfree_lit =
    3.33 -    "cnf(" ^ "tfree_tcs," ^ "negated_conjecture" ^ "," ^ tptp_pack[tfree_lit] ^ ").\n";
    3.34 +    tptp_cnf "tfree_tcs" "negated_conjecture" (tptp_pack [tfree_lit])
    3.35  
    3.36  fun tptp_of_arLit (TConsLit (c,t,args)) =
    3.37        tptp_sign true (make_type_class c ^ "(" ^ t ^ paren_pack args ^ ")")
    3.38 @@ -518,14 +520,14 @@
    3.39        tptp_sign false (make_type_class c ^ "(" ^ str ^ ")")
    3.40  
    3.41  fun tptp_arity_clause (ArityClause{axiom_name,conclLit,premLits,...}) =
    3.42 -  "cnf(" ^ string_of_ar axiom_name ^ ",axiom," ^
    3.43 -  tptp_pack (map tptp_of_arLit (conclLit :: premLits)) ^ ").\n";
    3.44 +  tptp_cnf (string_of_ar axiom_name) "axiom"
    3.45 +           (tptp_pack (map tptp_of_arLit (conclLit :: premLits)))
    3.46  
    3.47  fun tptp_classrelLits sub sup =
    3.48    let val tvar = "(T)"
    3.49    in  tptp_pack [tptp_sign false (sub^tvar), tptp_sign true (sup^tvar)]  end;
    3.50  
    3.51  fun tptp_classrel_clause (ClassrelClause {axiom_name,subclass,superclass,...}) =
    3.52 -  "cnf(" ^ axiom_name ^ ",axiom," ^ tptp_classrelLits subclass superclass ^ ").\n"
    3.53 +  tptp_cnf axiom_name "axiom" (tptp_classrelLits subclass superclass)
    3.54  
    3.55  end;
     4.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML	Wed Apr 14 21:22:48 2010 +0200
     4.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML	Thu Apr 15 13:49:46 2010 +0200
     4.3 @@ -45,6 +45,7 @@
     4.4  structure Sledgehammer_HOL_Clause : SLEDGEHAMMER_HOL_CLAUSE =
     4.5  struct
     4.6  
     4.7 +open Sledgehammer_Util
     4.8  open Sledgehammer_FOL_Clause
     4.9  open Sledgehammer_Fact_Preprocessor
    4.10  
    4.11 @@ -453,20 +454,26 @@
    4.12  
    4.13  fun write_tptp_file full_types file clauses =
    4.14    let
    4.15 +    fun section _ [] = []
    4.16 +      | section name ss = "\n% " ^ name ^ plural_s (length ss) ^ "\n" :: ss
    4.17      val (conjectures, axclauses, _, helper_clauses,
    4.18        classrel_clauses, arity_clauses) = clauses
    4.19      val (cma, cnh) = count_constants clauses
    4.20      val params = (full_types, cma, cnh)
    4.21      val (tptp_clss,tfree_litss) = ListPair.unzip (map (clause2tptp params) conjectures)
    4.22      val tfree_clss = map tptp_tfree_clause (List.foldl (uncurry (union (op =))) [] tfree_litss)
    4.23 +    val timestamp = Date.fmt "%Y-%m-%d %H:%M:%S" (Date.fromTimeLocal (Time.now ()))
    4.24      val _ =
    4.25        File.write_list file (
    4.26 -        map (#1 o (clause2tptp params)) axclauses @
    4.27 -        tfree_clss @
    4.28 -        tptp_clss @
    4.29 -        map tptp_classrel_clause classrel_clauses @
    4.30 -        map tptp_arity_clause arity_clauses @
    4.31 -        map (#1 o (clause2tptp params)) helper_clauses)
    4.32 +        "% This file was generated by Isabelle (most likely Sledgehammer)\n" ^
    4.33 +        "% " ^ timestamp ^ "\n" ::
    4.34 +        section "Relevant fact" (map (#1 o (clause2tptp params)) axclauses) @
    4.35 +        section "Type variable" tfree_clss @
    4.36 +        section "Class relationship"
    4.37 +                (map tptp_classrel_clause classrel_clauses) @
    4.38 +        section "Arity declaration" (map tptp_arity_clause arity_clauses) @
    4.39 +        section "Helper fact" (map (#1 o (clause2tptp params)) helper_clauses) @
    4.40 +        section "Conjecture" tptp_clss)
    4.41      in (length axclauses + 1, length tfree_clss + length tptp_clss)
    4.42    end;
    4.43  
    4.44 @@ -492,17 +499,17 @@
    4.45          string_of_descrip probname ::
    4.46          string_of_symbols (string_of_funcs funcs)
    4.47            (string_of_preds (cl_preds @ ty_preds)) ::
    4.48 -        "list_of_clauses(axioms,cnf).\n" ::
    4.49 +        "list_of_clauses(axioms, cnf).\n" ::
    4.50          axstrs @
    4.51          map dfg_classrel_clause classrel_clauses @
    4.52          map dfg_arity_clause arity_clauses @
    4.53          helper_clauses_strs @
    4.54 -        ["end_of_list.\n\nlist_of_clauses(conjectures,cnf).\n"] @
    4.55 +        ["end_of_list.\n\nlist_of_clauses(conjectures, cnf).\n"] @
    4.56          tfree_clss @
    4.57          dfg_clss @
    4.58          ["end_of_list.\n\n",
    4.59          (*VarWeight=3 helps the HO problems, probably by counteracting the presence of hAPP*)
    4.60 -         "list_of_settings(SPASS).\n{*\nset_flag(VarWeight,3).\n*}\nend_of_list.\n\n",
    4.61 +         "list_of_settings(SPASS).\n{*\nset_flag(VarWeight, 3).\n*}\nend_of_list.\n\n",
    4.62           "end_problem.\n"])
    4.63  
    4.64      in (length axclauses + length classrel_clauses + length arity_clauses +