From 43bd4e22a7de60aa9ecec0ad8bf103c717ad57e7 Mon Sep 17 00:00:00 2001 From: Yutaka Ng <7411634+yutakang@users.noreply.github.com> Date: Mon, 4 Nov 2024 23:38:06 +0100 Subject: [PATCH] Now, the AbductionProver can handle easy problems as well. --- Abduction/Abduction.thy | 33 ------------------------------ Abduction/Abduction_Graph.ML | 4 ++-- Abduction/Proof_By_Abduction.ML | 36 ++++++++++++++++++++++++--------- Abduction/Shared_State.ML | 6 +++--- 4 files changed, 32 insertions(+), 47 deletions(-) diff --git a/Abduction/Abduction.thy b/Abduction/Abduction.thy index 57505a30..c9a9dd27 100644 --- a/Abduction/Abduction.thy +++ b/Abduction/Abduction.thy @@ -148,37 +148,4 @@ val _ = theorem \<^command_keyword>\prove\ "prove"; end; \ -ML\ -structure TDU = Top_Down_Util; -structure SS = Shared_State; -structure SOOE = Seed_Of_Or2And_Edge; - -fun simp_explicit_conjecture (synched_term2string:SS.synched_term2string_table) (ctxt:Proof.context) - (simp as (_:string, simp_term:term)) (cnjctr as (_: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; - val simplifier = Basic_Simplifier.asm_full_simplify ctxt_w_simp: thm -> thm; - val simplifier_w_timeout = try (Isabelle_Utils.timeout_apply (Time.fromSeconds 1) simplifier): thm -> thm option; - val cnjctr_thm = TDU.term_to_thm ctxt simp_term: thm; - val simp_result = simplifier_w_timeout cnjctr_thm: thm option; - in - if is_none simp_result - then [cnjctr] - 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; - in - if simp_result_term = cnjctr_term - then [simp, (simp_result_name, simp_result_term)] - else [cnjctr] - end - end; - -fun simp_explicit_conjectures (synched_term2string:SS.synched_term2string_table) (ctxt:Proof.context) - (cnjctrs:SOOE.conjectures) (simp:SOOE.conjecture): SOOE.conjectures = - map (simp_explicit_conjecture synched_term2string ctxt simp) cnjctrs |> flat; -\ - end \ No newline at end of file diff --git a/Abduction/Abduction_Graph.ML b/Abduction/Abduction_Graph.ML index a6e10dc0..42d59442 100644 --- a/Abduction/Abduction_Graph.ML +++ b/Abduction/Abduction_Graph.ML @@ -386,8 +386,8 @@ fun final_goal_proved_completely (graph:abduction_graph) = (* prove_term_completely *) fun prove_term_completely (pst:Proof.state) (lemma_term:term) = let - val pst_to_prove = Top_Down_Util.mk_pst_to_prove_from_term pst lemma_term : Proof.state; - val timeouts = {overall = 60.0, hammer = 8.5, quickcheck = 1.0, nitpick = 2.0} : TBC_Utils.timeouts; + val pst_to_prove = Top_Down_Util.mk_pst_to_prove_from_term pst lemma_term : Proof.state; + val timeouts = {overall = 60.0, hammer = 8.5, quickcheck = 1.0, nitpick = 2.0} : TBC_Utils.timeouts; val maybe_result = TBC_Utils.pst_to_proofscripts_opt timeouts "Attack_On_Or_Node" pst_to_prove: (strings * Proof.state) option; val maybe_script = Option.map fst maybe_result : strings option; in diff --git a/Abduction/Proof_By_Abduction.ML b/Abduction/Proof_By_Abduction.ML index 2050fb84..5d615f88 100644 --- a/Abduction/Proof_By_Abduction.ML +++ b/Abduction/Proof_By_Abduction.ML @@ -318,15 +318,33 @@ fun proof_by_abduction (pst:Proof.state) (start:Timing.start) (term:term) = val synched_lemma_name_table = SS.mk_term2string_table (); val synched_proved_simps = SS.mk_synched_proved_simps (); val ori_prems = Logic.strip_imp_prems term |> map TDU.standardize_vnames |> map Isabelle_Utils.strip_atyp: terms; - val quintuple = (pst, synched_agraph, synched_refutation_table, synched_lemma_name_table, synched_proved_simps, ori_prems); - val _ = prove_standard_simp_rules quintuple standardized_term: unit; - val solved = loop 0 max_depth start quintuple; - val final_graph = Synchronized.value synched_agraph: Abduction_Graph.abduction_graph; - val lemma_name2term = abduction_graph_to_string2term_table final_graph: string2term_table; - val final_goal_name = lemma_name_of final_graph (Or_N, [standardized_term]): string; - val _ = if solved - then print_necessary_proofs_only pst final_graph lemma_name2term final_goal_name - else "" + val final_goal_key = (Or_N, [standardized_term]); + val _ = SS.try_to_prove_ornode_and_update_graph pst synched_agraph final_goal_key; + val solved = + if SS.final_goal_proved_completely synched_agraph: bool + then (*Proof by abduction is unnecessary.*) + let + val agraph = Synchronized.value synched_agraph; + val lemma_name2term = abduction_graph_to_string2term_table agraph: string2term_table; + val final_goal_name = lemma_name_of agraph (Or_N, [standardized_term]); + val _ = print_necessary_proofs_only pst agraph lemma_name2term final_goal_name; + in + true + end + else (*Proof by abduction is necessary.*) + let + val quintuple = (pst, synched_agraph, synched_refutation_table, synched_lemma_name_table, synched_proved_simps, ori_prems); + val _ = prove_standard_simp_rules quintuple standardized_term: unit; + val solved_in_loop = loop 0 max_depth start quintuple;(*expensive abduction!*) + val final_graph = Synchronized.value synched_agraph: Abduction_Graph.abduction_graph; + val lemma_name2term = abduction_graph_to_string2term_table final_graph: string2term_table; + val final_goal_name = lemma_name_of final_graph (Or_N, [standardized_term]): string; + val _ = if solved_in_loop + then print_necessary_proofs_only pst final_graph lemma_name2term final_goal_name + else "" + in + solved_in_loop + end; in solved end; diff --git a/Abduction/Shared_State.ML b/Abduction/Shared_State.ML index ecd36689..10173163 100644 --- a/Abduction/Shared_State.ML +++ b/Abduction/Shared_State.ML @@ -234,9 +234,9 @@ fun update_after_connecting_andnd_to_existing_ornd (ctxt:Proof.context) (sagraph 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; + 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