author  blanchet 
Thu, 15 Apr 2010 13:49:46 +0200  
changeset 36167  c1a35be8e476 
parent 36143  6490319b1703 
child 36169  27b1cc58715e 
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 

35969  23 
open Sledgehammer_Fact_Preprocessor 
35865  24 
open Sledgehammer_HOL_Clause 
25 
open Sledgehammer_Fact_Filter 

26 
open Sledgehammer_Proof_Reconstruct 

35867  27 
open ATP_Manager 
35826  28 

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

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

30 

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

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

32 

36001  33 
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

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

35 

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

36 
val (problem_prefix, problem_prefix_setup) = 
36001  37 
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

38 

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

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

42 

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

44 

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

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

46 
{command: Path.T, 
35969  47 
arguments: Time.time > string, 
35865  48 
failure_strs: string list, 
32864
a226f29d4bdc
reorganized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
32740
diff
changeset

49 
max_new_clauses: int, 
36059  50 
prefers_theory_const: bool, 
35969  51 
supports_isar_proofs: bool}; 
28596
fcd463a6b6de
tuned interfaces  plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset

52 

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 
(* basic template *) 
fcd463a6b6de
tuned interfaces  plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset

55 

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

56 
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

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

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

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

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

61 

35865  62 
fun find_failure strs proof = 
63 
case filter (fn s => String.isSubstring s proof) strs of 

64 
[] => if is_proof_well_formed proof then NONE 

65 
else SOME "Illformed ATP output" 

66 
 (failure :: _) => SOME failure 

67 

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

68 
fun generic_prover overlord get_facts prepare write cmd args failure_strs 
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

69 
produce_answer name ({full_types, ...} : params) 
35969  70 
({subgoal, goal, relevance_override, axiom_clauses, filtered_clauses} 
71 
: problem) = 

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

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

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

75 
val thy = ProofContext.theory_of ctxt; 
35865  76 
val chain_ths = map (Thm.put_name_hint chained_hint) chain_ths; 
35969  77 
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

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

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

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

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

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

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

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

87 
prepare goal_cls chain_ths the_axiom_clauses the_filtered_clauses thy; 
31750  88 

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

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

90 
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

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

92 
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

93 
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

94 
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

95 
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

96 
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

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

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

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

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

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

102 
then Path.append (Path.explode destdir') probfile 
32864
a226f29d4bdc
reorganized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
32740
diff
changeset

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

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

105 

31750  106 
(* write out problem file and call prover *) 
33247  107 
fun cmd_line probfile = 
108 
if Config.get ctxt measure_runtime 

109 
then (* Warning: suppresses error messages of ATPs *) 

110 
"TIMEFORMAT='%3U'; { time " ^ space_implode " " [File.shell_path cmd, 

111 
args, File.shell_path probfile] ^ " 2> /dev/null" ^ " ; } 2>&1" 

112 
else 

113 
space_implode " " ["exec", File.shell_path cmd, args, 

114 
File.shell_path probfile]; 

32510  115 
fun split_time s = 
116 
let 

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

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

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

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

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

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

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

123 
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

124 
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

125 
in (proof, as_time t) end; 
33247  126 
fun split_time' s = 
127 
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

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

129 
if File.exists cmd then 
35969  130 
write full_types 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

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

132 
else error ("Bad executable: " ^ Path.implode cmd ^ "."); 
28592  133 

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

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

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

136 
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

137 
fun export probfile (((proof, _), _), _) = 
b6711ec9de26
misc tuning and recovery of Isabelle coding style;
wenzelm
parents:
32941
diff
changeset

138 
if destdir' = "" then () 
b6711ec9de26
misc tuning and recovery of Isabelle coding style;
wenzelm
parents:
32941
diff
changeset

139 
else File.write (Path.explode (Path.implode probfile ^ "_proof")) proof; 
32257
bad5a99c16d8
neg_conjecture_clauses, neg_clausify_tac: proper context, eliminated METAHYPS;
wenzelm
parents:
32091
diff
changeset

140 

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

142 
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

143 

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

144 
(* Check for success and print out some information on failure. *) 
35865  145 
val failure = find_failure failure_strs proof; 
32942
b6711ec9de26
misc tuning and recovery of Isabelle coding style;
wenzelm
parents:
32941
diff
changeset

146 
val success = rc = 0 andalso is_none failure; 
35969  147 
val (message, relevant_thm_names) = 
36167
c1a35be8e476
make Sledgehammer's output more debugging friendly
blanchet
parents:
36143
diff
changeset

148 
if is_some failure then ("ATP failed to find a proof.", []) 
c1a35be8e476
make Sledgehammer's output more debugging friendly
blanchet
parents:
36143
diff
changeset

149 
else if rc <> 0 then ("ATP error: " ^ proof ^ ".", []) 
35969  150 
else 
151 
(produce_answer name (proof, internal_thm_names, conj_pos, ctxt, th, 

152 
subgoal)); 

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

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

154 
{success = success, message = message, 
35969  155 
relevant_thm_names = relevant_thm_names, 
156 
atp_run_time_in_msecs = atp_run_time_in_msecs, proof = proof, 

157 
internal_thm_names = internal_thm_names, 

158 
filtered_clauses = the_filtered_clauses} 

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

159 
end; 
28592  160 

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

161 

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

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

163 

35865  164 
fun generic_tptp_prover 
165 
(name, {command, arguments, failure_strs, max_new_clauses, 

36059  166 
prefers_theory_const, supports_isar_proofs}) 
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

167 
(params as {overlord, respect_no_atp, relevance_threshold, convergence, 
36064
48aec67c284f
added "modulus" and "sorts" options to control Sledgehammer's Isar proof output
blanchet
parents:
36059
diff
changeset

168 
theory_const, higher_order, follow_defs, isar_proof, 
48aec67c284f
added "modulus" and "sorts" options to control Sledgehammer's Isar proof output
blanchet
parents:
36059
diff
changeset

169 
modulus, sorts, ...}) 
36059  170 
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

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

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

173 
higher_order follow_defs max_new_clauses 
36059  174 
(the_default prefers_theory_const theory_const)) 
35969  175 
(prepare_clauses higher_order false) write_tptp_file command 
176 
(arguments timeout) failure_strs 

36064
48aec67c284f
added "modulus" and "sorts" options to control Sledgehammer's Isar proof output
blanchet
parents:
36059
diff
changeset

177 
(if supports_isar_proofs andalso isar_proof then 
48aec67c284f
added "modulus" and "sorts" options to control Sledgehammer's Isar proof output
blanchet
parents:
36059
diff
changeset

178 
structured_isar_proof modulus sorts 
48aec67c284f
added "modulus" and "sorts" options to control Sledgehammer's Isar proof output
blanchet
parents:
36059
diff
changeset

179 
else 
48aec67c284f
added "modulus" and "sorts" options to control Sledgehammer's Isar proof output
blanchet
parents:
36059
diff
changeset

180 
metis_lemma_list false) name params; 
28596
fcd463a6b6de
tuned interfaces  plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset

181 

35969  182 
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

183 

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

184 

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

185 
(** common provers **) 
28592  186 

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

187 
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

188 

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

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

190 

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

192 

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

195 
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

196 
string_of_int (generous_to_secs timeout)), 
35969  197 
failure_strs = 
198 
["Satisfiability detected", "Refutation not found", "CANNOT PROVE"], 

199 
max_new_clauses = 60, 

36059  200 
prefers_theory_const = false, 
35969  201 
supports_isar_proofs = true} 
202 
val vampire = tptp_prover "vampire" vampire_config 

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

203 

28592  204 

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

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

206 

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

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

210 
\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

211 
string_of_int (generous_to_secs timeout)), 
35969  212 
failure_strs = 
213 
["SZS status: Satisfiable", "SZS status Satisfiable", 

214 
"SZS status: ResourceOut", "SZS status ResourceOut", 

215 
"# Cannot determine problem status"], 

216 
max_new_clauses = 100, 

36059  217 
prefers_theory_const = false, 
35969  218 
supports_isar_proofs = true} 
219 
val e = tptp_prover "e" e_config 

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

220 

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

221 

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

222 
(* SPASS *) 
28592  223 

35865  224 
fun generic_dfg_prover 
225 
(name, ({command, arguments, failure_strs, max_new_clauses, 

36059  226 
prefers_theory_const, ...} : 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

227 
(params as {overlord, respect_no_atp, relevance_threshold, convergence, 
36064
48aec67c284f
added "modulus" and "sorts" options to control Sledgehammer's Isar proof output
blanchet
parents:
36059
diff
changeset

228 
theory_const, higher_order, follow_defs, ...}) 
36059  229 
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

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

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

232 
higher_order follow_defs max_new_clauses 
36059  233 
(the_default prefers_theory_const theory_const)) 
35969  234 
(prepare_clauses higher_order true) write_dfg_file command 
235 
(arguments timeout) failure_strs (metis_lemma_list true) name params; 

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

236 

35865  237 
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

238 

36059  239 
val spass_config : prover_config = 
35969  240 
{command = Path.explode "$SPASS_HOME/SPASS", 
241 
arguments = (fn timeout => "Auto SOS=1 PGiven=0 PProblem=0 Splits=0" ^ 

242 
" FullRed=0 DocProof TimeLimit=" ^ 

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

243 
string_of_int (generous_to_secs timeout)), 
35969  244 
failure_strs = 
245 
["SPASS beiseite: Completion found.", "SPASS beiseite: Ran out of time.", 

246 
"SPASS beiseite: Maximal number of loops exceeded."], 

247 
max_new_clauses = 40, 

36059  248 
prefers_theory_const = true, 
249 
supports_isar_proofs = false} 

35969  250 
val spass = dfg_prover ("spass", spass_config) 
251 

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

252 

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

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

254 

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

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

257 
fun get_systems () = 

258 
let 

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

263 
else 

264 
split_lines answer 

31835  265 
end; 
266 

35867  267 
fun refresh_systems_on_tptp () = 
268 
Synchronized.change systems (fn _ => get_systems ()); 

31835  269 

270 
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

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

272 
> `(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

273 

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

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

277 
 SOME sys => sys); 
31835  278 

35865  279 
val remote_failure_strs = ["Remotescript could not extract proof"]; 
280 

36059  281 
fun remote_prover_config prover_prefix args 
282 
({failure_strs, max_new_clauses, prefers_theory_const, ...} 

283 
: prover_config) : prover_config = 

35969  284 
{command = Path.explode "$ISABELLE_ATP_MANAGER/SystemOnTPTP", 
285 
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

286 
args ^ " t " ^ string_of_int (generous_to_secs timeout) ^ " s " ^ 
35969  287 
the_system prover_prefix), 
36059  288 
failure_strs = remote_failure_strs @ failure_strs, 
35969  289 
max_new_clauses = max_new_clauses, 
36059  290 
prefers_theory_const = prefers_theory_const, 
35969  291 
supports_isar_proofs = false} 
28596
fcd463a6b6de
tuned interfaces  plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset

292 

35969  293 
val remote_vampire = 
294 
tptp_prover "remote_vampire" 

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

296 

35969  297 
val remote_e = 
36059  298 
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

299 

35969  300 
val remote_spass = 
36059  301 
tptp_prover "remote_spass" (remote_prover_config "SPASS" "x" spass_config) 
28592  302 

36059  303 
val provers = [spass, vampire, e, remote_vampire, remote_spass, remote_e] 
35867  304 
val prover_setup = fold add_prover provers 
305 

306 
val setup = 

307 
destdir_setup 

308 
#> problem_prefix_setup 

309 
#> measure_runtime_setup 

310 
#> prover_setup; 

311 

28592  312 
end; 