author  blanchet 
Thu, 21 Oct 2010 14:55:09 +0200  
changeset 40059  6ad9081665db 
parent 39494  bf7dd4902321 
child 40060  5ef6747aa619 
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, 
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset

22 
provers: string list, 
35969  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 

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

32 
type atp_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 

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

39 
type atp_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 

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

50 
type atp = params > minimize_command > atp_problem > atp_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 
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset

55 
val available_provers : theory > unit 
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset

56 
val kill_provers : unit > unit 
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset

57 
val running_provers : unit > unit 
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset

58 
val messages : int option > unit 
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset

59 
val get_atp_fun : theory > string > atp 
38044  60 
val run_sledgehammer : 
39318  61 
params > bool > int > relevance_override > (string > minimize_command) 
62 
> Proof.state > bool * Proof.state 

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

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

65 

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

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

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

68 

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

70 
open ATP_Proof 
38028  71 
open ATP_Systems 
39494
bf7dd4902321
rename "Metis_Clauses" to "Metis_Translate" for consistency with "Sledgehammer_Translate"
blanchet
parents:
39493
diff
changeset

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

75 
open Sledgehammer_Translate 
38988  76 
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

77 

38023  78 

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

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

80 

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

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

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

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

85 
fun available_provers thy = 
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset

86 
priority ("Available provers: " ^ 
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset

87 
commas (sort_strings (available_atps thy)) ^ ".") 
35969  88 

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

89 
fun kill_provers () = Async_Manager.kill_threads das_Tool "provers" 
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset

90 
fun running_provers () = Async_Manager.running_threads das_Tool "provers" 
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset

91 
val messages = Async_Manager.thread_messages das_Tool "prover" 
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset

92 

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

93 
(** problems, results, ATPs, etc. **) 
35969  94 

95 
type params = 

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

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

97 
debug: bool, 
35969  98 
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

99 
overlord: bool, 
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset

100 
provers: string list, 
35969  101 
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

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

103 
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

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

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

108 
expect: string} 
35867  109 

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

110 
type atp_problem = 
39318  111 
{state: Proof.state, 
38998  112 
goal: thm, 
113 
subgoal: int, 

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

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

115 
only: bool} 
35867  116 

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

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

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

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

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

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

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

126 
conjecture_shape: int list list} 
35867  127 

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

128 
type atp = params > minimize_command > atp_problem > atp_result 
35867  129 

38023  130 
(* configuration attributes *) 
131 

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

133 
Attrib.config_string "sledgehammer_dest_dir" (K "") 
38991  134 
(* Empty string means create files in Isabelle's temporary files directory. *) 
38023  135 

136 
val (problem_prefix, problem_prefix_setup) = 

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

137 
Attrib.config_string "sledgehammer_problem_prefix" (K "prob") 
38023  138 

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

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

140 
Attrib.config_bool "sledgehammer_measure_run_time" (K false) 
28484  141 

38023  142 
fun with_path cleanup after f path = 
143 
Exn.capture f path 

144 
> tap (fn _ => cleanup path) 

145 
> Exn.release 

146 
> tap (after path) 

147 

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

148 
(* generic TPTPbased ATPs *) 
38023  149 

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

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

152 
val important_message_keep_factor = 0.1 
39492  153 

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

154 
fun atp_fun auto atp_name 
38645  155 
{exec, required_execs, arguments, has_incomplete_mode, proof_delims, 
38997  156 
known_failures, default_max_relevant, explicit_forall, 
157 
use_conjecture_for_hypotheses} 

38455  158 
({debug, verbose, overlord, full_types, explicit_apply, 
38998  159 
max_relevant, isar_proof, isar_shrink_factor, timeout, ...} : params) 
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset

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

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

165 
? take (the_default default_max_relevant max_relevant) 
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset

166 
val dest_dir = if overlord then getenv "ISABELLE_HOME_USER" 
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset

167 
else Config.get ctxt dest_dir 
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset

168 
val problem_prefix = Config.get ctxt problem_prefix 
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset

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

170 
Path.basic ((if overlord then "prob_" ^ atp_name 
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset

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

172 
^ "_" ^ string_of_int subgoal) 
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset

173 
val atp_problem_path_name = 
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset

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

175 
File.tmp_path atp_problem_file_name 
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset

176 
else if File.exists (Path.explode dest_dir) then 
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset

177 
Path.append (Path.explode dest_dir) atp_problem_file_name 
39003
c2aebd79981f
run relevance filter in a thread, to avoid blocking
blanchet
parents:
39000
diff
changeset

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

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

180 
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

181 
val command = Path.explode (getenv (fst exec) ^ "/" ^ snd exec) 
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset

182 
(* write out problem file and call ATP *) 
38645  183 
fun command_line complete timeout probfile = 
38023  184 
let 
185 
val core = File.shell_path command ^ " " ^ arguments complete timeout ^ 

186 
" " ^ File.shell_path probfile 

187 
in 

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

189 
else "exec " ^ core) ^ " 2>&1" 
38023  190 
end 
191 
fun split_time s = 

192 
let 

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

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

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

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

197 
val digit = Scan.one Symbol.is_ascii_digit; 

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

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

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

201 
in (output, as_time t) end; 

202 
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

203 
case filter (curry (op =) "" o getenv o fst) (exec :: required_execs) of 
38032  204 
(home_var, _) :: _ => 
38023  205 
error ("The environment variable " ^ quote home_var ^ " is not set.") 
38032  206 
 [] => 
207 
if File.exists command then 

208 
let 

39318  209 
fun run complete timeout = 
38032  210 
let 
38645  211 
val command = command_line complete timeout probfile 
38032  212 
val ((output, msecs), res_code) = 
213 
bash_output command 

214 
>> (if overlord then 

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

216 
else 

217 
I) 

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

218 
>> (if measure_run_time then split_time else rpair 0) 
39452  219 
val (tstplike_proof, outcome) = 
220 
extract_tstplike_proof_and_outcome complete res_code 

221 
proof_delims known_failures output 

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

38032  223 
val readable_names = debug andalso overlord 
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset

224 
val (atp_problem, pool, conjecture_offset, axiom_names) = 
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset

225 
prepare_atp_problem ctxt readable_names explicit_forall full_types 
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset

226 
explicit_apply hyp_ts concl_t axioms 
39452  227 
val ss = tptp_strings_for_atp_problem use_conjecture_for_hypotheses 
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset

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

229 
val _ = File.write_list probfile ss 
38032  230 
val conjecture_shape = 
231 
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

232 
> map single 
39318  233 
val run_twice = has_incomplete_mode andalso not auto 
38645  234 
val timer = Timer.startRealTimer () 
38032  235 
val result = 
39318  236 
run false (if run_twice then 
237 
Time.fromMilliseconds 

38645  238 
(2 * Time.toMilliseconds timeout div 3) 
39318  239 
else 
240 
timeout) 

241 
> run_twice 

38645  242 
? (fn (_, msecs0, _, SOME _) => 
39318  243 
run true (Time. (timeout, Timer.checkRealTimer timer)) 
39452  244 
> (fn (output, msecs, tstplike_proof, outcome) => 
245 
(output, msecs0 + msecs, tstplike_proof, outcome)) 

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

247 
in ((pool, conjecture_shape, axiom_names), result) end 
38032  248 
else 
249 
error ("Bad executable: " ^ Path.implode command ^ ".") 

38023  250 

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

252 
the proof file too. *) 

253 
fun cleanup probfile = 

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

254 
if dest_dir = "" then try File.rm probfile else NONE 
38023  255 
fun export probfile (_, (output, _, _, _)) = 
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset

256 
if dest_dir = "" then 
38023  257 
() 
258 
else 

259 
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

260 
val ((pool, conjecture_shape, axiom_names), 
39452  261 
(output, msecs, tstplike_proof, outcome)) = 
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset

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

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

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

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

267 
if random () <= important_message_keep_factor then 
39492  268 
extract_important_message output 
269 
else 

270 
"" 

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

38023  273 
val (message, used_thm_names) = 
274 
case outcome of 

275 
NONE => 

276 
proof_text isar_proof 

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

39452  278 
(banner, full_types, minimize_command, tstplike_proof, axiom_names, 
279 
goal, subgoal) 

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

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

281 
message ^ (if verbose then 
39371  282 
"\nATP real CPU time: " ^ string_of_int msecs ^ 
283 
" ms." 

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

284 
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

285 
"") ^ 
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

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

287 
"\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

288 
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

289 
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

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

291 
 SOME failure => (string_for_failure failure, []) 
38023  292 
in 
293 
{outcome = outcome, message = message, pool = pool, 

294 
used_thm_names = used_thm_names, atp_run_time_in_msecs = msecs, 

39452  295 
output = output, tstplike_proof = tstplike_proof, 
296 
axiom_names = axiom_names, conjecture_shape = conjecture_shape} 

38023  297 
end 
298 

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

299 
fun get_atp_fun thy name = atp_fun false name (get_atp thy name) 
38023  300 

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

301 
fun run_atp (params as {blocking, debug, verbose, max_relevant, timeout, expect, 
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset

302 
...}) 
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset

303 
auto i n minimize_command 
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset

304 
(atp_problem as {state, goal, axioms, ...}) 
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset

305 
(atp 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

306 
let 
39318  307 
val ctxt = Proof.context_of state 
37584  308 
val birth_time = Time.now () 
309 
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

310 
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

311 
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

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

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

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

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

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

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

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

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

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

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

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

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

325 
fun really_go () = 
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset

326 
atp_fun auto atp_name atp params (minimize_command atp_name) 
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset

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

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

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

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

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

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

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

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

335 
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

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

337 
ML_Compiler.exn_message exn ^ "\n")) 
39318  338 
val _ = 
339 
if expect = "" orelse outcome_code = expect then 

340 
() 

341 
else if blocking then 

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

343 
else 

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

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

346 
in 

347 
if auto then 

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

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

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

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

352 
end 
39318  353 
else if blocking then 
354 
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

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

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

357 
(success, state) 
39318  358 
end 
359 
else 

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

361 
(false, state)) 

37584  362 
end 
28582  363 

39318  364 
val auto_max_relevant_divisor = 2 
365 

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

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

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

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

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

371 
error "No prover is set." 
39318  372 
else case subgoal_count state of 
373 
0 => (priority "No subgoal!"; (false, state)) 

374 
 n => 

375 
let 

39364  376 
val _ = Proof.assert_backward state 
39318  377 
val thy = Proof.theory_of state 
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset

378 
val _ = () > not blocking ? kill_provers 
39318  379 
val _ = if auto then () else priority "Sledgehammering..." 
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset

380 
val atps = map (`(get_atp thy)) provers 
39318  381 
fun go () = 
382 
let 

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

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

385 
val max_max_relevant = 

386 
case max_relevant of 

387 
SOME n => n 

388 
 NONE => 

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

389 
0 > fold (Integer.max o #default_max_relevant o fst) atps 
39318  390 
> auto ? (fn n => n div auto_max_relevant_divisor) 
391 
val axioms = 

392 
relevant_facts ctxt full_types relevance_thresholds 

393 
max_max_relevant relevance_override chained_ths 

394 
hyp_ts concl_t 

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

395 
val atp_problem = 
39318  396 
{state = state, goal = goal, subgoal = i, 
39366
f58fbb959826
handle relevance filter corner cases more gracefully;
blanchet
parents:
39364
diff
changeset

397 
axioms = map (prepare_axiom ctxt) axioms, only = only} 
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset

398 
val run_atp = run_atp params auto i n minimize_command atp_problem 
39318  399 
in 
400 
if auto then 

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

401 
fold (fn atp => fn (true, state) => (true, state) 
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset

402 
 (false, _) => run_atp atp) 
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset

403 
atps (false, state) 
39318  404 
else 
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset

405 
(if blocking then Par_List.map else map) run_atp atps 
39318  406 
> exists fst > rpair state 
407 
end 

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

38044  409 

38023  410 
val setup = 
411 
dest_dir_setup 

412 
#> problem_prefix_setup 

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

413 
#> measure_run_time_setup 
38023  414 

28582  415 
end; 