src/HOL/Tools/res_atp_provers.ML
author mengj
Fri Nov 18 07:07:06 2005 +0100 (2005-11-18)
changeset 18196 02f1c4022484
parent 17907 c20e4bddcb11
child 18272 4f0904ba19c2
permissions -rw-r--r--
-- split up inputs to ATPs into two groups: temporary files (axioms and goals) and permanent helper files (e.g. combinator reduction axioms).
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@17905
    22
fun call_vampire (files:string list, time: int) = 
mengj@17905
    23
  let val output = (space_implode " " files) ^ "  "
mengj@17905
    24
      val runtime = "-t " ^ (string_of_int time)
mengj@17905
    25
      val vampire = ResAtp.helper_path "VAMPIRE_HOME" "vampire"
mengj@17905
    26
      val ch:(TextIO.instream,TextIO.outstream) Unix.proc = Unix.execute(vampire, [runtime,output])
mengj@17905
    27
      val (instr,outstr) = Unix.streamsOf ch
mengj@17905
    28
  in if_proof_vampire instr
mengj@17905
    29
  end;
mengj@17905
    30
mengj@17905
    31
fun call_eprover (files:string list, time:int) =
mengj@17905
    32
  let val output = (space_implode " " files) ^ "  "
mengj@17905
    33
      val eprover = ResAtp.helper_path "E_HOME" "/PROVER/eprover"
mengj@17905
    34
      val runtime = "--cpu-limit=" ^ (string_of_int time)
mengj@17905
    35
      val ch:(TextIO.instream,TextIO.outstream) Unix.proc = Unix.execute(eprover, [runtime,"--tptp-format","-tAuto","-xAuto",output])
mengj@17905
    36
      val (instr,outstr) = Unix.streamsOf ch
mengj@17905
    37
  in if_proof_E instr
mengj@17905
    38
  end; 
mengj@17905
    39
mengj@17905
    40
mengj@17905
    41
mengj@18196
    42
fun vampire_o thy ((helper,files),time) = (if (call_vampire (helper @ files,time)) then (warning (hd helper); ResAtpSetup.cond_rm_tmp files;HOLogic.mk_Trueprop HOLogic.false_const)  
mengj@17905
    43
  else (ResAtpSetup.cond_rm_tmp files;raise Fail ("vampire oracle failed")));
mengj@17905
    44
mengj@17905
    45
mengj@18196
    46
fun eprover_o thy ((helper,files),time) = (if (call_eprover (helper @ files,time)) then (warning (hd helper); ResAtpSetup.cond_rm_tmp files;HOLogic.mk_Trueprop HOLogic.false_const)
mengj@17905
    47
  else (raise Fail ("eprover oracle failed")));
mengj@17905
    48
mengj@17905
    49
end;
mengj@17905
    50