# HG changeset patch # User immler@in.tum.de # Date 1245683229 -7200 # Node ID 19a5f1c8a8445a82caf4b7f095f043a357d66698 # Parent fda2cf4fef5871e05a9f7716433d405346e7ceec use results of relevance-filter to determine additional clauses; (needed for minimize to be able to prove the same problems as sledgehammer) diff -r fda2cf4fef58 -r 19a5f1c8a844 src/HOL/Tools/atp_manager.ML --- a/src/HOL/Tools/atp_manager.ML Mon Jun 22 17:07:08 2009 +0200 +++ b/src/HOL/Tools/atp_manager.ML Mon Jun 22 17:07:09 2009 +0200 @@ -20,9 +20,9 @@ val info: unit -> unit val messages: int option -> unit type prover = int -> (thm * (string * int)) list option -> - (int Symtab.table * bool Symtab.table) option -> string -> int -> + (thm * (string * int)) list option -> string -> int -> Proof.context * (thm list * thm) -> - bool * string * string * string vector * (int Symtab.table * bool Symtab.table) + bool * string * string * string vector * (thm * (string * int)) list val add_prover: string -> prover -> theory -> theory val print_provers: theory -> unit val get_prover: string -> theory -> prover option @@ -292,9 +292,9 @@ (* named provers *) type prover = int -> (thm * (string * int)) list option -> - (int Symtab.table * bool Symtab.table) option -> string -> int -> + (thm * (string * int)) list option -> string -> int -> Proof.context * (thm list * thm) -> - bool * string * string * string vector * (int Symtab.table * bool Symtab.table) + bool * string * string * string vector * (thm * (string * int)) list fun err_dup_prover name = error ("Duplicate prover: " ^ quote name); diff -r fda2cf4fef58 -r 19a5f1c8a844 src/HOL/Tools/atp_minimal.ML --- a/src/HOL/Tools/atp_minimal.ML Mon Jun 22 17:07:08 2009 +0200 +++ b/src/HOL/Tools/atp_minimal.ML Mon Jun 22 17:07:09 2009 +0200 @@ -83,9 +83,9 @@ ("# Cannot determine problem status within resource limit", Timeout), ("Error", Error)] -fun produce_answer (success, message, result_string, thm_name_vec, const_counts) = +fun produce_answer (success, message, result_string, thm_name_vec, filtered) = if success then - (Success (Vector.foldr op:: [] thm_name_vec, const_counts), result_string) + (Success (Vector.foldr op:: [] thm_name_vec, filtered), result_string) else let val failure = failure_strings |> get_first (fn (s, t) => @@ -100,7 +100,7 @@ (* wrapper for calling external prover *) -fun sh_test_thms prover prover_name time_limit subgoalno state counts name_thms_pairs = +fun sh_test_thms prover prover_name time_limit subgoalno state filtered name_thms_pairs = let val _ = println ("Testing " ^ (length_string name_thms_pairs) ^ " theorems... ") val name_thm_pairs = @@ -109,7 +109,7 @@ val axclauses = ResAxioms.cnf_rules_pairs (Proof.theory_of state) name_thm_pairs val (result, proof) = produce_answer - (prover time_limit (SOME axclauses) counts prover_name subgoalno (Proof.get_goal state)) + (prover time_limit (SOME axclauses) filtered prover_name subgoalno (Proof.get_goal state)) val _ = println (string_of_result result) val _ = debug proof in @@ -127,11 +127,12 @@ val _ = debug_fn (fn () => app (fn (n, tl) => (debug n; app (fn t => debug (" " ^ Display.string_of_thm t)) tl)) name_thms_pairs) val test_thms_fun = sh_test_thms prover prover_name time_limit 1 state - fun test_thms counts thms = case test_thms_fun counts thms of (Success _, _) => true | _ => false + fun test_thms filtered thms = + case test_thms_fun filtered thms of (Success _, _) => true | _ => false in (* try prove first to check result and get used theorems *) (case test_thms_fun NONE name_thms_pairs of - (Success (used, const_counts), _) => + (Success (used, filtered), _) => let val ordered_used = order_unique used val to_use = @@ -139,7 +140,7 @@ filter (fn (name1, _) => List.exists (equal name1) ordered_used) name_thms_pairs else name_thms_pairs - val min_thms = (minimal (test_thms (SOME const_counts)) to_use) + val min_thms = (minimal (test_thms (SOME filtered)) to_use) val min_names = order_unique (map fst min_thms) val _ = println ("Minimal " ^ (length_string min_thms) ^ " theorems") val _ = debug_fn (fn () => print_names min_thms) diff -r fda2cf4fef58 -r 19a5f1c8a844 src/HOL/Tools/atp_wrapper.ML --- a/src/HOL/Tools/atp_wrapper.ML Mon Jun 22 17:07:08 2009 +0200 +++ b/src/HOL/Tools/atp_wrapper.ML Mon Jun 22 17:07:09 2009 +0200 @@ -41,7 +41,7 @@ (* basic template *) fun external_prover relevance_filter preparer writer (cmd, args) find_failure produce_answer - timeout axiom_clauses const_counts name subgoalno goal = + timeout axiom_clauses filtered_clauses name subgoalno goal = let (* path to unique problem file *) val destdir' = ! destdir @@ -62,24 +62,20 @@ 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 the_filtered_clauses = + case filtered_clauses of + NONE => relevance_filter goal goal_cls + | SOME fcls => fcls val the_axiom_clauses = case axiom_clauses of - NONE => relevance_filter goal goal_cls + NONE => the_filtered_clauses | SOME axcls => axcls - val (thm_names, clauses) = preparer goal_cls chain_ths the_axiom_clauses thy - val the_const_counts = case const_counts of - NONE => - ResHolClause.count_constants( - case axiom_clauses of - NONE => clauses - | SOME axcls => #2(preparer goal_cls chain_ths (relevance_filter goal goal_cls) thy) - ) - | SOME ccs => ccs + val (thm_names, clauses) = preparer goal_cls chain_ths the_axiom_clauses the_filtered_clauses thy (* write out problem file and call prover *) val probfile = prob_pathname subgoalno val fname = File.platform_path probfile - val _ = writer fname the_const_counts clauses + val _ = writer fname clauses val cmdline = if File.exists cmd then "exec " ^ File.shell_path cmd ^ " " ^ args else error ("Bad executable: " ^ Path.implode cmd) @@ -101,7 +97,7 @@ else if rc <> 0 then "External prover failed: " ^ proof else "Try this command: " ^ produce_answer name (proof, thm_names, ctxt, th, subgoalno) val _ = Output.debug (fn () => "Sledgehammer response (rc = " ^ string_of_int rc ^ "):\n" ^ proof) - in (success, message, proof, thm_names, the_const_counts) end; + in (success, message, proof, thm_names, the_filtered_clauses) end; @@ -109,7 +105,7 @@ (* generic TPTP-based provers *) -fun tptp_prover_opts_full max_new theory_const full command timeout ax_clauses ccs name n goal = +fun tptp_prover_opts_full max_new theory_const full command timeout ax_clauses fcls name n goal = external_prover (ResAtp.get_relevant max_new theory_const) (ResAtp.prepare_clauses false) @@ -117,7 +113,7 @@ command ResReconstruct.find_failure (if full then ResReconstruct.structured_proof else ResReconstruct.lemma_list_tstp) - timeout ax_clauses ccs name n goal; + timeout ax_clauses fcls name n goal; (*arbitrary ATP with TPTP input/output and problemfile as last argument*) fun tptp_prover_opts max_new theory_const = @@ -174,7 +170,7 @@ (* SPASS *) -fun spass_opts max_new theory_const timeout ax_clauses ccs name n goal = external_prover +fun spass_opts max_new theory_const timeout ax_clauses fcls name n goal = external_prover (ResAtp.get_relevant max_new theory_const) (ResAtp.prepare_clauses true) ResHolClause.dfg_write_file @@ -182,7 +178,7 @@ "-Auto -SOS=1 -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof -TimeLimit=" ^ string_of_int timeout) ResReconstruct.find_failure ResReconstruct.lemma_list_dfg - timeout ax_clauses ccs name n goal; + timeout ax_clauses fcls name n goal; val spass = spass_opts 40 true; diff -r fda2cf4fef58 -r 19a5f1c8a844 src/HOL/Tools/res_atp.ML --- a/src/HOL/Tools/res_atp.ML Mon Jun 22 17:07:08 2009 +0200 +++ b/src/HOL/Tools/res_atp.ML Mon Jun 22 17:07:09 2009 +0200 @@ -9,6 +9,7 @@ val get_relevant : int -> bool -> Proof.context * (thm list * 'a) -> thm list -> (thm * (string * int)) list val prepare_clauses : bool -> thm list -> thm list -> + (thm * (ResHolClause.axiom_name * ResHolClause.clause_id)) list -> (thm * (ResHolClause.axiom_name * ResHolClause.clause_id)) list -> theory -> ResHolClause.axiom_name vector * (ResHolClause.clause list * ResHolClause.clause list * ResHolClause.clause list * ResClause.classrelClause list * ResClause.arityClause list) @@ -526,26 +527,30 @@ relevance_filter max_new theory_const thy included_cls (map prop_of goal_cls) end; -(* prepare for passing to writer *) -fun prepare_clauses dfg goal_cls chain_ths axcls thy = +(* prepare for passing to writer, + create additional clauses based on the information from extra_cls *) +fun prepare_clauses dfg goal_cls chain_ths axcls extra_cls thy = let - val white_thms = filter check_named (map ResAxioms.pairname (if null chain_ths then whitelist else chain_ths)) + val white_thms = + filter check_named (map ResAxioms.pairname (if null chain_ths then whitelist else chain_ths)) val white_cls = ResAxioms.cnf_rules_pairs thy white_thms - val axcls = white_cls @ axcls - val ccls = subtract_cls goal_cls axcls + val extra_cls = white_cls @ extra_cls + val ccls = subtract_cls goal_cls extra_cls 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 + and axtms = map (prop_of o #1) extra_cls 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 (clnames, (conjectures, axiom_clauses, helper_clauses)) = - ResHolClause.prepare_clauses dfg thy (isFO thy goal_cls) ccls axcls [] + val conjectures = ResHolClause.make_conjecture_clauses dfg thy ccls + val (clnames,axiom_clauses) = ListPair.unzip (ResHolClause.make_axiom_clauses dfg thy axcls) + val helper_clauses = ResHolClause.get_helper_clauses dfg thy (isFO thy goal_cls) (conjectures, extra_cls, []) val (supers',arity_clauses) = ResClause.make_arity_clauses_dfg dfg thy tycons supers val classrel_clauses = ResClause.make_classrel_clauses thy subs supers' in - (Vector.fromList clnames, (conjectures, axiom_clauses, helper_clauses, classrel_clauses, arity_clauses)) + (Vector.fromList clnames, + (conjectures, axiom_clauses, helper_clauses, classrel_clauses, arity_clauses)) end end; diff -r fda2cf4fef58 -r 19a5f1c8a844 src/HOL/Tools/res_hol_clause.ML --- a/src/HOL/Tools/res_hol_clause.ML Mon Jun 22 17:07:08 2009 +0200 +++ b/src/HOL/Tools/res_hol_clause.ML Mon Jun 22 17:07:09 2009 +0200 @@ -28,13 +28,18 @@ val strip_comb: combterm -> combterm * combterm list val literals_of_term: theory -> term -> literal list * typ list exception TOO_TRIVIAL - val count_constants: clause list * clause list * clause list * 'a * 'b -> - int Symtab.table * bool Symtab.table - val prepare_clauses: bool -> theory -> bool -> thm list -> (thm * (axiom_name * clause_id)) list -> - string list -> axiom_name list * (clause list * clause list * clause list) - val tptp_write_file: string -> int Symtab.table * bool Symtab.table -> + val make_conjecture_clauses: bool -> theory -> thm list -> clause list (* dfg thy ccls *) + val make_axiom_clauses: bool -> + theory -> + (thm * (axiom_name * clause_id)) list -> (axiom_name * clause) list (* dfg thy axcls *) + val get_helper_clauses: bool -> + theory -> + bool -> + clause list * (thm * (axiom_name * clause_id)) list * string list -> + clause list + val tptp_write_file: string -> clause list * clause list * clause list * ResClause.classrelClause list * ResClause.arityClause list -> unit - val dfg_write_file: string -> int Symtab.table * bool Symtab.table -> + val dfg_write_file: string -> clause list * clause list * clause list * ResClause.classrelClause list * ResClause.arityClause list -> unit end @@ -403,10 +408,12 @@ fun cnf_helper_thms thy = ResAxioms.cnf_rules_pairs thy o map ResAxioms.pairname -fun get_helper_clauses dfg thy isFO (conjectures, axclauses, user_lemmas) = +fun get_helper_clauses dfg thy isFO (conjectures, axcls, user_lemmas) = if isFO then [] (*first-order*) else - let val ct0 = List.foldl count_clause init_counters conjectures + let + val axclauses = map #2 (make_axiom_clauses dfg thy axcls) + val ct0 = List.foldl count_clause init_counters conjectures val ct = List.foldl (count_user_clause user_lemmas) ct0 axclauses fun needed c = valOf (Symtab.lookup ct c) > 0 val IK = if needed "c_COMBI" orelse needed "c_COMBK" @@ -462,20 +469,12 @@ in (const_min_arity, const_needs_hBOOL) end else (Symtab.empty, Symtab.empty); - -fun prepare_clauses dfg thy isFO thms ax_tuples user_lemmas = - let - val conjectures = make_conjecture_clauses dfg thy thms - val (clnames,axclauses) = ListPair.unzip (make_axiom_clauses dfg thy ax_tuples) - val helper_clauses = get_helper_clauses dfg thy isFO (conjectures, axclauses, user_lemmas) - in - (clnames, (conjectures, axclauses, helper_clauses)) - end - (* tptp format *) -fun tptp_write_file filename const_counts (conjectures, axclauses, helper_clauses, classrel_clauses, arity_clauses) = +fun tptp_write_file filename clauses = let + val (conjectures, axclauses, helper_clauses, classrel_clauses, arity_clauses) = clauses + val const_counts = count_constants clauses val (tptp_clss,tfree_litss) = ListPair.unzip (map (clause2tptp const_counts) conjectures) val tfree_clss = map RC.tptp_tfree_clause (List.foldl (op union_string) [] tfree_litss) val out = TextIO.openOut filename @@ -492,8 +491,10 @@ (* dfg format *) -fun dfg_write_file filename const_counts (conjectures, axclauses, helper_clauses, classrel_clauses, arity_clauses) = +fun dfg_write_file filename clauses = let + val (conjectures, axclauses, helper_clauses, classrel_clauses, arity_clauses) = clauses + val const_counts = count_constants clauses val (dfg_clss, tfree_litss) = ListPair.unzip (map (clause2dfg const_counts) conjectures) and probname = Path.implode (Path.base (Path.explode filename)) val axstrs = map (#1 o (clause2dfg const_counts)) axclauses