author  mengj 
Tue, 07 Mar 2006 03:51:40 +0100  
changeset 19194  7681c04d8bff 
parent 18986  5060ca625e02 
child 19205  4ec788c69f82 
permissions  rwrr 
19194  1 
(* Author: Jia Meng, Cambridge University Computer Laboratory, NICTA 
15608  2 
ID: $Id$ 
3 
Copyright 2004 University of Cambridge 

15347  4 

5 
ATPs with TPTP format input. 

6 
*) 

15452  7 

16802
6eeee59dac4c
use Toplevel.print_state_hook instead of adhoc Proof.atp_hook;
wenzelm
parents:
16767
diff
changeset

8 
signature RES_ATP = 
6eeee59dac4c
use Toplevel.print_state_hook instead of adhoc Proof.atp_hook;
wenzelm
parents:
16767
diff
changeset

9 
sig 
17306  10 
val prover: string ref 
16802
6eeee59dac4c
use Toplevel.print_state_hook instead of adhoc Proof.atp_hook;
wenzelm
parents:
16767
diff
changeset

11 
val custom_spass: string list ref 
17484
f6a225f97f0a
simplification of the IsabelleATP code; hooks for batch generation of problems
paulson
parents:
17435
diff
changeset

12 
val destdir: string ref 
17849  13 
val helper_path: string > string > string 
17484
f6a225f97f0a
simplification of the IsabelleATP code; hooks for batch generation of problems
paulson
parents:
17435
diff
changeset

14 
val problem_name: string ref 
17690
8ba7c3cd24a8
time limit option; fixed bug concerning first line of ATP output
paulson
parents:
17525
diff
changeset

15 
val time_limit: int ref 
19194  16 

17 
datatype mode = Auto  Fol  Hol 

18 
val write_subgoal_file: mode > Proof.context > Thm.thm list > Thm.thm list > int > string 

19 
val vampire_time: int ref 

20 
val eprover_time: int ref 

21 
val run_vampire: int > unit 

22 
val run_eprover: int > unit 

23 
val vampireLimit: unit > int 

24 
val eproverLimit: unit > int 

25 
val atp_method: (ProofContext.context > Thm.thm list > int > Tactical.tactic) > 

26 
Method.src > ProofContext.context > Method.method 

27 
val cond_rm_tmp: string > unit 

28 
val keep_atp_input: bool ref 

29 
val fol_keep_types: bool ref 

30 
val hol_full_types: unit > unit 

31 
val hol_partial_types: unit > unit 

32 
val hol_const_types_only: unit > unit 

33 
val hol_no_types: unit > unit 

34 
val hol_typ_level: unit > ResHolClause.type_level 

35 
val run_relevance_filter: bool ref 

36 

15347  37 
end; 
38 

16802
6eeee59dac4c
use Toplevel.print_state_hook instead of adhoc Proof.atp_hook;
wenzelm
parents:
16767
diff
changeset

39 
structure ResAtp: RES_ATP = 
15347  40 
struct 
41 

19194  42 
(********************************************************************) 
43 
(* some settings for both background automatic ATP calling procedure*) 

44 
(* and also explicit ATP invocation methods *) 

45 
(********************************************************************) 

46 

47 
(*** background linkup ***) 

48 
val call_atp = ref false; 

17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
17091
diff
changeset

49 
val hook_count = ref 0; 
18675  50 
val time_limit = ref 30; 
17404
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17317
diff
changeset

51 
val prover = ref "E"; (* use E as the default prover *) 
17305
6cef3aedd661
axioms now included in tptp files, no /bin/cat and various tidying
paulson
parents:
17235
diff
changeset

52 
val custom_spass = (*specialized options for SPASS*) 
17690
8ba7c3cd24a8
time limit option; fixed bug concerning first line of ATP output
paulson
parents:
17525
diff
changeset

53 
ref ["Auto=0","FullRed=0","IORe","IOFc","RTaut","RFSub","RBSub"]; 
17484
f6a225f97f0a
simplification of the IsabelleATP code; hooks for batch generation of problems
paulson
parents:
17435
diff
changeset

54 
val destdir = ref ""; (*Empty means write files to /tmp*) 
f6a225f97f0a
simplification of the IsabelleATP code; hooks for batch generation of problems
paulson
parents:
17435
diff
changeset

55 
val problem_name = ref "prob"; 
f6a225f97f0a
simplification of the IsabelleATP code; hooks for batch generation of problems
paulson
parents:
17435
diff
changeset

56 

17819  57 
(*Return the path to a "helper" like SPASS or tptp2X, first checking that 
58 
it exists. FIXME: modify to use Path primitives and move to some central place.*) 

59 
fun helper_path evar base = 

60 
case getenv evar of 

61 
"" => error ("Isabelle environment variable " ^ evar ^ " not defined") 

62 
 home => 

63 
let val path = home ^ "/" ^ base 

64 
in if File.exists (File.unpack_platform_path path) then path 

65 
else error ("Could not find the file " ^ path) 

66 
end; 

67 

17717  68 
fun probfile_nosuffix _ = 
17484
f6a225f97f0a
simplification of the IsabelleATP code; hooks for batch generation of problems
paulson
parents:
17435
diff
changeset

69 
if !destdir = "" then File.platform_path (File.tmp_path (Path.basic (!problem_name))) 
f6a225f97f0a
simplification of the IsabelleATP code; hooks for batch generation of problems
paulson
parents:
17435
diff
changeset

70 
else if File.exists (File.unpack_platform_path (!destdir)) 
f6a225f97f0a
simplification of the IsabelleATP code; hooks for batch generation of problems
paulson
parents:
17435
diff
changeset

71 
then !destdir ^ "/" ^ !problem_name 
f6a225f97f0a
simplification of the IsabelleATP code; hooks for batch generation of problems
paulson
parents:
17435
diff
changeset

72 
else error ("No such directory: " ^ !destdir); 
15644  73 

17717  74 
fun prob_pathname n = probfile_nosuffix n ^ "_" ^ Int.toString n; 
75 

19194  76 

77 
(*** ATP methods ***) 

78 
val vampire_time = ref 60; 

79 
val eprover_time = ref 60; 

80 
fun run_vampire time = 

81 
if (time >0) then vampire_time:= time 

82 
else vampire_time:=60; 

83 

84 
fun run_eprover time = 

85 
if (time > 0) then eprover_time:= time 

86 
else eprover_time:=60; 

87 

88 
fun vampireLimit () = !vampire_time; 

89 
fun eproverLimit () = !eprover_time; 

90 

91 
val keep_atp_input = ref false; 

92 
val fol_keep_types = ResClause.keep_types; 

93 
val hol_full_types = ResHolClause.full_types; 

94 
val hol_partial_types = ResHolClause.partial_types; 

95 
val hol_const_types_only = ResHolClause.const_types_only; 

96 
val hol_no_types = ResHolClause.no_types; 

97 
fun hol_typ_level () = ResHolClause.find_typ_level (); 

98 
fun is_typed_hol () = 

99 
let val tp_level = hol_typ_level() 

100 
in 

101 
not (tp_level = ResHolClause.T_NONE) 

102 
end; 

103 
val include_combS = ResHolClause.include_combS; 

104 
val include_min_comb = ResHolClause.include_min_comb; 

105 

106 
fun atp_input_file () = 

107 
let val file = !problem_name 

108 
in 

109 
if !destdir = "" then File.platform_path (File.tmp_path (Path.basic file)) 

110 
else if File.exists (File.unpack_platform_path (!destdir)) 

111 
then !destdir ^ "/" ^ file 

112 
else error ("No such directory: " ^ !destdir) 

113 
end; 

114 

115 
val include_simpset = ref false; 

116 
val include_claset = ref false; 

117 
val include_atpset = ref true; 

118 
val add_simpset = (fn () => include_simpset:=true); 

119 
val add_claset = (fn () => include_claset:=true); 

120 
val add_clasimp = (fn () => include_simpset:=true;include_claset:=true); 

121 
val add_atpset = (fn () => include_atpset:=true); 

122 
val rm_simpset = (fn () => include_simpset:=false); 

123 
val rm_claset = (fn () => include_claset:=false); 

124 
val rm_clasimp = (fn () => include_simpset:=false;include_claset:=false); 

125 
val rm_atpset = (fn () => include_atpset:=false); 

126 

127 
(*** paths for HOL helper files ***) 

128 
fun full_typed_comb_inclS () = 

129 
helper_path "E_HOME" "additionals/full_comb_inclS" 

130 
handle _ => helper_path "VAMPIRE_HOME" "additionals/full_comb_inclS"; 

131 

132 
fun full_typed_comb_noS () = 

133 
helper_path "E_HOME" "additionals/full_comb_noS" 

134 
handle _ => helper_path "VAMPIRE_HOME" "additionals/full_comb_noS"; 

135 

136 
fun partial_typed_comb_inclS () = 

137 
helper_path "E_HOME" "additionals/par_comb_inclS" 

138 
handle _ => helper_path "VAMPIRE_HOME" "additionals/par_comb_inclS"; 

139 

140 
fun partial_typed_comb_noS () = 

141 
helper_path "E_HOME" "additionals/par_comb_noS" 

142 
handle _ => helper_path "VAMPIRE_HOME" "additionals/par_comb_noS"; 

143 

144 
fun const_typed_comb_inclS () = 

145 
helper_path "E_HOME" "additionals/const_comb_inclS" 

146 
handle _ => helper_path "VAMPIRE_HOME" "additionals/const_comb_inclS"; 

147 

148 
fun const_typed_comb_noS () = 

149 
helper_path "E_HOME" "additionals/const_comb_noS" 

150 
handle _ => helper_path "VAMPIRE_HOME" "additionals/const_comb_noS"; 

151 

152 
fun untyped_comb_inclS () = 

153 
helper_path "E_HOME" "additionals/u_comb_inclS" 

154 
handle _ => helper_path "VAMPIRE_HOME" "additionals/u_comb_inclS"; 

155 

156 
fun untyped_comb_noS () = 

157 
helper_path "E_HOME" "additionals/u_comb_noS" 

158 
handle _ => helper_path "VAMPIRE_HOME" "additionals/u_comb_noS"; 

159 

160 
fun full_typed_HOL_helper1 () = 

161 
helper_path "E_HOME" "additionals/full_helper1" 

162 
handle _ => helper_path "VAMPIRE_HOME" "additionals/full_helper1"; 

163 

164 
fun partial_typed_HOL_helper1 () = 

165 
helper_path "E_HOME" "additionals/par_helper1" 

166 
handle _ => helper_path "VAMPIRE_HOME" "additionals/par_helper1"; 

167 

168 
fun const_typed_HOL_helper1 () = 

169 
helper_path "E_HOME" "additionals/const_helper1" 

170 
handle _ => helper_path "VAMPIRE_HOME" "additionals/const_helper1"; 

171 

172 
fun untyped_HOL_helper1 () = 

173 
helper_path "E_HOME" "additionals/u_helper1" 

174 
handle _ => helper_path "VAMPIRE_HOME" "additionals/u_helper1"; 

175 

176 
fun get_full_typed_helpers () = 

177 
(full_typed_HOL_helper1 (), full_typed_comb_noS (), full_typed_comb_inclS ()); 

178 

179 
fun get_partial_typed_helpers () = 

180 
(partial_typed_HOL_helper1 (), partial_typed_comb_noS (), partial_typed_comb_inclS ()); 

181 

182 
fun get_const_typed_helpers () = 

183 
(const_typed_HOL_helper1 (), const_typed_comb_noS (), const_typed_comb_inclS ()); 

184 

185 
fun get_untyped_helpers () = 

186 
(untyped_HOL_helper1 (), untyped_comb_noS (), untyped_comb_inclS ()); 

187 

188 
fun get_all_helpers () = 

189 
(get_full_typed_helpers (), get_partial_typed_helpers (), get_const_typed_helpers (), get_untyped_helpers ()); 

190 

191 

192 
(**** relevance filter ****) 

193 
val run_relevance_filter = ref true; 

194 

195 
(******************************************************************) 

196 
(* detect whether a given problem (clauses) is FOL/HOL/HOLC/HOLCS *) 

197 
(******************************************************************) 

198 

199 
datatype logic = FOL  HOL  HOLC  HOLCS; 

200 

201 
fun string_of_logic FOL = "FOL" 

202 
 string_of_logic HOL = "HOL" 

203 
 string_of_logic HOLC = "HOLC" 

204 
 string_of_logic HOLCS = "HOLCS"; 

205 

206 

207 
fun is_fol_logic FOL = true 

208 
 is_fol_logic _ = false 

209 

210 

211 
(*HOLCS will not occur here*) 

212 
fun upgrade_lg HOLC _ = HOLC 

213 
 upgrade_lg HOL HOLC = HOLC 

214 
 upgrade_lg HOL _ = HOL 

215 
 upgrade_lg FOL lg = lg; 

216 

217 
(* check types *) 

218 
fun has_bool (Type("bool",_)) = true 

219 
 has_bool (Type(_, Ts)) = exists has_bool Ts 

220 
 has_bool _ = false; 

221 

222 
fun has_bool_arg tp = 

223 
let val (targs,tr) = strip_type tp 

224 
in 

225 
exists has_bool targs 

226 
end; 

227 

228 
fun is_fn_tp (Type("fun",_)) = true 

229 
 is_fn_tp _ = false; 

230 

231 

232 
exception FN_LG of term; 

233 

234 
fun fn_lg (t as Const(f,tp)) (lg,seen) = 

235 
if has_bool tp then (upgrade_lg HOL lg, t ins seen) else (lg, t ins seen) 

236 
 fn_lg (t as Free(f,tp)) (lg,seen) = 

237 
if has_bool tp then (upgrade_lg HOL lg, t ins seen) else (lg, t ins seen) 

238 
 fn_lg (t as Var(f,tp)) (lg,seen) = 

239 
if is_fn_tp tp orelse has_bool tp then (upgrade_lg HOL lg,t ins seen) 

240 
else (lg,t ins seen) 

241 
 fn_lg (t as Abs(_,_,_)) (lg,seen) = (upgrade_lg HOLC lg,t ins seen) 

242 
 fn_lg f _ = raise FN_LG(f); 

243 

244 

245 
fun term_lg [] (lg,seen) = (lg,seen) 

246 
 term_lg (tm::tms) (FOL,seen) = 

247 
let val (f,args) = strip_comb tm 

248 
val (lg',seen') = if f mem seen then (FOL,seen) 

249 
else fn_lg f (FOL,seen) 

250 

251 
in 

252 
term_lg (args@tms) (lg',seen') 

253 
end 

254 
 term_lg _ (lg,seen) = (lg,seen) 

255 

256 
exception PRED_LG of term; 

257 

258 
fun pred_lg (t as Const(P,tp)) (lg,seen)= 

259 
if has_bool_arg tp then (upgrade_lg HOL lg, t ins seen) else (lg,t ins seen) 

260 
 pred_lg (t as Free(P,tp)) (lg,seen) = 

261 
if has_bool_arg tp then (upgrade_lg HOL lg, t ins seen) else (lg,t ins seen) 

262 
 pred_lg (t as Var(_,_)) (lg,seen) = (upgrade_lg HOL lg, t ins seen) 

263 
 pred_lg P _ = raise PRED_LG(P); 

264 

265 

266 
fun lit_lg (Const("Not",_) $ P) (lg,seen) = lit_lg P (lg,seen) 

267 
 lit_lg P (lg,seen) = 

268 
let val (pred,args) = strip_comb P 

269 
val (lg',seen') = if pred mem seen then (lg,seen) 

270 
else pred_lg pred (lg,seen) 

271 
in 

272 
term_lg args (lg',seen') 

273 
end; 

274 

275 
fun lits_lg [] (lg,seen) = (lg,seen) 

276 
 lits_lg (lit::lits) (FOL,seen) = 

277 
lits_lg lits (lit_lg lit (FOL,seen)) 

278 
 lits_lg lits (lg,seen) = (lg,seen); 

279 

280 

281 
fun logic_of_clause tm (lg,seen) = 

282 
let val tm' = HOLogic.dest_Trueprop tm 

283 
val disjs = HOLogic.dest_disj tm' 

284 
in 

285 
lits_lg disjs (lg,seen) 

286 
end; 

287 

288 
fun lits_lg [] (lg,seen) = (lg,seen) 

289 
 lits_lg (lit::lits) (FOL,seen) = 

290 
lits_lg lits (lit_lg lit (FOL,seen)) 

291 
 lits_lg lits (lg,seen) = (lg,seen); 

292 

293 

294 
fun logic_of_clause tm (lg,seen) = 

295 
let val tm' = HOLogic.dest_Trueprop tm 

296 
val disjs = HOLogic.dest_disj tm' 

297 
in 

298 
lits_lg disjs (lg,seen) 

299 
end; 

300 

301 
fun logic_of_clauses [] (lg,seen) = (lg,seen) 

302 
 logic_of_clauses (cls::clss) (FOL,seen) = 

303 
logic_of_clauses clss (logic_of_clause cls (FOL,seen)) 

304 
 logic_of_clauses (cls::clss) (lg,seen) = (lg,seen); 

305 

306 
fun logic_of_nclauses [] (lg,seen) = (lg,seen) 

307 
 logic_of_nclauses (cls::clss) (FOL,seen) = 

308 
logic_of_nclauses clss (logic_of_clauses (snd cls) (FOL,seen)) 

309 
 logic_of_nclauses clss (lg,seen) = (lg,seen); 

310 

311 
fun problem_logic (goal_cls,rules_cls) = 

312 
let val (lg1,seen1) = logic_of_clauses goal_cls (FOL,[]) 

313 
val (lg2,seen2) = logic_of_nclauses rules_cls (lg1,seen1) 

314 
in 

315 
lg2 

316 
end; 

317 

318 
fun problem_logic_goals_aux [] (lg,seen) = lg 

319 
 problem_logic_goals_aux (subgoal::subgoals) (lg,seen) = 

320 
problem_logic_goals_aux subgoals (logic_of_clauses subgoal (lg,seen)); 

321 

322 
fun problem_logic_goals subgoals = problem_logic_goals_aux subgoals (FOL,[]); 

323 

324 

325 
(***************************************************************) 

326 
(* ATP invocation methods setup *) 

327 
(***************************************************************) 

328 

329 

330 
(**** proverspecific format: TPTP ****) 

331 

332 

333 
fun cnf_hyps_thms ctxt = 

334 
let val ths = ProofContext.prems_of ctxt 

335 
in 

336 
ResClause.union_all (map ResAxioms.skolem_thm ths) 

337 
end; 

338 

339 

340 
(**** write to files ****) 

341 

342 
datatype mode = Auto  Fol  Hol; 

343 

344 
fun tptp_writer logic goals filename (axioms,classrels,arities) = 

345 
if is_fol_logic logic then ResClause.tptp_write_file goals filename (axioms, classrels, arities) 

346 
else 

347 
ResHolClause.tptp_write_file goals filename (axioms, classrels, arities) (get_all_helpers()); 

348 

349 

350 
fun write_subgoal_file mode ctxt conjectures user_thms n = 

351 
let val conj_cls = map prop_of (make_clauses conjectures) 

352 
val hyp_cls = map prop_of (cnf_hyps_thms ctxt) 

353 
val goal_cls = conj_cls@hyp_cls 

354 
val user_rules = map ResAxioms.pairname user_thms 

355 
val (names_arr,axclauses_as_tms) = ResClasimp.get_clasimp_atp_lemmas ctxt (goal_cls) user_rules (!include_claset,!include_simpset,!include_atpset) (!run_relevance_filter) 

356 
val thy = ProofContext.theory_of ctxt 

357 
val prob_logic = case mode of Auto => problem_logic_goals [goal_cls] 

358 
 Fol => FOL 

359 
 Hol => HOL 

360 
val keep_types = if is_fol_logic prob_logic then !fol_keep_types else is_typed_hol () 

361 
val classrel_clauses = if keep_types then ResClause.classrel_clauses_thy thy else [] 

362 
val arity_clauses = if keep_types then ResClause.arity_clause_thy thy else [] 

363 
val writer = tptp_writer 

364 
val file = atp_input_file() 

365 
in 

366 
(writer prob_logic goal_cls file (axclauses_as_tms,classrel_clauses,arity_clauses); 

367 
warning ("Writing to " ^ file); 

368 
file) 

369 
end; 

370 

371 

372 
(**** remove tmp files ****) 

373 
fun cond_rm_tmp file = 

374 
if !keep_atp_input then warning "ATP input kept..." 

375 
else if !destdir <> "" then warning ("ATP input kept in directory " ^ (!destdir)) 

376 
else (warning "deleting ATP inputs..."; OS.FileSys.remove file); 

377 

378 

379 
(****** setup ATPs as Isabelle methods ******) 

380 
fun atp_meth' tac ths ctxt = 

381 
Method.SIMPLE_METHOD' HEADGOAL 

382 
(tac ctxt ths); 

383 

384 
fun atp_meth tac ths ctxt = 

385 
let val thy = ProofContext.theory_of ctxt 

386 
val _ = ResClause.init thy 

387 
val _ = ResHolClause.init thy 

388 
in 

389 
atp_meth' tac ths ctxt 

390 
end; 

391 

392 
fun atp_method tac = Method.thms_ctxt_args (atp_meth tac); 

393 

394 
(***************************************************************) 

395 
(* automatic ATP invocation *) 

396 
(***************************************************************) 

397 

17306  398 
(* call prover with settings and problem file for the current subgoal *) 
17764  399 
fun watcher_call_provers sign sg_terms (childin, childout, pid) = 
16802
6eeee59dac4c
use Toplevel.print_state_hook instead of adhoc Proof.atp_hook;
wenzelm
parents:
16767
diff
changeset

400 
let 
17422  401 
fun make_atp_list [] n = [] 
17717  402 
 make_atp_list (sg_term::xs) n = 
16802
6eeee59dac4c
use Toplevel.print_state_hook instead of adhoc Proof.atp_hook;
wenzelm
parents:
16767
diff
changeset

403 
let 
17717  404 
val probfile = prob_pathname n 
17690
8ba7c3cd24a8
time limit option; fixed bug concerning first line of ATP output
paulson
parents:
17525
diff
changeset

405 
val time = Int.toString (!time_limit) 
16802
6eeee59dac4c
use Toplevel.print_state_hook instead of adhoc Proof.atp_hook;
wenzelm
parents:
16767
diff
changeset

406 
in 
18680  407 
Output.debug ("problem file in watcher_call_provers is " ^ probfile); 
17317
3f12de2e2e6e
IsabelleATP link: sortable axiom names; no spaces in switches; general tidying
paulson
parents:
17306
diff
changeset

408 
(*Avoid command arguments containing spaces: Poly/ML and SML/NJ 
3f12de2e2e6e
IsabelleATP link: sortable axiom names; no spaces in switches; general tidying
paulson
parents:
17306
diff
changeset

409 
versions of Unix.execute treat them differently!*) 
17764  410 
(*options are separated by Watcher.setting_sep, currently #"%"*) 
17306  411 
if !prover = "spass" 
16802
6eeee59dac4c
use Toplevel.print_state_hook instead of adhoc Proof.atp_hook;
wenzelm
parents:
16767
diff
changeset

412 
then 
18700  413 
let val baseopts = "%PGiven=0%PProblem=0%Splits=0%FullRed=0%DocProof%TimeLimit=" ^ time 
414 
val infopts = 

17484
f6a225f97f0a
simplification of the IsabelleATP code; hooks for batch generation of problems
paulson
parents:
17435
diff
changeset

415 
if !AtpCommunication.reconstruct 
18700  416 
(*Proof reconstruction needs a limited set of inf rules*) 
417 
then space_implode "%" (!custom_spass) 

418 
else "Auto%SOS=1" 

419 
val spass = helper_path "SPASS_HOME" "SPASS" 

420 
in 

421 
([("spass", spass, infopts ^ baseopts, probfile)] @ 

18798  422 
make_atp_list xs (n+1)) 
16802
6eeee59dac4c
use Toplevel.print_state_hook instead of adhoc Proof.atp_hook;
wenzelm
parents:
16767
diff
changeset

423 
end 
17306  424 
else if !prover = "vampire" 
17235
8e55ad29b690
Added ECommunication.ML and modified res_atp.ML, Reconstruction.thy, and
quigley
parents:
17234
diff
changeset

425 
then 
17819  426 
let val vampire = helper_path "VAMPIRE_HOME" "vampire" 
16802
6eeee59dac4c
use Toplevel.print_state_hook instead of adhoc Proof.atp_hook;
wenzelm
parents:
16767
diff
changeset

427 
in 
17772
818cec5f82a4
major simplification: removal of the goalstring argument
paulson
parents:
17764
diff
changeset

428 
([("vampire", vampire, "m 100000%t " ^ time, probfile)] @ 
18798  429 
make_atp_list xs (n+1)) (*BEWARE! spaces in options!*) 
16802
6eeee59dac4c
use Toplevel.print_state_hook instead of adhoc Proof.atp_hook;
wenzelm
parents:
16767
diff
changeset

430 
end 
17306  431 
else if !prover = "E" 
432 
then 

17819  433 
let val Eprover = helper_path "E_HOME" "eproof" 
17306  434 
in 
17772
818cec5f82a4
major simplification: removal of the goalstring argument
paulson
parents:
17764
diff
changeset

435 
([("E", Eprover, 
17690
8ba7c3cd24a8
time limit option; fixed bug concerning first line of ATP output
paulson
parents:
17525
diff
changeset

436 
"tptpin%l5%xAuto%tAuto%cpulimit=" ^ time, 
17422  437 
probfile)] @ 
18798  438 
make_atp_list xs (n+1)) 
17306  439 
end 
440 
else error ("Invalid prover name: " ^ !prover) 

16802
6eeee59dac4c
use Toplevel.print_state_hook instead of adhoc Proof.atp_hook;
wenzelm
parents:
16767
diff
changeset

441 
end 
15452  442 

17422  443 
val atp_list = make_atp_list sg_terms 1 
16802
6eeee59dac4c
use Toplevel.print_state_hook instead of adhoc Proof.atp_hook;
wenzelm
parents:
16767
diff
changeset

444 
in 
6eeee59dac4c
use Toplevel.print_state_hook instead of adhoc Proof.atp_hook;
wenzelm
parents:
16767
diff
changeset

445 
Watcher.callResProvers(childout,atp_list); 
18680  446 
Output.debug "Sent commands to watcher!" 
16802
6eeee59dac4c
use Toplevel.print_state_hook instead of adhoc Proof.atp_hook;
wenzelm
parents:
16767
diff
changeset

447 
end 
16357  448 

17717  449 
(*We write out problem files for each subgoal. Argument pf generates filenames, 
18986  450 
and allows the suppression of the suffix "_1" in problemgeneration mode. 
451 
FIXME: does not cope with &&, and it isn't easy because one could have multiple 

452 
subgoals, each involving &&.*) 

17717  453 
fun write_problem_files pf (ctxt,th) = 
18753
aa82bd41555d
ResClasimp.get_clasimp_lemmas now takes all subgoals rather than only the first
paulson
parents:
18700
diff
changeset

454 
let val goals = Thm.prems_of th 
19194  455 
val _ = Output.debug ("number of subgoals = " ^ Int.toString (length goals)) 
456 
val (names_arr, axclauses_as_terms) = ResClasimp.get_clasimp_atp_lemmas ctxt goals [] (true,true,true) (!run_relevance_filter) (* no user supplied rules here, because no user invocation *) 

457 
val _ = Output.debug ("claset, simprules and atprules total clauses = " ^ 

458 
Int.toString (Array.length names_arr)) 

17717  459 
val thy = ProofContext.theory_of ctxt 
19194  460 
fun get_neg_subgoals n = 
461 
if n=0 then [] 

462 
else 

463 
let val st = Seq.hd (EVERY' 

464 
[rtac ccontr, ObjectLogic.atomize_tac, skolemize_tac] n th) 

465 
val negs = Option.valOf (metahyps_thms n st) 

466 
val negs_clauses = map prop_of (make_clauses negs) 

467 
in 

468 
negs_clauses::(get_neg_subgoals (n  1)) 

469 
end 

470 
val neg_subgoals = get_neg_subgoals (length goals) 

471 
val goals_logic = problem_logic_goals neg_subgoals 

472 
val keep_types = if is_fol_logic goals_logic then !ResClause.keep_types else is_typed_hol () 

473 
val classrel_clauses = if keep_types then ResClause.classrel_clauses_thy thy else [] 

18680  474 
val _ = Output.debug ("classrel clauses = " ^ Int.toString (length classrel_clauses)) 
19194  475 
val arity_clauses = if keep_types then ResClause.arity_clause_thy thy else [] 
18680  476 
val _ = Output.debug ("arity clauses = " ^ Int.toString (length arity_clauses)) 
19194  477 
val writer = (*if !prover ~= "spass" then *)tptp_writer 
478 
fun write_all [] _ = [] 

479 
 write_all (subgoal::subgoals) k = 

480 
(writer goals_logic subgoal (pf k) (axclauses_as_terms,classrel_clauses,arity_clauses); pf k):: (write_all subgoals (k  1)) 

481 
in 

482 
(write_all neg_subgoals (length goals), names_arr) 

483 
end; 

15644  484 

17775  485 
val last_watcher_pid = ref (NONE : (TextIO.instream * TextIO.outstream * 
486 
Posix.Process.pid * string list) option); 

487 

488 
fun kill_last_watcher () = 

489 
(case !last_watcher_pid of 

490 
NONE => () 

491 
 SOME (_, childout, pid, files) => 

18680  492 
(Output.debug ("Killing old watcher, pid = " ^ string_of_pid pid); 
17775  493 
Watcher.killWatcher pid; 
494 
ignore (map (try OS.FileSys.remove) files))) 

18680  495 
handle OS.SysErr _ => Output.debug "Attempt to kill watcher failed"; 
17525
ae5bb6001afb
tidying, and support for axclass/classrel clauses
paulson
parents:
17502
diff
changeset

496 

ae5bb6001afb
tidying, and support for axclass/classrel clauses
paulson
parents:
17502
diff
changeset

497 
(*writes out the current clasimpset to a tptp file; 
ae5bb6001afb
tidying, and support for axclass/classrel clauses
paulson
parents:
17502
diff
changeset

498 
turns off xsymbol at start of function, restoring it at end *) 
17484
f6a225f97f0a
simplification of the IsabelleATP code; hooks for batch generation of problems
paulson
parents:
17435
diff
changeset

499 
val isar_atp = setmp print_mode [] 
17717  500 
(fn (ctxt, th) => 
501 
if Thm.no_prems th then () 

16802
6eeee59dac4c
use Toplevel.print_state_hook instead of adhoc Proof.atp_hook;
wenzelm
parents:
16767
diff
changeset

502 
else 
6eeee59dac4c
use Toplevel.print_state_hook instead of adhoc Proof.atp_hook;
wenzelm
parents:
16767
diff
changeset

503 
let 
17775  504 
val _ = kill_last_watcher() 
19194  505 
val (files,names_arr) = write_problem_files prob_pathname (ctxt,th) 
506 
val (childin, childout, pid) = Watcher.createWatcher (th, names_arr) 

15608  507 
in 
17772
818cec5f82a4
major simplification: removal of the goalstring argument
paulson
parents:
17764
diff
changeset

508 
last_watcher_pid := SOME (childin, childout, pid, files); 
18680  509 
Output.debug ("problem files: " ^ space_implode ", " files); 
510 
Output.debug ("pid: " ^ string_of_pid pid); 

17717  511 
watcher_call_provers (sign_of_thm th) (Thm.prems_of th) (childin, childout, pid) 
16802
6eeee59dac4c
use Toplevel.print_state_hook instead of adhoc Proof.atp_hook;
wenzelm
parents:
16767
diff
changeset

512 
end); 
15608  513 

17422  514 
val isar_atp_writeonly = setmp print_mode [] 
17717  515 
(fn (ctxt,th) => 
516 
if Thm.no_prems th then () 

517 
else 

518 
let val pf = if Thm.nprems_of th = 1 then probfile_nosuffix 

519 
else prob_pathname 

520 
in ignore (write_problem_files pf (ctxt,th)) end); 

15452  521 

16357  522 

16802
6eeee59dac4c
use Toplevel.print_state_hook instead of adhoc Proof.atp_hook;
wenzelm
parents:
16767
diff
changeset

523 
(** the Isar toplevel hook **) 
6eeee59dac4c
use Toplevel.print_state_hook instead of adhoc Proof.atp_hook;
wenzelm
parents:
16767
diff
changeset

524 

17091  525 
val invoke_atp = Toplevel.unknown_proof o Toplevel.keep (fn state => 
16802
6eeee59dac4c
use Toplevel.print_state_hook instead of adhoc Proof.atp_hook;
wenzelm
parents:
16767
diff
changeset

526 
let 
17091  527 
val proof = Toplevel.proof_of state 
18680  528 
val (ctxt, (_, goal)) = Proof.get_goal proof; 
16802
6eeee59dac4c
use Toplevel.print_state_hook instead of adhoc Proof.atp_hook;
wenzelm
parents:
16767
diff
changeset

529 
val thy = ProofContext.theory_of ctxt; 
6eeee59dac4c
use Toplevel.print_state_hook instead of adhoc Proof.atp_hook;
wenzelm
parents:
16767
diff
changeset

530 
in 
18680  531 
Output.debug ("subgoals in isar_atp:\n" ^ 
17091  532 
Pretty.string_of (ProofContext.pretty_term ctxt 
533 
(Logic.mk_conjunction_list (Thm.prems_of goal)))); 

18680  534 
Output.debug ("current theory: " ^ Context.theory_name thy); 
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
17091
diff
changeset

535 
hook_count := !hook_count +1; 
18680  536 
Output.debug ("in hook for time: " ^ Int.toString (!hook_count)); 
16925
0fd7b1438d28
simpler variable names, and no types for monomorphic constants
paulson
parents:
16904
diff
changeset

537 
ResClause.init thy; 
19194  538 
ResHolClause.init thy; 
17690
8ba7c3cd24a8
time limit option; fixed bug concerning first line of ATP output
paulson
parents:
17525
diff
changeset

539 
if !destdir = "" andalso !time_limit > 0 then isar_atp (ctxt, goal) 
17502  540 
else isar_atp_writeonly (ctxt, goal) 
16802
6eeee59dac4c
use Toplevel.print_state_hook instead of adhoc Proof.atp_hook;
wenzelm
parents:
16767
diff
changeset

541 
end); 
16357  542 

17091  543 
val call_atpP = 
17746  544 
OuterSyntax.command 
17091  545 
"ProofGeneral.call_atp" 
546 
"call automatic theorem provers" 

547 
OuterKeyword.diag 

548 
(Scan.succeed (Toplevel.no_timing o invoke_atp)); 

549 

550 
val _ = OuterSyntax.add_parsers [call_atpP]; 

551 

15347  552 
end; 