--- a/src/HOL/Tools/ATP/VampCommunication.ML Fri Sep 16 11:38:49 2005 +0200
+++ b/src/HOL/Tools/ATP/VampCommunication.ML Fri Sep 16 11:39:09 2005 +0200
@@ -95,14 +95,14 @@
then (TextIO.output (proof_file, "No proof output seen \n");
TextIO.closeOut proof_file;
false)
- else if thisLine = "% Proof found. Thanks to Tanya!\n"
+ else if String.isPrefix "Refutation found. Thanks to Tanya" thisLine
then
(File.write (File.tmp_path (Path.basic "atp_response")) thisLine;
- startTransfer (Recon_Parse.start_V6, Recon_Parse.end_V6)
+ startTransfer (Recon_Parse.start_V8, Recon_Parse.end_V8)
(fromChild, toParent, ppid, goalstring,
childCmd, thm, sg_num, clause_arr, num_of_clauses))
- else if (thisLine = "% Unprovable.\n" ) orelse
- (thisLine = "% Proof not found. Time limit expired.\n")
+ else if (String.isPrefix "Satisfiability detected" thisLine) orelse
+ (String.isPrefix "Refutation not found" thisLine)
then
(File.write (File.tmp_path (Path.basic "atp_response")) thisLine;
TextIO.output (toParent,childCmd^"\n");
@@ -174,7 +174,6 @@
then
(Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
TextIO.output (toParent,childCmd^"\n" );
- TextIO.flushOut toParent;
TextIO.output (toParent, thisLine);
TextIO.flushOut toParent;
true)
@@ -195,9 +194,9 @@
val _ = File.write (File.tmp_path (Path.basic "atp_line")) thisLine
in (* reconstructed proof string *)
if thisLine = "" then ("No output from reconstruction process.\n","")
- else if String.sub (thisLine, 0) = #"[" orelse
- thisLine = "% Unprovable.\n" orelse
- thisLine ="% Proof not found. Time limit expired.\n" orelse
+ else if String.sub (thisLine, 0) = #"[" orelse (*FIXME: for SPASS?*)
+ String.isPrefix "Satisfiability detected" thisLine orelse
+ String.isPrefix "Refutation not found" thisLine orelse
String.isPrefix "Rules from" thisLine
then
let val goalstring = TextIO.inputLine instr
--- a/src/HOL/Tools/ATP/recon_parse.ML Fri Sep 16 11:38:49 2005 +0200
+++ b/src/HOL/Tools/ATP/recon_parse.ML Fri Sep 16 11:39:09 2005 +0200
@@ -129,10 +129,10 @@
o snd o cut_after ":"
o snd o cut_after "Here is a proof with"
o fst o cut_after " || -> .") s
- else if cut_exists start_V6 s then
- (kill_lines 0 (*Vampire 6.0*)
- o snd o cut_after start_V6
- o fst o cut_before end_V6) s
+ else if cut_exists start_V8 s then
+ (kill_lines 0 (*Vampire 8.0*)
+ o snd o cut_after start_V8
+ o fst o cut_before end_V8) s
else if cut_exists end_E s then
(kill_lines 0 (*eproof*)
o snd o cut_after start_E
--- a/src/HOL/Tools/ATP/watcher.ML Fri Sep 16 11:38:49 2005 +0200
+++ b/src/HOL/Tools/ATP/watcher.ML Fri Sep 16 11:39:09 2005 +0200
@@ -614,14 +614,20 @@
fun createWatcher (thm,clause_arr, num_of_clauses) =
- let val mychild = childInfo (setupWatcher(thm,clause_arr, num_of_clauses))
- val streams = snd mychild
- val childin = fst streams
- val childout = snd streams
- val childpid = fst mychild
+ let val (childpid,(childin,childout)) =
+ childInfo (setupWatcher(thm,clause_arr, num_of_clauses))
+ fun decr_watched() =
+ (goals_being_watched := (!goals_being_watched) - 1;
+ if !goals_being_watched = 0
+ then
+ (File.append (File.tmp_path (Path.basic "reap_found"))
+ ("Reaping a watcher, childpid = "^
+ LargeWord.toString (Posix.Process.pidToWord childpid)^"\n");
+ killWatcher childpid; reapWatcher (childpid,childin, childout); ())
+ else ())
val sign = sign_of_thm thm
val prems = prems_of thm
- val prems_string = Meson.concat_with_and (map (Sign.string_of_term sign) prems)
+ val prems_string = Meson.concat_with_and (map (Sign.string_of_term sign) prems)
val _ = debug ("subgoals forked to createWatcher: "^prems_string);
(*FIXME: do we need an E proofHandler??*)
fun vampire_proofHandler n =
@@ -639,82 +645,35 @@
then (Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
Recon_Transfer.apply_res_thm reconstr goalstring;
Pretty.writeln(Pretty.str (oct_char "361"));
-
- goals_being_watched := (!goals_being_watched) - 1;
-
- if !goals_being_watched = 0
- then
- let val _ = File.write (File.tmp_path (Path.basic "reap_found"))
- ("Reaping a watcher, goals watched now "^
- string_of_int (!goals_being_watched)^"\n")
- in
- killWatcher childpid; reapWatcher (childpid,childin, childout); ()
- end
- else () )
+ decr_watched())
(* if there's no proof, but a message from Spass *)
else if substring (reconstr, 0,5) = "SPASS"
- then (goals_being_watched := (!goals_being_watched) -1;
- Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
+ then (Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
Pretty.writeln(Pretty.str ((Recon_Transfer.restore_linebreaks goalstring)^reconstr));
Pretty.writeln(Pretty.str (oct_char "361"));
- if (!goals_being_watched = 0)
- then (File.write (File.tmp_path (Path.basic "foo_reap_comp"))
- ("Reaping a watcher, goals watched is: " ^
- (string_of_int (!goals_being_watched))^"\n");
- killWatcher childpid; reapWatcher (childpid,childin, childout); ())
- else () )
+ decr_watched())
(* print out a list of rules used from clasimpset*)
else if substring (reconstr, 0,5) = "Rules"
- then (goals_being_watched := (!goals_being_watched) -1;
- Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
+ then (Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
Pretty.writeln(Pretty.str (goalstring^reconstr));
Pretty.writeln(Pretty.str (oct_char "361"));
- if (!goals_being_watched = 0)
- then (File.write (File.tmp_path (Path.basic "foo_reap_comp"))
- ("Reaping a watcher, goals watched is: " ^
- (string_of_int (!goals_being_watched))^"\n");
- killWatcher childpid; reapWatcher (childpid,childin, childout);()
- )
- else () )
+ decr_watched())
(* if proof translation failed *)
else if substring (reconstr, 0,5) = "Proof"
- then (goals_being_watched := (!goals_being_watched) -1;
- Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
+ then (Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
Pretty.writeln(Pretty.str (goalstring^(Recon_Transfer.restore_linebreaks reconstr)));
Pretty.writeln(Pretty.str (oct_char "361"));
- if (!goals_being_watched = 0)
- then (File.write (File.tmp_path (Path.basic "foo_reap_comp"))
- ("Reaping a watcher, goals watched is: " ^
- (string_of_int (!goals_being_watched))^"\n");
- killWatcher childpid; reapWatcher (childpid,childin, childout);()
- )
- else () )
-
+ decr_watched())
else if substring (reconstr, 0,1) = "%"
- then (goals_being_watched := (!goals_being_watched) -1;
- Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
+ then (Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
Pretty.writeln(Pretty.str (goalstring^(Recon_Transfer.restore_linebreaks reconstr)));
Pretty.writeln(Pretty.str (oct_char "361"));
- if (!goals_being_watched = 0)
- then (File.write (File.tmp_path (Path.basic "foo_reap_comp"))
- ("Reaping a watcher, goals watched is: " ^
- (string_of_int (!goals_being_watched))^"\n");
- killWatcher childpid; reapWatcher (childpid,childin, childout);()
- )
- else () )
-
+ decr_watched())
else (* add something here ?*)
- (goals_being_watched := (!goals_being_watched) -1;
- Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
+ (Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
Pretty.writeln(Pretty.str ("Ran out of options in handler"));
Pretty.writeln(Pretty.str (oct_char "361"));
- if (!goals_being_watched = 0)
- then (File.write (File.tmp_path (Path.basic "foo_reap_comp"))
- ("Reaping a watcher, goals watched is: " ^
- (string_of_int (!goals_being_watched))^"\n");
- killWatcher childpid; reapWatcher (childpid,childin, childout);()
- )
- else () )
+ decr_watched())
end)
in IsaSignal.signal (IsaSignal.usr1, IsaSignal.SIG_HANDLE vampire_proofHandler);
--- a/src/HOL/Tools/res_atp.ML Fri Sep 16 11:38:49 2005 +0200
+++ b/src/HOL/Tools/res_atp.ML Fri Sep 16 11:39:09 2005 +0200
@@ -132,11 +132,10 @@
end
else if !prover = "vampire"
then
- let val vampire = ResLib.helper_path "VAMPIRE_HOME" "vkernel"
+ let val vampire = ResLib.helper_path "VAMPIRE_HOME" "vampire"
in
- ([("vampire", goalstring, vampire, "-t60%-m100000",
- probfile)] @
- (make_atp_list xs (n+1)))
+ ([("vampire", goalstring, vampire, "-t 60%-m 100000", probfile)] @
+ (make_atp_list xs (n+1))) (*BEWARE! spaces in options!*)
end
else if !prover = "E"
then