src/HOL/Tools/res_atp_provers.ML
author haftmann
Wed Jun 07 16:55:39 2006 +0200 (2006-06-07)
changeset 19818 5c5c1208a3fa
parent 19723 7602f74c914b
child 22373 c6002b06e63e
permissions -rw-r--r--
adding case theorems for code generator
     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 if_proof_vampire instr = (TextIO.inputLine instr = "Refutation found. Thanks to Tanya!\n");
    13 
    14 fun if_proof_E instr =
    15   let val thisLine = TextIO.inputLine instr
    16   in thisLine <> "" andalso 
    17      (thisLine = "# Proof found!\n" orelse if_proof_E instr) 
    18   end;
    19 
    20 fun if_proof_spass instr = 
    21     let val thisLine = TextIO.inputLine instr
    22     in thisLine <> "" andalso 
    23        (thisLine = "SPASS beiseite: Proof found.\n" orelse if_proof_spass instr) 
    24     end;
    25 
    26 local 
    27 
    28 fun location s = warning ("ATP input at: " ^ s);
    29 
    30 in 
    31 
    32 fun call_vampire (file:string, time: int) = 
    33   let val _ = location file
    34       val runtime = "-t " ^ (string_of_int time)
    35       val vampire = ResAtp.helper_path "VAMPIRE_HOME" "vampire"
    36       val ch:(TextIO.instream,TextIO.outstream) Unix.proc = 
    37           Unix.execute(vampire, [runtime,file])
    38       val (instr,outstr) = Unix.streamsOf ch
    39   in if_proof_vampire instr
    40   end;
    41 
    42 fun call_eprover (file:string, time:int) =
    43   let val _ = location file
    44       val eprover = ResAtp.helper_path "E_HOME" "/PROVER/eprover"
    45       val runtime = "--cpu-limit=" ^ (string_of_int time)
    46       val ch:(TextIO.instream,TextIO.outstream) Unix.proc = 
    47           Unix.execute(eprover, [runtime,"--tptp-format","-tAuto","-xAuto",file])
    48       val (instr,outstr) = Unix.streamsOf ch
    49   in if_proof_E instr
    50   end; 
    51 
    52 fun call_spass (file:string, time:int) =
    53     let val _ = location file
    54 	val runtime = "-TimeLimit=" ^ (string_of_int time)
    55 	val spass = ResAtp.helper_path "SPASS_HOME" "SPASS"
    56 	val ch:(TextIO.instream,TextIO.outstream) Unix.proc =
    57 	    Unix.execute(spass, [runtime,"-Splits=0", "-FullRed=0", "-SOS=1",file])
    58 	val (instr,outstr) = Unix.streamsOf ch
    59     in if_proof_spass instr
    60     end;
    61 
    62 
    63 end
    64 
    65 fun vampire_o _ (file,time) = 
    66   if call_vampire (file,time) 
    67   then (warning file; ResAtp.cond_rm_tmp file; HOLogic.mk_Trueprop HOLogic.false_const)  
    68   else (ResAtp.cond_rm_tmp file; raise Fail ("vampire oracle failed"));
    69 
    70 fun eprover_o _ (file,time) = 
    71   if call_eprover (file,time) 
    72   then (warning file; ResAtp.cond_rm_tmp file; HOLogic.mk_Trueprop HOLogic.false_const)
    73   else (ResAtp.cond_rm_tmp file; raise Fail ("eprover oracle failed"));
    74 
    75 fun spass_o _ (file,time) =
    76     if call_spass (file,time)
    77     then (warning file; ResAtp.cond_rm_tmp file; HOLogic.mk_Trueprop HOLogic.false_const)
    78     else (ResAtp.cond_rm_tmp file; raise Fail ("SPASS oracle failed"));
    79 
    80 
    81 end;
    82