src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
author blanchet
Mon, 04 Aug 2014 14:19:43 +0200
changeset 57782 b5dc0562c7fb
parent 57753 643e02500991
child 57814 7a9aaddb3203
permissions -rw-r--r--
renamed 'sh_minimize' to 'minimize'; compile;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
47847
7cddb6c8f93c updated headers;
wenzelm
parents: 47732
diff changeset
     1
(*  Title:      HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
32564
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
47480
24d8c9e9dae4 Mirabelle's 'usage' description relating to Sledgehammer now synchs with the ML code of the Mirabelle-Sledgehammer action
sultana
parents: 47477
diff changeset
     8
(*To facilitate synching the description of Mirabelle Sledgehammer parameters
24d8c9e9dae4 Mirabelle's 'usage' description relating to Sledgehammer now synchs with the ML code of the Mirabelle-Sledgehammer action
sultana
parents: 47477
diff changeset
     9
 (in ../lib/Tools/mirabelle) with the parameters actually used by this
24d8c9e9dae4 Mirabelle's 'usage' description relating to Sledgehammer now synchs with the ML code of the Mirabelle-Sledgehammer action
sultana
parents: 47477
diff changeset
    10
 interface, the former extracts PARAMETER and DESCRIPTION from code below which
24d8c9e9dae4 Mirabelle's 'usage' description relating to Sledgehammer now synchs with the ML code of the Mirabelle-Sledgehammer action
sultana
parents: 47477
diff changeset
    11
 has this pattern (provided it appears in a single line):
24d8c9e9dae4 Mirabelle's 'usage' description relating to Sledgehammer now synchs with the ML code of the Mirabelle-Sledgehammer action
sultana
parents: 47477
diff changeset
    12
   val .*K = "PARAMETER" (*DESCRIPTION*)
24d8c9e9dae4 Mirabelle's 'usage' description relating to Sledgehammer now synchs with the ML code of the Mirabelle-Sledgehammer action
sultana
parents: 47477
diff changeset
    13
*)
24d8c9e9dae4 Mirabelle's 'usage' description relating to Sledgehammer now synchs with the ML code of the Mirabelle-Sledgehammer action
sultana
parents: 47477
diff changeset
    14
(*NOTE: descriptions mention parameters (particularly NAME) without a defined range.*)
24d8c9e9dae4 Mirabelle's 'usage' description relating to Sledgehammer now synchs with the ML code of the Mirabelle-Sledgehammer action
sultana
parents: 47477
diff changeset
    15
val proverK = "prover" (*=NAME: name of the external prover to call*)
24d8c9e9dae4 Mirabelle's 'usage' description relating to Sledgehammer now synchs with the ML code of the Mirabelle-Sledgehammer action
sultana
parents: 47477
diff changeset
    16
val prover_timeoutK = "prover_timeout" (*=TIME: timeout for invoked ATP (seconds of process time)*)
24d8c9e9dae4 Mirabelle's 'usage' description relating to Sledgehammer now synchs with the ML code of the Mirabelle-Sledgehammer action
sultana
parents: 47477
diff changeset
    17
val keepK = "keep" (*=PATH: path where to keep temporary files created by sledgehammer*)
24d8c9e9dae4 Mirabelle's 'usage' description relating to Sledgehammer now synchs with the ML code of the Mirabelle-Sledgehammer action
sultana
parents: 47477
diff changeset
    18
55285
e88ad20035f4 merged 'reconstructors' and 'proof methods'
blanchet
parents: 55212
diff changeset
    19
val proof_methodK = "proof_method" (*=NAME: how to reconstruct proofs (ie. using metis/smt)*)
47480
24d8c9e9dae4 Mirabelle's 'usage' description relating to Sledgehammer now synchs with the ML code of the Mirabelle-Sledgehammer action
sultana
parents: 47477
diff changeset
    20
48293
914ca0827804 renamed Sledgehammer options
blanchet
parents: 48292
diff changeset
    21
val max_factsK = "max_facts" (*=NUM: max. relevant clauses to use*)
47480
24d8c9e9dae4 Mirabelle's 'usage' description relating to Sledgehammer now synchs with the ML code of the Mirabelle-Sledgehammer action
sultana
parents: 47477
diff changeset
    22
val max_relevantK = "max_relevant" (*=NUM: max. relevant clauses to use*)
24d8c9e9dae4 Mirabelle's 'usage' description relating to Sledgehammer now synchs with the ML code of the Mirabelle-Sledgehammer action
sultana
parents: 47477
diff changeset
    23
val max_callsK = "max_calls" (*=NUM: max. no. of calls to sledgehammer*)
24d8c9e9dae4 Mirabelle's 'usage' description relating to Sledgehammer now synchs with the ML code of the Mirabelle-Sledgehammer action
sultana
parents: 47477
diff changeset
    24
val preplay_timeoutK = "preplay_timeout" (*=TIME: timeout for finding reconstructed proof*)
56411
913dc982ef55 added option to Mirabelle
blanchet
parents: 55287
diff changeset
    25
val isar_proofsK = "isar_proofs" (*: enable Isar proof generation*)
57782
b5dc0562c7fb renamed 'sh_minimize' to 'minimize'; compile;
blanchet
parents: 57753
diff changeset
    26
val minimizeK = "minimize" (*: instruct sledgehammer to run its minimizer*)
47480
24d8c9e9dae4 Mirabelle's 'usage' description relating to Sledgehammer now synchs with the ML code of the Mirabelle-Sledgehammer action
sultana
parents: 47477
diff changeset
    27
24d8c9e9dae4 Mirabelle's 'usage' description relating to Sledgehammer now synchs with the ML code of the Mirabelle-Sledgehammer action
sultana
parents: 47477
diff changeset
    28
val check_trivialK = "check_trivial" (*: check if goals are "trivial" (false by default)*)
50334
74d453d1b084 added "fact_filter" option to Mirabelle
blanchet
parents: 50267
diff changeset
    29
val fact_filterK = "fact_filter" (*=STRING: fact filter*)
47480
24d8c9e9dae4 Mirabelle's 'usage' description relating to Sledgehammer now synchs with the ML code of the Mirabelle-Sledgehammer action
sultana
parents: 47477
diff changeset
    30
val type_encK = "type_enc" (*=STRING: type encoding scheme*)
24d8c9e9dae4 Mirabelle's 'usage' description relating to Sledgehammer now synchs with the ML code of the Mirabelle-Sledgehammer action
sultana
parents: 47477
diff changeset
    31
val lam_transK = "lam_trans" (*=STRING: lambda translation scheme*)
24d8c9e9dae4 Mirabelle's 'usage' description relating to Sledgehammer now synchs with the ML code of the Mirabelle-Sledgehammer action
sultana
parents: 47477
diff changeset
    32
val strictK = "strict" (*=BOOL: run in strict mode*)
24d8c9e9dae4 Mirabelle's 'usage' description relating to Sledgehammer now synchs with the ML code of the Mirabelle-Sledgehammer action
sultana
parents: 47477
diff changeset
    33
val sliceK = "slice" (*=BOOL: allow sledgehammer-level strategy-scheduling*)
24d8c9e9dae4 Mirabelle's 'usage' description relating to Sledgehammer now synchs with the ML code of the Mirabelle-Sledgehammer action
sultana
parents: 47477
diff changeset
    34
val uncurried_aliasesK = "uncurried_aliases" (*=SMART_BOOL: use fresh function names to alias curried applications*)
24d8c9e9dae4 Mirabelle's 'usage' description relating to Sledgehammer now synchs with the ML code of the Mirabelle-Sledgehammer action
sultana
parents: 47477
diff changeset
    35
val e_selection_heuristicK = "e_selection_heuristic" (*: FIXME*)
24d8c9e9dae4 Mirabelle's 'usage' description relating to Sledgehammer now synchs with the ML code of the Mirabelle-Sledgehammer action
sultana
parents: 47477
diff changeset
    36
val term_orderK = "term_order" (*: FIXME*)
24d8c9e9dae4 Mirabelle's 'usage' description relating to Sledgehammer now synchs with the ML code of the Mirabelle-Sledgehammer action
sultana
parents: 47477
diff changeset
    37
val force_sosK = "force_sos" (*: use SOS*)
24d8c9e9dae4 Mirabelle's 'usage' description relating to Sledgehammer now synchs with the ML code of the Mirabelle-Sledgehammer action
sultana
parents: 47477
diff changeset
    38
val max_new_mono_instancesK = "max_new_mono_instances" (*=NUM: max. new monomorphic instances*)
24d8c9e9dae4 Mirabelle's 'usage' description relating to Sledgehammer now synchs with the ML code of the Mirabelle-Sledgehammer action
sultana
parents: 47477
diff changeset
    39
val max_mono_itersK = "max_mono_iters" (*=NUM: max. iterations of monomorphiser*)
44448
04bd6a9307c6 don't perform a triviality check if the goal is skipped anyway
blanchet
parents: 44447
diff changeset
    40
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    41
fun sh_tag id = "#" ^ string_of_int id ^ " sledgehammer: "
55285
e88ad20035f4 merged 'reconstructors' and 'proof methods'
blanchet
parents: 55212
diff changeset
    42
fun proof_method_tag meth id = "#" ^ string_of_int id ^ " " ^ (!meth) ^ " (sledgehammer): "
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    43
32525
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
    44
val separator = "-----"
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
    45
47481
b5873d4ff1e2 gathered mirabelle_sledgehammer's hardcoded defaults
sultana
parents: 47480
diff changeset
    46
(*FIXME sensible to have Mirabelle-level Sledgehammer defaults?*)
b5873d4ff1e2 gathered mirabelle_sledgehammer's hardcoded defaults
sultana
parents: 47480
diff changeset
    47
(*defaults used in this Mirabelle action*)
57751
f453bbc289fa modernized Mirabelle (a bit) and made it compile
blanchet
parents: 57154
diff changeset
    48
val preplay_timeout_default = "1"
47481
b5873d4ff1e2 gathered mirabelle_sledgehammer's hardcoded defaults
sultana
parents: 47480
diff changeset
    49
val lam_trans_default = "smart"
b5873d4ff1e2 gathered mirabelle_sledgehammer's hardcoded defaults
sultana
parents: 47480
diff changeset
    50
val uncurried_aliases_default = "smart"
50334
74d453d1b084 added "fact_filter" option to Mirabelle
blanchet
parents: 50267
diff changeset
    51
val fact_filter_default = "smart"
47481
b5873d4ff1e2 gathered mirabelle_sledgehammer's hardcoded defaults
sultana
parents: 47480
diff changeset
    52
val type_enc_default = "smart"
b5873d4ff1e2 gathered mirabelle_sledgehammer's hardcoded defaults
sultana
parents: 47480
diff changeset
    53
val strict_default = "false"
48293
914ca0827804 renamed Sledgehammer options
blanchet
parents: 48292
diff changeset
    54
val max_facts_default = "smart"
47481
b5873d4ff1e2 gathered mirabelle_sledgehammer's hardcoded defaults
sultana
parents: 47480
diff changeset
    55
val slice_default = "true"
b5873d4ff1e2 gathered mirabelle_sledgehammer's hardcoded defaults
sultana
parents: 47480
diff changeset
    56
val max_calls_default = "10000000"
b5873d4ff1e2 gathered mirabelle_sledgehammer's hardcoded defaults
sultana
parents: 47480
diff changeset
    57
val trivial_default = "false"
46826
4c80c4034f1d added max_new_mono_instances, max_mono_iters, to Mirabelle-Sledgehammer; changed sh_minimize to avoid setting Mirabelle-level defaults;
sultana
parents: 46825
diff changeset
    58
4c80c4034f1d added max_new_mono_instances, max_mono_iters, to Mirabelle-Sledgehammer; changed sh_minimize to avoid setting Mirabelle-level defaults;
sultana
parents: 46825
diff changeset
    59
(*If a key is present in args then augment a list with its pair*)
4c80c4034f1d added max_new_mono_instances, max_mono_iters, to Mirabelle-Sledgehammer; changed sh_minimize to avoid setting Mirabelle-level defaults;
sultana
parents: 46825
diff changeset
    60
(*This is used to avoid fixing default values at the Mirabelle level, and
4c80c4034f1d added max_new_mono_instances, max_mono_iters, to Mirabelle-Sledgehammer; changed sh_minimize to avoid setting Mirabelle-level defaults;
sultana
parents: 46825
diff changeset
    61
  instead use the default values of the tool (Sledgehammer in this case).*)
4c80c4034f1d added max_new_mono_instances, max_mono_iters, to Mirabelle-Sledgehammer; changed sh_minimize to avoid setting Mirabelle-level defaults;
sultana
parents: 46825
diff changeset
    62
fun available_parameter args key label list =
4c80c4034f1d added max_new_mono_instances, max_mono_iters, to Mirabelle-Sledgehammer; changed sh_minimize to avoid setting Mirabelle-level defaults;
sultana
parents: 46825
diff changeset
    63
  let
4c80c4034f1d added max_new_mono_instances, max_mono_iters, to Mirabelle-Sledgehammer; changed sh_minimize to avoid setting Mirabelle-level defaults;
sultana
parents: 46825
diff changeset
    64
    val value = AList.lookup (op =) args key
4c80c4034f1d added max_new_mono_instances, max_mono_iters, to Mirabelle-Sledgehammer; changed sh_minimize to avoid setting Mirabelle-level defaults;
sultana
parents: 46825
diff changeset
    65
  in if is_some value then (label, the value) :: list else list end
4c80c4034f1d added max_new_mono_instances, max_mono_iters, to Mirabelle-Sledgehammer; changed sh_minimize to avoid setting Mirabelle-level defaults;
sultana
parents: 46825
diff changeset
    66
32549
338ccfd37f67 minimization: comparing w/ and w/o.
nipkow
parents: 32541
diff changeset
    67
datatype sh_data = ShData of {
338ccfd37f67 minimization: comparing w/ and w/o.
nipkow
parents: 32541
diff changeset
    68
  calls: int,
338ccfd37f67 minimization: comparing w/ and w/o.
nipkow
parents: 32541
diff changeset
    69
  success: int,
39337
ffa577c0bbfa keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents: 39321
diff changeset
    70
  nontriv_calls: int,
ffa577c0bbfa keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents: 39321
diff changeset
    71
  nontriv_success: int,
32585
e788b33dd2b4 revised lemma counting
nipkow
parents: 32574
diff changeset
    72
  lemmas: int,
32818
6c91e668b15e record max lemmas used
nipkow
parents: 32676
diff changeset
    73
  max_lems: int,
32549
338ccfd37f67 minimization: comparing w/ and w/o.
nipkow
parents: 32541
diff changeset
    74
  time_isa: int,
40062
cfaebaa8588f make Sledgehammer minimizer fully work with SMT
blanchet
parents: 40061
diff changeset
    75
  time_prover: int,
cfaebaa8588f make Sledgehammer minimizer fully work with SMT
blanchet
parents: 40061
diff changeset
    76
  time_prover_fail: int}
32549
338ccfd37f67 minimization: comparing w/ and w/o.
nipkow
parents: 32541
diff changeset
    77
40667
b8579f24ce67 make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents: 40627
diff changeset
    78
datatype re_data = ReData of {
32549
338ccfd37f67 minimization: comparing w/ and w/o.
nipkow
parents: 32541
diff changeset
    79
  calls: int,
338ccfd37f67 minimization: comparing w/ and w/o.
nipkow
parents: 32541
diff changeset
    80
  success: int,
39337
ffa577c0bbfa keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents: 39321
diff changeset
    81
  nontriv_calls: int,
ffa577c0bbfa keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents: 39321
diff changeset
    82
  nontriv_success: int,
32676
b1c85a117dec record how many "proof"s are solved by s/h
nipkow
parents: 32612
diff changeset
    83
  proofs: int,
32549
338ccfd37f67 minimization: comparing w/ and w/o.
nipkow
parents: 32541
diff changeset
    84
  time: int,
32550
d57c7a2d927c logging number of metis lemmas
nipkow
parents: 32549
diff changeset
    85
  timeout: int,
32990
717680b14041 added sums of squares for standard deviation
nipkow
parents: 32868
diff changeset
    86
  lemmas: int * int * int,
39341
d2b981a0429a indicate triviality in the list of proved things
blanchet
parents: 39340
diff changeset
    87
  posns: (Position.T * bool) list
32550
d57c7a2d927c logging number of metis lemmas
nipkow
parents: 32549
diff changeset
    88
  }
32549
338ccfd37f67 minimization: comparing w/ and w/o.
nipkow
parents: 32541
diff changeset
    89
32818
6c91e668b15e record max lemmas used
nipkow
parents: 32676
diff changeset
    90
fun make_sh_data
39337
ffa577c0bbfa keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents: 39321
diff changeset
    91
      (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
    92
       time_prover,time_prover_fail) =
39337
ffa577c0bbfa keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents: 39321
diff changeset
    93
  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
    94
         nontriv_success=nontriv_success, lemmas=lemmas, max_lems=max_lems,
40062
cfaebaa8588f make Sledgehammer minimizer fully work with SMT
blanchet
parents: 40061
diff changeset
    95
         time_isa=time_isa, time_prover=time_prover,
cfaebaa8588f make Sledgehammer minimizer fully work with SMT
blanchet
parents: 40061
diff changeset
    96
         time_prover_fail=time_prover_fail}
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
    97
40667
b8579f24ce67 make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents: 40627
diff changeset
    98
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
    99
                  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
   100
  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
   101
         nontriv_success=nontriv_success, proofs=proofs, time=time,
32990
717680b14041 added sums of squares for standard deviation
nipkow
parents: 32868
diff changeset
   102
         timeout=timeout, lemmas=lemmas, posns=posns}
32549
338ccfd37f67 minimization: comparing w/ and w/o.
nipkow
parents: 32541
diff changeset
   103
39337
ffa577c0bbfa keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents: 39321
diff changeset
   104
val empty_sh_data = make_sh_data (0, 0, 0, 0, 0, 0, 0, 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
   105
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
   106
39337
ffa577c0bbfa keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents: 39321
diff changeset
   107
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
   108
                              lemmas, max_lems, time_isa,
40062
cfaebaa8588f make Sledgehammer minimizer fully work with SMT
blanchet
parents: 40061
diff changeset
   109
  time_prover, time_prover_fail}) = (calls, success, nontriv_calls,
cfaebaa8588f make Sledgehammer minimizer fully work with SMT
blanchet
parents: 40061
diff changeset
   110
  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
   111
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
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
   113
  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
   114
  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
   115
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   116
datatype data = Data of {
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   117
  sh: sh_data,
57753
643e02500991 removed 'metisFT' support in Mirabelle
blanchet
parents: 57752
diff changeset
   118
  re_u: re_data (* proof method with unminimized set of lemmas *)
34035
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   119
  }
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   120
57753
643e02500991 removed 'metisFT' support in Mirabelle
blanchet
parents: 57752
diff changeset
   121
fun make_data (sh, re_u) = Data {sh=sh, re_u=re_u}
34035
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   122
57753
643e02500991 removed 'metisFT' support in Mirabelle
blanchet
parents: 57752
diff changeset
   123
val empty_data = make_data (empty_sh_data, empty_re_data)
34035
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   124
57753
643e02500991 removed 'metisFT' support in Mirabelle
blanchet
parents: 57752
diff changeset
   125
fun map_sh_data f (Data {sh, re_u}) =
57752
708347f9bfc6 removed Mirabelle minimization code
blanchet
parents: 57751
diff changeset
   126
  let val sh' = make_sh_data (f (tuple_of_sh_data sh))
57753
643e02500991 removed 'metisFT' support in Mirabelle
blanchet
parents: 57752
diff changeset
   127
  in make_data (sh', re_u) end
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   128
57753
643e02500991 removed 'metisFT' support in Mirabelle
blanchet
parents: 57752
diff changeset
   129
fun map_re_data f (Data {sh, re_u}) =
34035
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   130
  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
   131
    val f' = make_re_data o f o tuple_of_re_data
57753
643e02500991 removed 'metisFT' support in Mirabelle
blanchet
parents: 57752
diff changeset
   132
    val re_u' = f' re_u
643e02500991 removed 'metisFT' support in Mirabelle
blanchet
parents: 57752
diff changeset
   133
  in make_data (sh, re_u') end
32990
717680b14041 added sums of squares for standard deviation
nipkow
parents: 32868
diff changeset
   134
717680b14041 added sums of squares for standard deviation
nipkow
parents: 32868
diff changeset
   135
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
   136
32818
6c91e668b15e record max lemmas used
nipkow
parents: 32676
diff changeset
   137
val inc_sh_calls =  map_sh_data
40062
cfaebaa8588f make Sledgehammer minimizer fully work with SMT
blanchet
parents: 40061
diff changeset
   138
  (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
   139
    => (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
   140
32818
6c91e668b15e record max lemmas used
nipkow
parents: 32676
diff changeset
   141
val inc_sh_success = map_sh_data
40062
cfaebaa8588f make Sledgehammer minimizer fully work with SMT
blanchet
parents: 40061
diff changeset
   142
  (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
   143
    => (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
   144
ffa577c0bbfa keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents: 39321
diff changeset
   145
val inc_sh_nontriv_calls =  map_sh_data
40062
cfaebaa8588f make Sledgehammer minimizer fully work with SMT
blanchet
parents: 40061
diff changeset
   146
  (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
   147
    => (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
   148
ffa577c0bbfa keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents: 39321
diff changeset
   149
val inc_sh_nontriv_success = map_sh_data
40062
cfaebaa8588f make Sledgehammer minimizer fully work with SMT
blanchet
parents: 40061
diff changeset
   150
  (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
   151
    => (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
   152
32818
6c91e668b15e record max lemmas used
nipkow
parents: 32676
diff changeset
   153
fun inc_sh_lemmas n = map_sh_data
40062
cfaebaa8588f make Sledgehammer minimizer fully work with SMT
blanchet
parents: 40061
diff changeset
   154
  (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
   155
    => (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
   156
32818
6c91e668b15e record max lemmas used
nipkow
parents: 32676
diff changeset
   157
fun inc_sh_max_lems n = map_sh_data
40062
cfaebaa8588f make Sledgehammer minimizer fully work with SMT
blanchet
parents: 40061
diff changeset
   158
  (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
   159
    => (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
   160
32818
6c91e668b15e record max lemmas used
nipkow
parents: 32676
diff changeset
   161
fun inc_sh_time_isa t = map_sh_data
40062
cfaebaa8588f make Sledgehammer minimizer fully work with SMT
blanchet
parents: 40061
diff changeset
   162
  (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
   163
    => (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
   164
40062
cfaebaa8588f make Sledgehammer minimizer fully work with SMT
blanchet
parents: 40061
diff changeset
   165
fun inc_sh_time_prover t = map_sh_data
cfaebaa8588f make Sledgehammer minimizer fully work with SMT
blanchet
parents: 40061
diff changeset
   166
  (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
   167
    => (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
   168
40062
cfaebaa8588f make Sledgehammer minimizer fully work with SMT
blanchet
parents: 40061
diff changeset
   169
fun inc_sh_time_prover_fail t = map_sh_data
cfaebaa8588f make Sledgehammer minimizer fully work with SMT
blanchet
parents: 40061
diff changeset
   170
  (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
   171
    => (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
   172
55285
e88ad20035f4 merged 'reconstructors' and 'proof methods'
blanchet
parents: 55212
diff changeset
   173
val inc_proof_method_calls = map_re_data
39337
ffa577c0bbfa keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents: 39321
diff changeset
   174
  (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
   175
    => (calls + 1, success, nontriv_calls, nontriv_success, proofs, time, timeout, lemmas,posns))
32533
9735013cec72 tuned stats
nipkow
parents: 32526
diff changeset
   176
55285
e88ad20035f4 merged 'reconstructors' and 'proof methods'
blanchet
parents: 55212
diff changeset
   177
val inc_proof_method_success = map_re_data
39337
ffa577c0bbfa keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents: 39321
diff changeset
   178
  (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
   179
    => (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
   180
55285
e88ad20035f4 merged 'reconstructors' and 'proof methods'
blanchet
parents: 55212
diff changeset
   181
val inc_proof_method_nontriv_calls = map_re_data
39337
ffa577c0bbfa keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents: 39321
diff changeset
   182
  (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
   183
    => (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
   184
55285
e88ad20035f4 merged 'reconstructors' and 'proof methods'
blanchet
parents: 55212
diff changeset
   185
val inc_proof_method_nontriv_success = map_re_data
39337
ffa577c0bbfa keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents: 39321
diff changeset
   186
  (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
   187
    => (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
   188
55285
e88ad20035f4 merged 'reconstructors' and 'proof methods'
blanchet
parents: 55212
diff changeset
   189
val inc_proof_method_proofs = map_re_data
39337
ffa577c0bbfa keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents: 39321
diff changeset
   190
  (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
   191
    => (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
   192
57753
643e02500991 removed 'metisFT' support in Mirabelle
blanchet
parents: 57752
diff changeset
   193
fun inc_proof_method_time t = map_re_data
39337
ffa577c0bbfa keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents: 39321
diff changeset
   194
 (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns)
57753
643e02500991 removed 'metisFT' support in Mirabelle
blanchet
parents: 57752
diff changeset
   195
  => (calls, success, nontriv_calls, nontriv_success, proofs, time + t, timeout, lemmas,posns))
32536
ac56c62758d3 tuned stats
nipkow
parents: 32533
diff changeset
   196
55285
e88ad20035f4 merged 'reconstructors' and 'proof methods'
blanchet
parents: 55212
diff changeset
   197
val inc_proof_method_timeout = map_re_data
39337
ffa577c0bbfa keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents: 39321
diff changeset
   198
  (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
   199
    => (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
   200
57753
643e02500991 removed 'metisFT' support in Mirabelle
blanchet
parents: 57752
diff changeset
   201
fun inc_proof_method_lemmas n = map_re_data
39337
ffa577c0bbfa keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents: 39321
diff changeset
   202
  (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns)
57753
643e02500991 removed 'metisFT' support in Mirabelle
blanchet
parents: 57752
diff changeset
   203
    => (calls, success, nontriv_calls, nontriv_success, proofs, time, timeout, inc_max n lemmas, posns))
32551
421323205efd position information is now passed to all actions;
nipkow
parents: 32550
diff changeset
   204
57753
643e02500991 removed 'metisFT' support in Mirabelle
blanchet
parents: 57752
diff changeset
   205
fun inc_proof_method_posns pos = map_re_data
39337
ffa577c0bbfa keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents: 39321
diff changeset
   206
  (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns)
57753
643e02500991 removed 'metisFT' support in Mirabelle
blanchet
parents: 57752
diff changeset
   207
    => (calls, success, nontriv_calls, nontriv_success, proofs, time, timeout, lemmas, pos::posns))
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   208
44090
6ce82b9e2896 add line number prefix to output file name
blanchet
parents: 44089
diff changeset
   209
val str0 = string_of_int o the_default 0
6ce82b9e2896 add line number prefix to output file name
blanchet
parents: 44089
diff changeset
   210
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   211
local
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   212
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   213
val str = string_of_int
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   214
val str3 = Real.fmt (StringCvt.FIX (SOME 3))
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   215
fun percentage a b = string_of_int (a * 100 div b)
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   216
fun time t = Real.fromInt t / 1000.0
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   217
fun avg_time t n =
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   218
  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
   219
34035
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   220
fun log_sh_data log
40062
cfaebaa8588f make Sledgehammer minimizer fully work with SMT
blanchet
parents: 40061
diff changeset
   221
    (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
   222
 (log ("Total number of sledgehammer calls: " ^ str calls);
6c91e668b15e record max lemmas used
nipkow
parents: 32676
diff changeset
   223
  log ("Number of successful sledgehammer calls: " ^ str success);
6c91e668b15e record max lemmas used
nipkow
parents: 32676
diff changeset
   224
  log ("Number of sledgehammer lemmas: " ^ str lemmas);
6c91e668b15e record max lemmas used
nipkow
parents: 32676
diff changeset
   225
  log ("Max number of sledgehammer lemmas: " ^ str max_lems);
6c91e668b15e record max lemmas used
nipkow
parents: 32676
diff changeset
   226
  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
   227
  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
   228
  log ("Number of successful nontrivial sledgehammer calls: " ^ str nontriv_success);
32818
6c91e668b15e record max lemmas used
nipkow
parents: 32676
diff changeset
   229
  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
   230
  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
   231
  log ("Total time for failed sledgehammer calls (ATP): " ^ str3 (time time_prover_fail));
32536
ac56c62758d3 tuned stats
nipkow
parents: 32533
diff changeset
   232
  log ("Average time for sledgehammer calls (Isabelle): " ^
32818
6c91e668b15e record max lemmas used
nipkow
parents: 32676
diff changeset
   233
    str3 (avg_time time_isa calls));
32533
9735013cec72 tuned stats
nipkow
parents: 32526
diff changeset
   234
  log ("Average time for successful sledgehammer calls (ATP): " ^
40062
cfaebaa8588f make Sledgehammer minimizer fully work with SMT
blanchet
parents: 40061
diff changeset
   235
    str3 (avg_time time_prover success));
32536
ac56c62758d3 tuned stats
nipkow
parents: 32533
diff changeset
   236
  log ("Average time for failed sledgehammer calls (ATP): " ^
40062
cfaebaa8588f make Sledgehammer minimizer fully work with SMT
blanchet
parents: 40061
diff changeset
   237
    str3 (avg_time time_prover_fail (calls - success)))
32533
9735013cec72 tuned stats
nipkow
parents: 32526
diff changeset
   238
  )
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
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) =
47728
6ee015f6ea4b reintroduce file offsets in Mirabelle output, but make sure they are not influenced by the length of the path
blanchet
parents: 47532
diff changeset
   241
  str0 (Position.line_of pos) ^ ":" ^ str0 (Position.offset_of pos) ^
44090
6ce82b9e2896 add line number prefix to output file name
blanchet
parents: 44089
diff changeset
   242
  (if triv then "[T]" else "")
32551
421323205efd position information is now passed to all actions;
nipkow
parents: 32550
diff changeset
   243
40667
b8579f24ce67 make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents: 40627
diff changeset
   244
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
   245
     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
   246
    (lemmas, lems_sos, lems_max), re_posns) =
55285
e88ad20035f4 merged 'reconstructors' and 'proof methods'
blanchet
parents: 55212
diff changeset
   247
 (log ("Total number of " ^ tag ^ "proof method calls: " ^ str re_calls);
e88ad20035f4 merged 'reconstructors' and 'proof methods'
blanchet
parents: 55212
diff changeset
   248
  log ("Number of successful " ^ tag ^ "proof method calls: " ^ str re_success ^
40667
b8579f24ce67 make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents: 40627
diff changeset
   249
    " (proof: " ^ str re_proofs ^ ")");
55285
e88ad20035f4 merged 'reconstructors' and 'proof methods'
blanchet
parents: 55212
diff changeset
   250
  log ("Number of " ^ tag ^ "proof method timeouts: " ^ str re_timeout);
40667
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 ("Success rate: " ^ percentage re_success sh_calls ^ "%");
55285
e88ad20035f4 merged 'reconstructors' and 'proof methods'
blanchet
parents: 55212
diff changeset
   252
  log ("Total number of nontrivial " ^ tag ^ "proof method calls: " ^ str re_nontriv_calls);
e88ad20035f4 merged 'reconstructors' and 'proof methods'
blanchet
parents: 55212
diff changeset
   253
  log ("Number of successful nontrivial " ^ tag ^ "proof method calls: " ^ str re_nontriv_success ^
40667
b8579f24ce67 make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents: 40627
diff changeset
   254
    " (proof: " ^ str re_proofs ^ ")");
55285
e88ad20035f4 merged 'reconstructors' and 'proof methods'
blanchet
parents: 55212
diff changeset
   255
  log ("Number of successful " ^ tag ^ "proof method lemmas: " ^ str lemmas);
e88ad20035f4 merged 'reconstructors' and 'proof methods'
blanchet
parents: 55212
diff changeset
   256
  log ("SOS of successful " ^ tag ^ "proof method lemmas: " ^ str lems_sos);
e88ad20035f4 merged 'reconstructors' and 'proof methods'
blanchet
parents: 55212
diff changeset
   257
  log ("Max number of successful " ^ tag ^ "proof method lemmas: " ^ str lems_max);
e88ad20035f4 merged 'reconstructors' and 'proof methods'
blanchet
parents: 55212
diff changeset
   258
  log ("Total time for successful " ^ tag ^ "proof method calls: " ^ str3 (time re_time));
e88ad20035f4 merged 'reconstructors' and 'proof methods'
blanchet
parents: 55212
diff changeset
   259
  log ("Average time for successful " ^ tag ^ "proof method calls: " ^
40667
b8579f24ce67 make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents: 40627
diff changeset
   260
    str3 (avg_time re_time re_success));
32551
421323205efd position information is now passed to all actions;
nipkow
parents: 32550
diff changeset
   261
  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
   262
  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
   263
  else ()
421323205efd position information is now passed to all actions;
nipkow
parents: 32550
diff changeset
   264
 )
32571
d4bb776874b8 count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents: 32567
diff changeset
   265
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   266
in
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   267
57753
643e02500991 removed 'metisFT' support in Mirabelle
blanchet
parents: 57752
diff changeset
   268
fun log_data id log (Data {sh, re_u}) =
34035
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   269
  let
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   270
    val ShData {calls=sh_calls, ...} = sh
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   271
40667
b8579f24ce67 make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents: 40627
diff changeset
   272
    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
   273
    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
   274
      log_re_data log tag sh_calls (tuple_of_re_data m)
57753
643e02500991 removed 'metisFT' support in Mirabelle
blanchet
parents: 57752
diff changeset
   275
    fun log_proof_method (tag1, m1) = app_if m1 (fn () => (log_re tag1 m1; log ""))
34035
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   276
  in
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   277
    if sh_calls > 0
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   278
    then
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   279
     (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
   280
      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
   281
      log "";
57753
643e02500991 removed 'metisFT' support in Mirabelle
blanchet
parents: 57752
diff changeset
   282
      log_proof_method ("", re_u))
34035
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   283
    else ()
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   284
  end
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   285
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   286
end
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   287
55211
5d027af93a08 moved ML code around
blanchet
parents: 55208
diff changeset
   288
(* Warning: we implicitly assume single-threaded execution here *)
32740
9dd0a2f83429 explicit indication of Unsynchronized.ref;
wenzelm
parents: 32676
diff changeset
   289
val data = Unsynchronized.ref ([] : (int * data) list)
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   290
32740
9dd0a2f83429 explicit indication of Unsynchronized.ref;
wenzelm
parents: 32676
diff changeset
   291
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
   292
fun done id ({log, ...}: Mirabelle.done_args) =
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   293
  AList.lookup (op =) (!data) id
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   294
  |> Option.map (log_data id log)
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   295
  |> K ()
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   296
32740
9dd0a2f83429 explicit indication of Unsynchronized.ref;
wenzelm
parents: 32676
diff changeset
   297
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
   298
55205
8450622db0c5 refactor large ML file
blanchet
parents: 55202
diff changeset
   299
fun get_prover_name thy args =
33016
b73b74fe23c3 proper exceptions instead of unhandled partiality
boehmes
parents: 32991
diff changeset
   300
  let
40062
cfaebaa8588f make Sledgehammer minimizer fully work with SMT
blanchet
parents: 40061
diff changeset
   301
    fun default_prover_name () =
55205
8450622db0c5 refactor large ML file
blanchet
parents: 55202
diff changeset
   302
      hd (#provers (Sledgehammer_Commands.default_params thy []))
47060
e2741ec9ae36 prefer explicitly qualified exception List.Empty;
wenzelm
parents: 47049
diff changeset
   303
      handle List.Empty => error "No ATP available."
33016
b73b74fe23c3 proper exceptions instead of unhandled partiality
boehmes
parents: 32991
diff changeset
   304
  in
b73b74fe23c3 proper exceptions instead of unhandled partiality
boehmes
parents: 32991
diff changeset
   305
    (case AList.lookup (op =) args proverK of
50352
db8cae658807 added MaSh learning to Mirabelle
blanchet
parents: 50334
diff changeset
   306
      SOME name => name
db8cae658807 added MaSh learning to Mirabelle
blanchet
parents: 50334
diff changeset
   307
    | NONE => default_prover_name ())
db8cae658807 added MaSh learning to Mirabelle
blanchet
parents: 50334
diff changeset
   308
  end
db8cae658807 added MaSh learning to Mirabelle
blanchet
parents: 50334
diff changeset
   309
db8cae658807 added MaSh learning to Mirabelle
blanchet
parents: 50334
diff changeset
   310
fun get_prover ctxt name params goal all_facts =
db8cae658807 added MaSh learning to Mirabelle
blanchet
parents: 50334
diff changeset
   311
  let
54503
blanchet
parents: 54500
diff changeset
   312
    val learn = Sledgehammer_MaSh.mash_learn_proof ctxt params (prop_of goal) all_facts
50352
db8cae658807 added MaSh learning to Mirabelle
blanchet
parents: 50334
diff changeset
   313
  in
55202
824c48a539c9 renamed many Sledgehammer ML files to clarify structure
blanchet
parents: 55201
diff changeset
   314
    Sledgehammer_Prover_Minimize.get_minimizing_prover ctxt Sledgehammer_Prover.Normal learn name
33016
b73b74fe23c3 proper exceptions instead of unhandled partiality
boehmes
parents: 32991
diff changeset
   315
  end
32525
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   316
46340
cac402c486b0 separate orthogonal components
blanchet
parents: 46320
diff changeset
   317
type stature = ATP_Problem_Generate.stature
38752
6628adcae4a7 consider "locality" when assigning weights to facts
blanchet
parents: 38700
diff changeset
   318
53081
2a62d848a56a improved ad hoc success detection in Mirabelle -- if the metis call fails and the structured proof succeeds, remember only the success
blanchet
parents: 52555
diff changeset
   319
fun good_line s =
2a62d848a56a improved ad hoc success detection in Mirabelle -- if the metis call fails and the structured proof succeeds, remember only the success
blanchet
parents: 52555
diff changeset
   320
  (String.isSubstring " ms)" s orelse String.isSubstring " s)" s)
2a62d848a56a improved ad hoc success detection in Mirabelle -- if the metis call fails and the structured proof succeeds, remember only the success
blanchet
parents: 52555
diff changeset
   321
  andalso not (String.isSubstring "(> " s)
2a62d848a56a improved ad hoc success detection in Mirabelle -- if the metis call fails and the structured proof succeeds, remember only the success
blanchet
parents: 52555
diff changeset
   322
  andalso not (String.isSubstring ", > " s)
2a62d848a56a improved ad hoc success detection in Mirabelle -- if the metis call fails and the structured proof succeeds, remember only the success
blanchet
parents: 52555
diff changeset
   323
  andalso not (String.isSubstring "may fail" s)
2a62d848a56a improved ad hoc success detection in Mirabelle -- if the metis call fails and the structured proof succeeds, remember only the success
blanchet
parents: 52555
diff changeset
   324
51206
3fba6741ead2 improved hack
blanchet
parents: 51203
diff changeset
   325
(* Fragile hack *)
55285
e88ad20035f4 merged 'reconstructors' and 'proof methods'
blanchet
parents: 55212
diff changeset
   326
fun proof_method_from_msg args msg =
e88ad20035f4 merged 'reconstructors' and 'proof methods'
blanchet
parents: 55212
diff changeset
   327
  (case AList.lookup (op =) args proof_methodK of
41357
ae76960d86a2 added "sledgehammer_tac" as possible reconstructor in Mirabelle
blanchet
parents: 41338
diff changeset
   328
    SOME name => name
ae76960d86a2 added "sledgehammer_tac" as possible reconstructor in Mirabelle
blanchet
parents: 41338
diff changeset
   329
  | NONE =>
53081
2a62d848a56a improved ad hoc success detection in Mirabelle -- if the metis call fails and the structured proof succeeds, remember only the success
blanchet
parents: 52555
diff changeset
   330
    if exists good_line (split_lines msg) then
51203
4c6ae305462e trust preplayed proof in Mirabelle
blanchet
parents: 51187
diff changeset
   331
      "none" (* trust the preplayed proof *)
4c6ae305462e trust preplayed proof in Mirabelle
blanchet
parents: 51187
diff changeset
   332
    else if String.isSubstring "metis (" msg then
45519
cd6e78cb6ee8 make metis reconstruction handling more flexible
blanchet
parents: 45514
diff changeset
   333
      msg |> Substring.full
cd6e78cb6ee8 make metis reconstruction handling more flexible
blanchet
parents: 45514
diff changeset
   334
          |> Substring.position "metis ("
cd6e78cb6ee8 make metis reconstruction handling more flexible
blanchet
parents: 45514
diff changeset
   335
          |> snd |> Substring.position ")"
cd6e78cb6ee8 make metis reconstruction handling more flexible
blanchet
parents: 45514
diff changeset
   336
          |> fst |> Substring.string
cd6e78cb6ee8 make metis reconstruction handling more flexible
blanchet
parents: 45514
diff changeset
   337
          |> suffix ")"
cd6e78cb6ee8 make metis reconstruction handling more flexible
blanchet
parents: 45514
diff changeset
   338
    else if String.isSubstring "metis" msg then
cd6e78cb6ee8 make metis reconstruction handling more flexible
blanchet
parents: 45514
diff changeset
   339
      "metis"
cd6e78cb6ee8 make metis reconstruction handling more flexible
blanchet
parents: 45514
diff changeset
   340
    else
cd6e78cb6ee8 make metis reconstruction handling more flexible
blanchet
parents: 45514
diff changeset
   341
      "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
   342
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   343
local
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   344
32536
ac56c62758d3 tuned stats
nipkow
parents: 32533
diff changeset
   345
datatype sh_result =
46340
cac402c486b0 separate orthogonal components
blanchet
parents: 46320
diff changeset
   346
  SH_OK of int * int * (string * stature) list |
32536
ac56c62758d3 tuned stats
nipkow
parents: 32533
diff changeset
   347
  SH_FAIL of int * int |
ac56c62758d3 tuned stats
nipkow
parents: 32533
diff changeset
   348
  SH_ERROR
ac56c62758d3 tuned stats
nipkow
parents: 32533
diff changeset
   349
50352
db8cae658807 added MaSh learning to Mirabelle
blanchet
parents: 50334
diff changeset
   350
fun run_sh prover_name fact_filter type_enc strict max_facts slice
50334
74d453d1b084 added "fact_filter" option to Mirabelle
blanchet
parents: 50267
diff changeset
   351
      lam_trans uncurried_aliases e_selection_heuristic term_order force_sos
57782
b5dc0562c7fb renamed 'sh_minimize' to 'minimize'; compile;
blanchet
parents: 57753
diff changeset
   352
      hard_timeout timeout preplay_timeout isar_proofsLST minimizeLST
50334
74d453d1b084 added "fact_filter" option to Mirabelle
blanchet
parents: 50267
diff changeset
   353
      max_new_mono_instancesLST max_mono_itersLST dir pos st =
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   354
  let
55205
8450622db0c5 refactor large ML file
blanchet
parents: 55202
diff changeset
   355
    val thy = Proof.theory_of st
38998
f11a861e0061 share the relevance filter among the provers
blanchet
parents: 38988
diff changeset
   356
    val {context = ctxt, facts = chained_ths, goal} = Proof.goal st
f11a861e0061 share the relevance filter among the provers
blanchet
parents: 38988
diff changeset
   357
    val i = 1
44090
6ce82b9e2896 add line number prefix to output file name
blanchet
parents: 44089
diff changeset
   358
    fun set_file_name (SOME dir) =
55212
blanchet
parents: 55211
diff changeset
   359
        Config.put Sledgehammer_Prover_ATP.atp_dest_dir dir
blanchet
parents: 55211
diff changeset
   360
        #> Config.put Sledgehammer_Prover_ATP.atp_problem_prefix
44424
2434dd7519e8 clearer separator in generated file names
blanchet
parents: 44099
diff changeset
   361
          ("prob_" ^ str0 (Position.line_of pos) ^ "__")
57751
f453bbc289fa modernized Mirabelle (a bit) and made it compile
blanchet
parents: 57154
diff changeset
   362
        #> Config.put SMT2_Config.debug_files
56811
b66639331db5 optional case enforcement
haftmann
parents: 56411
diff changeset
   363
          (dir ^ "/" ^ Name.desymbolize (SOME false) (ATP_Util.timestamp ()) ^ "_"
41338
ffd730fcf0ac avoid weird symbols in path
blanchet
parents: 41337
diff changeset
   364
          ^ serial_string ())
44090
6ce82b9e2896 add line number prefix to output file name
blanchet
parents: 44089
diff changeset
   365
      | set_file_name NONE = I
39321
23951979a362 make Mirabelle happy
blanchet
parents: 39005
diff changeset
   366
    val st' =
47030
7e80e14247fc internal renamings
blanchet
parents: 46826
diff changeset
   367
      st
7e80e14247fc internal renamings
blanchet
parents: 46826
diff changeset
   368
      |> Proof.map_context
7e80e14247fc internal renamings
blanchet
parents: 46826
diff changeset
   369
           (set_file_name dir
47032
73cdeed236c0 more weight attribute tuning
blanchet
parents: 47030
diff changeset
   370
            #> (Option.map (Config.put ATP_Systems.e_selection_heuristic)
73cdeed236c0 more weight attribute tuning
blanchet
parents: 47030
diff changeset
   371
                  e_selection_heuristic |> the_default I)
47049
72bd3311ecba added term_order option to Mirabelle
blanchet
parents: 47032
diff changeset
   372
            #> (Option.map (Config.put ATP_Systems.term_order)
72bd3311ecba added term_order option to Mirabelle
blanchet
parents: 47032
diff changeset
   373
                  term_order |> the_default I)
47030
7e80e14247fc internal renamings
blanchet
parents: 46826
diff changeset
   374
            #> (Option.map (Config.put ATP_Systems.force_sos)
7e80e14247fc internal renamings
blanchet
parents: 46826
diff changeset
   375
                  force_sos |> the_default I))
57782
b5dc0562c7fb renamed 'sh_minimize' to 'minimize'; compile;
blanchet
parents: 57753
diff changeset
   376
    val params as {max_facts, minimize, preplay_timeout, ...} =
55205
8450622db0c5 refactor large ML file
blanchet
parents: 55202
diff changeset
   377
      Sledgehammer_Commands.default_params thy
46826
4c80c4034f1d added max_new_mono_instances, max_mono_iters, to Mirabelle-Sledgehammer; changed sh_minimize to avoid setting Mirabelle-level defaults;
sultana
parents: 46825
diff changeset
   378
         ([("verbose", "true"),
50334
74d453d1b084 added "fact_filter" option to Mirabelle
blanchet
parents: 50267
diff changeset
   379
           ("fact_filter", fact_filter),
43626
a867ebb12209 renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents: 43569
diff changeset
   380
           ("type_enc", type_enc),
46386
6b17c65d35c4 renamed Sledgehammer option
blanchet
parents: 46365
diff changeset
   381
           ("strict", strict),
47481
b5873d4ff1e2 gathered mirabelle_sledgehammer's hardcoded defaults
sultana
parents: 47480
diff changeset
   382
           ("lam_trans", lam_trans |> the_default lam_trans_default),
b5873d4ff1e2 gathered mirabelle_sledgehammer's hardcoded defaults
sultana
parents: 47480
diff changeset
   383
           ("uncurried_aliases", uncurried_aliases |> the_default uncurried_aliases_default),
48293
914ca0827804 renamed Sledgehammer options
blanchet
parents: 48292
diff changeset
   384
           ("max_facts", max_facts),
45706
418846ea4f99 renamed "slicing" to "slice"
blanchet
parents: 45520
diff changeset
   385
           ("slice", slice),
44448
04bd6a9307c6 don't perform a triviality check if the goal is skipped anyway
blanchet
parents: 44447
diff changeset
   386
           ("timeout", string_of_int timeout),
04bd6a9307c6 don't perform a triviality check if the goal is skipped anyway
blanchet
parents: 44447
diff changeset
   387
           ("preplay_timeout", preplay_timeout)]
56411
913dc982ef55 added option to Mirabelle
blanchet
parents: 55287
diff changeset
   388
          |> isar_proofsLST
57782
b5dc0562c7fb renamed 'sh_minimize' to 'minimize'; compile;
blanchet
parents: 57753
diff changeset
   389
          |> minimizeLST (*don't confuse the two minimization flags*)
46826
4c80c4034f1d added max_new_mono_instances, max_mono_iters, to Mirabelle-Sledgehammer; changed sh_minimize to avoid setting Mirabelle-level defaults;
sultana
parents: 46825
diff changeset
   390
          |> max_new_mono_instancesLST
4c80c4034f1d added max_new_mono_instances, max_mono_iters, to Mirabelle-Sledgehammer; changed sh_minimize to avoid setting Mirabelle-level defaults;
sultana
parents: 46825
diff changeset
   391
          |> max_mono_itersLST)
55205
8450622db0c5 refactor large ML file
blanchet
parents: 55202
diff changeset
   392
    val default_max_facts =
8450622db0c5 refactor large ML file
blanchet
parents: 55202
diff changeset
   393
      Sledgehammer_Prover_Minimize.default_max_facts_of_prover ctxt prover_name
52196
2281f33e8da6 redid rac7830871177 to avoid duplicate fixed variable (e.g. lemma "P (a::nat)" proof - have "!!a::int. Q a" sledgehammer [e])
blanchet
parents: 52125
diff changeset
   394
    val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal goal i ctxt
32574
719426c9e1eb added hard timeout for sledgehammer based on elapsed time (no need to trust ATP's timeout handling);
boehmes
parents: 32571
diff changeset
   395
    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
   396
      (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
   397
        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
   398
      | SOME secs => TimeLimit.timeLimit (Time.fromSeconds secs))
42953
26111aafab12 detect inappropriate problems and crashes better in Waldmeister
blanchet
parents: 42952
diff changeset
   399
    fun failed failure =
51009
e8ff34a1fa9a thread through fact triple component from which used facts come, for accurate index output
blanchet
parents: 51008
diff changeset
   400
      ({outcome = SOME failure, used_facts = [], used_from = [],
57751
f453bbc289fa modernized Mirabelle (a bit) and made it compile
blanchet
parents: 57154
diff changeset
   401
        preferred_methss = (Sledgehammer_Proof_Methods.Auto_Method, []), run_time = Time.zeroTime,
f453bbc289fa modernized Mirabelle (a bit) and made it compile
blanchet
parents: 57154
diff changeset
   402
        message = K ""}, ~1)
f453bbc289fa modernized Mirabelle (a bit) and made it compile
blanchet
parents: 57154
diff changeset
   403
    val ({outcome, used_facts, preferred_methss, run_time, message, ...}
55201
1ee776da8da7 renamed ML file
blanchet
parents: 55198
diff changeset
   404
         : Sledgehammer_Prover.prover_result,
51009
e8ff34a1fa9a thread through fact triple component from which used facts come, for accurate index output
blanchet
parents: 51008
diff changeset
   405
         time_isa) = time_limit (Mirabelle.cpu_time (fn () =>
41275
3897af72c731 move relevance filter into hard timeout
blanchet
parents: 41274
diff changeset
   406
      let
55212
blanchet
parents: 55211
diff changeset
   407
        val ho_atp = Sledgehammer_Prover_ATP.is_ho_atp ctxt prover_name
48299
5e5c6616f0fe centrally construct expensive data structures
blanchet
parents: 48293
diff changeset
   408
        val reserved = Sledgehammer_Util.reserved_isar_keyword_table ()
5e5c6616f0fe centrally construct expensive data structures
blanchet
parents: 48293
diff changeset
   409
        val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
41275
3897af72c731 move relevance filter into hard timeout
blanchet
parents: 41274
diff changeset
   410
        val facts =
48288
255c6e1fd505 rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents: 48250
diff changeset
   411
          Sledgehammer_Fact.nearly_all_facts ctxt ho_atp
48299
5e5c6616f0fe centrally construct expensive data structures
blanchet
parents: 48293
diff changeset
   412
              Sledgehammer_Fact.no_fact_override reserved css_table chained_ths
5e5c6616f0fe centrally construct expensive data structures
blanchet
parents: 48293
diff changeset
   413
              hyp_ts concl_t
51010
afd0213a3dab tuned data structure
blanchet
parents: 51009
diff changeset
   414
        val factss =
51007
4f694d52bf62 thread fact triple (MeSh, MePo, MaSh) to allow different filters in different slices
blanchet
parents: 51005
diff changeset
   415
          facts
48381
1b7d798460bb renamed ML structures
blanchet
parents: 48321
diff changeset
   416
          |> Sledgehammer_MaSh.relevant_facts ctxt params prover_name
48293
914ca0827804 renamed Sledgehammer options
blanchet
parents: 48292
diff changeset
   417
                 (the_default default_max_facts max_facts)
48292
7fcee834c7f5 more code rationalization in relevance filter
blanchet
parents: 48289
diff changeset
   418
                 Sledgehammer_Fact.no_fact_override hyp_ts concl_t
51010
afd0213a3dab tuned data structure
blanchet
parents: 51009
diff changeset
   419
          |> tap (fn factss =>
50868
4b30d461b3a6 more informative output
blanchet
parents: 50867
diff changeset
   420
                     "Line " ^ str0 (Position.line_of pos) ^ ": " ^
55202
824c48a539c9 renamed many Sledgehammer ML files to clarify structure
blanchet
parents: 55201
diff changeset
   421
                     Sledgehammer.string_of_factss factss
50867
48836c35d636 have Mirabelle produce more output
blanchet
parents: 50669
diff changeset
   422
                     |> Output.urgent_message)
50352
db8cae658807 added MaSh learning to Mirabelle
blanchet
parents: 50334
diff changeset
   423
        val prover = get_prover ctxt prover_name params goal facts
41275
3897af72c731 move relevance filter into hard timeout
blanchet
parents: 41274
diff changeset
   424
        val problem =
54141
f57f8e7a879f generate a comment storing the goal nickname in "learn_prover"
blanchet
parents: 54130
diff changeset
   425
          {comment = "", state = st', goal = goal, subgoal = i,
51010
afd0213a3dab tuned data structure
blanchet
parents: 51009
diff changeset
   426
           subgoal_count = Sledgehammer_Util.subgoal_count st, factss = factss}
57751
f453bbc289fa modernized Mirabelle (a bit) and made it compile
blanchet
parents: 57154
diff changeset
   427
      in prover params problem end)) ()
42953
26111aafab12 detect inappropriate problems and crashes better in Waldmeister
blanchet
parents: 42952
diff changeset
   428
      handle TimeLimit.TimeOut => failed ATP_Proof.TimedOut
26111aafab12 detect inappropriate problems and crashes better in Waldmeister
blanchet
parents: 42952
diff changeset
   429
           | Fail "inappropriate" => failed ATP_Proof.Inappropriate
45371
blanchet
parents: 44768
diff changeset
   430
    val time_prover = run_time |> Time.toMilliseconds
57782
b5dc0562c7fb renamed 'sh_minimize' to 'minimize'; compile;
blanchet
parents: 57753
diff changeset
   431
    val msg = message (fn () => Sledgehammer.play_one_line_proof minimize preplay_timeout used_facts
b5dc0562c7fb renamed 'sh_minimize' to 'minimize'; compile;
blanchet
parents: 57753
diff changeset
   432
      st' i preferred_methss)
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   433
  in
55211
5d027af93a08 moved ML code around
blanchet
parents: 55208
diff changeset
   434
    (case outcome of
43052
8d6a4978cc65 automatically minimize with Metis when this can be done within a few seconds
blanchet
parents: 43051
diff changeset
   435
      NONE => (msg, SH_OK (time_isa, time_prover, used_facts))
55211
5d027af93a08 moved ML code around
blanchet
parents: 55208
diff changeset
   436
    | SOME _ => (msg, SH_FAIL (time_isa, time_prover)))
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   437
  end
37994
b04307085a09 make TPTP generator accept full first-order formulas
blanchet
parents: 37631
diff changeset
   438
  handle ERROR msg => ("error: " ^ msg, SH_ERROR)
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   439
32498
1132c7c13f36 Mirabelle: actions are responsible for handling exceptions,
boehmes
parents: 32496
diff changeset
   440
in
1132c7c13f36 Mirabelle: actions are responsible for handling exceptions,
boehmes
parents: 32496
diff changeset
   441
55285
e88ad20035f4 merged 'reconstructors' and 'proof methods'
blanchet
parents: 55212
diff changeset
   442
fun run_sledgehammer trivial args proof_method named_thms id
44090
6ce82b9e2896 add line number prefix to output file name
blanchet
parents: 44089
diff changeset
   443
      ({pre=st, log, pos, ...}: Mirabelle.run_args) =
32385
594890623c46 split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff changeset
   444
  let
55205
8450622db0c5 refactor large ML file
blanchet
parents: 55202
diff changeset
   445
    val thy = Proof.theory_of st
39340
3998dc0bf82b indicate which goals are trivial
blanchet
parents: 39337
diff changeset
   446
    val triv_str = if trivial then "[T] " else ""
32536
ac56c62758d3 tuned stats
nipkow
parents: 32533
diff changeset
   447
    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
   448
    val _ = if trivial then () else change_data id inc_sh_nontriv_calls
55205
8450622db0c5 refactor large ML file
blanchet
parents: 55202
diff changeset
   449
    val prover_name = get_prover_name thy args
50334
74d453d1b084 added "fact_filter" option to Mirabelle
blanchet
parents: 50267
diff changeset
   450
    val fact_filter = AList.lookup (op =) args fact_filterK |> the_default fact_filter_default
47481
b5873d4ff1e2 gathered mirabelle_sledgehammer's hardcoded defaults
sultana
parents: 47480
diff changeset
   451
    val type_enc = AList.lookup (op =) args type_encK |> the_default type_enc_default
b5873d4ff1e2 gathered mirabelle_sledgehammer's hardcoded defaults
sultana
parents: 47480
diff changeset
   452
    val strict = AList.lookup (op =) args strictK |> the_default strict_default
48293
914ca0827804 renamed Sledgehammer options
blanchet
parents: 48292
diff changeset
   453
    val max_facts =
55211
5d027af93a08 moved ML code around
blanchet
parents: 55208
diff changeset
   454
      (case AList.lookup (op =) args max_factsK of
48293
914ca0827804 renamed Sledgehammer options
blanchet
parents: 48292
diff changeset
   455
        SOME max => max
55211
5d027af93a08 moved ML code around
blanchet
parents: 55208
diff changeset
   456
      | NONE =>
5d027af93a08 moved ML code around
blanchet
parents: 55208
diff changeset
   457
        (case AList.lookup (op =) args max_relevantK of
5d027af93a08 moved ML code around
blanchet
parents: 55208
diff changeset
   458
          SOME max => max
5d027af93a08 moved ML code around
blanchet
parents: 55208
diff changeset
   459
        | NONE => max_facts_default))
47481
b5873d4ff1e2 gathered mirabelle_sledgehammer's hardcoded defaults
sultana
parents: 47480
diff changeset
   460
    val slice = AList.lookup (op =) args sliceK |> the_default slice_default
45514
973bb7846505 parse lambda translation option in Metis
blanchet
parents: 45512
diff changeset
   461
    val lam_trans = AList.lookup (op =) args lam_transK
46415
26153cbe97bf added option to Mirabelle/Sledgehammer
blanchet
parents: 46386
diff changeset
   462
    val uncurried_aliases = AList.lookup (op =) args uncurried_aliasesK
47032
73cdeed236c0 more weight attribute tuning
blanchet
parents: 47030
diff changeset
   463
    val e_selection_heuristic = AList.lookup (op =) args e_selection_heuristicK
47049
72bd3311ecba added term_order option to Mirabelle
blanchet
parents: 47032
diff changeset
   464
    val term_order = AList.lookup (op =) args term_orderK
44099
5e14f591515e support local HOATPs
blanchet
parents: 44090
diff changeset
   465
    val force_sos = AList.lookup (op =) args force_sosK
42725
64dea91bbe0e added "force_sos" options to control SPASS's and Vampire's use of SOS in experiments + added corresponding Mirabelle options
blanchet
parents: 42642
diff changeset
   466
      |> Option.map (curry (op <>) "false")
32525
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   467
    val dir = AList.lookup (op =) args keepK
32541
cea1716eb106 timeout option for ATPs
boehmes
parents: 32536
diff changeset
   468
    val timeout = Mirabelle.get_int_setting args (prover_timeoutK, 30)
41268
56b7e277fd7d higher hard timeout
blanchet
parents: 41266
diff changeset
   469
    (* always use a hard timeout, but give some slack so that the automatic
56b7e277fd7d higher hard timeout
blanchet
parents: 41266
diff changeset
   470
       minimizer has a chance to do its magic *)
46825
98300d5f9cc0 added sh_minimize and preplay_timeout options to Mirabelle's Sledgehammer action;
sultana
parents: 46641
diff changeset
   471
    val preplay_timeout = AList.lookup (op =) args preplay_timeoutK
98300d5f9cc0 added sh_minimize and preplay_timeout options to Mirabelle's Sledgehammer action;
sultana
parents: 46641
diff changeset
   472
      |> the_default preplay_timeout_default
56411
913dc982ef55 added option to Mirabelle
blanchet
parents: 55287
diff changeset
   473
    val isar_proofsLST = available_parameter args isar_proofsK "isar_proofs"
57782
b5dc0562c7fb renamed 'sh_minimize' to 'minimize'; compile;
blanchet
parents: 57753
diff changeset
   474
    val minimizeLST = available_parameter args minimizeK "minimize"
46826
4c80c4034f1d added max_new_mono_instances, max_mono_iters, to Mirabelle-Sledgehammer; changed sh_minimize to avoid setting Mirabelle-level defaults;
sultana
parents: 46825
diff changeset
   475
    val max_new_mono_instancesLST =
4c80c4034f1d added max_new_mono_instances, max_mono_iters, to Mirabelle-Sledgehammer; changed sh_minimize to avoid setting Mirabelle-level defaults;
sultana
parents: 46825
diff changeset
   476
      available_parameter args max_new_mono_instancesK max_new_mono_instancesK
4c80c4034f1d added max_new_mono_instances, max_mono_iters, to Mirabelle-Sledgehammer; changed sh_minimize to avoid setting Mirabelle-level defaults;
sultana
parents: 46825
diff changeset
   477
    val max_mono_itersLST = available_parameter args max_mono_itersK max_mono_itersK
48702
e1752ccccc34 increase defensive timeout that should typically not kick in thanks to solid time limits in Sledgehammer (otherwise, Mirabelle-based evaluations might be distorted)
boehmes
parents: 48558
diff changeset
   478
    val hard_timeout = SOME (4 * timeout)
41155
85da8cbb4966 added support for "type_sys" option to Mirabelle
blanchet
parents: 41154
diff changeset
   479
    val (msg, result) =
50352
db8cae658807 added MaSh learning to Mirabelle
blanchet
parents: 50334
diff changeset
   480
      run_sh prover_name fact_filter type_enc strict max_facts slice lam_trans
db8cae658807 added MaSh learning to Mirabelle
blanchet
parents: 50334
diff changeset
   481
        uncurried_aliases e_selection_heuristic term_order force_sos
57782
b5dc0562c7fb renamed 'sh_minimize' to 'minimize'; compile;
blanchet
parents: 57753
diff changeset
   482
        hard_timeout timeout preplay_timeout isar_proofsLST minimizeLST
47049
72bd3311ecba added term_order option to Mirabelle
blanchet
parents: 47032
diff changeset
   483
        max_new_mono_instancesLST max_mono_itersLST dir pos st
32525
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   484
  in
55211
5d027af93a08 moved ML code around
blanchet
parents: 55208
diff changeset
   485
    (case result of
40062
cfaebaa8588f make Sledgehammer minimizer fully work with SMT
blanchet
parents: 40061
diff changeset
   486
      SH_OK (time_isa, time_prover, names) =>
38700
fcb0fe4c2f27 make Mirabelle happy
blanchet
parents: 38590
diff changeset
   487
        let
46340
cac402c486b0 separate orthogonal components
blanchet
parents: 46320
diff changeset
   488
          fun get_thms (name, stature) =
50267
1da2e67242d6 moved thms_of_name to Sledgehammer_Util and removed copies, updated references
smolkas
parents: 49916
diff changeset
   489
            try (Sledgehammer_Util.thms_of_name (Proof.context_of st))
49916
412346127bfa fixed theorem lookup code in Isar proof reconstruction
blanchet
parents: 49914
diff changeset
   490
              name
47154
2c357e2b8436 more robustness in case a theorem cannot be retrieved (which typically happens with backtick facts)
blanchet
parents: 47060
diff changeset
   491
            |> Option.map (pair (name, stature))
32525
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   492
        in
32818
6c91e668b15e record max lemmas used
nipkow
parents: 32676
diff changeset
   493
          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
   494
          if trivial then () else change_data id inc_sh_nontriv_success;
32818
6c91e668b15e record max lemmas used
nipkow
parents: 32676
diff changeset
   495
          change_data id (inc_sh_lemmas (length names));
6c91e668b15e record max lemmas used
nipkow
parents: 32676
diff changeset
   496
          change_data id (inc_sh_max_lems (length names));
6c91e668b15e record max lemmas used
nipkow
parents: 32676
diff changeset
   497
          change_data id (inc_sh_time_isa time_isa);
40062
cfaebaa8588f make Sledgehammer minimizer fully work with SMT
blanchet
parents: 40061
diff changeset
   498
          change_data id (inc_sh_time_prover time_prover);
55285
e88ad20035f4 merged 'reconstructors' and 'proof methods'
blanchet
parents: 55212
diff changeset
   499
          proof_method := proof_method_from_msg args msg;
38826
f42f425edf24 drop chained facts
blanchet
parents: 38752
diff changeset
   500
          named_thms := SOME (map_filter get_thms names);
39340
3998dc0bf82b indicate which goals are trivial
blanchet
parents: 39337
diff changeset
   501
          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
   502
            string_of_int time_prover ^ ") [" ^ prover_name ^ "]:\n" ^ msg)
32525
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   503
        end
40062
cfaebaa8588f make Sledgehammer minimizer fully work with SMT
blanchet
parents: 40061
diff changeset
   504
    | SH_FAIL (time_isa, time_prover) =>
32536
ac56c62758d3 tuned stats
nipkow
parents: 32533
diff changeset
   505
        let
ac56c62758d3 tuned stats
nipkow
parents: 32533
diff changeset
   506
          val _ = change_data id (inc_sh_time_isa time_isa)
40062
cfaebaa8588f make Sledgehammer minimizer fully work with SMT
blanchet
parents: 40061
diff changeset
   507
          val _ = change_data id (inc_sh_time_prover_fail time_prover)
39340
3998dc0bf82b indicate which goals are trivial
blanchet
parents: 39337
diff changeset
   508
        in log (sh_tag id ^ triv_str ^ "failed: " ^ msg) end
55211
5d027af93a08 moved ML code around
blanchet
parents: 55208
diff changeset
   509
    | SH_ERROR => log (sh_tag id ^ "failed: " ^ msg))
32525
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   510
  end
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   511
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   512
end
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   513
44542
3f5fd3635281 beef up sledgehammer_tac in Mirabelle some more
blanchet
parents: 44487
diff changeset
   514
fun override_params prover type_enc timeout =
3f5fd3635281 beef up sledgehammer_tac in Mirabelle some more
blanchet
parents: 44487
diff changeset
   515
  [("provers", prover),
48293
914ca0827804 renamed Sledgehammer options
blanchet
parents: 48292
diff changeset
   516
   ("max_facts", "0"),
44542
3f5fd3635281 beef up sledgehammer_tac in Mirabelle some more
blanchet
parents: 44487
diff changeset
   517
   ("type_enc", type_enc),
46386
6b17c65d35c4 renamed Sledgehammer option
blanchet
parents: 46365
diff changeset
   518
   ("strict", "true"),
45706
418846ea4f99 renamed "slicing" to "slice"
blanchet
parents: 45520
diff changeset
   519
   ("slice", "false"),
44461
5e19eecb0e1c specify timeout for "sledgehammer_tac"
blanchet
parents: 44449
diff changeset
   520
   ("timeout", timeout |> Time.toSeconds |> string_of_int)]
44430
c6f0490d432f beef up "sledgehammer_tac" reconstructor
blanchet
parents: 44424
diff changeset
   521
57753
643e02500991 removed 'metisFT' support in Mirabelle
blanchet
parents: 57752
diff changeset
   522
fun run_proof_method trivial full name meth named_thms id
32567
de411627a985 explicitly export type abbreviations (as usual in SML97);
wenzelm
parents: 32564
diff changeset
   523
    ({pre=st, timeout, log, pos, ...}: Mirabelle.run_args) =
32525
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   524
  let
55285
e88ad20035f4 merged 'reconstructors' and 'proof methods'
blanchet
parents: 55212
diff changeset
   525
    fun do_method named_thms ctxt =
44462
d9a657c44380 more reliable "sledgehammer\_tac" reconstruction, by avoiding "insert_tac"
blanchet
parents: 44461
diff changeset
   526
      let
d9a657c44380 more reliable "sledgehammer\_tac" reconstruction, by avoiding "insert_tac"
blanchet
parents: 44461
diff changeset
   527
        val ref_of_str =
d9a657c44380 more reliable "sledgehammer\_tac" reconstruction, by avoiding "insert_tac"
blanchet
parents: 44461
diff changeset
   528
          suffix ";" #> Outer_Syntax.scan Position.none #> Parse_Spec.xthm
d9a657c44380 more reliable "sledgehammer\_tac" reconstruction, by avoiding "insert_tac"
blanchet
parents: 44461
diff changeset
   529
          #> fst
d9a657c44380 more reliable "sledgehammer\_tac" reconstruction, by avoiding "insert_tac"
blanchet
parents: 44461
diff changeset
   530
        val thms = named_thms |> maps snd
d9a657c44380 more reliable "sledgehammer\_tac" reconstruction, by avoiding "insert_tac"
blanchet
parents: 44461
diff changeset
   531
        val facts = named_thms |> map (ref_of_str o fst o fst)
48292
7fcee834c7f5 more code rationalization in relevance filter
blanchet
parents: 48289
diff changeset
   532
        val fact_override = {add = facts, del = [], only = true}
44566
bf8331161ad9 split timeout among ATPs in and add Metis to the mix as backup
blanchet
parents: 44542
diff changeset
   533
        fun my_timeout time_slice =
bf8331161ad9 split timeout among ATPs in and add Metis to the mix as backup
blanchet
parents: 44542
diff changeset
   534
          timeout |> Time.toReal |> curry Real.* time_slice |> Time.fromReal
bf8331161ad9 split timeout among ATPs in and add Metis to the mix as backup
blanchet
parents: 44542
diff changeset
   535
        fun sledge_tac time_slice prover type_enc =
44542
3f5fd3635281 beef up sledgehammer_tac in Mirabelle some more
blanchet
parents: 44487
diff changeset
   536
          Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt
55211
5d027af93a08 moved ML code around
blanchet
parents: 55208
diff changeset
   537
            (override_params prover type_enc (my_timeout time_slice)) fact_override
44462
d9a657c44380 more reliable "sledgehammer\_tac" reconstruction, by avoiding "insert_tac"
blanchet
parents: 44461
diff changeset
   538
      in
55285
e88ad20035f4 merged 'reconstructors' and 'proof methods'
blanchet
parents: 55212
diff changeset
   539
        if !meth = "sledgehammer_tac" then
57154
f0eff6393a32 basic setup for zipperposition prover
fleury
parents: 56811
diff changeset
   540
          sledge_tac 0.2 ATP_Proof.vampireN "mono_native"
f0eff6393a32 basic setup for zipperposition prover
fleury
parents: 56811
diff changeset
   541
          ORELSE' sledge_tac 0.2 ATP_Proof.eN "poly_guards??"
f0eff6393a32 basic setup for zipperposition prover
fleury
parents: 56811
diff changeset
   542
          ORELSE' sledge_tac 0.2 ATP_Proof.spassN "mono_native"
f0eff6393a32 basic setup for zipperposition prover
fleury
parents: 56811
diff changeset
   543
          ORELSE' sledge_tac 0.2 ATP_Proof.z3_tptpN "poly_tags??"
57751
f453bbc289fa modernized Mirabelle (a bit) and made it compile
blanchet
parents: 57154
diff changeset
   544
          ORELSE' SMT2_Solver.smt2_tac ctxt thms
55285
e88ad20035f4 merged 'reconstructors' and 'proof methods'
blanchet
parents: 55212
diff changeset
   545
        else if !meth = "smt" then
57751
f453bbc289fa modernized Mirabelle (a bit) and made it compile
blanchet
parents: 57154
diff changeset
   546
          SMT2_Solver.smt2_tac ctxt thms
45519
cd6e78cb6ee8 make metis reconstruction handling more flexible
blanchet
parents: 45514
diff changeset
   547
        else if full then
46320
0b8b73b49848 renamed two files to make room for a new file
blanchet
parents: 45706
diff changeset
   548
          Metis_Tactic.metis_tac [ATP_Proof_Reconstruct.full_typesN]
54500
f625e0e79dd1 refactoring
blanchet
parents: 54141
diff changeset
   549
            ATP_Proof_Reconstruct.default_metis_lam_trans ctxt thms
55285
e88ad20035f4 merged 'reconstructors' and 'proof methods'
blanchet
parents: 55212
diff changeset
   550
        else if String.isPrefix "metis (" (!meth) then
45519
cd6e78cb6ee8 make metis reconstruction handling more flexible
blanchet
parents: 45514
diff changeset
   551
          let
cd6e78cb6ee8 make metis reconstruction handling more flexible
blanchet
parents: 45514
diff changeset
   552
            val (type_encs, lam_trans) =
55285
e88ad20035f4 merged 'reconstructors' and 'proof methods'
blanchet
parents: 55212
diff changeset
   553
              !meth
45519
cd6e78cb6ee8 make metis reconstruction handling more flexible
blanchet
parents: 45514
diff changeset
   554
              |> Outer_Syntax.scan Position.start
cd6e78cb6ee8 make metis reconstruction handling more flexible
blanchet
parents: 45514
diff changeset
   555
              |> filter Token.is_proper |> tl
cd6e78cb6ee8 make metis reconstruction handling more flexible
blanchet
parents: 45514
diff changeset
   556
              |> Metis_Tactic.parse_metis_options |> fst
46320
0b8b73b49848 renamed two files to make room for a new file
blanchet
parents: 45706
diff changeset
   557
              |>> the_default [ATP_Proof_Reconstruct.partial_typesN]
54500
f625e0e79dd1 refactoring
blanchet
parents: 54141
diff changeset
   558
              ||> the_default ATP_Proof_Reconstruct.default_metis_lam_trans
45519
cd6e78cb6ee8 make metis reconstruction handling more flexible
blanchet
parents: 45514
diff changeset
   559
          in Metis_Tactic.metis_tac type_encs lam_trans ctxt thms end
55285
e88ad20035f4 merged 'reconstructors' and 'proof methods'
blanchet
parents: 55212
diff changeset
   560
        else if !meth = "metis" then
55211
5d027af93a08 moved ML code around
blanchet
parents: 55208
diff changeset
   561
          Metis_Tactic.metis_tac [] ATP_Proof_Reconstruct.default_metis_lam_trans ctxt thms
44462
d9a657c44380 more reliable "sledgehammer\_tac" reconstruction, by avoiding "insert_tac"
blanchet
parents: 44461
diff changeset
   562
        else
d9a657c44380 more reliable "sledgehammer\_tac" reconstruction, by avoiding "insert_tac"
blanchet
parents: 44461
diff changeset
   563
          K all_tac
d9a657c44380 more reliable "sledgehammer\_tac" reconstruction, by avoiding "insert_tac"
blanchet
parents: 44461
diff changeset
   564
      end
55285
e88ad20035f4 merged 'reconstructors' and 'proof methods'
blanchet
parents: 55212
diff changeset
   565
    fun apply_method named_thms =
e88ad20035f4 merged 'reconstructors' and 'proof methods'
blanchet
parents: 55212
diff changeset
   566
      Mirabelle.can_apply timeout (do_method named_thms) st
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   567
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   568
    fun with_time (false, t) = "failed (" ^ string_of_int t ^ ")"
57753
643e02500991 removed 'metisFT' support in Mirabelle
blanchet
parents: 57752
diff changeset
   569
      | with_time (true, t) = (change_data id inc_proof_method_success;
40667
b8579f24ce67 make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents: 40627
diff changeset
   570
          if trivial then ()
57753
643e02500991 removed 'metisFT' support in Mirabelle
blanchet
parents: 57752
diff changeset
   571
          else change_data id inc_proof_method_nontriv_success;
643e02500991 removed 'metisFT' support in Mirabelle
blanchet
parents: 57752
diff changeset
   572
          change_data id (inc_proof_method_lemmas (length named_thms));
643e02500991 removed 'metisFT' support in Mirabelle
blanchet
parents: 57752
diff changeset
   573
          change_data id (inc_proof_method_time t);
643e02500991 removed 'metisFT' support in Mirabelle
blanchet
parents: 57752
diff changeset
   574
          change_data id (inc_proof_method_posns (pos, trivial));
643e02500991 removed 'metisFT' support in Mirabelle
blanchet
parents: 57752
diff changeset
   575
          if name = "proof" then change_data id inc_proof_method_proofs else ();
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   576
          "succeeded (" ^ string_of_int t ^ ")")
55285
e88ad20035f4 merged 'reconstructors' and 'proof methods'
blanchet
parents: 55212
diff changeset
   577
    fun timed_method named_thms =
e88ad20035f4 merged 'reconstructors' and 'proof methods'
blanchet
parents: 55212
diff changeset
   578
      (with_time (Mirabelle.cpu_time apply_method named_thms), true)
57753
643e02500991 removed 'metisFT' support in Mirabelle
blanchet
parents: 57752
diff changeset
   579
      handle TimeLimit.TimeOut => (change_data id inc_proof_method_timeout; ("timeout", false))
34052
b2e6245fb3da only invoke metisFT if metis failed
boehmes
parents: 34035
diff changeset
   580
           | ERROR msg => ("error: " ^ msg, false)
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   581
32525
ea322e847633 added signature ATP_MINIMAL,
boehmes
parents: 32523
diff changeset
   582
    val _ = log separator
57753
643e02500991 removed 'metisFT' support in Mirabelle
blanchet
parents: 57752
diff changeset
   583
    val _ = change_data id inc_proof_method_calls
643e02500991 removed 'metisFT' support in Mirabelle
blanchet
parents: 57752
diff changeset
   584
    val _ = if trivial then () else change_data id inc_proof_method_nontriv_calls
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   585
  in
44462
d9a657c44380 more reliable "sledgehammer\_tac" reconstruction, by avoiding "insert_tac"
blanchet
parents: 44461
diff changeset
   586
    named_thms
55285
e88ad20035f4 merged 'reconstructors' and 'proof methods'
blanchet
parents: 55212
diff changeset
   587
    |> timed_method
e88ad20035f4 merged 'reconstructors' and 'proof methods'
blanchet
parents: 55212
diff changeset
   588
    |>> log o prefix (proof_method_tag meth id)
34052
b2e6245fb3da only invoke metisFT if metis failed
boehmes
parents: 34035
diff changeset
   589
    |> snd
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32518
diff changeset
   590
  end
32385
594890623c46 split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff changeset
   591
41276
285aea0c153c two layers of timeouts seem to be less reliable than a single layer
blanchet
parents: 41275
diff changeset
   592
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
   593
44431
3e0ce0ae1022 added "max_calls" option to get a fixed number of Sledgehammer calls per theory
blanchet
parents: 44430
diff changeset
   594
(* crude hack *)
3e0ce0ae1022 added "max_calls" option to get a fixed number of Sledgehammer calls per theory
blanchet
parents: 44430
diff changeset
   595
val num_sledgehammer_calls = Unsynchronized.ref 0
3e0ce0ae1022 added "max_calls" option to get a fixed number of Sledgehammer calls per theory
blanchet
parents: 44430
diff changeset
   596
34035
08d34921b7dd also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents: 33316
diff changeset
   597
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
   598
  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
   599
    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
   600
    then () else
768d17f54125 use regular Proof.goal (which is what methods usually see) and prevent sledgehammer from crashing;
wenzelm
parents: 34052
diff changeset
   601
    let
44431
3e0ce0ae1022 added "max_calls" option to get a fixed number of Sledgehammer calls per theory
blanchet
parents: 44430
diff changeset
   602
      val max_calls =
47481
b5873d4ff1e2 gathered mirabelle_sledgehammer's hardcoded defaults
sultana
parents: 47480
diff changeset
   603
        AList.lookup (op =) args max_callsK |> the_default max_calls_default
44431
3e0ce0ae1022 added "max_calls" option to get a fixed number of Sledgehammer calls per theory
blanchet
parents: 44430
diff changeset
   604
        |> Int.fromString |> the
3e0ce0ae1022 added "max_calls" option to get a fixed number of Sledgehammer calls per theory
blanchet
parents: 44430
diff changeset
   605
      val _ = num_sledgehammer_calls := !num_sledgehammer_calls + 1;
44448
04bd6a9307c6 don't perform a triviality check if the goal is skipped anyway
blanchet
parents: 44447
diff changeset
   606
    in
44431
3e0ce0ae1022 added "max_calls" option to get a fixed number of Sledgehammer calls per theory
blanchet
parents: 44430
diff changeset
   607
      if !num_sledgehammer_calls > max_calls then ()
3e0ce0ae1022 added "max_calls" option to get a fixed number of Sledgehammer calls per theory
blanchet
parents: 44430
diff changeset
   608
      else
44448
04bd6a9307c6 don't perform a triviality check if the goal is skipped anyway
blanchet
parents: 44447
diff changeset
   609
        let
55285
e88ad20035f4 merged 'reconstructors' and 'proof methods'
blanchet
parents: 55212
diff changeset
   610
          val meth = Unsynchronized.ref ""
44448
04bd6a9307c6 don't perform a triviality check if the goal is skipped anyway
blanchet
parents: 44447
diff changeset
   611
          val named_thms =
46340
cac402c486b0 separate orthogonal components
blanchet
parents: 46320
diff changeset
   612
            Unsynchronized.ref (NONE : ((string * stature) * thm list) list option)
44448
04bd6a9307c6 don't perform a triviality check if the goal is skipped anyway
blanchet
parents: 44447
diff changeset
   613
          val trivial =
47481
b5873d4ff1e2 gathered mirabelle_sledgehammer's hardcoded defaults
sultana
parents: 47480
diff changeset
   614
            if AList.lookup (op =) args check_trivialK |> the_default trivial_default
51951
fab4ab92e812 more standard Isabelle/ML operations -- avoid inaccurate Bool.fromString;
wenzelm
parents: 51210
diff changeset
   615
                            |> Markup.parse_bool then
47201
06e6f352df1b made Mirabelle-SH's 'trivial' check optional;
sultana
parents: 47154
diff changeset
   616
              Try0.try0 (SOME try_timeout) ([], [], [], []) pre
06e6f352df1b made Mirabelle-SH's 'trivial' check optional;
sultana
parents: 47154
diff changeset
   617
              handle TimeLimit.TimeOut => false
06e6f352df1b made Mirabelle-SH's 'trivial' check optional;
sultana
parents: 47154
diff changeset
   618
            else false
57753
643e02500991 removed 'metisFT' support in Mirabelle
blanchet
parents: 57752
diff changeset
   619
          fun apply_method () =
643e02500991 removed 'metisFT' support in Mirabelle
blanchet
parents: 57752
diff changeset
   620
            (Mirabelle.catch_result (proof_method_tag meth) false
643e02500991 removed 'metisFT' support in Mirabelle
blanchet
parents: 57752
diff changeset
   621
              (run_proof_method trivial false name meth (these (!named_thms))) id st; ())
44448
04bd6a9307c6 don't perform a triviality check if the goal is skipped anyway
blanchet
parents: 44447
diff changeset
   622
        in
55285
e88ad20035f4 merged 'reconstructors' and 'proof methods'
blanchet
parents: 55212
diff changeset
   623
          Mirabelle.catch sh_tag (run_sledgehammer trivial args meth named_thms) id st;
57753
643e02500991 removed 'metisFT' support in Mirabelle
blanchet
parents: 57752
diff changeset
   624
          if is_some (!named_thms) then apply_method () else ()
44448
04bd6a9307c6 don't perform a triviality check if the goal is skipped anyway
blanchet
parents: 44447
diff changeset
   625
        end
35592
768d17f54125 use regular Proof.goal (which is what methods usually see) and prevent sledgehammer from crashing;
wenzelm
parents: 34052
diff changeset
   626
    end
32818
6c91e668b15e record max lemmas used
nipkow
parents: 32676
diff changeset
   627
  end
32385
594890623c46 split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff changeset
   628
32511
43d2ac4aa2de added option full_typed for sledgehammer action
boehmes
parents: 32510
diff changeset
   629
fun invoke args =
43569
b342cd125533 removed "full_types" option from Sledgehammer, now that virtually sound encodings are used as the default anyway
blanchet
parents: 43351
diff changeset
   630
  Mirabelle.register (init, sledgehammer_action args, done)
32385
594890623c46 split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff changeset
   631
594890623c46 split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff changeset
   632
end