src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
author blanchet
Fri, 22 Oct 2010 11:11:34 +0200
changeset 40062 cfaebaa8588f
parent 40061 71cc5aac8b76
child 40063 d086e3699e78
permissions -rw-r--r--
make Sledgehammer minimizer fully work with SMT
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"
32574
719426c9e1eb added hard timeout for sledgehammer based on elapsed time (no need to trust ATP's timeout handling);
boehmes
parents: 32571
diff changeset
    10
val prover_hard_timeoutK = "prover_hard_timeout"
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    11
val keepK = "keep"
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    12
val full_typesK = "full_types"
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): "
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    19
fun metis_tag id = "#" ^ string_of_int id ^ " metis (sledgehammer): "
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    20
32525
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
    21
val separator = "-----"
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
    22
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    23
32549
338ccfd37f67 minimization: comparing w/ and w/o.
nipkow
parents: 32541
diff changeset
    24
datatype sh_data = ShData of {
338ccfd37f67 minimization: comparing w/ and w/o.
nipkow
parents: 32541
diff changeset
    25
  calls: int,
338ccfd37f67 minimization: comparing w/ and w/o.
nipkow
parents: 32541
diff changeset
    26
  success: int,
39337
ffa577c0bbfa keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents: 39321
diff changeset
    27
  nontriv_calls: int,
ffa577c0bbfa keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents: 39321
diff changeset
    28
  nontriv_success: int,
32585
e788b33dd2b4 revised lemma counting
nipkow
parents: 32574
diff changeset
    29
  lemmas: int,
32818
6c91e668b15e record max lemmas used
nipkow
parents: 32676
diff changeset
    30
  max_lems: int,
32549
338ccfd37f67 minimization: comparing w/ and w/o.
nipkow
parents: 32541
diff changeset
    31
  time_isa: int,
40062
cfaebaa8588f make Sledgehammer minimizer fully work with SMT
blanchet
parents: 40061
diff changeset
    32
  time_prover: int,
cfaebaa8588f make Sledgehammer minimizer fully work with SMT
blanchet
parents: 40061
diff changeset
    33
  time_prover_fail: int}
32549
338ccfd37f67 minimization: comparing w/ and w/o.
nipkow
parents: 32541
diff changeset
    34
338ccfd37f67 minimization: comparing w/ and w/o.
nipkow
parents: 32541
diff changeset
    35
datatype me_data = MeData of {
338ccfd37f67 minimization: comparing w/ and w/o.
nipkow
parents: 32541
diff changeset
    36
  calls: int,
338ccfd37f67 minimization: comparing w/ and w/o.
nipkow
parents: 32541
diff changeset
    37
  success: int,
39337
ffa577c0bbfa keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents: 39321
diff changeset
    38
  nontriv_calls: int,
ffa577c0bbfa keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents: 39321
diff changeset
    39
  nontriv_success: int,
32676
b1c85a117dec record how many "proof"s are solved by s/h
nipkow
parents: 32612
diff changeset
    40
  proofs: int,
32549
338ccfd37f67 minimization: comparing w/ and w/o.
nipkow
parents: 32541
diff changeset
    41
  time: int,
32550
d57c7a2d927c logging number of metis lemmas
nipkow
parents: 32549
diff changeset
    42
  timeout: int,
32990
717680b14041 added sums of squares for standard deviation
nipkow
parents: 32868
diff changeset
    43
  lemmas: int * int * int,
39341
d2b981a0429a indicate triviality in the list of proved things
blanchet
parents: 39340
diff changeset
    44
  posns: (Position.T * bool) list
32550
d57c7a2d927c logging number of metis lemmas
nipkow
parents: 32549
diff changeset
    45
  }
32549
338ccfd37f67 minimization: comparing w/ and w/o.
nipkow
parents: 32541
diff changeset
    46
32571
d4bb776874b8 count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents: 32567
diff changeset
    47
datatype min_data = MinData of {
32609
2f3e7a92b522 modified minimization log
nipkow
parents: 32607
diff changeset
    48
  succs: int,
35866
513074557e06 move the Sledgehammer Isar commands together into one file;
blanchet
parents: 35830
diff changeset
    49
  ab_ratios: int
32571
d4bb776874b8 count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents: 32567
diff changeset
    50
  }
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    51
32818
6c91e668b15e record max lemmas used
nipkow
parents: 32676
diff changeset
    52
fun make_sh_data
39337
ffa577c0bbfa keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents: 39321
diff changeset
    53
      (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
    54
       time_prover,time_prover_fail) =
39337
ffa577c0bbfa keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents: 39321
diff changeset
    55
  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
    56
         nontriv_success=nontriv_success, lemmas=lemmas, max_lems=max_lems,
40062
cfaebaa8588f make Sledgehammer minimizer fully work with SMT
blanchet
parents: 40061
diff changeset
    57
         time_isa=time_isa, time_prover=time_prover,
cfaebaa8588f make Sledgehammer minimizer fully work with SMT
blanchet
parents: 40061
diff changeset
    58
         time_prover_fail=time_prover_fail}
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    59
35866
513074557e06 move the Sledgehammer Isar commands together into one file;
blanchet
parents: 35830
diff changeset
    60
fun make_min_data (succs, ab_ratios) =
513074557e06 move the Sledgehammer Isar commands together into one file;
blanchet
parents: 35830
diff changeset
    61
  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
    62
39337
ffa577c0bbfa keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents: 39321
diff changeset
    63
fun make_me_data (calls,success,nontriv_calls,nontriv_success,proofs,time,
ffa577c0bbfa keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents: 39321
diff changeset
    64
                  timeout,lemmas,posns) =
ffa577c0bbfa keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents: 39321
diff changeset
    65
  MeData{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
    66
         nontriv_success=nontriv_success, proofs=proofs, time=time,
32990
717680b14041 added sums of squares for standard deviation
nipkow
parents: 32868
diff changeset
    67
         timeout=timeout, lemmas=lemmas, posns=posns}
32549
338ccfd37f67 minimization: comparing w/ and w/o.
nipkow
parents: 32541
diff changeset
    68
39337
ffa577c0bbfa keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents: 39321
diff changeset
    69
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
    70
val empty_min_data = make_min_data (0, 0)
39337
ffa577c0bbfa keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents: 39321
diff changeset
    71
val empty_me_data = make_me_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
    72
39337
ffa577c0bbfa keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents: 39321
diff changeset
    73
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
    74
                              lemmas, max_lems, time_isa,
40062
cfaebaa8588f make Sledgehammer minimizer fully work with SMT
blanchet
parents: 40061
diff changeset
    75
  time_prover, time_prover_fail}) = (calls, success, nontriv_calls,
cfaebaa8588f make Sledgehammer minimizer fully work with SMT
blanchet
parents: 40061
diff changeset
    76
  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
    77
35866
513074557e06 move the Sledgehammer Isar commands together into one file;
blanchet
parents: 35830
diff changeset
    78
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
    79
39337
ffa577c0bbfa keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents: 39321
diff changeset
    80
fun tuple_of_me_data (MeData {calls, success, nontriv_calls, nontriv_success,
ffa577c0bbfa keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents: 39321
diff changeset
    81
  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
    82
  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
    83
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
datatype metis = Unminimized | Minimized | UnminimizedFT | MinimizedFT
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
    86
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
    87
datatype data = Data of {
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
    88
  sh: sh_data,
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
    89
  min: min_data,
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
    90
  me_u: me_data, (* metis with unminimized set of lemmas *)
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
    91
  me_m: me_data, (* metis with minimized set of lemmas *)
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
    92
  me_uft: me_data, (* metis with unminimized set of lemmas and fully-typed *)
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
    93
  me_mft: me_data, (* metis with minimized set of lemmas and fully-typed *)
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
    94
  mini: bool   (* with minimization *)
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
    95
  }
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    96
34035
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
    97
fun make_data (sh, min, me_u, me_m, me_uft, me_mft, mini) =
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
    98
  Data {sh=sh, min=min, me_u=me_u, me_m=me_m, me_uft=me_uft, me_mft=me_mft,
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
    99
    mini=mini}
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   100
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   101
val empty_data = make_data (empty_sh_data, empty_min_data,
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   102
  empty_me_data, empty_me_data, empty_me_data, empty_me_data, false)
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   103
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   104
fun map_sh_data f (Data {sh, min, me_u, me_m, me_uft, me_mft, mini}) =
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   105
  let val sh' = make_sh_data (f (tuple_of_sh_data sh))
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   106
  in make_data (sh', min, me_u, me_m, me_uft, me_mft, mini) end
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   107
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   108
fun map_min_data f (Data {sh, min, me_u, me_m, me_uft, me_mft, mini}) =
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   109
  let val min' = make_min_data (f (tuple_of_min_data min))
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   110
  in make_data (sh, min', me_u, me_m, me_uft, me_mft, mini) end
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   111
34035
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   112
fun map_me_data f m (Data {sh, min, me_u, me_m, me_uft, me_mft, mini}) =
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   113
  let
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   114
    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
   115
      | 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
   116
      | 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
   117
      | 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
   118
34035
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   119
    val f' = make_me_data o f o tuple_of_me_data
32571
d4bb776874b8 count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents: 32567
diff changeset
   120
34035
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   121
    val (me_u', me_m', me_uft', me_mft') =
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   122
      map_me f' m (me_u, me_m, me_uft, me_mft)
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   123
  in make_data (sh, min, me_u', me_m', me_uft', me_mft', mini) end
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   124
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   125
fun set_mini mini (Data {sh, min, me_u, me_m, me_uft, me_mft, ...}) =
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   126
  make_data (sh, min, me_u, me_m, me_uft, me_mft, mini)
32990
717680b14041 added sums of squares for standard deviation
nipkow
parents: 32868
diff changeset
   127
717680b14041 added sums of squares for standard deviation
nipkow
parents: 32868
diff changeset
   128
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
   129
32818
6c91e668b15e record max lemmas used
nipkow
parents: 32676
diff changeset
   130
val inc_sh_calls =  map_sh_data
40062
cfaebaa8588f make Sledgehammer minimizer fully work with SMT
blanchet
parents: 40061
diff changeset
   131
  (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
   132
    => (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
   133
32818
6c91e668b15e record max lemmas used
nipkow
parents: 32676
diff changeset
   134
val inc_sh_success = map_sh_data
40062
cfaebaa8588f make Sledgehammer minimizer fully work with SMT
blanchet
parents: 40061
diff changeset
   135
  (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
   136
    => (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
   137
ffa577c0bbfa keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents: 39321
diff changeset
   138
val inc_sh_nontriv_calls =  map_sh_data
40062
cfaebaa8588f make Sledgehammer minimizer fully work with SMT
blanchet
parents: 40061
diff changeset
   139
  (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
   140
    => (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
   141
ffa577c0bbfa keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents: 39321
diff changeset
   142
val inc_sh_nontriv_success = map_sh_data
40062
cfaebaa8588f make Sledgehammer minimizer fully work with SMT
blanchet
parents: 40061
diff changeset
   143
  (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
   144
    => (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
   145
32818
6c91e668b15e record max lemmas used
nipkow
parents: 32676
diff changeset
   146
fun inc_sh_lemmas n = map_sh_data
40062
cfaebaa8588f make Sledgehammer minimizer fully work with SMT
blanchet
parents: 40061
diff changeset
   147
  (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
   148
    => (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
   149
32818
6c91e668b15e record max lemmas used
nipkow
parents: 32676
diff changeset
   150
fun inc_sh_max_lems n = map_sh_data
40062
cfaebaa8588f make Sledgehammer minimizer fully work with SMT
blanchet
parents: 40061
diff changeset
   151
  (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
   152
    => (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
   153
32818
6c91e668b15e record max lemmas used
nipkow
parents: 32676
diff changeset
   154
fun inc_sh_time_isa t = map_sh_data
40062
cfaebaa8588f make Sledgehammer minimizer fully work with SMT
blanchet
parents: 40061
diff changeset
   155
  (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
   156
    => (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
   157
40062
cfaebaa8588f make Sledgehammer minimizer fully work with SMT
blanchet
parents: 40061
diff changeset
   158
fun inc_sh_time_prover t = map_sh_data
cfaebaa8588f make Sledgehammer minimizer fully work with SMT
blanchet
parents: 40061
diff changeset
   159
  (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
   160
    => (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
   161
40062
cfaebaa8588f make Sledgehammer minimizer fully work with SMT
blanchet
parents: 40061
diff changeset
   162
fun inc_sh_time_prover_fail t = map_sh_data
cfaebaa8588f make Sledgehammer minimizer fully work with SMT
blanchet
parents: 40061
diff changeset
   163
  (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
   164
    => (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
   165
32818
6c91e668b15e record max lemmas used
nipkow
parents: 32676
diff changeset
   166
val inc_min_succs = map_min_data
35866
513074557e06 move the Sledgehammer Isar commands together into one file;
blanchet
parents: 35830
diff changeset
   167
  (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
   168
32818
6c91e668b15e record max lemmas used
nipkow
parents: 32676
diff changeset
   169
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
   170
  (fn (succs, ab_ratios) => (succs, ab_ratios+r))
32549
338ccfd37f67 minimization: comparing w/ and w/o.
nipkow
parents: 32541
diff changeset
   171
32551
421323205efd position information is now passed to all actions;
nipkow
parents: 32550
diff changeset
   172
val inc_metis_calls = map_me_data
39337
ffa577c0bbfa keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents: 39321
diff changeset
   173
  (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
   174
    => (calls + 1, success, nontriv_calls, nontriv_success, proofs, time, timeout, lemmas,posns))
32533
9735013cec72 tuned stats
nipkow
parents: 32526
diff changeset
   175
32551
421323205efd position information is now passed to all actions;
nipkow
parents: 32550
diff changeset
   176
val inc_metis_success = map_me_data
39337
ffa577c0bbfa keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents: 39321
diff changeset
   177
  (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
   178
    => (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
   179
ffa577c0bbfa keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents: 39321
diff changeset
   180
val inc_metis_nontriv_calls = map_me_data
ffa577c0bbfa keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents: 39321
diff changeset
   181
  (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
   182
    => (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
   183
ffa577c0bbfa keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents: 39321
diff changeset
   184
val inc_metis_nontriv_success = map_me_data
ffa577c0bbfa keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents: 39321
diff changeset
   185
  (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
   186
    => (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
   187
b1c85a117dec record how many "proof"s are solved by s/h
nipkow
parents: 32612
diff changeset
   188
val inc_metis_proofs = map_me_data
39337
ffa577c0bbfa keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents: 39321
diff changeset
   189
  (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
   190
    => (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
   191
34035
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   192
fun inc_metis_time m t = map_me_data
39337
ffa577c0bbfa keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents: 39321
diff changeset
   193
 (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
   194
  => (calls, success, nontriv_calls, nontriv_success, proofs, time + t, timeout, lemmas,posns)) m
32536
ac56c62758d3 tuned stats
nipkow
parents: 32533
diff changeset
   195
32551
421323205efd position information is now passed to all actions;
nipkow
parents: 32550
diff changeset
   196
val inc_metis_timeout = map_me_data
39337
ffa577c0bbfa keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents: 39321
diff changeset
   197
  (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
   198
    => (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
   199
34035
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   200
fun inc_metis_lemmas m n = map_me_data
39337
ffa577c0bbfa keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents: 39321
diff changeset
   201
  (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
   202
    => (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
   203
34035
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   204
fun inc_metis_posns m pos = map_me_data
39337
ffa577c0bbfa keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents: 39321
diff changeset
   205
  (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
   206
    => (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
   207
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   208
local
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
val str = string_of_int
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   211
val str3 = Real.fmt (StringCvt.FIX (SOME 3))
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   212
fun percentage a b = string_of_int (a * 100 div b)
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   213
fun time t = Real.fromInt t / 1000.0
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   214
fun avg_time t n =
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   215
  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
   216
34035
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   217
fun log_sh_data log
40062
cfaebaa8588f make Sledgehammer minimizer fully work with SMT
blanchet
parents: 40061
diff changeset
   218
    (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
   219
 (log ("Total number of sledgehammer calls: " ^ str calls);
6c91e668b15e record max lemmas used
nipkow
parents: 32676
diff changeset
   220
  log ("Number of successful sledgehammer calls: " ^ str success);
6c91e668b15e record max lemmas used
nipkow
parents: 32676
diff changeset
   221
  log ("Number of sledgehammer lemmas: " ^ str lemmas);
6c91e668b15e record max lemmas used
nipkow
parents: 32676
diff changeset
   222
  log ("Max number of sledgehammer lemmas: " ^ str max_lems);
6c91e668b15e record max lemmas used
nipkow
parents: 32676
diff changeset
   223
  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
   224
  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
   225
  log ("Number of successful nontrivial sledgehammer calls: " ^ str nontriv_success);
32818
6c91e668b15e record max lemmas used
nipkow
parents: 32676
diff changeset
   226
  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
   227
  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
   228
  log ("Total time for failed sledgehammer calls (ATP): " ^ str3 (time time_prover_fail));
32536
ac56c62758d3 tuned stats
nipkow
parents: 32533
diff changeset
   229
  log ("Average time for sledgehammer calls (Isabelle): " ^
32818
6c91e668b15e record max lemmas used
nipkow
parents: 32676
diff changeset
   230
    str3 (avg_time time_isa calls));
32533
9735013cec72 tuned stats
nipkow
parents: 32526
diff changeset
   231
  log ("Average time for successful sledgehammer calls (ATP): " ^
40062
cfaebaa8588f make Sledgehammer minimizer fully work with SMT
blanchet
parents: 40061
diff changeset
   232
    str3 (avg_time time_prover success));
32536
ac56c62758d3 tuned stats
nipkow
parents: 32533
diff changeset
   233
  log ("Average time for failed sledgehammer calls (ATP): " ^
40062
cfaebaa8588f make Sledgehammer minimizer fully work with SMT
blanchet
parents: 40061
diff changeset
   234
    str3 (avg_time time_prover_fail (calls - success)))
32533
9735013cec72 tuned stats
nipkow
parents: 32526
diff changeset
   235
  )
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   236
32551
421323205efd position information is now passed to all actions;
nipkow
parents: 32550
diff changeset
   237
39341
d2b981a0429a indicate triviality in the list of proved things
blanchet
parents: 39340
diff changeset
   238
fun str_of_pos (pos, triv) =
32551
421323205efd position information is now passed to all actions;
nipkow
parents: 32550
diff changeset
   239
  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
   240
  in
d2b981a0429a indicate triviality in the list of proved things
blanchet
parents: 39340
diff changeset
   241
    str0 (Position.line_of pos) ^ ":" ^ str0 (Position.column_of pos) ^
d2b981a0429a indicate triviality in the list of proved things
blanchet
parents: 39340
diff changeset
   242
    (if triv then "[T]" else "")
d2b981a0429a indicate triviality in the list of proved things
blanchet
parents: 39340
diff changeset
   243
  end
32551
421323205efd position information is now passed to all actions;
nipkow
parents: 32550
diff changeset
   244
34035
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   245
fun log_me_data log tag sh_calls (metis_calls, metis_success,
39337
ffa577c0bbfa keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents: 39321
diff changeset
   246
     metis_nontriv_calls, metis_nontriv_success,
ffa577c0bbfa keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents: 39321
diff changeset
   247
     metis_proofs, metis_time, metis_timeout, (lemmas, lems_sos, lems_max),
34035
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   248
    metis_posns) =
32549
338ccfd37f67 minimization: comparing w/ and w/o.
nipkow
parents: 32541
diff changeset
   249
 (log ("Total number of " ^ tag ^ "metis calls: " ^ str metis_calls);
32740
9dd0a2f83429 explicit indication of Unsynchronized.ref;
wenzelm
parents: 32676
diff changeset
   250
  log ("Number of successful " ^ tag ^ "metis calls: " ^ str metis_success ^
9dd0a2f83429 explicit indication of Unsynchronized.ref;
wenzelm
parents: 32676
diff changeset
   251
    " (proof: " ^ str metis_proofs ^ ")");
32549
338ccfd37f67 minimization: comparing w/ and w/o.
nipkow
parents: 32541
diff changeset
   252
  log ("Number of " ^ tag ^ "metis timeouts: " ^ str metis_timeout);
32533
9735013cec72 tuned stats
nipkow
parents: 32526
diff changeset
   253
  log ("Success rate: " ^ percentage metis_success sh_calls ^ "%");
39337
ffa577c0bbfa keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents: 39321
diff changeset
   254
  log ("Total number of nontrivial " ^ tag ^ "metis calls: " ^ str metis_nontriv_calls);
ffa577c0bbfa keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents: 39321
diff changeset
   255
  log ("Number of successful nontrivial " ^ tag ^ "metis calls: " ^ str metis_nontriv_success ^
ffa577c0bbfa keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents: 39321
diff changeset
   256
    " (proof: " ^ str metis_proofs ^ ")");
32990
717680b14041 added sums of squares for standard deviation
nipkow
parents: 32868
diff changeset
   257
  log ("Number of successful " ^ tag ^ "metis lemmas: " ^ str lemmas);
717680b14041 added sums of squares for standard deviation
nipkow
parents: 32868
diff changeset
   258
  log ("SOS of successful " ^ tag ^ "metis lemmas: " ^ str lems_sos);
717680b14041 added sums of squares for standard deviation
nipkow
parents: 32868
diff changeset
   259
  log ("Max number of successful " ^ tag ^ "metis lemmas: " ^ str lems_max);
717680b14041 added sums of squares for standard deviation
nipkow
parents: 32868
diff changeset
   260
  log ("Total time for successful " ^ tag ^ "metis calls: " ^ str3 (time metis_time));
34035
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   261
  log ("Average time for successful " ^ tag ^ "metis calls: " ^
32551
421323205efd position information is now passed to all actions;
nipkow
parents: 32550
diff changeset
   262
    str3 (avg_time metis_time metis_success));
421323205efd position information is now passed to all actions;
nipkow
parents: 32550
diff changeset
   263
  if tag=""
421323205efd position information is now passed to all actions;
nipkow
parents: 32550
diff changeset
   264
  then log ("Proved: " ^ space_implode " " (map str_of_pos metis_posns))
421323205efd position information is now passed to all actions;
nipkow
parents: 32550
diff changeset
   265
  else ()
421323205efd position information is now passed to all actions;
nipkow
parents: 32550
diff changeset
   266
 )
32571
d4bb776874b8 count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents: 32567
diff changeset
   267
35866
513074557e06 move the Sledgehammer Isar commands together into one file;
blanchet
parents: 35830
diff changeset
   268
fun log_min_data log (succs, ab_ratios) =
32609
2f3e7a92b522 modified minimization log
nipkow
parents: 32607
diff changeset
   269
  (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
   270
   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
   271
  )
d4bb776874b8 count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents: 32567
diff changeset
   272
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   273
in
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   274
34035
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   275
fun log_data id log (Data {sh, min, me_u, me_m, me_uft, me_mft, mini}) =
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   276
  let
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   277
    val ShData {calls=sh_calls, ...} = sh
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   278
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   279
    fun app_if (MeData {calls, ...}) f = if calls > 0 then f () else ()
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   280
    fun log_me tag m =
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   281
      log_me_data log tag sh_calls (tuple_of_me_data m)
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   282
    fun log_metis (tag1, m1) (tag2, m2) = app_if m1 (fn () =>
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   283
      (log_me tag1 m1; log ""; app_if m2 (fn () => log_me tag2 m2)))
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   284
  in
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   285
    if sh_calls > 0
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   286
    then
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   287
     (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
   288
      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
   289
      log "";
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   290
      if not mini
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   291
      then log_metis ("", me_u) ("fully-typed ", me_uft)
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   292
      else
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   293
        app_if me_u (fn () =>
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   294
         (log_metis ("unminimized ", me_u) ("unminimized fully-typed ", me_uft);
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   295
          log "";
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   296
          app_if me_m (fn () =>
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   297
            (log_min_data log (tuple_of_min_data min); log "";
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   298
             log_metis ("", me_m) ("fully-typed ", me_mft))))))
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   299
    else ()
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   300
  end
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   301
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   302
end
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   303
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
(* Warning: we implicitly assume single-threaded execution here! *)
32740
9dd0a2f83429 explicit indication of Unsynchronized.ref;
wenzelm
parents: 32676
diff changeset
   306
val data = Unsynchronized.ref ([] : (int * data) list)
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   307
32740
9dd0a2f83429 explicit indication of Unsynchronized.ref;
wenzelm
parents: 32676
diff changeset
   308
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
   309
fun done id ({log, ...}: Mirabelle.done_args) =
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   310
  AList.lookup (op =) (!data) id
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   311
  |> Option.map (log_data id log)
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   312
  |> K ()
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   313
32740
9dd0a2f83429 explicit indication of Unsynchronized.ref;
wenzelm
parents: 32676
diff changeset
   314
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
   315
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   316
40062
cfaebaa8588f make Sledgehammer minimizer fully work with SMT
blanchet
parents: 40061
diff changeset
   317
fun get_prover thy args =
33016
b73b74fe23c3 proper exceptions instead of unhandled partiality
boehmes
parents: 32991
diff changeset
   318
  let
40062
cfaebaa8588f make Sledgehammer minimizer fully work with SMT
blanchet
parents: 40061
diff changeset
   319
    fun default_prover_name () =
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39494
diff changeset
   320
      hd (#provers (Sledgehammer_Isar.default_params thy []))
33016
b73b74fe23c3 proper exceptions instead of unhandled partiality
boehmes
parents: 32991
diff changeset
   321
      handle Empty => error "No ATP available."
40062
cfaebaa8588f make Sledgehammer minimizer fully work with SMT
blanchet
parents: 40061
diff changeset
   322
    fun get_prover name = (name, Sledgehammer.get_prover thy name)
33016
b73b74fe23c3 proper exceptions instead of unhandled partiality
boehmes
parents: 32991
diff changeset
   323
  in
b73b74fe23c3 proper exceptions instead of unhandled partiality
boehmes
parents: 32991
diff changeset
   324
    (case AList.lookup (op =) args proverK of
40062
cfaebaa8588f make Sledgehammer minimizer fully work with SMT
blanchet
parents: 40061
diff changeset
   325
      SOME name => get_prover name
cfaebaa8588f make Sledgehammer minimizer fully work with SMT
blanchet
parents: 40061
diff changeset
   326
    | NONE => get_prover (default_prover_name ()))
33016
b73b74fe23c3 proper exceptions instead of unhandled partiality
boehmes
parents: 32991
diff changeset
   327
  end
32525
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   328
38988
483879af0643 finished renaming
blanchet
parents: 38826
diff changeset
   329
type locality = Sledgehammer_Filter.locality
38752
6628adcae4a7 consider "locality" when assigning weights to facts
blanchet
parents: 38700
diff changeset
   330
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   331
local
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   332
32536
ac56c62758d3 tuned stats
nipkow
parents: 32533
diff changeset
   333
datatype sh_result =
38752
6628adcae4a7 consider "locality" when assigning weights to facts
blanchet
parents: 38700
diff changeset
   334
  SH_OK of int * int * (string * locality) list |
32536
ac56c62758d3 tuned stats
nipkow
parents: 32533
diff changeset
   335
  SH_FAIL of int * int |
ac56c62758d3 tuned stats
nipkow
parents: 32533
diff changeset
   336
  SH_ERROR
ac56c62758d3 tuned stats
nipkow
parents: 32533
diff changeset
   337
38998
f11a861e0061 share the relevance filter among the provers
blanchet
parents: 38988
diff changeset
   338
fun run_sh prover_name prover hard_timeout timeout dir st =
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   339
  let
38998
f11a861e0061 share the relevance filter among the provers
blanchet
parents: 38988
diff changeset
   340
    val {context = ctxt, facts = chained_ths, goal} = Proof.goal st
35971
4f24a4e9af4a make Mirabelle happy again
blanchet
parents: 35871
diff changeset
   341
    val thy = ProofContext.theory_of ctxt
38998
f11a861e0061 share the relevance filter among the provers
blanchet
parents: 38988
diff changeset
   342
    val i = 1
39321
23951979a362 make Mirabelle happy
blanchet
parents: 39005
diff changeset
   343
    fun change_dir (SOME dir) = Config.put Sledgehammer.dest_dir dir
23951979a362 make Mirabelle happy
blanchet
parents: 39005
diff changeset
   344
      | change_dir NONE = I
23951979a362 make Mirabelle happy
blanchet
parents: 39005
diff changeset
   345
    val st' =
23951979a362 make Mirabelle happy
blanchet
parents: 39005
diff changeset
   346
      st |> Proof.map_context
23951979a362 make Mirabelle happy
blanchet
parents: 39005
diff changeset
   347
                (change_dir dir
23951979a362 make Mirabelle happy
blanchet
parents: 39005
diff changeset
   348
                 #> Config.put Sledgehammer.measure_run_time true)
38998
f11a861e0061 share the relevance filter among the provers
blanchet
parents: 38988
diff changeset
   349
    val params as {full_types, relevance_thresholds, max_relevant, ...} =
f11a861e0061 share the relevance filter among the provers
blanchet
parents: 38988
diff changeset
   350
      Sledgehammer_Isar.default_params thy
f11a861e0061 share the relevance filter among the provers
blanchet
parents: 38988
diff changeset
   351
          [("timeout", Int.toString timeout ^ " s")]
f11a861e0061 share the relevance filter among the provers
blanchet
parents: 38988
diff changeset
   352
    val relevance_override = {add = [], del = [], only = false}
40062
cfaebaa8588f make Sledgehammer minimizer fully work with SMT
blanchet
parents: 40061
diff changeset
   353
    val default_max_relevant =
cfaebaa8588f make Sledgehammer minimizer fully work with SMT
blanchet
parents: 40061
diff changeset
   354
      if member (op =) Sledgehammer.smt_prover_names prover_name then
cfaebaa8588f make Sledgehammer minimizer fully work with SMT
blanchet
parents: 40061
diff changeset
   355
        Sledgehammer.smt_default_max_relevant
cfaebaa8588f make Sledgehammer minimizer fully work with SMT
blanchet
parents: 40061
diff changeset
   356
      else
cfaebaa8588f make Sledgehammer minimizer fully work with SMT
blanchet
parents: 40061
diff changeset
   357
        #default_max_relevant (ATP_Systems.get_atp thy prover_name)
38998
f11a861e0061 share the relevance filter among the provers
blanchet
parents: 38988
diff changeset
   358
    val (_, hyp_ts, concl_t) = Sledgehammer_Util.strip_subgoal goal i
f11a861e0061 share the relevance filter among the provers
blanchet
parents: 38988
diff changeset
   359
    val axioms =
f11a861e0061 share the relevance filter among the provers
blanchet
parents: 38988
diff changeset
   360
      Sledgehammer_Filter.relevant_facts ctxt full_types relevance_thresholds
f11a861e0061 share the relevance filter among the provers
blanchet
parents: 38988
diff changeset
   361
          (the_default default_max_relevant max_relevant)
f11a861e0061 share the relevance filter among the provers
blanchet
parents: 38988
diff changeset
   362
          relevance_override chained_ths hyp_ts concl_t
39004
f1b465f889b5 translate the axioms to FOF once and for all ATPs
blanchet
parents: 39003
diff changeset
   363
    val problem =
39321
23951979a362 make Mirabelle happy
blanchet
parents: 39005
diff changeset
   364
      {state = st', goal = goal, subgoal = i,
40061
71cc5aac8b76 generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents: 40060
diff changeset
   365
       axioms = axioms |> map Sledgehammer.Unprepared, only = true}
32574
719426c9e1eb added hard timeout for sledgehammer based on elapsed time (no need to trust ATP's timeout handling);
boehmes
parents: 32571
diff changeset
   366
    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
   367
      (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
   368
        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
   369
      | SOME secs => TimeLimit.timeLimit (Time.fromSeconds secs))
40062
cfaebaa8588f make Sledgehammer minimizer fully work with SMT
blanchet
parents: 40061
diff changeset
   370
    val ({outcome, message, used_axioms, run_time_in_msecs = SOME time_prover, ...}
40061
71cc5aac8b76 generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents: 40060
diff changeset
   371
         : Sledgehammer.prover_result,
35971
4f24a4e9af4a make Mirabelle happy again
blanchet
parents: 35871
diff changeset
   372
        time_isa) = time_limit (Mirabelle.cpu_time
38103
4339b1acfd4f make Mirabelle happy
blanchet
parents: 38084
diff changeset
   373
                      (prover params (K ""))) problem
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   374
  in
36405
05a8d79eb338 compile
blanchet
parents: 36373
diff changeset
   375
    case outcome of
40062
cfaebaa8588f make Sledgehammer minimizer fully work with SMT
blanchet
parents: 40061
diff changeset
   376
      NONE => (message, SH_OK (time_isa, time_prover, used_axioms))
cfaebaa8588f make Sledgehammer minimizer fully work with SMT
blanchet
parents: 40061
diff changeset
   377
    | SOME _ => (message, SH_FAIL (time_isa, time_prover))
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   378
  end
37994
b04307085a09 make TPTP generator accept full first-order formulas
blanchet
parents: 37631
diff changeset
   379
  handle ERROR msg => ("error: " ^ msg, SH_ERROR)
32574
719426c9e1eb added hard timeout for sledgehammer based on elapsed time (no need to trust ATP's timeout handling);
boehmes
parents: 32571
diff changeset
   380
       | TimeLimit.TimeOut => ("timeout", SH_ERROR)
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   381
32454
a1a5589207ad Mirabelle: proper parsing of theorem names found by sledgehammer, respecting test intervals given along with file names
boehmes
parents: 32452
diff changeset
   382
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
   383
  let
36960
01594f816e3a prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents: 36959
diff changeset
   384
    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
   385
    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
   386
  in
a1a5589207ad Mirabelle: proper parsing of theorem names found by sledgehammer, respecting test intervals given along with file names
boehmes
parents: 32452
diff changeset
   387
    Source.of_string name
a1a5589207ad Mirabelle: proper parsing of theorem names found by sledgehammer, respecting test intervals given along with file names
boehmes
parents: 32452
diff changeset
   388
    |> Symbol.source {do_recover=false}
36959
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 36954
diff changeset
   389
    |> 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
   390
    |> 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
   391
    |> 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
   392
    |> 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
   393
  end
32452
d84edd022efe apply metis with found theorems in case sledgehammer was successful
boehmes
parents: 32434
diff changeset
   394
32498
1132c7c13f36 Mirabelle: actions are responsible for handling exceptions,
boehmes
parents: 32496
diff changeset
   395
in
1132c7c13f36 Mirabelle: actions are responsible for handling exceptions,
boehmes
parents: 32496
diff changeset
   396
39337
ffa577c0bbfa keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents: 39321
diff changeset
   397
fun run_sledgehammer trivial args 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
   398
  let
39340
3998dc0bf82b indicate which goals are trivial
blanchet
parents: 39337
diff changeset
   399
    val triv_str = if trivial then "[T] " else ""
32536
ac56c62758d3 tuned stats
nipkow
parents: 32533
diff changeset
   400
    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
   401
    val _ = if trivial then () else change_data id inc_sh_nontriv_calls
40062
cfaebaa8588f make Sledgehammer minimizer fully work with SMT
blanchet
parents: 40061
diff changeset
   402
    val (prover_name, prover) = get_prover (Proof.theory_of st) args
32525
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   403
    val dir = AList.lookup (op =) args keepK
32541
cea1716eb106 timeout option for ATPs
boehmes
parents: 32536
diff changeset
   404
    val timeout = Mirabelle.get_int_setting args (prover_timeoutK, 30)
32574
719426c9e1eb added hard timeout for sledgehammer based on elapsed time (no need to trust ATP's timeout handling);
boehmes
parents: 32571
diff changeset
   405
    val hard_timeout = AList.lookup (op =) args prover_hard_timeoutK
719426c9e1eb added hard timeout for sledgehammer based on elapsed time (no need to trust ATP's timeout handling);
boehmes
parents: 32571
diff changeset
   406
      |> Option.map (fst o read_int o explode)
38998
f11a861e0061 share the relevance filter among the provers
blanchet
parents: 38988
diff changeset
   407
    val (msg, result) = run_sh prover_name prover hard_timeout timeout dir st
32525
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   408
  in
32536
ac56c62758d3 tuned stats
nipkow
parents: 32533
diff changeset
   409
    case result of
40062
cfaebaa8588f make Sledgehammer minimizer fully work with SMT
blanchet
parents: 40061
diff changeset
   410
      SH_OK (time_isa, time_prover, names) =>
38700
fcb0fe4c2f27 make Mirabelle happy
blanchet
parents: 38590
diff changeset
   411
        let
39377
blanchet
parents: 39366
diff changeset
   412
          fun get_thms (_, Sledgehammer_Filter.Chained) = NONE
38826
f42f425edf24 drop chained facts
blanchet
parents: 38752
diff changeset
   413
            | get_thms (name, loc) =
f42f425edf24 drop chained facts
blanchet
parents: 38752
diff changeset
   414
              SOME ((name, loc), thms_of_name (Proof.context_of st) name)
32525
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   415
        in
32818
6c91e668b15e record max lemmas used
nipkow
parents: 32676
diff changeset
   416
          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
   417
          if trivial then () else change_data id inc_sh_nontriv_success;
32818
6c91e668b15e record max lemmas used
nipkow
parents: 32676
diff changeset
   418
          change_data id (inc_sh_lemmas (length names));
6c91e668b15e record max lemmas used
nipkow
parents: 32676
diff changeset
   419
          change_data id (inc_sh_max_lems (length names));
6c91e668b15e record max lemmas used
nipkow
parents: 32676
diff changeset
   420
          change_data id (inc_sh_time_isa time_isa);
40062
cfaebaa8588f make Sledgehammer minimizer fully work with SMT
blanchet
parents: 40061
diff changeset
   421
          change_data id (inc_sh_time_prover time_prover);
38826
f42f425edf24 drop chained facts
blanchet
parents: 38752
diff changeset
   422
          named_thms := SOME (map_filter get_thms names);
39340
3998dc0bf82b indicate which goals are trivial
blanchet
parents: 39337
diff changeset
   423
          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
   424
            string_of_int time_prover ^ ") [" ^ prover_name ^ "]:\n" ^ msg)
32525
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   425
        end
40062
cfaebaa8588f make Sledgehammer minimizer fully work with SMT
blanchet
parents: 40061
diff changeset
   426
    | SH_FAIL (time_isa, time_prover) =>
32536
ac56c62758d3 tuned stats
nipkow
parents: 32533
diff changeset
   427
        let
ac56c62758d3 tuned stats
nipkow
parents: 32533
diff changeset
   428
          val _ = change_data id (inc_sh_time_isa time_isa)
40062
cfaebaa8588f make Sledgehammer minimizer fully work with SMT
blanchet
parents: 40061
diff changeset
   429
          val _ = change_data id (inc_sh_time_prover_fail time_prover)
39340
3998dc0bf82b indicate which goals are trivial
blanchet
parents: 39337
diff changeset
   430
        in log (sh_tag id ^ triv_str ^ "failed: " ^ msg) end
32536
ac56c62758d3 tuned stats
nipkow
parents: 32533
diff changeset
   431
    | SH_ERROR => log (sh_tag id ^ "failed: " ^ msg)
32525
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   432
  end
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   433
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   434
end
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   435
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   436
36499
7ec5ceef117b make Mirabelle happy
blanchet
parents: 36405
diff changeset
   437
val subgoal_count = Logic.count_prems o prop_of o #goal o Proof.goal
7ec5ceef117b make Mirabelle happy
blanchet
parents: 36405
diff changeset
   438
32567
de411627a985 explicitly export type abbreviations (as usual in SML97);
wenzelm
parents: 32564
diff changeset
   439
fun run_minimize args named_thms id ({pre=st, log, ...}: Mirabelle.run_args) =
32525
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   440
  let
39494
bf7dd4902321 rename "Metis_Clauses" to "Metis_Translate" for consistency with "Sledgehammer_Translate"
blanchet
parents: 39377
diff changeset
   441
    open Metis_Translate
35971
4f24a4e9af4a make Mirabelle happy again
blanchet
parents: 35871
diff changeset
   442
    val thy = Proof.theory_of st
32571
d4bb776874b8 count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents: 32567
diff changeset
   443
    val n0 = length (these (!named_thms))
40062
cfaebaa8588f make Sledgehammer minimizer fully work with SMT
blanchet
parents: 40061
diff changeset
   444
    val (prover_name, _) = get_prover thy args
32525
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   445
    val timeout =
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   446
      AList.lookup (op =) args minimize_timeoutK
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   447
      |> Option.map (fst o read_int o explode)
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   448
      |> the_default 5
38103
4339b1acfd4f make Mirabelle happy
blanchet
parents: 38084
diff changeset
   449
    val params = Sledgehammer_Isar.default_params thy
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39494
diff changeset
   450
      [("provers", prover_name), ("timeout", Int.toString timeout ^ " s")]
37587
466031e057a0 compile
blanchet
parents: 37578
diff changeset
   451
    val minimize =
40061
71cc5aac8b76 generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents: 40060
diff changeset
   452
      Sledgehammer_Minimize.minimize_facts params 1 (subgoal_count st)
32525
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   453
    val _ = log separator
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   454
  in
35971
4f24a4e9af4a make Mirabelle happy again
blanchet
parents: 35871
diff changeset
   455
    case minimize st (these (!named_thms)) of
35871
c93bda4fdf15 remove the iteration counter from Sledgehammer's minimizer
blanchet
parents: 35867
diff changeset
   456
      (SOME named_thms', msg) =>
32609
2f3e7a92b522 modified minimization log
nipkow
parents: 32607
diff changeset
   457
        (change_data id inc_min_succs;
2f3e7a92b522 modified minimization log
nipkow
parents: 32607
diff changeset
   458
         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
   459
         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
   460
         then log (minimize_tag id ^ "already minimal")
d4bb776874b8 count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents: 32567
diff changeset
   461
         else (named_thms := SOME named_thms';
d4bb776874b8 count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents: 32567
diff changeset
   462
               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
   463
        )
d4bb776874b8 count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents: 32567
diff changeset
   464
    | (NONE, msg) => log (minimize_tag id ^ "failed: " ^ msg)
32525
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   465
  end
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   466
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   467
39337
ffa577c0bbfa keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents: 39321
diff changeset
   468
fun run_metis trivial full m name named_thms id
32567
de411627a985 explicitly export type abbreviations (as usual in SML97);
wenzelm
parents: 32564
diff changeset
   469
    ({pre=st, timeout, log, pos, ...}: Mirabelle.run_args) =
32525
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   470
  let
34035
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   471
    fun metis thms ctxt =
35830
d4c4f88f6432 fix Mirabelle after renaming Sledgehammer structures
blanchet
parents: 35592
diff changeset
   472
      if full then Metis_Tactics.metisFT_tac ctxt thms
d4c4f88f6432 fix Mirabelle after renaming Sledgehammer structures
blanchet
parents: 35592
diff changeset
   473
      else Metis_Tactics.metis_tac ctxt thms
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   474
    fun apply_metis thms = Mirabelle.can_apply timeout (metis thms) st
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   475
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   476
    fun with_time (false, t) = "failed (" ^ string_of_int t ^ ")"
34035
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   477
      | with_time (true, t) = (change_data id (inc_metis_success m);
39337
ffa577c0bbfa keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents: 39321
diff changeset
   478
          if trivial then () else change_data id (inc_metis_nontriv_success m);
34035
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   479
          change_data id (inc_metis_lemmas m (length named_thms));
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   480
          change_data id (inc_metis_time m t);
39341
d2b981a0429a indicate triviality in the list of proved things
blanchet
parents: 39340
diff changeset
   481
          change_data id (inc_metis_posns m (pos, trivial));
34035
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   482
          if name = "proof" then change_data id (inc_metis_proofs m) else ();
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   483
          "succeeded (" ^ string_of_int t ^ ")")
34052
b2e6245fb3da only invoke metisFT if metis failed
boehmes
parents: 34035
diff changeset
   484
    fun timed_metis thms =
b2e6245fb3da only invoke metisFT if metis failed
boehmes
parents: 34035
diff changeset
   485
      (with_time (Mirabelle.cpu_time apply_metis thms), true)
b2e6245fb3da only invoke metisFT if metis failed
boehmes
parents: 34035
diff changeset
   486
      handle TimeLimit.TimeOut => (change_data id (inc_metis_timeout m);
b2e6245fb3da only invoke metisFT if metis failed
boehmes
parents: 34035
diff changeset
   487
               ("timeout", false))
b2e6245fb3da only invoke metisFT if metis failed
boehmes
parents: 34035
diff changeset
   488
           | ERROR msg => ("error: " ^ msg, false)
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   489
32525
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   490
    val _ = log separator
34035
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   491
    val _ = change_data id (inc_metis_calls m)
39337
ffa577c0bbfa keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents: 39321
diff changeset
   492
    val _ = if trivial then () else change_data id (inc_metis_nontriv_calls m)
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   493
  in
32525
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   494
    maps snd named_thms
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   495
    |> timed_metis
34052
b2e6245fb3da only invoke metisFT if metis failed
boehmes
parents: 34035
diff changeset
   496
    |>> log o prefix (metis_tag id)
b2e6245fb3da only invoke metisFT if metis failed
boehmes
parents: 34035
diff changeset
   497
    |> snd
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   498
  end
32385
594890623c46 split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff changeset
   499
39363
1c4e38d635e1 added a timeout around "try" call in Mirabelle
blanchet
parents: 39341
diff changeset
   500
val try_inner_timeout = Time.fromSeconds 5
1c4e38d635e1 added a timeout around "try" call in Mirabelle
blanchet
parents: 39341
diff changeset
   501
val try_outer_timeout = Time.fromSeconds 30
39337
ffa577c0bbfa keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents: 39321
diff changeset
   502
34035
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   503
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
   504
  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
   505
    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
   506
    then () else
768d17f54125 use regular Proof.goal (which is what methods usually see) and prevent sledgehammer from crashing;
wenzelm
parents: 34052
diff changeset
   507
    let
38700
fcb0fe4c2f27 make Mirabelle happy
blanchet
parents: 38590
diff changeset
   508
      val named_thms =
38752
6628adcae4a7 consider "locality" when assigning weights to facts
blanchet
parents: 38700
diff changeset
   509
        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
   510
      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
   511
      val metis_ft = AList.defined (op =) args metis_ftK
39363
1c4e38d635e1 added a timeout around "try" call in Mirabelle
blanchet
parents: 39341
diff changeset
   512
      val trivial = TimeLimit.timeLimit try_outer_timeout
1c4e38d635e1 added a timeout around "try" call in Mirabelle
blanchet
parents: 39341
diff changeset
   513
                                   (Try.invoke_try (SOME try_inner_timeout)) pre
1c4e38d635e1 added a timeout around "try" call in Mirabelle
blanchet
parents: 39341
diff changeset
   514
                    handle TimeLimit.TimeOut => false
35592
768d17f54125 use regular Proof.goal (which is what methods usually see) and prevent sledgehammer from crashing;
wenzelm
parents: 34052
diff changeset
   515
      fun apply_metis m1 m2 =
768d17f54125 use regular Proof.goal (which is what methods usually see) and prevent sledgehammer from crashing;
wenzelm
parents: 34052
diff changeset
   516
        if metis_ft
34052
b2e6245fb3da only invoke metisFT if metis failed
boehmes
parents: 34035
diff changeset
   517
        then
35592
768d17f54125 use regular Proof.goal (which is what methods usually see) and prevent sledgehammer from crashing;
wenzelm
parents: 34052
diff changeset
   518
          if not (Mirabelle.catch_result metis_tag false
39337
ffa577c0bbfa keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents: 39321
diff changeset
   519
              (run_metis trivial false m1 name (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
   520
          then
768d17f54125 use regular Proof.goal (which is what methods usually see) and prevent sledgehammer from crashing;
wenzelm
parents: 34052
diff changeset
   521
            (Mirabelle.catch_result metis_tag false
39337
ffa577c0bbfa keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents: 39321
diff changeset
   522
              (run_metis trivial true m2 name (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
   523
          else ()
768d17f54125 use regular Proof.goal (which is what methods usually see) and prevent sledgehammer from crashing;
wenzelm
parents: 34052
diff changeset
   524
        else
34052
b2e6245fb3da only invoke metisFT if metis failed
boehmes
parents: 34035
diff changeset
   525
          (Mirabelle.catch_result metis_tag false
39337
ffa577c0bbfa keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents: 39321
diff changeset
   526
            (run_metis trivial false m1 name (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
   527
    in 
768d17f54125 use regular Proof.goal (which is what methods usually see) and prevent sledgehammer from crashing;
wenzelm
parents: 34052
diff changeset
   528
      change_data id (set_mini minimize);
39337
ffa577c0bbfa keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents: 39321
diff changeset
   529
      Mirabelle.catch sh_tag (run_sledgehammer trivial args 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
   530
      if is_some (!named_thms)
32612
76dddd260d2f restructured code
nipkow
parents: 32609
diff changeset
   531
      then
35592
768d17f54125 use regular Proof.goal (which is what methods usually see) and prevent sledgehammer from crashing;
wenzelm
parents: 34052
diff changeset
   532
       (apply_metis Unminimized UnminimizedFT;
768d17f54125 use regular Proof.goal (which is what methods usually see) and prevent sledgehammer from crashing;
wenzelm
parents: 34052
diff changeset
   533
        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
   534
        then
768d17f54125 use regular Proof.goal (which is what methods usually see) and prevent sledgehammer from crashing;
wenzelm
parents: 34052
diff changeset
   535
         (Mirabelle.catch minimize_tag (run_minimize args named_thms) id st;
768d17f54125 use regular Proof.goal (which is what methods usually see) and prevent sledgehammer from crashing;
wenzelm
parents: 34052
diff changeset
   536
          apply_metis Minimized MinimizedFT)
768d17f54125 use regular Proof.goal (which is what methods usually see) and prevent sledgehammer from crashing;
wenzelm
parents: 34052
diff changeset
   537
        else ())
768d17f54125 use regular Proof.goal (which is what methods usually see) and prevent sledgehammer from crashing;
wenzelm
parents: 34052
diff changeset
   538
      else ()
768d17f54125 use regular Proof.goal (which is what methods usually see) and prevent sledgehammer from crashing;
wenzelm
parents: 34052
diff changeset
   539
    end
32818
6c91e668b15e record max lemmas used
nipkow
parents: 32676
diff changeset
   540
  end
32385
594890623c46 split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff changeset
   541
32511
43d2ac4aa2de added option full_typed for sledgehammer action
boehmes
parents: 32510
diff changeset
   542
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
   543
  let
36373
66af0a49de39 move some sledgehammer stuff out of "atp_manager.ML"
blanchet
parents: 36294
diff changeset
   544
    val _ = Sledgehammer_Isar.full_types := AList.defined (op =) args full_typesK
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   545
  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
   546
594890623c46 split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff changeset
   547
end