src/HOL/Tools/Sledgehammer/sledgehammer.ML
author blanchet
Wed Sep 08 16:01:06 2010 +0200 (2010-09-08)
changeset 39223 022f16801e4e
parent 39155 3e94ebe282f1
parent 39220 8420a873f534
child 39262 bdfcf2434601
permissions -rw-r--r--
merge
     1 (*  Title:      HOL/Tools/Sledgehammer/sledgehammer.ML
     2     Author:     Fabian Immler, TU Muenchen
     3     Author:     Makarius
     4     Author:     Jasmin Blanchette, TU Muenchen
     5 
     6 Sledgehammer's heart.
     7 *)
     8 
     9 signature SLEDGEHAMMER =
    10 sig
    11   type failure = ATP_Systems.failure
    12   type locality = Sledgehammer_Filter.locality
    13   type relevance_override = Sledgehammer_Filter.relevance_override
    14   type fol_formula = Sledgehammer_Translate.fol_formula
    15   type minimize_command = Sledgehammer_Reconstruct.minimize_command
    16   type params =
    17     {blocking: bool,
    18      debug: bool,
    19      verbose: bool,
    20      overlord: bool,
    21      atps: string list,
    22      full_types: bool,
    23      explicit_apply: bool,
    24      relevance_thresholds: real * real,
    25      max_relevant: int option,
    26      isar_proof: bool,
    27      isar_shrink_factor: int,
    28      timeout: Time.time,
    29      expect: string}
    30   type problem =
    31     {ctxt: Proof.context,
    32      goal: thm,
    33      subgoal: int,
    34      axioms: (term * ((string * locality) * fol_formula) option) list}
    35   type prover_result =
    36     {outcome: failure option,
    37      message: string,
    38      pool: string Symtab.table,
    39      used_thm_names: (string * locality) list,
    40      atp_run_time_in_msecs: int,
    41      output: string,
    42      proof: string,
    43      axiom_names: (string * locality) list vector,
    44      conjecture_shape: int list list}
    45   type prover = params -> minimize_command -> problem -> prover_result
    46 
    47   val dest_dir : string Config.T
    48   val problem_prefix : string Config.T
    49   val measure_run_time : bool Config.T
    50   val kill_atps: unit -> unit
    51   val running_atps: unit -> unit
    52   val messages: int option -> unit
    53   val get_prover_fun : theory -> string -> prover
    54   val run_sledgehammer :
    55     params -> int -> relevance_override -> (string -> minimize_command)
    56     -> Proof.state -> unit
    57   val setup : theory -> theory
    58 end;
    59 
    60 structure Sledgehammer : SLEDGEHAMMER =
    61 struct
    62 
    63 open ATP_Problem
    64 open ATP_Systems
    65 open Metis_Clauses
    66 open Sledgehammer_Util
    67 open Sledgehammer_Filter
    68 open Sledgehammer_Translate
    69 open Sledgehammer_Reconstruct
    70 
    71 
    72 (** The Sledgehammer **)
    73 
    74 (* Identifier to distinguish Sledgehammer from other tools using
    75    "Async_Manager". *)
    76 val das_Tool = "Sledgehammer"
    77 
    78 fun kill_atps () = Async_Manager.kill_threads das_Tool "ATPs"
    79 fun running_atps () = Async_Manager.running_threads das_Tool "ATPs"
    80 val messages = Async_Manager.thread_messages das_Tool "ATP"
    81 
    82 (** problems, results, provers, etc. **)
    83 
    84 type params =
    85   {blocking: bool,
    86    debug: bool,
    87    verbose: bool,
    88    overlord: bool,
    89    atps: string list,
    90    full_types: bool,
    91    explicit_apply: bool,
    92    relevance_thresholds: real * real,
    93    max_relevant: int option,
    94    isar_proof: bool,
    95    isar_shrink_factor: int,
    96    timeout: Time.time,
    97    expect: string}
    98 
    99 type problem =
   100   {ctxt: Proof.context,
   101    goal: thm,
   102    subgoal: int,
   103    axioms: (term * ((string * locality) * fol_formula) option) list}
   104 
   105 type prover_result =
   106   {outcome: failure option,
   107    message: string,
   108    pool: string Symtab.table,
   109    used_thm_names: (string * locality) list,
   110    atp_run_time_in_msecs: int,
   111    output: string,
   112    proof: string,
   113    axiom_names: (string * locality) list vector,
   114    conjecture_shape: int list list}
   115 
   116 type prover = params -> minimize_command -> problem -> prover_result
   117 
   118 (* configuration attributes *)
   119 
   120 val (dest_dir, dest_dir_setup) =
   121   Attrib.config_string "sledgehammer_dest_dir" (K "")
   122   (* Empty string means create files in Isabelle's temporary files directory. *)
   123 
   124 val (problem_prefix, problem_prefix_setup) =
   125   Attrib.config_string "sledgehammer_problem_prefix" (K "prob")
   126 
   127 val (measure_run_time, measure_run_time_setup) =
   128   Attrib.config_bool "sledgehammer_measure_run_time" (K false)
   129 
   130 fun with_path cleanup after f path =
   131   Exn.capture f path
   132   |> tap (fn _ => cleanup path)
   133   |> Exn.release
   134   |> tap (after path)
   135 
   136 fun extract_delimited (begin_delim, end_delim) output =
   137   output |> first_field begin_delim |> the |> snd
   138          |> first_field end_delim |> the |> fst
   139          |> first_field "\n" |> the |> snd
   140   handle Option.Option => ""
   141 
   142 val tstp_important_message_delims =
   143   ("% SZS start RequiredInformation", "% SZS end RequiredInformation")
   144 
   145 fun extract_important_message output =
   146   case extract_delimited tstp_important_message_delims output of
   147     "" => ""
   148   | s => s |> space_explode "\n" |> filter_out (curry (op =) "")
   149            |> map (perhaps (try (unprefix "%")))
   150            |> map (perhaps (try (unprefix " ")))
   151            |> space_implode "\n " |> quote
   152 
   153 (* Splits by the first possible of a list of delimiters. *)
   154 fun extract_proof delims output =
   155   case pairself (find_first (fn s => String.isSubstring s output))
   156                 (ListPair.unzip delims) of
   157     (SOME begin_delim, SOME end_delim) =>
   158     extract_delimited (begin_delim, end_delim) output
   159   | _ => ""
   160 
   161 fun extract_proof_and_outcome complete res_code proof_delims known_failures
   162                               output =
   163   case known_failure_in_output output known_failures of
   164     NONE => (case extract_proof proof_delims output of
   165              "" => ("", SOME MalformedOutput)
   166            | proof => if res_code = 0 then (proof, NONE)
   167                       else ("", SOME UnknownError))
   168   | SOME failure =>
   169     ("", SOME (if failure = IncompleteUnprovable andalso complete then
   170                  Unprovable
   171                else
   172                  failure))
   173 
   174 fun extract_clause_sequence output =
   175   let
   176     val tokens_of = String.tokens (not o Char.isAlphaNum)
   177     fun extract_num ("clause" :: (ss as _ :: _)) =
   178     Int.fromString (List.last ss)
   179       | extract_num _ = NONE
   180   in output |> split_lines |> map_filter (extract_num o tokens_of) end
   181 
   182 val set_ClauseFormulaRelationN = "set_ClauseFormulaRelation"
   183 
   184 val parse_clause_formula_pair =
   185   $$ "(" |-- scan_integer --| $$ ","
   186   -- (Symbol.scan_id ::: Scan.repeat ($$ "," |-- Symbol.scan_id)) --| $$ ")"
   187   --| Scan.option ($$ ",")
   188 val parse_clause_formula_relation =
   189   Scan.this_string set_ClauseFormulaRelationN |-- $$ "("
   190   |-- Scan.repeat parse_clause_formula_pair
   191 val extract_clause_formula_relation =
   192   Substring.full #> Substring.position set_ClauseFormulaRelationN
   193   #> snd #> Substring.position "." #> fst #> Substring.string
   194   #> explode #> filter_out Symbol.is_blank #> parse_clause_formula_relation
   195   #> fst
   196 
   197 (* TODO: move to "Sledgehammer_Reconstruct" *)
   198 fun repair_conjecture_shape_and_theorem_names output conjecture_shape
   199                                               axiom_names =
   200   if String.isSubstring set_ClauseFormulaRelationN output then
   201     (* This is a hack required for keeping track of axioms after they have been
   202        clausified by SPASS's Flotter tool. The "ATP/scripts/spass" script is
   203        also part of this hack. *)
   204     let
   205       val j0 = hd (hd conjecture_shape)
   206       val seq = extract_clause_sequence output
   207       val name_map = extract_clause_formula_relation output
   208       fun renumber_conjecture j =
   209         conjecture_prefix ^ string_of_int (j - j0)
   210         |> AList.find (fn (s, ss) => member (op =) ss s) name_map
   211         |> map (fn s => find_index (curry (op =) s) seq + 1)
   212       fun names_for_number j =
   213         j |> AList.lookup (op =) name_map |> these
   214           |> map_filter (try (unprefix axiom_prefix)) |> map unascii_of
   215           |> map (fn name =>
   216                      (name, name |> find_first_in_list_vector axiom_names
   217                                  |> the)
   218                      handle Option.Option =>
   219                             error ("No such fact: " ^ quote name ^ "."))
   220     in
   221       (conjecture_shape |> map (maps renumber_conjecture),
   222        seq |> map names_for_number |> Vector.fromList)
   223     end
   224   else
   225     (conjecture_shape, axiom_names)
   226 
   227 
   228 (* generic TPTP-based provers *)
   229 
   230 fun prover_fun atp_name
   231         {exec, required_execs, arguments, has_incomplete_mode, proof_delims,
   232          known_failures, default_max_relevant, explicit_forall,
   233          use_conjecture_for_hypotheses}
   234         ({debug, verbose, overlord, full_types, explicit_apply,
   235           max_relevant, isar_proof, isar_shrink_factor, timeout, ...} : params)
   236         minimize_command ({ctxt, goal, subgoal, axioms} : problem) =
   237   let
   238     val (_, hyp_ts, concl_t) = strip_subgoal goal subgoal
   239     val max_relevant = the_default default_max_relevant max_relevant
   240     val axioms = take max_relevant axioms
   241     (* path to unique problem file *)
   242     val the_dest_dir = if overlord then getenv "ISABELLE_HOME_USER"
   243                        else Config.get ctxt dest_dir
   244     val the_problem_prefix = Config.get ctxt problem_prefix
   245     val problem_file_name =
   246       Path.basic ((if overlord then "prob_" ^ atp_name
   247                    else the_problem_prefix ^ serial_string ())
   248                   ^ "_" ^ string_of_int subgoal)
   249     val problem_path_name =
   250       if the_dest_dir = "" then
   251         File.tmp_path problem_file_name
   252       else if File.exists (Path.explode the_dest_dir) then
   253         Path.append (Path.explode the_dest_dir) problem_file_name
   254       else
   255         error ("No such directory: " ^ quote the_dest_dir ^ ".")
   256     val measure_run_time = verbose orelse Config.get ctxt measure_run_time
   257     val command = Path.explode (getenv (fst exec) ^ "/" ^ snd exec)
   258     (* write out problem file and call prover *)
   259     fun command_line complete timeout probfile =
   260       let
   261         val core = File.shell_path command ^ " " ^ arguments complete timeout ^
   262                    " " ^ File.shell_path probfile
   263       in
   264         (if measure_run_time then "TIMEFORMAT='%3R'; { time " ^ core ^ " ; }"
   265          else "exec " ^ core) ^ " 2>&1"
   266       end
   267     fun split_time s =
   268       let
   269         val split = String.tokens (fn c => str c = "\n");
   270         val (output, t) = s |> split |> split_last |> apfst cat_lines;
   271         fun as_num f = f >> (fst o read_int);
   272         val num = as_num (Scan.many1 Symbol.is_ascii_digit);
   273         val digit = Scan.one Symbol.is_ascii_digit;
   274         val num3 = as_num (digit ::: digit ::: (digit >> single));
   275         val time = num --| Scan.$$ "." -- num3 >> (fn (a, b) => a * 1000 + b);
   276         val as_time = the_default 0 o Scan.read Symbol.stopper time o explode;
   277       in (output, as_time t) end;
   278     fun run_on probfile =
   279       case filter (curry (op =) "" o getenv o fst) (exec :: required_execs) of
   280         (home_var, _) :: _ =>
   281         error ("The environment variable " ^ quote home_var ^ " is not set.")
   282       | [] =>
   283         if File.exists command then
   284           let
   285             fun do_run complete timeout =
   286               let
   287                 val command = command_line complete timeout probfile
   288                 val ((output, msecs), res_code) =
   289                   bash_output command
   290                   |>> (if overlord then
   291                          prefix ("% " ^ command ^ "\n% " ^ timestamp () ^ "\n")
   292                        else
   293                          I)
   294                   |>> (if measure_run_time then split_time else rpair 0)
   295                 val (proof, outcome) =
   296                   extract_proof_and_outcome complete res_code proof_delims
   297                                             known_failures output
   298               in (output, msecs, proof, outcome) end
   299             val readable_names = debug andalso overlord
   300             val (problem, pool, conjecture_offset, axiom_names) =
   301               prepare_problem ctxt readable_names explicit_forall full_types
   302                               explicit_apply hyp_ts concl_t axioms
   303             val ss = strings_for_tptp_problem use_conjecture_for_hypotheses
   304                                               problem
   305             val _ = File.write_list probfile ss
   306             val conjecture_shape =
   307               conjecture_offset + 1 upto conjecture_offset + length hyp_ts + 1
   308               |> map single
   309             val timer = Timer.startRealTimer ()
   310             val result =
   311               do_run false (if has_incomplete_mode then
   312                               Time.fromMilliseconds
   313                                          (2 * Time.toMilliseconds timeout div 3)
   314                             else
   315                               timeout)
   316               |> has_incomplete_mode
   317                  ? (fn (_, msecs0, _, SOME _) =>
   318                        do_run true
   319                               (Time.- (timeout, Timer.checkRealTimer timer))
   320                        |> (fn (output, msecs, proof, outcome) =>
   321                               (output, msecs0 + msecs, proof, outcome))
   322                      | result => result)
   323           in ((pool, conjecture_shape, axiom_names), result) end
   324         else
   325           error ("Bad executable: " ^ Path.implode command ^ ".")
   326 
   327     (* If the problem file has not been exported, remove it; otherwise, export
   328        the proof file too. *)
   329     fun cleanup probfile =
   330       if the_dest_dir = "" then try File.rm probfile else NONE
   331     fun export probfile (_, (output, _, _, _)) =
   332       if the_dest_dir = "" then
   333         ()
   334       else
   335         File.write (Path.explode (Path.implode probfile ^ "_proof")) output
   336     val ((pool, conjecture_shape, axiom_names),
   337          (output, msecs, proof, outcome)) =
   338       with_path cleanup export run_on problem_path_name
   339     val (conjecture_shape, axiom_names) =
   340       repair_conjecture_shape_and_theorem_names output conjecture_shape
   341                                                 axiom_names
   342     val important_message = extract_important_message output
   343     val (message, used_thm_names) =
   344       case outcome of
   345         NONE =>
   346         proof_text isar_proof
   347             (pool, debug, isar_shrink_factor, ctxt, conjecture_shape)
   348             (full_types, minimize_command, proof, axiom_names, goal, subgoal)
   349         |>> (fn message =>
   350                 message ^ (if verbose then
   351                              "\nReal CPU time: " ^ string_of_int msecs ^ " ms."
   352                            else
   353                              "") ^
   354                 (if important_message <> "" then
   355                    "\n\nImportant message from Dr. Geoff Sutcliffe:\n" ^
   356                    important_message
   357                  else
   358                    ""))
   359       | SOME failure => (string_for_failure failure, [])
   360   in
   361     {outcome = outcome, message = message, pool = pool,
   362      used_thm_names = used_thm_names, atp_run_time_in_msecs = msecs,
   363      output = output, proof = proof, axiom_names = axiom_names,
   364      conjecture_shape = conjecture_shape}
   365   end
   366 
   367 fun get_prover_fun thy name = prover_fun name (get_prover thy name)
   368 
   369 fun run_prover ctxt (params as {blocking, verbose, max_relevant, timeout,
   370                                 expect, ...})
   371                i n relevance_override minimize_command
   372                (problem as {goal, axioms, ...})
   373                (prover as {default_max_relevant, ...}, atp_name) =
   374   let
   375     val birth_time = Time.now ()
   376     val death_time = Time.+ (birth_time, timeout)
   377     val max_relevant = the_default default_max_relevant max_relevant
   378     val num_axioms = Int.min (length axioms, max_relevant)
   379     val desc =
   380       "ATP " ^ quote atp_name ^
   381       (if verbose then
   382          " with " ^ string_of_int num_axioms ^ " fact" ^ plural_s num_axioms
   383        else
   384          "") ^
   385       " on " ^ (if n = 1 then "goal" else "subgoal " ^ string_of_int i) ^ ":" ^
   386       (if blocking then
   387          ""
   388        else
   389          "\n" ^ Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i)))
   390     fun run () =
   391       let
   392         val (outcome_code, message) =
   393           prover_fun atp_name prover params (minimize_command atp_name) problem
   394           |> (fn {outcome, message, ...} =>
   395                  (if is_some outcome then "none" else "some", message))
   396           handle ERROR message => ("unknown", "Error: " ^ message ^ "\n")
   397                | exn => ("unknown", "Internal error:\n" ^
   398                                     ML_Compiler.exn_message exn ^ "\n")
   399       in
   400         if expect = "" orelse outcome_code = expect then
   401           ()
   402         else if blocking then
   403           error ("Unexpected outcome: " ^ quote outcome_code ^ ".")
   404         else
   405           warning ("Unexpected outcome: " ^ quote outcome_code ^ ".");
   406         message
   407       end
   408   in
   409     if blocking then priority (desc ^ "\n" ^ TimeLimit.timeLimit timeout run ())
   410     else Async_Manager.launch das_Tool birth_time death_time desc run
   411   end
   412 
   413 fun run_sledgehammer (params as {blocking, verbose, atps, full_types,
   414                                  relevance_thresholds, max_relevant, ...})
   415                      i relevance_override minimize_command state =
   416     if null atps then error "No ATP is set."
   417     else case subgoal_count state of
   418       0 => priority "No subgoal!"
   419     | n =>
   420       let
   421         val thy = Proof.theory_of state
   422         val timer = Timer.startRealTimer ()
   423         val _ = () |> not blocking ? kill_atps
   424         val _ = priority "Sledgehammering..."
   425         val provers = map (`(get_prover thy)) atps
   426         fun run () =
   427           let
   428             val {context = ctxt, facts = chained_ths, goal} = Proof.goal state
   429             val (_, hyp_ts, concl_t) = strip_subgoal goal i
   430             val max_max_relevant =
   431               case max_relevant of
   432                 SOME n => n
   433               | NONE => fold (Integer.max o #default_max_relevant o fst)
   434                              provers 0
   435             val axioms =
   436               relevant_facts ctxt full_types relevance_thresholds
   437                              max_max_relevant relevance_override chained_ths
   438                              hyp_ts concl_t
   439             val problem =
   440               {ctxt = ctxt, goal = goal, subgoal = i,
   441                axioms = map (prepare_axiom ctxt) axioms}
   442             val num_axioms = length axioms
   443             val _ =
   444               (if blocking then Par_List.map else map)
   445                   (run_prover ctxt params i n relevance_override
   446                               minimize_command problem) provers
   447           in
   448             if verbose andalso blocking then
   449               priority ("Total time: " ^
   450                         signed_string_of_int (Time.toMilliseconds
   451                             (Timer.checkRealTimer timer)) ^ " ms.")
   452             else
   453               ()
   454           end
   455       in if blocking then run () else Future.fork run |> K () end
   456 
   457 val setup =
   458   dest_dir_setup
   459   #> problem_prefix_setup
   460   #> measure_run_time_setup
   461 
   462 end;