author  blanchet 
Wed, 08 Jun 2011 16:20:18 +0200  
changeset 43292  ff3d49e77359 
parent 43290  07eb0ad9bb93 
child 43306  03e6da81aee6 
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 
43290
07eb0ad9bb93
renamed option to avoid talking about seconds, since this is now the default Isabelle unit
blanchet
parents:
43261
diff
changeset

22 
val auto_minimize_max_time : 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) 
43290
07eb0ad9bb93
renamed option to avoid talking about seconds, since this is now the default Isabelle unit
blanchet
parents:
43261
diff
changeset

72 
val auto_minimize_max_time = 
07eb0ad9bb93
renamed option to avoid talking about seconds, since this is now the default Isabelle unit
blanchet
parents:
43261
diff
changeset

73 
Attrib.setup_config_real @{binding sledgehammer_auto_minimize_max_time} 
43052
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, 

43261
a4aeb26a6362
make sure that the message tail (timing + TPTP important message) is preserved upon automatic minimization
blanchet
parents:
43233
diff
changeset

79 
message, message_tail} : prover_result) = 
43292
ff3d49e77359
don't launch the automatic minimizer for zero facts
blanchet
parents:
43290
diff
changeset

80 
if is_some outcome orelse null used_facts then 
43164  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) 
43290
07eb0ad9bb93
renamed option to avoid talking about seconds, since this is now the default Isabelle unit
blanchet
parents:
43261
diff
changeset

93 
<= Config.get ctxt auto_minimize_max_time 
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

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 
43233
2749c357f865
use the proper prover name, e.g. metis_full_types, not metis (full_types), for minimizing
blanchet
parents:
43165
diff
changeset

105 
(true, prover_name_for_reconstructor reconstructor 
2749c357f865
use the proper prover name, e.g. metis_full_types, not metis (full_types), for minimizing
blanchet
parents:
43165
diff
changeset

106 
> the_default name) 
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

107 
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

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 
 _ => (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

110 
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

111 
end 
43164  112 
end 
113 
else 

114 
((false, name), preplay) 

43261
a4aeb26a6362
make sure that the message tail (timing + TPTP important message) is preserved upon automatic minimization
blanchet
parents:
43233
diff
changeset

115 
val (used_facts, (preplay, message, _)) = 
43164  116 
if minimize then 
117 
minimize_facts minimize_name params (not verbose) subgoal 

118 
subgoal_count state 

119 
(filter_used_facts used_facts 

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

121 
>> Option.map (map fst) 

122 
else 

43261
a4aeb26a6362
make sure that the message tail (timing + TPTP important message) is preserved upon automatic minimization
blanchet
parents:
43233
diff
changeset

123 
(SOME used_facts, (preplay, message, "")) 
43164  124 
in 
125 
case used_facts of 

126 
SOME used_facts => 

127 
(if debug andalso not (null used_facts) then 

128 
facts ~~ (0 upto length facts  1) 

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

130 
> filter_used_facts used_facts 

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

132 
> commas 

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

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

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

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

139 
run_time_in_msecs = run_time_in_msecs, preplay = preplay, 

43261
a4aeb26a6362
make sure that the message tail (timing + TPTP important message) is preserved upon automatic minimization
blanchet
parents:
43233
diff
changeset

140 
message = message, message_tail = message_tail}) 
43164  141 
 NONE => result 
142 
end 

143 

144 
fun get_minimizing_prover ctxt mode name params minimize_command problem = 

145 
get_prover ctxt mode name params minimize_command problem 

146 
> minimize ctxt mode name params problem 

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

147 

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

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

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

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

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

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

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

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

167 
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

168 
problem 
43051  169 
> get_minimizing_prover ctxt mode name params minimize_command 
43261
a4aeb26a6362
make sure that the message tail (timing + TPTP important message) is preserved upon automatic minimization
blanchet
parents:
43233
diff
changeset

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

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

172 
else if is_some outcome then noneN 
43261
a4aeb26a6362
make sure that the message tail (timing + TPTP important message) is preserved upon automatic minimization
blanchet
parents:
43233
diff
changeset

173 
else someN, fn () => message (preplay ()) ^ message_tail)) 
41089  174 
fun go () = 
175 
let 

176 
val (outcome_code, message) = 

177 
if debug then 

178 
really_go () 

179 
else 

180 
(really_go () 

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

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

184 
reraise exn 

185 
else 

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

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

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

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

190 
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

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

192 
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

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

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

197 
else 

198 
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

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

204 
state 

205 
> outcome_code = someN 

206 
? Proof.goal_message (fn () => 

207 
[Pretty.str "", 

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

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

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

214 
in 

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

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

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

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

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

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

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

43006  224 
(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

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

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

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

231 
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

232 
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

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

234 

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

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

236 
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

237 
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

238 
 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

239 
 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

240 

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

241 
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

242 
 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

243 

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

245 

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

248 
timeout, ...}) 

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

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

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

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

39364  256 
val _ = Proof.assert_backward state 
43021  257 
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

258 
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

259 
state > Proof.map_context (Config.put SMT_Config.verbose debug) 
40200  260 
val ctxt = Proof.context_of state 
261 
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

262 
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

263 
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

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

265 
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

266 
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

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

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

270 
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

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

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

274 
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

275 
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

276 
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

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

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

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

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

282 
(fn () => map_filter (try dest_SMT_Weighted_Fact) facts) i} 
43021  283 
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

284 
in 
43021  285 
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

286 
(unknownN, state) 
43021  287 
> 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

288 
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

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

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

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

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

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

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

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

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

297 
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

298 
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

299 
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

300 
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

301 
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

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

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

304 
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

305 
provers 
43021  306 
> mode = Auto_Try 
307 
? (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

308 
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

309 
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

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

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

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

313 
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

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

315 
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

316 
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

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

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

319 
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

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

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

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

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

324 
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

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

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

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

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

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

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

334 
> Output.urgent_message 

335 
else 

336 
(); 

337 
accum) 

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

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

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

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

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

342 
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

343 
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

344 
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

345 
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

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

347 
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

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

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

351 
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

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

353 
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

354 
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

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

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

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

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

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

360 
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

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

362 
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

363 
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

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

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

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

371 
> (if blocking then 
43021  372 
launch_full_atps 
373 
#> 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

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

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

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

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

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

28582  381 
end; 