# HG changeset patch # User quigley # Date 1119390258 -7200 # Node ID 7a9cda53bfa2682574f80b91853d92089b1441e0 # Parent b3235bd87da7a01f9d97b1cd7e530c840809514f Integrated vampire lemma code. diff -r b3235bd87da7 -r 7a9cda53bfa2 src/HOL/Tools/ATP/SpassCommunication.ML --- 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 diff -r b3235bd87da7 -r 7a9cda53bfa2 src/HOL/Tools/ATP/recon_parse.ML --- 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 []) diff -r b3235bd87da7 -r 7a9cda53bfa2 src/HOL/Tools/ATP/recon_transfer_proof.ML --- 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; diff -r b3235bd87da7 -r 7a9cda53bfa2 src/HOL/Tools/ATP/watcher.ML --- 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 diff -r b3235bd87da7 -r 7a9cda53bfa2 src/HOL/Tools/res_atp.ML --- 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 )))