src/HOL/Tools/res_atp_provers.ML

case_tac/induct_tac: use same declarations as cases/induct;

(*  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; HOLogic.mk_Trueprop HOLogic.false_const)
  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; HOLogic.mk_Trueprop HOLogic.false_const)
  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; HOLogic.mk_Trueprop HOLogic.false_const)
  else (ResAtp.cond_rm_tmp file; raise Fail ("SPASS oracle failed"));

end;