--- a/src/HOL/Tools/ATP/VampCommunication.ML Mon Jul 04 15:15:55 2005 +0200
+++ b/src/HOL/Tools/ATP/VampCommunication.ML Mon Jul 04 15:51:56 2005 +0200
@@ -184,16 +184,36 @@
Posix.Process.sleep(Time.fromSeconds 1);
true
end)
- else if (thisLine = "% Proof not found.\n")
+ else if (thisLine = "% Proof not found. Time limit expired.\n")
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;
+ (let val outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_proof"))); (* val _ = Posix.Process.sleep(Time.fromSeconds 3 );*)
+ val _ = TextIO.output (outfile, (thisLine))
+
+ val _ = TextIO.closeOut outfile
+ in
- true)
+ TextIO.output (toParent,childCmd^"\n" );
+ TextIO.flushOut toParent;
+ TextIO.output (vamp_proof_file, (thisLine));
+ TextIO.flushOut vamp_proof_file;
+ TextIO.closeOut vamp_proof_file;
+ (*TextIO.output (toParent, thisLine);
+ TextIO.flushOut toParent;
+ TextIO.output (toParent, "bar\n");
+ TextIO.flushOut toParent;*)
+
+ TextIO.output (toParent, thisLine^"\n");
+ TextIO.flushOut toParent;
+ TextIO.output (toParent, thmstring^"\n");
+ TextIO.flushOut toParent;
+ TextIO.output (toParent, goalstring^"\n");
+ TextIO.flushOut toParent;
+ Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
+ (* Attempt to prevent several signals from turning up simultaneously *)
+ Posix.Process.sleep(Time.fromSeconds 1);
+ true
+ end
+ )
else
(TextIO.output (vamp_proof_file, (thisLine));
@@ -238,7 +258,7 @@
(reconstr, thmstring, goalstring)
end
)
- else if (thisLine = "% Proof not found.\n")
+ else if (thisLine = "% Proof not found. Time limit expired.\n")
then
(
let val reconstr = thisLine
--- a/src/HOL/Tools/ATP/watcher.ML Mon Jul 04 15:15:55 2005 +0200
+++ b/src/HOL/Tools/ATP/watcher.ML Mon Jul 04 15:51:56 2005 +0200
@@ -165,8 +165,8 @@
(prover^thmstring^goalstring^proverCmd^settings^
clasimpfile^hypsfile^probfile)
in sendOutput (toWatcherStr,
- (prover^"*"^thmstring^"*"^goalstring^"*"^proverCmd^"*"^
- settings^"*"^clasimpfile^"*"^hypsfile^"*"^probfile^"\n"));
+ (prover^"$"^thmstring^"$"^goalstring^"$"^proverCmd^"$"^
+ settings^"$"^clasimpfile^"$"^hypsfile^"$"^probfile^"\n"));
goals_being_watched := (!goals_being_watched) + 1;
TextIO.flushOut toWatcherStr;
callResProvers (toWatcherStr,args)
@@ -213,33 +213,33 @@
let val outfile = TextIO.openAppend(*("sep_field")*)(File.platform_path(File.tmp_path (Path.basic "sep_field")))
val _ = TextIO.output (outfile,("In separateFields, str is: "^(implode str)^"\n\n") )
val _ = TextIO.closeOut outfile
- val (prover, rest) = takeUntil "*" str []
+ val (prover, rest) = takeUntil "$" str []
val prover = implode prover
- val (thmstring, rest) = takeUntil "*" rest []
+ val (thmstring, rest) = takeUntil "$" rest []
val thmstring = implode thmstring
- val (goalstring, rest) = takeUntil "*" rest []
+ val (goalstring, rest) = takeUntil "$" rest []
val goalstring = implode goalstring
- val (proverCmd, rest ) = takeUntil "*" rest []
+ val (proverCmd, rest ) = takeUntil "$" rest []
val proverCmd = implode proverCmd
- val (settings, rest) = takeUntil "*" rest []
+ val (settings, rest) = takeUntil "$" rest []
val settings = getSettings settings []
- val (clasimpfile, rest ) = takeUntil "*" rest []
+ val (clasimpfile, rest ) = takeUntil "$" rest []
val clasimpfile = implode clasimpfile
- val (hypsfile, rest ) = takeUntil "*" rest []
+ val (hypsfile, rest ) = takeUntil "$" rest []
val hypsfile = implode hypsfile
- val (file, rest) = takeUntil "*" rest []
+ val (file, rest) = takeUntil "$" rest []
val file = implode file
val _ = File.append (File.tmp_path (Path.basic "sep_comms"))
("Sep comms are: "^(implode str)^"**"^
- prover^thmstring^goalstring^proverCmd^clasimpfile^hypsfile^file^"\n\n")
+ prover^" thmstring: "^thmstring^"\n goalstr: "^goalstring^" \n provercmd: "^proverCmd^" \n clasimp "^clasimpfile^" \n hyps "^hypsfile^"\n prob "^file^"\n\n")
in
(prover,thmstring,goalstring, proverCmd, settings, clasimpfile, hypsfile, file)
end
@@ -289,6 +289,7 @@
val newfile = if !SpassComm.spass
then
dfg_path^"/ax_prob"^"_"^(probID)^".dfg"
+
else
(File.platform_path wholefile)
val _ = File.append (File.tmp_path (Path.basic"thmstring_in_watcher"))
@@ -813,6 +814,8 @@
VampComm.getVampInput childin; Pretty.writeln(Pretty.str (oct_char "361"));() )
+
+
fun spass_proofHandler (n) = (
let val outfile = TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic "foo_signal1")));
val _ = TextIO.output (outfile, ("In signal handler now\n"))
@@ -844,9 +847,8 @@
else
()
)
- (* if there's no proof, but a message from Spass *)
- else if ((substring (reconstr, 0,5))= "SPASS")
- then
+ (* if there's no proof, but a some sort of message from Spass *)
+ else
(
goals_being_watched := (!goals_being_watched) -1;
Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
@@ -862,67 +864,7 @@
end )
else
()
- )
- (* 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")])));
- Pretty.writeln(Pretty.str (goalstring^reconstr));
- Pretty.writeln(Pretty.str (oct_char "361"));
- if (!goals_being_watched = 0)
- then
- (let val outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_reap_comp")));
- val _ = TextIO.output (outfile, ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n"))
- val _ = TextIO.closeOut outfile
- in
- killWatcher (childpid); reapWatcher (childpid,childin, childout);()
- end )
- else
- ()
- )
-
- (* 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")])));
- Pretty.writeln(Pretty.str (goalstring^(Recon_Transfer.restore_linebreaks reconstr)));
- Pretty.writeln(Pretty.str (oct_char "361"));
- if (!goals_being_watched = 0)
- then
- (let val outfile = TextIO.openOut(File.platform_path (File.tmp_path (Path.basic "foo_reap_comp")));
- val _ = TextIO.output (outfile, ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n"))
- val _ = TextIO.closeOut outfile
- in
- killWatcher (childpid); reapWatcher (childpid,childin, childout); ()
- end )
- else
- ( )
- )
-
-
- 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 ("Ran out of options in handler"));
- Pretty.writeln(Pretty.str (oct_char "361"));
- if (!goals_being_watched = 0)
- then
- (let val outfile = TextIO.openOut(File.platform_path (File.tmp_path (Path.basic "foo_reap_comp")));
- val _ = TextIO.output (outfile, ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n"))
- val _ = TextIO.closeOut outfile
- in
- killWatcher (childpid); reapWatcher (childpid,childin, childout); ()
- end )
- else
- ( )
- )
-
-
+ )
end)
--- a/src/HOL/Tools/res_atp.ML Mon Jul 04 15:15:55 2005 +0200
+++ b/src/HOL/Tools/res_atp.ML Mon Jul 04 15:51:56 2005 +0200
@@ -48,7 +48,6 @@
(*val spass = ref true;*)
val custom_spass = ref ["Auto=0","-IORe","-IOFc","-RTaut","-RFSub","-RBSub","-DocProof","-TimeLimit=60"];
-
val vampire = ref false;
val trace_res = ref false;
@@ -209,7 +208,7 @@
else
let val vampire = ResLib.helper_path "VAMPIRE_HOME" "vkernel"
in
- ([("vampire", thmstr, goalstring, vampire, "-t 300%-m 100000",
+ ([("vampire", thmstr, goalstring, vampire, "-t 60%-m 100000",
clasimpfile, axfile, hypsfile, probfile)] @
(make_atp_list xs sign (n+1)))
end