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