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 rich_type_system =

    19     Dumb_Type_Sys of type_system |

    20     Smart_Type_Sys of bool

    22   type params =

    23     {debug: bool,

    24      verbose: bool,

    25      overlord: bool,

    26      blocking: bool,

    27      provers: string list,

    28      type_sys: rich_type_system,

    29      relevance_thresholds: real * real,

    30      max_relevant: int option,

    31      monomorphize_limit: int,

    32      explicit_apply: bool,

    33      isar_proof: bool,

    34      isar_shrink_factor: int,

    35      slicing: bool,

    36      timeout: Time.time,

    37      expect: string}

    39   datatype prover_fact =

    40     Untranslated_Fact of (string * locality) * thm |

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

    43   type prover_problem =

    44     {state: Proof.state,

    45      goal: thm,

    46      subgoal: int,

    47      subgoal_count: int,

    48      facts: prover_fact list,

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

    51   type prover_result =

    52     {outcome: failure option,

    53      used_facts: (string * locality) list,

    54      run_time_in_msecs: int option,

    55      message: string}

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

    59   (* for experimentation purposes -- do not use in production code *)

    60   val smt_triggers : bool Unsynchronized.ref

    61   val smt_weights : bool Unsynchronized.ref

    62   val smt_weight_min_facts : int Unsynchronized.ref

    63   val smt_min_weight : int Unsynchronized.ref

    64   val smt_max_weight : int Unsynchronized.ref

    65   val smt_max_weight_index : int Unsynchronized.ref

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

    67   val smt_max_slices : int Unsynchronized.ref

    68   val smt_slice_fact_frac : real Unsynchronized.ref

    69   val smt_slice_time_frac : real Unsynchronized.ref

    70   val smt_slice_min_secs : int Unsynchronized.ref

    72   val das_Tool : string

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

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

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

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

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

    78   val is_built_in_const_for_prover :

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

    80   val atp_relevance_fudge : relevance_fudge

    81   val smt_relevance_fudge : relevance_fudge

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

    83   val dest_dir : string Config.T

    84   val problem_prefix : string Config.T

    85   val measure_run_time : bool Config.T

    86   val weight_smt_fact :

    87     theory -> int -> ((string * locality) * thm) * int

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

    89   val is_rich_type_sys_fairly_sound : rich_type_system -> bool

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

    91   val smt_weighted_fact :

    92     theory -> int -> prover_fact * int

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

    94   val supported_provers : Proof.context -> unit

    95   val kill_provers : unit -> unit

    96   val running_provers : unit -> unit

    97   val messages : int option -> unit

    98   val get_prover : Proof.context -> bool -> string -> prover

    99 end;

   101 structure Sledgehammer_Provers : SLEDGEHAMMER_PROVERS =

   102 struct

   104 open ATP_Problem

   105 open ATP_Proof

   106 open ATP_Systems

   107 open Metis_Translate

   108 open Sledgehammer_Util

   109 open Sledgehammer_Filter

   110 open Sledgehammer_ATP_Translate

   111 open Sledgehammer_ATP_Reconstruct

   113 (** The Sledgehammer **)

   115 (* Identifier to distinguish Sledgehammer from other tools using

   116    "Async_Manager". *)

   117 val das_Tool = "Sledgehammer"

   119 val select_smt_solver =

   120   Context.proof_map o SMT_Config.select_solver

   122 fun is_smt_prover ctxt name =

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

   125 fun is_prover_supported ctxt name =

   126   let val thy = Proof_Context.theory_of ctxt in

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

   128   end

   130 fun is_prover_installed ctxt =

   131   is_smt_prover ctxt orf is_atp_installed (Proof_Context.theory_of ctxt)

   133 fun get_slices slicing slices =

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

   136 fun default_max_relevant_for_prover ctxt slicing name =

   137   let val thy = Proof_Context.theory_of ctxt in

   138     if is_smt_prover ctxt name then

   139       SMT_Solver.default_max_relevant ctxt name

   140     else

   141       fold (Integer.max o snd o snd o snd)

   142            (get_slices slicing (#best_slices (get_atp thy name) ())) 0

   143   end

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

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

   147 val atp_irrelevant_consts =

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

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

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

   152 fun is_built_in_const_for_prover ctxt name =

   153   if is_smt_prover ctxt name then

   154     let val ctxt = ctxt |> select_smt_solver name in

   155       fn x => fn ts =>

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

   157            (true, [])

   158          else if SMT_Builtin.is_builtin_fun_ext ctxt x ts then

   159            (true, ts)

   160          else

   161            (false, ts)

   162     end

   163   else

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

   166 (* FUDGE *)

   167 val atp_relevance_fudge =

   168   {allow_ext = true,

   169    local_const_multiplier = 1.5,

   170    worse_irrel_freq = 100.0,

   171    higher_order_irrel_weight = 1.05,

   172    abs_rel_weight = 0.5,

   173    abs_irrel_weight = 2.0,

   174    skolem_irrel_weight = 0.75,

   175    theory_const_rel_weight = 0.5,

   176    theory_const_irrel_weight = 0.25,

   177    intro_bonus = 0.15,

   178    elim_bonus = 0.15,

   179    simp_bonus = 0.15,

   180    local_bonus = 0.55,

   181    assum_bonus = 1.05,

   182    chained_bonus = 1.5,

   183    max_imperfect = 11.5,

   184    max_imperfect_exp = 1.0,

   185    threshold_divisor = 2.0,

   186    ridiculous_threshold = 0.01}

   188 (* FUDGE (FIXME) *)

   189 val smt_relevance_fudge =

   190   {allow_ext = false,

   191    local_const_multiplier = #local_const_multiplier atp_relevance_fudge,

   192    worse_irrel_freq = #worse_irrel_freq atp_relevance_fudge,

   193    higher_order_irrel_weight = #higher_order_irrel_weight atp_relevance_fudge,

   194    abs_rel_weight = #abs_rel_weight atp_relevance_fudge,

   195    abs_irrel_weight = #abs_irrel_weight atp_relevance_fudge,

   196    skolem_irrel_weight = #skolem_irrel_weight atp_relevance_fudge,

   197    theory_const_rel_weight = #theory_const_rel_weight atp_relevance_fudge,

   198    theory_const_irrel_weight = #theory_const_irrel_weight atp_relevance_fudge,

   199    intro_bonus = #intro_bonus atp_relevance_fudge,

   200    elim_bonus = #elim_bonus atp_relevance_fudge,

   201    simp_bonus = #simp_bonus atp_relevance_fudge,

   202    local_bonus = #local_bonus atp_relevance_fudge,

   203    assum_bonus = #assum_bonus atp_relevance_fudge,

   204    chained_bonus = #chained_bonus atp_relevance_fudge,

   205    max_imperfect = #max_imperfect atp_relevance_fudge,

   206    max_imperfect_exp = #max_imperfect_exp atp_relevance_fudge,

   207    threshold_divisor = #threshold_divisor atp_relevance_fudge,

   208    ridiculous_threshold = #ridiculous_threshold atp_relevance_fudge}

   210 fun relevance_fudge_for_prover ctxt name =

   211   if is_smt_prover ctxt name then smt_relevance_fudge else atp_relevance_fudge

   213 fun supported_provers ctxt =

   214   let

   215     val thy = Proof_Context.theory_of ctxt

   216     val (remote_provers, local_provers) =

   217       sort_strings (supported_atps thy) @

   218       sort_strings (SMT_Solver.available_solvers_of ctxt)

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

   220   in

   221     Output.urgent_message ("Supported provers: " ^

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

   223   end

   225 fun kill_provers () = Async_Manager.kill_threads das_Tool "provers"

   226 fun running_provers () = Async_Manager.running_threads das_Tool "provers"

   227 val messages = Async_Manager.thread_messages das_Tool "prover"

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

   231 datatype rich_type_system =

   232   Dumb_Type_Sys of type_system |

   233   Smart_Type_Sys of bool

   235 type params =

   236   {debug: bool,

   237    verbose: bool,

   238    overlord: bool,

   239    blocking: bool,

   240    provers: string list,

   241    type_sys: rich_type_system,

   242    relevance_thresholds: real * real,

   243    max_relevant: int option,

   244    monomorphize_limit: int,

   245    explicit_apply: bool,

   246    isar_proof: bool,

   247    isar_shrink_factor: int,

   248    slicing: bool,

   249    timeout: Time.time,

   250    expect: string}

   252 datatype prover_fact =

   253   Untranslated_Fact of (string * locality) * thm |

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

   256 type prover_problem =

   257   {state: Proof.state,

   258    goal: thm,

   259    subgoal: int,

   260    subgoal_count: int,

   261    facts: prover_fact list,

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

   264 type prover_result =

   265   {outcome: failure option,

   266    message: string,

   267    used_facts: (string * locality) list,

   268    run_time_in_msecs: int option}

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

   272 (* configuration attributes *)

   274 val dest_dir =

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

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

   278 val problem_prefix =

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

   281 val measure_run_time =

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

   284 fun with_path cleanup after f path =

   285   Exn.capture f path

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

   287   |> Exn.release

   288   |> tap (after path)

   290 fun proof_banner auto =

   291   if auto then "Auto Sledgehammer found a proof" else "Try this command"

   293 val smt_triggers = Unsynchronized.ref true

   294 val smt_weights = Unsynchronized.ref true

   295 val smt_weight_min_facts = Unsynchronized.ref 20

   297 (* FUDGE *)

   298 val smt_min_weight = Unsynchronized.ref 0

   299 val smt_max_weight = Unsynchronized.ref 10

   300 val smt_max_weight_index = Unsynchronized.ref 200

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

   303 fun smt_fact_weight j num_facts =

   304   if !smt_weights andalso num_facts >= !smt_weight_min_facts then

   305     SOME (!smt_max_weight

   306           - (!smt_max_weight - !smt_min_weight + 1)

   307             * !smt_weight_curve (Int.max (0, !smt_max_weight_index - j - 1))

   308             div !smt_weight_curve (!smt_max_weight_index))

   309   else

   310     NONE

   312 fun weight_smt_fact thy num_facts ((info, th), j) =

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

   315 fun is_rich_type_sys_fairly_sound (Dumb_Type_Sys type_sys) =

   316     is_type_sys_fairly_sound type_sys

   317   | is_rich_type_sys_fairly_sound (Smart_Type_Sys full_types) = full_types

   319 fun untranslated_fact (Untranslated_Fact p) = p

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

   321 fun atp_translated_fact ctxt fact =

   322     translate_atp_fact ctxt false (untranslated_fact fact)

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

   324   | smt_weighted_fact thy num_facts (fact, j) =

   325     (untranslated_fact fact, j) |> weight_smt_fact thy num_facts

   327 fun overlord_file_location_for_prover prover =

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

   331 (* generic TPTP-based ATPs *)

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

   334   | int_opt_add _ _ = NONE

   336 val atp_blacklist_max_iters = 10

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

   338    them each time. *)

   339 val atp_important_message_keep_factor = 0.1

   341 val fallback_best_type_systems =

   342   [Preds (Polymorphic, Const_Arg_Types), Many_Typed]

   344 fun adjust_dumb_type_sys formats Many_Typed =

   345     if member (op =) formats Tff then (Tff, Many_Typed)

   346     else (Fof, Preds (Mangled_Monomorphic, All_Types))

   347   | adjust_dumb_type_sys formats type_sys =

   348     if member (op =) formats Fof then (Fof, type_sys)

   349     else (Tff, Many_Typed)

   350 fun determine_format_and_type_sys _ formats (Dumb_Type_Sys type_sys) =

   351     adjust_dumb_type_sys formats type_sys

   352   | determine_format_and_type_sys best_type_systems formats

   353                                   (Smart_Type_Sys full_types) =

   354     best_type_systems @ fallback_best_type_systems

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

   356     |> the |> adjust_dumb_type_sys formats

   358 fun run_atp auto name

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

   360           hypothesis_kind, formats, best_slices, best_type_systems, ...}

   361          : atp_config)

   362         ({debug, verbose, overlord, type_sys, max_relevant, monomorphize_limit,

   363           explicit_apply, isar_proof, isar_shrink_factor, slicing, timeout, ...}

   364          : params)

   365         minimize_command ({state, goal, subgoal, facts, ...} : prover_problem) =

   366   let

   367     val thy = Proof.theory_of state

   368     val ctxt = Proof.context_of state

   369     val (format, type_sys) =

   370       determine_format_and_type_sys best_type_systems formats type_sys

   371     val (_, hyp_ts, concl_t) = strip_subgoal goal subgoal

   372     val (dest_dir, problem_prefix) =

   373       if overlord then overlord_file_location_for_prover name

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

   375     val problem_file_name =

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

   377                   "_" ^ string_of_int subgoal)

   378     val problem_path_name =

   379       if dest_dir = "" then

   380         File.tmp_path problem_file_name

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

   382         Path.append (Path.explode dest_dir) problem_file_name

   383       else

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

   385     val measure_run_time = verbose orelse Config.get ctxt measure_run_time

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

   387     fun split_time s =

   388       let

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

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

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

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

   393         val digit = Scan.one Symbol.is_ascii_digit

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

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

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

   397       in (output, as_time t) end

   398     fun run_on prob_file =

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

   400         (home_var, _) :: _ =>

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

   402       | [] =>

   403         if File.exists command then

   404           let

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

   406                entire time available. *)

   407             val actual_slices = get_slices slicing (best_slices ())

   408             val num_actual_slices = length actual_slices

   409             fun monomorphize_facts facts =

   410               let

   411                 val repair_context =

   412                   Config.put SMT_Config.verbose debug

   413                   #> Config.put SMT_Config.monomorph_full false

   414                   #> Config.put SMT_Config.monomorph_limit monomorphize_limit

   415                 val facts = facts |> map untranslated_fact

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

   417                 val subgoal_th =

   418                   Logic.list_implies (hyp_ts, concl_t)

   419                   |> Skip_Proof.make_thm thy

   420                 val indexed_facts =

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

   422               in

   423                 SMT_Monomorph.monomorph indexed_facts (repair_context ctxt)

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

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

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

   427               end

   428             fun run_slice blacklist

   429                           (slice, (time_frac, (complete, default_max_relevant)))

   430                           time_left =

   431               let

   432                 val num_facts =

   433                   length facts |> is_none max_relevant

   434                                   ? Integer.min default_max_relevant

   435                 val facts =

   436                   facts |> take num_facts

   437                         |> not (null blacklist)

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

   439                                          o untranslated_fact)

   440                         |> polymorphism_of_type_sys type_sys <> Polymorphic

   441                            ? monomorphize_facts

   442                         |> map (atp_translated_fact ctxt)

   443                 val real_ms = Real.fromInt o Time.toMilliseconds

   444                 val slice_timeout =

   445                   ((real_ms time_left

   446                     |> (if slice < num_actual_slices - 1 then

   447                           curry Real.min (time_frac * real_ms timeout)

   448                         else

   449                           I))

   450                    * 0.001) |> seconds

   451                 val _ =

   452                   if verbose then

   453                     "ATP slice " ^ string_of_int (slice + 1) ^ " with " ^

   454                     string_of_int num_facts ^ " fact" ^ plural_s num_facts ^

   455                     " for " ^ string_from_time slice_timeout ^ "..."

   456                     |> Output.urgent_message

   457                   else

   458                     ()

   459                 val (atp_problem, pool, conjecture_offset, facts_offset,

   460                      fact_names) =

   461                   prepare_atp_problem ctxt type_sys explicit_apply hyp_ts

   462                                       concl_t facts

   463                 fun weights () = atp_problem_weights atp_problem

   464                 val core =

   465                   File.shell_path command ^ " " ^

   466                   arguments slice slice_timeout weights ^ " " ^

   467                   File.shell_path prob_file

   468                 val command =

   469                   (if measure_run_time then

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

   471                    else

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

   473                 val _ =

   474                   atp_problem

   475                   |> tptp_strings_for_atp_problem hypothesis_kind format

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

   477                   |> File.write_list prob_file

   478                 val conjecture_shape =

   479                   conjecture_offset + 1

   480                     upto conjecture_offset + length hyp_ts + 1

   481                   |> map single

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

   483                   bash_output command

   484                   |>> (if overlord then

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

   486                        else

   487                          I)

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

   489                 val (atp_proof, outcome) =

   490                   extract_tstplike_proof_and_outcome debug verbose complete

   491                       res_code proof_delims known_failures output

   492                   |>> atp_proof_from_tstplike_proof

   493                 val (conjecture_shape, facts_offset, fact_names) =

   494                   if is_none outcome then

   495                     repair_conjecture_shape_and_fact_names output

   496                         conjecture_shape facts_offset fact_names

   497                   else

   498                     (* don't bother repairing *)

   499                     (conjecture_shape, facts_offset, fact_names)

   500                 val outcome =

   501                   case outcome of

   502                     NONE =>

   503                     if is_unsound_proof conjecture_shape facts_offset fact_names

   504                                         atp_proof then

   505                       SOME (UnsoundProof (is_type_sys_virtually_sound type_sys))

   506                     else

   507                       NONE

   508                   | SOME Unprovable =>

   509                     if null blacklist then outcome

   510                     else SOME IncompleteUnprovable

   511                   | _ => outcome

   512               in

   513                 ((pool, conjecture_shape, facts_offset, fact_names),

   514                  (output, msecs, atp_proof, outcome))

   515               end

   516             val timer = Timer.startRealTimer ()

   517             fun maybe_run_slice blacklist slice

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

   519                 let

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

   521                 in

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

   523                     result

   524                   else

   525                     (run_slice blacklist slice time_left

   526                      |> (fn (stuff, (output, msecs, atp_proof, outcome)) =>

   527                             (stuff, (output, int_opt_add msecs0 msecs, atp_proof,

   528                                      outcome))))

   529                 end

   530               | maybe_run_slice _ _ result = result

   531             fun maybe_blacklist_facts_and_retry iter blacklist

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

   533                                 (_, _, atp_proof, SOME (UnsoundProof false)))) =

   534                 (case used_facts_in_atp_proof facts_offset fact_names

   535                                               atp_proof of

   536                    [] => result

   537                  | new_baddies =>

   538                    let val blacklist = new_baddies @ blacklist in

   539                      result

   540                      |> maybe_run_slice blacklist (List.last actual_slices)

   541                      |> iter < atp_blacklist_max_iters

   542                         ? maybe_blacklist_facts_and_retry (iter + 1) blacklist

   543                    end)

   544               | maybe_blacklist_facts_and_retry _ _ result = result

   545           in

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

   547              ("", SOME 0, [], SOME InternalError))

   548             |> fold (maybe_run_slice []) actual_slices

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

   550                   without the offending facts! *)

   551             |> maybe_blacklist_facts_and_retry 0 []

   552           end

   553         else

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

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

   557        the proof file too. *)

   558     fun cleanup prob_file =

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

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

   561       if dest_dir = "" then

   562         ()

   563       else

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

   565     val ((pool, conjecture_shape, facts_offset, fact_names),

   566          (output, msecs, atp_proof, outcome)) =

   567       with_path cleanup export run_on problem_path_name

   568     val important_message =

   569       if not auto andalso random () <= atp_important_message_keep_factor then

   570         extract_important_message output

   571       else

   572         ""

   573     fun append_to_message message =

   574       message ^

   575       (if verbose then

   576          "\nATP real CPU time: " ^

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

   578        else

   579          "") ^

   580       (if important_message <> "" then

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

   582        else

   583          "")

   584     val isar_params =

   585       (ctxt, debug, type_sys, isar_shrink_factor, pool, conjecture_shape)

   586     val metis_params =

   587       (proof_banner auto, minimize_command, atp_proof, facts_offset, fact_names,

   588        goal, subgoal)

   589     val (outcome, (message, used_facts)) =

   590       case outcome of

   591         NONE =>

   592         (NONE, proof_text isar_proof isar_params metis_params

   593                |>> append_to_message)

   594       | SOME ProofMissing =>

   595         (NONE, metis_proof_text metis_params |>> append_to_message)

   596       | SOME failure => (outcome, (string_for_failure failure, []))

   597   in

   598     {outcome = outcome, message = message, used_facts = used_facts,

   599      run_time_in_msecs = msecs}

   600   end

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

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

   604    ourselves. *)

   605 val remote_smt_failures =

   606   [(22, CantConnect),

   607    (2, NoLibwwwPerl)]

   608 val z3_wrapper_failures =

   609   [(10, NoRealZ3),

   610    (11, InternalError),

   611    (12, InternalError),

   612    (13, InternalError)]

   613 val z3_failures =

   614   [(101, OutOfResources),

   615    (103, MalformedInput),

   616    (110, MalformedInput)]

   617 val unix_failures =

   618   [(139, Crashed)]

   619 val smt_failures =

   620   remote_smt_failures @ z3_wrapper_failures @ z3_failures @ unix_failures

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

   623     if is_real_cex then Unprovable else IncompleteUnprovable

   624   | failure_from_smt_failure SMT_Failure.Time_Out = TimedOut

   625   | failure_from_smt_failure (SMT_Failure.Abnormal_Termination code) =

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

   627        SOME failure => failure

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

   629                              string_of_int code ^ "."))

   630   | failure_from_smt_failure SMT_Failure.Out_Of_Memory = OutOfResources

   631   | failure_from_smt_failure (SMT_Failure.Other_Failure msg) =

   632     UnknownError msg

   634 (* FUDGE *)

   635 val smt_max_slices = Unsynchronized.ref 8

   636 val smt_slice_fact_frac = Unsynchronized.ref 0.5

   637 val smt_slice_time_frac = Unsynchronized.ref 0.5

   638 val smt_slice_min_secs = Unsynchronized.ref 5

   640 fun smt_filter_loop name ({debug, verbose, overlord, monomorphize_limit,

   641                            timeout, slicing, ...} : params)

   642                     state i smt_filter =

   643   let

   644     val ctxt = Proof.context_of state

   645     val max_slices = if slicing then !smt_max_slices else 1

   646     val repair_context =

   647       select_smt_solver name

   648       #> Config.put SMT_Config.verbose debug

   649       #> (if overlord then

   650             Config.put SMT_Config.debug_files

   651                        (overlord_file_location_for_prover name

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

   653           else

   654             I)

   655       #> Config.put SMT_Config.infer_triggers (!smt_triggers)

   656       #> Config.put SMT_Config.monomorph_full false

   657       #> Config.put SMT_Config.monomorph_limit monomorphize_limit

   658     val state = state |> Proof.map_context repair_context

   660     fun do_slice timeout slice outcome0 time_so_far facts =

   661       let

   662         val timer = Timer.startRealTimer ()

   663         val ms = timeout |> Time.toMilliseconds

   664         val slice_timeout =

   665           if slice < max_slices then

   666             Int.min (ms,

   667                 Int.max (1000 * !smt_slice_min_secs,

   668                     Real.ceil (!smt_slice_time_frac * Real.fromInt ms)))

   669             |> Time.fromMilliseconds

   670           else

   671             timeout

   672         val num_facts = length facts

   673         val _ =

   674           if verbose then

   675             "SMT slice with " ^ string_of_int num_facts ^ " fact" ^

   676             plural_s num_facts ^ " for " ^ string_from_time slice_timeout ^

   677             "..."

   678             |> Output.urgent_message

   679           else

   680             ()

   681         val birth = Timer.checkRealTimer timer

   682         val _ =

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

   684         val (outcome, used_facts) =

   685           (case (slice, smt_filter) of

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

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

   688           |> SMT_Solver.smt_filter_apply slice_timeout

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

   690           handle exn => if Exn.is_interrupt exn then

   691                           reraise exn

   692                         else

   693                           (ML_Compiler.exn_message exn

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

   695         val death = Timer.checkRealTimer timer

   696         val _ =

   697           if verbose andalso is_some outcome then

   698             "SMT outcome: " ^ SMT_Failure.string_of_failure ctxt (the outcome)

   699             |> Output.urgent_message

   700           else if debug then

   701             Output.urgent_message "SMT solver returned."

   702           else

   703             ()

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

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

   706         val too_many_facts_perhaps =

   707           case outcome of

   708             NONE => false

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

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

   711           | SOME (SMT_Failure.Abnormal_Termination code) =>

   712             (if verbose then

   713                "The SMT solver invoked with " ^ string_of_int num_facts ^

   714                " fact" ^ plural_s num_facts ^ " terminated abnormally with \

   715                \exit code " ^ string_of_int code ^ "."

   716                |> warning

   717              else

   718                ();

   719              true (* kind of *))

   720           | SOME SMT_Failure.Out_Of_Memory => true

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

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

   723       in

   724         if too_many_facts_perhaps andalso slice < max_slices andalso

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

   726           let

   727             val n = Real.ceil (!smt_slice_fact_frac * Real.fromInt num_facts)

   728           in

   729             do_slice timeout (slice + 1) outcome0 time_so_far (take n facts)

   730           end

   731         else

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

   733            used_facts = used_facts,

   734            run_time_in_msecs = SOME (Time.toMilliseconds time_so_far)}

   735       end

   736   in do_slice timeout 1 NONE Time.zeroTime end

   738 (* taken from "Mirabelle" and generalized *)

   739 fun can_apply timeout tac state i =

   740   let

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

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

   743   in

   744     case try (TimeLimit.timeLimit timeout (Seq.pull o full_tac)) goal of

   745       SOME (SOME _) => true

   746     | _ => false

   747   end

   749 val smt_metis_timeout = seconds 1.0

   751 fun can_apply_metis debug state i ths =

   752   can_apply smt_metis_timeout

   753             (Config.put Metis_Tactics.verbose debug

   754              #> (fn ctxt => Metis_Tactics.metis_tac ctxt ths)) state i

   756 fun run_smt_solver auto name (params as {debug, verbose, ...}) minimize_command

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

   758                     : prover_problem) =

   759   let

   760     val ctxt = Proof.context_of state

   761     val thy = Proof.theory_of state

   762     val num_facts = length facts

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

   764                 |> map (smt_weighted_fact thy num_facts)

   765     val {outcome, used_facts, run_time_in_msecs} =

   766       smt_filter_loop name params state subgoal smt_filter facts

   767     val (chained_lemmas, other_lemmas) = split_used_facts (map fst used_facts)

   768     val outcome = outcome |> Option.map failure_from_smt_failure

   769     val message =

   770       case outcome of

   771         NONE =>

   772         let

   773           val (method, settings) =

   774             if can_apply_metis debug state subgoal (map snd used_facts) then

   775               ("metis", "")

   776             else

   777               ("smt", if name = SMT_Solver.solver_name_of ctxt then ""

   778                       else "smt_solver = " ^ maybe_quote name)

   779         in

   780           try_command_line (proof_banner auto)

   781               (apply_on_subgoal settings subgoal subgoal_count ^

   782                command_call method (map fst other_lemmas)) ^

   783           minimize_line minimize_command

   784                         (map fst (other_lemmas @ chained_lemmas)) ^

   785           (if verbose then

   786              "\nSMT solver real CPU time: " ^

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

   788              "."

   789            else

   790              "")

   791         end

   792       | SOME failure => string_for_failure failure

   793   in

   794     {outcome = outcome, used_facts = map fst used_facts,

   795      run_time_in_msecs = run_time_in_msecs, message = message}

   796   end

   798 fun get_prover ctxt auto name =

   799   let val thy = Proof_Context.theory_of ctxt in

   800     if is_smt_prover ctxt name then

   801       run_smt_solver auto name

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

   803       run_atp auto name (get_atp thy name)

   804     else

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

   806   end

   808 end;

author	wenzelm
	Mon, 02 May 2011 16:33:21 +0200
changeset 43487	92715b528e78
parent 43464	f9d7f1331a00
child 43494	613b9b589ca0
permissions	-rw-r--r--