diff --git a/Abduction/Abduction.thy b/Abduction/Abduction.thy index 0ec70883..412648ee 100644 --- a/Abduction/Abduction.thy +++ b/Abduction/Abduction.thy @@ -65,8 +65,8 @@ strategy Attack_On_Or_Node = ] setup\ Config.put_global Top_Down_Util.timeout_config (60.0 * 60.0 * 10.0) \ -setup\ Config.put_global Top_Down_Util.limit_for_first_decrement 30 \ -setup\ Config.put_global Top_Down_Util.limit_for_other_decrement 10 \ +setup\ Config.put_global Top_Down_Util.limit_for_first_decrement 40 \ +setup\ Config.put_global Top_Down_Util.limit_for_other_decrement 15 \ (* UI *) ML\ (*This part (the definitions of long_keyword, long_statement, and short_statement) are from @@ -159,7 +159,7 @@ fun simp_explicit_conjecture (synched_term2string:SS.synched_term2string_table) else let val simp_result_term = the simp_result |> Thm.full_prop_of: term; - val simp_result_name = SS.get_lemma_name synched_term2string ctxt simp_result_term: string; + val simp_result_name = SS.get_lemma_name synched_term2string ctxt "" simp_result_term: string; in if simp_result_term = cnjctr_term then [simp, (simp_result_name, simp_result_term)] diff --git a/Abduction/Abstract_Same_Term.ML b/Abduction/Abstract_Same_Term.ML index 530b84e9..27b8ca29 100644 --- a/Abduction/Abstract_Same_Term.ML +++ b/Abduction/Abstract_Same_Term.ML @@ -79,7 +79,7 @@ fun abstract_same_term_str (ctxt:Proof.context) (trm:term) = val cnjctrs = map (try (Syntax.read_prop ctxt)) cnjctrs_strs |> map the_list |> flat: terms; val standardized_cnjctrs = map standardize_vnames cnjctrs : terms; val unique_cnjectrs = distinct (op =) standardized_cnjctrs : terms; - val tagged_cnjctrs = map (pair "abstract_same_term)") unique_cnjectrs : (string * term) list; + val tagged_cnjctrs = map (pair "abstract_same_term") unique_cnjectrs : (string * term) list; in tagged_cnjctrs end; diff --git a/Abduction/All_Top_Down_Conjecturing.ML b/Abduction/All_Top_Down_Conjecturing.ML index afea01bb..4e52855b 100644 --- a/Abduction/All_Top_Down_Conjecturing.ML +++ b/Abduction/All_Top_Down_Conjecturing.ML @@ -61,7 +61,7 @@ fun template_based_conjecture_for_simplification term2name (ctxt:Proof.context) @ TBC.ctxt_n_consts_to_projection ctxt tm @ TBC.ctxt_n_consts_to_square ctxt tm) |> map (apfst Template_Based_Conjecturing.property_as_string) - |> map (fn (_, term) => (SS.get_lemma_name term2name ctxt term, term));; + |> map (fn (lemma_typ, term) => (SS.get_lemma_name term2name ctxt lemma_typ term, term));; val result = map (ctxt_n_const_to_all_conjecture_term ctxt) (relevant_unary_funcs @ relevant_binary_funcs) |> flat: (string * term) list; in @@ -75,13 +75,16 @@ fun top_down_conjectures (term2name: SS.synched_term2string_table) (pst:Proof.st val _ = tracing' "[[[[[[[[[[[top_down_conjecture starts]]]]]]]]]]": unit; val standardized_trm = TDU.standardize_vnames trm val results = ( - Remove_Outermost_Assumption.top_down_conjectures term2name pst standardized_trm + (*It is important to have template_conjectures as the first because + * - we remove duplication based on the term. + * - we do not apply simplification for the conjectures produced by template-based conjecturing.*) + template_conjectures ctxt standardized_trm) + @ Remove_Outermost_Assumption.top_down_conjectures term2name pst standardized_trm @ Generalise_By_Renaming.top_down_conjectures term2name pst standardized_trm @ (Generalise_Then_Extend.top_down_conjectures term2name pst standardized_trm |> filter (fn (_, trm) => has_no_multiple_occ_of_composite_subtrm ctxt trm)) @ Remove_Function.top_down_conjectures term2name pst standardized_trm @ Abstract_Same_Term.top_down_conjectures term2name pst standardized_trm @ Replace_Imp_With_Eq.top_down_conjectures term2name pst standardized_trm - @ template_conjectures ctxt standardized_trm) |> Par_List.map (apsnd (TDU.simp_non_prop_term ctxt)) |> Par_List.map (apsnd TDU.standardize_vnames) |> map (fn (name, term) => (name, Syntax.check_term ctxt term))(*necessary to apply TDU.is_prop in some cases*) @@ -94,7 +97,7 @@ fun top_down_conjectures (term2name: SS.synched_term2string_table) (pst:Proof.st |> TDU.parallel_filter (fn (_, trm) => S4TD.run_assertion pst trm S4TD.does_not_have_trivial_equality) |> TDU.parallel_filter_out (fn (_, trm) => S4TD.run_assertion pst trm S4TD.nested_eq) |> TDU.parallel_filter_out (fn (_, trm) => S4TD.run_assertion pst trm S4TD.var_appears_many_times_but_always_in_the_same_subtrm) - |> map (fn (_, term) => (SS.get_lemma_name term2name ctxt term, term)); + |> map (fn (lemma_typ:string, term) => (SS.get_lemma_name term2name ctxt lemma_typ term, term)); val _ = tracing' "[[[[[[[[[[[top_down_conjecture ends]]]]]]]]]]": unit; in results diff --git a/Abduction/Or_Node.ML b/Abduction/Or_Node.ML index 91f40a58..f3b816a3 100644 --- a/Abduction/Or_Node.ML +++ b/Abduction/Or_Node.ML @@ -69,7 +69,7 @@ type is_final_goal = bool; fun mk_ornode (ctxt:Proof.context) (is_final_goal:is_final_goal) (lemma_name:string) (goal:term) = let val name = if is_final_goal - then Top_Down_Util.mk_new_lemma_name ctxt is_final_goal + then Top_Down_Util.mk_new_lemma_name ctxt is_final_goal "" else lemma_name; in {final_goal = is_final_goal, diff --git a/Abduction/Proof_By_Abduction.ML b/Abduction/Proof_By_Abduction.ML index e3d7f320..f8062211 100644 --- a/Abduction/Proof_By_Abduction.ML +++ b/Abduction/Proof_By_Abduction.ML @@ -96,7 +96,8 @@ fun expand_ornode_if_original_goral_is_unproved val seed_from_explicit = SOOE.conjectures_to_seed_of_or2and_edge term2name pst explicit_wo_counterexample : seed_of_or2and_edge; val explicit_cnjnctrs = #new_goals seed_from_explicit : SOOE.conjectures; val ctxt = Proof.context_of pst : Proof.context; - fun simp_explicit_conjecture (simp as (_:string, simp_term:term)) (cnjctr as (_:string, cnjctr_term:term)): SOOE.conjectures = + (*TODO: simp_explicit_conjecture should move to All_Top_Down_Conjecturing?*) + fun simp_explicit_conjecture (simp as (_:string, simp_term:term)) (cnjctr as (cnjctr_name:string, cnjctr_term:term)): SOOE.conjectures = let val simp_thm = TDU.term_to_thm ctxt simp_term: thm; val ctxt_w_simp = Simplifier.add_simp simp_thm ctxt: Proof.context; @@ -119,7 +120,7 @@ fun expand_ornode_if_original_goral_is_unproved val rm_Trueprop = Top_Down_Util.remove_Trueprop o Isabelle_Utils.strip_atyp; val simped_cnjctr_term = the simped_cnjctr |> Thm.full_prop_of |> remove_schematic - val simped_cnjctr_name = SS.get_lemma_name term2name ctxt simped_cnjctr_term: string; + val simped_cnjctr_name = SS.get_lemma_name term2name ctxt ("simped_" ^ cnjctr_name) simped_cnjctr_term: string; val size_of_simped_cnjctr = Term.size_of_term (rm_Trueprop simped_cnjctr_term): int; val size_of_orig_cnjctr = Term.size_of_term (rm_Trueprop cnjctr_term): int; in @@ -131,11 +132,15 @@ fun expand_ornode_if_original_goral_is_unproved end; fun simp_explicit_conjectures_for_one_rule (simp:SOOE.conjecture) (cnjctrs:SOOE.conjectures): SOOE.conjectures = map (simp_explicit_conjecture simp) cnjctrs |> flat |> distinct (op =); - fun simp_explicit_conjectures_for_many_rules (cnjctrs:SOOE.conjectures) (simps:SOOE.conjectures)= + fun simp_explicit_conjectures_for_many_rules (cnjctrs:SOOE.conjectures) (simps:SOOE.conjectures) = fold simp_explicit_conjectures_for_one_rule simps cnjctrs: SOOE.conjectures; val simps = Synchronized.value proved_ors: SS.proved_simps; - val simped_explicit_conjectures = simp_explicit_conjectures_for_many_rules explicit_cnjnctrs simps: SOOE.conjectures; - val _ = SOOE.abduction_for_explicit_conjectures pst or_key simped_explicit_conjectures + val (tb_cnjctrs, td_cnjctrs) = List.partition (TDU.is_template_based o fst) explicit_cnjnctrs: (SOOE.conjectures * SOOE.conjectures); + val simped_explicit_conjectures = simp_explicit_conjectures_for_many_rules td_cnjctrs simps: SOOE.conjectures; + val tb_and_simped_conjectures = tb_cnjctrs @ simped_explicit_conjectures + val standardized_conjectures = map (apsnd Top_Down_Util.standardize_vnames) tb_and_simped_conjectures + |> distinct (op =)(*TODO: should it be done here?*) + val _ = SOOE.abduction_for_explicit_conjectures pst or_key standardized_conjectures (term2name, refutation, synched_agraph, proved_ors): unit; (*tactic application as conjecturing. A little expensive*) val pst_to_prove = TDU.mk_pst_to_prove_from_term pst lemma_term: state; @@ -185,7 +190,9 @@ fun loop (counter:int) (max_depth:int) (start:Timing.start) val expand_ornode = expand_ornode_if_original_goral_is_unproved_w_timeout start (pst, synched_agraph, refutation, term2name, proved_ors, orig_prems) : Abduction_Graph.key -> bool; - val top_ornodes = take 8 sorted_orkeys: keys;(*TODO: magic number*) + val numb_of_processors = Thread.numProcessors ():int; + val _ = tracing ("numb_of_processors is " ^ Int.toString numb_of_processors ^ "."); + val top_ornodes = take numb_of_processors sorted_orkeys: keys;(*TODO: magic number*) val some_orkey = Par_List.find_some expand_ornode top_ornodes: key option; val solved = is_some some_orkey: bool; val _ = tracing ("We have " ^ (if solved then "already solved" else "not solve") ^ " the final goal."); diff --git a/Abduction/Remove_Function.ML b/Abduction/Remove_Function.ML index 9b800c23..2cb821f6 100644 --- a/Abduction/Remove_Function.ML +++ b/Abduction/Remove_Function.ML @@ -72,7 +72,7 @@ fun top_down_conjectures _ (pst:Proof.state) (trm:term) = val cnjctrs = one_less_occ @ one_less_prnt |> distinct (op =) : terms; val standardized_cnjctrs = map standardize_vnames cnjctrs : terms; val unique_cnjectrs = distinct (op =) standardized_cnjctrs : terms; - val tagged_cnjctrs = map (pair "remove_function)") unique_cnjectrs : (string * term) list; + val tagged_cnjctrs = map (pair "remove_function") unique_cnjectrs : (string * term) list; in tagged_cnjctrs end; diff --git a/Abduction/Seed_Of_Or2And_Edge.ML b/Abduction/Seed_Of_Or2And_Edge.ML index a40b5972..c6429f05 100644 --- a/Abduction/Seed_Of_Or2And_Edge.ML +++ b/Abduction/Seed_Of_Or2And_Edge.ML @@ -90,18 +90,18 @@ fun apply_PSL_to_get_seeds_of_or2and_edges val result_seq = TBC_Utils.psl_strategy_to_monadic_tactic timeouts extend_str pst []: (Dynamic_Utils.log * Proof.state) Seq.seq; val result_list = Seq.list_of result_seq : (Dynamic_Utils.log * Proof.state) list; val pairs_n_psts = map (apfst Dynamic_Utils.log_to_script_n_importance) result_list : ((strings * real) * Proof.state) list; - fun mk_proof_key_value ((pscript, importance), pst) = + fun mk_proof_key_value ((pscript:strings, importance), pst) = let val subgs = Isabelle_Utils.pst_to_subgs pst val subgs_wo_meta_uni = map TDU.strip_outermost_meta_quantifiers subgs: terms; val standardized_subgs = map Top_Down_Util.standardize_vnames subgs_wo_meta_uni: terms; val standardized_props = map (fn term => if Top_Down_Util.is_prop term then term else HOLogic.mk_Trueprop term) standardized_subgs: terms; - val mk_lemma_name = SS.get_lemma_name name_table ctxt: term -> string; + val mk_lemma_name = SS.get_lemma_name name_table ctxt "tactic": term -> string; val nonempty_subgs = if length subgs = 0 (*orelse not (pass_check_print_read_terms ctxt standardized_props)*) then [(mk_lemma_name @{prop "True"}, @{prop "True"})] else map mk_lemma_name standardized_props ~~ standardized_props: (string * term) list; - val nonempty_subgs_terms = map snd nonempty_subgs: terms; + val nonempty_subgs_terms = map snd nonempty_subgs |> map Top_Down_Util.standardize_vnames |> distinct (op =): terms; val new_importance = importance * SS.refute_any_of_these refutation pst nonempty_subgs_terms: real; val result = if length subgs = 0 (*orelse not (pass_check_print_read_terms ctxt standardized_props)*) then NONE @@ -112,8 +112,9 @@ fun apply_PSL_to_get_seeds_of_or2and_edges in result: seed_of_or2and_edge option end; + val result = List.mapPartial mk_proof_key_value pairs_n_psts: seeds_of_or2and_edge; in - List.mapPartial mk_proof_key_value pairs_n_psts: seeds_of_or2and_edge + result end; (*TODO: maybe we should add the premises of parent_or to orig_prems after cleaning types and free-variable names.*) @@ -173,16 +174,16 @@ fun conjecture_to_seed_of_or2and_edge (conjectures:(string * term) list): seed_o fun conjectures_to_seed_of_or2and_edge (term2name:SS.synched_term2string_table) (pst:Proof.state) (conjectures_w_name: (string * term) list) = let - fun get_ctxt_w_proof_goal trm = Proof.context_of (TDU.mk_pst_to_prove_from_term pst trm) : Proof.context; - fun mk_prop term = if Top_Down_Util.is_prop term then term else HOLogic.mk_Trueprop term : term; - fun check_prop (trm:term) = try (Syntax.check_prop (get_ctxt_w_proof_goal trm)) trm : term option; - val conjectures = map snd conjectures_w_name : terms; - val conjectures_as_props = map mk_prop conjectures : terms; - val checked_conjectures = List.mapPartial check_prop conjectures_as_props : terms; - val ctxt = Proof.context_of pst : Proof.context; - val attach_lemma_name = fn conjecture => (SS.get_lemma_name term2name ctxt conjecture, conjecture): string * term; - val name_conjecture_pairs = map attach_lemma_name checked_conjectures: (string * term) list : (string * term) list; - val result = conjecture_to_seed_of_or2and_edge name_conjecture_pairs : seed_of_or2and_edge; + fun get_ctxt_w_proof_goal trm = Proof.context_of (TDU.mk_pst_to_prove_from_term pst trm) : Proof.context; + fun mk_prop term = if Top_Down_Util.is_prop term then term else HOLogic.mk_Trueprop term: term; + fun check_prop (trm:term) = try (Syntax.check_prop (get_ctxt_w_proof_goal trm)) trm : term option; + val conjectures = map snd conjectures_w_name : terms; + val conjectures_as_props = map mk_prop conjectures : terms; + val checked_conjectures = List.mapPartial check_prop conjectures_as_props : terms; + val ctxt = Proof.context_of pst : Proof.context; + fun attach_lemma_name conjctr = (SS.get_lemma_name term2name ctxt "" conjctr, conjctr) : string * term; + val name_conjecture_pairs = map attach_lemma_name checked_conjectures: (string * term) list : (string * term) list; + val result = conjecture_to_seed_of_or2and_edge name_conjecture_pairs : seed_of_or2and_edge; in result: seed_of_or2and_edge end; @@ -214,7 +215,7 @@ fun prove_goal_assuming_conjectures (pst:Proof.state) ((Or_N, [orterm]): key)(*p (*apply_proof considers the first result only.*) fun apply_proof (proof:string) (pst_tobe_proved:Proof.state) = let - val sh_result = Subtools.tool_output_n_timeout_to_logtac proof NONE 5.0 pst_tobe_proved; + val sh_result = Subtools.tool_output_n_timeout_to_logtac proof NONE 15.0 pst_tobe_proved; val result_pst = Seq.pull sh_result <$> fst <$> snd |> Utils.the' "prove_goal_assuming_conjectures failed.": Proof.state; in result_pst @@ -222,7 +223,7 @@ fun prove_goal_assuming_conjectures (pst:Proof.state) ((Or_N, [orterm]): key)(*p fun apply_proofs (proofs:strings) (pst_tobe_proved:Proof.state) = fold apply_proof proofs pst_tobe_proved: Proof.state; val proof_to_get_here = Or2And_Edge.how_to_get_andnodes_from_ornode_of proof: strings; val pst_after_applying_how_to_get_andnodes_from_ornode = apply_proofs proof_to_get_here pst_to_apply_tactics: Proof.state; - val timeouts = {overall = 30.0, hammer = 5.0, quickcheck = 1.0, nitpick = 2.0}: TBC_Utils.timeouts; + val timeouts = {overall = 30.0, hammer = 10.0, quickcheck = 1.0, nitpick = 2.0}: TBC_Utils.timeouts; (*very expensive*) val script_opt_gen = TBC_Utils.pst_to_proofscript_opt timeouts "Finish_Goal_After_Assuming_Subgoals_And_Conjectures" pst_after_applying_how_to_get_andnodes_from_ornode <$> fst: string option; @@ -243,7 +244,7 @@ fun prove_ornode_assuming_andnode (seed_of_or2and_edge as {new_goals, proof, importance}: seed_of_or2and_edge)(*child nodes*) : add_or2and_edge option = let - val _ = SS.update_is_branch parent_orkey sagraph: unit; + val _ = SS.update_is_branch parent_orkey sagraph: unit;(*TODO: Double-check. Why do I need to update_is_branch here? It should be done when expanding the parental or-node.*) val (proved_parent_or, script_opt_gen) = prove_goal_assuming_conjectures pst parent_orkey seed_of_or2and_edge: (bool * string option); in if proved_parent_or @@ -384,13 +385,12 @@ fun decremental _ (_:Proof.state, _:SS.synched_abduction_graph, _:SS.synched_p fun abduction_for_explicit_conjectures (pst:Proof.state) (parent_orkey:key) (conjectures:conjectures) (sterm2name:SS.synched_term2string_table, refutation: SS.synched_term2real_table, sagraph: SS.synched_abduction_graph, proved_ors:SS.synched_proved_simps) = let - fun tracing' mssg = (); + fun tracing' mssg = tracing mssg; val _ = tracing' "\n ** Trying to prove **:"; val _ = tracing' (SS.get_orkey_name sterm2name (Proof.context_of pst) parent_orkey); val ctxt = Proof.context_of pst; val _ = Abduction_Graph.print_key ctxt parent_orkey; val _ = tracing' " decremental abduction starts"; - val _ = map snd conjectures |> map (tracing' o Isabelle_Utils.trm_to_string ctxt); val limit = if Abduction_Graph.is_final_goal (Synchronized.value sagraph) parent_orkey then Config.get ctxt Top_Down_Util.limit_for_first_decrement else Config.get ctxt Top_Down_Util.limit_for_other_decrement diff --git a/Abduction/Shared_State.ML b/Abduction/Shared_State.ML index 3702a4e1..1e405176 100644 --- a/Abduction/Shared_State.ML +++ b/Abduction/Shared_State.ML @@ -27,7 +27,7 @@ val any_of_these_is_refuted: synched_term2real_table -> Proof.state -> terms -> type term2string_table; type synched_term2string_table; val mk_term2string_table: unit -> synched_term2string_table; -val get_lemma_name : synched_term2string_table -> Proof.context -> term -> string; +val get_lemma_name : synched_term2string_table -> Proof.context -> string -> term -> string; (*TODO: Do we really need get_orkey_name even though we have get_lemma_name?*) val get_orkey_name : synched_term2string_table -> Proof.context -> Abduction_Graph.key -> string; @@ -143,12 +143,13 @@ fun insert_string (cnjctr:term, lemma_name:string) (old_table:term2string_table) in -fun get_lemma_name (synched_table:synched_term2string_table) (ctxt:Proof.context) (term:term) = +fun get_lemma_name (synched_table:synched_term2string_table) (ctxt:Proof.context) (candidate:string) (term:term) = let - val standardized_term = Top_Down_Util.standardize_vnames term : term; - val old_table = Synchronized.value synched_table : term2string_table; - val already_checked = defined old_table standardized_term : bool; - fun mk_new_name_pair _ = (standardized_term, Top_Down_Util.mk_new_lemma_name ctxt false) : (term * string); + val standardized_term = Top_Down_Util.standardize_vnames term : term; + val old_table = Synchronized.value synched_table : term2string_table; + val already_checked = defined old_table standardized_term : bool; + val mk_new_lemma_name = Top_Down_Util.mk_new_lemma_name : Proof.context -> bool -> string -> string; + fun mk_new_name_pair _ = (standardized_term, mk_new_lemma_name ctxt false candidate): (term * string); val _ = if already_checked then () @@ -173,7 +174,7 @@ structure AG = Abduction_Graph; structure UAG = Update_Abduction_Graph; fun get_orkey_name (synched_table:synched_term2string_table) (ctxt:Proof.context) ((AG.Or_N, [term]): AG.key) = - get_lemma_name synched_table ctxt term + get_lemma_name synched_table ctxt "" term | get_orkey_name _ _ _ = error "get_orkey_name failed. Not an orkey." type synched_abduction_graph = abduction_graph Synchronized.var; diff --git a/Abduction/Top_Down_Util.ML b/Abduction/Top_Down_Util.ML index f1850f93..a8102151 100644 --- a/Abduction/Top_Down_Util.ML +++ b/Abduction/Top_Down_Util.ML @@ -30,7 +30,7 @@ val mk_prop : Proof.context -> term -> term; val mk_unbound_bound_vars_free_vars : Proof.context -> term -> term; val get_lemma_names_from_sh_output : theory -> string -> strings; val is_thm_name_registered : Proof.context -> string -> bool; -val mk_new_lemma_name : Proof.context -> bool(*is_final_goal*) -> string; +val mk_new_lemma_name : Proof.context -> bool(*is_final_goal*) -> string (*lemma_type*) -> string; val term_compare : term * term -> order; val term_to_thm : Proof.context -> term -> thm; val timeout_config : real Config.T; @@ -48,6 +48,7 @@ val mk_extended_rhses : Proof.context -> terms -> term -> terms; val replace_redundant_compound_subtrm_with_free_var: Proof.context -> (term * term) -> (term * term); val parallel_filter : ('a -> bool) -> 'a list -> 'a list; val parallel_filter_out : ('a -> bool) -> 'a list -> 'a list; +val is_template_based : string -> bool; end; @@ -224,21 +225,21 @@ fun get_lemma_names_from_sh_output (thy:theory) (sh_output:string) = val strings = map Token.unparse tokens : strings; fun get_base_name (name:string) = if Long_Name.is_qualified name then Long_Name.base_name name else name; val base_names = map get_base_name strings: strings; - val filtered = filter (String.isPrefix "top_down_lemma_") base_names: strings; + val filtered = filter (String.isPrefix "abduced_lemma_") base_names: strings; in filtered end; fun is_thm_name_registered (ctxt:Proof.context) (thm_name:string) = try (Proof_Context.get_thm ctxt) thm_name |> is_some: bool; -fun mk_new_lemma_name (ctxt:Proof.context) (is_final_goal:bool): string = +fun mk_new_lemma_name (ctxt:Proof.context) (is_final_goal:bool) (lemma_type:string): string = let - val name_header = if is_final_goal then "original_goal_" else "top_down_lemma_"; + val name_header = (if is_final_goal then "original_goal_" else "abduced_lemma_") ^ lemma_type; val candidate_name = name_header ^ Int.toString (serial()): string; val this_name_is_already_taken = is_thm_name_registered ctxt candidate_name; in if this_name_is_already_taken - then mk_new_lemma_name ctxt is_final_goal + then mk_new_lemma_name ctxt is_final_goal lemma_type else candidate_name end @@ -440,4 +441,28 @@ fun parallel_filter_in_or_out (filter_in:bool) (condition:'a -> bool) (xs:'a lis fun parallel_filter (condition:'a -> bool) (xs:'a list) = parallel_filter_in_or_out true condition xs; fun parallel_filter_out (condition:'a -> bool) (xs:'a list) = parallel_filter_in_or_out false condition xs; +val isPrefix = String.isPrefix; + +fun is_template_based (name:string) = + isPrefix "abduced_lemma_Associativity" name orelse + isPrefix "abduced_lemma_Identity" name orelse + isPrefix "abduced_lemma_Invertibility" name orelse + isPrefix "abduced_lemma_Commutativity" name orelse + isPrefix "abduced_lemma_Idempotent_Element" name orelse + isPrefix "abduced_lemma_Idempotency" name orelse + isPrefix "abduced_lemma_Zero_Element" name orelse + isPrefix "abduced_lemma_Distributivity" name orelse + isPrefix "abduced_lemma_Ant_Distributivity" name orelse + isPrefix "abduced_lemma_Homomorphism_2" name orelse + isPrefix "abduced_lemma_Transitivity" name orelse + isPrefix "abduced_lemma_Symmetry" name orelse + isPrefix "abduced_lemma_Connexity" name orelse + isPrefix "abduced_lemma_Reflexivity" name orelse + isPrefix "abduced_lemma_Square" name orelse + isPrefix "abduced_lemma_Square_Root" name orelse + isPrefix "abduced_lemma_Projection" name orelse + isPrefix "abduced_lemma_Swap_Constructor" name orelse + isPrefix "abduced_lemma_Swap_Unary" name orelse + isPrefix "abduced_lemma_Composite_Commutativity" name; + end; \ No newline at end of file diff --git a/PSL/Subtool.ML b/PSL/Subtool.ML index 6fbcd8c3..4d154976 100644 --- a/PSL/Subtool.ML +++ b/PSL/Subtool.ML @@ -148,20 +148,20 @@ fun tool_output_n_timeout_to_logtac (sh_output:string) (importance: real option) in if Utils.debug then (tracing1 (); tracing2 (); tracing3 (); ()) else () end; - val state_w_using = Proof.using_cmd using_raw state : Proof.state; fun timeout f = Utils.try_with Seq.empty (Isabelle_Utils.timeout_apply (seconds to) f) val tac_results = timeout (Proof.apply checked_range) state_w_using |> Seq.filter_results - (*Why Seq.try Seq.hd? Because we want to evaluate the head of - sequence strictly here to catch errors immediately.*) - |> Utils.try_with Seq.empty (Seq.try Seq.hd): Proof.state Seq.seq; + (*Why Seq.try Seq.hd? Because we want to evaluate the head of + sequence strictly here to catch errors immediately.*) + (*Note that we have to use timeout here due to the use of lazy sequence.*) + |> Utils.try_with Seq.empty (timeout (Seq.try Seq.hd)): Proof.state Seq.seq; val results_w_log = Seq.map (fn x => ([node], x)) tac_results : (Dynamic_Utils.log * Proof.state) Seq.seq; in results_w_log : (Dynamic_Utils.log * Proof.state) Seq.seq end; -fun sh_output_to_sh_stttac (output:string) = Dynamic_Utils.logtac_to_stttac (tool_output_n_timeout_to_logtac output NONE 10.0) +fun sh_output_to_sh_stttac (output:string) = Dynamic_Utils.logtac_to_stttac (tool_output_n_timeout_to_logtac output NONE 7.0) : Proof.state Dynamic_Utils.stttac; (** Sledgehammer_Tacctic: Sledgehammer as a state monad based tactic. **) @@ -252,7 +252,7 @@ fun state_stttacs (timeout:real) (pst:Proof.state) = val induct_output_strs = Utils.try_with [] (Isabelle_Utils.timeout_apply (seconds timeout) pst_to_smart_induct_output_strs) pst: strings; val numb_of_candidates = length induct_output_strs; val low_importances = replicate numb_of_candidates 0.7: real list; - val importances = 0.95 :: 0.9 :: 0.85 :: 0.8 :: 0.75 :: low_importances (*TODO: magic number*) + val importances = 0.95 :: 0.9 :: 0.85 :: 0.8 :: 0.75 :: low_importances (*TODO: magic number for Abduction Prover*) |> take numb_of_candidates: real list; val induct_outputs = induct_output_strs ~~ importances: (string * real) list; val stttacs = Par_List.map mk_state_stttac induct_outputs: Proof.state Dynamic_Utils.stttac list; diff --git a/Smart_Isabelle.thy b/Smart_Isabelle.thy index 0dd02072..a637af87 100644 --- a/Smart_Isabelle.thy +++ b/Smart_Isabelle.thy @@ -6,7 +6,4 @@ theory Smart_Isabelle "Abduction.Abduction" begin -lemma "True" - oops - end \ No newline at end of file diff --git a/TBC/TBC.thy b/TBC/TBC.thy index 547c92f9..fd4bedb9 100644 --- a/TBC/TBC.thy +++ b/TBC/TBC.thy @@ -385,7 +385,7 @@ then conjectures_n_pst_to_pst_n_proof' unprocessed_pnodes new_pst (processed_pnodes @ [processed_pnode]) end; - val _ = if counter = 0 then () else tracing ("\nProperty-Based Conjecturing. Round: " ^ Int.toString counter ^ "."); + val _ = if counter = 0 then () else tracing ("\nTemplate-Based Conjecturing. Round: " ^ Int.toString counter ^ "."); val (new_pst, processed_pnodes) = conjectures_n_pst_to_pst_n_proof' unprocessed_pnodes pst []; in if original_goal_is_proved processed_pnodes