Integrated vampire lemma code.
--- a/src/HOL/Tools/ATP/SpassCommunication.ML Tue Jun 21 21:41:08 2005 +0200
+++ b/src/HOL/Tools/ATP/SpassCommunication.ML Tue Jun 21 23:44:18 2005 +0200
@@ -42,8 +42,7 @@
(**********************************************************************)
-val atomize_tac =
- SUBGOAL
+val atomize_tac = SUBGOAL
(fn (prop,_) =>
let val ts = Logic.strip_assums_hyp prop
in EVERY1
--- a/src/HOL/Tools/ATP/recon_parse.ML Tue Jun 21 21:41:08 2005 +0200
+++ b/src/HOL/Tools/ATP/recon_parse.ML Tue Jun 21 23:44:18 2005 +0200
@@ -209,16 +209,24 @@
then
nums
else
- let val num = hd rest
- val int_of = num_int num
-
+ let val first = hd rest
+
in
- linenums rest (int_of::nums)
+ if (first = (Other "*") )
+ then
+
+ linenums rest ((num_int (hd (tl rest)))::nums)
+ else
+ linenums rest ((num_int first)::nums)
end
end
-fun get_linenums proofstr = let val s = extract_proof proofstr
- val tokens = #1(lex s)
+
+(* This relies on a Vampire proof line starting "% Number" or "% * Number"*)
+(* Check this is right *)
+
+fun get_linenums proofstr = let (*val s = extract_proof proofstr*)
+ val tokens = #1(lex proofstr)
in
rev (linenums tokens [])
--- a/src/HOL/Tools/ATP/recon_transfer_proof.ML Tue Jun 21 21:41:08 2005 +0200
+++ b/src/HOL/Tools/ATP/recon_transfer_proof.ML Tue Jun 21 23:44:18 2005 +0200
@@ -475,7 +475,7 @@
(***********************************)
val (axiom_names) = get_axiom_names_vamp proofstr thms clause_arr num_of_clauses
- val ax_str = "Rules from clasimpset used in proof found by SPASS: "^(rules_to_string axiom_names "")
+ val ax_str = "Rules from clasimpset used in proof found by Vampire: "^(rules_to_string axiom_names "")
val outfile = TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic "reconstrfile"))); val _ = TextIO.output (outfile, ("reconstring is: "^ax_str^" "^goalstring))
val _ = TextIO.closeOut outfile
@@ -496,7 +496,7 @@
val _ = TextIO.output (outfile, ("In exception handler"));
val _ = TextIO.closeOut outfile
in
- TextIO.output (toParent,"Proof found but translation failed for resolution proof: "^(remove_linebreaks proofstr) );
+ TextIO.output (toParent,"Proof found by Vampire but translation failed for resolution proof: "^(remove_linebreaks proofstr) );
TextIO.flushOut toParent;
TextIO.output (toParent, thmstring^"\n");
TextIO.flushOut toParent;
--- a/src/HOL/Tools/ATP/watcher.ML Tue Jun 21 21:41:08 2005 +0200
+++ b/src/HOL/Tools/ATP/watcher.ML Tue Jun 21 23:44:18 2005 +0200
@@ -514,7 +514,12 @@
val _ = File.append (File.tmp_path (Path.basic "child_command"))
(childCmd^"\n")
(* now get the number of the subgoal from the filename *)
- val sg_num = int_of_string(ReconOrderClauses.get_nth 5 (rev(explode childCmd)))
+ val sg_num = if (!SpassComm.spass )
+ then
+ int_of_string(ReconOrderClauses.get_nth 5 (rev(explode childCmd)))
+ else
+ int_of_string(hd (rev(explode childCmd)))
+
val childIncoming = pollChildInput childInput
val _ = File.append (File.tmp_path (Path.basic "child_check_polled"))
("finished polling child \n")
@@ -562,7 +567,7 @@
(********************************************************************)
(* call resolution processes *)
(* settings should be a list of strings *)
- (* e.g. ["-t 300", "-m 100000"] *)
+ (* e.g. ["-t 300", "-m 100000"] (TextIO.input instr)^ *)
(* takes list of (string, string, string list, string)list proclist *)
(********************************************************************)
@@ -600,7 +605,7 @@
instr = instr,
outstr = outstr })::procList))
- val _ = File.append (File.tmp_path (Path.basic "exec_child")) ("executing command for goal:\n"^goalstring^proverCmd^(concat settings)^file^(TextIO.input instr)^" at "^(Date.toString(Date.fromTimeLocal(Time.now()))))
+ val _ = File.append (File.tmp_path (Path.basic "exec_child")) ("executing command for goal:\n"^goalstring^proverCmd^(concat settings)^file^" at "^(Date.toString(Date.fromTimeLocal(Time.now()))))
in
Posix.Process.sleep (Time.fromSeconds 1); execCmds cmds newProcList
end
@@ -789,95 +794,125 @@
end
-fun createWatcher (thm,clause_arr, ( num_of_clauses:int)) =
- 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
- 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 _ = (warning ("subgoals forked to createWatcher: "^prems_string));
- fun vampire_proofHandler (n) =
- (Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
- VampComm.getVampInput childin; Pretty.writeln(Pretty.str (oct_char "361")))
+
+fun createWatcher (thm,clause_arr, ( num_of_clauses:int)) = 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
+ 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 _ = (warning ("subgoals forked to createWatcher: "^prems_string));
+ fun vampire_proofHandler (n) =
+ (Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
+ VampComm.getVampInput childin; Pretty.writeln(Pretty.str (oct_char "361"));() )
+
+
+fun spass_proofHandler (n) = (
+ let val outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_signal1")));
+ val _ = TextIO.output (outfile, ("In signal handler now\n"))
+ val _ = TextIO.closeOut outfile
+ val (reconstr, goalstring, thmstring) = SpassComm.getSpassInput childin
+ val outfile = TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic "foo_signal")));
+
+ val _ = TextIO.output (outfile, ("In signal handler "^reconstr^thmstring^goalstring^"goals_being_watched is: "^(string_of_int (!goals_being_watched))))
+ val _ = TextIO.closeOut outfile
+ in (* if a proof has been found and sent back as a reconstruction proof *)
+ if ( (substring (reconstr, 0,1))= "[")
+ then
- fun spass_proofHandler (n) =
- let val _ = File.write (File.tmp_path (Path.basic "foo_signal1")) "In signal handler now\n"
- val (reconstr, goalstring, thmstring) = SpassComm.getSpassInput childin
- val _ = File.append (File.tmp_path (Path.basic "foo_signal"))
- ("In signal handler "^reconstr^thmstring^goalstring^"goals_being_watched is: "^(string_of_int (!goals_being_watched)))
- in (* if a proof has been found and sent back as a reconstruction proof *)
- if ( (substring (reconstr, 0,1))= "[")
- 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 "foo_reap_found"))
- ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n")
- in
- killWatcher (childpid); reapWatcher (childpid,childin, childout); ()
- end
- else ()
- )
- (* 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")])));
- 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 ()
- )
- (* 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
- (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 ()
- )
-
- (* 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
- (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
- ()
- )
- else (* add something here ?*)
- ()
-
- end
-
- in IsaSignal.signal (IsaSignal.usr1, IsaSignal.SIG_HANDLE vampire_proofHandler);
- IsaSignal.signal (IsaSignal.usr2, IsaSignal.SIG_HANDLE spass_proofHandler);
- (childin, childout, childpid)
+ (
+ 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 outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_reap_found")));
+ 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 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")])));
+ Pretty.writeln(Pretty.str ((Recon_Transfer.restore_linebreaks 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
+ ()
+ )
+ (* 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 ?*)
+ ()
+
+
+
+ end)
+
+
+
+ in IsaSignal.signal (IsaSignal.usr1, IsaSignal.SIG_HANDLE vampire_proofHandler);
+ IsaSignal.signal (IsaSignal.usr2, IsaSignal.SIG_HANDLE spass_proofHandler);
+ (childin, childout, childpid)
+
end
--- a/src/HOL/Tools/res_atp.ML Tue Jun 21 21:41:08 2005 +0200
+++ b/src/HOL/Tools/res_atp.ML Tue Jun 21 23:44:18 2005 +0200
@@ -1,5 +1,7 @@
(* Author: Jia Meng, Cambridge University Computer Laboratory
+
ID: $Id$
+
Copyright 2004 University of Cambridge
ATPs with TPTP format input.
@@ -24,6 +26,7 @@
val full_spass: bool ref
(*val spass: bool ref*)
val vampire: bool ref
+val custom_spass :string list ref
end;
structure ResAtp : RES_ATP =
@@ -44,6 +47,8 @@
(* use spass as default prover *)
(*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;
@@ -156,12 +161,16 @@
fun call_resolve_tac (thms: Thm.thm list list) sign (sg_terms: Term.term list) (childin, childout,pid) n =
let
val axfile = (File.platform_path axiom_file)
- val hypsfile = (File.platform_path hyps_file)
- val clasimpfile = (File.platform_path clasimp_file)
-
+
+ val hypsfile = (File.platform_path hyps_file)
+ val clasimpfile = (File.platform_path clasimp_file)
+ val spass_home = getenv "SPASS_HOME"
+
+
fun make_atp_list [] sign n = []
| make_atp_list ((sko_thm, sg_term)::xs) sign n =
let
+
val skothmstr = Meson.concat_with_and (map string_of_thm sko_thm)
val thmproofstr = proofstring ( skothmstr)
val no_returns =List.filter not_newline ( thmproofstr)
@@ -175,6 +184,7 @@
val _ = warning ("goalstring in make_atp_lists is: "^goalstring)
val probfile = (File.platform_path prob_file) ^ "_" ^ (string_of_int n)
+
val _ = (warning ("prob file in cal_res_tac is: "^probfile))
in
if !SpassComm.spass
@@ -183,14 +193,17 @@
in (*We've checked that SPASS is there for ATP/spassshell to run.*)
if !full_spass
then (*Allow SPASS to run in Auto mode, using all its inference rules*)
+
([("spass", thmstr, goalstring (*,spass_home*),
- getenv "ISABELLE_HOME" ^ "/src/HOL/Tools/ATP/spassshell",
- "-DocProof%-TimeLimit=60",
+
+ getenv "ISABELLE_HOME" ^ "/src/HOL/Tools/ATP/spassshell"(*( getenv "SPASS_HOME")^"/SPASS"*),
+ "-DocProof%-TimeLimit=60%-SOS",
+
clasimpfile, axfile, hypsfile, probfile)]@(make_atp_list xs sign (n+1)))
else (*Restrict SPASS to a small set of rules that we can parse*)
([("spass", thmstr, goalstring (*,spass_home*),
getenv "ISABELLE_HOME" ^"/src/HOL/Tools/ATP/spassshell"(* (getenv "SPASS_HOME")^"/SPASS"*),
- "-Auto=0%-IORe%-IOFc%-RTaut%-RFSub%-RBSub%-DocProof%-TimeLimit=60",
+ ("-" ^ space_implode "%-" (!custom_spass)),
clasimpfile, axfile, hypsfile, probfile)]@(make_atp_list xs sign (n+1)))
end
else
@@ -209,21 +222,7 @@
warning("Sent commands to watcher!");
dummy_tac
end
-(*
- val axfile = (File.platform_path axiom_file)
- val hypsfile = (File.platform_path hyps_file)
- val clasimpfile = (File.platform_path clasimp_file)
- val spass_home = getenv "SPASS_HOME"
- val probfile = (File.platform_path prob_file) ^ "_" ^ (string_of_int 1)
-
- val (clause_arr, num_of_clauses) = ResClasimp.write_out_clasimp_small (File.platform_path clasimp_file) ;
- val (childin,childout,pid) = Watcher.createWatcher(mp, clause_arr, num_of_clauses);
-Watcher.callResProvers(childout, [("spass", "thmstring", "goalstr", spass_home, "-DocProof", clasimpfile, axfile, hypsfile,probfile)]);
-Watcher.callResProvers(childout, [("spass", "thmstring", "goalstr", "/homes/clq20/spassshell", "", clasimpfile, axfile, hypsfile,probfile)]);
-
-
-*)
(**********************************************************)
(* write out the current subgoal as a tptp file, probN, *)
(* then call dummy_tac - should be call_res_tac *)
@@ -263,9 +262,7 @@
get_sko_thms tfree_lits sign prems (childin, childout, pid) thm n []
end ;
-(*fun isar_atp_goal thm n_subgoals tfree_lits (childin, childout, pid) =
- (if (!debug) then warning (string_of_thm thm)
- else (isar_atp_goal' thm n_subgoals tfree_lits (childin, childout, pid) ));*)
+
(**************************************************)
(* convert clauses from "assume" to conjecture. *)
@@ -305,18 +302,7 @@
ResClasimp.write_out_clasimp(*_small*) (File.platform_path clasimp_file)
(ProofContext.theory_of ctxt)
val _ = (warning ("clasimp_file is this: "^(File.platform_path clasimp_file)) )
-
- (* cq: add write out clasimps to file *)
- (* cq:create watcher and pass to isar_atp_aux *)
- (* tracing *)
- (*val tenth_ax = fst( Array.sub(clause_arr, 1))
- val tenth_ax_thms = Recon_Transfer.memo_find_clause (tenth_ax, clause_tab)
- val clause_str = Meson.concat_with_and (map string_of_thm tenth_ax_thms)
- val _ = (warning ("tenth axiom in array is: "^tenth_ax))
- val _ = (warning ("tenth axiom in table is: "^clause_str))
-
- val _ = (warning ("num_of_clauses is: "^(string_of_int (num_of_clauses))) )
- *)
+
val (childin,childout,pid) = Watcher.createWatcher(thm,clause_arr, num_of_clauses)
val pidstring = string_of_int(Word.toInt (Word.fromLargeWord ( Posix.Process.pidToWord pid )))