# HG changeset patch # User paulson # Date 1126863549 -7200 # Node ID 0eed5a1c00c10125047530e7ebc8a570e768dbbd # Parent c2efacfe8ab8703fea0116a59267f1e6e9508e20 PARTIAL conversion to Vampire8 diff -r c2efacfe8ab8 -r 0eed5a1c00c1 src/HOL/Tools/ATP/VampCommunication.ML --- 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 diff -r c2efacfe8ab8 -r 0eed5a1c00c1 src/HOL/Tools/ATP/recon_parse.ML --- 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 diff -r c2efacfe8ab8 -r 0eed5a1c00c1 src/HOL/Tools/ATP/watcher.ML --- 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); diff -r c2efacfe8ab8 -r 0eed5a1c00c1 src/HOL/Tools/res_atp.ML --- 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