Skip to content

Commit

Permalink
Abduction: major bug fixed.
Browse files Browse the repository at this point in the history 
- one bug in PSL/Subtool.ML about timeout
- one bug in Abduction/Proof_By_Abduction about free variable names.
  • Loading branch information
@yutakang
yutakang committed Sep 24, 2023
1 parent 7f63c6d commit fd15f0a
Show file tree
Hide file tree
Showing 12 changed files with 90 additions and 57 deletions.
6 changes: 3 additions & 3 deletions Abduction/Abduction.thy
View file
Original file line number Diff line number Diff line change
Expand Up @@ -65,8 +65,8 @@ strategy Attack_On_Or_Node =
]

setup\<open> Config.put_global Top_Down_Util.timeout_config (60.0 * 60.0 * 10.0) \<close>
setup\<open> Config.put_global Top_Down_Util.limit_for_first_decrement 30 \<close>
setup\<open> Config.put_global Top_Down_Util.limit_for_other_decrement 10 \<close>
setup\<open> Config.put_global Top_Down_Util.limit_for_first_decrement 40 \<close>
setup\<open> Config.put_global Top_Down_Util.limit_for_other_decrement 15 \<close>

(* UI *)
ML\<open> (*This part (the definitions of long_keyword, long_statement, and short_statement) are from
Expand Down Expand Up @@ -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)]
Expand Down
2 changes: 1 addition & 1 deletion Abduction/Abstract_Same_Term.ML
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down
11 changes: 7 additions & 4 deletions Abduction/All_Top_Down_Conjecturing.ML
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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*)
Expand All @@ -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
Expand Down
2 changes: 1 addition & 1 deletion Abduction/Or_Node.ML
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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,
Expand Down
19 changes: 13 additions & 6 deletions Abduction/Proof_By_Abduction.ML
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand All @@ -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
Expand All @@ -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;
Expand Down Expand Up @@ -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.");
Expand Down
2 changes: 1 addition & 1 deletion Abduction/Remove_Function.ML
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down
38 changes: 19 additions & 19 deletions Abduction/Seed_Of_Or2And_Edge.ML
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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.*)
Expand Down Expand Up @@ -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;
Expand Down Expand Up @@ -214,15 +215,15 @@ 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
end;
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;
Expand All @@ -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
Expand Down Expand Up @@ -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
Expand Down
Loading

0 comments on commit fd15f0a

Please sign in to comment.