src/HOL/Tools/ATP/AtpCommunication.ML
author paulson
Fri Nov 24 16:38:42 2006 +0100 (2006-11-24)
changeset 21513 9e9fff87dc6c
parent 20826 32640c8956e7
child 21858 05f57309170c
permissions -rw-r--r--
Conversion of "equal" to "=" for TSTP format; big tidy-up
     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 checkEProofFound: 
    13           TextIO.instream * TextIO.outstream * Posix.Process.pid * 
    14           string * string Array.array -> bool
    15     val checkVampProofFound: 
    16           TextIO.instream * TextIO.outstream * Posix.Process.pid * 
    17           string * string Array.array -> bool
    18     val checkSpassProofFound:  
    19           TextIO.instream * TextIO.outstream * Posix.Process.pid * 
    20           string * thm * int * string Array.array -> bool
    21     val signal_parent:  
    22           TextIO.outstream * Posix.Process.pid * string * string -> unit
    23   end;
    24 
    25 structure AtpCommunication : ATP_COMMUNICATION =
    26 struct
    27 
    28 val trace_path = Path.basic "atp_trace";
    29 
    30 fun trace s = if !Output.show_debug_msgs then File.append (File.tmp_path trace_path) s 
    31               else ();
    32 
    33 exception EOF;
    34 
    35 
    36 (**** retrieve the axioms that were used in the proof ****)
    37 
    38 (*Get names of axioms used. Axioms are indexed from 1, while the array is indexed from 0*)
    39 fun get_axiom_names (names_arr: string array) step_nums = 
    40     let fun is_axiom n = n <= Array.length names_arr 
    41         fun index i = Array.sub(names_arr, i-1)
    42         val axnums = List.filter is_axiom step_nums
    43         val axnames = sort_distinct string_ord (map index axnums)
    44     in
    45 	if length axnums = length step_nums then "UNSOUND!!" :: axnames
    46 	else axnames
    47     end
    48 
    49  (*String contains multiple lines. We want those of the form 
    50      "253[0:Inp] et cetera..."
    51   A list consisting of the first number in each line is returned. *)
    52 fun get_spass_linenums proofstr = 
    53   let val toks = String.tokens (not o Char.isAlphaNum)
    54       fun inputno (ntok::"0"::"Inp"::_) = Int.fromString ntok
    55         | inputno _ = NONE
    56       val lines = String.tokens (fn c => c = #"\n") proofstr
    57   in  List.mapPartial (inputno o toks) lines  end
    58 
    59 fun get_axiom_names_spass proofstr names_arr =
    60    get_axiom_names names_arr (get_spass_linenums proofstr);
    61     
    62  (*String contains multiple lines. We want those of the form 
    63    "number : ...: ...: initial..." *)
    64 fun get_e_linenums proofstr = 
    65   let val fields = String.fields (fn c => c = #":")
    66       val nospaces = String.translate (fn c => if c = #" " then "" else str c)
    67       fun initial s = String.isPrefix "initial" (nospaces s)
    68       fun firstno (line :: _ :: _ :: rule :: _) = 
    69             if initial rule then Int.fromString line else NONE
    70         | firstno _ = NONE
    71       val lines = String.tokens (fn c => c = #"\n") proofstr
    72   in  List.mapPartial (firstno o fields) lines  end
    73 
    74 fun get_axiom_names_e proofstr names_arr =
    75    get_axiom_names names_arr (get_e_linenums proofstr);
    76     
    77  (*String contains multiple lines. We want those of the form 
    78      "*********** [448, input] ***********".
    79   A list consisting of the first number in each line is returned. *)
    80 fun get_vamp_linenums proofstr = 
    81   let val toks = String.tokens (not o Char.isAlphaNum)
    82       fun inputno [ntok,"input"] = Int.fromString ntok
    83         | inputno _ = NONE
    84       val lines = String.tokens (fn c => c = #"\n") proofstr
    85   in  List.mapPartial (inputno o toks) lines  end
    86 
    87 fun get_axiom_names_vamp proofstr names_arr =
    88    get_axiom_names names_arr (get_vamp_linenums proofstr);
    89     
    90 fun rules_to_string [] = "NONE"
    91   | rules_to_string xs = space_implode "  " xs
    92 
    93 
    94 (*The signal handler in watcher.ML must be able to read the output of this.*)
    95 fun prover_lemma_list_aux getax proofstr probfile toParent ppid names_arr = 
    96  let val _ = trace
    97                ("\n\nGetting lemma names. proofstr is " ^ proofstr ^
    98                 "\nprobfile is " ^ probfile ^
    99                 "  num of clauses is " ^ string_of_int (Array.length names_arr))
   100      val axiom_names = getax proofstr names_arr
   101      val ax_str = rules_to_string axiom_names
   102     in 
   103 	 trace ("\nDone. Lemma list is " ^ ax_str);
   104          TextIO.output (toParent, "Success. Lemmas used in automatic proof: " ^
   105                   ax_str ^ "\n");
   106 	 TextIO.output (toParent, probfile ^ "\n");
   107 	 TextIO.flushOut toParent;
   108 	 Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2)
   109     end
   110     handle exn => (*FIXME: exn handler is too general!*)
   111      (trace ("\nprover_lemma_list_aux: In exception handler: " ^ 
   112              Toplevel.exn_message exn);
   113       TextIO.output (toParent, "Translation failed for the proof: " ^ 
   114                      String.toString proofstr ^ "\n");
   115       TextIO.output (toParent, probfile);
   116       TextIO.flushOut toParent;
   117       Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2));
   118 
   119 val e_lemma_list = prover_lemma_list_aux get_axiom_names_e;
   120 
   121 val vamp_lemma_list = prover_lemma_list_aux get_axiom_names_vamp;
   122 
   123 val spass_lemma_list = prover_lemma_list_aux get_axiom_names_spass;
   124 
   125 
   126 (**** Extracting proofs from an ATP's output ****)
   127 
   128 (*Return everything in s that comes before the string t*)
   129 fun cut_before t s = 
   130   let val (s1,s2) = Substring.position t (Substring.full s)
   131       val _ = assert (Substring.size s2 <> 0) "cut_before: string not found" 
   132   in Substring.string s2 end;
   133 
   134 val start_E = "# Proof object starts here."
   135 val end_E   = "# Proof object ends here."
   136 val start_V6 = "%================== Proof: ======================"
   137 val end_V6   = "%==============  End of proof. =================="
   138 val start_V8 = "=========== Refutation =========="
   139 val end_V8 = "======= End of refutation ======="
   140 val end_SPASS = "Formulae used in the proof"
   141 
   142 (*********************************************************************************)
   143 (*  Inspect the output of an ATP process to see if it has found a proof,     *)
   144 (*  and if so, transfer output to the input pipe of the main Isabelle process    *)
   145 (*********************************************************************************)
   146 
   147 fun startTransfer (endS, fromChild, toParent, ppid, probfile, names_arr) =
   148  let fun transferInput currentString =
   149       let val thisLine = TextIO.inputLine fromChild
   150       in
   151 	if thisLine = "" (*end of file?*)
   152 	then (trace ("\n extraction_failed.  End bracket: " ^ endS ^
   153 	             "\naccumulated text: " ^ currentString);
   154 	      raise EOF)                    
   155 	else if String.isPrefix endS thisLine
   156 	then let val proofextract = currentString ^ cut_before endS thisLine
   157 	         val lemma_list = if endS = end_V8 then vamp_lemma_list
   158 			  	  else e_lemma_list
   159 	     in
   160 	       trace ("\nExtracted proof:\n" ^ proofextract); 
   161 	       lemma_list proofextract probfile toParent ppid names_arr
   162 	     end
   163 	else transferInput (currentString^thisLine)
   164       end
   165  in
   166      transferInput "";  true
   167  end handle EOF => false
   168 
   169 
   170 (*The signal handler in watcher.ML must be able to read the output of this.*)
   171 fun signal_parent (toParent, ppid, msg, probfile) =
   172  (TextIO.output (toParent, msg);
   173   TextIO.output (toParent, probfile ^ "\n");
   174   TextIO.flushOut toParent;
   175   trace ("\nSignalled parent: " ^ msg ^ probfile);
   176   Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
   177   (*Give the parent time to respond before possibly sending another signal*)
   178   OS.Process.sleep (Time.fromMilliseconds 600));
   179 
   180 (*Called from watcher. Returns true if the Vampire process has returned a verdict.*)
   181 fun checkVampProofFound (fromChild, toParent, ppid, probfile, names_arr) =
   182  let val thisLine = TextIO.inputLine fromChild
   183  in   
   184      trace thisLine;
   185      if thisLine = "" 
   186      then (trace "\nNo proof output seen"; false)
   187      else if String.isPrefix start_V8 thisLine
   188      then startTransfer (end_V8, fromChild, toParent, ppid, probfile, names_arr)
   189      else if (String.isPrefix "Satisfiability detected" thisLine) orelse
   190              (String.isPrefix "Refutation not found" thisLine)
   191      then (signal_parent (toParent, ppid, "Failure\n", probfile);
   192 	   true)
   193      else checkVampProofFound  (fromChild, toParent, ppid, probfile, names_arr)
   194   end
   195 
   196 (*Called from watcher. Returns true if the E process has returned a verdict.*)
   197 fun checkEProofFound (fromChild, toParent, ppid, probfile, names_arr) = 
   198  let val thisLine = TextIO.inputLine fromChild  
   199  in   
   200      trace thisLine;
   201      if thisLine = "" then (trace "\nNo proof output seen"; false)
   202      else if String.isPrefix start_E thisLine
   203      then startTransfer (end_E, fromChild, toParent, ppid, probfile, names_arr)
   204      else if String.isPrefix "# Problem is satisfiable" thisLine
   205      then (signal_parent (toParent, ppid, "Invalid\n", probfile);
   206 	   true)
   207      else if String.isPrefix "# Cannot determine problem status within resource limit" thisLine
   208      then (signal_parent (toParent, ppid, "Failure\n", probfile);
   209 	   true)
   210      else checkEProofFound (fromChild, toParent, ppid, probfile, names_arr)
   211  end
   212 
   213 (*FIXME: can't these two functions be replaced by startTransfer above?*)
   214 fun transferSpassInput (fromChild, toParent, ppid, probfile,
   215                         currentString, thm, sg_num, names_arr) = 
   216  let val thisLine = TextIO.inputLine fromChild 
   217  in 
   218     trace thisLine;
   219     if thisLine = "" (*end of file?*)
   220     then (trace ("\nspass_extraction_failed: " ^ currentString);
   221 	  raise EOF)                    
   222     else if String.isPrefix "Formulae used in the proof" thisLine
   223     then 
   224       let val proofextract = currentString ^ cut_before end_SPASS thisLine
   225       in 
   226 	 trace ("\nextracted spass proof: " ^ proofextract);
   227 	 spass_lemma_list proofextract probfile toParent ppid names_arr 
   228       end
   229     else transferSpassInput (fromChild, toParent, ppid, probfile,
   230 			     currentString ^ thisLine, thm, sg_num, names_arr)
   231  end;
   232 
   233 (*Inspect the output of a SPASS process to see if it has found a proof,   
   234   and if so, transfer output to the input pipe of the main Isabelle process*)
   235 fun startSpassTransfer (fromChild, toParent, ppid, probfile, thm, sg_num,names_arr) = 
   236    let val thisLine = TextIO.inputLine fromChild  
   237    in                 
   238       if thisLine = "" then false
   239       else if String.isPrefix "Here is a proof" thisLine then     
   240 	 (trace ("\nabout to transfer SPASS proof:\n");
   241 	  transferSpassInput (fromChild, toParent, ppid, probfile, thisLine, 
   242  	                     thm, sg_num,names_arr);
   243 	  true) handle EOF => false
   244       else startSpassTransfer (fromChild, toParent, ppid, probfile, thm, sg_num,names_arr)
   245     end
   246 
   247 
   248 (*Called from watcher. Returns true if the SPASS process has returned a verdict.*)
   249 fun checkSpassProofFound (fromChild, toParent, ppid, probfile, thm, sg_num, names_arr) = 
   250  let val thisLine = TextIO.inputLine fromChild  
   251  in    
   252      trace thisLine;
   253      if thisLine = "" then (trace "\nNo proof output seen"; false)
   254      else if thisLine = "SPASS beiseite: Proof found.\n"
   255      then      
   256         startSpassTransfer (fromChild, toParent, ppid, probfile, thm, sg_num, names_arr)
   257      else if thisLine = "SPASS beiseite: Completion found.\n"
   258      then (signal_parent (toParent, ppid, "Invalid\n", probfile);
   259 	   true)
   260      else if thisLine = "SPASS beiseite: Ran out of time.\n" orelse
   261              thisLine = "SPASS beiseite: Maximal number of loops exceeded.\n"
   262      then (signal_parent (toParent, ppid, "Failure\n", probfile);
   263 	   true)
   264     else checkSpassProofFound (fromChild, toParent, ppid, probfile, thm, sg_num, names_arr)
   265  end
   266 
   267 end;