From 2c5fb016b3f2f1561c0ce191d2bed86e41ef869e Mon Sep 17 00:00:00 2001 From: Yutaka Ng <7411634+yutakang@users.noreply.github.com> Date: Sun, 1 Oct 2023 20:13:00 +0100 Subject: [PATCH] Abduction: bug fixed. add type cleaning and type checking to refutation. --- Abduction/Abduction.thy | 2 +- Abduction/Seed_Of_Or2And_Edge.ML | 15 ++++++++------- Abduction/Shared_State.ML | 11 +++++++---- 3 files changed, 16 insertions(+), 12 deletions(-) diff --git a/Abduction/Abduction.thy b/Abduction/Abduction.thy index 3e8a0df4..57505a30 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 20 \ +setup\ Config.put_global Top_Down_Util.limit_for_other_decrement 40 \ (* UI *) ML\ (*This part (the definitions of long_keyword, long_statement, and short_statement) are from diff --git a/Abduction/Seed_Of_Or2And_Edge.ML b/Abduction/Seed_Of_Or2And_Edge.ML index e542170c..3be75c9c 100644 --- a/Abduction/Seed_Of_Or2And_Edge.ML +++ b/Abduction/Seed_Of_Or2And_Edge.ML @@ -126,12 +126,6 @@ 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 @@ -140,12 +134,19 @@ fun condition_to_filter_out_conjecture (parent_or(*parent_or*):term) (refutation 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; + fun concl_of_conj_refuted_even_cncl_of_parent_is_not _ = + if is_none concl_of_meta_imp_in_parent orelse is_none concl_of_meta_imp_in_conjec + then false + else if SS.is_refuted refutation pst (the concl_of_meta_imp_in_parent) + then false + else SS.is_refuted refutation pst (the concl_of_meta_imp_in_conjec); 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 - concls_are_same () + concls_are_same () orelse + concl_of_conj_refuted_even_cncl_of_parent_is_not () (* (*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.*) *) diff --git a/Abduction/Shared_State.ML b/Abduction/Shared_State.ML index 37a11cc5..f0c626c7 100644 --- a/Abduction/Shared_State.ML +++ b/Abduction/Shared_State.ML @@ -97,8 +97,11 @@ in fun refute (synched_table:synched_term2real_table) (pst:Proof.state) (cnjctr:term): real = let val cnjctr_prop = if Top_Down_Util.is_prop cnjctr then cnjctr else HOLogic.mk_Trueprop cnjctr: term; + val cnjctr_prop_clean = Top_Down_Util.standardize_vnames cnjctr_prop + |> Isabelle_Utils.strip_atyp + |> Utils.try_with @{prop "False"} (Syntax.check_prop (Proof.context_of pst)) : term; val old_table = Synchronized.value synched_table : term2real_table; - val already_checked = defined old_table cnjctr_prop : bool; + val already_checked = defined old_table cnjctr_prop_clean : bool; fun quickcheck cnjctr = (cnjctr, TBC_Utils.term_has_counterexample_in_pst pst cnjctr) : (term * real); val _ = if already_checked then () @@ -107,12 +110,12 @@ fun refute (synched_table:synched_term2real_table) (pst:Proof.state) (cnjctr:ter (* It is okay to spend some time to run quick-check before calling Synchronized.change: * Even if other threads find a counter-example for the same conjecture, * the result should be the same. *) - val pair = quickcheck cnjctr_prop + val pair = quickcheck cnjctr_prop_clean 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_clean: real; in result: real end;