PARTIAL conversion to Vampire8
authorpaulson
Fri Sep 16 11:39:09 2005 +0200 (2005-09-16)
changeset 174350eed5a1c00c1
parent 17434 c2efacfe8ab8
child 17436 4e603046e539
PARTIAL conversion to Vampire8
src/HOL/Tools/ATP/VampCommunication.ML
src/HOL/Tools/ATP/recon_parse.ML
src/HOL/Tools/ATP/watcher.ML
src/HOL/Tools/res_atp.ML
     1.1 --- a/src/HOL/Tools/ATP/VampCommunication.ML	Fri Sep 16 11:38:49 2005 +0200
     1.2 +++ b/src/HOL/Tools/ATP/VampCommunication.ML	Fri Sep 16 11:39:09 2005 +0200
     1.3 @@ -95,14 +95,14 @@
     1.4       then (TextIO.output (proof_file, "No proof output seen \n");
     1.5  	   TextIO.closeOut proof_file;
     1.6  	   false)
     1.7 -     else if thisLine = "% Proof found. Thanks to Tanya!\n"
     1.8 +     else if String.isPrefix "Refutation found. Thanks to Tanya" thisLine
     1.9       then
    1.10         (File.write (File.tmp_path (Path.basic "atp_response")) thisLine;
    1.11 -	startTransfer (Recon_Parse.start_V6, Recon_Parse.end_V6)
    1.12 +	startTransfer (Recon_Parse.start_V8, Recon_Parse.end_V8)
    1.13  	      (fromChild, toParent, ppid, goalstring,
    1.14  	       childCmd, thm, sg_num, clause_arr, num_of_clauses))
    1.15 -     else if (thisLine = "% Unprovable.\n" ) orelse
    1.16 -             (thisLine = "% Proof not found. Time limit expired.\n")
    1.17 +     else if (String.isPrefix "Satisfiability detected" thisLine) orelse
    1.18 +             (String.isPrefix "Refutation not found" thisLine)
    1.19       then
    1.20         (File.write (File.tmp_path (Path.basic "atp_response")) thisLine;
    1.21  	TextIO.output (toParent,childCmd^"\n");
    1.22 @@ -174,7 +174,6 @@
    1.23       then
    1.24  	(Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
    1.25  	 TextIO.output (toParent,childCmd^"\n" );
    1.26 -	 TextIO.flushOut toParent;
    1.27  	 TextIO.output (toParent, thisLine);
    1.28  	 TextIO.flushOut toParent;
    1.29  	 true)
    1.30 @@ -195,9 +194,9 @@
    1.31  	val _ = File.write (File.tmp_path (Path.basic "atp_line")) thisLine
    1.32      in    (* reconstructed proof string *)
    1.33        if thisLine = "" then ("No output from reconstruction process.\n","")
    1.34 -      else if String.sub (thisLine, 0) = #"[" orelse
    1.35 -              thisLine = "% Unprovable.\n" orelse
    1.36 -              thisLine ="% Proof not found. Time limit expired.\n" orelse
    1.37 +      else if String.sub (thisLine, 0) = #"[" orelse (*FIXME: for SPASS?*)
    1.38 +              String.isPrefix "Satisfiability detected" thisLine orelse
    1.39 +              String.isPrefix "Refutation not found" thisLine orelse
    1.40                String.isPrefix "Rules from" thisLine
    1.41        then
    1.42  	let val goalstring = TextIO.inputLine instr
     2.1 --- a/src/HOL/Tools/ATP/recon_parse.ML	Fri Sep 16 11:38:49 2005 +0200
     2.2 +++ b/src/HOL/Tools/ATP/recon_parse.ML	Fri Sep 16 11:39:09 2005 +0200
     2.3 @@ -129,10 +129,10 @@
     2.4       o snd o cut_after ":"
     2.5       o snd o cut_after "Here is a proof with"
     2.6       o fst o cut_after " ||  -> .") s
     2.7 -  else if cut_exists start_V6 s then
     2.8 -    (kill_lines 0    (*Vampire 6.0*)
     2.9 -     o snd o cut_after start_V6
    2.10 -     o fst o cut_before end_V6) s
    2.11 +  else if cut_exists start_V8 s then
    2.12 +    (kill_lines 0    (*Vampire 8.0*)
    2.13 +     o snd o cut_after start_V8
    2.14 +     o fst o cut_before end_V8) s
    2.15    else if cut_exists end_E s then
    2.16      (kill_lines 0    (*eproof*)
    2.17       o snd o cut_after start_E
     3.1 --- a/src/HOL/Tools/ATP/watcher.ML	Fri Sep 16 11:38:49 2005 +0200
     3.2 +++ b/src/HOL/Tools/ATP/watcher.ML	Fri Sep 16 11:39:09 2005 +0200
     3.3 @@ -614,14 +614,20 @@
     3.4  
     3.5  
     3.6  fun createWatcher (thm,clause_arr, num_of_clauses) =
     3.7 - let val mychild = childInfo (setupWatcher(thm,clause_arr,  num_of_clauses))
     3.8 -     val streams = snd mychild
     3.9 -     val childin = fst streams
    3.10 -     val childout = snd streams
    3.11 -     val childpid = fst mychild
    3.12 + let val (childpid,(childin,childout)) =
    3.13 +           childInfo (setupWatcher(thm,clause_arr, num_of_clauses))
    3.14 +     fun decr_watched() =
    3.15 +	  (goals_being_watched := (!goals_being_watched) - 1;
    3.16 +	   if !goals_being_watched = 0
    3.17 +	   then 
    3.18 +	     (File.append (File.tmp_path (Path.basic "reap_found"))
    3.19 +	       ("Reaping a watcher, childpid = "^
    3.20 +		LargeWord.toString (Posix.Process.pidToWord childpid)^"\n");
    3.21 +	      killWatcher childpid; reapWatcher (childpid,childin, childout); ())
    3.22 +	    else ())
    3.23       val sign = sign_of_thm thm
    3.24       val prems = prems_of thm
    3.25 -     val prems_string =  Meson.concat_with_and (map (Sign.string_of_term sign) prems) 
    3.26 +     val prems_string = Meson.concat_with_and (map (Sign.string_of_term sign) prems) 
    3.27       val _ = debug ("subgoals forked to createWatcher: "^prems_string);
    3.28  (*FIXME: do we need an E proofHandler??*)
    3.29       fun vampire_proofHandler n =
    3.30 @@ -639,82 +645,35 @@
    3.31  	 then (Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
    3.32  	       Recon_Transfer.apply_res_thm reconstr goalstring;
    3.33  	       Pretty.writeln(Pretty.str  (oct_char "361"));
    3.34 -	       
    3.35 -	       goals_being_watched := (!goals_being_watched) - 1;
    3.36 -       
    3.37 -	       if !goals_being_watched = 0
    3.38 -	       then 
    3.39 -		  let val _ = File.write (File.tmp_path (Path.basic "reap_found"))
    3.40 -                                   ("Reaping a watcher, goals watched now "^
    3.41 -                                    string_of_int (!goals_being_watched)^"\n")
    3.42 -		   in
    3.43 -		       killWatcher childpid; reapWatcher (childpid,childin, childout); ()
    3.44 -		   end
    3.45 -		else () )
    3.46 +	       decr_watched())
    3.47  	 (* if there's no proof, but a message from Spass *)
    3.48  	 else if substring (reconstr, 0,5) = "SPASS"
    3.49 -	 then (goals_being_watched := (!goals_being_watched) -1;
    3.50 -	       Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
    3.51 +	 then (Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
    3.52  	       Pretty.writeln(Pretty.str ((Recon_Transfer.restore_linebreaks goalstring)^reconstr));
    3.53  	       Pretty.writeln(Pretty.str  (oct_char "361"));
    3.54 -	       if (!goals_being_watched = 0)
    3.55 -	       then (File.write (File.tmp_path (Path.basic "foo_reap_comp"))
    3.56 -	              ("Reaping a watcher, goals watched is: " ^
    3.57 -	                 (string_of_int (!goals_being_watched))^"\n");
    3.58 -	             killWatcher childpid; reapWatcher (childpid,childin, childout); ())
    3.59 -		else () ) 
    3.60 +	       decr_watched()) 
    3.61  	(* print out a list of rules used from clasimpset*)
    3.62  	 else if substring (reconstr, 0,5) = "Rules"
    3.63 -	 then (goals_being_watched := (!goals_being_watched) -1;
    3.64 -	       Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
    3.65 +	 then (Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
    3.66  	       Pretty.writeln(Pretty.str (goalstring^reconstr));
    3.67  	       Pretty.writeln(Pretty.str  (oct_char "361"));
    3.68 -	       if (!goals_being_watched = 0)
    3.69 -	       then (File.write (File.tmp_path (Path.basic "foo_reap_comp"))
    3.70 -	              ("Reaping a watcher, goals watched is: " ^
    3.71 -	                 (string_of_int (!goals_being_watched))^"\n");
    3.72 -	             killWatcher childpid;  reapWatcher (childpid,childin, childout);()
    3.73 -		     )
    3.74 -	       else () )
    3.75 +	       decr_watched())
    3.76  	  (* if proof translation failed *)
    3.77  	 else if substring (reconstr, 0,5) = "Proof"
    3.78 -	 then (goals_being_watched := (!goals_being_watched) -1;
    3.79 -	       Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
    3.80 +	 then (Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
    3.81  	       Pretty.writeln(Pretty.str (goalstring^(Recon_Transfer.restore_linebreaks reconstr)));
    3.82  	       Pretty.writeln(Pretty.str  (oct_char "361"));
    3.83 -	       if (!goals_being_watched = 0)
    3.84 -	       then (File.write (File.tmp_path (Path.basic "foo_reap_comp"))
    3.85 -	              ("Reaping a watcher, goals watched is: " ^
    3.86 -	                 (string_of_int (!goals_being_watched))^"\n");
    3.87 -	             killWatcher childpid;  reapWatcher (childpid,childin, childout);()
    3.88 -		     )
    3.89 -	       else () )
    3.90 -
    3.91 +	       decr_watched())
    3.92  	 else if substring (reconstr, 0,1) = "%"
    3.93 -	 then (goals_being_watched := (!goals_being_watched) -1;
    3.94 -	       Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
    3.95 +	 then (Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
    3.96  	       Pretty.writeln(Pretty.str (goalstring^(Recon_Transfer.restore_linebreaks reconstr)));
    3.97  	       Pretty.writeln(Pretty.str  (oct_char "361"));
    3.98 -	       if (!goals_being_watched = 0)
    3.99 -	       then (File.write (File.tmp_path (Path.basic "foo_reap_comp"))
   3.100 -	              ("Reaping a watcher, goals watched is: " ^
   3.101 -	                 (string_of_int (!goals_being_watched))^"\n");
   3.102 -	             killWatcher childpid;  reapWatcher (childpid,childin, childout);()
   3.103 -		     )
   3.104 -	       else () )
   3.105 -
   3.106 +	       decr_watched())
   3.107  	 else  (* add something here ?*)
   3.108 -	      (goals_being_watched := (!goals_being_watched) -1;
   3.109 -	       Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
   3.110 +	      (Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
   3.111  	       Pretty.writeln(Pretty.str ("Ran out of options in handler"));
   3.112  	       Pretty.writeln(Pretty.str  (oct_char "361"));
   3.113 -	       if (!goals_being_watched = 0)
   3.114 -	       then (File.write (File.tmp_path (Path.basic "foo_reap_comp"))
   3.115 -		     ("Reaping a watcher, goals watched is: " ^
   3.116 -			(string_of_int (!goals_being_watched))^"\n");
   3.117 -		    killWatcher childpid;  reapWatcher (childpid,childin, childout);()
   3.118 -		    )
   3.119 -	       else () )
   3.120 +	       decr_watched())
   3.121         end)
   3.122  
   3.123   in IsaSignal.signal (IsaSignal.usr1, IsaSignal.SIG_HANDLE vampire_proofHandler);
     4.1 --- a/src/HOL/Tools/res_atp.ML	Fri Sep 16 11:38:49 2005 +0200
     4.2 +++ b/src/HOL/Tools/res_atp.ML	Fri Sep 16 11:39:09 2005 +0200
     4.3 @@ -132,11 +132,10 @@
     4.4                end
     4.5              else if !prover = "vampire"
     4.6  	    then 
     4.7 -              let val vampire = ResLib.helper_path "VAMPIRE_HOME" "vkernel"
     4.8 +              let val vampire = ResLib.helper_path "VAMPIRE_HOME" "vampire"
     4.9                in
    4.10 -                ([("vampire", goalstring, vampire, "-t60%-m100000",
    4.11 -                   probfile)] @
    4.12 -                 (make_atp_list xs (n+1)))
    4.13 +                ([("vampire", goalstring, vampire, "-t 60%-m 100000", probfile)] @
    4.14 +                 (make_atp_list xs (n+1)))       (*BEWARE! spaces in options!*)
    4.15                end
    4.16        	     else if !prover = "E"
    4.17        	     then