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

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

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

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

5 

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

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

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

8 

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

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

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

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

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

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

16 

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

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

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

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

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

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

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

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

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

28 

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

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

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

31 

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

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

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

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

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

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

39 

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

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

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

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

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

44 

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

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

46 

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

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

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

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

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

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

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

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

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

55 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

75 

43165
8cf188ff76a3
refined auto minimization code: don't use Metis if Isar proofs are desired, and fall back on prover if Metis is too slow
blanchet
parents:
43164
diff
changeset

76 
fun minimize ctxt mode name (params as {debug, verbose, isar_proof, ...}) 
43164  77 
({state, subgoal, subgoal_count, facts, ...} : prover_problem) 
78 
(result as {outcome, used_facts, run_time_in_msecs, preplay, 

79 
message} : prover_result) = 

80 
if is_some outcome then 

81 
result 

82 
else 

83 
let 

84 
val num_facts = length used_facts 

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

86 
if mode = Normal then 

87 
if num_facts >= Config.get ctxt auto_minimize_min_facts then 

88 
((true, name), preplay) 

89 
else 

43165
8cf188ff76a3
refined auto minimization code: don't use Metis if Isar proofs are desired, and fall back on prover if Metis is too slow
blanchet
parents:
43164
diff
changeset

90 
let 
8cf188ff76a3
refined auto minimization code: don't use Metis if Isar proofs are desired, and fall back on prover if Metis is too slow
blanchet
parents:
43164
diff
changeset

91 
fun can_min_fast_enough msecs = 
8cf188ff76a3
refined auto minimization code: don't use Metis if Isar proofs are desired, and fall back on prover if Metis is too slow
blanchet
parents:
43164
diff
changeset

92 
0.001 * Real.fromInt ((num_facts + 2) * msecs) 
8cf188ff76a3
refined auto minimization code: don't use Metis if Isar proofs are desired, and fall back on prover if Metis is too slow
blanchet
parents:
43164
diff
changeset

93 
<= Config.get ctxt auto_minimize_max_seconds 
8cf188ff76a3
refined auto minimization code: don't use Metis if Isar proofs are desired, and fall back on prover if Metis is too slow
blanchet
parents:
43164
diff
changeset

94 
val prover_fast_enough = 
8cf188ff76a3
refined auto minimization code: don't use Metis if Isar proofs are desired, and fall back on prover if Metis is too slow
blanchet
parents:
43164
diff
changeset

95 
run_time_in_msecs > Option.map can_min_fast_enough 
8cf188ff76a3
refined auto minimization code: don't use Metis if Isar proofs are desired, and fall back on prover if Metis is too slow
blanchet
parents:
43164
diff
changeset

96 
> the_default false 
8cf188ff76a3
refined auto minimization code: don't use Metis if Isar proofs are desired, and fall back on prover if Metis is too slow
blanchet
parents:
43164
diff
changeset

97 
in 
8cf188ff76a3
refined auto minimization code: don't use Metis if Isar proofs are desired, and fall back on prover if Metis is too slow
blanchet
parents:
43164
diff
changeset

98 
if isar_proof then 
8cf188ff76a3
refined auto minimization code: don't use Metis if Isar proofs are desired, and fall back on prover if Metis is too slow
blanchet
parents:
43164
diff
changeset

99 
((prover_fast_enough, name), preplay) 
8cf188ff76a3
refined auto minimization code: don't use Metis if Isar proofs are desired, and fall back on prover if Metis is too slow
blanchet
parents:
43164
diff
changeset

100 
else 
8cf188ff76a3
refined auto minimization code: don't use Metis if Isar proofs are desired, and fall back on prover if Metis is too slow
blanchet
parents:
43164
diff
changeset

101 
let val preplay = preplay () in 
8cf188ff76a3
refined auto minimization code: don't use Metis if Isar proofs are desired, and fall back on prover if Metis is too slow
blanchet
parents:
43164
diff
changeset

102 
(case preplay of 
8cf188ff76a3
refined auto minimization code: don't use Metis if Isar proofs are desired, and fall back on prover if Metis is too slow
blanchet
parents:
43164
diff
changeset

103 
Played (reconstructor, timeout) => 
8cf188ff76a3
refined auto minimization code: don't use Metis if Isar proofs are desired, and fall back on prover if Metis is too slow
blanchet
parents:
43164
diff
changeset

104 
if can_min_fast_enough (Time.toMilliseconds timeout) then 
8cf188ff76a3
refined auto minimization code: don't use Metis if Isar proofs are desired, and fall back on prover if Metis is too slow
blanchet
parents:
43164
diff
changeset

105 
(true, reconstructor_name reconstructor) 
8cf188ff76a3
refined auto minimization code: don't use Metis if Isar proofs are desired, and fall back on prover if Metis is too slow
blanchet
parents:
43164
diff
changeset

106 
else 
8cf188ff76a3
refined auto minimization code: don't use Metis if Isar proofs are desired, and fall back on prover if Metis is too slow
blanchet
parents:
43164
diff
changeset

107 
(prover_fast_enough, name) 
8cf188ff76a3
refined auto minimization code: don't use Metis if Isar proofs are desired, and fall back on prover if Metis is too slow
blanchet
parents:
43164
diff
changeset

108 
 _ => (prover_fast_enough, name), 
8cf188ff76a3
refined auto minimization code: don't use Metis if Isar proofs are desired, and fall back on prover if Metis is too slow
blanchet
parents:
43164
diff
changeset

109 
K preplay) 
8cf188ff76a3
refined auto minimization code: don't use Metis if Isar proofs are desired, and fall back on prover if Metis is too slow
blanchet
parents:
43164
diff
changeset

110 
end 
43164  111 
end 
112 
else 

113 
((false, name), preplay) 

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

115 
if minimize then 

116 
minimize_facts minimize_name params (not verbose) subgoal 

117 
subgoal_count state 

118 
(filter_used_facts used_facts 

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

120 
>> Option.map (map fst) 

121 
else 

122 
(SOME used_facts, (preplay, message)) 

123 
in 

124 
case used_facts of 

125 
SOME used_facts => 

126 
(if debug andalso not (null used_facts) then 

127 
facts ~~ (0 upto length facts  1) 

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

129 
> filter_used_facts used_facts 

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

131 
> commas 

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

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

134 
> Output.urgent_message 

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

135 
else 
43164  136 
(); 
137 
{outcome = NONE, used_facts = used_facts, 

138 
run_time_in_msecs = run_time_in_msecs, preplay = preplay, 

139 
message = message}) 

140 
 NONE => result 

141 
end 

142 

143 
fun get_minimizing_prover ctxt mode name params minimize_command problem = 

144 
get_prover ctxt mode name params minimize_command problem 

145 
> minimize ctxt mode name params problem 

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

146 

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

43021  149 
mode minimize_command only 
41741  150 
{state, goal, subgoal, subgoal_count, facts, smt_filter} name = 
41089  151 
let 
152 
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

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

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

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

158 
> the_default (default_max_relevant_for_prover ctxt slicing name) 
41089  159 
val num_facts = length facts > not only ? Integer.min max_relevant 
43006  160 
fun desc () = 
41089  161 
prover_description ctxt params name num_facts subgoal subgoal_count goal 
162 
val problem = 

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

164 
subgoal_count = subgoal_count, facts = facts > take num_facts, 
41741  165 
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

166 
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

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

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

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

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

172 
else someN, message o preplay)) 
41089  173 
fun go () = 
174 
let 

175 
val (outcome_code, message) = 

176 
if debug then 

177 
really_go () 

178 
else 

179 
(really_go () 

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

180 
handle ERROR msg => (unknownN, fn () => "Error: " ^ msg ^ "\n") 
41089  181 
 exn => 
182 
if Exn.is_interrupt exn then 

183 
reraise exn 

184 
else 

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

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

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

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

189 
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

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

191 
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

192 
not (is_prover_installed ctxt name) then 
41089  193 
() 
194 
else if blocking then 

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

196 
else 

197 
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

198 
in (outcome_code, message) end 
41089  199 
in 
43021  200 
if mode = Auto_Try then 
43006  201 
let val (outcome_code, message) = TimeLimit.timeLimit timeout go () in 
202 
(outcome_code, 

203 
state 

204 
> outcome_code = someN 

205 
? Proof.goal_message (fn () => 

206 
[Pretty.str "", 

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

207 
Pretty.mark Markup.hilite (Pretty.str (message ()))] 
43006  208 
> Pretty.chunks)) 
41089  209 
end 
210 
else if blocking then 

43006  211 
let 
212 
val (outcome_code, message) = TimeLimit.timeLimit hard_timeout go () 

213 
in 

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

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

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

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

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

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

219 
> List.app Output.urgent_message; 
43006  220 
(outcome_code, state) 
41089  221 
end 
222 
else 

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

224 
((fn (outcome_code, message) => 
43059  225 
(verbose orelse outcome_code = someN, 
226 
message ())) o go); 

43006  227 
(unknownN, state)) 
41089  228 
end 
229 

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

230 
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

231 
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

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

233 

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

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

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

236 
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

237 
 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

238 
 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

239 

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

240 
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

241 
 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

242 

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

244 

42946  245 
fun run_sledgehammer (params as {debug, verbose, blocking, provers, 
246 
relevance_thresholds, max_relevant, slicing, 

247 
timeout, ...}) 

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

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

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

252 
0 => (Output.urgent_message "No subgoal!"; (false, (noneN, state))) 
39318  253 
 n => 
254 
let 

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

257 
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

258 
state > Proof.map_context (Config.put SMT_Config.verbose debug) 
40200  259 
val ctxt = Proof.context_of state 
260 
val {facts = chained_ths, goal, ...} = Proof.goal state 

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

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

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

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

264 
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

265 
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

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

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

269 
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

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

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

273 
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

274 
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

275 
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

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

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

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

279 
facts = facts, 
41741  280 
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

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

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

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

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

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

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

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

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

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

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

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

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

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

297 
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

298 
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

299 
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

300 
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

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

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

303 
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

304 
provers 
43021  305 
> mode = Auto_Try 
306 
? (fn n => n div auto_try_max_relevant_divisor) 

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

307 
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

308 
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

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

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

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

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

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

314 
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

315 
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

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

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

318 
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

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

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

321 
(facts > map (fst o fst) > space_implode " ") ^ ".") 
41773  322 

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

323 
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

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

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

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

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

329 
else if not (is_appropriate_prop concl_t) then 
42946  330 
(if verbose orelse length atps = length provers then 
331 
"Goal outside the scope of " ^ 

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

333 
> Output.urgent_message 

334 
else 

335 
(); 

336 
accum) 

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

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

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

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

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

341 
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

342 
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

343 
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

344 
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

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

346 
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

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

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

350 
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

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

352 
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

353 
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

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

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

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

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

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

359 
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

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

361 
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

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

363 
[launch_full_atps, launch_smts, launch_ueq_atps] 
43021  364 
> smart_par_list_map (fn f => ignore (f (unknownN, state))) 
41773  365 
handle ERROR msg => (print ("Error: " ^ msg); error msg) 
43021  366 
fun maybe f (accum as (outcome_code, _)) = 
367 
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

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

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

370 
> (if blocking then 
43021  371 
launch_full_atps 
372 
#> mode <> Auto_Try ? (maybe launch_ueq_atps #> maybe launch_smts) 

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

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

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

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

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

378 
> `(fn (outcome_code, _) => outcome_code = someN) 
38044  379 

28582  380 
end; 