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

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

     2     Author:     Jasmin Blanchette, TU Muenchen

     4 Adds "sledgehammer" and related commands to Isabelle/Isar's outer syntax.

     5 *)

     7 signature SLEDGEHAMMER_COMMANDS =

     8 sig

     9   type params = Sledgehammer_Prover.params

    11   val provers : string Unsynchronized.ref

    12   val default_params : theory -> (string * string) list -> params

    13 end;

    15 structure Sledgehammer_Commands : SLEDGEHAMMER_COMMANDS =

    16 struct

    18 open ATP_Util

    19 open ATP_Systems

    20 open ATP_Problem_Generate

    21 open ATP_Proof

    22 open ATP_Proof_Reconstruct

    23 open Sledgehammer_Util

    24 open Sledgehammer_Fact

    25 open Sledgehammer_Prover

    26 open Sledgehammer_Prover_Minimize

    27 open Sledgehammer_MaSh

    28 open Sledgehammer

    30 (* val cvc3N = "cvc3" *)

    31 val z3N = "z3"

    33 val runN = "run"

    34 val minN = "min"

    35 val messagesN = "messages"

    36 val supported_proversN = "supported_provers"

    37 val kill_allN = "kill_all"

    38 val running_proversN = "running_provers"

    39 val running_learnersN = "running_learners"

    40 val refresh_tptpN = "refresh_tptp"

    42 val _ =

    43   ProofGeneral.preference_option ProofGeneral.category_tracing

    44     NONE

    45     @{system_option auto_sledgehammer}

    46     "auto-sledgehammer"

    47     "Run Sledgehammer automatically"

    49 (** Sledgehammer commands **)

    51 fun add_fact_override ns : fact_override = {add = ns, del = [], only = false}

    52 fun del_fact_override ns : fact_override = {add = [], del = ns, only = false}

    53 fun only_fact_override ns : fact_override = {add = ns, del = [], only = true}

    54 fun merge_fact_override_pairwise (r1 : fact_override) (r2 : fact_override) =

    55   {add = #add r1 @ #add r2, del = #del r1 @ #del r2, only = #only r1 andalso #only r2}

    56 fun merge_fact_overrides rs = fold merge_fact_override_pairwise rs (only_fact_override [])

    58 (*** parameters ***)

    60 val provers = Unsynchronized.ref ""

    62 val _ =

    63   ProofGeneral.preference_string ProofGeneral.category_proof

    64     NONE

    65     provers

    66     "Sledgehammer: Provers"

    67     "Default automatic provers (separated by whitespace)"

    69 val _ =

    70   ProofGeneral.preference_option ProofGeneral.category_proof

    71     NONE

    72     @{system_option sledgehammer_timeout}

    73     "Sledgehammer: Time Limit"

    74     "ATPs will be interrupted after this time (in seconds)"

    76 type raw_param = string * string list

    78 val default_default_params =

    79   [("debug", "false"),

    80    ("verbose", "false"),

    81    ("overlord", "false"),

    82    ("spy", "false"),

    83    ("blocking", "false"),

    84    ("type_enc", "smart"),

    85    ("strict", "false"),

    86    ("lam_trans", "smart"),

    87    ("uncurried_aliases", "smart"),

    88    ("learn", "true"),

    89    ("fact_filter", "smart"),

    90    ("max_facts", "smart"),

    91    ("fact_thresholds", "0.45 0.85"),

    92    ("max_mono_iters", "smart"),

    93    ("max_new_mono_instances", "smart"),

    94    ("isar_proofs", "smart"),

    95    ("compress", "10"),

    96    ("try0", "true"),

    97    ("smt_proofs", "smart"),

    98    ("slice", "true"),

    99    ("minimize", "smart"),

   100    ("preplay_timeout", "2")]

   102 val alias_params =

   103   [("prover", ("provers", [])), (* undocumented *)

   104    ("dont_preplay", ("preplay_timeout", ["0"])),

   105    ("dont_compress", ("compress", ["0"])),

   106    ("isar_proof", ("isar_proofs", [])) (* legacy *)]

   107 val negated_alias_params =

   108   [("no_debug", "debug"),

   109    ("quiet", "verbose"),

   110    ("no_overlord", "overlord"),

   111    ("dont_spy", "spy"),

   112    ("non_blocking", "blocking"),

   113    ("non_strict", "strict"),

   114    ("no_uncurried_aliases", "uncurried_aliases"),

   115    ("dont_learn", "learn"),

   116    ("no_isar_proofs", "isar_proofs"),

   117    ("dont_slice", "slice"),

   118    ("dont_minimize", "minimize"),

   119    ("dont_try0", "try0"),

   120    ("no_smt_proofs", "smt_proofs")]

   122 val params_not_for_minimize =

   123   ["provers", "blocking", "fact_filter", "max_facts", "fact_thresholds", "slice", "minimize"];

   125 val property_dependent_params = ["provers", "timeout"]

   127 fun is_known_raw_param s =

   128   AList.defined (op =) default_default_params s orelse

   129   AList.defined (op =) alias_params s orelse

   130   AList.defined (op =) negated_alias_params s orelse

   131   member (op =) property_dependent_params s orelse s = "expect"

   133 fun is_prover_list ctxt s =

   134   (case space_explode " " s of

   135     ss as _ :: _ => forall (is_prover_supported ctxt) ss

   136   | _ => false)

   138 fun unalias_raw_param (name, value) =

   139   (case AList.lookup (op =) alias_params name of

   140     SOME (name', []) => (name', value)

   141   | SOME (param' as (name', _)) =>

   142     if value <> ["false"] then

   143       param'

   144     else

   145       error ("Parameter " ^ quote name ^ " cannot be set to \"false\" \

   146              \(cf. " ^ quote name' ^ ").")

   147   | NONE =>

   148     (case AList.lookup (op =) negated_alias_params name of

   149       SOME name' => (name',

   150         (case value of

   151           ["false"] => ["true"]

   152         | ["true"] => ["false"]

   153         | [] => ["false"]

   154         | _ => value))

   155     | NONE => (name, value)))

   157 val any_type_enc = type_enc_of_string Strict "erased"

   159 (* "provers =", "type_enc =", "lam_trans =", "fact_filter =", and "max_facts ="

   160    can be omitted. For the last four, this is a secret feature. *)

   161 fun normalize_raw_param ctxt =

   162   unalias_raw_param

   163   #> (fn (name, value) =>

   164          if is_known_raw_param name then

   165            (name, value)

   166          else if null value then

   167            if is_prover_list ctxt name then

   168              ("provers", [name])

   169            else if can (type_enc_of_string Strict) name then

   170              ("type_enc", [name])

   171            else if can (trans_lams_of_string ctxt any_type_enc) name then

   172              ("lam_trans", [name])

   173            else if member (op =) fact_filters name then

   174              ("fact_filter", [name])

   175            else if is_some (Int.fromString name) then

   176              ("max_facts", [name])

   177            else

   178              error ("Unknown parameter: " ^ quote name ^ ".")

   179          else

   180            error ("Unknown parameter: " ^ quote name ^ "."))

   182 (* Ensures that type encodings such as "mono_native?" and "poly_guards!!" are

   183    read correctly. *)

   184 val implode_param = strip_spaces_except_between_idents o space_implode " "

   186 (* FIXME: use "Generic_Data" *)

   187 structure Data = Theory_Data

   188 (

   189   type T = raw_param list

   190   val empty = default_default_params |> map (apsnd single)

   191   val extend = I

   192   fun merge data : T = AList.merge (op =) (K true) data

   193 )

   195 fun remotify_prover_if_supported_and_not_already_remote ctxt name =

   196   if String.isPrefix remote_prefix name then

   197     SOME name

   198   else

   199     let val remote_name = remote_prefix ^ name in

   200       if is_prover_supported ctxt remote_name then SOME remote_name else NONE

   201     end

   203 fun remotify_prover_if_not_installed ctxt name =

   204   if is_prover_supported ctxt name andalso is_prover_installed ctxt name then SOME name

   205   else remotify_prover_if_supported_and_not_already_remote ctxt name

   207 (* The first ATP of the list is used by Auto Sledgehammer. Because of the low

   208    timeout, it makes sense to put E first. *)

   209 fun default_provers_param_value mode ctxt =

   210   [eN, spassN, z3N, e_sineN, vampireN]

   211   |> map_filter (remotify_prover_if_not_installed ctxt)

   212   (* In "try" mode, leave at least one thread to another slow tool (e.g. Nitpick) *)

   213   |> take (Multithreading.max_threads_value () - (if mode = Try then 1 else 0))

   214   |> implode_param

   216 fun set_default_raw_param param thy =

   217   let val ctxt = Proof_Context.init_global thy in

   218     thy |> Data.map (AList.update (op =) (normalize_raw_param ctxt param))

   219   end

   221 fun default_raw_params mode thy =

   222   let val ctxt = Proof_Context.init_global thy in

   223     Data.get thy

   224     |> fold (AList.default (op =))

   225          [("provers", [(case !provers of "" => default_provers_param_value mode ctxt | s => s)]),

   226           ("timeout",

   227            let val timeout = Options.default_int @{system_option sledgehammer_timeout} in

   228              [if timeout <= 0 then "none" else string_of_int timeout]

   229            end)]

   230   end

   232 fun extract_params mode default_params override_params =

   233   let

   234     val raw_params = rev override_params @ rev default_params

   235     val lookup = Option.map implode_param o AList.lookup (op =) raw_params

   236     val lookup_string = the_default "" o lookup

   237     fun general_lookup_bool option default_value name =

   238       (case lookup name of

   239         SOME s => parse_bool_option option name s

   240       | NONE => default_value)

   241     val lookup_bool = the o general_lookup_bool false (SOME false)

   242     fun lookup_time name =

   243       (case lookup name of

   244         SOME s => parse_time name s

   245       | NONE => Time.zeroTime)

   246     fun lookup_int name =

   247       (case lookup name of

   248         NONE => 0

   249       | SOME s =>

   250         (case Int.fromString s of

   251           SOME n => n

   252         | NONE => error ("Parameter " ^ quote name ^ " must be assigned an integer value.")))

   253     fun lookup_real name =

   254       (case lookup name of

   255         NONE => 0.0

   256       | SOME s =>

   257         (case Real.fromString s of

   258           SOME n => n

   259         | NONE => error ("Parameter " ^ quote name ^ " must be assigned a real value.")))

   260     fun lookup_real_pair name =

   261       (case lookup name of

   262         NONE => (0.0, 0.0)

   263       | SOME s =>

   264         (case s |> space_explode " " |> map Real.fromString of

   265           [SOME r1, SOME r2] => (r1, r2)

   266         | _ => error ("Parameter " ^ quote name ^ " must be assigned a pair of floating-point \

   267                  \values (e.g., \"0.6 0.95\")")))

   268     fun lookup_option lookup' name =

   269       (case lookup name of

   270         SOME "smart" => NONE

   271       | _ => SOME (lookup' name))

   272     val debug = mode <> Auto_Try andalso lookup_bool "debug"

   273     val verbose = debug orelse (mode <> Auto_Try andalso lookup_bool "verbose")

   274     val overlord = lookup_bool "overlord"

   275     val spy = getenv "SLEDGEHAMMER_SPY" = "yes" orelse lookup_bool "spy"

   276     val blocking =

   277       Isabelle_Process.is_active () orelse mode <> Normal orelse debug orelse lookup_bool "blocking"

   278     val provers = lookup_string "provers" |> space_explode " "

   279                   |> mode = Auto_Try ? single o hd

   280     val type_enc =

   281       if mode = Auto_Try then

   282         NONE

   283       else

   284         (case lookup_string "type_enc" of

   285           "smart" => NONE

   286         | s => (type_enc_of_string Strict s; SOME s))

   287     val strict = mode = Auto_Try orelse lookup_bool "strict"

   288     val lam_trans = lookup_option lookup_string "lam_trans"

   289     val uncurried_aliases = lookup_option lookup_bool "uncurried_aliases"

   290     val learn = lookup_bool "learn"

   291     val fact_filter =

   292       lookup_option lookup_string "fact_filter"

   293       |> mode = Auto_Try ? (fn NONE => SOME mepoN | sf => sf)

   294     val max_facts = lookup_option lookup_int "max_facts"

   295     val fact_thresholds = lookup_real_pair "fact_thresholds"

   296     val max_mono_iters = lookup_option lookup_int "max_mono_iters"

   297     val max_new_mono_instances =

   298       lookup_option lookup_int "max_new_mono_instances"

   299     val isar_proofs = lookup_option lookup_bool "isar_proofs"

   300     val compress = Real.max (1.0, lookup_real "compress")

   301     val try0 = lookup_bool "try0"

   302     val smt_proofs = lookup_option lookup_bool "smt_proofs"

   303     val slice = mode <> Auto_Try andalso lookup_bool "slice"

   304     val minimize = if mode = Auto_Try then NONE else lookup_option lookup_bool "minimize"

   305     val timeout = lookup_time "timeout"

   306     val preplay_timeout = if mode = Auto_Try then Time.zeroTime else lookup_time "preplay_timeout"

   307     val expect = lookup_string "expect"

   308   in

   309     {debug = debug, verbose = verbose, overlord = overlord, spy = spy, blocking = blocking,

   310      provers = provers, type_enc = type_enc, strict = strict, lam_trans = lam_trans,

   311      uncurried_aliases = uncurried_aliases, learn = learn, fact_filter = fact_filter,

   312      max_facts = max_facts, fact_thresholds = fact_thresholds, max_mono_iters = max_mono_iters,

   313      max_new_mono_instances = max_new_mono_instances, isar_proofs = isar_proofs,

   314      compress = compress, try0 = try0, smt_proofs = smt_proofs, slice = slice, minimize = minimize,

   315      timeout = timeout, preplay_timeout = preplay_timeout, expect = expect}

   316   end

   318 fun get_params mode = extract_params mode o default_raw_params mode

   319 fun default_params thy = get_params Normal thy o map (apsnd single)

   321 (* Sledgehammer the given subgoal *)

   323 val default_minimize_prover = metisN

   325 fun is_raw_param_relevant_for_minimize (name, _) =

   326   not (member (op =) params_not_for_minimize name)

   327 fun string_of_raw_param (key, values) =

   328   key ^ (case implode_param values of "" => "" | value => " = " ^ value)

   329 fun nice_string_of_raw_param (p as (key, ["false"])) =

   330     (case AList.find (op =) negated_alias_params key of

   331        [neg] => neg

   332      | _ => string_of_raw_param p)

   333   | nice_string_of_raw_param p = string_of_raw_param p

   335 fun minimize_command override_params i more_override_params prover_name

   336                      fact_names =

   337   let

   338     val params =

   339       (override_params

   340        |> filter_out (AList.defined (op =) more_override_params o fst)) @

   341       more_override_params

   342       |> filter is_raw_param_relevant_for_minimize

   343       |> map nice_string_of_raw_param

   344       |> (if prover_name = default_minimize_prover then I else cons prover_name)

   345       |> space_implode ", "

   346   in

   347     sledgehammerN ^ " " ^ minN ^

   348     (if params = "" then "" else enclose " [" "]" params) ^

   349     " (" ^ space_implode " " fact_names ^ ")" ^

   350     (if i = 1 then "" else " " ^ string_of_int i)

   351   end

   353 val default_learn_prover_timeout = 2.0

   355 fun hammer_away override_params subcommand opt_i fact_override state0 =

   356   let

   357     val state =

   358       Proof.map_contexts (Try0.silence_methods false #> Config.put SMT2_Config.verbose false) state0

   359     val thy = Proof.theory_of state

   360     val ctxt = Proof.context_of state

   362     val override_params = override_params |> map (normalize_raw_param ctxt)

   363     val _ = Isabelle_System.mkdir (Path.explode (getenv "ISABELLE_TMP"))

   364   in

   365     if subcommand = runN then

   366       let val i = the_default 1 opt_i in

   367         run_sledgehammer (get_params Normal thy override_params) Normal NONE i fact_override

   368           (minimize_command override_params i) state

   369         |> K ()

   370       end

   371     else if subcommand = minN then

   372       let

   373         val ctxt = ctxt |> Config.put instantiate_inducts false

   374         val i = the_default 1 opt_i

   375         val params =

   376           get_params Minimize thy (("provers", [default_minimize_prover]) :: override_params)

   377         val goal = prop_of (#goal (Proof.goal state))

   378         val facts = nearly_all_facts ctxt false fact_override Symtab.empty

   379                                      Termtab.empty [] [] goal

   380         val learn = mash_learn_proof ctxt params goal facts

   381       in run_minimize params learn i (#add fact_override) state end

   382     else if subcommand = messagesN then

   383       messages opt_i

   384     else if subcommand = supported_proversN then

   385       supported_provers ctxt

   386     else if subcommand = kill_allN then

   387       (kill_provers ();

   388        kill_learners ctxt (get_params Normal thy override_params))

   389     else if subcommand = running_proversN then

   390       running_provers ()

   391     else if subcommand = unlearnN then

   392       mash_unlearn ctxt (get_params Normal thy override_params)

   393     else if subcommand = learn_isarN orelse subcommand = learn_proverN orelse

   394             subcommand = relearn_isarN orelse subcommand = relearn_proverN then

   395       (if subcommand = relearn_isarN orelse subcommand = relearn_proverN then

   396          mash_unlearn ctxt (get_params Normal thy override_params)

   397        else

   398          ();

   399        mash_learn ctxt

   400            (* TODO: Use MaSh mode instead and have the special defaults hardcoded in "get_params" *)

   401            (get_params Normal thy

   402                 ([("timeout", [string_of_real default_learn_prover_timeout]),

   403                   ("slice", ["false"])] @

   404                  override_params @

   405                  [("minimize", ["true"]),

   406                   ("preplay_timeout", ["0"])]))

   407            fact_override (#facts (Proof.goal state))

   408            (subcommand = learn_proverN orelse subcommand = relearn_proverN))

   409     else if subcommand = running_learnersN then

   410       running_learners ()

   411     else if subcommand = refresh_tptpN then

   412       refresh_systems_on_tptp ()

   413     else

   414       error ("Unknown subcommand: " ^ quote subcommand ^ ".")

   415   end

   417 fun sledgehammer_trans (((subcommand, params), fact_override), opt_i) =

   418   Toplevel.unknown_proof o

   419   Toplevel.keep (hammer_away params subcommand opt_i fact_override

   420                  o Toplevel.proof_of)

   422 fun string_of_raw_param (name, value) = name ^ " = " ^ implode_param value

   424 fun sledgehammer_params_trans params =

   425   Toplevel.theory

   426     (fold set_default_raw_param params

   427      #> tap (fn thy =>

   428           writeln ("Default parameters for Sledgehammer:\n" ^

   429             (case rev (default_raw_params Normal thy) of

   430               [] => "none"

   431             | params => params |> map string_of_raw_param |> sort_strings |> cat_lines))))

   433 val parse_query_bang = @{keyword "?"} || @{keyword "!"} || @{keyword "!!"}

   434 val parse_key =

   435   Scan.repeat1 (Parse.typ_group || parse_query_bang) >> implode_param

   436 val parse_value =

   437   Scan.repeat1 (Parse.xname || Parse.float_number || parse_query_bang)

   438 val parse_param = parse_key -- Scan.optional (@{keyword "="} |-- parse_value) []

   439 val parse_params = Scan.optional (Args.bracks (Parse.list parse_param)) []

   440 val parse_fact_refs =

   441   Scan.repeat1 (Scan.unless (Parse.name -- Args.colon) Parse_Spec.xthm)

   442 val parse_fact_override_chunk =

   443   (Args.add |-- Args.colon |-- parse_fact_refs >> add_fact_override)

   444   || (Args.del |-- Args.colon |-- parse_fact_refs >> del_fact_override)

   445   || (parse_fact_refs >> only_fact_override)

   446 val parse_fact_override =

   447   Scan.optional (Args.parens (Scan.repeat parse_fact_override_chunk

   448                               >> merge_fact_overrides))

   449                 no_fact_override

   451 val _ =

   452   Outer_Syntax.improper_command @{command_spec "sledgehammer"}

   453     "search for first-order proof using automatic theorem provers"

   454     ((Scan.optional Parse.short_ident runN -- parse_params

   455       -- parse_fact_override -- Scan.option Parse.nat) #>> sledgehammer_trans)

   456 val _ =

   457   Outer_Syntax.command @{command_spec "sledgehammer_params"}

   458     "set and display the default parameters for Sledgehammer"

   459     (parse_params #>> sledgehammer_params_trans)

   461 fun try_sledgehammer auto state =

   462   let

   463     val thy = Proof.theory_of state

   464     val mode = if auto then Auto_Try else Try

   465     val i = 1

   466   in

   467     run_sledgehammer (get_params mode thy []) mode NONE i no_fact_override (minimize_command [] i)

   468       state

   469   end

   471 val _ = Try.tool_setup (sledgehammerN, (40, @{system_option auto_sledgehammer}, try_sledgehammer))

   473 val _ =

   474   Query_Operation.register sledgehammerN (fn {state = st, args, output_result} =>

   475     (case try Toplevel.proof_of st of

   476       SOME state =>

   477         let

   478           val thy = Proof.theory_of state

   479           val ctxt = Proof.context_of state

   480           val [provers_arg, isar_proofs_arg] = args

   482           val override_params =

   483             ((if provers_arg = "" then [] else [("provers", space_explode " " provers_arg)]) @

   484               [("isar_proofs", [isar_proofs_arg]),

   485                ("blocking", ["true"]),

   486                ("minimize", ["true"]),

   487                ("debug", ["false"]),

   488                ("verbose", ["false"]),

   489                ("overlord", ["false"])])

   490             |> map (normalize_raw_param ctxt)

   492           val _ = run_sledgehammer (get_params Normal thy override_params) Normal

   493             (SOME output_result) 1 no_fact_override (minimize_command override_params 1) state

   494         in () end

   495     | NONE => error "Unknown proof context"))

   497 end;

author	blanchet
	Wed, 18 Jun 2014 14:19:42 +0200
changeset 58615	01b68f625550
parent 58587	f6bf6d5341ee
child 58616	0acfdb151e52
permissions	-rw-r--r--