src/HOL/Tools/res_atp_provers.ML
author wenzelm
Thu Mar 27 14:41:09 2008 +0100 (2008-03-27)
changeset 26424 a6cad32a27b0
parent 23139 aa899bce7c3b
child 28290 4cc2b6046258
permissions -rw-r--r--
eliminated theory ProtoPure;
     1 (*  ID:         $Id$
     2     Author:     Jia Meng, NICTA
     3 
     4 Functions used for ATP Oracle.
     5 *)
     6 
     7 structure ResAtpProvers =
     8 struct
     9 
    10 fun seek_line s instr =
    11   (case TextIO.inputLine instr of
    12     NONE => false
    13   | SOME thisLine => thisLine = s orelse seek_line s instr);
    14 
    15 fun location s = warning ("ATP input at: " ^ s);
    16 
    17 fun call_vampire (file:string, time: int) =
    18   let val _ = location file
    19       val runtime = "-t " ^ (string_of_int time)
    20       val vampire = ResAtp.helper_path "VAMPIRE_HOME" "vampire"
    21       val (instr,outstr) = Unix.streamsOf (Unix.execute(vampire, [runtime,"--mode casc",file]))
    22   in seek_line "--------------------- PROVED ----------------------\n" instr
    23   end;
    24 
    25 fun call_eprover (file:string, time:int) =
    26   let val _ = location file
    27       val eprover = ResAtp.helper_path "E_HOME" "eprover"
    28       val runtime = "--cpu-limit=" ^ (string_of_int time)
    29       val (instr,outstr) = Unix.streamsOf (Unix.execute(eprover,
    30                               [runtime,"--tstp-in","-tAutoDev","-xAutoDev",file]))
    31   in seek_line "# Proof found!\n" instr
    32   end;
    33 
    34 fun call_spass (file:string, time:int) =
    35   let val _ = location file
    36       val runtime = "-TimeLimit=" ^ (string_of_int time)
    37       val spass = ResAtp.helper_path "SPASS_HOME" "SPASS"
    38       val (instr,outstr) = Unix.streamsOf (Unix.execute(spass,
    39 			      [runtime,"-Splits=0", "-FullRed=0", "-SOS=1",file]))
    40   in seek_line "SPASS beiseite: Proof found.\n" instr
    41   end;
    42 
    43 fun vampire_o _ (file,time) =
    44   if call_vampire (file,time)
    45   then (warning file; ResAtp.cond_rm_tmp file; HOLogic.mk_Trueprop HOLogic.false_const)
    46   else (ResAtp.cond_rm_tmp file; raise Fail ("vampire oracle failed"));
    47 
    48 fun eprover_o _ (file,time) =
    49   if call_eprover (file,time)
    50   then (warning file; ResAtp.cond_rm_tmp file; HOLogic.mk_Trueprop HOLogic.false_const)
    51   else (ResAtp.cond_rm_tmp file; raise Fail ("eprover oracle failed"));
    52 
    53 fun spass_o _ (file,time) =
    54   if call_spass (file,time)
    55   then (warning file; ResAtp.cond_rm_tmp file; HOLogic.mk_Trueprop HOLogic.false_const)
    56   else (ResAtp.cond_rm_tmp file; raise Fail ("SPASS oracle failed"));
    57 
    58 end;