author | mengj |
Tue, 07 Mar 2006 03:54:11 +0100 | |
changeset 19195 | e0b483dea2c0 |
parent 19129 | b66dff8ab7e9 |
child 19479 | caaf68a64ac4 |
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 |
Functions used for ATP Oracle. |
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 |
|
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 |
structure ResAtpProvers = |
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 |
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
|
11 |
|
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 |
fun if_proof_vampire instr = (TextIO.inputLine instr = "Refutation found. Thanks to Tanya!\n"); |
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 if_proof_E instr = |
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 |
let val thisLine = TextIO.inputLine instr |
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 |
in |
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 |
if thisLine = "# Proof found!\n" |
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 |
then true |
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 |
else if (thisLine = "") then false |
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 if_proof_E instr end; |
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 |
|
19129 | 22 |
|
18726 | 23 |
local |
24 |
||
19195
e0b483dea2c0
Moved the settings for ATP time limit to res_atp.ML
mengj
parents:
19129
diff
changeset
|
25 |
fun location s = warning ("ATP input at: " ^ s); |
18726 | 26 |
|
27 |
in |
|
28 |
||
19195
e0b483dea2c0
Moved the settings for ATP time limit to res_atp.ML
mengj
parents:
19129
diff
changeset
|
29 |
fun call_vampire (file:string, time: int) = |
e0b483dea2c0
Moved the settings for ATP time limit to res_atp.ML
mengj
parents:
19129
diff
changeset
|
30 |
let val _ = location file |
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
|
31 |
val runtime = "-t " ^ (string_of_int 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
|
32 |
val vampire = ResAtp.helper_path "VAMPIRE_HOME" "vampire" |
19195
e0b483dea2c0
Moved the settings for ATP time limit to res_atp.ML
mengj
parents:
19129
diff
changeset
|
33 |
val ch:(TextIO.instream,TextIO.outstream) Unix.proc = Unix.execute(vampire, [runtime,file]) |
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
|
34 |
val (instr,outstr) = Unix.streamsOf ch |
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 |
in if_proof_vampire instr |
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
|
36 |
end; |
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 |
|
19195
e0b483dea2c0
Moved the settings for ATP time limit to res_atp.ML
mengj
parents:
19129
diff
changeset
|
38 |
fun call_eprover (file:string, time:int) = |
e0b483dea2c0
Moved the settings for ATP time limit to res_atp.ML
mengj
parents:
19129
diff
changeset
|
39 |
let val _ = location file |
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
|
40 |
val eprover = ResAtp.helper_path "E_HOME" "/PROVER/eprover" |
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
|
41 |
val runtime = "--cpu-limit=" ^ (string_of_int time) |
19195
e0b483dea2c0
Moved the settings for ATP time limit to res_atp.ML
mengj
parents:
19129
diff
changeset
|
42 |
val ch:(TextIO.instream,TextIO.outstream) Unix.proc = Unix.execute(eprover, [runtime,"--tptp-format","-tAuto","-xAuto",file]) |
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
|
43 |
val (instr,outstr) = Unix.streamsOf ch |
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 |
in if_proof_E instr |
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
|
45 |
end; |
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
|
46 |
|
18726 | 47 |
end |
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 |
|
19195
e0b483dea2c0
Moved the settings for ATP time limit to res_atp.ML
mengj
parents:
19129
diff
changeset
|
49 |
fun vampire_o thy (file,time) = (if (call_vampire (file,time)) then (warning file; ResAtp.cond_rm_tmp file;HOLogic.mk_Trueprop HOLogic.false_const) |
e0b483dea2c0
Moved the settings for ATP time limit to res_atp.ML
mengj
parents:
19129
diff
changeset
|
50 |
else (ResAtp.cond_rm_tmp file;raise Fail ("vampire oracle failed"))); |
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
|
51 |
|
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
|
52 |
|
19195
e0b483dea2c0
Moved the settings for ATP time limit to res_atp.ML
mengj
parents:
19129
diff
changeset
|
53 |
fun eprover_o thy (file,time) = (if (call_eprover (file,time)) then (warning file; ResAtp.cond_rm_tmp file;HOLogic.mk_Trueprop HOLogic.false_const) |
e0b483dea2c0
Moved the settings for ATP time limit to res_atp.ML
mengj
parents:
19129
diff
changeset
|
54 |
else (ResAtp.cond_rm_tmp file;raise Fail ("eprover oracle failed"))); |
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
|
55 |
|
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
|
56 |
end; |
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 |