src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML
author haftmann
Thu, 08 Jul 2010 16:19:24 +0200
changeset 37744 3daaf23b9ab4
parent 37628 78334f400ae6
child 37926 e6ff246c0cdb
permissions -rw-r--r--
tuned titles
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
36375
2482446a604c move the minimizer to the Sledgehammer directory
blanchet
parents: 36370
diff changeset
     1
(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.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
35867
16279c4c7a33 move all ATP setup code into ATP_Wrapper
blanchet
parents: 35866
diff changeset
     5
Minimization of theorem list for Metis using automatic theorem 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
36375
2482446a604c move the minimizer to the Sledgehammer directory
blanchet
parents: 36370
diff changeset
     8
signature SLEDGEHAMMER_FACT_MINIMIZER =
32525
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32510
diff changeset
     9
sig
35969
c9565298df9e added support for Sledgehammer parameters;
blanchet
parents: 35867
diff changeset
    10
  type params = ATP_Manager.params
35867
16279c4c7a33 move all ATP setup code into ATP_Wrapper
blanchet
parents: 35866
diff changeset
    11
  type prover_result = ATP_Manager.prover_result
16279c4c7a33 move all ATP setup code into ATP_Wrapper
blanchet
parents: 35866
diff changeset
    12
35866
513074557e06 move the Sledgehammer Isar commands together into one file;
blanchet
parents: 35865
diff changeset
    13
  val minimize_theorems :
36481
af99c98121d6 make Sledgehammer more friendly if no subgoal is left
blanchet
parents: 36402
diff changeset
    14
    params -> int -> int -> Proof.state -> (string * thm list) list
35866
513074557e06 move the Sledgehammer Isar commands together into one file;
blanchet
parents: 35865
diff changeset
    15
    -> (string * thm list) list option * string
513074557e06 move the Sledgehammer Isar commands together into one file;
blanchet
parents: 35865
diff changeset
    16
end;
32525
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32510
diff changeset
    17
36375
2482446a604c move the minimizer to the Sledgehammer directory
blanchet
parents: 36370
diff changeset
    18
structure Sledgehammer_Fact_Minimizer : SLEDGEHAMMER_FACT_MINIMIZER =
31037
ac8669134e7a added Philipp Meyer's implementation of AtpMinimal
immler@in.tum.de
parents:
diff changeset
    19
struct
ac8669134e7a added Philipp Meyer's implementation of AtpMinimal
immler@in.tum.de
parents:
diff changeset
    20
37574
b8c1f4c46983 renamed "Sledgehammer_Fact_Preprocessor" to "Clausifier";
blanchet
parents: 37506
diff changeset
    21
open Clausifier
37578
9367cb36b1c4 renamed "Sledgehammer_FOL_Clauses" to "Metis_Clauses", so that Metis doesn't depend on Sledgehammer
blanchet
parents: 37577
diff changeset
    22
open Metis_Clauses
36142
f5e15e9aae10 make Sledgehammer "minimize" output less confusing + round up (not down) time limits to nearest second
blanchet
parents: 36063
diff changeset
    23
open Sledgehammer_Util
36063
cdc6855a6387 make Sledgehammer output "by" vs. "apply", "qed" vs. "next", and any necessary "prefer"
blanchet
parents: 35969
diff changeset
    24
open Sledgehammer_Proof_Reconstruct
35867
16279c4c7a33 move all ATP setup code into ATP_Wrapper
blanchet
parents: 35866
diff changeset
    25
open ATP_Manager
35866
513074557e06 move the Sledgehammer Isar commands together into one file;
blanchet
parents: 35865
diff changeset
    26
513074557e06 move the Sledgehammer Isar commands together into one file;
blanchet
parents: 35865
diff changeset
    27
(* Linear minimization algorithm *)
33492
4168294a9f96 Command atp_minimize uses the naive linear algorithm now
nipkow
parents: 33316
diff changeset
    28
36223
217ca1273786 make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents: 36143
diff changeset
    29
fun linear_minimize test s =
35866
513074557e06 move the Sledgehammer Isar commands together into one file;
blanchet
parents: 35865
diff changeset
    30
  let
36223
217ca1273786 make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents: 36143
diff changeset
    31
    fun aux [] p = p
217ca1273786 make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents: 36143
diff changeset
    32
      | aux (x :: xs) (needed, result) =
217ca1273786 make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents: 36143
diff changeset
    33
        case test (xs @ needed) of
217ca1273786 make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents: 36143
diff changeset
    34
          SOME result => aux xs (needed, result)
217ca1273786 make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents: 36143
diff changeset
    35
        | NONE => aux xs (x :: needed, result)
217ca1273786 make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents: 36143
diff changeset
    36
  in aux s end
31236
2a1f5c87ac28 proper signature constraint;
wenzelm
parents: 31037
diff changeset
    37
31037
ac8669134e7a added Philipp Meyer's implementation of AtpMinimal
immler@in.tum.de
parents:
diff changeset
    38
36370
a4f601daa175 centralized ATP-specific error handling in "atp_wrapper.ML"
blanchet
parents: 36369
diff changeset
    39
(* wrapper for calling external prover *)
31236
2a1f5c87ac28 proper signature constraint;
wenzelm
parents: 31037
diff changeset
    40
36370
a4f601daa175 centralized ATP-specific error handling in "atp_wrapper.ML"
blanchet
parents: 36369
diff changeset
    41
fun string_for_failure Unprovable = "Unprovable."
37418
c02bd0bb276d missing case
blanchet
parents: 36924
diff changeset
    42
  | string_for_failure IncompleteUnprovable = "Failed."
36370
a4f601daa175 centralized ATP-specific error handling in "atp_wrapper.ML"
blanchet
parents: 36369
diff changeset
    43
  | string_for_failure TimedOut = "Timed out."
a4f601daa175 centralized ATP-specific error handling in "atp_wrapper.ML"
blanchet
parents: 36369
diff changeset
    44
  | string_for_failure OutOfResources = "Failed."
a4f601daa175 centralized ATP-specific error handling in "atp_wrapper.ML"
blanchet
parents: 36369
diff changeset
    45
  | string_for_failure OldSpass = "Error."
a4f601daa175 centralized ATP-specific error handling in "atp_wrapper.ML"
blanchet
parents: 36369
diff changeset
    46
  | string_for_failure MalformedOutput = "Error."
a4f601daa175 centralized ATP-specific error handling in "atp_wrapper.ML"
blanchet
parents: 36369
diff changeset
    47
  | string_for_failure UnknownError = "Failed."
a4f601daa175 centralized ATP-specific error handling in "atp_wrapper.ML"
blanchet
parents: 36369
diff changeset
    48
fun string_for_outcome NONE = "Success."
a4f601daa175 centralized ATP-specific error handling in "atp_wrapper.ML"
blanchet
parents: 36369
diff changeset
    49
  | string_for_outcome (SOME failure) = string_for_failure failure
31236
2a1f5c87ac28 proper signature constraint;
wenzelm
parents: 31037
diff changeset
    50
37498
b426cbdb5a23 removed Sledgehammer's support for the DFG syntax;
blanchet
parents: 37479
diff changeset
    51
fun sledgehammer_test_theorems (params : params) prover timeout subgoal state
b426cbdb5a23 removed Sledgehammer's support for the DFG syntax;
blanchet
parents: 37479
diff changeset
    52
                               filtered_clauses name_thms_pairs =
31236
2a1f5c87ac28 proper signature constraint;
wenzelm
parents: 31037
diff changeset
    53
  let
37628
78334f400ae6 Sledgehammer can save some msecs by cheating
blanchet
parents: 37578
diff changeset
    54
    val thy = Proof.theory_of state
36142
f5e15e9aae10 make Sledgehammer "minimize" output less confusing + round up (not down) time limits to nearest second
blanchet
parents: 36063
diff changeset
    55
    val num_theorems = length name_thms_pairs
f5e15e9aae10 make Sledgehammer "minimize" output less confusing + round up (not down) time limits to nearest second
blanchet
parents: 36063
diff changeset
    56
    val _ = priority ("Testing " ^ string_of_int num_theorems ^
f5e15e9aae10 make Sledgehammer "minimize" output less confusing + round up (not down) time limits to nearest second
blanchet
parents: 36063
diff changeset
    57
                      " theorem" ^ plural_s num_theorems ^ "...")
32525
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32510
diff changeset
    58
    val name_thm_pairs = maps (fn (n, ths) => map (pair n) ths) name_thms_pairs
37628
78334f400ae6 Sledgehammer can save some msecs by cheating
blanchet
parents: 37578
diff changeset
    59
    val axclauses = cnf_rules_pairs thy true name_thm_pairs
36263
56bf63d70120 use "Proof.goal" in Sledgehammer's minimizer (just like everywhere else in Sledgehammer), not "Proof.raw_goal"
blanchet
parents: 36232
diff changeset
    60
    val {context = ctxt, facts, goal} = Proof.goal state
32941
72d48e333b77 eliminated extraneous wrapping of public records;
wenzelm
parents: 32937
diff changeset
    61
    val problem =
36063
cdc6855a6387 make Sledgehammer output "by" vs. "apply", "qed" vs. "next", and any necessary "prefer"
blanchet
parents: 35969
diff changeset
    62
     {subgoal = subgoal, goal = (ctxt, (facts, goal)),
35969
c9565298df9e added support for Sledgehammer parameters;
blanchet
parents: 35867
diff changeset
    63
      relevance_override = {add = [], del = [], only = false},
36232
4d425766a47f don't redo an axiom selection in the first round of Sledgehammer "minimize"!;
blanchet
parents: 36231
diff changeset
    64
      axiom_clauses = SOME axclauses,
4d425766a47f don't redo an axiom selection in the first round of Sledgehammer "minimize"!;
blanchet
parents: 36231
diff changeset
    65
      filtered_clauses = SOME (the_default axclauses filtered_clauses)}
36223
217ca1273786 make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents: 36143
diff changeset
    66
  in
36370
a4f601daa175 centralized ATP-specific error handling in "atp_wrapper.ML"
blanchet
parents: 36369
diff changeset
    67
    prover params (K "") timeout problem
36607
e5f7235f39c5 made sml/nj happy about Sledgehammer and Nitpick (cf. 6f11c9b1fb3e, 3c2438efe224)
krauss
parents: 36488
diff changeset
    68
    |> tap (fn result : prover_result =>
e5f7235f39c5 made sml/nj happy about Sledgehammer and Nitpick (cf. 6f11c9b1fb3e, 3c2438efe224)
krauss
parents: 36488
diff changeset
    69
         priority (string_for_outcome (#outcome result)))
36223
217ca1273786 make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents: 36143
diff changeset
    70
  end
31236
2a1f5c87ac28 proper signature constraint;
wenzelm
parents: 31037
diff changeset
    71
2a1f5c87ac28 proper signature constraint;
wenzelm
parents: 31037
diff changeset
    72
(* minimalization of thms *)
2a1f5c87ac28 proper signature constraint;
wenzelm
parents: 31037
diff changeset
    73
36909
7d5587f6d5f7 made Sledgehammer's full-typed proof reconstruction work for the first time;
blanchet
parents: 36607
diff changeset
    74
fun minimize_theorems (params as {debug, atps, full_types, minimize_timeout,
36924
ff01d3ae9ad4 renamed options
blanchet
parents: 36909
diff changeset
    75
                                  isar_proof, isar_shrink_factor, ...})
36481
af99c98121d6 make Sledgehammer more friendly if no subgoal is left
blanchet
parents: 36402
diff changeset
    76
                      i n state name_thms_pairs =
31236
2a1f5c87ac28 proper signature constraint;
wenzelm
parents: 31037
diff changeset
    77
  let
36378
f32c567dbcaa remove some bloat
blanchet
parents: 36375
diff changeset
    78
    val thy = Proof.theory_of state
f32c567dbcaa remove some bloat
blanchet
parents: 36375
diff changeset
    79
    val prover = case atps of
f32c567dbcaa remove some bloat
blanchet
parents: 36375
diff changeset
    80
                   [atp_name] => get_prover thy atp_name
f32c567dbcaa remove some bloat
blanchet
parents: 36375
diff changeset
    81
                 | _ => error "Expected a single ATP."
35969
c9565298df9e added support for Sledgehammer parameters;
blanchet
parents: 35867
diff changeset
    82
    val msecs = Time.toMilliseconds minimize_timeout
31236
2a1f5c87ac28 proper signature constraint;
wenzelm
parents: 31037
diff changeset
    83
    val _ =
36378
f32c567dbcaa remove some bloat
blanchet
parents: 36375
diff changeset
    84
      priority ("Sledgehammer minimizer: ATP " ^ quote (the_single atps) ^
36224
109dce8410d5 cosmetics
blanchet
parents: 36223
diff changeset
    85
                " with a time limit of " ^ string_of_int msecs ^ " ms.")
35969
c9565298df9e added support for Sledgehammer parameters;
blanchet
parents: 35867
diff changeset
    86
    val test_thms_fun =
36063
cdc6855a6387 make Sledgehammer output "by" vs. "apply", "qed" vs. "next", and any necessary "prefer"
blanchet
parents: 35969
diff changeset
    87
      sledgehammer_test_theorems params prover minimize_timeout i state
31752
19a5f1c8a844 use results of relevance-filter to determine additional clauses;
immler@in.tum.de
parents: 31409
diff changeset
    88
    fun test_thms filtered thms =
36223
217ca1273786 make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents: 36143
diff changeset
    89
      case test_thms_fun filtered thms of
36370
a4f601daa175 centralized ATP-specific error handling in "atp_wrapper.ML"
blanchet
parents: 36369
diff changeset
    90
        (result as {outcome = NONE, ...}) => SOME result
36223
217ca1273786 make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents: 36143
diff changeset
    91
      | _ => NONE
217ca1273786 make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents: 36143
diff changeset
    92
37498
b426cbdb5a23 removed Sledgehammer's support for the DFG syntax;
blanchet
parents: 37479
diff changeset
    93
    val {context = ctxt, goal, ...} = Proof.goal state;
31236
2a1f5c87ac28 proper signature constraint;
wenzelm
parents: 31037
diff changeset
    94
  in
2a1f5c87ac28 proper signature constraint;
wenzelm
parents: 31037
diff changeset
    95
    (* try prove first to check result and get used theorems *)
31409
d8537ba165b5 split preparing clauses and writing problemfile;
immler@in.tum.de
parents: 31236
diff changeset
    96
    (case test_thms_fun NONE name_thms_pairs of
36402
1b20805974c7 introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents: 36393
diff changeset
    97
      result as {outcome = NONE, pool, internal_thm_names, conjecture_shape,
1b20805974c7 introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents: 36393
diff changeset
    98
                 filtered_clauses, ...} =>
31236
2a1f5c87ac28 proper signature constraint;
wenzelm
parents: 31037
diff changeset
    99
        let
36223
217ca1273786 make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents: 36143
diff changeset
   100
          val used = internal_thm_names |> Vector.foldr (op ::) []
217ca1273786 make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents: 36143
diff changeset
   101
                                        |> sort_distinct string_ord
31236
2a1f5c87ac28 proper signature constraint;
wenzelm
parents: 31037
diff changeset
   102
          val to_use =
36223
217ca1273786 make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents: 36143
diff changeset
   103
            if length used < length name_thms_pairs then
36393
be73a2b2443b support readable names even when Isar proof reconstruction is enabled -- useful for debugging
blanchet
parents: 36382
diff changeset
   104
              filter (fn (name1, _) => exists (curry (op =) name1) used)
36223
217ca1273786 make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents: 36143
diff changeset
   105
                     name_thms_pairs
33305
wenzelm
parents: 33292
diff changeset
   106
            else name_thms_pairs
36231
bede2d49ba3b get rid of "conjecture_pos", which is no longer necessary now that it's Metis's job, not Sledgehammer's, to report inconsistent contexts
blanchet
parents: 36224
diff changeset
   107
          val (min_thms, {proof, internal_thm_names, ...}) =
36223
217ca1273786 make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents: 36143
diff changeset
   108
            linear_minimize (test_thms (SOME filtered_clauses)) to_use
217ca1273786 make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents: 36143
diff changeset
   109
                            ([], result)
36481
af99c98121d6 make Sledgehammer more friendly if no subgoal is left
blanchet
parents: 36402
diff changeset
   110
          val m = length min_thms
32947
3c19b98a35cd ATP_Manager.get_prover: canonical argument order;
wenzelm
parents: 32942
diff changeset
   111
          val _ = priority (cat_lines
36481
af99c98121d6 make Sledgehammer more friendly if no subgoal is left
blanchet
parents: 36402
diff changeset
   112
            ["Minimized: " ^ string_of_int m ^ " theorem" ^ plural_s m] ^ ".")
36223
217ca1273786 make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents: 36143
diff changeset
   113
        in
217ca1273786 make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents: 36143
diff changeset
   114
          (SOME min_thms,
36402
1b20805974c7 introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents: 36393
diff changeset
   115
           proof_text isar_proof
37479
f6b1ee5b420b try to improve Sledgehammer/Metis's behavior in full_types mode, e.g. by handing True, False, and If better
blanchet
parents: 37418
diff changeset
   116
               (pool, debug, isar_shrink_factor, ctxt, conjecture_shape)
f6b1ee5b420b try to improve Sledgehammer/Metis's behavior in full_types mode, e.g. by handing True, False, and If better
blanchet
parents: 37418
diff changeset
   117
               (full_types, K "", proof, internal_thm_names, goal, i) |> fst)
36223
217ca1273786 make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents: 36143
diff changeset
   118
        end
36370
a4f601daa175 centralized ATP-specific error handling in "atp_wrapper.ML"
blanchet
parents: 36369
diff changeset
   119
    | {outcome = SOME TimedOut, ...} =>
36142
f5e15e9aae10 make Sledgehammer "minimize" output less confusing + round up (not down) time limits to nearest second
blanchet
parents: 36063
diff changeset
   120
        (NONE, "Timeout: You can increase the time limit using the \"timeout\" \
f5e15e9aae10 make Sledgehammer "minimize" output less confusing + round up (not down) time limits to nearest second
blanchet
parents: 36063
diff changeset
   121
               \option (e.g., \"timeout = " ^
f5e15e9aae10 make Sledgehammer "minimize" output less confusing + round up (not down) time limits to nearest second
blanchet
parents: 36063
diff changeset
   122
               string_of_int (10 + msecs div 1000) ^ " s\").")
36370
a4f601daa175 centralized ATP-specific error handling in "atp_wrapper.ML"
blanchet
parents: 36369
diff changeset
   123
    | {outcome = SOME UnknownError, ...} =>
36142
f5e15e9aae10 make Sledgehammer "minimize" output less confusing + round up (not down) time limits to nearest second
blanchet
parents: 36063
diff changeset
   124
        (* Failure sometimes mean timeout, unfortunately. *)
f5e15e9aae10 make Sledgehammer "minimize" output less confusing + round up (not down) time limits to nearest second
blanchet
parents: 36063
diff changeset
   125
        (NONE, "Failure: No proof was found with the current time limit. You \
f5e15e9aae10 make Sledgehammer "minimize" output less confusing + round up (not down) time limits to nearest second
blanchet
parents: 36063
diff changeset
   126
               \can increase the time limit using the \"timeout\" \
f5e15e9aae10 make Sledgehammer "minimize" output less confusing + round up (not down) time limits to nearest second
blanchet
parents: 36063
diff changeset
   127
               \option (e.g., \"timeout = " ^
36370
a4f601daa175 centralized ATP-specific error handling in "atp_wrapper.ML"
blanchet
parents: 36369
diff changeset
   128
               string_of_int (10 + msecs div 1000) ^ " s\").")
a4f601daa175 centralized ATP-specific error handling in "atp_wrapper.ML"
blanchet
parents: 36369
diff changeset
   129
    | {message, ...} => (NONE, "ATP error: " ^ message))
37506
32a1ee39c49b missing "Unsynchronized" + make exception take a unit
blanchet
parents: 37498
diff changeset
   130
    handle TRIVIAL () => (SOME [], metis_line full_types i n [])
36382
b90fc0d75bca cosmetics
blanchet
parents: 36378
diff changeset
   131
         | ERROR msg => (NONE, "Error: " ^ msg)
31236
2a1f5c87ac28 proper signature constraint;
wenzelm
parents: 31037
diff changeset
   132
  end
2a1f5c87ac28 proper signature constraint;
wenzelm
parents: 31037
diff changeset
   133
35866
513074557e06 move the Sledgehammer Isar commands together into one file;
blanchet
parents: 35865
diff changeset
   134
end;