author  blanchet 
Fri, 19 Mar 2010 15:33:18 +0100  
changeset 35867  16279c4c7a33 
parent 35865  2f8fb5242799 
child 35868  491a97039ce1 
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 

35865  23 
open Sledgehammer_HOL_Clause 
24 
open Sledgehammer_Fact_Filter 

25 
open Sledgehammer_Proof_Reconstruct 

35867  26 
open ATP_Manager 
35826  27 

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

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

29 

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

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

31 

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

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

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

34 

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

35 
val (problem_prefix, problem_prefix_setup) = 
a226f29d4bdc
reorganized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
32740
diff
changeset

36 
Attrib.config_string "atp_problem_prefix" "prob"; 
a226f29d4bdc
reorganized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
32740
diff
changeset

37 

33247  38 
val (measure_runtime, measure_runtime_setup) = 
39 
Attrib.config_bool "atp_measure_runtime" false; 

40 

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

41 

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

43 

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

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

45 
{command: Path.T, 
32864
a226f29d4bdc
reorganized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
32740
diff
changeset

46 
arguments: int > string, 
35865  47 
failure_strs: string list, 
32864
a226f29d4bdc
reorganized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
32740
diff
changeset

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

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

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

51 

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

54 

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

55 
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

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

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

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

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

60 

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

63 
[] => if is_proof_well_formed proof then NONE 

64 
else SOME "Illformed ATP output" 

65 
 (failure :: _) => SOME failure 

66 

67 
fun external_prover relevance_filter prepare write cmd args failure_strs 

68 
produce_answer name ({with_full_types, subgoal, goal, axiom_clauses, 

69 
filtered_clauses}: problem) = 

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

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

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

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

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

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

78 
NONE => relevance_filter goal goal_cls 
b6711ec9de26
misc tuning and recovery of Isabelle coding style;
wenzelm
parents:
32941
diff
changeset

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

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

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

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

83 
 SOME axcls => axcls); 
32257
bad5a99c16d8
neg_conjecture_clauses, neg_clausify_tac: proper context, eliminated METAHYPS;
wenzelm
parents:
32091
diff
changeset

84 
val (thm_names, clauses) = 
32942
b6711ec9de26
misc tuning and recovery of Isabelle coding style;
wenzelm
parents:
32941
diff
changeset

85 
prepare goal_cls chain_ths the_axiom_clauses the_filtered_clauses thy; 
31750  86 

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

87 
(* path to unique problem file *) 
32942
b6711ec9de26
misc tuning and recovery of Isabelle coding style;
wenzelm
parents:
32941
diff
changeset

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

89 
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

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

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

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

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

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

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

96 
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

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

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

99 

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

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

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

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

106 
else 

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

108 
File.shell_path probfile]; 

32510  109 
fun split_time s = 
110 
let 

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

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

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

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

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

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

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

117 
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

118 
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

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

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

123 
if File.exists cmd then 
35570
0e30eef52d85
basic simplification of external_prover signature;
wenzelm
parents:
35010
diff
changeset

124 
write with_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

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

126 
else error ("Bad executable: " ^ Path.implode cmd); 
28592  127 

31751  128 
(* 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

129 
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

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

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

132 
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

133 

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

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

135 
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

136 

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

139 
val success = rc = 0 andalso is_none failure; 
32864
a226f29d4bdc
reorganized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
32740
diff
changeset

140 
val (message, real_thm_names) = 
32451
8f0dc876fb1b
propagate theorem names, in addition to generated return message
boehmes
parents:
32327
diff
changeset

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

142 
else if rc <> 0 then ("External prover failed: " ^ proof, []) 
8f0dc876fb1b
propagate theorem names, in addition to generated return message
boehmes
parents:
32327
diff
changeset

143 
else apfst (fn s => "Try this command: " ^ s) 
35570
0e30eef52d85
basic simplification of external_prover signature;
wenzelm
parents:
35010
diff
changeset

144 
(produce_answer name (proof, thm_names, conj_pos, ctxt, th, subgoal)); 
32864
a226f29d4bdc
reorganized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
32740
diff
changeset

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

146 
{success = success, message = message, 
72d48e333b77
eliminated extraneous wrapping of public records;
wenzelm
parents:
32936
diff
changeset

147 
theorem_names = real_thm_names, runtime = time, proof = proof, 
72d48e333b77
eliminated extraneous wrapping of public records;
wenzelm
parents:
32936
diff
changeset

148 
internal_thm_names = thm_names, filtered_clauses = the_filtered_clauses} 
32942
b6711ec9de26
misc tuning and recovery of Isabelle coding style;
wenzelm
parents:
32941
diff
changeset

149 
end; 
28592  150 

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

151 

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

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

153 

35865  154 
fun generic_tptp_prover 
155 
(name, {command, arguments, failure_strs, max_new_clauses, 

156 
insert_theory_const, emit_structured_proof}) timeout = 

157 
external_prover (get_relevant_facts max_new_clauses insert_theory_const) 

158 
(prepare_clauses false) write_tptp_file command (arguments timeout) 

159 
failure_strs 

160 
(if emit_structured_proof then structured_isar_proof 

161 
else metis_lemma_list false) name; 

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

162 

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

164 

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

165 

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

166 
(** common provers **) 
28592  167 

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

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

169 

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

170 
(*NB: Vampire does not work without explicit timelimit*) 
fcd463a6b6de
tuned interfaces  plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset

171 

35865  172 
val vampire_failure_strs = 
173 
["Satisfiability detected", "Refutation not found", "CANNOT PROVE"]; 

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

174 
val vampire_max_new_clauses = 60; 
b6711ec9de26
misc tuning and recovery of Isabelle coding style;
wenzelm
parents:
32941
diff
changeset

175 
val vampire_insert_theory_const = false; 
28596
fcd463a6b6de
tuned interfaces  plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset

176 

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

177 
fun vampire_prover_config full : prover_config = 
72d48e333b77
eliminated extraneous wrapping of public records;
wenzelm
parents:
32936
diff
changeset

178 
{command = Path.explode "$VAMPIRE_HOME/vampire", 
32864
a226f29d4bdc
reorganized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
32740
diff
changeset

179 
arguments = (fn timeout => "output_syntax tptp mode casc" ^ 
a226f29d4bdc
reorganized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
32740
diff
changeset

180 
" t " ^ string_of_int timeout), 
35865  181 
failure_strs = vampire_failure_strs, 
32864
a226f29d4bdc
reorganized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
32740
diff
changeset

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

183 
insert_theory_const = vampire_insert_theory_const, 
32942
b6711ec9de26
misc tuning and recovery of Isabelle coding style;
wenzelm
parents:
32941
diff
changeset

184 
emit_structured_proof = full}; 
28596
fcd463a6b6de
tuned interfaces  plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset

185 

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

186 
val vampire = tptp_prover ("vampire", vampire_prover_config false); 
b6711ec9de26
misc tuning and recovery of Isabelle coding style;
wenzelm
parents:
32941
diff
changeset

187 
val vampire_full = tptp_prover ("vampire_full", vampire_prover_config true); 
28596
fcd463a6b6de
tuned interfaces  plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset

188 

28592  189 

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

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

191 

35865  192 
val eprover_failure_strs = 
193 
["SZS status: Satisfiable", "SZS status Satisfiable", 

194 
"SZS status: ResourceOut", "SZS status ResourceOut", 

195 
"# Cannot determine problem status"]; 

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

196 
val eprover_max_new_clauses = 100; 
b6711ec9de26
misc tuning and recovery of Isabelle coding style;
wenzelm
parents:
32941
diff
changeset

197 
val eprover_insert_theory_const = false; 
28596
fcd463a6b6de
tuned interfaces  plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset

198 

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

199 
fun eprover_config full : prover_config = 
72d48e333b77
eliminated extraneous wrapping of public records;
wenzelm
parents:
32936
diff
changeset

200 
{command = Path.explode "$E_HOME/eproof", 
32864
a226f29d4bdc
reorganized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
32740
diff
changeset

201 
arguments = (fn timeout => "tstpin tstpout l5 xAutoDev tAutoDev" ^ 
a226f29d4bdc
reorganized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
32740
diff
changeset

202 
" silent cpulimit=" ^ string_of_int timeout), 
35865  203 
failure_strs = eprover_failure_strs, 
32864
a226f29d4bdc
reorganized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
32740
diff
changeset

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

205 
insert_theory_const = eprover_insert_theory_const, 
32942
b6711ec9de26
misc tuning and recovery of Isabelle coding style;
wenzelm
parents:
32941
diff
changeset

206 
emit_structured_proof = full}; 
28596
fcd463a6b6de
tuned interfaces  plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset

207 

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

208 
val eprover = tptp_prover ("e", eprover_config false); 
b6711ec9de26
misc tuning and recovery of Isabelle coding style;
wenzelm
parents:
32941
diff
changeset

209 
val eprover_full = tptp_prover ("e_full", eprover_config true); 
28596
fcd463a6b6de
tuned interfaces  plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset

210 

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

211 

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

212 
(* SPASS *) 
28592  213 

35865  214 
val spass_failure_strs = 
215 
["SPASS beiseite: Completion found.", "SPASS beiseite: Ran out of time.", 

216 
"SPASS beiseite: Maximal number of loops exceeded."]; 

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

217 
val spass_max_new_clauses = 40; 
b6711ec9de26
misc tuning and recovery of Isabelle coding style;
wenzelm
parents:
32941
diff
changeset

218 
val spass_insert_theory_const = true; 
28596
fcd463a6b6de
tuned interfaces  plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset

219 

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

220 
fun spass_config insert_theory_const: prover_config = 
72d48e333b77
eliminated extraneous wrapping of public records;
wenzelm
parents:
32936
diff
changeset

221 
{command = Path.explode "$SPASS_HOME/SPASS", 
32864
a226f29d4bdc
reorganized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
32740
diff
changeset

222 
arguments = (fn timeout => "Auto SOS=1 PGiven=0 PProblem=0 Splits=0" ^ 
a226f29d4bdc
reorganized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
32740
diff
changeset

223 
" FullRed=0 DocProof TimeLimit=" ^ string_of_int timeout), 
35865  224 
failure_strs = spass_failure_strs, 
32864
a226f29d4bdc
reorganized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
32740
diff
changeset

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

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

227 
emit_structured_proof = false}; 
32864
a226f29d4bdc
reorganized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
32740
diff
changeset

228 

35865  229 
fun generic_dfg_prover 
230 
(name, ({command, arguments, failure_strs, max_new_clauses, 

231 
insert_theory_const, ...} : prover_config)) timeout = 

232 
external_prover 

233 
(get_relevant_facts max_new_clauses insert_theory_const) 

234 
(prepare_clauses true) 

235 
write_dfg_file 

236 
command 

237 
(arguments timeout) 

238 
failure_strs 

239 
(metis_lemma_list true) 

240 
name; 

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

241 

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

243 

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

244 
val spass = dfg_prover ("spass", spass_config spass_insert_theory_const); 
b6711ec9de26
misc tuning and recovery of Isabelle coding style;
wenzelm
parents:
32941
diff
changeset

245 
val spass_no_tc = dfg_prover ("spass_no_tc", spass_config false); 
28592  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 

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

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

259 

35867  260 
fun refresh_systems_on_tptp () = 
261 
Synchronized.change systems (fn _ => get_systems ()); 

31835  262 

263 
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

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

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

266 

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

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

270 
 SOME sys => sys); 
31835  271 

35865  272 
val remote_failure_strs = ["Remotescript could not extract proof"]; 
273 

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

274 
fun remote_prover_config prover_prefix args max_new insert_tc: prover_config = 
72d48e333b77
eliminated extraneous wrapping of public records;
wenzelm
parents:
32936
diff
changeset

275 
{command = Path.explode "$ISABELLE_ATP_MANAGER/SystemOnTPTP", 
35865  276 
arguments = (fn timeout => 
277 
args ^ " t " ^ string_of_int timeout ^ " s " ^ the_system prover_prefix), 

278 
failure_strs = remote_failure_strs, 

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

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

280 
insert_theory_const = insert_tc, 
32942
b6711ec9de26
misc tuning and recovery of Isabelle coding style;
wenzelm
parents:
32941
diff
changeset

281 
emit_structured_proof = false}; 
28596
fcd463a6b6de
tuned interfaces  plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset

282 

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

283 
val remote_vampire = tptp_prover ("remote_vampire", remote_prover_config 
32942
b6711ec9de26
misc tuning and recovery of Isabelle coding style;
wenzelm
parents:
32941
diff
changeset

284 
"Vampire9" "" vampire_max_new_clauses vampire_insert_theory_const); 
32864
a226f29d4bdc
reorganized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
32740
diff
changeset

285 

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

286 
val remote_eprover = tptp_prover ("remote_e", remote_prover_config 
32942
b6711ec9de26
misc tuning and recovery of Isabelle coding style;
wenzelm
parents:
32941
diff
changeset

287 
"EP" "" eprover_max_new_clauses eprover_insert_theory_const); 
32864
a226f29d4bdc
reorganized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
32740
diff
changeset

288 

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

289 
val remote_spass = tptp_prover ("remote_spass", remote_prover_config 
32942
b6711ec9de26
misc tuning and recovery of Isabelle coding style;
wenzelm
parents:
32941
diff
changeset

290 
"SPASS" "x" spass_max_new_clauses spass_insert_theory_const); 
28592  291 

35867  292 
val provers = 
293 
[spass, vampire, eprover, vampire_full, eprover_full, spass_no_tc, 

294 
remote_vampire, remote_spass, remote_eprover] 

295 
val prover_setup = fold add_prover provers 

296 

297 
val setup = 

298 
destdir_setup 

299 
#> problem_prefix_setup 

300 
#> measure_runtime_setup 

301 
#> prover_setup; 

302 

28592  303 
end; 