src/HOL/Tools/ATP/AtpCommunication.ML

tidying, and support for axclass/classrel clauses

(*  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 ATP_COMMUNICATION =
  sig
    val reconstruct : bool ref
    val checkEProofFound: 
          TextIO.instream * TextIO.outstream * Posix.Process.pid * 
          string * string * (ResClause.clause * thm) Array.array -> bool
    val checkVampProofFound: 
          TextIO.instream * TextIO.outstream * Posix.Process.pid * 
          string * string * (ResClause.clause * thm) Array.array -> bool
    val checkSpassProofFound:  
          TextIO.instream * TextIO.outstream * Posix.Process.pid * 
          string * string * thm * int * (ResClause.clause * thm) Array.array -> bool
  end;

structure AtpCommunication : ATP_COMMUNICATION =
struct

(* switch for whether to reconstruct a proof found, or just list the lemmas used *)
val reconstruct = ref false;

exception EOF;

val start_E = "# Proof object starts here."
val end_E   = "# Proof object ends here."
val start_V6 = "%================== Proof: ======================"
val end_V6   = "%==============  End of proof. =================="
val start_V8 = "=========== Refutation =========="
val end_V8 = "======= End of refutation ======="

(*Identifies the start/end lines of an ATP's output*)
local open Recon_Parse in
fun extract_proof s =
  if cut_exists "Here is a proof with" s then
    (kill_lines 0
     o snd o cut_after ":"
     o snd o cut_after "Here is a proof with"
     o fst o cut_after " ||  -> .") s
  else if cut_exists start_V8 s then
    (kill_lines 0    (*Vampire 8.0*)
     o snd o cut_after start_V8
     o fst o cut_before end_V8) s
  else if cut_exists end_E s then
    (kill_lines 0    (*eproof*)
     o snd o cut_after start_E
     o fst o cut_before end_E) s
  else "??extract_proof failed" (*Couldn't find a proof*)
end;


(*********************************************************************************)
(*  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, clause_arr) =
 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 = extract_proof (currentString^thisLine)
	     in
	       File.write (File.tmp_path (Path.basic"extracted_prf")) proofextract; 
	       Recon_Transfer.prover_lemma_list proofextract goalstring toParent ppid clause_arr
	     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, first line is: " ^ thisLine);
     transferInput thisLine;
     true) handle EOF => false
   else
      startTransfer (startS,endS)
                    (fromChild, toParent, ppid, goalstring,
		     childCmd, clause_arr)
 end

(*Called from watcher. Returns true if the Vampire process has returned a verdict.*)
fun checkVampProofFound (fromChild, toParent, ppid, goalstring, childCmd, clause_arr) =
 let val proof_file = TextIO.openAppend
	   (File.platform_path(File.tmp_path (Path.basic "vampire_proof")))
     val _ = File.write (File.tmp_path (Path.basic "vampire_checking_prf"))
			("checking if proof found. childCmd is " ^ childCmd ^
			 "\ngoalstring is: " ^ goalstring)
     val thisLine = TextIO.inputLine fromChild
 in   
     File.write (File.tmp_path (Path.basic "vampire_response")) thisLine;
     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
       startTransfer (start_V8, end_V8)
	      (fromChild, toParent, ppid, goalstring,
	       childCmd, clause_arr)
     else if (String.isPrefix "Satisfiability detected" thisLine) orelse
             (String.isPrefix "Refutation not found" thisLine)
     then
       (TextIO.output (toParent, "Failure\n");
	TextIO.output (toParent, goalstring^"\n");
	TextIO.flushOut toParent;
	TextIO.output (proof_file, thisLine);
	TextIO.closeOut proof_file;
	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, clause_arr))
  end


(*Called from watcher. Returns true if the E process has returned a verdict.*)
fun checkEProofFound (fromChild, toParent, ppid,goalstring, childCmd, clause_arr) = 
 let val E_proof_file = TextIO.openAppend
	   (File.platform_path(File.tmp_path (Path.basic "e_proof")))
     val _ = File.write (File.tmp_path (Path.basic "e_checking_prf"))
			("checking if proof found. childCmd is " ^ childCmd ^
			 "\ngoalstring is: " ^ goalstring)
     val thisLine = TextIO.inputLine fromChild  
 in   
     File.write (File.tmp_path (Path.basic "e_response")) thisLine;
     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      
       startTransfer (start_E, end_E)
             (fromChild, toParent, ppid, goalstring, childCmd, clause_arr)
     else if String.isPrefix "# Problem is satisfiable" thisLine
     then  
       (TextIO.output (toParent, "Invalid\n");
	TextIO.output (toParent, goalstring^"\n");
	TextIO.flushOut toParent;
	TextIO.output (E_proof_file, thisLine);
	TextIO.closeOut E_proof_file;
	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 String.isPrefix "# Failure: Resource limit exceeded" thisLine
     then  (*In fact, E distingishes "out of time" and "out of memory"*)
       (File.write (File.tmp_path (Path.basic "e_response")) thisLine;
	TextIO.output (toParent, "Failure\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
	(TextIO.output (E_proof_file, thisLine);
	TextIO.flushOut E_proof_file;
	checkEProofFound (fromChild, toParent, ppid, goalstring, childCmd, clause_arr))
 end


(**********************************************************************)
(*  Reconstruct the Spass 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 spass_reconstruct_tac proofextract goalstring toParent ppid sg_num 
                    clause_arr = 
 SELECT_GOAL
  (EVERY1 [rtac ccontr, ObjectLogic.atomize_tac, skolemize_tac, 
	   METAHYPS(fn negs => 
  Recon_Transfer.spass_reconstruct proofextract goalstring toParent ppid negs clause_arr)]) sg_num;


fun transferSpassInput (fromChild, toParent, ppid, goalstring, 
                        currentString, thm, sg_num, clause_arr) = 
 let val thisLine = TextIO.inputLine fromChild 
 in 
    if thisLine = "" (*end of file?*)
    then (File.write (File.tmp_path (Path.basic"spass_extraction_failed")) currentString;
	  raise EOF)                    
    else if String.isPrefix "--------------------------SPASS-STOP" thisLine
    then 
      let val proofextract = extract_proof (currentString^thisLine)
      in 
	 File.write (File.tmp_path (Path.basic"spass_extracted_prf")) proofextract;
	 if !reconstruct 
	 then (spass_reconstruct_tac proofextract goalstring toParent ppid sg_num 
		clause_arr thm; ())
	 else Recon_Transfer.spass_lemma_list proofextract goalstring 
	        toParent ppid clause_arr 
      end
    else transferSpassInput (fromChild, toParent, ppid, goalstring,
			     (currentString^thisLine), thm, sg_num, clause_arr)
 end;


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

 
fun startSpassTransfer (fromChild, toParent, ppid, goalstring,childCmd,
                        thm, sg_num,clause_arr) = 
   let val thisLine = TextIO.inputLine fromChild  
   in                 
      if thisLine = "" then false
      else if String.isPrefix "Here is a proof" thisLine then     
	 (File.append (File.tmp_path (Path.basic "spass_transfer"))
		      ("about to transfer proof, thm is: " ^ string_of_thm thm ^ "\n");
	  transferSpassInput (fromChild, toParent, ppid, goalstring,thisLine, 
 	                     thm, sg_num,clause_arr);
	  true) handle EOF => false
      else startSpassTransfer (fromChild, toParent, ppid, goalstring,
                               childCmd, thm, sg_num,clause_arr)
    end


(*Called from watcher. Returns true if the E process has returned a verdict.*)
fun checkSpassProofFound (fromChild, toParent, ppid, goalstring, childCmd,
                          thm, sg_num, clause_arr) = 
 let val spass_proof_file = TextIO.openAppend
           (File.platform_path(File.tmp_path (Path.basic "spass_proof")))
     val _ = File.write(File.tmp_path (Path.basic "spass_checking_prf"))
		("checking if proof found, thm is: "^(string_of_thm thm))
     val thisLine = TextIO.inputLine fromChild  
 in    
     File.write (File.tmp_path (Path.basic "spass_response")) thisLine;
     if thisLine = "" 
     then (TextIO.output (spass_proof_file, ("No proof output seen \n"));
	   TextIO.closeOut spass_proof_file;
	   false)
     else if thisLine = "SPASS beiseite: Proof found.\n"
     then      
        startSpassTransfer (fromChild, toParent, ppid, goalstring,
	                    childCmd, thm, sg_num, clause_arr)
     else if thisLine = "SPASS beiseite: Completion found.\n"
     then  
       (TextIO.output (spass_proof_file, thisLine);
	TextIO.closeOut spass_proof_file;
	TextIO.output (toParent, "Invalid\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 = "SPASS beiseite: Ran out of time.\n" orelse
             thisLine = "SPASS beiseite: Maximal number of loops exceeded.\n"
     then  
       (TextIO.output (toParent, "Failure\n");
	TextIO.output (toParent, goalstring^"\n");
	TextIO.flushOut toParent;
	Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
	TextIO.output (spass_proof_file, "signalled parent\n");
	TextIO.closeOut spass_proof_file;
	(* Attempt to prevent several signals from turning up simultaneously *)
	Posix.Process.sleep(Time.fromSeconds 1);
	true)
    else
       (TextIO.output (spass_proof_file, thisLine);
       TextIO.flushOut spass_proof_file;
       checkSpassProofFound  (fromChild, toParent, ppid, goalstring,
       childCmd, thm, sg_num, clause_arr))
 end

end;