author  blanchet 
Fri, 04 Oct 2013 11:12:28 +0200  
changeset 54308  1a87db1f3701 
parent 53815  e8aa538e959e 
child 54062  427380d5d1d7 
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 
51008  11 
type fact = Sledgehammer_Fact.fact 
48292  12 
type fact_override = Sledgehammer_Fact.fact_override 
52555  13 
type minimize_command = Sledgehammer_Reconstructor.minimize_command 
43021  14 
type mode = Sledgehammer_Provers.mode 
41087
d7b5fd465198
split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems
blanchet
parents:
41066
diff
changeset

15 
type params = Sledgehammer_Provers.params 
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 
51010  21 
val string_of_factss : (string * fact list) list > string 
38044  22 
val run_sledgehammer : 
53048
0f76e620561f
more direct sledgehammer configuration via mode = Normal_Result and output_result;
wenzelm
parents:
52997
diff
changeset

23 
params > mode > (string > unit) option > int > fact_override 
45520  24 
> ((string * string list) list > string > minimize_command) 
43020
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43006
diff
changeset

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

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

27 

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

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

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

30 

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

31 
open ATP_Util 
46320  32 
open ATP_Problem_Generate 
53800  33 
open ATP_Proof 
46320  34 
open ATP_Proof_Reconstruct 
38023  35 
open Sledgehammer_Util 
48250
1065c307fafe
further ML structure split to permit finergrained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
47904
diff
changeset

36 
open Sledgehammer_Fact 
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 
48381  39 
open Sledgehammer_MaSh 
40072
27f2a45b0aab
more robust handling of "remote_" vs. non"remote_" provers
blanchet
parents:
40071
diff
changeset

40 

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

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

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

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

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

45 

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

46 
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

47 

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

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

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

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

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

52 
 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

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

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

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

56 

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

57 
fun prover_description ctxt ({verbose, blocking, ...} : params) name num_facts i 
41089  58 
n goal = 
48319
340187063d84
use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents:
48299
diff
changeset

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

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

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

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

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

64 
" on " ^ (if n = 1 then "goal" else "subgoal " ^ string_of_int i) ^ 
45379
0147a4348ca1
try "smt" as a fallback for ATPs if "metis" fails/times out
blanchet
parents:
45370
diff
changeset

65 
(if blocking then "." 
0147a4348ca1
try "smt" as a fallback for ATPs if "metis" fails/times out
blanchet
parents:
45370
diff
changeset

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

53800  68 
fun launch_prover (params as {debug, verbose, spy, blocking, max_facts, slice, 
43059  69 
timeout, expect, ...}) 
53048
0f76e620561f
more direct sledgehammer configuration via mode = Normal_Result and output_result;
wenzelm
parents:
52997
diff
changeset

70 
mode output_result minimize_command only learn 
51010  71 
{state, goal, subgoal, subgoal_count, factss as (_, facts) :: _} name = 
41089  72 
let 
73 
val ctxt = Proof.context_of state 

53800  74 

50749
82dee320d340
increased hard timeout  minimization can take time
blanchet
parents:
50669
diff
changeset

75 
val hard_timeout = time_mult 3.0 (timeout > the_default one_day) 
53815
e8aa538e959e
encode goal digest in spying log (to detect duplicates)
blanchet
parents:
53814
diff
changeset

76 
val _ = spying spy (fn () => (state, subgoal, name, "launched")); 
41089  77 
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

78 
val death_time = Time.+ (birth_time, hard_timeout) 
53800  79 
val max_facts = max_facts > the_default (default_max_facts_of_prover ctxt slice name) 
48293  80 
val num_facts = length facts > not only ? Integer.min max_facts 
53800  81 

82 
fun desc () = prover_description ctxt params name num_facts subgoal subgoal_count goal 

83 

41089  84 
val problem = 
47904
67663c968d70
distinguish between instantiated and uninstantiated inductions  the latter are OK for firstorder provers
blanchet
parents:
47531
diff
changeset

85 
{state = state, goal = goal, subgoal = subgoal, 
67663c968d70
distinguish between instantiated and uninstantiated inductions  the latter are OK for firstorder provers
blanchet
parents:
47531
diff
changeset

86 
subgoal_count = subgoal_count, 
53800  87 
factss = factss 
51010  88 
> map (apsnd ((not (is_ho_atp ctxt name) 
89 
? filter_out (fn ((_, (_, Induction)), _) => true 

90 
 _ => false)) 

91 
#> take num_facts))} 

53800  92 

51009
e8ff34a1fa9a
thread through fact triple component from which used facts come, for accurate index output
blanchet
parents:
51008
diff
changeset

93 
fun print_used_facts used_facts used_from = 
e8ff34a1fa9a
thread through fact triple component from which used facts come, for accurate index output
blanchet
parents:
51008
diff
changeset

94 
tag_list 1 used_from 
51005
ce4290c33d73
eliminated needless speed optimization  and simplified code quite a bit
blanchet
parents:
51004
diff
changeset

95 
> map (fn (j, fact) => fact > apsnd (K j)) 
48798  96 
> filter_used_facts false used_facts 
48394
82fc8c956cdc
fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully
blanchet
parents:
48384
diff
changeset

97 
> map (fn ((name, _), j) => name ^ "@" ^ string_of_int j) 
82fc8c956cdc
fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully
blanchet
parents:
48384
diff
changeset

98 
> commas 
82fc8c956cdc
fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully
blanchet
parents:
48384
diff
changeset

99 
> enclose ("Fact" ^ plural_s (length facts) ^ " in " ^ quote name ^ 
82fc8c956cdc
fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully
blanchet
parents:
48384
diff
changeset

100 
" proof (of " ^ string_of_int (length facts) ^ "): ") "." 
82fc8c956cdc
fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully
blanchet
parents:
48384
diff
changeset

101 
> Output.urgent_message 
53800  102 

53814  103 
fun spying_str_of_res ({outcome = NONE, used_facts, ...} : prover_result) = 
53800  104 
let val num_used_facts = length used_facts in 
105 
"success: Found proof with " ^ string_of_int num_used_facts ^ " fact" ^ 

106 
plural_s num_used_facts 

107 
end 

108 
 spying_str_of_res {outcome = SOME failure, ...} = 

109 
"failure: " ^ string_of_atp_failure failure 

110 

41255
a80024d7b71b
added debugging option to find out how good the relevance filter was at identifying relevant facts
blanchet
parents:
41245
diff
changeset

111 
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

112 
problem 
51187
c344cf148e8f
avoid using "smt" for minimization  better use the prover itself, since then Sledgehammer gets to try metis again and gives the opportunity to output an Isar proof  and show Isar proof as fallback for SMT proofs
blanchet
parents:
51010
diff
changeset

113 
> get_minimizing_prover ctxt mode learn name params minimize_command 
51009
e8ff34a1fa9a
thread through fact triple component from which used facts come, for accurate index output
blanchet
parents:
51008
diff
changeset

114 
> verbose 
e8ff34a1fa9a
thread through fact triple component from which used facts come, for accurate index output
blanchet
parents:
51008
diff
changeset

115 
? tap (fn {outcome = NONE, used_facts as _ :: _, used_from, ...} => 
e8ff34a1fa9a
thread through fact triple component from which used facts come, for accurate index output
blanchet
parents:
51008
diff
changeset

116 
print_used_facts used_facts used_from 
e8ff34a1fa9a
thread through fact triple component from which used facts come, for accurate index output
blanchet
parents:
51008
diff
changeset

117 
 _ => ()) 
53800  118 
> spy 
53815
e8aa538e959e
encode goal digest in spying log (to detect duplicates)
blanchet
parents:
53814
diff
changeset

119 
? tap (fn res => spying spy (fn () => (state, subgoal, name, spying_str_of_res res))) 
43261
a4aeb26a6362
make sure that the message tail (timing + TPTP important message) is preserved upon automatic minimization
blanchet
parents:
43233
diff
changeset

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

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

122 
else if is_some outcome then noneN 
50669
84c7cf36b2e0
use "Lazy" to simplify control flow a bit and guarantee single evaluation (at most)
blanchet
parents:
50668
diff
changeset

123 
else someN, fn () => message (Lazy.force preplay) ^ message_tail)) 
53800  124 

41089  125 
fun go () = 
126 
let 

127 
val (outcome_code, message) = 

128 
if debug then 

129 
really_go () 

130 
else 

131 
(really_go () 

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

132 
handle ERROR msg => (unknownN, fn () => "Error: " ^ msg ^ "\n") 
41089  133 
 exn => 
134 
if Exn.is_interrupt exn then 

135 
reraise exn 

136 
else 

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

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

138 
ML_Compiler.exn_message exn ^ "\n")) 
41089  139 
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

140 
(* 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

141 
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

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

143 
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

144 
not (is_prover_installed ctxt name) then 
41089  145 
() 
146 
else if blocking then 

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

148 
else 

149 
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

150 
in (outcome_code, message) end 
41089  151 
in 
43021  152 
if mode = Auto_Try then 
50557  153 
let val (outcome_code, message) = time_limit timeout go () in 
43006  154 
(outcome_code, 
155 
state 

156 
> outcome_code = someN 

157 
? Proof.goal_message (fn () => 

52643
34c29356930e
more explicit Markup.information for messages produced by "auto" tools;
wenzelm
parents:
52555
diff
changeset

158 
Pretty.mark Markup.information (Pretty.str (message ())))) 
41089  159 
end 
160 
else if blocking then 

43006  161 
let 
162 
val (outcome_code, message) = TimeLimit.timeLimit hard_timeout go () 

53048
0f76e620561f
more direct sledgehammer configuration via mode = Normal_Result and output_result;
wenzelm
parents:
52997
diff
changeset

163 
val outcome = 
53052
a0db255af8c5
sledgehammer sendback always uses Markup.padding_command: sensible default for most practical applications  oldstyle inline replacement is superseded by auto mode or panel;
wenzelm
parents:
53048
diff
changeset

164 
if outcome_code = someN orelse mode = Normal then 
53048
0f76e620561f
more direct sledgehammer configuration via mode = Normal_Result and output_result;
wenzelm
parents:
52997
diff
changeset

165 
quote name ^ ": " ^ message () 
0f76e620561f
more direct sledgehammer configuration via mode = Normal_Result and output_result;
wenzelm
parents:
52997
diff
changeset

166 
else "" 
0f76e620561f
more direct sledgehammer configuration via mode = Normal_Result and output_result;
wenzelm
parents:
52997
diff
changeset

167 
val _ = 
53052
a0db255af8c5
sledgehammer sendback always uses Markup.padding_command: sensible default for most practical applications  oldstyle inline replacement is superseded by auto mode or panel;
wenzelm
parents:
53048
diff
changeset

168 
if outcome <> "" andalso is_some output_result then 
53048
0f76e620561f
more direct sledgehammer configuration via mode = Normal_Result and output_result;
wenzelm
parents:
52997
diff
changeset

169 
the output_result outcome 
52908
3461985dcbc3
dockable window for Sledgehammer, based on asynchronous/parallel query operation;
wenzelm
parents:
52643
diff
changeset

170 
else 
53048
0f76e620561f
more direct sledgehammer configuration via mode = Normal_Result and output_result;
wenzelm
parents:
52997
diff
changeset

171 
outcome 
0f76e620561f
more direct sledgehammer configuration via mode = Normal_Result and output_result;
wenzelm
parents:
52997
diff
changeset

172 
> Async_Manager.break_into_chunks 
0f76e620561f
more direct sledgehammer configuration via mode = Normal_Result and output_result;
wenzelm
parents:
52997
diff
changeset

173 
> List.app Output.urgent_message 
0f76e620561f
more direct sledgehammer configuration via mode = Normal_Result and output_result;
wenzelm
parents:
52997
diff
changeset

174 
in (outcome_code, state) end 
41089  175 
else 
52048
9003b293e775
tuned signature  emphasize thread creation here;
wenzelm
parents:
51998
diff
changeset

176 
(Async_Manager.thread SledgehammerN 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

177 
((fn (outcome_code, message) => 
43059  178 
(verbose orelse outcome_code = someN, 
179 
message ())) o go); 

43006  180 
(unknownN, state)) 
41089  181 
end 
182 

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

184 

51008  185 
fun string_of_facts facts = 
186 
"Including " ^ string_of_int (length facts) ^ 

187 
" relevant fact" ^ plural_s (length facts) ^ ":\n" ^ 

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

189 

51010  190 
fun string_of_factss factss = 
191 
if forall (null o snd) factss then 

192 
"Found no relevant facts." 

193 
else case factss of 

194 
[(_, facts)] => string_of_facts facts 

195 
 _ => 

196 
factss 

197 
> map (fn (filter, facts) => quote filter ^ ": " ^ string_of_facts facts) 

198 
> space_implode "\n\n" 

51008  199 

53800  200 
fun run_sledgehammer (params as {debug, verbose, spy, blocking, provers, max_facts, slice, ...}) 
53048
0f76e620561f
more direct sledgehammer configuration via mode = Normal_Result and output_result;
wenzelm
parents:
52997
diff
changeset

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

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

203 
error "No prover is set." 
39318  204 
else case subgoal_count state of 
52908
3461985dcbc3
dockable window for Sledgehammer, based on asynchronous/parallel query operation;
wenzelm
parents:
52643
diff
changeset

205 
0 => 
3461985dcbc3
dockable window for Sledgehammer, based on asynchronous/parallel query operation;
wenzelm
parents:
52643
diff
changeset

206 
((if blocking then error else Output.urgent_message) "No subgoal!"; (false, (noneN, state))) 
39318  207 
 n => 
208 
let 

39364  209 
val _ = Proof.assert_backward state 
53052
a0db255af8c5
sledgehammer sendback always uses Markup.padding_command: sensible default for most practical applications  oldstyle inline replacement is superseded by auto mode or panel;
wenzelm
parents:
53048
diff
changeset

210 
val print = 
a0db255af8c5
sledgehammer sendback always uses Markup.padding_command: sensible default for most practical applications  oldstyle inline replacement is superseded by auto mode or panel;
wenzelm
parents:
53048
diff
changeset

211 
if mode = Normal andalso is_none output_result 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

212 
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

213 
state > Proof.map_context (Config.put SMT_Config.verbose debug) 
40200  214 
val ctxt = Proof.context_of state 
48396  215 
val {facts = chained, goal, ...} = Proof.goal state 
52196
2281f33e8da6
redid rac7830871177 to avoid duplicate fixed variable (e.g. lemma "P (a::nat)" proof  have "!!a::int. Q a" sledgehammer [e])
blanchet
parents:
52125
diff
changeset

216 
val (_, hyp_ts, concl_t) = strip_subgoal goal i ctxt 
51007
4f694d52bf62
thread fact triple (MeSh, MePo, MaSh) to allow different filters in different slices
blanchet
parents:
51006
diff
changeset

217 
val ho_atp = exists (is_ho_atp ctxt) provers 
48299  218 
val reserved = reserved_isar_keyword_table () 
48396  219 
val css = clasimpset_rule_table_of ctxt 
48407  220 
val all_facts = 
48396  221 
nearly_all_facts ctxt ho_atp fact_override reserved css chained hyp_ts 
222 
concl_t 

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

224 
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

225 
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

226 
 NONE => () 
41773  227 
val _ = print "Sledgehammering..." 
53815
e8aa538e959e
encode goal digest in spying log (to detect duplicates)
blanchet
parents:
53814
diff
changeset

228 
val _ = 
e8aa538e959e
encode goal digest in spying log (to detect duplicates)
blanchet
parents:
53814
diff
changeset

229 
spying spy (fn () => (state, i, "***", "starting " ^ @{make_string} mode ^ " mode")) 
42944
9e620869a576
improved Waldmeister support  even run it by default on unit equational goals
blanchet
parents:
42850
diff
changeset

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

231 
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

232 
> List.partition (is_unit_equational_atp ctxt) 
53800  233 

234 
val spying_str_of_factss = 

235 
commas o map (fn (filter, facts) => filter ^ ": " ^ string_of_int (length facts)) 

236 

51010  237 
fun get_factss label is_appropriate_prop 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

238 
let 
48293  239 
val max_max_facts = 
240 
case max_facts of 

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

241 
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

242 
 NONE => 
51998
f732a674db1b
renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents:
51741
diff
changeset

243 
0 > fold (Integer.max o default_max_facts_of_prover ctxt slice) 
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

244 
provers 
48293  245 
> mode = Auto_Try ? (fn n => n div auto_try_max_facts_divisor) 
53815
e8aa538e959e
encode goal digest in spying log (to detect duplicates)
blanchet
parents:
53814
diff
changeset

246 
val _ = spying spy (fn () => (state, i, label ^ "s", 
e8aa538e959e
encode goal digest in spying log (to detect duplicates)
blanchet
parents:
53814
diff
changeset

247 
"filtering " ^ string_of_int (length all_facts) ^ " 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

248 
in 
48407  249 
all_facts 
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:
43306
diff
changeset

250 
> (case is_appropriate_prop of 
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:
43306
diff
changeset

251 
SOME is_app => filter (is_app o prop_of o snd) 
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:
43306
diff
changeset

252 
 NONE => I) 
48293  253 
> relevant_facts ctxt params (hd provers) max_max_facts fact_override 
254 
hyp_ts concl_t 

51010  255 
> tap (fn factss => 
48394
82fc8c956cdc
fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully
blanchet
parents:
48384
diff
changeset

256 
if verbose 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

257 
label ^ plural_s (length provers) ^ ": " ^ 
51010  258 
string_of_factss factss 
41773  259 

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

260 
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

261 
()) 
53800  262 
> spy ? tap (fn factss => 
53815
e8aa538e959e
encode goal digest in spying log (to detect duplicates)
blanchet
parents:
53814
diff
changeset

263 
spying spy (fn () => 
e8aa538e959e
encode goal digest in spying log (to detect duplicates)
blanchet
parents:
53814
diff
changeset

264 
(state, i, label ^ "s", "selected facts: " ^ spying_str_of_factss factss))) 
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

265 
end 
53800  266 

51006  267 
fun launch_provers state label is_appropriate_prop provers = 
268 
let 

51010  269 
val factss = get_factss label is_appropriate_prop provers 
51006  270 
val problem = 
271 
{state = state, goal = goal, subgoal = i, subgoal_count = n, 

51010  272 
factss = factss} 
51006  273 
fun learn prover = 
274 
mash_learn_proof ctxt params prover (prop_of goal) all_facts 

53549  275 
val launch = 
276 
launch_prover params mode output_result minimize_command only learn 

51006  277 
in 
53048
0f76e620561f
more direct sledgehammer configuration via mode = Normal_Result and output_result;
wenzelm
parents:
52997
diff
changeset

278 
if mode = Auto_Try then 
51006  279 
(unknownN, state) 
280 
> fold (fn prover => fn accum as (outcome_code, _) => 

281 
if outcome_code = someN then accum 

282 
else launch problem prover) 

283 
provers 

284 
else 

285 
provers 

286 
> (if blocking then Par_List.map else map) (launch problem #> fst) 

287 
> max_outcome_code > rpair state 

288 
end 

53800  289 

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

290 
fun launch_atps label is_appropriate_prop atps accum = 
42946  291 
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

292 
accum 
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:
43306
diff
changeset

293 
else if is_some is_appropriate_prop andalso 
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:
43306
diff
changeset

294 
not (the is_appropriate_prop concl_t) then 
42946  295 
(if verbose orelse length atps = length provers then 
296 
"Goal outside the scope of " ^ 

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

298 
> Output.urgent_message 

299 
else 

300 
(); 

301 
accum) 

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

302 
else 
51006  303 
launch_provers state label is_appropriate_prop atps 
53800  304 

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

305 
fun launch_smts accum = 
51006  306 
if null smts then accum else launch_provers state "SMT solver" NONE smts 
53800  307 

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:
43306
diff
changeset

308 
val launch_full_atps = launch_atps "ATP" NONE full_atps 
53800  309 

310 
val launch_ueq_atps = launch_atps "Unitequational provers" (SOME is_unit_equality) ueq_atps 

311 

54308  312 
fun launch_atps_and_smt_solvers p = 
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

313 
[launch_full_atps, launch_smts, launch_ueq_atps] 
54308  314 
> Par_List.map (fn f => fst (f p)) 
41773  315 
handle ERROR msg => (print ("Error: " ^ msg); error msg) 
53800  316 

43021  317 
fun maybe f (accum as (outcome_code, _)) = 
53052
a0db255af8c5
sledgehammer sendback always uses Markup.padding_command: sensible default for most practical applications  oldstyle inline replacement is superseded by auto mode or panel;
wenzelm
parents:
53048
diff
changeset

318 
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

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

320 
(unknownN, state) 
54308  321 
> (if mode = Auto_Try then 
43021  322 
launch_full_atps 
54308  323 
else if blocking then 
324 
launch_atps_and_smt_solvers #> max_outcome_code #> rpair state 

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

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

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

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

330 
> `(fn (outcome_code, _) => outcome_code = someN) 
38044  331 

28582  332 
end; 