src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
author blanchet
Tue, 21 Dec 2010 06:53:20 +0100
changeset 41338 ffd730fcf0ac
parent 41337 263fe1670067
child 41357 ae76960d86a2
permissions -rw-r--r--
avoid weird symbols in path
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
32564
378528d2f7eb standard headers and text sections;
wenzelm
parents: 32551
diff changeset
     1
(*  Title:      HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
378528d2f7eb standard headers and text sections;
wenzelm
parents: 32551
diff changeset
     2
    Author:     Jasmin Blanchette and Sascha Boehme and Tobias Nipkow, TU Munich
32385
594890623c46 split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff changeset
     3
*)
594890623c46 split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff changeset
     4
594890623c46 split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff changeset
     5
structure Mirabelle_Sledgehammer : MIRABELLE_ACTION =
594890623c46 split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff changeset
     6
struct
594890623c46 split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff changeset
     7
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
     8
val proverK = "prover"
32541
cea1716eb106 timeout option for ATPs
boehmes
parents: 32536
diff changeset
     9
val prover_timeoutK = "prover_timeout"
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    10
val keepK = "keep"
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    11
val full_typesK = "full_types"
41155
85da8cbb4966 added support for "type_sys" option to Mirabelle
blanchet
parents: 41154
diff changeset
    12
val type_sysK = "type_sys"
32525
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
    13
val minimizeK = "minimize"
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
    14
val minimize_timeoutK = "minimize_timeout"
34035
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
    15
val metis_ftK = "metis_ft"
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    16
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    17
fun sh_tag id = "#" ^ string_of_int id ^ " sledgehammer: "
32525
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
    18
fun minimize_tag id = "#" ^ string_of_int id ^ " minimize (sledgehammer): "
40667
b8579f24ce67 make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents: 40627
diff changeset
    19
fun reconstructor_tag reconstructor id =
b8579f24ce67 make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents: 40627
diff changeset
    20
  "#" ^ string_of_int id ^ " " ^ (!reconstructor) ^ " (sledgehammer): "
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    21
32525
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
    22
val separator = "-----"
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
    23
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    24
32549
338ccfd37f67 minimization: comparing w/ and w/o.
nipkow
parents: 32541
diff changeset
    25
datatype sh_data = ShData of {
338ccfd37f67 minimization: comparing w/ and w/o.
nipkow
parents: 32541
diff changeset
    26
  calls: int,
338ccfd37f67 minimization: comparing w/ and w/o.
nipkow
parents: 32541
diff changeset
    27
  success: int,
39337
ffa577c0bbfa keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents: 39321
diff changeset
    28
  nontriv_calls: int,
ffa577c0bbfa keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents: 39321
diff changeset
    29
  nontriv_success: int,
32585
e788b33dd2b4 revised lemma counting
nipkow
parents: 32574
diff changeset
    30
  lemmas: int,
32818
6c91e668b15e record max lemmas used
nipkow
parents: 32676
diff changeset
    31
  max_lems: int,
32549
338ccfd37f67 minimization: comparing w/ and w/o.
nipkow
parents: 32541
diff changeset
    32
  time_isa: int,
40062
cfaebaa8588f make Sledgehammer minimizer fully work with SMT
blanchet
parents: 40061
diff changeset
    33
  time_prover: int,
cfaebaa8588f make Sledgehammer minimizer fully work with SMT
blanchet
parents: 40061
diff changeset
    34
  time_prover_fail: int}
32549
338ccfd37f67 minimization: comparing w/ and w/o.
nipkow
parents: 32541
diff changeset
    35
40667
b8579f24ce67 make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents: 40627
diff changeset
    36
datatype re_data = ReData of {
32549
338ccfd37f67 minimization: comparing w/ and w/o.
nipkow
parents: 32541
diff changeset
    37
  calls: int,
338ccfd37f67 minimization: comparing w/ and w/o.
nipkow
parents: 32541
diff changeset
    38
  success: int,
39337
ffa577c0bbfa keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents: 39321
diff changeset
    39
  nontriv_calls: int,
ffa577c0bbfa keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents: 39321
diff changeset
    40
  nontriv_success: int,
32676
b1c85a117dec record how many "proof"s are solved by s/h
nipkow
parents: 32612
diff changeset
    41
  proofs: int,
32549
338ccfd37f67 minimization: comparing w/ and w/o.
nipkow
parents: 32541
diff changeset
    42
  time: int,
32550
d57c7a2d927c logging number of metis lemmas
nipkow
parents: 32549
diff changeset
    43
  timeout: int,
32990
717680b14041 added sums of squares for standard deviation
nipkow
parents: 32868
diff changeset
    44
  lemmas: int * int * int,
39341
d2b981a0429a indicate triviality in the list of proved things
blanchet
parents: 39340
diff changeset
    45
  posns: (Position.T * bool) list
32550
d57c7a2d927c logging number of metis lemmas
nipkow
parents: 32549
diff changeset
    46
  }
32549
338ccfd37f67 minimization: comparing w/ and w/o.
nipkow
parents: 32541
diff changeset
    47
32571
d4bb776874b8 count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents: 32567
diff changeset
    48
datatype min_data = MinData of {
32609
2f3e7a92b522 modified minimization log
nipkow
parents: 32607
diff changeset
    49
  succs: int,
35866
513074557e06 move the Sledgehammer Isar commands together into one file;
blanchet
parents: 35830
diff changeset
    50
  ab_ratios: int
32571
d4bb776874b8 count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents: 32567
diff changeset
    51
  }
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    52
32818
6c91e668b15e record max lemmas used
nipkow
parents: 32676
diff changeset
    53
fun make_sh_data
39337
ffa577c0bbfa keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents: 39321
diff changeset
    54
      (calls,success,nontriv_calls,nontriv_success,lemmas,max_lems,time_isa,
40062
cfaebaa8588f make Sledgehammer minimizer fully work with SMT
blanchet
parents: 40061
diff changeset
    55
       time_prover,time_prover_fail) =
39337
ffa577c0bbfa keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents: 39321
diff changeset
    56
  ShData{calls=calls, success=success, nontriv_calls=nontriv_calls,
ffa577c0bbfa keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents: 39321
diff changeset
    57
         nontriv_success=nontriv_success, lemmas=lemmas, max_lems=max_lems,
40062
cfaebaa8588f make Sledgehammer minimizer fully work with SMT
blanchet
parents: 40061
diff changeset
    58
         time_isa=time_isa, time_prover=time_prover,
cfaebaa8588f make Sledgehammer minimizer fully work with SMT
blanchet
parents: 40061
diff changeset
    59
         time_prover_fail=time_prover_fail}
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    60
35866
513074557e06 move the Sledgehammer Isar commands together into one file;
blanchet
parents: 35830
diff changeset
    61
fun make_min_data (succs, ab_ratios) =
513074557e06 move the Sledgehammer Isar commands together into one file;
blanchet
parents: 35830
diff changeset
    62
  MinData{succs=succs, ab_ratios=ab_ratios}
32571
d4bb776874b8 count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents: 32567
diff changeset
    63
40667
b8579f24ce67 make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents: 40627
diff changeset
    64
fun make_re_data (calls,success,nontriv_calls,nontriv_success,proofs,time,
39337
ffa577c0bbfa keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents: 39321
diff changeset
    65
                  timeout,lemmas,posns) =
40667
b8579f24ce67 make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents: 40627
diff changeset
    66
  ReData{calls=calls, success=success, nontriv_calls=nontriv_calls,
39337
ffa577c0bbfa keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents: 39321
diff changeset
    67
         nontriv_success=nontriv_success, proofs=proofs, time=time,
32990
717680b14041 added sums of squares for standard deviation
nipkow
parents: 32868
diff changeset
    68
         timeout=timeout, lemmas=lemmas, posns=posns}
32549
338ccfd37f67 minimization: comparing w/ and w/o.
nipkow
parents: 32541
diff changeset
    69
39337
ffa577c0bbfa keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents: 39321
diff changeset
    70
val empty_sh_data = make_sh_data (0, 0, 0, 0, 0, 0, 0, 0, 0)
35871
c93bda4fdf15 remove the iteration counter from Sledgehammer's minimizer
blanchet
parents: 35867
diff changeset
    71
val empty_min_data = make_min_data (0, 0)
40667
b8579f24ce67 make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents: 40627
diff changeset
    72
val empty_re_data = make_re_data (0, 0, 0, 0, 0, 0, 0, (0,0,0), [])
34035
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
    73
39337
ffa577c0bbfa keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents: 39321
diff changeset
    74
fun tuple_of_sh_data (ShData {calls, success, nontriv_calls, nontriv_success,
ffa577c0bbfa keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents: 39321
diff changeset
    75
                              lemmas, max_lems, time_isa,
40062
cfaebaa8588f make Sledgehammer minimizer fully work with SMT
blanchet
parents: 40061
diff changeset
    76
  time_prover, time_prover_fail}) = (calls, success, nontriv_calls,
cfaebaa8588f make Sledgehammer minimizer fully work with SMT
blanchet
parents: 40061
diff changeset
    77
  nontriv_success, lemmas, max_lems, time_isa, time_prover, time_prover_fail)
34035
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
    78
35866
513074557e06 move the Sledgehammer Isar commands together into one file;
blanchet
parents: 35830
diff changeset
    79
fun tuple_of_min_data (MinData {succs, ab_ratios}) = (succs, ab_ratios)
34035
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
    80
40667
b8579f24ce67 make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents: 40627
diff changeset
    81
fun tuple_of_re_data (ReData {calls, success, nontriv_calls, nontriv_success,
39337
ffa577c0bbfa keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents: 39321
diff changeset
    82
  proofs, time, timeout, lemmas, posns}) = (calls, success, nontriv_calls,
ffa577c0bbfa keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents: 39321
diff changeset
    83
  nontriv_success, proofs, time, timeout, lemmas, posns)
34035
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
    84
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
    85
40667
b8579f24ce67 make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents: 40627
diff changeset
    86
datatype reconstructor_mode =
b8579f24ce67 make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents: 40627
diff changeset
    87
  Unminimized | Minimized | UnminimizedFT | MinimizedFT
34035
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
    88
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
    89
datatype data = Data of {
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
    90
  sh: sh_data,
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
    91
  min: min_data,
40667
b8579f24ce67 make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents: 40627
diff changeset
    92
  re_u: re_data, (* reconstructor with unminimized set of lemmas *)
b8579f24ce67 make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents: 40627
diff changeset
    93
  re_m: re_data, (* reconstructor with minimized set of lemmas *)
b8579f24ce67 make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents: 40627
diff changeset
    94
  re_uft: re_data, (* reconstructor with unminimized set of lemmas and fully-typed *)
b8579f24ce67 make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents: 40627
diff changeset
    95
  re_mft: re_data, (* reconstructor with minimized set of lemmas and fully-typed *)
34035
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
    96
  mini: bool   (* with minimization *)
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
    97
  }
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    98
40667
b8579f24ce67 make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents: 40627
diff changeset
    99
fun make_data (sh, min, re_u, re_m, re_uft, re_mft, mini) =
b8579f24ce67 make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents: 40627
diff changeset
   100
  Data {sh=sh, min=min, re_u=re_u, re_m=re_m, re_uft=re_uft, re_mft=re_mft,
34035
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   101
    mini=mini}
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   102
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   103
val empty_data = make_data (empty_sh_data, empty_min_data,
40667
b8579f24ce67 make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents: 40627
diff changeset
   104
  empty_re_data, empty_re_data, empty_re_data, empty_re_data, false)
34035
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   105
40667
b8579f24ce67 make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents: 40627
diff changeset
   106
fun map_sh_data f (Data {sh, min, re_u, re_m, re_uft, re_mft, mini}) =
34035
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   107
  let val sh' = make_sh_data (f (tuple_of_sh_data sh))
40667
b8579f24ce67 make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents: 40627
diff changeset
   108
  in make_data (sh', min, re_u, re_m, re_uft, re_mft, mini) end
34035
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   109
40667
b8579f24ce67 make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents: 40627
diff changeset
   110
fun map_min_data f (Data {sh, min, re_u, re_m, re_uft, re_mft, mini}) =
34035
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   111
  let val min' = make_min_data (f (tuple_of_min_data min))
40667
b8579f24ce67 make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents: 40627
diff changeset
   112
  in make_data (sh, min', re_u, re_m, re_uft, re_mft, mini) end
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   113
40667
b8579f24ce67 make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents: 40627
diff changeset
   114
fun map_re_data f m (Data {sh, min, re_u, re_m, re_uft, re_mft, mini}) =
34035
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   115
  let
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   116
    fun map_me g Unminimized   (u, m, uft, mft) = (g u, m, uft, mft)
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   117
      | map_me g Minimized     (u, m, uft, mft) = (u, g m, uft, mft)
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   118
      | map_me g UnminimizedFT (u, m, uft, mft) = (u, m, g uft, mft)
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   119
      | map_me g MinimizedFT   (u, m, uft, mft) = (u, m, uft, g mft)
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   120
40667
b8579f24ce67 make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents: 40627
diff changeset
   121
    val f' = make_re_data o f o tuple_of_re_data
32571
d4bb776874b8 count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents: 32567
diff changeset
   122
40667
b8579f24ce67 make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents: 40627
diff changeset
   123
    val (re_u', re_m', re_uft', re_mft') =
b8579f24ce67 make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents: 40627
diff changeset
   124
      map_me f' m (re_u, re_m, re_uft, re_mft)
b8579f24ce67 make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents: 40627
diff changeset
   125
  in make_data (sh, min, re_u', re_m', re_uft', re_mft', mini) end
34035
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   126
40667
b8579f24ce67 make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents: 40627
diff changeset
   127
fun set_mini mini (Data {sh, min, re_u, re_m, re_uft, re_mft, ...}) =
b8579f24ce67 make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents: 40627
diff changeset
   128
  make_data (sh, min, re_u, re_m, re_uft, re_mft, mini)
32990
717680b14041 added sums of squares for standard deviation
nipkow
parents: 32868
diff changeset
   129
717680b14041 added sums of squares for standard deviation
nipkow
parents: 32868
diff changeset
   130
fun inc_max (n:int) (s,sos,m) = (s+n, sos + n*n, Int.max(m,n));
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   131
32818
6c91e668b15e record max lemmas used
nipkow
parents: 32676
diff changeset
   132
val inc_sh_calls =  map_sh_data
40062
cfaebaa8588f make Sledgehammer minimizer fully work with SMT
blanchet
parents: 40061
diff changeset
   133
  (fn (calls, success, nontriv_calls, nontriv_success, lemmas,max_lems, time_isa, time_prover, time_prover_fail)
cfaebaa8588f make Sledgehammer minimizer fully work with SMT
blanchet
parents: 40061
diff changeset
   134
    => (calls + 1, success, nontriv_calls, nontriv_success, lemmas, max_lems, time_isa, time_prover, time_prover_fail))
32549
338ccfd37f67 minimization: comparing w/ and w/o.
nipkow
parents: 32541
diff changeset
   135
32818
6c91e668b15e record max lemmas used
nipkow
parents: 32676
diff changeset
   136
val inc_sh_success = map_sh_data
40062
cfaebaa8588f make Sledgehammer minimizer fully work with SMT
blanchet
parents: 40061
diff changeset
   137
  (fn (calls, success, nontriv_calls, nontriv_success, lemmas,max_lems, time_isa, time_prover, time_prover_fail)
cfaebaa8588f make Sledgehammer minimizer fully work with SMT
blanchet
parents: 40061
diff changeset
   138
    => (calls, success + 1, nontriv_calls, nontriv_success, lemmas,max_lems, time_isa, time_prover, time_prover_fail))
39337
ffa577c0bbfa keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents: 39321
diff changeset
   139
ffa577c0bbfa keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents: 39321
diff changeset
   140
val inc_sh_nontriv_calls =  map_sh_data
40062
cfaebaa8588f make Sledgehammer minimizer fully work with SMT
blanchet
parents: 40061
diff changeset
   141
  (fn (calls, success, nontriv_calls, nontriv_success, lemmas,max_lems, time_isa, time_prover, time_prover_fail)
cfaebaa8588f make Sledgehammer minimizer fully work with SMT
blanchet
parents: 40061
diff changeset
   142
    => (calls, success, nontriv_calls + 1, nontriv_success, lemmas, max_lems, time_isa, time_prover, time_prover_fail))
39337
ffa577c0bbfa keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents: 39321
diff changeset
   143
ffa577c0bbfa keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents: 39321
diff changeset
   144
val inc_sh_nontriv_success = map_sh_data
40062
cfaebaa8588f make Sledgehammer minimizer fully work with SMT
blanchet
parents: 40061
diff changeset
   145
  (fn (calls, success, nontriv_calls, nontriv_success, lemmas,max_lems, time_isa, time_prover, time_prover_fail)
cfaebaa8588f make Sledgehammer minimizer fully work with SMT
blanchet
parents: 40061
diff changeset
   146
    => (calls, success, nontriv_calls, nontriv_success + 1, lemmas,max_lems, time_isa, time_prover, time_prover_fail))
32585
e788b33dd2b4 revised lemma counting
nipkow
parents: 32574
diff changeset
   147
32818
6c91e668b15e record max lemmas used
nipkow
parents: 32676
diff changeset
   148
fun inc_sh_lemmas n = map_sh_data
40062
cfaebaa8588f make Sledgehammer minimizer fully work with SMT
blanchet
parents: 40061
diff changeset
   149
  (fn (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_prover,time_prover_fail)
cfaebaa8588f make Sledgehammer minimizer fully work with SMT
blanchet
parents: 40061
diff changeset
   150
    => (calls,success,nontriv_calls, nontriv_success, lemmas+n,max_lems,time_isa,time_prover,time_prover_fail))
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   151
32818
6c91e668b15e record max lemmas used
nipkow
parents: 32676
diff changeset
   152
fun inc_sh_max_lems n = map_sh_data
40062
cfaebaa8588f make Sledgehammer minimizer fully work with SMT
blanchet
parents: 40061
diff changeset
   153
  (fn (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_prover,time_prover_fail)
cfaebaa8588f make Sledgehammer minimizer fully work with SMT
blanchet
parents: 40061
diff changeset
   154
    => (calls,success,nontriv_calls, nontriv_success, lemmas,Int.max(max_lems,n),time_isa,time_prover,time_prover_fail))
32549
338ccfd37f67 minimization: comparing w/ and w/o.
nipkow
parents: 32541
diff changeset
   155
32818
6c91e668b15e record max lemmas used
nipkow
parents: 32676
diff changeset
   156
fun inc_sh_time_isa t = map_sh_data
40062
cfaebaa8588f make Sledgehammer minimizer fully work with SMT
blanchet
parents: 40061
diff changeset
   157
  (fn (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_prover,time_prover_fail)
cfaebaa8588f make Sledgehammer minimizer fully work with SMT
blanchet
parents: 40061
diff changeset
   158
    => (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa + t,time_prover,time_prover_fail))
32818
6c91e668b15e record max lemmas used
nipkow
parents: 32676
diff changeset
   159
40062
cfaebaa8588f make Sledgehammer minimizer fully work with SMT
blanchet
parents: 40061
diff changeset
   160
fun inc_sh_time_prover t = map_sh_data
cfaebaa8588f make Sledgehammer minimizer fully work with SMT
blanchet
parents: 40061
diff changeset
   161
  (fn (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_prover,time_prover_fail)
cfaebaa8588f make Sledgehammer minimizer fully work with SMT
blanchet
parents: 40061
diff changeset
   162
    => (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_prover + t,time_prover_fail))
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   163
40062
cfaebaa8588f make Sledgehammer minimizer fully work with SMT
blanchet
parents: 40061
diff changeset
   164
fun inc_sh_time_prover_fail t = map_sh_data
cfaebaa8588f make Sledgehammer minimizer fully work with SMT
blanchet
parents: 40061
diff changeset
   165
  (fn (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_prover,time_prover_fail)
cfaebaa8588f make Sledgehammer minimizer fully work with SMT
blanchet
parents: 40061
diff changeset
   166
    => (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_prover,time_prover_fail + t))
32571
d4bb776874b8 count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents: 32567
diff changeset
   167
32818
6c91e668b15e record max lemmas used
nipkow
parents: 32676
diff changeset
   168
val inc_min_succs = map_min_data
35866
513074557e06 move the Sledgehammer Isar commands together into one file;
blanchet
parents: 35830
diff changeset
   169
  (fn (succs,ab_ratios) => (succs+1, ab_ratios))
32571
d4bb776874b8 count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents: 32567
diff changeset
   170
32818
6c91e668b15e record max lemmas used
nipkow
parents: 32676
diff changeset
   171
fun inc_min_ab_ratios r = map_min_data
35866
513074557e06 move the Sledgehammer Isar commands together into one file;
blanchet
parents: 35830
diff changeset
   172
  (fn (succs, ab_ratios) => (succs, ab_ratios+r))
32549
338ccfd37f67 minimization: comparing w/ and w/o.
nipkow
parents: 32541
diff changeset
   173
40667
b8579f24ce67 make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents: 40627
diff changeset
   174
val inc_reconstructor_calls = map_re_data
39337
ffa577c0bbfa keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents: 39321
diff changeset
   175
  (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns)
ffa577c0bbfa keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents: 39321
diff changeset
   176
    => (calls + 1, success, nontriv_calls, nontriv_success, proofs, time, timeout, lemmas,posns))
32533
9735013cec72 tuned stats
nipkow
parents: 32526
diff changeset
   177
40667
b8579f24ce67 make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents: 40627
diff changeset
   178
val inc_reconstructor_success = map_re_data
39337
ffa577c0bbfa keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents: 39321
diff changeset
   179
  (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns)
ffa577c0bbfa keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents: 39321
diff changeset
   180
    => (calls, success + 1, nontriv_calls, nontriv_success, proofs, time, timeout, lemmas,posns))
ffa577c0bbfa keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents: 39321
diff changeset
   181
40667
b8579f24ce67 make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents: 40627
diff changeset
   182
val inc_reconstructor_nontriv_calls = map_re_data
39337
ffa577c0bbfa keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents: 39321
diff changeset
   183
  (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns)
ffa577c0bbfa keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents: 39321
diff changeset
   184
    => (calls, success, nontriv_calls + 1, nontriv_success, proofs, time, timeout, lemmas,posns))
ffa577c0bbfa keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents: 39321
diff changeset
   185
40667
b8579f24ce67 make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents: 40627
diff changeset
   186
val inc_reconstructor_nontriv_success = map_re_data
39337
ffa577c0bbfa keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents: 39321
diff changeset
   187
  (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns)
ffa577c0bbfa keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents: 39321
diff changeset
   188
    => (calls, success, nontriv_calls, nontriv_success + 1, proofs, time, timeout, lemmas,posns))
32676
b1c85a117dec record how many "proof"s are solved by s/h
nipkow
parents: 32612
diff changeset
   189
40667
b8579f24ce67 make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents: 40627
diff changeset
   190
val inc_reconstructor_proofs = map_re_data
39337
ffa577c0bbfa keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents: 39321
diff changeset
   191
  (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns)
ffa577c0bbfa keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents: 39321
diff changeset
   192
    => (calls, success, nontriv_calls, nontriv_success, proofs + 1, time, timeout, lemmas,posns))
32551
421323205efd position information is now passed to all actions;
nipkow
parents: 32550
diff changeset
   193
40667
b8579f24ce67 make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents: 40627
diff changeset
   194
fun inc_reconstructor_time m t = map_re_data
39337
ffa577c0bbfa keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents: 39321
diff changeset
   195
 (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns)
ffa577c0bbfa keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents: 39321
diff changeset
   196
  => (calls, success, nontriv_calls, nontriv_success, proofs, time + t, timeout, lemmas,posns)) m
32536
ac56c62758d3 tuned stats
nipkow
parents: 32533
diff changeset
   197
40667
b8579f24ce67 make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents: 40627
diff changeset
   198
val inc_reconstructor_timeout = map_re_data
39337
ffa577c0bbfa keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents: 39321
diff changeset
   199
  (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns)
ffa577c0bbfa keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents: 39321
diff changeset
   200
    => (calls, success, nontriv_calls, nontriv_success, proofs, time, timeout + 1, lemmas,posns))
32549
338ccfd37f67 minimization: comparing w/ and w/o.
nipkow
parents: 32541
diff changeset
   201
40667
b8579f24ce67 make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents: 40627
diff changeset
   202
fun inc_reconstructor_lemmas m n = map_re_data
39337
ffa577c0bbfa keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents: 39321
diff changeset
   203
  (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns)
ffa577c0bbfa keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents: 39321
diff changeset
   204
    => (calls, success, nontriv_calls, nontriv_success, proofs, time, timeout, inc_max n lemmas, posns)) m
32551
421323205efd position information is now passed to all actions;
nipkow
parents: 32550
diff changeset
   205
40667
b8579f24ce67 make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents: 40627
diff changeset
   206
fun inc_reconstructor_posns m pos = map_re_data
39337
ffa577c0bbfa keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents: 39321
diff changeset
   207
  (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns)
ffa577c0bbfa keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents: 39321
diff changeset
   208
    => (calls, success, nontriv_calls, nontriv_success, proofs, time, timeout, lemmas, pos::posns)) m
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   209
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   210
local
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   211
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   212
val str = string_of_int
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   213
val str3 = Real.fmt (StringCvt.FIX (SOME 3))
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   214
fun percentage a b = string_of_int (a * 100 div b)
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   215
fun time t = Real.fromInt t / 1000.0
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   216
fun avg_time t n =
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   217
  if n > 0 then (Real.fromInt t / 1000.0) / Real.fromInt n else 0.0
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   218
34035
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   219
fun log_sh_data log
40062
cfaebaa8588f make Sledgehammer minimizer fully work with SMT
blanchet
parents: 40061
diff changeset
   220
    (calls, success, nontriv_calls, nontriv_success, lemmas, max_lems, time_isa, time_prover, time_prover_fail) =
32818
6c91e668b15e record max lemmas used
nipkow
parents: 32676
diff changeset
   221
 (log ("Total number of sledgehammer calls: " ^ str calls);
6c91e668b15e record max lemmas used
nipkow
parents: 32676
diff changeset
   222
  log ("Number of successful sledgehammer calls: " ^ str success);
6c91e668b15e record max lemmas used
nipkow
parents: 32676
diff changeset
   223
  log ("Number of sledgehammer lemmas: " ^ str lemmas);
6c91e668b15e record max lemmas used
nipkow
parents: 32676
diff changeset
   224
  log ("Max number of sledgehammer lemmas: " ^ str max_lems);
6c91e668b15e record max lemmas used
nipkow
parents: 32676
diff changeset
   225
  log ("Success rate: " ^ percentage success calls ^ "%");
39337
ffa577c0bbfa keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents: 39321
diff changeset
   226
  log ("Total number of nontrivial sledgehammer calls: " ^ str nontriv_calls);
ffa577c0bbfa keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents: 39321
diff changeset
   227
  log ("Number of successful nontrivial sledgehammer calls: " ^ str nontriv_success);
32818
6c91e668b15e record max lemmas used
nipkow
parents: 32676
diff changeset
   228
  log ("Total time for sledgehammer calls (Isabelle): " ^ str3 (time time_isa));
40062
cfaebaa8588f make Sledgehammer minimizer fully work with SMT
blanchet
parents: 40061
diff changeset
   229
  log ("Total time for successful sledgehammer calls (ATP): " ^ str3 (time time_prover));
cfaebaa8588f make Sledgehammer minimizer fully work with SMT
blanchet
parents: 40061
diff changeset
   230
  log ("Total time for failed sledgehammer calls (ATP): " ^ str3 (time time_prover_fail));
32536
ac56c62758d3 tuned stats
nipkow
parents: 32533
diff changeset
   231
  log ("Average time for sledgehammer calls (Isabelle): " ^
32818
6c91e668b15e record max lemmas used
nipkow
parents: 32676
diff changeset
   232
    str3 (avg_time time_isa calls));
32533
9735013cec72 tuned stats
nipkow
parents: 32526
diff changeset
   233
  log ("Average time for successful sledgehammer calls (ATP): " ^
40062
cfaebaa8588f make Sledgehammer minimizer fully work with SMT
blanchet
parents: 40061
diff changeset
   234
    str3 (avg_time time_prover success));
32536
ac56c62758d3 tuned stats
nipkow
parents: 32533
diff changeset
   235
  log ("Average time for failed sledgehammer calls (ATP): " ^
40062
cfaebaa8588f make Sledgehammer minimizer fully work with SMT
blanchet
parents: 40061
diff changeset
   236
    str3 (avg_time time_prover_fail (calls - success)))
32533
9735013cec72 tuned stats
nipkow
parents: 32526
diff changeset
   237
  )
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   238
32551
421323205efd position information is now passed to all actions;
nipkow
parents: 32550
diff changeset
   239
39341
d2b981a0429a indicate triviality in the list of proved things
blanchet
parents: 39340
diff changeset
   240
fun str_of_pos (pos, triv) =
32551
421323205efd position information is now passed to all actions;
nipkow
parents: 32550
diff changeset
   241
  let val str0 = string_of_int o the_default 0
39341
d2b981a0429a indicate triviality in the list of proved things
blanchet
parents: 39340
diff changeset
   242
  in
d2b981a0429a indicate triviality in the list of proved things
blanchet
parents: 39340
diff changeset
   243
    str0 (Position.line_of pos) ^ ":" ^ str0 (Position.column_of pos) ^
d2b981a0429a indicate triviality in the list of proved things
blanchet
parents: 39340
diff changeset
   244
    (if triv then "[T]" else "")
d2b981a0429a indicate triviality in the list of proved things
blanchet
parents: 39340
diff changeset
   245
  end
32551
421323205efd position information is now passed to all actions;
nipkow
parents: 32550
diff changeset
   246
40667
b8579f24ce67 make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents: 40627
diff changeset
   247
fun log_re_data log tag sh_calls (re_calls, re_success, re_nontriv_calls,
b8579f24ce67 make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents: 40627
diff changeset
   248
     re_nontriv_success, re_proofs, re_time, re_timeout,
b8579f24ce67 make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents: 40627
diff changeset
   249
    (lemmas, lems_sos, lems_max), re_posns) =
b8579f24ce67 make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents: 40627
diff changeset
   250
 (log ("Total number of " ^ tag ^ "reconstructor calls: " ^ str re_calls);
b8579f24ce67 make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents: 40627
diff changeset
   251
  log ("Number of successful " ^ tag ^ "reconstructor calls: " ^ str re_success ^
b8579f24ce67 make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents: 40627
diff changeset
   252
    " (proof: " ^ str re_proofs ^ ")");
b8579f24ce67 make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents: 40627
diff changeset
   253
  log ("Number of " ^ tag ^ "reconstructor timeouts: " ^ str re_timeout);
b8579f24ce67 make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents: 40627
diff changeset
   254
  log ("Success rate: " ^ percentage re_success sh_calls ^ "%");
b8579f24ce67 make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents: 40627
diff changeset
   255
  log ("Total number of nontrivial " ^ tag ^ "reconstructor calls: " ^ str re_nontriv_calls);
b8579f24ce67 make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents: 40627
diff changeset
   256
  log ("Number of successful nontrivial " ^ tag ^ "reconstructor calls: " ^ str re_nontriv_success ^
b8579f24ce67 make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents: 40627
diff changeset
   257
    " (proof: " ^ str re_proofs ^ ")");
b8579f24ce67 make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents: 40627
diff changeset
   258
  log ("Number of successful " ^ tag ^ "reconstructor lemmas: " ^ str lemmas);
b8579f24ce67 make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents: 40627
diff changeset
   259
  log ("SOS of successful " ^ tag ^ "reconstructor lemmas: " ^ str lems_sos);
b8579f24ce67 make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents: 40627
diff changeset
   260
  log ("Max number of successful " ^ tag ^ "reconstructor lemmas: " ^ str lems_max);
b8579f24ce67 make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents: 40627
diff changeset
   261
  log ("Total time for successful " ^ tag ^ "reconstructor calls: " ^ str3 (time re_time));
b8579f24ce67 make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents: 40627
diff changeset
   262
  log ("Average time for successful " ^ tag ^ "reconstructor calls: " ^
b8579f24ce67 make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents: 40627
diff changeset
   263
    str3 (avg_time re_time re_success));
32551
421323205efd position information is now passed to all actions;
nipkow
parents: 32550
diff changeset
   264
  if tag=""
40667
b8579f24ce67 make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents: 40627
diff changeset
   265
  then log ("Proved: " ^ space_implode " " (map str_of_pos re_posns))
32551
421323205efd position information is now passed to all actions;
nipkow
parents: 32550
diff changeset
   266
  else ()
421323205efd position information is now passed to all actions;
nipkow
parents: 32550
diff changeset
   267
 )
32571
d4bb776874b8 count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents: 32567
diff changeset
   268
35866
513074557e06 move the Sledgehammer Isar commands together into one file;
blanchet
parents: 35830
diff changeset
   269
fun log_min_data log (succs, ab_ratios) =
32609
2f3e7a92b522 modified minimization log
nipkow
parents: 32607
diff changeset
   270
  (log ("Number of successful minimizations: " ^ string_of_int succs);
35866
513074557e06 move the Sledgehammer Isar commands together into one file;
blanchet
parents: 35830
diff changeset
   271
   log ("After/before ratios: " ^ string_of_int ab_ratios)
32571
d4bb776874b8 count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents: 32567
diff changeset
   272
  )
d4bb776874b8 count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents: 32567
diff changeset
   273
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   274
in
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   275
40667
b8579f24ce67 make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents: 40627
diff changeset
   276
fun log_data id log (Data {sh, min, re_u, re_m, re_uft, re_mft, mini}) =
34035
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   277
  let
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   278
    val ShData {calls=sh_calls, ...} = sh
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   279
40667
b8579f24ce67 make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents: 40627
diff changeset
   280
    fun app_if (ReData {calls, ...}) f = if calls > 0 then f () else ()
b8579f24ce67 make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents: 40627
diff changeset
   281
    fun log_re tag m =
b8579f24ce67 make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents: 40627
diff changeset
   282
      log_re_data log tag sh_calls (tuple_of_re_data m)
b8579f24ce67 make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents: 40627
diff changeset
   283
    fun log_reconstructor (tag1, m1) (tag2, m2) = app_if m1 (fn () =>
b8579f24ce67 make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents: 40627
diff changeset
   284
      (log_re tag1 m1; log ""; app_if m2 (fn () => log_re tag2 m2)))
34035
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   285
  in
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   286
    if sh_calls > 0
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   287
    then
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   288
     (log ("\n\n\nReport #" ^ string_of_int id ^ ":\n");
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   289
      log_sh_data log (tuple_of_sh_data sh);
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   290
      log "";
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   291
      if not mini
40667
b8579f24ce67 make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents: 40627
diff changeset
   292
      then log_reconstructor ("", re_u) ("fully-typed ", re_uft)
34035
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   293
      else
40667
b8579f24ce67 make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents: 40627
diff changeset
   294
        app_if re_u (fn () =>
b8579f24ce67 make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents: 40627
diff changeset
   295
         (log_reconstructor ("unminimized ", re_u) ("unminimized fully-typed ", re_uft);
34035
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   296
          log "";
40667
b8579f24ce67 make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents: 40627
diff changeset
   297
          app_if re_m (fn () =>
34035
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   298
            (log_min_data log (tuple_of_min_data min); log "";
40667
b8579f24ce67 make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents: 40627
diff changeset
   299
             log_reconstructor ("", re_m) ("fully-typed ", re_mft))))))
34035
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   300
    else ()
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   301
  end
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   302
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   303
end
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   304
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   305
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   306
(* Warning: we implicitly assume single-threaded execution here! *)
32740
9dd0a2f83429 explicit indication of Unsynchronized.ref;
wenzelm
parents: 32676
diff changeset
   307
val data = Unsynchronized.ref ([] : (int * data) list)
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   308
32740
9dd0a2f83429 explicit indication of Unsynchronized.ref;
wenzelm
parents: 32676
diff changeset
   309
fun init id thy = (Unsynchronized.change data (cons (id, empty_data)); thy)
32567
de411627a985 explicitly export type abbreviations (as usual in SML97);
wenzelm
parents: 32564
diff changeset
   310
fun done id ({log, ...}: Mirabelle.done_args) =
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   311
  AList.lookup (op =) (!data) id
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   312
  |> Option.map (log_data id log)
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   313
  |> K ()
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   314
32740
9dd0a2f83429 explicit indication of Unsynchronized.ref;
wenzelm
parents: 32676
diff changeset
   315
fun change_data id f = (Unsynchronized.change data (AList.map_entry (op =) id f); ())
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   316
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   317
40069
6f7bf79b1506 fixed signature of "is_smt_solver_installed";
blanchet
parents: 40065
diff changeset
   318
fun get_prover ctxt args =
33016
b73b74fe23c3 proper exceptions instead of unhandled partiality
boehmes
parents: 32991
diff changeset
   319
  let
40062
cfaebaa8588f make Sledgehammer minimizer fully work with SMT
blanchet
parents: 40061
diff changeset
   320
    fun default_prover_name () =
40069
6f7bf79b1506 fixed signature of "is_smt_solver_installed";
blanchet
parents: 40065
diff changeset
   321
      hd (#provers (Sledgehammer_Isar.default_params ctxt []))
33016
b73b74fe23c3 proper exceptions instead of unhandled partiality
boehmes
parents: 32991
diff changeset
   322
      handle Empty => error "No ATP available."
41087
d7b5fd465198 split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems
blanchet
parents: 40983
diff changeset
   323
    fun get_prover name =
41264
a96b0b62f588 use minimizing prover in Mirabelle
blanchet
parents: 41260
diff changeset
   324
      (name, Sledgehammer_Run.get_minimizing_prover ctxt false name)
33016
b73b74fe23c3 proper exceptions instead of unhandled partiality
boehmes
parents: 32991
diff changeset
   325
  in
b73b74fe23c3 proper exceptions instead of unhandled partiality
boehmes
parents: 32991
diff changeset
   326
    (case AList.lookup (op =) args proverK of
40062
cfaebaa8588f make Sledgehammer minimizer fully work with SMT
blanchet
parents: 40061
diff changeset
   327
      SOME name => get_prover name
cfaebaa8588f make Sledgehammer minimizer fully work with SMT
blanchet
parents: 40061
diff changeset
   328
    | NONE => get_prover (default_prover_name ()))
33016
b73b74fe23c3 proper exceptions instead of unhandled partiality
boehmes
parents: 32991
diff changeset
   329
  end
32525
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   330
38988
483879af0643 finished renaming
blanchet
parents: 38826
diff changeset
   331
type locality = Sledgehammer_Filter.locality
38752
6628adcae4a7 consider "locality" when assigning weights to facts
blanchet
parents: 38700
diff changeset
   332
40667
b8579f24ce67 make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents: 40627
diff changeset
   333
(* hack *)
b8579f24ce67 make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents: 40627
diff changeset
   334
fun reconstructor_from_msg msg =
41154
5ccc40f679d8 honor "metisFT" in Mirabelle
blanchet
parents: 41138
diff changeset
   335
  if String.isSubstring "metisFT" msg then "metisFT"
5ccc40f679d8 honor "metisFT" in Mirabelle
blanchet
parents: 41138
diff changeset
   336
  else if String.isSubstring "metis" msg then "metis"
5ccc40f679d8 honor "metisFT" in Mirabelle
blanchet
parents: 41138
diff changeset
   337
  else "smt"
40667
b8579f24ce67 make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents: 40627
diff changeset
   338
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   339
local
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   340
32536
ac56c62758d3 tuned stats
nipkow
parents: 32533
diff changeset
   341
datatype sh_result =
38752
6628adcae4a7 consider "locality" when assigning weights to facts
blanchet
parents: 38700
diff changeset
   342
  SH_OK of int * int * (string * locality) list |
32536
ac56c62758d3 tuned stats
nipkow
parents: 32533
diff changeset
   343
  SH_FAIL of int * int |
ac56c62758d3 tuned stats
nipkow
parents: 32533
diff changeset
   344
  SH_ERROR
ac56c62758d3 tuned stats
nipkow
parents: 32533
diff changeset
   345
41155
85da8cbb4966 added support for "type_sys" option to Mirabelle
blanchet
parents: 41154
diff changeset
   346
fun run_sh prover_name prover type_sys hard_timeout timeout dir st =
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   347
  let
38998
f11a861e0061 share the relevance filter among the provers
blanchet
parents: 38988
diff changeset
   348
    val {context = ctxt, facts = chained_ths, goal} = Proof.goal st
f11a861e0061 share the relevance filter among the provers
blanchet
parents: 38988
diff changeset
   349
    val i = 1
41337
263fe1670067 mechanism to keep SMT input and output files around in Mirabelle
blanchet
parents: 41276
diff changeset
   350
    fun change_dir (SOME dir) =
263fe1670067 mechanism to keep SMT input and output files around in Mirabelle
blanchet
parents: 41276
diff changeset
   351
        Config.put Sledgehammer_Provers.dest_dir dir
263fe1670067 mechanism to keep SMT input and output files around in Mirabelle
blanchet
parents: 41276
diff changeset
   352
        #> Config.put SMT_Config.debug_files
41338
ffd730fcf0ac avoid weird symbols in path
blanchet
parents: 41337
diff changeset
   353
          (dir ^ "/" ^ Name.desymbolize false (ATP_Problem.timestamp ()) ^ "_"
ffd730fcf0ac avoid weird symbols in path
blanchet
parents: 41337
diff changeset
   354
          ^ serial_string ())
39321
23951979a362 make Mirabelle happy
blanchet
parents: 39005
diff changeset
   355
      | change_dir NONE = I
23951979a362 make Mirabelle happy
blanchet
parents: 39005
diff changeset
   356
    val st' =
23951979a362 make Mirabelle happy
blanchet
parents: 39005
diff changeset
   357
      st |> Proof.map_context
23951979a362 make Mirabelle happy
blanchet
parents: 39005
diff changeset
   358
                (change_dir dir
41087
d7b5fd465198 split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems
blanchet
parents: 40983
diff changeset
   359
                 #> Config.put Sledgehammer_Provers.measure_run_time true)
41138
eb80538166b6 implemented partially-typed "tags" type encoding
blanchet
parents: 41091
diff changeset
   360
    val params as {type_sys, relevance_thresholds, max_relevant, ...} =
40069
6f7bf79b1506 fixed signature of "is_smt_solver_installed";
blanchet
parents: 40065
diff changeset
   361
      Sledgehammer_Isar.default_params ctxt
40554
ff446d5e9a62 turn on Sledgehammer verbosity so we can track down crashes
blanchet
parents: 40526
diff changeset
   362
          [("verbose", "true"),
41155
85da8cbb4966 added support for "type_sys" option to Mirabelle
blanchet
parents: 41154
diff changeset
   363
           ("type_sys", type_sys),
40554
ff446d5e9a62 turn on Sledgehammer verbosity so we can track down crashes
blanchet
parents: 40526
diff changeset
   364
           ("timeout", Int.toString timeout)]
40062
cfaebaa8588f make Sledgehammer minimizer fully work with SMT
blanchet
parents: 40061
diff changeset
   365
    val default_max_relevant =
41087
d7b5fd465198 split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems
blanchet
parents: 40983
diff changeset
   366
      Sledgehammer_Provers.default_max_relevant_for_prover ctxt prover_name
40369
53dca3bd4250 use the SMT integration's official list of built-ins
blanchet
parents: 40301
diff changeset
   367
    val is_built_in_const =
41087
d7b5fd465198 split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems
blanchet
parents: 40983
diff changeset
   368
      Sledgehammer_Provers.is_built_in_const_for_prover ctxt prover_name
40941
a3e6f8634a11 replace "smt" prover with specific SMT solvers, e.g. "z3" -- whatever the SMT module gives us
blanchet
parents: 40694
diff changeset
   369
    val relevance_fudge =
41087
d7b5fd465198 split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems
blanchet
parents: 40983
diff changeset
   370
      Sledgehammer_Provers.relevance_fudge_for_prover ctxt prover_name
40070
bdb890782d4a replaced references with proper record that's threaded through
blanchet
parents: 40069
diff changeset
   371
    val relevance_override = {add = [], del = [], only = false}
38998
f11a861e0061 share the relevance filter among the provers
blanchet
parents: 38988
diff changeset
   372
    val (_, hyp_ts, concl_t) = Sledgehammer_Util.strip_subgoal goal i
41138
eb80538166b6 implemented partially-typed "tags" type encoding
blanchet
parents: 41091
diff changeset
   373
    val no_dangerous_types =
eb80538166b6 implemented partially-typed "tags" type encoding
blanchet
parents: 41091
diff changeset
   374
      Sledgehammer_ATP_Translate.types_dangerous_types type_sys
32574
719426c9e1eb added hard timeout for sledgehammer based on elapsed time (no need to trust ATP's timeout handling);
boehmes
parents: 32571
diff changeset
   375
    val time_limit =
719426c9e1eb added hard timeout for sledgehammer based on elapsed time (no need to trust ATP's timeout handling);
boehmes
parents: 32571
diff changeset
   376
      (case hard_timeout of
719426c9e1eb added hard timeout for sledgehammer based on elapsed time (no need to trust ATP's timeout handling);
boehmes
parents: 32571
diff changeset
   377
        NONE => I
719426c9e1eb added hard timeout for sledgehammer based on elapsed time (no need to trust ATP's timeout handling);
boehmes
parents: 32571
diff changeset
   378
      | SOME secs => TimeLimit.timeLimit (Time.fromSeconds secs))
41274
6a9306c427b9 handle timeouts in Mirabelle more gracefully
blanchet
parents: 41268
diff changeset
   379
    val ({outcome, message, used_facts, run_time_in_msecs}
41087
d7b5fd465198 split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems
blanchet
parents: 40983
diff changeset
   380
         : Sledgehammer_Provers.prover_result,
41275
3897af72c731 move relevance filter into hard timeout
blanchet
parents: 41274
diff changeset
   381
        time_isa) = time_limit (Mirabelle.cpu_time (fn () =>
3897af72c731 move relevance filter into hard timeout
blanchet
parents: 41274
diff changeset
   382
      let
3897af72c731 move relevance filter into hard timeout
blanchet
parents: 41274
diff changeset
   383
        val facts =
3897af72c731 move relevance filter into hard timeout
blanchet
parents: 41274
diff changeset
   384
          Sledgehammer_Filter.relevant_facts ctxt no_dangerous_types
3897af72c731 move relevance filter into hard timeout
blanchet
parents: 41274
diff changeset
   385
              relevance_thresholds
3897af72c731 move relevance filter into hard timeout
blanchet
parents: 41274
diff changeset
   386
              (the_default default_max_relevant max_relevant) is_built_in_const
3897af72c731 move relevance filter into hard timeout
blanchet
parents: 41274
diff changeset
   387
              relevance_fudge relevance_override chained_ths hyp_ts concl_t
3897af72c731 move relevance filter into hard timeout
blanchet
parents: 41274
diff changeset
   388
        val problem =
3897af72c731 move relevance filter into hard timeout
blanchet
parents: 41274
diff changeset
   389
          {state = st', goal = goal, subgoal = i,
3897af72c731 move relevance filter into hard timeout
blanchet
parents: 41274
diff changeset
   390
           subgoal_count = Sledgehammer_Util.subgoal_count st,
3897af72c731 move relevance filter into hard timeout
blanchet
parents: 41274
diff changeset
   391
           facts = facts |> map Sledgehammer_Provers.Untranslated_Fact,
3897af72c731 move relevance filter into hard timeout
blanchet
parents: 41274
diff changeset
   392
           smt_head = NONE}
3897af72c731 move relevance filter into hard timeout
blanchet
parents: 41274
diff changeset
   393
      in prover params (K "") problem end)) ()
41274
6a9306c427b9 handle timeouts in Mirabelle more gracefully
blanchet
parents: 41268
diff changeset
   394
      handle TimeLimit.TimeOut =>
6a9306c427b9 handle timeouts in Mirabelle more gracefully
blanchet
parents: 41268
diff changeset
   395
             ({outcome = SOME ATP_Proof.TimedOut, message = "", used_facts = [],
6a9306c427b9 handle timeouts in Mirabelle more gracefully
blanchet
parents: 41268
diff changeset
   396
               run_time_in_msecs = NONE}, ~1)
40374
443b426e05ea make Mirabelle work correctly if the prover (e.g. the SMT solver) returns no timing information
blanchet
parents: 40372
diff changeset
   397
    val time_prover = run_time_in_msecs |> the_default ~1
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   398
  in
36405
05a8d79eb338 compile
blanchet
parents: 36373
diff changeset
   399
    case outcome of
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
   400
      NONE => (message, SH_OK (time_isa, time_prover, used_facts))
40062
cfaebaa8588f make Sledgehammer minimizer fully work with SMT
blanchet
parents: 40061
diff changeset
   401
    | SOME _ => (message, SH_FAIL (time_isa, time_prover))
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   402
  end
37994
b04307085a09 make TPTP generator accept full first-order formulas
blanchet
parents: 37631
diff changeset
   403
  handle ERROR msg => ("error: " ^ msg, SH_ERROR)
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   404
32454
a1a5589207ad Mirabelle: proper parsing of theorem names found by sledgehammer, respecting test intervals given along with file names
boehmes
parents: 32452
diff changeset
   405
fun thms_of_name ctxt name =
a1a5589207ad Mirabelle: proper parsing of theorem names found by sledgehammer, respecting test intervals given along with file names
boehmes
parents: 32452
diff changeset
   406
  let
36960
01594f816e3a prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents: 36959
diff changeset
   407
    val lex = Keyword.get_lexicons
32454
a1a5589207ad Mirabelle: proper parsing of theorem names found by sledgehammer, respecting test intervals given along with file names
boehmes
parents: 32452
diff changeset
   408
    val get = maps (ProofContext.get_fact ctxt o fst)
a1a5589207ad Mirabelle: proper parsing of theorem names found by sledgehammer, respecting test intervals given along with file names
boehmes
parents: 32452
diff changeset
   409
  in
a1a5589207ad Mirabelle: proper parsing of theorem names found by sledgehammer, respecting test intervals given along with file names
boehmes
parents: 32452
diff changeset
   410
    Source.of_string name
40526
ca3c6b1bfcdb total Symbol.source;
wenzelm
parents: 40417
diff changeset
   411
    |> Symbol.source
36959
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 36954
diff changeset
   412
    |> Token.source {do_recover=SOME false} lex Position.start
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 36954
diff changeset
   413
    |> Token.source_proper
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 36954
diff changeset
   414
    |> Source.source Token.stopper (Parse_Spec.xthms1 >> get) NONE
32454
a1a5589207ad Mirabelle: proper parsing of theorem names found by sledgehammer, respecting test intervals given along with file names
boehmes
parents: 32452
diff changeset
   415
    |> Source.exhaust
a1a5589207ad Mirabelle: proper parsing of theorem names found by sledgehammer, respecting test intervals given along with file names
boehmes
parents: 32452
diff changeset
   416
  end
32452
d84edd022efe apply metis with found theorems in case sledgehammer was successful
boehmes
parents: 32434
diff changeset
   417
32498
1132c7c13f36 Mirabelle: actions are responsible for handling exceptions,
boehmes
parents: 32496
diff changeset
   418
in
1132c7c13f36 Mirabelle: actions are responsible for handling exceptions,
boehmes
parents: 32496
diff changeset
   419
40667
b8579f24ce67 make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents: 40627
diff changeset
   420
fun run_sledgehammer trivial args reconstructor named_thms id ({pre=st, log, ...}: Mirabelle.run_args) =
32385
594890623c46 split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff changeset
   421
  let
39340
3998dc0bf82b indicate which goals are trivial
blanchet
parents: 39337
diff changeset
   422
    val triv_str = if trivial then "[T] " else ""
32536
ac56c62758d3 tuned stats
nipkow
parents: 32533
diff changeset
   423
    val _ = change_data id inc_sh_calls
39337
ffa577c0bbfa keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents: 39321
diff changeset
   424
    val _ = if trivial then () else change_data id inc_sh_nontriv_calls
40069
6f7bf79b1506 fixed signature of "is_smt_solver_installed";
blanchet
parents: 40065
diff changeset
   425
    val (prover_name, prover) = get_prover (Proof.context_of st) args
41155
85da8cbb4966 added support for "type_sys" option to Mirabelle
blanchet
parents: 41154
diff changeset
   426
    val type_sys = AList.lookup (op =) args type_sysK |> the_default "smart"
32525
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   427
    val dir = AList.lookup (op =) args keepK
32541
cea1716eb106 timeout option for ATPs
boehmes
parents: 32536
diff changeset
   428
    val timeout = Mirabelle.get_int_setting args (prover_timeoutK, 30)
41268
56b7e277fd7d higher hard timeout
blanchet
parents: 41266
diff changeset
   429
    (* always use a hard timeout, but give some slack so that the automatic
56b7e277fd7d higher hard timeout
blanchet
parents: 41266
diff changeset
   430
       minimizer has a chance to do its magic *)
56b7e277fd7d higher hard timeout
blanchet
parents: 41266
diff changeset
   431
    val hard_timeout = SOME (2 * timeout)
41155
85da8cbb4966 added support for "type_sys" option to Mirabelle
blanchet
parents: 41154
diff changeset
   432
    val (msg, result) =
85da8cbb4966 added support for "type_sys" option to Mirabelle
blanchet
parents: 41154
diff changeset
   433
      run_sh prover_name prover type_sys hard_timeout timeout dir st
32525
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   434
  in
32536
ac56c62758d3 tuned stats
nipkow
parents: 32533
diff changeset
   435
    case result of
40062
cfaebaa8588f make Sledgehammer minimizer fully work with SMT
blanchet
parents: 40061
diff changeset
   436
      SH_OK (time_isa, time_prover, names) =>
38700
fcb0fe4c2f27 make Mirabelle happy
blanchet
parents: 38590
diff changeset
   437
        let
39377
blanchet
parents: 39366
diff changeset
   438
          fun get_thms (_, Sledgehammer_Filter.Chained) = NONE
38826
f42f425edf24 drop chained facts
blanchet
parents: 38752
diff changeset
   439
            | get_thms (name, loc) =
f42f425edf24 drop chained facts
blanchet
parents: 38752
diff changeset
   440
              SOME ((name, loc), thms_of_name (Proof.context_of st) name)
32525
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   441
        in
32818
6c91e668b15e record max lemmas used
nipkow
parents: 32676
diff changeset
   442
          change_data id inc_sh_success;
39337
ffa577c0bbfa keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents: 39321
diff changeset
   443
          if trivial then () else change_data id inc_sh_nontriv_success;
32818
6c91e668b15e record max lemmas used
nipkow
parents: 32676
diff changeset
   444
          change_data id (inc_sh_lemmas (length names));
6c91e668b15e record max lemmas used
nipkow
parents: 32676
diff changeset
   445
          change_data id (inc_sh_max_lems (length names));
6c91e668b15e record max lemmas used
nipkow
parents: 32676
diff changeset
   446
          change_data id (inc_sh_time_isa time_isa);
40062
cfaebaa8588f make Sledgehammer minimizer fully work with SMT
blanchet
parents: 40061
diff changeset
   447
          change_data id (inc_sh_time_prover time_prover);
40667
b8579f24ce67 make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents: 40627
diff changeset
   448
          reconstructor := reconstructor_from_msg msg;
38826
f42f425edf24 drop chained facts
blanchet
parents: 38752
diff changeset
   449
          named_thms := SOME (map_filter get_thms names);
39340
3998dc0bf82b indicate which goals are trivial
blanchet
parents: 39337
diff changeset
   450
          log (sh_tag id ^ triv_str ^ "succeeded (" ^ string_of_int time_isa ^ "+" ^
40062
cfaebaa8588f make Sledgehammer minimizer fully work with SMT
blanchet
parents: 40061
diff changeset
   451
            string_of_int time_prover ^ ") [" ^ prover_name ^ "]:\n" ^ msg)
32525
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   452
        end
40062
cfaebaa8588f make Sledgehammer minimizer fully work with SMT
blanchet
parents: 40061
diff changeset
   453
    | SH_FAIL (time_isa, time_prover) =>
32536
ac56c62758d3 tuned stats
nipkow
parents: 32533
diff changeset
   454
        let
ac56c62758d3 tuned stats
nipkow
parents: 32533
diff changeset
   455
          val _ = change_data id (inc_sh_time_isa time_isa)
40062
cfaebaa8588f make Sledgehammer minimizer fully work with SMT
blanchet
parents: 40061
diff changeset
   456
          val _ = change_data id (inc_sh_time_prover_fail time_prover)
39340
3998dc0bf82b indicate which goals are trivial
blanchet
parents: 39337
diff changeset
   457
        in log (sh_tag id ^ triv_str ^ "failed: " ^ msg) end
32536
ac56c62758d3 tuned stats
nipkow
parents: 32533
diff changeset
   458
    | SH_ERROR => log (sh_tag id ^ "failed: " ^ msg)
32525
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   459
  end
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   460
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   461
end
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   462
40667
b8579f24ce67 make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents: 40627
diff changeset
   463
fun run_minimize args reconstructor named_thms id
b8579f24ce67 make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents: 40627
diff changeset
   464
        ({pre=st, log, ...}: Mirabelle.run_args) =
32525
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   465
  let
40069
6f7bf79b1506 fixed signature of "is_smt_solver_installed";
blanchet
parents: 40065
diff changeset
   466
    val ctxt = Proof.context_of st
32571
d4bb776874b8 count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents: 32567
diff changeset
   467
    val n0 = length (these (!named_thms))
40069
6f7bf79b1506 fixed signature of "is_smt_solver_installed";
blanchet
parents: 40065
diff changeset
   468
    val (prover_name, _) = get_prover ctxt args
41155
85da8cbb4966 added support for "type_sys" option to Mirabelle
blanchet
parents: 41154
diff changeset
   469
    val type_sys = AList.lookup (op =) args type_sysK |> the_default "smart"
32525
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   470
    val timeout =
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   471
      AList.lookup (op =) args minimize_timeoutK
40627
becf5d5187cc renamed raw "explode" function to "raw_explode" to emphasize its meaning;
wenzelm
parents: 40554
diff changeset
   472
      |> Option.map (fst o read_int o raw_explode)  (* FIXME Symbol.explode (?) *)
32525
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   473
      |> the_default 5
40069
6f7bf79b1506 fixed signature of "is_smt_solver_installed";
blanchet
parents: 40065
diff changeset
   474
    val params = Sledgehammer_Isar.default_params ctxt
41155
85da8cbb4966 added support for "type_sys" option to Mirabelle
blanchet
parents: 41154
diff changeset
   475
      [("provers", prover_name),
85da8cbb4966 added support for "type_sys" option to Mirabelle
blanchet
parents: 41154
diff changeset
   476
       ("verbose", "true"),
85da8cbb4966 added support for "type_sys" option to Mirabelle
blanchet
parents: 41154
diff changeset
   477
       ("type_sys", type_sys),
40554
ff446d5e9a62 turn on Sledgehammer verbosity so we can track down crashes
blanchet
parents: 40526
diff changeset
   478
       ("timeout", Int.toString timeout)]
37587
466031e057a0 compile
blanchet
parents: 37578
diff changeset
   479
    val minimize =
41266
b6b77c963f11 compile
blanchet
parents: 41264
diff changeset
   480
      Sledgehammer_Minimize.minimize_facts prover_name params true 1
40065
1e4c7185f3f9 remove more needless code ("run_smt_solvers");
blanchet
parents: 40063
diff changeset
   481
                                           (Sledgehammer_Util.subgoal_count st)
32525
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   482
    val _ = log separator
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   483
  in
35971
4f24a4e9af4a make Mirabelle happy again
blanchet
parents: 35871
diff changeset
   484
    case minimize st (these (!named_thms)) of
35871
c93bda4fdf15 remove the iteration counter from Sledgehammer's minimizer
blanchet
parents: 35867
diff changeset
   485
      (SOME named_thms', msg) =>
32609
2f3e7a92b522 modified minimization log
nipkow
parents: 32607
diff changeset
   486
        (change_data id inc_min_succs;
2f3e7a92b522 modified minimization log
nipkow
parents: 32607
diff changeset
   487
         change_data id (inc_min_ab_ratios ((100 * length named_thms') div n0));
32571
d4bb776874b8 count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents: 32567
diff changeset
   488
         if length named_thms' = n0
d4bb776874b8 count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents: 32567
diff changeset
   489
         then log (minimize_tag id ^ "already minimal")
40667
b8579f24ce67 make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents: 40627
diff changeset
   490
         else (reconstructor := reconstructor_from_msg msg;
b8579f24ce67 make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents: 40627
diff changeset
   491
               named_thms := SOME named_thms';
32571
d4bb776874b8 count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents: 32567
diff changeset
   492
               log (minimize_tag id ^ "succeeded:\n" ^ msg))
d4bb776874b8 count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents: 32567
diff changeset
   493
        )
d4bb776874b8 count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents: 32567
diff changeset
   494
    | (NONE, msg) => log (minimize_tag id ^ "failed: " ^ msg)
32525
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   495
  end
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   496
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   497
40667
b8579f24ce67 make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents: 40627
diff changeset
   498
fun run_reconstructor trivial full m name reconstructor named_thms id
32567
de411627a985 explicitly export type abbreviations (as usual in SML97);
wenzelm
parents: 32564
diff changeset
   499
    ({pre=st, timeout, log, pos, ...}: Mirabelle.run_args) =
32525
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   500
  let
40667
b8579f24ce67 make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents: 40627
diff changeset
   501
    fun do_reconstructor thms ctxt =
41154
5ccc40f679d8 honor "metisFT" in Mirabelle
blanchet
parents: 41138
diff changeset
   502
      (if !reconstructor = "smt" then
5ccc40f679d8 honor "metisFT" in Mirabelle
blanchet
parents: 41138
diff changeset
   503
         SMT_Solver.smt_tac
5ccc40f679d8 honor "metisFT" in Mirabelle
blanchet
parents: 41138
diff changeset
   504
       else if full orelse !reconstructor = "metisFT" then
5ccc40f679d8 honor "metisFT" in Mirabelle
blanchet
parents: 41138
diff changeset
   505
         Metis_Tactics.metisFT_tac
5ccc40f679d8 honor "metisFT" in Mirabelle
blanchet
parents: 41138
diff changeset
   506
       else
5ccc40f679d8 honor "metisFT" in Mirabelle
blanchet
parents: 41138
diff changeset
   507
         Metis_Tactics.metis_tac) ctxt thms
40667
b8579f24ce67 make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents: 40627
diff changeset
   508
    fun apply_reconstructor thms =
b8579f24ce67 make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents: 40627
diff changeset
   509
      Mirabelle.can_apply timeout (do_reconstructor thms) st
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   510
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   511
    fun with_time (false, t) = "failed (" ^ string_of_int t ^ ")"
40667
b8579f24ce67 make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents: 40627
diff changeset
   512
      | with_time (true, t) = (change_data id (inc_reconstructor_success m);
b8579f24ce67 make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents: 40627
diff changeset
   513
          if trivial then ()
b8579f24ce67 make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents: 40627
diff changeset
   514
          else change_data id (inc_reconstructor_nontriv_success m);
b8579f24ce67 make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents: 40627
diff changeset
   515
          change_data id (inc_reconstructor_lemmas m (length named_thms));
b8579f24ce67 make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents: 40627
diff changeset
   516
          change_data id (inc_reconstructor_time m t);
b8579f24ce67 make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents: 40627
diff changeset
   517
          change_data id (inc_reconstructor_posns m (pos, trivial));
b8579f24ce67 make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents: 40627
diff changeset
   518
          if name = "proof" then change_data id (inc_reconstructor_proofs m)
b8579f24ce67 make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents: 40627
diff changeset
   519
          else ();
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   520
          "succeeded (" ^ string_of_int t ^ ")")
40667
b8579f24ce67 make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents: 40627
diff changeset
   521
    fun timed_reconstructor thms =
b8579f24ce67 make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents: 40627
diff changeset
   522
      (with_time (Mirabelle.cpu_time apply_reconstructor thms), true)
b8579f24ce67 make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents: 40627
diff changeset
   523
      handle TimeLimit.TimeOut => (change_data id (inc_reconstructor_timeout m);
34052
b2e6245fb3da only invoke metisFT if metis failed
boehmes
parents: 34035
diff changeset
   524
               ("timeout", false))
b2e6245fb3da only invoke metisFT if metis failed
boehmes
parents: 34035
diff changeset
   525
           | ERROR msg => ("error: " ^ msg, false)
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   526
32525
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   527
    val _ = log separator
40667
b8579f24ce67 make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents: 40627
diff changeset
   528
    val _ = change_data id (inc_reconstructor_calls m)
b8579f24ce67 make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents: 40627
diff changeset
   529
    val _ = if trivial then ()
b8579f24ce67 make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents: 40627
diff changeset
   530
            else change_data id (inc_reconstructor_nontriv_calls m)
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   531
  in
32525
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   532
    maps snd named_thms
40667
b8579f24ce67 make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents: 40627
diff changeset
   533
    |> timed_reconstructor
b8579f24ce67 make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents: 40627
diff changeset
   534
    |>> log o prefix (reconstructor_tag reconstructor id)
34052
b2e6245fb3da only invoke metisFT if metis failed
boehmes
parents: 34035
diff changeset
   535
    |> snd
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   536
  end
32385
594890623c46 split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff changeset
   537
41276
285aea0c153c two layers of timeouts seem to be less reliable than a single layer
blanchet
parents: 41275
diff changeset
   538
val try_timeout = seconds 5.0
39337
ffa577c0bbfa keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents: 39321
diff changeset
   539
34035
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   540
fun sledgehammer_action args id (st as {pre, name, ...}: Mirabelle.run_args) =
35592
768d17f54125 use regular Proof.goal (which is what methods usually see) and prevent sledgehammer from crashing;
wenzelm
parents: 34052
diff changeset
   541
  let val goal = Thm.major_prem_of (#goal (Proof.goal pre)) in
768d17f54125 use regular Proof.goal (which is what methods usually see) and prevent sledgehammer from crashing;
wenzelm
parents: 34052
diff changeset
   542
    if can Logic.dest_conjunction goal orelse can Logic.dest_equals goal
768d17f54125 use regular Proof.goal (which is what methods usually see) and prevent sledgehammer from crashing;
wenzelm
parents: 34052
diff changeset
   543
    then () else
768d17f54125 use regular Proof.goal (which is what methods usually see) and prevent sledgehammer from crashing;
wenzelm
parents: 34052
diff changeset
   544
    let
40667
b8579f24ce67 make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents: 40627
diff changeset
   545
      val reconstructor = Unsynchronized.ref ""
38700
fcb0fe4c2f27 make Mirabelle happy
blanchet
parents: 38590
diff changeset
   546
      val named_thms =
38752
6628adcae4a7 consider "locality" when assigning weights to facts
blanchet
parents: 38700
diff changeset
   547
        Unsynchronized.ref (NONE : ((string * locality) * thm list) list option)
35592
768d17f54125 use regular Proof.goal (which is what methods usually see) and prevent sledgehammer from crashing;
wenzelm
parents: 34052
diff changeset
   548
      val minimize = AList.defined (op =) args minimizeK
768d17f54125 use regular Proof.goal (which is what methods usually see) and prevent sledgehammer from crashing;
wenzelm
parents: 34052
diff changeset
   549
      val metis_ft = AList.defined (op =) args metis_ftK
41276
285aea0c153c two layers of timeouts seem to be less reliable than a single layer
blanchet
parents: 41275
diff changeset
   550
      val trivial = Try.invoke_try (SOME try_timeout) pre
285aea0c153c two layers of timeouts seem to be less reliable than a single layer
blanchet
parents: 41275
diff changeset
   551
        handle TimeLimit.TimeOut => false
40667
b8579f24ce67 make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents: 40627
diff changeset
   552
      fun apply_reconstructor m1 m2 =
35592
768d17f54125 use regular Proof.goal (which is what methods usually see) and prevent sledgehammer from crashing;
wenzelm
parents: 34052
diff changeset
   553
        if metis_ft
34052
b2e6245fb3da only invoke metisFT if metis failed
boehmes
parents: 34035
diff changeset
   554
        then
40667
b8579f24ce67 make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents: 40627
diff changeset
   555
          if not (Mirabelle.catch_result (reconstructor_tag reconstructor) false
b8579f24ce67 make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents: 40627
diff changeset
   556
              (run_reconstructor trivial false m1 name reconstructor
b8579f24ce67 make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents: 40627
diff changeset
   557
                   (these (!named_thms))) id st)
35592
768d17f54125 use regular Proof.goal (which is what methods usually see) and prevent sledgehammer from crashing;
wenzelm
parents: 34052
diff changeset
   558
          then
40667
b8579f24ce67 make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents: 40627
diff changeset
   559
            (Mirabelle.catch_result (reconstructor_tag reconstructor) false
b8579f24ce67 make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents: 40627
diff changeset
   560
              (run_reconstructor trivial true m2 name reconstructor
b8579f24ce67 make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents: 40627
diff changeset
   561
                   (these (!named_thms))) id st; ())
35592
768d17f54125 use regular Proof.goal (which is what methods usually see) and prevent sledgehammer from crashing;
wenzelm
parents: 34052
diff changeset
   562
          else ()
768d17f54125 use regular Proof.goal (which is what methods usually see) and prevent sledgehammer from crashing;
wenzelm
parents: 34052
diff changeset
   563
        else
40667
b8579f24ce67 make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents: 40627
diff changeset
   564
          (Mirabelle.catch_result (reconstructor_tag reconstructor) false
b8579f24ce67 make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents: 40627
diff changeset
   565
            (run_reconstructor trivial false m1 name reconstructor
b8579f24ce67 make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents: 40627
diff changeset
   566
                 (these (!named_thms))) id st; ())
35592
768d17f54125 use regular Proof.goal (which is what methods usually see) and prevent sledgehammer from crashing;
wenzelm
parents: 34052
diff changeset
   567
    in 
768d17f54125 use regular Proof.goal (which is what methods usually see) and prevent sledgehammer from crashing;
wenzelm
parents: 34052
diff changeset
   568
      change_data id (set_mini minimize);
40667
b8579f24ce67 make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents: 40627
diff changeset
   569
      Mirabelle.catch sh_tag (run_sledgehammer trivial args reconstructor
b8579f24ce67 make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents: 40627
diff changeset
   570
                                               named_thms) id st;
35592
768d17f54125 use regular Proof.goal (which is what methods usually see) and prevent sledgehammer from crashing;
wenzelm
parents: 34052
diff changeset
   571
      if is_some (!named_thms)
32612
76dddd260d2f restructured code
nipkow
parents: 32609
diff changeset
   572
      then
40667
b8579f24ce67 make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents: 40627
diff changeset
   573
       (apply_reconstructor Unminimized UnminimizedFT;
35592
768d17f54125 use regular Proof.goal (which is what methods usually see) and prevent sledgehammer from crashing;
wenzelm
parents: 34052
diff changeset
   574
        if minimize andalso not (null (these (!named_thms)))
768d17f54125 use regular Proof.goal (which is what methods usually see) and prevent sledgehammer from crashing;
wenzelm
parents: 34052
diff changeset
   575
        then
40667
b8579f24ce67 make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents: 40627
diff changeset
   576
         (Mirabelle.catch minimize_tag
b8579f24ce67 make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents: 40627
diff changeset
   577
              (run_minimize args reconstructor named_thms) id st;
b8579f24ce67 make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents: 40627
diff changeset
   578
          apply_reconstructor Minimized MinimizedFT)
35592
768d17f54125 use regular Proof.goal (which is what methods usually see) and prevent sledgehammer from crashing;
wenzelm
parents: 34052
diff changeset
   579
        else ())
768d17f54125 use regular Proof.goal (which is what methods usually see) and prevent sledgehammer from crashing;
wenzelm
parents: 34052
diff changeset
   580
      else ()
768d17f54125 use regular Proof.goal (which is what methods usually see) and prevent sledgehammer from crashing;
wenzelm
parents: 34052
diff changeset
   581
    end
32818
6c91e668b15e record max lemmas used
nipkow
parents: 32676
diff changeset
   582
  end
32385
594890623c46 split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff changeset
   583
32511
43d2ac4aa2de added option full_typed for sledgehammer action
boehmes
parents: 32510
diff changeset
   584
fun invoke args =
32515
e7c0d3c0494a Mirabelle: actions are responsible for catching exceptions and producing suitable log messages (makes log message uniform),
boehmes
parents: 32511
diff changeset
   585
  let
36373
66af0a49de39 move some sledgehammer stuff out of "atp_manager.ML"
blanchet
parents: 36294
diff changeset
   586
    val _ = Sledgehammer_Isar.full_types := AList.defined (op =) args full_typesK
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   587
  in Mirabelle.register (init, sledgehammer_action args, done) end
32385
594890623c46 split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff changeset
   588
594890623c46 split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff changeset
   589
end