src/HOL/Tools/ATP/AtpCommunication.ML
author paulson
Wed Dec 20 17:03:46 2006 +0100 (2006-12-20)
changeset 21888 c75a44597fb7
parent 21858 05f57309170c
child 21900 f386d7eb17d1
permissions -rw-r--r--
change from "Array" to "Vector"
     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 Vector.vector -> bool
    15     val checkVampProofFound: 
    16           TextIO.instream * TextIO.outstream * Posix.Process.pid * 
    17           string * 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 
    36 (**** retrieve the axioms that were used in the proof ****)
    37 
    38 (*Get names of axioms used. Axioms are indexed from 1, while the vector is indexed from 0*)
    39 fun get_axiom_names (thm_names: string vector) step_nums = 
    40     let fun is_axiom n = n <= Vector.length thm_names 
    41         fun index i = Vector.sub(thm_names, 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 thm_names =
    60    get_axiom_names thm_names (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 thm_names =
    75    get_axiom_names thm_names (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 thm_names =
    88    get_axiom_names thm_names (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 thm_names = 
    96  let val _ = trace
    97                ("\n\nGetting lemma names. proofstr is " ^ proofstr ^
    98                 "\nprobfile is " ^ probfile ^
    99                 "  num of clauses is " ^ string_of_int (Vector.length thm_names))
   100      val axiom_names = getax proofstr thm_names
   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 _ = Substring.size s2 <> 0
   132         orelse error "cut_before: string not found"
   133   in Substring.string s2 end;
   134 
   135 val start_E = "# Proof object starts here."
   136 val end_E   = "# Proof object ends here."
   137 val start_V6 = "%================== Proof: ======================"
   138 val end_V6   = "%==============  End of proof. =================="
   139 val start_V8 = "=========== Refutation =========="
   140 val end_V8 = "======= End of refutation ======="
   141 val end_SPASS = "Formulae used in the proof"
   142 
   143 (*********************************************************************************)
   144 (*  Inspect the output of an ATP process to see if it has found a proof,     *)
   145 (*  and if so, transfer output to the input pipe of the main Isabelle process    *)
   146 (*********************************************************************************)
   147 
   148 fun startTransfer (endS, fromChild, toParent, ppid, probfile, thm_names) =
   149  let fun transferInput currentString =
   150       let val thisLine = TextIO.inputLine fromChild
   151       in
   152 	if thisLine = "" (*end of file?*)
   153 	then (trace ("\n extraction_failed.  End bracket: " ^ endS ^
   154 	             "\naccumulated text: " ^ currentString);
   155 	      raise EOF)                    
   156 	else if String.isPrefix endS thisLine
   157 	then let val proofextract = currentString ^ cut_before endS thisLine
   158 	         val lemma_list = if endS = end_V8 then vamp_lemma_list
   159 			  	  else e_lemma_list
   160 	     in
   161 	       trace ("\nExtracted proof:\n" ^ proofextract); 
   162 	       lemma_list proofextract probfile toParent ppid thm_names
   163 	     end
   164 	else transferInput (currentString^thisLine)
   165       end
   166  in
   167      transferInput "";  true
   168  end handle EOF => false
   169 
   170 
   171 (*The signal handler in watcher.ML must be able to read the output of this.*)
   172 fun signal_parent (toParent, ppid, msg, probfile) =
   173  (TextIO.output (toParent, msg);
   174   TextIO.output (toParent, probfile ^ "\n");
   175   TextIO.flushOut toParent;
   176   trace ("\nSignalled parent: " ^ msg ^ probfile);
   177   Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
   178   (*Give the parent time to respond before possibly sending another signal*)
   179   OS.Process.sleep (Time.fromMilliseconds 600));
   180 
   181 (*Called from watcher. Returns true if the Vampire process has returned a verdict.*)
   182 fun checkVampProofFound (fromChild, toParent, ppid, probfile, thm_names) =
   183  let val thisLine = TextIO.inputLine fromChild
   184  in   
   185      trace thisLine;
   186      if thisLine = "" 
   187      then (trace "\nNo proof output seen"; false)
   188      else if String.isPrefix start_V8 thisLine
   189      then startTransfer (end_V8, fromChild, toParent, ppid, probfile, thm_names)
   190      else if (String.isPrefix "Satisfiability detected" thisLine) orelse
   191              (String.isPrefix "Refutation not found" thisLine)
   192      then (signal_parent (toParent, ppid, "Failure\n", probfile);
   193 	   true)
   194      else checkVampProofFound  (fromChild, toParent, ppid, probfile, thm_names)
   195   end
   196 
   197 (*Called from watcher. Returns true if the E process has returned a verdict.*)
   198 fun checkEProofFound (fromChild, toParent, ppid, probfile, thm_names) = 
   199  let val thisLine = TextIO.inputLine fromChild  
   200  in   
   201      trace thisLine;
   202      if thisLine = "" then (trace "\nNo proof output seen"; false)
   203      else if String.isPrefix start_E thisLine
   204      then startTransfer (end_E, fromChild, toParent, ppid, probfile, thm_names)
   205      else if String.isPrefix "# Problem is satisfiable" thisLine
   206      then (signal_parent (toParent, ppid, "Invalid\n", probfile);
   207 	   true)
   208      else if String.isPrefix "# Cannot determine problem status within resource limit" thisLine
   209      then (signal_parent (toParent, ppid, "Failure\n", probfile);
   210 	   true)
   211      else checkEProofFound (fromChild, toParent, ppid, probfile, thm_names)
   212  end
   213 
   214 (*FIXME: can't these two functions be replaced by startTransfer above?*)
   215 fun transferSpassInput (fromChild, toParent, ppid, probfile,
   216                         currentString, thm, sg_num, thm_names) = 
   217  let val thisLine = TextIO.inputLine fromChild 
   218  in 
   219     trace thisLine;
   220     if thisLine = "" (*end of file?*)
   221     then (trace ("\nspass_extraction_failed: " ^ currentString);
   222 	  raise EOF)                    
   223     else if String.isPrefix "Formulae used in the proof" thisLine
   224     then 
   225       let val proofextract = currentString ^ cut_before end_SPASS thisLine
   226       in 
   227 	 trace ("\nextracted spass proof: " ^ proofextract);
   228 	 spass_lemma_list proofextract probfile toParent ppid thm_names 
   229       end
   230     else transferSpassInput (fromChild, toParent, ppid, probfile,
   231 			     currentString ^ thisLine, thm, sg_num, thm_names)
   232  end;
   233 
   234 (*Inspect the output of a SPASS process to see if it has found a proof,   
   235   and if so, transfer output to the input pipe of the main Isabelle process*)
   236 fun startSpassTransfer (fromChild, toParent, ppid, probfile, thm, sg_num,thm_names) = 
   237    let val thisLine = TextIO.inputLine fromChild  
   238    in                 
   239       if thisLine = "" then false
   240       else if String.isPrefix "Here is a proof" thisLine then     
   241 	 (trace ("\nabout to transfer SPASS proof:\n");
   242 	  transferSpassInput (fromChild, toParent, ppid, probfile, thisLine, 
   243  	                     thm, sg_num,thm_names);
   244 	  true) handle EOF => false
   245       else startSpassTransfer (fromChild, toParent, ppid, probfile, thm, sg_num,thm_names)
   246     end
   247 
   248 
   249 (*Called from watcher. Returns true if the SPASS process has returned a verdict.*)
   250 fun checkSpassProofFound (fromChild, toParent, ppid, probfile, thm, sg_num, thm_names) = 
   251  let val thisLine = TextIO.inputLine fromChild  
   252  in    
   253      trace thisLine;
   254      if thisLine = "" then (trace "\nNo proof output seen"; false)
   255      else if thisLine = "SPASS beiseite: Proof found.\n"
   256      then      
   257         startSpassTransfer (fromChild, toParent, ppid, probfile, thm, sg_num, thm_names)
   258      else if thisLine = "SPASS beiseite: Completion found.\n"
   259      then (signal_parent (toParent, ppid, "Invalid\n", probfile);
   260 	   true)
   261      else if thisLine = "SPASS beiseite: Ran out of time.\n" orelse
   262              thisLine = "SPASS beiseite: Maximal number of loops exceeded.\n"
   263      then (signal_parent (toParent, ppid, "Failure\n", probfile);
   264 	   true)
   265     else checkSpassProofFound (fromChild, toParent, ppid, probfile, thm, sg_num, thm_names)
   266  end
   267 
   268 end;