tidying the ATP communications
authorpaulson
Fri Dec 22 21:00:42 2006 +0100 (2006-12-22)
changeset 21900f386d7eb17d1
parent 21899 dab16d14db60
child 21901 07d2a81f69c8
tidying the ATP communications
src/HOL/Tools/ATP/AtpCommunication.ML
src/HOL/Tools/ATP/watcher.ML
src/HOL/Tools/meson.ML
src/HOL/Tools/res_atp.ML
src/HOL/Tools/res_axioms.ML
     1.1 --- a/src/HOL/Tools/ATP/AtpCommunication.ML	Fri Dec 22 20:58:14 2006 +0100
     1.2 +++ b/src/HOL/Tools/ATP/AtpCommunication.ML	Fri Dec 22 21:00:42 2006 +0100
     1.3 @@ -11,10 +11,10 @@
     1.4    sig
     1.5      val checkEProofFound: 
     1.6            TextIO.instream * TextIO.outstream * Posix.Process.pid * 
     1.7 -          string * string Vector.vector -> bool
     1.8 +          string * thm * int * string Vector.vector -> bool
     1.9      val checkVampProofFound: 
    1.10            TextIO.instream * TextIO.outstream * Posix.Process.pid * 
    1.11 -          string * string Vector.vector -> bool
    1.12 +          string * thm * int * string Vector.vector -> bool
    1.13      val checkSpassProofFound:  
    1.14            TextIO.instream * TextIO.outstream * Posix.Process.pid * 
    1.15            string * thm * int * string Vector.vector -> bool
    1.16 @@ -32,7 +32,6 @@
    1.17  
    1.18  exception EOF;
    1.19  
    1.20 -
    1.21  (**** retrieve the axioms that were used in the proof ****)
    1.22  
    1.23  (*Get names of axioms used. Axioms are indexed from 1, while the vector is indexed from 0*)
    1.24 @@ -59,20 +58,23 @@
    1.25  fun get_axiom_names_spass proofstr thm_names =
    1.26     get_axiom_names thm_names (get_spass_linenums proofstr);
    1.27      
    1.28 - (*String contains multiple lines. We want those of the form 
    1.29 -   "number : ...: ...: initial..." *)
    1.30 -fun get_e_linenums proofstr = 
    1.31 -  let val fields = String.fields (fn c => c = #":")
    1.32 -      val nospaces = String.translate (fn c => if c = #" " then "" else str c)
    1.33 -      fun initial s = String.isPrefix "initial" (nospaces s)
    1.34 -      fun firstno (line :: _ :: _ :: rule :: _) = 
    1.35 -            if initial rule then Int.fromString line else NONE
    1.36 -        | firstno _ = NONE
    1.37 -      val lines = String.tokens (fn c => c = #"\n") proofstr
    1.38 -  in  List.mapPartial (firstno o fields) lines  end
    1.39 +fun not_comma c = c <>  #",";
    1.40  
    1.41 -fun get_axiom_names_e proofstr thm_names =
    1.42 -   get_axiom_names thm_names (get_e_linenums proofstr);
    1.43 +(*A valid TSTP axiom line has the form  cnf(NNN,axiom,...) where NNN is a positive integer.*)
    1.44 +fun parse_tstp_line s =
    1.45 +  let val ss = Substring.full (unprefix "cnf(" (nospaces s))
    1.46 +      val (intf,rest) = Substring.splitl not_comma ss
    1.47 +      val (rolef,rest) = Substring.splitl not_comma (Substring.triml 1 rest)
    1.48 +      (*We only allow negated_conjecture because the line number will be removed in
    1.49 +        get_axiom_names above, while suppressing the UNSOUND warning*)
    1.50 +      val ints = if Substring.string rolef mem_string ["axiom","negated_conjecture"]
    1.51 +                 then Substring.string intf 
    1.52 +                 else "error" 
    1.53 +  in  Int.fromString ints  end
    1.54 +  handle Fail _ => NONE; 
    1.55 +
    1.56 +fun get_axiom_names_tstp proofstr thm_names =
    1.57 +   get_axiom_names thm_names (List.mapPartial parse_tstp_line (split_lines proofstr));
    1.58      
    1.59   (*String contains multiple lines. We want those of the form 
    1.60       "*********** [448, input] ***********".
    1.61 @@ -97,8 +99,7 @@
    1.62                 ("\n\nGetting lemma names. proofstr is " ^ proofstr ^
    1.63                  "\nprobfile is " ^ probfile ^
    1.64                  "  num of clauses is " ^ string_of_int (Vector.length thm_names))
    1.65 -     val axiom_names = getax proofstr thm_names
    1.66 -     val ax_str = rules_to_string axiom_names
    1.67 +     val ax_str = rules_to_string (getax proofstr thm_names)
    1.68      in 
    1.69  	 trace ("\nDone. Lemma list is " ^ ax_str);
    1.70           TextIO.output (toParent, "Success. Lemmas used in automatic proof: " ^
    1.71 @@ -116,7 +117,7 @@
    1.72        TextIO.flushOut toParent;
    1.73        Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2));
    1.74  
    1.75 -val e_lemma_list = prover_lemma_list_aux get_axiom_names_e;
    1.76 +val e_lemma_list = prover_lemma_list_aux get_axiom_names_tstp;
    1.77  
    1.78  val vamp_lemma_list = prover_lemma_list_aux get_axiom_names_vamp;
    1.79  
    1.80 @@ -128,9 +129,9 @@
    1.81  (*Return everything in s that comes before the string t*)
    1.82  fun cut_before t s = 
    1.83    let val (s1,s2) = Substring.position t (Substring.full s)
    1.84 -      val _ = Substring.size s2 <> 0
    1.85 -        orelse error "cut_before: string not found"
    1.86 -  in Substring.string s2 end;
    1.87 +  in  if Substring.size s2 = 0 then error "cut_before: string not found" 
    1.88 +      else Substring.string s2
    1.89 +  end;
    1.90  
    1.91  val start_E = "# Proof object starts here."
    1.92  val end_E   = "# Proof object ends here."
    1.93 @@ -145,7 +146,7 @@
    1.94  (*  and if so, transfer output to the input pipe of the main Isabelle process    *)
    1.95  (*********************************************************************************)
    1.96  
    1.97 -fun startTransfer (endS, fromChild, toParent, ppid, probfile, thm_names) =
    1.98 +fun startTransfer (endS, fromChild, toParent, ppid, probfile, th, sgno, thm_names) =
    1.99   let fun transferInput currentString =
   1.100        let val thisLine = TextIO.inputLine fromChild
   1.101        in
   1.102 @@ -156,6 +157,7 @@
   1.103  	else if String.isPrefix endS thisLine
   1.104  	then let val proofextract = currentString ^ cut_before endS thisLine
   1.105  	         val lemma_list = if endS = end_V8 then vamp_lemma_list
   1.106 +			  	  else if endS = end_SPASS then spass_lemma_list
   1.107  			  	  else e_lemma_list
   1.108  	     in
   1.109  	       trace ("\nExtracted proof:\n" ^ proofextract); 
   1.110 @@ -179,82 +181,47 @@
   1.111    OS.Process.sleep (Time.fromMilliseconds 600));
   1.112  
   1.113  (*Called from watcher. Returns true if the Vampire process has returned a verdict.*)
   1.114 -fun checkVampProofFound (fromChild, toParent, ppid, probfile, thm_names) =
   1.115 +fun checkVampProofFound (fromChild, toParent, ppid, probfile, th, sgno, thm_names) =
   1.116   let val thisLine = TextIO.inputLine fromChild
   1.117   in   
   1.118       trace thisLine;
   1.119       if thisLine = "" 
   1.120       then (trace "\nNo proof output seen"; false)
   1.121       else if String.isPrefix start_V8 thisLine
   1.122 -     then startTransfer (end_V8, fromChild, toParent, ppid, probfile, thm_names)
   1.123 +     then startTransfer (end_V8, fromChild, toParent, ppid, probfile, th, sgno, thm_names)
   1.124       else if (String.isPrefix "Satisfiability detected" thisLine) orelse
   1.125               (String.isPrefix "Refutation not found" thisLine)
   1.126       then (signal_parent (toParent, ppid, "Failure\n", probfile);
   1.127  	   true)
   1.128 -     else checkVampProofFound  (fromChild, toParent, ppid, probfile, thm_names)
   1.129 +     else checkVampProofFound  (fromChild, toParent, ppid, probfile, th, sgno, thm_names)
   1.130    end
   1.131  
   1.132  (*Called from watcher. Returns true if the E process has returned a verdict.*)
   1.133 -fun checkEProofFound (fromChild, toParent, ppid, probfile, thm_names) = 
   1.134 +fun checkEProofFound (fromChild, toParent, ppid, probfile, th, sgno, thm_names) = 
   1.135   let val thisLine = TextIO.inputLine fromChild  
   1.136   in   
   1.137       trace thisLine;
   1.138       if thisLine = "" then (trace "\nNo proof output seen"; false)
   1.139       else if String.isPrefix start_E thisLine
   1.140 -     then startTransfer (end_E, fromChild, toParent, ppid, probfile, thm_names)
   1.141 +     then startTransfer (end_E, fromChild, toParent, ppid, probfile, th, sgno, thm_names)
   1.142       else if String.isPrefix "# Problem is satisfiable" thisLine
   1.143       then (signal_parent (toParent, ppid, "Invalid\n", probfile);
   1.144  	   true)
   1.145       else if String.isPrefix "# Cannot determine problem status within resource limit" thisLine
   1.146       then (signal_parent (toParent, ppid, "Failure\n", probfile);
   1.147  	   true)
   1.148 -     else checkEProofFound (fromChild, toParent, ppid, probfile, thm_names)
   1.149 - end
   1.150 -
   1.151 -(*FIXME: can't these two functions be replaced by startTransfer above?*)
   1.152 -fun transferSpassInput (fromChild, toParent, ppid, probfile,
   1.153 -                        currentString, thm, sg_num, thm_names) = 
   1.154 - let val thisLine = TextIO.inputLine fromChild 
   1.155 - in 
   1.156 -    trace thisLine;
   1.157 -    if thisLine = "" (*end of file?*)
   1.158 -    then (trace ("\nspass_extraction_failed: " ^ currentString);
   1.159 -	  raise EOF)                    
   1.160 -    else if String.isPrefix "Formulae used in the proof" thisLine
   1.161 -    then 
   1.162 -      let val proofextract = currentString ^ cut_before end_SPASS thisLine
   1.163 -      in 
   1.164 -	 trace ("\nextracted spass proof: " ^ proofextract);
   1.165 -	 spass_lemma_list proofextract probfile toParent ppid thm_names 
   1.166 -      end
   1.167 -    else transferSpassInput (fromChild, toParent, ppid, probfile,
   1.168 -			     currentString ^ thisLine, thm, sg_num, thm_names)
   1.169 +     else checkEProofFound (fromChild, toParent, ppid, probfile, th, sgno, thm_names)
   1.170   end;
   1.171  
   1.172 -(*Inspect the output of a SPASS process to see if it has found a proof,   
   1.173 -  and if so, transfer output to the input pipe of the main Isabelle process*)
   1.174 -fun startSpassTransfer (fromChild, toParent, ppid, probfile, thm, sg_num,thm_names) = 
   1.175 -   let val thisLine = TextIO.inputLine fromChild  
   1.176 -   in                 
   1.177 -      if thisLine = "" then false
   1.178 -      else if String.isPrefix "Here is a proof" thisLine then     
   1.179 -	 (trace ("\nabout to transfer SPASS proof:\n");
   1.180 -	  transferSpassInput (fromChild, toParent, ppid, probfile, thisLine, 
   1.181 - 	                     thm, sg_num,thm_names);
   1.182 -	  true) handle EOF => false
   1.183 -      else startSpassTransfer (fromChild, toParent, ppid, probfile, thm, sg_num,thm_names)
   1.184 -    end
   1.185 -
   1.186 -
   1.187  (*Called from watcher. Returns true if the SPASS process has returned a verdict.*)
   1.188 -fun checkSpassProofFound (fromChild, toParent, ppid, probfile, thm, sg_num, thm_names) = 
   1.189 +fun checkSpassProofFound (fromChild, toParent, ppid, probfile, th, sgno, thm_names) = 
   1.190   let val thisLine = TextIO.inputLine fromChild  
   1.191   in    
   1.192       trace thisLine;
   1.193       if thisLine = "" then (trace "\nNo proof output seen"; false)
   1.194 -     else if thisLine = "SPASS beiseite: Proof found.\n"
   1.195 +     else if String.isPrefix "Here is a proof" thisLine
   1.196       then      
   1.197 -        startSpassTransfer (fromChild, toParent, ppid, probfile, thm, sg_num, thm_names)
   1.198 +        startTransfer (end_SPASS, fromChild, toParent, ppid, probfile, th, sgno, thm_names)
   1.199       else if thisLine = "SPASS beiseite: Completion found.\n"
   1.200       then (signal_parent (toParent, ppid, "Invalid\n", probfile);
   1.201  	   true)
   1.202 @@ -262,7 +229,7 @@
   1.203               thisLine = "SPASS beiseite: Maximal number of loops exceeded.\n"
   1.204       then (signal_parent (toParent, ppid, "Failure\n", probfile);
   1.205  	   true)
   1.206 -    else checkSpassProofFound (fromChild, toParent, ppid, probfile, thm, sg_num, thm_names)
   1.207 +    else checkSpassProofFound (fromChild, toParent, ppid, probfile, th, sgno, thm_names)
   1.208   end
   1.209  
   1.210  end;
     2.1 --- a/src/HOL/Tools/ATP/watcher.ML	Fri Dec 22 20:58:14 2006 +0100
     2.2 +++ b/src/HOL/Tools/ATP/watcher.ML	Fri Dec 22 21:00:42 2006 +0100
     2.3 @@ -226,9 +226,9 @@
     2.4  	       let val _ = trace ("\nInput available from child: " ^ file)
     2.5  		   val childDone = (case prover of
     2.6  		       "vampire" => AtpCommunication.checkVampProofFound
     2.7 -			    (childIn, toParentStr, ppid, file, thm_names)  
     2.8 +			    (childIn, toParentStr, ppid, file, th, sgno, thm_names)  
     2.9  		     | "E" => AtpCommunication.checkEProofFound
    2.10 -			    (childIn, toParentStr, ppid, file, thm_names)             
    2.11 +			    (childIn, toParentStr, ppid, file, th, sgno, thm_names)             
    2.12  		     | "spass" => AtpCommunication.checkSpassProofFound
    2.13  			    (childIn, toParentStr, ppid, file, th, sgno, thm_names)  
    2.14  		     | _ => (trace ("\nBad prover! " ^ prover); true) )
     3.1 --- a/src/HOL/Tools/meson.ML	Fri Dec 22 20:58:14 2006 +0100
     3.2 +++ b/src/HOL/Tools/meson.ML	Fri Dec 22 21:00:42 2006 +0100
     3.3 @@ -193,7 +193,7 @@
     3.4  
     3.5  (*** The basic CNF transformation ***)
     3.6  
     3.7 -val max_clauses = ref 20;
     3.8 +val max_clauses = ref 40;
     3.9  
    3.10  fun sum x y = if x < !max_clauses andalso y < !max_clauses then x+y else !max_clauses;
    3.11  fun prod x y = if x < !max_clauses andalso y < !max_clauses then x*y else !max_clauses;
    3.12 @@ -648,7 +648,7 @@
    3.13  
    3.14  (*Top-level conversion to meta-level clauses. Each clause has  
    3.15    leading !!-bound universal variables, to express generality. To get 
    3.16 -  disjunctions instead of meta-clauses, remove "make_meta_clauses" below.*)
    3.17 +  meta-clauses instead of disjunctions, uncomment "make_meta_clauses" below.*)
    3.18  val make_clauses_tac = 
    3.19    SUBGOAL
    3.20      (fn (prop,_) =>
    3.21 @@ -658,7 +658,7 @@
    3.22  	    (fn hyps => 
    3.23                (Method.insert_tac
    3.24                  (map forall_intr_vars 
    3.25 -                  (make_meta_clauses (make_clauses hyps))) 1)),
    3.26 +                  ( (**make_meta_clauses**) (make_clauses hyps))) 1)),
    3.27  	  REPEAT_DETERM_N (length ts) o (etac thin_rl)]
    3.28       end);
    3.29       
     4.1 --- a/src/HOL/Tools/res_atp.ML	Fri Dec 22 20:58:14 2006 +0100
     4.2 +++ b/src/HOL/Tools/res_atp.ML	Fri Dec 22 21:00:42 2006 +0100
     4.3 @@ -807,7 +807,7 @@
     4.4                 let val Eprover = helper_path "E_HOME" "eproof"
     4.5                 in
     4.6                    ("E", Eprover,
     4.7 -                     "--tstp-in%-l5%-xAutoDev%-tAutoDev%--silent%--cpu-limit=" ^ time, probfile) ::
     4.8 +                     "--tstp-in%--tstp-out%-l5%-xAutoDev%-tAutoDev%--silent%--cpu-limit=" ^ time, probfile) ::
     4.9                     make_atp_list xs (n+1)
    4.10                 end
    4.11               else error ("Invalid prover name: " ^ !prover)
     5.1 --- a/src/HOL/Tools/res_axioms.ML	Fri Dec 22 20:58:14 2006 +0100
     5.2 +++ b/src/HOL/Tools/res_axioms.ML	Fri Dec 22 21:00:42 2006 +0100
     5.3 @@ -23,14 +23,14 @@
     5.4    val atpset_rules_of: Proof.context -> (string * thm) list
     5.5  end;
     5.6  
     5.7 -structure ResAxioms: RES_AXIOMS =
     5.8 +structure ResAxioms =
     5.9  struct
    5.10  
    5.11  (*For running the comparison between combinators and abstractions.
    5.12    CANNOT be a ref, as the setting is used while Isabelle is built.
    5.13    Currently FALSE, i.e. all the "abstraction" code below is unused, but so far
    5.14    it seems to be inferior to combinators...*)
    5.15 -val abstract_lambdas = false;
    5.16 +val abstract_lambdas = true;
    5.17  
    5.18  val trace_abs = ref false;
    5.19  
    5.20 @@ -527,9 +527,6 @@
    5.21  
    5.22  (**** Extract and Clausify theorems from a theory's claset and simpset ****)
    5.23  
    5.24 -(*Preserve the name of "th" after the transformation "f"*)
    5.25 -fun preserve_name f th = PureThy.put_name_hint (PureThy.get_name_hint th) (f th);
    5.26 -
    5.27  fun rules_of_claset cs =
    5.28    let val {safeIs,safeEs,hazIs,hazEs,...} = rep_cs cs
    5.29        val intros = safeIs @ hazIs