--- a/src/HOL/Tools/res_atp_provers.ML Fri Oct 03 14:07:41 2008 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,58 +0,0 @@
-(* ID: $Id$
- Author: Jia Meng, NICTA
-
-Functions used for ATP Oracle.
-*)
-
-structure ResAtpProvers =
-struct
-
-fun seek_line s instr =
- (case TextIO.inputLine instr of
- NONE => false
- | SOME thisLine => thisLine = s orelse seek_line s instr);
-
-fun location s = warning ("ATP input at: " ^ s);
-
-fun call_vampire (file:string, time: int) =
- let val _ = location file
- val runtime = "-t " ^ (string_of_int time)
- val vampire = ResAtp.helper_path "VAMPIRE_HOME" "vampire"
- val (instr,outstr) = Unix.streamsOf (Unix.execute(vampire, [runtime,"--mode casc",file]))
- in seek_line "--------------------- PROVED ----------------------\n" instr
- end;
-
-fun call_eprover (file:string, time:int) =
- let val _ = location file
- val eprover = ResAtp.helper_path "E_HOME" "eprover"
- val runtime = "--cpu-limit=" ^ (string_of_int time)
- val (instr,outstr) = Unix.streamsOf (Unix.execute(eprover,
- [runtime,"--tstp-in","-tAutoDev","-xAutoDev",file]))
- in seek_line "# Proof found!\n" instr
- end;
-
-fun call_spass (file:string, time:int) =
- let val _ = location file
- val runtime = "-TimeLimit=" ^ (string_of_int time)
- val spass = ResAtp.helper_path "SPASS_HOME" "SPASS"
- val (instr,outstr) = Unix.streamsOf (Unix.execute(spass,
- [runtime,"-Splits=0", "-FullRed=0", "-SOS=1",file]))
- in seek_line "SPASS beiseite: Proof found.\n" instr
- end;
-
-fun vampire_o (file,time) =
- if call_vampire (file,time)
- then (warning file; ResAtp.cond_rm_tmp file; @{cprop False})
- else (ResAtp.cond_rm_tmp file; raise Fail ("vampire oracle failed"));
-
-fun eprover_o (file,time) =
- if call_eprover (file,time)
- then (warning file; ResAtp.cond_rm_tmp file; @{cprop False})
- else (ResAtp.cond_rm_tmp file; raise Fail ("eprover oracle failed"));
-
-fun spass_o (file,time) =
- if call_spass (file,time)
- then (warning file; ResAtp.cond_rm_tmp file; @{cprop False})
- else (ResAtp.cond_rm_tmp file; raise Fail ("SPASS oracle failed"));
-
-end;