Theory Watched_Literals_Watch_List

theory Watched_Literals_Watch_List_Inprocessing imports Watched_Literals_Watch_List Watched_Literals_List_Inprocessing Watched_Literals_Watch_List_Restart begin definition simplify_clause_with_unit_st_wl_pre where ‹simplify_clause_with_unit_st_wl_pre C S ⟷ (∃T. (S, T) ∈ state_wl_l None ∧ simplify_clause_with_unit_st_pre C T)› definition simplify_clause_with_unit_st_wl :: ‹nat ⇒ 'v twl_st_wl ⇒ 'v twl_st_wl nres› where ‹simplify_clause_with_unit_st_wl = (λC (M, N₀, D, NE, UE, NEk, UEk, NS, US, N0, U0, Q, W). do { ASSERT(simplify_clause_with_unit_st_wl_pre C (M, N₀, D, NE, UE, NEk, UEk, NS, US, N0, U0, Q, W)); ASSERT (C ∈# dom_m N₀ ∧ count_decided M = 0 ∧ D = None ∧ no_dup M ∧ C ≠ 0); let S = (M, N₀, D, NE, UE, NEk, UEk, NS, US, N0, U0, Q, W); if False then RETURN S else do { let E = mset (N₀ ∝ C); let irr = irred N₀ C; (unc, b, N) ← simplify_clause_with_unit C M N₀; if unc then do { ASSERT (N = N₀); RETURN S } else if b then do { let T = (M, fmdrop C N, D, (if irr then add_mset E else id) NE, (if ¬irr then add_mset E else id) UE, NEk, UEk, NS, US, N0, U0, Q, W); ASSERT(set_mset (all_learned_lits_of_wl T) = set_mset (all_learned_lits_of_wl S)); ASSERT(set_mset (all_init_lits_of_wl T) = set_mset (all_init_lits_of_wl S)); RETURN T } else if size (N ∝ C) = 1 then do { let L = ((N ∝ C) ! 0); let T = (Propagated L 0 # M, fmdrop C N, D, NE, UE, (if irr then add_mset {#L#} else id) NEk, (if ¬irr then add_mset {#L#} else id)UEk, (if irr then add_mset E else id) NS, (if ¬irr then add_mset E else id)US, N0, U0, add_mset (-L) Q, W); ASSERT(set_mset (all_learned_lits_of_wl T) = set_mset (all_learned_lits_of_wl S)); ASSERT(set_mset (all_init_lits_of_wl T) = set_mset (all_init_lits_of_wl S)); ASSERT (undefined_lit M L ∧ L ∈# all_lits_st S); RETURN T } else if size (N ∝ C) = 0 then do { let T = (M, fmdrop C N, Some {#}, NE, UE, NEk, UEk, (if irr then add_mset E else id) NS, (if ¬irr then add_mset E else id) US, (if irr then add_mset {#} else id) N0, (if ¬irr then add_mset {#} else id)U0, {#}, W); ASSERT(set_mset (all_learned_lits_of_wl T) = set_mset (all_learned_lits_of_wl S)); ASSERT(set_mset (all_init_lits_of_wl T) = set_mset (all_init_lits_of_wl S)); RETURN T } else do { let T = (M, N, D, NE, UE, NEk, UEk, (if irr then add_mset E else id) NS, (if ¬irr then add_mset E else id) US, N0, U0, Q, W); ASSERT(set_mset (all_learned_lits_of_wl T) = set_mset (all_learned_lits_of_wl S)); ASSERT(set_mset (all_init_lits_of_wl T) = set_mset (all_init_lits_of_wl S)); RETURN T } } })› definition simplify_clauses_with_unit_st_wl_pre where ‹simplify_clauses_with_unit_st_wl_pre S ⟷ (∃T. (S, T) ∈ state_wl_l None ∧ no_lost_clause_in_WL S ∧ simplify_clauses_with_unit_st_pre T)› definition simplify_clauses_with_unit_st_wl_inv where ‹simplify_clauses_with_unit_st_wl_inv S₀ it S ⟷ (∃T₀ T. (S₀, T₀) ∈ state_wl_l None ∧ (S, T) ∈ state_wl_l None ∧ simplify_clauses_with_unit_st_inv T₀ it T ∧ no_lost_clause_in_WL S)› definition simplify_clauses_with_unit_st_wl :: ‹'v twl_st_wl ⇒ 'v twl_st_wl nres› where ‹simplify_clauses_with_unit_st_wl S = do { ASSERT(simplify_clauses_with_unit_st_wl_pre S); xs ← SPEC(λxs. finite xs); T ← FOREACHci(λit T. simplify_clauses_with_unit_st_wl_inv S it T) (xs) (λS. get_conflict_wl S = None) (λi S. if i ∈# dom_m (get_clauses_wl S) then simplify_clause_with_unit_st_wl i S else RETURN S) S; ASSERT(set_mset (all_learned_lits_of_wl T) ⊆ set_mset (all_learned_lits_of_wl S)); ASSERT(set_mset (all_init_lits_of_wl T) = set_mset (all_init_lits_of_wl S)); RETURN T }› lemma clauses_pointed_to_union: ‹clauses_pointed_to (A ∪ B) W = clauses_pointed_to A W ∪ clauses_pointed_to B W› by (auto simp: clauses_pointed_to_def) lemma clauses_pointed_to_mono: ‹A ⊆ B ⟹ clauses_pointed_to A W ⊆ clauses_pointed_to B W› by (auto simp: clauses_pointed_to_def) lemma simplify_clause_with_unit_st_wl_simplify_clause_with_unit_st: assumes ST: ‹(S, T) ∈ state_wl_l None› and ‹(i,j) ∈ nat_rel› and point: ‹no_lost_clause_in_WL S› shows ‹simplify_clause_with_unit_st_wl i S ≤ ⇓ {(S',T). (S',T) ∈ state_wl_l None ∧ no_lost_clause_in_WL S' ∧ get_watched_wl S' = get_watched_wl S} (simplify_clause_with_unit_st j T)› proof - have Id: ‹A = B ⟹ A ≤ ⇓Id B› for A B by auto have ij: ‹i = j› using assms by auto have [simp]: ‹irred b j ⟹ j ∈# dom_m b ⟹ add_mset (mset (b ∝ j)) ({#mset (fst x). x ∈# remove1_mset (the (fmlookup b j)) (init_clss_l b)#} + d + f + h) = ({#mset (fst x). x ∈# (init_clss_l b)#} + d + f + h)› for C D d b f h j by (auto simp: image_mset_remove1_mset_if ran_m_def dest!: multi_member_split) have KK[simp]: ‹irred b j ⟹ j ∈# dom_m b ⟹ C ⊆# mset (b ∝ j) ⟹ set_mset (all_lits_of_mm (add_mset (mset (b ∝ j)) (add_mset C (mset `# remove1_mset (b ∝ j) (init_clss_lf b) + d + f + h)))) = set_mset (all_lits_of_mm (mset `# (init_clss_lf b) + d + f + h))› for b j C d f h using all_lits_of_m_mono[of C ‹mset (b ∝ j)›] by (auto simp: image_mset_remove1_mset_if ran_m_def conj_disj_distribR Collect_disj_eq image_Un Collect_conv_if all_lits_of_mm_add_mset simp flip: insert_compr dest!: multi_member_split[of j]) have H: ‹fmdrop j x2 = fmdrop j b ⟹ mset (x2 ∝ j) ⊆# mset (b ∝ j) ⟹ irred x2 j ⟹ irred b j ⟹ j ∈# dom_m b ⟹ j ∈# dom_m x2 ⟹ set_mset (all_lits_of_mm (add_mset (mset (b ∝ j)) ({#mset (fst x). x ∈# init_clss_l x2#} + d + f + h))) = set_mset (all_lits_of_mm ({#mset (fst x). x ∈# init_clss_l b#} + d + f + h))› for j x2 b d f h using distinct_mset_dom[of x2] distinct_mset_dom[of b] apply (subgoal_tac ‹{#mset (fst x). x ∈# filter_mset snd {#the (fmlookup b x). x ∈# remove1_mset j (dom_m b)#}#} = {#mset (fst x). x ∈# filter_mset snd {#the (fmlookup x2 x). x ∈# remove1_mset j (dom_m x2)#} #}›) (*TODO fix, broke during update to 2021-1*) apply (auto simp: ran_m_def all_lits_of_mm_add_mset dest!: multi_member_split[of _ ‹dom_m _›] dest: all_lits_of_m_mono intro!: image_mset_cong2 filter_mset_cong2) apply (auto 5 3 simp: ran_m_def all_lits_of_mm_add_mset dest!: multi_member_split[of _ ‹dom_m _›] dest: all_lits_of_m_mono intro!: image_mset_cong2 filter_mset_cong2) apply (metis fmdrop_eq_update_eq fmupd_lookup union_single_eq_member) by (metis add_mset_remove_trivial dom_m_fmdrop) have [simp]: ‹mset a ⊆# mset b ⟹ length a= 1 ⟹ a ! 0 ∈ set b› for a b by (cases a, auto) have K1: ‹∀L∈#all_lits_of_mm ({#mset (fst x). x ∈# init_clss_l b#} + d + f + h). distinct_watched (k L) ⟹ irred b j ⟹ j ∈# dom_m b ⟹ L ∈# all_lits_of_m (mset (b ∝ j)) ⟹ distinct_watched (k L)› for b d f h k j L by (auto simp: ran_m_def all_lits_of_mm_add_mset dest!: multi_member_split) have K2: ‹∀L∈#all_lits_of_mm ({#mset (fst x). x ∈# init_clss_l b#} + d + f + h). distinct_watched (k L) ⟹ irred b j ⟹ j ∈# dom_m b ⟹ mset C ⊆# mset (b ∝ j) ⟹ length C = Suc 0 ⟹ L ∈# all_lits_of_m ({#C!0#}) ⟹ distinct_watched (k L)› for b d f h k j L C using all_lits_of_m_mono[of ‹mset C› ‹mset (b ∝ j)›] all_lits_of_m_mono[of ‹{#C!0#}› ‹mset C›] by (auto simp: ran_m_def all_lits_of_mm_add_mset dest!: multi_member_split[of _ ‹dom_m _›]) have K3: ‹∀L∈#all_lits_of_mm ({#mset (fst x). x ∈# init_clss_l b#} + d + f + h). distinct_watched (k L) ⟹ L ∈# all_lits_of_mm ({#mset (fst x). x ∈# remove1_mset (the (fmlookup b j)) (init_clss_l b)#} + d + f + h) ⟹ distinct_watched (k L)› for b d f h k j L C by (cases ‹j ∈# dom_m b›; cases ‹irred b j›) (auto dest!: multi_member_split[of _ ‹dom_m _›] simp: ran_m_def all_lits_of_mm_union all_lits_of_mm_add_mset image_mset_remove1_mset_if split: if_splits) have K4: ‹ irred b j ⟹ j ∈# dom_m b ⟹ all_lits_of_mm (add_mset (mset (b ∝ j)) ({#mset (fst x). x ∈# init_clss_l (fmdrop j b)#} + d + f + h)) = all_lits_of_mm ({#mset (fst x). x ∈# init_clss_l b#} + d + f + h)› ‹¬irred b j ⟹ j ∈# dom_m b ⟹ all_lits_of_mm (add_mset (mset (b ∝ j)) ({#mset (fst x). x ∈# learned_clss_l (fmdrop j b)#} + d + f + h)) = all_lits_of_mm ({#mset (fst x). x ∈# learned_clss_l b#} + d + f + h)› for d f h j b using distinct_mset_dom[of b] apply (auto simp add: init_clss_l_fmdrop learned_clss_l_fmdrop_if) by (smt (z3) fmupd_same image_mset_add_mset learned_clss_l_mapsto_upd prod.collapse union_mset_add_mset_left) show ?thesis supply [[goals_limit=1]] using ST point apply (cases S; hypsubst) apply (cases T; hypsubst) unfolding simplify_clause_with_unit_st_wl_def simplify_clause_with_unit_st_def ij state_wl_l_def prod.simps Let_def[of ‹(_,_)›] apply refine_rcg subgoal for a b c d e f g h i ja k l m aa ba ca da ea fa ga ha ia jaa ka la ma using ST unfolding simplify_clause_with_unit_st_wl_pre_def by (rule_tac x = ‹(aa, ba, ca, da, ea, fa, ga, ha, ia, jaa, ka, la, ma)› in exI) simp subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto apply (rule Id) subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by (auto simp add: all_learned_lits_of_wl_def all_init_lits_of_l_def all_learned_lits_of_l_def get_init_clss_l_def) subgoal by (auto simp: all_learned_lits_of_wl_def all_init_lits_of_l_def all_learned_lits_of_l_def get_init_clss_l_def) subgoal by (auto simp: all_init_lits_of_wl_def init_clss_l_fmdrop init_clss_l_fmdrop_irrelev literals_are_ℒ_i_n'_def blits_in_ℒ_i_n'_def no_lost_clause_in_WL_def dest: in_diffD) subgoal by auto subgoal by (auto simp: all_learned_lits_of_wl_def all_init_lits_of_l_def all_learned_lits_of_l_def get_init_clss_l_def) subgoal by (auto simp: all_learned_lits_of_wl_def all_init_lits_of_l_def all_learned_lits_of_l_def get_init_clss_l_def all_init_lits_of_wl_def) subgoal by auto subgoal by (auto simp: all_lits_st_alt_def all_learned_lits_of_wl_def all_init_lits_of_l_def all_init_lits_of_wl_def get_init_clss_l_def) subgoal apply (auto simp: all_init_lits_of_wl_def init_clss_l_fmdrop init_clss_l_fmdrop_irrelev add_mset_commute no_lost_clause_in_WL_def dest: in_diffD intro:) done subgoal by auto subgoal by (auto simp: all_learned_lits_of_wl_def all_init_lits_of_l_def all_learned_lits_of_l_def get_init_clss_l_def) subgoal by (auto simp: all_learned_lits_of_wl_def all_init_lits_of_l_def all_learned_lits_of_l_def get_init_clss_l_def all_init_lits_of_wl_def) subgoal by (auto simp: all_init_lits_of_wl_def init_clss_l_fmdrop init_clss_l_fmdrop_irrelev all_lits_of_mm_add_mset no_lost_clause_in_WL_def dest: in_diffD) subgoal by (auto simp: all_learned_lits_of_wl_def all_init_lits_of_l_def all_learned_lits_of_l_def get_init_clss_l_def) subgoal by (auto simp: all_learned_lits_of_wl_def all_init_lits_of_l_def all_learned_lits_of_l_def get_init_clss_l_def all_init_lits_of_wl_def) subgoal for a b c d e f g h i ja k aa ba ca da ea fa ga ha ia jaa ka x x' x1 x2 x1a x2a apply (auto simp: all_init_lits_of_wl_def init_clss_l_fmdrop init_clss_l_fmdrop_irrelev H no_lost_clause_in_WL_def dest: in_diffD intro: ) apply (metis (no_types, lifting) basic_trans_rules(31) dom_m_fmdrop insert_DiffM) apply (metis (no_types, lifting) basic_trans_rules(31) dom_m_fmdrop init_clss_l_fmdrop_irrelev insert_DiffM) done done qed lemma [twl_st_wl, simp]: assumes ‹(σ, σ') ∈ state_wl_l None› shows all_learned_lits_of_l_all_learned_lits_of_wl: ‹all_learned_lits_of_l σ' = all_learned_lits_of_wl σ› and all_init_lits_of_l_all_init_lits_of_wl: ‹all_init_lits_of_l σ' = all_init_lits_of_wl σ› using assms by (auto simp: state_wl_l_def all_learned_lits_of_l_def all_learned_lits_of_wl_def all_init_lits_of_l_def all_init_lits_of_wl_def) lemma simplify_clauses_with_unit_st_wl_simplify_clause_with_unit_st: assumes ST: ‹(S, T) ∈ state_wl_l None› and point: ‹correct_watching'_nobin S› and lits: ‹literals_are_ℒ_i_n' S› shows ‹simplify_clauses_with_unit_st_wl S ≤ ⇓ {(S',T). (S',T) ∈ state_wl_l None ∧ no_lost_clause_in_WL S' ∧ literals_are_ℒ_i_n' S' ∧ get_watched_wl S' = get_watched_wl S} (simplify_clauses_with_unit_st T)› proof - have [refine0]: ‹inj_on id xs› for xs by auto have 1: ‹simplify_clauses_with_unit_st_wl S = do { T ← simplify_clauses_with_unit_st_wl S; RETURN T}› by auto have 2: ‹simplify_clauses_with_unit_st T = do { T ← simplify_clauses_with_unit_st T; RETURN T}› by auto have ST2: ‹(S,T) ∈ {(S',U). (S',U) ∈ state_wl_l None ∧ no_lost_clause_in_WL S' ∧ get_watched_wl S = get_watched_wl S'}› if ‹simplify_clauses_with_unit_st_pre T› using assms that correct_watching'_nobin_clauses_pointed_to0[OF ST] unfolding simplify_clauses_with_unit_st_inv_def simplify_clauses_with_unit_st_pre_def by auto show ?thesis apply (subst 1) unfolding simplify_clauses_with_unit_st_wl_def simplify_clauses_with_unit_st_def nres_monad3 apply (refine_rcg simplify_clause_with_unit_st_wl_simplify_clause_with_unit_st) subgoal using assms ST2 unfolding simplify_clauses_with_unit_st_wl_pre_def by blast subgoal using ST by auto apply (rule ST2, assumption) subgoal by auto subgoal for xs xsa it σ it' σ' using assms apply - unfolding simplify_clauses_with_unit_st_wl_inv_def apply (rule exI[of _ T]) apply (rule exI[of _ σ']) by auto subgoal by auto apply (rule_tac T1=σ' and j1 = x' in simplify_clause_with_unit_st_wl_simplify_clause_with_unit_st[THEN order_trans]) subgoal by auto subgoal by auto subgoal by auto subgoal by (rule conc_fun_R_mono) (use assms(3) in ‹auto simp: literals_are_ℒ_i_n'_def blits_in_ℒ_i_n'_def›) subgoal using ST by auto subgoal using ST lits by (auto 4 3 simp: literals_are_ℒ_i_n'_def watched_by_alt_def blits_in_ℒ_i_n'_def) subgoal using ST lits by (auto 4 3 simp: literals_are_ℒ_i_n'_def watched_by_alt_def blits_in_ℒ_i_n'_def) done qed lemma simplify_clauses_with_unit_st_wl_simplify_clause_with_unit_st2: assumes ST: ‹(S, T) ∈ state_wl_l None› and point: ‹no_lost_clause_in_WL S› and lits: ‹literals_are_ℒ_i_n' S› shows ‹simplify_clauses_with_unit_st_wl S ≤ ⇓ {(S',T). (S',T) ∈ state_wl_l None ∧ no_lost_clause_in_WL S' ∧ literals_are_ℒ_i_n' S' ∧ get_watched_wl S' = get_watched_wl S} (simplify_clauses_with_unit_st T)› proof - have [refine0]: ‹inj_on id xs› for xs by auto have 1: ‹simplify_clauses_with_unit_st_wl S = do { T ← simplify_clauses_with_unit_st_wl S; RETURN T}› by auto have 2: ‹simplify_clauses_with_unit_st T = do { T ← simplify_clauses_with_unit_st T; RETURN T}› by auto have ST2: ‹(S,T) ∈ {(S',U). (S',U) ∈ state_wl_l None ∧ no_lost_clause_in_WL S' ∧ get_watched_wl S = get_watched_wl S'}› if ‹simplify_clauses_with_unit_st_pre T› using assms that correct_watching'_nobin_clauses_pointed_to0[OF ST] unfolding simplify_clauses_with_unit_st_inv_def simplify_clauses_with_unit_st_pre_def by auto show ?thesis apply (subst 1) unfolding simplify_clauses_with_unit_st_wl_def simplify_clauses_with_unit_st_def nres_monad3 apply (refine_rcg simplify_clause_with_unit_st_wl_simplify_clause_with_unit_st) subgoal using assms ST2 unfolding simplify_clauses_with_unit_st_wl_pre_def by blast subgoal using ST by auto apply (rule ST2, assumption) subgoal by auto subgoal for xs xsa it σ it' σ' using assms apply - unfolding simplify_clauses_with_unit_st_wl_inv_def apply (rule exI[of _ T]) apply (rule exI[of _ σ']) by auto subgoal by auto apply (rule_tac T1=σ' and j1 = x' in simplify_clause_with_unit_st_wl_simplify_clause_with_unit_st[THEN order_trans]) subgoal by auto subgoal by auto subgoal by auto subgoal by (rule conc_fun_R_mono) (use assms(3) in ‹auto simp: literals_are_ℒ_i_n'_def blits_in_ℒ_i_n'_def›) subgoal using ST by auto subgoal using ST lits by (auto 4 3 simp: literals_are_ℒ_i_n'_def watched_by_alt_def blits_in_ℒ_i_n'_def) subgoal using ST lits by (auto 4 3 simp: literals_are_ℒ_i_n'_def watched_by_alt_def blits_in_ℒ_i_n'_def) done qed definition simplify_clauses_with_units_st_wl_pre where ‹simplify_clauses_with_units_st_wl_pre S ⟷ (∃T. (S, T) ∈ state_wl_l None ∧ literals_are_ℒ_i_n' S)› definition simplify_clauses_with_units_st_wl where ‹simplify_clauses_with_units_st_wl S = do { ASSERT(simplify_clauses_with_units_st_wl_pre S); new_units ← SPEC (λb. b ⟶ get_conflict_wl S = None); if new_units then simplify_clauses_with_unit_st_wl S else RETURN S}› lemma simplify_clauses_with_units_st_wl_simplify_clause_with_units_st: assumes ST: ‹(S, T) ∈ state_wl_l None› and point: ‹correct_watching'_nobin S› and lits: ‹literals_are_ℒ_i_n' S› shows ‹simplify_clauses_with_units_st_wl S ≤ ⇓ {(S',T). (S',T) ∈ state_wl_l None ∧ no_lost_clause_in_WL S' ∧ literals_are_ℒ_i_n' S' ∧ get_watched_wl S' = get_watched_wl S} (simplify_clauses_with_units_st T)› unfolding simplify_clauses_with_units_st_wl_def simplify_clauses_with_units_st_def apply (refine_vcg simplify_clauses_with_unit_st_wl_simplify_clause_with_unit_st) subgoal using assms unfolding simplify_clauses_with_units_st_wl_pre_def by fast subgoal using ST by auto subgoal using assms by auto subgoal using assms by auto subgoal using assms by auto subgoal using assms by auto subgoal using assms unfolding simplify_clauses_with_units_st_pre_def by (fast intro!: correct_watching'_nobin_clauses_pointed_to0(2)) done lemma simplify_clauses_with_units_st_wl_simplify_clause_with_units_st2: assumes ST: ‹(S, T) ∈ state_wl_l None› and point: ‹no_lost_clause_in_WL S› and lits: ‹literals_are_ℒ_i_n' S› shows ‹simplify_clauses_with_units_st_wl S ≤ ⇓ {(S',T). (S',T) ∈ state_wl_l None ∧ no_lost_clause_in_WL S' ∧ literals_are_ℒ_i_n' S' ∧ get_watched_wl S' = get_watched_wl S} (simplify_clauses_with_units_st T)› unfolding simplify_clauses_with_units_st_wl_def simplify_clauses_with_units_st_def apply (refine_vcg simplify_clauses_with_unit_st_wl_simplify_clause_with_unit_st2) subgoal using assms unfolding simplify_clauses_with_units_st_wl_pre_def by fast subgoal using ST by auto subgoal using assms by auto subgoal using assms by auto subgoal using assms by auto subgoal using assms by auto subgoal using assms unfolding simplify_clauses_with_units_st_pre_def by (fast intro!: correct_watching'_nobin_clauses_pointed_to0(2)) done subsection ‹Forward subsumption› text ‹We follow the implementation of forward that is in Splatz and not the more advanced one in CaDiCaL that relies on occurrence lists. Both version are similar (so changing it is not a problem), but IsaSAT needs a way to say that the state is not watching. This in turns means that GC needs to go over the clause domain instead of the watch lists, but makes it possible to reuse the watch lists for other things, like forward subsumption (that again only differs by the lists we use to check subsumption). Compared to Splatz the literal-move-to-front trick is not included (at least not currently). There is critical but major subtility: The algorithm does not work on binary clauses: Binary clauses can yield new units, which in turn, can shorten clauses later, forcing a rehash of the clauses. There are two solutions to this problem: ▪ avoid it completely by making sure that there are no binary clauses, requiring to duplicate the code (even if only few invariants change) ▪ give up on the invariant ▪ implement forward subsumption directly. Long story short: we gave up and implemented the forward approach directly. We do the simplifications in two rounds: ▪ once with binary clauses only (this was part of the sc2020 version) ▪ once with all other clauses (this is onging work) › subsubsection ‹Binary clauses› text ‹This version does not enforce that binary clauses have not been deleted.› fun correct_watching'_leaking_bin :: ‹'v twl_st_wl ⇒ bool› where ‹correct_watching'_leaking_bin (M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, Q, W) ⟷ (∀L ∈# all_init_lits_of_wl (M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, Q, W). distinct_watched (W L) ∧ (∀(i, K, b)∈#mset (W L). i ∈# dom_m N ⟶ K ∈ set (N ∝ i) ∧ K ≠ L ∧ correctly_marked_as_binary N (i, K, b)) ∧ filter_mset (λi. i ∈# dom_m N) (fst `# mset (W L)) = clause_to_update L (M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, {#}, {#}))› declare correct_watching'_leaking_bin.simps[simp del] definition clause_remove_duplicate_clause_wl_pre :: ‹_› where ‹clause_remove_duplicate_clause_wl_pre C S ⟷ (∃S'. (S, S') ∈ state_wl_l None ∧ clause_remove_duplicate_clause_pre C S' ∧ correct_watching'_leaking_bin S)› definition clause_remove_duplicate_clause_wl :: ‹nat ⇒ 'v twl_st_wl ⇒ 'v twl_st_wl nres› where ‹clause_remove_duplicate_clause_wl C = (λ(M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, WS, Q). do { ASSERT (clause_remove_duplicate_clause_wl_pre C (M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, WS, Q)); RETURN (M, fmdrop C N, D, NE, UE, NEk, 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, WS, Q) })› (*TODO Move*) lemma filter_image_mset_removeAll: ‹{#C ∈# A. P C#} - {#C ∈# replicate_mset (count A C') C'. P C#} = {#C ∈# A. P C ∧ C ≠ C'#}› by (metis count_filter_mset filter_filter_mset filter_mset_neq image_filter_replicate_mset replicate_mset_0) lemma filter_image_mset_swap: ‹distinct_mset A ⟹ distinct_mset B ⟹ {#i ∈# A. i ∈# B ∧ P i#} = {#i ∈# B. i ∈# A ∧ P i#}› by (smt (z3) Collect_cong distinct_mset_filter distinct_set_mset_eq set_mset_filter) (*END Move*) lemma correctly_marked_as_binary_fmdrop: ‹i ∈# dom_m x1m ⟹ i ≠ C' ⟹ correctly_marked_as_binary x1m (i, K, b)⟹ correctly_marked_as_binary (fmdrop C' x1m) (i, K, b) › by (auto simp: correctly_marked_as_binary.simps) lemma correct_watching'_leaking_bin_remove_subsumedI: ‹correct_watching'_leaking_bin (x1l, x1m, x1n, x1o, x1p, x1q, x1r, x1s, x1t, x1u, x1v, x1w, x2w) ⟹ C' ∈# dom_m x1m ⟹ irred x1m C' ⟹ correct_watching'_leaking_bin (x1l, fmdrop C' x1m, x1n, x1o, x1p, x1q, x1r, add_mset (mset (x1m ∝ C')) x1s, x1t, x1u, x1v, x1w, x2w)› ‹correct_watching'_leaking_bin (x1l, x1m, x1n, x1o, x1p, x1q, x1r, x1s, x1t, x1u, x1v, x1w, x2w) ⟹ C' ∈# dom_m x1m ⟹ ¬ irred x1m C' ⟹ correct_watching'_leaking_bin (x1l, fmdrop C' x1m, x1n, x1o, x1p, x1q, x1r, x1s, add_mset (mset (x1m ∝ C')) x1t, x1u, x1v, x1w, x2w)› ‹correct_watching'_leaking_bin (x1l, x1m, x1n, x1o, x1p, x1q, x1r, x1s, x1t, x1u, x1v, x1w, x2w) ⟹ C' ∈# dom_m x1m ⟹ irred x1m C' ⟹ correct_watching'_leaking_bin (x1l, fmdrop C' x1m, x1n, add_mset (mset (x1m ∝ C')) x1o, x1p, x1q, x1r, x1s, x1t, x1u, x1v, x1w, x2w)› ‹correct_watching'_leaking_bin (x1l, x1m, x1n, x1o, x1p, x1q, x1r, x1s, x1t, x1u, x1v, x1w, x2w) ⟹ C' ∈# dom_m x1m ⟹ ¬ irred x1m C' ⟹ correct_watching'_leaking_bin (x1l, fmdrop C' x1m, x1n, x1o, add_mset (mset (x1m ∝ C')) x1p, x1q, x1r, x1s, x1t, x1u, x1v, x1w, x2w)› apply (auto simp: correct_watching'_leaking_bin.simps all_init_lits_of_wl_def image_mset_remove1_mset_if distinct_mset_remove1_All distinct_mset_dom correctly_marked_as_binary.simps clause_to_update_def filter_image_mset_removeAll) apply (drule bspec) apply assumption apply normalize_goal+ apply (drule arg_cong[where f=‹filter_mset (λC. C ≠ C')›]) apply (auto simp add: filter_filter_mset intro: filter_mset_cong) apply (drule bspec) apply assumption apply normalize_goal+ apply (drule arg_cong[where f=‹filter_mset (λC. C ≠ C')›]) apply (auto simp add: filter_filter_mset intro: filter_mset_cong) apply (drule bspec) apply assumption apply normalize_goal+ apply (drule arg_cong[where f=‹filter_mset (λC. C ≠ C')›]) apply (auto simp add: filter_filter_mset intro: filter_mset_cong) apply (drule bspec) apply assumption apply normalize_goal+ apply (drule arg_cong[where f=‹filter_mset (λC. C ≠ C')›]) apply (auto simp add: filter_filter_mset intro: filter_mset_cong) done lemma clause_remove_duplicate_clause_wl_clause_remove_duplicate_clause: assumes ‹(C,C')∈nat_rel› ‹(S,T)∈ state_wl_l None› ‹correct_watching'_leaking_bin S› shows ‹clause_remove_duplicate_clause_wl C S ≤ ⇓{(U, V). (U,V)∈ state_wl_l None ∧ correct_watching'_leaking_bin U ∧ get_watched_wl U = get_watched_wl S} (clause_remove_duplicate_clause C' T)› using assms unfolding clause_remove_duplicate_clause_wl_def clause_remove_duplicate_clause_def apply (refine_vcg) subgoal unfolding clause_remove_duplicate_clause_wl_pre_def by fast subgoal for 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 x1n x2n x1o x2o x1p x2p x1q x2q x1r x2r x1s x2s x1t x2t x1u x2u x1v x2v x1w x2w by (auto simp: state_wl_l_def clause_remove_duplicate_clause_pre_def intro!: correct_watching'_leaking_bin_remove_subsumedI) done definition binary_clause_subres_lits_wl_pre :: ‹_› where ‹binary_clause_subres_lits_wl_pre C L L' S ⟷ (∃S'. (S, S') ∈ state_wl_l None ∧ binary_clause_subres_lits_pre C L L' S')› definition binary_clause_subres_wl :: ‹nat ⇒ 'v literal ⇒ 'v literal ⇒ 'v twl_st_wl ⇒ 'v twl_st_wl nres› where ‹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)); RETURN (Propagated L 0 # 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) })› lemma all_init_lits_of_wl_add_drop_irred: assumes ‹C' ∈# dom_m (x1m)› ‹irred x1m C'› shows ‹all_init_lits_of_wl ([], fmdrop C' x1m, x1n, x1o, {#}, x1q, {#}, add_mset (mset (x1m ∝ C')) x1s, {#}, x1u, {#}, x1w, x2w) = all_init_lits_of_wl ([], x1m, x1n, x1o, {#}, x1q, {#}, x1s, {#}, x1u, {#}, x1w, x2w)› (is ?A) and ‹K' ∈ set (x1m ∝ C') ⟹ set_mset (all_init_lits_of_wl (x1l, x1m, None, x1o, x1p, add_mset {#K'#} x1q, x1r, x1s, x1t, x1u, x1v, add_mset (- K') x1w, x2w)) = set_mset (all_init_lits_of_wl (x1l, x1m, None, x1o, x1p, x1q, x1r, x1s, x1t, x1u, x1v, x1w, x2w))› (is ‹_ ⟹ ?B›) proof - have A: ‹init_clss_l x1m = add_mset (x1m ∝ C', irred x1m C') (init_clss_l (fmdrop C' x1m))› by (smt (z3) assms(1) assms(2) eq_fst_iff fmdrop_eq_update_eq2 init_clss_l_fmdrop_if init_clss_l_mapsto_upd le_boolD le_boolI' sndE) show ?A using assms by (auto simp: all_init_lits_of_wl_def all_lits_of_mm_add_mset init_clss_l_fmdrop_if image_mset_remove1_mset_if dest!: multi_member_split)[] show ?B if ‹K' ∈ set (x1m ∝ C')› using assms that apply - apply (auto simp: all_init_lits_of_wl_def all_lits_of_mm_add_mset all_lits_of_m_add_mset in_all_lits_of_mm_uminus_iff) apply (subst A) apply (auto simp add: all_lits_of_mm_add_mset all_lits_of_m_add_mset add_mset_eq_add_mset in_clause_in_all_lits_of_m in_set_mset_eq_in) apply (subst A) apply (auto simp add: all_lits_of_mm_add_mset all_lits_of_m_add_mset add_mset_eq_add_mset in_clause_in_all_lits_of_m in_set_mset_eq_in) done qed lemma correct_watching'_leaking_bin_fmdropI: assumes ‹C' ∈# dom_m (x1m)› ‹irred x1m C'› shows ‹correct_watching'_leaking_bin (x1l, x1m, x1n, x1o, x1p, x1q, x1r, x1s, x1t, x1u, x1v, x1w, x2w) ⟹ correct_watching'_leaking_bin (Propagated K' 0 # x1l, fmdrop C' x1m, x1n, x1o, x1p, x1q, x1r, add_mset (mset (x1m ∝ C')) x1s, x1t, x1u, x1v, x1w, x2w)› using assms distinct_mset_dom[of x1m] unfolding correct_watching'_leaking_bin.simps apply (auto simp: all_init_lits_of_wl_add_drop_irred distinct_mset_remove1_All clause_to_update_def filter_image_mset_removeAll correctly_marked_as_binary.simps dest: multi_member_split[of C']) apply (drule bspec) apply assumption apply normalize_goal+ apply (drule arg_cong[where f=‹filter_mset (λC. C ≠ C')›]) apply (auto simp add: filter_filter_mset intro: filter_mset_cong) done lemma correct_watching'_leaking_bin_fmdropI_red: assumes ‹C' ∈# dom_m (x1m)› ‹¬irred x1m C'› shows ‹correct_watching'_leaking_bin (x1l, x1m, x1n, x1o, x1p, x1q, x1r, x1s, x1t, x1u, x1v, x1w, x2w) ⟹ correct_watching'_leaking_bin (Propagated K' 0 # x1l, fmdrop C' x1m, x1n, x1o, x1p, x1q, x1r, x1s, add_mset (mset (x1m ∝ C')) x1t, x1u, x1v, x1w, x2w)› ‹correct_watching'_leaking_bin (x1l, x1m, x1n, x1o, x1p, x1q, x1r, x1s, x1t, x1u, x1v, x1w, x2w) ⟹ correct_watching'_leaking_bin (x1l, x1m, None, x1o, x1p, x1q, add_mset {#K'#} x1r, x1s, x1t, x1u, x1v, add_mset (- K') x1w, x2w)› subgoal using assms distinct_mset_dom[of x1m] unfolding correct_watching'_leaking_bin.simps apply (auto simp: all_init_lits_of_wl_add_drop_irred distinct_mset_remove1_All clause_to_update_def filter_image_mset_removeAll correctly_marked_as_binary.simps dest: multi_member_split[of C'])[] apply (drule bspec) apply assumption apply normalize_goal+ apply (drule arg_cong[where f=‹filter_mset (λC. C ≠ C')›]) apply (auto simp add: filter_filter_mset intro: filter_mset_cong) done subgoal using assms distinct_mset_dom[of x1m] unfolding correct_watching'_leaking_bin.simps by (auto simp: all_init_lits_of_wl_add_drop_irred distinct_mset_remove1_All clause_to_update_def filter_image_mset_removeAll all_init_lits_of_wl_def correctly_marked_as_binary.simps dest: multi_member_split[of C'])[] done lemma correct_watching'_leaking_bin_add_unitI: assumes ‹K' ∈# mset (x1m ∝ C')› ‹C' ∈# dom_m x1m› ‹irred x1m C'› shows ‹correct_watching'_leaking_bin (x1l, x1m, None, x1o, x1p, x1q, x1r, x1s, x1t, x1u, x1v, x1w, x2w) ⟹ correct_watching'_leaking_bin (x1l, x1m, None, x1o, x1p, add_mset {#K'#} x1q, x1r, x1s, x1t, x1u, x1v, add_mset (- K') x1w, x2w)› using assms by (auto simp: correct_watching'_leaking_bin.simps clause_to_update_def all_init_lits_of_wl_add_drop_irred) lemma binary_clause_subres_wl_binary_clause_subres: assumes ‹(C,C')∈nat_rel› ‹(K,K')∈Id› ‹(L,L')∈Id› ‹(S,S')∈ state_wl_l None› ‹correct_watching'_leaking_bin S› shows ‹binary_clause_subres_wl C K L S ≤ ⇓{(U, V). (U,V)∈ state_wl_l None ∧ correct_watching'_leaking_bin U ∧ get_watched_wl U = get_watched_wl S} (binary_clause_subres C' K' L' S')› using assms unfolding binary_clause_subres_wl_def binary_clause_subres_def apply (refine_vcg) subgoal unfolding binary_clause_subres_lits_wl_pre_def by fast subgoal for 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 x1n x2n x1o x2o x1p x2p x1q x2q x1r x2r x1s x2s x1t x2t x1u x2u x1v x2v x1w x2w apply (auto simp: state_wl_l_def intro!: correct_watching'_leaking_bin_fmdropI correct_watching'_leaking_bin_add_unitI correct_watching'_leaking_bin_fmdropI_red) apply (auto simp: binary_clause_subres_lits_pre_def)[2] apply (auto simp: state_wl_l_def intro!: correct_watching'_leaking_bin_fmdropI correct_watching'_leaking_bin_add_unitI correct_watching'_leaking_bin_fmdropI_red) apply (auto simp: binary_clause_subres_lits_pre_def)[2] apply (auto simp: state_wl_l_def intro!: correct_watching'_leaking_bin_fmdropI correct_watching'_leaking_bin_add_unitI correct_watching'_leaking_bin_fmdropI_red) done done definition deduplicate_binary_clauses_pre_wl :: ‹'v literal ⇒ 'v twl_st_wl ⇒ bool› where ‹deduplicate_binary_clauses_pre_wl L S ⟷ (∃T. (S, T) ∈ state_wl_l None ∧ deduplicate_binary_clauses_pre L T ∧ correct_watching'_leaking_bin S ∧ literals_are_ℒ_i_n' S)› definition deduplicate_binary_clauses_inv_wl :: ‹'v twl_st_wl ⇒ 'v literal ⇒ bool × nat × _× 'v twl_st_wl ⇒ bool› where ‹deduplicate_binary_clauses_inv_wl S L = (λ(abort, i, mark, T). (∃S' T'. (S, S') ∈ state_wl_l None ∧ (T, T') ∈ state_wl_l None ∧ deduplicate_binary_clauses_inv L (fst `# mset (watched_by T L)) S' (abort, fst `# mset (drop i (watched_by T L)), mark, T') ∧ correct_watching'_leaking_bin T ∧ literals_are_ℒ_i_n' S ∧ get_watched_wl T = get_watched_wl S))› lemma deduplicate_binary_clauses_inv_wl_literals_are_in: ‹deduplicate_binary_clauses_inv_wl S L (abort, i, mark, T) ⟹ literals_are_ℒ_i_n' T› supply [[goals_limit=1]] unfolding deduplicate_binary_clauses_inv_wl_def prod.simps deduplicate_binary_clauses_inv_def literals_are_ℒ_i_n'_def blits_in_ℒ_i_n'_def apply normalize_goal+ apply (frule rtranclp_cdcl_twl_inprocessing_l_all_learned_lits_of_l) apply (frule rtranclp_cdcl_twl_inprocessing_l_all_init_lits_of_l) by (auto simp: watched_by_alt_def) definition deduplicate_binary_clauses_wl :: ‹'v literal ⇒ 'v twl_st_wl ⇒ 'v twl_st_wl nres› where ‹deduplicate_binary_clauses_wl L S = do { ASSERT (deduplicate_binary_clauses_pre_wl L S); let CS = (λ_. None); let l = length (watched_by 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 { let (C,L', b) = (watched_by S L ! i); if C ∉# dom_m (get_clauses_wl S) ∨ ¬b then RETURN (abort, i+1, CS, S) else do { let L' = 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)); RETURN (defined_lit (get_trail_wl U) L, i+1, CS, U) } else if CS L' ≠ None then do { let C' = (if ¬snd (the (CS L')) ⟶ ¬irred (get_clauses_wl S) C then C else fst (the (CS L'))); let CS = (if ¬snd (the (CS L')) ⟶ ¬irred (get_clauses_wl S) C then CS else CS (L' := Some (C, irred (get_clauses_wl S) C))); S ← clause_remove_duplicate_clause_wl C' S; RETURN (abort, i+1, CS, S) } else if CS (-L') ≠ None then do { S ← binary_clause_subres_wl C L (-L') S; RETURN (True, i+1, CS, S) } else do { RETURN (abort, i+1, CS (L' := Some (C, irred (get_clauses_wl S) C)), S) } } }) (defined_lit (get_trail_wl S) L, 0, CS, S); RETURN S }› lemma correct_watching'_leaking_bin_pure_lit: assumes ‹correct_watching'_leaking_bin (a, b, c, d, e, f, g, h, i, ja, k, l, m)› ‹L ∈# all_init_lits_of_wl (a, b, c, d, e, f, g, h, i, ja, k, l, m)› shows ‹correct_watching'_leaking_bin (Propagated L 0 # a, b, c, d, e, add_mset {#L#} f, g, h, i, ja, k, add_mset (-L) l, m)› proof - have [simp]: ‹set_mset (all_init_lits_of_wl ([], b, c, d, {#}, add_mset {#L#} f, {#}, h, {#}, ja, {#}, add_mset (-L) l, m)) = set_mset (all_init_lits_of_wl ([], b, c, d, {#}, f, {#}, h, {#}, ja, {#}, l, m))› using assms unfolding all_init_lits_of_wl_def by (auto simp: all_init_lits_of_wl_def all_lits_of_mm_add_mset all_lits_of_m_add_mset all_lits_of_mm_union in_all_lits_of_mm_uminus_iff) show ?thesis using assms by (auto simp: correct_watching'_leaking_bin.simps clause_to_update_def) qed lemma correct_watching'_leaking_bin_propagate_unit_irred: assumes ‹irred b j› and ‹j ∈# dom_m b› and ‹correct_watching'_leaking_bin (a, b, c, d, e, f, g, h, i, ja, k, l, m)› ‹L ∈ set (b ∝ j)› shows ‹correct_watching'_leaking_bin (Propagated L 0 # a, b, c, d, e, add_mset {#L#} f, g, h, i, ja, k, add_mset (-L) l, m)› proof - have ‹L ∈# all_init_lits_of_wl (a, b, c, d, e, f, g, h, i, ja, k, l, m)› using assms by (auto simp: all_lits_of_mm_union all_lits_of_mm_add_mset all_init_lits_of_wl_def ran_m_def in_clause_in_all_lits_of_m dest!: multi_member_split) from correct_watching'_leaking_bin_pure_lit[OF _ this] show ?thesis using assms by blast qed lemma correct_watching'_leaking_bin_propagate_unit_red: assumes ‹¬irred b j› and ‹j ∈# dom_m b› and ‹correct_watching'_leaking_bin (a, b, None, d, e, f, g, h, i, ja, k, l, m)› ‹L ∈ set (b ∝ j)› shows ‹correct_watching'_leaking_bin (Propagated L 0 # a, b, None, d, e, f, add_mset {#L#} g, h, i, ja, k, add_mset (-L) l, m)› proof - have [simp]: ‹set_mset (all_init_lits_of_wl ([], b, None, d, {#}, f, {#}, h, {#}, ja, {#}, add_mset (- L) l, m)) = set_mset (all_init_lits_of_wl ([], b, None, d, {#}, f, {#}, h, {#}, ja, {#}, l, m))› using assms unfolding all_init_lits_of_wl_def by (auto simp: all_init_lits_of_wl_def all_lits_of_mm_add_mset all_lits_of_m_add_mset all_lits_of_mm_union) show ?thesis using assms by (auto simp: correct_watching'_leaking_bin.simps clause_to_update_def) qed lemma correct_watching'_leaking_bin_empty_conflict: ‹correct_watching'_leaking_bin (a, b, c, d, e, f, g, h, i, ja, k, l, m) ⟹ correct_watching'_leaking_bin (a, b, Some {#}, d, e, f, g, h, i, add_mset {#} ja, k, {#}, m)› ‹correct_watching'_leaking_bin (a, b, c, d, e, f, g, h, i, ja, k, l, m) ⟹ correct_watching'_leaking_bin (a, b, Some {#}, d, e, f, g, h, i, ja, add_mset {#} k, {#}, m)› by (auto simp: correct_watching'_leaking_bin.simps all_init_lits_of_wl_def all_lits_of_mm_add_mset all_lits_of_m_add_mset clause_to_update_def) text ‹For binary clauses, we can prove a stronger version of @{thm simplify_clause_with_unit_st_wl_simplify_clause_with_unit_st}, because watched literals do not have to be changed.› lemma simplify_clause_with_unit_st_wl_simplify_clause_with_unit_st_correct_watching: assumes ST: ‹(S, T) ∈ state_wl_l None› and ij: ‹(i,j) ∈ nat_rel› and point: ‹correct_watching'_leaking_bin S› and ‹i ∈# dom_m (get_clauses_wl S)› and Si: ‹length (get_clauses_wl S ∝ i) = 2› shows ‹simplify_clause_with_unit_st_wl i S ≤ ⇓ {(S',T). (S',T) ∈ state_wl_l None ∧ correct_watching'_leaking_bin S' ∧ get_watched_wl S' = get_watched_wl S} (simplify_clause_with_unit_st j T)› proof - have Id: ‹A = B ⟹ A ≤ ⇓Id B› for A B by auto have ij: ‹i = j› using assms by auto have [simp]: ‹irred b j ⟹ j ∈# dom_m b ⟹ add_mset (mset (b ∝ j)) ({#mset (fst x). x ∈# remove1_mset (the (fmlookup b j)) (init_clss_l b)#} + d + f + h) = ({#mset (fst x). x ∈# (init_clss_l b)#} + d + f + h)› for C D d b f h j by (auto simp: image_mset_remove1_mset_if ran_m_def dest!: multi_member_split) have KK[simp]: ‹irred b j ⟹ j ∈# dom_m b ⟹ C ⊆# mset (b ∝ j) ⟹ set_mset (all_lits_of_mm (add_mset (mset (b ∝ j)) (add_mset C (mset `# remove1_mset (b ∝ j) (init_clss_lf b) + d + f + h)))) = set_mset (all_lits_of_mm (mset `# (init_clss_lf b) + d + f + h))› for b j C d f h using all_lits_of_m_mono[of C ‹mset (b ∝ j)›] by (auto simp: image_mset_remove1_mset_if ran_m_def conj_disj_distribR Collect_disj_eq image_Un Collect_conv_if all_lits_of_mm_add_mset simp flip: insert_compr dest!: multi_member_split[of j]) have H: ‹fmdrop j x2 = fmdrop j b ⟹ mset (x2 ∝ j) ⊆# mset (b ∝ j) ⟹ irred x2 j ⟹ irred b j ⟹ j ∈# dom_m b ⟹ j ∈# dom_m x2 ⟹ set_mset (all_lits_of_mm (add_mset (mset (b ∝ j)) ({#mset (fst x). x ∈# init_clss_l x2#} + d + f + h))) = set_mset (all_lits_of_mm ({#mset (fst x). x ∈# init_clss_l b#} + d + f + h))› for j x2 b d f h using distinct_mset_dom[of x2] distinct_mset_dom[of b] apply (subgoal_tac ‹{#mset (fst x). x ∈# filter_mset snd {#the (fmlookup b x). x ∈# remove1_mset j (dom_m b)#}#} = {#mset (fst x). x ∈# filter_mset snd {#the (fmlookup x2 x). x ∈# remove1_mset j (dom_m x2)#} #}›) apply (auto 5 2 simp: ran_m_def all_lits_of_mm_add_mset dest!: multi_member_split[of _ ‹dom_m _›] dest: all_lits_of_m_mono intro!: image_mset_cong2 filter_mset_cong2) apply (metis all_lits_of_m_union mset_subset_eq_exists_conv union_iff) apply (metis fmdrop_eq_update_eq fmupd_lookup union_single_eq_member) apply (metis add_mset_remove_trivial dom_m_fmdrop) done have [simp]: ‹mset a ⊆# mset b ⟹ length a= 1 ⟹ a ! 0 ∈ set b› for a b by (cases a, auto) have K1: ‹∀L∈#all_lits_of_mm ({#mset (fst x). x ∈# init_clss_l b#} + d + f + h). distinct_watched (k L) ⟹ irred b j ⟹ j ∈# dom_m b ⟹ L ∈# all_lits_of_m (mset (b ∝ j)) ⟹ distinct_watched (k L)› for b d f h k j L by (auto simp: ran_m_def all_lits_of_mm_add_mset dest!: multi_member_split) have K2: ‹∀L∈#all_lits_of_mm ({#mset (fst x). x ∈# init_clss_l b#} + d + f + h). distinct_watched (k L) ⟹ irred b j ⟹ j ∈# dom_m b ⟹ mset C ⊆# mset (b ∝ j) ⟹ length C = Suc 0 ⟹ L ∈# all_lits_of_m ({#C!0#}) ⟹ distinct_watched (k L)› for b d f h k j L C using all_lits_of_m_mono[of ‹mset C› ‹mset (b ∝ j)›] all_lits_of_m_mono[of ‹{#C!0#}› ‹mset C›] by (auto simp: ran_m_def all_lits_of_mm_add_mset dest!: multi_member_split[of _ ‹dom_m _›]) have K3: ‹∀L∈#all_lits_of_mm ({#mset (fst x). x ∈# init_clss_l b#} + d + f + h). distinct_watched (k L) ⟹ L ∈# all_lits_of_mm ({#mset (fst x). x ∈# remove1_mset (the (fmlookup b j)) (init_clss_l b)#} + d + f + h) ⟹ distinct_watched (k L)› for b d f h k j L C by (cases ‹j ∈# dom_m b›; cases ‹irred b j›) (auto dest!: multi_member_split[of _ ‹dom_m _›] simp: ran_m_def all_lits_of_mm_union all_lits_of_mm_add_mset image_mset_remove1_mset_if split: if_splits) have K4: ‹ irred b j ⟹ j ∈# dom_m b ⟹ all_lits_of_mm (add_mset (mset (b ∝ j)) ({#mset (fst x). x ∈# init_clss_l (fmdrop j b)#} + d + f + h)) = all_lits_of_mm ({#mset (fst x). x ∈# init_clss_l b#} + d + f + h)› ‹¬irred b j ⟹ j ∈# dom_m b ⟹ all_lits_of_mm (add_mset (mset (b ∝ j)) ({#mset (fst x). x ∈# learned_clss_l (fmdrop j b)#} + d + f + h)) = all_lits_of_mm ({#mset (fst x). x ∈# learned_clss_l b#} + d + f + h)› for d f h j b using distinct_mset_dom[of b] apply (auto simp add: init_clss_l_fmdrop learned_clss_l_fmdrop_if) by (smt (z3) fmupd_same image_mset_add_mset learned_clss_l_mapsto_upd prod.collapse union_mset_add_mset_left) text ‹This case is most likely impossible. It comes from the fact that we do not attempt to prove that the unchanged exactly captures when things are unchanged (missing backimplication).› have correct_watching_after_same_length: ‹¬ irred b j ⟶ correct_watching'_leaking_bin (a, x2a, None, d, e, f, g, h, add_mset (mset (b ∝ j)) i, ja, k, l, m)› (is ?A) ‹irred b j ⟶ correct_watching'_leaking_bin (a, x2a, None, d, e, f, g, add_mset (mset (b ∝ j)) h, i, ja, k, l, m)› (is ?B) if st: ‹aa = a ∧ ba = b ∧ da = d ∧ ea = e ∧ fa = f ∧ ga = g ∧ ha = h ∧ ia = i ∧ jaa = ja ∧ ka = k ∧ ma = l› and corr: ‹correct_watching'_leaking_bin (a, b, None, d, e, f, g, h, i, ja, k, l, m)› and S: ‹S = (a, b, None, d, e, f, g, h, i, ja, k, l, m)› and ‹T = (a, b, None, d, e, f, g, h, i, ja, k, {#}, l)› and ‹simplify_clause_with_unit_st_pre j (a, b, None, d, e, f, g, h, i, ja, k, {#}, l)› and ‹ca = None ∧ la = {#}› and ‹simplify_clause_with_unit_st_wl_pre j (a, b, None, d, e, f, g, h, i, ja, k, l, m)› and ‹j ∈# dom_m b ∧ count_decided a = 0 ∧ c = None ∧ no_dup a ∧ 0 < j› and ‹x2c = x2a› and ‹x2 = (False, x2a)› and ‹x' = (False, False, x2a)› and ‹x2b = (False, x2a)› and ‹x = (False, False, x2a)› and b: ‹fmdrop j x2a = fmdrop j b ∧ irred x2a j = irred b j ∧ mset (x2a ∝ j) ⊆# mset (b ∝ j) ∧ j ∈# dom_m x2a› and ‹¬ x1b› and ‹¬ x1› and ‹¬ x1c› and ‹¬ x1a› and le: ‹length (x2a ∝ j) ≠ Suc 0› ‹x2a ∝ j ≠ []› and eq: ‹set_mset (all_init_lits_of_l (a, x2a, None, d, e, f, g, (if irred b j then add_mset (mset (ba ∝ j)) else id) h, (if irred b j then id else add_mset (mset (ba ∝ j))) i, ja, k, {#}, l)) = set_mset (all_init_lits_of_l (a, b, None, d, e, f, g, h, i, ja, k, {#}, l))› ‹set_mset (all_learned_lits_of_l (a, x2a, None, d, e, f, g, (if irred b j then add_mset (mset (ba ∝ j)) else id) h, (if irred b j then id else add_mset (mset (ba ∝ j))) i, ja, k, {#}, l)) = set_mset (all_learned_lits_of_l (a, b, None, d, e, f, g, h, i, ja, k, {#}, l))› ‹set_mset (all_learned_lits_of_wl ([], x2a, None, d, e, f, g, (if irred b j then add_mset (mset (b ∝ j)) else id) h, (if irred b j then id else add_mset (mset (b ∝ j))) i, ja, k, l, m)) = set_mset (all_learned_lits_of_wl ([], b, None, d, e, f, g, h, i, ja, k, l, m))› ‹set_mset (all_init_lits_of_wl ([], x2a, None, d, {#}, f, {#}, (if irred b j then add_mset (mset (b ∝ j)) else id) h, {#}, ja, {#}, l, m)) = set_mset (all_init_lits_of_wl ([], b, None, d, {#}, f, {#}, h, {#}, ja, {#}, l, m))› for a b c d e f g h i ja k l m aa ba ca da ea fa ga ha ia jaa ka la ma x x' x1 x2 x1a x2a x1b x2b x1c x2c proof - note [[goals_limit=1]] have [simp]: ‹aa ∈# dom_m x2a ⟹ length (x2a ∝ aa) = length (b ∝ aa)› for aa apply (cases ‹aa = j›) subgoal using le b Si ij size_mset_mono[of ‹mset (x2a ∝ aa)› ‹mset (b ∝ aa)›] by (cases ‹x2a ∝ aa›; cases ‹tl (x2a ∝ aa)›) (clarsimp simp add: length_list_2 S subseteq_mset_size_eql_iff add_mset_eq_add_mset)+ subgoal using b apply - apply normalize_goal+ by (drule arg_cong [of _ _ ‹λa. a ∝ aa›]) auto done have [simp]: ‹aa ∈# dom_m x2a ⟹ set (x2a ∝ aa) = set (b ∝ aa)› for aa apply (cases ‹aa = j›) subgoal using le b Si ij size_mset_mono[of ‹mset (x2a ∝ aa)› ‹mset (b ∝ aa)›] apply (simp add: S) apply (clarsimp_all simp add: length_list_2 S) by (cases ‹x2a ∝ aa›; cases ‹tl (x2a ∝ aa)›) (auto simp add: length_list_2 S subseteq_mset_size_eql_iff add_mset_eq_add_mset) subgoal using b apply - apply normalize_goal+ by (drule arg_cong [of _ _ ‹λa. a ∝ aa›]) auto done have [simp]: ‹aa ∈# dom_m x2a ⟹ set (watched_l (x2a ∝ aa)) = set (watched_l (b ∝ aa))› for aa apply (cases ‹aa = j›) subgoal using le b Si ij size_mset_mono[of ‹mset (x2a ∝ aa)› ‹mset (b ∝ aa)›] by (simp add: S) subgoal using b apply - apply normalize_goal+ by (drule arg_cong [of _ _ ‹λa. a ∝ aa›]) auto done have [simp]: ‹dom_m x2a = dom_m b› using b by (metis dom_m_fmdrop insert_DiffM that(8)) show ?A ?B using corr eq by (auto simp: st correct_watching'_leaking_bin.simps clause_to_update_def correctly_marked_as_binary.simps intro!: filter_mset_cong) qed show ?thesis supply [[goals_limit=1]] using ST point apply (cases S; hypsubst) apply (cases T; hypsubst) unfolding simplify_clause_with_unit_st_wl_def simplify_clause_with_unit_st_def ij state_wl_l_def prod.simps Let_def[of ‹(_,_)›] apply refine_rcg subgoal for a b c d e f g h i ja k l m aa ba ca da ea fa ga ha ia jaa ka la ma using ST unfolding simplify_clause_with_unit_st_wl_pre_def by (rule_tac x = ‹(aa, ba, ca, da, ea, fa, ga, ha, ia, jaa, ka, la, ma)› in exI) simp subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto apply (rule Id) subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by (auto simp add: all_learned_lits_of_wl_def all_init_lits_of_l_def all_learned_lits_of_l_def get_init_clss_l_def) subgoal by (auto simp: all_learned_lits_of_wl_def all_init_lits_of_l_def all_learned_lits_of_l_def get_init_clss_l_def) subgoal by (auto simp: all_init_lits_of_wl_def init_clss_l_fmdrop init_clss_l_fmdrop_irrelev literals_are_ℒ_i_n'_def blits_in_ℒ_i_n'_def no_lost_clause_in_WL_def intro: correct_watching'_leaking_bin_remove_subsumedI dest: in_diffD) subgoal by auto subgoal by (auto simp: all_learned_lits_of_wl_def all_init_lits_of_l_def all_learned_lits_of_l_def get_init_clss_l_def) subgoal by (auto simp: all_learned_lits_of_wl_def all_init_lits_of_l_def all_learned_lits_of_l_def get_init_clss_l_def all_init_lits_of_wl_def) subgoal by auto subgoal by (auto simp: all_lits_st_alt_def all_learned_lits_of_wl_def all_init_lits_of_l_def all_init_lits_of_wl_def get_init_clss_l_def) subgoal for a b c d e f g h i ja k l m aa ba ca da ea fa ga ha ia jaa ka la ma x x' x1 x2 x1a x2a x1b x2b x1c x2c apply (auto simp: all_init_lits_of_wl_def init_clss_l_fmdrop init_clss_l_fmdrop_irrelev add_mset_commute no_lost_clause_in_WL_def intro: correct_watching'_leaking_bin_remove_subsumedI correct_watching'_leaking_bin_propagate_unit_irred[where j=j] correct_watching'_leaking_bin_propagate_unit_red[where j=j] dest: in_diffD intro:) apply (rule correct_watching'_leaking_bin_remove_subsumedI) apply (rule correct_watching'_leaking_bin_propagate_unit_irred[where j=j]) apply auto apply (rule correct_watching'_leaking_bin_remove_subsumedI) apply (rule correct_watching'_leaking_bin_propagate_unit_red[where j=j]) apply auto done subgoal by auto subgoal by (auto simp: all_learned_lits_of_wl_def all_init_lits_of_l_def all_learned_lits_of_l_def get_init_clss_l_def) subgoal by (auto simp: all_learned_lits_of_wl_def all_init_lits_of_l_def all_learned_lits_of_l_def get_init_clss_l_def all_init_lits_of_wl_def) subgoal by (auto simp: all_init_lits_of_wl_def init_clss_l_fmdrop init_clss_l_fmdrop_irrelev all_lits_of_mm_add_mset intro: correct_watching'_leaking_bin_remove_subsumedI correct_watching'_leaking_bin_empty_conflict dest: in_diffD) subgoal by (auto simp: all_learned_lits_of_wl_def all_init_lits_of_l_def all_learned_lits_of_l_def get_init_clss_l_def) subgoal by (auto simp: all_learned_lits_of_wl_def all_init_lits_of_l_def all_learned_lits_of_l_def get_init_clss_l_def all_init_lits_of_wl_def) subgoal for a b c d e f g h i ja k l m aa ba ca da ea fa ga ha ia jaa ka la ma x x' x1 x2 x1a x2a x1b x2b x1c x2c by (simp) (intro conjI; rule correct_watching_after_same_length; assumption)+ done qed (*TODO Move*) lemma WHILEIT_refine_with_inv: assumes R0: "I' x' ⟹ (x,x')∈R" assumes IREF: "⋀x x'. ⟦ (x,x')∈R; I' x' ⟧ ⟹ I x" assumes COND_REF: "⋀x x'. ⟦ (x,x')∈R; I x; I' x' ⟧ ⟹ b x = b' x'" assumes STEP_REF: "⋀x x'. ⟦ (x,x')∈R; b x; b' x'; I x; I' x' ⟧ ⟹ f x ≤ ⇓R (f' x')" shows "WHILEIT I b f x ≤⇓{(a,b). (a,b) ∈ R ∧ I a ∧ I' b} (WHILEIT I' b' f' x')" apply (rule WHILEIT_refine_with_post) subgoal using R0 IREF by blast subgoal using IREF by blast subgoal using COND_REF by blast subgoal using STEP_REF IREF by (smt (verit, best) in_pair_collect_simp inres_SPEC pw_ref_iff) done lemma deduplicate_binary_clauses_wl_deduplicate_binary_clauses: assumes ‹(L,L')∈Id› ‹(S,S')∈ state_wl_l None› ‹correct_watching'_leaking_bin S› ‹literals_are_ℒ_i_n' S› shows ‹deduplicate_binary_clauses_wl L S ≤ ⇓{(S, T). (S,T)∈ state_wl_l None ∧ correct_watching'_leaking_bin S ∧ literals_are_ℒ_i_n' S} (deduplicate_binary_clauses L' S')› proof - let ?watched = ‹{(i, CS). i = (length (watched_by S L)) ∧ CS = fst `# mset (watched_by S L) ∧ (∀C. (C ∈# CS ⟶ C ∈# dom_m (get_clauses_l S') ⟶ L' ∈ set (get_clauses_l S' ∝ C)))}› have [refine0]: ‹deduplicate_binary_clauses_pre_wl L S ⟹ RETURN (length (watched_by S L)) ≤ ⇓ ?watched (SPEC (λCS. ∀C. (C ∈# CS ⟶ C ∈# dom_m (get_clauses_l S') ⟶ L' ∈ set (get_clauses_l S' ∝ C)) ∧ distinct_mset CS))› using assms apply (cases S) apply (auto simp: RETURN_RES_refine_iff correct_watching'_leaking_bin.simps deduplicate_binary_clauses_pre_wl_def deduplicate_binary_clauses_pre_def) apply (drule bspec) apply assumption apply auto apply (drule bspec) apply assumption apply (auto simp: clause_to_update_def distinct_mset_image_mset distinct_watched_alt_def dest: in_set_takeD dest!: multi_member_split split: if_splits) apply (meson in_set_takeD) apply (smt (z3) filter_mset_add_mset filter_mset_eq_add_msetD fst_conv image_mset_add_mset in_multiset_in_set multi_member_split) done let ?S = ‹{((abort, i, CS, U), (abort', xs, CS', U')). abort=abort' ∧ fst `# mset (drop i (watched_by S L)) = xs ∧ CS=CS' ∧ (U,U')∈ state_wl_l None ∧ get_watched_wl U = get_watched_wl S ∧ correct_watching'_leaking_bin U}› have [refine0]: ‹(length (watched_by S L), xs) ∈ ?watched ⟹ ((defined_lit (get_trail_wl S) L, 0, Map.empty, S), defined_lit (get_trail_l S') L', xs, Map.empty, S') ∈ ?S› for xs using assms by auto have watched_by: ‹RETURN (watched_by x2e L ! x1d) ≤ ⇓ {((C, K, b), C'). C=C' ∧ (C ∈# dom_m (get_clauses_wl x2e) ⟶ b = (length (get_clauses_wl x2e ∝ C) = 2) ∧ K ≠ L ∧ K ∈ set (get_clauses_wl x2e ∝ C) ∧ L ∈ set (get_clauses_wl x2e ∝ C))} (SPEC (λC. C ∈# x1a))› (is ‹_ ≤ ⇓?watch _›) if LL': ‹(L, L') ∈ Id› and SS': ‹(S, S') ∈ state_wl_l None› and ‹correct_watching'_leaking_bin S› and ‹literals_are_ℒ_i_n' S› and pre: ‹deduplicate_binary_clauses_pre L' S'› and ‹deduplicate_binary_clauses_pre_wl L S› and watched: ‹(length (watched_by S L), xs) ∈ ?watched› and xx': ‹(x, x') ∈ ?S› and abort: ‹case x of (abort, i, CS, Sa) ⇒ ¬ abort ∧ i < length (watched_by S L) ∧ get_conflict_wl Sa = None› and ‹case x' of (abort, xs, CS, S) ⇒ ¬ abort ∧ xs ≠ {#} ∧ get_conflict_l S = None› and inv: ‹deduplicate_binary_clauses_inv_wl S L x› and inv2: ‹deduplicate_binary_clauses_inv L' xs S' x'› and st: ‹x2a = (x1b, x2b)› ‹x2 = (x1a, x2a)› ‹x' = (x1, x2)› ‹x2d = (x1e, x2e)› ‹x2c = (x1d, x2d)› ‹x = (x1c, x2c)› for xs x x' x1 x2 x1a x2a x1b x2b x1c x2c x1d x2d x1e x2e proof - have L_S: ‹L ∈# all_init_lits_of_wl S› ‹cdcl_twl_inprocessing_l^*^* S' x2b› ‹set_mset (all_init_lits_of_l x2b) = set_mset (all_init_lits_of_l S')› ‹set_mset (all_init_lits_of_wl x2e) = set_mset (all_init_lits_of_wl S)› using pre SS' LL' inv2 xx' by (auto simp: deduplicate_binary_clauses_pre_def deduplicate_binary_clauses_inv_def st dest: rtranclp_cdcl_twl_inprocessing_l_all_init_lits_of_l) have ‹x1d < length (get_watched_wl S L)› using xx' abort by (auto simp: watched_by_alt_def st) then have ‹watched_by x2e L ! x1d ∈ set (get_watched_wl S L)› ‹get_watched_wl x2e = get_watched_wl S› ‹correct_watching'_leaking_bin x2e› ‹x1a = fst `# mset (drop x1d (watched_by S L))› ‹get_watched_wl S L ! x1d ∈ set (drop x1d (get_watched_wl S L))› using xx' abort by (auto simp: watched_by_alt_def st intro!: in_set_dropI) moreover have ‹fst (get_watched_wl S L ! x1d) ∈# dom_m (get_clauses_wl x2e) ⟹ L ∈ set (get_clauses_wl x2e ∝ fst (get_watched_wl S L ! x1d))› using L_S(1) xx' ‹watched_by x2e L ! x1d ∈ set (get_watched_wl S L)› xx' multi_member_split[of ‹watched_by x2e L ! x1d› ‹mset (get_watched_wl S L)›] unfolding L_S(4)[symmetric] by (cases x2e) (auto simp: watched_by_alt_def correct_watching'_leaking_bin.simps st clause_to_update_def dest!: multi_member_split[of L] dest!: filter_mset_eq_add_msetD' in_set_takeD) ultimately show ?thesis using L_S unfolding st by (cases x2e) (auto simp: RETURN_RES_refine_iff watched_by_alt_def eq_commute[of ‹(_, _, _)›] correct_watching'_leaking_bin.simps correctly_marked_as_binary.simps intro!: bexI[of _ ‹watched_by x2e L ! x1d›] dest!: multi_member_split[of L]) qed have correct_blit: ‹mset (get_clauses_l x2b ∝ C) = {#L', x1g#}› if LL': ‹(L, L') ∈ Id› and SS': ‹(S, S') ∈ state_wl_l None› and ‹correct_watching'_leaking_bin S› and ‹literals_are_ℒ_i_n' S› and pre: ‹deduplicate_binary_clauses_pre L' S'› and ‹deduplicate_binary_clauses_pre_wl L S› and xs: ‹(length (watched_by S L), xs) ∈ ?watched› and xx': ‹(x, x') ∈ ?S› and abort: ‹case x of (abort, i, CS, Sa) ⇒ ¬ abort ∧ i < length (watched_by S L) ∧ get_conflict_wl Sa = None› and ‹case x' of (abort, xs, CS, S) ⇒ ¬ abort ∧ xs ≠ {#} ∧ get_conflict_l S = None› and inv: ‹deduplicate_binary_clauses_inv_wl S L x› and inv2: ‹deduplicate_binary_clauses_inv L' xs S' x'› and st: ‹x2a = (x1b, x2b)› ‹x2 = (x1a, x2a)› ‹x' = (x1, x2)› ‹x2d = (x1e, x2e)› ‹x2c = (x1d, x2d)› ‹x = (x1c, x2c)› and watch: ‹(watched_by x2e L ! x1d, C) ∈ ?watch x2e› and watcher: ‹watched_by x2e L ! x1d = (x1f, x2f)› ‹x2f = (x1g, x2g)› and bin: ‹¬ (x1f ∉# dom_m (get_clauses_wl x2e) ∨ ¬ x2g)› ‹¬ (C ∉# dom_m (get_clauses_l x2b) ∨ length (get_clauses_l x2b ∝ C) ≠ 2)› for xs x x' x1 x2 x1a x2a x1b x2b x1c x2c x1d x2d x1e x2e C x1f x2f x1g x2g proof - show ?thesis using watch xs bin SS' xx' LL' watcher by (auto simp: st length_list_2 watched_by_alt_def) qed have post_inv: ‹(x2e, x2b) ∈ {(S, T). (S, T) ∈ state_wl_l None ∧ correct_watching'_leaking_bin S ∧ literals_are_ℒ_i_n' S}› if ‹(L, L') ∈ Id› and SS': ‹(S, S') ∈ state_wl_l None› and ‹correct_watching'_leaking_bin S› and ‹literals_are_ℒ_i_n' S› and ‹deduplicate_binary_clauses_pre L' S'› and ‹deduplicate_binary_clauses_pre_wl L S› and ‹(length (watched_by S L), xs) ∈ ?watched› and xx': ‹(x, x') ∈{(a,b). (a,b) ∈ ?S ∧ deduplicate_binary_clauses_inv_wl S L a ∧ deduplicate_binary_clauses_inv L' xs S' b}› and st: ‹x2a = (x1b, x2b)› ‹x2 = (x1a, x2a)› ‹x' = (x1, x2)› ‹x2d = (x1e, x2e)› ‹x2c = (x1d, x2d)› ‹x = (x1c, x2c)› for xs x x' x1 x2 x1a x2a x1b x2b x1c x2c x1d x2d x1e x2e proof - show ?thesis using xx' assms(4) SS' apply - unfolding mem_Collect_eq prod.simps st deduplicate_binary_clauses_inv_def apply normalize_goal+ using rtranclp_cdcl_twl_inprocessing_l_all_init_lits_of_l[of S' x2b] rtranclp_cdcl_twl_inprocessing_l_all_learned_lits_of_l[of S' x2b] by (auto simp add: literals_are_ℒ_i_n'_def st blits_in_ℒ_i_n'_def watched_by_alt_def) qed show ?thesis supply [[goals_limit=1]] using assms unfolding deduplicate_binary_clauses_wl_def deduplicate_binary_clauses_def apply (refine_vcg simplify_clause_with_unit_st_wl_simplify_clause_with_unit_st_correct_watching clause_remove_duplicate_clause_wl_clause_remove_duplicate_clause binary_clause_subres_wl_binary_clause_subres WHILEIT_refine_with_inv) subgoal unfolding deduplicate_binary_clauses_pre_wl_def by fast subgoal for xs x x' unfolding deduplicate_binary_clauses_inv_wl_def prod.simps case_prod_beta apply (rule exI[of _ S']) apply (rule exI[of _ ‹snd (snd (snd x'))›]) by (auto simp: watched_by_alt_def) subgoal for xs x x' by auto apply (rule watched_by; assumption) subgoal for xs x x' x1 x2 x1a x2a x1b x2b x1c x2c x1d x2d x1e x2e by (auto intro!: imageI in_set_dropI simp: watched_by_alt_def) subgoal by (auto simp flip: Cons_nth_drop_Suc simp: watched_by_alt_def) subgoal by (rule correct_blit) subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by (clarsimp dest!: rtranclp_cdcl_twl_inprocessing_l_all_init_lits_of_l simp: all_init_atms_st_alt_def) subgoal by (auto simp flip: Cons_nth_drop_Suc simp: watched_by_alt_def dest: deduplicate_binary_clauses_inv_wl_literals_are_in) subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by (auto simp flip: Cons_nth_drop_Suc simp: watched_by_alt_def dest: deduplicate_binary_clauses_inv_wl_literals_are_in) subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by (auto simp flip: Cons_nth_drop_Suc simp: watched_by_alt_def dest: deduplicate_binary_clauses_inv_wl_literals_are_in) subgoal by (auto simp flip: Cons_nth_drop_Suc simp: watched_by_alt_def dest: deduplicate_binary_clauses_inv_wl_literals_are_in) subgoal by (auto simp flip: Cons_nth_drop_Suc simp: watched_by_alt_def dest: deduplicate_binary_clauses_inv_wl_literals_are_in) subgoal by (rule post_inv) done qed definition mark_duplicated_binary_clauses_as_garbage_pre_wl :: ‹'v twl_st_wl ⇒ bool› where ‹mark_duplicated_binary_clauses_as_garbage_pre_wl = (λS. (∃T. (S,T) ∈ state_wl_l None ∧ correct_watching'_leaking_bin S ∧ literals_are_ℒ_i_n' S))› definition mark_duplicated_binary_clauses_as_garbage_wl_inv :: ‹'v multiset ⇒ 'v twl_st_wl ⇒ 'v twl_st_wl × 'v multiset ⇒ bool› where ‹mark_duplicated_binary_clauses_as_garbage_wl_inv = (λxs S (U, ys). ∃S' U'. (U, U') ∈ state_wl_l None ∧ (S, S') ∈ state_wl_l None ∧ mark_duplicated_binary_clauses_as_garbage_inv xs S' (U', ys))› definition mark_duplicated_binary_clauses_as_garbage_wl :: ‹_ ⇒ 'v twl_st_wl nres› where ‹mark_duplicated_binary_clauses_as_garbage_wl S = do { ASSERT (mark_duplicated_binary_clauses_as_garbage_pre_wl S); Ls ← SPEC (λLs:: 'v multiset. ∀L∈#Ls. L ∈# atm_of `# all_init_lits_of_wl S); (S, _) ← WHILE_T⇗mark_duplicated_binary_clauses_as_garbage_wl_inv Ls S⇖(λ(S, Ls). Ls ≠ {#} ∧ get_conflict_wl S = None) (λ(S, Ls). do { L ← SPEC (λL. L ∈# Ls); ASSERT (L ∈# atm_of `# all_init_lits_of_wl S); skip ← RES (UNIV :: bool set); if skip then RETURN (S, remove1_mset L Ls) else do { S ← deduplicate_binary_clauses_wl (Pos L) S; S ← deduplicate_binary_clauses_wl (Neg L) S; RETURN (S, remove1_mset L Ls) } }) (S, Ls); RETURN S }› lemma mark_duplicated_binary_clauses_as_garbage_wl: assumes ‹(S, S') ∈ {(S, T). (S, T) ∈ state_wl_l None ∧ correct_watching'_leaking_bin S ∧ literals_are_ℒ_i_n' S}› shows ‹mark_duplicated_binary_clauses_as_garbage_wl S ≤ ⇓ {(S, T). (S, T) ∈ state_wl_l None ∧ correct_watching'_leaking_bin S ∧ literals_are_ℒ_i_n' S} (mark_duplicated_binary_clauses_as_garbage S')› proof - let ?R = ‹{(S, T). (S, T) ∈ state_wl_l None ∧ correct_watching'_leaking_bin S ∧ literals_are_ℒ_i_n' S} ×_f Id› have loop: ‹(Ls,Ls')∈Id ⟹ ((S, Ls), (S', Ls')) ∈ ?R› for Ls Ls' using assms by auto show ?thesis unfolding mark_duplicated_binary_clauses_as_garbage_wl_def mark_duplicated_binary_clauses_as_garbage_def apply (refine_vcg loop deduplicate_binary_clauses_wl_deduplicate_binary_clauses) subgoal using assms unfolding mark_duplicated_binary_clauses_as_garbage_pre_wl_def apply - by (rule exI[of _ S']) auto subgoal using assms by auto subgoal for Ls Lsa x x' unfolding mark_duplicated_binary_clauses_as_garbage_wl_inv_def apply (cases x, cases x', hypsubst, unfold prod.simps) apply (rule exI[of _ S'], rule exI[of _ ‹fst x'›]) apply (use assms in simp) done subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto done qed subsubsection ‹Large clauses› definition subsume_clauses_match_pre :: ‹_› where ‹subsume_clauses_match_pre C C' N ⟷ length (N ∝ C) ≤ length (N ∝ C') ∧ C ∈# dom_m N ∧ C' ∈# dom_m N ∧ distinct (N ∝ C) ∧ distinct (N ∝ C') ∧ ¬tautology (mset (N ∝ C))› definition subsume_clauses_match :: ‹nat ⇒ nat ⇒ (nat, 'v literal list × bool) fmap ⇒ 'v subsumption nres› where ‹subsume_clauses_match C C' N = do { ASSERT (subsume_clauses_match_pre C C' N); (i, st) ← WHILE_T⇗ λ(i,s). try_to_subsume C' C (N (C ↪ take i (N ∝ C))) s⇖ (λ(i, st). i < length (N ∝ C) ∧ st ≠ NONE) (λ(i, st). do { let L = N ∝ C ! i; if L ∈ set (N ∝ C') then RETURN (i+1, st) else if -L ∈ set (N ∝ C') then if is_subsumed st then RETURN (i+1, STRENGTHENED_BY L C) else RETURN (i+1, NONE) else RETURN (i+1, NONE) }) (0, SUBSUMED_BY C); RETURN st }› lemma subset_remove1_mset_notin: ‹b ∉# A ⟹ A ⊆# remove1_mset b B ⟷ A⊆#B› by (metis diff_subset_eq_self mset_le_subtract remove1_mset_eqE subset_mset.order_trans) lemma subsume_clauses_match: assumes ‹subsume_clauses_match_pre C C' N› shows ‹subsume_clauses_match C C' N ≤ ⇓ Id (SPEC(try_to_subsume C' C N))› proof - let ?R = ‹measure (λ(i, _). Suc (length(N ∝ C)) - i)› have [refine]: ‹wf ?R› by auto have H: ‹distinct_mset(mset (N ∝ C))› ‹distinct (N ∝ C')› using assms by (auto simp: subsume_clauses_match_pre_def) then have [simp]: ‹a < length (N ∝ C) ⟹ distinct_mset (add_mset (N ∝ C ! a) (mset (take a (N ∝ C))))› ‹a < length (N ∝ C) ⟹ distinct_mset ((mset (take a (N ∝ C))))›for a by (simp_all add: distinct_in_set_take_iff) then have [simp]: ‹a < length (N ∝ C) ⟹ distinct_mset (add_mset (N ∝ C ! a) (remove1_mset L (mset (take a (N ∝ C)))))› for a L using diff_subset_eq_self distinct_mset_add_mset in_diffD distinct_mset_mono by metis have neg_notin: ‹a < length (N ∝ C) ⟹- N ∝ C ! a ∉ set (N ∝ C)› for a using assms by (smt (z3) mset_le_trans mset_lt_single_iff nth_mem set_mset_mset subsume_clauses_match_pre_def tautology_minus) have neg_notin2: ‹a < length (N ∝ C) ⟹- N ∝ C ! a ∉ set (take a (N ∝ C))› for a using assms by (meson in_set_takeD neg_notin) have [simp]: ‹fmupd C (the (fmlookup N C)) N = N› by (meson assms fmupd_same subsume_clauses_match_pre_def) have [simp]: ‹try_to_subsume C' C N NONE› by (auto simp: try_to_subsume_def) have [simp]: ‹a < length (N ∝ C) ⟹ x21 ∈ set (take a (N ∝ C)) ⟹ N ∝ C ! a ∈# remove1_mset (- x21) (mset (N ∝ C')) ⟷ N ∝ C ! a ∈# mset (N ∝ C')› for a x21 apply (cases ‹(- x21) ∈# mset (N ∝ C')›) apply (drule multi_member_split) by (auto simp del: set_mset_mset in_multiset_in_set simp: uminus_lit_swap neg_notin2 eq_commute[of ‹N ∝ C ! _›]) show ?thesis unfolding subsume_clauses_match_def apply (refine_vcg) subgoal using assms by auto subgoal by (auto simp add: try_to_subsume_def) subgoal for s a b x1 x2 by (auto 9 7 simp: try_to_subsume_def take_Suc_conv_app_nth subset_remove1_mset_notin neg_notin2 split: subsumption.splits simp del: distinct_mset_add_mset simp flip: distinct_subseteq_iff) subgoal by auto subgoal for s a b x1 x2 by (auto 7 4 simp: try_to_subsume_def take_Suc_conv_app_nth subset_remove1_mset_notin neg_notin2 split: subsumption.splits simp del: distinct_mset_add_mset simp flip: distinct_subseteq_iff) subgoal by auto subgoal for s a b x1 x2 by (auto 7 4 simp: try_to_subsume_def take_Suc_conv_app_nth split: subsumption.splits simp del: distinct_mset_add_mset simp flip: distinct_subseteq_iff) subgoal by auto subgoal by (auto simp: try_to_subsume_def) subgoal by auto subgoal by auto done qed definition subsume_or_strengthen_wl_pre :: ‹nat ⇒ 'v subsumption ⇒ 'v twl_st_wl ⇒ bool› where ‹subsume_or_strengthen_wl_pre C s S ⟷ (∃T. (S, T) ∈ state_wl_l None ∧ subsume_or_strengthen_pre C s T ∧ length (get_clauses_wl S ∝ C) > 2)› definition strengthen_clause_wl :: ‹nat ⇒ nat ⇒ 'v literal ⇒ 'v twl_st_wl ⇒ 'v twl_st_wl nres› where ‹strengthen_clause_wl = (λC C' L (M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, Q, W). do { ASSERT (subsume_or_strengthen_wl_pre C (STRENGTHENED_BY L C') (M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, Q, W)); E ← SPEC (λE. mset E = mset (remove1 (-L) (N ∝ C))); if length (N ∝ C) = 2 then do { ASSERT (length (remove1 (-L) (N ∝ C)) = 1); let L = hd E; RETURN (Propagated L 0 # M, fmdrop C' (fmdrop C N), D, (if irred N C' then add_mset (mset (N ∝ C')) else id) NE, (if ¬irred N C' then add_mset (mset (N ∝ C')) else id) UE, (if irred N C then add_mset {#L#} else id) NEk, (if ¬irred N C then add_mset {#L#} else id) UEk, ((if irred N C then add_mset (mset (N ∝ C)) else id)) NS, ((if ¬irred N C then add_mset (mset (N ∝ C)) else id)) US, N0, U0, add_mset (-L) Q, W) } else if length (N ∝ C) = length (N ∝ C') then RETURN (M, fmdrop C' (fmupd C (E, irred N C ∨ irred N C') N), D, NE, UE, NEk, UEk, ((if irred N C' then add_mset (mset (N ∝ C')) else id) o (if irred N C then add_mset (mset (N ∝ C)) else id)) NS, ((if ¬irred N C' then add_mset (mset (N ∝ C')) else id) o (if ¬irred N C then add_mset (mset (N ∝ C)) else id)) US, N0, U0, Q, W) else RETURN (M, fmupd C (E, irred N C) N, D, NE, UE, NEk, UEk, (if irred N C then add_mset (mset (N ∝ C)) else id) NS, (if ¬irred N C then add_mset (mset (N ∝ C)) else id) US, N0, U0, Q, W)})› definition subsume_or_strengthen_wl :: ‹nat ⇒ 'v subsumption ⇒ 'v twl_st_wl ⇒ _ nres› where ‹subsume_or_strengthen_wl = (λC s (M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, Q, W). do { ASSERT(subsume_or_strengthen_wl_pre C s (M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, Q, W)); (case s of NONE ⇒ RETURN (M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, Q, W) | SUBSUMED_BY C' ⇒ do { let T = (M, fmdrop C (if ¬irred N C' ∧ irred N C then fmupd C' (N ∝ C', True) N else N), D, NE, UE, NEk, UEk, (if irred N C then add_mset (mset (N ∝ C)) else id) NS, (if ¬irred N C then add_mset (mset (N ∝ C)) else id) US, N0, U0, Q, W); ASSERT (set_mset (all_init_atms_st T) = set_mset (all_init_atms_st (M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, Q, W))); RETURN T } | STRENGTHENED_BY L C' ⇒ strengthen_clause_wl C C' L (M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, Q, W)) })› definition strengthen_clause_pre :: ‹_› where ‹strengthen_clause_pre xs C s t S ⟷ distinct xs ∧ C ∈# dom_m (get_clauses_wl S) › lemma no_lost_clause_in_WLI: ‹no_lost_clause_in_WL S ⟹ set_mset (dom_m (get_clauses_wl T)) ⊆ set_mset (dom_m (get_clauses_wl S)) ⟹ set_mset (all_init_lits_of_wl T) = set_mset (all_init_lits_of_wl S) ⟹ get_watched_wl S = get_watched_wl T ⟹ no_lost_clause_in_WL T› by (auto simp: no_lost_clause_in_WL_def clauses_pointed_to_def watched_by_alt_def dest!: multi_member_split) lemma filter_mset_remove_add_mset: ‹a ∈# M ⟹ {#x ∈# M - add_mset a M'. P x#} = (if P a then remove1_mset a {#x ∈# M - M'. P x#} else {#x ∈# M - M'. P x#})› by (auto dest!: multi_member_split) lemma image_mset_remove_add_mset: ‹a ∈# M ⟹ a ∉# M' ⟹ {#f x. x ∈# M - add_mset a M'#} = remove1_mset (f a) {#f x. x ∈# M - M'#}› by (auto dest!: multi_member_split) lemma strengthen_clause_wl_strengthen_clause: assumes ‹(C, C') ∈ nat_rel› and ‹(s, s') ∈ nat_rel› and ‹(t, t') ∈ Id› and ‹(S, S') ∈ state_wl_l None› and b: ‹strengthen_clause_pre xs C s t S› and pre2: ‹subsume_or_strengthen_wl_pre C (STRENGTHENED_BY t' s') S› shows ‹strengthen_clause_wl C s t S ≤ ⇓ {(T, T'). (T, T') ∈ state_wl_l None ∧ get_watched_wl T = get_watched_wl S} (strengthen_clause C' s' t' S')› proof - have dist: ‹distinct xs› using b unfolding strengthen_clause_pre_def by auto have [simp]: ‹x ∉# dom_m x1m - {#a, x#}› ‹x ∉# dom_m x1m - {#x, a#}› ‹x ∉# dom_m x1m - {#x#}› for x1m a x by (smt (z3) add_mset_commute add_mset_diff_bothsides add_mset_remove_trivial_eq distinct_mset_add_mset distinct_mset_dom in_diffD)+ have H: ‹C ∈# dom_m (get_clauses_wl S)› using assms by (auto simp: strengthen_clause_pre_def) have [simp]: ‹s' ∈# remove1_mset C (dom_m a) ⟷ s' ≠ C ∧ s' ∈#dom_m a› for a s' C by (auto dest: in_diffD) show ?thesis supply [[goals_limit=1]] using assms unfolding strengthen_clause_wl_def strengthen_clause_def apply refine_vcg subgoal using pre2 by fast subgoal by (auto simp: state_wl_l_def split: subsumption.splits) subgoal by (auto simp: state_wl_l_def split: subsumption.splits) subgoal for 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 x1n x2n x1o x2o x1p x2p x1q x2q x1r x2r x1s x2s x1t x2t x1u x2u x1v x2v x1w x2w using distinct_mset_dom[of ‹get_clauses_wl S›] by (auto 5 2 simp: state_wl_l_def all_init_lits_of_wl_def init_clss_l_fmdrop_if strengthen_clause_pre_def Watched_Literals_List_Inprocessing.strengthen_clause_pre_def image_mset_remove_add_mset split: subsumption.splits dest: in_diffD dest: multi_member_split) subgoal by (auto simp: state_wl_l_def split: subsumption.splits) subgoal by (auto simp: state_wl_l_def length_remove1 no_lost_clause_in_WL_def split: subsumption.splits) subgoal by (auto simp: state_wl_l_def length_remove1 no_lost_clause_in_WL_def split: subsumption.splits) subgoal using H apply (cases ‹irred (get_clauses_wl S) C›) by (auto simp: state_wl_l_def no_lost_clause_in_WL_def all_init_lits_of_wl_def all_lits_of_mm_add_mset init_clss_l_mapsto_upd all_lits_of_mm_union init_clss_l_mapsto_upd_irrel dest!: all_lits_of_m_diffD split: subsumption.splits) done qed lemma case_subsumption_refine: ‹(a,b)∈Id ⟹ (is_subsumed a ⟹ f(subsumed_by a )≤ ⇓R (f' (subsumed_by b))) ⟹ (is_strengthened a ⟹ g (strengthened_on_lit a) (strengthened_by a) ≤ ⇓R (g' (strengthened_on_lit a) (strengthened_by a))) ⟹ (a = NONE ⟹ h ≤⇓R h') ⟹ case_subsumption f g h a ≤ ⇓ R (case_subsumption f' g' h' b)› by (cases a) auto lemma subsume_or_strengthen_wl_subsume_or_strengthen: assumes ‹(C, C') ∈ nat_rel› and ‹(s, s') ∈ Id› and ‹(S, S') ∈ state_wl_l None› and ‹C ∈# dom_m (get_clauses_wl S)› ‹length (get_clauses_wl S ∝ C) > 2› shows ‹subsume_or_strengthen_wl C s S ≤ ⇓{(T, T'). (T, T') ∈ state_wl_l None ∧ get_watched_wl T = get_watched_wl S} (subsume_or_strengthen C' s' S')› using assms unfolding subsume_or_strengthen_wl_def subsume_or_strengthen_def Let_def apply (refine_vcg strengthen_clause_wl_strengthen_clause case_subsumption_refine) subgoal unfolding subsume_or_strengthen_wl_pre_def by fast subgoal premises p using assms p(32-) unfolding p(1-31) by (auto simp: state_wl_l_def all_init_lits_of_wl_def all_init_lits_of_l_def all_init_atms_st_alt_def get_init_clss_l_def) subgoal unfolding in_pair_collect_simp by (auto simp: state_wl_l_def subsume_or_strengthen_pre_def strengthen_clause_pre_def intro!: strengthen_clause_wl_strengthen_clause[THEN order_trans] ASSERT_leI split: subsumption.splits) subgoal by (auto simp: state_wl_l_def subsume_or_strengthen_pre_def strengthen_clause_pre_def intro!: strengthen_clause_wl_strengthen_clause[THEN order_trans] split: subsumption.splits) subgoal by (auto simp: state_wl_l_def subsume_or_strengthen_pre_def strengthen_clause_pre_def no_lost_clause_in_WL_def intro!: strengthen_clause_wl_strengthen_clause[THEN order_trans] split: subsumption.splits) done definition forward_subsumption_one_wl_pre :: ‹nat ⇒ nat multiset ⇒ 'v twl_st_wl ⇒ bool› where ‹forward_subsumption_one_wl_pre = (λC cands S. (∃S'. (S, S') ∈ state_wl_l None ∧ no_lost_clause_in_WL S ∧ forward_subsumption_one_pre C cands S' ∧ literals_are_ℒ_i_n' S))› definition forward_subsumption_one_wl_inv :: ‹'v twl_st_wl ⇒ nat ⇒ nat multiset ⇒ nat multiset × 'v subsumption ⇒ bool› where ‹forward_subsumption_one_wl_inv = (λS C cands (i, x). (∃S'. (S, S') ∈ state_wl_l None ∧ forward_subsumption_one_inv C S' cands (i, x)))› definition forward_subsumption_one_wl_select where ‹forward_subsumption_one_wl_select C cands S = (λxs. C ∉# xs ∧ cands ∩# xs = {#} ∧ (∀D∈#xs. D ∈# dom_m (get_clauses_wl S) ⟶ (∀L∈ set (get_clauses_wl S ∝ D). undefined_lit (get_trail_wl S) L) ∧ (length (get_clauses_wl S ∝ D) ≤ length (get_clauses_wl S ∝ C))))› definition forward_subsumption_one_wl :: ‹nat ⇒ nat multiset ⇒ 'v twl_st_wl ⇒ ('v twl_st_wl × bool) nres› where ‹forward_subsumption_one_wl = (λC cands S₀ . do { ASSERT (forward_subsumption_one_wl_pre C cands S₀); ys ← SPEC (forward_subsumption_one_wl_select C cands S₀); (xs, s) ← WHILE_T⇗ forward_subsumption_one_wl_inv S₀ C ys ⇖ (λ(xs, s). xs ≠ {#} ∧ s = NONE) (λ(xs, s). do { C' ← SPEC (λC'. C' ∈# xs); if C' ∉# dom_m (get_clauses_wl S₀) then RETURN (remove1_mset C' xs, s) else do { s ← subsume_clauses_match C' C (get_clauses_wl S₀); RETURN (remove1_mset C' xs, s) } }) (ys, NONE); S ← subsume_or_strengthen_wl C s S₀; ASSERT (literals_are_ℒ_i_n' S ∧ set_mset (all_init_lits_of_wl S) = set_mset (all_init_lits_of_wl S₀)); RETURN (S, s ≠ NONE) })› lemma forward_subsumption_one_wl: assumes SS': ‹(S, S') ∈ state_wl_l None› and ‹no_lost_clause_in_WL S› and ‹literals_are_ℒ_i_n' S› and cands: ‹(cands, cands') ∈ Id› shows ‹forward_subsumption_one_wl C cands S ≤ ⇓({(T, T'). (T, T') ∈ state_wl_l None ∧ get_watched_wl T = get_watched_wl S} ×_f bool_rel) (forward_subsumption_one C cands' S')› proof - have [refine0]: ‹(xs, ys) ∈ Id ⟹ ((xs, NONE), (ys, NONE)) ∈ {(a,b). a = b ∧ b ⊆# ys} ×_f Id› (is ‹_ ⟹ _ ∈ ?loop›) for xs ys :: ‹nat multiset› by auto have subsume_clauses_match_pre: ‹subsume_clauses_match_pre C' C (get_clauses_wl S)› if pre: ‹forward_subsumption_one_pre C cands' S'› and ‹forward_subsumption_one_wl_pre C cands S› and xs_ys: ‹(ys, xs) ∈ Id› and ys: ‹ys ∈ Collect (forward_subsumption_one_wl_select C cands S)› and xs: ‹xs ∈ Collect (forward_subsumption_one_select C cands' S')› and xx': ‹(x, x') ∈ ?loop xs› and x: ‹case x of (xs, s) ⇒ xs ≠ {#} ∧ s = NONE› and x': ‹case x' of (xs, s) ⇒ xs ≠ {#} ∧ s = NONE› and ‹forward_subsumption_one_wl_inv S C xs0 x› and inv: ‹forward_subsumption_one_inv C S' ys0 x'› and st: ‹x' = (x1, x2)› ‹x = (x1a, x2a)› and C': ‹(C', C'a) ∈ nat_rel› ‹C' ∈ {C'. C' ∈# x1a}› ‹C'a ∈ {C'. C' ∈# x1}› ‹¬ C' ∉# dom_m (get_clauses_wl S)› ‹¬ C'a ∉# dom_m (get_clauses_l S')› for C C' C'a x x' x1 x2 x1a x2a xs ys ys0 xs0 proof - obtain S'' where inv: ‹forward_subsumption_one_inv C S' ys0 (x1a, x2a)› and ‹C ≠ 0› and S'S'': ‹(S', S'') ∈ twl_st_l None› and struct: ‹twl_struct_invs S''› and list_invs: ‹twl_list_invs S'› and C_dom: ‹C ∈# dom_m (get_clauses_wl S)› using inv C' pre assms xx' unfolding forward_subsumption_one_wl_inv_def prod.simps forward_subsumption_one_wl_pre_def forward_subsumption_one_pre_def st by auto have ‹length (get_clauses_wl S ∝ C') ≤ length (get_clauses_wl S ∝ C)› and k_dom: ‹C' ∈# dom_m (get_clauses_wl S)› using xs_ys xx' xs C' SS' unfolding C' st forward_subsumption_one_select_def by (auto) moreover have ‹distinct (get_clauses_wl S ∝ C)› ‹distinct (get_clauses_wl S ∝ C')› ‹¬tautology (mset (get_clauses_wl S ∝ C))› ‹¬tautology (mset (get_clauses_wl S ∝ C'))› using C' SS' S'S'' struct k_dom list_invs C_dom unfolding C' st twl_list_invs_def by (auto simp: subsume_or_strengthen_pre_def state_wl_l_def twl_struct_invs_def pcdcl_all_struct_invs_def cdcl_W_restart_mset.cdcl_W_all_struct_inv_def cdcl_W_restart_mset.distinct_cdcl_W_state_alt_def ran_m_def add_mset_eq_add_mset split: subsumption.splits dest!: multi_member_split) ultimately show ?thesis using C_dom C' SS' unfolding subsume_clauses_match_pre_def by auto qed show ?thesis unfolding forward_subsumption_one_wl_def forward_subsumption_one_def apply (refine_vcg subsume_clauses_match[unfolded Down_id_eq]) subgoal using assms unfolding forward_subsumption_one_wl_pre_def by fast subgoal using assms unfolding forward_subsumption_one_wl_select_def forward_subsumption_one_select_def by auto subgoal for ys xs x x' using assms unfolding forward_subsumption_one_wl_inv_def case_prod_beta by (cases x; cases x') fastforce subgoal by auto subgoal by auto subgoal using assms by auto subgoal by auto apply (rule subsume_clauses_match_pre; assumption?) subgoal using assms by auto subgoal by auto apply (rule subsume_or_strengthen_wl_subsume_or_strengthen) subgoal by auto subgoal by auto subgoal using assms by auto subgoal using assms unfolding forward_subsumption_one_inv_def subsume_or_strengthen_pre_def prod.simps apply - apply normalize_goal+ by (simp add: try_to_subsume_def forward_subsumption_one_inv_def subsume_or_strengthen_pre_def split: subsumption.splits) subgoal unfolding forward_subsumption_one_wl_pre_def forward_subsumption_one_pre_def by normalize_goal+ auto subgoal using assms(3) SS' by (force simp: literals_are_ℒ_i_n'_def blits_in_ℒ_i_n'_def watched_by_alt_def) subgoal using SS' by auto subgoal by auto done qed definition try_to_forward_subsume_wl_pre :: ‹nat ⇒ nat multiset ⇒ 'v twl_st_wl ⇒ bool› where ‹try_to_forward_subsume_wl_pre C cands S = (∃T. (S,T)∈state_wl_l None ∧ try_to_forward_subsume_pre C cands T ∧ literals_are_ℒ_i_n' S ∧ no_lost_clause_in_WL S)› definition try_to_forward_subsume_wl_inv :: ‹_› where ‹try_to_forward_subsume_wl_inv S cands C = (λ(i,break, T). (∃S' T'. (S,S')∈state_wl_l None ∧ (T,T')∈state_wl_l None ∧ no_lost_clause_in_WL S ∧ try_to_forward_subsume_inv S' cands C (i, break, T') ∧ get_watched_wl T = get_watched_wl S ∧ literals_are_ℒ_i_n' S)) › definition try_to_forward_subsume_wl :: ‹nat ⇒ nat multiset ⇒ 'v twl_st_wl ⇒ 'v twl_st_wl nres› where ‹try_to_forward_subsume_wl C cands S = do { ASSERT (try_to_forward_subsume_wl_pre C cands S); n ← RES {_::nat. True}; ebreak ← RES {_::bool. True}; (_, _, S) ← WHILE_T⇗ try_to_forward_subsume_wl_inv S cands C⇖ (λ(i, break, S). ¬break ∧ i < n) (λ(i, break, S). do { (S, subs) ← forward_subsumption_one_wl C cands S; ebreak ← RES {_::bool. True}; RETURN (i+1, subs ∨ ebreak, S) }) (0, ebreak, S); RETURN S } › lemma cdcl_twl_inprocessing_l_dom_get_clauses_mono: ‹cdcl_twl_inprocessing_l S T ⟹ set_mset (dom_m (get_clauses_l T)) ⊆ set_mset (dom_m (get_clauses_l S))› by (cases rule: cdcl_twl_inprocessing_l.cases) (auto simp: cdcl_twl_unitres_l.simps cdcl_twl_unitres_true_l.simps cdcl_twl_subsumed_l.simps cdcl_twl_subresolution_l.simps cdcl_twl_pure_remove_l.simps dest: in_diffD) lemma rtranclp_cdcl_twl_inprocessing_l_dom_get_clauses_mono: ‹cdcl_twl_inprocessing_l^*^* S T ⟹ set_mset (dom_m (get_clauses_l T)) ⊆ set_mset (dom_m (get_clauses_l S))› by (induction rule: rtranclp_induct) (auto dest: cdcl_twl_inprocessing_l_dom_get_clauses_mono) lemma try_to_forward_subsume_wl_inv_no_lost_clause_in_WLD: assumes ‹try_to_forward_subsume_wl_inv S cands C (i, break, T)› shows ‹no_lost_clause_in_WL T› and ‹literals_are_ℒ_i_n' T› proof - obtain S' T' where SS': ‹(S, S') ∈ state_wl_l None› and TT': ‹(T, T') ∈ state_wl_l None› and lost: ‹no_lost_clause_in_WL S› ‹try_to_forward_subsume_inv S' cands C (i, break, T')› and S'T': ‹cdcl_twl_inprocessing_l^*^* S' T'› and w: ‹get_watched_wl T = get_watched_wl S› and lits: ‹literals_are_ℒ_i_n' S› using assms unfolding try_to_forward_subsume_wl_inv_def prod.simps try_to_forward_subsume_inv_def by blast have ‹set_mset (dom_m (get_clauses_wl T)) ⊆ set_mset (dom_m (get_clauses_wl S))› using SS' TT' rtranclp_cdcl_twl_inprocessing_l_dom_get_clauses_mono[OF S'T'] by auto moreover have eq: ‹set_mset (all_init_lits_of_l S') = set_mset (all_init_lits_of_l T')› using S'T' rtranclp_cdcl_twl_inprocessing_l_all_init_lits_of_l by blast ultimately show ‹no_lost_clause_in_WL T› using lost SS' TT' w unfolding no_lost_clause_in_WL_def by (auto simp: watched_by_alt_def) show ‹literals_are_ℒ_i_n' T› using eq SS' TT' rtranclp_cdcl_twl_inprocessing_l_all_learned_lits_of_l[OF S'T'] w lits unfolding literals_are_ℒ_i_n'_def by (auto simp: blits_in_ℒ_i_n'_def watched_by_alt_def) qed lemma try_to_forward_subsume_wl: assumes SS': ‹(S, S') ∈ state_wl_l None› and ‹no_lost_clause_in_WL S› and ‹(C,C')∈nat_rel› and ‹literals_are_ℒ_i_n' S› and ‹(cands, cands') ∈Id› shows ‹try_to_forward_subsume_wl C cands S ≤ ⇓({(T, T'). (T, T') ∈ state_wl_l None ∧ get_watched_wl T = get_watched_wl S}) (try_to_forward_subsume C' cands' S')› proof - have CC': ‹C' = C› using assms by auto have [refine0]: ‹(xs, ys) ∈ Id ⟹ (ebreak, ebreak') ∈ Id ⟹ ((xs, ebreak, S), (ys, ebreak', S')) ∈ Id ×_r bool_rel ×_r {(U,V). (U,V)∈ state_wl_l None ∧ get_watched_wl U = get_watched_wl S}› (is ‹_ ⟹ _ ⟹ _ ∈ ?loop›) for xs ys :: ‹nat› and ebreak ebreak' using assms by auto show ?thesis unfolding try_to_forward_subsume_wl_def try_to_forward_subsume_def CC' apply (refine_vcg simplify_clause_with_unit_st_wl_simplify_clause_with_unit_st forward_subsumption_one_wl) subgoal using assms unfolding try_to_forward_subsume_wl_pre_def by fast subgoal using assms by auto subgoal for xs xsa ebreak ebreak' x x' using assms unfolding try_to_forward_subsume_wl_inv_def case_prod_beta prod_rel_fst_snd_iff by (rule_tac x=S' in exI, rule_tac x=‹snd (snd x')› in exI) (auto) subgoal by auto subgoal by auto subgoal by (auto dest: try_to_forward_subsume_wl_inv_no_lost_clause_in_WLD) subgoal by (auto dest: try_to_forward_subsume_wl_inv_no_lost_clause_in_WLD) subgoal using assms by auto subgoal by auto subgoal by auto done qed definition forward_subsumption_all_wl_pre :: ‹'v twl_st_wl ⇒ bool› where ‹forward_subsumption_all_wl_pre S = (∃T. (S, T) ∈ state_wl_l None ∧ forward_subsumption_all_pre T ∧ literals_are_ℒ_i_n' S)› definition forward_subsumption_all_wl_inv :: ‹'v twl_st_wl ⇒ nat multiset ⇒ nat multiset × 'v twl_st_wl ⇒ bool› where ‹forward_subsumption_all_wl_inv = (λS cands (xs, s). (∃T s'. (S, T) ∈ state_wl_l None ∧ (s, s') ∈ state_wl_l None ∧ forward_subsumption_all_inv T (xs, s') ∧ no_lost_clause_in_WL S ∧ get_watched_wl s = get_watched_wl S ∧ literals_are_ℒ_i_n' S))› definition forward_subsumption_wl_all_cands where ‹forward_subsumption_wl_all_cands S xs ⟷ xs ⊆# dom_m (get_clauses_wl S) ∧ (∀C∈#xs. (∀L∈set (get_clauses_wl S ∝ C). undefined_lit (get_trail_wl S) L) ∧ length (get_clauses_wl S ∝ C) > 2)› definition forward_subsumption_all_wl :: ‹'v twl_st_wl ⇒ 'v twl_st_wl nres› where ‹forward_subsumption_all_wl = (λS. do { ASSERT (forward_subsumption_all_wl_pre S); xs ← SPEC (forward_subsumption_wl_all_cands S); (xs, S) ← WHILE_T⇗ forward_subsumption_all_wl_inv S xs ⇖ (λ(xs, S). xs ≠ {#} ∧ get_conflict_wl S = None) (λ(xs, S). do { C ← SPEC (λC. C ∈# xs); T ← try_to_forward_subsume_wl C xs S; ASSERT (∀D∈#remove1_mset C xs. get_clauses_wl T ∝ D = get_clauses_wl S ∝ D); RETURN (remove1_mset C xs, T) }) (xs, S); RETURN S } )› definition forward_subsume_wl_needed :: ‹'v twl_st_wl ⇒ bool nres› where ‹forward_subsume_wl_needed S = SPEC (λ_. True)› definition forward_subsume_wl :: ‹'v twl_st_wl ⇒ 'v twl_st_wl nres› where ‹forward_subsume_wl S = do { ASSERT (forward_subsumption_all_wl_pre S); b ← forward_subsume_wl_needed S; if b then forward_subsumption_all_wl S else RETURN S }› lemma assumes ‹forward_subsumption_all_wl_inv S cands (xs, T)› shows forward_subsumption_all_wl_inv_no_lost_clause_in_WLD: ‹no_lost_clause_in_WL T› and forward_subsumption_all_wl_inv_literals_are_ℒ_i_n'D: ‹literals_are_ℒ_i_n' T› proof - obtain S' T' where SS': ‹(S, S') ∈ state_wl_l None› and TT': ‹(T, T') ∈ state_wl_l None› and lost: ‹no_lost_clause_in_WL S› and S'T': ‹cdcl_twl_inprocessing_l^*^* S' T'› and w: ‹get_watched_wl T = get_watched_wl S› and lits: ‹literals_are_ℒ_i_n' S› using assms unfolding forward_subsumption_all_wl_inv_def prod.simps forward_subsumption_all_inv_def by blast have ‹set_mset (dom_m (get_clauses_wl T)) ⊆ set_mset (dom_m (get_clauses_wl S))› using SS' TT' rtranclp_cdcl_twl_inprocessing_l_dom_get_clauses_mono[OF S'T'] by auto moreover have eq: ‹set_mset (all_init_lits_of_l S') = set_mset (all_init_lits_of_l T')› using S'T' rtranclp_cdcl_twl_inprocessing_l_all_init_lits_of_l by blast ultimately show ‹no_lost_clause_in_WL T› using lost SS' TT' w unfolding no_lost_clause_in_WL_def by (auto simp: watched_by_alt_def) show ‹literals_are_ℒ_i_n' T› using eq SS' TT' rtranclp_cdcl_twl_inprocessing_l_all_learned_lits_of_l[OF S'T'] w lits unfolding literals_are_ℒ_i_n'_def by (auto simp: blits_in_ℒ_i_n'_def watched_by_alt_def) qed lemma forward_subsumption_all_wl_inv_alt_def: ‹forward_subsumption_all_wl_inv = (λS cands (xs, s). (∃T s'. (S, T) ∈ state_wl_l None ∧ (s, s') ∈ state_wl_l None ∧ forward_subsumption_all_inv T (xs, s') ∧ no_lost_clause_in_WL S ∧ get_watched_wl s = get_watched_wl S ∧ literals_are_ℒ_i_n' S ∧ literals_are_ℒ_i_n' s))› using forward_subsumption_all_wl_inv_literals_are_ℒ_i_n'D unfolding forward_subsumption_all_wl_inv_def by fast lemma forward_subsumption_all_wl: assumes SS': ‹(S, S') ∈ state_wl_l None› and lost: ‹correct_watching'_leaking_bin S› and lits: ‹literals_are_ℒ_i_n' S› shows ‹forward_subsumption_all_wl S ≤ ⇓({(T, T'). (T, T') ∈ state_wl_l None ∧ get_watched_wl T = get_watched_wl S ∧ no_lost_clause_in_WL T ∧ literals_are_ℒ_i_n' T}) (forward_subsumption_all S')› proof - have lost: ‹no_lost_clause_in_WL S› if pre: ‹forward_subsumption_all_pre S'› proof - obtain S'' where S'S'': ‹(S', S'') ∈ twl_st_l None› and struct_invs: ‹twl_struct_invs S''› and ‹twl_list_invs S'› ‹cdcl_W_restart_mset.cdcl_W_learned_clauses_entailed_by_init (state_W_of S'')› and ‹set (get_all_mark_of_propagated (get_trail_l S')) ⊆ {0}› and ‹clauses_to_update_l S' = {#}› and ‹count_decided (get_trail_l S') = 0› using pre unfolding forward_subsumption_all_pre_def by fast have ‹correct_watching'_nobin S› using assms(2) by (cases S) (auto simp: correct_watching'_leaking_bin.simps correct_watching'_nobin.simps) then show ?thesis using correct_watching'_nobin_clauses_pointed_to0[OF assms(1) _ assms(3) S'S'' struct_invs] by fast qed then have [refine0]: ‹(xs, ys) ∈ Id ⟹ forward_subsumption_all_pre S' ⟹ forward_subsumption_all_inv S' (ys, S') ⟹ forward_subsumption_all_wl_inv S xs (xs, S)› for xs ys :: ‹nat multiset› using assms unfolding forward_subsumption_all_wl_inv_def case_prod_beta prod_rel_fst_snd_iff by (rule_tac x=S' in exI, rule_tac x=‹S'› in exI) auto then have [refine0]: ‹(xs, ys) ∈ Id ⟹ ((xs, S), (ys, S')) ∈ Id ×_f {(U,V). (U,V)∈ state_wl_l None ∧ get_watched_wl U = get_watched_wl S}› (is ‹_ ⟹ _ ∈ ?loop›) for xs ys :: ‹nat multiset› using assms by auto show ?thesis unfolding forward_subsumption_all_wl_def forward_subsumption_all_def apply (refine_vcg simplify_clause_with_unit_st_wl_simplify_clause_with_unit_st forward_subsumption_one_wl try_to_forward_subsume_wl WHILEIT_refine_with_all_loopinvariants) subgoal using assms unfolding forward_subsumption_all_wl_pre_def by fast subgoal using assms unfolding forward_subsumption_all_cands_def forward_subsumption_wl_all_cands_def by auto subgoal for xs xsa x x' using assms lost unfolding forward_subsumption_all_wl_inv_def case_prod_beta prod_rel_fst_snd_iff by (rule_tac x=S' in exI, rule_tac x=‹snd x'› in exI; auto) subgoal by auto subgoal by auto subgoal by auto subgoal by (auto dest: forward_subsumption_all_wl_inv_no_lost_clause_in_WLD forward_subsumption_all_wl_inv_literals_are_ℒ_i_n'D) subgoal by (auto dest: forward_subsumption_all_wl_inv_no_lost_clause_in_WLD forward_subsumption_all_wl_inv_literals_are_ℒ_i_n'D) subgoal by auto subgoal by auto subgoal by auto subgoal by (auto dest: forward_subsumption_all_wl_inv_no_lost_clause_in_WLD forward_subsumption_all_wl_inv_literals_are_ℒ_i_n'D) done qed lemma forward_subsume_wl: assumes SS': ‹(S, S') ∈ state_wl_l None› and lost: ‹correct_watching'_leaking_bin S› and lits: ‹literals_are_ℒ_i_n' S› shows ‹forward_subsume_wl S ≤ ⇓({(T, T'). (T, T') ∈ state_wl_l None ∧ get_watched_wl T = get_watched_wl S ∧ no_lost_clause_in_WL T ∧ literals_are_ℒ_i_n' T}) (forward_subsume_l S')› proof - have lost: ‹no_lost_clause_in_WL S› if pre: ‹forward_subsumption_all_pre S'› proof - obtain S'' where S'S'': ‹(S', S'') ∈ twl_st_l None› and struct_invs: ‹twl_struct_invs S''› and ‹twl_list_invs S'› ‹cdcl_W_restart_mset.cdcl_W_learned_clauses_entailed_by_init (state_W_of S'')› and ‹set (get_all_mark_of_propagated (get_trail_l S')) ⊆ {0}› and ‹clauses_to_update_l S' = {#}› and ‹count_decided (get_trail_l S') = 0› using pre unfolding forward_subsumption_all_pre_def by fast have ‹correct_watching'_nobin S› using assms(2) by (cases S) (auto simp: correct_watching'_leaking_bin.simps correct_watching'_nobin.simps) then show ?thesis using correct_watching'_nobin_clauses_pointed_to0[OF assms(1) _ assms(3) S'S'' struct_invs] by fast qed show ?thesis unfolding forward_subsume_wl_def forward_subsume_l_def forward_subsumption_needed_l_def forward_subsume_wl_needed_def apply (refine_vcg forward_subsumption_all_wl) subgoal using assms unfolding forward_subsumption_all_wl_pre_def by fast subgoal by auto subgoal using assms by auto subgoal using assms by auto subgoal using assms by auto subgoal using assms lost by simp done qed lemma cdcl_twl_inprocessing_l_dom_get_clauses_l_mono: ‹cdcl_twl_inprocessing_l S T ⟹ dom_m (get_clauses_l T) ⊆# dom_m (get_clauses_l S)› by (auto simp: cdcl_twl_inprocessing_l.simps cdcl_twl_unitres_true_l.simps cdcl_twl_unitres_l.simps cdcl_twl_subsumed_l.simps cdcl_twl_subresolution_l.simps add_mset_eq_add_mset cdcl_twl_pure_remove_l.simps dest!: multi_member_split) lemma rtranclp_cdcl_twl_inprocessing_l_dom_get_clauses_l_mono: ‹cdcl_twl_inprocessing_l^*^* S T ⟹ dom_m (get_clauses_l T) ⊆# dom_m (get_clauses_l S)› by (induction rule: rtranclp_induct) (auto dest: cdcl_twl_inprocessing_l_dom_get_clauses_l_mono) subsection ‹Pure literal deletion› definition propagate_pure_wl_pre:: ‹'v literal ⇒ 'v twl_st_wl ⇒ bool› where ‹propagate_pure_wl_pre L S ⟷ (∃S'. (S, S') ∈ state_wl_l None ∧ propagate_pure_l_pre L S' ∧ no_lost_clause_in_WL S ∧ literals_are_ℒ_i_n' S)› definition propagate_pure_bt_wl :: ‹'v literal ⇒ 'v twl_st_wl ⇒ 'v twl_st_wl nres› where ‹propagate_pure_bt_wl = (λL (M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, Q, WS). do { ASSERT(propagate_pure_wl_pre L (M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, Q, WS)); M ← cons_trail_propagate_l L 0 M; RETURN (M, N, D, NE, UE, add_mset {#L#} NEk, UEk, NS, US, N0, U0, add_mset (-L) Q, WS)})› lemma propagate_pure_bt_wl_propagate_pure_bt_l: assumes ‹(S,S')∈ state_wl_l None› and ‹no_lost_clause_in_WL S› ‹literals_are_ℒ_i_n' S› ‹(L,L')∈ Id› shows ‹propagate_pure_bt_wl L S ≤⇓{(S,T). no_lost_clause_in_WL S ∧ (S,T)∈ state_wl_l None ∧ literals_are_ℒ_i_n' S} (propagate_pure_bt_l L' S')› proof - have K: ‹cons_trail_propagate_l L 0 a = cons_trail_propagate_l L 0 b ⟹ cons_trail_propagate_l L 0 a ≤⇓{(x,y). x = y ∧ y = Propagated L 0 # a} (cons_trail_propagate_l L' 0 b)› for a b using assms unfolding cons_trail_propagate_l_def by refine_rcg auto show ?thesis unfolding propagate_pure_bt_wl_def propagate_pure_bt_l_def apply refine_rcg subgoal using assms unfolding propagate_pure_wl_pre_def apply - by (rule exI[of _ S']) fast apply (rule K) subgoal using assms by (auto simp: state_wl_l_def no_lost_clause_in_WL_def) subgoal using assms by (auto simp: state_wl_l_def propagate_pure_l_pre_def in_all_lits_of_mm_uminusD all_init_lits_of_wl_def all_init_lits_of_l_def get_init_clss_l_def simp: no_lost_clause_in_WL_def simp: literals_are_ℒ_i_n'_def all_lits_of_mm_add_mset all_lits_of_m_add_mset all_learned_lits_of_wl_def blits_in_ℒ_i_n'_def) done qed definition pure_literal_deletion_wl_pre where ‹pure_literal_deletion_wl_pre S ⟷ (∃S'. (S, S') ∈ state_wl_l None ∧ pure_literal_deletion_pre S' ∧ no_lost_clause_in_WL S ∧ literals_are_ℒ_i_n' S)› definition pure_literal_deletion_candidates_wl where ‹pure_literal_deletion_candidates_wl S = SPEC (λLs. set_mset Ls ⊆ set_mset (all_init_atms_st S))› definition pure_literal_deletion_wl_inv where ‹pure_literal_deletion_wl_inv S xs0 = (λ(T, xs). ∃S' T'. (S, S') ∈ state_wl_l None ∧ (T, T') ∈ state_wl_l None ∧ pure_literal_deletion_l_inv S' xs0 (T', xs) ∧ no_lost_clause_in_WL T ∧ literals_are_ℒ_i_n' T)› definition pure_literal_deletion_wl :: ‹('v literal ⇒ bool) ⇒ 'v twl_st_wl ⇒ 'v twl_st_wl nres› where ‹pure_literal_deletion_wl occs S = do { ASSERT (pure_literal_deletion_wl_pre S); let As = ⋃(set_mset ` set_mset (mset `# get_init_clss_wl S)); xs ← pure_literal_deletion_candidates_wl S; (S, xs) ← WHILE_T⇗pure_literal_deletion_wl_inv S xs⇖ (λ(S, xs). xs ≠ {#}) (λ(S, xs). do { L ← SPEC (λL. L ∈# xs); let A = (if occs (Pos L) ∧ ¬occs (Neg L) then Pos L else Neg L); if ¬occs (-A) ∧ undefined_lit (get_trail_wl S) A then do {S ← propagate_pure_bt_wl A S; RETURN (S, remove1_mset L xs)} else RETURN (S, remove1_mset L xs) }) (S, xs); RETURN S }› lemma pure_literal_deletion_wl_pure_literal_deletion_l: assumes ‹(S,S')∈ state_wl_l None› and ‹no_lost_clause_in_WL S› ‹literals_are_ℒ_i_n' S› ‹(occs, occs') ∈ Id› shows ‹pure_literal_deletion_wl occs S ≤⇓{(S,T). no_lost_clause_in_WL S ∧ (S,T)∈ state_wl_l None ∧ literals_are_ℒ_i_n' S} (pure_literal_deletion_l2 occs' S')› (is ‹_ ≤⇓ ?A _›) proof - have [refine0]: ‹(xs, ys) ∈ Id ⟹ ((S, xs), (S', ys)) ∈ ?A ×_f Id› for xs ys by (use assms in auto) have [refine0]: ‹pure_literal_deletion_candidates_wl S ≤ ⇓ Id (pure_literal_deletion_candidates S')› using assms by (auto simp: pure_literal_deletion_candidates_wl_def pure_literal_deletion_candidates_def all_init_atms_st_def all_init_atms_alt_def) show ?thesis unfolding pure_literal_deletion_wl_def pure_literal_deletion_l2_def apply (refine_rcg propagate_pure_bt_wl_propagate_pure_bt_l) subgoal using assms unfolding pure_literal_deletion_wl_pre_def by blast subgoal for xs xsa x x' using assms unfolding pure_literal_deletion_wl_inv_def case_prod_beta by (rule_tac x=S' in exI, rule_tac x=‹fst x'› in exI, case_tac x, case_tac x') auto subgoal by auto subgoal by auto subgoal by (subst twl_st_wl, use assms in auto) subgoal by auto subgoal unfolding pure_literal_deletion_wl_inv_def by blast subgoal by simp subgoal using assms by auto subgoal by auto subgoal by auto subgoal by auto done qed definition pure_literal_count_occs_clause_wl_invs :: ‹nat ⇒ 'v twl_st_wl ⇒ ('v literal ⇒ bool) ⇒ nat × ('v literal ⇒ bool) ⇒ bool› where ‹pure_literal_count_occs_clause_wl_invs C S occs = (λ(i, occs2). ∃S'. (S,S')∈state_wl_l None ∧ pure_literal_count_occs_l_clause_invs C S' occs (i, occs2))› definition pure_literal_count_occs_clause_wl_pre :: ‹nat ⇒ 'v twl_st_wl ⇒ _ ⇒ bool› where ‹pure_literal_count_occs_clause_wl_pre C S occs = (∃S'. (S,S')∈state_wl_l None ∧ pure_literal_count_occs_l_clause_pre C S' occs)› definition pure_literal_count_occs_clause_wl :: ‹nat ⇒ 'v twl_st_wl ⇒ _› where ‹pure_literal_count_occs_clause_wl C S occs = do { ASSERT (pure_literal_count_occs_clause_wl_pre C S occs); (i, occs) ← WHILE_T⇗pure_literal_count_occs_clause_wl_invs C S occs⇖ (λ(i, occs). i < length (get_clauses_wl S ∝ C)) (λ(i, occs). do { let L = get_clauses_wl S ∝ C ! i; let occs = occs (L := True); RETURN (i+1, occs) }) (0, occs); RETURN occs }› lemma pure_literal_count_occs_clause_wl_pure_literal_count_occs_l_clause: assumes ‹(S, S') ∈ state_wl_l None› ‹(C,C')∈nat_rel› ‹(occs, occs') ∈ Id› shows ‹pure_literal_count_occs_clause_wl C S occs ≤ ⇓Id (pure_literal_count_occs_l_clause C' S' occs')› proof - have [refine0]: ‹((0, occs), 0, occs') ∈ nat_rel ×_f Id› using assms by auto show ?thesis unfolding pure_literal_count_occs_clause_wl_def pure_literal_count_occs_l_clause_def apply (refine_vcg) subgoal using assms unfolding pure_literal_count_occs_clause_wl_pre_def by fast subgoal using assms unfolding pure_literal_count_occs_clause_wl_invs_def case_prod_beta prod.collapse by fastforce subgoal using assms by auto subgoal using assms by auto subgoal by auto done qed definition pure_literal_count_occs_wl_pre :: ‹_› where ‹pure_literal_count_occs_wl_pre S ⟷ (∃S'. (S, S') ∈ state_wl_l None ∧ no_lost_clause_in_WL S ∧ literals_are_ℒ_i_n' S ∧ pure_literal_count_occs_l_pre S')› definition pure_literal_count_occs_wl_inv :: ‹_› where ‹pure_literal_count_occs_wl_inv S T ⟷ (∃S' T'. (S,S')∈ state_wl_l None ∧ (T, T') ∈ state_wl_l None ∧ cdcl_twl_inprocessing_l S' T')› definition pure_literal_count_occs_wl :: ‹'v twl_st_wl ⇒ _› where ‹pure_literal_count_occs_wl S = do { ASSERT (pure_literal_count_occs_wl_pre S); xs ← SPEC (λxs. distinct_mset xs ∧ (∀C∈#dom_m (get_clauses_wl S). irred (get_clauses_wl S) C ⟶ C ∈# xs)); abort ← RES (UNIV :: bool set); let occs = (λ_. False); (_, occs, abort) ← WHILE_T(λ(A, occs, abort). A ≠ {#} ∧ ¬abort) (λ(A, occs, abort). do { ASSERT (A ≠ {#}); C ← SPEC (λC. C ∈# A); if (C ∈# dom_m (get_clauses_wl S) ∧ irred (get_clauses_wl S) C) then do { occs ← pure_literal_count_occs_clause_wl C S occs; abort ← RES (UNIV :: bool set); RETURN (remove1_mset C A, occs, abort) } else RETURN (remove1_mset C A, occs, abort) }) (xs, occs, abort); RETURN (abort, occs) }› lemma pure_literal_count_occs_wl_pure_literal_count_occs_l: assumes ‹(S, S') ∈ state_wl_l None› ‹no_lost_clause_in_WL S› ‹literals_are_ℒ_i_n' S› shows ‹pure_literal_count_occs_wl S ≤ ⇓Id (pure_literal_count_occs_l S')› proof - have [refine0]: ‹(xs, xsa)∈ Id ⟹ (abort, abort') ∈ bool_rel ⟹ ((xs, λ_. False, abort), xsa, λ_. False, abort') ∈ Id ×_r Id ×_r bool_rel› for xs xsa abort abort' by auto show ?thesis unfolding pure_literal_count_occs_wl_def pure_literal_count_occs_l_def apply (refine_vcg pure_literal_count_occs_clause_wl_pure_literal_count_occs_l_clause) subgoal using assms unfolding pure_literal_count_occs_wl_pre_def by fast subgoal using assms by auto subgoal using assms by auto subgoal by auto subgoal by auto subgoal by auto subgoal using assms by auto subgoal using assms by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto done qed definition pure_literal_elimination_round_wl_pre where ‹pure_literal_elimination_round_wl_pre S ⟷ (∃T. (S, T) ∈ state_wl_l None ∧ pure_literal_elimination_round_pre T)› definition pure_literal_elimination_round_wl where ‹pure_literal_elimination_round_wl S = do { ASSERT (pure_literal_elimination_round_wl_pre S); S ← simplify_clauses_with_units_st_wl S; if get_conflict_wl S = None then do { (abort, occs) ← pure_literal_count_occs_wl S; if ¬abort then pure_literal_deletion_wl occs S else RETURN S} else RETURN S }› lemma pure_literal_elimination_round_wl_pure_literal_elimination_round_l: assumes ‹(S, S') ∈ state_wl_l None› ‹no_lost_clause_in_WL S› ‹literals_are_ℒ_i_n' S› shows ‹pure_literal_elimination_round_wl S ≤ ⇓{(S,T). no_lost_clause_in_WL S ∧ (S,T)∈ state_wl_l None ∧ literals_are_ℒ_i_n' S} (pure_literal_elimination_round S')› proof - show ?thesis unfolding pure_literal_elimination_round_wl_def pure_literal_elimination_round_def apply (refine_vcg simplify_clauses_with_units_st_wl_simplify_clause_with_units_st2 pure_literal_count_occs_wl_pure_literal_count_occs_l pure_literal_deletion_wl_pure_literal_deletion_l) subgoal using assms unfolding pure_literal_elimination_round_wl_pre_def by fast subgoal using assms by fast subgoal using assms by fast subgoal using assms by fast subgoal by auto subgoal by auto subgoal by blast subgoal by auto subgoal by auto subgoal by auto subgoal by blast subgoal by auto subgoal by auto subgoal by blast subgoal by blast done qed definition pure_literal_elimination_wl_pre where ‹pure_literal_elimination_wl_pre S ⟷ (∃T. (S, T) ∈ state_wl_l None ∧ pure_literal_elimination_l_pre T ∧ no_lost_clause_in_WL S ∧ literals_are_ℒ_i_n' S)› definition pure_literal_elimination_wl_inv where ‹pure_literal_elimination_wl_inv S max_rounds = (λ(U,m,abort). ∃T U'. (S, T) ∈ state_wl_l None ∧ (U, U') ∈ state_wl_l None ∧ no_lost_clause_in_WL U ∧ literals_are_ℒ_i_n' U ∧ pure_literal_elimination_l_inv T max_rounds (U',m,abort))› definition pure_literal_elimination_wl :: ‹_› where ‹pure_literal_elimination_wl S = do { ASSERT (pure_literal_elimination_wl_pre S); max_rounds ← RES (UNIV :: nat set); (S, _, _) ← WHILE_T⇗pure_literal_elimination_wl_inv S max_rounds⇖ (λ(S, m, abort). m < max_rounds ∧ ¬abort) (λ(S, m, abort). do { S ← pure_literal_elimination_round_wl S; abort ← RES (UNIV :: bool set); RETURN (S, m+1, abort) }) (S, 0, False); RETURN S }› lemma pure_literal_elimination_wl: assumes ‹(S, S') ∈ state_wl_l None› ‹no_lost_clause_in_WL S› ‹literals_are_ℒ_i_n' S› shows ‹pure_literal_elimination_wl S ≤ ⇓{(S,T). no_lost_clause_in_WL S ∧ (S,T)∈ state_wl_l None ∧ literals_are_ℒ_i_n' S} (pure_literal_elimination_l S')› proof - have [refine0]: ‹pure_literal_elimination_l_pre S' ⟹ ((S, 0, False), S', 0, False) ∈ {(S,T). no_lost_clause_in_WL S ∧ (S,T)∈ state_wl_l None ∧ literals_are_ℒ_i_n' S} ×_r nat_rel ×_r bool_rel› using assms by auto show ?thesis unfolding pure_literal_elimination_wl_def pure_literal_elimination_l_def apply (refine_vcg pure_literal_elimination_round_wl_pure_literal_elimination_round_l) subgoal using assms unfolding pure_literal_elimination_wl_pre_def by blast subgoal for max_rounds max_roundsa x x' using assms unfolding pure_literal_elimination_wl_inv_def case_prod_beta prod_rel_fst_snd_iff apply - by (rule exI[of _ S'], rule exI[of _ ‹fst x'›]) auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto done qed definition pure_literal_eliminate_wl_needed :: ‹_› where ‹pure_literal_eliminate_wl_needed S = SPEC (λ_. True)› definition pure_literal_eliminate_wl :: ‹_› where ‹pure_literal_eliminate_wl S = do { ASSERT (pure_literal_elimination_wl_pre S); b ← pure_literal_eliminate_wl_needed S; if b then pure_literal_elimination_wl S else RETURN S }› lemma pure_literal_eliminate_wl: assumes ‹(S, S') ∈ state_wl_l None› ‹no_lost_clause_in_WL S› ‹literals_are_ℒ_i_n' S› shows ‹pure_literal_eliminate_wl S ≤ ⇓{(S,T). no_lost_clause_in_WL S ∧ (S,T)∈ state_wl_l None ∧ literals_are_ℒ_i_n' S} (pure_literal_eliminate_l S')› unfolding pure_literal_eliminate_wl_def pure_literal_eliminate_l_def pure_literal_eliminate_wl_needed_def pure_literal_elimination_l_needed_def apply (refine_vcg pure_literal_elimination_wl) subgoal using assms unfolding pure_literal_elimination_wl_pre_def by blast subgoal by auto subgoal using assms by auto subgoal using assms by auto subgoal using assms by auto subgoal using assms by auto done end

Theory Watched_Literals_Watch_List_Inprocessing