src/HOL/Tools/ATP/AtpCommunication.ML
author paulson
Mon Oct 10 15:35:29 2005 +0200 (2005-10-10)
changeset 17819 1241e5d31d5b
parent 17773 a7258e1020b7
child 18700 f04a8755d6ca
permissions -rw-r--r--
small tidy-up of utility functions
     1 (*  Title:      VampCommunication.ml
     2     ID:         $Id$
     3     Author:     Claire Quigley
     4     Copyright   2004  University of Cambridge
     5 *)
     6 
     7 (***************************************************************************)
     8 (*  Code to deal with the transfer of proofs from a Vampire process          *)
     9 (***************************************************************************)
    10 signature ATP_COMMUNICATION =
    11   sig
    12     val reconstruct : bool ref
    13     val checkEProofFound: 
    14           TextIO.instream * TextIO.outstream * Posix.Process.pid * 
    15           string * (ResClause.clause * thm) Array.array -> bool
    16     val checkVampProofFound: 
    17           TextIO.instream * TextIO.outstream * Posix.Process.pid * 
    18           string * (ResClause.clause * thm) Array.array -> bool
    19     val checkSpassProofFound:  
    20           TextIO.instream * TextIO.outstream * Posix.Process.pid * 
    21           string * thm * int * (ResClause.clause * thm) Array.array -> bool
    22     val signal_parent:  
    23           TextIO.outstream * Posix.Process.pid * string * string -> unit
    24   end;
    25 
    26 structure AtpCommunication : ATP_COMMUNICATION =
    27 struct
    28 
    29 (* switch for whether to reconstruct a proof found, or just list the lemmas used *)
    30 val reconstruct = ref false;
    31 
    32 val trace_path = Path.basic "atp_trace";
    33 
    34 fun trace s = if !Output.show_debug_msgs then File.append (File.tmp_path trace_path) s 
    35               else ();
    36 
    37 exception EOF;
    38 
    39 val start_E = "# Proof object starts here."
    40 val end_E   = "# Proof object ends here."
    41 val start_V6 = "%================== Proof: ======================"
    42 val end_V6   = "%==============  End of proof. =================="
    43 val start_V8 = "=========== Refutation =========="
    44 val end_V8 = "======= End of refutation ======="
    45 
    46 (*Identifies the start/end lines of an ATP's output*)
    47 local open Recon_Parse in
    48 fun extract_proof s =
    49   if cut_exists "Here is a proof with" s then
    50     (kill_lines 0
    51      o snd o cut_after ":"
    52      o snd o cut_after "Here is a proof with"
    53      o fst o cut_after " ||  -> .") s
    54   else if cut_exists end_V8 s then
    55     (kill_lines 0    (*Vampire 8.0*)
    56      o fst o cut_before end_V8) s
    57   else if cut_exists end_E s then
    58     (kill_lines 0    (*eproof*)
    59      o fst o cut_before end_E) s
    60   else "??extract_proof failed" (*Couldn't find a proof*)
    61 end;
    62 
    63 
    64 (*********************************************************************************)
    65 (*  Inspect the output of an ATP process to see if it has found a proof,     *)
    66 (*  and if so, transfer output to the input pipe of the main Isabelle process    *)
    67 (*********************************************************************************)
    68 
    69 fun startTransfer (endS, fromChild, toParent, ppid, probfile, clause_arr) =
    70  let fun transferInput currentString =
    71       let val thisLine = TextIO.inputLine fromChild
    72       in
    73 	if thisLine = "" (*end of file?*)
    74 	then (trace ("\n extraction_failed.  End bracket: " ^ endS ^
    75 	             "\naccumulated text: " ^ currentString);
    76 	      raise EOF)                    
    77 	else if String.isPrefix endS thisLine
    78 	then let val proofextract = extract_proof (currentString^thisLine)
    79 	         val lemma_list = if endS = end_V8 
    80 			  	  then Recon_Transfer.vamp_lemma_list
    81 			  	  else Recon_Transfer.e_lemma_list
    82 	     in
    83 	       trace ("\nExtracted proof:\n" ^ proofextract); 
    84 	       lemma_list proofextract probfile toParent ppid clause_arr
    85 	     end
    86 	else transferInput (currentString^thisLine)
    87       end
    88  in
    89      transferInput "";  true
    90  end handle EOF => false
    91 
    92 
    93 (*The signal handler in watcher.ML must be able to read the output of this.*)
    94 fun signal_parent (toParent, ppid, msg, probfile) =
    95  (TextIO.output (toParent, msg);
    96   TextIO.output (toParent, probfile ^ "\n");
    97   TextIO.flushOut toParent;
    98   trace ("\nSignalled parent: " ^ msg ^ probfile);
    99   Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
   100   (*Give the parent time to respond before possibly sending another signal*)
   101   OS.Process.sleep (Time.fromMilliseconds 600));
   102 
   103 (*Called from watcher. Returns true if the Vampire process has returned a verdict.*)
   104 fun checkVampProofFound (fromChild, toParent, ppid, probfile, clause_arr) =
   105  let val thisLine = TextIO.inputLine fromChild
   106  in   
   107      trace thisLine;
   108      if thisLine = "" 
   109      then (trace "\nNo proof output seen"; false)
   110      else if String.isPrefix start_V8 thisLine
   111      then startTransfer (end_V8, fromChild, toParent, ppid, probfile, clause_arr)
   112      else if (String.isPrefix "Satisfiability detected" thisLine) orelse
   113              (String.isPrefix "Refutation not found" thisLine)
   114      then (signal_parent (toParent, ppid, "Failure\n", probfile);
   115 	   true)
   116      else
   117         checkVampProofFound  (fromChild, toParent, ppid, probfile, clause_arr)
   118   end
   119 
   120 
   121 (*Called from watcher. Returns true if the E process has returned a verdict.*)
   122 fun checkEProofFound (fromChild, toParent, ppid, probfile, clause_arr) = 
   123  let val thisLine = TextIO.inputLine fromChild  
   124  in   
   125      trace thisLine;
   126      if thisLine = "" 
   127      then (trace "\nNo proof output seen"; false)
   128      else if String.isPrefix start_E thisLine
   129      then      
   130        startTransfer (end_E, fromChild, toParent, ppid, probfile, clause_arr)
   131      else if String.isPrefix "# Problem is satisfiable" thisLine
   132      then (signal_parent (toParent, ppid, "Invalid\n", probfile);
   133 	   true)
   134      else if String.isPrefix "# Cannot determine problem status within resource limit" thisLine
   135      then (signal_parent (toParent, ppid, "Failure\n", probfile);
   136 	   true)
   137      else
   138 	checkEProofFound (fromChild, toParent, ppid, probfile, clause_arr)
   139  end
   140 
   141 
   142 (**********************************************************************)
   143 (*  Reconstruct the Spass proof w.r.t. thmstring (string version of   *)
   144 (*  Isabelle goal to be proved), then transfer the reconstruction     *)
   145 (*  steps as a string to the input pipe of the main Isabelle process  *)
   146 (**********************************************************************)
   147 
   148 fun spass_reconstruct_tac proofextract toParent ppid probfile sg_num clause_arr = 
   149  SELECT_GOAL
   150   (EVERY1 [rtac ccontr, ObjectLogic.atomize_tac, skolemize_tac, 
   151 	   METAHYPS(fn negs => 
   152 		  Recon_Transfer.spass_reconstruct proofextract probfile 
   153 				toParent ppid negs clause_arr)]) sg_num;
   154 
   155 
   156 fun transferSpassInput (fromChild, toParent, ppid, probfile,
   157                         currentString, thm, sg_num, clause_arr) = 
   158  let val thisLine = TextIO.inputLine fromChild 
   159  in 
   160     trace thisLine;
   161     if thisLine = "" (*end of file?*)
   162     then (trace ("\nspass_extraction_failed: " ^ currentString);
   163 	  raise EOF)                    
   164     else if String.isPrefix "--------------------------SPASS-STOP" thisLine
   165     then 
   166       let val proofextract = extract_proof (currentString^thisLine)
   167       in 
   168 	 trace ("\nextracted spass proof: " ^ proofextract);
   169 	 if !reconstruct 
   170 	 then (spass_reconstruct_tac proofextract toParent ppid probfile sg_num 
   171 		clause_arr thm; ())
   172 	 else Recon_Transfer.spass_lemma_list proofextract probfile toParent
   173 	        ppid clause_arr 
   174       end
   175     else transferSpassInput (fromChild, toParent, ppid, probfile,
   176 			     (currentString^thisLine), thm, sg_num, clause_arr)
   177  end;
   178 
   179 
   180 (*********************************************************************************)
   181 (*  Inspect the output of a Spass   process to see if it has found a proof,     *)
   182 (*  and if so, transfer output to the input pipe of the main Isabelle process    *)
   183 (*********************************************************************************)
   184 
   185  
   186 fun startSpassTransfer (fromChild, toParent, ppid, probfile,
   187                         thm, sg_num,clause_arr) = 
   188    let val thisLine = TextIO.inputLine fromChild  
   189    in                 
   190       if thisLine = "" then false
   191       else if String.isPrefix "Here is a proof" thisLine then     
   192 	 (trace ("\nabout to transfer SPASS proof\n:");
   193 	  transferSpassInput (fromChild, toParent, ppid, probfile, thisLine, 
   194  	                     thm, sg_num,clause_arr);
   195 	  true) handle EOF => false
   196       else startSpassTransfer (fromChild, toParent, ppid, probfile, thm, sg_num,clause_arr)
   197     end
   198 
   199 
   200 (*Called from watcher. Returns true if the SPASS process has returned a verdict.*)
   201 fun checkSpassProofFound (fromChild, toParent, ppid, probfile,
   202                           thm, sg_num, clause_arr) = 
   203  let val thisLine = TextIO.inputLine fromChild  
   204  in    
   205      trace thisLine;
   206      if thisLine = "" then (trace "\nNo proof output seen"; false)
   207      else if thisLine = "SPASS beiseite: Proof found.\n"
   208      then      
   209         startSpassTransfer (fromChild, toParent, ppid, probfile, thm, sg_num, clause_arr)
   210      else if thisLine = "SPASS beiseite: Completion found.\n"
   211      then (signal_parent (toParent, ppid, "Invalid\n", probfile);
   212 	   true)
   213      else if thisLine = "SPASS beiseite: Ran out of time.\n" orelse
   214              thisLine = "SPASS beiseite: Maximal number of loops exceeded.\n"
   215      then (signal_parent (toParent, ppid, "Failure\n", probfile);
   216 	   true)
   217     else checkSpassProofFound (fromChild, toParent, ppid, probfile, thm, sg_num, clause_arr)
   218  end
   219 
   220 end;