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
     1 (*  ID:         $Id$
     2     Author:     Jia Meng, NICTA
     3 
     4 Functions used for ATP Oracle.
     5 *)
     6 
     7 
     8 structure ResAtpProvers =
     9 
    10 struct
    11 
    12 fun seek_line s instr =
    13   let val thisLine = TextIO.inputLine instr
    14   in thisLine <> "" andalso 
    15      (thisLine = s orelse seek_line s instr) 
    16   end;
    17 
    18 fun location s = warning ("ATP input at: " ^ s);
    19 
    20 fun call_vampire (file:string, time: int) = 
    21   let val _ = location file
    22       val runtime = "-t " ^ (string_of_int time)
    23       val vampire = ResAtp.helper_path "VAMPIRE_HOME" "vampire"
    24       val (instr,outstr) = Unix.streamsOf (Unix.execute(vampire, [runtime,"--mode casc",file]))
    25   in seek_line "--------------------- PROVED ----------------------\n" instr
    26   end;
    27 
    28 fun call_eprover (file:string, time:int) =
    29   let val _ = location file
    30       val eprover = ResAtp.helper_path "E_HOME" "eprover"
    31       val runtime = "--cpu-limit=" ^ (string_of_int time)
    32       val (instr,outstr) = Unix.streamsOf (Unix.execute(eprover, 
    33                               [runtime,"--tstp-in","-tAutoDev","-xAutoDev",file]))
    34   in seek_line "# Proof found!\n" instr
    35   end; 
    36 
    37 fun call_spass (file:string, time:int) =
    38   let val _ = location file
    39       val runtime = "-TimeLimit=" ^ (string_of_int time)
    40       val spass = ResAtp.helper_path "SPASS_HOME" "SPASS"
    41       val (instr,outstr) = Unix.streamsOf (Unix.execute(spass, 
    42 			      [runtime,"-Splits=0", "-FullRed=0", "-SOS=1",file]))
    43   in seek_line "SPASS beiseite: Proof found.\n" instr
    44   end;
    45 
    46 fun vampire_o _ (file,time) = 
    47   if call_vampire (file,time) 
    48   then (warning file; ResAtp.cond_rm_tmp file; HOLogic.mk_Trueprop HOLogic.false_const)  
    49   else (ResAtp.cond_rm_tmp file; raise Fail ("vampire oracle failed"));
    50 
    51 fun eprover_o _ (file,time) = 
    52   if call_eprover (file,time) 
    53   then (warning file; ResAtp.cond_rm_tmp file; HOLogic.mk_Trueprop HOLogic.false_const)
    54   else (ResAtp.cond_rm_tmp file; raise Fail ("eprover oracle failed"));
    55 
    56 fun spass_o _ (file,time) =
    57     if call_spass (file,time)
    58     then (warning file; ResAtp.cond_rm_tmp file; HOLogic.mk_Trueprop HOLogic.false_const)
    59     else (ResAtp.cond_rm_tmp file; raise Fail ("SPASS oracle failed"));
    60 
    61 
    62 end;
    63