|
1 (* ID: $Id$ |
|
2 Author: Jia Meng |
|
3 *) |
|
4 |
|
5 |
|
6 structure ResAtpMethods = |
|
7 |
|
8 struct |
|
9 |
|
10 |
|
11 val vampire_time = ref 60; |
|
12 val eprover_time = ref 60; |
|
13 |
|
14 fun run_vampire time = |
|
15 if (time >0) then vampire_time:= time |
|
16 else vampire_time:=60; |
|
17 |
|
18 fun run_eprover time = |
|
19 if (time > 0) then eprover_time:= time |
|
20 else eprover_time:=60; |
|
21 |
|
22 fun vampireLimit () = !vampire_time; |
|
23 fun eproverLimit () = !eprover_time; |
|
24 |
|
25 |
|
26 |
|
27 (* convert the negated 1st subgoal into CNF, write to files and call an ATP oracle *) |
|
28 fun res_atp_tac res_atp_oracle timeLimit ctxt files tfrees n thm = |
|
29 SELECT_GOAL |
|
30 ((EVERY1 [rtac ccontr,ObjectLogic.atomize_tac, skolemize_tac, |
|
31 METAHYPS(fn negs => |
|
32 HEADGOAL(Tactic.rtac |
|
33 (res_atp_oracle (ProofContext.theory_of ctxt) |
|
34 ((ResAtpSetup.tptp_form (make_clauses (map make_nnf negs)) n tfrees)::files, timeLimit))))]) handle Fail _ => no_tac) n thm; |
|
35 |
|
36 |
|
37 (* vampire_tac and eprover_tac *) |
|
38 val vampire_tac = res_atp_tac vampire_oracle (!vampire_time); |
|
39 |
|
40 val eprover_tac = res_atp_tac eprover_oracle (!eprover_time); |
|
41 |
|
42 |
|
43 val ResAtps_setup = [Method.add_methods |
|
44 [("vampire", ResAtpSetup.atp_method vampire_tac, "A Vampire method"), |
|
45 ("eprover", ResAtpSetup.atp_method eprover_tac, "A E prover method")]]; |
|
46 |
|
47 |
|
48 |
|
49 |
|
50 end |