src/HOL/Tools/res_atp_provers.ML
author paulson
Tue May 22 17:56:06 2007 +0200 (2007-05-22)
changeset 23075 69e30a7e8880
parent 22373 c6002b06e63e
child 23139 aa899bce7c3b
permissions -rw-r--r--
Some hacks for SPASS format
mengj@17905
     1
(*  ID:         $Id$
mengj@17907
     2
    Author:     Jia Meng, NICTA
mengj@17905
     3
mengj@17905
     4
Functions used for ATP Oracle.
mengj@17905
     5
*)
mengj@17905
     6
mengj@17905
     7
mengj@17905
     8
structure ResAtpProvers =
mengj@17905
     9
mengj@17905
    10
struct
mengj@17905
    11
paulson@22373
    12
fun seek_line s instr =
mengj@17905
    13
  let val thisLine = TextIO.inputLine instr
paulson@19479
    14
  in thisLine <> "" andalso 
paulson@22373
    15
     (thisLine = s orelse seek_line s instr) 
paulson@19479
    16
  end;
mengj@17905
    17
mengj@19195
    18
fun location s = warning ("ATP input at: " ^ s);
mengj@18726
    19
mengj@19195
    20
fun call_vampire (file:string, time: int) = 
mengj@19195
    21
  let val _ = location file
mengj@17905
    22
      val runtime = "-t " ^ (string_of_int time)
mengj@17905
    23
      val vampire = ResAtp.helper_path "VAMPIRE_HOME" "vampire"
paulson@22373
    24
      val (instr,outstr) = Unix.streamsOf (Unix.execute(vampire, [runtime,"--mode casc",file]))
paulson@22373
    25
  in seek_line "--------------------- PROVED ----------------------\n" instr
mengj@17905
    26
  end;
mengj@17905
    27
mengj@19195
    28
fun call_eprover (file:string, time:int) =
mengj@19195
    29
  let val _ = location file
paulson@22373
    30
      val eprover = ResAtp.helper_path "E_HOME" "eprover"
mengj@17905
    31
      val runtime = "--cpu-limit=" ^ (string_of_int time)
paulson@22373
    32
      val (instr,outstr) = Unix.streamsOf (Unix.execute(eprover, 
paulson@22373
    33
                              [runtime,"--tstp-in","-tAutoDev","-xAutoDev",file]))
paulson@22373
    34
  in seek_line "# Proof found!\n" instr
mengj@17905
    35
  end; 
mengj@17905
    36
mengj@19723
    37
fun call_spass (file:string, time:int) =
paulson@22373
    38
  let val _ = location file
paulson@22373
    39
      val runtime = "-TimeLimit=" ^ (string_of_int time)
paulson@22373
    40
      val spass = ResAtp.helper_path "SPASS_HOME" "SPASS"
paulson@22373
    41
      val (instr,outstr) = Unix.streamsOf (Unix.execute(spass, 
paulson@22373
    42
			      [runtime,"-Splits=0", "-FullRed=0", "-SOS=1",file]))
paulson@22373
    43
  in seek_line "SPASS beiseite: Proof found.\n" instr
paulson@22373
    44
  end;
mengj@17905
    45
paulson@19479
    46
fun vampire_o _ (file,time) = 
paulson@19479
    47
  if call_vampire (file,time) 
paulson@19479
    48
  then (warning file; ResAtp.cond_rm_tmp file; HOLogic.mk_Trueprop HOLogic.false_const)  
paulson@19479
    49
  else (ResAtp.cond_rm_tmp file; raise Fail ("vampire oracle failed"));
mengj@17905
    50
paulson@19479
    51
fun eprover_o _ (file,time) = 
paulson@19479
    52
  if call_eprover (file,time) 
paulson@19479
    53
  then (warning file; ResAtp.cond_rm_tmp file; HOLogic.mk_Trueprop HOLogic.false_const)
paulson@19479
    54
  else (ResAtp.cond_rm_tmp file; raise Fail ("eprover oracle failed"));
mengj@17905
    55
mengj@19723
    56
fun spass_o _ (file,time) =
mengj@19723
    57
    if call_spass (file,time)
mengj@19723
    58
    then (warning file; ResAtp.cond_rm_tmp file; HOLogic.mk_Trueprop HOLogic.false_const)
mengj@19723
    59
    else (ResAtp.cond_rm_tmp file; raise Fail ("SPASS oracle failed"));
mengj@19723
    60
mengj@19723
    61
mengj@17905
    62
end;
mengj@17905
    63