From 03644fbbc7c4af11fc18767d3b3893c2b1acd29e Mon Sep 17 00:00:00 2001 From: Yutaka Ng <7411634+yutakang@users.noreply.github.com> Date: Sun, 1 Oct 2023 17:06:19 +0100 Subject: [PATCH] Abduction: critical change. conditino to filter out changed. Also, higher importance for template-based conjectures. --- Abduction/Abduction.thy | 2 +- Abduction/Abduction_Graph.ML | 15 ++- Abduction/Abduction_Node.ML | 5 + Abduction/Or_Node.ML | 6 ++ Abduction/Proof_By_Abduction.ML | 156 ++++++++++++++----------------- Abduction/Seed_Of_Or2And_Edge.ML | 49 +++++++--- Abduction/Shared_State.ML | 43 +++++---- 7 files changed, 151 insertions(+), 125 deletions(-) diff --git a/Abduction/Abduction.thy b/Abduction/Abduction.thy index 64e0652b..3e8a0df4 100644 --- a/Abduction/Abduction.thy +++ b/Abduction/Abduction.thy @@ -75,7 +75,7 @@ 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 40 \ -setup\ Config.put_global Top_Down_Util.limit_for_other_decrement 15 \ +setup\ Config.put_global Top_Down_Util.limit_for_other_decrement 20 \ (* UI *) ML\ (*This part (the definitions of long_keyword, long_statement, and short_statement) are from diff --git a/Abduction/Abduction_Graph.ML b/Abduction/Abduction_Graph.ML index 57e083e1..335fafe4 100644 --- a/Abduction/Abduction_Graph.ML +++ b/Abduction/Abduction_Graph.ML @@ -54,6 +54,7 @@ val lemma_name_of : abduction_graph -> key -> str val print_orkey : Proof.context -> abduction_graph -> key -> unit; val proof_of : abduction_graph -> key -> strings; val proof_id_of : abduction_graph -> key -> int option; +val is_template_based : abduction_graph -> key -> bool; val compute_importance_of_ornode : abduction_graph -> key -> real; val sort_orkeys_based_on_importance : abduction_graph -> keys -> keys; @@ -309,14 +310,26 @@ fun is_worth_proving (ctxt:Proof.context) (graph:abduction_graph) (key:key) = (* proof_id_of *) fun proof_id_of (graph:abduction_graph) (key:key) = PGraph.get_node graph key |> Abduction_Node.proof_id_of: int option; +(* is_template_based *) +fun is_template_based (ag:abduction_graph) (key:key) = + let + val node = PGraph.get_node ag key: abduction_node; + val result = Abduction_Node.is_template_based node; + in + result + end; + (* compute_importance_of_ornode *) fun compute_importance_of_ornode (ag:abduction_graph) (orkey as (Or_N, _)) = let val parent_andkeys = PGraph.immediate_preds ag orkey: keys; val importances_of_parents = map (importance ag) parent_andkeys: real list; - val importance = case Utils.reals_to_max_option importances_of_parents of + val importance_from_parent = case Utils.reals_to_max_option importances_of_parents of NONE => error "compute_importance_of_ornode. No ancestral andnode." | SOME max => max: real; + val importance = if is_template_based ag orkey + then (1.0 + importance_from_parent) / 2.0 + else importance_from_parent: real; (*TODO: magic number & magic formula*) in importance end diff --git a/Abduction/Abduction_Node.ML b/Abduction/Abduction_Node.ML index f82ca1bb..73bbc54d 100644 --- a/Abduction/Abduction_Node.ML +++ b/Abduction/Abduction_Node.ML @@ -34,6 +34,7 @@ val proof_of : abduction_node -> strings opt val is_branch : abduction_node -> bool; val is_final_goal : abduction_node -> bool; val lemma_name_of : abduction_node -> string; +val is_template_based : abduction_node -> bool; val is_worth_proving : Proof.context -> abduction_node -> bool; (* query on abduction_node for or2and_edge *) @@ -119,6 +120,10 @@ fun or2and_edge_to_proof (Or_To_And or2and_edge:abduction_node) = Or2And_Edge.or fun lemma_name_of (Or_Node or_nd) = #lemma_name or_nd | lemma_name_of _ = error "lemma_name_of failed. Not an Or_Node." +(* is_template_based *) +fun is_template_based (Or_Node ornode) = Or_Node.is_template_based ornode + | is_template_based _ = error "is_template_based in Abduction_Node.ML failed"; + (** destructors on abduction_node **) (* dest_Or_Node *) fun dest_Or_Node (Or_Node or_b) = or_b diff --git a/Abduction/Or_Node.ML b/Abduction/Or_Node.ML index 8089a692..c3819453 100644 --- a/Abduction/Or_Node.ML +++ b/Abduction/Or_Node.ML @@ -21,6 +21,8 @@ val is_worth_proving : Proof.context -> ornode -> bool; type is_final_goal = bool; val mk_ornode: Proof.context -> is_final_goal -> string -> term -> ornode; +val is_template_based: ornode -> bool; + (* update of ornode *) val update_gg_parent_not_finished: ornode -> bool -> ornode; val update_proved_completely : ornode -> ornode; @@ -68,6 +70,7 @@ fun is_worth_proving (ctxt:Proof.context) (ornode:ornode) = (* creation of ornode *) 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 @@ -87,6 +90,9 @@ fun mk_ornode (ctxt:Proof.context) (is_final_goal:is_final_goal) (lemma_name:str }: ornode end; +fun is_template_based ({lemma_name, ...}: ornode) = + Top_Down_Util.is_template_based lemma_name; + (** update of ornode **) (* update_gg_parent_not_finished *) (* diff --git a/Abduction/Proof_By_Abduction.ML b/Abduction/Proof_By_Abduction.ML index e25eff78..d4118622 100644 --- a/Abduction/Proof_By_Abduction.ML +++ b/Abduction/Proof_By_Abduction.ML @@ -39,7 +39,7 @@ fun prove_standard_simp_rules synched_agraph: SS.synched_abduction_graph, refutation : SS.synched_term2real_table, term2name : SS.synched_term2string_table, - proved_ors : SS.synched_proved_simps, + proved_simps : SS.synched_proved_simps, orig_prems : terms) (lemma_term:term): unit = let @@ -51,15 +51,15 @@ fun prove_standard_simp_rules val filtered_explicit = TDU.parallel_filter_out condition_to_filter_out explicit_conjectures : (string * term) list; val refute = Shared_State.is_refuted refutation pst o snd : (string * term) -> bool; val explicit_wo_counterexample = TDU.parallel_filter_out refute filtered_explicit : (string * term) list; - fun prove_save_in_graph (lem_name:string, lem_term:term) = + fun prove_save_in_shared_state (lem_name:string, lem_term:term) = let (*expensive*) val maybe_prf = prove_term_completely pst lem_term: strings option; in if is_none maybe_prf then () - else SS.add_proved_simp proved_ors (lem_name, lem_term) + else SS.add_proved_simp proved_simps (lem_name, lem_term) end; - val _ = Par_List.map prove_save_in_graph explicit_wo_counterexample: unit list; + val _ = Par_List.map prove_save_in_shared_state explicit_wo_counterexample: unit list; in () end; @@ -70,91 +70,75 @@ fun expand_ornode_if_original_goal_is_unproved synched_agraph: SS.synched_abduction_graph, refutation : SS.synched_term2real_table, term2name : SS.synched_term2string_table, - proved_ors : SS.synched_proved_simps, + proved_simps : SS.synched_proved_simps, orig_prems : terms) (or_key as (Or_N, [lemma_term]):key): bool = let - (*very expensive*) - val graph = Synchronized.value synched_agraph : abduction_graph; - in -(* - if is_some maybe_proof (*ornode was proved completely.*) - then + val graph = Synchronized.value synched_agraph : abduction_graph; + (*top-down explicit conjecturing*) + val explicit_conjectures = All_Top_Down_Conjecturing.top_down_conjectures term2name pst lemma_term : (string * term) list; + val condition_to_filter_out = SOOE.condition_to_filter_out_conjecture lemma_term refutation orig_prems pst graph false o snd: string * term -> bool; + val filtered_explicit = TDU.parallel_filter_out condition_to_filter_out explicit_conjectures: (string * term) list : (string * term) list; + val explicit_wo_counterexample = TDU.parallel_filter_out (Shared_State.is_refuted refutation pst o snd) filtered_explicit : (string * term) list; + 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; + (*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 proof = the maybe_proof: strings; - val _ = SS.update_after_proving_ornode proof or_key (Proof.context_of pst) synched_agraph; + val simp_thm = TDU.term_to_thm ctxt simp_term: thm; + val ctxt_w_simp = Simplifier.add_simp simp_thm ctxt: Proof.context; + val simplifier = Basic_Simplifier.simplify ctxt_w_simp: thm -> thm;(*asm_full_simplify*) + val simplifier_w_timeout = try (Isabelle_Utils.timeout_apply (Time.fromSeconds 1) simplifier): thm -> thm option; + val cnjctr_thm = TDU.term_to_thm ctxt cnjctr_term: thm; + val simped_cnjctr = simplifier_w_timeout cnjctr_thm: thm option; + fun schematic_to_free (Var ((str, _), typ)) =(*TODO: Can I do something better than this?*) + let + val vname = space_explode "." str |> hd + in Free (vname, typ) + end + | schematic_to_free aterm = aterm; + fun remove_schematic (term:term) = (map_aterms schematic_to_free term); in - SS.final_goal_proved_completely synched_agraph - end - else (*if we cannot prove the ornode completely, expand it using Extend_Leaf and conjecturing*) -*) - let - (*top-down explicit conjecturing*) - val explicit_conjectures = All_Top_Down_Conjecturing.top_down_conjectures term2name pst lemma_term : (string * term) list; - val condition_to_filter_out = SOOE.condition_to_filter_out_conjecture lemma_term refutation orig_prems pst graph false o snd: string * term -> bool; - val filtered_explicit = TDU.parallel_filter_out condition_to_filter_out explicit_conjectures: (string * term) list : (string * term) list; - val explicit_wo_counterexample = TDU.parallel_filter_out (Shared_State.is_refuted refutation pst o snd) filtered_explicit : (string * term) list; - 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; - (*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 = + if is_none simped_cnjctr + then [cnjctr] + else let - val simp_thm = TDU.term_to_thm ctxt simp_term: thm; - val ctxt_w_simp = Simplifier.add_simp simp_thm ctxt: Proof.context; - val simplifier = Basic_Simplifier.simplify ctxt_w_simp: thm -> thm;(*asm_full_simplify*) - val simplifier_w_timeout = try (Isabelle_Utils.timeout_apply (Time.fromSeconds 1) simplifier): thm -> thm option; - val cnjctr_thm = TDU.term_to_thm ctxt cnjctr_term: thm; - val simped_cnjctr = simplifier_w_timeout cnjctr_thm: thm option; - fun schematic_to_free (Var ((str, _), typ)) =(*TODO: Can I do something better than this?*) - let - val vname = space_explode "." str |> hd - in Free (vname, typ) - end - | schematic_to_free aterm = aterm; - fun remove_schematic (term:term) = (map_aterms schematic_to_free term); + 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_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 - if is_none simped_cnjctr + if size_of_simped_cnjctr >= size_of_orig_cnjctr (*orelse simped_cnjctr_term = @{term True}*) + (*orelse rm_Trueprop simped_cnjctr_term = rm_Trueprop lemma_term*) then [cnjctr] - else - let - 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_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 - if size_of_simped_cnjctr >= size_of_orig_cnjctr (*orelse simped_cnjctr_term = @{term True}*) - (*orelse rm_Trueprop simped_cnjctr_term = rm_Trueprop lemma_term*) - then [cnjctr] - else [simp, (simped_cnjctr_name, simped_cnjctr_term)](*TODO: not efficient.*) - end - 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) = - fold simp_explicit_conjectures_for_one_rule simps cnjctrs: SOOE.conjectures; - - val simps = Synchronized.value proved_ors: SS.proved_simps; - 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; - val seeds_from_tactics = SOOE.apply_PSL_to_get_seeds_of_or2and_edges (term2name, refutation) pst_to_prove: seeds_of_or2and_edge; - val graph_extended_by_conjecture = Synchronized.value synched_agraph: abduction_graph; - val filtered_seeds_from_tactics = SOOE.filter_out_bad_seeds_from_tactic lemma_term refutation orig_prems pst graph_extended_by_conjecture seeds_from_tactics - val tactics_seeds_wo_counterexam = filter_out (SOOE.seed_has_counterexample refutation pst) filtered_seeds_from_tactics: seeds_of_or2and_edge; - val _ = SOOE.abduction_for_tactic_based_conjectures pst or_key tactics_seeds_wo_counterexam synched_agraph: unit; - in - (*seeds_to_updated_graph is very expensive*) - SS.final_goal_proved_completely synched_agraph - end + else [simp, (simped_cnjctr_name, simped_cnjctr_term)](*TODO: not efficient.*) + end + 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) = + fold simp_explicit_conjectures_for_one_rule simps cnjctrs: SOOE.conjectures; + val simps = Synchronized.value proved_simps: SS.proved_simps; + 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_simps): unit; + (*tactic application as conjecturing. A little expensive*) + val pst_to_prove = TDU.mk_pst_to_prove_from_term pst lemma_term: state; + val seeds_from_tactics = SOOE.apply_PSL_to_get_seeds_of_or2and_edges (term2name, refutation) pst_to_prove: seeds_of_or2and_edge; + val graph_extended_by_conjecture = Synchronized.value synched_agraph: abduction_graph; + val filtered_seeds_from_tactics = SOOE.filter_out_bad_seeds_from_tactic lemma_term refutation orig_prems pst graph_extended_by_conjecture seeds_from_tactics + val tactics_seeds_wo_counterexam = filter_out (SOOE.seed_has_counterexample refutation pst) filtered_seeds_from_tactics: seeds_of_or2and_edge; + val _ = SOOE.abduction_for_tactic_based_conjectures pst or_key tactics_seeds_wo_counterexam synched_agraph: unit; + in + (*seeds_to_updated_graph is very expensive*) + SS.final_goal_proved_completely synched_agraph end | expand_ornode_if_original_goal_is_unproved _ _ = error "expand_ornode failed. Not an Or_N."; @@ -163,9 +147,9 @@ fun current_time (start:Timing.start) = Time.toReal (#elapsed (Timing.result sta fun still_has_time (start:Timing.start) (pst:Proof.state) = current_time start < get_timeout pst: bool; fun expand_ornode_if_original_goal_is_unproved_w_timeout (start:Timing.start) - (pst:state, synched_agraph, refutation, term2name, proved_ors, orig_prems) (or_key as (Or_N, [_]):key): bool = + (pst:state, synched_agraph, refutation, term2name, proved_simps, orig_prems) (or_key as (Or_N, [_]):key): bool = if Time.toReal (#elapsed (Timing.result start)) < get_timeout pst - then expand_ornode_if_original_goal_is_unproved (pst, synched_agraph, refutation, term2name, proved_ors, orig_prems) or_key + then expand_ornode_if_original_goal_is_unproved (pst, synched_agraph, refutation, term2name, proved_simps, orig_prems) or_key else false | expand_ornode_if_original_goal_is_unproved_w_timeout _ _ _ = error "expand_ornode_if_original_goral_is_unproved_w_timeout failed."; @@ -176,7 +160,7 @@ fun loop (counter:int) (max_depth:int) (start:Timing.start) synched_agraph: SS.synched_abduction_graph, refutation:SS.synched_term2real_table, term2name:SS.synched_term2string_table, - proved_ors:SS.synched_proved_simps, + proved_simps:SS.synched_proved_simps, orig_prems: terms)) = if counter < 8 andalso still_has_time start pst then @@ -190,11 +174,11 @@ fun loop (counter:int) (max_depth:int) (start:Timing.start) val _ = tracing "They are:" val _ = map (print_orkey ctxt abduction_graph) sorted_orkeys val expand_ornode = expand_ornode_if_original_goal_is_unproved_w_timeout start - (pst, synched_agraph, refutation, term2name, proved_ors, orig_prems) + (pst, synched_agraph, refutation, term2name, proved_simps, orig_prems) : Abduction_Graph.key -> bool; val numb_of_processors = Thread.numProcessors ():int; val _ = tracing ("numb_of_processors is " ^ Int.toString numb_of_processors ^ "."); - val numb_of_nds_to_expand = 2 * numb_of_processors;(*TODO: magic number*) + val numb_of_nds_to_expand = numb_of_processors;(*TODO: magic number*) val top_ornodes = take numb_of_nds_to_expand sorted_orkeys: keys; val some_orkey = Par_List.find_some expand_ornode top_ornodes: key option; val solved = is_some some_orkey: bool; diff --git a/Abduction/Seed_Of_Or2And_Edge.ML b/Abduction/Seed_Of_Or2And_Edge.ML index acb19490..e542170c 100644 --- a/Abduction/Seed_Of_Or2And_Edge.ML +++ b/Abduction/Seed_Of_Or2And_Edge.ML @@ -76,7 +76,7 @@ fun apply_PSL_to_get_seeds_of_or2and_edges let val ctxt = Proof.context_of pst; val extend_str = PSL_Interface.lookup ctxt "Extend_Leaf" |> the : PSL_Interface.strategy; - val timeouts = {overall = 60.0, hammer = 8.5, quickcheck = 1.0, nitpick = 2.0} : TBC_Utils.timeouts; + val timeouts = {overall = 60.0, hammer = 9.0, quickcheck = 1.0, nitpick = 2.0} : TBC_Utils.timeouts; 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; @@ -126,12 +126,29 @@ fun condition_to_filter_out_conjecture (parent_or(*parent_or*):term) (refutation not (SFTD.run_assertion pst parent_or SFTD.has_func_with_three_occs_in_a_row) andalso SFTD.run_assertion pst conjecture SFTD.has_func_with_three_occs_in_a_row; + fun has_counter_example_in_prems (pst:Proof.state) (term:term) = + let + val prems = Logic.strip_imp_prems term: terms; + in + SS.any_of_these_is_refuted refutation pst prems: bool + end; + fun get_concl (term:term) = try (snd o Logic.dest_implies) term + <$> Top_Down_Util.standardize_vnames + <$> Isabelle_Utils.strip_atyp + : term option; + val concl_of_meta_imp_in_parent = get_concl parent_or : term option; + val concl_of_meta_imp_in_conjec = get_concl conjecture: term option; + fun concls_are_same _ = Utils.mk_option_pair (concl_of_meta_imp_in_parent, concl_of_meta_imp_in_conjec) + <$> (op =) |> Utils.is_some_true; in too_large () orelse eq_to_final_goal () andalso from_tactic orelse concl_is_eq_to_final_goal () (*andalso seed_is_from_tactic seed*) orelse - has_func_with_three_occs_in_a_row_even_though_the_parent_does_not_have_those ()(* orelse - not from_tactic andalso not orig_prem_is_refuted andalso has_counter_example_in_prems pst conjecture: This is BAD.*) + has_func_with_three_occs_in_a_row_even_though_the_parent_does_not_have_those () orelse + concls_are_same () +(* + (*not from_tactic andalso not orig_prem_is_refuted andalso*) has_counter_example_in_prems pst conjecture(*TODO: This is BAD. We should also check if the conclusions are the same in the parent-node and the conjecture.*) +*) end; datatype conjecture_typ = Explicit_Conjecturing | Implicit_Conjecturing (*tactic application*); @@ -187,7 +204,8 @@ fun prove_goal_assuming_conjectures (pst:Proof.state) ((Or_N, [orterm]): key)(*p val ctxt = Proof.context_of pst : Proof.context; val conjecture_as_thm = TDU.term_to_thm ctxt conjecture : thm; val pst_w_conjecture_opt = try (Proof.map_context (register_thm_in_lthy name conjecture_as_thm)) pst: Proof.state option; - val pst_w_conjecture = case pst_w_conjecture_opt of SOME no_dup_pst => no_dup_pst | _ => pst + val pst_w_conjecture = case pst_w_conjecture_opt of SOME no_dup_pst => no_dup_pst + | _ => (tracing ("Warning! We could not assume " ^ name ^ "successfully."); pst) in pst_w_conjecture end; @@ -204,7 +222,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 = 60.0, hammer = 8.5, quickcheck = 1.0, nitpick = 2.0}: TBC_Utils.timeouts; + val timeouts = {overall = 60.0, hammer = 9.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; @@ -214,7 +232,7 @@ fun prove_goal_assuming_conjectures (pst:Proof.state) ((Or_N, [orterm]): key)(*p end | prove_goal_assuming_conjectures _ _ _ = error "prove_goal_assuming_conjectures failed badly."; -type add_or2and_edge = (key * abduction_node * conjectures); +type add_or2and_edge = ((*edge key*)key * (*edge val*)abduction_node * (*used*)conjectures); (*step 1. prove the parental or-node using some conjectures.*) fun prove_ornode_assuming_andnode @@ -248,7 +266,7 @@ fun prove_ornode_assuming_andnode SOME (or2and_edge_key, or2and_edge_val, relevant_new_goals) end else - NONE + NONE end | prove_ornode_assuming_andnode _ _ _ _ _ = error "how_to_prove_ornode_assmng_subgs_of_andnode failed."; @@ -317,9 +335,10 @@ fun eq_conjectures (pairs1:conjectures, pairs2:conjectures): bool = eq_set (op =) (goal_names1, goal_names2) end; -fun decremental _ (_:Proof.state, _:SS.synched_abduction_graph, _:SS.synched_proved_simps) (_:key) ([]:conjectures list) (_:conjectures list) _ results = results +fun decremental _ (_:Proof.state, _:SS.synched_abduction_graph, _:SS.synched_proved_simps) (_:key) ([]:conjectures list) (_:conjectures list) _ results = + results: add_or2and_edge list | decremental (counter:int) - (pst:Proof.state, synched_agraph:SS.synched_abduction_graph, synched_proved_ors:SS.synched_proved_simps) + (pst:Proof.state, synched_agraph:SS.synched_abduction_graph, synched_proved_simps:SS.synched_proved_simps) (parent_ornd:key) (conjectures::conjecturess:conjectures list) (checked:conjectures list) (failed_set:conjectures list) (results:add_or2and_edge list) = if counter > 0 @@ -331,8 +350,8 @@ fun decremental _ (_:Proof.state, _:SS.synched_abduction_graph, _:SS.synched_p val used_conjectures = if is_none triple_opt then [] else #3 (Utils.the' "decremental failed." triple_opt): conjectures; (*2 identify used conjectures that are not proved.*) - val proved_ors = Synchronized.value synched_proved_ors; - fun is_completely_proved cnjctr = member (op =) proved_ors cnjctr: bool; + val proved_simps = Synchronized.value synched_proved_simps; + fun is_completely_proved cnjctr = member (op =) proved_simps cnjctr: bool; val unproved_used_conjectures = filter_out is_completely_proved used_conjectures: conjectures; val (new_failed_set, new_candidates): (conjectures list * conjectures list) = (if null used_conjectures @@ -365,12 +384,12 @@ fun decremental _ (_:Proof.state, _:SS.synched_abduction_graph, _:SS.synched_p val promising_candidates = filter_out is_subset_of_any_failed_conjectures genuinely_new_candidates; val new_results = (if is_none triple_opt then [] else [the triple_opt]) @ results in - decremental (counter - 1) (pst, synched_agraph, synched_proved_ors) parent_ornd promising_candidates newly_checked new_failed_set new_results + decremental (counter - 1) (pst, synched_agraph, synched_proved_simps) parent_ornd promising_candidates newly_checked new_failed_set new_results end else results; 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) = + (sterm2name:SS.synched_term2string_table, refutation: SS.synched_term2real_table, sagraph: SS.synched_abduction_graph, proved_simps:SS.synched_proved_simps) = let fun tracing' mssg = tracing mssg; val _ = tracing' "\n ** Trying to prove **:"; @@ -382,9 +401,9 @@ fun abduction_for_explicit_conjectures (pst:Proof.state) (parent_orkey:key) (con val limit = if Abduction_Graph.is_final_goal agraph parent_orkey then Config.get ctxt Top_Down_Util.limit_for_first_decrement else Config.get ctxt Top_Down_Util.limit_for_other_decrement - val triples = decremental limit (pst, sagraph, proved_ors) parent_orkey [conjectures] [] [] []: add_or2and_edge list; + val triples = decremental limit (pst, sagraph, proved_simps) parent_orkey [conjectures] [] [] []: add_or2and_edge list; val _ = tracing' " decremental abduction ends"; - fun update_imp (key, abd_node, cnjctrs) = + fun update_imp (key, abd_node, cnjctrs:conjectures) = let val orig_term = Abduction_Graph.get_final_goal_term agraph: term; val orig_size = Term.size_of_term orig_term: int; diff --git a/Abduction/Shared_State.ML b/Abduction/Shared_State.ML index 3cfde19d..37a11cc5 100644 --- a/Abduction/Shared_State.ML +++ b/Abduction/Shared_State.ML @@ -111,8 +111,8 @@ fun refute (synched_table:synched_term2real_table) (pst:Proof.state) (cnjctr:ter in Synchronized.change synched_table (insert_bool pair): unit end; - val new_table = Synchronized.value synched_table: term2real_table; - val result = lookup new_table cnjctr_prop : real; + val new_table = Synchronized.value synched_table: term2real_table; + val result = lookup new_table cnjctr_prop : real; in result: real end; @@ -139,7 +139,7 @@ fun mk_term2string_table _ = Synchronized.var "synched_term2string_table" Term_T local -val lookup = Utils.the' "lookup for term2string_table failed." oo Term_Table.lookup; +val lookup = Utils.the' "lookup for term2string_table failed." oo Term_Table.lookup; fun insert_string (cnjctr:term, lemma_name:string) (old_table:term2string_table) = case try (Term_Table.insert (op =) (cnjctr, lemma_name)) old_table of NONE => old_table @@ -154,8 +154,7 @@ fun get_lemma_name (synched_table:synched_term2string_table) (ctxt:Proof.context 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 _ = + val _ = if already_checked then () else let @@ -166,8 +165,8 @@ fun get_lemma_name (synched_table:synched_term2string_table) (ctxt:Proof.context in Synchronized.change synched_table (insert_string pair): unit end; - val new_table = Synchronized.value synched_table : term2string_table; - val result = lookup new_table standardized_term: string; + val new_table = Synchronized.value synched_table : term2string_table; + val result = lookup new_table standardized_term: string; in result end; @@ -225,21 +224,21 @@ fun update_after_connecting_andnd_to_existing_ornd (ctxt:Proof.context) (sagraph map (update_after_connecting_andnd_to_existing_ornd' ctxt sagraph) orkeys; fun try_to_prove_ornode_and_update_graph (pst:Proof.state) (sagraph:synched_abduction_graph) (orkey:AG.key) = - let - val graph = Synchronized.value sagraph : abduction_graph; - val maybe_proof = AG.prove_orkey_completely orkey graph pst: strings option; - val _ = update_attacked sagraph orkey : unit; - in - if is_some maybe_proof (*ornode was proved completely.*) - then - let - val proof = the maybe_proof: strings; - val _ = update_after_proving_ornode proof orkey (Proof.context_of pst) sagraph; - in - () - end - else () - end; + let + val graph = Synchronized.value sagraph : abduction_graph; + val maybe_proof = AG.prove_orkey_completely orkey graph pst: strings option; + val _ = update_attacked sagraph orkey : unit; + in + if is_some maybe_proof (*ornode was proved completely.*) + then + let + val proof = the maybe_proof: strings; + val _ = update_after_proving_ornode proof orkey (Proof.context_of pst) sagraph; + in + () + end + else () + end; fun final_goal_proved_completely (sagraph:synched_abduction_graph) = let