src/HOL/Tools/Sledgehammer/sledgehammer.ML
author blanchet
Fri Oct 22 11:11:34 2010 +0200 (2010-10-22 ago)
changeset 40062 cfaebaa8588f
parent 40061 71cc5aac8b76
child 40063 d086e3699e78
permissions -rw-r--r--
make Sledgehammer minimizer fully work with SMT
     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 
    17   type params =
    18     {blocking: bool,
    19      debug: bool,
    20      verbose: bool,
    21      overlord: bool,
    22      provers: string list,
    23      full_types: bool,
    24      explicit_apply: bool,
    25      relevance_thresholds: real * real,
    26      max_relevant: int option,
    27      isar_proof: bool,
    28      isar_shrink_factor: int,
    29      timeout: Time.time,
    30      expect: string}
    31 
    32   datatype axiom =
    33     Unprepared of (string * locality) * thm |
    34     Prepared of term * ((string * locality) * fol_formula) option
    35 
    36   type prover_problem =
    37     {state: Proof.state,
    38      goal: thm,
    39      subgoal: int,
    40      axioms: axiom list,
    41      only: bool}
    42 
    43   type prover_result =
    44     {outcome: failure option,
    45      used_axioms: (string * locality) list,
    46      run_time_in_msecs: int option,
    47      message: string}
    48 
    49   type prover = params -> minimize_command -> prover_problem -> prover_result
    50 
    51   val smtN : string
    52   val smt_prover_names : string list
    53   val smt_default_max_relevant : int
    54   val dest_dir : string Config.T
    55   val problem_prefix : string Config.T
    56   val measure_run_time : bool Config.T
    57   val available_provers : theory -> unit
    58   val kill_provers : unit -> unit
    59   val running_provers : unit -> unit
    60   val messages : int option -> unit
    61   val get_prover : theory -> string -> prover
    62   val run_sledgehammer :
    63     params -> bool -> int -> relevance_override -> (string -> minimize_command)
    64     -> Proof.state -> bool * Proof.state
    65   val setup : theory -> theory
    66 end;
    67 
    68 structure Sledgehammer : SLEDGEHAMMER =
    69 struct
    70 
    71 open ATP_Problem
    72 open ATP_Proof
    73 open ATP_Systems
    74 open Metis_Translate
    75 open Sledgehammer_Util
    76 open Sledgehammer_Filter
    77 open Sledgehammer_Translate
    78 open Sledgehammer_Reconstruct
    79 
    80 
    81 (** The Sledgehammer **)
    82 
    83 (* Identifier to distinguish Sledgehammer from other tools using
    84    "Async_Manager". *)
    85 val das_Tool = "Sledgehammer"
    86 
    87 val smtN = "smt"
    88 val smt_prover_names = [smtN, remote_prefix ^ smtN]
    89 
    90 val smt_default_max_relevant = 300 (* FUDGE *)
    91 val auto_max_relevant_divisor = 2 (* FUDGE *)
    92 
    93 fun available_provers thy =
    94   let
    95     val (remote_provers, local_provers) =
    96       sort_strings (available_atps thy) @ smt_prover_names
    97       |> List.partition (String.isPrefix remote_prefix)
    98   in
    99     priority ("Available provers: " ^ commas (local_provers @ remote_provers) ^
   100               ".")
   101   end
   102 
   103 fun kill_provers () = Async_Manager.kill_threads das_Tool "provers"
   104 fun running_provers () = Async_Manager.running_threads das_Tool "provers"
   105 val messages = Async_Manager.thread_messages das_Tool "prover"
   106 
   107 (** problems, results, ATPs, etc. **)
   108 
   109 type params =
   110   {blocking: bool,
   111    debug: bool,
   112    verbose: bool,
   113    overlord: bool,
   114    provers: string list,
   115    full_types: bool,
   116    explicit_apply: bool,
   117    relevance_thresholds: real * real,
   118    max_relevant: int option,
   119    isar_proof: bool,
   120    isar_shrink_factor: int,
   121    timeout: Time.time,
   122    expect: string}
   123 
   124 datatype axiom =
   125   Unprepared of (string * locality) * thm |
   126   Prepared of term * ((string * locality) * fol_formula) option
   127 
   128 type prover_problem =
   129   {state: Proof.state,
   130    goal: thm,
   131    subgoal: int,
   132    axioms: axiom list,
   133    only: bool}
   134 
   135 type prover_result =
   136   {outcome: failure option,
   137    message: string,
   138    used_axioms: (string * locality) list,
   139    run_time_in_msecs: int option}
   140 
   141 type prover = params -> minimize_command -> prover_problem -> prover_result
   142 
   143 (* configuration attributes *)
   144 
   145 val (dest_dir, dest_dir_setup) =
   146   Attrib.config_string "sledgehammer_dest_dir" (K "")
   147   (* Empty string means create files in Isabelle's temporary files directory. *)
   148 
   149 val (problem_prefix, problem_prefix_setup) =
   150   Attrib.config_string "sledgehammer_problem_prefix" (K "prob")
   151 
   152 val (measure_run_time, measure_run_time_setup) =
   153   Attrib.config_bool "sledgehammer_measure_run_time" (K false)
   154 
   155 fun with_path cleanup after f path =
   156   Exn.capture f path
   157   |> tap (fn _ => cleanup path)
   158   |> Exn.release
   159   |> tap (after path)
   160 
   161 fun prover_description ctxt ({blocking, verbose, ...} : params) name num_axioms
   162                        i n goal =
   163   quote name ^
   164   (if verbose then
   165      " with " ^ string_of_int num_axioms ^ " fact" ^ plural_s num_axioms
   166    else
   167      "") ^
   168   " on " ^ (if n = 1 then "goal" else "subgoal " ^ string_of_int i) ^ ":" ^
   169   (if blocking then
   170      ""
   171    else
   172      "\n" ^ Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i)))
   173 
   174 fun proof_banner auto =
   175   if auto then "Sledgehammer found a proof" else "Try this command"
   176 
   177 (* generic TPTP-based ATPs *)
   178 
   179 fun dest_Unprepared (Unprepared p) = p
   180   | dest_Unprepared (Prepared _) = raise Fail "dest_Unprepared"
   181 fun prepared_axiom ctxt (Unprepared p) = prepare_axiom ctxt p
   182   | prepared_axiom _ (Prepared p) = p
   183 
   184 fun int_option_add (SOME m) (SOME n) = SOME (m + n)
   185   | int_option_add _ _ = NONE
   186 
   187 (* Important messages are important but not so important that users want to see
   188    them each time. *)
   189 val important_message_keep_factor = 0.1
   190 
   191 fun atp_fun auto atp_name
   192         {exec, required_execs, arguments, has_incomplete_mode, proof_delims,
   193          known_failures, default_max_relevant, explicit_forall,
   194          use_conjecture_for_hypotheses}
   195         ({debug, verbose, overlord, full_types, explicit_apply,
   196           max_relevant, isar_proof, isar_shrink_factor, timeout, ...} : params)
   197         minimize_command
   198         ({state, goal, subgoal, axioms, only} : prover_problem) =
   199   let
   200     val ctxt = Proof.context_of state
   201     val (_, hyp_ts, concl_t) = strip_subgoal goal subgoal
   202     val axioms =
   203       axioms |> not only ? take (the_default default_max_relevant max_relevant)
   204              |> map (prepared_axiom ctxt)
   205     val dest_dir = if overlord then getenv "ISABELLE_HOME_USER"
   206                    else Config.get ctxt dest_dir
   207     val problem_prefix = Config.get ctxt problem_prefix
   208     val problem_file_name =
   209       Path.basic ((if overlord then "prob_" ^ atp_name
   210                    else problem_prefix ^ serial_string ())
   211                   ^ "_" ^ string_of_int subgoal)
   212     val problem_path_name =
   213       if dest_dir = "" then
   214         File.tmp_path problem_file_name
   215       else if File.exists (Path.explode dest_dir) then
   216         Path.append (Path.explode dest_dir) problem_file_name
   217       else
   218         error ("No such directory: " ^ quote dest_dir ^ ".")
   219     val measure_run_time = verbose orelse Config.get ctxt measure_run_time
   220     val command = Path.explode (getenv (fst exec) ^ "/" ^ snd exec)
   221     (* write out problem file and call ATP *)
   222     fun command_line complete timeout probfile =
   223       let
   224         val core = File.shell_path command ^ " " ^ arguments complete timeout ^
   225                    " " ^ File.shell_path probfile
   226       in
   227         (if measure_run_time then "TIMEFORMAT='%3R'; { time " ^ core ^ " ; }"
   228          else "exec " ^ core) ^ " 2>&1"
   229       end
   230     fun split_time s =
   231       let
   232         val split = String.tokens (fn c => str c = "\n");
   233         val (output, t) = s |> split |> split_last |> apfst cat_lines;
   234         fun as_num f = f >> (fst o read_int);
   235         val num = as_num (Scan.many1 Symbol.is_ascii_digit);
   236         val digit = Scan.one Symbol.is_ascii_digit;
   237         val num3 = as_num (digit ::: digit ::: (digit >> single));
   238         val time = num --| Scan.$$ "." -- num3 >> (fn (a, b) => a * 1000 + b);
   239         val as_time = Scan.read Symbol.stopper time o explode
   240       in (output, as_time t) end;
   241     fun run_on probfile =
   242       case filter (curry (op =) "" o getenv o fst) (exec :: required_execs) of
   243         (home_var, _) :: _ =>
   244         error ("The environment variable " ^ quote home_var ^ " is not set.")
   245       | [] =>
   246         if File.exists command then
   247           let
   248             fun run complete timeout =
   249               let
   250                 val command = command_line complete timeout probfile
   251                 val ((output, msecs), res_code) =
   252                   bash_output command
   253                   |>> (if overlord then
   254                          prefix ("% " ^ command ^ "\n% " ^ timestamp () ^ "\n")
   255                        else
   256                          I)
   257                   |>> (if measure_run_time then split_time else rpair NONE)
   258                 val (tstplike_proof, outcome) =
   259                   extract_tstplike_proof_and_outcome complete res_code
   260                       proof_delims known_failures output
   261               in (output, msecs, tstplike_proof, outcome) end
   262             val readable_names = debug andalso overlord
   263             val (atp_problem, pool, conjecture_offset, axiom_names) =
   264               prepare_atp_problem ctxt readable_names explicit_forall full_types
   265                                   explicit_apply hyp_ts concl_t axioms
   266             val ss = tptp_strings_for_atp_problem use_conjecture_for_hypotheses
   267                                                   atp_problem
   268             val _ = File.write_list probfile ss
   269             val conjecture_shape =
   270               conjecture_offset + 1 upto conjecture_offset + length hyp_ts + 1
   271               |> map single
   272             val run_twice = has_incomplete_mode andalso not auto
   273             val timer = Timer.startRealTimer ()
   274             val result =
   275               run false (if run_twice then
   276                            Time.fromMilliseconds
   277                                          (2 * Time.toMilliseconds timeout div 3)
   278                          else
   279                            timeout)
   280               |> run_twice
   281                  ? (fn (_, msecs0, _, SOME _) =>
   282                        run true (Time.- (timeout, Timer.checkRealTimer timer))
   283                        |> (fn (output, msecs, tstplike_proof, outcome) =>
   284                               (output, int_option_add msecs0 msecs,
   285                                tstplike_proof, outcome))
   286                      | result => result)
   287           in ((pool, conjecture_shape, axiom_names), result) end
   288         else
   289           error ("Bad executable: " ^ Path.implode command ^ ".")
   290 
   291     (* If the problem file has not been exported, remove it; otherwise, export
   292        the proof file too. *)
   293     fun cleanup probfile =
   294       if dest_dir = "" then try File.rm probfile else NONE
   295     fun export probfile (_, (output, _, _, _)) =
   296       if dest_dir = "" then
   297         ()
   298       else
   299         File.write (Path.explode (Path.implode probfile ^ "_proof")) output
   300     val ((pool, conjecture_shape, axiom_names),
   301          (output, msecs, tstplike_proof, outcome)) =
   302       with_path cleanup export run_on problem_path_name
   303     val (conjecture_shape, axiom_names) =
   304       repair_conjecture_shape_and_axiom_names output conjecture_shape
   305                                               axiom_names
   306     val important_message =
   307       if random () <= important_message_keep_factor then
   308         extract_important_message output
   309       else
   310         ""
   311     val (message, used_axioms) =
   312       case outcome of
   313         NONE =>
   314         proof_text isar_proof
   315             (pool, debug, isar_shrink_factor, ctxt, conjecture_shape)
   316             (proof_banner auto, full_types, minimize_command, tstplike_proof,
   317              axiom_names, goal, subgoal)
   318         |>> (fn message =>
   319                 message ^ (if verbose then
   320                              "\nATP real CPU time: " ^
   321                              string_of_int (the msecs) ^ " ms."
   322                            else
   323                              "") ^
   324                 (if important_message <> "" then
   325                    "\n\nImportant message from Dr. Geoff Sutcliffe:\n" ^
   326                    important_message
   327                  else
   328                    ""))
   329       | SOME failure => (string_for_failure failure, [])
   330   in
   331     {outcome = outcome, message = message, used_axioms = used_axioms,
   332      run_time_in_msecs = msecs}
   333   end
   334 
   335 fun get_atp_as_prover thy name = atp_fun false name (get_atp thy name)
   336 
   337 fun run_atp_somehow (params as {blocking, debug, max_relevant, timeout,
   338                                 expect, ...})
   339                     auto i n minimize_command
   340                     (problem as {state, goal, axioms, ...})
   341                     (prover as {default_max_relevant, ...}, atp_name) =
   342   let
   343     val ctxt = Proof.context_of state
   344     val birth_time = Time.now ()
   345     val death_time = Time.+ (birth_time, timeout)
   346     val max_relevant = the_default default_max_relevant max_relevant
   347     val num_axioms = Int.min (length axioms, max_relevant)
   348     val desc = prover_description ctxt params atp_name num_axioms i n goal
   349     fun go () =
   350       let
   351         fun really_go () =
   352           atp_fun auto atp_name prover params (minimize_command atp_name)
   353                   problem
   354           |> (fn {outcome, message, ...} =>
   355                  (if is_some outcome then "none" else "some", message))
   356         val (outcome_code, message) =
   357           if debug then
   358             really_go ()
   359           else
   360             (really_go ()
   361              handle ERROR message => ("unknown", "Error: " ^ message ^ "\n")
   362                   | exn => ("unknown", "Internal error:\n" ^
   363                                        ML_Compiler.exn_message exn ^ "\n"))
   364         val _ =
   365           if expect = "" orelse outcome_code = expect then
   366             ()
   367           else if blocking then
   368             error ("Unexpected outcome: " ^ quote outcome_code ^ ".")
   369           else
   370             warning ("Unexpected outcome: " ^ quote outcome_code ^ ".");
   371       in (outcome_code = "some", message) end
   372   in
   373     if auto then
   374       let val (success, message) = TimeLimit.timeLimit timeout go () in
   375         (success, state |> success ? Proof.goal_message (fn () =>
   376              Pretty.chunks [Pretty.str "", Pretty.mark Markup.hilite
   377                  (Pretty.str message)]))
   378       end
   379     else if blocking then
   380       let val (success, message) = TimeLimit.timeLimit timeout go () in
   381         List.app priority
   382                  (Async_Manager.break_into_chunks [desc ^ "\n" ^ message]);
   383         (success, state)
   384       end
   385     else
   386       (Async_Manager.launch das_Tool birth_time death_time desc (snd o go);
   387        (false, state))
   388   end
   389 
   390 (* FIXME: dummy *)
   391 fun run_smt_solver remote timeout state axioms i =
   392   {outcome = NONE, used_axioms = axioms |> take 5 |> map fst,
   393    run_time_in_msecs = NONE}
   394 
   395 fun get_smt_solver_as_prover remote ({timeout, ...} : params) minimize_command
   396                              ({state, subgoal, axioms, ...} : prover_problem) =
   397   let
   398     val {outcome, used_axioms, run_time_in_msecs} =
   399       run_smt_solver remote timeout state
   400                      (map_filter (try dest_Unprepared) axioms) subgoal
   401     val message =
   402       if outcome = NONE then
   403         sendback_line (proof_banner false)
   404                       (apply_on_subgoal subgoal (subgoal_count state) ^
   405                        command_call smtN (map fst used_axioms))
   406       else
   407         ""
   408   in
   409     {outcome = outcome, used_axioms = used_axioms,
   410      run_time_in_msecs = run_time_in_msecs, message = message}
   411   end
   412 
   413 fun get_prover thy name =
   414   if member (op =) smt_prover_names name then
   415     get_smt_solver_as_prover (String.isPrefix remote_prefix)
   416   else
   417     get_atp_as_prover thy name
   418 
   419 fun run_smt_solver_somehow state params minimize_command i n goal axioms
   420                            (remote, name) =
   421   let
   422     val ctxt = Proof.context_of state
   423     val desc = prover_description ctxt params name (length axioms) i n goal
   424     val problem =
   425       {state = state, goal = goal, subgoal = i,
   426        axioms = axioms |> map Unprepared, only = true}
   427     val {outcome, used_axioms, message, ...} =
   428       get_smt_solver_as_prover remote params minimize_command problem
   429     val _ =
   430       priority (das_Tool ^ ": " ^ desc ^ "\n" ^
   431                 (if outcome = NONE then message
   432                  else "An unknown error occurred."))
   433   in outcome = NONE end
   434 
   435 fun run_sledgehammer (params as {blocking, provers, full_types,
   436                                  relevance_thresholds, max_relevant, timeout,
   437                                  ...})
   438                      auto i (relevance_override as {only, ...}) minimize_command
   439                      state =
   440   if null provers then
   441     error "No prover is set."
   442   else case subgoal_count state of
   443     0 => (priority "No subgoal!"; (false, state))
   444   | n =>
   445     let
   446       val _ = Proof.assert_backward state
   447       val thy = Proof.theory_of state
   448       val {context = ctxt, facts = chained_ths, goal} = Proof.goal state
   449       val (_, hyp_ts, concl_t) = strip_subgoal goal i
   450       val _ = () |> not blocking ? kill_provers
   451       val _ = if auto then () else priority "Sledgehammering..."
   452       val (smts, atps) =
   453         provers |> List.partition (member (op =) smt_prover_names)
   454                 |>> (take 1 #> map (`(String.isPrefix remote_prefix)))
   455                 ||> map (`(get_atp thy))
   456       fun run_atps (res as (success, state)) =
   457         if success orelse null atps then
   458           res
   459         else
   460           let
   461             val max_max_relevant =
   462               case max_relevant of
   463                 SOME n => n
   464               | NONE =>
   465                 0 |> fold (Integer.max o #default_max_relevant o fst) atps
   466                   |> auto ? (fn n => n div auto_max_relevant_divisor)
   467             val axioms =
   468               relevant_facts ctxt full_types relevance_thresholds
   469                              max_max_relevant relevance_override chained_ths
   470                              hyp_ts concl_t
   471             val problem =
   472               {state = state, goal = goal, subgoal = i,
   473                axioms = axioms |> map (Prepared o prepare_axiom ctxt),
   474                only = only}
   475             val run_atp_somehow =
   476               run_atp_somehow params auto i n minimize_command problem
   477           in
   478             if auto then
   479               fold (fn prover => fn (true, state) => (true, state)
   480                                   | (false, _) => run_atp_somehow prover)
   481                    atps (false, state)
   482             else
   483               atps |> (if blocking then Par_List.map else map) run_atp_somehow
   484                    |> exists fst |> rpair state
   485           end
   486       fun run_smt_solvers (res as (success, state)) =
   487         if success orelse null smts then
   488           res
   489         else
   490           let
   491             val max_relevant =
   492               max_relevant |> the_default smt_default_max_relevant
   493             val axioms =
   494               relevant_facts ctxt full_types relevance_thresholds
   495                              max_relevant relevance_override chained_ths
   496                              hyp_ts concl_t
   497           in
   498             smts |> map (run_smt_solver_somehow state params minimize_command i
   499                                                 n goal axioms)
   500                  |> exists I |> rpair state
   501           end
   502       fun run_atps_and_smt_solvers () =
   503         [run_atps, run_smt_solvers]
   504         |> Par_List.map (fn f => f (false, state) |> K ())
   505     in
   506       if blocking then
   507         (false, state) |> run_atps |> not auto ? run_smt_solvers
   508       else
   509         Future.fork (tap run_atps_and_smt_solvers) |> K (false, state)
   510     end
   511 
   512 val setup =
   513   dest_dir_setup
   514   #> problem_prefix_setup
   515   #> measure_run_time_setup
   516 
   517 end;