11 |
11 |
12 fun if_proof_vampire instr = (TextIO.inputLine instr = "Refutation found. Thanks to Tanya!\n"); |
12 fun if_proof_vampire instr = (TextIO.inputLine instr = "Refutation found. Thanks to Tanya!\n"); |
13 |
13 |
14 fun if_proof_E instr = |
14 fun if_proof_E instr = |
15 let val thisLine = TextIO.inputLine instr |
15 let val thisLine = TextIO.inputLine instr |
16 in |
16 in thisLine <> "" andalso |
17 if thisLine = "# Proof found!\n" |
17 (thisLine = "# Proof found!\n" orelse if_proof_E instr) |
18 then true |
18 end; |
19 else if (thisLine = "") then false |
|
20 else if_proof_E instr end; |
|
21 |
19 |
22 |
20 |
23 local |
21 local |
24 |
22 |
25 fun location s = warning ("ATP input at: " ^ s); |
23 fun location s = warning ("ATP input at: " ^ s); |
28 |
26 |
29 fun call_vampire (file:string, time: int) = |
27 fun call_vampire (file:string, time: int) = |
30 let val _ = location file |
28 let val _ = location file |
31 val runtime = "-t " ^ (string_of_int time) |
29 val runtime = "-t " ^ (string_of_int time) |
32 val vampire = ResAtp.helper_path "VAMPIRE_HOME" "vampire" |
30 val vampire = ResAtp.helper_path "VAMPIRE_HOME" "vampire" |
33 val ch:(TextIO.instream,TextIO.outstream) Unix.proc = Unix.execute(vampire, [runtime,file]) |
31 val ch:(TextIO.instream,TextIO.outstream) Unix.proc = |
|
32 Unix.execute(vampire, [runtime,file]) |
34 val (instr,outstr) = Unix.streamsOf ch |
33 val (instr,outstr) = Unix.streamsOf ch |
35 in if_proof_vampire instr |
34 in if_proof_vampire instr |
36 end; |
35 end; |
37 |
36 |
38 fun call_eprover (file:string, time:int) = |
37 fun call_eprover (file:string, time:int) = |
39 let val _ = location file |
38 let val _ = location file |
40 val eprover = ResAtp.helper_path "E_HOME" "/PROVER/eprover" |
39 val eprover = ResAtp.helper_path "E_HOME" "/PROVER/eprover" |
41 val runtime = "--cpu-limit=" ^ (string_of_int time) |
40 val runtime = "--cpu-limit=" ^ (string_of_int time) |
42 val ch:(TextIO.instream,TextIO.outstream) Unix.proc = Unix.execute(eprover, [runtime,"--tptp-format","-tAuto","-xAuto",file]) |
41 val ch:(TextIO.instream,TextIO.outstream) Unix.proc = |
|
42 Unix.execute(eprover, [runtime,"--tptp-format","-tAuto","-xAuto",file]) |
43 val (instr,outstr) = Unix.streamsOf ch |
43 val (instr,outstr) = Unix.streamsOf ch |
44 in if_proof_E instr |
44 in if_proof_E instr |
45 end; |
45 end; |
46 |
46 |
47 end |
47 end |
48 |
48 |
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) |
49 fun vampire_o _ (file,time) = |
50 else (ResAtp.cond_rm_tmp file;raise Fail ("vampire oracle failed"))); |
50 if call_vampire (file,time) |
|
51 then (warning file; ResAtp.cond_rm_tmp file; HOLogic.mk_Trueprop HOLogic.false_const) |
|
52 else (ResAtp.cond_rm_tmp file; raise Fail ("vampire oracle failed")); |
51 |
53 |
52 |
54 fun eprover_o _ (file,time) = |
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) |
55 if call_eprover (file,time) |
54 else (ResAtp.cond_rm_tmp file;raise Fail ("eprover oracle failed"))); |
56 then (warning file; ResAtp.cond_rm_tmp file; HOLogic.mk_Trueprop HOLogic.false_const) |
|
57 else (ResAtp.cond_rm_tmp file; raise Fail ("eprover oracle failed")); |
55 |
58 |
56 end; |
59 end; |
57 |
60 |