wneuper/isa: src/HOL/Tools/Sledgehammer/sledgehammer

     1 (*  Title:      HOL/Tools/Sledgehammer/sledgehammer_provers.ML

     2     Author:     Fabian Immler, TU Muenchen

     3     Author:     Makarius

     4     Author:     Jasmin Blanchette, TU Muenchen

     6 Generic prover abstraction for Sledgehammer.

     7 *)

     9 signature SLEDGEHAMMER_PROVERS =

    10 sig

    11   type failure = ATP_Proof.failure

    12   type locality = Sledgehammer_Filter.locality

    13   type relevance_fudge = Sledgehammer_Filter.relevance_fudge

    14   type translated_formula = Sledgehammer_ATP_Translate.translated_formula

    15   type type_system = Sledgehammer_ATP_Translate.type_system

    16   type minimize_command = Sledgehammer_ATP_Reconstruct.minimize_command

    18   datatype mode = Auto_Try | Try | Normal | Minimize

    20   datatype rich_type_system =

    21     Dumb_Type_Sys of type_system |

    22     Smart_Type_Sys of bool

    24   type params =

    25     {debug: bool,

    26      verbose: bool,

    27      overlord: bool,

    28      blocking: bool,

    29      provers: string list,

    30      type_sys: rich_type_system,

    31      relevance_thresholds: real * real,

    32      max_relevant: int option,

    33      max_mono_iters: int,

    34      max_new_mono_instances: int,

    35      explicit_apply: bool,

    36      isar_proof: bool,

    37      isar_shrink_factor: int,

    38      slicing: bool,

    39      timeout: Time.time,

    40      preplay_timeout: Time.time,

    41      expect: string}

    43   datatype prover_fact =

    44     Untranslated_Fact of (string * locality) * thm |

    45     SMT_Weighted_Fact of (string * locality) * (int option * thm)

    47   type prover_problem =

    48     {state: Proof.state,

    49      goal: thm,

    50      subgoal: int,

    51      subgoal_count: int,

    52      facts: prover_fact list,

    53      smt_filter: (string * locality) SMT_Solver.smt_filter_data option}

    55   type prover_result =

    56     {outcome: failure option,

    57      used_facts: (string * locality) list,

    58      run_time_in_msecs: int option,

    59      message: string}

    61   type prover = params -> minimize_command -> prover_problem -> prover_result

    63   val smt_triggers : bool Config.T

    64   val smt_weights : bool Config.T

    65   val smt_weight_min_facts : int Config.T

    66   val smt_min_weight : int Config.T

    67   val smt_max_weight : int Config.T

    68   val smt_max_weight_index : int Config.T

    69   val smt_weight_curve : (int -> int) Unsynchronized.ref

    70   val smt_max_slices : int Config.T

    71   val smt_slice_fact_frac : real Config.T

    72   val smt_slice_time_frac : real Config.T

    73   val smt_slice_min_secs : int Config.T

    74   val das_tool : string

    75   val select_smt_solver : string -> Proof.context -> Proof.context

    76   val is_smt_prover : Proof.context -> string -> bool

    77   val is_unit_equational_atp : Proof.context -> string -> bool

    78   val is_prover_supported : Proof.context -> string -> bool

    79   val is_prover_installed : Proof.context -> string -> bool

    80   val default_max_relevant_for_prover : Proof.context -> bool -> string -> int

    81   val is_unit_equality : term -> bool

    82   val is_appropriate_prop_for_prover : Proof.context -> string -> term -> bool

    83   val is_built_in_const_for_prover :

    84     Proof.context -> string -> string * typ -> term list -> bool * term list

    85   val atp_relevance_fudge : relevance_fudge

    86   val smt_relevance_fudge : relevance_fudge

    87   val relevance_fudge_for_prover : Proof.context -> string -> relevance_fudge

    88   val dest_dir : string Config.T

    89   val problem_prefix : string Config.T

    90   val measure_run_time : bool Config.T

    91   val weight_smt_fact :

    92     Proof.context -> int -> ((string * locality) * thm) * int

    93     -> (string * locality) * (int option * thm)

    94   val untranslated_fact : prover_fact -> (string * locality) * thm

    95   val smt_weighted_fact :

    96     Proof.context -> int -> prover_fact * int

    97     -> (string * locality) * (int option * thm)

    98   val supported_provers : Proof.context -> unit

    99   val kill_provers : unit -> unit

   100   val running_provers : unit -> unit

   101   val messages : int option -> unit

   102   val filter_used_facts : ''a list -> (''a * 'b) list -> (''a * 'b) list

   103   val get_prover : Proof.context -> mode -> string -> prover

   104 end;

   106 structure Sledgehammer_Provers : SLEDGEHAMMER_PROVERS =

   107 struct

   109 open ATP_Problem

   110 open ATP_Proof

   111 open ATP_Systems

   112 open Metis_Translate

   113 open Sledgehammer_Util

   114 open Sledgehammer_Filter

   115 open Sledgehammer_ATP_Translate

   116 open Sledgehammer_ATP_Reconstruct

   118 (** The Sledgehammer **)

   120 datatype mode = Auto_Try | Try | Normal | Minimize

   122 (* Identifier to distinguish Sledgehammer from other tools using

   123    "Async_Manager". *)

   124 val das_tool = "Sledgehammer"

   126 val select_smt_solver =

   127   Context.proof_map o SMT_Config.select_solver

   129 fun is_smt_prover ctxt name =

   130   member (op =) (SMT_Solver.available_solvers_of ctxt) name

   132 fun is_unit_equational_atp ctxt name =

   133   let val thy = Proof_Context.theory_of ctxt in

   134     case try (get_atp thy) name of

   135       SOME {formats, ...} => member (op =) formats CNF_UEQ

   136     | NONE => false

   137   end

   139 fun is_prover_supported ctxt name =

   140   let val thy = Proof_Context.theory_of ctxt in

   141     is_smt_prover ctxt name orelse member (op =) (supported_atps thy) name

   142   end

   144 fun is_prover_installed ctxt =

   145   is_smt_prover ctxt orf is_atp_installed (Proof_Context.theory_of ctxt)

   147 fun get_slices slicing slices =

   148   (0 upto length slices - 1) ~~ slices |> not slicing ? (List.last #> single)

   150 fun default_max_relevant_for_prover ctxt slicing name =

   151   let val thy = Proof_Context.theory_of ctxt in

   152     if is_smt_prover ctxt name then

   153       SMT_Solver.default_max_relevant ctxt name

   154     else

   155       fold (Integer.max o fst o snd o snd o snd)

   156            (get_slices slicing (#best_slices (get_atp thy name) ctxt)) 0

   157   end

   159 (* These are either simplified away by "Meson.presimplify" (most of the time) or

   160    handled specially via "fFalse", "fTrue", ..., "fequal". *)

   161 val atp_irrelevant_consts =

   162   [@{const_name False}, @{const_name True}, @{const_name Not},

   163    @{const_name conj}, @{const_name disj}, @{const_name implies},

   164    @{const_name HOL.eq}, @{const_name If}, @{const_name Let}]

   166 fun is_if (@{const_name If}, _) = true

   167   | is_if _ = false

   169 (* Beware of "if and only if" (which is translated as such) and "If" (which is

   170    translated to conditional equations). *)

   171 fun is_good_unit_equality T t u =

   172   T <> @{typ bool} andalso not (exists (exists_Const is_if) [t, u])

   174 fun is_unit_equality (@{const Trueprop} $ t) = is_unit_equality t

   175   | is_unit_equality (Const (@{const_name all}, _) $ Abs (_, _, t)) =

   176     is_unit_equality t

   177   | is_unit_equality (Const (@{const_name All}, _) $ Abs (_, _, t)) =

   178     is_unit_equality t

   179   | is_unit_equality (Const (@{const_name "=="}, Type (_, [T, _])) $ t $ u) =

   180     is_good_unit_equality T t u

   181   | is_unit_equality (Const (@{const_name HOL.eq}, Type (_ , [T, _])) $ t $ u) =

   182     is_good_unit_equality T t u

   183   | is_unit_equality _ = false

   185 fun is_appropriate_prop_for_prover ctxt name =

   186   if is_unit_equational_atp ctxt name then is_unit_equality else K true

   188 fun is_built_in_const_for_prover ctxt name =

   189   if is_smt_prover ctxt name then

   190     let val ctxt = ctxt |> select_smt_solver name in

   191       fn x => fn ts =>

   192          if SMT_Builtin.is_builtin_num_ext ctxt (list_comb (Const x, ts)) then

   193            (true, [])

   194          else if SMT_Builtin.is_builtin_fun_ext ctxt x ts then

   195            (true, ts)

   196          else

   197            (false, ts)

   198     end

   199   else

   200     fn (s, _) => fn ts => (member (op =) atp_irrelevant_consts s, ts)

   202 (* FUDGE *)

   203 val atp_relevance_fudge =

   204   {local_const_multiplier = 1.5,

   205    worse_irrel_freq = 100.0,

   206    higher_order_irrel_weight = 1.05,

   207    abs_rel_weight = 0.5,

   208    abs_irrel_weight = 2.0,

   209    skolem_irrel_weight = 0.25,

   210    theory_const_rel_weight = 0.5,

   211    theory_const_irrel_weight = 0.25,

   212    chained_const_irrel_weight = 0.25,

   213    intro_bonus = 0.15,

   214    elim_bonus = 0.15,

   215    simp_bonus = 0.15,

   216    local_bonus = 0.55,

   217    assum_bonus = 1.05,

   218    chained_bonus = 1.5,

   219    max_imperfect = 11.5,

   220    max_imperfect_exp = 1.0,

   221    threshold_divisor = 2.0,

   222    ridiculous_threshold = 0.01}

   224 (* FUDGE (FIXME) *)

   225 val smt_relevance_fudge =

   226   {local_const_multiplier = #local_const_multiplier atp_relevance_fudge,

   227    worse_irrel_freq = #worse_irrel_freq atp_relevance_fudge,

   228    higher_order_irrel_weight = #higher_order_irrel_weight atp_relevance_fudge,

   229    abs_rel_weight = #abs_rel_weight atp_relevance_fudge,

   230    abs_irrel_weight = #abs_irrel_weight atp_relevance_fudge,

   231    skolem_irrel_weight = #skolem_irrel_weight atp_relevance_fudge,

   232    theory_const_rel_weight = #theory_const_rel_weight atp_relevance_fudge,

   233    theory_const_irrel_weight = #theory_const_irrel_weight atp_relevance_fudge,

   234    chained_const_irrel_weight = #chained_const_irrel_weight atp_relevance_fudge,

   235    intro_bonus = #intro_bonus atp_relevance_fudge,

   236    elim_bonus = #elim_bonus atp_relevance_fudge,

   237    simp_bonus = #simp_bonus atp_relevance_fudge,

   238    local_bonus = #local_bonus atp_relevance_fudge,

   239    assum_bonus = #assum_bonus atp_relevance_fudge,

   240    chained_bonus = #chained_bonus atp_relevance_fudge,

   241    max_imperfect = #max_imperfect atp_relevance_fudge,

   242    max_imperfect_exp = #max_imperfect_exp atp_relevance_fudge,

   243    threshold_divisor = #threshold_divisor atp_relevance_fudge,

   244    ridiculous_threshold = #ridiculous_threshold atp_relevance_fudge}

   246 fun relevance_fudge_for_prover ctxt name =

   247   if is_smt_prover ctxt name then smt_relevance_fudge else atp_relevance_fudge

   249 fun supported_provers ctxt =

   250   let

   251     val thy = Proof_Context.theory_of ctxt

   252     val (remote_provers, local_provers) =

   253       sort_strings (supported_atps thy) @

   254       sort_strings (SMT_Solver.available_solvers_of ctxt)

   255       |> List.partition (String.isPrefix remote_prefix)

   256   in

   257     Output.urgent_message ("Supported provers: " ^

   258                            commas (local_provers @ remote_provers) ^ ".")

   259   end

   261 fun kill_provers () = Async_Manager.kill_threads das_tool "prover"

   262 fun running_provers () = Async_Manager.running_threads das_tool "prover"

   263 val messages = Async_Manager.thread_messages das_tool "prover"

   265 (** problems, results, ATPs, etc. **)

   267 datatype rich_type_system =

   268   Dumb_Type_Sys of type_system |

   269   Smart_Type_Sys of bool

   271 type params =

   272   {debug: bool,

   273    verbose: bool,

   274    overlord: bool,

   275    blocking: bool,

   276    provers: string list,

   277    type_sys: rich_type_system,

   278    relevance_thresholds: real * real,

   279    max_relevant: int option,

   280    max_mono_iters: int,

   281    max_new_mono_instances: int,

   282    explicit_apply: bool,

   283    isar_proof: bool,

   284    isar_shrink_factor: int,

   285    slicing: bool,

   286    timeout: Time.time,

   287    preplay_timeout: Time.time,

   288    expect: string}

   290 datatype prover_fact =

   291   Untranslated_Fact of (string * locality) * thm |

   292   SMT_Weighted_Fact of (string * locality) * (int option * thm)

   294 type prover_problem =

   295   {state: Proof.state,

   296    goal: thm,

   297    subgoal: int,

   298    subgoal_count: int,

   299    facts: prover_fact list,

   300    smt_filter: (string * locality) SMT_Solver.smt_filter_data option}

   302 type prover_result =

   303   {outcome: failure option,

   304    message: string,

   305    used_facts: (string * locality) list,

   306    run_time_in_msecs: int option}

   308 type prover = params -> minimize_command -> prover_problem -> prover_result

   311 (* configuration attributes *)

   313 val dest_dir =

   314   Attrib.setup_config_string @{binding sledgehammer_dest_dir} (K "")

   315   (* Empty string means create files in Isabelle's temporary files directory. *)

   317 val problem_prefix =

   318   Attrib.setup_config_string @{binding sledgehammer_problem_prefix} (K "prob")

   320 val measure_run_time =

   321   Attrib.setup_config_bool @{binding sledgehammer_measure_run_time} (K false)

   323 val smt_triggers =

   324   Attrib.setup_config_bool @{binding sledgehammer_smt_triggers} (K true)

   325 val smt_weights =

   326   Attrib.setup_config_bool @{binding sledgehammer_smt_weights} (K true)

   327 val smt_weight_min_facts =

   328   Attrib.setup_config_int @{binding sledgehammer_smt_weight_min_facts} (K 20)

   330 (* FUDGE *)

   331 val smt_min_weight =

   332   Attrib.setup_config_int @{binding sledgehammer_smt_min_weight} (K 0)

   333 val smt_max_weight =

   334   Attrib.setup_config_int @{binding sledgehammer_smt_max_weight} (K 10)

   335 val smt_max_weight_index =

   336   Attrib.setup_config_int @{binding sledgehammer_smt_max_weight_index} (K 200)

   337 val smt_weight_curve = Unsynchronized.ref (fn x : int => x * x)

   339 fun smt_fact_weight ctxt j num_facts =

   340   if Config.get ctxt smt_weights andalso

   341      num_facts >= Config.get ctxt smt_weight_min_facts then

   342     let

   343       val min = Config.get ctxt smt_min_weight

   344       val max = Config.get ctxt smt_max_weight

   345       val max_index = Config.get ctxt smt_max_weight_index

   346       val curve = !smt_weight_curve

   347     in

   348       SOME (max - (max - min + 1) * curve (Int.max (0, max_index - j - 1))

   349             div curve max_index)

   350     end

   351   else

   352     NONE

   354 fun weight_smt_fact ctxt num_facts ((info, th), j) =

   355   let val thy = Proof_Context.theory_of ctxt in

   356     (info, (smt_fact_weight ctxt j num_facts, th |> Thm.transfer thy))

   357   end

   359 fun untranslated_fact (Untranslated_Fact p) = p

   360   | untranslated_fact (SMT_Weighted_Fact (info, (_, th))) = (info, th)

   361 fun atp_translated_fact ctxt format type_sys fact =

   362   translate_atp_fact ctxt format type_sys false (untranslated_fact fact)

   363 fun smt_weighted_fact _ _ (SMT_Weighted_Fact p, _) = p

   364   | smt_weighted_fact ctxt num_facts (fact, j) =

   365     (untranslated_fact fact, j) |> weight_smt_fact ctxt num_facts

   367 fun overlord_file_location_for_prover prover =

   368   (getenv "ISABELLE_HOME_USER", "prob_" ^ prover)

   370 fun with_path cleanup after f path =

   371   Exn.capture f path

   372   |> tap (fn _ => cleanup path)

   373   |> Exn.release

   374   |> tap (after path)

   376 fun proof_banner mode blocking name =

   377   case mode of

   378     Auto_Try => "Auto Sledgehammer (" ^ quote name ^ ") found a proof"

   379   | Try => "Sledgehammer (" ^ quote name ^ ") found a proof"

   380   | Normal => if blocking then quote name ^ " found a proof"

   381               else "Try this"

   382   | Minimize => "Try this"

   384 (* based on "Mirabelle.can_apply" and generalized *)

   385 fun timed_apply timeout tac state i =

   386   let

   387     val {context = ctxt, facts, goal} = Proof.goal state

   388     val full_tac = Method.insert_tac facts i THEN tac ctxt i

   389   in TimeLimit.timeLimit timeout (try (Seq.pull o full_tac)) goal end

   391 fun tac_for_reconstructor Metis = Metis_Tactics.metisHO_tac

   392   | tac_for_reconstructor MetisFT = Metis_Tactics.metisFT_tac

   393   | tac_for_reconstructor _ = raise Fail "unexpected reconstructor"

   395 fun timed_reconstructor reconstructor debug timeout ths =

   396   (Config.put Metis_Tactics.verbose debug

   397    #> (fn ctxt => tac_for_reconstructor reconstructor ctxt ths))

   398   |> timed_apply timeout

   400 fun filter_used_facts used = filter (member (op =) used o fst)

   402 fun preplay_one_line_proof debug timeout ths state i reconstructors =

   403   let

   404     fun preplay [] [] = Failed_to_Preplay

   405       | preplay (timed_out :: _) [] = Trust_Playable (timed_out, SOME timeout)

   406       | preplay timed_out (reconstructor :: reconstructors) =

   407         let val timer = Timer.startRealTimer () in

   408           case timed_reconstructor reconstructor debug timeout ths state i of

   409             SOME (SOME _) =>

   410             Preplayed (reconstructor, Timer.checkRealTimer timer)

   411           | _ => preplay timed_out reconstructors

   412         end

   413         handle TimeLimit.TimeOut =>

   414                preplay (reconstructor :: timed_out) reconstructors

   415   in

   416     if timeout = Time.zeroTime then Trust_Playable (hd reconstructors, NONE)

   417     else preplay [] reconstructors

   418   end

   421 (* generic TPTP-based ATPs *)

   423 (* Too general means, positive equality literal with a variable X as one

   424    operand, when X does not occur properly in the other operand. This rules out

   425    clearly inconsistent facts such as X = a | X = b, though it by no means

   426    guarantees soundness. *)

   428 (* Unwanted equalities are those between a (bound or schematic) variable that

   429    does not properly occur in the second operand. *)

   430 val is_exhaustive_finite =

   431   let

   432     fun is_bad_equal (Var z) t =

   433         not (exists_subterm (fn Var z' => z = z' | _ => false) t)

   434       | is_bad_equal (Bound j) t = not (loose_bvar1 (t, j))

   435       | is_bad_equal _ _ = false

   436     fun do_equals t1 t2 = is_bad_equal t1 t2 orelse is_bad_equal t2 t1

   437     fun do_formula pos t =

   438       case (pos, t) of

   439         (_, @{const Trueprop} $ t1) => do_formula pos t1

   440       | (true, Const (@{const_name all}, _) $ Abs (_, _, t')) =>

   441         do_formula pos t'

   442       | (true, Const (@{const_name All}, _) $ Abs (_, _, t')) =>

   443         do_formula pos t'

   444       | (false, Const (@{const_name Ex}, _) $ Abs (_, _, t')) =>

   445         do_formula pos t'

   446       | (_, @{const "==>"} $ t1 $ t2) =>

   447         do_formula (not pos) t1 andalso

   448         (t2 = @{prop False} orelse do_formula pos t2)

   449       | (_, @{const HOL.implies} $ t1 $ t2) =>

   450         do_formula (not pos) t1 andalso

   451         (t2 = @{const False} orelse do_formula pos t2)

   452       | (_, @{const Not} $ t1) => do_formula (not pos) t1

   453       | (true, @{const HOL.disj} $ t1 $ t2) => forall (do_formula pos) [t1, t2]

   454       | (false, @{const HOL.conj} $ t1 $ t2) => forall (do_formula pos) [t1, t2]

   455       | (true, Const (@{const_name HOL.eq}, _) $ t1 $ t2) => do_equals t1 t2

   456       | (true, Const (@{const_name "=="}, _) $ t1 $ t2) => do_equals t1 t2

   457       | _ => false

   458   in do_formula true end

   460 fun has_bound_or_var_of_type pred =

   461   exists_subterm (fn Var (_, T as Type _) => pred T

   462                    | Abs (_, T as Type _, _) => pred T

   463                    | _ => false)

   465 (* Facts are forbidden to contain variables of these types. The typical reason

   466    is that they lead to unsoundness. Note that "unit" satisfies numerous

   467    equations like "?x = ()". The resulting clauses will have no type constraint,

   468    yielding false proofs. Even "bool" leads to many unsound proofs, though only

   469    for higher-order problems. *)

   471 (* Facts containing variables of type "unit" or "bool" or of the form

   472    "ALL x. x = A | x = B | x = C" are likely to lead to unsound proofs if types

   473    are omitted. *)

   474 fun is_dangerous_prop ctxt =

   475   transform_elim_prop

   476   #> (has_bound_or_var_of_type (is_type_surely_finite ctxt) orf

   477       is_exhaustive_finite)

   479 fun int_opt_add (SOME m) (SOME n) = SOME (m + n)

   480   | int_opt_add _ _ = NONE

   482 val atp_blacklist_max_iters = 10

   483 (* Important messages are important but not so important that users want to see

   484    them each time. *)

   485 val atp_important_message_keep_quotient = 10

   487 val fallback_best_type_systems =

   488   [Preds (Mangled_Monomorphic, Nonmonotonic_Types, Light)]

   490 fun adjust_dumb_type_sys formats (Simple_Types level) =

   491     if member (op =) formats THF then

   492       (THF, Simple_Types level)

   493     else if member (op =) formats TFF then

   494       (TFF, Simple_Types level)

   495     else

   496       adjust_dumb_type_sys formats (Preds (Mangled_Monomorphic, level, Heavy))

   497   | adjust_dumb_type_sys formats type_sys =

   498     (case hd formats of

   499        CNF_UEQ =>

   500        (CNF_UEQ, case type_sys of

   501                    Preds stuff =>

   502                    (if is_type_sys_fairly_sound type_sys then Preds else Tags)

   503                        stuff

   504                  | _ => type_sys)

   505      | format => (format, type_sys))

   507 fun determine_format_and_type_sys _ formats (Dumb_Type_Sys type_sys) =

   508     adjust_dumb_type_sys formats type_sys

   509   | determine_format_and_type_sys best_type_systems formats

   510                                   (Smart_Type_Sys full_types) =

   511     map type_sys_from_string best_type_systems @ fallback_best_type_systems

   512     |> find_first (if full_types then is_type_sys_virtually_sound else K true)

   513     |> the |> adjust_dumb_type_sys formats

   515 fun repair_smt_monomorph_context debug max_mono_iters max_mono_instances =

   516   Config.put SMT_Config.verbose debug

   517   #> Config.put SMT_Config.monomorph_full false

   518   #> Config.put SMT_Config.monomorph_limit max_mono_iters

   519   #> Config.put SMT_Config.monomorph_instances max_mono_instances

   521 fun run_atp mode name

   522         ({exec, required_execs, arguments, proof_delims, known_failures,

   523           conj_sym_kind, prem_kind, formats, best_slices, ...} : atp_config)

   524         ({debug, verbose, overlord, blocking, type_sys, max_relevant,

   525           max_mono_iters, max_new_mono_instances, explicit_apply, isar_proof,

   526           isar_shrink_factor, slicing, timeout, preplay_timeout, ...} : params)

   527         minimize_command

   528         ({state, goal, subgoal, subgoal_count, facts, ...} : prover_problem) =

   529   let

   530     val thy = Proof.theory_of state

   531     val ctxt = Proof.context_of state

   532     val (_, hyp_ts, concl_t) = strip_subgoal ctxt goal subgoal

   533     val (dest_dir, problem_prefix) =

   534       if overlord then overlord_file_location_for_prover name

   535       else (Config.get ctxt dest_dir, Config.get ctxt problem_prefix)

   536     val problem_file_name =

   537       Path.basic (problem_prefix ^ (if overlord then "" else serial_string ()) ^

   538                   "_" ^ string_of_int subgoal)

   539     val problem_path_name =

   540       if dest_dir = "" then

   541         File.tmp_path problem_file_name

   542       else if File.exists (Path.explode dest_dir) then

   543         Path.append (Path.explode dest_dir) problem_file_name

   544       else

   545         error ("No such directory: " ^ quote dest_dir ^ ".")

   546     val measure_run_time = verbose orelse Config.get ctxt measure_run_time

   547     val command = Path.explode (getenv (fst exec) ^ "/" ^ snd exec)

   548     fun split_time s =

   549       let

   550         val split = String.tokens (fn c => str c = "\n")

   551         val (output, t) = s |> split |> split_last |> apfst cat_lines

   552         fun as_num f = f >> (fst o read_int)

   553         val num = as_num (Scan.many1 Symbol.is_ascii_digit)

   554         val digit = Scan.one Symbol.is_ascii_digit

   555         val num3 = as_num (digit ::: digit ::: (digit >> single))

   556         val time = num --| Scan.$$ "." -- num3 >> (fn (a, b) => a * 1000 + b)

   557         val as_time = Scan.read Symbol.stopper time o raw_explode

   558       in (output, as_time t) end

   559     fun run_on prob_file =

   560       case filter (curry (op =) "" o getenv o fst) (exec :: required_execs) of

   561         (home_var, _) :: _ =>

   562         error ("The environment variable " ^ quote home_var ^ " is not set.")

   563       | [] =>

   564         if File.exists command then

   565           let

   566             (* If slicing is disabled, we expand the last slice to fill the

   567                entire time available. *)

   568             val actual_slices = get_slices slicing (best_slices ctxt)

   569             val num_actual_slices = length actual_slices

   570             fun monomorphize_facts facts =

   571               let

   572                 val facts = facts |> map untranslated_fact

   573                 (* pseudo-theorem involving the same constants as the subgoal *)

   574                 val subgoal_th =

   575                   Logic.list_implies (hyp_ts, concl_t)

   576                   |> Skip_Proof.make_thm thy

   577                 val indexed_facts =

   578                   (~1, subgoal_th) :: (0 upto length facts - 1 ~~ map snd facts)

   579                 val max_mono_instances = max_new_mono_instances + length facts

   580               in

   581                 ctxt |> repair_smt_monomorph_context debug max_mono_iters

   582                                                      max_mono_instances

   583                      |> SMT_Monomorph.monomorph indexed_facts

   584                      |> fst |> sort (int_ord o pairself fst)

   585                      |> filter_out (curry (op =) ~1 o fst)

   586                      |> map (Untranslated_Fact o apfst (fst o nth facts))

   587               end

   588             fun run_slice blacklist (slice, (time_frac, (complete,

   589                                        (best_max_relevant, best_type_systems))))

   590                           time_left =

   591               let

   592                 val num_facts =

   593                   length facts |> is_none max_relevant

   594                                   ? Integer.min best_max_relevant

   595                 val (format, type_sys) =

   596                   determine_format_and_type_sys best_type_systems formats

   597                                                 type_sys

   598                 val fairly_sound = is_type_sys_fairly_sound type_sys

   599                 val facts =

   600                   facts |> not fairly_sound

   601                            ? filter_out (is_dangerous_prop ctxt o prop_of o snd

   602                                          o untranslated_fact)

   603                         |> take num_facts

   604                         |> not (null blacklist)

   605                            ? filter_out (member (op =) blacklist o fst

   606                                          o untranslated_fact)

   607                         |> polymorphism_of_type_sys type_sys <> Polymorphic

   608                            ? monomorphize_facts

   609                         |> map (atp_translated_fact ctxt format type_sys)

   610                 val real_ms = Real.fromInt o Time.toMilliseconds

   611                 val slice_timeout =

   612                   ((real_ms time_left

   613                     |> (if slice < num_actual_slices - 1 then

   614                           curry Real.min (time_frac * real_ms timeout)

   615                         else

   616                           I))

   617                    * 0.001) |> seconds

   618                 val _ =

   619                   if debug then

   620                     quote name ^ " slice #" ^ string_of_int (slice + 1) ^

   621                     " with " ^ string_of_int num_facts ^ " fact" ^

   622                     plural_s num_facts ^ " for " ^

   623                     string_from_time slice_timeout ^ "..."

   624                     |> Output.urgent_message

   625                   else

   626                     ()

   627                 val (atp_problem, pool, conjecture_offset, facts_offset,

   628                      fact_names, typed_helpers, sym_tab) =

   629                   prepare_atp_problem ctxt format conj_sym_kind prem_kind

   630                       type_sys explicit_apply hyp_ts concl_t facts

   631                 fun weights () = atp_problem_weights atp_problem

   632                 val core =

   633                   File.shell_path command ^ " " ^

   634                   arguments ctxt slice slice_timeout weights ^ " " ^

   635                   File.shell_path prob_file

   636                 val command =

   637                   (if measure_run_time then

   638                      "TIMEFORMAT='%3R'; { time " ^ core ^ " ; }"

   639                    else

   640                      "exec " ^ core) ^ " 2>&1"

   641                 val _ =

   642                   atp_problem

   643                   |> tptp_strings_for_atp_problem format

   644                   |> cons ("% " ^ command ^ "\n")

   645                   |> File.write_list prob_file

   646                 val conjecture_shape =

   647                   conjecture_offset + 1

   648                     upto conjecture_offset + length hyp_ts + 1

   649                   |> map single

   650                 val ((output, msecs), res_code) =

   651                   bash_output command

   652                   |>> (if overlord then

   653                          prefix ("% " ^ command ^ "\n% " ^ timestamp () ^ "\n")

   654                        else

   655                          I)

   656                   |>> (if measure_run_time then split_time else rpair NONE)

   657                 val (atp_proof, outcome) =

   658                   extract_tstplike_proof_and_outcome verbose complete res_code

   659                       proof_delims known_failures output

   660                   |>> atp_proof_from_tstplike_proof atp_problem

   661                   handle UNRECOGNIZED_ATP_PROOF () => ([], SOME ProofIncomplete)

   662                 val (conjecture_shape, facts_offset, fact_names,

   663                      typed_helpers) =

   664                   if is_none outcome then

   665                     repair_conjecture_shape_and_fact_names type_sys output

   666                         conjecture_shape facts_offset fact_names typed_helpers

   667                   else

   668                     (* don't bother repairing *)

   669                     (conjecture_shape, facts_offset, fact_names, typed_helpers)

   670                 val outcome =

   671                   case outcome of

   672                     NONE =>

   673                     used_facts_in_unsound_atp_proof ctxt type_sys

   674                         conjecture_shape facts_offset fact_names atp_proof

   675                     |> Option.map (fn facts =>

   676                            UnsoundProof (is_type_sys_virtually_sound type_sys,

   677                                          facts |> sort string_ord))

   678                   | SOME Unprovable =>

   679                     if null blacklist then outcome

   680                     else SOME IncompleteUnprovable

   681                   | _ => outcome

   682               in

   683                 ((pool, conjecture_shape, facts_offset, fact_names,

   684                   typed_helpers, sym_tab),

   685                  (output, msecs, type_sys, atp_proof, outcome))

   686               end

   687             val timer = Timer.startRealTimer ()

   688             fun maybe_run_slice blacklist slice

   689                                 (result as (_, (_, msecs0, _, _, SOME _))) =

   690                 let

   691                   val time_left = Time.- (timeout, Timer.checkRealTimer timer)

   692                 in

   693                   if Time.<= (time_left, Time.zeroTime) then

   694                     result

   695                   else

   696                     (run_slice blacklist slice time_left

   697                      |> (fn (stuff, (output, msecs, type_sys, atp_proof,

   698                                      outcome)) =>

   699                             (stuff, (output, int_opt_add msecs0 msecs, type_sys,

   700                                      atp_proof, outcome))))

   701                 end

   702               | maybe_run_slice _ _ result = result

   703             fun maybe_blacklist_facts_and_retry iter blacklist

   704                     (result as ((_, _, facts_offset, fact_names, _, _),

   705                                 (_, _, type_sys, atp_proof,

   706                                  SOME (UnsoundProof (false, _))))) =

   707                 (case used_facts_in_atp_proof ctxt type_sys facts_offset

   708                                               fact_names atp_proof of

   709                    [] => result

   710                  | new_baddies =>

   711                    if slicing andalso iter < atp_blacklist_max_iters - 1 then

   712                      let val blacklist = new_baddies @ blacklist in

   713                        result

   714                        |> maybe_run_slice blacklist (List.last actual_slices)

   715                        |> maybe_blacklist_facts_and_retry (iter + 1) blacklist

   716                      end

   717                    else

   718                      result)

   719               | maybe_blacklist_facts_and_retry _ _ result = result

   720           in

   721             ((Symtab.empty, [], 0, Vector.fromList [], [], Symtab.empty),

   722              ("", SOME 0, hd fallback_best_type_systems, [],

   723               SOME InternalError))

   724             |> fold (maybe_run_slice []) actual_slices

   725                (* The ATP found an unsound proof? Automatically try again

   726                   without the offending facts! *)

   727             |> maybe_blacklist_facts_and_retry 0 []

   728           end

   729         else

   730           error ("Bad executable: " ^ Path.print command ^ ".")

   732     (* If the problem file has not been exported, remove it; otherwise, export

   733        the proof file too. *)

   734     fun cleanup prob_file =

   735       if dest_dir = "" then try File.rm prob_file else NONE

   736     fun export prob_file (_, (output, _, _, _, _)) =

   737       if dest_dir = "" then

   738         ()

   739       else

   740         File.write (Path.explode (Path.implode prob_file ^ "_proof")) output

   741     val ((pool, conjecture_shape, facts_offset, fact_names, typed_helpers,

   742           sym_tab),

   743          (output, msecs, type_sys, atp_proof, outcome)) =

   744       with_path cleanup export run_on problem_path_name

   745     val important_message =

   746       if mode = Normal andalso

   747          random_range 0 (atp_important_message_keep_quotient - 1) = 0 then

   748         extract_important_message output

   749       else

   750         ""

   751     val (message, used_facts) =

   752       case outcome of

   753         NONE =>

   754         let

   755           val used_facts =

   756             used_facts_in_atp_proof ctxt type_sys facts_offset fact_names

   757                                     atp_proof

   758           val reconstructors =

   759             if uses_typed_helpers typed_helpers atp_proof then [MetisFT, Metis]

   760             else [Metis, MetisFT]

   761           val used_ths =

   762             facts |> map untranslated_fact

   763                   |> filter_used_facts used_facts

   764                   |> map snd

   765           val preplay =

   766             preplay_one_line_proof debug preplay_timeout used_ths state subgoal

   767                                    reconstructors

   768           val full_types = uses_typed_helpers typed_helpers atp_proof

   769           val isar_params =

   770             (debug, full_types, isar_shrink_factor, type_sys, pool,

   771              conjecture_shape, facts_offset, fact_names, sym_tab, atp_proof,

   772              goal)

   773           val one_line_params =

   774             (preplay, proof_banner mode blocking name, used_facts,

   775              minimize_command, subgoal, subgoal_count)

   776         in

   777           (proof_text ctxt isar_proof isar_params one_line_params ^

   778            (if verbose then

   779               "\nATP real CPU time: " ^

   780               string_from_time (Time.fromMilliseconds (the msecs)) ^ "."

   781             else

   782               "") ^

   783            (if important_message <> "" then

   784               "\n\nImportant message from Dr. Geoff Sutcliffe:\n" ^

   785               important_message

   786             else

   787               ""),

   788            used_facts)

   789         end

   790       | SOME failure => (string_for_failure failure, [])

   791   in

   792     {outcome = outcome, message = message, used_facts = used_facts,

   793      run_time_in_msecs = msecs}

   794   end

   796 (* "SMT_Failure.Abnormal_Termination" carries the solver's return code. Until

   797    these are sorted out properly in the SMT module, we have to interpret these

   798    ourselves. *)

   799 val remote_smt_failures =

   800   [(22, CantConnect),

   801    (2, NoLibwwwPerl)]

   802 val z3_wrapper_failures =

   803   [(10, NoRealZ3),

   804    (11, InternalError),

   805    (12, InternalError),

   806    (13, InternalError)]

   807 val z3_failures =

   808   [(101, OutOfResources),

   809    (103, MalformedInput),

   810    (110, MalformedInput)]

   811 val unix_failures =

   812   [(139, Crashed)]

   813 val smt_failures =

   814   remote_smt_failures @ z3_wrapper_failures @ z3_failures @ unix_failures

   816 fun failure_from_smt_failure (SMT_Failure.Counterexample {is_real_cex, ...}) =

   817     if is_real_cex then Unprovable else IncompleteUnprovable

   818   | failure_from_smt_failure SMT_Failure.Time_Out = TimedOut

   819   | failure_from_smt_failure (SMT_Failure.Abnormal_Termination code) =

   820     (case AList.lookup (op =) smt_failures code of

   821        SOME failure => failure

   822      | NONE => UnknownError ("Abnormal termination with exit code " ^

   823                              string_of_int code ^ "."))

   824   | failure_from_smt_failure SMT_Failure.Out_Of_Memory = OutOfResources

   825   | failure_from_smt_failure (SMT_Failure.Other_Failure msg) =

   826     UnknownError msg

   828 (* FUDGE *)

   829 val smt_max_slices =

   830   Attrib.setup_config_int @{binding sledgehammer_smt_max_slices} (K 8)

   831 val smt_slice_fact_frac =

   832   Attrib.setup_config_real @{binding sledgehammer_smt_slice_fact_frac} (K 0.5)

   833 val smt_slice_time_frac =

   834   Attrib.setup_config_real @{binding sledgehammer_smt_slice_time_frac} (K 0.5)

   835 val smt_slice_min_secs =

   836   Attrib.setup_config_int @{binding sledgehammer_smt_slice_min_secs} (K 5)

   838 fun smt_filter_loop ctxt name

   839                     ({debug, verbose, overlord, max_mono_iters,

   840                       max_new_mono_instances, timeout, slicing, ...} : params)

   841                     state i smt_filter =

   842   let

   843     val max_slices = if slicing then Config.get ctxt smt_max_slices else 1

   844     val repair_context =

   845           select_smt_solver name

   846           #> (if overlord then

   847                 Config.put SMT_Config.debug_files

   848                            (overlord_file_location_for_prover name

   849                             |> (fn (path, name) => path ^ "/" ^ name))

   850               else

   851                 I)

   852           #> Config.put SMT_Config.infer_triggers (Config.get ctxt smt_triggers)

   853     val state = state |> Proof.map_context repair_context

   854     fun do_slice timeout slice outcome0 time_so_far facts =

   855       let

   856         val timer = Timer.startRealTimer ()

   857         val state =

   858           state |> Proof.map_context

   859                        (repair_smt_monomorph_context debug max_mono_iters

   860                             (max_new_mono_instances + length facts))

   861         val ms = timeout |> Time.toMilliseconds

   862         val slice_timeout =

   863           if slice < max_slices then

   864             Int.min (ms,

   865                 Int.max (1000 * Config.get ctxt smt_slice_min_secs,

   866                     Real.ceil (Config.get ctxt smt_slice_time_frac

   867                                * Real.fromInt ms)))

   868             |> Time.fromMilliseconds

   869           else

   870             timeout

   871         val num_facts = length facts

   872         val _ =

   873           if debug then

   874             quote name ^ " slice " ^ string_of_int slice ^ " with " ^

   875             string_of_int num_facts ^ " fact" ^ plural_s num_facts ^ " for " ^

   876             string_from_time slice_timeout ^ "..."

   877             |> Output.urgent_message

   878           else

   879             ()

   880         val birth = Timer.checkRealTimer timer

   881         val _ =

   882           if debug then Output.urgent_message "Invoking SMT solver..." else ()

   883         val (outcome, used_facts) =

   884           (case (slice, smt_filter) of

   885              (1, SOME head) => head |> apsnd (apsnd repair_context)

   886            | _ => SMT_Solver.smt_filter_preprocess state facts i)

   887           |> SMT_Solver.smt_filter_apply slice_timeout

   888           |> (fn {outcome, used_facts} => (outcome, used_facts))

   889           handle exn => if Exn.is_interrupt exn then

   890                           reraise exn

   891                         else

   892                           (ML_Compiler.exn_message exn

   893                            |> SMT_Failure.Other_Failure |> SOME, [])

   894         val death = Timer.checkRealTimer timer

   895         val outcome0 = if is_none outcome0 then SOME outcome else outcome0

   896         val time_so_far = Time.+ (time_so_far, Time.- (death, birth))

   897         val too_many_facts_perhaps =

   898           case outcome of

   899             NONE => false

   900           | SOME (SMT_Failure.Counterexample _) => false

   901           | SOME SMT_Failure.Time_Out => slice_timeout <> timeout

   902           | SOME (SMT_Failure.Abnormal_Termination _) => true (* kind of *)

   903           | SOME SMT_Failure.Out_Of_Memory => true

   904           | SOME (SMT_Failure.Other_Failure _) => true

   905         val timeout = Time.- (timeout, Timer.checkRealTimer timer)

   906       in

   907         if too_many_facts_perhaps andalso slice < max_slices andalso

   908            num_facts > 0 andalso Time.> (timeout, Time.zeroTime) then

   909           let

   910             val new_num_facts =

   911               Real.ceil (Config.get ctxt smt_slice_fact_frac

   912                          * Real.fromInt num_facts)

   913             val _ =

   914               if verbose andalso is_some outcome then

   915                 quote name ^ " invoked with " ^ string_of_int num_facts ^

   916                 " fact" ^ plural_s num_facts ^ ": " ^

   917                 string_for_failure (failure_from_smt_failure (the outcome)) ^

   918                 " Retrying with " ^ string_of_int new_num_facts ^ " fact" ^

   919                 plural_s new_num_facts ^ "..."

   920                 |> Output.urgent_message

   921               else

   922                 ()

   923           in

   924             facts |> take new_num_facts

   925                   |> do_slice timeout (slice + 1) outcome0 time_so_far

   926           end

   927         else

   928           {outcome = if is_none outcome then NONE else the outcome0,

   929            used_facts = used_facts,

   930            run_time_in_msecs = SOME (Time.toMilliseconds time_so_far)}

   931       end

   932   in do_slice timeout 1 NONE Time.zeroTime end

   934 fun run_smt_solver mode name

   935         (params as {debug, verbose, blocking, preplay_timeout, ...})

   936         minimize_command

   937         ({state, subgoal, subgoal_count, facts, smt_filter, ...}

   938          : prover_problem) =

   939   let

   940     val ctxt = Proof.context_of state

   941     val num_facts = length facts

   942     val facts = facts ~~ (0 upto num_facts - 1)

   943                 |> map (smt_weighted_fact ctxt num_facts)

   944     val {outcome, used_facts, run_time_in_msecs} =

   945       smt_filter_loop ctxt name params state subgoal smt_filter facts

   946     val (used_facts, used_ths) = used_facts |> ListPair.unzip

   947     val outcome = outcome |> Option.map failure_from_smt_failure

   948     val message =

   949       case outcome of

   950         NONE =>

   951         let

   952           fun smt_settings () =

   953             if name = SMT_Solver.solver_name_of ctxt then ""

   954             else "smt_solver = " ^ maybe_quote name

   955           val preplay =

   956             case preplay_one_line_proof debug preplay_timeout used_ths state

   957                                         subgoal [Metis, MetisFT] of

   958               p as Preplayed _ => p

   959             | _ => Trust_Playable (SMT (smt_settings ()), NONE)

   960           val one_line_params =

   961             (preplay, proof_banner mode blocking name, used_facts,

   962              minimize_command, subgoal, subgoal_count)

   963         in

   964           one_line_proof_text one_line_params ^

   965           (if verbose then

   966              "\nSMT solver real CPU time: " ^

   967              string_from_time (Time.fromMilliseconds (the run_time_in_msecs)) ^

   968              "."

   969            else

   970              "")

   971         end

   972       | SOME failure => string_for_failure failure

   973   in

   974     {outcome = outcome, used_facts = used_facts,

   975      run_time_in_msecs = run_time_in_msecs, message = message}

   976   end

   978 fun get_prover ctxt mode name =

   979   let val thy = Proof_Context.theory_of ctxt in

   980     if is_smt_prover ctxt name then

   981       run_smt_solver mode name

   982     else if member (op =) (supported_atps thy) name then

   983       run_atp mode name (get_atp thy name)

   984     else

   985       error ("No such prover: " ^ name ^ ".")

   986   end

   988 end;

author	blanchet
	Sun, 29 May 2011 19:40:56 +0200
changeset 43885	5945375700aa
parent 43878	ade5c84f860f
child 43891	59284a13abc4
permissions	-rw-r--r--