author  blanchet 
Sun, 22 May 2011 14:51:42 +0200  
changeset 42946  ddff373cf3ad 
parent 42944  9e620869a576 
child 42952  96f62b77748f 
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 
38988  11 
type relevance_override = Sledgehammer_Filter.relevance_override 
40068  12 
type minimize_command = Sledgehammer_ATP_Reconstruct.minimize_command 
41087
d7b5fd465198
split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems
blanchet
parents:
41066
diff
changeset

13 
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

14 
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

15 

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

16 
val auto_minimize_min_facts : int Config.T 
42444
8e5438dc70bb
cleanup: get rid of "may_slice" arguments without changing semantics
blanchet
parents:
42443
diff
changeset

17 
val get_minimizing_prover : Proof.context > bool > string > prover 
38044  18 
val run_sledgehammer : 
42444
8e5438dc70bb
cleanup: get rid of "may_slice" arguments without changing semantics
blanchet
parents:
42443
diff
changeset

19 
params > bool > int > relevance_override > (string > minimize_command) 
8e5438dc70bb
cleanup: get rid of "may_slice" arguments without changing semantics
blanchet
parents:
42443
diff
changeset

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

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

22 

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

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

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

25 

38023  26 
open Sledgehammer_Util 
38988  27 
open Sledgehammer_Filter 
40068  28 
open Sledgehammer_ATP_Translate 
41087
d7b5fd465198
split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems
blanchet
parents:
41066
diff
changeset

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

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

31 

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

32 
fun prover_description ctxt ({verbose, blocking, ...} : params) name num_facts i 
41089  33 
n goal = 
34 
quote name ^ 

35 
(if verbose then 

36 
" with " ^ string_of_int num_facts ^ " fact" ^ plural_s num_facts 

37 
else 

38 
"") ^ 

41743  39 
" on " ^ (if n = 1 then "goal" else "subgoal " ^ string_of_int i) ^ 
41089  40 
(if blocking then 
41743  41 
"." 
41089  42 
else 
41743  43 
":\n" ^ Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i))) 
41089  44 

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

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

46 
Attrib.setup_config_int @{binding sledgehammer_auto_minimize_min_facts} 
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42642
diff
changeset

47 
(fn generic => Config.get_generic generic binary_min_facts) 
41091
0afdf5cde874
implicitly call the minimizer for SMT solvers that don't return an unsat core
blanchet
parents:
41090
diff
changeset

48 

42444
8e5438dc70bb
cleanup: get rid of "may_slice" arguments without changing semantics
blanchet
parents:
42443
diff
changeset

49 
fun get_minimizing_prover ctxt auto name 
41742
11e862c68b40
automatically minimize Z3asanATP proofs (cf. CVC3 and Yices)
blanchet
parents:
41741
diff
changeset

50 
(params as {debug, verbose, explicit_apply, ...}) minimize_command 
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

51 
(problem as {state, subgoal, subgoal_count, facts, ...}) = 
42444
8e5438dc70bb
cleanup: get rid of "may_slice" arguments without changing semantics
blanchet
parents:
42443
diff
changeset

52 
get_prover ctxt auto name params minimize_command problem 
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

53 
> (fn result as {outcome, used_facts, run_time_in_msecs, message} => 
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

54 
if is_some outcome then 
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

55 
result 
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

56 
else 
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

57 
let 
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

58 
val (used_facts, message) = 
42646
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42642
diff
changeset

59 
if length used_facts 
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42642
diff
changeset

60 
>= Config.get ctxt auto_minimize_min_facts then 
41742
11e862c68b40
automatically minimize Z3asanATP proofs (cf. CVC3 and Yices)
blanchet
parents:
41741
diff
changeset

61 
minimize_facts name params (SOME explicit_apply) (not verbose) 
11e862c68b40
automatically minimize Z3asanATP proofs (cf. CVC3 and Yices)
blanchet
parents:
41741
diff
changeset

62 
subgoal subgoal_count state 
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

63 
(filter_used_facts used_facts 
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

64 
(map (apsnd single o untranslated_fact) facts)) 
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

65 
>> Option.map (map fst) 
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

66 
else 
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

67 
(SOME used_facts, message) 
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

68 
in 
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

69 
case used_facts of 
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

70 
SOME used_facts => 
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

71 
(if debug andalso not (null used_facts) then 
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

72 
facts ~~ (0 upto length facts  1) 
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

73 
> map (fn (fact, j) => 
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

74 
fact > untranslated_fact > apsnd (K j)) 
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

75 
> filter_used_facts used_facts 
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

76 
> map (fn ((name, _), j) => name ^ "@" ^ string_of_int j) 
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

77 
> commas 
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

78 
> enclose ("Fact" ^ plural_s (length facts) ^ " in " ^ 
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

79 
quote name ^ " proof (of " ^ 
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

80 
string_of_int (length facts) ^ "): ") "." 
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

81 
> Output.urgent_message 
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

82 
else 
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

83 
(); 
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

84 
{outcome = NONE, used_facts = used_facts, 
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

85 
run_time_in_msecs = run_time_in_msecs, message = message}) 
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

86 
 NONE => result 
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

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

88 

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

89 
fun launch_prover (params as {debug, blocking, max_relevant, slicing, timeout, 
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42361
diff
changeset

90 
expect, ...}) 
42444
8e5438dc70bb
cleanup: get rid of "may_slice" arguments without changing semantics
blanchet
parents:
42443
diff
changeset

91 
auto minimize_command only 
41741  92 
{state, goal, subgoal, subgoal_count, facts, smt_filter} name = 
41089  93 
let 
94 
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

95 
val hard_timeout = Time.+ (timeout, timeout) 
41089  96 
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

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

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

100 
> the_default (default_max_relevant_for_prover ctxt slicing name) 
41089  101 
val num_facts = length facts > not only ? Integer.min max_relevant 
102 
val desc = 

103 
prover_description ctxt params name num_facts subgoal subgoal_count goal 

104 
val problem = 

105 
{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

106 
subgoal_count = subgoal_count, facts = facts > take num_facts, 
41741  107 
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

108 
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

109 
problem 
42444
8e5438dc70bb
cleanup: get rid of "may_slice" arguments without changing semantics
blanchet
parents:
42443
diff
changeset

110 
> get_minimizing_prover ctxt auto name params (minimize_command name) 
41262
095ecb0c687f
factored out running a prover with (optionally) an implicit minimizer phrase
blanchet
parents:
41260
diff
changeset

111 
> (fn {outcome, message, ...} => 
095ecb0c687f
factored out running a prover with (optionally) an implicit minimizer phrase
blanchet
parents:
41260
diff
changeset

112 
(if is_some outcome then "none" else "some" (* sic *), message)) 
41089  113 
fun go () = 
114 
let 

115 
val (outcome_code, message) = 

116 
if debug then 

117 
really_go () 

118 
else 

119 
(really_go () 

120 
handle ERROR message => ("unknown", "Error: " ^ message ^ "\n") 

121 
 exn => 

122 
if Exn.is_interrupt exn then 

123 
reraise exn 

124 
else 

125 
("unknown", "Internal error:\n" ^ 

126 
ML_Compiler.exn_message exn ^ "\n")) 

127 
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

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

129 
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

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

131 
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

132 
not (is_prover_installed ctxt name) then 
41089  133 
() 
134 
else if blocking then 

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

136 
else 

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

138 
in (outcome_code = "some", message) end 

139 
in 

140 
if auto then 

141 
let val (success, message) = TimeLimit.timeLimit timeout go () in 

142 
(success, state > success ? Proof.goal_message (fn () => 

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

143 
Pretty.chunks [Pretty.str "", 
0afdf5cde874
implicitly call the minimizer for SMT solvers that don't return an unsat core
blanchet
parents:
41090
diff
changeset

144 
Pretty.mark Markup.hilite (Pretty.str message)])) 
41089  145 
end 
146 
else if blocking then 

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 
let val (success, message) = TimeLimit.timeLimit hard_timeout go () in 
41089  148 
List.app Output.urgent_message 
149 
(Async_Manager.break_into_chunks [desc ^ "\n" ^ message]); 

150 
(success, state) 

151 
end 

152 
else 

153 
(Async_Manager.launch das_Tool birth_time death_time desc (snd o go); 

154 
(false, state)) 

155 
end 

156 

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

157 
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

158 
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

159 
> 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

160 

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

161 
(* Makes backtraces more transparent and might be more efficient as well. *) 
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

162 
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

163 
 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

164 
 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

165 

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

166 
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

167 
 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

168 

42579
2552c09b1a72
implement the new ATP type system in Sledgehammer
blanchet
parents:
42544
diff
changeset

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

170 

42946  171 
fun run_sledgehammer (params as {debug, verbose, blocking, provers, 
172 
relevance_thresholds, max_relevant, slicing, 

173 
timeout, ...}) 

42444
8e5438dc70bb
cleanup: get rid of "may_slice" arguments without changing semantics
blanchet
parents:
42443
diff
changeset

174 
auto 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

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

176 
error "No prover is set." 
39318  177 
else case subgoal_count state of 
40132
7ee65dbffa31
renamed Output.priority to Output.urgent_message to emphasize its special role more clearly;
wenzelm
parents:
40114
diff
changeset

178 
0 => (Output.urgent_message "No subgoal!"; (false, state)) 
39318  179 
 n => 
180 
let 

39364  181 
val _ = Proof.assert_backward state 
41773  182 
val print = if auto then K () else Output.urgent_message 
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

183 
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

184 
state > Proof.map_context (Config.put SMT_Config.verbose debug) 
40200  185 
val ctxt = Proof.context_of state 
186 
val {facts = chained_ths, goal, ...} = Proof.goal state 

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

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

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

189 
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

190 
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

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

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

194 
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

195 
> List.partition (is_unit_equational_atp ctxt) 
41741  196 
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

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

198 
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

199 
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

200 
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

201 
> 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

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

203 
{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

204 
facts = facts, 
41741  205 
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

206 
(fn () => map_filter (try dest_SMT_Weighted_Fact) facts) i} 
42444
8e5438dc70bb
cleanup: get rid of "may_slice" arguments without changing semantics
blanchet
parents:
42443
diff
changeset

207 
val launch = launch_prover params auto 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

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

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

210 
fold (fn prover => fn (true, state) => (true, state) 
41262
095ecb0c687f
factored out running a prover with (optionally) an implicit minimizer phrase
blanchet
parents:
41260
diff
changeset

211 
 (false, _) => launch problem prover) 
41256
0e7d45cc005f
put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents:
41255
diff
changeset

212 
provers (false, state) 
0e7d45cc005f
put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents:
41255
diff
changeset

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

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

215 
> (if blocking then smart_par_list_map else map) (launch problem) 
41256
0e7d45cc005f
put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents:
41255
diff
changeset

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

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

218 
fun get_facts label is_good_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

219 
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

220 
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

221 
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

222 
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

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

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

225 
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

226 
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

227 
> auto ? (fn n => n div auto_max_relevant_divisor) 
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 
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

229 
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

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

231 
relevant_facts ctxt relevance_thresholds max_max_relevant is_good_prop 
42579
2552c09b1a72
implement the new ATP type system in Sledgehammer
blanchet
parents:
42544
diff
changeset

232 
is_built_in_const relevance_fudge relevance_override 
2552c09b1a72
implement the new ATP type system in Sledgehammer
blanchet
parents:
42544
diff
changeset

233 
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

234 
> 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

235 
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

236 
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

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

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

239 
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

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

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

242 
(facts > map (fst o fst) > space_implode " ") ^ ".") 
41773  243 

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

245 
()) 
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

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

247 
fun launch_atps label is_good_prop atps accum = 
42946  248 
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

249 
accum 
42946  250 
else if not (is_good_prop concl_t) then 
251 
(if verbose orelse length atps = length provers then 

252 
"Goal outside the scope of " ^ 

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

254 
> Output.urgent_message 

255 
else 

256 
(); 

257 
accum) 

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

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

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

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

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

262 
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

263 
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

264 
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

265 
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

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

267 
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

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

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

271 
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

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

273 
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

274 
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

275 
> AList.group (op =) 
41741  276 
> map (launch_provers state (K facts) weight smt_filter o snd) 
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

277 
> exists fst > rpair 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

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

279 
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

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

281 
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

282 
fun launch_atps_and_smt_solvers () = 
42944
9e620869a576
improved Waldmeister support  even run it by default on unit equational goals
blanchet
parents:
42850
diff
changeset

283 
[launch_full_atps, launch_ueq_atps, launch_smts] 
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

284 
> smart_par_list_map (fn f => f (false, state) > K ()) 
41773  285 
handle ERROR msg => (print ("Error: " ^ msg); error msg) 
40060
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset

286 
in 
40065  287 
(false, state) 
42944
9e620869a576
improved Waldmeister support  even run it by default on unit equational goals
blanchet
parents:
42850
diff
changeset

288 
> (if blocking then 
9e620869a576
improved Waldmeister support  even run it by default on unit equational goals
blanchet
parents:
42850
diff
changeset

289 
launch_full_atps #> not auto ? (launch_ueq_atps #> launch_smts) 
9e620869a576
improved Waldmeister support  even run it by default on unit equational goals
blanchet
parents:
42850
diff
changeset

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

291 
(fn p => Future.fork (tap launch_atps_and_smt_solvers) > K p)) 
41773  292 
handle TimeLimit.TimeOut => 
293 
(print "Sledgehammer ran out of time."; (false, state)) 

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

294 
end 
38044  295 

28582  296 
end; 