20 else if_proof_E instr end; |
20 else if_proof_E instr end; |
21 |
21 |
22 |
22 |
23 local |
23 local |
24 |
24 |
25 fun locations [] = () |
25 fun location s = warning ("ATP input at: " ^ s); |
26 | locations (s::ss) = (warning s; locations ss); |
|
27 |
26 |
28 in |
27 in |
29 |
28 |
30 fun call_vampire (files:string list, time: int) = |
29 fun call_vampire (file:string, time: int) = |
31 let val _ = locations files |
30 let val _ = location file |
32 val output = (space_implode " " files) ^ " " |
|
33 val runtime = "-t " ^ (string_of_int time) |
31 val runtime = "-t " ^ (string_of_int time) |
34 val vampire = ResAtp.helper_path "VAMPIRE_HOME" "vampire" |
32 val vampire = ResAtp.helper_path "VAMPIRE_HOME" "vampire" |
35 val ch:(TextIO.instream,TextIO.outstream) Unix.proc = Unix.execute(vampire, [runtime,output]) |
33 val ch:(TextIO.instream,TextIO.outstream) Unix.proc = Unix.execute(vampire, [runtime,file]) |
36 val (instr,outstr) = Unix.streamsOf ch |
34 val (instr,outstr) = Unix.streamsOf ch |
37 in if_proof_vampire instr |
35 in if_proof_vampire instr |
38 end; |
36 end; |
39 |
37 |
40 fun call_eprover (files:string list, time:int) = |
38 fun call_eprover (file:string, time:int) = |
41 let val _ = locations files |
39 let val _ = location file |
42 val output = (space_implode " " files) ^ " " |
|
43 val eprover = ResAtp.helper_path "E_HOME" "/PROVER/eprover" |
40 val eprover = ResAtp.helper_path "E_HOME" "/PROVER/eprover" |
44 val runtime = "--cpu-limit=" ^ (string_of_int time) |
41 val runtime = "--cpu-limit=" ^ (string_of_int time) |
45 val ch:(TextIO.instream,TextIO.outstream) Unix.proc = Unix.execute(eprover, [runtime,"--tptp-format","-tAuto","-xAuto",output]) |
42 val ch:(TextIO.instream,TextIO.outstream) Unix.proc = Unix.execute(eprover, [runtime,"--tptp-format","-tAuto","-xAuto",file]) |
46 val (instr,outstr) = Unix.streamsOf ch |
43 val (instr,outstr) = Unix.streamsOf ch |
47 in if_proof_E instr |
44 in if_proof_E instr |
48 end; |
45 end; |
49 |
46 |
50 end |
47 end |
51 |
48 |
52 fun vampire_o thy ((helper,files),time) = (if (call_vampire (helper @ files,time)) then (warning (hd files); ResAtpSetup.cond_rm_tmp files;HOLogic.mk_Trueprop HOLogic.false_const) |
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) |
53 else (ResAtpSetup.cond_rm_tmp files;raise Fail ("vampire oracle failed"))); |
50 else (ResAtp.cond_rm_tmp file;raise Fail ("vampire oracle failed"))); |
54 |
51 |
55 |
52 |
56 fun eprover_o thy ((helper,files),time) = (if (call_eprover (helper @ files,time)) then (warning (hd files); ResAtpSetup.cond_rm_tmp files;HOLogic.mk_Trueprop HOLogic.false_const) |
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) |
57 else (ResAtpSetup.cond_rm_tmp files;raise Fail ("eprover oracle failed"))); |
54 else (ResAtp.cond_rm_tmp file;raise Fail ("eprover oracle failed"))); |
58 |
55 |
59 end; |
56 end; |
60 |
57 |