1 (* ID: $Id$ |
|
2 Author: Jia Meng, NICTA |
|
3 *) |
|
4 |
|
5 signature RES_ATP_METHODS = |
|
6 sig |
|
7 val vampire_tac: Proof.context -> thm list -> int -> tactic |
|
8 val eprover_tac: Proof.context -> thm list -> int -> tactic |
|
9 val spass_tac: Proof.context -> thm list -> int -> tactic |
|
10 val vampireF_tac: Proof.context -> thm list -> int -> tactic |
|
11 val vampireH_tac: Proof.context -> thm list -> int -> tactic |
|
12 val eproverF_tac: Proof.context -> thm list -> int -> tactic |
|
13 val eproverH_tac: Proof.context -> thm list -> int -> tactic |
|
14 val spassF_tac: Proof.context -> thm list -> int -> tactic |
|
15 val spassH_tac: Proof.context -> thm list -> int -> tactic |
|
16 val setup: theory -> theory |
|
17 end |
|
18 |
|
19 structure ResAtpMethods = |
|
20 struct |
|
21 |
|
22 (* convert the negated 1st subgoal into CNF, write to file and call an ATP oracle *) |
|
23 fun res_atp_tac dfg res_atp_oracle mode timeLimit ctxt user_thms i st = |
|
24 (EVERY' |
|
25 [rtac ccontr, |
|
26 ObjectLogic.atomize_prems_tac, |
|
27 Meson.skolemize_tac, |
|
28 METAHYPS (fn negs => |
|
29 HEADGOAL (Tactic.rtac |
|
30 (res_atp_oracle |
|
31 (ResAtp.write_subgoal_file dfg mode ctxt negs user_thms i, timeLimit))))] i st) handle Fail _ => Seq.empty; |
|
32 |
|
33 |
|
34 (* vampire, eprover and spass tactics *) |
|
35 |
|
36 fun vampire_tac st = res_atp_tac false vampire_oracle ResAtp.Auto (!ResAtp.time_limit) st; |
|
37 fun eprover_tac st = res_atp_tac false eprover_oracle ResAtp.Auto (!ResAtp.time_limit) st; |
|
38 fun spass_tac st = res_atp_tac true spass_oracle ResAtp.Auto (!ResAtp.time_limit) st; |
|
39 |
|
40 |
|
41 fun vampireF_tac st = res_atp_tac false vampire_oracle ResAtp.Fol (!ResAtp.time_limit) st; |
|
42 |
|
43 fun vampireH_tac st = res_atp_tac false vampire_oracle ResAtp.Hol (!ResAtp.time_limit) st; |
|
44 |
|
45 fun eproverF_tac st = res_atp_tac false eprover_oracle ResAtp.Fol (!ResAtp.time_limit) st; |
|
46 |
|
47 fun eproverH_tac st = res_atp_tac false eprover_oracle ResAtp.Hol (!ResAtp.time_limit) st; |
|
48 |
|
49 fun spassF_tac st = res_atp_tac true spass_oracle ResAtp.Fol (!ResAtp.time_limit) st; |
|
50 |
|
51 fun spassH_tac st = res_atp_tac true spass_oracle ResAtp.Hol (!ResAtp.time_limit) st; |
|
52 |
|
53 |
|
54 fun atp_method tac = |
|
55 Method.thms_ctxt_args (fn ths => fn ctxt => Method.SIMPLE_METHOD' (tac ctxt ths)); |
|
56 |
|
57 val setup = |
|
58 Method.add_methods |
|
59 [("vampireF", atp_method vampireF_tac, "Vampire for FOL problems"), |
|
60 ("eproverF", atp_method eproverF_tac, "E prover for FOL problems"), |
|
61 ("vampireH", atp_method vampireH_tac, "Vampire for HOL problems"), |
|
62 ("eproverH", atp_method eproverH_tac, "E prover for HOL problems"), |
|
63 ("eprover", atp_method eprover_tac, "E prover for FOL and HOL problems"), |
|
64 ("vampire", atp_method vampire_tac, "Vampire for FOL and HOL problems"), |
|
65 ("spassF", atp_method spassF_tac, "SPASS for FOL problems"), |
|
66 ("spassH", atp_method spassH_tac, "SPASS for HOL problems"), |
|
67 ("spass", atp_method spass_tac, "SPASS for FOL and HOL problems")]; |
|
68 |
|
69 end; |
|