author  blanchet 
Wed, 14 Apr 2010 18:23:51 +0200  
changeset 36142  f5e15e9aae10 
parent 36064  48aec67c284f 
child 36143  6490319b1703 
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 

35969  68 
fun generic_prover get_facts prepare write cmd args failure_strs produce_answer 
69 
name ({full_types, ...} : params) 

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 *) 
32942
b6711ec9de26
misc tuning and recovery of Isabelle coding style;
wenzelm
parents:
32941
diff
changeset

90 
val destdir' = Config.get ctxt destdir; 
b6711ec9de26
misc tuning and recovery of Isabelle coding style;
wenzelm
parents:
32941
diff
changeset

91 
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

92 
fun prob_pathname nr = 
32942
b6711ec9de26
misc tuning and recovery of Isabelle coding style;
wenzelm
parents:
32941
diff
changeset

93 
let val probfile = 
b6711ec9de26
misc tuning and recovery of Isabelle coding style;
wenzelm
parents:
32941
diff
changeset

94 
Path.basic (problem_prefix' ^ serial_string () ^ "_" ^ string_of_int nr) 
b6711ec9de26
misc tuning and recovery of Isabelle coding style;
wenzelm
parents:
32941
diff
changeset

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

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

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

98 
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

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

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

101 

31750  102 
(* write out problem file and call prover *) 
33247  103 
fun cmd_line probfile = 
104 
if Config.get ctxt measure_runtime 

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

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

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

108 
else 

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

110 
File.shell_path probfile]; 

32510  111 
fun split_time s = 
112 
let 

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

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

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

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

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

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

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

119 
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

120 
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

121 
in (proof, as_time t) end; 
33247  122 
fun split_time' s = 
123 
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

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

125 
if File.exists cmd then 
35969  126 
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

127 
> pair (apfst split_time' (bash_output (cmd_line probfile))) 
32942
b6711ec9de26
misc tuning and recovery of Isabelle coding style;
wenzelm
parents:
32941
diff
changeset

128 
else error ("Bad executable: " ^ Path.implode cmd); 
28592  129 

31751  130 
(* if problemfile has not been exported, delete problemfile; otherwise export proof, too *) 
32942
b6711ec9de26
misc tuning and recovery of Isabelle coding style;
wenzelm
parents:
32941
diff
changeset

131 
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

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

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

134 
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

135 

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

137 
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

138 

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

141 
val success = rc = 0 andalso is_none failure; 
35969  142 
val (message, relevant_thm_names) = 
32451
8f0dc876fb1b
propagate theorem names, in addition to generated return message
boehmes
parents:
32327
diff
changeset

143 
if is_some failure then ("External prover failed.", []) 
8f0dc876fb1b
propagate theorem names, in addition to generated return message
boehmes
parents:
32327
diff
changeset

144 
else if rc <> 0 then ("External prover failed: " ^ proof, []) 
35969  145 
else 
146 
(produce_answer name (proof, internal_thm_names, conj_pos, ctxt, th, 

147 
subgoal)); 

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

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

149 
{success = success, message = message, 
35969  150 
relevant_thm_names = relevant_thm_names, 
151 
atp_run_time_in_msecs = atp_run_time_in_msecs, proof = proof, 

152 
internal_thm_names = internal_thm_names, 

153 
filtered_clauses = the_filtered_clauses} 

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

154 
end; 
28592  155 

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

156 

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

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

158 

35865  159 
fun generic_tptp_prover 
160 
(name, {command, arguments, failure_strs, max_new_clauses, 

36059  161 
prefers_theory_const, supports_isar_proofs}) 
36058
8256d5a185bd
added "respect_no_atp" and "convergence" options to Sledgehammer;
blanchet
parents:
36001
diff
changeset

162 
(params as {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

163 
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

164 
modulus, sorts, ...}) 
36059  165 
timeout = 
35969  166 
generic_prover 
36058
8256d5a185bd
added "respect_no_atp" and "convergence" options to Sledgehammer;
blanchet
parents:
36001
diff
changeset

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

168 
higher_order follow_defs max_new_clauses 
36059  169 
(the_default prefers_theory_const theory_const)) 
35969  170 
(prepare_clauses higher_order false) write_tptp_file command 
171 
(arguments timeout) failure_strs 

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

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

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

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

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

176 

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

178 

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

179 

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

180 
(** common provers **) 
28592  181 

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

182 
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

183 

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

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

185 

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

187 

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

190 
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

191 
string_of_int (generous_to_secs timeout)), 
35969  192 
failure_strs = 
193 
["Satisfiability detected", "Refutation not found", "CANNOT PROVE"], 

194 
max_new_clauses = 60, 

36059  195 
prefers_theory_const = false, 
35969  196 
supports_isar_proofs = true} 
197 
val vampire = tptp_prover "vampire" vampire_config 

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

198 

28592  199 

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

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

201 

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

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

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

206 
string_of_int (generous_to_secs timeout)), 
35969  207 
failure_strs = 
208 
["SZS status: Satisfiable", "SZS status Satisfiable", 

209 
"SZS status: ResourceOut", "SZS status ResourceOut", 

210 
"# Cannot determine problem status"], 

211 
max_new_clauses = 100, 

36059  212 
prefers_theory_const = false, 
35969  213 
supports_isar_proofs = true} 
214 
val e = tptp_prover "e" e_config 

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

215 

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

216 

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

217 
(* SPASS *) 
28592  218 

35865  219 
fun generic_dfg_prover 
220 
(name, ({command, arguments, failure_strs, max_new_clauses, 

36059  221 
prefers_theory_const, ...} : prover_config)) 
36058
8256d5a185bd
added "respect_no_atp" and "convergence" options to Sledgehammer;
blanchet
parents:
36001
diff
changeset

222 
(params as {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

223 
theory_const, higher_order, follow_defs, ...}) 
36059  224 
timeout = 
35969  225 
generic_prover 
36058
8256d5a185bd
added "respect_no_atp" and "convergence" options to Sledgehammer;
blanchet
parents:
36001
diff
changeset

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

227 
higher_order follow_defs max_new_clauses 
36059  228 
(the_default prefers_theory_const theory_const)) 
35969  229 
(prepare_clauses higher_order true) write_dfg_file command 
230 
(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

231 

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

233 

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

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

238 
string_of_int (generous_to_secs timeout)), 
35969  239 
failure_strs = 
240 
["SPASS beiseite: Completion found.", "SPASS beiseite: Ran out of time.", 

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

242 
max_new_clauses = 40, 

36059  243 
prefers_theory_const = true, 
244 
supports_isar_proofs = false} 

35969  245 
val spass = dfg_prover ("spass", spass_config) 
246 

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

247 

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

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

249 

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

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

252 
fun get_systems () = 

253 
let 

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

258 
else 

259 
split_lines answer 

31835  260 
end; 
261 

35867  262 
fun refresh_systems_on_tptp () = 
263 
Synchronized.change systems (fn _ => get_systems ()); 

31835  264 

265 
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

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

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

268 

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

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

272 
 SOME sys => sys); 
31835  273 

35865  274 
val remote_failure_strs = ["Remotescript could not extract proof"]; 
275 

36059  276 
fun remote_prover_config prover_prefix args 
277 
({failure_strs, max_new_clauses, prefers_theory_const, ...} 

278 
: prover_config) : prover_config = 

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

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

287 

35969  288 
val remote_vampire = 
289 
tptp_prover "remote_vampire" 

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

291 

35969  292 
val remote_e = 
36059  293 
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

294 

35969  295 
val remote_spass = 
36059  296 
tptp_prover "remote_spass" (remote_prover_config "SPASS" "x" spass_config) 
28592  297 

36059  298 
val provers = [spass, vampire, e, remote_vampire, remote_spass, remote_e] 
35867  299 
val prover_setup = fold add_prover provers 
300 

301 
val setup = 

302 
destdir_setup 

303 
#> problem_prefix_setup 

304 
#> measure_runtime_setup 

305 
#> prover_setup; 

306 

28592  307 
end; 