author  blanchet 
Wed, 08 Dec 2010 22:17:52 +0100  
changeset 41089  2e69fb6331cb 
parent 41088  54eb8e7c7f9b 
child 41090  b98fe4de1ecd 
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 
40061
71cc5aac8b76
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents:
40060
diff
changeset

14 

38044  15 
val run_sledgehammer : 
39318  16 
params > bool > int > relevance_override > (string > minimize_command) 
17 
> Proof.state > bool * Proof.state 

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

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

19 

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

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

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

22 

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

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

27 

41089  28 
fun prover_description ctxt ({blocking, verbose, ...} : params) name num_facts i 
29 
n goal = 

30 
quote name ^ 

31 
(if verbose then 

32 
" with " ^ string_of_int num_facts ^ " fact" ^ plural_s num_facts 

33 
else 

34 
"") ^ 

35 
" on " ^ (if n = 1 then "goal" else "subgoal " ^ string_of_int i) ^ ":" ^ 

36 
(if blocking then 

37 
"" 

38 
else 

39 
"\n" ^ Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i))) 

40 

41 
fun run_prover (params as {blocking, debug, max_relevant, timeout, expect, ...}) 

42 
auto minimize_command only 

43 
{state, goal, subgoal, subgoal_count, facts} name = 

44 
let 

45 
val ctxt = Proof.context_of state 

46 
val birth_time = Time.now () 

47 
val death_time = Time.+ (birth_time, timeout) 

48 
val max_relevant = 

49 
the_default (default_max_relevant_for_prover ctxt name) max_relevant 

50 
val num_facts = length facts > not only ? Integer.min max_relevant 

51 
val desc = 

52 
prover_description ctxt params name num_facts subgoal subgoal_count goal 

53 
val prover = get_prover ctxt auto name 

54 
val problem = 

55 
{state = state, goal = goal, subgoal = subgoal, 

56 
subgoal_count = subgoal_count, facts = take num_facts facts} 

57 
fun go () = 

58 
let 

59 
fun really_go () = 

60 
prover params (minimize_command name) problem 

61 
> (fn {outcome, message, ...} => 

62 
(if is_some outcome then "none" else "some", message)) 

63 
val (outcome_code, message) = 

64 
if debug then 

65 
really_go () 

66 
else 

67 
(really_go () 

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

69 
 exn => 

70 
if Exn.is_interrupt exn then 

71 
reraise exn 

72 
else 

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

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

75 
val _ = 

76 
if expect = "" orelse outcome_code = expect then 

77 
() 

78 
else if blocking then 

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

80 
else 

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

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

83 
in 

84 
if auto then 

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

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

87 
Pretty.chunks [Pretty.str "", Pretty.mark Markup.hilite 

88 
(Pretty.str message)])) 

89 
end 

90 
else if blocking then 

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

92 
List.app Output.urgent_message 

93 
(Async_Manager.break_into_chunks [desc ^ "\n" ^ message]); 

94 
(success, state) 

95 
end 

96 
else 

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

98 
(false, state)) 

99 
end 

100 

40698  101 
(* FUDGE *) 
102 
val auto_max_relevant_divisor = 2 

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

103 

40205
277508b07418
if "debug" is on, print list of relevant facts (poweruser request);
blanchet
parents:
40204
diff
changeset

104 
fun fact_name (Untranslated ((name, _), _)) = SOME name 
41088  105 
 fact_name (ATP_Translated (_, p)) = Option.map (fst o fst) p 
40061
71cc5aac8b76
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents:
40060
diff
changeset

106 

40205
277508b07418
if "debug" is on, print list of relevant facts (poweruser request);
blanchet
parents:
40204
diff
changeset

107 
fun run_sledgehammer (params as {blocking, debug, provers, full_types, 
40069  108 
relevance_thresholds, max_relevant, ...}) 
39366
f58fbb959826
handle relevance filter corner cases more gracefully;
blanchet
parents:
39364
diff
changeset

109 
auto i (relevance_override as {only, ...}) minimize_command 
f58fbb959826
handle relevance filter corner cases more gracefully;
blanchet
parents:
39364
diff
changeset

110 
state = 
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset

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

112 
error "No prover is set." 
39318  113 
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

114 
0 => (Output.urgent_message "No subgoal!"; (false, state)) 
39318  115 
 n => 
116 
let 

39364  117 
val _ = Proof.assert_backward state 
40200  118 
val ctxt = Proof.context_of state 
119 
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

120 
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

121 
val _ = () > not blocking ? kill_provers 
40941
a3e6f8634a11
replace "smt" prover with specific SMT solvers, e.g. "z3"  whatever the SMT module gives us
blanchet
parents:
40723
diff
changeset

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

123 
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

124 
 NONE => () 
40132
7ee65dbffa31
renamed Output.priority to Output.urgent_message to emphasize its special role more clearly;
wenzelm
parents:
40114
diff
changeset

125 
val _ = if auto then () else Output.urgent_message "Sledgehammering..." 
40941
a3e6f8634a11
replace "smt" prover with specific SMT solvers, e.g. "z3"  whatever the SMT module gives us
blanchet
parents:
40723
diff
changeset

126 
val (smts, atps) = provers > List.partition (is_smt_prover ctxt) 
40369
53dca3bd4250
use the SMT integration's official list of builtins
blanchet
parents:
40341
diff
changeset

127 
fun run_provers label full_types relevance_fudge maybe_translate provers 
53dca3bd4250
use the SMT integration's official list of builtins
blanchet
parents:
40341
diff
changeset

128 
(res as (success, state)) = 
40065  129 
if success orelse null provers then 
40060
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset

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

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

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

133 
val max_max_relevant = 
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset

134 
case max_relevant of 
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset

135 
SOME n => n 
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset

136 
 NONE => 
40941
a3e6f8634a11
replace "smt" prover with specific SMT solvers, e.g. "z3"  whatever the SMT module gives us
blanchet
parents:
40723
diff
changeset

137 
0 > fold (Integer.max o default_max_relevant_for_prover ctxt) 
40065  138 
provers 
40060
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset

139 
> auto ? (fn n => n div auto_max_relevant_divisor) 
40369
53dca3bd4250
use the SMT integration's official list of builtins
blanchet
parents:
40341
diff
changeset

140 
val is_built_in_const = 
53dca3bd4250
use the SMT integration's official list of builtins
blanchet
parents:
40341
diff
changeset

141 
is_built_in_const_for_prover ctxt (hd provers) 
40204
da97d75e20e6
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer  but keep "Axiom" in the lowerlevel "ATP_Problem" module
blanchet
parents:
40202
diff
changeset

142 
val facts = 
40065  143 
relevant_facts ctxt full_types relevance_thresholds 
40369
53dca3bd4250
use the SMT integration's official list of builtins
blanchet
parents:
40341
diff
changeset

144 
max_max_relevant is_built_in_const relevance_fudge 
40071
658a37c80b53
generalized the relevance filter so that it takes the list of "irrelevant constants" as argument (since the ATP and SMT preprocessing are different)
blanchet
parents:
40070
diff
changeset

145 
relevance_override chained_ths hyp_ts concl_t 
40114  146 
> map maybe_translate 
40062  147 
val problem = 
40065  148 
{state = state, goal = goal, subgoal = i, subgoal_count = n, 
40983  149 
facts = facts} 
150 
val run_prover = run_prover params auto minimize_command only 

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

151 
in 
40205
277508b07418
if "debug" is on, print list of relevant facts (poweruser request);
blanchet
parents:
40204
diff
changeset

152 
if debug then 
40370  153 
Output.urgent_message (label ^ plural_s (length provers) ^ ": " ^ 
40205
277508b07418
if "debug" is on, print list of relevant facts (poweruser request);
blanchet
parents:
40204
diff
changeset

154 
(if null facts then 
277508b07418
if "debug" is on, print list of relevant facts (poweruser request);
blanchet
parents:
40204
diff
changeset

155 
"Found no relevant facts." 
277508b07418
if "debug" is on, print list of relevant facts (poweruser request);
blanchet
parents:
40204
diff
changeset

156 
else 
277508b07418
if "debug" is on, print list of relevant facts (poweruser request);
blanchet
parents:
40204
diff
changeset

157 
"Including (up to) " ^ string_of_int (length facts) ^ 
277508b07418
if "debug" is on, print list of relevant facts (poweruser request);
blanchet
parents:
40204
diff
changeset

158 
" relevant fact" ^ plural_s (length facts) ^ ":\n" ^ 
277508b07418
if "debug" is on, print list of relevant facts (poweruser request);
blanchet
parents:
40204
diff
changeset

159 
(facts > map_filter fact_name 
277508b07418
if "debug" is on, print list of relevant facts (poweruser request);
blanchet
parents:
40204
diff
changeset

160 
> space_implode " ") ^ ".")) 
277508b07418
if "debug" is on, print list of relevant facts (poweruser request);
blanchet
parents:
40204
diff
changeset

161 
else 
277508b07418
if "debug" is on, print list of relevant facts (poweruser request);
blanchet
parents:
40204
diff
changeset

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

163 
if auto then 
40061
71cc5aac8b76
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents:
40060
diff
changeset

164 
fold (fn prover => fn (true, state) => (true, state) 
40064
db8413d82c3b
got rid of duplicate functionality ("run_smt_solver_somehow");
blanchet
parents:
40063
diff
changeset

165 
 (false, _) => run_prover problem prover) 
40065  166 
provers (false, state) 
40060
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset

167 
else 
40065  168 
provers > (if blocking then Par_List.map else map) 
169 
(run_prover problem) 

170 
> exists fst > rpair state 

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

171 
end 
40071
658a37c80b53
generalized the relevance filter so that it takes the list of "irrelevant constants" as argument (since the ATP and SMT preprocessing are different)
blanchet
parents:
40070
diff
changeset

172 
val run_atps = 
40370  173 
run_provers "ATP" full_types atp_relevance_fudge 
41088  174 
(ATP_Translated o translate_atp_fact ctxt) atps 
40071
658a37c80b53
generalized the relevance filter so that it takes the list of "irrelevant constants" as argument (since the ATP and SMT preprocessing are different)
blanchet
parents:
40070
diff
changeset

175 
val run_smts = 
40370  176 
run_provers "SMT solver" true smt_relevance_fudge Untranslated smts 
40060
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset

177 
fun run_atps_and_smt_solvers () = 
40065  178 
[run_atps, run_smts] > Par_List.map (fn f => f (false, state) > K ()) 
40060
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset

179 
in 
40065  180 
(false, state) 
181 
> (if blocking then run_atps #> not auto ? run_smts 

182 
else (fn p => Future.fork (tap run_atps_and_smt_solvers) > K p)) 

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

183 
end 
38044  184 

28582  185 
end; 