Theory IsaSAT_Simplify

theory IsaSAT_Simplify_Binaries imports IsaSAT_Setup Watched_Literals.Watched_Literals_Watch_List_Inprocessing More_Refinement_Libs.WB_More_Refinement_Loops IsaSAT_Simplify_Binaries_Defs IsaSAT_Simplify_Units IsaSAT_Restart begin section ‹Simplification of binary clauses› text ‹Special handling of binary clauses is required to avoid special cases of units in the general forward subsumption algorithm (which, as of writing, does not exist).› lemma all_atms_st_add_remove[simp]: ‹C ∈# dom_m N ⟹ all_atms_st (M, fmdrop C N, D, NE, UE, NEk, UEk, add_mset (mset (N ∝ C)) NS, US, N0, U0, Q, W) = all_atms_st (M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, Q, W)› ‹C ∈# dom_m N ⟹ all_atms_st (M, fmdrop C N, D, NE, UE, NEk, UEk, NS, add_mset (mset (N ∝ C)) US, N0, U0, Q, W) = all_atms_st (M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, Q, W)› ‹C ∈# dom_m N ⟹ all_atms_st (M, fmdrop C N, D, NE, UE, add_mset (mset (N ∝ C)) NEk, UEk, NS, US, N0, U0, Q, W) = all_atms_st (M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, Q, W)› ‹C ∈# dom_m N ⟹ all_atms_st (M, fmdrop C N, D, NE, UE, NEk, UEk, add_mset (mset (N ∝ C)) NS, US, N0, U0, Q, W) = all_atms_st (M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, Q, W)› ‹all_atms_st (L # M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, Q, W) = all_atms_st (M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, Q, W)› ‹all_atms_st (M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, add_mset K Q, W) = all_atms_st (M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, Q, W)› apply (auto simp: all_atms_st_def all_atms_def all_lits_def all_lits_of_mm_union all_lits_of_mm_add_mset distinct_mset_remove1_All dest!: multi_member_split simp del: all_atms_def[symmetric]) by (metis (no_types, lifting) Watched_Literals_Clauses.ran_m_fmdrop Watched_Literals_Clauses.ran_m_mapsto_upd all_lits_of_mm_add_mset fmupd_same image_mset_add_mset image_mset_union union_single_eq_member)+ lemma all_atms_st_add_kep[simp]: ‹L ∈# ℒ_a_l_l (all_atms_st (M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, Q, W)) ⟹ set_mset (all_atms_st (M, N, D, NE, UE, add_mset {#L#} NEk, UEk, NS, US, N0, U0, Q, W)) = set_mset (all_atms_st (M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, Q, W))› ‹L ∈# ℒ_a_l_l (all_atms_st (M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, Q, W)) ⟹ set_mset (all_atms_st (M, N, D, NE, UE, NEk, add_mset {#L#} UEk, NS, US, N0, U0, Q, W)) = set_mset (all_atms_st (M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, Q, W))› by (auto simp: all_atms_st_def in_ℒ_a_l_l_atm_of_𝒜_i_n all_atms_def all_lits_def all_lits_of_mm_union all_lits_of_mm_add_mset all_lits_of_m_add_mset simp del: all_atms_def[symmetric]) lemma clss_size_corr_in_dom_red_clss_size_lcount_ge0: ‹C ∈# dom_m N ⟹ ¬irred N C ⟹ clss_size_corr N NE UE NEk UEk NS US N0 U0 lcount ⟹ clss_size_lcount lcount ≥ Suc 0› apply (auto dest!: multi_member_split simp: clss_size_corr_def clss_size_def) by (metis member_add_mset red_in_dom_number_of_learned_ge1) abbreviation twl_st_heur_restart_ana'' :: ‹_› where ‹twl_st_heur_restart_ana'' r u ns lw ≡ {(S, T). (S, T) ∈ twl_st_heur_restart_ana r ∧ learned_clss_count S ≤ u ∧ get_vmtf_heur S = ns ∧ length (get_watched_wl_heur S) = lw}› lemma isa_clause_remove_duplicate_clause_wl_clause_remove_duplicate_clause_wl: ‹(uncurry isa_clause_remove_duplicate_clause_wl, uncurry clause_remove_duplicate_clause_wl) ∈ [λ(C, S). C ∈# dom_m (get_clauses_wl S)]_f nat_rel ×_ftwl_st_heur_restart_ana'' r u ns lw → ⟨twl_st_heur_restart_ana'' r u ns lw⟩nres_rel› proof - show ?thesis supply [[goals_limit=1]] unfolding isa_clause_remove_duplicate_clause_wl_def clause_remove_duplicate_clause_wl_def uncurry_def mop_arena_status_def nres_monad3 apply (intro frefI nres_relI) apply (refine_vcg log_del_clause_heur_log_clause[THEN order_trans]) apply (solves auto)[] apply (solves auto)[] apply (solves auto)[] subgoal for x y x1 x2 x1a x2a x1b x2b x1c x2c x1d x2d x1e x2e x1f x2f x1g x2g x1h x2h x1i x2i x1j x2j x1k a b c d e unfolding arena_is_valid_clause_vdom_def apply (rule exI[of _ ‹get_clauses_wl x2›], rule exI[of _ ‹set (get_vdom e)›]) by (simp add: twl_st_heur_restart_ana_def twl_st_heur_restart_def) subgoal for x y x1 x2 x1a x2a x1b x2b x1c x2c x1d x2d x1e x2e x1f x2f x1g x2g x1h x2h x1i x2i x1j x2j x1k a b c d e unfolding mark_garbage_pre_def arena_is_valid_clause_idx_def prod.simps apply (rule exI[of _ ‹get_clauses_wl x2›], rule exI[of _ ‹set (get_vdom e)›]) by (simp add: twl_st_heur_restart_ana_def twl_st_heur_restart_def) subgoal for x y x1 x2 x1a x2a x1b x2b x1c x2c x1d x2d x1e x2e x1f x2f x1g x2g x1h x2h x1i x2i x1j x2j x1k x2k x1l x2l x1m x2m by (auto simp: clause_remove_duplicate_clause_wl_pre_def clause_remove_duplicate_clause_pre_def state_wl_l_def red_in_dom_number_of_learned_ge1 twl_st_heur_restart_def twl_st_heur_restart_ana_def clss_size_corr_in_dom_red_clss_size_lcount_ge0 arena_lifting clss_size_corr_restart_def) subgoal by (auto simp: twl_st_heur_restart_def twl_st_heur_restart_ana_def valid_arena_extra_information_mark_to_delete' aivdom_inv_dec_remove_clause arena_lifting all_init_atms_fmdrop_add_mset_unit learned_clss_count_def dest!: in_vdom_m_fmdropD) done qed (*TODO Move*) lemma [simp]: ‹(S, x) ∈ state_wl_l None ⟹ defined_lit (get_trail_l x) L ⟷ defined_lit (get_trail_wl S) L› by (auto simp: state_wl_l_def) (*END Move*) lemma binary_clause_subres_wl_alt_def: ‹binary_clause_subres_wl C L L' = (λ(M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, Q, W). do { ASSERT (binary_clause_subres_lits_wl_pre C L L' (M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, Q, W)); ASSERT (L' ∈# ℒ_a_l_l (all_init_atms_st (M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, Q, W))); ASSERT (L ∈# ℒ_a_l_l (all_init_atms_st (M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, Q, W))); ASSERT (get_conflict_wl (M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, Q, W) = None ∧ undefined_lit M L ∧ C ∈# dom_m N); M' ← cons_trail_propagate_l L 0 M; ASSERT (M' = Propagated L 0 # M); let S = (M', fmdrop C N, D, NE, UE, (if irred N C then add_mset {#L#} else id) NEk, (if irred N C then id else add_mset {#L#}) UEk, (if irred N C then add_mset (mset (N ∝ C)) else id) NS, (if irred N C then id else add_mset (mset (N ∝ C))) US, N0, U0, add_mset (-L) Q, W); ASSERT (set_mset (all_init_atms_st (M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, Q, W)) = set_mset (all_init_atms_st S)); RETURN S })› (is ‹?A = ?B›) proof - have H: ‹binary_clause_subres_lits_wl_pre C L L' S ⟹ set_mset (all_atms_st S) = set_mset (all_init_atms_st S)› for S unfolding binary_clause_subres_lits_wl_pre_def binary_clause_subres_lits_pre_def apply normalize_goal+ using literals_are_ℒ_i_n'_literals_are_ℒ_i_n_iff(3) by fast have H: ‹binary_clause_subres_lits_wl_pre C L L' S ⟷ binary_clause_subres_lits_wl_pre C L L' S ∧ L' ∈# ℒ_a_l_l (all_init_atms_st S) ∧ L ∈# ℒ_a_l_l (all_init_atms_st S) ∧ undefined_lit (get_trail_wl S) L ∧ get_conflict_wl S = None ∧ C ∈# dom_m (get_clauses_wl S)› for S apply (rule iffI) apply simp_all apply (frule ℒ_a_l_l_cong[OF H, symmetric]) unfolding binary_clause_subres_lits_wl_pre_def binary_clause_subres_lits_pre_def binary_clause_subres_lits_pre_def apply normalize_goal+ apply (simp add: ) by (cases S; auto simp: all_atms_st_def ℒ_a_l_l_all_atms_all_lits all_lits_def ran_m_def all_lits_of_mm_add_mset all_lits_of_m_add_mset dest!: multi_member_split) have [simp]: ‹L ∈# all_init_lits x1a (x1c + x1e + x1g + x1i) ⟹ set_mset (all_init_atms x1a (add_mset {#L#} (x1c + x1e + x1g + x1i))) = set_mset (all_init_atms x1a ((x1c + x1e + x1g + x1i)))› for x1a x1c x1e x1g x1i by (auto simp: all_init_atms_def all_init_lits_def all_lits_of_mm_add_mset all_lits_of_m_add_mset simp del: all_init_atms_def[symmetric]) have ‹?A S ≤ ⇓Id (?B S)› for S unfolding binary_clause_subres_wl_def summarize_ASSERT_conv cons_trail_propagate_l_def nres_monad3 Let_def bind_to_let_conv apply (subst (2) H) by refine_vcg auto moreover have ‹?B S ≤ ⇓Id (?A S)› for S unfolding binary_clause_subres_wl_def summarize_ASSERT_conv cons_trail_propagate_l_def nres_monad3 Let_def bind_to_let_conv apply (subst (2) H) by refine_vcg (auto simp: all_init_atms_st_def all_init_atms_fmdrop_add_mset_unit ℒ_a_l_l_all_init_atms) ultimately show ?thesis unfolding Down_id_eq by (intro ext, rule antisym) qed lemma isa_binary_clause_subres_isa_binary_clause_subres_wl: ‹(uncurry3 isa_binary_clause_subres_wl, uncurry3 binary_clause_subres_wl) ∈ nat_rel ×_f nat_lit_lit_rel ×_f nat_lit_lit_rel ×_f twl_st_heur_restart_ana'' r u ns lw →_f ⟨twl_st_heur_restart_ana'' r u ns lw⟩nres_rel› proof - have A: ‹A ∈ twl_st_heur_restart_ana'' r u ns lw ⟹ A ∈ twl_st_heur_restart_ana'' r u ns lw› for A by auto note cong = trail_pol_cong option_lookup_clause_rel_cong map_fun_rel_D₀_cong isa_vmtf_cong phase_saving_cong cach_refinement_empty_cong' vdom_m_cong' vdom_m_cong'' isasat_input_bounded_cong[THEN iffD1] isasat_input_nempty_cong[THEN iffD1] heuristic_rel_cong empty_occs_list_cong' show ?thesis unfolding isa_binary_clause_subres_wl_def binary_clause_subres_wl_alt_def uncurry_def Let_def mop_arena_status_def nres_monad3 apply (intro frefI nres_relI) subgoal for S T apply (refine_vcg cons_trail_Propagated_tr[of ‹all_init_atms_st (snd T)›, THEN fref_to_Down_curry2]) subgoal unfolding isa_binary_clause_subres_lits_wl_pre_def twl_st_heur_restart_ana_def by force subgoal by auto subgoal by (auto simp: DECISION_REASON_def) subgoal by (auto simp: twl_st_heur_restart_ana_def twl_st_heur_restart_def all_init_atms_st_def) subgoal for x1 x1a x1b x2 x2a x2b x1c x2c x1d x2d x1e x2e x1f x2f x1g x2g x1h x2h x1i x2i x1j x2j x1k x2k x1l x2l x1m x2m x1n x2n x1o x1p x1q x2o x2p x2q M M' unfolding arena_is_valid_clause_vdom_def apply (rule exI[of _ ‹get_clauses_wl x2b›], rule exI[of _ ‹set (get_vdom x2q)›]) by (simp add: twl_st_heur_restart_ana_def twl_st_heur_restart_def) subgoal for x1 x1a x1b x2 x2a x2b x1c x2c x1d x2d x1e x2e x1f x2f x1g x2g x1h x2h x1i x2i x1j x2j x1k x2k x1l x2l x1m x2m x1n x2n x1o x1p x1q x2o x2p x2q M M' unfolding mark_garbage_pre_def arena_is_valid_clause_idx_def prod.simps by (rule exI[of _ ‹get_clauses_wl x2b›], rule exI[of _ ‹set (get_vdom x2q)›]) (simp add: twl_st_heur_restart_ana_def twl_st_heur_restart_def) subgoal H by (auto simp: clause_remove_duplicate_clause_wl_pre_def clause_remove_duplicate_clause_pre_def state_wl_l_def red_in_dom_number_of_learned_ge1 twl_st_heur_restart_def twl_st_heur_restart_ana_def clss_size_corr_in_dom_red_clss_size_lcount_ge0 arena_lifting clss_size_corr_restart_def) subgoal by (frule H; assumption?) (auto simp: learned_clss_count_def) apply (rule A) subgoal premises p using p apply (simp only: twl_st_heur_restart_alt_def2 Let_def twl_st_heur_restart_ana_def in_pair_collect_simp prod.simps prod_rel_fst_snd_iff get_trail_wl.simps fst_conv snd_conv) apply normalize_goal+ apply (drule cong[OF p(28)])+ apply (auto simp: twl_st_heur_restart_def twl_st_heur_restart_ana_def valid_arena_extra_information_mark_to_delete' aivdom_inv_dec_remove_clause arena_lifting isa_vmtf_consD all_init_atms_st_def dest!: in_vdom_m_fmdropD) apply (auto simp: twl_st_heur_restart_def twl_st_heur_restart_ana_def valid_arena_extra_information_mark_to_delete' aivdom_inv_dec_remove_clause arena_lifting isa_vmtf_consD clss_size_corr_restart_def clss_size_def learned_clss_count_def dest!: in_vdom_m_fmdropD) done done done qed lemma deduplicate_binary_clauses_inv_wl_strengthen_def: ‹deduplicate_binary_clauses_inv_wl S L (abort, i, a, T) ⟷ deduplicate_binary_clauses_inv_wl S L (abort, i, a, T) ∧ set_mset (all_init_atms_st T) = set_mset (all_init_atms_st S)› apply (rule iffI) subgoal apply (intro conjI) apply (solves simp) unfolding deduplicate_binary_clauses_inv_wl_def prod.simps deduplicate_binary_clauses_inv_def apply normalize_goal+ apply simp subgoal for xa xb xc apply - unfolding mem_Collect_eq prod.simps deduplicate_binary_clauses_inv_def using rtranclp_cdcl_twl_inprocessing_l_all_init_lits_of_l[of xa xb] rtranclp_cdcl_twl_inprocessing_l_all_learned_lits_of_l[of xa xb] by (auto simp add: ℒ_a_l_l_all_init_atms all_init_atms_st_alt_def) done subgoal by simp done lemma deduplicate_binary_clauses_inv_wl_strengthen_def2: ‹deduplicate_binary_clauses_inv_wl S L = (λ(abort, i, a, T). deduplicate_binary_clauses_inv_wl S L (abort, i, a, T) ∧ set_mset (all_init_atms_st T) = set_mset (all_init_atms_st S) ∧ set_mset (ℒ_a_l_l (all_init_atms_st T)) = set_mset (ℒ_a_l_l (all_init_atms_st S)))› apply (intro ext, clarsimp simp only:) apply (subst deduplicate_binary_clauses_inv_wl_strengthen_def) apply auto using ℒ_a_l_l_cong apply blast+ done definition mop_watched_by_at_init :: ‹'v twl_st_wl ⇒ 'v literal ⇒ nat ⇒ 'v watcher nres› where ‹mop_watched_by_at_init = (λS L w. do { ASSERT(L ∈# all_init_lits_of_wl S); ASSERT(w < length (watched_by S L)); RETURN (watched_by S L ! w) })› lemma mop_watched_by_app_heur_mop_watched_by_at_init_ana: ‹(uncurry2 mop_watched_by_app_heur, uncurry2 mop_watched_by_at_init) ∈ twl_st_heur_restart_ana u ×_f nat_lit_lit_rel ×_f nat_rel →_f ⟨Id⟩nres_rel› unfolding mop_watched_by_app_heur_def mop_watched_by_at_init_def uncurry_def all_lits_def[symmetric] all_lits_alt_def[symmetric] twl_st_heur_restart_ana_def twl_st_heur_restart_alt_def2 Let_def by (intro frefI nres_relI, refine_rcg) (simp_all add: map_fun_rel_def ℒ_a_l_l_all_init_atms(2) watched_by_alt_def) lemma deduplicate_binary_clauses_wl_alt_def: ‹deduplicate_binary_clauses_wl L S = do { ASSERT (deduplicate_binary_clauses_pre_wl L S); ASSERT (L ∈# ℒ_a_l_l (all_init_atms_st S)); let CS = (λ_::nat literal. None); let l = length (watched_by S L); let val = polarity (get_trail_wl S) L; (_, _, _, S) ← WHILE_T⇗deduplicate_binary_clauses_inv_wl S L⇖ (λ(abort, i, CS, S). ¬abort ∧ i < l ∧ get_conflict_wl S = None) (λ(abort, i, CS, S). do { (C,L', b) ← mop_watched_by_at_init S L i; ASSERT (L' ∈# ℒ_a_l_l (all_init_atms_st S)); let st = C ∈# dom_m (get_clauses_wl S); if ¬st ∨ ¬b then RETURN (abort, i+1, CS, S) else do { let _ = polarity (get_trail_wl S) L'; if defined_lit (get_trail_wl S) L' then do { U ← simplify_clause_with_unit_st_wl C S; ASSERT (set_mset (all_init_atms_st U) = set_mset (all_init_atms_st S)); ASSERT (L ∈# ℒ_a_l_l (all_init_atms_st U)); let _ = polarity (get_trail_wl U) L; RETURN (defined_lit (get_trail_wl U) L, i+1, CS, U) } else do { let c = CS L'; let _ = CS L'; if c ≠ None then do { let C' = (if ¬snd (the c) ⟶ ¬irred (get_clauses_wl S) C then C else fst (the c)); let CS = (if ¬snd (the c) ⟶ ¬irred (get_clauses_wl S) C then CS else CS (L' := Some (C, irred (get_clauses_wl S) C))); ASSERT (C' ∈# dom_m (get_clauses_wl S)); S ← clause_remove_duplicate_clause_wl C' S; RETURN (abort, i+1, CS, S) } else do { let c = CS (-L'); if CS (-L') ≠ None then do { S ← binary_clause_subres_wl C L (-L') S; RETURN (True, i+1, CS, S) } else do { let CS' = CS (L' := Some (C, irred (get_clauses_wl S) C)); RETURN (abort, i+1, CS', S) } } } } }) (defined_lit (get_trail_wl S) L, 0, CS, S); let CS = (λ_::nat literal. None); RETURN S }› (is ‹?A = ?B›) proof - have H: ‹a = b ⟹ (a, b) ∈ Id› ‹x =y ⟹ x ≤ ⇓Id y› for a b x y by auto have ‹?A ≤ ⇓ Id ?B› supply [[goals_limit=1]] unfolding Let_def deduplicate_binary_clauses_wl_def bind_to_let_conv mop_watched_by_at_init_def nres_monad3 by (refine_vcg H(1); (rule H refl)?; simp) moreover have ‹?B ≤ ⇓Id ?A› unfolding Let_def deduplicate_binary_clauses_wl_def bind_to_let_conv mop_watched_by_at_init_def nres_monad3 apply (refine_vcg H(1); (rule H)?) subgoal unfolding deduplicate_binary_clauses_pre_wl_def deduplicate_binary_clauses_pre_def apply normalize_goal+ by (simp add: ℒ_a_l_l_all_init_atms_all_init_lits all_init_lits_of_wl_def all_init_lits_def IsaSAT_Setup.get_unit_init_clss_wl_alt_def ac_simps ℒ_a_l_l_all_init_atms) subgoal by auto subgoal by auto subgoal by auto subgoal for x x' x1 x2 x1a x2a x1b x2b x1c x2c x1d x2d x1e x2e x1f x2f x1g x2g x1h x2h x1i x2i apply (subst (asm) deduplicate_binary_clauses_inv_wl_def) unfolding deduplicate_binary_clauses_inv_alt_def case_prod_beta apply normalize_goal+ apply simp subgoal for xa xb xc xd apply - unfolding mem_Collect_eq prod.simps apply normalize_goal+ using rtranclp_cdcl_twl_inprocessing_l_all_init_lits_of_l[of xa xb] rtranclp_cdcl_twl_inprocessing_l_all_learned_lits_of_l[of xa xb] by (simp add: ℒ_a_l_l_all_init_atms(2) literals_are_ℒ_i_n'_literals_are_ℒ_i_n_iff(4)) done subgoal for x x' x1 x2 x1a x2a x1b x2b x1c x2c x1d x2d x1e x2e x1f x2f x1g x2g x1h x2h x1i x2i apply (subst (asm) deduplicate_binary_clauses_inv_wl_def) unfolding deduplicate_binary_clauses_inv_alt_def case_prod_beta apply normalize_goal+ apply simp subgoal for xa xb xc xd apply - unfolding mem_Collect_eq prod.simps apply normalize_goal+ using rtranclp_cdcl_twl_inprocessing_l_all_init_lits_of_l[of xa xb] rtranclp_cdcl_twl_inprocessing_l_all_learned_lits_of_l[of xa xb] by (auto simp add: literals_are_ℒ_i_n'_def blits_in_ℒ_i_n'_def watched_by_alt_def ℒ_a_l_l_all_init_atms dest!: multi_member_split nth_mem) done subgoal for x x' x1 x2 x1a x2a x1b x2b x1c x2c x1d x2d x1e x2e x1f x2f x1g x2g x1h x2h x1i x2i apply (subst (asm) deduplicate_binary_clauses_inv_wl_def) unfolding deduplicate_binary_clauses_inv_alt_def case_prod_beta apply normalize_goal+ apply simp subgoal for xa xb xc xd apply - unfolding mem_Collect_eq prod.simps apply normalize_goal+ using rtranclp_cdcl_twl_inprocessing_l_all_init_lits_of_l[of xa xb] rtranclp_cdcl_twl_inprocessing_l_all_learned_lits_of_l[of xa xb] by (auto simp add: literals_are_ℒ_i_n'_def blits_in_ℒ_i_n'_def watched_by_alt_def ℒ_a_l_l_all_init_atms dest!: multi_member_split nth_mem) done subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal apply (subst (asm) deduplicate_binary_clauses_inv_wl_strengthen_def2) apply (clarsimp dest!: ) apply (drule ℒ_a_l_l_cong) by presburger subgoal by auto subgoal by auto subgoal unfolding case_prod_beta deduplicate_binary_clauses_inv_wl_def deduplicate_binary_clauses_inv_def deduplicate_binary_clauses_correctly_marked_def by normalize_goal+ (auto split: if_splits) subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto done ultimately show ?thesis unfolding Down_id_eq by (rule antisym) qed lemma deduplicate_binary_clauses_pre_wl_in_all_atmsD: ‹deduplicate_binary_clauses_pre_wl L S ⟹ L ∈# ℒ_a_l_l (all_init_atms_st S)› ‹deduplicate_binary_clauses_pre_wl L S ⟹ L ∈# ℒ_a_l_l (all_atms_st S)› proof - assume ‹deduplicate_binary_clauses_pre_wl L S› then show ‹L ∈# ℒ_a_l_l (all_init_atms_st S)› unfolding deduplicate_binary_clauses_pre_wl_def deduplicate_binary_clauses_pre_def apply - apply normalize_goal+ by (simp add: ℒ_a_l_l_all_init_atms_all_init_lits all_init_lits_of_wl_def all_init_lits_def IsaSAT_Setup.get_unit_init_clss_wl_alt_def ac_simps ℒ_a_l_l_all_init_atms) then show ‹L ∈# ℒ_a_l_l (all_atms_st S)› using ℒ_a_l_l_init_all by blast qed lemma isa_deduplicate_binary_clauses_mark_duplicated_binary_clauses_as_garbage_wl: assumes ‹(S, S') ∈ twl_st_heur_restart_ana'' r u ns lw› ‹(L,L')∈ nat_lit_lit_rel› and ‹(CS, Map.empty) ∈ {((c, m), c'). c = c' ∧ m = (length (get_watched_wl_heur S))}› (is ‹_ ∈ ?CS›) shows ‹isa_deduplicate_binary_clauses_wl L CS S ≤ ⇓{((CS, T), T'). (T,T') ∈ twl_st_heur_restart_ana'' r u ns lw ∧ (CS, Map.empty) ∈ {((c, m), c'). c = c' ∧ m = (length (get_watched_wl_heur S))}} (deduplicate_binary_clauses_wl L' S')› proof - have [simp]: ‹L' = L› using assms by auto have [simp]: ‹all_init_atms (get_clauses_wl S') (IsaSAT_Setup.get_unkept_unit_init_clss_wl S' + IsaSAT_Setup.get_kept_unit_init_clss_wl S' + get_subsumed_init_clauses_wl S' + get_init_clauses0_wl S') = all_init_atms_st S'› by (auto simp: all_init_atms_st_def IsaSAT_Setup.get_unit_init_clss_wl_alt_def) have [refine0]: ‹(CS, Map.empty) ∈?CS ⟹ (val, polarity (get_trail_wl S') L') ∈ ⟨bool_rel⟩option_rel ⟹ deduplicate_binary_clauses_inv_wl S' L' (defined_lit (get_trail_wl S') L', 0, Map.empty, S') ⟹ ((val ≠ UNSET, 0, CS, S), defined_lit (get_trail_wl S') L', 0, Map.empty, S') ∈ bool_rel ×_r nat_rel ×_r ?CS ×_r ({(a, b). (a,b)∈ twl_st_heur_restart_ana'' r u ns lw ∧ learned_clss_count a ≤ learned_clss_count S})› (is ‹_ ⟹ _ ⟹ _⟹ _ ∈ ?loop›) for CS val using assms by (auto simp: polarity_def) have [refine0]: ‹isa_simplify_clause_with_unit_st2 C S ≤ ⇓ {(a, b). (a, b) ∈ twl_st_heur_restart ∧ get_avdom a = get_avdom S ∧ get_vdom a = get_vdom S ∧ get_ivdom a = get_ivdom S ∧ length (get_clauses_wl_heur a) = r ∧ learned_clss_count a ≤ u ∧ learned_clss_count a ≤ learned_clss_count S ∧ get_vmtf_heur a = get_vmtf_heur S ∧ length (get_watched_wl_heur a) = lw} (simplify_clause_with_unit_st_wl C' T)› if ‹(S,T) ∈ {(a, b). (a, b) ∈ twl_st_heur_restart ∧ get_avdom a = get_avdom S ∧ get_vdom a = get_vdom S ∧ get_ivdom a = get_ivdom S ∧ length (get_clauses_wl_heur a) = r ∧ learned_clss_count a ≤ u ∧ get_vmtf_heur a = get_vmtf_heur S ∧ length (get_watched_wl_heur a) = lw}› ‹(C,C') ∈ Id› for S T C C' apply (rule isa_simplify_clause_with_unit_st2_simplify_clause_with_unit_st2[THEN order_trans]) apply (rule that) apply (rule that) apply (rule ref_two_step'') defer apply (rule simplify_clause_with_unit_st2_simplify_clause_with_unit_st[THEN order_trans, of _ C' T T]) apply auto done have [simp]: ‹(Sa, U) ∈ twl_st_heur_restart_ana (length (get_clauses_wl_heur Sa)) ⟷ (Sa, U) ∈ twl_st_heur_restart› for Sa U by (auto simp: twl_st_heur_restart_ana_def) have KK: ‹set_mset (ℒ_a_l_l (all_init_atms_st T)) = set_mset (ℒ_a_l_l (all_init_atms_st S')) ⟷ set_mset ((all_init_atms_st T)) = set_mset ((all_init_atms_st S'))› for S' T apply (auto simp: ℒ_a_l_l_all_init_atms(2)) apply (metis ℒ_a_l_l_all_init_atms(2) atms_of_ℒ_a_l_l_𝒜_i_n atms_of_cong_set_mset) apply (metis ℒ_a_l_l_all_init_atms(2) atms_of_ℒ_a_l_l_𝒜_i_n atms_of_cong_set_mset) apply (metis ℒ_a_l_l_all_init_atms(2) ℒ_a_l_l_cong)+ done have get_watched_wl_heur: ‹mop_watched_by_app_heur x2e L x1d ≤ ⇓ {(a,b). a = b ∧ a = get_watched_wl_heur x2e ! nat_of_lit L ! x1d ∧ b = watched_by x2b L' ! x1a ∧ fst a ∈ set (get_vdom x2e)} (mop_watched_by_at_init x2b L' x1a)› (is ‹_ ≤⇓ ?watched _›) if ‹(S, S') ∈ twl_st_heur_restart_ana'' r u ns lw› and ‹(L, L') ∈ nat_lit_lit_rel› and ‹deduplicate_binary_clauses_pre_wl L' S'› and ‹L' ∈# ℒ_a_l_l (all_init_atms_st S')› and ‹(CS, Map.empty) ∈ {((c, m), c'). c = c' ∧ m = length (get_watched_wl_heur S)}› and ‹polarity_pol_pre (get_trail_wl_heur S) L› and ‹inres (RETURN (polarity_pol (get_trail_wl_heur S) L)) val› and ‹(val, polarity (get_trail_wl S') L') ∈ ⟨bool_rel⟩option_rel› and ‹(x, x') ∈ ?loop› and ‹case x of (abort, i, CS, Sa) ⇒ ¬ abort ∧ i < l ∧ get_conflict_wl_is_None_heur Sa› and ‹case x' of (abort, i, CS, S) ⇒ ¬ abort ∧ i < length (watched_by S' L') ∧ get_conflict_wl S = None› and ‹case x' of (abort, i, a, T) ⇒ deduplicate_binary_clauses_inv_wl S' L' (abort, i, a, T) ∧ set_mset (all_init_atms_st T) = set_mset (all_init_atms_st S') ∧ set_mset (ℒ_a_l_l (all_init_atms_st T)) = set_mset (ℒ_a_l_l (all_init_atms_st S'))› and ‹x2a = (x1b, x2b)› and ‹x2 = (x1a, x2a)› and ‹x' = (x1, x2)› and ‹x2d = (x1e, x2e)› and ‹x2c = (x1d, x2d)› and ‹x = (x1c, x2c)› and ‹(l, length (watched_by S' L')) ∈ {(l, l'). (l, l') ∈ nat_rel ∧ l' = length (watched_by S' L')}› for CS val x x' x1 x2 x1a x2a x1b x2b x1c x2c x1d x2d x1e x2e l proof - show ?thesis apply (rule order_trans) apply (rule mop_watched_by_app_heur_mop_watched_by_at_init_ana[of r, THEN fref_to_Down_curry2, of _ _ _ x2b L' x1a]) subgoal by fast subgoal using that by auto unfolding Down_id_eq mop_watched_by_at_init_def apply (refine_rcg) using that twl_st_heur_restart_ana_watchlist_in_vdom[where L=L and x2e=x2e and x2f=x2b and x1d = x1d and a=‹fst (get_watched_wl_heur x2e ! nat_of_lit L ! x1d)› and b=‹snd(get_watched_wl_heur x2e ! nat_of_lit L ! x1d)› and r=r] by (auto simp: twl_st_heur_restart_ana_state_simp watched_by_alt_def deduplicate_binary_clauses_inv_wl_def mop_watched_by_at_init_def) qed have watched_in_vdom: ‹x1h ∈ set (get_vdom x2e)› ‹(x1h, x1f) ∈ nat_rel› if ‹(xa, x'a) ∈ ?watched x1d x1a x2b x2e› ‹x'a = (x1f, x2f)› ‹x2f = (x3f, x3f')› ‹xa = (x1h, x2h)› ‹x2h = (x3h, x3h')› for x2e xa x'a x1h x2h x1f x2f x1d x1a x2b x3f x3f' x3h x3h' using that by auto have irred_status: ‹¬ (x1f ∉# dom_m (get_clauses_wl x2b) ∨ ¬ x2g) ⟹ (xb, x1f ∈# dom_m (get_clauses_wl x2b)) ∈ {(a, b). (a ≠ DELETED) = b ∧ (a = IRRED) = (irred (get_clauses_wl x2b) x1f ∧ b) ∧ (a = LEARNED) = (¬ irred (get_clauses_wl x2b) x1f ∧ b)} ⟹ (xb, irred (get_clauses_wl x2b) x1f) ∈ {(a,b). a ≠ DELETED ∧ ((a=IRRED) ⟷ b) ∧ ((a=LEARNED) ⟷ ¬b)}› for xb x2b x1f x2g by (cases xb) auto have twl_st_heur_restart_ana_stateD: ‹valid_arena (get_clauses_wl_heur x2e) (get_clauses_wl x2b) (set (get_vdom x2e))› if ‹(x2e, x2b) ∈ twl_st_heur_restart_ana r› for x2e x2b using that unfolding twl_st_heur_restart_ana_def twl_st_heur_restart_def by simp have is_markedI: ‹(x1e, x1e') ∈ ?CS ⟹ (x1i, x1i') ∈ nat_lit_lit_rel ⟹ x1i' ∈# ℒ_a_l_l (all_init_atms_st S') ⟹ is_marked x1e x1i ≤ SPEC (λc. (c, x1e' x1i') ∈ {(a,b). a ⟷ b≠None})› ‹(x1e, x1e') ∈ ?CS ⟹ (x1i, x1i') ∈ nat_lit_lit_rel ⟹ (m, x1e' x1i') ∈ {(a,b). a ⟷ b≠None} ⟹x1i' ∈# ℒ_a_l_l (all_init_atms_st S') ⟹ (if m then get_marked x1e x1i else RETURN (1, True)) ≤ SPEC (λc. (c, x1e' x1i') ∈ {(a,b). b ≠ None ⟶ a = the b})› ‹(x1e, x1e') ∈ ?CS ⟹ (x1i, x1i') ∈ nat_lit_lit_rel ⟹ x1i' ∈# ℒ_a_l_l (all_init_atms_st S') ⟹ (x, x') ∈ Id ⟹ (m, x1e' x1i') ∈ {(a,b). a ⟷ b≠None} ⟹ ¬m ⟹ set_marked x1e x1i x ≤ SPEC (λc. (c, x1e'(x1i' ↦ x')) ∈ ?CS)› for x1e x1e' x1i x1i' m x x' using assms(1) unfolding is_marked_def get_marked_def set_marked_def by (auto intro!: ASSERT_leI simp: twl_st_heur_restart_ana_def twl_st_heur_restart_def map_fun_rel_def) have length_watchlist: ‹(S, S') ∈ twl_st_heur_restart_ana'' r u ns lw ⟹ (L, L') ∈ nat_lit_lit_rel ⟹ L' ∈# ℒ_a_l_l (all_init_atms_st S') ⟹ mop_length_watched_by_int S L ≤ SPEC (λc. (c, length (watched_by S' L')) ∈ {(l,l'). (l,l') ∈ nat_rel ∧ l' = length (watched_by S' L')})› by (auto simp: mop_length_watched_by_int_def twl_st_heur_restart_ana_def twl_st_heur_restart_def map_fun_rel_def watched_by_alt_def intro!: ASSERT_leI) have [refine0]: ‹(CS, a) ∈ ?CS ⟹ empty CS ≤ SPEC (λu. (u, Map.empty) ∈ ?CS)› for a CS by (auto simp: empty_def) have update_marked: ‹(if ¬ snd n ⟶ st = LEARNED then RETURN x1e else update_marked x1e x1i (x1h, st = IRRED)) ≤ SPEC (λc. (c, if ¬ snd (the (x1b x1g)) ⟶ ¬ irred (get_clauses_wl x2b) x1f then x1b else x1b(x1g ↦ (x1f, irred (get_clauses_wl x2b) x1f))) ∈ ?CS)› if loop: ‹(x, x') ∈ ?loop› and ‹case x' of (abort, i, a, T) ⇒ deduplicate_binary_clauses_inv_wl S' L' (abort, i, a, T) ∧ set_mset (all_init_atms_st T) = set_mset (all_init_atms_st S') ∧ set_mset (ℒ_a_l_l (all_init_atms_st T)) = set_mset (ℒ_a_l_l (all_init_atms_st S'))› and st: ‹x2a = (x1b, x2b)› ‹x2 = (x1a, x2a)› ‹x' = (x1, x2)› ‹x2d = (x1e, x2e)› ‹x2c = (x1d, x2d)› ‹x = (x1c, x2c)› ‹x2f = (x1g, x2g)› ‹x'a = (x1f, x2f)› ‹x2h = (x1i, x2i)› ‹xa = (x1h, x2h)› and ‹x1d < l› and ‹(xa, x'a) ∈ {(a, b). a = b ∧ a = get_watched_wl_heur x2e ! nat_of_lit L ! x1d ∧ b = watched_by x2b L' ! x1a ∧ fst a ∈ set (get_vdom x2e)}› and ‹x1g ∈# ℒ_a_l_l (all_init_atms_st x2b)› and ‹0 < x1h ∧ x1h < length (get_clauses_wl_heur x2e)› and ‹(st, x1f ∈# dom_m (get_clauses_wl x2b)) ∈ {(a, b). (a ≠ DELETED) = b ∧ (a = IRRED) = (irred (get_clauses_wl x2b) x1f ∧ b) ∧ (a = LEARNED) = (¬ irred (get_clauses_wl x2b) x1f ∧ b)}› and ‹¬ (st = DELETED ∨ ¬ x2i)› and ‹¬ (x1f ∉# dom_m (get_clauses_wl x2b) ∨ ¬ x2g)› and m: ‹(m, x1b x1g) ∈ {a. case a of (a, b) ⇒ a = (b ≠ None)}› m and ‹(n, x1b x1g) ∈ {a. case a of (a, b) ⇒ b ≠ None ⟶ a = the b}› and ‹x1b x1g ≠ None› for l val x x' x1 x2 x1a x2a x1b x2b x1c x2c x1d x2d x1e x2e xa x'a x1f x2f x1g x2g x1h x2h x1i x2i st vala m n proof - have ‹(get_watched_wl_heur S, get_watched_wl S') ∈ ⟨Id⟩map_fun_rel (D₀ (all_init_atms_st S'))› using assms by (auto intro!: ASSERT_leI simp: st twl_st_heur_restart_def twl_st_heur_restart_ana_def) then show ?thesis using that unfolding update_marked_def by (auto intro!: ASSERT_leI simp: st map_fun_rel_def) qed show ?thesis supply [[goals_limit=1]] using assms unfolding isa_deduplicate_binary_clauses_wl_def deduplicate_binary_clauses_wl_alt_def mop_polarity_pol_def nres_monad3 apply - apply (subst deduplicate_binary_clauses_wl_alt_def) apply (subst deduplicate_binary_clauses_inv_wl_strengthen_def2) apply (refine_rcg polarity_pol_polarity[of ‹all_init_atms_st S'›, THEN fref_to_Down_unRET_uncurry] mop_arena_status_vdom isa_clause_remove_duplicate_clause_wl_clause_remove_duplicate_clause_wl[of r ‹learned_clss_count S› ns lw for S, THEN fref_to_Down_curry, of _ _ _ S S for S] isa_binary_clause_subres_isa_binary_clause_subres_wl[of r ‹learned_clss_count S› ns lw for S, THEN fref_to_Down_curry3, of _ _ _ S _ _ _ _ S for S] length_watchlist) subgoal using length_watched_le_ana[of S' S ‹length (get_clauses_wl_heur S)› L] by (auto simp add: deduplicate_binary_clauses_pre_wl_def watched_by_alt_def deduplicate_binary_clauses_pre_wl_in_all_atmsD ℒ_a_l_l_all_init_atms(2) twl_st_heur_restart_ana_state_simp twl_st_heur_restart_ana_def) subgoal by (rule polarity_pol_pre) (use assms in ‹auto simp: twl_st_heur_restart_ana_def twl_st_heur_restart_def›)[2] subgoal by auto subgoal by (use assms in ‹auto simp: twl_st_heur_restart_ana_def twl_st_heur_restart_def›) subgoal by auto subgoal for CS val by (auto simp: watched_by_alt_def deduplicate_binary_clauses_pre_wl_in_all_atmsD get_conflict_wl_is_None_def twl_st_heur_restart_ana_state_simp get_conflict_wl_is_None_heur_get_conflict_wl_is_None_ana[THEN fref_to_Down_unRET_Id]) subgoal by auto subgoal by (auto simp: twl_st_heur_restart_ana_def) subgoal using assms by (auto simp: twl_st_heur_restart_ana_def) apply (rule get_watched_wl_heur; assumption) subgoal by (auto simp: twl_st_heur_restart_ana_def twl_st_heur_restart_def) (metis (no_types, lifting) arena_dom_status_iff(3) bot_nat_0.extremum gr0I le_antisym numeral_le_iff semiring_norm(69))+ subgoal by (auto simp: twl_st_heur_restart_ana_def twl_st_heur_restart_def intro!: valid_arena_in_vdom_le_arena) apply (solves auto) subgoal for CS val x x' x1 x2 x1a x2a x1b x2b x1c x2c x1d x2d x1e x2e by auto subgoal by (auto simp: twl_st_heur_restart_ana_def twl_st_heur_restart_def) subgoal by auto subgoal by (simp add: deduplicate_binary_clauses_pre_wl_in_all_atmsD ℒ_a_l_l_all_init_atms(2)) subgoal apply (rule polarity_pol_pre) apply (use assms in ‹auto simp: twl_st_heur_restart_ana_def twl_st_heur_restart_alt_def2 Let_def›)[] apply (clarsimp simp add: watched_by_alt_def twl_st_heur_restart_ana_state_simp) done subgoal by auto subgoal unfolding prod_rel_iff apply (intro conjI impI) subgoal unfolding twl_st_heur_restart_alt_def2 twl_st_heur_restart_ana_def Let_def KK prod.simps apply (simp only: in_pair_collect_simp prod_rel_iff prod.simps) apply normalize_goal+ apply (rule trail_pol_cong, assumption, assumption) done subgoal by (clarsimp simp: watched_by_alt_def twl_st_heur_restart_ana_state_simp dest: trail_pol_cong) done subgoal by (auto simp: polarity_def) subgoal by (auto simp: twl_st_heur_restart_ana_def) subgoal by (clarsimp simp add: watched_by_alt_def twl_st_heur_restart_ana_state_simp) subgoal apply (rule polarity_pol_pre) apply (use assms in ‹auto simp: twl_st_heur_restart_ana_def twl_st_heur_restart_alt_def2 Let_def›)[] apply (clarsimp simp add: watched_by_alt_def twl_st_heur_restart_ana_state_simp) done subgoal by (clarsimp simp add: twl_st_heur_restart_ana_def) subgoal unfolding twl_st_heur_restart_alt_def2 twl_st_heur_restart_ana_def Let_def KK prod.simps apply (simp only: in_pair_collect_simp prod_rel_iff prod.simps) apply normalize_goal+ by (metis (no_types, lifting) trail_pol_cong) subgoal by (auto simp: twl_st_heur_restart_ana_state_simp polarity_def) apply (rule is_markedI) subgoal by simp subgoal by simp subgoal by simp apply (rule is_markedI) subgoal by simp subgoal by simp subgoal by simp subgoal by simp subgoal by auto apply (rule update_marked; assumption) subgoal by (auto split: if_splits) subgoal by simp subgoal by simp apply (rule is_markedI) subgoal by simp subgoal by simp subgoal by (simp add: uminus_𝒜_i_n_iff) subgoal by simp subgoal by simp subgoal by simp subgoal by simp apply (rule is_markedI) subgoal by simp subgoal by simp subgoal by (simp add: uminus_𝒜_i_n_iff) subgoal by simp apply assumption subgoal by auto apply (solves auto) apply (solves auto) subgoal by auto done qed lemma lambda_split_second: ‹(λ(a, x). f a x) = (λ(a,b,c:: isasat). f a (b,c))› by (auto intro!: ext) lemma isa_mark_duplicated_binary_clauses_as_garbage_wl_alt_def: ‹isa_mark_duplicated_binary_clauses_as_garbage_wl S₀ = do { ASSERT (mark_duplicated_binary_clauses_as_garbage_pre_wl_heur S₀); let skip = should_eliminate_pure_st S₀; CS ← create (length (get_watched_wl_heur S₀)); (CS, S) ← iterate_over_VMTFC (λA (CS, S). do {ASSERT (get_vmtf_heur_array S₀ = (get_vmtf_heur_array S)); skip_lit ← mop_is_marked_added_heur_st S A; if ¬skip then RETURN (CS, S) else do { ASSERT (length (get_clauses_wl_heur S) ≤ length (get_clauses_wl_heur S₀) ∧ learned_clss_count S ≤ learned_clss_count S₀); (CS, S) ← isa_deduplicate_binary_clauses_wl (Pos A) CS S; ASSERT (length (get_clauses_wl_heur S) ≤ length (get_clauses_wl_heur S₀) ∧ learned_clss_count S ≤ learned_clss_count S₀); (CS, S) ← isa_deduplicate_binary_clauses_wl (Neg A) CS S; ASSERT (get_vmtf_heur_array S₀ = (get_vmtf_heur_array S)); RETURN (CS, S) }}) (λ(CS, S). get_vmtf_heur_array S₀ = (get_vmtf_heur_array S)) (λ(CS, S). get_conflict_wl_is_None_heur S) (get_vmtf_heur_array S₀, Some (get_vmtf_heur_fst S₀)) (CS, S₀); RETURN S }› unfolding iterate_over_VMTFC_def prod.simps nres_monad3 Let_def apply (rewrite at ‹WHILE_T⇗_⇖ _ ⌑› lambda_split_second) unfolding isa_mark_duplicated_binary_clauses_as_garbage_wl_def apply (rewrite at ‹WHILE_T⇗_⇖ _ ⌑ _› lambda_split_second) apply (auto intro!: bind_cong simp: Let_def) done definition mark_duplicated_binary_clauses_as_garbage_wl2 :: ‹_ ⇒ 'v twl_st_wl nres› where ‹mark_duplicated_binary_clauses_as_garbage_wl2 S = do { ASSERT (mark_duplicated_binary_clauses_as_garbage_pre_wl S); Ls ← SPEC (λLs:: 'v multiset. set_mset Ls = set_mset (atm_of `# all_init_lits_of_wl S) ∧ distinct_mset Ls); (_, S) ← WHILE_T⇗λ(L, T). mark_duplicated_binary_clauses_as_garbage_wl_inv Ls S (T, L)⇖(λ(Ls, S). Ls ≠ {#} ∧ get_conflict_wl S = None) (λ(Ls, S). do { ASSERT (Ls ≠ {#}); L ← SPEC (λL. L ∈# Ls); ASSERT (L ∈# atm_of `# all_init_lits_of_wl S); skip ← RES (UNIV :: bool set); if skip then RETURN (remove1_mset L Ls, S) else do { S ← deduplicate_binary_clauses_wl (Pos L) S; S ← deduplicate_binary_clauses_wl (Neg L) S; RETURN (remove1_mset L Ls, S) } }) (Ls, S); RETURN S }› lemma mark_duplicated_binary_clauses_as_garbage_wl2_alt_def: ‹mark_duplicated_binary_clauses_as_garbage_wl2 S = do { ASSERT (mark_duplicated_binary_clauses_as_garbage_pre_wl S); Ls ← SPEC (λLs:: 'v multiset. set_mset Ls = set_mset (atm_of `# all_init_lits_of_wl S) ∧ distinct_mset Ls); (_, S) ← WHILE_T⇗λ(L, T). mark_duplicated_binary_clauses_as_garbage_wl_inv Ls S (T, L)⇖(λ(Ls, S). Ls ≠ {#} ∧ get_conflict_wl S = None) (λ(Ls, S). do { ASSERT (Ls ≠ {#}); L ← SPEC (λL. L ∈# Ls); S ← do { ASSERT (L ∈# atm_of `# all_init_lits_of_wl S); skip ← RES (UNIV :: bool set); if skip then RETURN (S) else do { S ← deduplicate_binary_clauses_wl (Pos L) S; S ← deduplicate_binary_clauses_wl (Neg L) S; RETURN (S) } }; RETURN (remove1_mset L Ls, S) }) (Ls, S); RETURN S }› unfolding nres_monad_laws mark_duplicated_binary_clauses_as_garbage_wl2_def bind_to_let_conv Let_def apply (auto intro!: bind_cong[OF refl] simp: bind_to_let_conv) apply (subst bind_to_let_conv Let_def)+ apply (auto simp: Let_def nres_monad_laws intro!: bind_cong) apply (subst nres_monad_laws)+ apply auto done lemma mark_duplicated_binary_clauses_as_garbage_wl2_ge_ℒ_a_l_l: ‹⇓ Id (mark_duplicated_binary_clauses_as_garbage_wl2 S) ≥ do { ASSERT (mark_duplicated_binary_clauses_as_garbage_pre_wl S); iterate_over_ℒ_a_l_lC (λL S. do { ASSERT (L ∈# atm_of `# all_init_lits_of_wl S); skip ← RES (UNIV :: bool set); if skip then RETURN (S) else do { S ← deduplicate_binary_clauses_wl (Pos L) S; S ← deduplicate_binary_clauses_wl (Neg L) S; RETURN (S) } }) (atm_of `# all_init_lits_of_wl S) (λ𝒜 T. mark_duplicated_binary_clauses_as_garbage_wl_inv (all_init_atms_st S) S (T, 𝒜)) (λS. get_conflict_wl S = None) S}› proof - have H: ‹a=b ⟹ (a,b) ∈ Id› for a b by auto have H': ‹a=b ⟹ a ≤⇓Id b› for a b by auto have HH: ‹mark_duplicated_binary_clauses_as_garbage_wl_inv Ls S (x2, x1) ⟹ set_mset Ls = set_mset (all_init_atms_st S) ⟹ distinct_mset Ls ⟹ mark_duplicated_binary_clauses_as_garbage_wl_inv (all_init_atms_st S) S (x2, x1)› for Ls x2 x1 unfolding mark_duplicated_binary_clauses_as_garbage_wl_inv_def mark_duplicated_binary_clauses_as_garbage_inv_def prod.simps apply normalize_goal+ apply (rule_tac x=x in exI, rule_tac x=xa in exI) apply simp by (metis Duplicate_Free_Multiset.distinct_mset_mono distinct_subseteq_iff) show ?thesis unfolding iterate_over_ℒ_a_l_lC_def mark_duplicated_binary_clauses_as_garbage_wl2_alt_def apply refine_vcg apply (rule H) subgoal by auto subgoal by (auto simp flip: all_init_atms_st_alt_def intro: HH) subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto apply (rule H) subgoal by auto apply (rule H') subgoal by auto apply (rule H') subgoal by auto subgoal by auto subgoal by auto subgoal by auto done qed lemma mark_duplicated_binary_clauses_as_garbage_wl2_mark_duplicated_binary_clauses_as_garbage_wl: ‹mark_duplicated_binary_clauses_as_garbage_wl2 S ≤ ⇓Id (mark_duplicated_binary_clauses_as_garbage_wl S)› proof - have H: ‹fst a = snd b ∧ snd a = fst b ⟹ (a,b) ∈ {((s,t), (u, v)). (s=v) ∧ (t=u)}› for a b by (cases a; cases b) simp have H': ‹a = b ⟹ a ≤ ⇓Id b› for a b by auto show ?thesis unfolding mark_duplicated_binary_clauses_as_garbage_wl2_def mark_duplicated_binary_clauses_as_garbage_wl_def apply (refine_vcg) subgoal by auto apply (rule H) subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto apply (rule H') subgoal by auto apply (rule H') subgoal by auto subgoal by auto subgoal by auto done qed lemma isa_mark_duplicated_binary_clauses_as_garbage_wl_mark_duplicated_binary_clauses_as_garbage_wl: assumes ‹(S, S') ∈ twl_st_heur_restart_ana' r u› shows ‹isa_mark_duplicated_binary_clauses_as_garbage_wl S ≤ ⇓(twl_st_heur_restart_ana' r u) (mark_duplicated_binary_clauses_as_garbage_wl S')› proof - have 1: ‹get_vmtf_heur S ∈ bump_heur (atm_of `# all_init_lits_of_wl S') (get_trail_wl S')› and 2: ‹isasat_input_nempty (all_init_atms_st S')› and 3: ‹isasat_input_bounded (all_init_atms_st S')› using assms unfolding twl_st_heur_restart_ana_def twl_st_heur_restart_alt_def2 Let_def by (simp_all add: all_init_atms_st_alt_def) have [refine0]: ‹RETURN False ≤ ⇓ {(a,b). a = b ∧ ¬b} (RES UNIV)› by (auto intro!: RETURN_RES_refine) have create: ‹create (length (get_watched_wl_heur S)) ≤ SPEC (λc. (c, Map.empty) ∈ {((c :: nat literal ⇒ (nat × bool) option, m::nat), c'). c = c' ∧ m = (length (get_watched_wl_heur S))})› (is ‹_ _≤ SPEC(λ_. _ ∈ ?CS)›) by (auto simp: create_def) have init: ‹(x2a, x2) ∈ ⟨nat_rel⟩option_rel ⟹ (CS, Map.empty) ∈ ?CS ⟹ ((x2a, CS, S), x2, S') ∈ {((a,CS,T), (b,T')). ((a,T), b,T') ∈ ⟨nat_rel⟩option_rel ×_r {(a,b). (a,b)∈ twl_st_heur_restart_ana'' (length (get_clauses_wl_heur S)) (learned_clss_count S) (get_vmtf_heur S) (length (get_watched_wl_heur S))} ∧ (CS, Map.empty) ∈ {((c :: nat literal ⇒ (nat × bool) option, m::nat), c'). c = c' ∧ m = (length (get_watched_wl_heur T))}}› (is ‹_ ⟹ _ ⟹ _ ∈ ?loop›) for x2a x2 CS using assms by (auto simp: get_vmtf_heur_array_def twl_st_heur_restart_ana_def) have rel: ‹(xa, Sa) ∈ {((CS, T), T'). (T, T') ∈ twl_st_heur_restart_ana'' (length (get_clauses_wl_heur S)) (learned_clss_count S) (get_vmtf_heur S) (length (get_watched_wl_heur S)) ∧ (CS, Map.empty) ∈ {((c, m), c'). c = c' ∧ m = length (get_watched_wl_heur x2d)}} ⟹ xa = (x1e, x2e) ⟹ length (get_clauses_wl_heur x2e) ≤ length (get_clauses_wl_heur S) ∧ learned_clss_count x2e ≤ learned_clss_count S ⟹ (xb, x'a) ∈ {((CS, T), T'). (T, T') ∈ twl_st_heur_restart_ana'' (length (get_clauses_wl_heur S)) (learned_clss_count S) (get_vmtf_heur S) (length (get_watched_wl_heur S)) ∧ (CS, Map.empty) ∈ {((c, m), c'::nat literal ⇒ (nat × bool) option). c = c' ∧ m = length (get_watched_wl_heur x2e)}} ⟹ xb = (a, b) ⟹ get_vmtf_heur_array S = get_vmtf_heur_array b ⟹ ((a, b), x'a) ∈ {((CS, T), T'). (T,T')∈twl_st_heur_restart_ana'' (length (get_clauses_wl_heur S)) (learned_clss_count S) (get_vmtf_heur S) (length (get_watched_wl_heur S)) ∧ (CS, Map.empty) ∈ {((c, m), c'::nat literal ⇒ (nat × bool) option). c = c' ∧ m = length (get_watched_wl_heur S)}}› for A Sa x1d x2d skip xa x1e x2e xb x'a a b by auto have rel2: ‹(x, x') ∈ {((a, CS, T), b, T'). ((a, T), b, T') ∈ ⟨nat_rel⟩option_rel ×_f {(a, b). (a, b) ∈ twl_st_heur_restart_ana'' (length (get_clauses_wl_heur S)) (learned_clss_count S) (get_vmtf_heur S) (length (get_watched_wl_heur S))} ∧ (CS, Map.empty) ∈ {((c, m), c'). c = c' ∧ m = length (get_watched_wl_heur T)}} ⟹ x' = (x1b, x2b) ⟹ x = (x1c, x2c) ⟹ (x2c, x2b) ∈ {((CS, T), T'). ((T), T') ∈ {(a, b). (a, b) ∈ twl_st_heur_restart_ana'' (length (get_clauses_wl_heur S)) (learned_clss_count S) (get_vmtf_heur S) (length (get_watched_wl_heur S))} ∧ (CS, Map.empty) ∈ {((c, m), c'). c = c' ∧ m = length (get_watched_wl_heur T)}}› for x' x1b x2b x1c x2c x by auto have rel0: ‹((x1d, x2d), x2b) ∈ {((CS, T), T'). (T,T')∈twl_st_heur_restart_ana'' (length (get_clauses_wl_heur S)) (learned_clss_count S) (get_vmtf_heur S) (length (get_watched_wl_heur S)) ∧ (CS, Map.empty) ∈ {((c, m), c'::nat literal ⇒ (nat × bool) option). c = c' ∧ m = length (get_watched_wl_heur S)}}› if ‹mark_duplicated_binary_clauses_as_garbage_pre_wl S'› and ‹mark_duplicated_binary_clauses_as_garbage_pre_wl_heur S› and ‹inres (create (length (get_watched_wl_heur S))) CS› and ‹(CS, Map.empty) ∈ {((c, m), c'). c = c' ∧ m = length (get_watched_wl_heur S)}› and ‹(get_vmtf_heur_array S, Some (get_vmtf_heur_fst S)) = (x1a, x2a)› and ‹(x, x') ∈ {((a, CS, T), b, T'). ((a, T), b, T') ∈ ⟨nat_rel⟩option_rel ×_f {(a, b). (a, b) ∈ twl_st_heur_restart_ana'' (length (get_clauses_wl_heur S)) (learned_clss_count S) (get_vmtf_heur S) (length (get_watched_wl_heur S))} ∧ (CS, Map.empty) ∈ {((c, m), c'). c = c' ∧ m = length (get_watched_wl_heur T)}}› and ‹case x of (n, x) ⇒ ∀x1 x2. x = (x1, x2) ⟶ n ≠ None ∧ get_conflict_wl_is_None_heur x2› and ‹case x' of (n, x) ⇒ n ≠ None ∧ get_conflict_wl x = None› and ‹case x of (n, CS, Sa) ⇒ get_vmtf_heur_array S = get_vmtf_heur_array Sa› and ‹case x' of (n, x) ⇒ ∃ℬ'. mark_duplicated_binary_clauses_as_garbage_wl_inv (all_init_atms_st S') S' (x, ℬ')› and ‹x' = (x1b, x2b)› and ‹x = (x1c, x2c)› and ‹x1b ≠ None› and ‹x1c ≠ None› and ‹the x1b < length x1› and ‹the x1b ≤ unat32_max div 2› and ‹the x1c < length x1a› and ‹the x1c ≤ unat32_max div 2› and ‹x2c = (x1d, x2d)› and ‹get_vmtf_heur_array S = get_vmtf_heur_array x2d› and ‹the x1b ∈# atm_of `# all_init_lits_of_wl x2b› for skip CS x1 x2 x1a x2a x x' x1b x2b x1c x2c x1d x2d skipa using that by auto have binary_deduplicate_required: ‹(should_eliminate_pure_st S, True) ∈ UNIV› for S skip v by (auto simp: should_eliminate_pure_st_def) have GC_required_skip: ‹mop_is_marked_added_heur_st x2d (the x1c) ≤ ⇓ {(a,b). (¬skip,b)∈bool_rel} (RES UNIV)› if ‹mark_duplicated_binary_clauses_as_garbage_pre_wl S'› and ‹mark_duplicated_binary_clauses_as_garbage_pre_wl_heur S› and ‹inres (create (length (get_watched_wl_heur S))) CS› and ‹(CS, Map.empty) ∈ {((c, m), c'). c = c' ∧ m = length (get_watched_wl_heur S)}› and ‹(get_vmtf_heur_array S, Some (get_vmtf_heur_fst S)) = (x1a, x2a)› and ‹(x, x') ∈ {((a, CS, T), b, T'). ((a, T), b, T') ∈ ⟨nat_rel⟩option_rel ×_f {(a, b). (a, b) ∈ twl_st_heur_restart_ana'' (length (get_clauses_wl_heur S)) (learned_clss_count S) (get_vmtf_heur S) (length (get_watched_wl_heur S))} ∧ (CS, Map.empty) ∈ {((c, m), c'). c = c' ∧ m = length (get_watched_wl_heur T)}}› and ‹case x of (n, x) ⇒ ∀x1 x2. x = (x1, x2) ⟶ n ≠ None ∧ get_conflict_wl_is_None_heur x2› and ‹case x' of (n, x) ⇒ n ≠ None ∧ get_conflict_wl x = None› and ‹case x of (n, CS, Sa) ⇒ get_vmtf_heur_array S = get_vmtf_heur_array Sa› and ‹case x' of (n, x) ⇒ ∃ℬ'. mark_duplicated_binary_clauses_as_garbage_wl_inv (all_init_atms_st S') S' (x, ℬ')› and ‹x' = (x1b, x2b)› and ‹x = (x1c, x2c)› and ‹x1b ≠ None› and ‹x1c ≠ None› and ‹the x1b < length x1› and ‹the x1b ≤ unat32_max div 2› and ‹the x1c < length x1a› and ‹the x1c ≤ unat32_max div 2› and ‹x2c = (x1d, x2d)› and ‹get_vmtf_heur_array S = get_vmtf_heur_array x2d› and ‹the x1b ∈# atm_of `# all_init_lits_of_wl x2b› for skip CS x1 x2 x1a x2a x x' x1b x2b x1c x2c x1d x2d proof - term ?thesis have heur: ‹heuristic_rel (all_init_atms_st x2b) (get_heur x2d)› using that by (auto simp: twl_st_heur_restart_ana_def twl_st_heur_restart_def all_init_atms_st_def get_unit_init_clss_wl_alt_def) moreover have ‹the x1c ∈# all_init_atms_st x2b› using that by (auto simp: all_init_atms_st_alt_def) ultimately have ‹is_marked_added_heur_pre (get_heur x2d) (the x1c)› unfolding is_marked_added_heur_pre_def by (auto simp: heuristic_rel_def is_marked_added_heur_pre_stats_def heuristic_rel_stats_def phase_saving_def atms_of_ℒ_a_l_l_𝒜_i_n) then show ?thesis unfolding mop_is_marked_added_heur_st_def mop_is_marked_added_heur_def by (auto intro!: RETURN_RES_refine) qed have skip: ‹(skip_lit, skip) ∈ {(a, b). (¬should_eliminate_pure_st S, b) ∈ bool_rel} ⟹ skip ∈ UNIV ⟹ (¬ should_eliminate_pure_st S) = skip› for skip_lit skip by auto have last_step: ‹do { _ ← ASSERT (mark_duplicated_binary_clauses_as_garbage_pre_wl_heur S); let skip = should_eliminate_pure_st S; (CS::(nat literal ⇒ (nat × bool) option)× nat) ← create (length (get_watched_wl_heur S)); (CS, S) ← iterate_over_VMTFC (λA (CS, Sa). do { _ ← ASSERT (get_vmtf_heur_array S = get_vmtf_heur_array Sa); _ ← mop_is_marked_added_heur_st Sa A; if ¬skip then RETURN (CS, Sa) else do { ASSERT (length (get_clauses_wl_heur Sa) ≤ length (get_clauses_wl_heur S) ∧ learned_clss_count Sa ≤ learned_clss_count S); (CS, Sa) ← isa_deduplicate_binary_clauses_wl (Pos A) CS Sa; ASSERT (length (get_clauses_wl_heur Sa) ≤ length (get_clauses_wl_heur S) ∧ learned_clss_count Sa ≤ learned_clss_count S); (CS, Sa) ← isa_deduplicate_binary_clauses_wl (Neg A) CS Sa; _ ← ASSERT (get_vmtf_heur_array S = get_vmtf_heur_array Sa); RETURN (CS, Sa) } }) (λ(CS, Sa). get_vmtf_heur_array S = get_vmtf_heur_array Sa) (λ(CS, S). get_conflict_wl_is_None_heur S) (get_vmtf_heur_array S, Some (get_vmtf_heur_fst S)) (CS, S); RETURN S } ≤ ⇓ (twl_st_heur_restart_ana' r u) (do { x ← ASSERT (mark_duplicated_binary_clauses_as_garbage_pre_wl S'); let _ = True; let _ = (λ_::nat literal. None :: (nat × bool) option); x ← iterate_over_VMTFC (λL (S). do { _ ← ASSERT (L ∈# atm_of `# all_init_lits_of_wl S); skip ← RES UNIV; if skip then RETURN (S) else do { (S) ← deduplicate_binary_clauses_wl (Pos L) S; (S) ← deduplicate_binary_clauses_wl (Neg L) S; RETURN (S) } }) (λ(x). ∃ℬ'. mark_duplicated_binary_clauses_as_garbage_wl_inv (all_init_atms_st S') S' (x, ℬ')) (λ(x). get_conflict_wl x = None) (get_vmtf_heur_array S, Some (get_vmtf_heur_fst S)) (S'); RETURN x })› for CS supply [[goals_limit=1]] unfolding iterate_over_VMTFC_def apply (refine_vcg isa_deduplicate_binary_clauses_mark_duplicated_binary_clauses_as_garbage_wl[where r=‹length (get_clauses_wl_heur S)› and u=‹learned_clss_count S› and ns = ‹get_vmtf_heur S› and lw=‹length (get_watched_wl_heur S)›]) subgoal using assms unfolding mark_duplicated_binary_clauses_as_garbage_pre_wl_heur_def by fast apply (rule create) apply (rule init) subgoal by (use in ‹auto simp: get_vmtf_heur_fst_def›) subgoal by auto subgoal by (auto simp: get_vmtf_heur_array_def) subgoal apply auto apply (subst (asm) get_conflict_wl_is_None_heur_get_conflict_wl_is_None_ana[THEN fref_to_Down_unRET_Id]) apply (auto simp: get_conflict_wl_is_None_def) apply (subst get_conflict_wl_is_None_heur_get_conflict_wl_is_None_ana[THEN fref_to_Down_unRET_Id]) apply (auto simp: get_conflict_wl_is_None_def) done subgoal by auto subgoal by auto subgoal by auto subgoal by auto apply (rule GC_required_skip; assumption?) apply (rule skip; assumption) apply (rule rel0; assumption) subgoal by (auto simp add: twl_st_heur_restart_ana_def) subgoal by (auto simp add: twl_st_heur_restart_ana_def) subgoal by simp subgoal by simp subgoal by auto subgoal by (auto simp add: twl_st_heur_restart_ana_def) subgoal by auto subgoal by auto subgoal by auto subgoal by simp subgoal premises p using p(25-) unfolding get_vmtf_heur_array_def by simp apply (rule rel; assumption?) subgoal by auto apply (rule rel2; assumption) subgoal using assms by (auto simp: twl_st_heur_restart_ana_def) done let ?vm = ‹get_vmtf_heur S› obtain M' where vmtf': ‹(get_vmtf_heur_array S, fst (snd (bump_get_heuristics ?vm)), get_vmtf_heur_fst S, fst (snd (snd (snd (bump_get_heuristics ?vm)))), snd (snd (snd (snd (bump_get_heuristics ?vm))))) ∈ vmtf (atm_of `# all_init_lits_of_wl S') M'› using 1 unfolding bump_heur_def get_vmtf_heur_array_def bump_get_heuristics_def get_vmtf_heur_fst_def by (cases ‹bump_get_heuristics ?vm›) (auto simp: bump_get_heuristics_def bumped_vmtf_array_fst_def split: if_splits) show ?thesis unfolding isa_mark_duplicated_binary_clauses_as_garbage_wl_alt_def apply (rule order_trans) defer apply (rule ref_two_step'') apply (rule subset_refl) apply (rule mark_duplicated_binary_clauses_as_garbage_wl2_mark_duplicated_binary_clauses_as_garbage_wl[unfolded Down_id_eq]) apply (rule order_trans) defer apply (rule ref_two_step'') apply (rule subset_refl) apply (rule mark_duplicated_binary_clauses_as_garbage_wl2_ge_ℒ_a_l_l[unfolded Down_id_eq]) defer apply (rule order_trans) defer apply (rule ref_two_step'') apply (rule subset_refl) apply (rule bind_refine[of _ _ _ _ Id, unfolded Down_id_eq]) apply (rule Id_refine) apply (rule iterate_over_VMTFC_iterate_over_ℒ_a_l_lC[unfolded Down_id_eq, where I = ‹λx. ∃ℬ'. mark_duplicated_binary_clauses_as_garbage_wl_inv (all_init_atms_st S') S' (x, ℬ')› and P = ‹λx. get_conflict_wl x = None› for ℬ]) apply (rule vmtf') apply (solves ‹use 2 in ‹auto simp: all_init_atms_st_alt_def››) apply (solves ‹use 3 in ‹auto simp: all_init_atms_st_alt_def››) apply (solves auto) apply (solves auto) apply (rule last_step[THEN order_trans]) by auto (*getting rid of the last RETURN*) qed lemma isa_mark_duplicated_binary_clauses_as_garbage_wl2_isa_mark_duplicated_binary_clauses_as_garbage_wl: ‹isa_mark_duplicated_binary_clauses_as_garbage_wl2 S ≤ ⇓Id (isa_mark_duplicated_binary_clauses_as_garbage_wl S)› proof - have H: ‹a=b⟹ (a,b)∈Id› ‹c=d ⟹ c ≤⇓Id d› for a b c d by auto have K: ‹(Sb, Sc) ∈ Id ⟹(CSb, CSc) ∈ Id ⟹ get_vmtf_heur_array S = get_vmtf_heur_array Sb ⟹ ((CSb, Sb), (CSc, Sc)) ∈ {((CSa, a), (CSb, b)). (CSa, CSb)∈Id ∧ (a,b)∈Id ∧ get_vmtf_heur_array S = get_vmtf_heur_array a}› for Sb Sc CSb CSc by auto show ?thesis unfolding isa_mark_duplicated_binary_clauses_as_garbage_wl2_def isa_mark_duplicated_binary_clauses_as_garbage_wl_def nres_monad3 Let_def apply refine_rcg apply (rule H) subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto apply (rule H) subgoal by auto subgoal by auto apply (rule K) subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto apply (rule H) subgoal by auto subgoal by auto subgoal by auto apply (rule H) subgoal by auto subgoal by auto apply (rule K; assumption?) subgoal by auto subgoal by auto subgoal by auto subgoal by auto done qed lemma isa_mark_duplicated_binary_clauses_as_garbage_wl_mark_duplicated_binary_clauses_as_garbage_wl2: assumes ‹(S, S') ∈ twl_st_heur_restart_ana' r u› shows ‹isa_mark_duplicated_binary_clauses_as_garbage_wl2 S ≤ ⇓(twl_st_heur_restart_ana' r u) (mark_duplicated_binary_clauses_as_garbage_wl S')› apply (rule order_trans) apply (rule isa_mark_duplicated_binary_clauses_as_garbage_wl2_isa_mark_duplicated_binary_clauses_as_garbage_wl) unfolding Down_id_eq apply (rule isa_mark_duplicated_binary_clauses_as_garbage_wl_mark_duplicated_binary_clauses_as_garbage_wl) apply (rule assms)+ done end

Theory IsaSAT_Simplify_Binaries