src/HOL/Tools/ATP/AtpCommunication.ML
author paulson
Fri Dec 22 21:00:42 2006 +0100 (2006-12-22)
changeset 21900 f386d7eb17d1
parent 21888 c75a44597fb7
child 21918 71e312d6d19a
permissions -rw-r--r--
tidying the ATP communications
     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 * thm * int * string Vector.vector -> bool
    15     val checkVampProofFound: 
    16           TextIO.instream * TextIO.outstream * Posix.Process.pid * 
    17           string * thm * int * string Vector.vector -> bool
    18     val checkSpassProofFound:  
    19           TextIO.instream * TextIO.outstream * Posix.Process.pid * 
    20           string * thm * int * string Vector.vector -> 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 (**** retrieve the axioms that were used in the proof ****)
    36 
    37 (*Get names of axioms used. Axioms are indexed from 1, while the vector is indexed from 0*)
    38 fun get_axiom_names (thm_names: string vector) step_nums = 
    39     let fun is_axiom n = n <= Vector.length thm_names 
    40         fun index i = Vector.sub(thm_names, i-1)
    41         val axnums = List.filter is_axiom step_nums
    42         val axnames = sort_distinct string_ord (map index axnums)
    43     in
    44 	if length axnums = length step_nums then "UNSOUND!!" :: axnames
    45 	else axnames
    46     end
    47 
    48  (*String contains multiple lines. We want those of the form 
    49      "253[0:Inp] et cetera..."
    50   A list consisting of the first number in each line is returned. *)
    51 fun get_spass_linenums proofstr = 
    52   let val toks = String.tokens (not o Char.isAlphaNum)
    53       fun inputno (ntok::"0"::"Inp"::_) = Int.fromString ntok
    54         | inputno _ = NONE
    55       val lines = String.tokens (fn c => c = #"\n") proofstr
    56   in  List.mapPartial (inputno o toks) lines  end
    57 
    58 fun get_axiom_names_spass proofstr thm_names =
    59    get_axiom_names thm_names (get_spass_linenums proofstr);
    60     
    61 fun not_comma c = c <>  #",";
    62 
    63 (*A valid TSTP axiom line has the form  cnf(NNN,axiom,...) where NNN is a positive integer.*)
    64 fun parse_tstp_line s =
    65   let val ss = Substring.full (unprefix "cnf(" (nospaces s))
    66       val (intf,rest) = Substring.splitl not_comma ss
    67       val (rolef,rest) = Substring.splitl not_comma (Substring.triml 1 rest)
    68       (*We only allow negated_conjecture because the line number will be removed in
    69         get_axiom_names above, while suppressing the UNSOUND warning*)
    70       val ints = if Substring.string rolef mem_string ["axiom","negated_conjecture"]
    71                  then Substring.string intf 
    72                  else "error" 
    73   in  Int.fromString ints  end
    74   handle Fail _ => NONE; 
    75 
    76 fun get_axiom_names_tstp proofstr thm_names =
    77    get_axiom_names thm_names (List.mapPartial parse_tstp_line (split_lines proofstr));
    78     
    79  (*String contains multiple lines. We want those of the form 
    80      "*********** [448, input] ***********".
    81   A list consisting of the first number in each line is returned. *)
    82 fun get_vamp_linenums proofstr = 
    83   let val toks = String.tokens (not o Char.isAlphaNum)
    84       fun inputno [ntok,"input"] = Int.fromString ntok
    85         | inputno _ = NONE
    86       val lines = String.tokens (fn c => c = #"\n") proofstr
    87   in  List.mapPartial (inputno o toks) lines  end
    88 
    89 fun get_axiom_names_vamp proofstr thm_names =
    90    get_axiom_names thm_names (get_vamp_linenums proofstr);
    91     
    92 fun rules_to_string [] = "NONE"
    93   | rules_to_string xs = space_implode "  " xs
    94 
    95 
    96 (*The signal handler in watcher.ML must be able to read the output of this.*)
    97 fun prover_lemma_list_aux getax proofstr probfile toParent ppid thm_names = 
    98  let val _ = trace
    99                ("\n\nGetting lemma names. proofstr is " ^ proofstr ^
   100                 "\nprobfile is " ^ probfile ^
   101                 "  num of clauses is " ^ string_of_int (Vector.length thm_names))
   102      val ax_str = rules_to_string (getax proofstr thm_names)
   103     in 
   104 	 trace ("\nDone. Lemma list is " ^ ax_str);
   105          TextIO.output (toParent, "Success. Lemmas used in automatic proof: " ^
   106                   ax_str ^ "\n");
   107 	 TextIO.output (toParent, probfile ^ "\n");
   108 	 TextIO.flushOut toParent;
   109 	 Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2)
   110     end
   111     handle exn => (*FIXME: exn handler is too general!*)
   112      (trace ("\nprover_lemma_list_aux: In exception handler: " ^ 
   113              Toplevel.exn_message exn);
   114       TextIO.output (toParent, "Translation failed for the proof: " ^ 
   115                      String.toString proofstr ^ "\n");
   116       TextIO.output (toParent, probfile);
   117       TextIO.flushOut toParent;
   118       Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2));
   119 
   120 val e_lemma_list = prover_lemma_list_aux get_axiom_names_tstp;
   121 
   122 val vamp_lemma_list = prover_lemma_list_aux get_axiom_names_vamp;
   123 
   124 val spass_lemma_list = prover_lemma_list_aux get_axiom_names_spass;
   125 
   126 
   127 (**** Extracting proofs from an ATP's output ****)
   128 
   129 (*Return everything in s that comes before the string t*)
   130 fun cut_before t s = 
   131   let val (s1,s2) = Substring.position t (Substring.full s)
   132   in  if Substring.size s2 = 0 then error "cut_before: string not found" 
   133       else Substring.string s2
   134   end;
   135 
   136 val start_E = "# Proof object starts here."
   137 val end_E   = "# Proof object ends here."
   138 val start_V6 = "%================== Proof: ======================"
   139 val end_V6   = "%==============  End of proof. =================="
   140 val start_V8 = "=========== Refutation =========="
   141 val end_V8 = "======= End of refutation ======="
   142 val end_SPASS = "Formulae used in the proof"
   143 
   144 (*********************************************************************************)
   145 (*  Inspect the output of an ATP process to see if it has found a proof,     *)
   146 (*  and if so, transfer output to the input pipe of the main Isabelle process    *)
   147 (*********************************************************************************)
   148 
   149 fun startTransfer (endS, fromChild, toParent, ppid, probfile, th, sgno, thm_names) =
   150  let fun transferInput currentString =
   151       let val thisLine = TextIO.inputLine fromChild
   152       in
   153 	if thisLine = "" (*end of file?*)
   154 	then (trace ("\n extraction_failed.  End bracket: " ^ endS ^
   155 	             "\naccumulated text: " ^ currentString);
   156 	      raise EOF)                    
   157 	else if String.isPrefix endS thisLine
   158 	then let val proofextract = currentString ^ cut_before endS thisLine
   159 	         val lemma_list = if endS = end_V8 then vamp_lemma_list
   160 			  	  else if endS = end_SPASS then spass_lemma_list
   161 			  	  else e_lemma_list
   162 	     in
   163 	       trace ("\nExtracted proof:\n" ^ proofextract); 
   164 	       lemma_list proofextract probfile toParent ppid thm_names
   165 	     end
   166 	else transferInput (currentString^thisLine)
   167       end
   168  in
   169      transferInput "";  true
   170  end handle EOF => false
   171 
   172 
   173 (*The signal handler in watcher.ML must be able to read the output of this.*)
   174 fun signal_parent (toParent, ppid, msg, probfile) =
   175  (TextIO.output (toParent, msg);
   176   TextIO.output (toParent, probfile ^ "\n");
   177   TextIO.flushOut toParent;
   178   trace ("\nSignalled parent: " ^ msg ^ probfile);
   179   Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
   180   (*Give the parent time to respond before possibly sending another signal*)
   181   OS.Process.sleep (Time.fromMilliseconds 600));
   182 
   183 (*Called from watcher. Returns true if the Vampire process has returned a verdict.*)
   184 fun checkVampProofFound (fromChild, toParent, ppid, probfile, th, sgno, thm_names) =
   185  let val thisLine = TextIO.inputLine fromChild
   186  in   
   187      trace thisLine;
   188      if thisLine = "" 
   189      then (trace "\nNo proof output seen"; false)
   190      else if String.isPrefix start_V8 thisLine
   191      then startTransfer (end_V8, fromChild, toParent, ppid, probfile, th, sgno, thm_names)
   192      else if (String.isPrefix "Satisfiability detected" thisLine) orelse
   193              (String.isPrefix "Refutation not found" thisLine)
   194      then (signal_parent (toParent, ppid, "Failure\n", probfile);
   195 	   true)
   196      else checkVampProofFound  (fromChild, toParent, ppid, probfile, th, sgno, thm_names)
   197   end
   198 
   199 (*Called from watcher. Returns true if the E process has returned a verdict.*)
   200 fun checkEProofFound (fromChild, toParent, ppid, probfile, th, sgno, thm_names) = 
   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 String.isPrefix start_E thisLine
   206      then startTransfer (end_E, fromChild, toParent, ppid, probfile, th, sgno, thm_names)
   207      else if String.isPrefix "# Problem is satisfiable" thisLine
   208      then (signal_parent (toParent, ppid, "Invalid\n", probfile);
   209 	   true)
   210      else if String.isPrefix "# Cannot determine problem status within resource limit" thisLine
   211      then (signal_parent (toParent, ppid, "Failure\n", probfile);
   212 	   true)
   213      else checkEProofFound (fromChild, toParent, ppid, probfile, th, sgno, thm_names)
   214  end;
   215 
   216 (*Called from watcher. Returns true if the SPASS process has returned a verdict.*)
   217 fun checkSpassProofFound (fromChild, toParent, ppid, probfile, th, sgno, thm_names) = 
   218  let val thisLine = TextIO.inputLine fromChild  
   219  in    
   220      trace thisLine;
   221      if thisLine = "" then (trace "\nNo proof output seen"; false)
   222      else if String.isPrefix "Here is a proof" thisLine
   223      then      
   224         startTransfer (end_SPASS, fromChild, toParent, ppid, probfile, th, sgno, thm_names)
   225      else if thisLine = "SPASS beiseite: Completion found.\n"
   226      then (signal_parent (toParent, ppid, "Invalid\n", probfile);
   227 	   true)
   228      else if thisLine = "SPASS beiseite: Ran out of time.\n" orelse
   229              thisLine = "SPASS beiseite: Maximal number of loops exceeded.\n"
   230      then (signal_parent (toParent, ppid, "Failure\n", probfile);
   231 	   true)
   232     else checkSpassProofFound (fromChild, toParent, ppid, probfile, th, sgno, thm_names)
   233  end
   234 
   235 end;