src/HOL/Tools/res_atp_provers.ML
author haftmann
Fri Dec 16 09:00:11 2005 +0100 (2005-12-16)
changeset 18418 bf448d999b7e
parent 18272 4f0904ba19c2
child 18726 02b310b1fa10
permissions -rw-r--r--
re-arranged tuples (theory * 'a) to ('a * theory) in Pure
     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 fun call_vampire (files:string list, time: int) = 
    23   let val output = (space_implode " " files) ^ "  "
    24       val runtime = "-t " ^ (string_of_int time)
    25       val vampire = ResAtp.helper_path "VAMPIRE_HOME" "vampire"
    26       val ch:(TextIO.instream,TextIO.outstream) Unix.proc = Unix.execute(vampire, [runtime,output])
    27       val (instr,outstr) = Unix.streamsOf ch
    28   in if_proof_vampire instr
    29   end;
    30 
    31 fun call_eprover (files:string list, time:int) =
    32   let val output = (space_implode " " files) ^ "  "
    33       val eprover = ResAtp.helper_path "E_HOME" "/PROVER/eprover"
    34       val runtime = "--cpu-limit=" ^ (string_of_int time)
    35       val ch:(TextIO.instream,TextIO.outstream) Unix.proc = Unix.execute(eprover, [runtime,"--tptp-format","-tAuto","-xAuto",output])
    36       val (instr,outstr) = Unix.streamsOf ch
    37   in if_proof_E instr
    38   end; 
    39 
    40 
    41 
    42 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)  
    43   else (ResAtpSetup.cond_rm_tmp files;raise Fail ("vampire oracle failed")));
    44 
    45 
    46 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)
    47   else (raise Fail ("eprover oracle failed")));
    48 
    49 end;
    50