src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
author blanchet
Sun Jul 17 14:21:19 2011 +0200 (2011-07-17)
changeset 43864 58a7b3fdc193
parent 43863 a43d61270142
child 43928 24d6e759753f
permissions -rw-r--r--
fixed lambda-liftg: must ensure the formulas are in close form
     1 (*  Title:      HOL/Tools/Sledgehammer/sledgehammer_provers.ML
     2     Author:     Fabian Immler, TU Muenchen
     3     Author:     Makarius
     4     Author:     Jasmin Blanchette, TU Muenchen
     5 
     6 Generic prover abstraction for Sledgehammer.
     7 *)
     8 
     9 signature SLEDGEHAMMER_PROVERS =
    10 sig
    11   type failure = ATP_Proof.failure
    12   type locality = ATP_Translate.locality
    13   type type_enc = ATP_Translate.type_enc
    14   type reconstructor = ATP_Reconstruct.reconstructor
    15   type play = ATP_Reconstruct.play
    16   type minimize_command = ATP_Reconstruct.minimize_command
    17   type relevance_fudge = Sledgehammer_Filter.relevance_fudge
    18 
    19   datatype mode = Auto_Try | Try | Normal | Minimize
    20 
    21   type params =
    22     {debug: bool,
    23      verbose: bool,
    24      overlord: bool,
    25      blocking: bool,
    26      provers: string list,
    27      type_enc: type_enc option,
    28      sound: bool,
    29      relevance_thresholds: real * real,
    30      max_relevant: int option,
    31      max_mono_iters: int,
    32      max_new_mono_instances: int,
    33      isar_proof: bool,
    34      isar_shrink_factor: int,
    35      slicing: bool,
    36      timeout: Time.time,
    37      preplay_timeout: Time.time,
    38      expect: string}
    39 
    40   datatype prover_fact =
    41     Untranslated_Fact of (string * locality) * thm |
    42     SMT_Weighted_Fact of (string * locality) * (int option * thm)
    43 
    44   type prover_problem =
    45     {state: Proof.state,
    46      goal: thm,
    47      subgoal: int,
    48      subgoal_count: int,
    49      facts: prover_fact list,
    50      smt_filter: (string * locality) SMT_Solver.smt_filter_data option}
    51 
    52   type prover_result =
    53     {outcome: failure option,
    54      used_facts: (string * locality) list,
    55      run_time_in_msecs: int option,
    56      preplay: unit -> play,
    57      message: play -> string,
    58      message_tail: string}
    59 
    60   type prover =
    61     params -> (string -> minimize_command) -> prover_problem -> prover_result
    62 
    63   val concealedN : string
    64   val liftingN : string
    65   val combinatorsN : string
    66   val lambdasN : string
    67   val smartN : string
    68   val dest_dir : string Config.T
    69   val problem_prefix : string Config.T
    70   val measure_run_time : bool Config.T
    71   val atp_lambda_translation : string Config.T
    72   val atp_readable_names : bool Config.T
    73   val smt_triggers : bool Config.T
    74   val smt_weights : bool Config.T
    75   val smt_weight_min_facts : int Config.T
    76   val smt_min_weight : int Config.T
    77   val smt_max_weight : int Config.T
    78   val smt_max_weight_index : int Config.T
    79   val smt_weight_curve : (int -> int) Unsynchronized.ref
    80   val smt_max_slices : int Config.T
    81   val smt_slice_fact_frac : real Config.T
    82   val smt_slice_time_frac : real Config.T
    83   val smt_slice_min_secs : int Config.T
    84   val das_tool : string
    85   val select_smt_solver : string -> Proof.context -> Proof.context
    86   val prover_name_for_reconstructor : reconstructor -> string option
    87   val is_metis_prover : string -> bool
    88   val is_atp : theory -> string -> bool
    89   val is_smt_prover : Proof.context -> string -> bool
    90   val is_unit_equational_atp : Proof.context -> string -> bool
    91   val is_prover_supported : Proof.context -> string -> bool
    92   val is_prover_installed : Proof.context -> string -> bool
    93   val default_max_relevant_for_prover : Proof.context -> bool -> string -> int
    94   val is_unit_equality : term -> bool
    95   val is_appropriate_prop_for_prover : Proof.context -> string -> term -> bool
    96   val is_built_in_const_for_prover :
    97     Proof.context -> string -> string * typ -> term list -> bool * term list
    98   val atp_relevance_fudge : relevance_fudge
    99   val smt_relevance_fudge : relevance_fudge
   100   val relevance_fudge_for_prover : Proof.context -> string -> relevance_fudge
   101   val weight_smt_fact :
   102     Proof.context -> int -> ((string * locality) * thm) * int
   103     -> (string * locality) * (int option * thm)
   104   val untranslated_fact : prover_fact -> (string * locality) * thm
   105   val smt_weighted_fact :
   106     Proof.context -> int -> prover_fact * int
   107     -> (string * locality) * (int option * thm)
   108   val supported_provers : Proof.context -> unit
   109   val kill_provers : unit -> unit
   110   val running_provers : unit -> unit
   111   val messages : int option -> unit
   112   val filter_used_facts : ''a list -> (''a * 'b) list -> (''a * 'b) list
   113   val get_prover : Proof.context -> mode -> string -> prover
   114 end;
   115 
   116 structure Sledgehammer_Provers : SLEDGEHAMMER_PROVERS =
   117 struct
   118 
   119 open ATP_Util
   120 open ATP_Problem
   121 open ATP_Proof
   122 open ATP_Systems
   123 open ATP_Translate
   124 open ATP_Reconstruct
   125 open Sledgehammer_Util
   126 open Sledgehammer_Filter
   127 
   128 (** The Sledgehammer **)
   129 
   130 datatype mode = Auto_Try | Try | Normal | Minimize
   131 
   132 (* Identifier to distinguish Sledgehammer from other tools using
   133    "Async_Manager". *)
   134 val das_tool = "Sledgehammer"
   135 
   136 val metisN = Metis_Tactics.metisN
   137 val metis_full_typesN = metisN ^ "_" ^ Metis_Tactics.full_typesN
   138 val metis_no_typesN = metisN ^ "_" ^ Metis_Tactics.no_typesN
   139 
   140 val metis_prover_infos =
   141   [(metisN, Metis),
   142    (metis_full_typesN, Metis_Full_Types),
   143    (metis_no_typesN, Metis_No_Types)]
   144 
   145 val prover_name_for_reconstructor =
   146   AList.find (op =) metis_prover_infos #> try hd
   147 
   148 val metis_reconstructors = map snd metis_prover_infos
   149 
   150 val is_metis_prover = AList.defined (op =) metis_prover_infos
   151 val is_atp = member (op =) o supported_atps
   152 
   153 val select_smt_solver = Context.proof_map o SMT_Config.select_solver
   154 
   155 fun is_smt_prover ctxt name =
   156   member (op =) (SMT_Solver.available_solvers_of ctxt) name
   157 
   158 fun is_unit_equational_atp ctxt name =
   159   let val thy = Proof_Context.theory_of ctxt in
   160     case try (get_atp thy) name of
   161       SOME {formats, ...} => member (op =) formats CNF_UEQ
   162     | NONE => false
   163   end
   164 
   165 fun is_prover_supported ctxt name =
   166   let val thy = Proof_Context.theory_of ctxt in
   167     is_metis_prover name orelse is_atp thy name orelse is_smt_prover ctxt name
   168   end
   169 
   170 fun is_prover_installed ctxt =
   171   is_metis_prover orf is_smt_prover ctxt orf
   172   is_atp_installed (Proof_Context.theory_of ctxt)
   173 
   174 fun get_slices slicing slices =
   175   (0 upto length slices - 1) ~~ slices |> not slicing ? (List.last #> single)
   176 
   177 val metis_default_max_relevant = 20
   178 
   179 fun default_max_relevant_for_prover ctxt slicing name =
   180   let val thy = Proof_Context.theory_of ctxt in
   181     if is_metis_prover name then
   182       metis_default_max_relevant
   183     else if is_atp thy name then
   184       fold (Integer.max o #1 o snd o snd o snd)
   185            (get_slices slicing (#best_slices (get_atp thy name) ctxt)) 0
   186     else (* is_smt_prover ctxt name *)
   187       SMT_Solver.default_max_relevant ctxt name
   188   end
   189 
   190 fun is_if (@{const_name If}, _) = true
   191   | is_if _ = false
   192 
   193 (* Beware of "if and only if" (which is translated as such) and "If" (which is
   194    translated to conditional equations). *)
   195 fun is_good_unit_equality T t u =
   196   T <> @{typ bool} andalso not (exists (exists_Const is_if) [t, u])
   197 
   198 fun is_unit_equality (@{const Trueprop} $ t) = is_unit_equality t
   199   | is_unit_equality (Const (@{const_name all}, _) $ Abs (_, _, t)) =
   200     is_unit_equality t
   201   | is_unit_equality (Const (@{const_name All}, _) $ Abs (_, _, t)) =
   202     is_unit_equality t
   203   | is_unit_equality (Const (@{const_name "=="}, Type (_, [T, _])) $ t $ u) =
   204     is_good_unit_equality T t u
   205   | is_unit_equality (Const (@{const_name HOL.eq}, Type (_ , [T, _])) $ t $ u) =
   206     is_good_unit_equality T t u
   207   | is_unit_equality _ = false
   208 
   209 fun is_appropriate_prop_for_prover ctxt name =
   210   if is_unit_equational_atp ctxt name then is_unit_equality else K true
   211 
   212 fun is_built_in_const_for_prover ctxt name =
   213   if is_smt_prover ctxt name then
   214     let val ctxt = ctxt |> select_smt_solver name in
   215       fn x => fn ts =>
   216          if SMT_Builtin.is_builtin_num_ext ctxt (list_comb (Const x, ts)) then
   217            (true, [])
   218          else if SMT_Builtin.is_builtin_fun_ext ctxt x ts then
   219            (true, ts)
   220          else
   221            (false, ts)
   222     end
   223   else
   224     fn (s, _) => fn ts => (member (op =) atp_irrelevant_consts s, ts)
   225 
   226 (* FUDGE *)
   227 val atp_relevance_fudge =
   228   {local_const_multiplier = 1.5,
   229    worse_irrel_freq = 100.0,
   230    higher_order_irrel_weight = 1.05,
   231    abs_rel_weight = 0.5,
   232    abs_irrel_weight = 2.0,
   233    skolem_irrel_weight = 0.25,
   234    theory_const_rel_weight = 0.5,
   235    theory_const_irrel_weight = 0.25,
   236    chained_const_irrel_weight = 0.25,
   237    intro_bonus = 0.15,
   238    elim_bonus = 0.15,
   239    simp_bonus = 0.15,
   240    local_bonus = 0.55,
   241    assum_bonus = 1.05,
   242    chained_bonus = 1.5,
   243    max_imperfect = 11.5,
   244    max_imperfect_exp = 1.0,
   245    threshold_divisor = 2.0,
   246    ridiculous_threshold = 0.01}
   247 
   248 (* FUDGE (FIXME) *)
   249 val smt_relevance_fudge =
   250   {local_const_multiplier = #local_const_multiplier atp_relevance_fudge,
   251    worse_irrel_freq = #worse_irrel_freq atp_relevance_fudge,
   252    higher_order_irrel_weight = #higher_order_irrel_weight atp_relevance_fudge,
   253    abs_rel_weight = #abs_rel_weight atp_relevance_fudge,
   254    abs_irrel_weight = #abs_irrel_weight atp_relevance_fudge,
   255    skolem_irrel_weight = #skolem_irrel_weight atp_relevance_fudge,
   256    theory_const_rel_weight = #theory_const_rel_weight atp_relevance_fudge,
   257    theory_const_irrel_weight = #theory_const_irrel_weight atp_relevance_fudge,
   258    chained_const_irrel_weight = #chained_const_irrel_weight atp_relevance_fudge,
   259    intro_bonus = #intro_bonus atp_relevance_fudge,
   260    elim_bonus = #elim_bonus atp_relevance_fudge,
   261    simp_bonus = #simp_bonus atp_relevance_fudge,
   262    local_bonus = #local_bonus atp_relevance_fudge,
   263    assum_bonus = #assum_bonus atp_relevance_fudge,
   264    chained_bonus = #chained_bonus atp_relevance_fudge,
   265    max_imperfect = #max_imperfect atp_relevance_fudge,
   266    max_imperfect_exp = #max_imperfect_exp atp_relevance_fudge,
   267    threshold_divisor = #threshold_divisor atp_relevance_fudge,
   268    ridiculous_threshold = #ridiculous_threshold atp_relevance_fudge}
   269 
   270 fun relevance_fudge_for_prover ctxt name =
   271   if is_smt_prover ctxt name then smt_relevance_fudge else atp_relevance_fudge
   272 
   273 fun supported_provers ctxt =
   274   let
   275     val thy = Proof_Context.theory_of ctxt
   276     val (remote_provers, local_provers) =
   277       map fst metis_prover_infos @
   278       sort_strings (supported_atps thy) @
   279       sort_strings (SMT_Solver.available_solvers_of ctxt)
   280       |> List.partition (String.isPrefix remote_prefix)
   281   in
   282     Output.urgent_message ("Supported provers: " ^
   283                            commas (local_provers @ remote_provers) ^ ".")
   284   end
   285 
   286 fun kill_provers () = Async_Manager.kill_threads das_tool "prover"
   287 fun running_provers () = Async_Manager.running_threads das_tool "prover"
   288 val messages = Async_Manager.thread_messages das_tool "prover"
   289 
   290 (** problems, results, ATPs, etc. **)
   291 
   292 type params =
   293   {debug: bool,
   294    verbose: bool,
   295    overlord: bool,
   296    blocking: bool,
   297    provers: string list,
   298    type_enc: type_enc option,
   299    sound: bool,
   300    relevance_thresholds: real * real,
   301    max_relevant: int option,
   302    max_mono_iters: int,
   303    max_new_mono_instances: int,
   304    isar_proof: bool,
   305    isar_shrink_factor: int,
   306    slicing: bool,
   307    timeout: Time.time,
   308    preplay_timeout: Time.time,
   309    expect: string}
   310 
   311 datatype prover_fact =
   312   Untranslated_Fact of (string * locality) * thm |
   313   SMT_Weighted_Fact of (string * locality) * (int option * thm)
   314 
   315 type prover_problem =
   316   {state: Proof.state,
   317    goal: thm,
   318    subgoal: int,
   319    subgoal_count: int,
   320    facts: prover_fact list,
   321    smt_filter: (string * locality) SMT_Solver.smt_filter_data option}
   322 
   323 type prover_result =
   324   {outcome: failure option,
   325    used_facts: (string * locality) list,
   326    run_time_in_msecs: int option,
   327    preplay: unit -> play,
   328    message: play -> string,
   329    message_tail: string}
   330 
   331 type prover =
   332   params -> (string -> minimize_command) -> prover_problem -> prover_result
   333 
   334 
   335 (* configuration attributes *)
   336 
   337 val concealedN = "concealed"
   338 val liftingN = "lifting"
   339 val combinatorsN = "combinators"
   340 val lambdasN = "lambdas"
   341 val smartN = "smart"
   342 
   343 (* Empty string means create files in Isabelle's temporary files directory. *)
   344 val dest_dir =
   345   Attrib.setup_config_string @{binding sledgehammer_dest_dir} (K "")
   346 val problem_prefix =
   347   Attrib.setup_config_string @{binding sledgehammer_problem_prefix} (K "prob")
   348 val measure_run_time =
   349   Attrib.setup_config_bool @{binding sledgehammer_measure_run_time} (K false)
   350 
   351 val atp_lambda_translation =
   352   Attrib.setup_config_string @{binding sledgehammer_atp_lambda_translation}
   353                              (K smartN)
   354 (* In addition to being easier to read, readable names are often much shorter,
   355    especially if types are mangled in names. For these reason, they are enabled
   356    by default. *)
   357 val atp_readable_names =
   358   Attrib.setup_config_bool @{binding sledgehammer_atp_readable_names} (K true)
   359 
   360 val smt_triggers =
   361   Attrib.setup_config_bool @{binding sledgehammer_smt_triggers} (K true)
   362 val smt_weights =
   363   Attrib.setup_config_bool @{binding sledgehammer_smt_weights} (K true)
   364 val smt_weight_min_facts =
   365   Attrib.setup_config_int @{binding sledgehammer_smt_weight_min_facts} (K 20)
   366 
   367 (* FUDGE *)
   368 val smt_min_weight =
   369   Attrib.setup_config_int @{binding sledgehammer_smt_min_weight} (K 0)
   370 val smt_max_weight =
   371   Attrib.setup_config_int @{binding sledgehammer_smt_max_weight} (K 10)
   372 val smt_max_weight_index =
   373   Attrib.setup_config_int @{binding sledgehammer_smt_max_weight_index} (K 200)
   374 val smt_weight_curve = Unsynchronized.ref (fn x : int => x * x)
   375 
   376 fun smt_fact_weight ctxt j num_facts =
   377   if Config.get ctxt smt_weights andalso
   378      num_facts >= Config.get ctxt smt_weight_min_facts then
   379     let
   380       val min = Config.get ctxt smt_min_weight
   381       val max = Config.get ctxt smt_max_weight
   382       val max_index = Config.get ctxt smt_max_weight_index
   383       val curve = !smt_weight_curve
   384     in
   385       SOME (max - (max - min + 1) * curve (Int.max (0, max_index - j - 1))
   386             div curve max_index)
   387     end
   388   else
   389     NONE
   390 
   391 fun weight_smt_fact ctxt num_facts ((info, th), j) =
   392   let val thy = Proof_Context.theory_of ctxt in
   393     (info, (smt_fact_weight ctxt j num_facts, th |> Thm.transfer thy))
   394   end
   395 
   396 fun untranslated_fact (Untranslated_Fact p) = p
   397   | untranslated_fact (SMT_Weighted_Fact (info, (_, th))) = (info, th)
   398 fun smt_weighted_fact _ _ (SMT_Weighted_Fact p, _) = p
   399   | smt_weighted_fact ctxt num_facts (fact, j) =
   400     (untranslated_fact fact, j) |> weight_smt_fact ctxt num_facts
   401 
   402 fun overlord_file_location_for_prover prover =
   403   (getenv "ISABELLE_HOME_USER", "prob_" ^ prover)
   404 
   405 fun with_path cleanup after f path =
   406   Exn.capture f path
   407   |> tap (fn _ => cleanup path)
   408   |> Exn.release
   409   |> tap (after path)
   410 
   411 fun proof_banner mode name =
   412   case mode of
   413     Auto_Try => "Auto Sledgehammer (" ^ quote name ^ ") found a proof"
   414   | Try => "Sledgehammer (" ^ quote name ^ ") found a proof"
   415   | _ => "Try this"
   416 
   417 (* based on "Mirabelle.can_apply" and generalized *)
   418 fun timed_apply timeout tac state i =
   419   let
   420     val {context = ctxt, facts, goal} = Proof.goal state
   421     val full_tac = Method.insert_tac facts i THEN tac ctxt i
   422   in TimeLimit.timeLimit timeout (try (Seq.pull o full_tac)) goal end
   423 
   424 fun tac_for_reconstructor Metis =
   425     Metis_Tactics.metis_tac [Metis_Tactics.partial_type_enc]
   426   | tac_for_reconstructor Metis_Full_Types =
   427     Metis_Tactics.metis_tac Metis_Tactics.full_type_syss
   428   | tac_for_reconstructor Metis_No_Types =
   429     Metis_Tactics.metis_tac [Metis_Tactics.no_type_enc]
   430   | tac_for_reconstructor _ = raise Fail "unexpected reconstructor"
   431 
   432 fun timed_reconstructor reconstructor debug timeout ths =
   433   (Config.put Metis_Tactics.verbose debug
   434    #> (fn ctxt => tac_for_reconstructor reconstructor ctxt ths))
   435   |> timed_apply timeout
   436 
   437 fun filter_used_facts used = filter (member (op =) used o fst)
   438 
   439 fun play_one_line_proof debug timeout ths state i reconstructors =
   440   let
   441     fun play [] [] = Failed_to_Play (hd reconstructors)
   442       | play timed_outs [] = Trust_Playable (List.last timed_outs, SOME timeout)
   443       | play timed_out (reconstructor :: reconstructors) =
   444         let val timer = Timer.startRealTimer () in
   445           case timed_reconstructor reconstructor debug timeout ths state i of
   446             SOME (SOME _) => Played (reconstructor, Timer.checkRealTimer timer)
   447           | _ => play timed_out reconstructors
   448         end
   449         handle TimeLimit.TimeOut =>
   450                play (reconstructor :: timed_out) reconstructors
   451   in
   452     if timeout = Time.zeroTime then Trust_Playable (hd reconstructors, NONE)
   453     else play [] reconstructors
   454   end
   455 
   456 
   457 (* generic TPTP-based ATPs *)
   458 
   459 (* Too general means, positive equality literal with a variable X as one
   460    operand, when X does not occur properly in the other operand. This rules out
   461    clearly inconsistent facts such as X = a | X = b, though it by no means
   462    guarantees soundness. *)
   463 
   464 (* Unwanted equalities are those between a (bound or schematic) variable that
   465    does not properly occur in the second operand. *)
   466 val is_exhaustive_finite =
   467   let
   468     fun is_bad_equal (Var z) t =
   469         not (exists_subterm (fn Var z' => z = z' | _ => false) t)
   470       | is_bad_equal (Bound j) t = not (loose_bvar1 (t, j))
   471       | is_bad_equal _ _ = false
   472     fun do_equals t1 t2 = is_bad_equal t1 t2 orelse is_bad_equal t2 t1
   473     fun do_formula pos t =
   474       case (pos, t) of
   475         (_, @{const Trueprop} $ t1) => do_formula pos t1
   476       | (true, Const (@{const_name all}, _) $ Abs (_, _, t')) =>
   477         do_formula pos t'
   478       | (true, Const (@{const_name All}, _) $ Abs (_, _, t')) =>
   479         do_formula pos t'
   480       | (false, Const (@{const_name Ex}, _) $ Abs (_, _, t')) =>
   481         do_formula pos t'
   482       | (_, @{const "==>"} $ t1 $ t2) =>
   483         do_formula (not pos) t1 andalso
   484         (t2 = @{prop False} orelse do_formula pos t2)
   485       | (_, @{const HOL.implies} $ t1 $ t2) =>
   486         do_formula (not pos) t1 andalso
   487         (t2 = @{const False} orelse do_formula pos t2)
   488       | (_, @{const Not} $ t1) => do_formula (not pos) t1
   489       | (true, @{const HOL.disj} $ t1 $ t2) => forall (do_formula pos) [t1, t2]
   490       | (false, @{const HOL.conj} $ t1 $ t2) => forall (do_formula pos) [t1, t2]
   491       | (true, Const (@{const_name HOL.eq}, _) $ t1 $ t2) => do_equals t1 t2
   492       | (true, Const (@{const_name "=="}, _) $ t1 $ t2) => do_equals t1 t2
   493       | _ => false
   494   in do_formula true end
   495 
   496 fun has_bound_or_var_of_type pred =
   497   exists_subterm (fn Var (_, T as Type _) => pred T
   498                    | Abs (_, T as Type _, _) => pred T
   499                    | _ => false)
   500 
   501 (* Facts are forbidden to contain variables of these types. The typical reason
   502    is that they lead to unsoundness. Note that "unit" satisfies numerous
   503    equations like "?x = ()". The resulting clauses will have no type constraint,
   504    yielding false proofs. Even "bool" leads to many unsound proofs, though only
   505    for higher-order problems. *)
   506 
   507 (* Facts containing variables of type "unit" or "bool" or of the form
   508    "ALL x. x = A | x = B | x = C" are likely to lead to unsound proofs if types
   509    are omitted. *)
   510 fun is_dangerous_prop ctxt =
   511   transform_elim_prop
   512   #> (has_bound_or_var_of_type (is_type_surely_finite ctxt false) orf
   513       is_exhaustive_finite)
   514 
   515 fun int_opt_add (SOME m) (SOME n) = SOME (m + n)
   516   | int_opt_add _ _ = NONE
   517 
   518 (* Important messages are important but not so important that users want to see
   519    them each time. *)
   520 val atp_important_message_keep_quotient = 10
   521 
   522 fun choose_format_and_type_enc best_type_enc formats type_enc_opt =
   523   (case type_enc_opt of
   524      SOME ts => ts
   525    | NONE => type_enc_from_string best_type_enc)
   526   |> choose_format formats
   527 
   528 fun translate_atp_lambdas ctxt type_enc =
   529   Config.get ctxt atp_lambda_translation
   530   |> (fn trans =>
   531          if trans = smartN then
   532            if is_type_enc_higher_order type_enc then lambdasN else combinatorsN
   533          else if trans = lambdasN andalso
   534                  not (is_type_enc_higher_order type_enc) then
   535            error ("Lambda translation method incompatible with first-order \
   536                   \encoding.")
   537          else
   538            trans)
   539   |> (fn trans =>
   540          if trans = concealedN then
   541            rpair [] o map (conceal_lambdas ctxt)
   542          else if trans = liftingN then
   543            map (close_form o Envir.eta_contract)
   544            #> SMT_Translate.lift_lambdas ctxt false #> snd #> swap
   545          else if trans = combinatorsN then
   546            rpair [] o map (introduce_combinators ctxt)
   547          else if trans = lambdasN then
   548            rpair [] o map (Envir.eta_contract)
   549          else
   550            error ("Unknown lambda translation method: " ^ quote trans ^ "."))
   551 
   552 val metis_minimize_max_time = seconds 2.0
   553 
   554 fun choose_minimize_command minimize_command name preplay =
   555   (case preplay of
   556      Played (reconstructor, time) =>
   557      if Time.<= (time, metis_minimize_max_time) then
   558        prover_name_for_reconstructor reconstructor |> the_default name
   559      else
   560        name
   561    | _ => name)
   562   |> minimize_command
   563 
   564 fun repair_monomorph_context max_iters max_new_instances =
   565   Config.put Monomorph.max_rounds max_iters
   566   #> Config.put Monomorph.max_new_instances max_new_instances
   567   #> Config.put Monomorph.keep_partial_instances false
   568 
   569 (* Give the ATPs some slack before interrupting them the hard way. "z3_atp" on
   570    Linux appears to be the only ATP that does not honor its time limit. *)
   571 val atp_timeout_slack = seconds 1.0
   572 
   573 fun run_atp mode name
   574         ({exec, required_execs, arguments, proof_delims, known_failures,
   575           conj_sym_kind, prem_kind, formats, best_slices, ...} : atp_config)
   576         ({debug, verbose, overlord, type_enc, sound, max_relevant,
   577           max_mono_iters, max_new_mono_instances, isar_proof,
   578           isar_shrink_factor, slicing, timeout, preplay_timeout, ...} : params)
   579         minimize_command
   580         ({state, goal, subgoal, subgoal_count, facts, ...} : prover_problem) =
   581   let
   582     val thy = Proof.theory_of state
   583     val ctxt = Proof.context_of state
   584     val (_, hyp_ts, concl_t) = strip_subgoal ctxt goal subgoal
   585     val (dest_dir, problem_prefix) =
   586       if overlord then overlord_file_location_for_prover name
   587       else (Config.get ctxt dest_dir, Config.get ctxt problem_prefix)
   588     val problem_file_name =
   589       Path.basic (problem_prefix ^ (if overlord then "" else serial_string ()) ^
   590                   "_" ^ string_of_int subgoal)
   591     val problem_path_name =
   592       if dest_dir = "" then
   593         File.tmp_path problem_file_name
   594       else if File.exists (Path.explode dest_dir) then
   595         Path.append (Path.explode dest_dir) problem_file_name
   596       else
   597         error ("No such directory: " ^ quote dest_dir ^ ".")
   598     val measure_run_time = verbose orelse Config.get ctxt measure_run_time
   599     val command = Path.explode (getenv (fst exec) ^ "/" ^ snd exec)
   600     fun split_time s =
   601       let
   602         val split = String.tokens (fn c => str c = "\n")
   603         val (output, t) = s |> split |> split_last |> apfst cat_lines
   604         fun as_num f = f >> (fst o read_int)
   605         val num = as_num (Scan.many1 Symbol.is_ascii_digit)
   606         val digit = Scan.one Symbol.is_ascii_digit
   607         val num3 = as_num (digit ::: digit ::: (digit >> single))
   608         val time = num --| Scan.$$ "." -- num3 >> (fn (a, b) => a * 1000 + b)
   609         val as_time = Scan.read Symbol.stopper time o raw_explode
   610       in (output, as_time t) end
   611     fun run_on prob_file =
   612       case filter (curry (op =) "" o getenv o fst) (exec :: required_execs) of
   613         (home_var, _) :: _ =>
   614         error ("The environment variable " ^ quote home_var ^ " is not set.")
   615       | [] =>
   616         if File.exists command then
   617           let
   618             (* If slicing is disabled, we expand the last slice to fill the
   619                entire time available. *)
   620             val actual_slices = get_slices slicing (best_slices ctxt)
   621             val num_actual_slices = length actual_slices
   622             fun monomorphize_facts facts =
   623               let
   624                 val ctxt =
   625                   ctxt |> repair_monomorph_context max_mono_iters
   626                                                    max_new_mono_instances
   627                 (* pseudo-theorem involving the same constants as the subgoal *)
   628                 val subgoal_th =
   629                   Logic.list_implies (hyp_ts, concl_t)
   630                   |> Skip_Proof.make_thm thy
   631                 val rths =
   632                   facts |> chop (length facts div 4)
   633                         |>> map (pair 1 o snd)
   634                         ||> map (pair 2 o snd)
   635                         |> op @
   636                         |> cons (0, subgoal_th)
   637               in
   638                 Monomorph.monomorph atp_schematic_consts_of rths ctxt
   639                 |> fst |> tl
   640                 |> curry ListPair.zip (map fst facts)
   641                 |> maps (fn (name, rths) => map (pair name o snd) rths)
   642               end
   643             fun run_slice (slice, (time_frac, (complete,
   644                                     (best_max_relevant, best_type_enc, extra))))
   645                           time_left =
   646               let
   647                 val num_facts =
   648                   length facts |> is_none max_relevant
   649                                   ? Integer.min best_max_relevant
   650                 val (format, type_enc) =
   651                   choose_format_and_type_enc best_type_enc formats type_enc
   652                 val fairly_sound = is_type_enc_fairly_sound type_enc
   653                 val facts =
   654                   facts |> map untranslated_fact
   655                         |> not fairly_sound
   656                            ? filter_out (is_dangerous_prop ctxt o prop_of o snd)
   657                         |> take num_facts
   658                         |> polymorphism_of_type_enc type_enc <> Polymorphic
   659                            ? monomorphize_facts
   660                         |> map (apsnd prop_of)
   661                 val real_ms = Real.fromInt o Time.toMilliseconds
   662                 val slice_timeout =
   663                   ((real_ms time_left
   664                     |> (if slice < num_actual_slices - 1 then
   665                           curry Real.min (time_frac * real_ms timeout)
   666                         else
   667                           I))
   668                    * 0.001) |> seconds
   669                 val generous_slice_timeout =
   670                   Time.+ (slice_timeout, atp_timeout_slack)
   671                 val _ =
   672                   if debug then
   673                     quote name ^ " slice #" ^ string_of_int (slice + 1) ^
   674                     " with " ^ string_of_int num_facts ^ " fact" ^
   675                     plural_s num_facts ^ " for " ^
   676                     string_from_time slice_timeout ^ "..."
   677                     |> Output.urgent_message
   678                   else
   679                     ()
   680                 val (atp_problem, pool, conjecture_offset, facts_offset,
   681                      fact_names, typed_helpers, sym_tab) =
   682                   prepare_atp_problem ctxt format conj_sym_kind prem_kind
   683                       type_enc sound false (translate_atp_lambdas ctxt type_enc)
   684                       (Config.get ctxt atp_readable_names) true hyp_ts concl_t
   685                       facts
   686                 fun weights () = atp_problem_weights atp_problem
   687                 val full_proof = debug orelse isar_proof
   688                 val core =
   689                   File.shell_path command ^ " " ^
   690                   arguments ctxt full_proof extra slice_timeout weights ^ " " ^
   691                   File.shell_path prob_file
   692                 val command =
   693                   (if measure_run_time then
   694                      "TIMEFORMAT='%3R'; { time " ^ core ^ " ; }"
   695                    else
   696                      "exec " ^ core) ^ " 2>&1"
   697                 val _ =
   698                   atp_problem
   699                   |> tptp_lines_for_atp_problem format
   700                   |> cons ("% " ^ command ^ "\n")
   701                   |> File.write_list prob_file
   702                 val conjecture_shape =
   703                   conjecture_offset + 1
   704                     upto conjecture_offset + length hyp_ts + 1
   705                   |> map single
   706                 val ((output, msecs), (atp_proof, outcome)) =
   707                   TimeLimit.timeLimit generous_slice_timeout Isabelle_System.bash_output command
   708                   |>> (if overlord then
   709                          prefix ("% " ^ command ^ "\n% " ^ timestamp () ^ "\n")
   710                        else
   711                          I)
   712                   |> fst
   713                   |> (if measure_run_time then split_time else rpair NONE)
   714                   |> (fn accum as (output, _) =>
   715                          (accum,
   716                           extract_tstplike_proof_and_outcome verbose complete
   717                               proof_delims known_failures output
   718                           |>> atp_proof_from_tstplike_proof atp_problem output
   719                           handle UNRECOGNIZED_ATP_PROOF () =>
   720                                  ([], SOME ProofIncomplete)))
   721                   handle TimeLimit.TimeOut =>
   722                          (("", SOME (Time.toMilliseconds slice_timeout)),
   723                           ([], SOME TimedOut))
   724                 val outcome =
   725                   case outcome of
   726                     NONE =>
   727                     used_facts_in_unsound_atp_proof ctxt
   728                         conjecture_shape facts_offset fact_names atp_proof
   729                     |> Option.map (fn facts =>
   730                            UnsoundProof
   731                                (if is_type_enc_virtually_sound type_enc then
   732                                   SOME sound
   733                                 else
   734                                   NONE, facts |> sort string_ord))
   735                   | _ => outcome
   736               in
   737                 ((pool, conjecture_shape, facts_offset, fact_names,
   738                   typed_helpers, sym_tab),
   739                  (output, msecs, atp_proof, outcome))
   740               end
   741             val timer = Timer.startRealTimer ()
   742             fun maybe_run_slice slice (result as (_, (_, msecs0, _, SOME _))) =
   743                 let
   744                   val time_left = Time.- (timeout, Timer.checkRealTimer timer)
   745                 in
   746                   if Time.<= (time_left, Time.zeroTime) then
   747                     result
   748                   else
   749                     (run_slice slice time_left
   750                      |> (fn (stuff, (output, msecs, atp_proof, outcome)) =>
   751                             (stuff, (output, int_opt_add msecs0 msecs,
   752                                      atp_proof, outcome))))
   753                 end
   754               | maybe_run_slice _ result = result
   755           in
   756             ((Symtab.empty, [], 0, Vector.fromList [], [], Symtab.empty),
   757              ("", SOME 0, [], SOME InternalError))
   758             |> fold maybe_run_slice actual_slices
   759           end
   760         else
   761           error ("Bad executable: " ^ Path.print command)
   762 
   763     (* If the problem file has not been exported, remove it; otherwise, export
   764        the proof file too. *)
   765     fun cleanup prob_file =
   766       if dest_dir = "" then try File.rm prob_file else NONE
   767     fun export prob_file (_, (output, _, _, _)) =
   768       if dest_dir = "" then
   769         ()
   770       else
   771         File.write (Path.explode (Path.implode prob_file ^ "_proof")) output
   772     val ((pool, conjecture_shape, facts_offset, fact_names, typed_helpers,
   773           sym_tab),
   774          (output, msecs, atp_proof, outcome)) =
   775       with_path cleanup export run_on problem_path_name
   776     val important_message =
   777       if mode = Normal andalso
   778          random_range 0 (atp_important_message_keep_quotient - 1) = 0 then
   779         extract_important_message output
   780       else
   781         ""
   782     val (used_facts, preplay, message, message_tail) =
   783       case outcome of
   784         NONE =>
   785         let
   786           val used_facts =
   787             used_facts_in_atp_proof ctxt facts_offset fact_names atp_proof
   788         in
   789           (used_facts,
   790            fn () =>
   791               let
   792                 val used_ths =
   793                   facts |> map untranslated_fact |> filter_used_facts used_facts
   794                         |> map snd
   795               in
   796                 (if mode = Minimize then
   797                    Output.urgent_message "Preplaying proof..."
   798                  else
   799                    ());
   800                 play_one_line_proof debug preplay_timeout used_ths state subgoal
   801                                     metis_reconstructors
   802               end,
   803            fn preplay =>
   804               let
   805                 val full_types = uses_typed_helpers typed_helpers atp_proof
   806                 val isar_params =
   807                   (debug, full_types, isar_shrink_factor, pool,
   808                    conjecture_shape, facts_offset, fact_names, sym_tab,
   809                    atp_proof, goal)
   810                 val one_line_params =
   811                   (preplay, proof_banner mode name, used_facts,
   812                    choose_minimize_command minimize_command name preplay,
   813                    subgoal, subgoal_count)
   814               in proof_text ctxt isar_proof isar_params one_line_params end,
   815            (if verbose then
   816               "\nATP real CPU time: " ^
   817               string_from_time (Time.fromMilliseconds (the msecs)) ^ "."
   818             else
   819               "") ^
   820            (if important_message <> "" then
   821               "\n\nImportant message from Dr. Geoff Sutcliffe:\n" ^
   822               important_message
   823             else
   824               ""))
   825         end
   826       | SOME failure =>
   827         ([], K (Failed_to_Play Metis), fn _ => string_for_failure failure, "")
   828   in
   829     {outcome = outcome, used_facts = used_facts, run_time_in_msecs = msecs,
   830      preplay = preplay, message = message, message_tail = message_tail}
   831   end
   832 
   833 (* "SMT_Failure.Abnormal_Termination" carries the solver's return code. Until
   834    these are sorted out properly in the SMT module, we have to interpret these
   835    ourselves. *)
   836 val remote_smt_failures =
   837   [(2, NoLibwwwPerl),
   838    (22, CantConnect)]
   839 val z3_failures =
   840   [(101, OutOfResources),
   841    (103, MalformedInput),
   842    (110, MalformedInput)]
   843 val unix_failures =
   844   [(139, Crashed)]
   845 val smt_failures = remote_smt_failures @ z3_failures @ unix_failures
   846 
   847 fun failure_from_smt_failure (SMT_Failure.Counterexample {is_real_cex, ...}) =
   848     if is_real_cex then Unprovable else GaveUp
   849   | failure_from_smt_failure SMT_Failure.Time_Out = TimedOut
   850   | failure_from_smt_failure (SMT_Failure.Abnormal_Termination code) =
   851     (case AList.lookup (op =) smt_failures code of
   852        SOME failure => failure
   853      | NONE => UnknownError ("Abnormal termination with exit code " ^
   854                              string_of_int code ^ "."))
   855   | failure_from_smt_failure SMT_Failure.Out_Of_Memory = OutOfResources
   856   | failure_from_smt_failure (SMT_Failure.Other_Failure msg) =
   857     UnknownError msg
   858 
   859 (* FUDGE *)
   860 val smt_max_slices =
   861   Attrib.setup_config_int @{binding sledgehammer_smt_max_slices} (K 8)
   862 val smt_slice_fact_frac =
   863   Attrib.setup_config_real @{binding sledgehammer_smt_slice_fact_frac} (K 0.5)
   864 val smt_slice_time_frac =
   865   Attrib.setup_config_real @{binding sledgehammer_smt_slice_time_frac} (K 0.5)
   866 val smt_slice_min_secs =
   867   Attrib.setup_config_int @{binding sledgehammer_smt_slice_min_secs} (K 5)
   868 
   869 fun smt_filter_loop ctxt name
   870                     ({debug, verbose, overlord, max_mono_iters,
   871                       max_new_mono_instances, timeout, slicing, ...} : params)
   872                     state i smt_filter =
   873   let
   874     val max_slices = if slicing then Config.get ctxt smt_max_slices else 1
   875     val repair_context =
   876       select_smt_solver name
   877       #> (if overlord then
   878             Config.put SMT_Config.debug_files
   879                        (overlord_file_location_for_prover name
   880                         |> (fn (path, name) => path ^ "/" ^ name))
   881           else
   882             I)
   883       #> Config.put SMT_Config.infer_triggers (Config.get ctxt smt_triggers)
   884     val state = state |> Proof.map_context repair_context
   885     fun do_slice timeout slice outcome0 time_so_far facts =
   886       let
   887         val timer = Timer.startRealTimer ()
   888         val state =
   889           state |> Proof.map_context
   890                        (repair_monomorph_context max_mono_iters
   891                                                  max_new_mono_instances)
   892         val ms = timeout |> Time.toMilliseconds
   893         val slice_timeout =
   894           if slice < max_slices then
   895             Int.min (ms,
   896                 Int.max (1000 * Config.get ctxt smt_slice_min_secs,
   897                     Real.ceil (Config.get ctxt smt_slice_time_frac
   898                                * Real.fromInt ms)))
   899             |> Time.fromMilliseconds
   900           else
   901             timeout
   902         val num_facts = length facts
   903         val _ =
   904           if debug then
   905             quote name ^ " slice " ^ string_of_int slice ^ " with " ^
   906             string_of_int num_facts ^ " fact" ^ plural_s num_facts ^ " for " ^
   907             string_from_time slice_timeout ^ "..."
   908             |> Output.urgent_message
   909           else
   910             ()
   911         val birth = Timer.checkRealTimer timer
   912         val _ =
   913           if debug then Output.urgent_message "Invoking SMT solver..." else ()
   914         val (outcome, used_facts) =
   915           (case (slice, smt_filter) of
   916              (1, SOME head) => head |> apsnd (apsnd repair_context)
   917            | _ => SMT_Solver.smt_filter_preprocess state facts i)
   918           |> SMT_Solver.smt_filter_apply slice_timeout
   919           |> (fn {outcome, used_facts} => (outcome, used_facts))
   920           handle exn => if Exn.is_interrupt exn then
   921                           reraise exn
   922                         else
   923                           (ML_Compiler.exn_message exn
   924                            |> SMT_Failure.Other_Failure |> SOME, [])
   925         val death = Timer.checkRealTimer timer
   926         val outcome0 = if is_none outcome0 then SOME outcome else outcome0
   927         val time_so_far = Time.+ (time_so_far, Time.- (death, birth))
   928         val too_many_facts_perhaps =
   929           case outcome of
   930             NONE => false
   931           | SOME (SMT_Failure.Counterexample _) => false
   932           | SOME SMT_Failure.Time_Out => slice_timeout <> timeout
   933           | SOME (SMT_Failure.Abnormal_Termination _) => true (* kind of *)
   934           | SOME SMT_Failure.Out_Of_Memory => true
   935           | SOME (SMT_Failure.Other_Failure _) => true
   936         val timeout = Time.- (timeout, Timer.checkRealTimer timer)
   937       in
   938         if too_many_facts_perhaps andalso slice < max_slices andalso
   939            num_facts > 0 andalso Time.> (timeout, Time.zeroTime) then
   940           let
   941             val new_num_facts =
   942               Real.ceil (Config.get ctxt smt_slice_fact_frac
   943                          * Real.fromInt num_facts)
   944             val _ =
   945               if verbose andalso is_some outcome then
   946                 quote name ^ " invoked with " ^ string_of_int num_facts ^
   947                 " fact" ^ plural_s num_facts ^ ": " ^
   948                 string_for_failure (failure_from_smt_failure (the outcome)) ^
   949                 " Retrying with " ^ string_of_int new_num_facts ^ " fact" ^
   950                 plural_s new_num_facts ^ "..."
   951                 |> Output.urgent_message
   952               else
   953                 ()
   954           in
   955             facts |> take new_num_facts
   956                   |> do_slice timeout (slice + 1) outcome0 time_so_far
   957           end
   958         else
   959           {outcome = if is_none outcome then NONE else the outcome0,
   960            used_facts = used_facts,
   961            run_time_in_msecs = SOME (Time.toMilliseconds time_so_far)}
   962       end
   963   in do_slice timeout 1 NONE Time.zeroTime end
   964 
   965 fun run_smt_solver mode name (params as {debug, verbose, preplay_timeout, ...})
   966         minimize_command
   967         ({state, subgoal, subgoal_count, facts, smt_filter, ...}
   968          : prover_problem) =
   969   let
   970     val ctxt = Proof.context_of state
   971     val num_facts = length facts
   972     val facts = facts ~~ (0 upto num_facts - 1)
   973                 |> map (smt_weighted_fact ctxt num_facts)
   974     val {outcome, used_facts, run_time_in_msecs} =
   975       smt_filter_loop ctxt name params state subgoal smt_filter facts
   976     val (used_facts, used_ths) = used_facts |> ListPair.unzip
   977     val outcome = outcome |> Option.map failure_from_smt_failure
   978     val (preplay, message, message_tail) =
   979       case outcome of
   980         NONE =>
   981         (fn () =>
   982             let
   983               fun smt_settings () =
   984                 if name = SMT_Solver.solver_name_of ctxt then ""
   985                 else "smt_solver = " ^ maybe_quote name
   986             in
   987               case play_one_line_proof debug preplay_timeout used_ths state
   988                                        subgoal metis_reconstructors of
   989                 p as Played _ => p
   990               | _ => Trust_Playable (SMT (smt_settings ()), NONE)
   991             end,
   992          fn preplay =>
   993             let
   994               val one_line_params =
   995                 (preplay, proof_banner mode name, used_facts,
   996                  choose_minimize_command minimize_command name preplay,
   997                  subgoal, subgoal_count)
   998             in one_line_proof_text one_line_params end,
   999          if verbose then
  1000            "\nSMT solver real CPU time: " ^
  1001            string_from_time (Time.fromMilliseconds
  1002                                  (the run_time_in_msecs)) ^ "."
  1003          else
  1004            "")
  1005       | SOME failure =>
  1006         (K (Failed_to_Play Metis), fn _ => string_for_failure failure, "")
  1007   in
  1008     {outcome = outcome, used_facts = used_facts,
  1009      run_time_in_msecs = run_time_in_msecs, preplay = preplay,
  1010      message = message, message_tail = message_tail}
  1011   end
  1012 
  1013 fun run_metis mode name ({debug, timeout, ...} : params) minimize_command
  1014               ({state, subgoal, subgoal_count, facts, ...} : prover_problem) =
  1015   let
  1016     val reconstructor =
  1017       case AList.lookup (op =) metis_prover_infos name of
  1018         SOME r => r
  1019       | NONE => raise Fail ("unknown Metis version: " ^ quote name)
  1020     val (used_facts, used_ths) =
  1021       facts |> map untranslated_fact |> ListPair.unzip
  1022   in
  1023     case play_one_line_proof debug timeout used_ths state subgoal
  1024                              [reconstructor] of
  1025       play as Played (_, time) =>
  1026       {outcome = NONE, used_facts = used_facts,
  1027        run_time_in_msecs = SOME (Time.toMilliseconds time),
  1028        preplay = K play,
  1029        message = fn play =>
  1030                     let
  1031                       val one_line_params =
  1032                          (play, proof_banner mode name, used_facts,
  1033                           minimize_command name, subgoal, subgoal_count)
  1034                     in one_line_proof_text one_line_params end,
  1035        message_tail = ""}
  1036     | play =>
  1037       let
  1038         val failure = case play of Failed_to_Play _ => GaveUp | _ => TimedOut
  1039       in
  1040         {outcome = SOME failure, used_facts = [], run_time_in_msecs = NONE,
  1041          preplay = K play, message = fn _ => string_for_failure failure,
  1042          message_tail = ""}
  1043       end
  1044   end
  1045 
  1046 fun get_prover ctxt mode name =
  1047   let val thy = Proof_Context.theory_of ctxt in
  1048     if is_metis_prover name then run_metis mode name
  1049     else if is_atp thy name then run_atp mode name (get_atp thy name)
  1050     else if is_smt_prover ctxt name then run_smt_solver mode name
  1051     else error ("No such prover: " ^ name ^ ".")
  1052   end
  1053 
  1054 end;