author  wenzelm 
Tue, 14 Oct 2008 20:10:45 +0200  
changeset 28596  fcd463a6b6de 
parent 28592  824f8390aaa2 
child 29587  96599d8d8268 
permissions  rwrr 
28592  1 
(* Title: HOL/Tools/atp_wrapper.ML 
2 
ID: $Id$ 

3 
Author: Fabian Immler, TU Muenchen 

4 

5 
Wrapper functions for external ATPs. 

6 
*) 

7 

8 
signature ATP_WRAPPER = 

9 
sig 

10 
val destdir: string ref 

11 
val problem_name: string ref 

12 
val external_prover: 

13 
((int > Path.T) > Proof.context * thm list * thm > string list * ResHolClause.axiom_name Vector.vector list) > 

14 
Path.T * string > 

15 
(string * int > bool) > 

16 
(string * string vector * Proof.context * thm * int > string) > 

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

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

18 
val tptp_prover_opts_full: int > bool > bool > Path.T * string > AtpManager.prover 
fcd463a6b6de
tuned interfaces  plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset

19 
val tptp_prover_opts: int > bool > Path.T * string > AtpManager.prover 
fcd463a6b6de
tuned interfaces  plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset

20 
val tptp_prover: Path.T * string > AtpManager.prover 
fcd463a6b6de
tuned interfaces  plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset

21 
val full_prover_opts: int > bool > Path.T * string > AtpManager.prover 
fcd463a6b6de
tuned interfaces  plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset

22 
val full_prover: Path.T * string > AtpManager.prover 
fcd463a6b6de
tuned interfaces  plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset

23 
val vampire_opts: int > bool > AtpManager.prover 
fcd463a6b6de
tuned interfaces  plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset

24 
val vampire: AtpManager.prover 
fcd463a6b6de
tuned interfaces  plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset

25 
val vampire_opts_full: int > bool > AtpManager.prover 
fcd463a6b6de
tuned interfaces  plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset

26 
val vampire_full: AtpManager.prover 
fcd463a6b6de
tuned interfaces  plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset

27 
val eprover_opts: int > bool > AtpManager.prover 
fcd463a6b6de
tuned interfaces  plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset

28 
val eprover: AtpManager.prover 
fcd463a6b6de
tuned interfaces  plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset

29 
val eprover_opts_full: int > bool > AtpManager.prover 
fcd463a6b6de
tuned interfaces  plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset

30 
val eprover_full: AtpManager.prover 
fcd463a6b6de
tuned interfaces  plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset

31 
val spass_opts: int > bool > AtpManager.prover 
fcd463a6b6de
tuned interfaces  plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset

32 
val spass: AtpManager.prover 
fcd463a6b6de
tuned interfaces  plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset

33 
val remote_prover_opts: int > bool > string > string > AtpManager.prover 
fcd463a6b6de
tuned interfaces  plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset

34 
val remote_prover: string > string > AtpManager.prover 
28592  35 
end; 
36 

37 
structure AtpWrapper: ATP_WRAPPER = 

38 
struct 

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

39 

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

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

41 

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

42 
(* global hooks for writing problemfiles *) 
fcd463a6b6de
tuned interfaces  plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset

43 

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

44 
val destdir = ref ""; (*Empty means write files to /tmp*) 
fcd463a6b6de
tuned interfaces  plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset

45 
val problem_name = ref "prob"; 
fcd463a6b6de
tuned interfaces  plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset

46 

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

47 

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

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

49 

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

50 
fun external_prover write_problem_files (cmd, args) check_success produce_answer subgoalno state = 
fcd463a6b6de
tuned interfaces  plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset

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

52 
(* path to unique problem file *) 
28592  53 
val destdir' = ! destdir 
54 
val problem_name' = ! problem_name 

55 
fun prob_pathname nr = 

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

56 
let val probfile = Path.basic (problem_name' ^ serial_string () ^ "_" ^ string_of_int nr) 
28592  57 
in if destdir' = "" then File.tmp_path probfile 
58 
else if File.exists (Path.explode (destdir')) 

59 
then Path.append (Path.explode (destdir')) probfile 

60 
else error ("No such directory: " ^ destdir') 

61 
end 

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

62 

28592  63 
(* write out problem file and call prover *) 
28596
fcd463a6b6de
tuned interfaces  plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset

64 
val (ctxt, (chain_ths, goal)) = Proof.get_goal state 
fcd463a6b6de
tuned interfaces  plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset

65 
val chain_ths = map (Thm.put_name_hint ResReconstruct.chained_hint) chain_ths 
fcd463a6b6de
tuned interfaces  plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset

66 
val (filenames, thm_names_list) = write_problem_files prob_pathname (ctxt, chain_ths, goal) 
fcd463a6b6de
tuned interfaces  plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset

67 
val thm_names = nth thm_names_list (subgoalno  1) 
fcd463a6b6de
tuned interfaces  plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset

68 

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

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

70 
if File.exists cmd then File.shell_path cmd ^ " " ^ args 
fcd463a6b6de
tuned interfaces  plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset

71 
else error ("Bad executable: " ^ Path.implode cmd) 
fcd463a6b6de
tuned interfaces  plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset

72 
val (proof, rc) = system_out (cmdline ^ " " ^ nth filenames (subgoalno  1)) 
fcd463a6b6de
tuned interfaces  plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset

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

74 
if rc <> 0 then 
fcd463a6b6de
tuned interfaces  plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset

75 
warning ("Sledgehammer prover exited with return code " ^ string_of_int rc ^ "\n" ^ cmdline) 
fcd463a6b6de
tuned interfaces  plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset

76 
else () 
28592  77 

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

78 
(* remove *temporary* files *) 
fcd463a6b6de
tuned interfaces  plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset

79 
val _ = if destdir' = "" then List.app OS.FileSys.remove filenames else () 
28592  80 

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

81 
val success = check_success (proof, rc) 
fcd463a6b6de
tuned interfaces  plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset

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

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

84 
then "Try this command: " ^ produce_answer (proof, thm_names, ctxt, goal, subgoalno) 
fcd463a6b6de
tuned interfaces  plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset

85 
else "Failed." 
fcd463a6b6de
tuned interfaces  plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset

86 
in (success, message) end; 
fcd463a6b6de
tuned interfaces  plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset

87 

28592  88 

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

89 

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

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

91 

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

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

93 

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

94 
fun tptp_prover_opts_full max_new theory_const full command = 
fcd463a6b6de
tuned interfaces  plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset

95 
external_prover 
28592  96 
(ResAtp.write_problem_files ResHolClause.tptp_write_file max_new theory_const) 
97 
command 

98 
ResReconstruct.check_success_e_vamp_spass 

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

99 
(if full then ResReconstruct.structured_proof else ResReconstruct.lemma_list_tstp); 
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 
(*arbitrary ATP with TPTP input/output and problemfile as last argument*) 
fcd463a6b6de
tuned interfaces  plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset

102 
fun tptp_prover_opts max_new theory_const = 
fcd463a6b6de
tuned interfaces  plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset

103 
tptp_prover_opts_full max_new theory_const false; 
fcd463a6b6de
tuned interfaces  plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset

104 

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

105 
val tptp_prover = tptp_prover_opts 60 true; 
fcd463a6b6de
tuned interfaces  plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset

106 

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

107 
(*for structured proofs: prover must support TSTP*) 
fcd463a6b6de
tuned interfaces  plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset

108 
fun full_prover_opts max_new theory_const = 
fcd463a6b6de
tuned interfaces  plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset

109 
tptp_prover_opts_full max_new theory_const true; 
fcd463a6b6de
tuned interfaces  plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset

110 

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

111 
val full_prover = full_prover_opts 60 true; 
fcd463a6b6de
tuned interfaces  plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset

112 

28592  113 

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

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

115 

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

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

117 

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

118 
fun vampire_opts max_new theory_const = tptp_prover_opts 
fcd463a6b6de
tuned interfaces  plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset

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

120 
(Path.explode "$VAMPIRE_HOME/vampire", "output_syntax tptp mode casc t 3600"); 
fcd463a6b6de
tuned interfaces  plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset

121 

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

122 
val vampire = vampire_opts 60 false; 
fcd463a6b6de
tuned interfaces  plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset

123 

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

124 
fun vampire_opts_full max_new theory_const = full_prover_opts 
fcd463a6b6de
tuned interfaces  plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset

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

126 
(Path.explode "$VAMPIRE_HOME/vampire", "output_syntax tptp mode casc t 3600"); 
fcd463a6b6de
tuned interfaces  plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset

127 

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

128 
val vampire_full = vampire_opts 60 false; 
fcd463a6b6de
tuned interfaces  plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset

129 

28592  130 

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

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

132 

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

133 
fun eprover_opts max_new theory_const = tptp_prover_opts 
fcd463a6b6de
tuned interfaces  plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset

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

135 
(Path.explode "$E_HOME/eproof", "tstpin tstpout l5 xAutoDev tAutoDev silent"); 
fcd463a6b6de
tuned interfaces  plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset

136 

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

137 
val eprover = eprover_opts 100 false; 
fcd463a6b6de
tuned interfaces  plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset

138 

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

139 
fun eprover_opts_full max_new theory_const = full_prover_opts 
fcd463a6b6de
tuned interfaces  plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset

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

141 
(Path.explode "$E_HOME/eproof", "tstpin tstpout l5 xAutoDev tAutoDev silent"); 
fcd463a6b6de
tuned interfaces  plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset

142 

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

143 
val eprover_full = eprover_opts_full 100 false; 
fcd463a6b6de
tuned interfaces  plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset

144 

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

145 

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

146 
(* SPASS *) 
28592  147 

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

148 
fun spass_opts max_new theory_const = external_prover 
fcd463a6b6de
tuned interfaces  plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset

149 
(ResAtp.write_problem_files ResHolClause.dfg_write_file max_new theory_const) 
fcd463a6b6de
tuned interfaces  plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset

150 
(Path.explode "$SPASS_HOME/SPASS", "Auto SOS=1 PGiven=0 PProblem=0 Splits=0 FullRed=0 DocProof") 
fcd463a6b6de
tuned interfaces  plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset

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

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

153 

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

154 
val spass = spass_opts 40 true; 
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 
(* remote prover invocation via SystemOnTPTP *) 
fcd463a6b6de
tuned interfaces  plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset

158 

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

159 
fun remote_prover_opts max_new theory_const name command = 
fcd463a6b6de
tuned interfaces  plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset

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

161 
(Path.explode "$ISABELLE_HOME/contrib/SystemOnTPTP/remote", name ^ " " ^ command); 
fcd463a6b6de
tuned interfaces  plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset

162 

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

163 
val remote_prover = remote_prover_opts 60 false; 
28592  164 

165 
end; 