author  blanchet 
Mon, 06 Jun 2011 20:36:34 +0200  
changeset 43164  b4edfe260d54 
parent 43085  0a2f5b86bdd7 
child 43165  8cf188ff76a3 
permissions  rwrr 
41087
d7b5fd465198
split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems
blanchet
parents:
41066
diff
changeset

1 
(* Title: HOL/Tools/Sledgehammer/sledgehammer_run.ML 
28477
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset

2 
Author: Fabian Immler, TU Muenchen 
32996
d2e48879e65a
removed disjunctive group cancellation  provers run independently;
wenzelm
parents:
32995
diff
changeset

3 
Author: Makarius 
35969  4 
Author: Jasmin Blanchette, TU Muenchen 
28477
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset

5 

38021
e024504943d1
rename "ATP_Manager" ML module to "Sledgehammer";
blanchet
parents:
38020
diff
changeset

6 
Sledgehammer's heart. 
28477
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset

7 
*) 
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset

8 

41087
d7b5fd465198
split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems
blanchet
parents:
41066
diff
changeset

9 
signature SLEDGEHAMMER_RUN = 
28477
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset

10 
sig 
43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

11 
type minimize_command = ATP_Reconstruct.minimize_command 
38988  12 
type relevance_override = Sledgehammer_Filter.relevance_override 
43021  13 
type mode = Sledgehammer_Provers.mode 
41087
d7b5fd465198
split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems
blanchet
parents:
41066
diff
changeset

14 
type params = Sledgehammer_Provers.params 
41263
4cac389c005f
renamed function to run prover with minimizer and changed signature to clarify its semantics and make it a drop in replacement for "get_prover"
blanchet
parents:
41262
diff
changeset

15 
type prover = Sledgehammer_Provers.prover 
40061
71cc5aac8b76
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents:
40060
diff
changeset

16 

43020
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43006
diff
changeset

17 
val someN : string 
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43006
diff
changeset

18 
val noneN : string 
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43006
diff
changeset

19 
val timeoutN : string 
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43006
diff
changeset

20 
val unknownN : string 
42646
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42642
diff
changeset

21 
val auto_minimize_min_facts : int Config.T 
43058
5f8bac7a2945
minimize automatically even if Metis failed, if the external prover was really fast
blanchet
parents:
43052
diff
changeset

22 
val auto_minimize_max_seconds : real Config.T 
43021  23 
val get_minimizing_prover : Proof.context > mode > string > prover 
38044  24 
val run_sledgehammer : 
43021  25 
params > mode > int > relevance_override > (string > minimize_command) 
43020
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43006
diff
changeset

26 
> Proof.state > bool * (string * Proof.state) 
28477
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset

27 
end; 
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset

28 

41087
d7b5fd465198
split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems
blanchet
parents:
41066
diff
changeset

29 
structure Sledgehammer_Run : SLEDGEHAMMER_RUN = 
28477
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset

30 
struct 
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset

31 

43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

32 
open ATP_Util 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

33 
open ATP_Translate 
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset

34 
open ATP_Reconstruct 
38023  35 
open Sledgehammer_Util 
38988  36 
open Sledgehammer_Filter 
41087
d7b5fd465198
split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems
blanchet
parents:
41066
diff
changeset

37 
open Sledgehammer_Provers 
41091
0afdf5cde874
implicitly call the minimizer for SMT solvers that don't return an unsat core
blanchet
parents:
41090
diff
changeset

38 
open Sledgehammer_Minimize 
40072
27f2a45b0aab
more robust handling of "remote_" vs. non"remote_" provers
blanchet
parents:
40071
diff
changeset

39 

43020
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43006
diff
changeset

40 
val someN = "some" 
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43006
diff
changeset

41 
val noneN = "none" 
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43006
diff
changeset

42 
val timeoutN = "timeout" 
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43006
diff
changeset

43 
val unknownN = "unknown" 
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43006
diff
changeset

44 

abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43006
diff
changeset

45 
val ordered_outcome_codes = [someN, unknownN, timeoutN, noneN] 
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43006
diff
changeset

46 

abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43006
diff
changeset

47 
fun max_outcome_code codes = 
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43006
diff
changeset

48 
NONE 
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43006
diff
changeset

49 
> fold (fn candidate => 
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43006
diff
changeset

50 
fn accum as SOME _ => accum 
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43006
diff
changeset

51 
 NONE => if member (op =) codes candidate then SOME candidate 
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43006
diff
changeset

52 
else NONE) 
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43006
diff
changeset

53 
ordered_outcome_codes 
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43006
diff
changeset

54 
> the_default unknownN 
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43006
diff
changeset

55 

41208
1b28c43a7074
make "debug" imply "blocking", since in blocking mode the exceptions flow through and are more instructive
blanchet
parents:
41180
diff
changeset

56 
fun prover_description ctxt ({verbose, blocking, ...} : params) name num_facts i 
41089  57 
n goal = 
43005
c96f06bffd90
merge timeout messages from several ATPs into one message to avoid clutter
blanchet
parents:
43004
diff
changeset

58 
(name, 
c96f06bffd90
merge timeout messages from several ATPs into one message to avoid clutter
blanchet
parents:
43004
diff
changeset

59 
(if verbose then 
c96f06bffd90
merge timeout messages from several ATPs into one message to avoid clutter
blanchet
parents:
43004
diff
changeset

60 
" with " ^ string_of_int num_facts ^ " fact" ^ plural_s num_facts 
c96f06bffd90
merge timeout messages from several ATPs into one message to avoid clutter
blanchet
parents:
43004
diff
changeset

61 
else 
c96f06bffd90
merge timeout messages from several ATPs into one message to avoid clutter
blanchet
parents:
43004
diff
changeset

62 
"") ^ 
c96f06bffd90
merge timeout messages from several ATPs into one message to avoid clutter
blanchet
parents:
43004
diff
changeset

63 
" on " ^ (if n = 1 then "goal" else "subgoal " ^ string_of_int i) ^ 
c96f06bffd90
merge timeout messages from several ATPs into one message to avoid clutter
blanchet
parents:
43004
diff
changeset

64 
(if blocking then 
c96f06bffd90
merge timeout messages from several ATPs into one message to avoid clutter
blanchet
parents:
43004
diff
changeset

65 
"." 
c96f06bffd90
merge timeout messages from several ATPs into one message to avoid clutter
blanchet
parents:
43004
diff
changeset

66 
else 
43037  67 
"\n" ^ Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i)))) 
41089  68 

42646
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42642
diff
changeset

69 
val auto_minimize_min_facts = 
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42642
diff
changeset

70 
Attrib.setup_config_int @{binding sledgehammer_auto_minimize_min_facts} 
42968
74415622d293
more work on parsing LEOII proofs and extracting uses of extensionality
blanchet
parents:
42966
diff
changeset

71 
(fn generic => Config.get_generic generic binary_min_facts) 
43052
8d6a4978cc65
automatically minimize with Metis when this can be done within a few seconds
blanchet
parents:
43051
diff
changeset

72 
val auto_minimize_max_seconds = 
8d6a4978cc65
automatically minimize with Metis when this can be done within a few seconds
blanchet
parents:
43051
diff
changeset

73 
Attrib.setup_config_real @{binding sledgehammer_auto_minimize_max_seconds} 
8d6a4978cc65
automatically minimize with Metis when this can be done within a few seconds
blanchet
parents:
43051
diff
changeset

74 
(K 5.0) 
8d6a4978cc65
automatically minimize with Metis when this can be done within a few seconds
blanchet
parents:
43051
diff
changeset

75 

43164  76 
fun minimize ctxt mode name (params as {debug, verbose, ...}) 
77 
({state, subgoal, subgoal_count, facts, ...} : prover_problem) 

78 
(result as {outcome, used_facts, run_time_in_msecs, preplay, 

79 
message} : prover_result) = 

80 
if is_some outcome then 

81 
result 

82 
else 

83 
let 

84 
val num_facts = length used_facts 

85 
fun can_minimize_fast_enough msecs = 

86 
0.001 * Real.fromInt ((num_facts + 2) * msecs) 

87 
<= Config.get ctxt auto_minimize_max_seconds 

88 
val ((minimize, minimize_name), preplay) = 

89 
if mode = Normal then 

90 
if num_facts >= Config.get ctxt auto_minimize_min_facts then 

91 
((true, name), preplay) 

92 
else 

93 
let val preplay = preplay () in 

94 
(case preplay of 

95 
Played (reconstructor, timeout) => 

96 
(can_minimize_fast_enough (Time.toMilliseconds timeout), 

97 
reconstructor_name reconstructor) 

98 
 _ => 

99 
case run_time_in_msecs of 

100 
SOME msecs => (can_minimize_fast_enough msecs, name) 

101 
 NONE => (false, name), 

102 
K preplay) 

103 
end 

104 
else 

105 
((false, name), preplay) 

106 
val (used_facts, (preplay, message)) = 

107 
if minimize then 

108 
minimize_facts minimize_name params (not verbose) subgoal 

109 
subgoal_count state 

110 
(filter_used_facts used_facts 

111 
(map (apsnd single o untranslated_fact) facts)) 

112 
>> Option.map (map fst) 

113 
else 

114 
(SOME used_facts, (preplay, message)) 

115 
in 

116 
case used_facts of 

117 
SOME used_facts => 

118 
(if debug andalso not (null used_facts) then 

119 
facts ~~ (0 upto length facts  1) 

120 
> map (fn (fact, j) => fact > untranslated_fact > apsnd (K j)) 

121 
> filter_used_facts used_facts 

122 
> map (fn ((name, _), j) => name ^ "@" ^ string_of_int j) 

123 
> commas 

124 
> enclose ("Fact" ^ plural_s (length facts) ^ " in " ^ quote name ^ 

125 
" proof (of " ^ string_of_int (length facts) ^ "): ") "." 

126 
> Output.urgent_message 

41263
4cac389c005f
renamed function to run prover with minimizer and changed signature to clarify its semantics and make it a drop in replacement for "get_prover"
blanchet
parents:
41262
diff
changeset

127 
else 
43164  128 
(); 
129 
{outcome = NONE, used_facts = used_facts, 

130 
run_time_in_msecs = run_time_in_msecs, preplay = preplay, 

131 
message = message}) 

132 
 NONE => result 

133 
end 

134 

135 
fun get_minimizing_prover ctxt mode name params minimize_command problem = 

136 
get_prover ctxt mode name params minimize_command problem 

137 
> minimize ctxt mode name params problem 

41262
095ecb0c687f
factored out running a prover with (optionally) an implicit minimizer phrase
blanchet
parents:
41260
diff
changeset

138 

43059  139 
fun launch_prover (params as {debug, verbose, blocking, max_relevant, slicing, 
140 
timeout, expect, ...}) 

43021  141 
mode minimize_command only 
41741  142 
{state, goal, subgoal, subgoal_count, facts, smt_filter} name = 
41089  143 
let 
144 
val ctxt = Proof.context_of state 

42850
c8709be8a40f
distinguish between a soft timeout (30 s by defalt) and a hard timeout (60 s), to let minimizationbased provers (such as CVC3, Yices, and occasionally the other provers) do their job
blanchet
parents:
42646
diff
changeset

145 
val hard_timeout = Time.+ (timeout, timeout) 
41089  146 
val birth_time = Time.now () 
42850
c8709be8a40f
distinguish between a soft timeout (30 s by defalt) and a hard timeout (60 s), to let minimizationbased provers (such as CVC3, Yices, and occasionally the other provers) do their job
blanchet
parents:
42646
diff
changeset

147 
val death_time = Time.+ (birth_time, hard_timeout) 
41089  148 
val max_relevant = 
42443
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42361
diff
changeset

149 
max_relevant 
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42361
diff
changeset

150 
> the_default (default_max_relevant_for_prover ctxt slicing name) 
41089  151 
val num_facts = length facts > not only ? Integer.min max_relevant 
43006  152 
fun desc () = 
41089  153 
prover_description ctxt params name num_facts subgoal subgoal_count goal 
154 
val problem = 

155 
{state = state, goal = goal, subgoal = subgoal, 

42638
a7a30721767a
have each ATP filter out dangerous facts for themselves, based on their type system
blanchet
parents:
42613
diff
changeset

156 
subgoal_count = subgoal_count, facts = facts > take num_facts, 
41741  157 
smt_filter = smt_filter} 
41255
a80024d7b71b
added debugging option to find out how good the relevance filter was at identifying relevant facts
blanchet
parents:
41245
diff
changeset

158 
fun really_go () = 
41263
4cac389c005f
renamed function to run prover with minimizer and changed signature to clarify its semantics and make it a drop in replacement for "get_prover"
blanchet
parents:
41262
diff
changeset

159 
problem 
43051  160 
> get_minimizing_prover ctxt mode name params minimize_command 
43052
8d6a4978cc65
automatically minimize with Metis when this can be done within a few seconds
blanchet
parents:
43051
diff
changeset

161 
> (fn {outcome, preplay, message, ...} => 
43005
c96f06bffd90
merge timeout messages from several ATPs into one message to avoid clutter
blanchet
parents:
43004
diff
changeset

162 
(if outcome = SOME ATP_Proof.TimedOut then timeoutN 
c96f06bffd90
merge timeout messages from several ATPs into one message to avoid clutter
blanchet
parents:
43004
diff
changeset

163 
else if is_some outcome then noneN 
43052
8d6a4978cc65
automatically minimize with Metis when this can be done within a few seconds
blanchet
parents:
43051
diff
changeset

164 
else someN, message o preplay)) 
41089  165 
fun go () = 
166 
let 

167 
val (outcome_code, message) = 

168 
if debug then 

169 
really_go () 

170 
else 

171 
(really_go () 

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

172 
handle ERROR msg => (unknownN, fn () => "Error: " ^ msg ^ "\n") 
41089  173 
 exn => 
174 
if Exn.is_interrupt exn then 

175 
reraise exn 

176 
else 

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

177 
(unknownN, fn () => "Internal error:\n" ^ 
8d6a4978cc65
automatically minimize with Metis when this can be done within a few seconds
blanchet
parents:
43051
diff
changeset

178 
ML_Compiler.exn_message exn ^ "\n")) 
41089  179 
val _ = 
41142
43e2b051339c
weaken the "expect" flag so that it doesn't trigger errors if a prover is not installed
blanchet
parents:
41138
diff
changeset

180 
(* The "expect" argument is deliberately ignored if the prover is 
43e2b051339c
weaken the "expect" flag so that it doesn't trigger errors if a prover is not installed
blanchet
parents:
41138
diff
changeset

181 
missing so that the "Metis_Examples" can be processed on any 
43e2b051339c
weaken the "expect" flag so that it doesn't trigger errors if a prover is not installed
blanchet
parents:
41138
diff
changeset

182 
machine. *) 
43e2b051339c
weaken the "expect" flag so that it doesn't trigger errors if a prover is not installed
blanchet
parents:
41138
diff
changeset

183 
if expect = "" orelse outcome_code = expect orelse 
43e2b051339c
weaken the "expect" flag so that it doesn't trigger errors if a prover is not installed
blanchet
parents:
41138
diff
changeset

184 
not (is_prover_installed ctxt name) then 
41089  185 
() 
186 
else if blocking then 

187 
error ("Unexpected outcome: " ^ quote outcome_code ^ ".") 

188 
else 

189 
warning ("Unexpected outcome: " ^ quote outcome_code ^ "."); 

43005
c96f06bffd90
merge timeout messages from several ATPs into one message to avoid clutter
blanchet
parents:
43004
diff
changeset

190 
in (outcome_code, message) end 
41089  191 
in 
43021  192 
if mode = Auto_Try then 
43006  193 
let val (outcome_code, message) = TimeLimit.timeLimit timeout go () in 
194 
(outcome_code, 

195 
state 

196 
> outcome_code = someN 

197 
? Proof.goal_message (fn () => 

198 
[Pretty.str "", 

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

199 
Pretty.mark Markup.hilite (Pretty.str (message ()))] 
43006  200 
> Pretty.chunks)) 
41089  201 
end 
202 
else if blocking then 

43006  203 
let 
204 
val (outcome_code, message) = TimeLimit.timeLimit hard_timeout go () 

205 
in 

43058
5f8bac7a2945
minimize automatically even if Metis failed, if the external prover was really fast
blanchet
parents:
43052
diff
changeset

206 
(if outcome_code = someN orelse mode = Normal then 
5f8bac7a2945
minimize automatically even if Metis failed, if the external prover was really fast
blanchet
parents:
43052
diff
changeset

207 
quote name ^ ": " ^ message () 
5f8bac7a2945
minimize automatically even if Metis failed, if the external prover was really fast
blanchet
parents:
43052
diff
changeset

208 
else 
5f8bac7a2945
minimize automatically even if Metis failed, if the external prover was really fast
blanchet
parents:
43052
diff
changeset

209 
"") 
43005
c96f06bffd90
merge timeout messages from several ATPs into one message to avoid clutter
blanchet
parents:
43004
diff
changeset

210 
> Async_Manager.break_into_chunks 
c96f06bffd90
merge timeout messages from several ATPs into one message to avoid clutter
blanchet
parents:
43004
diff
changeset

211 
> List.app Output.urgent_message; 
43006  212 
(outcome_code, state) 
41089  213 
end 
214 
else 

43006  215 
(Async_Manager.launch das_tool birth_time death_time (desc ()) 
43052
8d6a4978cc65
automatically minimize with Metis when this can be done within a few seconds
blanchet
parents:
43051
diff
changeset

216 
((fn (outcome_code, message) => 
43059  217 
(verbose orelse outcome_code = someN, 
218 
message ())) o go); 

43006  219 
(unknownN, state)) 
41089  220 
end 
221 

41242
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset

222 
fun class_of_smt_solver ctxt name = 
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset

223 
ctxt > select_smt_solver name 
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset

224 
> SMT_Config.solver_class_of > SMT_Utils.string_of_class 
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset

225 

43043
1406f6fc5dc3
normalize indices in chained facts to make sure that backtick facts (which often result in different names) are recognized + changed definition of urgent messages
blanchet
parents:
43037
diff
changeset

226 
(* Makes backtraces more transparent and might well be more efficient as 
1406f6fc5dc3
normalize indices in chained facts to make sure that backtick facts (which often result in different names) are recognized + changed definition of urgent messages
blanchet
parents:
43037
diff
changeset

227 
well. *) 
41242
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset

228 
fun smart_par_list_map _ [] = [] 
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset

229 
 smart_par_list_map f [x] = [f x] 
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset

230 
 smart_par_list_map f xs = Par_List.map f xs 
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset

231 

41256
0e7d45cc005f
put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents:
41255
diff
changeset

232 
fun dest_SMT_Weighted_Fact (SMT_Weighted_Fact p) = p 
0e7d45cc005f
put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents:
41255
diff
changeset

233 
 dest_SMT_Weighted_Fact _ = raise Fail "dest_SMT_Weighted_Fact" 
0e7d45cc005f
put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents:
41255
diff
changeset

234 

43021  235 
val auto_try_max_relevant_divisor = 2 (* FUDGE *) 
40060
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset

236 

42946  237 
fun run_sledgehammer (params as {debug, verbose, blocking, provers, 
238 
relevance_thresholds, max_relevant, slicing, 

239 
timeout, ...}) 

43021  240 
mode i (relevance_override as {only, ...}) minimize_command state = 
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset

241 
if null provers then 
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset

242 
error "No prover is set." 
39318  243 
else case subgoal_count state of 
43020
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43006
diff
changeset

244 
0 => (Output.urgent_message "No subgoal!"; (false, (noneN, state))) 
39318  245 
 n => 
246 
let 

39364  247 
val _ = Proof.assert_backward state 
43021  248 
val print = if mode = Normal then Output.urgent_message else K () 
41242
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset

249 
val state = 
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset

250 
state > Proof.map_context (Config.put SMT_Config.verbose debug) 
40200  251 
val ctxt = Proof.context_of state 
252 
val {facts = chained_ths, goal, ...} = Proof.goal state 

43043
1406f6fc5dc3
normalize indices in chained facts to make sure that backtick facts (which often result in different names) are recognized + changed definition of urgent messages
blanchet
parents:
43037
diff
changeset

253 
val chained_ths = chained_ths > normalize_chained_theorems 
43004
20e9caff1f86
fix soundness bug in Sledgehammer: distinguish params in goals from fixed variables in context
blanchet
parents:
42968
diff
changeset

254 
val (_, hyp_ts, concl_t) = strip_subgoal ctxt goal i 
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset

255 
val _ = () > not blocking ? kill_provers 
41727
ab3f6d76fb23
available_provers ~> supported_provers (for clarity)
blanchet
parents:
41432
diff
changeset

256 
val _ = case find_first (not o is_prover_supported ctxt) provers of 
40941
a3e6f8634a11
replace "smt" prover with specific SMT solvers, e.g. "z3"  whatever the SMT module gives us
blanchet
parents:
40723
diff
changeset

257 
SOME name => error ("No such prover: " ^ name ^ ".") 
a3e6f8634a11
replace "smt" prover with specific SMT solvers, e.g. "z3"  whatever the SMT module gives us
blanchet
parents:
40723
diff
changeset

258 
 NONE => () 
41773  259 
val _ = print "Sledgehammering..." 
42944
9e620869a576
improved Waldmeister support  even run it by default on unit equational goals
blanchet
parents:
42850
diff
changeset

260 
val (smts, (ueq_atps, full_atps)) = 
9e620869a576
improved Waldmeister support  even run it by default on unit equational goals
blanchet
parents:
42850
diff
changeset

261 
provers > List.partition (is_smt_prover ctxt) 
9e620869a576
improved Waldmeister support  even run it by default on unit equational goals
blanchet
parents:
42850
diff
changeset

262 
> List.partition (is_unit_equational_atp ctxt) 
41741  263 
fun launch_provers state get_facts translate maybe_smt_filter provers = 
41256
0e7d45cc005f
put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents:
41255
diff
changeset

264 
let 
0e7d45cc005f
put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents:
41255
diff
changeset

265 
val facts = get_facts () 
0e7d45cc005f
put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents:
41255
diff
changeset

266 
val num_facts = length facts 
0e7d45cc005f
put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents:
41255
diff
changeset

267 
val facts = facts ~~ (0 upto num_facts  1) 
0e7d45cc005f
put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents:
41255
diff
changeset

268 
> map (translate num_facts) 
0e7d45cc005f
put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents:
41255
diff
changeset

269 
val problem = 
0e7d45cc005f
put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents:
41255
diff
changeset

270 
{state = state, goal = goal, subgoal = i, subgoal_count = n, 
0e7d45cc005f
put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents:
41255
diff
changeset

271 
facts = facts, 
41741  272 
smt_filter = maybe_smt_filter 
41256
0e7d45cc005f
put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents:
41255
diff
changeset

273 
(fn () => map_filter (try dest_SMT_Weighted_Fact) facts) i} 
43021  274 
val launch = launch_prover params mode minimize_command only 
41256
0e7d45cc005f
put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents:
41255
diff
changeset

275 
in 
43021  276 
if mode = Auto_Try orelse mode = Try then 
43020
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43006
diff
changeset

277 
(unknownN, state) 
43021  278 
> fold (fn prover => fn accum as (outcome_code, _) => 
43020
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43006
diff
changeset

279 
if outcome_code = someN then accum 
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43006
diff
changeset

280 
else launch problem prover) 
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43006
diff
changeset

281 
provers 
41256
0e7d45cc005f
put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents:
41255
diff
changeset

282 
else 
0e7d45cc005f
put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents:
41255
diff
changeset

283 
provers 
43020
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43006
diff
changeset

284 
> (if blocking then smart_par_list_map else map) 
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43006
diff
changeset

285 
(launch problem #> fst) 
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43006
diff
changeset

286 
> max_outcome_code > rpair state 
41256
0e7d45cc005f
put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents:
41255
diff
changeset

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

288 
fun get_facts label is_appropriate_prop relevance_fudge provers = 
41242
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset

289 
let 
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset

290 
val max_max_relevant = 
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset

291 
case max_relevant of 
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset

292 
SOME n => n 
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset

293 
 NONE => 
42443
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42361
diff
changeset

294 
0 > fold (Integer.max 
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42361
diff
changeset

295 
o default_max_relevant_for_prover ctxt slicing) 
41242
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset

296 
provers 
43021  297 
> mode = Auto_Try 
298 
? (fn n => n div auto_try_max_relevant_divisor) 

41242
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset

299 
val is_built_in_const = 
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset

300 
is_built_in_const_for_prover ctxt (hd provers) 
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset

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

302 
relevant_facts ctxt relevance_thresholds max_max_relevant 
96f62b77748f
tuning  the "appropriate" terminology is inspired from TPTP
blanchet
parents:
42946
diff
changeset

303 
is_appropriate_prop is_built_in_const relevance_fudge 
96f62b77748f
tuning  the "appropriate" terminology is inspired from TPTP
blanchet
parents:
42946
diff
changeset

304 
relevance_override chained_ths hyp_ts concl_t 
41242
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset

305 
> tap (fn facts => 
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset

306 
if debug then 
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset

307 
label ^ plural_s (length provers) ^ ": " ^ 
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset

308 
(if null facts then 
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset

309 
"Found no relevant facts." 
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset

310 
else 
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset

311 
"Including (up to) " ^ string_of_int (length facts) ^ 
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset

312 
" relevant fact" ^ plural_s (length facts) ^ ":\n" ^ 
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset

313 
(facts > map (fst o fst) > space_implode " ") ^ ".") 
41773  314 

41242
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset

315 
else 
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset

316 
()) 
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset

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

318 
fun launch_atps label is_appropriate_prop atps accum = 
42946  319 
if null atps then 
41256
0e7d45cc005f
put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents:
41255
diff
changeset

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

321 
else if not (is_appropriate_prop concl_t) then 
42946  322 
(if verbose orelse length atps = length provers then 
323 
"Goal outside the scope of " ^ 

324 
space_implode " " (serial_commas "and" (map quote atps)) ^ "." 

325 
> Output.urgent_message 

326 
else 

327 
(); 

328 
accum) 

41256
0e7d45cc005f
put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents:
41255
diff
changeset

329 
else 
42944
9e620869a576
improved Waldmeister support  even run it by default on unit equational goals
blanchet
parents:
42850
diff
changeset

330 
launch_provers state 
42952
96f62b77748f
tuning  the "appropriate" terminology is inspired from TPTP
blanchet
parents:
42946
diff
changeset

331 
(get_facts label is_appropriate_prop atp_relevance_fudge o K atps) 
42944
9e620869a576
improved Waldmeister support  even run it by default on unit equational goals
blanchet
parents:
42850
diff
changeset

332 
(K (Untranslated_Fact o fst)) (K (K NONE)) atps 
41746
e590971528b2
run all provers in blocking mode, even if a proof was already found  this behavior is less confusing to the user
blanchet
parents:
41743
diff
changeset

333 
fun launch_smts accum = 
e590971528b2
run all provers in blocking mode, even if a proof was already found  this behavior is less confusing to the user
blanchet
parents:
41743
diff
changeset

334 
if null smts then 
41242
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset

335 
accum 
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset

336 
else 
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset

337 
let 
42944
9e620869a576
improved Waldmeister support  even run it by default on unit equational goals
blanchet
parents:
42850
diff
changeset

338 
val facts = get_facts "SMT solver" (K true) smt_relevance_fudge smts 
42646
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42642
diff
changeset

339 
val weight = SMT_Weighted_Fact oo weight_smt_fact ctxt 
41741  340 
fun smt_filter facts = 
41788
adfd365c7ea4
added a timeout around SMT preprocessing (notably monomorphization)
blanchet
parents:
41773
diff
changeset

341 
(if debug then curry (op o) SOME 
adfd365c7ea4
added a timeout around SMT preprocessing (notably monomorphization)
blanchet
parents:
41773
diff
changeset

342 
else TimeLimit.timeLimit timeout o try) 
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41335
diff
changeset

343 
(SMT_Solver.smt_filter_preprocess state (facts ())) 
41242
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset

344 
in 
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset

345 
smts > map (`(class_of_smt_solver ctxt)) 
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset

346 
> AList.group (op =) 
43020
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43006
diff
changeset

347 
> map (snd #> launch_provers state (K facts) weight smt_filter 
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43006
diff
changeset

348 
#> fst) 
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43006
diff
changeset

349 
> max_outcome_code > rpair state 
41242
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset

350 
end 
42944
9e620869a576
improved Waldmeister support  even run it by default on unit equational goals
blanchet
parents:
42850
diff
changeset

351 
val launch_full_atps = launch_atps "ATP" (K true) full_atps 
9e620869a576
improved Waldmeister support  even run it by default on unit equational goals
blanchet
parents:
42850
diff
changeset

352 
val launch_ueq_atps = 
9e620869a576
improved Waldmeister support  even run it by default on unit equational goals
blanchet
parents:
42850
diff
changeset

353 
launch_atps "Unit equational provers" is_unit_equality ueq_atps 
41262
095ecb0c687f
factored out running a prover with (optionally) an implicit minimizer phrase
blanchet
parents:
41260
diff
changeset

354 
fun launch_atps_and_smt_solvers () = 
43043
1406f6fc5dc3
normalize indices in chained facts to make sure that backtick facts (which often result in different names) are recognized + changed definition of urgent messages
blanchet
parents:
43037
diff
changeset

355 
[launch_full_atps, launch_smts, launch_ueq_atps] 
43021  356 
> smart_par_list_map (fn f => ignore (f (unknownN, state))) 
41773  357 
handle ERROR msg => (print ("Error: " ^ msg); error msg) 
43021  358 
fun maybe f (accum as (outcome_code, _)) = 
359 
accum > (mode = Normal orelse outcome_code <> someN) ? f 

40060
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset

360 
in 
43020
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43006
diff
changeset

361 
(unknownN, state) 
42944
9e620869a576
improved Waldmeister support  even run it by default on unit equational goals
blanchet
parents:
42850
diff
changeset

362 
> (if blocking then 
43021  363 
launch_full_atps 
364 
#> mode <> Auto_Try ? (maybe launch_ueq_atps #> maybe launch_smts) 

42944
9e620869a576
improved Waldmeister support  even run it by default on unit equational goals
blanchet
parents:
42850
diff
changeset

365 
else 
9e620869a576
improved Waldmeister support  even run it by default on unit equational goals
blanchet
parents:
42850
diff
changeset

366 
(fn p => Future.fork (tap launch_atps_and_smt_solvers) > K p)) 
41773  367 
handle TimeLimit.TimeOut => 
43020
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43006
diff
changeset

368 
(print "Sledgehammer ran out of time."; (unknownN, state)) 
40060
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset

369 
end 
43020
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43006
diff
changeset

370 
> `(fn (outcome_code, _) => outcome_code = someN) 
38044  371 

28582  372 
end; 