split relevance-filter and writing of problem-files;
perform relevance-filtering for only one subgoal;
added additional explicit timeout to provers
--- a/src/HOL/Tools/atp_wrapper.ML Sat Mar 14 15:45:45 2009 +0100
+++ b/src/HOL/Tools/atp_wrapper.ML Sat Mar 14 16:46:23 2009 +0100
@@ -10,9 +10,9 @@
val destdir: string ref
val problem_name: string ref
val external_prover:
- ((int -> Path.T) -> Proof.context * thm list * thm -> string list * ResHolClause.axiom_name Vector.vector list) ->
- Path.T * string ->
- (string -> string option) ->
+ (thm * (string * int)) list ->
+ (Path.T -> thm -> int -> (thm * (string * int)) list -> theory -> string vector) ->
+ Path.T * string -> (string -> string option) ->
(string * string vector * Proof.context * thm * int -> string) ->
AtpManager.prover
val tptp_prover_opts_full: int -> bool -> bool -> Path.T * string -> AtpManager.prover
@@ -47,7 +47,7 @@
(* basic template *)
-fun external_prover write_problem_files (cmd, args) find_failure produce_answer timeout subgoalno state =
+fun external_prover axiom_clauses write_problem_file (cmd, args) find_failure produce_answer timeout subgoalno state =
let
(* path to unique problem file *)
val destdir' = ! destdir
@@ -62,24 +62,25 @@
(* write out problem file and call prover *)
val (ctxt, (chain_ths, goal)) = Proof.get_goal state
+ val thy = ProofContext.theory_of ctxt
val chain_ths = map (Thm.put_name_hint ResReconstruct.chained_hint) chain_ths
- val (filenames, thm_names_list) = write_problem_files prob_pathname (ctxt, chain_ths, goal)
- val thm_names = nth thm_names_list (subgoalno - 1)
-
+ val probfile = prob_pathname subgoalno
+ val fname = File.platform_path probfile
+ val thm_names = write_problem_file probfile goal subgoalno axiom_clauses thy
val cmdline =
if File.exists cmd then File.shell_path cmd ^ " " ^ args
else error ("Bad executable: " ^ Path.implode cmd)
- val (proof, rc) = system_out (cmdline ^ " " ^ nth filenames (subgoalno - 1))
+ val (proof, rc) = system_out (cmdline ^ " " ^ fname)
(* remove *temporary* files *)
- val _ = if destdir' = "" then List.app OS.FileSys.remove filenames else ()
+ val _ = if destdir' = "" then OS.FileSys.remove fname else ()
(* check for success and print out some information on failure *)
val failure = find_failure proof
val success = rc = 0 andalso is_none failure
val message =
if isSome failure then "Proof attempt failed."
- else if rc <> 0 then "Proof attempt failed: " ^ proof
+ else if rc <> 0 then "Proof attempt failed: " ^ proof
else "Try this command: " ^ produce_answer (proof, thm_names, ctxt, goal, subgoalno)
val _ = if isSome failure
@@ -96,12 +97,14 @@
(* generic TPTP-based provers *)
-fun tptp_prover_opts_full max_new theory_const full command =
+fun tptp_prover_opts_full max_new theory_const full command timeout n state =
external_prover
- (ResAtp.write_problem_files false max_new theory_const)
+ (ResAtp.get_relevant max_new theory_const (Proof.get_goal state) n)
+ (ResAtp.write_problem_file false)
command
ResReconstruct.find_failure_e_vamp_spass
- (if full then ResReconstruct.structured_proof else ResReconstruct.lemma_list_tstp);
+ (if full then ResReconstruct.structured_proof else ResReconstruct.lemma_list_tstp)
+ timeout n state;
(*arbitrary ATP with TPTP input/output and problemfile as last argument*)
fun tptp_prover_opts max_new theory_const =
@@ -139,26 +142,33 @@
(* E prover *)
-fun eprover_opts max_new theory_const = tptp_prover_opts
+fun eprover_opts max_new theory_const timeout = tptp_prover_opts
max_new theory_const
- (Path.explode "$E_HOME/eproof", "--tstp-in --tstp-out -l5 -xAutoDev -tAutoDev --silent");
+ (Path.explode "$E_HOME/eproof",
+ "--tstp-in --tstp-out -l5 -xAutoDev -tAutoDev --silent --cpu-limit=" ^ string_of_int timeout)
+ timeout;
val eprover = eprover_opts 100 false;
-fun eprover_opts_full max_new theory_const = full_prover_opts
+fun eprover_opts_full max_new theory_const timeout = full_prover_opts
max_new theory_const
- (Path.explode "$E_HOME/eproof", "--tstp-in --tstp-out -l5 -xAutoDev -tAutoDev --silent");
+ (Path.explode "$E_HOME/eproof",
+ "--tstp-in --tstp-out -l5 -xAutoDev -tAutoDev --silent --cpu-limit=" ^ string_of_int timeout)
+ timeout;
val eprover_full = eprover_opts_full 100 false;
(* SPASS *)
-fun spass_opts max_new theory_const = external_prover
- (ResAtp.write_problem_files true max_new theory_const)
- (Path.explode "$SPASS_HOME/SPASS", "-Auto -SOS=1 -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof")
+fun spass_opts max_new theory_const timeout n state = external_prover
+ (ResAtp.get_relevant max_new theory_const (Proof.get_goal state) n)
+ (ResAtp.write_problem_file true)
+ (Path.explode "$SPASS_HOME/SPASS",
+ "-Auto -SOS=1 -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof -TimeLimit=" ^ string_of_int timeout)
ResReconstruct.find_failure_e_vamp_spass
- ResReconstruct.lemma_list_dfg;
+ ResReconstruct.lemma_list_dfg
+ timeout n state;
val spass = spass_opts 40 true;
@@ -173,3 +183,5 @@
val remote_prover = remote_prover_opts 60 false;
end;
+
+
--- a/src/HOL/Tools/res_atp.ML Sat Mar 14 15:45:45 2009 +0100
+++ b/src/HOL/Tools/res_atp.ML Sat Mar 14 16:46:23 2009 +0100
@@ -6,9 +6,10 @@
val tvar_classes_of_terms : term list -> string list
val tfree_classes_of_terms : term list -> string list
val type_consts_of_terms : theory -> term list -> string list
- val write_problem_files : bool -> int -> bool
- -> (int -> Path.T) -> Proof.context * thm list * thm
- -> string list * ResHolClause.axiom_name Vector.vector list
+ val get_relevant : int -> bool -> Proof.context * (thm list * thm) -> int
+ -> (thm * (string * int)) list
+ val write_problem_file : bool -> Path.T -> thm -> int -> (thm * (string * int)) list -> theory
+ -> string vector
end;
structure ResAtp: RES_ATP =
@@ -510,54 +511,51 @@
likely to lead to unsound proofs.*)
fun remove_unwanted_clauses cls = filter (not o unwanted o prop_of o fst) cls;
-(* TODO: problem file for *one* subgoal would be sufficient *)
-(*Write out problem files for each subgoal.
- Argument probfile generates filenames from subgoal-number
- Arguments max_new and theory_const are booleans controlling relevance_filter
- (necessary for different provers)
-*)
-fun write_problem_files dfg max_new theory_const probfile (ctxt, chain_ths, th) =
- let val goals = Thm.prems_of th
- val thy = ProofContext.theory_of ctxt
- fun get_neg_subgoals [] _ = []
- | get_neg_subgoals (gl::gls) n = #1 (ResAxioms.neg_conjecture_clauses th n) ::
- get_neg_subgoals gls (n+1)
- val goal_cls = get_neg_subgoals goals 1
- handle THM ("assume: variables", _, _) =>
- error "Sledgehammer: Goal contains type variables (TVars)"
- val isFO = case linkup_logic_mode of
- Auto => forall (Meson.is_fol_term thy) (map prop_of (List.concat goal_cls))
- | Fol => true
- | Hol => false
- val (included_thms,white_thms) = get_clasimp_atp_lemmas ctxt chain_ths
- val included_cls = included_thms |> ResAxioms.cnf_rules_pairs thy |> make_unique
- |> restrict_to_logic thy isFO
- |> remove_unwanted_clauses
- val white_cls = ResAxioms.cnf_rules_pairs thy white_thms
- (*clauses relevant to goal gl*)
- val axcls_list = map (fn ngcls => white_cls @ relevance_filter max_new theory_const thy included_cls (map prop_of ngcls)) goal_cls
- val writer = if dfg then ResHolClause.dfg_write_file else ResHolClause.tptp_write_file
- fun write_all [] [] _ = []
- | write_all (ccls::ccls_list) (axcls::axcls_list) k =
- let val fname = File.platform_path (probfile k)
- val axcls = make_unique axcls
- val _ = app (fn th => Output.debug (fn _ => Display.string_of_thm th)) ccls
- val ccls = subtract_cls ccls axcls
- val _ = app (fn th => Output.debug (fn _ => Display.string_of_thm th)) ccls
- val ccltms = map prop_of ccls
- and axtms = map (prop_of o #1) axcls
- val subs = tfree_classes_of_terms ccltms
- and supers = tvar_classes_of_terms axtms
- and tycons = type_consts_of_terms thy (ccltms@axtms)
- (*TFrees in conjecture clauses; TVars in axiom clauses*)
- val (supers',arity_clauses) = ResClause.make_arity_clauses_dfg dfg thy tycons supers
- val classrel_clauses = ResClause.make_classrel_clauses thy subs supers'
- val clnames = writer thy isFO ccls fname (axcls,classrel_clauses,arity_clauses) []
- val thm_names = Vector.fromList clnames
- in (thm_names,fname) :: write_all ccls_list axcls_list (k+1) end
- val (thm_names_list, filenames) = ListPair.unzip (write_all goal_cls axcls_list 1)
+fun isFO thy goal_cls = case linkup_logic_mode of
+ Auto => forall (Meson.is_fol_term thy) (map prop_of goal_cls)
+ | Fol => true
+ | Hol => false
+
+fun get_relevant max_new theory_const (ctxt, (chain_ths, th)) n =
+ let
+ val thy = ProofContext.theory_of ctxt
+ val goal_cls = #1 (ResAxioms.neg_conjecture_clauses th n)
+ handle THM ("assume: variables", _, _) =>
+ error "Sledgehammer: Goal contains type variables (TVars)"
+ val (included_thms,white_thms) = get_clasimp_atp_lemmas ctxt chain_ths
+ val included_cls = included_thms |> ResAxioms.cnf_rules_pairs thy |> make_unique
+ |> restrict_to_logic thy (isFO thy goal_cls)
+ |> remove_unwanted_clauses
+ val white_cls = ResAxioms.cnf_rules_pairs thy white_thms
+ (*clauses relevant to goal gl*)
in
- (filenames, thm_names_list)
+ white_cls @ relevance_filter max_new theory_const thy included_cls (map prop_of goal_cls)
+ end;
+
+(* Write out problem file *)
+fun write_problem_file dfg probfile goal n axcls thy =
+ let val writer = if dfg then ResHolClause.dfg_write_file else ResHolClause.tptp_write_file
+ val fname = File.platform_path probfile
+ val axcls = make_unique axcls
+ val goal_cls = #1 (ResAxioms.neg_conjecture_clauses goal n)
+ handle THM ("assume: variables", _, _) =>
+ error "Sledgehammer: Goal contains type variables (TVars)"
+ val _ = app (fn th => Output.debug (fn _ => Display.string_of_thm th)) goal_cls
+ val ccls = subtract_cls goal_cls axcls
+ val _ = app (fn th => Output.debug (fn _ => Display.string_of_thm th)) ccls
+ val ccltms = map prop_of ccls
+ and axtms = map (prop_of o #1) axcls
+ val subs = tfree_classes_of_terms ccltms
+ and supers = tvar_classes_of_terms axtms
+ and tycons = type_consts_of_terms thy (ccltms@axtms)
+ (*TFrees in conjecture clauses; TVars in axiom clauses*)
+ val (supers',arity_clauses) = ResClause.make_arity_clauses_dfg dfg thy tycons supers
+ val classrel_clauses = ResClause.make_classrel_clauses thy subs supers'
+ val clnames = writer thy (isFO thy goal_cls) ccls fname (axcls,classrel_clauses,arity_clauses) []
+ in
+ Vector.fromList clnames
end;
end;
+
+