src/HOL/Tools/ATP/AtpCommunication.ML
author haftmann
Tue May 09 10:09:37 2006 +0200 (2006-05-09)
changeset 19599 a5c7eb37d14f
parent 19199 b338c218cc6e
child 20762 a7a5157c5e75
permissions -rw-r--r--
added DatatypeHooks
     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 * string Array.array -> bool
    16     val checkVampProofFound: 
    17           TextIO.instream * TextIO.outstream * Posix.Process.pid * 
    18           string * string Array.array -> bool
    19     val checkSpassProofFound:  
    20           TextIO.instream * TextIO.outstream * Posix.Process.pid * 
    21           string * thm * int * string 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 "Formulae used in the proof" s then  (*SPASS*)
    50     (kill_lines 0
    51      o fst o cut_before "Formulae used in the proof") s
    52   else if cut_exists end_V8 s then
    53     (kill_lines 0    (*Vampire 8.0*)
    54      o fst o cut_before end_V8) s
    55   else if cut_exists end_E s then
    56     (kill_lines 0    (*eproof*)
    57      o fst o cut_before end_E) s
    58   else "??extract_proof failed" (*Couldn't find a proof*)
    59 end;
    60 
    61 
    62 (*********************************************************************************)
    63 (*  Inspect the output of an ATP process to see if it has found a proof,     *)
    64 (*  and if so, transfer output to the input pipe of the main Isabelle process    *)
    65 (*********************************************************************************)
    66 
    67 fun startTransfer (endS, fromChild, toParent, ppid, probfile, names_arr) =
    68  let fun transferInput currentString =
    69       let val thisLine = TextIO.inputLine fromChild
    70       in
    71 	if thisLine = "" (*end of file?*)
    72 	then (trace ("\n extraction_failed.  End bracket: " ^ endS ^
    73 	             "\naccumulated text: " ^ currentString);
    74 	      raise EOF)                    
    75 	else if String.isPrefix endS thisLine
    76 	then let val proofextract = extract_proof (currentString^thisLine)
    77 	         val lemma_list = if endS = end_V8 
    78 			  	  then Recon_Transfer.vamp_lemma_list
    79 			  	  else Recon_Transfer.e_lemma_list
    80 	     in
    81 	       trace ("\nExtracted proof:\n" ^ proofextract); 
    82 	       lemma_list proofextract probfile toParent ppid names_arr
    83 	     end
    84 	else transferInput (currentString^thisLine)
    85       end
    86  in
    87      transferInput "";  true
    88  end handle EOF => false
    89 
    90 
    91 (*The signal handler in watcher.ML must be able to read the output of this.*)
    92 fun signal_parent (toParent, ppid, msg, probfile) =
    93  (TextIO.output (toParent, msg);
    94   TextIO.output (toParent, probfile ^ "\n");
    95   TextIO.flushOut toParent;
    96   trace ("\nSignalled parent: " ^ msg ^ probfile);
    97   Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
    98   (*Give the parent time to respond before possibly sending another signal*)
    99   OS.Process.sleep (Time.fromMilliseconds 600));
   100 
   101 (*Called from watcher. Returns true if the Vampire process has returned a verdict.*)
   102 fun checkVampProofFound (fromChild, toParent, ppid, probfile, names_arr) =
   103  let val thisLine = TextIO.inputLine fromChild
   104  in   
   105      trace thisLine;
   106      if thisLine = "" 
   107      then (trace "\nNo proof output seen"; false)
   108      else if String.isPrefix start_V8 thisLine
   109      then startTransfer (end_V8, fromChild, toParent, ppid, probfile, names_arr)
   110      else if (String.isPrefix "Satisfiability detected" thisLine) orelse
   111              (String.isPrefix "Refutation not found" thisLine)
   112      then (signal_parent (toParent, ppid, "Failure\n", probfile);
   113 	   true)
   114      else
   115         checkVampProofFound  (fromChild, toParent, ppid, probfile, names_arr)
   116   end
   117 
   118 
   119 (*Called from watcher. Returns true if the E process has returned a verdict.*)
   120 fun checkEProofFound (fromChild, toParent, ppid, probfile, names_arr) = 
   121  let val thisLine = TextIO.inputLine fromChild  
   122  in   
   123      trace thisLine;
   124      if thisLine = "" 
   125      then (trace "\nNo proof output seen"; false)
   126      else if String.isPrefix start_E thisLine
   127      then      
   128        startTransfer (end_E, fromChild, toParent, ppid, probfile, names_arr)
   129      else if String.isPrefix "# Problem is satisfiable" thisLine
   130      then (signal_parent (toParent, ppid, "Invalid\n", probfile);
   131 	   true)
   132      else if String.isPrefix "# Cannot determine problem status within resource limit" thisLine
   133      then (signal_parent (toParent, ppid, "Failure\n", probfile);
   134 	   true)
   135      else
   136 	checkEProofFound (fromChild, toParent, ppid, probfile, names_arr)
   137  end
   138 
   139 
   140 (**********************************************************************)
   141 (*  Reconstruct the Spass proof w.r.t. thmstring (string version of   *)
   142 (*  Isabelle goal to be proved), then transfer the reconstruction     *)
   143 (*  steps as a string to the input pipe of the main Isabelle process  *)
   144 (**********************************************************************)
   145 
   146 fun spass_reconstruct_tac proofextract toParent ppid probfile sg_num names_arr = 
   147  SELECT_GOAL
   148   (EVERY1 [rtac ccontr, ObjectLogic.atomize_tac, skolemize_tac, 
   149 	   METAHYPS(fn negs => 
   150 		  Recon_Transfer.spass_reconstruct proofextract probfile 
   151 				toParent ppid negs names_arr)]) sg_num;
   152 
   153 
   154 fun transferSpassInput (fromChild, toParent, ppid, probfile,
   155                         currentString, thm, sg_num, names_arr) = 
   156  let val thisLine = TextIO.inputLine fromChild 
   157  in 
   158     trace thisLine;
   159     if thisLine = "" (*end of file?*)
   160     then (trace ("\nspass_extraction_failed: " ^ currentString);
   161 	  raise EOF)                    
   162     else if String.isPrefix "Formulae used in the proof" thisLine
   163     then 
   164       let val proofextract = extract_proof (currentString^thisLine)
   165       in 
   166 	 trace ("\nextracted spass proof: " ^ proofextract);
   167 	 if !reconstruct 
   168 	 then (spass_reconstruct_tac proofextract toParent ppid probfile sg_num 
   169 		names_arr thm; ())
   170 	 else Recon_Transfer.spass_lemma_list proofextract probfile toParent
   171 	        ppid names_arr 
   172       end
   173     else transferSpassInput (fromChild, toParent, ppid, probfile,
   174 			     (currentString^thisLine), thm, sg_num, names_arr)
   175  end;
   176 
   177 
   178 (*********************************************************************************)
   179 (*  Inspect the output of a Spass   process to see if it has found a proof,     *)
   180 (*  and if so, transfer output to the input pipe of the main Isabelle process    *)
   181 (*********************************************************************************)
   182 
   183  
   184 fun startSpassTransfer (fromChild, toParent, ppid, probfile,
   185                         thm, sg_num,names_arr) = 
   186    let val thisLine = TextIO.inputLine fromChild  
   187    in                 
   188       if thisLine = "" then false
   189       else if String.isPrefix "Here is a proof" thisLine then     
   190 	 (trace ("\nabout to transfer SPASS proof:\n");
   191 	  transferSpassInput (fromChild, toParent, ppid, probfile, thisLine, 
   192  	                     thm, sg_num,names_arr);
   193 	  true) handle EOF => false
   194       else startSpassTransfer (fromChild, toParent, ppid, probfile, thm, sg_num,names_arr)
   195     end
   196 
   197 
   198 (*Called from watcher. Returns true if the SPASS process has returned a verdict.*)
   199 fun checkSpassProofFound (fromChild, toParent, ppid, probfile,
   200                           thm, sg_num, names_arr) = 
   201  let val thisLine = TextIO.inputLine fromChild  
   202  in    
   203      trace thisLine;
   204      if thisLine = "" then (trace "\nNo proof output seen"; false)
   205      else if thisLine = "SPASS beiseite: Proof found.\n"
   206      then      
   207         startSpassTransfer (fromChild, toParent, ppid, probfile, thm, sg_num, names_arr)
   208      else if thisLine = "SPASS beiseite: Completion found.\n"
   209      then (signal_parent (toParent, ppid, "Invalid\n", probfile);
   210 	   true)
   211      else if thisLine = "SPASS beiseite: Ran out of time.\n" orelse
   212              thisLine = "SPASS beiseite: Maximal number of loops exceeded.\n"
   213      then (signal_parent (toParent, ppid, "Failure\n", probfile);
   214 	   true)
   215     else checkSpassProofFound (fromChild, toParent, ppid, probfile, thm, sg_num, names_arr)
   216  end
   217 
   218 end;