author | berghofe |
Mon, 05 Dec 2005 00:38:07 +0100 | |
changeset 18349 | 58de95a16d3c |
parent 18271 | 0e9a851db989 |
child 18708 | 4b3dadb4fe33 |
permissions | -rw-r--r-- |
17905
1574533861b1
Added files in order to use external ATPs as oracles and invoke these ATPs by calling Isabelle methods (currently "vampire" and "eprover").
mengj
parents:
diff
changeset
|
1 |
(* ID: $Id$ |
17907 | 2 |
Author: Jia Meng, NICTA |
17905
1574533861b1
Added files in order to use external ATPs as oracles and invoke these ATPs by calling Isabelle methods (currently "vampire" and "eprover").
mengj
parents:
diff
changeset
|
3 |
*) |
1574533861b1
Added files in order to use external ATPs as oracles and invoke these ATPs by calling Isabelle methods (currently "vampire" and "eprover").
mengj
parents:
diff
changeset
|
4 |
|
1574533861b1
Added files in order to use external ATPs as oracles and invoke these ATPs by calling Isabelle methods (currently "vampire" and "eprover").
mengj
parents:
diff
changeset
|
5 |
|
1574533861b1
Added files in order to use external ATPs as oracles and invoke these ATPs by calling Isabelle methods (currently "vampire" and "eprover").
mengj
parents:
diff
changeset
|
6 |
structure ResAtpMethods = |
1574533861b1
Added files in order to use external ATPs as oracles and invoke these ATPs by calling Isabelle methods (currently "vampire" and "eprover").
mengj
parents:
diff
changeset
|
7 |
|
1574533861b1
Added files in order to use external ATPs as oracles and invoke these ATPs by calling Isabelle methods (currently "vampire" and "eprover").
mengj
parents:
diff
changeset
|
8 |
struct |
1574533861b1
Added files in order to use external ATPs as oracles and invoke these ATPs by calling Isabelle methods (currently "vampire" and "eprover").
mengj
parents:
diff
changeset
|
9 |
|
1574533861b1
Added files in order to use external ATPs as oracles and invoke these ATPs by calling Isabelle methods (currently "vampire" and "eprover").
mengj
parents:
diff
changeset
|
10 |
|
1574533861b1
Added files in order to use external ATPs as oracles and invoke these ATPs by calling Isabelle methods (currently "vampire" and "eprover").
mengj
parents:
diff
changeset
|
11 |
val vampire_time = ref 60; |
1574533861b1
Added files in order to use external ATPs as oracles and invoke these ATPs by calling Isabelle methods (currently "vampire" and "eprover").
mengj
parents:
diff
changeset
|
12 |
val eprover_time = ref 60; |
1574533861b1
Added files in order to use external ATPs as oracles and invoke these ATPs by calling Isabelle methods (currently "vampire" and "eprover").
mengj
parents:
diff
changeset
|
13 |
|
1574533861b1
Added files in order to use external ATPs as oracles and invoke these ATPs by calling Isabelle methods (currently "vampire" and "eprover").
mengj
parents:
diff
changeset
|
14 |
fun run_vampire time = |
1574533861b1
Added files in order to use external ATPs as oracles and invoke these ATPs by calling Isabelle methods (currently "vampire" and "eprover").
mengj
parents:
diff
changeset
|
15 |
if (time >0) then vampire_time:= time |
1574533861b1
Added files in order to use external ATPs as oracles and invoke these ATPs by calling Isabelle methods (currently "vampire" and "eprover").
mengj
parents:
diff
changeset
|
16 |
else vampire_time:=60; |
1574533861b1
Added files in order to use external ATPs as oracles and invoke these ATPs by calling Isabelle methods (currently "vampire" and "eprover").
mengj
parents:
diff
changeset
|
17 |
|
1574533861b1
Added files in order to use external ATPs as oracles and invoke these ATPs by calling Isabelle methods (currently "vampire" and "eprover").
mengj
parents:
diff
changeset
|
18 |
fun run_eprover time = |
1574533861b1
Added files in order to use external ATPs as oracles and invoke these ATPs by calling Isabelle methods (currently "vampire" and "eprover").
mengj
parents:
diff
changeset
|
19 |
if (time > 0) then eprover_time:= time |
1574533861b1
Added files in order to use external ATPs as oracles and invoke these ATPs by calling Isabelle methods (currently "vampire" and "eprover").
mengj
parents:
diff
changeset
|
20 |
else eprover_time:=60; |
1574533861b1
Added files in order to use external ATPs as oracles and invoke these ATPs by calling Isabelle methods (currently "vampire" and "eprover").
mengj
parents:
diff
changeset
|
21 |
|
1574533861b1
Added files in order to use external ATPs as oracles and invoke these ATPs by calling Isabelle methods (currently "vampire" and "eprover").
mengj
parents:
diff
changeset
|
22 |
fun vampireLimit () = !vampire_time; |
1574533861b1
Added files in order to use external ATPs as oracles and invoke these ATPs by calling Isabelle methods (currently "vampire" and "eprover").
mengj
parents:
diff
changeset
|
23 |
fun eproverLimit () = !eprover_time; |
1574533861b1
Added files in order to use external ATPs as oracles and invoke these ATPs by calling Isabelle methods (currently "vampire" and "eprover").
mengj
parents:
diff
changeset
|
24 |
|
1574533861b1
Added files in order to use external ATPs as oracles and invoke these ATPs by calling Isabelle methods (currently "vampire" and "eprover").
mengj
parents:
diff
changeset
|
25 |
|
1574533861b1
Added files in order to use external ATPs as oracles and invoke these ATPs by calling Isabelle methods (currently "vampire" and "eprover").
mengj
parents:
diff
changeset
|
26 |
|
1574533861b1
Added files in order to use external ATPs as oracles and invoke these ATPs by calling Isabelle methods (currently "vampire" and "eprover").
mengj
parents:
diff
changeset
|
27 |
(* convert the negated 1st subgoal into CNF, write to files and call an ATP oracle *) |
18271
0e9a851db989
Added two methods "vampire" and "eprover" that handle both HOL and FOL proofs.
mengj
parents:
18195
diff
changeset
|
28 |
fun res_atp_tac res_atp_oracle mode timeLimit ctxt user_thms n thm = |
17905
1574533861b1
Added files in order to use external ATPs as oracles and invoke these ATPs by calling Isabelle methods (currently "vampire" and "eprover").
mengj
parents:
diff
changeset
|
29 |
SELECT_GOAL |
1574533861b1
Added files in order to use external ATPs as oracles and invoke these ATPs by calling Isabelle methods (currently "vampire" and "eprover").
mengj
parents:
diff
changeset
|
30 |
((EVERY1 [rtac ccontr,ObjectLogic.atomize_tac, skolemize_tac, |
1574533861b1
Added files in order to use external ATPs as oracles and invoke these ATPs by calling Isabelle methods (currently "vampire" and "eprover").
mengj
parents:
diff
changeset
|
31 |
METAHYPS(fn negs => |
1574533861b1
Added files in order to use external ATPs as oracles and invoke these ATPs by calling Isabelle methods (currently "vampire" and "eprover").
mengj
parents:
diff
changeset
|
32 |
HEADGOAL(Tactic.rtac |
1574533861b1
Added files in order to use external ATPs as oracles and invoke these ATPs by calling Isabelle methods (currently "vampire" and "eprover").
mengj
parents:
diff
changeset
|
33 |
(res_atp_oracle (ProofContext.theory_of ctxt) |
18271
0e9a851db989
Added two methods "vampire" and "eprover" that handle both HOL and FOL proofs.
mengj
parents:
18195
diff
changeset
|
34 |
(ResAtpSetup.prep_atp_input mode ctxt negs user_thms n, timeLimit))))]) handle Fail _ => no_tac) n thm; |
17905
1574533861b1
Added files in order to use external ATPs as oracles and invoke these ATPs by calling Isabelle methods (currently "vampire" and "eprover").
mengj
parents:
diff
changeset
|
35 |
|
18002
35ec4681d38f
Added several new functions that are used to prove HOL goals. Added new methods "vampireH" and "eproverH" that can prove both FOL and HOL goals. The old "vampire" and "eprover" methods are renamed to "vampireF" and "eproverF"; they can only prove FOL goals.
mengj
parents:
17907
diff
changeset
|
36 |
(* vampire and eprover tactics *) |
17905
1574533861b1
Added files in order to use external ATPs as oracles and invoke these ATPs by calling Isabelle methods (currently "vampire" and "eprover").
mengj
parents:
diff
changeset
|
37 |
|
18271
0e9a851db989
Added two methods "vampire" and "eprover" that handle both HOL and FOL proofs.
mengj
parents:
18195
diff
changeset
|
38 |
val vampire_tac = res_atp_tac vampire_oracle ResAtpSetup.Auto (!vampire_time); |
0e9a851db989
Added two methods "vampire" and "eprover" that handle both HOL and FOL proofs.
mengj
parents:
18195
diff
changeset
|
39 |
val eprover_tac = res_atp_tac eprover_oracle ResAtpSetup.Auto(!eprover_time); |
0e9a851db989
Added two methods "vampire" and "eprover" that handle both HOL and FOL proofs.
mengj
parents:
18195
diff
changeset
|
40 |
|
0e9a851db989
Added two methods "vampire" and "eprover" that handle both HOL and FOL proofs.
mengj
parents:
18195
diff
changeset
|
41 |
val vampireF_tac = res_atp_tac vampire_oracle ResAtpSetup.Fol(!vampire_time); |
17905
1574533861b1
Added files in order to use external ATPs as oracles and invoke these ATPs by calling Isabelle methods (currently "vampire" and "eprover").
mengj
parents:
diff
changeset
|
42 |
|
18271
0e9a851db989
Added two methods "vampire" and "eprover" that handle both HOL and FOL proofs.
mengj
parents:
18195
diff
changeset
|
43 |
val vampireH_tac = res_atp_tac vampire_oracle ResAtpSetup.Hol (!vampire_time); |
17905
1574533861b1
Added files in order to use external ATPs as oracles and invoke these ATPs by calling Isabelle methods (currently "vampire" and "eprover").
mengj
parents:
diff
changeset
|
44 |
|
18271
0e9a851db989
Added two methods "vampire" and "eprover" that handle both HOL and FOL proofs.
mengj
parents:
18195
diff
changeset
|
45 |
val eproverF_tac = res_atp_tac eprover_oracle ResAtpSetup.Fol (!eprover_time); |
0e9a851db989
Added two methods "vampire" and "eprover" that handle both HOL and FOL proofs.
mengj
parents:
18195
diff
changeset
|
46 |
|
0e9a851db989
Added two methods "vampire" and "eprover" that handle both HOL and FOL proofs.
mengj
parents:
18195
diff
changeset
|
47 |
val eproverH_tac = res_atp_tac eprover_oracle ResAtpSetup.Hol (!eprover_time); |
17905
1574533861b1
Added files in order to use external ATPs as oracles and invoke these ATPs by calling Isabelle methods (currently "vampire" and "eprover").
mengj
parents:
diff
changeset
|
48 |
|
1574533861b1
Added files in order to use external ATPs as oracles and invoke these ATPs by calling Isabelle methods (currently "vampire" and "eprover").
mengj
parents:
diff
changeset
|
49 |
val ResAtps_setup = [Method.add_methods |
18271
0e9a851db989
Added two methods "vampire" and "eprover" that handle both HOL and FOL proofs.
mengj
parents:
18195
diff
changeset
|
50 |
[("vampireF", ResAtpSetup.atp_method vampireF_tac, "A Vampire method for FOL problems"), |
0e9a851db989
Added two methods "vampire" and "eprover" that handle both HOL and FOL proofs.
mengj
parents:
18195
diff
changeset
|
51 |
("eproverF", ResAtpSetup.atp_method eproverF_tac, "A E prover method for FOL problems"), |
0e9a851db989
Added two methods "vampire" and "eprover" that handle both HOL and FOL proofs.
mengj
parents:
18195
diff
changeset
|
52 |
("vampireH",ResAtpSetup.atp_method vampireH_tac, "A Vampire method for HOL problems"), |
0e9a851db989
Added two methods "vampire" and "eprover" that handle both HOL and FOL proofs.
mengj
parents:
18195
diff
changeset
|
53 |
("eproverH",ResAtpSetup.atp_method eproverH_tac,"A E prover method for HOL problems"), |
0e9a851db989
Added two methods "vampire" and "eprover" that handle both HOL and FOL proofs.
mengj
parents:
18195
diff
changeset
|
54 |
("eprover",ResAtpSetup.atp_method eprover_tac,"A E prover method for FOL and HOL problems"), |
0e9a851db989
Added two methods "vampire" and "eprover" that handle both HOL and FOL proofs.
mengj
parents:
18195
diff
changeset
|
55 |
("vampire",ResAtpSetup.atp_method vampire_tac,"A Vampire method for FOL and HOL problems") |
0e9a851db989
Added two methods "vampire" and "eprover" that handle both HOL and FOL proofs.
mengj
parents:
18195
diff
changeset
|
56 |
]]; |
17905
1574533861b1
Added files in order to use external ATPs as oracles and invoke these ATPs by calling Isabelle methods (currently "vampire" and "eprover").
mengj
parents:
diff
changeset
|
57 |
|
1574533861b1
Added files in order to use external ATPs as oracles and invoke these ATPs by calling Isabelle methods (currently "vampire" and "eprover").
mengj
parents:
diff
changeset
|
58 |
|
1574533861b1
Added files in order to use external ATPs as oracles and invoke these ATPs by calling Isabelle methods (currently "vampire" and "eprover").
mengj
parents:
diff
changeset
|
59 |
|
1574533861b1
Added files in order to use external ATPs as oracles and invoke these ATPs by calling Isabelle methods (currently "vampire" and "eprover").
mengj
parents:
diff
changeset
|
60 |
|
17907 | 61 |
end |