src/HOL/Tools/res_atp_provers.ML

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/res_atp_provers.ML	Wed Oct 19 06:33:24 2005 +0200
@@ -0,0 +1,50 @@
+(*  ID:         $Id$
+    Author:     Jia Meng 
+
+Functions used for ATP Oracle.
+*)
+
+
+structure ResAtpProvers =
+
+struct
+
+fun if_proof_vampire instr = (TextIO.inputLine instr = "Refutation found. Thanks to Tanya!\n");
+
+fun if_proof_E instr =
+  let val thisLine = TextIO.inputLine instr
+  in
+  if thisLine = "# Proof found!\n"
+  then true
+  else if (thisLine = "") then false
+  else if_proof_E instr end;		
+
+fun call_vampire (files:string list, time: int) = 
+  let val output = (space_implode " " files) ^ "  "
+      val runtime = "-t " ^ (string_of_int time)
+      val vampire = ResAtp.helper_path "VAMPIRE_HOME" "vampire"
+      val ch:(TextIO.instream,TextIO.outstream) Unix.proc = Unix.execute(vampire, [runtime,output])
+      val (instr,outstr) = Unix.streamsOf ch
+  in if_proof_vampire instr
+  end;
+
+fun call_eprover (files:string list, time:int) =
+  let val output = (space_implode " " files) ^ "  "
+      val eprover = ResAtp.helper_path "E_HOME" "/PROVER/eprover"
+      val runtime = "--cpu-limit=" ^ (string_of_int time)
+      val ch:(TextIO.instream,TextIO.outstream) Unix.proc = Unix.execute(eprover, [runtime,"--tptp-format","-tAuto","-xAuto",output])
+      val (instr,outstr) = Unix.streamsOf ch
+  in if_proof_E instr
+  end; 
+
+
+
+fun vampire_o thy (files,time) = (if (call_vampire (files,time)) then (ResAtpSetup.cond_rm_tmp files;HOLogic.mk_Trueprop HOLogic.false_const)  
+  else (ResAtpSetup.cond_rm_tmp files;raise Fail ("vampire oracle failed")));
+
+
+fun eprover_o thy (files,time) = (if (call_eprover (files,time)) then (ResAtpSetup.cond_rm_tmp files;HOLogic.mk_Trueprop HOLogic.false_const)
+  else (raise Fail ("eprover oracle failed")));
+
+end;
+