src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML
author blanchet
Tue, 30 Sep 2014 14:18:07 +0200
changeset 58494 ed380b9594b5
parent 58085 ee65e9cfe284
child 58654 3e1cad27fc2f
permissions -rw-r--r--
always minimize, to reinvoke the prover with nicer options and yield a nicer Isar proof (potentially -- cf. 'full_proof')
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
55202
824c48a539c9 renamed many Sledgehammer ML files to clarify structure
blanchet
parents: 55201
diff changeset
     1
(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML
31037
ac8669134e7a added Philipp Meyer's implementation of AtpMinimal
immler@in.tum.de
parents:
diff changeset
     2
    Author:     Philipp Meyer, TU Muenchen
36370
a4f601daa175 centralized ATP-specific error handling in "atp_wrapper.ML"
blanchet
parents: 36369
diff changeset
     3
    Author:     Jasmin Blanchette, TU Muenchen
31037
ac8669134e7a added Philipp Meyer's implementation of AtpMinimal
immler@in.tum.de
parents:
diff changeset
     4
40977
9140c5950494 [mq]: sledge_binary_minimizer
blanchet
parents: 40941
diff changeset
     5
Minimization of fact list for Metis using external provers.
31037
ac8669134e7a added Philipp Meyer's implementation of AtpMinimal
immler@in.tum.de
parents:
diff changeset
     6
*)
ac8669134e7a added Philipp Meyer's implementation of AtpMinimal
immler@in.tum.de
parents:
diff changeset
     7
55202
824c48a539c9 renamed many Sledgehammer ML files to clarify structure
blanchet
parents: 55201
diff changeset
     8
signature SLEDGEHAMMER_PROVER_MINIMIZE =
32525
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32510
diff changeset
     9
sig
46340
cac402c486b0 separate orthogonal components
blanchet
parents: 46320
diff changeset
    10
  type stature = ATP_Problem_Generate.stature
55287
ffa306239316 renamed ML file
blanchet
parents: 55285
diff changeset
    11
  type proof_method = Sledgehammer_Proof_Methods.proof_method
ffa306239316 renamed ML file
blanchet
parents: 55285
diff changeset
    12
  type play_outcome = Sledgehammer_Proof_Methods.play_outcome
55201
1ee776da8da7 renamed ML file
blanchet
parents: 55183
diff changeset
    13
  type mode = Sledgehammer_Prover.mode
1ee776da8da7 renamed ML file
blanchet
parents: 55183
diff changeset
    14
  type params = Sledgehammer_Prover.params
1ee776da8da7 renamed ML file
blanchet
parents: 55183
diff changeset
    15
  type prover = Sledgehammer_Prover.prover
35867
16279c4c7a33 move all ATP setup code into ATP_Wrapper
blanchet
parents: 35866
diff changeset
    16
55205
8450622db0c5 refactor large ML file
blanchet
parents: 55202
diff changeset
    17
  val is_prover_supported : Proof.context -> string -> bool
8450622db0c5 refactor large ML file
blanchet
parents: 55202
diff changeset
    18
  val is_prover_installed : Proof.context -> string -> bool
8450622db0c5 refactor large ML file
blanchet
parents: 55202
diff changeset
    19
  val default_max_facts_of_prover : Proof.context -> string -> int
8450622db0c5 refactor large ML file
blanchet
parents: 55202
diff changeset
    20
  val get_prover : Proof.context -> mode -> string -> prover
8450622db0c5 refactor large ML file
blanchet
parents: 55202
diff changeset
    21
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42579
diff changeset
    22
  val binary_min_facts : int Config.T
54824
4e58a38b330b refactored preplaying outcome data structure
blanchet
parents: 54816
diff changeset
    23
  val minimize_facts : (thm list -> unit) -> string -> params -> bool -> int -> int ->
57734
18bb3e1ff6f6 rationalized preplaying by eliminating (now superfluous) laziness
blanchet
parents: 57732
diff changeset
    24
    Proof.state -> thm -> ((string * stature) * thm list) list ->
57739
blanchet
parents: 57738
diff changeset
    25
    ((string * stature) * thm list) list option
57750
670cbec816b9 restored a bit of laziness
blanchet
parents: 57739
diff changeset
    26
    * ((unit -> (string * stature) list * (proof_method * play_outcome)) -> string)
54503
blanchet
parents: 54141
diff changeset
    27
  val get_minimizing_prover : Proof.context -> mode -> (thm list -> unit) -> string -> prover
35866
513074557e06 move the Sledgehammer Isar commands together into one file;
blanchet
parents: 35865
diff changeset
    28
end;
32525
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32510
diff changeset
    29
55202
824c48a539c9 renamed many Sledgehammer ML files to clarify structure
blanchet
parents: 55201
diff changeset
    30
structure Sledgehammer_Prover_Minimize : SLEDGEHAMMER_PROVER_MINIMIZE =
31037
ac8669134e7a added Philipp Meyer's implementation of AtpMinimal
immler@in.tum.de
parents:
diff changeset
    31
struct
ac8669134e7a added Philipp Meyer's implementation of AtpMinimal
immler@in.tum.de
parents:
diff changeset
    32
43085
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation
blanchet
parents: 43064
diff changeset
    33
open ATP_Util
39496
a52a4e4399c1 got caught once again by SML's pattern maching (ctor vs. var)
blanchet
parents: 39491
diff changeset
    34
open ATP_Proof
46320
0b8b73b49848 renamed two files to make room for a new file
blanchet
parents: 46301
diff changeset
    35
open ATP_Problem_Generate
55212
blanchet
parents: 55205
diff changeset
    36
open ATP_Proof_Reconstruct
51200
260cb10aac4b minimize SMT proofs with E if Isar proofs are desired and Metis managed to preplay
blanchet
parents: 51191
diff changeset
    37
open ATP_Systems
36142
f5e15e9aae10 make Sledgehammer "minimize" output less confusing + round up (not down) time limits to nearest second
blanchet
parents: 36063
diff changeset
    38
open Sledgehammer_Util
48250
1065c307fafe further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents: 48085
diff changeset
    39
open Sledgehammer_Fact
55287
ffa306239316 renamed ML file
blanchet
parents: 55285
diff changeset
    40
open Sledgehammer_Proof_Methods
55202
824c48a539c9 renamed many Sledgehammer ML files to clarify structure
blanchet
parents: 55201
diff changeset
    41
open Sledgehammer_Isar
55201
1ee776da8da7 renamed ML file
blanchet
parents: 55183
diff changeset
    42
open Sledgehammer_Prover
55205
8450622db0c5 refactor large ML file
blanchet
parents: 55202
diff changeset
    43
open Sledgehammer_Prover_ATP
58061
3d060f43accb renamed new SMT module from 'SMT2' to 'SMT'
blanchet
parents: 57781
diff changeset
    44
open Sledgehammer_Prover_SMT
55205
8450622db0c5 refactor large ML file
blanchet
parents: 55202
diff changeset
    45
8450622db0c5 refactor large ML file
blanchet
parents: 55202
diff changeset
    46
fun is_prover_supported ctxt =
8450622db0c5 refactor large ML file
blanchet
parents: 55202
diff changeset
    47
  let val thy = Proof_Context.theory_of ctxt in
58061
3d060f43accb renamed new SMT module from 'SMT2' to 'SMT'
blanchet
parents: 57781
diff changeset
    48
    is_atp thy orf is_smt_prover ctxt
55205
8450622db0c5 refactor large ML file
blanchet
parents: 55202
diff changeset
    49
  end
8450622db0c5 refactor large ML file
blanchet
parents: 55202
diff changeset
    50
8450622db0c5 refactor large ML file
blanchet
parents: 55202
diff changeset
    51
fun is_prover_installed ctxt =
58061
3d060f43accb renamed new SMT module from 'SMT2' to 'SMT'
blanchet
parents: 57781
diff changeset
    52
  is_smt_prover ctxt orf is_atp_installed (Proof_Context.theory_of ctxt)
55205
8450622db0c5 refactor large ML file
blanchet
parents: 55202
diff changeset
    53
8450622db0c5 refactor large ML file
blanchet
parents: 55202
diff changeset
    54
fun default_max_facts_of_prover ctxt name =
8450622db0c5 refactor large ML file
blanchet
parents: 55202
diff changeset
    55
  let val thy = Proof_Context.theory_of ctxt in
57732
e1b2442dc629 simplified minimization logic
blanchet
parents: 57723
diff changeset
    56
    if is_atp thy name then
55205
8450622db0c5 refactor large ML file
blanchet
parents: 55202
diff changeset
    57
      fold (Integer.max o fst o #1 o fst o snd) (#best_slices (get_atp thy name ()) ctxt) 0
58061
3d060f43accb renamed new SMT module from 'SMT2' to 'SMT'
blanchet
parents: 57781
diff changeset
    58
    else if is_smt_prover ctxt name then
3d060f43accb renamed new SMT module from 'SMT2' to 'SMT'
blanchet
parents: 57781
diff changeset
    59
      SMT_Solver.default_max_relevant ctxt name
56081
72fad75baf7e integrate SMT2 with Sledgehammer
blanchet
parents: 55452
diff changeset
    60
    else
72fad75baf7e integrate SMT2 with Sledgehammer
blanchet
parents: 55452
diff changeset
    61
      error ("No such prover: " ^ name ^ ".")
55205
8450622db0c5 refactor large ML file
blanchet
parents: 55202
diff changeset
    62
  end
8450622db0c5 refactor large ML file
blanchet
parents: 55202
diff changeset
    63
8450622db0c5 refactor large ML file
blanchet
parents: 55202
diff changeset
    64
fun get_prover ctxt mode name =
8450622db0c5 refactor large ML file
blanchet
parents: 55202
diff changeset
    65
  let val thy = Proof_Context.theory_of ctxt in
57732
e1b2442dc629 simplified minimization logic
blanchet
parents: 57723
diff changeset
    66
    if is_atp thy name then run_atp mode name
58061
3d060f43accb renamed new SMT module from 'SMT2' to 'SMT'
blanchet
parents: 57781
diff changeset
    67
    else if is_smt_prover ctxt name then run_smt_solver mode name
55205
8450622db0c5 refactor large ML file
blanchet
parents: 55202
diff changeset
    68
    else error ("No such prover: " ^ name ^ ".")
8450622db0c5 refactor large ML file
blanchet
parents: 55202
diff changeset
    69
  end
35866
513074557e06 move the Sledgehammer Isar commands together into one file;
blanchet
parents: 35865
diff changeset
    70
36370
a4f601daa175 centralized ATP-specific error handling in "atp_wrapper.ML"
blanchet
parents: 36369
diff changeset
    71
(* wrapper for calling external prover *)
31236
2a1f5c87ac28 proper signature constraint;
wenzelm
parents: 31037
diff changeset
    72
40061
71cc5aac8b76 generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents: 40060
diff changeset
    73
fun n_facts names =
38698
d19c3a7ce38b clean handling of whether a fact is chained or not;
blanchet
parents: 38696
diff changeset
    74
  let val n = length names in
40061
71cc5aac8b76 generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents: 40060
diff changeset
    75
    string_of_int n ^ " fact" ^ plural_s n ^
57781
c1ce4ef23be5 restored more sorting
blanchet
parents: 57776
diff changeset
    76
    (if n > 0 then ": " ^ (names |> map fst |> sort string_ord |> space_implode " ") else "")
38092
81a003f7de0d speed up the minimizer by using the time taken for the first iteration as a timeout for the following iterations, and fix a subtle bug in "string_for_failure"
blanchet
parents: 38084
diff changeset
    77
  end
81a003f7de0d speed up the minimizer by using the time taken for the first iteration as a timeout for the following iterations, and fix a subtle bug in "string_for_failure"
blanchet
parents: 38084
diff changeset
    78
41091
0afdf5cde874 implicitly call the minimizer for SMT solvers that don't return an unsat core
blanchet
parents: 41090
diff changeset
    79
fun print silent f = if silent then () else Output.urgent_message (f ())
0afdf5cde874 implicitly call the minimizer for SMT solvers that don't return an unsat core
blanchet
parents: 41090
diff changeset
    80
54824
4e58a38b330b refactored preplaying outcome data structure
blanchet
parents: 54816
diff changeset
    81
fun test_facts ({debug, verbose, overlord, spy, provers, max_mono_iters, max_new_mono_instances,
57245
f6bf6d5341ee renamed Sledgehammer options
blanchet
parents: 57208
diff changeset
    82
      type_enc, strict, lam_trans, uncurried_aliases, isar_proofs, compress, try0, smt_proofs,
57673
858c1a63967f don't lose 'minimize' flag before it reaches Isar proof text generation
blanchet
parents: 57245
diff changeset
    83
      minimize, preplay_timeout, ...} : params)
54824
4e58a38b330b refactored preplaying outcome data structure
blanchet
parents: 54816
diff changeset
    84
    silent (prover : prover) timeout i n state goal facts =
31236
2a1f5c87ac28 proper signature constraint;
wenzelm
parents: 31037
diff changeset
    85
  let
57054
blanchet
parents: 56985
diff changeset
    86
    val _ = print silent (fn () => "Testing " ^ n_facts (map fst facts) ^
blanchet
parents: 56985
diff changeset
    87
      (if verbose then " (timeout: " ^ string_of_time timeout ^ ")" else "") ^ "...")
blanchet
parents: 56985
diff changeset
    88
51005
ce4290c33d73 eliminated needless speed optimization -- and simplified code quite a bit
blanchet
parents: 50669
diff changeset
    89
    val facts = facts |> maps (fn (n, ths) => map (pair n) ths)
38100
e458a0dd3dc1 use "explicit_apply" in the minimizer whenever it might make a difference to prevent freak failures;
blanchet
parents: 38094
diff changeset
    90
    val params =
53800
ac1ec5065316 added "spy" option to Sledgehammer
blanchet
parents: 53764
diff changeset
    91
      {debug = debug, verbose = verbose, overlord = overlord, spy = spy, blocking = true,
ac1ec5065316 added "spy" option to Sledgehammer
blanchet
parents: 53764
diff changeset
    92
       provers = provers, type_enc = type_enc, strict = strict, lam_trans = lam_trans,
ac1ec5065316 added "spy" option to Sledgehammer
blanchet
parents: 53764
diff changeset
    93
       uncurried_aliases = uncurried_aliases, learn = false, fact_filter = NONE,
ac1ec5065316 added "spy" option to Sledgehammer
blanchet
parents: 53764
diff changeset
    94
       max_facts = SOME (length facts), fact_thresholds = (1.01, 1.01),
ac1ec5065316 added "spy" option to Sledgehammer
blanchet
parents: 53764
diff changeset
    95
       max_mono_iters = max_mono_iters, max_new_mono_instances = max_new_mono_instances,
57245
f6bf6d5341ee renamed Sledgehammer options
blanchet
parents: 57208
diff changeset
    96
       isar_proofs = isar_proofs, compress = compress, try0 = try0, smt_proofs = smt_proofs,
57673
858c1a63967f don't lose 'minimize' flag before it reaches Isar proof text generation
blanchet
parents: 57245
diff changeset
    97
       slice = false, minimize = minimize, timeout = timeout, preplay_timeout = preplay_timeout,
57245
f6bf6d5341ee renamed Sledgehammer options
blanchet
parents: 57208
diff changeset
    98
       expect = ""}
40065
1e4c7185f3f9 remove more needless code ("run_smt_solvers");
blanchet
parents: 40063
diff changeset
    99
    val problem =
54141
f57f8e7a879f generate a comment storing the goal nickname in "learn_prover"
blanchet
parents: 54130
diff changeset
   100
      {comment = "", state = state, goal = goal, subgoal = i, subgoal_count = n,
f57f8e7a879f generate a comment storing the goal nickname in "learn_prover"
blanchet
parents: 54130
diff changeset
   101
       factss = [("", facts)]}
57735
056a55b44ec7 eliminated Sledgehammer's "min" subcommand (and lots of complications in the code)
blanchet
parents: 57734
diff changeset
   102
    val result as {outcome, used_facts, run_time, ...} = prover params problem
36223
217ca1273786 make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents: 36143
diff changeset
   103
  in
55202
824c48a539c9 renamed many Sledgehammer ML files to clarify structure
blanchet
parents: 55201
diff changeset
   104
    print silent (fn () =>
824c48a539c9 renamed many Sledgehammer ML files to clarify structure
blanchet
parents: 55201
diff changeset
   105
      (case outcome of
824c48a539c9 renamed many Sledgehammer ML files to clarify structure
blanchet
parents: 55201
diff changeset
   106
        SOME failure => string_of_atp_failure failure
824c48a539c9 renamed many Sledgehammer ML files to clarify structure
blanchet
parents: 55201
diff changeset
   107
      | NONE =>
824c48a539c9 renamed many Sledgehammer ML files to clarify structure
blanchet
parents: 55201
diff changeset
   108
        "Found proof" ^
824c48a539c9 renamed many Sledgehammer ML files to clarify structure
blanchet
parents: 55201
diff changeset
   109
         (if length used_facts = length facts then "" else " with " ^ n_facts used_facts) ^
824c48a539c9 renamed many Sledgehammer ML files to clarify structure
blanchet
parents: 55201
diff changeset
   110
         " (" ^ string_of_time run_time ^ ")."));
38092
81a003f7de0d speed up the minimizer by using the time taken for the first iteration as a timeout for the following iterations, and fix a subtle bug in "string_for_failure"
blanchet
parents: 38084
diff changeset
   111
    result
36223
217ca1273786 make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents: 36143
diff changeset
   112
  end
31236
2a1f5c87ac28 proper signature constraint;
wenzelm
parents: 31037
diff changeset
   113
40204
da97d75e20e6 standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer -- but keep "Axiom" in the lower-level "ATP_Problem" module
blanchet
parents: 40200
diff changeset
   114
(* minimalization of facts *)
31236
2a1f5c87ac28 proper signature constraint;
wenzelm
parents: 31037
diff changeset
   115
45372
cc455b2897f8 cascading timeouts in minimizer, part 2
blanchet
parents: 45371
diff changeset
   116
(* Give the external prover some slack. The ATP gets further slack because the
cc455b2897f8 cascading timeouts in minimizer, part 2
blanchet
parents: 45371
diff changeset
   117
   Sledgehammer preprocessing time is included in the estimate below but isn't
cc455b2897f8 cascading timeouts in minimizer, part 2
blanchet
parents: 45371
diff changeset
   118
   part of the timeout. *)
cc455b2897f8 cascading timeouts in minimizer, part 2
blanchet
parents: 45371
diff changeset
   119
val slack_msecs = 200
cc455b2897f8 cascading timeouts in minimizer, part 2
blanchet
parents: 45371
diff changeset
   120
54816
10d48c2a3e32 made timeouts in Sledgehammer not be 'option's -- simplified lots of code
blanchet
parents: 54815
diff changeset
   121
fun new_timeout timeout run_time =
10d48c2a3e32 made timeouts in Sledgehammer not be 'option's -- simplified lots of code
blanchet
parents: 54815
diff changeset
   122
  Int.min (Time.toMilliseconds timeout, Time.toMilliseconds run_time + slack_msecs)
10d48c2a3e32 made timeouts in Sledgehammer not be 'option's -- simplified lots of code
blanchet
parents: 54815
diff changeset
   123
  |> Time.fromMilliseconds
45372
cc455b2897f8 cascading timeouts in minimizer, part 2
blanchet
parents: 45371
diff changeset
   124
45367
cb54f1b34cf9 shortcut binary minimization algorithm
blanchet
parents: 45366
diff changeset
   125
(* The linear algorithm usually outperforms the binary algorithm when over 60%
cb54f1b34cf9 shortcut binary minimization algorithm
blanchet
parents: 45366
diff changeset
   126
   of the facts are actually needed. The binary algorithm is much more
cb54f1b34cf9 shortcut binary minimization algorithm
blanchet
parents: 45366
diff changeset
   127
   appropriate for provers that cannot return the list of used facts and hence
cb54f1b34cf9 shortcut binary minimization algorithm
blanchet
parents: 45366
diff changeset
   128
   returns all facts as used. Since we cannot know in advance how many facts are
cb54f1b34cf9 shortcut binary minimization algorithm
blanchet
parents: 45366
diff changeset
   129
   actually needed, we heuristically set the threshold to 10 facts. *)
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42579
diff changeset
   130
val binary_min_facts =
55202
824c48a539c9 renamed many Sledgehammer ML files to clarify structure
blanchet
parents: 55201
diff changeset
   131
  Attrib.setup_config_int @{binding sledgehammer_minimize_binary_min_facts} (K 20)
40977
9140c5950494 [mq]: sledge_binary_minimizer
blanchet
parents: 40941
diff changeset
   132
45368
ff2edf24e83a cascading timeouts in minimizer
blanchet
parents: 45367
diff changeset
   133
fun linear_minimize test timeout result xs =
ff2edf24e83a cascading timeouts in minimizer
blanchet
parents: 45367
diff changeset
   134
  let
ff2edf24e83a cascading timeouts in minimizer
blanchet
parents: 45367
diff changeset
   135
    fun min _ [] p = p
ff2edf24e83a cascading timeouts in minimizer
blanchet
parents: 45367
diff changeset
   136
      | min timeout (x :: xs) (seen, result) =
54816
10d48c2a3e32 made timeouts in Sledgehammer not be 'option's -- simplified lots of code
blanchet
parents: 54815
diff changeset
   137
        (case test timeout (xs @ seen) of
10d48c2a3e32 made timeouts in Sledgehammer not be 'option's -- simplified lots of code
blanchet
parents: 54815
diff changeset
   138
          result as {outcome = NONE, used_facts, run_time, ...} : prover_result =>
55202
824c48a539c9 renamed many Sledgehammer ML files to clarify structure
blanchet
parents: 55201
diff changeset
   139
          min (new_timeout timeout run_time) (filter_used_facts true used_facts xs)
824c48a539c9 renamed many Sledgehammer ML files to clarify structure
blanchet
parents: 55201
diff changeset
   140
            (filter_used_facts false used_facts seen, result)
54816
10d48c2a3e32 made timeouts in Sledgehammer not be 'option's -- simplified lots of code
blanchet
parents: 54815
diff changeset
   141
        | _ => min timeout xs (x :: seen, result))
10d48c2a3e32 made timeouts in Sledgehammer not be 'option's -- simplified lots of code
blanchet
parents: 54815
diff changeset
   142
  in
10d48c2a3e32 made timeouts in Sledgehammer not be 'option's -- simplified lots of code
blanchet
parents: 54815
diff changeset
   143
    min timeout xs ([], result)
10d48c2a3e32 made timeouts in Sledgehammer not be 'option's -- simplified lots of code
blanchet
parents: 54815
diff changeset
   144
  end
38015
b30c3c2e1030 implemented "sublinear" minimization algorithm
blanchet
parents: 38002
diff changeset
   145
45368
ff2edf24e83a cascading timeouts in minimizer
blanchet
parents: 45367
diff changeset
   146
fun binary_minimize test timeout result xs =
40977
9140c5950494 [mq]: sledge_binary_minimizer
blanchet
parents: 40941
diff changeset
   147
  let
55202
824c48a539c9 renamed many Sledgehammer ML files to clarify structure
blanchet
parents: 55201
diff changeset
   148
    fun min depth (result as {run_time, ...} : prover_result) sup (xs as _ :: _ :: _) =
41743
blanchet
parents: 41742
diff changeset
   149
        let
45367
cb54f1b34cf9 shortcut binary minimization algorithm
blanchet
parents: 45366
diff changeset
   150
          val (l0, r0) = chop (length xs div 2) xs
41743
blanchet
parents: 41742
diff changeset
   151
(*
55202
824c48a539c9 renamed many Sledgehammer ML files to clarify structure
blanchet
parents: 55201
diff changeset
   152
          val _ = warning (replicate_string depth " " ^ "{ " ^ "sup: " ^ n_facts (map fst sup))
824c48a539c9 renamed many Sledgehammer ML files to clarify structure
blanchet
parents: 55201
diff changeset
   153
          val _ = warning (replicate_string depth " " ^ " " ^ "xs: " ^ n_facts (map fst xs))
824c48a539c9 renamed many Sledgehammer ML files to clarify structure
blanchet
parents: 55201
diff changeset
   154
          val _ = warning (replicate_string depth " " ^ " " ^ "l0: " ^ n_facts (map fst l0))
824c48a539c9 renamed many Sledgehammer ML files to clarify structure
blanchet
parents: 55201
diff changeset
   155
          val _ = warning (replicate_string depth " " ^ " " ^ "r0: " ^ n_facts (map fst r0))
41743
blanchet
parents: 41742
diff changeset
   156
*)
45367
cb54f1b34cf9 shortcut binary minimization algorithm
blanchet
parents: 45366
diff changeset
   157
          val depth = depth + 1
45372
cc455b2897f8 cascading timeouts in minimizer, part 2
blanchet
parents: 45371
diff changeset
   158
          val timeout = new_timeout timeout run_time
41743
blanchet
parents: 41742
diff changeset
   159
        in
55202
824c48a539c9 renamed many Sledgehammer ML files to clarify structure
blanchet
parents: 55201
diff changeset
   160
          (case test timeout (sup @ l0) of
45372
cc455b2897f8 cascading timeouts in minimizer, part 2
blanchet
parents: 45371
diff changeset
   161
            result as {outcome = NONE, used_facts, ...} =>
48798
9152e66f98da be less aggressive at kicking out chained facts
blanchet
parents: 48796
diff changeset
   162
            min depth result (filter_used_facts true used_facts sup)
57781
c1ce4ef23be5 restored more sorting
blanchet
parents: 57776
diff changeset
   163
              (filter_used_facts true used_facts l0)
45367
cb54f1b34cf9 shortcut binary minimization algorithm
blanchet
parents: 45366
diff changeset
   164
          | _ =>
55202
824c48a539c9 renamed many Sledgehammer ML files to clarify structure
blanchet
parents: 55201
diff changeset
   165
            (case test timeout (sup @ r0) of
45367
cb54f1b34cf9 shortcut binary minimization algorithm
blanchet
parents: 45366
diff changeset
   166
              result as {outcome = NONE, used_facts, ...} =>
48798
9152e66f98da be less aggressive at kicking out chained facts
blanchet
parents: 48796
diff changeset
   167
              min depth result (filter_used_facts true used_facts sup)
57054
blanchet
parents: 56985
diff changeset
   168
                (filter_used_facts true used_facts r0)
45367
cb54f1b34cf9 shortcut binary minimization algorithm
blanchet
parents: 45366
diff changeset
   169
            | _ =>
cb54f1b34cf9 shortcut binary minimization algorithm
blanchet
parents: 45366
diff changeset
   170
              let
cb54f1b34cf9 shortcut binary minimization algorithm
blanchet
parents: 45366
diff changeset
   171
                val (sup_r0, (l, result)) = min depth result (sup @ r0) l0
55202
824c48a539c9 renamed many Sledgehammer ML files to clarify structure
blanchet
parents: 55201
diff changeset
   172
                val (sup, r0) = (sup, r0) |> pairself (filter_used_facts true (map fst sup_r0))
45367
cb54f1b34cf9 shortcut binary minimization algorithm
blanchet
parents: 45366
diff changeset
   173
                val (sup_l, (r, result)) = min depth result (sup @ l) r0
48798
9152e66f98da be less aggressive at kicking out chained facts
blanchet
parents: 48796
diff changeset
   174
                val sup = sup |> filter_used_facts true (map fst sup_l)
55202
824c48a539c9 renamed many Sledgehammer ML files to clarify structure
blanchet
parents: 55201
diff changeset
   175
              in (sup, (l @ r, result)) end))
40977
9140c5950494 [mq]: sledge_binary_minimizer
blanchet
parents: 40941
diff changeset
   176
        end
41743
blanchet
parents: 41742
diff changeset
   177
(*
blanchet
parents: 41742
diff changeset
   178
        |> tap (fn _ => warning (replicate_string depth " " ^ "}"))
blanchet
parents: 41742
diff changeset
   179
*)
45367
cb54f1b34cf9 shortcut binary minimization algorithm
blanchet
parents: 45366
diff changeset
   180
      | min _ result sup xs = (sup, (xs, result))
cb54f1b34cf9 shortcut binary minimization algorithm
blanchet
parents: 45366
diff changeset
   181
  in
55202
824c48a539c9 renamed many Sledgehammer ML files to clarify structure
blanchet
parents: 55201
diff changeset
   182
    (case snd (min 0 result [] xs) of
45372
cc455b2897f8 cascading timeouts in minimizer, part 2
blanchet
parents: 45371
diff changeset
   183
      ([x], result as {run_time, ...}) =>
cc455b2897f8 cascading timeouts in minimizer, part 2
blanchet
parents: 45371
diff changeset
   184
      (case test (new_timeout timeout run_time) [] of
55202
824c48a539c9 renamed many Sledgehammer ML files to clarify structure
blanchet
parents: 55201
diff changeset
   185
        result as {outcome = NONE, ...} => ([], result)
824c48a539c9 renamed many Sledgehammer ML files to clarify structure
blanchet
parents: 55201
diff changeset
   186
      | _ => ([x], result))
824c48a539c9 renamed many Sledgehammer ML files to clarify structure
blanchet
parents: 55201
diff changeset
   187
    | p => p)
45367
cb54f1b34cf9 shortcut binary minimization algorithm
blanchet
parents: 45366
diff changeset
   188
  end
40977
9140c5950494 [mq]: sledge_binary_minimizer
blanchet
parents: 40941
diff changeset
   189
54816
10d48c2a3e32 made timeouts in Sledgehammer not be 'option's -- simplified lots of code
blanchet
parents: 54815
diff changeset
   190
fun minimize_facts do_learn prover_name (params as {learn, timeout, ...}) silent i n state goal
57734
18bb3e1ff6f6 rationalized preplaying by eliminating (now superfluous) laziness
blanchet
parents: 57732
diff changeset
   191
    facts =
31236
2a1f5c87ac28 proper signature constraint;
wenzelm
parents: 31037
diff changeset
   192
  let
40941
a3e6f8634a11 replace "smt" prover with specific SMT solvers, e.g. "z3" -- whatever the SMT module gives us
blanchet
parents: 40553
diff changeset
   193
    val ctxt = Proof.context_of state
58085
ee65e9cfe284 merged minimize and auto_minimize
blanchet
parents: 58061
diff changeset
   194
    val prover = get_prover ctxt Minimize prover_name
54130
b4e6cd4cab92 thread the goal through instead of relying on unreliable (possibly fake) state
blanchet
parents: 54127
diff changeset
   195
    fun test timeout = test_facts params silent prover timeout i n state goal
48796
0f94b8b69e79 consider removing chained facts last, so that they're more likely to be kept
blanchet
parents: 48399
diff changeset
   196
    val (chained, non_chained) = List.partition is_fact_chained facts
57054
blanchet
parents: 56985
diff changeset
   197
    (* Push chained facts to the back, so that they are less likely to be kicked out by the linear
blanchet
parents: 56985
diff changeset
   198
       minimization algorithm. *)
48796
0f94b8b69e79 consider removing chained facts last, so that they're more likely to be kept
blanchet
parents: 48399
diff changeset
   199
    val facts = non_chained @ chained
31236
2a1f5c87ac28 proper signature constraint;
wenzelm
parents: 31037
diff changeset
   200
  in
54815
4f6ec8754bf5 simplified data structure
blanchet
parents: 54813
diff changeset
   201
    (print silent (fn () => "Sledgehammer minimizer: " ^ quote prover_name ^ ".");
55202
824c48a539c9 renamed many Sledgehammer ML files to clarify structure
blanchet
parents: 55201
diff changeset
   202
     (case test timeout facts of
45371
blanchet
parents: 45370
diff changeset
   203
       result as {outcome = NONE, used_facts, run_time, ...} =>
38015
b30c3c2e1030 implemented "sublinear" minimization algorithm
blanchet
parents: 38002
diff changeset
   204
       let
48798
9152e66f98da be less aggressive at kicking out chained facts
blanchet
parents: 48796
diff changeset
   205
         val facts = filter_used_facts true used_facts facts
45372
cc455b2897f8 cascading timeouts in minimizer, part 2
blanchet
parents: 45371
diff changeset
   206
         val min =
54815
4f6ec8754bf5 simplified data structure
blanchet
parents: 54813
diff changeset
   207
           if length facts >= Config.get ctxt binary_min_facts then binary_minimize
4f6ec8754bf5 simplified data structure
blanchet
parents: 54813
diff changeset
   208
           else linear_minimize
57738
25d1495e6641 eliminated needlessly complex message tail
blanchet
parents: 57735
diff changeset
   209
         val (min_facts, {message, ...}) = min test (new_timeout timeout run_time) result facts
48321
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48314
diff changeset
   210
       in
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48314
diff changeset
   211
         print silent (fn () => cat_lines
57750
670cbec816b9 restored a bit of laziness
blanchet
parents: 57739
diff changeset
   212
           ["Minimized to " ^ n_facts (map fst min_facts)] ^
670cbec816b9 restored a bit of laziness
blanchet
parents: 57739
diff changeset
   213
            (case min_facts |> filter is_fact_chained |> length of
670cbec816b9 restored a bit of laziness
blanchet
parents: 57739
diff changeset
   214
              0 => ""
670cbec816b9 restored a bit of laziness
blanchet
parents: 57739
diff changeset
   215
            | n => "\n(including " ^ string_of_int n ^ " chained)") ^ ".");
54503
blanchet
parents: 54141
diff changeset
   216
         (if learn then do_learn (maps snd min_facts) else ());
57738
25d1495e6641 eliminated needlessly complex message tail
blanchet
parents: 57735
diff changeset
   217
         (SOME min_facts, message)
48321
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48314
diff changeset
   218
       end
57734
18bb3e1ff6f6 rationalized preplaying by eliminating (now superfluous) laziness
blanchet
parents: 57732
diff changeset
   219
     | {outcome = SOME TimedOut, ...} =>
57738
25d1495e6641 eliminated needlessly complex message tail
blanchet
parents: 57735
diff changeset
   220
       (NONE, fn _ =>
54816
10d48c2a3e32 made timeouts in Sledgehammer not be 'option's -- simplified lots of code
blanchet
parents: 54815
diff changeset
   221
          "Timeout: You can increase the time limit using the \"timeout\" option (e.g., \
57738
25d1495e6641 eliminated needlessly complex message tail
blanchet
parents: 57735
diff changeset
   222
          \timeout = " ^ string_of_int (10 + Time.toMilliseconds timeout div 1000) ^ "\").")
25d1495e6641 eliminated needlessly complex message tail
blanchet
parents: 57735
diff changeset
   223
     | {message, ...} => (NONE, (prefix "Prover error: " o message))))
25d1495e6641 eliminated needlessly complex message tail
blanchet
parents: 57735
diff changeset
   224
    handle ERROR msg => (NONE, fn _ => "Error: " ^ msg)
31236
2a1f5c87ac28 proper signature constraint;
wenzelm
parents: 31037
diff changeset
   225
  end
2a1f5c87ac28 proper signature constraint;
wenzelm
parents: 31037
diff changeset
   226
57732
e1b2442dc629 simplified minimization logic
blanchet
parents: 57723
diff changeset
   227
fun maybe_minimize mode do_learn name (params as {verbose, minimize, ...})
55205
8450622db0c5 refactor large ML file
blanchet
parents: 55202
diff changeset
   228
    ({state, goal, subgoal, subgoal_count, ...} : prover_problem)
57738
25d1495e6641 eliminated needlessly complex message tail
blanchet
parents: 57735
diff changeset
   229
    (result as {outcome, used_facts, used_from, preferred_methss, run_time, message}
57734
18bb3e1ff6f6 rationalized preplaying by eliminating (now superfluous) laziness
blanchet
parents: 57732
diff changeset
   230
     : prover_result) =
58494
ed380b9594b5 always minimize, to reinvoke the prover with nicer options and yield a nicer Isar proof (potentially -- cf. 'full_proof')
blanchet
parents: 58085
diff changeset
   231
  if is_some outcome then
48250
1065c307fafe further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents: 48085
diff changeset
   232
    result
1065c307fafe further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents: 48085
diff changeset
   233
  else
1065c307fafe further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents: 48085
diff changeset
   234
    let
57738
25d1495e6641 eliminated needlessly complex message tail
blanchet
parents: 57735
diff changeset
   235
      val (used_facts, message) =
48250
1065c307fafe further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents: 48085
diff changeset
   236
        if minimize then
57732
e1b2442dc629 simplified minimization logic
blanchet
parents: 57723
diff changeset
   237
          minimize_facts do_learn name params
54824
4e58a38b330b refactored preplaying outcome data structure
blanchet
parents: 54816
diff changeset
   238
            (not verbose orelse (mode <> Normal andalso mode <> MaSh)) subgoal subgoal_count state
57734
18bb3e1ff6f6 rationalized preplaying by eliminating (now superfluous) laziness
blanchet
parents: 57732
diff changeset
   239
            goal (filter_used_facts true used_facts (map (apsnd single) used_from))
48250
1065c307fafe further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents: 48085
diff changeset
   240
          |>> Option.map (map fst)
1065c307fafe further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents: 48085
diff changeset
   241
        else
57738
25d1495e6641 eliminated needlessly complex message tail
blanchet
parents: 57735
diff changeset
   242
          (SOME used_facts, message)
48250
1065c307fafe further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents: 48085
diff changeset
   243
    in
55202
824c48a539c9 renamed many Sledgehammer ML files to clarify structure
blanchet
parents: 55201
diff changeset
   244
      (case used_facts of
48250
1065c307fafe further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents: 48085
diff changeset
   245
        SOME used_facts =>
57781
c1ce4ef23be5 restored more sorting
blanchet
parents: 57776
diff changeset
   246
        {outcome = NONE, used_facts = sort_wrt fst used_facts, used_from = used_from,
57738
25d1495e6641 eliminated needlessly complex message tail
blanchet
parents: 57735
diff changeset
   247
         preferred_methss = preferred_methss, run_time = run_time, message = message}
55202
824c48a539c9 renamed many Sledgehammer ML files to clarify structure
blanchet
parents: 55201
diff changeset
   248
      | NONE => result)
48250
1065c307fafe further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents: 48085
diff changeset
   249
    end
1065c307fafe further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents: 48085
diff changeset
   250
57735
056a55b44ec7 eliminated Sledgehammer's "min" subcommand (and lots of complications in the code)
blanchet
parents: 57734
diff changeset
   251
fun get_minimizing_prover ctxt mode do_learn name params problem =
056a55b44ec7 eliminated Sledgehammer's "min" subcommand (and lots of complications in the code)
blanchet
parents: 57734
diff changeset
   252
  get_prover ctxt mode name params problem
57732
e1b2442dc629 simplified minimization logic
blanchet
parents: 57723
diff changeset
   253
  |> maybe_minimize mode do_learn name params problem
48250
1065c307fafe further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents: 48085
diff changeset
   254
35866
513074557e06 move the Sledgehammer Isar commands together into one file;
blanchet
parents: 35865
diff changeset
   255
end;