author  blanchet 
Thu, 16 Sep 2010 15:38:46 +0200  
changeset 39493  cb2208f2c07d 
parent 39492  b1172d65dd28 
child 39494  bf7dd4902321 
permissions  rwrr 
38021
e024504943d1
rename "ATP_Manager" ML module to "Sledgehammer";
blanchet
parents:
38020
diff
changeset

1 
(* Title: HOL/Tools/Sledgehammer/sledgehammer.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 

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

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

10 
sig 
38023  11 
type failure = ATP_Systems.failure 
38988  12 
type locality = Sledgehammer_Filter.locality 
13 
type relevance_override = Sledgehammer_Filter.relevance_override 

39004
f1b465f889b5
translate the axioms to FOF once and for all ATPs
blanchet
parents:
39003
diff
changeset

14 
type fol_formula = Sledgehammer_Translate.fol_formula 
38988  15 
type minimize_command = Sledgehammer_Reconstruct.minimize_command 
39493
cb2208f2c07d
move SPASS's Flotter hack to "Sledgehammer_Reconstruct"
blanchet
parents:
39492
diff
changeset

16 

35969  17 
type params = 
38982
820b8221ed48
added "blocking" option to Sledgehammer to run in synchronous mode;
blanchet
parents:
38893
diff
changeset

18 
{blocking: bool, 
820b8221ed48
added "blocking" option to Sledgehammer to run in synchronous mode;
blanchet
parents:
38893
diff
changeset

19 
debug: bool, 
35969  20 
verbose: bool, 
36143
6490319b1703
added "overlord" option (to get easy access to output files for debugging) + systematically use "raw_goal" rather than an inconsistent mixture
blanchet
parents:
36064
diff
changeset

21 
overlord: bool, 
35969  22 
atps: string list, 
23 
full_types: bool, 

36235
61159615a0c5
added "explicit_apply" option to Sledgehammer, to control whether an explicit apply function should be used as much or as little as possible (replaces a previous global variable)
blanchet
parents:
36231
diff
changeset

24 
explicit_apply: bool, 
38745
ad577fd62ee4
reorganize options regarding to the relevance threshold and decay
blanchet
parents:
38744
diff
changeset

25 
relevance_thresholds: real * real, 
38744
2b6333f78a9e
make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents:
38741
diff
changeset

26 
max_relevant: int option, 
35969  27 
isar_proof: bool, 
36924  28 
isar_shrink_factor: int, 
38985
162bbbea4e4d
added "expect" feature of Nitpick to Sledgehammer, for regression testing
blanchet
parents:
38982
diff
changeset

29 
timeout: Time.time, 
162bbbea4e4d
added "expect" feature of Nitpick to Sledgehammer, for regression testing
blanchet
parents:
38982
diff
changeset

30 
expect: string} 
39493
cb2208f2c07d
move SPASS's Flotter hack to "Sledgehammer_Reconstruct"
blanchet
parents:
39492
diff
changeset

31 

35867  32 
type problem = 
39318  33 
{state: Proof.state, 
38998  34 
goal: thm, 
35 
subgoal: int, 

39366
f58fbb959826
handle relevance filter corner cases more gracefully;
blanchet
parents:
39364
diff
changeset

36 
axioms: (term * ((string * locality) * fol_formula) option) list, 
f58fbb959826
handle relevance filter corner cases more gracefully;
blanchet
parents:
39364
diff
changeset

37 
only: bool} 
39493
cb2208f2c07d
move SPASS's Flotter hack to "Sledgehammer_Reconstruct"
blanchet
parents:
39492
diff
changeset

38 

35867  39 
type prover_result = 
36370
a4f601daa175
centralized ATPspecific error handling in "atp_wrapper.ML"
blanchet
parents:
36369
diff
changeset

40 
{outcome: failure option, 
35969  41 
message: string, 
37926
e6ff246c0cdb
renamings + only need second component of name pool to reconstruct proofs
blanchet
parents:
37627
diff
changeset

42 
pool: string Symtab.table, 
38752
6628adcae4a7
consider "locality" when assigning weights to facts
blanchet
parents:
38748
diff
changeset

43 
used_thm_names: (string * locality) list, 
35969  44 
atp_run_time_in_msecs: int, 
36369
d2cd0d04b8e6
handle ATP proof delimiters in a cleaner, more extensible fashion
blanchet
parents:
36289
diff
changeset

45 
output: string, 
39452  46 
tstplike_proof: string, 
38818
61cf050f8b2e
improve SPASS hack, when a clause comes from several facts
blanchet
parents:
38752
diff
changeset

47 
axiom_names: (string * locality) list vector, 
38083
c4b57f68ddb3
remove the "extra_clauses" business introduced in 19a5f1c8a844;
blanchet
parents:
38061
diff
changeset

48 
conjecture_shape: int list list} 
39493
cb2208f2c07d
move SPASS's Flotter hack to "Sledgehammer_Reconstruct"
blanchet
parents:
39492
diff
changeset

49 

38100
e458a0dd3dc1
use "explicit_apply" in the minimizer whenever it might make a difference to prevent freak failures;
blanchet
parents:
38098
diff
changeset

50 
type prover = params > minimize_command > problem > prover_result 
35867  51 

38023  52 
val dest_dir : string Config.T 
53 
val problem_prefix : string Config.T 

39003
c2aebd79981f
run relevance filter in a thread, to avoid blocking
blanchet
parents:
39000
diff
changeset

54 
val measure_run_time : bool Config.T 
35969  55 
val kill_atps: unit > unit 
56 
val running_atps: unit > unit 

29112
f2b45eea6dac
added 'atp_messages' command, which displays recent messages synchronously;
wenzelm
parents:
28835
diff
changeset

57 
val messages: int option > unit 
38023  58 
val get_prover_fun : theory > string > prover 
38044  59 
val run_sledgehammer : 
39318  60 
params > bool > int > relevance_override > (string > minimize_command) 
61 
> Proof.state > bool * Proof.state 

38023  62 
val setup : theory > theory 
28477
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset

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

64 

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

65 
structure Sledgehammer : SLEDGEHAMMER = 
28477
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset

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

67 

38028  68 
open ATP_Problem 
39491
2416666e6f94
refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents:
39453
diff
changeset

69 
open ATP_Proof 
38028  70 
open ATP_Systems 
37578
9367cb36b1c4
renamed "Sledgehammer_FOL_Clauses" to "Metis_Clauses", so that Metis doesn't depend on Sledgehammer
blanchet
parents:
37577
diff
changeset

71 
open Metis_Clauses 
38023  72 
open Sledgehammer_Util 
38988  73 
open Sledgehammer_Filter 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
38277
diff
changeset

74 
open Sledgehammer_Translate 
38988  75 
open Sledgehammer_Reconstruct 
37583
9ce2451647d5
factored nonATP specific code from "ATP_Manager" out, so that it can be reused for the LEOII integration
blanchet
parents:
37581
diff
changeset

76 

38023  77 

37583
9ce2451647d5
factored nonATP specific code from "ATP_Manager" out, so that it can be reused for the LEOII integration
blanchet
parents:
37581
diff
changeset

78 
(** The Sledgehammer **) 
9ce2451647d5
factored nonATP specific code from "ATP_Manager" out, so that it can be reused for the LEOII integration
blanchet
parents:
37581
diff
changeset

79 

38102
019a49759829
fix bug in the newly introduced "bound concealing" code
blanchet
parents:
38100
diff
changeset

80 
(* Identifier to distinguish Sledgehammer from other tools using 
019a49759829
fix bug in the newly introduced "bound concealing" code
blanchet
parents:
38100
diff
changeset

81 
"Async_Manager". *) 
37585  82 
val das_Tool = "Sledgehammer" 
83 

84 
fun kill_atps () = Async_Manager.kill_threads das_Tool "ATPs" 

85 
fun running_atps () = Async_Manager.running_threads das_Tool "ATPs" 

86 
val messages = Async_Manager.thread_messages das_Tool "ATP" 

35969  87 

36281
dbbf4d5d584d
pass relevant options from "sledgehammer" to "sledgehammer minimize";
blanchet
parents:
36235
diff
changeset

88 
(** problems, results, provers, etc. **) 
35969  89 

90 
type params = 

38982
820b8221ed48
added "blocking" option to Sledgehammer to run in synchronous mode;
blanchet
parents:
38893
diff
changeset

91 
{blocking: bool, 
820b8221ed48
added "blocking" option to Sledgehammer to run in synchronous mode;
blanchet
parents:
38893
diff
changeset

92 
debug: bool, 
35969  93 
verbose: bool, 
36143
6490319b1703
added "overlord" option (to get easy access to output files for debugging) + systematically use "raw_goal" rather than an inconsistent mixture
blanchet
parents:
36064
diff
changeset

94 
overlord: bool, 
35969  95 
atps: string list, 
96 
full_types: bool, 

36235
61159615a0c5
added "explicit_apply" option to Sledgehammer, to control whether an explicit apply function should be used as much or as little as possible (replaces a previous global variable)
blanchet
parents:
36231
diff
changeset

97 
explicit_apply: bool, 
38745
ad577fd62ee4
reorganize options regarding to the relevance threshold and decay
blanchet
parents:
38744
diff
changeset

98 
relevance_thresholds: real * real, 
38744
2b6333f78a9e
make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents:
38741
diff
changeset

99 
max_relevant: int option, 
35969  100 
isar_proof: bool, 
36924  101 
isar_shrink_factor: int, 
38985
162bbbea4e4d
added "expect" feature of Nitpick to Sledgehammer, for regression testing
blanchet
parents:
38982
diff
changeset

102 
timeout: Time.time, 
162bbbea4e4d
added "expect" feature of Nitpick to Sledgehammer, for regression testing
blanchet
parents:
38982
diff
changeset

103 
expect: string} 
35867  104 

105 
type problem = 

39318  106 
{state: Proof.state, 
38998  107 
goal: thm, 
108 
subgoal: int, 

39366
f58fbb959826
handle relevance filter corner cases more gracefully;
blanchet
parents:
39364
diff
changeset

109 
axioms: (term * ((string * locality) * fol_formula) option) list, 
f58fbb959826
handle relevance filter corner cases more gracefully;
blanchet
parents:
39364
diff
changeset

110 
only: bool} 
35867  111 

112 
type prover_result = 

36370
a4f601daa175
centralized ATPspecific error handling in "atp_wrapper.ML"
blanchet
parents:
36369
diff
changeset

113 
{outcome: failure option, 
35969  114 
message: string, 
37926
e6ff246c0cdb
renamings + only need second component of name pool to reconstruct proofs
blanchet
parents:
37627
diff
changeset

115 
pool: string Symtab.table, 
38752
6628adcae4a7
consider "locality" when assigning weights to facts
blanchet
parents:
38748
diff
changeset

116 
used_thm_names: (string * locality) list, 
35969  117 
atp_run_time_in_msecs: int, 
36369
d2cd0d04b8e6
handle ATP proof delimiters in a cleaner, more extensible fashion
blanchet
parents:
36289
diff
changeset

118 
output: string, 
39452  119 
tstplike_proof: string, 
38818
61cf050f8b2e
improve SPASS hack, when a clause comes from several facts
blanchet
parents:
38752
diff
changeset

120 
axiom_names: (string * locality) list vector, 
38083
c4b57f68ddb3
remove the "extra_clauses" business introduced in 19a5f1c8a844;
blanchet
parents:
38061
diff
changeset

121 
conjecture_shape: int list list} 
35867  122 

38100
e458a0dd3dc1
use "explicit_apply" in the minimizer whenever it might make a difference to prevent freak failures;
blanchet
parents:
38098
diff
changeset

123 
type prover = params > minimize_command > problem > prover_result 
35867  124 

38023  125 
(* configuration attributes *) 
126 

38991  127 
val (dest_dir, dest_dir_setup) = 
39003
c2aebd79981f
run relevance filter in a thread, to avoid blocking
blanchet
parents:
39000
diff
changeset

128 
Attrib.config_string "sledgehammer_dest_dir" (K "") 
38991  129 
(* Empty string means create files in Isabelle's temporary files directory. *) 
38023  130 

131 
val (problem_prefix, problem_prefix_setup) = 

39003
c2aebd79981f
run relevance filter in a thread, to avoid blocking
blanchet
parents:
39000
diff
changeset

132 
Attrib.config_string "sledgehammer_problem_prefix" (K "prob") 
38023  133 

39003
c2aebd79981f
run relevance filter in a thread, to avoid blocking
blanchet
parents:
39000
diff
changeset

134 
val (measure_run_time, measure_run_time_setup) = 
c2aebd79981f
run relevance filter in a thread, to avoid blocking
blanchet
parents:
39000
diff
changeset

135 
Attrib.config_bool "sledgehammer_measure_run_time" (K false) 
28484  136 

38023  137 
fun with_path cleanup after f path = 
138 
Exn.capture f path 

139 
> tap (fn _ => cleanup path) 

140 
> Exn.release 

141 
> tap (after path) 

142 

143 
(* generic TPTPbased provers *) 

144 

39492  145 
(* Important messages are important but not so important that users want to see 
146 
them each time. *) 

39493
cb2208f2c07d
move SPASS's Flotter hack to "Sledgehammer_Reconstruct"
blanchet
parents:
39492
diff
changeset

147 
val important_message_keep_factor = 0.1 
39492  148 

39318  149 
fun prover_fun auto atp_name 
38645  150 
{exec, required_execs, arguments, has_incomplete_mode, proof_delims, 
38997  151 
known_failures, default_max_relevant, explicit_forall, 
152 
use_conjecture_for_hypotheses} 

38455  153 
({debug, verbose, overlord, full_types, explicit_apply, 
38998  154 
max_relevant, isar_proof, isar_shrink_factor, timeout, ...} : params) 
39366
f58fbb959826
handle relevance filter corner cases more gracefully;
blanchet
parents:
39364
diff
changeset

155 
minimize_command ({state, goal, subgoal, axioms, only} : problem) = 
38023  156 
let 
39318  157 
val ctxt = Proof.context_of state 
38998  158 
val (_, hyp_ts, concl_t) = strip_subgoal goal subgoal 
39366
f58fbb959826
handle relevance filter corner cases more gracefully;
blanchet
parents:
39364
diff
changeset

159 
val axioms = axioms > not only 
f58fbb959826
handle relevance filter corner cases more gracefully;
blanchet
parents:
39364
diff
changeset

160 
? take (the_default default_max_relevant max_relevant) 
38023  161 
val the_dest_dir = if overlord then getenv "ISABELLE_HOME_USER" 
38998  162 
else Config.get ctxt dest_dir 
163 
val the_problem_prefix = Config.get ctxt problem_prefix 

39003
c2aebd79981f
run relevance filter in a thread, to avoid blocking
blanchet
parents:
39000
diff
changeset

164 
val problem_file_name = 
c2aebd79981f
run relevance filter in a thread, to avoid blocking
blanchet
parents:
39000
diff
changeset

165 
Path.basic ((if overlord then "prob_" ^ atp_name 
c2aebd79981f
run relevance filter in a thread, to avoid blocking
blanchet
parents:
39000
diff
changeset

166 
else the_problem_prefix ^ serial_string ()) 
c2aebd79981f
run relevance filter in a thread, to avoid blocking
blanchet
parents:
39000
diff
changeset

167 
^ "_" ^ string_of_int subgoal) 
c2aebd79981f
run relevance filter in a thread, to avoid blocking
blanchet
parents:
39000
diff
changeset

168 
val problem_path_name = 
c2aebd79981f
run relevance filter in a thread, to avoid blocking
blanchet
parents:
39000
diff
changeset

169 
if the_dest_dir = "" then 
c2aebd79981f
run relevance filter in a thread, to avoid blocking
blanchet
parents:
39000
diff
changeset

170 
File.tmp_path problem_file_name 
c2aebd79981f
run relevance filter in a thread, to avoid blocking
blanchet
parents:
39000
diff
changeset

171 
else if File.exists (Path.explode the_dest_dir) then 
c2aebd79981f
run relevance filter in a thread, to avoid blocking
blanchet
parents:
39000
diff
changeset

172 
Path.append (Path.explode the_dest_dir) problem_file_name 
c2aebd79981f
run relevance filter in a thread, to avoid blocking
blanchet
parents:
39000
diff
changeset

173 
else 
c2aebd79981f
run relevance filter in a thread, to avoid blocking
blanchet
parents:
39000
diff
changeset

174 
error ("No such directory: " ^ quote the_dest_dir ^ ".") 
c2aebd79981f
run relevance filter in a thread, to avoid blocking
blanchet
parents:
39000
diff
changeset

175 
val measure_run_time = verbose orelse Config.get ctxt measure_run_time 
38092
81a003f7de0d
speed up the minimizer by using the time taken for the first iteration as a timeout for the following iterations, and fix a subtle bug in "string_for_failure"
blanchet
parents:
38091
diff
changeset

176 
val command = Path.explode (getenv (fst exec) ^ "/" ^ snd exec) 
38023  177 
(* write out problem file and call prover *) 
38645  178 
fun command_line complete timeout probfile = 
38023  179 
let 
180 
val core = File.shell_path command ^ " " ^ arguments complete timeout ^ 

181 
" " ^ File.shell_path probfile 

182 
in 

39010  183 
(if measure_run_time then "TIMEFORMAT='%3R'; { time " ^ core ^ " ; }" 
38744
2b6333f78a9e
make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents:
38741
diff
changeset

184 
else "exec " ^ core) ^ " 2>&1" 
38023  185 
end 
186 
fun split_time s = 

187 
let 

188 
val split = String.tokens (fn c => str c = "\n"); 

189 
val (output, t) = s > split > split_last > apfst cat_lines; 

190 
fun as_num f = f >> (fst o read_int); 

191 
val num = as_num (Scan.many1 Symbol.is_ascii_digit); 

192 
val digit = Scan.one Symbol.is_ascii_digit; 

193 
val num3 = as_num (digit ::: digit ::: (digit >> single)); 

194 
val time = num  Scan.$$ "."  num3 >> (fn (a, b) => a * 1000 + b); 

195 
val as_time = the_default 0 o Scan.read Symbol.stopper time o explode; 

196 
in (output, as_time t) end; 

197 
fun run_on probfile = 

38092
81a003f7de0d
speed up the minimizer by using the time taken for the first iteration as a timeout for the following iterations, and fix a subtle bug in "string_for_failure"
blanchet
parents:
38091
diff
changeset

198 
case filter (curry (op =) "" o getenv o fst) (exec :: required_execs) of 
38032  199 
(home_var, _) :: _ => 
38023  200 
error ("The environment variable " ^ quote home_var ^ " is not set.") 
38032  201 
 [] => 
202 
if File.exists command then 

203 
let 

39318  204 
fun run complete timeout = 
38032  205 
let 
38645  206 
val command = command_line complete timeout probfile 
38032  207 
val ((output, msecs), res_code) = 
208 
bash_output command 

209 
>> (if overlord then 

210 
prefix ("% " ^ command ^ "\n% " ^ timestamp () ^ "\n") 

211 
else 

212 
I) 

38744
2b6333f78a9e
make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents:
38741
diff
changeset

213 
>> (if measure_run_time then split_time else rpair 0) 
39452  214 
val (tstplike_proof, outcome) = 
215 
extract_tstplike_proof_and_outcome complete res_code 

216 
proof_delims known_failures output 

217 
in (output, msecs, tstplike_proof, outcome) end 

38032  218 
val readable_names = debug andalso overlord 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
38277
diff
changeset

219 
val (problem, pool, conjecture_offset, axiom_names) = 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
38277
diff
changeset

220 
prepare_problem ctxt readable_names explicit_forall full_types 
39005  221 
explicit_apply hyp_ts concl_t axioms 
39452  222 
val ss = tptp_strings_for_atp_problem use_conjecture_for_hypotheses 
223 
problem 

38631
979a0b37f981
prefer TPTP "conjecture" tag to "hypothesis" on ATPs where this is possible;
blanchet
parents:
38600
diff
changeset

224 
val _ = File.write_list probfile ss 
38032  225 
val conjecture_shape = 
226 
conjecture_offset + 1 upto conjecture_offset + length hyp_ts + 1 

38040
174568533593
fix bug in the SPASS Flotter hack, when a conjecture FOF is translated to several CNF clauses
blanchet
parents:
38039
diff
changeset

227 
> map single 
39318  228 
val run_twice = has_incomplete_mode andalso not auto 
38645  229 
val timer = Timer.startRealTimer () 
38032  230 
val result = 
39318  231 
run false (if run_twice then 
232 
Time.fromMilliseconds 

38645  233 
(2 * Time.toMilliseconds timeout div 3) 
39318  234 
else 
235 
timeout) 

236 
> run_twice 

38645  237 
? (fn (_, msecs0, _, SOME _) => 
39318  238 
run true (Time. (timeout, Timer.checkRealTimer timer)) 
39452  239 
> (fn (output, msecs, tstplike_proof, outcome) => 
240 
(output, msecs0 + msecs, tstplike_proof, outcome)) 

38645  241 
 result => result) 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
38277
diff
changeset

242 
in ((pool, conjecture_shape, axiom_names), result) end 
38032  243 
else 
244 
error ("Bad executable: " ^ Path.implode command ^ ".") 

38023  245 

246 
(* If the problem file has not been exported, remove it; otherwise, export 

247 
the proof file too. *) 

248 
fun cleanup probfile = 

249 
if the_dest_dir = "" then try File.rm probfile else NONE 

250 
fun export probfile (_, (output, _, _, _)) = 

251 
if the_dest_dir = "" then 

252 
() 

253 
else 

254 
File.write (Path.explode (Path.implode probfile ^ "_proof")) output 

38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
38277
diff
changeset

255 
val ((pool, conjecture_shape, axiom_names), 
39452  256 
(output, msecs, tstplike_proof, outcome)) = 
39003
c2aebd79981f
run relevance filter in a thread, to avoid blocking
blanchet
parents:
39000
diff
changeset

257 
with_path cleanup export run_on problem_path_name 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
38277
diff
changeset

258 
val (conjecture_shape, axiom_names) = 
39493
cb2208f2c07d
move SPASS's Flotter hack to "Sledgehammer_Reconstruct"
blanchet
parents:
39492
diff
changeset

259 
repair_conjecture_shape_and_axiom_names output conjecture_shape 
cb2208f2c07d
move SPASS's Flotter hack to "Sledgehammer_Reconstruct"
blanchet
parents:
39492
diff
changeset

260 
axiom_names 
39492  261 
val important_message = 
39493
cb2208f2c07d
move SPASS's Flotter hack to "Sledgehammer_Reconstruct"
blanchet
parents:
39492
diff
changeset

262 
if random () <= important_message_keep_factor then 
39492  263 
extract_important_message output 
264 
else 

265 
"" 

39327  266 
val banner = if auto then "Sledgehammer found a proof" 
267 
else "Try this command" 

38023  268 
val (message, used_thm_names) = 
269 
case outcome of 

270 
NONE => 

271 
proof_text isar_proof 

272 
(pool, debug, isar_shrink_factor, ctxt, conjecture_shape) 

39452  273 
(banner, full_types, minimize_command, tstplike_proof, axiom_names, 
274 
goal, subgoal) 

38744
2b6333f78a9e
make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents:
38741
diff
changeset

275 
>> (fn message => 
2b6333f78a9e
make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents:
38741
diff
changeset

276 
message ^ (if verbose then 
39371  277 
"\nATP real CPU time: " ^ string_of_int msecs ^ 
278 
" ms." 

38744
2b6333f78a9e
make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
blanchet
parents:
38741
diff
changeset

279 
else 
39107
0a62f8a94af3
If Geoff puts some important message in his TPTP problems (e.g., money requests), we should show them to the user
blanchet
parents:
39010
diff
changeset

280 
"") ^ 
0a62f8a94af3
If Geoff puts some important message in his TPTP problems (e.g., money requests), we should show them to the user
blanchet
parents:
39010
diff
changeset

281 
(if important_message <> "" then 
0a62f8a94af3
If Geoff puts some important message in his TPTP problems (e.g., money requests), we should show them to the user
blanchet
parents:
39010
diff
changeset

282 
"\n\nImportant message from Dr. Geoff Sutcliffe:\n" ^ 
0a62f8a94af3
If Geoff puts some important message in his TPTP problems (e.g., money requests), we should show them to the user
blanchet
parents:
39010
diff
changeset

283 
important_message 
0a62f8a94af3
If Geoff puts some important message in his TPTP problems (e.g., money requests), we should show them to the user
blanchet
parents:
39010
diff
changeset

284 
else 
0a62f8a94af3
If Geoff puts some important message in his TPTP problems (e.g., money requests), we should show them to the user
blanchet
parents:
39010
diff
changeset

285 
"")) 
38597
db482afec7f0
no spurious trailing "\n" at the end of Sledgehammer's output
blanchet
parents:
38590
diff
changeset

286 
 SOME failure => (string_for_failure failure, []) 
38023  287 
in 
288 
{outcome = outcome, message = message, pool = pool, 

289 
used_thm_names = used_thm_names, atp_run_time_in_msecs = msecs, 

39452  290 
output = output, tstplike_proof = tstplike_proof, 
291 
axiom_names = axiom_names, conjecture_shape = conjecture_shape} 

38023  292 
end 
293 

39318  294 
fun get_prover_fun thy name = prover_fun false name (get_prover thy name) 
38023  295 

39453
1740a2d6bef9
use the same TSTP/Vampire/SPASS parser for oneliners as for Isar proofs
blanchet
parents:
39452
diff
changeset

296 
fun run_prover (params as {blocking, debug, verbose, max_relevant, timeout, 
1740a2d6bef9
use the same TSTP/Vampire/SPASS parser for oneliners as for Isar proofs
blanchet
parents:
39452
diff
changeset

297 
expect, ...}) 
39338  298 
auto i n minimize_command (problem as {state, goal, axioms, ...}) 
39110
a74bd9bfa880
show the number of facts for each prover in "verbose" mode
blanchet
parents:
39108
diff
changeset

299 
(prover as {default_max_relevant, ...}, atp_name) = 
36379
20ef039bccff
make "ATP_Manager.get_prover" a total function, since we always want to show the same error text
blanchet
parents:
36373
diff
changeset

300 
let 
39318  301 
val ctxt = Proof.context_of state 
37584  302 
val birth_time = Time.now () 
303 
val death_time = Time.+ (birth_time, timeout) 

39110
a74bd9bfa880
show the number of facts for each prover in "verbose" mode
blanchet
parents:
39108
diff
changeset

304 
val max_relevant = the_default default_max_relevant max_relevant 
a74bd9bfa880
show the number of facts for each prover in "verbose" mode
blanchet
parents:
39108
diff
changeset

305 
val num_axioms = Int.min (length axioms, max_relevant) 
36379
20ef039bccff
make "ATP_Manager.get_prover" a total function, since we always want to show the same error text
blanchet
parents:
36373
diff
changeset

306 
val desc = 
39110
a74bd9bfa880
show the number of facts for each prover in "verbose" mode
blanchet
parents:
39108
diff
changeset

307 
"ATP " ^ quote atp_name ^ 
a74bd9bfa880
show the number of facts for each prover in "verbose" mode
blanchet
parents:
39108
diff
changeset

308 
(if verbose then 
a74bd9bfa880
show the number of facts for each prover in "verbose" mode
blanchet
parents:
39108
diff
changeset

309 
" with " ^ string_of_int num_axioms ^ " fact" ^ plural_s num_axioms 
a74bd9bfa880
show the number of facts for each prover in "verbose" mode
blanchet
parents:
39108
diff
changeset

310 
else 
a74bd9bfa880
show the number of facts for each prover in "verbose" mode
blanchet
parents:
39108
diff
changeset

311 
"") ^ 
a74bd9bfa880
show the number of facts for each prover in "verbose" mode
blanchet
parents:
39108
diff
changeset

312 
" on " ^ (if n = 1 then "goal" else "subgoal " ^ string_of_int i) ^ ":" ^ 
38985
162bbbea4e4d
added "expect" feature of Nitpick to Sledgehammer, for regression testing
blanchet
parents:
38982
diff
changeset

313 
(if blocking then 
162bbbea4e4d
added "expect" feature of Nitpick to Sledgehammer, for regression testing
blanchet
parents:
38982
diff
changeset

314 
"" 
162bbbea4e4d
added "expect" feature of Nitpick to Sledgehammer, for regression testing
blanchet
parents:
38982
diff
changeset

315 
else 
162bbbea4e4d
added "expect" feature of Nitpick to Sledgehammer, for regression testing
blanchet
parents:
38982
diff
changeset

316 
"\n" ^ Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i))) 
39318  317 
fun go () = 
38982
820b8221ed48
added "blocking" option to Sledgehammer to run in synchronous mode;
blanchet
parents:
38893
diff
changeset

318 
let 
39453
1740a2d6bef9
use the same TSTP/Vampire/SPASS parser for oneliners as for Isar proofs
blanchet
parents:
39452
diff
changeset

319 
fun really_go () = 
39318  320 
prover_fun auto atp_name prover params (minimize_command atp_name) 
321 
problem 

38985
162bbbea4e4d
added "expect" feature of Nitpick to Sledgehammer, for regression testing
blanchet
parents:
38982
diff
changeset

322 
> (fn {outcome, message, ...} => 
162bbbea4e4d
added "expect" feature of Nitpick to Sledgehammer, for regression testing
blanchet
parents:
38982
diff
changeset

323 
(if is_some outcome then "none" else "some", message)) 
39453
1740a2d6bef9
use the same TSTP/Vampire/SPASS parser for oneliners as for Isar proofs
blanchet
parents:
39452
diff
changeset

324 
val (outcome_code, message) = 
1740a2d6bef9
use the same TSTP/Vampire/SPASS parser for oneliners as for Isar proofs
blanchet
parents:
39452
diff
changeset

325 
if debug then 
1740a2d6bef9
use the same TSTP/Vampire/SPASS parser for oneliners as for Isar proofs
blanchet
parents:
39452
diff
changeset

326 
really_go () 
1740a2d6bef9
use the same TSTP/Vampire/SPASS parser for oneliners as for Isar proofs
blanchet
parents:
39452
diff
changeset

327 
else 
1740a2d6bef9
use the same TSTP/Vampire/SPASS parser for oneliners as for Isar proofs
blanchet
parents:
39452
diff
changeset

328 
(really_go () 
1740a2d6bef9
use the same TSTP/Vampire/SPASS parser for oneliners as for Isar proofs
blanchet
parents:
39452
diff
changeset

329 
handle ERROR message => ("unknown", "Error: " ^ message ^ "\n") 
1740a2d6bef9
use the same TSTP/Vampire/SPASS parser for oneliners as for Isar proofs
blanchet
parents:
39452
diff
changeset

330 
 exn => ("unknown", "Internal error:\n" ^ 
1740a2d6bef9
use the same TSTP/Vampire/SPASS parser for oneliners as for Isar proofs
blanchet
parents:
39452
diff
changeset

331 
ML_Compiler.exn_message exn ^ "\n")) 
39318  332 
val _ = 
333 
if expect = "" orelse outcome_code = expect then 

334 
() 

335 
else if blocking then 

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

337 
else 

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

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

340 
in 

341 
if auto then 

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

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

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

39327  345 
(Pretty.str message)])) 
38982
820b8221ed48
added "blocking" option to Sledgehammer to run in synchronous mode;
blanchet
parents:
38893
diff
changeset

346 
end 
39318  347 
else if blocking then 
348 
let val (success, message) = TimeLimit.timeLimit timeout go () in 

39370
f8292d3020db
use same hack as in "Async_Manager" to work around Proof General bug
blanchet
parents:
39366
diff
changeset

349 
List.app priority 
f8292d3020db
use same hack as in "Async_Manager" to work around Proof General bug
blanchet
parents:
39366
diff
changeset

350 
(Async_Manager.break_into_chunks [desc ^ "\n" ^ message]); 
f8292d3020db
use same hack as in "Async_Manager" to work around Proof General bug
blanchet
parents:
39366
diff
changeset

351 
(success, state) 
39318  352 
end 
353 
else 

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

355 
(false, state)) 

37584  356 
end 
28582  357 

39318  358 
val auto_max_relevant_divisor = 2 
359 

39373  360 
fun run_sledgehammer (params as {blocking, atps, full_types, 
38998  361 
relevance_thresholds, max_relevant, ...}) 
39366
f58fbb959826
handle relevance filter corner cases more gracefully;
blanchet
parents:
39364
diff
changeset

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

363 
state = 
39318  364 
if null atps then 
365 
error "No ATP is set." 

366 
else case subgoal_count state of 

367 
0 => (priority "No subgoal!"; (false, state)) 

368 
 n => 

369 
let 

39364  370 
val _ = Proof.assert_backward state 
39318  371 
val thy = Proof.theory_of state 
372 
val _ = () > not blocking ? kill_atps 

373 
val _ = if auto then () else priority "Sledgehammering..." 

374 
val provers = map (`(get_prover thy)) atps 

375 
fun go () = 

376 
let 

377 
val {context = ctxt, facts = chained_ths, goal} = Proof.goal state 

378 
val (_, hyp_ts, concl_t) = strip_subgoal goal i 

379 
val max_max_relevant = 

380 
case max_relevant of 

381 
SOME n => n 

382 
 NONE => 

383 
0 > fold (Integer.max o #default_max_relevant o fst) provers 

384 
> auto ? (fn n => n div auto_max_relevant_divisor) 

385 
val axioms = 

386 
relevant_facts ctxt full_types relevance_thresholds 

387 
max_max_relevant relevance_override chained_ths 

388 
hyp_ts concl_t 

389 
val problem = 

390 
{state = state, goal = goal, subgoal = i, 

39366
f58fbb959826
handle relevance filter corner cases more gracefully;
blanchet
parents:
39364
diff
changeset

391 
axioms = map (prepare_axiom ctxt) axioms, only = only} 
39338  392 
val run_prover = run_prover params auto i n minimize_command problem 
39318  393 
in 
394 
if auto then 

395 
fold (fn prover => fn (true, state) => (true, state) 

396 
 (false, _) => run_prover prover) 

397 
provers (false, state) 

398 
else 

399 
(if blocking then Par_List.map else map) run_prover provers 

400 
> exists fst > rpair state 

401 
end 

402 
in if blocking then go () else Future.fork (tap go) > K (false, state) end 

38044  403 

38023  404 
val setup = 
405 
dest_dir_setup 

406 
#> problem_prefix_setup 

39003
c2aebd79981f
run relevance filter in a thread, to avoid blocking
blanchet
parents:
39000
diff
changeset

407 
#> measure_run_time_setup 
38023  408 

28582  409 
end; 