author  blanchet 
Sun, 13 Jan 2013 22:00:45 +0100  
changeset 50868  4b30d461b3a6 
parent 50867  48836c35d636 
child 51003  198cb05fb35b 
permissions  rwrr 
47847  1 
(* Title: HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML 
32564  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 MirabelleSledgehammer 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 MirabelleSledgehammer 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 MirabelleSledgehammer 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 MirabelleSledgehammer 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 MirabelleSledgehammer 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 MirabelleSledgehammer action
sultana
parents:
47477
diff
changeset

13 
*) 
24d8c9e9dae4
Mirabelle's 'usage' description relating to Sledgehammer now synchs with the ML code of the MirabelleSledgehammer 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 MirabelleSledgehammer 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 MirabelleSledgehammer 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 MirabelleSledgehammer 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 MirabelleSledgehammer action
sultana
parents:
47477
diff
changeset

18 
val minimizeK = "minimize" (*: enable minimization of theorem set found by sledgehammer*) 
24d8c9e9dae4
Mirabelle's 'usage' description relating to Sledgehammer now synchs with the ML code of the MirabelleSledgehammer action
sultana
parents:
47477
diff
changeset

19 
(*refers to minimization attempted by Mirabelle*) 
24d8c9e9dae4
Mirabelle's 'usage' description relating to Sledgehammer now synchs with the ML code of the MirabelleSledgehammer action
sultana
parents:
47477
diff
changeset

20 
val minimize_timeoutK = "minimize_timeout" (*=TIME: timeout for each minimization step (seconds of*) 
24d8c9e9dae4
Mirabelle's 'usage' description relating to Sledgehammer now synchs with the ML code of the MirabelleSledgehammer action
sultana
parents:
47477
diff
changeset

21 

24d8c9e9dae4
Mirabelle's 'usage' description relating to Sledgehammer now synchs with the ML code of the MirabelleSledgehammer action
sultana
parents:
47477
diff
changeset

22 
val reconstructorK = "reconstructor" (*=NAME: how to reconstruct proofs (ie. using metis/smt)*) 
24d8c9e9dae4
Mirabelle's 'usage' description relating to Sledgehammer now synchs with the ML code of the MirabelleSledgehammer action
sultana
parents:
47477
diff
changeset

23 
val metis_ftK = "metis_ft" (*: apply metis with fullytyped encoding to the theorems found by sledgehammer*) 
24d8c9e9dae4
Mirabelle's 'usage' description relating to Sledgehammer now synchs with the ML code of the MirabelleSledgehammer action
sultana
parents:
47477
diff
changeset

24 

48293  25 
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 MirabelleSledgehammer action
sultana
parents:
47477
diff
changeset

26 
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 MirabelleSledgehammer action
sultana
parents:
47477
diff
changeset

27 
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 MirabelleSledgehammer action
sultana
parents:
47477
diff
changeset

28 
val preplay_timeoutK = "preplay_timeout" (*=TIME: timeout for finding reconstructed proof*) 
24d8c9e9dae4
Mirabelle's 'usage' description relating to Sledgehammer now synchs with the ML code of the MirabelleSledgehammer action
sultana
parents:
47477
diff
changeset

29 
val sh_minimizeK = "sh_minimize" (*: instruct sledgehammer to run its minimizer*) 
24d8c9e9dae4
Mirabelle's 'usage' description relating to Sledgehammer now synchs with the ML code of the MirabelleSledgehammer action
sultana
parents:
47477
diff
changeset

30 

24d8c9e9dae4
Mirabelle's 'usage' description relating to Sledgehammer now synchs with the ML code of the MirabelleSledgehammer action
sultana
parents:
47477
diff
changeset

31 
val check_trivialK = "check_trivial" (*: check if goals are "trivial" (false by default)*) 
50334  32 
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 MirabelleSledgehammer action
sultana
parents:
47477
diff
changeset

33 
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 MirabelleSledgehammer action
sultana
parents:
47477
diff
changeset

34 
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 MirabelleSledgehammer action
sultana
parents:
47477
diff
changeset

35 
val strictK = "strict" (*=BOOL: run in strict mode*) 
24d8c9e9dae4
Mirabelle's 'usage' description relating to Sledgehammer now synchs with the ML code of the MirabelleSledgehammer action
sultana
parents:
47477
diff
changeset

36 
val sliceK = "slice" (*=BOOL: allow sledgehammerlevel strategyscheduling*) 
24d8c9e9dae4
Mirabelle's 'usage' description relating to Sledgehammer now synchs with the ML code of the MirabelleSledgehammer action
sultana
parents:
47477
diff
changeset

37 
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 MirabelleSledgehammer action
sultana
parents:
47477
diff
changeset

38 
val e_selection_heuristicK = "e_selection_heuristic" (*: FIXME*) 
24d8c9e9dae4
Mirabelle's 'usage' description relating to Sledgehammer now synchs with the ML code of the MirabelleSledgehammer action
sultana
parents:
47477
diff
changeset

39 
val term_orderK = "term_order" (*: FIXME*) 
24d8c9e9dae4
Mirabelle's 'usage' description relating to Sledgehammer now synchs with the ML code of the MirabelleSledgehammer action
sultana
parents:
47477
diff
changeset

40 
val force_sosK = "force_sos" (*: use SOS*) 
24d8c9e9dae4
Mirabelle's 'usage' description relating to Sledgehammer now synchs with the ML code of the MirabelleSledgehammer action
sultana
parents:
47477
diff
changeset

41 
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 MirabelleSledgehammer action
sultana
parents:
47477
diff
changeset

42 
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

43 

32521  44 
fun sh_tag id = "#" ^ string_of_int id ^ " sledgehammer: " 
32525  45 
fun minimize_tag id = "#" ^ string_of_int id ^ " minimize (sledgehammer): " 
40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

46 
fun reconstructor_tag reconstructor id = 
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

47 
"#" ^ string_of_int id ^ " " ^ (!reconstructor) ^ " (sledgehammer): " 
32521  48 

32525  49 
val separator = "" 
50 

47481
b5873d4ff1e2
gathered mirabelle_sledgehammer's hardcoded defaults
sultana
parents:
47480
diff
changeset

51 
(*FIXME sensible to have Mirabellelevel Sledgehammer defaults?*) 
b5873d4ff1e2
gathered mirabelle_sledgehammer's hardcoded defaults
sultana
parents:
47480
diff
changeset

52 
(*defaults used in this Mirabelle action*) 
46825
98300d5f9cc0
added sh_minimize and preplay_timeout options to Mirabelle's Sledgehammer action;
sultana
parents:
46641
diff
changeset

53 
val preplay_timeout_default = "4" 
47481
b5873d4ff1e2
gathered mirabelle_sledgehammer's hardcoded defaults
sultana
parents:
47480
diff
changeset

54 
val lam_trans_default = "smart" 
b5873d4ff1e2
gathered mirabelle_sledgehammer's hardcoded defaults
sultana
parents:
47480
diff
changeset

55 
val uncurried_aliases_default = "smart" 
50334  56 
val fact_filter_default = "smart" 
47481
b5873d4ff1e2
gathered mirabelle_sledgehammer's hardcoded defaults
sultana
parents:
47480
diff
changeset

57 
val type_enc_default = "smart" 
b5873d4ff1e2
gathered mirabelle_sledgehammer's hardcoded defaults
sultana
parents:
47480
diff
changeset

58 
val strict_default = "false" 
48293  59 
val max_facts_default = "smart" 
47481
b5873d4ff1e2
gathered mirabelle_sledgehammer's hardcoded defaults
sultana
parents:
47480
diff
changeset

60 
val slice_default = "true" 
b5873d4ff1e2
gathered mirabelle_sledgehammer's hardcoded defaults
sultana
parents:
47480
diff
changeset

61 
val max_calls_default = "10000000" 
b5873d4ff1e2
gathered mirabelle_sledgehammer's hardcoded defaults
sultana
parents:
47480
diff
changeset

62 
val trivial_default = "false" 
b5873d4ff1e2
gathered mirabelle_sledgehammer's hardcoded defaults
sultana
parents:
47480
diff
changeset

63 
val minimize_timeout_default = 5 
46826
4c80c4034f1d
added max_new_mono_instances, max_mono_iters, to MirabelleSledgehammer; changed sh_minimize to avoid setting Mirabellelevel defaults;
sultana
parents:
46825
diff
changeset

64 

4c80c4034f1d
added max_new_mono_instances, max_mono_iters, to MirabelleSledgehammer; changed sh_minimize to avoid setting Mirabellelevel defaults;
sultana
parents:
46825
diff
changeset

65 
(*If a key is present in args then augment a list with its pair*) 
4c80c4034f1d
added max_new_mono_instances, max_mono_iters, to MirabelleSledgehammer; changed sh_minimize to avoid setting Mirabellelevel defaults;
sultana
parents:
46825
diff
changeset

66 
(*This is used to avoid fixing default values at the Mirabelle level, and 
4c80c4034f1d
added max_new_mono_instances, max_mono_iters, to MirabelleSledgehammer; changed sh_minimize to avoid setting Mirabellelevel defaults;
sultana
parents:
46825
diff
changeset

67 
instead use the default values of the tool (Sledgehammer in this case).*) 
4c80c4034f1d
added max_new_mono_instances, max_mono_iters, to MirabelleSledgehammer; changed sh_minimize to avoid setting Mirabellelevel defaults;
sultana
parents:
46825
diff
changeset

68 
fun available_parameter args key label list = 
4c80c4034f1d
added max_new_mono_instances, max_mono_iters, to MirabelleSledgehammer; changed sh_minimize to avoid setting Mirabellelevel defaults;
sultana
parents:
46825
diff
changeset

69 
let 
4c80c4034f1d
added max_new_mono_instances, max_mono_iters, to MirabelleSledgehammer; changed sh_minimize to avoid setting Mirabellelevel defaults;
sultana
parents:
46825
diff
changeset

70 
val value = AList.lookup (op =) args key 
4c80c4034f1d
added max_new_mono_instances, max_mono_iters, to MirabelleSledgehammer; changed sh_minimize to avoid setting Mirabellelevel defaults;
sultana
parents:
46825
diff
changeset

71 
in if is_some value then (label, the value) :: list else list end 
4c80c4034f1d
added max_new_mono_instances, max_mono_iters, to MirabelleSledgehammer; changed sh_minimize to avoid setting Mirabellelevel defaults;
sultana
parents:
46825
diff
changeset

72 

32521  73 

32549  74 
datatype sh_data = ShData of { 
75 
calls: int, 

76 
success: int, 

39337
ffa577c0bbfa
keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents:
39321
diff
changeset

77 
nontriv_calls: int, 
ffa577c0bbfa
keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents:
39321
diff
changeset

78 
nontriv_success: int, 
32585  79 
lemmas: int, 
32818  80 
max_lems: int, 
32549  81 
time_isa: int, 
40062  82 
time_prover: int, 
83 
time_prover_fail: int} 

32549  84 

40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

85 
datatype re_data = ReData of { 
32549  86 
calls: int, 
87 
success: int, 

39337
ffa577c0bbfa
keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents:
39321
diff
changeset

88 
nontriv_calls: int, 
ffa577c0bbfa
keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents:
39321
diff
changeset

89 
nontriv_success: int, 
32676  90 
proofs: int, 
32549  91 
time: int, 
32550  92 
timeout: int, 
32990  93 
lemmas: int * int * int, 
39341
d2b981a0429a
indicate triviality in the list of proved things
blanchet
parents:
39340
diff
changeset

94 
posns: (Position.T * bool) list 
32550  95 
} 
32549  96 

32571
d4bb776874b8
count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents:
32567
diff
changeset

97 
datatype min_data = MinData of { 
32609  98 
succs: int, 
35866
513074557e06
move the Sledgehammer Isar commands together into one file;
blanchet
parents:
35830
diff
changeset

99 
ab_ratios: int 
32571
d4bb776874b8
count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents:
32567
diff
changeset

100 
} 
32521  101 

32818  102 
fun make_sh_data 
39337
ffa577c0bbfa
keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents:
39321
diff
changeset

103 
(calls,success,nontriv_calls,nontriv_success,lemmas,max_lems,time_isa, 
40062  104 
time_prover,time_prover_fail) = 
39337
ffa577c0bbfa
keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents:
39321
diff
changeset

105 
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

106 
nontriv_success=nontriv_success, lemmas=lemmas, max_lems=max_lems, 
40062  107 
time_isa=time_isa, time_prover=time_prover, 
108 
time_prover_fail=time_prover_fail} 

32521  109 

35866
513074557e06
move the Sledgehammer Isar commands together into one file;
blanchet
parents:
35830
diff
changeset

110 
fun make_min_data (succs, ab_ratios) = 
513074557e06
move the Sledgehammer Isar commands together into one file;
blanchet
parents:
35830
diff
changeset

111 
MinData{succs=succs, ab_ratios=ab_ratios} 
32571
d4bb776874b8
count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents:
32567
diff
changeset

112 

40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

113 
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

114 
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

115 
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

116 
nontriv_success=nontriv_success, proofs=proofs, time=time, 
32990  117 
timeout=timeout, lemmas=lemmas, posns=posns} 
32549  118 

39337
ffa577c0bbfa
keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents:
39321
diff
changeset

119 
val empty_sh_data = make_sh_data (0, 0, 0, 0, 0, 0, 0, 0, 0) 
35871
c93bda4fdf15
remove the iteration counter from Sledgehammer's minimizer
blanchet
parents:
35867
diff
changeset

120 
val empty_min_data = make_min_data (0, 0) 
40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

121 
val empty_re_data = make_re_data (0, 0, 0, 0, 0, 0, 0, (0,0,0), []) 
34035
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

122 

39337
ffa577c0bbfa
keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents:
39321
diff
changeset

123 
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

124 
lemmas, max_lems, time_isa, 
40062  125 
time_prover, time_prover_fail}) = (calls, success, nontriv_calls, 
126 
nontriv_success, lemmas, max_lems, time_isa, time_prover, time_prover_fail) 

34035
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

127 

35866
513074557e06
move the Sledgehammer Isar commands together into one file;
blanchet
parents:
35830
diff
changeset

128 
fun tuple_of_min_data (MinData {succs, ab_ratios}) = (succs, ab_ratios) 
34035
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

129 

40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

130 
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

131 
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

132 
nontriv_success, proofs, time, timeout, lemmas, posns) 
34035
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

133 

08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

134 

40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

135 
datatype reconstructor_mode = 
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

136 
Unminimized  Minimized  UnminimizedFT  MinimizedFT 
34035
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

137 

08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

138 
datatype data = Data of { 
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

139 
sh: sh_data, 
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

140 
min: min_data, 
40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

141 
re_u: re_data, (* reconstructor with unminimized set of lemmas *) 
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

142 
re_m: re_data, (* reconstructor with minimized set of lemmas *) 
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

143 
re_uft: re_data, (* reconstructor with unminimized set of lemmas and fullytyped *) 
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

144 
re_mft: re_data, (* reconstructor with minimized set of lemmas and fullytyped *) 
34035
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

145 
mini: bool (* with minimization *) 
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

146 
} 
32521  147 

40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

148 
fun make_data (sh, min, re_u, re_m, re_uft, re_mft, mini) = 
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

149 
Data {sh=sh, min=min, re_u=re_u, re_m=re_m, re_uft=re_uft, re_mft=re_mft, 
34035
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

150 
mini=mini} 
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

151 

08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

152 
val empty_data = make_data (empty_sh_data, empty_min_data, 
40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

153 
empty_re_data, empty_re_data, empty_re_data, empty_re_data, false) 
34035
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

154 

40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

155 
fun map_sh_data f (Data {sh, min, re_u, re_m, re_uft, re_mft, mini}) = 
34035
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

156 
let val sh' = make_sh_data (f (tuple_of_sh_data sh)) 
40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

157 
in make_data (sh', min, re_u, re_m, re_uft, re_mft, mini) end 
34035
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

158 

40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

159 
fun map_min_data f (Data {sh, min, re_u, re_m, re_uft, re_mft, mini}) = 
34035
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

160 
let val min' = make_min_data (f (tuple_of_min_data min)) 
40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

161 
in make_data (sh, min', re_u, re_m, re_uft, re_mft, mini) end 
32521  162 

40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

163 
fun map_re_data f m (Data {sh, min, re_u, re_m, re_uft, re_mft, mini}) = 
34035
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

164 
let 
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

165 
fun map_me g Unminimized (u, m, uft, mft) = (g u, m, uft, mft) 
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

166 
 map_me g Minimized (u, m, uft, mft) = (u, g m, uft, mft) 
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

167 
 map_me g UnminimizedFT (u, m, uft, mft) = (u, m, g uft, mft) 
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

168 
 map_me g MinimizedFT (u, m, uft, mft) = (u, m, uft, g mft) 
32521  169 

40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

170 
val f' = make_re_data o f o tuple_of_re_data 
32571
d4bb776874b8
count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents:
32567
diff
changeset

171 

40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

172 
val (re_u', re_m', re_uft', re_mft') = 
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

173 
map_me f' m (re_u, re_m, re_uft, re_mft) 
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

174 
in make_data (sh, min, re_u', re_m', re_uft', re_mft', mini) end 
34035
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

175 

40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

176 
fun set_mini mini (Data {sh, min, re_u, re_m, re_uft, re_mft, ...}) = 
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

177 
make_data (sh, min, re_u, re_m, re_uft, re_mft, mini) 
32990  178 

179 
fun inc_max (n:int) (s,sos,m) = (s+n, sos + n*n, Int.max(m,n)); 

32521  180 

32818  181 
val inc_sh_calls = map_sh_data 
40062  182 
(fn (calls, success, nontriv_calls, nontriv_success, lemmas,max_lems, time_isa, time_prover, time_prover_fail) 
183 
=> (calls + 1, success, nontriv_calls, nontriv_success, lemmas, max_lems, time_isa, time_prover, time_prover_fail)) 

32549  184 

32818  185 
val inc_sh_success = map_sh_data 
40062  186 
(fn (calls, success, nontriv_calls, nontriv_success, lemmas,max_lems, time_isa, time_prover, time_prover_fail) 
187 
=> (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

188 

ffa577c0bbfa
keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents:
39321
diff
changeset

189 
val inc_sh_nontriv_calls = map_sh_data 
40062  190 
(fn (calls, success, nontriv_calls, nontriv_success, lemmas,max_lems, time_isa, time_prover, time_prover_fail) 
191 
=> (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

192 

ffa577c0bbfa
keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents:
39321
diff
changeset

193 
val inc_sh_nontriv_success = map_sh_data 
40062  194 
(fn (calls, success, nontriv_calls, nontriv_success, lemmas,max_lems, time_isa, time_prover, time_prover_fail) 
195 
=> (calls, success, nontriv_calls, nontriv_success + 1, lemmas,max_lems, time_isa, time_prover, time_prover_fail)) 

32585  196 

32818  197 
fun inc_sh_lemmas n = map_sh_data 
40062  198 
(fn (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_prover,time_prover_fail) 
199 
=> (calls,success,nontriv_calls, nontriv_success, lemmas+n,max_lems,time_isa,time_prover,time_prover_fail)) 

32521  200 

32818  201 
fun inc_sh_max_lems n = map_sh_data 
40062  202 
(fn (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_prover,time_prover_fail) 
203 
=> (calls,success,nontriv_calls, nontriv_success, lemmas,Int.max(max_lems,n),time_isa,time_prover,time_prover_fail)) 

32549  204 

32818  205 
fun inc_sh_time_isa t = map_sh_data 
40062  206 
(fn (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_prover,time_prover_fail) 
207 
=> (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa + t,time_prover,time_prover_fail)) 

32818  208 

40062  209 
fun inc_sh_time_prover t = map_sh_data 
210 
(fn (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_prover,time_prover_fail) 

211 
=> (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_prover + t,time_prover_fail)) 

32521  212 

40062  213 
fun inc_sh_time_prover_fail t = map_sh_data 
214 
(fn (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_prover,time_prover_fail) 

215 
=> (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

216 

32818  217 
val inc_min_succs = map_min_data 
35866
513074557e06
move the Sledgehammer Isar commands together into one file;
blanchet
parents:
35830
diff
changeset

218 
(fn (succs,ab_ratios) => (succs+1, ab_ratios)) 
32571
d4bb776874b8
count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents:
32567
diff
changeset

219 

32818  220 
fun inc_min_ab_ratios r = map_min_data 
35866
513074557e06
move the Sledgehammer Isar commands together into one file;
blanchet
parents:
35830
diff
changeset

221 
(fn (succs, ab_ratios) => (succs, ab_ratios+r)) 
32549  222 

40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

223 
val inc_reconstructor_calls = map_re_data 
39337
ffa577c0bbfa
keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents:
39321
diff
changeset

224 
(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

225 
=> (calls + 1, success, nontriv_calls, nontriv_success, proofs, time, timeout, lemmas,posns)) 
32533  226 

40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

227 
val inc_reconstructor_success = map_re_data 
39337
ffa577c0bbfa
keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents:
39321
diff
changeset

228 
(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

229 
=> (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

230 

40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

231 
val inc_reconstructor_nontriv_calls = map_re_data 
39337
ffa577c0bbfa
keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents:
39321
diff
changeset

232 
(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

233 
=> (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

234 

40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

235 
val inc_reconstructor_nontriv_success = map_re_data 
39337
ffa577c0bbfa
keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents:
39321
diff
changeset

236 
(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

237 
=> (calls, success, nontriv_calls, nontriv_success + 1, proofs, time, timeout, lemmas,posns)) 
32676  238 

40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

239 
val inc_reconstructor_proofs = map_re_data 
39337
ffa577c0bbfa
keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents:
39321
diff
changeset

240 
(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

241 
=> (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

242 

40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

243 
fun inc_reconstructor_time m t = map_re_data 
39337
ffa577c0bbfa
keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents:
39321
diff
changeset

244 
(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

245 
=> (calls, success, nontriv_calls, nontriv_success, proofs, time + t, timeout, lemmas,posns)) m 
32536  246 

40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

247 
val inc_reconstructor_timeout = map_re_data 
39337
ffa577c0bbfa
keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents:
39321
diff
changeset

248 
(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

249 
=> (calls, success, nontriv_calls, nontriv_success, proofs, time, timeout + 1, lemmas,posns)) 
32549  250 

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 
fun inc_reconstructor_lemmas m n = map_re_data 
39337
ffa577c0bbfa
keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents:
39321
diff
changeset

252 
(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

253 
=> (calls, success, nontriv_calls, nontriv_success, proofs, time, timeout, inc_max n lemmas, posns)) m 
32551
421323205efd
position information is now passed to all actions;
nipkow
parents:
32550
diff
changeset

254 

40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

255 
fun inc_reconstructor_posns m pos = map_re_data 
39337
ffa577c0bbfa
keep track of trivial vs. nontrivial calls using "try" for 30 seconds
blanchet
parents:
39321
diff
changeset

256 
(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

257 
=> (calls, success, nontriv_calls, nontriv_success, proofs, time, timeout, lemmas, pos::posns)) m 
32521  258 

44090  259 
val str0 = string_of_int o the_default 0 
260 

32521  261 
local 
262 

263 
val str = string_of_int 

264 
val str3 = Real.fmt (StringCvt.FIX (SOME 3)) 

265 
fun percentage a b = string_of_int (a * 100 div b) 

266 
fun time t = Real.fromInt t / 1000.0 

267 
fun avg_time t n = 

268 
if n > 0 then (Real.fromInt t / 1000.0) / Real.fromInt n else 0.0 

269 

34035
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

270 
fun log_sh_data log 
40062  271 
(calls, success, nontriv_calls, nontriv_success, lemmas, max_lems, time_isa, time_prover, time_prover_fail) = 
32818  272 
(log ("Total number of sledgehammer calls: " ^ str calls); 
273 
log ("Number of successful sledgehammer calls: " ^ str success); 

274 
log ("Number of sledgehammer lemmas: " ^ str lemmas); 

275 
log ("Max number of sledgehammer lemmas: " ^ str max_lems); 

276 
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

277 
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

278 
log ("Number of successful nontrivial sledgehammer calls: " ^ str nontriv_success); 
32818  279 
log ("Total time for sledgehammer calls (Isabelle): " ^ str3 (time time_isa)); 
40062  280 
log ("Total time for successful sledgehammer calls (ATP): " ^ str3 (time time_prover)); 
281 
log ("Total time for failed sledgehammer calls (ATP): " ^ str3 (time time_prover_fail)); 

32536  282 
log ("Average time for sledgehammer calls (Isabelle): " ^ 
32818  283 
str3 (avg_time time_isa calls)); 
32533  284 
log ("Average time for successful sledgehammer calls (ATP): " ^ 
40062  285 
str3 (avg_time time_prover success)); 
32536  286 
log ("Average time for failed sledgehammer calls (ATP): " ^ 
40062  287 
str3 (avg_time time_prover_fail (calls  success))) 
32533  288 
) 
32521  289 

39341
d2b981a0429a
indicate triviality in the list of proved things
blanchet
parents:
39340
diff
changeset

290 
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

291 
str0 (Position.line_of pos) ^ ":" ^ str0 (Position.offset_of pos) ^ 
44090  292 
(if triv then "[T]" else "") 
32551
421323205efd
position information is now passed to all actions;
nipkow
parents:
32550
diff
changeset

293 

40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

294 
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

295 
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

296 
(lemmas, lems_sos, lems_max), re_posns) = 
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

297 
(log ("Total number of " ^ tag ^ "reconstructor calls: " ^ str re_calls); 
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

298 
log ("Number of successful " ^ tag ^ "reconstructor calls: " ^ str re_success ^ 
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

299 
" (proof: " ^ str re_proofs ^ ")"); 
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

300 
log ("Number of " ^ tag ^ "reconstructor timeouts: " ^ str re_timeout); 
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

301 
log ("Success rate: " ^ percentage re_success sh_calls ^ "%"); 
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

302 
log ("Total number of nontrivial " ^ tag ^ "reconstructor calls: " ^ str re_nontriv_calls); 
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

303 
log ("Number of successful nontrivial " ^ tag ^ "reconstructor calls: " ^ str re_nontriv_success ^ 
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

304 
" (proof: " ^ str re_proofs ^ ")"); 
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

305 
log ("Number of successful " ^ tag ^ "reconstructor lemmas: " ^ str lemmas); 
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

306 
log ("SOS of successful " ^ tag ^ "reconstructor lemmas: " ^ str lems_sos); 
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

307 
log ("Max number of successful " ^ tag ^ "reconstructor lemmas: " ^ str lems_max); 
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

308 
log ("Total time for successful " ^ tag ^ "reconstructor calls: " ^ str3 (time re_time)); 
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

309 
log ("Average time for successful " ^ tag ^ "reconstructor calls: " ^ 
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

310 
str3 (avg_time re_time re_success)); 
32551
421323205efd
position information is now passed to all actions;
nipkow
parents:
32550
diff
changeset

311 
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

312 
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

313 
else () 
421323205efd
position information is now passed to all actions;
nipkow
parents:
32550
diff
changeset

314 
) 
32571
d4bb776874b8
count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents:
32567
diff
changeset

315 

35866
513074557e06
move the Sledgehammer Isar commands together into one file;
blanchet
parents:
35830
diff
changeset

316 
fun log_min_data log (succs, ab_ratios) = 
32609  317 
(log ("Number of successful minimizations: " ^ string_of_int succs); 
35866
513074557e06
move the Sledgehammer Isar commands together into one file;
blanchet
parents:
35830
diff
changeset

318 
log ("After/before ratios: " ^ string_of_int ab_ratios) 
32571
d4bb776874b8
count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents:
32567
diff
changeset

319 
) 
d4bb776874b8
count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents:
32567
diff
changeset

320 

32521  321 
in 
322 

40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

323 
fun log_data id log (Data {sh, min, re_u, re_m, re_uft, re_mft, mini}) = 
34035
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

324 
let 
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

325 
val ShData {calls=sh_calls, ...} = sh 
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

326 

40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

327 
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

328 
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

329 
log_re_data log tag sh_calls (tuple_of_re_data m) 
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

330 
fun log_reconstructor (tag1, m1) (tag2, m2) = app_if m1 (fn () => 
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

331 
(log_re tag1 m1; log ""; app_if m2 (fn () => log_re tag2 m2))) 
34035
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

332 
in 
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

333 
if sh_calls > 0 
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

334 
then 
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

335 
(log ("\n\n\nReport #" ^ string_of_int id ^ ":\n"); 
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

336 
log_sh_data log (tuple_of_sh_data sh); 
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

337 
log ""; 
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

338 
if not mini 
40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

339 
then log_reconstructor ("", re_u) ("fullytyped ", re_uft) 
34035
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

340 
else 
40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

341 
app_if re_u (fn () => 
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

342 
(log_reconstructor ("unminimized ", re_u) ("unminimized fullytyped ", re_uft); 
34035
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

343 
log ""; 
40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

344 
app_if re_m (fn () => 
34035
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

345 
(log_min_data log (tuple_of_min_data min); log ""; 
40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

346 
log_reconstructor ("", re_m) ("fullytyped ", re_mft)))))) 
34035
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

347 
else () 
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

348 
end 
32521  349 

350 
end 

351 

352 

353 
(* Warning: we implicitly assume singlethreaded execution here! *) 

32740  354 
val data = Unsynchronized.ref ([] : (int * data) list) 
32521  355 

32740  356 
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

357 
fun done id ({log, ...}: Mirabelle.done_args) = 
32521  358 
AList.lookup (op =) (!data) id 
359 
> Option.map (log_data id log) 

360 
> K () 

361 

32740  362 
fun change_data id f = (Unsynchronized.change data (AList.map_entry (op =) id f); ()) 
32521  363 

50352  364 
fun get_prover_name ctxt args = 
33016
b73b74fe23c3
proper exceptions instead of unhandled partiality
boehmes
parents:
32991
diff
changeset

365 
let 
40062  366 
fun default_prover_name () = 
40069  367 
hd (#provers (Sledgehammer_Isar.default_params ctxt [])) 
47060
e2741ec9ae36
prefer explicitly qualified exception List.Empty;
wenzelm
parents:
47049
diff
changeset

368 
handle List.Empty => error "No ATP available." 
33016
b73b74fe23c3
proper exceptions instead of unhandled partiality
boehmes
parents:
32991
diff
changeset

369 
in 
b73b74fe23c3
proper exceptions instead of unhandled partiality
boehmes
parents:
32991
diff
changeset

370 
(case AList.lookup (op =) args proverK of 
50352  371 
SOME name => name 
372 
 NONE => default_prover_name ()) 

373 
end 

374 

375 
fun get_prover ctxt name params goal all_facts = 

376 
let 

377 
fun learn prover = 

378 
Sledgehammer_MaSh.mash_learn_proof ctxt params prover (prop_of goal) all_facts 

379 
in 

50668  380 
Sledgehammer_Minimize.get_minimizing_isar_prover ctxt Sledgehammer_Provers.Normal 
50352  381 
learn name 
33016
b73b74fe23c3
proper exceptions instead of unhandled partiality
boehmes
parents:
32991
diff
changeset

382 
end 
32525  383 

46340  384 
type stature = ATP_Problem_Generate.stature 
38752
6628adcae4a7
consider "locality" when assigning weights to facts
blanchet
parents:
38700
diff
changeset

385 

40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

386 
(* hack *) 
41357
ae76960d86a2
added "sledgehammer_tac" as possible reconstructor in Mirabelle
blanchet
parents:
41338
diff
changeset

387 
fun reconstructor_from_msg args msg = 
ae76960d86a2
added "sledgehammer_tac" as possible reconstructor in Mirabelle
blanchet
parents:
41338
diff
changeset

388 
(case AList.lookup (op =) args reconstructorK of 
ae76960d86a2
added "sledgehammer_tac" as possible reconstructor in Mirabelle
blanchet
parents:
41338
diff
changeset

389 
SOME name => name 
ae76960d86a2
added "sledgehammer_tac" as possible reconstructor in Mirabelle
blanchet
parents:
41338
diff
changeset

390 
 NONE => 
45519
cd6e78cb6ee8
make metis reconstruction handling more flexible
blanchet
parents:
45514
diff
changeset

391 
if String.isSubstring "metis (" msg then 
cd6e78cb6ee8
make metis reconstruction handling more flexible
blanchet
parents:
45514
diff
changeset

392 
msg > Substring.full 
cd6e78cb6ee8
make metis reconstruction handling more flexible
blanchet
parents:
45514
diff
changeset

393 
> Substring.position "metis (" 
cd6e78cb6ee8
make metis reconstruction handling more flexible
blanchet
parents:
45514
diff
changeset

394 
> snd > Substring.position ")" 
cd6e78cb6ee8
make metis reconstruction handling more flexible
blanchet
parents:
45514
diff
changeset

395 
> fst > Substring.string 
cd6e78cb6ee8
make metis reconstruction handling more flexible
blanchet
parents:
45514
diff
changeset

396 
> suffix ")" 
cd6e78cb6ee8
make metis reconstruction handling more flexible
blanchet
parents:
45514
diff
changeset

397 
else if String.isSubstring "metis" msg then 
cd6e78cb6ee8
make metis reconstruction handling more flexible
blanchet
parents:
45514
diff
changeset

398 
"metis" 
cd6e78cb6ee8
make metis reconstruction handling more flexible
blanchet
parents:
45514
diff
changeset

399 
else 
cd6e78cb6ee8
make metis reconstruction handling more flexible
blanchet
parents:
45514
diff
changeset

400 
"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

401 

32521  402 
local 
403 

32536  404 
datatype sh_result = 
46340  405 
SH_OK of int * int * (string * stature) list  
32536  406 
SH_FAIL of int * int  
407 
SH_ERROR 

408 

50352  409 
fun run_sh prover_name fact_filter type_enc strict max_facts slice 
50334  410 
lam_trans uncurried_aliases e_selection_heuristic term_order force_sos 
411 
hard_timeout timeout preplay_timeout sh_minimizeLST 

412 
max_new_mono_instancesLST max_mono_itersLST dir pos st = 

32521  413 
let 
38998  414 
val {context = ctxt, facts = chained_ths, goal} = Proof.goal st 
415 
val i = 1 

44090  416 
fun set_file_name (SOME dir) = 
41337
263fe1670067
mechanism to keep SMT input and output files around in Mirabelle
blanchet
parents:
41276
diff
changeset

417 
Config.put Sledgehammer_Provers.dest_dir dir 
44090  418 
#> Config.put Sledgehammer_Provers.problem_prefix 
44424  419 
("prob_" ^ str0 (Position.line_of pos) ^ "__") 
41337
263fe1670067
mechanism to keep SMT input and output files around in Mirabelle
blanchet
parents:
41276
diff
changeset

420 
#> Config.put SMT_Config.debug_files 
43088  421 
(dir ^ "/" ^ Name.desymbolize false (ATP_Util.timestamp ()) ^ "_" 
41338  422 
^ serial_string ()) 
44090  423 
 set_file_name NONE = I 
39321  424 
val st' = 
47030  425 
st 
426 
> Proof.map_context 

427 
(set_file_name dir 

47032  428 
#> (Option.map (Config.put ATP_Systems.e_selection_heuristic) 
429 
e_selection_heuristic > the_default I) 

47049  430 
#> (Option.map (Config.put ATP_Systems.term_order) 
431 
term_order > the_default I) 

47030  432 
#> (Option.map (Config.put ATP_Systems.force_sos) 
433 
force_sos > the_default I)) 

48293  434 
val params as {max_facts, slice, ...} = 
40069  435 
Sledgehammer_Isar.default_params ctxt 
46826
4c80c4034f1d
added max_new_mono_instances, max_mono_iters, to MirabelleSledgehammer; changed sh_minimize to avoid setting Mirabellelevel defaults;
sultana
parents:
46825
diff
changeset

436 
([("verbose", "true"), 
50334  437 
("fact_filter", fact_filter), 
43626
a867ebb12209
renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents:
43569
diff
changeset

438 
("type_enc", type_enc), 
46386  439 
("strict", strict), 
47481
b5873d4ff1e2
gathered mirabelle_sledgehammer's hardcoded defaults
sultana
parents:
47480
diff
changeset

440 
("lam_trans", lam_trans > the_default lam_trans_default), 
b5873d4ff1e2
gathered mirabelle_sledgehammer's hardcoded defaults
sultana
parents:
47480
diff
changeset

441 
("uncurried_aliases", uncurried_aliases > the_default uncurried_aliases_default), 
48293  442 
("max_facts", max_facts), 
45706  443 
("slice", slice), 
44448
04bd6a9307c6
don't perform a triviality check if the goal is skipped anyway
blanchet
parents:
44447
diff
changeset

444 
("timeout", string_of_int timeout), 
04bd6a9307c6
don't perform a triviality check if the goal is skipped anyway
blanchet
parents:
44447
diff
changeset

445 
("preplay_timeout", preplay_timeout)] 
46826
4c80c4034f1d
added max_new_mono_instances, max_mono_iters, to MirabelleSledgehammer; changed sh_minimize to avoid setting Mirabellelevel defaults;
sultana
parents:
46825
diff
changeset

446 
> sh_minimizeLST (*don't confuse the two minimization flags*) 
4c80c4034f1d
added max_new_mono_instances, max_mono_iters, to MirabelleSledgehammer; changed sh_minimize to avoid setting Mirabellelevel defaults;
sultana
parents:
46825
diff
changeset

447 
> max_new_mono_instancesLST 
4c80c4034f1d
added max_new_mono_instances, max_mono_iters, to MirabelleSledgehammer; changed sh_minimize to avoid setting Mirabellelevel defaults;
sultana
parents:
46825
diff
changeset

448 
> max_mono_itersLST) 
48293  449 
val default_max_facts = 
450 
Sledgehammer_Provers.default_max_facts_for_prover ctxt slice prover_name 

42952
96f62b77748f
tuning  the "appropriate" terminology is inspired from TPTP
blanchet
parents:
42944
diff
changeset

451 
val is_appropriate_prop = 
96f62b77748f
tuning  the "appropriate" terminology is inspired from TPTP
blanchet
parents:
42944
diff
changeset

452 
Sledgehammer_Provers.is_appropriate_prop_for_prover ctxt prover_name 
43088  453 
val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal i 
32574
719426c9e1eb
added hard timeout for sledgehammer based on elapsed time (no need to trust ATP's timeout handling);
boehmes
parents:
32571
diff
changeset

454 
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

455 
(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

456 
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

457 
 SOME secs => TimeLimit.timeLimit (Time.fromSeconds secs)) 
42953
26111aafab12
detect inappropriate problems and crashes better in Waldmeister
blanchet
parents:
42952
diff
changeset

458 
fun failed failure = 
45371  459 
({outcome = SOME failure, used_facts = [], run_time = Time.zeroTime, 
50669
84c7cf36b2e0
use "Lazy" to simplify control flow a bit and guarantee single evaluation (at most)
blanchet
parents:
50668
diff
changeset

460 
preplay = Lazy.value (Sledgehammer_Reconstruct.Failed_to_Play 
84c7cf36b2e0
use "Lazy" to simplify control flow a bit and guarantee single evaluation (at most)
blanchet
parents:
50668
diff
changeset

461 
Sledgehammer_Provers.plain_metis), 
43261
a4aeb26a6362
make sure that the message tail (timing + TPTP important message) is preserved upon automatic minimization
blanchet
parents:
43228
diff
changeset

462 
message = K "", message_tail = ""}, ~1) 
45371  463 
val ({outcome, used_facts, run_time, preplay, message, message_tail} 
464 
: Sledgehammer_Provers.prover_result, 

41275  465 
time_isa) = time_limit (Mirabelle.cpu_time (fn () => 
466 
let 

42953
26111aafab12
detect inappropriate problems and crashes better in Waldmeister
blanchet
parents:
42952
diff
changeset

467 
val _ = if is_appropriate_prop concl_t then () 
26111aafab12
detect inappropriate problems and crashes better in Waldmeister
blanchet
parents:
42952
diff
changeset

468 
else raise Fail "inappropriate" 
44625  469 
val ho_atp = Sledgehammer_Provers.is_ho_atp ctxt prover_name 
48299  470 
val reserved = Sledgehammer_Util.reserved_isar_keyword_table () 
471 
val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt 

41275  472 
val facts = 
48288
255c6e1fd505
rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents:
48250
diff
changeset

473 
Sledgehammer_Fact.nearly_all_facts ctxt ho_atp 
48299  474 
Sledgehammer_Fact.no_fact_override reserved css_table chained_ths 
475 
hyp_ts concl_t 

43351
b19d95b4d736
compute the set of base facts only once (instead of three times in parallel)  this saves about .5 s of CPU time, albeit much less clock wall time
blanchet
parents:
43261
diff
changeset

476 
> filter (is_appropriate_prop o prop_of o snd) 
48381  477 
> Sledgehammer_MaSh.relevant_facts ctxt params prover_name 
48293  478 
(the_default default_max_facts max_facts) 
48292  479 
Sledgehammer_Fact.no_fact_override hyp_ts concl_t 
50867  480 
> map (apfst (apfst (fn name => name ()))) 
481 
> tap (fn facts => 

50868  482 
"Line " ^ str0 (Position.line_of pos) ^ ": " ^ 
50867  483 
(if null facts then 
484 
"Found no relevant facts." 

485 
else 

486 
"Including " ^ string_of_int (length facts) ^ 

487 
" relevant fact(s):\n" ^ 

488 
(facts > map (fst o fst) > space_implode " ") ^ ".") 

489 
> Output.urgent_message) 

50352  490 
val prover = get_prover ctxt prover_name params goal facts 
41275  491 
val problem = 
492 
{state = st', goal = goal, subgoal = i, 

493 
subgoal_count = Sledgehammer_Util.subgoal_count st, 

50867  494 
facts = facts > map Sledgehammer_Provers.Untranslated_Fact} 
45520  495 
in prover params (K (K (K ""))) problem end)) () 
42953
26111aafab12
detect inappropriate problems and crashes better in Waldmeister
blanchet
parents:
42952
diff
changeset

496 
handle TimeLimit.TimeOut => failed ATP_Proof.TimedOut 
26111aafab12
detect inappropriate problems and crashes better in Waldmeister
blanchet
parents:
42952
diff
changeset

497 
 Fail "inappropriate" => failed ATP_Proof.Inappropriate 
45371  498 
val time_prover = run_time > Time.toMilliseconds 
50669
84c7cf36b2e0
use "Lazy" to simplify control flow a bit and guarantee single evaluation (at most)
blanchet
parents:
50668
diff
changeset

499 
val msg = message (Lazy.force preplay) ^ message_tail 
32521  500 
in 
36405  501 
case outcome of 
43052
8d6a4978cc65
automatically minimize with Metis when this can be done within a few seconds
blanchet
parents:
43051
diff
changeset

502 
NONE => (msg, SH_OK (time_isa, time_prover, used_facts)) 
8d6a4978cc65
automatically minimize with Metis when this can be done within a few seconds
blanchet
parents:
43051
diff
changeset

503 
 SOME _ => (msg, SH_FAIL (time_isa, time_prover)) 
32521  504 
end 
37994
b04307085a09
make TPTP generator accept full firstorder formulas
blanchet
parents:
37631
diff
changeset

505 
handle ERROR msg => ("error: " ^ msg, SH_ERROR) 
32521  506 

32498
1132c7c13f36
Mirabelle: actions are responsible for handling exceptions,
boehmes
parents:
32496
diff
changeset

507 
in 
1132c7c13f36
Mirabelle: actions are responsible for handling exceptions,
boehmes
parents:
32496
diff
changeset

508 

44090  509 
fun run_sledgehammer trivial args reconstructor named_thms id 
510 
({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

511 
let 
50352  512 
val ctxt = Proof.context_of st 
39340  513 
val triv_str = if trivial then "[T] " else "" 
32536  514 
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

515 
val _ = if trivial then () else change_data id inc_sh_nontriv_calls 
50352  516 
val prover_name = get_prover_name ctxt args 
50334  517 
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

518 
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

519 
val strict = AList.lookup (op =) args strictK > the_default strict_default 
48293  520 
val max_facts = 
521 
case AList.lookup (op =) args max_factsK of 

522 
SOME max => max 

523 
 NONE => case AList.lookup (op =) args max_relevantK of 

524 
SOME max => max 

525 
 NONE => max_facts_default 

47481
b5873d4ff1e2
gathered mirabelle_sledgehammer's hardcoded defaults
sultana
parents:
47480
diff
changeset

526 
val slice = AList.lookup (op =) args sliceK > the_default slice_default 
45514  527 
val lam_trans = AList.lookup (op =) args lam_transK 
46415  528 
val uncurried_aliases = AList.lookup (op =) args uncurried_aliasesK 
47032  529 
val e_selection_heuristic = AList.lookup (op =) args e_selection_heuristicK 
47049  530 
val term_order = AList.lookup (op =) args term_orderK 
44099  531 
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

532 
> Option.map (curry (op <>) "false") 
32525  533 
val dir = AList.lookup (op =) args keepK 
32541  534 
val timeout = Mirabelle.get_int_setting args (prover_timeoutK, 30) 
41268  535 
(* always use a hard timeout, but give some slack so that the automatic 
536 
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

537 
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

538 
> the_default preplay_timeout_default 
46826
4c80c4034f1d
added max_new_mono_instances, max_mono_iters, to MirabelleSledgehammer; changed sh_minimize to avoid setting Mirabellelevel defaults;
sultana
parents:
46825
diff
changeset

539 
val sh_minimizeLST = available_parameter args sh_minimizeK "minimize" 
4c80c4034f1d
added max_new_mono_instances, max_mono_iters, to MirabelleSledgehammer; changed sh_minimize to avoid setting Mirabellelevel defaults;
sultana
parents:
46825
diff
changeset

540 
val max_new_mono_instancesLST = 
4c80c4034f1d
added max_new_mono_instances, max_mono_iters, to MirabelleSledgehammer; changed sh_minimize to avoid setting Mirabellelevel defaults;
sultana
parents:
46825
diff
changeset

541 
available_parameter args max_new_mono_instancesK max_new_mono_instancesK 
4c80c4034f1d
added max_new_mono_instances, max_mono_iters, to MirabelleSledgehammer; changed sh_minimize to avoid setting Mirabellelevel defaults;
sultana
parents:
46825
diff
changeset

542 
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, Mirabellebased evaluations might be distorted)
boehmes
parents:
48558
diff
changeset

543 
val hard_timeout = SOME (4 * timeout) 
41155
85da8cbb4966
added support for "type_sys" option to Mirabelle
blanchet
parents:
41154
diff
changeset

544 
val (msg, result) = 
50352  545 
run_sh prover_name fact_filter type_enc strict max_facts slice lam_trans 
546 
uncurried_aliases e_selection_heuristic term_order force_sos 

47049  547 
hard_timeout timeout preplay_timeout sh_minimizeLST 
548 
max_new_mono_instancesLST max_mono_itersLST dir pos st 

32525  549 
in 
32536  550 
case result of 
40062  551 
SH_OK (time_isa, time_prover, names) => 
38700  552 
let 
46340  553 
fun get_thms (name, stature) = 
50267
1da2e67242d6
moved thms_of_name to Sledgehammer_Util and removed copies, updated references
smolkas
parents:
49916
diff
changeset

554 
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

555 
name 
47154
2c357e2b8436
more robustness in case a theorem cannot be retrieved (which typically happens with backtick facts)
blanchet
parents:
47060
diff
changeset

556 
> Option.map (pair (name, stature)) 
32525  557 
in 
32818  558 
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

559 
if trivial then () else change_data id inc_sh_nontriv_success; 
32818  560 
change_data id (inc_sh_lemmas (length names)); 
561 
change_data id (inc_sh_max_lems (length names)); 

562 
change_data id (inc_sh_time_isa time_isa); 

40062  563 
change_data id (inc_sh_time_prover time_prover); 
41357
ae76960d86a2
added "sledgehammer_tac" as possible reconstructor in Mirabelle
blanchet
parents:
41338
diff
changeset

564 
reconstructor := reconstructor_from_msg args msg; 
38826  565 
named_thms := SOME (map_filter get_thms names); 
39340  566 
log (sh_tag id ^ triv_str ^ "succeeded (" ^ string_of_int time_isa ^ "+" ^ 
40062  567 
string_of_int time_prover ^ ") [" ^ prover_name ^ "]:\n" ^ msg) 
32525  568 
end 
40062  569 
 SH_FAIL (time_isa, time_prover) => 
32536  570 
let 
571 
val _ = change_data id (inc_sh_time_isa time_isa) 

40062  572 
val _ = change_data id (inc_sh_time_prover_fail time_prover) 
39340  573 
in log (sh_tag id ^ triv_str ^ "failed: " ^ msg) end 
32536  574 
 SH_ERROR => log (sh_tag id ^ "failed: " ^ msg) 
32525  575 
end 
576 

577 
end 

578 

40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

579 
fun run_minimize args reconstructor named_thms id 
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

580 
({pre=st, log, ...}: Mirabelle.run_args) = 
32525  581 
let 
40069  582 
val ctxt = Proof.context_of st 
32571
d4bb776874b8
count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents:
32567
diff
changeset

583 
val n0 = length (these (!named_thms)) 
50352  584 
val prover_name = get_prover_name ctxt args 
47481
b5873d4ff1e2
gathered mirabelle_sledgehammer's hardcoded defaults
sultana
parents:
47480
diff
changeset

585 
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

586 
val strict = AList.lookup (op =) args strictK > the_default strict_default 
32525  587 
val timeout = 
588 
AList.lookup (op =) args minimize_timeoutK 

40627
becf5d5187cc
renamed raw "explode" function to "raw_explode" to emphasize its meaning;
wenzelm
parents:
40554
diff
changeset

589 
> Option.map (fst o read_int o raw_explode) (* FIXME Symbol.explode (?) *) 
47481
b5873d4ff1e2
gathered mirabelle_sledgehammer's hardcoded defaults
sultana
parents:
47480
diff
changeset

590 
> the_default minimize_timeout_default 
46825
98300d5f9cc0
added sh_minimize and preplay_timeout options to Mirabelle's Sledgehammer action;
sultana
parents:
46641
diff
changeset

591 
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

592 
> the_default preplay_timeout_default 
46826
4c80c4034f1d
added max_new_mono_instances, max_mono_iters, to MirabelleSledgehammer; changed sh_minimize to avoid setting Mirabellelevel defaults;
sultana
parents:
46825
diff
changeset

593 
val sh_minimizeLST = available_parameter args sh_minimizeK "minimize" 
4c80c4034f1d
added max_new_mono_instances, max_mono_iters, to MirabelleSledgehammer; changed sh_minimize to avoid setting Mirabellelevel defaults;
sultana
parents:
46825
diff
changeset

594 
val max_new_mono_instancesLST = 
4c80c4034f1d
added max_new_mono_instances, max_mono_iters, to MirabelleSledgehammer; changed sh_minimize to avoid setting Mirabellelevel defaults;
sultana
parents:
46825
diff
changeset

595 
available_parameter args max_new_mono_instancesK max_new_mono_instancesK 
4c80c4034f1d
added max_new_mono_instances, max_mono_iters, to MirabelleSledgehammer; changed sh_minimize to avoid setting Mirabellelevel defaults;
sultana
parents:
46825
diff
changeset

596 
val max_mono_itersLST = available_parameter args max_mono_itersK max_mono_itersK 
43064
b6e61d22fa61
made "explicit_apply" smarter  no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents:
43052
diff
changeset

597 
val params = Sledgehammer_Isar.default_params ctxt 
46826
4c80c4034f1d
added max_new_mono_instances, max_mono_iters, to MirabelleSledgehammer; changed sh_minimize to avoid setting Mirabellelevel defaults;
sultana
parents:
46825
diff
changeset

598 
([("provers", prover_name), 
41155
85da8cbb4966
added support for "type_sys" option to Mirabelle
blanchet
parents:
41154
diff
changeset

599 
("verbose", "true"), 
43626
a867ebb12209
renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents:
43569
diff
changeset

600 
("type_enc", type_enc), 
46386  601 
("strict", strict), 
44448
04bd6a9307c6
don't perform a triviality check if the goal is skipped anyway
blanchet
parents:
44447
diff
changeset

602 
("timeout", string_of_int timeout), 
46826
4c80c4034f1d
added max_new_mono_instances, max_mono_iters, to MirabelleSledgehammer; changed sh_minimize to avoid setting Mirabellelevel defaults;
sultana
parents:
46825
diff
changeset

603 
("preplay_timeout", preplay_timeout)] 
4c80c4034f1d
added max_new_mono_instances, max_mono_iters, to MirabelleSledgehammer; changed sh_minimize to avoid setting Mirabellelevel defaults;
sultana
parents:
46825
diff
changeset

604 
> sh_minimizeLST (*don't confuse the two minimization flags*) 
4c80c4034f1d
added max_new_mono_instances, max_mono_iters, to MirabelleSledgehammer; changed sh_minimize to avoid setting Mirabellelevel defaults;
sultana
parents:
46825
diff
changeset

605 
> max_new_mono_instancesLST 
4c80c4034f1d
added max_new_mono_instances, max_mono_iters, to MirabelleSledgehammer; changed sh_minimize to avoid setting Mirabellelevel defaults;
sultana
parents:
46825
diff
changeset

606 
> max_mono_itersLST) 
37587  607 
val minimize = 
48399
4bacc8983b3d
learn from SMT proofs when they can be minimized by Metis
blanchet
parents:
48381
diff
changeset

608 
Sledgehammer_Minimize.minimize_facts (K (K ())) prover_name params 
43064
b6e61d22fa61
made "explicit_apply" smarter  no need to force explicit applications in minimizer on all constants, better do it more fine granularly
blanchet
parents:
43052
diff
changeset

609 
true 1 (Sledgehammer_Util.subgoal_count st) 
32525  610 
val _ = log separator 
43261
a4aeb26a6362
make sure that the message tail (timing + TPTP important message) is preserved upon automatic minimization
blanchet
parents:
43228
diff
changeset

611 
val (used_facts, (preplay, message, message_tail)) = 
a4aeb26a6362
make sure that the message tail (timing + TPTP important message) is preserved upon automatic minimization
blanchet
parents:
43228
diff
changeset

612 
minimize st (these (!named_thms)) 
50669
84c7cf36b2e0
use "Lazy" to simplify control flow a bit and guarantee single evaluation (at most)
blanchet
parents:
50668
diff
changeset

613 
val msg = message (Lazy.force preplay) ^ message_tail 
32525  614 
in 
43052
8d6a4978cc65
automatically minimize with Metis when this can be done within a few seconds
blanchet
parents:
43051
diff
changeset

615 
case used_facts of 
8d6a4978cc65
automatically minimize with Metis when this can be done within a few seconds
blanchet
parents:
43051
diff
changeset

616 
SOME named_thms' => 
32609  617 
(change_data id inc_min_succs; 
618 
change_data id (inc_min_ab_ratios ((100 * length named_thms') div n0)); 

32571
d4bb776874b8
count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents:
32567
diff
changeset

619 
if length named_thms' = n0 
d4bb776874b8
count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents:
32567
diff
changeset

620 
then log (minimize_tag id ^ "already minimal") 
41357
ae76960d86a2
added "sledgehammer_tac" as possible reconstructor in Mirabelle
blanchet
parents:
41338
diff
changeset

621 
else (reconstructor := reconstructor_from_msg args msg; 
40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

622 
named_thms := SOME named_thms'; 
32571
d4bb776874b8
count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents:
32567
diff
changeset

623 
log (minimize_tag id ^ "succeeded:\n" ^ msg)) 
d4bb776874b8
count number of iterations required for minimization (and fixed bug: minimization was always called)
nipkow
parents:
32567
diff
changeset

624 
) 
43052
8d6a4978cc65
automatically minimize with Metis when this can be done within a few seconds
blanchet
parents:
43051
diff
changeset

625 
 NONE => log (minimize_tag id ^ "failed: " ^ msg) 
32525  626 
end 
627 

44542  628 
fun override_params prover type_enc timeout = 
629 
[("provers", prover), 

48293  630 
("max_facts", "0"), 
44542  631 
("type_enc", type_enc), 
46386  632 
("strict", "true"), 
45706  633 
("slice", "false"), 
44461  634 
("timeout", timeout > Time.toSeconds > string_of_int)] 
44430  635 

40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

636 
fun run_reconstructor trivial full m name reconstructor named_thms id 
32567
de411627a985
explicitly export type abbreviations (as usual in SML97);
wenzelm
parents:
32564
diff
changeset

637 
({pre=st, timeout, log, pos, ...}: Mirabelle.run_args) = 
32525  638 
let 
44462
d9a657c44380
more reliable "sledgehammer\_tac" reconstruction, by avoiding "insert_tac"
blanchet
parents:
44461
diff
changeset

639 
fun do_reconstructor named_thms ctxt = 
d9a657c44380
more reliable "sledgehammer\_tac" reconstruction, by avoiding "insert_tac"
blanchet
parents:
44461
diff
changeset

640 
let 
d9a657c44380
more reliable "sledgehammer\_tac" reconstruction, by avoiding "insert_tac"
blanchet
parents:
44461
diff
changeset

641 
val ref_of_str = 
d9a657c44380
more reliable "sledgehammer\_tac" reconstruction, by avoiding "insert_tac"
blanchet
parents:
44461
diff
changeset

642 
suffix ";" #> Outer_Syntax.scan Position.none #> Parse_Spec.xthm 
d9a657c44380
more reliable "sledgehammer\_tac" reconstruction, by avoiding "insert_tac"
blanchet
parents:
44461
diff
changeset

643 
#> fst 
d9a657c44380
more reliable "sledgehammer\_tac" reconstruction, by avoiding "insert_tac"
blanchet
parents:
44461
diff
changeset

644 
val thms = named_thms > maps snd 
d9a657c44380
more reliable "sledgehammer\_tac" reconstruction, by avoiding "insert_tac"
blanchet
parents:
44461
diff
changeset

645 
val facts = named_thms > map (ref_of_str o fst o fst) 
48292  646 
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

647 
fun my_timeout time_slice = 
bf8331161ad9
split timeout among ATPs in and add Metis to the mix as backup
blanchet
parents:
44542
diff
changeset

648 
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

649 
fun sledge_tac time_slice prover type_enc = 
44542  650 
Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt 
48292  651 
(override_params prover type_enc (my_timeout time_slice)) 
652 
fact_override 

44462
d9a657c44380
more reliable "sledgehammer\_tac" reconstruction, by avoiding "insert_tac"
blanchet
parents:
44461
diff
changeset

653 
in 
d9a657c44380
more reliable "sledgehammer\_tac" reconstruction, by avoiding "insert_tac"
blanchet
parents:
44461
diff
changeset

654 
if !reconstructor = "sledgehammer_tac" then 
48558
fabbed3abc1e
tweaks in preparation for type encoding evaluation
blanchet
parents:
48399
diff
changeset

655 
sledge_tac 0.2 ATP_Systems.vampireN "mono_native" 
fabbed3abc1e
tweaks in preparation for type encoding evaluation
blanchet
parents:
48399
diff
changeset

656 
ORELSE' sledge_tac 0.2 ATP_Systems.eN "poly_guards??" 
fabbed3abc1e
tweaks in preparation for type encoding evaluation
blanchet
parents:
48399
diff
changeset

657 
ORELSE' sledge_tac 0.2 ATP_Systems.spassN "mono_native" 
fabbed3abc1e
tweaks in preparation for type encoding evaluation
blanchet
parents:
48399
diff
changeset

658 
ORELSE' sledge_tac 0.2 ATP_Systems.z3_tptpN "poly_tags??" 
fabbed3abc1e
tweaks in preparation for type encoding evaluation
blanchet
parents:
48399
diff
changeset

659 
ORELSE' SMT_Solver.smt_tac ctxt thms 
44462
d9a657c44380
more reliable "sledgehammer\_tac" reconstruction, by avoiding "insert_tac"
blanchet
parents:
44461
diff
changeset

660 
else if !reconstructor = "smt" then 
d9a657c44380
more reliable "sledgehammer\_tac" reconstruction, by avoiding "insert_tac"
blanchet
parents:
44461
diff
changeset

661 
SMT_Solver.smt_tac ctxt thms 
45519
cd6e78cb6ee8
make metis reconstruction handling more flexible
blanchet
parents:
45514
diff
changeset

662 
else if full then 
46320  663 
Metis_Tactic.metis_tac [ATP_Proof_Reconstruct.full_typesN] 
664 
ATP_Proof_Reconstruct.metis_default_lam_trans ctxt thms 

45519
cd6e78cb6ee8
make metis reconstruction handling more flexible
blanchet
parents:
45514
diff
changeset

665 
else if String.isPrefix "metis (" (!reconstructor) then 
cd6e78cb6ee8
make metis reconstruction handling more flexible
blanchet
parents:
45514
diff
changeset

666 
let 
cd6e78cb6ee8
make metis reconstruction handling more flexible
blanchet
parents:
45514
diff
changeset

667 
val (type_encs, lam_trans) = 
cd6e78cb6ee8
make metis reconstruction handling more flexible
blanchet
parents:
45514
diff
changeset

668 
!reconstructor 
cd6e78cb6ee8
make metis reconstruction handling more flexible
blanchet
parents:
45514
diff
changeset

669 
> Outer_Syntax.scan Position.start 
cd6e78cb6ee8
make metis reconstruction handling more flexible
blanchet
parents:
45514
diff
changeset

670 
> filter Token.is_proper > tl 
cd6e78cb6ee8
make metis reconstruction handling more flexible
blanchet
parents:
45514
diff
changeset

671 
> Metis_Tactic.parse_metis_options > fst 
46320  672 
>> the_default [ATP_Proof_Reconstruct.partial_typesN] 
673 
> the_default ATP_Proof_Reconstruct.metis_default_lam_trans 

45519
cd6e78cb6ee8
make metis reconstruction handling more flexible
blanchet
parents:
45514
diff
changeset

674 
in Metis_Tactic.metis_tac type_encs lam_trans ctxt thms end 
44462
d9a657c44380
more reliable "sledgehammer\_tac" reconstruction, by avoiding "insert_tac"
blanchet
parents:
44461
diff
changeset

675 
else if !reconstructor = "metis" then 
46320  676 
Metis_Tactic.metis_tac [] ATP_Proof_Reconstruct.metis_default_lam_trans ctxt 
45519
cd6e78cb6ee8
make metis reconstruction handling more flexible
blanchet
parents:
45514
diff
changeset

677 
thms 
44462
d9a657c44380
more reliable "sledgehammer\_tac" reconstruction, by avoiding "insert_tac"
blanchet
parents:
44461
diff
changeset

678 
else 
d9a657c44380
more reliable "sledgehammer\_tac" reconstruction, by avoiding "insert_tac"
blanchet
parents:
44461
diff
changeset

679 
K all_tac 
d9a657c44380
more reliable "sledgehammer\_tac" reconstruction, by avoiding "insert_tac"
blanchet
parents:
44461
diff
changeset

680 
end 
d9a657c44380
more reliable "sledgehammer\_tac" reconstruction, by avoiding "insert_tac"
blanchet
parents:
44461
diff
changeset

681 
fun apply_reconstructor named_thms = 
d9a657c44380
more reliable "sledgehammer\_tac" reconstruction, by avoiding "insert_tac"
blanchet
parents:
44461
diff
changeset

682 
Mirabelle.can_apply timeout (do_reconstructor named_thms) st 
32521  683 

684 
fun with_time (false, t) = "failed (" ^ string_of_int t ^ ")" 

40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

685 
 with_time (true, t) = (change_data id (inc_reconstructor_success m); 
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

686 
if trivial then () 
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

687 
else change_data id (inc_reconstructor_nontriv_success m); 
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

688 
change_data id (inc_reconstructor_lemmas m (length named_thms)); 
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

689 
change_data id (inc_reconstructor_time m t); 
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

690 
change_data id (inc_reconstructor_posns m (pos, trivial)); 
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

691 
if name = "proof" then change_data id (inc_reconstructor_proofs m) 
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

692 
else (); 
32521  693 
"succeeded (" ^ string_of_int t ^ ")") 
44462
d9a657c44380
more reliable "sledgehammer\_tac" reconstruction, by avoiding "insert_tac"
blanchet
parents:
44461
diff
changeset

694 
fun timed_reconstructor named_thms = 
d9a657c44380
more reliable "sledgehammer\_tac" reconstruction, by avoiding "insert_tac"
blanchet
parents:
44461
diff
changeset

695 
(with_time (Mirabelle.cpu_time apply_reconstructor named_thms), true) 
40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

696 
handle TimeLimit.TimeOut => (change_data id (inc_reconstructor_timeout m); 
34052  697 
("timeout", false)) 
698 
 ERROR msg => ("error: " ^ msg, false) 

32521  699 

32525  700 
val _ = log separator 
40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

701 
val _ = change_data id (inc_reconstructor_calls m) 
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

702 
val _ = if trivial then () 
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

703 
else change_data id (inc_reconstructor_nontriv_calls m) 
32521  704 
in 
44462
d9a657c44380
more reliable "sledgehammer\_tac" reconstruction, by avoiding "insert_tac"
blanchet
parents:
44461
diff
changeset

705 
named_thms 
40667
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

706 
> timed_reconstructor 
b8579f24ce67
make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT
blanchet
parents:
40627
diff
changeset

707 
>> log o prefix (reconstructor_tag reconstructor id) 
34052  708 
> snd 
32521  709 
end 
32385
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff
changeset

710 

41276
285aea0c153c
two layers of timeouts seem to be less reliable than a single layer
blanchet
parents:
41275
diff
changeset

711 
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

712 

44431
3e0ce0ae1022
added "max_calls" option to get a fixed number of Sledgehammer calls per theory
blanchet
parents:
44430
diff
changeset

713 
(* crude hack *) 
3e0ce0ae1022
added "max_calls" option to get a fixed number of Sledgehammer calls per theory
blanchet
parents:
44430
diff
changeset

714 
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

715 

34035
08d34921b7dd
also consider the fullytyped version of metis for Mirabelle measurements
boehmes
parents:
33316
diff
changeset

716 
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

717 
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

718 
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

719 
then () else 
768d17f54125
use regular Proof.goal (which is what methods usually see) and prevent sledgehammer from crashing;
wenzelm
parents:
34052
diff
changeset

720 
let 
44431
3e0ce0ae1022
added "max_calls" option to get a fixed number of Sledgehammer calls per theory
blanchet
parents:
44430
diff
changeset

721 
val max_calls = 
47481
b5873d4ff1e2
gathered mirabelle_sledgehammer's hardcoded defaults
sultana
parents:
47480
diff
changeset

722 
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

723 
> Int.fromString > the 
3e0ce0ae1022
added "max_calls" option to get a fixed number of Sledgehammer calls per theory
blanchet
parents:
44430
diff
changeset

724 
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

725 
in 
44431
3e0ce0ae1022
added "max_calls" option to get a fixed number of Sledgehammer calls per theory
blanchet
parents:
44430
diff
changeset

726 
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

727 
else 
44448
04bd6a9307c6
don't perform a triviality check if the goal is skipped anyway
blanchet
parents:
44447
diff
changeset

728 
let 
04bd6a9307c6
don't perform a triviality check if the goal is skipped anyway
blanchet
parents:
44447
diff
changeset

729 
val reconstructor = Unsynchronized.ref "" 
04bd6a9307c6
don't perform a triviality check if the goal is skipped anyway
blanchet
parents:
44447
diff
changeset

730 
val named_thms = 
46340  731 
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

732 
val minimize = AList.defined (op =) args minimizeK 
04bd6a9307c6
don't perform a triviality check if the goal is skipped anyway
blanchet
parents:
44447
diff
changeset

733 
val metis_ft = AList.defined (op =) args metis_ftK 
04bd6a9307c6
don't perform a triviality check if the goal is skipped anyway
blanchet
parents:
44447
diff
changeset

734 
val trivial = 
47481
b5873d4ff1e2
gathered mirabelle_sledgehammer's hardcoded defaults
sultana
parents:
47480
diff
changeset

735 
if AList.lookup (op =) args check_trivialK > the_default trivial_default 
47201  736 
> Bool.fromString > the then 
737 
Try0.try0 (SOME try_timeout) ([], [], [], []) pre 

738 
handle TimeLimit.TimeOut => false 

739 
else false 

44448
04bd6a9307c6
don't perform a triviality check if the goal is skipped anyway
blanchet
parents:
44447
diff
changeset

740 
fun apply_reconstructor m1 m2 = 
04bd6a9307c6
don't perform a triviality check if the goal is skipped anyway
blanchet
parents:
44447
diff
changeset

741 
if metis_ft 
04bd6a9307c6
don't perform a triviality check if the goal is skipped anyway
blanchet
parents:
44447
diff
changeset

742 
then 
04bd6a9307c6
don't perform a triviality check if the goal is skipped anyway
blanchet
parents:
44447
diff
changeset

743 
if not (Mirabelle.catch_result (reconstructor_tag reconstructor) false 
04bd6a9307c6
don't perform a triviality check if the goal is skipped anyway
blanchet
parents:
44447
diff
changeset

744 
(run_reconstructor trivial false m1 name reconstructor 
04bd6a9307c6
don't perform a triviality check if the goal is skipped anyway
blanchet
parents:
44447
diff
changeset

745 
(these (!named_thms))) id st) 
04bd6a9307c6
don't perform a triviality check if the goal is skipped anyway
blanchet
parents:
44447
diff
changeset

746 
then 
04bd6a9307c6
don't perform a triviality check if the goal is skipped anyway
blanchet
parents:
44447
diff
changeset

747 
(Mirabelle.catch_result (reconstructor_tag reconstructor) false 
04bd6a9307c6
don't perform a triviality check if the goal is skipped anyway
blanchet
parents:
44447
diff
changeset

748 
(run_reconstructor trivial true m2 name reconstructor 
04bd6a9307c6
don't perform a triviality check if the goal is skipped anyway
blanchet
parents:
44447
diff
changeset

749 
(these (!named_thms))) id st; ()) 
04bd6a9307c6
don't perform a triviality check if the goal is skipped anyway
blanchet
parents:
44447
diff
changeset

750 
else () 
04bd6a9307c6
don't perform a triviality check if the goal is skipped anyway
blanchet
parents:
44447
diff
changeset

751 
else 
04bd6a9307c6
don't perform a triviality check if the goal is skipped anyway
blanchet
parents:
44447
diff
changeset

752 
(Mirabelle.catch_result (reconstructor_tag reconstructor) false 
04bd6a9307c6
don't perform a triviality check if the goal is skipped anyway
blanchet
parents:
44447
diff
changeset

753 
(run_reconstructor trivial false m1 name reconstructor 
04bd6a9307c6
don't perform a triviality check if the goal is skipped anyway
blanchet
parents:
44447
diff
changeset

754 
(these (!named_thms))) id st; ()) 
04bd6a9307c6
don't perform a triviality check if the goal is skipped anyway
blanchet
parents:
44447
diff
changeset

755 
in 
04bd6a9307c6
don't perform a triviality check if the goal is skipped anyway
blanchet
parents:
44447
diff
changeset

756 
change_data id (set_mini minimize); 
04bd6a9307c6
don't perform a triviality check if the goal is skipped anyway
blanchet
parents:
44447
diff
changeset

757 
Mirabelle.catch sh_tag (run_sledgehammer trivial args reconstructor 
04bd6a9307c6
don't perform a triviality check if the goal is skipped anyway
blanchet
parents:
44447
diff
changeset

758 
named_thms) id st; 
04bd6a9307c6
don't perform a triviality check if the goal is skipped anyway
blanchet
parents:
44447
diff
changeset

759 
if is_some (!named_thms) 
44431
3e0ce0ae1022
added "max_calls" option to get a fixed number of Sledgehammer calls per theory
blanchet
parents:
44430
diff
changeset

760 
then 
44448
04bd6a9307c6
don't perform a triviality check if the goal is skipped anyway
blanchet
parents:
44447
diff
changeset

761 
(apply_reconstructor Unminimized UnminimizedFT; 
04bd6a9307c6
don't perform a triviality check if the goal is skipped anyway
blanchet
parents:
44447
diff
changeset

762 
if minimize andalso not (null (these (!named_thms))) 
04bd6a9307c6
don't perform a triviality check if the goal is skipped anyway
blanchet
parents:
44447
diff
changeset

763 
then 
04bd6a9307c6
don't perform a triviality check if the goal is skipped anyway
blanchet
parents:
44447
diff
changeset

764 
(Mirabelle.catch minimize_tag 
04bd6a9307c6
don't perform a triviality check if the goal is skipped anyway
blanchet
parents:
44447
diff
changeset

765 
(run_minimize args reconstructor named_thms) id st; 
04bd6a9307c6
don't perform a triviality check if the goal is skipped anyway
blanchet
parents:
44447
diff
changeset

766 
apply_reconstructor Minimized MinimizedFT) 
04bd6a9307c6
don't perform a triviality check if the goal is skipped anyway
blanchet
parents:
44447
diff
changeset

767 
else ()) 
04bd6a9307c6
don't perform a triviality check if the goal is skipped anyway
blanchet
parents:
44447
diff
changeset

768 
else () 
04bd6a9307c6
don't perform a triviality check if the goal is skipped anyway
blanchet
parents:
44447
diff
changeset

769 
end 
35592
768d17f54125
use regular Proof.goal (which is what methods usually see) and prevent sledgehammer from crashing;
wenzelm
parents:
34052
diff
changeset

770 
end 
32818  771 
end 
32385
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff
changeset

772 

32511  773 
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

774 
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

775 

594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff
changeset

776 
end 