src/HOL/Tools/res_atp_provers.ML

fixed one proof that broke because of the changes
Markus did on the rules ex1I

(*  ID:         $Id$
    Author:     Jia Meng, NICTA

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 ((helper,files),time) = (if (call_vampire (helper @ files,time)) then (warning (hd files); 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 ((helper,files),time) = (if (call_eprover (helper @ files,time)) then (warning (hd files); ResAtpSetup.cond_rm_tmp files;HOLogic.mk_Trueprop HOLogic.false_const)
  else (raise Fail ("eprover oracle failed")));

end;