src/HOL/Tools/ATP/VampCommunication.ML

PARTIAL conversion to Vampire8

(*  Title:      VampCommunication.ml
    ID:         $Id$
    Author:     Claire Quigley
    Copyright   2004  University of Cambridge
*)

(***************************************************************************)
(*  Code to deal with the transfer of proofs from a Vampire process          *)
(***************************************************************************)
signature VAMP_COMM =
  sig
    val getEInput : TextIO.instream -> string * string
    val checkEProofFound: 
          TextIO.instream * TextIO.outstream * Posix.Process.pid * 
          string * string * thm * int * (ResClause.clause * thm) Array.array * int -> bool

    val getVampInput : TextIO.instream -> string * string
    val checkVampProofFound: 
          TextIO.instream * TextIO.outstream * Posix.Process.pid * 
          string * string * thm * int * (ResClause.clause * thm) Array.array * int -> bool
  end;

structure VampComm : VAMP_COMM =
struct

exception EOF;

(**********************************************************************)
(*  Reconstruct the Vampire/E proof w.r.t. thmstring (string version of   *)
(*  Isabelle goal to be proved), then transfer the reconstruction     *)
(*  steps as a string to the input pipe of the main Isabelle process  *)
(**********************************************************************)

fun reconstruct_tac proofextract goalstring toParent ppid sg_num 
                    clause_arr num_of_clauses =
    SELECT_GOAL
      (EVERY1
        [rtac ccontr, ResLib.atomize_tac, skolemize_tac,
	 METAHYPS(fn negs =>
		     (Recon_Transfer.proverString_to_lemmaString proofextract  
		       goalstring toParent ppid negs clause_arr num_of_clauses))]) sg_num


(*********************************************************************************)
(*  Inspect the output of an ATP process to see if it has found a proof,     *)
(*  and if so, transfer output to the input pipe of the main Isabelle process    *)
(*********************************************************************************)

fun startTransfer (startS,endS)
      (fromChild, toParent, ppid, goalstring,childCmd,
       thm, sg_num,clause_arr, num_of_clauses) =
 let val thisLine = TextIO.inputLine fromChild
     fun transferInput currentString =
      let val thisLine = TextIO.inputLine fromChild
      in
	if thisLine = "" (*end of file?*)
	then (File.write (File.tmp_path (Path.basic"extraction_failed")) 
	                 ("start bracket: " ^ startS ^
	                  "\nend bracket: " ^ endS ^
	                  "\naccumulated text: " ^ currentString);
	      raise EOF)                    
	else if String.isPrefix endS thisLine
	then let val proofextract = Recon_Parse.extract_proof (currentString^thisLine)
	     in
	       File.write (File.tmp_path (Path.basic"extracted_prf")) proofextract; 
	       reconstruct_tac proofextract goalstring toParent ppid sg_num  
			       clause_arr num_of_clauses thm
	     end
	else transferInput (currentString^thisLine)
      end
 in
   if thisLine = "" then false
   else if String.isPrefix startS thisLine
   then
    (File.append (File.tmp_path (Path.basic "transfer_start"))
		 ("about to transfer proof, thm is: " ^ string_of_thm thm);
     transferInput thisLine;
     true) handle EOF => false
   else
      startTransfer (startS,endS)
                    (fromChild, toParent, ppid, goalstring,
		     childCmd, thm, sg_num,clause_arr, num_of_clauses)
 end


fun checkVampProofFound (fromChild, toParent, ppid, goalstring, childCmd, 
                         thm, sg_num, clause_arr, num_of_clauses) =
 let val proof_file = TextIO.openAppend
	   (File.platform_path(File.tmp_path (Path.basic "atp_proof")))
     val _ = File.write (File.tmp_path (Path.basic "atp_checking_prf"))
			("checking if proof found, thm is: " ^ string_of_thm thm)
     val thisLine = TextIO.inputLine fromChild
 in   
     if thisLine = "" 
     then (TextIO.output (proof_file, "No proof output seen \n");
	   TextIO.closeOut proof_file;
	   false)
     else if String.isPrefix "Refutation found. Thanks to Tanya" thisLine
     then
       (File.write (File.tmp_path (Path.basic "atp_response")) thisLine;
	startTransfer (Recon_Parse.start_V8, Recon_Parse.end_V8)
	      (fromChild, toParent, ppid, goalstring,
	       childCmd, thm, sg_num, clause_arr, num_of_clauses))
     else if (String.isPrefix "Satisfiability detected" thisLine) orelse
             (String.isPrefix "Refutation not found" thisLine)
     then
       (File.write (File.tmp_path (Path.basic "atp_response")) thisLine;
	TextIO.output (toParent,childCmd^"\n");
	TextIO.flushOut toParent;
	TextIO.output (proof_file, thisLine);
	TextIO.closeOut proof_file;
 
	TextIO.output (toParent, thisLine^"\n");
	TextIO.output (toParent, goalstring^"\n");
	TextIO.flushOut toParent;
	Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
	(* Attempt to prevent several signals from turning up simultaneously *)
	Posix.Process.sleep(Time.fromSeconds 1);
	true)
     else
       (TextIO.output (proof_file, thisLine);
	TextIO.flushOut proof_file;
	checkVampProofFound  (fromChild, toParent, ppid, 
	   goalstring,childCmd, thm, sg_num, clause_arr, num_of_clauses))
  end


fun checkEProofFound (fromChild, toParent, ppid,goalstring, childCmd,
                      thm, sg_num, clause_arr, num_of_clauses) = 
 let val E_proof_file = TextIO.openAppend
	   (File.platform_path(File.tmp_path (Path.basic "atp_proof")))
     val _ = File.write (File.tmp_path (Path.basic "atp_checking_prf"))
			("checking if proof found, thm is: " ^ string_of_thm thm)
     val thisLine = TextIO.inputLine fromChild  
 in   
     if thisLine = "" 
     then (TextIO.output (E_proof_file, ("No proof output seen \n"));
	    TextIO.closeOut E_proof_file;
	    false)
     else if thisLine = "# TSTP exit status: Unsatisfiable\n"
     then      
       (File.write (File.tmp_path (Path.basic "atp_response")) thisLine;
       startTransfer (Recon_Parse.start_E, Recon_Parse.end_E)
             (fromChild, toParent, ppid, goalstring,
	      childCmd, thm, sg_num, clause_arr, num_of_clauses))
     else if thisLine= "# Problem is satisfiable (or invalid), generating saturation derivation\n"
     then  
       (File.write (File.tmp_path (Path.basic "atp_response")) thisLine;
	TextIO.output (toParent,childCmd^"\n" );
	TextIO.flushOut toParent;
	TextIO.output (E_proof_file, thisLine);
	TextIO.closeOut E_proof_file;

	TextIO.output (toParent, thisLine^"\n");
	TextIO.output (toParent, goalstring^"\n");
	TextIO.flushOut toParent;
	Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
	(* Attempt to prevent several signals from turning up simultaneously *)
	Posix.Process.sleep(Time.fromSeconds 1);
	 true)
     else if thisLine = "# Failure: Resource limit exceeded (time)\n" 
     then  
       (File.write (File.tmp_path (Path.basic "atp_response")) thisLine;
	TextIO.output (toParent, thisLine^"\n");
	TextIO.output (toParent, goalstring^"\n");
	TextIO.flushOut toParent;
	Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
	TextIO.output (E_proof_file, "signalled parent\n");
	TextIO.closeOut E_proof_file;
	(* Attempt to prevent several signals from turning up simultaneously *)
	Posix.Process.sleep(Time.fromSeconds 1);
	true)
     else if thisLine = "# Failure: Resource limit exceeded (memory)\n"
     then
	(Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
	 TextIO.output (toParent,childCmd^"\n" );
	 TextIO.output (toParent, thisLine);
	 TextIO.flushOut toParent;
	 true)
     else
	(TextIO.output (E_proof_file, thisLine);
	TextIO.flushOut E_proof_file;
	checkEProofFound  (fromChild, toParent, ppid, goalstring,
	childCmd, thm, sg_num, clause_arr, num_of_clauses))
 end


(***********************************************************************)
(*  Function used by the Isabelle process to read in a Vampire proof   *)
(***********************************************************************)

fun getVampInput instr =
    let val thisLine = TextIO.inputLine instr
	val _ = File.write (File.tmp_path (Path.basic "atp_line")) thisLine
    in    (* reconstructed proof string *)
      if thisLine = "" then ("No output from reconstruction process.\n","")
      else if String.sub (thisLine, 0) = #"[" orelse (*FIXME: for SPASS?*)
              String.isPrefix "Satisfiability detected" thisLine orelse
              String.isPrefix "Refutation not found" thisLine orelse
              String.isPrefix "Rules from" thisLine
      then
	let val goalstring = TextIO.inputLine instr
	in (thisLine, goalstring) end
      else if thisLine = "Proof found but translation failed!"
      then
	 let val goalstring = TextIO.inputLine instr
	     val _ = debug "getVampInput: translation of proof failed"
	 in (thisLine, goalstring) end
      else getVampInput instr
    end


(***********************************************************************)
(*  Function used by the Isabelle process to read in an E proof   *)
(***********************************************************************)

fun getEInput instr =
    let val thisLine = TextIO.inputLine instr
	val _ = File.write (File.tmp_path (Path.basic "atp_line")) thisLine
    in    (* reconstructed proof string *)
      if thisLine = "" then ("No output from reconstruction process.\n","")
      else if String.isPrefix "# Problem is satisfiable" thisLine orelse
              String.isPrefix "# Cannot determine problem status" thisLine orelse
              String.isPrefix "# Failure:" thisLine
      then
	let val goalstring = TextIO.inputLine instr
	in (thisLine, goalstring) end
      else if thisLine = "Proof found but translation failed!"
      then
	 let val goalstring = TextIO.inputLine instr
	     val _ = debug "getEInput: translation of proof failed"
	 in (thisLine, goalstring) end
      else getEInput instr
    end

end;