--- a/src/HOL/Tools/res_atp.ML Thu Sep 15 17:45:17 2005 +0200
+++ b/src/HOL/Tools/res_atp.ML Thu Sep 15 17:46:00 2005 +0200
@@ -7,7 +7,6 @@
signature RES_ATP =
sig
- val axiom_file : Path.T
val prover: string ref
val custom_spass: string list ref
val hook_count: int ref
@@ -27,8 +26,6 @@
ref ["Auto=0","-FullRed=0","-IORe","-IOFc","-RTaut","-RFSub","-RBSub",
"-DocProof","-TimeLimit=60"];
-val axiom_file = File.tmp_path (Path.basic "axioms");
-val hyps_file = File.tmp_path (Path.basic "hyps");
val prob_file = File.tmp_path (Path.basic "prob");
@@ -58,42 +55,18 @@
(*********************************************************************)
-(* convert clauses from "assume" to conjecture. write to file "hyps" *)
-(* hypotheses of the goal currently being proved *)
-(*********************************************************************)
-(*perhaps have 2 different versions of this, depending on whether or not spass is set *)
-fun isar_atp_h thms =
- let val prems = map (skolemize o make_nnf o ObjectLogic.atomize_thm) thms
- val prems' = map repeat_someI_ex prems
- val prems'' = make_clauses prems'
- val prems''' = ResAxioms.rm_Eps [] prems''
- val clss = map ResClause.make_conjecture_clause prems'''
- val (tptp_clss,tfree_litss) = ListPair.unzip (map ResClause.clause2tptp clss)
- val tfree_lits = ResLib.flat_noDup tfree_litss
- (* tfree clause is different in tptp and dfg versions *)
- val tfree_clss = map ResClause.tfree_clause tfree_lits
- val hypsfile = File.platform_path hyps_file
- val out = TextIO.openOut(hypsfile)
- in
- ResLib.writeln_strs out (tfree_clss @ tptp_clss);
- TextIO.closeOut out; debug hypsfile;
- tfree_lits
- end;
-
-
-(*********************************************************************)
(* write out a subgoal as tptp clauses to the file "probN" *)
(* where N is the number of this subgoal *)
(*********************************************************************)
-fun tptp_inputs_tfrees thms n tfrees axclauses =
+fun tptp_inputs_tfrees thms n axclauses =
let
val _ = debug ("in tptp_inputs_tfrees 0")
val clss = map (ResClause.make_conjecture_clause_thm) thms
val _ = debug ("in tptp_inputs_tfrees 1")
val (tptp_clss,tfree_litss) = ListPair.unzip (map ResClause.clause2tptp clss)
val _ = debug ("in tptp_inputs_tfrees 2")
- val tfree_clss = map ResClause.tfree_clause ((ResLib.flat_noDup tfree_litss) \\ tfrees)
+ val tfree_clss = map ResClause.tfree_clause (ResLib.flat_noDup tfree_litss)
val _ = debug ("in tptp_inputs_tfrees 3")
val probfile = File.platform_path prob_file ^ "_" ^ string_of_int n
val out = TextIO.openOut(probfile)
@@ -110,14 +83,12 @@
(* where N is the number of this subgoal *)
(*********************************************************************)
-fun dfg_inputs_tfrees thms n tfrees axclauses =
+fun dfg_inputs_tfrees thms n axclauses =
let val clss = map (ResClause.make_conjecture_clause_thm) thms
val probfile = (File.platform_path prob_file) ^ "_" ^ (string_of_int n)
val _ = debug ("about to write out dfg prob file " ^ probfile)
- (*val (dfg_clss,tfree_litss) = ListPair.unzip (map ResClause.clause2dfg clss)
- val tfree_clss = map ResClause.tfree_dfg_clause ((ResLib.flat_noDup tfree_litss) \\ tfrees) *)
val probN = ResClause.clauses2dfg clss ("prob" ^ (string_of_int n))
- axclauses [] [] [] tfrees
+ axclauses [] [] []
val out = TextIO.openOut(probfile)
in
(ResLib.writeln_strs out [probN]; TextIO.closeOut out; debug probfile )
@@ -129,23 +100,16 @@
(* call prover with settings and problem file for the current subgoal *)
(*********************************************************************)
(* now passing in list of skolemized thms and list of sgterms to go with them *)
-fun call_resolve_tac (thms: thm list list) sign (sg_terms: term list) (childin, childout,pid) n =
+fun watcher_call_provers sign sg_terms (childin, childout,pid) =
let
- val axfile = (File.platform_path axiom_file)
-
- val hypsfile = (File.platform_path hyps_file)
-
- fun make_atp_list [] sign n = []
- | make_atp_list ((sko_thm, sg_term)::xs) sign n =
+ fun make_atp_list [] n = []
+ | make_atp_list ((sg_term)::xs) n =
let
- val thmstr = proofstring (Meson.concat_with_and (map string_of_thm sko_thm))
- val _ = debug ("thmstring in make_atp_lists is " ^ thmstr)
-
val goalstring = proofstring (Sign.string_of_term sign sg_term)
val _ = debug ("goalstring in make_atp_lists is " ^ goalstring)
val probfile = File.platform_path prob_file ^ "_" ^ (string_of_int n)
- val _ = debug ("prob file in call_resolve_tac is " ^ probfile)
+ val _ = debug ("prob file in watcher_call_provers is " ^ probfile)
in
(*Avoid command arguments containing spaces: Poly/ML and SML/NJ
versions of Unix.execute treat them differently!*)
@@ -161,93 +125,60 @@
val _ = ResLib.helper_path "SPASS_HOME" "SPASS"
(*We've checked that SPASS is there for ATP/spassshell to run.*)
in
- ([("spass", thmstr, goalstring,
+ ([("spass", goalstring,
getenv "ISABELLE_HOME" ^ "/src/HOL/Tools/ATP/spassshell",
- optionline, axfile, hypsfile, probfile)] @
- (make_atp_list xs sign (n+1)))
+ optionline, probfile)] @
+ (make_atp_list xs (n+1)))
end
else if !prover = "vampire"
then
let val vampire = ResLib.helper_path "VAMPIRE_HOME" "vkernel"
in
- ([("vampire", thmstr, goalstring, vampire, "-t60%-m100000",
- axfile, hypsfile, probfile)] @
- (make_atp_list xs sign (n+1)))
+ ([("vampire", goalstring, vampire, "-t60%-m100000",
+ probfile)] @
+ (make_atp_list xs (n+1)))
end
else if !prover = "E"
then
let val Eprover = ResLib.helper_path "E_HOME" "eproof"
in
- ([("E", thmstr, goalstring, Eprover,
+ ([("E", goalstring, Eprover,
"--tptp-in%-l5%-xAuto%-tAuto%--soft-cpu-limit=60",
- axfile, hypsfile, probfile)] @
- (make_atp_list xs sign (n+1)))
+ probfile)] @
+ (make_atp_list xs (n+1)))
end
else error ("Invalid prover name: " ^ !prover)
end
- val atp_list = make_atp_list (ListPair.zip (thms, sg_terms)) sign 1
+ val atp_list = make_atp_list sg_terms 1
in
Watcher.callResProvers(childout,atp_list);
- debug "Sent commands to watcher!";
- all_tac
+ debug "Sent commands to watcher!"
end
-(**********************************************************)
-(* write out the current subgoal as a tptp file, probN, *)
-(* then call all_tac - should be call_res_tac *)
-(**********************************************************)
-
-
-fun get_sko_thms tfrees sign sg_terms (childin, childout,pid) thm n sko_thms axclauses =
- if n=0 then
- (call_resolve_tac (rev sko_thms)
- sign sg_terms (childin, childout, pid) (List.length sg_terms);
- all_tac thm)
+(*We write out problem files for each subgoal, but work is repeated (skolemize)*)
+fun write_problem_files axclauses thm n =
+ if n=0 then ()
else
-
- (SELECT_GOAL
+ (SELECT_GOAL
(EVERY1 [rtac ccontr, ResLib.atomize_tac, skolemize_tac,
METAHYPS(fn negs =>
(if !prover = "spass"
- then dfg_inputs_tfrees (make_clauses negs) n tfrees axclauses
- else tptp_inputs_tfrees (make_clauses negs) n tfrees axclauses;
- get_sko_thms tfrees sign sg_terms (childin, childout, pid)
- thm (n-1) (negs::sko_thms) axclauses;
- all_tac))]) n thm)
-
-
-
-(**********************************************)
-(* recursively call atp_tac_g on all subgoals *)
-(* sg_term is the nth subgoal as a term - used*)
-(* in proof reconstruction *)
-(**********************************************)
+ then dfg_inputs_tfrees (make_clauses negs) n axclauses
+ else tptp_inputs_tfrees (make_clauses negs) n axclauses;
+ write_problem_files axclauses thm (n-1);
+ all_tac))]) n thm;
+ ());
-fun isar_atp_aux thms thm n_subgoals (childin, childout, pid) axclauses =
- let val tfree_lits = isar_atp_h thms
- val prems = Thm.prems_of thm
- val sign = sign_of_thm thm
- val thmstring = string_of_thm thm
- in
- debug ("in isar_atp_aux");
- debug("thmstring in isar_atp_goal': " ^ thmstring);
- (* go and call callResProvers with this subgoal *)
- (* isar_atp_g tfree_lits sg_term (childin, childout, pid) k thm; *)
- (* recursive call to pick up the remaining subgoals *)
- (* isar_atp_goal' thm (k+1) n tfree_lits (childin, childout, pid) *)
- get_sko_thms tfree_lits sign prems (childin, childout, pid)
- thm n_subgoals [] axclauses
- end;
(******************************************************************)
(* called in Isar automatically *)
(* writes out the current clasimpset to a tptp file *)
-(* passes all subgoals on to isar_atp_aux for further processing *)
(* turns off xsymbol at start of function, restoring it at end *)
(******************************************************************)
(*FIX changed to clasimp_file *)
-val isar_atp' = setmp print_mode [] (fn (ctxt, thms, thm) =>
+val isar_atp' = setmp print_mode []
+ (fn (ctxt, thms, thm) =>
if Thm.no_prems thm then ()
else
let
@@ -260,18 +191,34 @@
(*set up variables for writing out the clasimps to a tptp file*)
val (clause_arr, num_of_clauses, axclauses) =
ResClasimp.get_clasimp_lemmas thy (hd prems) (*FIXME: hack!! need to do all prems*)
- val _ = debug ("claset and simprules total " ^ (string_of_int num_of_clauses)^ " clauses")
- val (childin, childout, pid) = Watcher.createWatcher (thm, clause_arr, num_of_clauses)
+ val _ = debug ("claset and simprules total " ^ (string_of_int num_of_clauses)^
+ " clauses")
+ val (childin, childout, pid) =
+ Watcher.createWatcher (thm, clause_arr, num_of_clauses)
val pid_string =
string_of_int (Word.toInt (Word.fromLargeWord (Posix.Process.pidToWord pid)))
in
debug ("initial thms: " ^ thms_string);
debug ("subgoals: " ^ prems_string);
debug ("pid: "^ pid_string);
- isar_atp_aux thms thm (length prems) (childin, childout, pid) axclauses;
- ()
+ write_problem_files axclauses thm (length prems);
+ watcher_call_provers (sign_of_thm thm) (Thm.prems_of thm) (childin, childout, pid)
end);
+val isar_atp_writeonly = setmp print_mode []
+ (fn (ctxt, thms, thm) =>
+ if Thm.no_prems thm then ()
+ else
+ let
+ val thy = ProofContext.theory_of ctxt
+ val prems = Thm.prems_of thm
+
+ (*set up variables for writing out the clasimps to a tptp file*)
+ val (clause_arr, num_of_clauses, axclauses) =
+ ResClasimp.get_clasimp_lemmas thy (hd prems) (*FIXME: hack!! need to do all prems*)
+ in
+ write_problem_files axclauses thm (length prems)
+ end);
fun get_thms_cs claset =
let val {safeEs, safeIs, hazEs, hazIs, ...} = rep_cs claset