src/HOL/Tools/res_atp_provers.ML
author paulson
Thu Feb 09 12:20:31 2006 +0100 (2006-02-09)
changeset 18986 5060ca625e02
parent 18726 02b310b1fa10
child 19129 b66dff8ab7e9
permissions -rw-r--r--
tidying
mengj@17905
     1
(*  ID:         $Id$
mengj@17907
     2
    Author:     Jia Meng, NICTA
mengj@17905
     3
mengj@17905
     4
Functions used for ATP Oracle.
mengj@17905
     5
*)
mengj@17905
     6
mengj@17905
     7
mengj@17905
     8
structure ResAtpProvers =
mengj@17905
     9
mengj@17905
    10
struct
mengj@17905
    11
mengj@17905
    12
fun if_proof_vampire instr = (TextIO.inputLine instr = "Refutation found. Thanks to Tanya!\n");
mengj@17905
    13
mengj@17905
    14
fun if_proof_E instr =
mengj@17905
    15
  let val thisLine = TextIO.inputLine instr
mengj@17905
    16
  in
mengj@17905
    17
  if thisLine = "# Proof found!\n"
mengj@17905
    18
  then true
mengj@17905
    19
  else if (thisLine = "") then false
mengj@17905
    20
  else if_proof_E instr end;		
mengj@17905
    21
mengj@18726
    22
local 
mengj@18726
    23
mengj@18726
    24
fun locations [] = ()
mengj@18726
    25
|   locations (s::ss) = (warning s; locations ss);
mengj@18726
    26
mengj@18726
    27
in 
mengj@18726
    28
mengj@17905
    29
fun call_vampire (files:string list, time: int) = 
mengj@17905
    30
  let val output = (space_implode " " files) ^ "  "
mengj@17905
    31
      val runtime = "-t " ^ (string_of_int time)
mengj@17905
    32
      val vampire = ResAtp.helper_path "VAMPIRE_HOME" "vampire"
mengj@17905
    33
      val ch:(TextIO.instream,TextIO.outstream) Unix.proc = Unix.execute(vampire, [runtime,output])
mengj@17905
    34
      val (instr,outstr) = Unix.streamsOf ch
mengj@17905
    35
  in if_proof_vampire instr
mengj@17905
    36
  end;
mengj@17905
    37
mengj@17905
    38
fun call_eprover (files:string list, time:int) =
mengj@17905
    39
  let val output = (space_implode " " files) ^ "  "
mengj@17905
    40
      val eprover = ResAtp.helper_path "E_HOME" "/PROVER/eprover"
mengj@17905
    41
      val runtime = "--cpu-limit=" ^ (string_of_int time)
mengj@17905
    42
      val ch:(TextIO.instream,TextIO.outstream) Unix.proc = Unix.execute(eprover, [runtime,"--tptp-format","-tAuto","-xAuto",output])
mengj@17905
    43
      val (instr,outstr) = Unix.streamsOf ch
mengj@17905
    44
  in if_proof_E instr
mengj@17905
    45
  end; 
mengj@17905
    46
mengj@18726
    47
end
mengj@17905
    48
mengj@18272
    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)  
mengj@17905
    50
  else (ResAtpSetup.cond_rm_tmp files;raise Fail ("vampire oracle failed")));
mengj@17905
    51
mengj@17905
    52
mengj@18272
    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)
mengj@17905
    54
  else (raise Fail ("eprover oracle failed")));
mengj@17905
    55
mengj@17905
    56
end;
mengj@17905
    57