author  blanchet 
Wed, 21 Apr 2010 12:22:04 +0200  
changeset 36265  41c9e755e552 
parent 36264  3c2490917710 
child 36281  dbbf4d5d584d 
permissions  rwrr 
32327
0971cc0b6a57
src/HOL/Tools/ATP_Manager as separate component, with (almost) everything in one place;
wenzelm
parents:
32257
diff
changeset

1 
(* Title: HOL/Tools/ATP_Manager/atp_wrapper.ML 
28592  2 
Author: Fabian Immler, TU Muenchen 
3 

4 
Wrapper functions for external ATPs. 

5 
*) 

6 

7 
signature ATP_WRAPPER = 

8 
sig 

35867  9 
type prover = ATP_Manager.prover 
32864
a226f29d4bdc
reorganized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
32740
diff
changeset

10 

35867  11 
(* hooks for problem files *) 
12 
val destdir : string Config.T 

13 
val problem_prefix : string Config.T 

14 
val measure_runtime : bool Config.T 

32864
a226f29d4bdc
reorganized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
32740
diff
changeset

15 

35867  16 
val refresh_systems_on_tptp : unit > unit 
17 
val setup : theory > theory 

28592  18 
end; 
19 

35865  20 
structure ATP_Wrapper : ATP_WRAPPER = 
28592  21 
struct 
28596
fcd463a6b6de
tuned interfaces  plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset

22 

36187  23 
open Sledgehammer_Util 
35969  24 
open Sledgehammer_Fact_Preprocessor 
35865  25 
open Sledgehammer_HOL_Clause 
26 
open Sledgehammer_Fact_Filter 

27 
open Sledgehammer_Proof_Reconstruct 

35867  28 
open ATP_Manager 
35826  29 

28596
fcd463a6b6de
tuned interfaces  plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset

30 
(** generic ATP wrapper **) 
fcd463a6b6de
tuned interfaces  plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset

31 

32944
ecc0705174c2
clarified File.platform_path vs. File.shell_path;
wenzelm
parents:
32942
diff
changeset

32 
(* external problem files *) 
32864
a226f29d4bdc
reorganized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
32740
diff
changeset

33 

36001  34 
val (destdir, destdir_setup) = Attrib.config_string "atp_destdir" (K ""); 
32864
a226f29d4bdc
reorganized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
32740
diff
changeset

35 
(*Empty string means create files in Isabelle's temporary files directory.*) 
a226f29d4bdc
reorganized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
32740
diff
changeset

36 

a226f29d4bdc
reorganized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
32740
diff
changeset

37 
val (problem_prefix, problem_prefix_setup) = 
36001  38 
Attrib.config_string "atp_problem_prefix" (K "prob"); 
32864
a226f29d4bdc
reorganized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
32740
diff
changeset

39 

33247  40 
val (measure_runtime, measure_runtime_setup) = 
36001  41 
Attrib.config_bool "atp_measure_runtime" (K false); 
33247  42 

32864
a226f29d4bdc
reorganized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
32740
diff
changeset

43 

35867  44 
(* prover configuration *) 
32864
a226f29d4bdc
reorganized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
32740
diff
changeset

45 

32941
72d48e333b77
eliminated extraneous wrapping of public records;
wenzelm
parents:
32936
diff
changeset

46 
type prover_config = 
72d48e333b77
eliminated extraneous wrapping of public records;
wenzelm
parents:
32936
diff
changeset

47 
{command: Path.T, 
35969  48 
arguments: Time.time > string, 
36265
41c9e755e552
distinguish between the different ATP errors in the user interface;
blanchet
parents:
36264
diff
changeset

49 
known_failures: (string list * string) list, 
32864
a226f29d4bdc
reorganized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
32740
diff
changeset

50 
max_new_clauses: int, 
36220
f3655a3ae1ab
rename Sledgehammer "theory_const" option to "theory_relevant", now that I understand better what it does
blanchet
parents:
36219
diff
changeset

51 
prefers_theory_relevant: bool, 
35969  52 
supports_isar_proofs: bool}; 
28596
fcd463a6b6de
tuned interfaces  plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset

53 

fcd463a6b6de
tuned interfaces  plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset

54 

fcd463a6b6de
tuned interfaces  plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset

55 
(* basic template *) 
fcd463a6b6de
tuned interfaces  plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset

56 

32458
de6834b20e9e
sledgehammer's temporary files are removed properly (even in case of an exception occurs)
boehmes
parents:
32451
diff
changeset

57 
fun with_path cleanup after f path = 
de6834b20e9e
sledgehammer's temporary files are removed properly (even in case of an exception occurs)
boehmes
parents:
32451
diff
changeset

58 
Exn.capture f path 
de6834b20e9e
sledgehammer's temporary files are removed properly (even in case of an exception occurs)
boehmes
parents:
32451
diff
changeset

59 
> tap (fn _ => cleanup path) 
de6834b20e9e
sledgehammer's temporary files are removed properly (even in case of an exception occurs)
boehmes
parents:
32451
diff
changeset

60 
> Exn.release 
32941
72d48e333b77
eliminated extraneous wrapping of public records;
wenzelm
parents:
32936
diff
changeset

61 
> tap (after path); 
32458
de6834b20e9e
sledgehammer's temporary files are removed properly (even in case of an exception occurs)
boehmes
parents:
32451
diff
changeset

62 

36265
41c9e755e552
distinguish between the different ATP errors in the user interface;
blanchet
parents:
36264
diff
changeset

63 
fun find_known_failure known_failures proof = 
41c9e755e552
distinguish between the different ATP errors in the user interface;
blanchet
parents:
36264
diff
changeset

64 
case map_filter (fn (patterns, message) => 
41c9e755e552
distinguish between the different ATP errors in the user interface;
blanchet
parents:
36264
diff
changeset

65 
if exists (fn pattern => String.isSubstring pattern proof) 
41c9e755e552
distinguish between the different ATP errors in the user interface;
blanchet
parents:
36264
diff
changeset

66 
patterns then 
41c9e755e552
distinguish between the different ATP errors in the user interface;
blanchet
parents:
36264
diff
changeset

67 
SOME message 
41c9e755e552
distinguish between the different ATP errors in the user interface;
blanchet
parents:
36264
diff
changeset

68 
else 
41c9e755e552
distinguish between the different ATP errors in the user interface;
blanchet
parents:
36264
diff
changeset

69 
NONE) known_failures of 
41c9e755e552
distinguish between the different ATP errors in the user interface;
blanchet
parents:
36264
diff
changeset

70 
[] => if is_proof_well_formed proof then "" 
41c9e755e552
distinguish between the different ATP errors in the user interface;
blanchet
parents:
36264
diff
changeset

71 
else "Error: The ATP output is illformed." 
41c9e755e552
distinguish between the different ATP errors in the user interface;
blanchet
parents:
36264
diff
changeset

72 
 (message :: _) => message 
35865  73 

36265
41c9e755e552
distinguish between the different ATP errors in the user interface;
blanchet
parents:
36264
diff
changeset

74 
fun generic_prover overlord get_facts prepare write_file cmd args known_failures 
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

75 
proof_text name ({debug, full_types, explicit_apply, ...} : params) 
35969  76 
({subgoal, goal, relevance_override, axiom_clauses, filtered_clauses} 
77 
: problem) = 

28596
fcd463a6b6de
tuned interfaces  plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset

78 
let 
31750  79 
(* get clauses and prepare them for writing *) 
32942
b6711ec9de26
misc tuning and recovery of Isabelle coding style;
wenzelm
parents:
32941
diff
changeset

80 
val (ctxt, (chain_ths, th)) = goal; 
b6711ec9de26
misc tuning and recovery of Isabelle coding style;
wenzelm
parents:
32941
diff
changeset

81 
val thy = ProofContext.theory_of ctxt; 
35865  82 
val chain_ths = map (Thm.put_name_hint chained_hint) chain_ths; 
35969  83 
val goal_cls = #1 (neg_conjecture_clauses ctxt th subgoal); 
31752
19a5f1c8a844
use results of relevancefilter to determine additional clauses;
immler@in.tum.de
parents:
31751
diff
changeset

84 
val the_filtered_clauses = 
32942
b6711ec9de26
misc tuning and recovery of Isabelle coding style;
wenzelm
parents:
32941
diff
changeset

85 
(case filtered_clauses of 
35969  86 
NONE => get_facts relevance_override goal goal_cls 
32942
b6711ec9de26
misc tuning and recovery of Isabelle coding style;
wenzelm
parents:
32941
diff
changeset

87 
 SOME fcls => fcls); 
31409
d8537ba165b5
split preparing clauses and writing problemfile;
immler@in.tum.de
parents:
31368
diff
changeset

88 
val the_axiom_clauses = 
32942
b6711ec9de26
misc tuning and recovery of Isabelle coding style;
wenzelm
parents:
32941
diff
changeset

89 
(case axiom_clauses of 
b6711ec9de26
misc tuning and recovery of Isabelle coding style;
wenzelm
parents:
32941
diff
changeset

90 
NONE => the_filtered_clauses 
b6711ec9de26
misc tuning and recovery of Isabelle coding style;
wenzelm
parents:
32941
diff
changeset

91 
 SOME axcls => axcls); 
35969  92 
val (internal_thm_names, clauses) = 
32942
b6711ec9de26
misc tuning and recovery of Isabelle coding style;
wenzelm
parents:
32941
diff
changeset

93 
prepare goal_cls chain_ths the_axiom_clauses the_filtered_clauses thy; 
31750  94 

32864
a226f29d4bdc
reorganized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
32740
diff
changeset

95 
(* path to unique problem file *) 
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:
36142
diff
changeset

96 
val destdir' = if overlord then getenv "ISABELLE_HOME_USER" 
6490319b1703
added "overlord" option (to get easy access to output files for debugging) + systematically use "raw_goal" rather than an inconsistent mixture
blanchet
parents:
36142
diff
changeset

97 
else Config.get ctxt destdir; 
32942
b6711ec9de26
misc tuning and recovery of Isabelle coding style;
wenzelm
parents:
32941
diff
changeset

98 
val problem_prefix' = Config.get ctxt problem_prefix; 
32864
a226f29d4bdc
reorganized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
32740
diff
changeset

99 
fun prob_pathname nr = 
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:
36142
diff
changeset

100 
let 
6490319b1703
added "overlord" option (to get easy access to output files for debugging) + systematically use "raw_goal" rather than an inconsistent mixture
blanchet
parents:
36142
diff
changeset

101 
val probfile = 
6490319b1703
added "overlord" option (to get easy access to output files for debugging) + systematically use "raw_goal" rather than an inconsistent mixture
blanchet
parents:
36142
diff
changeset

102 
Path.basic (problem_prefix' ^ 
6490319b1703
added "overlord" option (to get easy access to output files for debugging) + systematically use "raw_goal" rather than an inconsistent mixture
blanchet
parents:
36142
diff
changeset

103 
(if overlord then "_" ^ name else serial_string ()) 
6490319b1703
added "overlord" option (to get easy access to output files for debugging) + systematically use "raw_goal" rather than an inconsistent mixture
blanchet
parents:
36142
diff
changeset

104 
^ "_" ^ string_of_int nr) 
32942
b6711ec9de26
misc tuning and recovery of Isabelle coding style;
wenzelm
parents:
32941
diff
changeset

105 
in 
b6711ec9de26
misc tuning and recovery of Isabelle coding style;
wenzelm
parents:
32941
diff
changeset

106 
if destdir' = "" then File.tmp_path probfile 
35570
0e30eef52d85
basic simplification of external_prover signature;
wenzelm
parents:
35010
diff
changeset

107 
else if File.exists (Path.explode destdir') 
0e30eef52d85
basic simplification of external_prover signature;
wenzelm
parents:
35010
diff
changeset

108 
then Path.append (Path.explode destdir') probfile 
36169
27b1cc58715e
store nonmangled names along with mangled type names in Sledgehammer for debugging purposes
blanchet
parents:
36167
diff
changeset

109 
else error ("No such directory: " ^ destdir' ^ ".") 
32942
b6711ec9de26
misc tuning and recovery of Isabelle coding style;
wenzelm
parents:
32941
diff
changeset

110 
end; 
32864
a226f29d4bdc
reorganized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
32740
diff
changeset

111 

31750  112 
(* write out problem file and call prover *) 
33247  113 
fun cmd_line probfile = 
36265
41c9e755e552
distinguish between the different ATP errors in the user interface;
blanchet
parents:
36264
diff
changeset

114 
if Config.get ctxt measure_runtime then 
33247  115 
"TIMEFORMAT='%3U'; { time " ^ space_implode " " [File.shell_path cmd, 
36265
41c9e755e552
distinguish between the different ATP errors in the user interface;
blanchet
parents:
36264
diff
changeset

116 
args, File.shell_path probfile] ^ " ; } 2>&1" 
33247  117 
else 
118 
space_implode " " ["exec", File.shell_path cmd, args, 

36265
41c9e755e552
distinguish between the different ATP errors in the user interface;
blanchet
parents:
36264
diff
changeset

119 
File.shell_path probfile, "2>&1"]; 
32510  120 
fun split_time s = 
121 
let 

32942
b6711ec9de26
misc tuning and recovery of Isabelle coding style;
wenzelm
parents:
32941
diff
changeset

122 
val split = String.tokens (fn c => str c = "\n"); 
b6711ec9de26
misc tuning and recovery of Isabelle coding style;
wenzelm
parents:
32941
diff
changeset

123 
val (proof, t) = s > split > split_last > apfst cat_lines; 
b6711ec9de26
misc tuning and recovery of Isabelle coding style;
wenzelm
parents:
32941
diff
changeset

124 
fun as_num f = f >> (fst o read_int); 
b6711ec9de26
misc tuning and recovery of Isabelle coding style;
wenzelm
parents:
32941
diff
changeset

125 
val num = as_num (Scan.many1 Symbol.is_ascii_digit); 
b6711ec9de26
misc tuning and recovery of Isabelle coding style;
wenzelm
parents:
32941
diff
changeset

126 
val digit = Scan.one Symbol.is_ascii_digit; 
b6711ec9de26
misc tuning and recovery of Isabelle coding style;
wenzelm
parents:
32941
diff
changeset

127 
val num3 = as_num (digit ::: digit ::: (digit >> single)); 
b6711ec9de26
misc tuning and recovery of Isabelle coding style;
wenzelm
parents:
32941
diff
changeset

128 
val time = num  Scan.$$ "."  num3 >> (fn (a, b) => a * 1000 + b); 
b6711ec9de26
misc tuning and recovery of Isabelle coding style;
wenzelm
parents:
32941
diff
changeset

129 
val as_time = the_default 0 o Scan.read Symbol.stopper time o explode; 
b6711ec9de26
misc tuning and recovery of Isabelle coding style;
wenzelm
parents:
32941
diff
changeset

130 
in (proof, as_time t) end; 
33247  131 
fun split_time' s = 
132 
if Config.get ctxt measure_runtime then split_time s else (s, 0) 

32458
de6834b20e9e
sledgehammer's temporary files are removed properly (even in case of an exception occurs)
boehmes
parents:
32451
diff
changeset

133 
fun run_on probfile = 
32942
b6711ec9de26
misc tuning and recovery of Isabelle coding style;
wenzelm
parents:
32941
diff
changeset

134 
if File.exists cmd then 
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

135 
write_file full_types explicit_apply probfile clauses 
35010
d6e492cea6e4
renamed system/system_out to bash/bash_output  to emphasized that this is really GNU bash, not some undefined POSIX sh;
wenzelm
parents:
33316
diff
changeset

136 
> pair (apfst split_time' (bash_output (cmd_line probfile))) 
36167
c1a35be8e476
make Sledgehammer's output more debugging friendly
blanchet
parents:
36143
diff
changeset

137 
else error ("Bad executable: " ^ Path.implode cmd ^ "."); 
28592  138 

36167
c1a35be8e476
make Sledgehammer's output more debugging friendly
blanchet
parents:
36143
diff
changeset

139 
(* If the problem file has not been exported, remove it; otherwise, export 
c1a35be8e476
make Sledgehammer's output more debugging friendly
blanchet
parents:
36143
diff
changeset

140 
the proof file too. *) 
32942
b6711ec9de26
misc tuning and recovery of Isabelle coding style;
wenzelm
parents:
32941
diff
changeset

141 
fun cleanup probfile = if destdir' = "" then try File.rm probfile else NONE; 
b6711ec9de26
misc tuning and recovery of Isabelle coding style;
wenzelm
parents:
32941
diff
changeset

142 
fun export probfile (((proof, _), _), _) = 
36187  143 
if destdir' = "" then 
144 
() 

145 
else 

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

36190  147 
("% " ^ timestamp () ^ "\n" ^ proof) 
32257
bad5a99c16d8
neg_conjecture_clauses, neg_clausify_tac: proper context, eliminated METAHYPS;
wenzelm
parents:
32091
diff
changeset

148 

36231
bede2d49ba3b
get rid of "conjecture_pos", which is no longer necessary now that it's Metis's job, not Sledgehammer's, to report inconsistent contexts
blanchet
parents:
36223
diff
changeset

149 
val (((proof, atp_run_time_in_msecs), rc), _) = 
35570
0e30eef52d85
basic simplification of external_prover signature;
wenzelm
parents:
35010
diff
changeset

150 
with_path cleanup export run_on (prob_pathname subgoal); 
32458
de6834b20e9e
sledgehammer's temporary files are removed properly (even in case of an exception occurs)
boehmes
parents:
32451
diff
changeset

151 

36167
c1a35be8e476
make Sledgehammer's output more debugging friendly
blanchet
parents:
36143
diff
changeset

152 
(* Check for success and print out some information on failure. *) 
36265
41c9e755e552
distinguish between the different ATP errors in the user interface;
blanchet
parents:
36264
diff
changeset

153 
val failure = find_known_failure known_failures proof; 
41c9e755e552
distinguish between the different ATP errors in the user interface;
blanchet
parents:
36264
diff
changeset

154 
val success = rc = 0 andalso failure = ""; 
35969  155 
val (message, relevant_thm_names) = 
36265
41c9e755e552
distinguish between the different ATP errors in the user interface;
blanchet
parents:
36264
diff
changeset

156 
if success then 
41c9e755e552
distinguish between the different ATP errors in the user interface;
blanchet
parents:
36264
diff
changeset

157 
proof_text name proof internal_thm_names ctxt th subgoal 
41c9e755e552
distinguish between the different ATP errors in the user interface;
blanchet
parents:
36264
diff
changeset

158 
else if failure <> "" then 
41c9e755e552
distinguish between the different ATP errors in the user interface;
blanchet
parents:
36264
diff
changeset

159 
(failure, []) 
41c9e755e552
distinguish between the different ATP errors in the user interface;
blanchet
parents:
36264
diff
changeset

160 
else 
41c9e755e552
distinguish between the different ATP errors in the user interface;
blanchet
parents:
36264
diff
changeset

161 
("Unknown ATP error: " ^ proof ^ ".\n", []) 
32864
a226f29d4bdc
reorganized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
32740
diff
changeset

162 
in 
36231
bede2d49ba3b
get rid of "conjecture_pos", which is no longer necessary now that it's Metis's job, not Sledgehammer's, to report inconsistent contexts
blanchet
parents:
36223
diff
changeset

163 
{success = success, message = message, 
35969  164 
relevant_thm_names = relevant_thm_names, 
165 
atp_run_time_in_msecs = atp_run_time_in_msecs, proof = proof, 

166 
internal_thm_names = internal_thm_names, 

167 
filtered_clauses = the_filtered_clauses} 

32942
b6711ec9de26
misc tuning and recovery of Isabelle coding style;
wenzelm
parents:
32941
diff
changeset

168 
end; 
28592  169 

28596
fcd463a6b6de
tuned interfaces  plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset

170 

fcd463a6b6de
tuned interfaces  plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset

171 
(* generic TPTPbased provers *) 
fcd463a6b6de
tuned interfaces  plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset

172 

35865  173 
fun generic_tptp_prover 
36265
41c9e755e552
distinguish between the different ATP errors in the user interface;
blanchet
parents:
36264
diff
changeset

174 
(name, {command, arguments, known_failures, max_new_clauses, 
36220
f3655a3ae1ab
rename Sledgehammer "theory_const" option to "theory_relevant", now that I understand better what it does
blanchet
parents:
36219
diff
changeset

175 
prefers_theory_relevant, supports_isar_proofs}) 
36264
3c2490917710
added "spass_tptp" prover, which requires SPASS x.y > 3.0;
blanchet
parents:
36235
diff
changeset

176 
(params as {debug, overlord, respect_no_atp, relevance_threshold, 
3c2490917710
added "spass_tptp" prover, which requires SPASS x.y > 3.0;
blanchet
parents:
36235
diff
changeset

177 
convergence, theory_relevant, higher_order, follow_defs, 
3c2490917710
added "spass_tptp" prover, which requires SPASS x.y > 3.0;
blanchet
parents:
36235
diff
changeset

178 
isar_proof, modulus, sorts, ...}) 
36059  179 
timeout = 
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:
36142
diff
changeset

180 
generic_prover overlord 
36058
8256d5a185bd
added "respect_no_atp" and "convergence" options to Sledgehammer;
blanchet
parents:
36001
diff
changeset

181 
(get_relevant_facts respect_no_atp relevance_threshold convergence 
8256d5a185bd
added "respect_no_atp" and "convergence" options to Sledgehammer;
blanchet
parents:
36001
diff
changeset

182 
higher_order follow_defs max_new_clauses 
36220
f3655a3ae1ab
rename Sledgehammer "theory_const" option to "theory_relevant", now that I understand better what it does
blanchet
parents:
36219
diff
changeset

183 
(the_default prefers_theory_relevant theory_relevant)) 
36222
0e3e49bd658d
don't use readable names if proof reconstruction is needed, because it uses the structure of names
blanchet
parents:
36220
diff
changeset

184 
(prepare_clauses higher_order false) 
36264
3c2490917710
added "spass_tptp" prover, which requires SPASS x.y > 3.0;
blanchet
parents:
36235
diff
changeset

185 
(write_tptp_file (debug andalso overlord andalso not isar_proof)) command 
36265
41c9e755e552
distinguish between the different ATP errors in the user interface;
blanchet
parents:
36264
diff
changeset

186 
(arguments timeout) known_failures 
36223
217ca1273786
make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents:
36222
diff
changeset

187 
(proof_text (supports_isar_proofs andalso isar_proof) false modulus sorts) 
217ca1273786
make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents:
36222
diff
changeset

188 
name params 
28596
fcd463a6b6de
tuned interfaces  plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset

189 

35969  190 
fun tptp_prover name p = (name, generic_tptp_prover (name, p)); 
28596
fcd463a6b6de
tuned interfaces  plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset

191 

32941
72d48e333b77
eliminated extraneous wrapping of public records;
wenzelm
parents:
32936
diff
changeset

192 

32864
a226f29d4bdc
reorganized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
32740
diff
changeset

193 
(** common provers **) 
28592  194 

36142
f5e15e9aae10
make Sledgehammer "minimize" output less confusing + round up (not down) time limits to nearest second
blanchet
parents:
36064
diff
changeset

195 
fun generous_to_secs time = (Time.toMilliseconds time + 999) div 1000 
f5e15e9aae10
make Sledgehammer "minimize" output less confusing + round up (not down) time limits to nearest second
blanchet
parents:
36064
diff
changeset

196 

28596
fcd463a6b6de
tuned interfaces  plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset

197 
(* Vampire *) 
fcd463a6b6de
tuned interfaces  plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset

198 

35969  199 
(* NB: Vampire does not work without explicit time limit. *) 
28596
fcd463a6b6de
tuned interfaces  plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset

200 

35969  201 
val vampire_config : prover_config = 
202 
{command = Path.explode "$VAMPIRE_HOME/vampire", 

203 
arguments = (fn timeout => "output_syntax tptp mode casc t " ^ 

36142
f5e15e9aae10
make Sledgehammer "minimize" output less confusing + round up (not down) time limits to nearest second
blanchet
parents:
36064
diff
changeset

204 
string_of_int (generous_to_secs timeout)), 
36265
41c9e755e552
distinguish between the different ATP errors in the user interface;
blanchet
parents:
36264
diff
changeset

205 
known_failures = 
41c9e755e552
distinguish between the different ATP errors in the user interface;
blanchet
parents:
36264
diff
changeset

206 
[(["Satisfiability detected", "CANNOT PROVE"], 
41c9e755e552
distinguish between the different ATP errors in the user interface;
blanchet
parents:
36264
diff
changeset

207 
"The ATP problem is unprovable."), 
41c9e755e552
distinguish between the different ATP errors in the user interface;
blanchet
parents:
36264
diff
changeset

208 
(["Refutation not found"], 
41c9e755e552
distinguish between the different ATP errors in the user interface;
blanchet
parents:
36264
diff
changeset

209 
"The ATP failed to determine the problem's status.")], 
35969  210 
max_new_clauses = 60, 
36220
f3655a3ae1ab
rename Sledgehammer "theory_const" option to "theory_relevant", now that I understand better what it does
blanchet
parents:
36219
diff
changeset

211 
prefers_theory_relevant = false, 
35969  212 
supports_isar_proofs = true} 
213 
val vampire = tptp_prover "vampire" vampire_config 

28596
fcd463a6b6de
tuned interfaces  plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset

214 

28592  215 

28596
fcd463a6b6de
tuned interfaces  plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset

216 
(* E prover *) 
fcd463a6b6de
tuned interfaces  plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset

217 

35969  218 
val e_config : prover_config = 
219 
{command = Path.explode "$E_HOME/eproof", 

220 
arguments = (fn timeout => "tstpin tstpout l5 xAutoDev \ 

221 
\tAutoDev silent cpulimit=" ^ 

36142
f5e15e9aae10
make Sledgehammer "minimize" output less confusing + round up (not down) time limits to nearest second
blanchet
parents:
36064
diff
changeset

222 
string_of_int (generous_to_secs timeout)), 
36265
41c9e755e552
distinguish between the different ATP errors in the user interface;
blanchet
parents:
36264
diff
changeset

223 
known_failures = 
41c9e755e552
distinguish between the different ATP errors in the user interface;
blanchet
parents:
36264
diff
changeset

224 
[(["SZS status: Satisfiable", "SZS status Satisfiable"], 
41c9e755e552
distinguish between the different ATP errors in the user interface;
blanchet
parents:
36264
diff
changeset

225 
"The ATP problem is unprovable."), 
41c9e755e552
distinguish between the different ATP errors in the user interface;
blanchet
parents:
36264
diff
changeset

226 
(["SZS status: ResourceOut", "SZS status ResourceOut"], 
41c9e755e552
distinguish between the different ATP errors in the user interface;
blanchet
parents:
36264
diff
changeset

227 
"The ATP ran out of resources."), 
41c9e755e552
distinguish between the different ATP errors in the user interface;
blanchet
parents:
36264
diff
changeset

228 
(["# Cannot determine problem status"], 
41c9e755e552
distinguish between the different ATP errors in the user interface;
blanchet
parents:
36264
diff
changeset

229 
"The ATP failed to determine the problem's status.")], 
35969  230 
max_new_clauses = 100, 
36220
f3655a3ae1ab
rename Sledgehammer "theory_const" option to "theory_relevant", now that I understand better what it does
blanchet
parents:
36219
diff
changeset

231 
prefers_theory_relevant = false, 
35969  232 
supports_isar_proofs = true} 
233 
val e = tptp_prover "e" e_config 

28596
fcd463a6b6de
tuned interfaces  plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset

234 

fcd463a6b6de
tuned interfaces  plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset

235 

fcd463a6b6de
tuned interfaces  plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset

236 
(* SPASS *) 
28592  237 

35865  238 
fun generic_dfg_prover 
36265
41c9e755e552
distinguish between the different ATP errors in the user interface;
blanchet
parents:
36264
diff
changeset

239 
(name, ({command, arguments, known_failures, max_new_clauses, 
36220
f3655a3ae1ab
rename Sledgehammer "theory_const" option to "theory_relevant", now that I understand better what it does
blanchet
parents:
36219
diff
changeset

240 
prefers_theory_relevant, ...} : prover_config)) 
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:
36142
diff
changeset

241 
(params as {overlord, respect_no_atp, relevance_threshold, convergence, 
36220
f3655a3ae1ab
rename Sledgehammer "theory_const" option to "theory_relevant", now that I understand better what it does
blanchet
parents:
36219
diff
changeset

242 
theory_relevant, higher_order, follow_defs, ...}) 
36059  243 
timeout = 
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:
36142
diff
changeset

244 
generic_prover overlord 
36058
8256d5a185bd
added "respect_no_atp" and "convergence" options to Sledgehammer;
blanchet
parents:
36001
diff
changeset

245 
(get_relevant_facts respect_no_atp relevance_threshold convergence 
8256d5a185bd
added "respect_no_atp" and "convergence" options to Sledgehammer;
blanchet
parents:
36001
diff
changeset

246 
higher_order follow_defs max_new_clauses 
36220
f3655a3ae1ab
rename Sledgehammer "theory_const" option to "theory_relevant", now that I understand better what it does
blanchet
parents:
36219
diff
changeset

247 
(the_default prefers_theory_relevant theory_relevant)) 
35969  248 
(prepare_clauses higher_order true) write_dfg_file command 
36265
41c9e755e552
distinguish between the different ATP errors in the user interface;
blanchet
parents:
36264
diff
changeset

249 
(arguments timeout) known_failures (metis_proof_text false false) 
36223
217ca1273786
make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents:
36222
diff
changeset

250 
name params 
32869
159309603edc
recovered support for Spass: reenabled writing problems in DFG format
boehmes
parents:
32864
diff
changeset

251 

36264
3c2490917710
added "spass_tptp" prover, which requires SPASS x.y > 3.0;
blanchet
parents:
36235
diff
changeset

252 
fun dfg_prover name p = (name, generic_dfg_prover (name, p)) 
32869
159309603edc
recovered support for Spass: reenabled writing problems in DFG format
boehmes
parents:
32864
diff
changeset

253 

36219
16670b4f0baa
set SPASS option on the commandline, so that it doesn't vanish when moving to TPTP format
blanchet
parents:
36190
diff
changeset

254 
(* The "VarWeight=3" option helps the higherorder problems, probably by 
16670b4f0baa
set SPASS option on the commandline, so that it doesn't vanish when moving to TPTP format
blanchet
parents:
36190
diff
changeset

255 
counteracting the presence of "hAPP". *) 
36059  256 
val spass_config : prover_config = 
35969  257 
{command = Path.explode "$SPASS_HOME/SPASS", 
258 
arguments = (fn timeout => "Auto SOS=1 PGiven=0 PProblem=0 Splits=0" ^ 

36219
16670b4f0baa
set SPASS option on the commandline, so that it doesn't vanish when moving to TPTP format
blanchet
parents:
36190
diff
changeset

259 
" FullRed=0 DocProof VarWeight=3 TimeLimit=" ^ 
36142
f5e15e9aae10
make Sledgehammer "minimize" output less confusing + round up (not down) time limits to nearest second
blanchet
parents:
36064
diff
changeset

260 
string_of_int (generous_to_secs timeout)), 
36265
41c9e755e552
distinguish between the different ATP errors in the user interface;
blanchet
parents:
36264
diff
changeset

261 
known_failures = 
41c9e755e552
distinguish between the different ATP errors in the user interface;
blanchet
parents:
36264
diff
changeset

262 
[(["SPASS beiseite: Completion found."], "The ATP problem is unprovable."), 
41c9e755e552
distinguish between the different ATP errors in the user interface;
blanchet
parents:
36264
diff
changeset

263 
(["SPASS beiseite: Ran out of time."], "The ATP timed out."), 
41c9e755e552
distinguish between the different ATP errors in the user interface;
blanchet
parents:
36264
diff
changeset

264 
(["SPASS beiseite: Maximal number of loops exceeded."], 
41c9e755e552
distinguish between the different ATP errors in the user interface;
blanchet
parents:
36264
diff
changeset

265 
"The ATP hit its loop limit.")], 
35969  266 
max_new_clauses = 40, 
36220
f3655a3ae1ab
rename Sledgehammer "theory_const" option to "theory_relevant", now that I understand better what it does
blanchet
parents:
36219
diff
changeset

267 
prefers_theory_relevant = true, 
36059  268 
supports_isar_proofs = false} 
36264
3c2490917710
added "spass_tptp" prover, which requires SPASS x.y > 3.0;
blanchet
parents:
36235
diff
changeset

269 
val spass = dfg_prover "spass" spass_config 
3c2490917710
added "spass_tptp" prover, which requires SPASS x.y > 3.0;
blanchet
parents:
36235
diff
changeset

270 

3c2490917710
added "spass_tptp" prover, which requires SPASS x.y > 3.0;
blanchet
parents:
36235
diff
changeset

271 
(* SPASS 3.7 supports both the DFG and the TPTP syntax, whereas SPASS 3.0 
3c2490917710
added "spass_tptp" prover, which requires SPASS x.y > 3.0;
blanchet
parents:
36235
diff
changeset

272 
supports only the DFG syntax. As soon as all Isabelle repository/snapshot 
3c2490917710
added "spass_tptp" prover, which requires SPASS x.y > 3.0;
blanchet
parents:
36235
diff
changeset

273 
users have upgraded to 3.7, we can kill "spass" (and all DFG support in 
3c2490917710
added "spass_tptp" prover, which requires SPASS x.y > 3.0;
blanchet
parents:
36235
diff
changeset

274 
Sledgehammer) and rename "spass_tptp" "spass". *) 
35969  275 

36265
41c9e755e552
distinguish between the different ATP errors in the user interface;
blanchet
parents:
36264
diff
changeset

276 
(* FIXME: Change the error message below to point to the Isabelle download 
41c9e755e552
distinguish between the different ATP errors in the user interface;
blanchet
parents:
36264
diff
changeset

277 
page once the package is there (around the Isabelle2010 release). *) 
41c9e755e552
distinguish between the different ATP errors in the user interface;
blanchet
parents:
36264
diff
changeset

278 

36264
3c2490917710
added "spass_tptp" prover, which requires SPASS x.y > 3.0;
blanchet
parents:
36235
diff
changeset

279 
val spass_tptp_config = 
3c2490917710
added "spass_tptp" prover, which requires SPASS x.y > 3.0;
blanchet
parents:
36235
diff
changeset

280 
{command = #command spass_config, 
3c2490917710
added "spass_tptp" prover, which requires SPASS x.y > 3.0;
blanchet
parents:
36235
diff
changeset

281 
arguments = prefix "TPTP " o #arguments spass_config, 
36265
41c9e755e552
distinguish between the different ATP errors in the user interface;
blanchet
parents:
36264
diff
changeset

282 
known_failures = 
41c9e755e552
distinguish between the different ATP errors in the user interface;
blanchet
parents:
36264
diff
changeset

283 
#known_failures spass_config @ 
41c9e755e552
distinguish between the different ATP errors in the user interface;
blanchet
parents:
36264
diff
changeset

284 
[(["unrecognized option `TPTP'", "Unrecognized option TPTP"], 
41c9e755e552
distinguish between the different ATP errors in the user interface;
blanchet
parents:
36264
diff
changeset

285 
"Warning: Sledgehammer requires a more recent version of SPASS with \ 
41c9e755e552
distinguish between the different ATP errors in the user interface;
blanchet
parents:
36264
diff
changeset

286 
\support for the TPTP syntax. To install it, download and untar the \ 
41c9e755e552
distinguish between the different ATP errors in the user interface;
blanchet
parents:
36264
diff
changeset

287 
\package \"http://isabelle.in.tum.de/~blanchet/spass3.7.tgz\" and add \ 
41c9e755e552
distinguish between the different ATP errors in the user interface;
blanchet
parents:
36264
diff
changeset

288 
\the \"spass3.7\" directory's full path to \"" ^ 
41c9e755e552
distinguish between the different ATP errors in the user interface;
blanchet
parents:
36264
diff
changeset

289 
Path.implode (Path.expand (Path.appends 
41c9e755e552
distinguish between the different ATP errors in the user interface;
blanchet
parents:
36264
diff
changeset

290 
(Path.variable "ISABELLE_HOME_USER" :: 
41c9e755e552
distinguish between the different ATP errors in the user interface;
blanchet
parents:
36264
diff
changeset

291 
map Path.basic ["etc", "components"]))) ^ 
41c9e755e552
distinguish between the different ATP errors in the user interface;
blanchet
parents:
36264
diff
changeset

292 
"\" on a line of its own.")], 
36264
3c2490917710
added "spass_tptp" prover, which requires SPASS x.y > 3.0;
blanchet
parents:
36235
diff
changeset

293 
max_new_clauses = #max_new_clauses spass_config, 
3c2490917710
added "spass_tptp" prover, which requires SPASS x.y > 3.0;
blanchet
parents:
36235
diff
changeset

294 
prefers_theory_relevant = #prefers_theory_relevant spass_config, 
3c2490917710
added "spass_tptp" prover, which requires SPASS x.y > 3.0;
blanchet
parents:
36235
diff
changeset

295 
supports_isar_proofs = #supports_isar_proofs spass_config} 
3c2490917710
added "spass_tptp" prover, which requires SPASS x.y > 3.0;
blanchet
parents:
36235
diff
changeset

296 
val spass_tptp = tptp_prover "spass_tptp" spass_tptp_config 
28596
fcd463a6b6de
tuned interfaces  plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset

297 

fcd463a6b6de
tuned interfaces  plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset

298 
(* remote prover invocation via SystemOnTPTP *) 
fcd463a6b6de
tuned interfaces  plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset

299 

32942
b6711ec9de26
misc tuning and recovery of Isabelle coding style;
wenzelm
parents:
32941
diff
changeset

300 
val systems = Synchronized.var "atp_wrapper_systems" ([]: string list); 
31835  301 

302 
fun get_systems () = 

303 
let 

35969  304 
val (answer, rc) = bash_output "\"$ISABELLE_ATP_MANAGER/SystemOnTPTP\" w" 
31835  305 
in 
35969  306 
if rc <> 0 then 
307 
error ("Failed to get available systems at SystemOnTPTP:\n" ^ answer) 

308 
else 

309 
split_lines answer 

31835  310 
end; 
311 

35867  312 
fun refresh_systems_on_tptp () = 
313 
Synchronized.change systems (fn _ => get_systems ()); 

31835  314 

315 
fun get_system prefix = Synchronized.change_result systems (fn systems => 

32864
a226f29d4bdc
reorganized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
32740
diff
changeset

316 
(if null systems then get_systems () else systems) 
32942
b6711ec9de26
misc tuning and recovery of Isabelle coding style;
wenzelm
parents:
32941
diff
changeset

317 
> `(find_first (String.isPrefix prefix))); 
32864
a226f29d4bdc
reorganized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
32740
diff
changeset

318 

32948  319 
fun the_system prefix = 
32864
a226f29d4bdc
reorganized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
32740
diff
changeset

320 
(case get_system prefix of 
35826  321 
NONE => error ("System " ^ quote prefix ^ " not available at SystemOnTPTP") 
32942
b6711ec9de26
misc tuning and recovery of Isabelle coding style;
wenzelm
parents:
32941
diff
changeset

322 
 SOME sys => sys); 
31835  323 

36265
41c9e755e552
distinguish between the different ATP errors in the user interface;
blanchet
parents:
36264
diff
changeset

324 
val remote_known_failures = 
41c9e755e552
distinguish between the different ATP errors in the user interface;
blanchet
parents:
36264
diff
changeset

325 
[(["Remotescript could not extract proof"], 
41c9e755e552
distinguish between the different ATP errors in the user interface;
blanchet
parents:
36264
diff
changeset

326 
"Error: The remote ATP proof is illformed.")] 
35865  327 

36059  328 
fun remote_prover_config prover_prefix args 
36265
41c9e755e552
distinguish between the different ATP errors in the user interface;
blanchet
parents:
36264
diff
changeset

329 
({known_failures, max_new_clauses, prefers_theory_relevant, ...} 
36059  330 
: prover_config) : prover_config = 
35969  331 
{command = Path.explode "$ISABELLE_ATP_MANAGER/SystemOnTPTP", 
332 
arguments = (fn timeout => 

36142
f5e15e9aae10
make Sledgehammer "minimize" output less confusing + round up (not down) time limits to nearest second
blanchet
parents:
36064
diff
changeset

333 
args ^ " t " ^ string_of_int (generous_to_secs timeout) ^ " s " ^ 
35969  334 
the_system prover_prefix), 
36265
41c9e755e552
distinguish between the different ATP errors in the user interface;
blanchet
parents:
36264
diff
changeset

335 
known_failures = remote_known_failures @ known_failures, 
35969  336 
max_new_clauses = max_new_clauses, 
36220
f3655a3ae1ab
rename Sledgehammer "theory_const" option to "theory_relevant", now that I understand better what it does
blanchet
parents:
36219
diff
changeset

337 
prefers_theory_relevant = prefers_theory_relevant, 
35969  338 
supports_isar_proofs = false} 
28596
fcd463a6b6de
tuned interfaces  plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset

339 

35969  340 
val remote_vampire = 
341 
tptp_prover "remote_vampire" 

36059  342 
(remote_prover_config "Vampire9" "" vampire_config) 
32864
a226f29d4bdc
reorganized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
32740
diff
changeset

343 

35969  344 
val remote_e = 
36059  345 
tptp_prover "remote_e" (remote_prover_config "EP" "" e_config) 
32864
a226f29d4bdc
reorganized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
32740
diff
changeset

346 

35969  347 
val remote_spass = 
36059  348 
tptp_prover "remote_spass" (remote_prover_config "SPASS" "x" spass_config) 
28592  349 

36264
3c2490917710
added "spass_tptp" prover, which requires SPASS x.y > 3.0;
blanchet
parents:
36235
diff
changeset

350 
val provers = [spass, spass_tptp, vampire, e, remote_vampire, remote_spass, 
3c2490917710
added "spass_tptp" prover, which requires SPASS x.y > 3.0;
blanchet
parents:
36235
diff
changeset

351 
remote_e] 
35867  352 
val prover_setup = fold add_prover provers 
353 

354 
val setup = 

355 
destdir_setup 

356 
#> problem_prefix_setup 

357 
#> measure_runtime_setup 

358 
#> prover_setup; 

359 

28592  360 
end; 