author  wenzelm 
Thu, 15 Oct 2009 12:23:24 +0200  
changeset 32942  b6711ec9de26 
parent 32941  72d48e333b77 
child 32944  ecc0705174c2 
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 

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

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

10 
val destdir: string Config.T 
a226f29d4bdc
reorganized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
32740
diff
changeset

11 
val problem_prefix: string Config.T 
a226f29d4bdc
reorganized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
32740
diff
changeset

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

13 

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

14 
(*prover configuration, problem format, and prover result*) 
32941
72d48e333b77
eliminated extraneous wrapping of public records;
wenzelm
parents:
32936
diff
changeset

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

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

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

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

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

20 
emit_structured_proof: bool} 
72d48e333b77
eliminated extraneous wrapping of public records;
wenzelm
parents:
32936
diff
changeset

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

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

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

24 
goal: Proof.context * (thm list * thm), 
a226f29d4bdc
reorganized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
32740
diff
changeset

25 
axiom_clauses: (thm * (string * int)) list option, 
32941
72d48e333b77
eliminated extraneous wrapping of public records;
wenzelm
parents:
32936
diff
changeset

26 
filtered_clauses: (thm * (string * int)) list option} 
72d48e333b77
eliminated extraneous wrapping of public records;
wenzelm
parents:
32936
diff
changeset

27 
val atp_problem_of_goal: bool > int > Proof.context * (thm list * thm) > atp_problem 
72d48e333b77
eliminated extraneous wrapping of public records;
wenzelm
parents:
32936
diff
changeset

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

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

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

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

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

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

34 
internal_thm_names: string Vector.vector, 
32941
72d48e333b77
eliminated extraneous wrapping of public records;
wenzelm
parents:
32936
diff
changeset

35 
filtered_clauses: (thm * (string * int)) list} 
32864
a226f29d4bdc
reorganized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
32740
diff
changeset

36 
type prover = atp_problem > int > prover_result 
a226f29d4bdc
reorganized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
32740
diff
changeset

37 

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

38 
(*common provers*) 
a226f29d4bdc
reorganized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
32740
diff
changeset

39 
val vampire: string * prover 
a226f29d4bdc
reorganized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
32740
diff
changeset

40 
val vampire_full: string * prover 
a226f29d4bdc
reorganized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
32740
diff
changeset

41 
val eprover: string * prover 
a226f29d4bdc
reorganized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
32740
diff
changeset

42 
val eprover_full: string * prover 
a226f29d4bdc
reorganized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
32740
diff
changeset

43 
val spass: string * prover 
a226f29d4bdc
reorganized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
32740
diff
changeset

44 
val spass_no_tc: string * prover 
a226f29d4bdc
reorganized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
32740
diff
changeset

45 
val remote_vampire: string * prover 
a226f29d4bdc
reorganized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
32740
diff
changeset

46 
val remote_eprover: string * prover 
a226f29d4bdc
reorganized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
32740
diff
changeset

47 
val remote_spass: string * prover 
31835  48 
val refresh_systems: unit > unit 
28592  49 
end; 
50 

32936  51 
structure ATP_Wrapper: ATP_WRAPPER = 
28592  52 
struct 
28596
fcd463a6b6de
tuned interfaces  plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset

53 

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

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

55 

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

56 
(* hooks for writing problem files *) 
a226f29d4bdc
reorganized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
32740
diff
changeset

57 

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

58 
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

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

60 

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

61 
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

62 
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

63 

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

64 
val setup = destdir_setup #> problem_prefix_setup; 
a226f29d4bdc
reorganized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
32740
diff
changeset

65 

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

66 

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

67 
(* prover configuration, problem format, and prover result *) 
a226f29d4bdc
reorganized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
32740
diff
changeset

68 

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

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

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

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

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

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

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

75 

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

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

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

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

79 
goal: Proof.context * (thm list * thm), 
a226f29d4bdc
reorganized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
32740
diff
changeset

80 
axiom_clauses: (thm * (string * int)) list option, 
32941
72d48e333b77
eliminated extraneous wrapping of public records;
wenzelm
parents:
32936
diff
changeset

81 
filtered_clauses: (thm * (string * int)) list option}; 
32864
a226f29d4bdc
reorganized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
32740
diff
changeset

82 

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

83 
fun atp_problem_of_goal with_full_types subgoal goal : atp_problem = 
72d48e333b77
eliminated extraneous wrapping of public records;
wenzelm
parents:
32936
diff
changeset

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

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

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

87 
axiom_clauses = NONE, 
32941
72d48e333b77
eliminated extraneous wrapping of public records;
wenzelm
parents:
32936
diff
changeset

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

89 

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

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

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

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

93 
theorem_names: string list, (*relevant theorems*) 
72d48e333b77
eliminated extraneous wrapping of public records;
wenzelm
parents:
32936
diff
changeset

94 
runtime: int, (*user time of the ATP, in milliseconds*) 
32864
a226f29d4bdc
reorganized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
32740
diff
changeset

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

96 
internal_thm_names: string Vector.vector, 
32941
72d48e333b77
eliminated extraneous wrapping of public records;
wenzelm
parents:
32936
diff
changeset

97 
filtered_clauses: (thm * (string * int)) list}; 
32864
a226f29d4bdc
reorganized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
32740
diff
changeset

98 

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

99 
type prover = atp_problem > int > prover_result; 
28596
fcd463a6b6de
tuned interfaces  plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset

100 

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

101 

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

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

103 

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

104 
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

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

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

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

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

109 

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

110 
fun external_prover relevance_filter prepare write cmd args find_failure produce_answer 
32864
a226f29d4bdc
reorganized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
32740
diff
changeset

111 
axiom_clauses filtered_clauses name subgoalno goal = 
28596
fcd463a6b6de
tuned interfaces  plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset

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

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

115 
val thy = ProofContext.theory_of ctxt; 
b6711ec9de26
misc tuning and recovery of Isabelle coding style;
wenzelm
parents:
32941
diff
changeset

116 
val chain_ths = map (Thm.put_name_hint ResReconstruct.chained_hint) chain_ths; 
b6711ec9de26
misc tuning and recovery of Isabelle coding style;
wenzelm
parents:
32941
diff
changeset

117 
val goal_cls = #1 (ResAxioms.neg_conjecture_clauses ctxt th subgoalno); 
31752
19a5f1c8a844
use results of relevancefilter to determine additional clauses;
immler@in.tum.de
parents:
31751
diff
changeset

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

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

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

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

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

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

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

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

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

127 
prepare goal_cls chain_ths the_axiom_clauses the_filtered_clauses thy; 
31750  128 

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

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

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

131 
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

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

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

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

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

136 
if destdir' = "" then File.tmp_path probfile 
32864
a226f29d4bdc
reorganized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
32740
diff
changeset

137 
else if File.exists (Path.explode (destdir')) 
a226f29d4bdc
reorganized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
32740
diff
changeset

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

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

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

141 

31750  142 
(* write out problem file and call prover *) 
32593
3711565687a6
undo changes from revision 719426c9e1eb: removed Perl script for ATP invocation, measuring time using Bashbuiltin "time";
boehmes
parents:
32574
diff
changeset

143 
fun cmd_line probfile = "TIMEFORMAT='%3U'; { time " ^ space_implode " " 
3711565687a6
undo changes from revision 719426c9e1eb: removed Perl script for ATP invocation, measuring time using Bashbuiltin "time";
boehmes
parents:
32574
diff
changeset

144 
[File.shell_path cmd, args, File.platform_path probfile] ^ " ; } 2>&1" 
32510  145 
fun split_time s = 
146 
let 

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

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

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

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

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

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

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

153 
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

154 
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

155 
in (proof, as_time t) end; 
32458
de6834b20e9e
sledgehammer's temporary files are removed properly (even in case of an exception occurs)
boehmes
parents:
32451
diff
changeset

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

157 
if File.exists cmd then 
b6711ec9de26
misc tuning and recovery of Isabelle coding style;
wenzelm
parents:
32941
diff
changeset

158 
write probfile clauses 
32510  159 
> pair (apfst split_time (system_out (cmd_line probfile))) 
32942
b6711ec9de26
misc tuning and recovery of Isabelle coding style;
wenzelm
parents:
32941
diff
changeset

160 
else error ("Bad executable: " ^ Path.implode cmd); 
28592  161 

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

163 
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

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

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

166 
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

167 

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

168 
val (((proof, time), rc), conj_pos) = 
b6711ec9de26
misc tuning and recovery of Isabelle coding style;
wenzelm
parents:
32941
diff
changeset

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

170 

29590  171 
(* check for success and print out some information on failure *) 
32942
b6711ec9de26
misc tuning and recovery of Isabelle coding style;
wenzelm
parents:
32941
diff
changeset

172 
val failure = find_failure proof; 
b6711ec9de26
misc tuning and recovery of Isabelle coding style;
wenzelm
parents:
32941
diff
changeset

173 
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

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

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

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

177 
else apfst (fn s => "Try this command: " ^ s) 
32942
b6711ec9de26
misc tuning and recovery of Isabelle coding style;
wenzelm
parents:
32941
diff
changeset

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

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

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

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

182 
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

183 
end; 
28592  184 

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

185 

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

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

187 

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

188 
fun gen_tptp_prover (name, prover_config) problem timeout = 
a226f29d4bdc
reorganized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
32740
diff
changeset

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

190 
val {max_new_clauses, insert_theory_const, emit_structured_proof, command, arguments} = 
32942
b6711ec9de26
misc tuning and recovery of Isabelle coding style;
wenzelm
parents:
32941
diff
changeset

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

192 
val {with_full_types, subgoal, goal, axiom_clauses, filtered_clauses} = problem; 
32864
a226f29d4bdc
reorganized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
32740
diff
changeset

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

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

195 
(ResAtp.get_relevant max_new_clauses insert_theory_const) 
a226f29d4bdc
reorganized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
32740
diff
changeset

196 
(ResAtp.prepare_clauses false) 
a226f29d4bdc
reorganized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
32740
diff
changeset

197 
(ResHolClause.tptp_write_file with_full_types) 
a226f29d4bdc
reorganized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
32740
diff
changeset

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

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

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

201 
(if emit_structured_proof then ResReconstruct.structured_proof 
32941
72d48e333b77
eliminated extraneous wrapping of public records;
wenzelm
parents:
32936
diff
changeset

202 
else ResReconstruct.lemma_list false) 
32864
a226f29d4bdc
reorganized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
32740
diff
changeset

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

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

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

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

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

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

209 

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

210 
fun tptp_prover (name, config) = (name, gen_tptp_prover (name, config)); 
28596
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 

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

213 

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

214 
(** common provers **) 
28592  215 

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

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

217 

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

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

219 

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

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

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

222 

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

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

224 
{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

225 
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

226 
" t " ^ string_of_int timeout), 
a226f29d4bdc
reorganized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
32740
diff
changeset

227 
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

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

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

230 

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

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

232 
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

233 

28592  234 

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

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

236 

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

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

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

239 

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

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

241 
{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

242 
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

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

244 
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

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

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

247 

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

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

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

250 

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

251 

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

252 
(* SPASS *) 
28592  253 

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

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

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

256 

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

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

258 
{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

259 
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

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

261 
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

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

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

264 

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

265 
fun gen_dfg_prover (name, prover_config: prover_config) problem timeout = 
32869
159309603edc
recovered support for Spass: reenabled writing problems in DFG format
boehmes
parents:
32864
diff
changeset

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

267 
val {max_new_clauses, insert_theory_const, command, arguments, ...} = prover_config 
32941
72d48e333b77
eliminated extraneous wrapping of public records;
wenzelm
parents:
32936
diff
changeset

268 
val {with_full_types, subgoal, goal, axiom_clauses, filtered_clauses} = problem 
32869
159309603edc
recovered support for Spass: reenabled writing problems in DFG format
boehmes
parents:
32864
diff
changeset

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

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

271 
(ResAtp.get_relevant max_new_clauses insert_theory_const) 
159309603edc
recovered support for Spass: reenabled writing problems in DFG format
boehmes
parents:
32864
diff
changeset

272 
(ResAtp.prepare_clauses true) 
159309603edc
recovered support for Spass: reenabled writing problems in DFG format
boehmes
parents:
32864
diff
changeset

273 
(ResHolClause.dfg_write_file with_full_types) 
159309603edc
recovered support for Spass: reenabled writing problems in DFG format
boehmes
parents:
32864
diff
changeset

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

275 
(arguments timeout) 
159309603edc
recovered support for Spass: reenabled writing problems in DFG format
boehmes
parents:
32864
diff
changeset

276 
ResReconstruct.find_failure 
159309603edc
recovered support for Spass: reenabled writing problems in DFG format
boehmes
parents:
32864
diff
changeset

277 
(ResReconstruct.lemma_list true) 
159309603edc
recovered support for Spass: reenabled writing problems in DFG format
boehmes
parents:
32864
diff
changeset

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

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

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

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

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

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

284 

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

285 
fun dfg_prover (name, config) = (name, gen_dfg_prover (name, config)); 
32869
159309603edc
recovered support for Spass: reenabled writing problems in DFG format
boehmes
parents:
32864
diff
changeset

286 

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

287 
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

288 
val spass_no_tc = dfg_prover ("spass_no_tc", spass_config false); 
28592  289 

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

290 

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

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

292 

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

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

295 
fun get_systems () = 

296 
let 

32327
0971cc0b6a57
src/HOL/Tools/ATP_Manager as separate component, with (almost) everything in one place;
wenzelm
parents:
32257
diff
changeset

297 
val (answer, rc) = system_out ("\"$ISABELLE_ATP_MANAGER/SystemOnTPTP\" w") 
31835  298 
in 
32327
0971cc0b6a57
src/HOL/Tools/ATP_Manager as separate component, with (almost) everything in one place;
wenzelm
parents:
32257
diff
changeset

299 
if rc <> 0 then error ("Failed to get available systems from SystemOnTPTP:\n" ^ answer) 
31835  300 
else split_lines answer 
301 
end; 

302 

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

303 
fun refresh_systems () = Synchronized.change systems (fn _ => get_systems ()); 
31835  304 

305 
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

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

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

308 

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

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

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

311 
NONE => error ("No system like " ^ quote prefix ^ " at SystemOnTPTP") 
32942
b6711ec9de26
misc tuning and recovery of Isabelle coding style;
wenzelm
parents:
32941
diff
changeset

312 
 SOME sys => sys); 
31835  313 

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

314 
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

315 
{command = Path.explode "$ISABELLE_ATP_MANAGER/SystemOnTPTP", 
32942
b6711ec9de26
misc tuning and recovery of Isabelle coding style;
wenzelm
parents:
32941
diff
changeset

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

317 
(fn timeout => args ^ " t " ^ string_of_int timeout ^ " s " ^ get_the_system prover_prefix), 
32864
a226f29d4bdc
reorganized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
32740
diff
changeset

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

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

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

321 

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

322 
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

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

324 

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

325 
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

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

327 

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

328 
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

329 
"SPASS" "x" spass_max_new_clauses spass_insert_theory_const); 
28592  330 

331 
end; 