src/HOL/Tools/res_atp_provers.ML
author wenzelm
Sat Jan 21 23:02:14 2006 +0100 (2006-01-21)
changeset 18728 6790126ab5f6
parent 18726 02b310b1fa10
child 19129 b66dff8ab7e9
permissions -rw-r--r--
simplified type attribute;
     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
    17   if thisLine = "# Proof found!\n"
    18   then true
    19   else if (thisLine = "") then false
    20   else if_proof_E instr end;		
    21 
    22 local 
    23 
    24 fun locations [] = ()
    25 |   locations (s::ss) = (warning s; locations ss);
    26 
    27 in 
    28 
    29 fun call_vampire (files:string list, time: int) = 
    30   let val output = (space_implode " " files) ^ "  "
    31       val runtime = "-t " ^ (string_of_int time)
    32       val vampire = ResAtp.helper_path "VAMPIRE_HOME" "vampire"
    33       val ch:(TextIO.instream,TextIO.outstream) Unix.proc = Unix.execute(vampire, [runtime,output])
    34       val (instr,outstr) = Unix.streamsOf ch
    35   in if_proof_vampire instr
    36   end;
    37 
    38 fun call_eprover (files:string list, time:int) =
    39   let val output = (space_implode " " files) ^ "  "
    40       val eprover = ResAtp.helper_path "E_HOME" "/PROVER/eprover"
    41       val runtime = "--cpu-limit=" ^ (string_of_int time)
    42       val ch:(TextIO.instream,TextIO.outstream) Unix.proc = Unix.execute(eprover, [runtime,"--tptp-format","-tAuto","-xAuto",output])
    43       val (instr,outstr) = Unix.streamsOf ch
    44   in if_proof_E instr
    45   end; 
    46 
    47 end
    48 
    49 fun vampire_o thy ((helper,files),time) = (if (call_vampire (helper @ files,time)) then (warning (hd files); ResAtpSetup.cond_rm_tmp files;HOLogic.mk_Trueprop HOLogic.false_const)  
    50   else (ResAtpSetup.cond_rm_tmp files;raise Fail ("vampire oracle failed")));
    51 
    52 
    53 fun eprover_o thy ((helper,files),time) = (if (call_eprover (helper @ files,time)) then (warning (hd files); ResAtpSetup.cond_rm_tmp files;HOLogic.mk_Trueprop HOLogic.false_const)
    54   else (raise Fail ("eprover oracle failed")));
    55 
    56 end;
    57