src/HOL/Tools/res_atp_provers.ML
changeset 17905 1574533861b1
child 17907 c20e4bddcb11
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Tools/res_atp_provers.ML	Wed Oct 19 06:33:24 2005 +0200
     1.3 @@ -0,0 +1,50 @@
     1.4 +(*  ID:         $Id$
     1.5 +    Author:     Jia Meng 
     1.6 +
     1.7 +Functions used for ATP Oracle.
     1.8 +*)
     1.9 +
    1.10 +
    1.11 +structure ResAtpProvers =
    1.12 +
    1.13 +struct
    1.14 +
    1.15 +fun if_proof_vampire instr = (TextIO.inputLine instr = "Refutation found. Thanks to Tanya!\n");
    1.16 +
    1.17 +fun if_proof_E instr =
    1.18 +  let val thisLine = TextIO.inputLine instr
    1.19 +  in
    1.20 +  if thisLine = "# Proof found!\n"
    1.21 +  then true
    1.22 +  else if (thisLine = "") then false
    1.23 +  else if_proof_E instr end;		
    1.24 +
    1.25 +fun call_vampire (files:string list, time: int) = 
    1.26 +  let val output = (space_implode " " files) ^ "  "
    1.27 +      val runtime = "-t " ^ (string_of_int time)
    1.28 +      val vampire = ResAtp.helper_path "VAMPIRE_HOME" "vampire"
    1.29 +      val ch:(TextIO.instream,TextIO.outstream) Unix.proc = Unix.execute(vampire, [runtime,output])
    1.30 +      val (instr,outstr) = Unix.streamsOf ch
    1.31 +  in if_proof_vampire instr
    1.32 +  end;
    1.33 +
    1.34 +fun call_eprover (files:string list, time:int) =
    1.35 +  let val output = (space_implode " " files) ^ "  "
    1.36 +      val eprover = ResAtp.helper_path "E_HOME" "/PROVER/eprover"
    1.37 +      val runtime = "--cpu-limit=" ^ (string_of_int time)
    1.38 +      val ch:(TextIO.instream,TextIO.outstream) Unix.proc = Unix.execute(eprover, [runtime,"--tptp-format","-tAuto","-xAuto",output])
    1.39 +      val (instr,outstr) = Unix.streamsOf ch
    1.40 +  in if_proof_E instr
    1.41 +  end; 
    1.42 +
    1.43 +
    1.44 +
    1.45 +fun vampire_o thy (files,time) = (if (call_vampire (files,time)) then (ResAtpSetup.cond_rm_tmp files;HOLogic.mk_Trueprop HOLogic.false_const)  
    1.46 +  else (ResAtpSetup.cond_rm_tmp files;raise Fail ("vampire oracle failed")));
    1.47 +
    1.48 +
    1.49 +fun eprover_o thy (files,time) = (if (call_eprover (files,time)) then (ResAtpSetup.cond_rm_tmp files;HOLogic.mk_Trueprop HOLogic.false_const)
    1.50 +  else (raise Fail ("eprover oracle failed")));
    1.51 +
    1.52 +end;
    1.53 +