src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML
author wenzelm
Sat Apr 02 23:29:05 2016 +0200 (2016-04-02 ago)
changeset 62826 eb94e570c1a4
parent 62735 23de054397e5
child 63692 1bc4bc2c9fd1
permissions -rw-r--r--
prefer infix operations;
     1 (*  Title:      HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML
     2     Author:     Fabian Immler, TU Muenchen
     3     Author:     Makarius
     4     Author:     Jasmin Blanchette, TU Muenchen
     5 
     6 ATPs as Sledgehammer provers.
     7 *)
     8 
     9 signature SLEDGEHAMMER_PROVER_ATP =
    10 sig
    11   type mode = Sledgehammer_Prover.mode
    12   type prover = Sledgehammer_Prover.prover
    13 
    14   val atp_dest_dir : string Config.T
    15   val atp_problem_prefix : string Config.T
    16   val atp_completish : int Config.T
    17   val atp_full_names : bool Config.T
    18 
    19   val is_ho_atp : Proof.context -> string -> bool
    20 
    21   val run_atp : mode -> string -> prover
    22 end;
    23 
    24 structure Sledgehammer_Prover_ATP : SLEDGEHAMMER_PROVER_ATP =
    25 struct
    26 
    27 open ATP_Util
    28 open ATP_Problem
    29 open ATP_Proof
    30 open ATP_Problem_Generate
    31 open ATP_Proof_Reconstruct
    32 open ATP_Waldmeister
    33 open ATP_Satallax
    34 open ATP_Systems
    35 open Sledgehammer_Util
    36 open Sledgehammer_Proof_Methods
    37 open Sledgehammer_Isar
    38 open Sledgehammer_Prover
    39 
    40 (* Empty string means create files in Isabelle's temporary files directory. *)
    41 val atp_dest_dir = Attrib.setup_config_string @{binding sledgehammer_atp_dest_dir} (K "")
    42 val atp_problem_prefix =
    43   Attrib.setup_config_string @{binding sledgehammer_atp_problem_prefix} (K "prob")
    44 val atp_completish = Attrib.setup_config_int @{binding sledgehammer_atp_completish} (K 0)
    45 (* In addition to being easier to read, readable names are often much shorter, especially if types
    46    are mangled in names. This makes a difference for some provers (e.g., E). For these reason, short
    47    names are enabled by default. *)
    48 val atp_full_names = Attrib.setup_config_bool @{binding sledgehammer_atp_full_names} (K false)
    49 
    50 fun is_atp_of_format is_format ctxt name =
    51   let val thy = Proof_Context.theory_of ctxt in
    52     (case try (get_atp thy) name of
    53       SOME config =>
    54       exists (fn (_, ((_, format, _, _, _), _)) => is_format format) (#best_slices (config ()) ctxt)
    55     | NONE => false)
    56   end
    57 
    58 val is_ho_atp = is_atp_of_format is_format_higher_order
    59 
    60 fun choose_type_enc strictness best_type_enc format =
    61   the_default best_type_enc
    62   #> type_enc_of_string strictness
    63   #> adjust_type_enc format
    64 
    65 fun has_bound_or_var_of_type pred =
    66   exists_subterm (fn Var (_, T as Type _) => pred T
    67                    | Abs (_, T as Type _, _) => pred T
    68                    | _ => false)
    69 
    70 (* Unwanted equalities are those between a (bound or schematic) variable that does not properly
    71    occur in the second operand. *)
    72 val is_exhaustive_finite =
    73   let
    74     fun is_bad_equal (Var z) t =
    75         not (exists_subterm (fn Var z' => z = z' | _ => false) t)
    76       | is_bad_equal (Bound j) t = not (loose_bvar1 (t, j))
    77       | is_bad_equal _ _ = false
    78     fun do_equals t1 t2 = is_bad_equal t1 t2 orelse is_bad_equal t2 t1
    79     fun do_formula pos t =
    80       (case (pos, t) of
    81         (_, @{const Trueprop} $ t1) => do_formula pos t1
    82       | (true, Const (@{const_name Pure.all}, _) $ Abs (_, _, t')) => do_formula pos t'
    83       | (true, Const (@{const_name All}, _) $ Abs (_, _, t')) => do_formula pos t'
    84       | (false, Const (@{const_name Ex}, _) $ Abs (_, _, t')) => do_formula pos t'
    85       | (_, @{const Pure.imp} $ t1 $ t2) =>
    86         do_formula (not pos) t1 andalso (t2 = @{prop False} orelse do_formula pos t2)
    87       | (_, @{const HOL.implies} $ t1 $ t2) =>
    88         do_formula (not pos) t1 andalso (t2 = @{const False} orelse do_formula pos t2)
    89       | (_, @{const Not} $ t1) => do_formula (not pos) t1
    90       | (true, @{const HOL.disj} $ t1 $ t2) => forall (do_formula pos) [t1, t2]
    91       | (false, @{const HOL.conj} $ t1 $ t2) => forall (do_formula pos) [t1, t2]
    92       | (true, Const (@{const_name HOL.eq}, _) $ t1 $ t2) => do_equals t1 t2
    93       | (true, Const (@{const_name Pure.eq}, _) $ t1 $ t2) => do_equals t1 t2
    94       | _ => false)
    95   in do_formula true end
    96 
    97 (* Facts containing variables of finite types such as "unit" or "bool" or of the form
    98    "ALL x. x = A | x = B | x = C" are likely to lead to untypable proofs for unsound type
    99    encodings. *)
   100 fun is_dangerous_prop ctxt =
   101   transform_elim_prop
   102   #> (has_bound_or_var_of_type (is_type_surely_finite ctxt) orf is_exhaustive_finite)
   103 
   104 fun get_slices slice slices =
   105   (0 upto length slices - 1) ~~ slices |> not slice ? (List.last #> single)
   106 
   107 fun get_facts_of_filter _ [(_, facts)] = facts
   108   | get_facts_of_filter fact_filter factss =
   109     (case AList.lookup (op =) factss fact_filter of
   110       SOME facts => facts
   111     | NONE => snd (hd factss))
   112 
   113 (* For low values of "max_facts", this fudge value ensures that most slices are invoked with a
   114    nontrivial amount of facts. *)
   115 val max_fact_factor_fudge = 5
   116 
   117 val mono_max_privileged_facts = 10
   118 
   119 fun suffix_of_mode Auto_Try = "_try"
   120   | suffix_of_mode Try = "_try"
   121   | suffix_of_mode Normal = ""
   122   | suffix_of_mode MaSh = ""
   123   | suffix_of_mode Minimize = "_min"
   124 
   125 (* Give the ATPs some slack before interrupting them the hard way. "z3_tptp" on Linux appears to be
   126    the only ATP that does not honor its time limit. *)
   127 val atp_timeout_slack = seconds 1.0
   128 
   129 (* Important messages are important but not so important that users want to see them each time. *)
   130 val atp_important_message_keep_quotient = 25
   131 
   132 fun run_atp mode name
   133     ({debug, verbose, overlord, type_enc, strict, lam_trans, uncurried_aliases, fact_filter,
   134      max_facts, max_mono_iters, max_new_mono_instances, isar_proofs, compress, try0, smt_proofs,
   135      slice, minimize, timeout, preplay_timeout, ...} : params)
   136     ({comment, state, goal, subgoal, subgoal_count, factss, found_proof, ...} : prover_problem) =
   137   let
   138     val thy = Proof.theory_of state
   139     val ctxt = Proof.context_of state
   140 
   141     val {exec, arguments, proof_delims, known_failures, prem_role, best_slices, best_max_mono_iters,
   142       best_max_new_mono_instances, ...} = get_atp thy name ()
   143 
   144     val full_proofs = isar_proofs |> the_default (mode = Minimize)
   145     val local_name = perhaps (try (unprefix remote_prefix)) name
   146     val waldmeister_new = (local_name = waldmeister_newN)
   147     val spassy = (local_name = pirateN orelse local_name = spassN)
   148 
   149     val completish = Config.get ctxt atp_completish
   150     val atp_mode = if completish > 0 then Sledgehammer_Completish completish else Sledgehammer
   151     val (_, hyp_ts, concl_t) = strip_subgoal goal subgoal ctxt
   152     val (dest_dir, problem_prefix) =
   153       if overlord then overlord_file_location_of_prover name
   154       else (Config.get ctxt atp_dest_dir, Config.get ctxt atp_problem_prefix)
   155     val problem_file_name =
   156       Path.basic (problem_prefix ^ (if overlord then "" else serial_string ()) ^
   157         suffix_of_mode mode ^ "_" ^ string_of_int subgoal)
   158     val prob_path =
   159       if dest_dir = "" then
   160         File.tmp_path problem_file_name
   161       else if File.exists (Path.explode dest_dir) then
   162         Path.append (Path.explode dest_dir) problem_file_name
   163       else
   164         error ("No such directory: " ^ quote dest_dir ^ ".")
   165     val exec = exec full_proofs
   166     val command0 =
   167       (case find_first (fn var => getenv var <> "") (fst exec) of
   168         SOME var =>
   169         let
   170           val pref = getenv var ^ "/"
   171           val paths =
   172             map (Path.explode o prefix pref)
   173               (if ML_System.platform_is_windows then
   174                 map (suffix ".exe") (snd exec) @ snd exec
   175                else snd exec);
   176         in
   177           (case find_first File.exists paths of
   178             SOME path => path
   179           | NONE => error ("Bad executable: " ^ Path.print (hd paths) ^ "."))
   180         end
   181       | NONE => error ("The environment variable " ^ quote (List.last (fst exec)) ^ " is not set."))
   182 
   183     fun split_time s =
   184       let
   185         val split = String.tokens (fn c => str c = "\n")
   186         val (output, t) = s |> split |> (try split_last #> the_default ([], "0")) |>> cat_lines
   187         val num = Scan.many1 Symbol.is_ascii_digit >> (fst o read_int)
   188         val digit = Scan.one Symbol.is_ascii_digit
   189         val num3 = digit ::: digit ::: (digit >> single) >> (fst o read_int)
   190         val time = num --| Scan.$$ "." -- num3 >> (fn (a, b) => a * 1000 + b)
   191         val as_time = raw_explode #> Scan.read Symbol.stopper time #> the_default 0
   192       in (output, as_time t |> Time.fromMilliseconds) end
   193 
   194     fun run () =
   195       let
   196         (* If slicing is disabled, we expand the last slice to fill the entire time available. *)
   197         val all_slices = best_slices ctxt
   198         val actual_slices = get_slices slice all_slices
   199 
   200         fun max_facts_of_slices (slices : (real * (slice_spec * string)) list) =
   201           fold (Integer.max o fst o #1 o fst o snd) slices 0
   202 
   203         val num_actual_slices = length actual_slices
   204         val max_fact_factor =
   205           Real.fromInt (case max_facts of NONE => max_facts_of_slices all_slices | SOME max => max)
   206           / Real.fromInt (max_facts_of_slices (map snd actual_slices))
   207 
   208         fun monomorphize_facts facts =
   209           let
   210             val ctxt =
   211               ctxt
   212               |> repair_monomorph_context max_mono_iters best_max_mono_iters max_new_mono_instances
   213                    best_max_new_mono_instances
   214             (* pseudo-theorem involving the same constants as the subgoal *)
   215             val subgoal_th =
   216               Logic.list_implies (hyp_ts, concl_t) |> Skip_Proof.make_thm thy
   217             val rths =
   218               facts |> chop mono_max_privileged_facts
   219                     |>> map (pair 1 o snd)
   220                     ||> map (pair 2 o snd)
   221                     |> op @
   222                     |> cons (0, subgoal_th)
   223           in
   224             Monomorph.monomorph atp_schematic_consts_of ctxt rths
   225             |> tl |> curry ListPair.zip (map fst facts)
   226             |> maps (fn (name, rths) => map (pair name o zero_var_indexes o snd) rths)
   227           end
   228 
   229         fun run_slice time_left (cache_key, cache_value) (slice, (time_frac,
   230             (key as ((best_max_facts, best_fact_filter), format, best_type_enc, best_lam_trans,
   231                best_uncurried_aliases),
   232              extra))) =
   233           let
   234             val effective_fact_filter = fact_filter |> the_default best_fact_filter
   235             val facts = get_facts_of_filter effective_fact_filter factss
   236             val num_facts =
   237               Real.ceil (max_fact_factor * Real.fromInt best_max_facts) + max_fact_factor_fudge
   238               |> Integer.min (length facts)
   239             val generate_info = (case format of DFG _ => true | _ => false)
   240             val strictness = if strict then Strict else Non_Strict
   241             val type_enc = type_enc |> choose_type_enc strictness best_type_enc format
   242             val sound = is_type_enc_sound type_enc
   243             val real_ms = Real.fromInt o Time.toMilliseconds
   244             val slice_timeout =
   245               (real_ms time_left
   246                |> (if slice < num_actual_slices - 1 then
   247                      curry Real.min (time_frac * real_ms timeout)
   248                    else
   249                      I))
   250               * 0.001
   251               |> seconds
   252             val generous_slice_timeout =
   253               if mode = MaSh then one_day else slice_timeout + atp_timeout_slack
   254             val _ =
   255               if debug then
   256                 quote name ^ " slice #" ^ string_of_int (slice + 1) ^
   257                 " with " ^ string_of_int num_facts ^ " fact" ^
   258                 plural_s num_facts ^ " for " ^ string_of_time slice_timeout ^ "..."
   259                 |> writeln
   260               else
   261                 ()
   262             val readable_names = not (Config.get ctxt atp_full_names)
   263             val lam_trans = lam_trans |> the_default best_lam_trans
   264             val uncurried_aliases = uncurried_aliases |> the_default best_uncurried_aliases
   265             val value as (atp_problem, _, _, _, _) =
   266               if cache_key = SOME key then
   267                 cache_value
   268               else
   269                 facts
   270                 |> not sound ? filter_out (is_dangerous_prop ctxt o Thm.prop_of o snd)
   271                 |> take num_facts
   272                 |> not (is_type_enc_polymorphic type_enc) ? monomorphize_facts
   273                 |> map (apsnd Thm.prop_of)
   274                 |> (if waldmeister_new then
   275                       generate_waldmeister_problem ctxt hyp_ts concl_t
   276                       #> (fn (a, b, c, d, e) => (a, b, c, d, SOME e))
   277                     else
   278                       generate_atp_problem ctxt generate_info format prem_role type_enc atp_mode
   279                         lam_trans uncurried_aliases readable_names true hyp_ts concl_t
   280                       #> (fn (a, b, c, d) => (a, b, c, d, NONE)))
   281 
   282             fun sel_weights () = atp_problem_selection_weights atp_problem
   283             fun ord_info () = atp_problem_term_order_info atp_problem
   284 
   285             val ord = effective_term_order ctxt name
   286             val args =
   287               arguments ctxt full_proofs extra slice_timeout (File.bash_path prob_path)
   288                 (ord, ord_info, sel_weights)
   289             val command =
   290               "(exec 2>&1; " ^ File.bash_path command0 ^ " " ^ args ^ " " ^ ")"
   291               |> enclose "TIMEFORMAT='%3R'; { time " " ; }"
   292 
   293             val _ =
   294               atp_problem
   295               |> lines_of_atp_problem format ord ord_info
   296               |> cons ("% " ^ command ^ "\n" ^ (if comment = "" then "" else "% " ^ comment ^ "\n"))
   297               |> File.write_list prob_path
   298 
   299             val ((output, run_time), (atp_proof, outcome)) =
   300               Timeout.apply generous_slice_timeout Isabelle_System.bash_output command
   301               |>> (if overlord then prefix ("% " ^ command ^ "\n% " ^ timestamp () ^ "\n") else I)
   302               |> fst |> split_time
   303               |> (fn accum as (output, _) =>
   304                 (accum,
   305                  extract_tstplike_proof_and_outcome verbose proof_delims known_failures output
   306                  |>> atp_proof_of_tstplike_proof (perhaps (try (unprefix remote_prefix)) name)
   307                    atp_problem
   308                  handle UNRECOGNIZED_ATP_PROOF () => ([], SOME ProofUnparsable)))
   309               handle Timeout.TIMEOUT _ => (("", slice_timeout), ([], SOME TimedOut))
   310 
   311             val outcome =
   312               (case outcome of
   313                 NONE =>
   314                 (case used_facts_in_unsound_atp_proof ctxt (map fst facts) atp_proof of
   315                   SOME facts =>
   316                   let
   317                     val failure = UnsoundProof (is_type_enc_sound type_enc, sort string_ord facts)
   318                   in
   319                     if debug then (warning (string_of_atp_failure failure); NONE) else SOME failure
   320                   end
   321                 | NONE => (found_proof (); NONE))
   322               | _ => outcome)
   323           in
   324             ((SOME key, value), (output, run_time, facts, atp_proof, outcome),
   325               SOME (format, type_enc))
   326           end
   327 
   328         val timer = Timer.startRealTimer ()
   329 
   330         fun maybe_run_slice slice (result as (cache, (_, run_time0, _, _, SOME _), _)) =
   331             let val time_left = timeout - Timer.checkRealTimer timer in
   332               if time_left <= Time.zeroTime then
   333                 result
   334               else
   335                 run_slice time_left cache slice
   336                 |> (fn (cache, (output, run_time, used_from, atp_proof, outcome),
   337                         format_type_enc) =>
   338                   (cache, (output, run_time0 + run_time, used_from, atp_proof, outcome),
   339                    format_type_enc))
   340             end
   341           | maybe_run_slice _ result = result
   342       in
   343         ((NONE, ([], Symtab.empty, [], Symtab.empty,NONE)),
   344          ("", Time.zeroTime, [], [], SOME InternalError), NONE)
   345         |> fold maybe_run_slice actual_slices
   346       end
   347 
   348     (* If the problem file has not been exported, remove it; otherwise, export
   349        the proof file too. *)
   350     fun clean_up () = if dest_dir = "" then (try File.rm prob_path; ()) else ()
   351     fun export (_, (output, _, _, _, _), _) =
   352       if dest_dir = "" then ()
   353       else File.write (Path.explode (Path.implode prob_path ^ "_proof")) output
   354 
   355     val ((_, (_, pool, lifted, sym_tab,wm_info)), (output, run_time, used_from, atp_proof, outcome),
   356          SOME (format, type_enc)) =
   357       with_cleanup clean_up run () |> tap export
   358 
   359     val important_message =
   360       if mode = Normal andalso Random.random_range 0 (atp_important_message_keep_quotient - 1) = 0
   361       then extract_important_message output
   362       else ""
   363 
   364     val (used_facts, preferred_methss, message) =
   365       (case outcome of
   366         NONE =>
   367         let
   368           val used_facts = sort_by fst (used_facts_in_atp_proof ctxt (map fst used_from) atp_proof)
   369           val needs_full_types = is_typed_helper_used_in_atp_proof atp_proof
   370           val preferred_methss =
   371             (Metis_Method (NONE, NONE),
   372              bunches_of_proof_methods try0 (smt_proofs <> SOME false) needs_full_types
   373                (if atp_proof_prefers_lifting atp_proof then liftingN else hide_lamsN))
   374         in
   375           (used_facts, preferred_methss,
   376            fn preplay =>
   377               let
   378                 val _ = if verbose then writeln "Generating proof text..." else ()
   379 
   380                 fun isar_params () =
   381                   let
   382                     val metis_type_enc =
   383                       if is_typed_helper_used_in_atp_proof atp_proof then SOME full_typesN else NONE
   384                     val metis_lam_trans =
   385                       if atp_proof_prefers_lifting atp_proof then SOME liftingN else NONE
   386                     val atp_proof =
   387                       atp_proof
   388                       |> (if waldmeister_new then termify_waldmeister_proof ctxt pool
   389                           else termify_atp_proof ctxt name format type_enc pool lifted sym_tab)
   390                       |> spassy ? introduce_spassy_skolems
   391                       |> (if waldmeister_new then introduce_waldmeister_skolems (the wm_info) else I)
   392                       |> factify_atp_proof (map fst used_from) hyp_ts concl_t
   393                   in
   394                     (verbose, (metis_type_enc, metis_lam_trans), preplay_timeout, compress, try0,
   395                      minimize, atp_proof, goal)
   396                   end
   397 
   398                 val one_line_params = (preplay (), proof_banner mode name, subgoal, subgoal_count)
   399                 val num_chained = length (#facts (Proof.goal state))
   400               in
   401                 proof_text ctxt debug isar_proofs smt_proofs isar_params num_chained
   402                   one_line_params ^
   403                 (if important_message <> "" then
   404                    "\n\nImportant message from Dr. Geoff Sutcliffe:\n" ^ important_message
   405                  else
   406                    "")
   407               end)
   408         end
   409       | SOME failure =>
   410         ([], (Auto_Method (* dummy *), []), fn _ => string_of_atp_failure failure))
   411   in
   412     {outcome = outcome, used_facts = used_facts, used_from = used_from,
   413      preferred_methss = preferred_methss, run_time = run_time, message = message}
   414   end
   415 
   416 end;