Skip to content

Commit

Permalink
Now, the AbductionProver can handle easy problems as well.
Browse files Browse the repository at this point in the history
  • Loading branch information
@yutakang
yutakang committed Nov 4, 2024
1 parent 482a0f7 commit 43bd4e2
Show file tree
Hide file tree
Showing 4 changed files with 32 additions and 47 deletions.
33 changes: 0 additions & 33 deletions Abduction/Abduction.thy
View file
Original file line number Diff line number Diff line change
Expand Up @@ -148,37 +148,4 @@ val _ = theorem \<^command_keyword>\<open>prove\<close> "prove";
end;
\<close>

ML\<open>
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;
\<close>

end
4 changes: 2 additions & 2 deletions Abduction/Abduction_Graph.ML
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
36 changes: 27 additions & 9 deletions Abduction/Proof_By_Abduction.ML
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down
6 changes: 3 additions & 3 deletions Abduction/Shared_State.ML
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down

0 comments on commit 43bd4e2

Please sign in to comment.