# HG changeset patch # User immler@in.tum.de # Date 1237045583 -3600 # Node ID 07b4f050e4df2e9044536608b78b57d650ef54d0 # Parent db8b10fd51a4f07103853443daae4ee95d40a895 split relevance-filter and writing of problem-files; perform relevance-filtering for only one subgoal; added additional explicit timeout to provers diff -r db8b10fd51a4 -r 07b4f050e4df src/HOL/Tools/atp_wrapper.ML --- 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; + + diff -r db8b10fd51a4 -r 07b4f050e4df src/HOL/Tools/res_atp.ML --- 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; + +