theory Watched_Literals_Watch_List_Domain imports Watched_Literals_Watch_List begin text ‹We refine the implementation by adding a ∗‹domain› on the literals› subsection ‹State Conversion› subsubsection ‹Functions and Types:› type_synonym ann_lits_l = ‹(nat, nat) ann_lits› type_synonym clauses_to_update_ll = ‹nat list› subsection ‹Refinement› subsubsection ‹Set of all literals of the problem› definition all_lits :: ‹('a, 'v literal list × 'b) fmap ⇒ 'v literal multiset multiset ⇒ 'v literal multiset› where ‹all_lits S NUE = all_lits_of_mm ((λC. mset (fst C)) `# ran_m S + NUE)› abbreviation all_lits_st :: ‹'v twl_st_wl ⇒ 'v literal multiset› where ‹all_lits_st S ≡ all_lits (get_clauses_wl S) (get_unit_clauses_wl S)› definition all_atms :: ‹_ ⇒ _ ⇒ 'v multiset› where ‹all_atms N NUE = atm_of `# all_lits N NUE› abbreviation all_atms_st :: ‹'v twl_st_wl ⇒ 'v multiset› where ‹all_atms_st S ≡ atm_of `# all_lits_st S› text ‹We start in a context where we have an initial set of atoms. We later extend the locale to include a bound on the largest atom (in order to generate more efficient code). › context fixes 𝒜⇩i⇩n :: ‹nat multiset› begin text ‹This is the ∗‹completion› of \<^term>‹𝒜⇩i⇩n›, containing the positive and the negation of every literal of \<^term>‹𝒜⇩i⇩n›:› definition ℒ⇩a⇩l⇩l where ‹ℒ⇩a⇩l⇩l = poss 𝒜⇩i⇩n + negs 𝒜⇩i⇩n› lemma atms_of_ℒ⇩a⇩l⇩l_𝒜⇩i⇩n: ‹atms_of ℒ⇩a⇩l⇩l = set_mset 𝒜⇩i⇩n› unfolding ℒ⇩a⇩l⇩l_def by (auto simp: atms_of_def image_Un image_image) definition is_ℒ⇩a⇩l⇩l :: ‹nat literal multiset ⇒ bool› where ‹is_ℒ⇩a⇩l⇩l S ⟷ set_mset ℒ⇩a⇩l⇩l = set_mset S› definition literals_are_in_ℒ⇩i⇩n :: ‹nat clause ⇒ bool› where ‹literals_are_in_ℒ⇩i⇩n C ⟷ set_mset (all_lits_of_m C) ⊆ set_mset ℒ⇩a⇩l⇩l› lemma literals_are_in_ℒ⇩i⇩n_empty[simp]: ‹literals_are_in_ℒ⇩i⇩n {#}› by (auto simp: literals_are_in_ℒ⇩i⇩n_def) lemma in_ℒ⇩a⇩l⇩l_atm_of_in_atms_of_iff: ‹x ∈# ℒ⇩a⇩l⇩l ⟷ atm_of x ∈ atms_of ℒ⇩a⇩l⇩l› by (cases x) (auto simp: ℒ⇩a⇩l⇩l_def atms_of_def atm_of_eq_atm_of image_Un image_image) lemma literals_are_in_ℒ⇩i⇩n_add_mset: ‹literals_are_in_ℒ⇩i⇩n (add_mset L A) ⟷ literals_are_in_ℒ⇩i⇩n A ∧ L ∈# ℒ⇩a⇩l⇩l› by (auto simp: literals_are_in_ℒ⇩i⇩n_def all_lits_of_m_add_mset in_ℒ⇩a⇩l⇩l_atm_of_in_atms_of_iff) lemma literals_are_in_ℒ⇩i⇩n_mono: assumes N: ‹literals_are_in_ℒ⇩i⇩n D'› and D: ‹D ⊆# D'› shows ‹literals_are_in_ℒ⇩i⇩n D› proof - have ‹set_mset (all_lits_of_m D) ⊆ set_mset (all_lits_of_m D')› using D by (auto simp: in_all_lits_of_m_ain_atms_of_iff atm_iff_pos_or_neg_lit) then show ?thesis using N unfolding literals_are_in_ℒ⇩i⇩n_def by fast qed lemma literals_are_in_ℒ⇩i⇩n_sub: ‹literals_are_in_ℒ⇩i⇩n y ⟹ literals_are_in_ℒ⇩i⇩n (y - z)› using literals_are_in_ℒ⇩i⇩n_mono[of y ‹y - z›] by auto lemma all_lits_of_m_subset_all_lits_of_mmD: ‹a ∈# b ⟹ set_mset (all_lits_of_m a) ⊆ set_mset (all_lits_of_mm b)› by (auto simp: all_lits_of_m_def all_lits_of_mm_def) lemma all_lits_of_m_remdups_mset: ‹set_mset (all_lits_of_m (remdups_mset N)) = set_mset (all_lits_of_m N)› by (auto simp: all_lits_of_m_def) lemma literals_are_in_ℒ⇩i⇩n_remdups[simp]: ‹literals_are_in_ℒ⇩i⇩n (remdups_mset N) = literals_are_in_ℒ⇩i⇩n N› by (auto simp: literals_are_in_ℒ⇩i⇩n_def all_lits_of_m_remdups_mset) lemma uminus_𝒜⇩i⇩n_iff: ‹- L ∈# ℒ⇩a⇩l⇩l ⟷ L ∈# ℒ⇩a⇩l⇩l› by (simp add: in_ℒ⇩a⇩l⇩l_atm_of_in_atms_of_iff) definition literals_are_in_ℒ⇩i⇩n_mm :: ‹nat clauses ⇒ bool› where ‹literals_are_in_ℒ⇩i⇩n_mm C ⟷ set_mset (all_lits_of_mm C) ⊆ set_mset ℒ⇩a⇩l⇩l› lemma literals_are_in_ℒ⇩i⇩n_mm_add_msetD: ‹literals_are_in_ℒ⇩i⇩n_mm (add_mset C N) ⟹ L ∈# C ⟹ L ∈# ℒ⇩a⇩l⇩l› by (auto simp: literals_are_in_ℒ⇩i⇩n_mm_def all_lits_of_mm_add_mset all_lits_of_m_add_mset dest!: multi_member_split) lemma literals_are_in_ℒ⇩i⇩n_mm_add_mset: ‹literals_are_in_ℒ⇩i⇩n_mm (add_mset C N) ⟷ literals_are_in_ℒ⇩i⇩n_mm N ∧ literals_are_in_ℒ⇩i⇩n C› unfolding literals_are_in_ℒ⇩i⇩n_mm_def literals_are_in_ℒ⇩i⇩n_def by (auto simp: all_lits_of_mm_add_mset) definition literals_are_in_ℒ⇩i⇩n_trail :: ‹(nat, 'mark) ann_lits ⇒ bool› where ‹literals_are_in_ℒ⇩i⇩n_trail M ⟷ set_mset (lit_of `# mset M) ⊆ set_mset ℒ⇩a⇩l⇩l› lemma literals_are_in_ℒ⇩i⇩n_trail_in_lits_of_l: ‹literals_are_in_ℒ⇩i⇩n_trail M ⟹ a ∈ lits_of_l M ⟹ a ∈# ℒ⇩a⇩l⇩l› by (auto simp: literals_are_in_ℒ⇩i⇩n_trail_def lits_of_def) lemma literals_are_in_ℒ⇩i⇩n_trail_uminus_in_lits_of_l: ‹literals_are_in_ℒ⇩i⇩n_trail M ⟹ -a ∈ lits_of_l M ⟹ a ∈# ℒ⇩a⇩l⇩l› by (auto simp: literals_are_in_ℒ⇩i⇩n_trail_def lits_of_def uminus_lit_swap uminus_𝒜⇩i⇩n_iff) lemma literals_are_in_ℒ⇩i⇩n_trail_uminus_in_lits_of_l_atms: ‹literals_are_in_ℒ⇩i⇩n_trail M ⟹ -a ∈ lits_of_l M ⟹ atm_of a ∈# 𝒜⇩i⇩n› using literals_are_in_ℒ⇩i⇩n_trail_uminus_in_lits_of_l[of M a] unfolding in_ℒ⇩a⇩l⇩l_atm_of_in_atms_of_iff[symmetric] atms_of_ℒ⇩a⇩l⇩l_𝒜⇩i⇩n[symmetric] . end lemma isasat_input_ops_ℒ⇩a⇩l⇩l_empty[simp]: ‹ℒ⇩a⇩l⇩l {#} = {#}› unfolding ℒ⇩a⇩l⇩l_def by auto lemma ℒ⇩a⇩l⇩l_atm_of_all_lits_of_mm: ‹set_mset (ℒ⇩a⇩l⇩l (atm_of `# all_lits_of_mm A)) = set_mset (all_lits_of_mm A)› apply (auto simp: ℒ⇩a⇩l⇩l_def in_all_lits_of_mm_ain_atms_of_iff) by (metis (no_types, lifting) image_iff in_all_lits_of_mm_ain_atms_of_iff literal.exhaust_sel) definition blits_in_ℒ⇩i⇩n :: ‹nat twl_st_wl ⇒ bool› where ‹blits_in_ℒ⇩i⇩n S ⟷ (∀L ∈# ℒ⇩a⇩l⇩l (all_atms_st S). ∀(i, K, b) ∈ set (watched_by S L). K ∈# ℒ⇩a⇩l⇩l (all_atms_st S))› definition literals_are_ℒ⇩i⇩n :: ‹nat multiset ⇒ nat twl_st_wl ⇒ bool› where ‹literals_are_ℒ⇩i⇩n 𝒜 S ≡ (is_ℒ⇩a⇩l⇩l 𝒜 (all_lits_st S) ∧ blits_in_ℒ⇩i⇩n S)› lemma literals_are_in_ℒ⇩i⇩n_nth: fixes C :: nat assumes dom: ‹C ∈# dom_m (get_clauses_wl S)› and ‹literals_are_ℒ⇩i⇩n 𝒜 S› shows ‹literals_are_in_ℒ⇩i⇩n 𝒜 (mset (get_clauses_wl S ∝ C))› proof - let ?N = ‹get_clauses_wl S› have ‹?N ∝ C ∈# ran_mf ?N› using dom by (auto simp: ran_m_def) then have ‹mset (?N ∝ C) ∈# mset `# (ran_mf ?N)› by blast from all_lits_of_m_subset_all_lits_of_mmD[OF this] show ?thesis using assms(2) unfolding is_ℒ⇩a⇩l⇩l_def literals_are_in_ℒ⇩i⇩n_def literals_are_ℒ⇩i⇩n_def by (auto simp add: all_lits_of_mm_union all_lits_def) qed lemma literals_are_in_ℒ⇩i⇩n_mm_in_ℒ⇩a⇩l⇩l: assumes N1: ‹literals_are_in_ℒ⇩i⇩n_mm 𝒜 (mset `# ran_mf xs)› and i_xs: ‹i ∈# dom_m xs› and j_xs: ‹j < length (xs ∝ i)› shows ‹xs ∝ i ! j ∈# ℒ⇩a⇩l⇩l 𝒜› proof - have ‹xs ∝ i ∈# ran_mf xs› using i_xs by auto then have ‹xs ∝ i ! j ∈ set_mset (all_lits_of_mm (mset `# ran_mf xs))› using j_xs by (auto simp: in_all_lits_of_mm_ain_atms_of_iff atms_of_ms_def Bex_def intro!: exI[of _ ‹xs ∝ i›]) then show ?thesis using N1 unfolding literals_are_in_ℒ⇩i⇩n_mm_def by blast qed lemma literals_are_in_ℒ⇩i⇩n_trail_in_lits_of_l_atms: ‹literals_are_in_ℒ⇩i⇩n_trail 𝒜⇩i⇩n M ⟹ a ∈ lits_of_l M ⟹ atm_of a ∈# 𝒜⇩i⇩n› using literals_are_in_ℒ⇩i⇩n_trail_in_lits_of_l[of 𝒜⇩i⇩n M a] unfolding in_ℒ⇩a⇩l⇩l_atm_of_in_atms_of_iff[symmetric] atms_of_ℒ⇩a⇩l⇩l_𝒜⇩i⇩n[symmetric] . lemma literals_are_in_ℒ⇩i⇩n_trail_Cons: ‹literals_are_in_ℒ⇩i⇩n_trail 𝒜⇩i⇩n (L # M) ⟷ literals_are_in_ℒ⇩i⇩n_trail 𝒜⇩i⇩n M ∧ lit_of L ∈# ℒ⇩a⇩l⇩l 𝒜⇩i⇩n› by (auto simp: literals_are_in_ℒ⇩i⇩n_trail_def) lemma literals_are_in_ℒ⇩i⇩n_trail_empty[simp]: ‹literals_are_in_ℒ⇩i⇩n_trail 𝒜 []› by (auto simp: literals_are_in_ℒ⇩i⇩n_trail_def) lemma literals_are_in_ℒ⇩i⇩n_trail_lit_of_mset: ‹literals_are_in_ℒ⇩i⇩n_trail 𝒜 M = literals_are_in_ℒ⇩i⇩n 𝒜 (lit_of `# mset M)› by (induction M) (auto simp: literals_are_in_ℒ⇩i⇩n_add_mset literals_are_in_ℒ⇩i⇩n_trail_Cons) lemma literals_are_in_ℒ⇩i⇩n_in_mset_ℒ⇩a⇩l⇩l: ‹literals_are_in_ℒ⇩i⇩n 𝒜 C ⟹ L ∈# C ⟹ L ∈# ℒ⇩a⇩l⇩l 𝒜› unfolding literals_are_in_ℒ⇩i⇩n_def by (auto dest!: multi_member_split simp: all_lits_of_m_add_mset) lemma literals_are_in_ℒ⇩i⇩n_in_ℒ⇩a⇩l⇩l: assumes N1: ‹literals_are_in_ℒ⇩i⇩n 𝒜 (mset xs)› and i_xs: ‹i < length xs› shows ‹xs ! i ∈# ℒ⇩a⇩l⇩l 𝒜› using literals_are_in_ℒ⇩i⇩n_in_mset_ℒ⇩a⇩l⇩l[of 𝒜 ‹mset xs› ‹xs!i›] assms by auto lemma is_ℒ⇩a⇩l⇩l_ℒ⇩a⇩l⇩l_rewrite[simp]: ‹is_ℒ⇩a⇩l⇩l 𝒜 (all_lits_of_mm 𝒜') ⟹ set_mset (ℒ⇩a⇩l⇩l (atm_of `# all_lits_of_mm 𝒜')) = set_mset (ℒ⇩a⇩l⇩l 𝒜)› using in_all_lits_of_mm_ain_atms_of_iff unfolding set_mset_set_mset_eq_iff is_ℒ⇩a⇩l⇩l_def Ball_def in_ℒ⇩a⇩l⇩l_atm_of_in_atms_of_iff in_all_lits_of_mm_ain_atms_of_iff atms_of_ℒ⇩a⇩l⇩l_𝒜⇩i⇩n by (auto simp: in_all_lits_of_mm_ain_atms_of_iff) lemma literals_are_ℒ⇩i⇩n_set_mset_ℒ⇩a⇩l⇩l[simp]: ‹literals_are_ℒ⇩i⇩n 𝒜 S ⟹ set_mset (ℒ⇩a⇩l⇩l (all_atms_st S)) = set_mset (ℒ⇩a⇩l⇩l 𝒜)› using in_all_lits_of_mm_ain_atms_of_iff unfolding set_mset_set_mset_eq_iff is_ℒ⇩a⇩l⇩l_def Ball_def in_ℒ⇩a⇩l⇩l_atm_of_in_atms_of_iff in_all_lits_of_mm_ain_atms_of_iff atms_of_ℒ⇩a⇩l⇩l_𝒜⇩i⇩n literals_are_ℒ⇩i⇩n_def by (auto simp: in_all_lits_of_mm_ain_atms_of_iff) lemma is_ℒ⇩a⇩l⇩l_all_lits_st_ℒ⇩a⇩l⇩l[simp]: ‹is_ℒ⇩a⇩l⇩l 𝒜 (all_lits_st S) ⟹ set_mset (ℒ⇩a⇩l⇩l (all_atms_st S)) = set_mset (ℒ⇩a⇩l⇩l 𝒜)› ‹is_ℒ⇩a⇩l⇩l 𝒜 (all_lits N NUE) ⟹ set_mset (ℒ⇩a⇩l⇩l (all_atms N NUE)) = set_mset (ℒ⇩a⇩l⇩l 𝒜)› ‹is_ℒ⇩a⇩l⇩l 𝒜 (all_lits N NUE) ⟹ set_mset (ℒ⇩a⇩l⇩l (atm_of `# all_lits N NUE)) = set_mset (ℒ⇩a⇩l⇩l 𝒜)› using in_all_lits_of_mm_ain_atms_of_iff unfolding set_mset_set_mset_eq_iff is_ℒ⇩a⇩l⇩l_def Ball_def in_ℒ⇩a⇩l⇩l_atm_of_in_atms_of_iff in_all_lits_of_mm_ain_atms_of_iff atms_of_ℒ⇩a⇩l⇩l_𝒜⇩i⇩n by (auto simp: in_all_lits_of_mm_ain_atms_of_iff all_lits_def all_atms_def) lemma is_ℒ⇩a⇩l⇩l_alt_def: ‹is_ℒ⇩a⇩l⇩l 𝒜 (all_lits_of_mm A) ⟷ atms_of (ℒ⇩a⇩l⇩l 𝒜) = atms_of_mm A› unfolding set_mset_set_mset_eq_iff is_ℒ⇩a⇩l⇩l_def Ball_def in_ℒ⇩a⇩l⇩l_atm_of_in_atms_of_iff in_all_lits_of_mm_ain_atms_of_iff by auto (metis literal.sel(2))+ lemma in_ℒ⇩a⇩l⇩l_atm_of_𝒜⇩i⇩n: ‹L ∈# ℒ⇩a⇩l⇩l 𝒜⇩i⇩n ⟷ atm_of L ∈# 𝒜⇩i⇩n› by (cases L) (auto simp: ℒ⇩a⇩l⇩l_def) lemma literals_are_in_ℒ⇩i⇩n_alt_def: ‹literals_are_in_ℒ⇩i⇩n 𝒜 S ⟷ atms_of S ⊆ atms_of (ℒ⇩a⇩l⇩l 𝒜)› apply (auto simp: literals_are_in_ℒ⇩i⇩n_def all_lits_of_mm_union lits_of_def in_all_lits_of_m_ain_atms_of_iff in_all_lits_of_mm_ain_atms_of_iff atms_of_ℒ⇩a⇩l⇩l_𝒜⇩i⇩n atm_of_eq_atm_of uminus_𝒜⇩i⇩n_iff subset_iff in_ℒ⇩a⇩l⇩l_atm_of_𝒜⇩i⇩n) apply (auto simp: atms_of_def) done lemma assumes x2_T: ‹(x2, T) ∈ state_wl_l b› and struct: ‹twl_struct_invs U› and T_U: ‹(T, U) ∈ twl_st_l b'› shows literals_are_ℒ⇩i⇩n_literals_are_ℒ⇩i⇩n_trail: ‹literals_are_ℒ⇩i⇩n 𝒜⇩i⇩n x2 ⟹ literals_are_in_ℒ⇩i⇩n_trail 𝒜⇩i⇩n (get_trail_wl x2)› (is ‹_⟹ ?trail›) and literals_are_ℒ⇩i⇩n_literals_are_in_ℒ⇩i⇩n_conflict: ‹literals_are_ℒ⇩i⇩n 𝒜⇩i⇩n x2 ⟹ get_conflict_wl x2 ≠ None ⟹ literals_are_in_ℒ⇩i⇩n 𝒜⇩i⇩n (the (get_conflict_wl x2))› and conflict_not_tautology: ‹get_conflict_wl x2 ≠ None ⟹ ¬tautology (the (get_conflict_wl x2))› proof - have alien: ‹cdcl⇩W_restart_mset.no_strange_atm (state⇩W_of U)› and confl: ‹cdcl⇩W_restart_mset.cdcl⇩W_conflicting (state⇩W_of U)› and M_lev: ‹cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv (state⇩W_of U)› and dist: ‹cdcl⇩W_restart_mset.distinct_cdcl⇩W_state (state⇩W_of U)› using struct unfolding twl_struct_invs_def cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def by fast+ show lits_trail: ‹literals_are_in_ℒ⇩i⇩n_trail 𝒜⇩i⇩n (get_trail_wl x2)› if ‹literals_are_ℒ⇩i⇩n 𝒜⇩i⇩n x2› using alien that x2_T T_U unfolding is_ℒ⇩a⇩l⇩l_def literals_are_in_ℒ⇩i⇩n_trail_def cdcl⇩W_restart_mset.no_strange_atm_def literals_are_ℒ⇩i⇩n_def all_lits_def all_atms_def by (subst (asm) all_clss_l_ran_m[symmetric]) (auto 5 2 simp del: all_clss_l_ran_m union_filter_mset_complement simp: twl_st twl_st_l twl_st_wl all_lits_of_mm_union lits_of_def convert_lits_l_def image_image in_all_lits_of_mm_ain_atms_of_iff get_unit_clauses_wl_alt_def) { assume conf: ‹get_conflict_wl x2 ≠ None› show lits_confl: ‹literals_are_in_ℒ⇩i⇩n 𝒜⇩i⇩n (the (get_conflict_wl x2))› if ‹literals_are_ℒ⇩i⇩n 𝒜⇩i⇩n x2› using x2_T T_U alien that conf unfolding is_ℒ⇩a⇩l⇩l_alt_def cdcl⇩W_restart_mset.no_strange_atm_def literals_are_in_ℒ⇩i⇩n_alt_def literals_are_ℒ⇩i⇩n_def all_lits_def all_atms_def apply (subst (asm) all_clss_l_ran_m[symmetric]) unfolding image_mset_union all_lits_of_mm_union by (auto simp add: twl_st all_lits_of_mm_union lits_of_def image_image in_all_lits_of_mm_ain_atms_of_iff in_all_lits_of_m_ain_atms_of_iff get_unit_clauses_wl_alt_def simp del: all_clss_l_ran_m) have M_confl: ‹get_trail_wl x2 ⊨as CNot (the (get_conflict_wl x2))› using confl conf x2_T T_U unfolding cdcl⇩W_restart_mset.cdcl⇩W_conflicting_def by (auto 5 5 simp: twl_st true_annots_def) moreover have n_d: ‹no_dup (get_trail_wl x2)› using M_lev x2_T T_U unfolding cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv_def by (auto simp: twl_st) ultimately show 4: ‹¬tautology (the (get_conflict_wl x2))› using n_d M_confl by (meson no_dup_consistentD tautology_decomp' true_annots_true_cls_def_iff_negation_in_model) } qed lemma literals_are_in_ℒ⇩i⇩n_trail_atm_of: ‹literals_are_in_ℒ⇩i⇩n_trail 𝒜⇩i⇩n M ⟷ atm_of ` lits_of_l M ⊆ set_mset 𝒜⇩i⇩n› apply (rule iffI) subgoal by (auto dest: literals_are_in_ℒ⇩i⇩n_trail_in_lits_of_l_atms) subgoal by (fastforce simp: literals_are_in_ℒ⇩i⇩n_trail_def lits_of_def in_ℒ⇩a⇩l⇩l_atm_of_𝒜⇩i⇩n) done lemma literals_are_in_ℒ⇩i⇩n_poss_remdups_mset: ‹literals_are_in_ℒ⇩i⇩n 𝒜⇩i⇩n (poss (remdups_mset (atm_of `# C))) ⟷ literals_are_in_ℒ⇩i⇩n 𝒜⇩i⇩n C› by (induction C) (auto simp: literals_are_in_ℒ⇩i⇩n_add_mset in_ℒ⇩a⇩l⇩l_atm_of_in_atms_of_iff atm_of_eq_atm_of dest!: multi_member_split) lemma literals_are_in_ℒ⇩i⇩n_negs_remdups_mset: ‹literals_are_in_ℒ⇩i⇩n 𝒜⇩i⇩n (negs (remdups_mset (atm_of `# C))) ⟷ literals_are_in_ℒ⇩i⇩n 𝒜⇩i⇩n C› by (induction C) (auto simp: literals_are_in_ℒ⇩i⇩n_add_mset in_ℒ⇩a⇩l⇩l_atm_of_in_atms_of_iff atm_of_eq_atm_of dest!: multi_member_split) lemma ℒ⇩a⇩l⇩l_atm_of_all_lits_of_m: ‹set_mset (ℒ⇩a⇩l⇩l (atm_of `# all_lits_of_m C)) = set_mset C ∪ uminus ` set_mset C› supply lit_eq_Neg_Pos_iff[iff] by (auto simp: ℒ⇩a⇩l⇩l_def all_lits_of_m_def image_iff dest!: multi_member_split) lemma atm_of_all_lits_of_mm: ‹set_mset (atm_of `# all_lits_of_mm bw) = atms_of_mm bw› ‹atm_of ` set_mset (all_lits_of_mm bw) = atms_of_mm bw› using in_all_lits_of_mm_ain_atms_of_iff apply (auto simp: image_iff) by (metis (full_types) image_eqI literal.sel(1))+ lemma in_set_all_atms_iff: ‹y ∈# all_atms bu bw ⟷ y ∈ atms_of_mm (mset `# ran_mf bu) ∨ y ∈ atms_of_mm bw› by (auto simp: all_atms_def all_lits_def in_all_lits_of_mm_ain_atms_of_iff atm_of_all_lits_of_mm) lemma ℒ⇩a⇩l⇩l_union: ‹set_mset (ℒ⇩a⇩l⇩l (A + B)) = set_mset (ℒ⇩a⇩l⇩l A) ∪ set_mset (ℒ⇩a⇩l⇩l B)› by (auto simp: ℒ⇩a⇩l⇩l_def) lemma ℒ⇩a⇩l⇩l_cong: ‹set_mset A = set_mset B ⟹ set_mset (ℒ⇩a⇩l⇩l A) = set_mset (ℒ⇩a⇩l⇩l B)› by (auto simp: ℒ⇩a⇩l⇩l_def) lemma atms_of_ℒ⇩a⇩l⇩l_cong: ‹set_mset 𝒜 = set_mset ℬ ⟹ atms_of (ℒ⇩a⇩l⇩l 𝒜) = atms_of (ℒ⇩a⇩l⇩l ℬ)› unfolding ℒ⇩a⇩l⇩l_def by auto definition unit_prop_body_wl_D_inv :: ‹nat twl_st_wl ⇒ nat ⇒ nat ⇒ nat literal ⇒ bool› where ‹unit_prop_body_wl_D_inv T' j w L ⟷ unit_prop_body_wl_inv T' j w L ∧ literals_are_ℒ⇩i⇩n (all_atms_st T') T' ∧ L ∈# ℒ⇩a⇩l⇩l (all_atms_st T')› text ‹ ▪ should be the definition of \<^term>‹unit_prop_body_wl_find_unwatched_inv›. ▪ the distinctiveness should probably be only a property, not a part of the definition. › definition unit_prop_body_wl_D_find_unwatched_inv where ‹unit_prop_body_wl_D_find_unwatched_inv f C S ⟷ unit_prop_body_wl_find_unwatched_inv f C S ∧ (f ≠ None ⟶ the f ≥ 2 ∧ the f < length (get_clauses_wl S ∝ C) ∧ get_clauses_wl S ∝ C ! (the f) ≠ get_clauses_wl S ∝ C ! 0 ∧ get_clauses_wl S ∝ C ! (the f) ≠ get_clauses_wl S ∝ C ! 1)› definition unit_propagation_inner_loop_wl_loop_D_inv where ‹unit_propagation_inner_loop_wl_loop_D_inv L = (λ(j, w, S). literals_are_ℒ⇩i⇩n (all_atms_st S) S ∧ L ∈# ℒ⇩a⇩l⇩l (all_atms_st S) ∧ unit_propagation_inner_loop_wl_loop_inv L (j, w, S))› definition unit_propagation_inner_loop_wl_loop_D_pre where ‹unit_propagation_inner_loop_wl_loop_D_pre L = (λ(j, w, S). unit_propagation_inner_loop_wl_loop_D_inv L (j, w, S) ∧ unit_propagation_inner_loop_wl_loop_pre L (j, w, S))› definition unit_propagation_inner_loop_body_wl_D :: ‹nat literal ⇒ nat ⇒ nat ⇒ nat twl_st_wl ⇒ (nat × nat × nat twl_st_wl) nres› where ‹unit_propagation_inner_loop_body_wl_D L j w S = do { ASSERT(unit_propagation_inner_loop_wl_loop_D_pre L (j, w, S)); let (C, K, b) = (watched_by S L) ! w; let S = keep_watch L j w S; ASSERT(unit_prop_body_wl_D_inv S j w L); let val_K = polarity (get_trail_wl S) K; if val_K = Some True then RETURN (j+1, w+1, S) else do { if b then do { ASSERT(propagate_proper_bin_case L K S C); if val_K = Some False then do {RETURN (j+1, w+1, set_conflict_wl (get_clauses_wl S ∝ C) S)} else do { let i = (if ((get_clauses_wl S)∝C) ! 0 = L then 0 else 1); RETURN (j+1, w+1, propagate_lit_wl_bin K C i S) } } ―‹Now the costly operations:› else if C ∉# dom_m (get_clauses_wl S) then RETURN (j, w+1, S) else do { let i = (if ((get_clauses_wl S)∝C) ! 0 = L then 0 else 1); let L' = ((get_clauses_wl S)∝C) ! (1 - i); let val_L' = polarity (get_trail_wl S) L'; if val_L' = Some True then update_blit_wl L C b j w L' S else do { f ← find_unwatched_l (get_trail_wl S) (get_clauses_wl S ∝C); ASSERT (unit_prop_body_wl_D_find_unwatched_inv f C S); case f of None ⇒ do { if val_L' = Some False then RETURN (j+1, w+1, set_conflict_wl (get_clauses_wl S ∝ C) S) else RETURN (j+1, w+1, propagate_lit_wl L' C i S) } | Some f ⇒ do { let K = get_clauses_wl S ∝ C ! f; let val_L' = polarity (get_trail_wl S) K; if val_L' = Some True then update_blit_wl L C b j w K S else update_clause_wl L C b j w i f S } } } } }› declare Id_refine[refine_vcg del] refine0(5)[refine_vcg del] lemma unit_prop_body_wl_D_inv_clauses_distinct_eq: assumes x[simp]: ‹watched_by S K ! w = (x1, x2)› and inv: ‹unit_prop_body_wl_D_inv (keep_watch K i w S) i w K› and y: ‹y < length (get_clauses_wl S ∝ (fst (watched_by S K ! w)))› and w: ‹fst(watched_by S K ! w) ∈# dom_m (get_clauses_wl (keep_watch K i w S))› and y': ‹y' < length (get_clauses_wl S ∝ (fst (watched_by S K ! w)))› and w_le: ‹w < length (watched_by S K)› shows ‹get_clauses_wl S ∝ x1 ! y = get_clauses_wl S ∝ x1 ! y' ⟷ y = y'› (is ‹?eq ⟷ ?y›) proof assume eq: ?eq let ?S = ‹keep_watch K i w S› let ?C = ‹fst (watched_by ?S K ! w)› have dom: ‹fst (watched_by (keep_watch K i w S) K ! w) ∈# dom_m (get_clauses_wl (keep_watch K i w S))› ‹fst (watched_by (keep_watch K i w S) K ! w) ∈# dom_m (get_clauses_wl S)› using w_le assms by (auto simp: x twl_st_wl) obtain T U where ST: ‹(?S, T) ∈ state_wl_l (Some (K, w))› and TU: ‹(set_clauses_to_update_l (clauses_to_update_l (remove_one_lit_from_wq ?C T) + {#?C#}) (remove_one_lit_from_wq ?C T), U) ∈ twl_st_l (Some K)› and struct_U: ‹twl_struct_invs U› and i_w: ‹i ≤ w› and w_le: ‹w < length (watched_by (keep_watch K i w S) K)› using inv w unfolding unit_prop_body_wl_D_inv_def unit_prop_body_wl_inv_def unit_prop_body_wl_inv_def unit_propagation_inner_loop_body_l_inv_def x fst_conv apply - apply (simp only: simp_thms dom) apply normalize_goal+ by blast have ‹cdcl⇩W_restart_mset.distinct_cdcl⇩W_state (state⇩W_of U)› using struct_U unfolding twl_struct_invs_def cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def by fast then have ‹distinct_mset_mset (mset `# ran_mf (get_clauses_wl S))› using ST TU unfolding image_Un cdcl⇩W_restart_mset.distinct_cdcl⇩W_state_def all_clss_lf_ran_m[symmetric] image_mset_union by (auto simp: drop_Suc twl_st_wl twl_st_l twl_st) then have ‹distinct (get_clauses_wl S ∝ C)› if ‹C > 0› and ‹C ∈# dom_m (get_clauses_wl S)› for C using that ST TU unfolding cdcl⇩W_restart_mset.distinct_cdcl⇩W_state_def distinct_mset_set_def by (auto simp: nth_in_set_tl mset_take_mset_drop_mset cdcl⇩W_restart_mset_state distinct_mset_set_distinct twl_st) moreover have ‹?C > 0› and ‹?C ∈# dom_m (get_clauses_wl S)› using inv w unfolding unit_propagation_inner_loop_body_l_inv_def unit_prop_body_wl_D_inv_def unit_prop_body_wl_inv_def x apply - apply (simp only: simp_thms twl_st_wl x fst_conv dom) apply normalize_goal+ apply (solves simp) apply (simp only: simp_thms twl_st_wl x fst_conv dom) done ultimately have ‹distinct (get_clauses_wl S ∝ ?C)› by blast moreover have ‹fst (watched_by (keep_watch K i w S) K ! w) = fst (watched_by S K ! w)› using i_w w_le by (cases S; cases ‹i=w›) (auto simp: keep_watch_def) ultimately show ?y using y y' eq by (auto simp: nth_eq_iff_index_eq twl_st_wl x) next assume ?y then show ?eq by blast qed lemma in_all_lits_uminus_iff[simp]: ‹(- xa ∈# all_lits N NUE) = (xa ∈# all_lits N NUE)› unfolding all_lits_def by (auto simp: in_all_lits_of_mm_uminus_iff) lemma is_ℒ⇩a⇩l⇩l_all_atms_st_all_lits_st[simp]: ‹is_ℒ⇩a⇩l⇩l (all_atms_st S) (all_lits_st S)› unfolding is_ℒ⇩a⇩l⇩l_def by (auto simp: in_ℒ⇩a⇩l⇩l_atm_of_in_atms_of_iff atms_of_ℒ⇩a⇩l⇩l_𝒜⇩i⇩n atm_of_eq_atm_of) lemma literals_are_ℒ⇩i⇩n_all_atms_st: ‹blits_in_ℒ⇩i⇩n S ⟹ literals_are_ℒ⇩i⇩n (all_atms_st S) S› unfolding literals_are_ℒ⇩i⇩n_def by auto lemma blits_in_ℒ⇩i⇩n_keep_watch: assumes ‹blits_in_ℒ⇩i⇩n (a, b, c, d, e, f, g)› and w:‹w < length (watched_by (a, b, c, d, e, f, g) K)› shows ‹blits_in_ℒ⇩i⇩n (a, b, c, d, e, f, g (K := (g K)[j := g K ! w]))› proof - let ?S = ‹(a, b, c, d, e, f, g)› let ?T = ‹(a, b, c, d, e, f, g (K := (g K)[j := g K ! w]))› let ?g = ‹g (K := (g K)[j := g K ! w])› have H: ‹⋀L i K b. L∈# ℒ⇩a⇩l⇩l (all_atms_st ?S) ⟹ (i, K, b) ∈set (g L) ⟹ K ∈# ℒ⇩a⇩l⇩l (all_atms_st ?S)› using assms unfolding blits_in_ℒ⇩i⇩n_def watched_by.simps by blast have ‹ L∈#ℒ⇩a⇩l⇩l (all_atms_st ?S) ⟹ (i, K', b') ∈set (?g L) ⟹ K' ∈# ℒ⇩a⇩l⇩l (all_atms_st ?S)› for L i K' b' using H[of L i K'] H[of L ‹fst (g K ! w)› ‹fst (snd (g K ! w))›] nth_mem[OF w] unfolding blits_in_ℒ⇩i⇩n_def watched_by.simps by (cases ‹j < length (g K)›; cases ‹g K ! w›) (auto split: if_splits elim!: in_set_upd_cases) moreover have ‹all_atms_st ?S = all_atms_st ?T› by (auto simp: all_lits_def all_atms_def) ultimately show ?thesis unfolding blits_in_ℒ⇩i⇩n_def watched_by.simps by force qed text ‹We mark as safe intro rule, since we will always be in a case where the equivalence holds, although in general the equivalence does not hold.› lemma literals_are_ℒ⇩i⇩n_keep_watch[twl_st_wl, simp, intro!]: ‹literals_are_ℒ⇩i⇩n 𝒜 S ⟹ w < length (watched_by S K) ⟹ literals_are_ℒ⇩i⇩n 𝒜 (keep_watch K j w S)› by (cases S) (auto simp: keep_watch_def literals_are_ℒ⇩i⇩n_def blits_in_ℒ⇩i⇩n_keep_watch all_lits_def all_atms_def) lemma all_lits_update_swap[simp]: ‹x1 ∈# dom_m x1aa ⟹ n < length (x1aa ∝ x1) ⟹n' < length (x1aa ∝ x1) ⟹ all_lits (x1aa(x1 ↪ swap (x1aa ∝ x1) n n')) = all_lits x1aa› using distinct_mset_dom[of x1aa] unfolding all_lits_def by (auto simp: ran_m_def if_distrib image_mset_If filter_mset_eq not_in_iff[THEN iffD1] removeAll_mset_filter_mset[symmetric] dest!: multi_member_split[of x1] intro!: ext) lemma blits_in_ℒ⇩i⇩n_propagate: ‹x1 ∈# dom_m x1aa ⟹ n < length (x1aa ∝ x1) ⟹ n' < length (x1aa ∝ x1) ⟹ blits_in_ℒ⇩i⇩n (Propagated A x1' # x1b, x1aa (x1 ↪ swap (x1aa ∝ x1) n n'), D, x1c, x1d, add_mset A' x1e, x2e) ⟷ blits_in_ℒ⇩i⇩n (x1b, x1aa, D, x1c, x1d, x1e, x2e)› ‹x1 ∈# dom_m x1aa ⟹ n < length (x1aa ∝ x1) ⟹ n' < length (x1aa ∝ x1) ⟹ blits_in_ℒ⇩i⇩n (x1b, x1aa (x1 ↪ swap (x1aa ∝ x1) n n'), D, x1c, x1d,x1e, x2e) ⟷ blits_in_ℒ⇩i⇩n (x1b, x1aa, D, x1c, x1d, x1e, x2e)› ‹blits_in_ℒ⇩i⇩n (Propagated A x1' # x1b, x1aa, D, x1c, x1d, add_mset A' x1e, x2e) ⟷ blits_in_ℒ⇩i⇩n (x1b, x1aa, D, x1c, x1d, x1e, x2e)› ‹x1' ∈# dom_m x1aa ⟹ n < length (x1aa ∝ x1') ⟹ n' < length (x1aa ∝ x1') ⟹ K ∈# ℒ⇩a⇩l⇩l (all_atms_st (x1b, x1aa, D, x1c, x1d, x1e, x2e)) ⟹ blits_in_ℒ⇩i⇩n (x1a, x1aa(x1' ↪ swap (x1aa ∝ x1') n n'), D, x1c, x1d, x1e, x2e (x1aa ∝ x1' ! n' := x2e (x1aa ∝ x1' ! n') @ [(x1', K, b')])) ⟷ blits_in_ℒ⇩i⇩n (x1a, x1aa, D, x1c, x1d, x1e, x2e)› ‹K ∈# ℒ⇩a⇩l⇩l (all_atms_st (x1b, x1aa, D, x1c, x1d, x1e, x2e)) ⟹ blits_in_ℒ⇩i⇩n (x1a, x1aa, D, x1c, x1d, x1e, x2e (x1aa ∝ x1' ! n' := x2e (x1aa ∝ x1' ! n') @ [(x1', K, b')])) ⟷ blits_in_ℒ⇩i⇩n (x1a, x1aa, D, x1c, x1d, x1e, x2e)› unfolding blits_in_ℒ⇩i⇩n_def by (auto split: if_splits)[5] lemma literals_are_ℒ⇩i⇩n_set_conflict_wl: ‹literals_are_ℒ⇩i⇩n 𝒜 (set_conflict_wl D S) ⟷ literals_are_ℒ⇩i⇩n 𝒜 S› by (cases S; auto simp: blits_in_ℒ⇩i⇩n_def literals_are_ℒ⇩i⇩n_def set_conflict_wl_def) lemma blits_in_ℒ⇩i⇩n_keep_watch': assumes K': ‹K' ∈# ℒ⇩a⇩l⇩l (all_atms_st (a, b, c, d, e, f, g))› and w:‹blits_in_ℒ⇩i⇩n (a, b, c, d, e, f, g)› shows ‹blits_in_ℒ⇩i⇩n (a, b, c, d, e, f, g (K := (g K)[j := (i, K', b')]))› proof - let ?𝒜 = ‹all_atms_st (a, b, c, d, e, f, g)› let ?g = ‹g (K := (g K)[j := (i, K', b')])› have H: ‹⋀L i K b'. L∈#ℒ⇩a⇩l⇩l ?𝒜 ⟹ (i, K, b') ∈set (g L) ⟹ K ∈# ℒ⇩a⇩l⇩l ?𝒜› using assms unfolding blits_in_ℒ⇩i⇩n_def watched_by.simps by blast have ‹ L∈#ℒ⇩a⇩l⇩l ?𝒜 ⟹ (i, K', b') ∈set (?g L) ⟹ K' ∈# ℒ⇩a⇩l⇩l ?𝒜› for L i K' b' using H[of L i K'] K' unfolding blits_in_ℒ⇩i⇩n_def watched_by.simps by (cases ‹j < length (g K)›; cases ‹g K ! w›) (auto split: if_splits elim!: in_set_upd_cases) then show ?thesis unfolding blits_in_ℒ⇩i⇩n_def watched_by.simps by force qed lemma literals_are_ℒ⇩i⇩n_all_atms_stD[dest]: ‹literals_are_ℒ⇩i⇩n 𝒜 S ⟹ literals_are_ℒ⇩i⇩n (all_atms_st S) S› unfolding literals_are_ℒ⇩i⇩n_def by auto lemma blits_in_ℒ⇩i⇩n_set_conflict[simp]: ‹blits_in_ℒ⇩i⇩n (set_conflict_wl D S) = blits_in_ℒ⇩i⇩n S› by (cases S) (auto simp: blits_in_ℒ⇩i⇩n_def set_conflict_wl_def) lemma unit_propagation_inner_loop_body_wl_D_spec: fixes S :: ‹nat twl_st_wl› and K :: ‹nat literal› and w :: nat assumes K: ‹K ∈# ℒ⇩a⇩l⇩l 𝒜› and 𝒜⇩i⇩n: ‹literals_are_ℒ⇩i⇩n 𝒜 S› shows ‹unit_propagation_inner_loop_body_wl_D K j w S ≤ ⇓ {((j', n', T'), (j, n, T)). j' = j ∧ n' = n ∧ T = T' ∧ literals_are_ℒ⇩i⇩n 𝒜 T'} (unit_propagation_inner_loop_body_wl K j w S)› proof - obtain M N D NE UE Q W where S: ‹S = (M, N, D, NE, UE, Q, W)› by (cases S) have f': ‹(f, f') ∈ ⟨Id⟩option_rel› if ‹(f, f') ∈ Id› for f f' using that by auto define find_unwatched_wl :: ‹(nat,nat) ann_lits ⇒ _› where ‹find_unwatched_wl = find_unwatched_l› let ?C = ‹fst ((watched_by S K) ! w)› have find_unwatched: ‹find_unwatched_wl (get_trail_wl S) ((get_clauses_wl S)∝D) ≤ ⇓ {(L, L'). L = L' ∧ (L ≠ None ⟶ the L < length ((get_clauses_wl S)∝C) ∧ the L ≥ 2)} (find_unwatched_l (get_trail_wl S) ((get_clauses_wl S)∝C))› (is ‹_ ≤ ⇓ ?find_unwatched _›) if ‹C = D› for C D and L and K and S unfolding find_unwatched_l_def find_unwatched_wl_def that by (auto simp: intro!: RES_refine) have propagate_lit_wl: ‹((j+1, w + 1, propagate_lit_wl (get_clauses_wl S ∝ x1a ! (1 - (if get_clauses_wl S ∝ x1a ! 0 = K then 0 else 1))) x1a (if get_clauses_wl S ∝ x1a ! 0 = K then 0 else 1) S), j+1, w + 1, propagate_lit_wl (get_clauses_wl S ∝ x1 ! (1 - (if get_clauses_wl S ∝ x1 ! 0 = K then 0 else 1))) x1 (if get_clauses_wl S ∝ x1 ! 0 = K then 0 else 1) S) ∈ {((j', n', T'), j, n, T). j' = j ∧ n' = n ∧ T = T' ∧ literals_are_ℒ⇩i⇩n 𝒜 T'}› if ‹unit_prop_body_wl_D_inv S j w K› and ‹¬x1 ∉# dom_m (get_clauses_wl S)› and ‹(watched_by S K) ! w = (x1a, x2a)› and ‹(watched_by S K) ! w = (x1, x2)› and ‹literals_are_ℒ⇩i⇩n 𝒜 S› for f f' j S x1 x2 x1a x2a unfolding propagate_lit_wl_def S apply clarify apply refine_vcg using that 𝒜⇩i⇩n by (auto simp: clauses_def unit_prop_body_wl_find_unwatched_inv_def mset_take_mset_drop_mset' S unit_prop_body_wl_D_inv_def unit_prop_body_wl_inv_def ran_m_mapsto_upd unit_propagation_inner_loop_body_l_inv_def blits_in_ℒ⇩i⇩n_propagate state_wl_l_def image_mset_remove1_mset_if literals_are_ℒ⇩i⇩n_def) have update_clause_wl: ‹update_clause_wl K x1' b' j w (if get_clauses_wl S ∝ x1' ! 0 = K then 0 else 1) n S ≤ ⇓ {((j', n', T'), j, n, T). j' = j ∧ n' = n ∧ T = T' ∧ literals_are_ℒ⇩i⇩n 𝒜 T'} (update_clause_wl K x1 b j w (if get_clauses_wl S ∝ x1 ! 0 = K then 0 else 1) n' S)› if ‹(n, n') ∈ Id› and ‹unit_prop_body_wl_D_inv S j w K› ‹(f, f') ∈ ?find_unwatched x1 S› and ‹f = Some n› ‹f' = Some n'› and ‹unit_prop_body_wl_D_find_unwatched_inv f x1' S› and ‹¬x1 ∉# dom_m (get_clauses_wl S)› and ‹watched_by S K ! w = (x1, x2)› and ‹watched_by S K ! w = (x1', x2')› and ‹(b, b') ∈ Id› and ‹literals_are_ℒ⇩i⇩n 𝒜 S› for n n' f f' S x1 x2 x1' x2' b b' unfolding update_clause_wl_def S apply refine_vcg using that 𝒜⇩i⇩n by (auto simp: clauses_def mset_take_mset_drop_mset unit_prop_body_wl_find_unwatched_inv_def mset_take_mset_drop_mset' S unit_prop_body_wl_D_inv_def unit_prop_body_wl_inv_def ran_m_clause_upd unit_propagation_inner_loop_body_l_inv_def blits_in_ℒ⇩i⇩n_propagate state_wl_l_def image_mset_remove1_mset_if literals_are_ℒ⇩i⇩n_def) have H: ‹watched_by S K ! w = A ⟹ watched_by (keep_watch K j w S) K ! w = A› for S j w K A x1 by (cases S; cases ‹j=w›) (auto simp: keep_watch_def) have update_blit_wl: ‹update_blit_wl K x1a b' j w (get_clauses_wl (keep_watch K j w S) ∝ x1a ! (1 - (if get_clauses_wl (keep_watch K j w S) ∝ x1a ! 0 = K then 0 else 1))) (keep_watch K j w S) ≤ ⇓ {((j', n', T'), j, n, T). j' = j ∧ n' = n ∧ T = T' ∧ literals_are_ℒ⇩i⇩n 𝒜 T'} (update_blit_wl K x1 b j w (get_clauses_wl (keep_watch K j w S) ∝ x1 ! (1 - (if get_clauses_wl (keep_watch K j w S) ∝ x1 ! 0 = K then 0 else 1))) (keep_watch K j w S))› if x: ‹watched_by S K ! w = (x1, x2)› and xa: ‹watched_by S K ! w = (x1a, x2a)› and unit: ‹unit_prop_body_wl_D_inv (keep_watch K j w S) j w K› and x1: ‹¬x1 ∉# dom_m (get_clauses_wl (keep_watch K j w S))› and bb': ‹(b, b') ∈ Id› for x1 x2 x1a x2a b b' proof - have [simp]: ‹x1a = x1› and x1a: ‹x1 ∈# dom_m (get_clauses_wl S)› ‹fst (watched_by (keep_watch K j w S) K ! w) ∈# dom_m (get_clauses_wl (keep_watch K j w S))› using x xa x1 unit unfolding unit_prop_body_wl_D_inv_def unit_prop_body_wl_inv_def by auto have ‹get_clauses_wl S ∝x1 ! 0 ∈# ℒ⇩a⇩l⇩l 𝒜 ∧ get_clauses_wl S ∝ x1 ! Suc 0 ∈# ℒ⇩a⇩l⇩l 𝒜› using assms that literals_are_in_ℒ⇩i⇩n_nth[of x1 S] literals_are_in_ℒ⇩i⇩n_in_ℒ⇩a⇩l⇩l[of 𝒜 ‹get_clauses_wl S ∝ x1› 0] literals_are_in_ℒ⇩i⇩n_in_ℒ⇩a⇩l⇩l[of 𝒜 ‹get_clauses_wl S ∝ x1› 1] unfolding unit_prop_body_wl_D_inv_def unit_prop_body_wl_inv_def unit_propagation_inner_loop_body_l_inv_def x1a apply (simp only: x1a fst_conv simp_thms) apply normalize_goal+ by (auto simp del: simp: x1a) then show ?thesis using assms unit bb' by (cases S) (auto simp: keep_watch_def update_blit_wl_def literals_are_ℒ⇩i⇩n_def blits_in_ℒ⇩i⇩n_propagate blits_in_ℒ⇩i⇩n_keep_watch' unit_prop_body_wl_D_inv_def) qed have update_blit_wl': ‹update_blit_wl K x1a b' j w (get_clauses_wl (keep_watch K j w S) ∝ x1a ! x) (keep_watch K j w S) ≤ ⇓ {((j', n', T'), j, n, T). j' = j ∧ n' = n ∧ T = T' ∧ literals_are_ℒ⇩i⇩n 𝒜 T'} (update_blit_wl K x1 b j w (get_clauses_wl (keep_watch K j w S) ∝ x1 ! x') (keep_watch K j w S))› if x1: ‹watched_by S K ! w = (x1, x2)› and xa: ‹watched_by S K ! w = (x1a, x2a)› and unw: ‹unit_prop_body_wl_D_find_unwatched_inv f x1a (keep_watch K j w S)› and dom: ‹¬x1 ∉# dom_m(get_clauses_wl (keep_watch K j w S))› and unit: ‹unit_prop_body_wl_D_inv (keep_watch K j w S) j w K› and f: ‹f = Some x› and xx': ‹(x, x') ∈ nat_rel› and bb': ‹(b, b') ∈ Id› for x1 x2 x1a x2a f fa x x' b b' proof - have [simp]: ‹x1a = x1› ‹x = x'› using x1 xa xx' by auto have x1a: ‹x1 ∈# dom_m (get_clauses_wl S)› ‹fst (watched_by S K ! w) ∈# dom_m (get_clauses_wl S)› using dom x1 by auto have ‹get_clauses_wl S ∝x1 ! x ∈# ℒ⇩a⇩l⇩l 𝒜› using assms that literals_are_in_ℒ⇩i⇩n_nth[of x1 S] literals_are_in_ℒ⇩i⇩n_in_ℒ⇩a⇩l⇩l[of 𝒜 ‹get_clauses_wl S ∝ x1› x] unw unfolding unit_prop_body_wl_D_find_unwatched_inv_def by auto then show ?thesis using assms bb' by (cases S) (auto simp: keep_watch_def update_blit_wl_def literals_are_ℒ⇩i⇩n_def blits_in_ℒ⇩i⇩n_propagate blits_in_ℒ⇩i⇩n_keep_watch') qed have set_conflict_rel: ‹((j + 1, w + 1, set_conflict_wl (get_clauses_wl (keep_watch K j w S) ∝ x1a) (keep_watch K j w S)), j + 1, w + 1, set_conflict_wl (get_clauses_wl (keep_watch K j w S) ∝ x1) (keep_watch K j w S)) ∈ {((j', n', T'), j, n, T). j' = j ∧ n' = n ∧ T = T' ∧ literals_are_ℒ⇩i⇩n 𝒜 T'}› if pre: ‹unit_propagation_inner_loop_wl_loop_D_pre K (j, w, S)› and x: ‹watched_by S K ! w = (x1, x2)› and xa: ‹watched_by S K ! w = (x1a, x2a')› and xa': ‹x2a' = (x2a, x3)› and unit: ‹unit_prop_body_wl_D_inv (keep_watch K j w S) j w K› and dom: ‹¬ x1a ∉# dom_m (get_clauses_wl (keep_watch K j w S))› for x1 x2 x1a x2a f fa x2a' x3 proof - have [simp]: ‹blits_in_ℒ⇩i⇩n (set_conflict_wl D (a, b, c, d, e, fb, g(K := (g K)[j := de]))) ⟷ blits_in_ℒ⇩i⇩n ((a, b, c, d, e, fb, g(K := (g K)[j := de])))› for a b c d e f g de D by (auto simp: blits_in_ℒ⇩i⇩n_def set_conflict_wl_def) have [simp]: ‹x1a = x1› using xa x by auto have ‹x2a ∈# ℒ⇩a⇩l⇩l 𝒜› using xa x dom assms pre unit nth_mem[of w ‹watched_by S K›] xa' by (cases S) (auto simp: unit_prop_body_wl_D_inv_def literals_are_ℒ⇩i⇩n_def unit_prop_body_wl_inv_def blits_in_ℒ⇩i⇩n_def keep_watch_def unit_propagation_inner_loop_wl_loop_D_pre_def dest!: multi_member_split split: if_splits) then show ?thesis using assms that by (cases S) (auto simp: keep_watch_def literals_are_ℒ⇩i⇩n_set_conflict_wl literals_are_ℒ⇩i⇩n_def blits_in_ℒ⇩i⇩n_keep_watch') qed have bin_set_conflict: ‹((j + 1, w + 1, set_conflict_wl (get_clauses_wl (keep_watch K j w S) ∝ x1b) (keep_watch K j w S)), j + 1, w + 1, set_conflict_wl (get_clauses_wl (keep_watch K j w S) ∝ x1) (keep_watch K j w S)) ∈ {((j', n', T'), j, n, T). j' = j ∧ n' = n ∧ T = T' ∧ literals_are_ℒ⇩i⇩n 𝒜 T'}› if ‹unit_propagation_inner_loop_wl_loop_pre K (j, w, S)› and ‹unit_propagation_inner_loop_wl_loop_D_pre K (j, w, S)› and ‹x2 = (x1a, x2a)› and ‹watched_by S K ! w = (x1, x2)› and ‹x2b = (x1c, x2c)› and ‹watched_by S K ! w = (x1b, x2b)› and ‹unit_prop_body_wl_inv (keep_watch K j w S) j w K› and ‹unit_prop_body_wl_D_inv (keep_watch K j w S) j w K› and ‹polarity (get_trail_wl (keep_watch K j w S)) x1c ≠ Some True› and ‹polarity (get_trail_wl (keep_watch K j w S)) x1a ≠ Some True› and ‹x2c› and ‹x2a› and ‹polarity (get_trail_wl (keep_watch K j w S)) x1c = Some False› and ‹polarity (get_trail_wl (keep_watch K j w S)) x1a = Some False› for x1 x2 x1a x2a x1b x2b x1c x2c proof - show ?thesis using that assms by (auto simp: literals_are_ℒ⇩i⇩n_set_conflict_wl unit_propagation_inner_loop_wl_loop_pre_def) qed have bin_prop: ‹((j + 1, w + 1, propagate_lit_wl_bin x1c x1b (if get_clauses_wl (keep_watch K j w S) ∝ x1b ! 0 = K then 0 else 1) (keep_watch K j w S)), j + 1, w + 1, propagate_lit_wl_bin x1a x1 (if get_clauses_wl (keep_watch K j w S) ∝ x1 ! 0 = K then 0 else 1) (keep_watch K j w S)) ∈ {((j', n', T'), j, n, T). j' = j ∧ n' = n ∧ T = T' ∧ literals_are_ℒ⇩i⇩n 𝒜 T'}› if ‹unit_propagation_inner_loop_wl_loop_pre K (j, w, S)› and ‹unit_propagation_inner_loop_wl_loop_D_pre K (j, w, S)› and ‹x2 = (x1a, x2a)› and ‹watched_by S K ! w = (x1, x2)› and ‹x2b = (x1c, x2c)› and ‹watched_by S K ! w = (x1b, x2b)› and ‹unit_prop_body_wl_inv (keep_watch K j w S) j w K› and ‹unit_prop_body_wl_D_inv (keep_watch K j w S) j w K› and ‹polarity (get_trail_wl (keep_watch K j w S)) x1c ≠ Some True› and ‹polarity (get_trail_wl (keep_watch K j w S)) x1a ≠ Some True› and ‹x2c› and ‹x2a› and ‹polarity (get_trail_wl (keep_watch K j w S)) x1c ≠ Some False› and ‹polarity (get_trail_wl (keep_watch K j w S)) x1a ≠ Some False› and ‹propagate_proper_bin_case K x1a (keep_watch K j w S) x1› for x1 x2 x1a x2a x1b x2b x1c x2c unfolding propagate_lit_wl_bin_def S propagate_proper_bin_case_def apply clarify apply refine_vcg using that 𝒜⇩i⇩n by (simp_all add: unit_prop_body_wl_find_unwatched_inv_def propagate_proper_bin_case_def unit_prop_body_wl_inv_def S unit_prop_body_wl_D_inv_def keep_watch_def state_wl_l_def literals_are_ℒ⇩i⇩n_def Let_def blits_in_ℒ⇩i⇩n_propagate) show ?thesis unfolding unit_propagation_inner_loop_body_wl_D_def find_unwatched_wl_def[symmetric] unfolding unit_propagation_inner_loop_body_wl_def supply [[goals_limit=1]] apply (refine_rcg find_unwatched f') subgoal using assms unfolding unit_propagation_inner_loop_wl_loop_D_inv_def unit_propagation_inner_loop_wl_loop_D_pre_def unit_propagation_inner_loop_wl_loop_pre_def by auto subgoal using assms unfolding unit_prop_body_wl_D_inv_def unit_propagation_inner_loop_wl_loop_pre_def by auto subgoal by simp subgoal using assms by (auto simp: unit_propagation_inner_loop_wl_loop_pre_def) subgoal by simp subgoal using assms by (auto simp: unit_prop_body_wl_D_inv_clauses_distinct_eq unit_propagation_inner_loop_wl_loop_pre_def) subgoal by auto subgoal by (rule bin_set_conflict) subgoal for x1 x2 x1a x2a x1b x2b x1c x2c by (rule bin_prop) subgoal by simp subgoal using assms by (auto simp: unit_prop_body_wl_D_inv_clauses_distinct_eq unit_propagation_inner_loop_wl_loop_pre_def) subgoal by simp subgoal by (rule update_blit_wl) auto subgoal by simp subgoal using assms unfolding unit_prop_body_wl_D_find_unwatched_inv_def unit_prop_body_wl_inv_def by (cases ‹watched_by S K ! w›) (auto simp: unit_prop_body_wl_D_inv_clauses_distinct_eq twl_st_wl) subgoal by (auto simp: twl_st_wl) subgoal by (auto simp: twl_st_wl) subgoal for x1 x2 x1a x2a f fa by (rule set_conflict_rel) subgoal by (rule propagate_lit_wl[OF _ _ H H]; assumption?) (simp add: assms literals_are_ℒ⇩i⇩n_keep_watch assms unit_propagation_inner_loop_wl_loop_pre_def) subgoal by (auto simp: twl_st_wl) subgoal by (rule update_blit_wl') auto subgoal by (rule update_clause_wl[OF _ _ _ _ _ _ _ H H]; assumption?) (auto simp: assms unit_propagation_inner_loop_wl_loop_pre_def) done qed lemma unit_propagation_inner_loop_body_wl_D_unit_propagation_inner_loop_body_wl_D: ‹(uncurry3 unit_propagation_inner_loop_body_wl_D, uncurry3 unit_propagation_inner_loop_body_wl) ∈ [λ(((K, j), w), S). literals_are_ℒ⇩i⇩n 𝒜 S ∧ K ∈# ℒ⇩a⇩l⇩l 𝒜]⇩f Id ×⇩r Id ×⇩r Id ×⇩r Id → ⟨nat_rel ×⇩r nat_rel ×⇩r {(T', T). T = T' ∧ literals_are_ℒ⇩i⇩n 𝒜 T}⟩ nres_rel› (is ‹?G1›) and unit_propagation_inner_loop_body_wl_D_unit_propagation_inner_loop_body_wl_D_weak: ‹(uncurry3 unit_propagation_inner_loop_body_wl_D, uncurry3 unit_propagation_inner_loop_body_wl) ∈ [λ(((K, j), w), S). literals_are_ℒ⇩i⇩n 𝒜 S ∧ K ∈# ℒ⇩a⇩l⇩l 𝒜]⇩f Id ×⇩r Id ×⇩r Id ×⇩r Id → ⟨nat_rel ×⇩r nat_rel ×⇩r Id⟩ nres_rel› (is ‹?G2›) proof - have 1: ‹nat_rel ×⇩r nat_rel ×⇩r {(T', T). T = T' ∧ literals_are_ℒ⇩i⇩n 𝒜 T} = {((j', n', T'), (j, (n, T))). j' = j ∧ n' = n ∧ T = T' ∧ literals_are_ℒ⇩i⇩n 𝒜 T'}› by auto show ?G1 by (auto simp add: fref_def nres_rel_def uncurry_def simp del: twl_st_of_wl.simps intro!: unit_propagation_inner_loop_body_wl_D_spec[of _ 𝒜, unfolded 1[symmetric]]) then show ?G2 apply - apply (match_spec) apply (match_fun_rel; match_fun_rel?) by fastforce+ qed definition unit_propagation_inner_loop_wl_loop_D :: ‹nat literal ⇒ nat twl_st_wl ⇒ (nat × nat × nat twl_st_wl) nres› where ‹unit_propagation_inner_loop_wl_loop_D L S⇩0 = do { ASSERT(L ∈# ℒ⇩a⇩l⇩l (all_atms_st S⇩0)); let n = length (watched_by S⇩0 L); WHILE⇩T⇗unit_propagation_inner_loop_wl_loop_D_inv L⇖ (λ(j, w, S). w < n ∧ get_conflict_wl S = None) (λ(j, w, S). do { unit_propagation_inner_loop_body_wl_D L j w S }) (0, 0, S⇩0) } › lemma unit_propagation_inner_loop_wl_spec: assumes 𝒜⇩i⇩n: ‹literals_are_ℒ⇩i⇩n 𝒜 S› and K: ‹K ∈# ℒ⇩a⇩l⇩l 𝒜› shows ‹unit_propagation_inner_loop_wl_loop_D K S ≤ ⇓ {((j', n', T'), j, n, T). j' = j ∧ n' = n ∧ T = T' ∧ literals_are_ℒ⇩i⇩n 𝒜 T'} (unit_propagation_inner_loop_wl_loop K S)› proof - have u: ‹unit_propagation_inner_loop_body_wl_D K j w S ≤ ⇓ {((j', n', T'), j, n, T). j' = j ∧ n' = n ∧ T = T' ∧ literals_are_ℒ⇩i⇩n 𝒜 T'} (unit_propagation_inner_loop_body_wl K' j' w' S')› if ‹K ∈# ℒ⇩a⇩l⇩l 𝒜› and ‹literals_are_ℒ⇩i⇩n 𝒜 S› and ‹S = S'› ‹K = K'› ‹w = w'› ‹j'=j› for S S' and w w' and K K' and j' j using unit_propagation_inner_loop_body_wl_D_spec[of K 𝒜 S j w] that by auto show ?thesis unfolding unit_propagation_inner_loop_wl_loop_D_def unit_propagation_inner_loop_wl_loop_def apply (refine_vcg u) subgoal using assms by auto subgoal using assms by auto subgoal using assms unfolding unit_propagation_inner_loop_wl_loop_D_inv_def by (auto dest: literals_are_ℒ⇩i⇩n_set_mset_ℒ⇩a⇩l⇩l) subgoal by auto subgoal using K by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto done qed definition unit_propagation_inner_loop_wl_D :: ‹nat literal ⇒ nat twl_st_wl ⇒ nat twl_st_wl nres› where ‹unit_propagation_inner_loop_wl_D L S⇩0 = do { (j, w, S) ← unit_propagation_inner_loop_wl_loop_D L S⇩0; ASSERT (j ≤ w ∧ w ≤ length (watched_by S L) ∧ L ∈# ℒ⇩a⇩l⇩l (all_atms_st S⇩0) ∧ L ∈# ℒ⇩a⇩l⇩l (all_atms_st S)); S ← cut_watch_list j w L S; RETURN S }› lemma unit_propagation_inner_loop_wl_D_spec: assumes 𝒜⇩i⇩n: ‹literals_are_ℒ⇩i⇩n 𝒜 S› and K: ‹K ∈# ℒ⇩a⇩l⇩l 𝒜› shows ‹unit_propagation_inner_loop_wl_D K S ≤ ⇓ {(T', T). T = T' ∧ literals_are_ℒ⇩i⇩n 𝒜 T} (unit_propagation_inner_loop_wl K S)› proof - have cut_watch_list: ‹cut_watch_list x1b x1c K x2c ⤜ RETURN ≤ ⇓ {(T', T). T = T' ∧ literals_are_ℒ⇩i⇩n 𝒜 T} (cut_watch_list x1 x1a K x2a)› if ‹(x, x') ∈ {((j', n', T'), j, n, T). j' = j ∧ n' = n ∧ T = T' ∧ literals_are_ℒ⇩i⇩n 𝒜 T'}› and ‹x2 = (x1a, x2a)› and ‹x' = (x1, x2)› and ‹x2b = (x1c, x2c)› and ‹x = (x1b, x2b)› and ‹x1 ≤ x1a ∧ x1a ≤ length (watched_by x2a K)› for x x' x1 x2 x1a x2a x1b x2b x1c x2c proof - show ?thesis using that unfolding literals_are_ℒ⇩i⇩n_def by (cases x2c) (auto simp: cut_watch_list_def blits_in_ℒ⇩i⇩n_def dest!: in_set_takeD in_set_dropD) qed show ?thesis unfolding unit_propagation_inner_loop_wl_D_def unit_propagation_inner_loop_wl_def apply (refine_vcg unit_propagation_inner_loop_wl_spec[of 𝒜]) subgoal using 𝒜⇩i⇩n . subgoal using K . subgoal by auto subgoal by auto subgoal using 𝒜⇩i⇩n K by auto subgoal using 𝒜⇩i⇩n K by auto subgoal by (rule cut_watch_list) done qed definition unit_propagation_outer_loop_wl_D_inv where ‹unit_propagation_outer_loop_wl_D_inv S ⟷ unit_propagation_outer_loop_wl_inv S ∧ literals_are_ℒ⇩i⇩n (all_atms_st S) S› definition unit_propagation_outer_loop_wl_D :: ‹nat twl_st_wl ⇒ nat twl_st_wl nres› where ‹unit_propagation_outer_loop_wl_D S⇩0 = WHILE⇩T⇗unit_propagation_outer_loop_wl_D_inv⇖ (λS. literals_to_update_wl S ≠ {#}) (λS. do { ASSERT(literals_to_update_wl S ≠ {#}); (S', L) ← select_and_remove_from_literals_to_update_wl S; ASSERT(L ∈# ℒ⇩a⇩l⇩l (all_atms_st S)); unit_propagation_inner_loop_wl_D L S' }) (S⇩0 :: nat twl_st_wl)› lemma literals_are_ℒ⇩i⇩n_set_lits_to_upd[twl_st_wl, simp]: ‹literals_are_ℒ⇩i⇩n 𝒜 (set_literals_to_update_wl C S) ⟷ literals_are_ℒ⇩i⇩n 𝒜 S› by (cases S) (auto simp: literals_are_ℒ⇩i⇩n_def blits_in_ℒ⇩i⇩n_def) lemma unit_propagation_outer_loop_wl_D_spec: assumes 𝒜⇩i⇩n: ‹literals_are_ℒ⇩i⇩n 𝒜 S› shows ‹unit_propagation_outer_loop_wl_D S ≤ ⇓ {(T', T). T = T' ∧ literals_are_ℒ⇩i⇩n 𝒜 T} (unit_propagation_outer_loop_wl S)› proof - have H: ‹set_mset (all_lits_of_mm (mset `# ran_mf (get_clauses_wl S') + get_unit_clauses_wl S')) = set_mset (ℒ⇩a⇩l⇩l (all_atms_st S'))› for S' by (auto simp: in_all_lits_of_mm_ain_atms_of_iff all_atms_def all_lits_def in_ℒ⇩a⇩l⇩l_atm_of_𝒜⇩i⇩n) have select: ‹select_and_remove_from_literals_to_update_wl S ≤ ⇓ {((T', L'), (T, L)). T = T' ∧ L = L' ∧ T = set_literals_to_update_wl (literals_to_update_wl S - {#L#}) S} (select_and_remove_from_literals_to_update_wl S')› if ‹S = S'› for S S' :: ‹nat twl_st_wl› unfolding select_and_remove_from_literals_to_update_wl_def select_and_remove_from_literals_to_update_def apply (rule RES_refine) using that unfolding select_and_remove_from_literals_to_update_wl_def by blast have unit_prop: ‹literals_are_ℒ⇩i⇩n 𝒜 S ⟹ K ∈# ℒ⇩a⇩l⇩l 𝒜 ⟹ unit_propagation_inner_loop_wl_D K S ≤ ⇓ {(T', T). T = T' ∧ literals_are_ℒ⇩i⇩n 𝒜 T} (unit_propagation_inner_loop_wl K' S')› if ‹K = K'› and ‹S = S'› for K K' and S S' :: ‹nat twl_st_wl› unfolding that by (rule unit_propagation_inner_loop_wl_D_spec) show ?thesis unfolding unit_propagation_outer_loop_wl_D_def unit_propagation_outer_loop_wl_def H apply (refine_vcg select unit_prop) subgoal using 𝒜⇩i⇩n by simp subgoal unfolding unit_propagation_outer_loop_wl_D_inv_def by auto subgoal by auto subgoal by auto subgoal using 𝒜⇩i⇩n apply simp by auto subgoal by auto subgoal by auto subgoal using 𝒜⇩i⇩n by (auto simp: twl_st_wl) subgoal for S' S T'L' TL T' L' T L using 𝒜⇩i⇩n by auto done qed lemma unit_propagation_outer_loop_wl_D_spec': shows ‹(unit_propagation_outer_loop_wl_D, unit_propagation_outer_loop_wl) ∈ {(T', T). T = T' ∧ literals_are_ℒ⇩i⇩n 𝒜 T} →⇩f ⟨{(T', T). T = T' ∧ literals_are_ℒ⇩i⇩n 𝒜 T}⟩nres_rel› apply (intro frefI nres_relI) subgoal for x y apply (rule order_trans) apply (rule unit_propagation_outer_loop_wl_D_spec[of 𝒜 x]) apply (auto simp: prod_rel_def intro: conc_fun_R_mono) done done definition skip_and_resolve_loop_wl_D_inv where ‹skip_and_resolve_loop_wl_D_inv S⇩0 brk S ≡ skip_and_resolve_loop_wl_inv S⇩0 brk S ∧ literals_are_ℒ⇩i⇩n (all_atms_st S) S› definition skip_and_resolve_loop_wl_D :: ‹nat twl_st_wl ⇒ nat twl_st_wl nres› where ‹skip_and_resolve_loop_wl_D S⇩0 = do { ASSERT(get_conflict_wl S⇩0 ≠ None); (_, S) ← WHILE⇩T⇗λ(brk, S). skip_and_resolve_loop_wl_D_inv S⇩0 brk S⇖ (λ(brk, S). ¬brk ∧ ¬is_decided (hd (get_trail_wl S))) (λ(brk, S). do { ASSERT(¬brk ∧ ¬is_decided (hd (get_trail_wl S))); let D' = the (get_conflict_wl S); let (L, C) = lit_and_ann_of_propagated (hd (get_trail_wl S)); if -L ∉# D' then do {RETURN (False, tl_state_wl S)} else if get_maximum_level (get_trail_wl S) (remove1_mset (-L) D') = count_decided (get_trail_wl S) then do {RETURN (update_confl_tl_wl C L S)} else do {RETURN (True, S)} } ) (False, S⇩0); RETURN S } › lemma literals_are_ℒ⇩i⇩n_tl_state_wl[simp]: ‹literals_are_ℒ⇩i⇩n 𝒜 (tl_state_wl S) = literals_are_ℒ⇩i⇩n 𝒜 S› by (cases S) (auto simp: is_ℒ⇩a⇩l⇩l_def tl_state_wl_def literals_are_ℒ⇩i⇩n_def blits_in_ℒ⇩i⇩n_def) lemma get_clauses_wl_tl_state: ‹get_clauses_wl (tl_state_wl T) = get_clauses_wl T› unfolding tl_state_wl_def by (cases T) auto lemma blits_in_ℒ⇩i⇩n_skip_and_resolve[simp]: ‹blits_in_ℒ⇩i⇩n (tl x1aa, N, D, ar, as, at, bd) = blits_in_ℒ⇩i⇩n (x1aa, N, D, ar, as, at, bd)› ‹blits_in_ℒ⇩i⇩n (x1aa, N, Some (resolve_cls_wl' (x1aa', N', x1ca', ar', as', at', bd') x2b x1b), ar, as, at, bd) = blits_in_ℒ⇩i⇩n (x1aa, N, x1ca', ar, as, at, bd)› by (auto simp: blits_in_ℒ⇩i⇩n_def) lemma skip_and_resolve_loop_wl_D_spec: assumes 𝒜⇩i⇩n: ‹literals_are_ℒ⇩i⇩n 𝒜 S› shows ‹skip_and_resolve_loop_wl_D S ≤ ⇓ {(T', T). T = T' ∧ literals_are_ℒ⇩i⇩n 𝒜 T ∧ get_clauses_wl T = get_clauses_wl S} (skip_and_resolve_loop_wl S)› (is ‹_ ≤ ⇓ ?R _›) proof - define invar where ‹invar = (λ(brk, T). skip_and_resolve_loop_wl_D_inv S brk T)› have 1: ‹((get_conflict_wl S = Some {#}, S), get_conflict_wl S = Some {#}, S) ∈ Id› by auto show ?thesis unfolding skip_and_resolve_loop_wl_D_def skip_and_resolve_loop_wl_def apply (subst (2) WHILEIT_add_post_condition) apply (refine_rcg 1 WHILEIT_refine[where R = ‹{((i', S'), (i, S)). i = i' ∧ (S', S) ∈ ?R}›]) subgoal using assms by auto subgoal unfolding skip_and_resolve_loop_wl_D_inv_def by fast subgoal by fast subgoal by fast subgoal by fast subgoal by auto subgoal unfolding skip_and_resolve_loop_wl_D_inv_def update_confl_tl_wl_def by (auto split: prod.splits) (simp add: get_clauses_wl_tl_state) subgoal by auto subgoal unfolding skip_and_resolve_loop_wl_D_inv_def update_confl_tl_wl_def by (auto split: prod.splits simp: literals_are_ℒ⇩i⇩n_def) subgoal by auto subgoal by auto done qed definition find_lit_of_max_level_wl' :: ‹_ ⇒ _ ⇒ _ ⇒ _ ⇒ _ ⇒ _ ⇒ _ ⇒ _ ⇒ nat literal nres› where ‹find_lit_of_max_level_wl' M N D NE UE Q W L = find_lit_of_max_level_wl (M, N, Some D, NE, UE, Q, W) L› definition (in -) list_of_mset2 :: ‹nat literal ⇒ nat literal ⇒ nat clause ⇒ nat clause_l nres› where ‹list_of_mset2 L L' D = SPEC (λE. mset E = D ∧ E!0 = L ∧ E!1 = L' ∧ length E ≥ 2)› definition single_of_mset where ‹single_of_mset D = SPEC(λL. D = mset [L])› definition backtrack_wl_D_inv where ‹backtrack_wl_D_inv S ⟷ backtrack_wl_inv S ∧ literals_are_ℒ⇩i⇩n (all_atms_st S) S› definition propagate_bt_wl_D :: ‹nat literal ⇒ nat literal ⇒ nat twl_st_wl ⇒ nat twl_st_wl nres› where ‹propagate_bt_wl_D = (λL L' (M, N, D, NE, UE, Q, W). do { D'' ← list_of_mset2 (-L) L' (the D); i ← get_fresh_index_wl N (NE+UE) W; let b = (length D'' = 2); RETURN (Propagated (-L) i # M, fmupd i (D'', False) N, None, NE, UE, {#L#}, W(-L:= W (-L) @ [(i, L', b)], L':= W L' @ [(i, -L, b)])) })› definition propagate_unit_bt_wl_D :: ‹nat literal ⇒ nat twl_st_wl ⇒ (nat twl_st_wl) nres› where ‹propagate_unit_bt_wl_D = (λL (M, N, D, NE, UE, Q, W). do { D' ← single_of_mset (the D); RETURN (Propagated (-L) 0 # M, N, None, NE, add_mset {#D'#} UE, {#L#}, W) })› definition backtrack_wl_D :: ‹nat twl_st_wl ⇒ nat twl_st_wl nres› where ‹backtrack_wl_D S = do { ASSERT(backtrack_wl_D_inv S); let L = lit_of (hd (get_trail_wl S)); S ← extract_shorter_conflict_wl S; S ← find_decomp_wl L S; if size (the (get_conflict_wl S)) > 1 then do { L' ← find_lit_of_max_level_wl S L; propagate_bt_wl_D L L' S } else do { propagate_unit_bt_wl_D L S } }› lemma backtrack_wl_D_spec: fixes S :: ‹nat twl_st_wl› assumes 𝒜⇩i⇩n: ‹literals_are_ℒ⇩i⇩n 𝒜 S› and confl: ‹get_conflict_wl S ≠ None› shows ‹backtrack_wl_D S ≤ ⇓ {(T', T). T = T' ∧ literals_are_ℒ⇩i⇩n 𝒜 T} (backtrack_wl S)› proof - have 1: ‹((get_conflict_wl S = Some {#}, S), get_conflict_wl S = Some {#}, S) ∈ Id› by auto have 3: ‹find_lit_of_max_level_wl S M ≤ ⇓{(L', L). L' ∈# remove1_mset (-M) (the (get_conflict_wl S)) ∧ L' = L} (find_lit_of_max_level_wl S' M')› if ‹S = S'› and ‹M = M'› for S S' :: ‹nat twl_st_wl› and M M' using that by (cases S; cases S') (auto simp: find_lit_of_max_level_wl_def intro!: RES_refine) have H: ‹mset `# mset (take n (tl xs)) + a + (mset `# mset (drop (Suc n) xs) + b) = mset `# mset (tl xs) + a + b› for n and xs :: ‹'a list list› and a b apply (subst (2) append_take_drop_id[of n ‹tl xs›, symmetric]) apply (subst mset_append) by (auto simp: drop_Suc) have list_of_mset: ‹list_of_mset2 L L' D ≤ ⇓ {(E, F). F = [L, L'] @ remove1 L (remove1 L' E) ∧ D = mset E ∧ E!0 = L ∧ E!1 = L' ∧ E=F} (list_of_mset D')› (is ‹_ ≤ ⇓ ?list_of_mset _›) if ‹D = D'› and uL_D: ‹L ∈# D› and L'_D: ‹L' ∈# D› and L_uL': ‹L ≠ L'› for D D' L L' unfolding list_of_mset_def list_of_mset2_def proof (rule RES_refine) fix s assume s: ‹s ∈ {E. mset E = D ∧ E ! 0 = L ∧ E ! 1 = L' ∧ length E ≥ 2}› then show ‹∃s'∈{D'a. D' = mset D'a}. (s, s') ∈ {(E, F). F = [L, L'] @ remove1 L (remove1 L' E) ∧ D = mset E ∧ E ! 0 = L ∧ E ! 1 = L'∧ E=F}› apply (cases s; cases ‹tl s›) using that by (auto simp: diff_single_eq_union diff_diff_add_mset[symmetric] simp del: diff_diff_add_mset) qed define extract_shorter_conflict_wl' where ‹extract_shorter_conflict_wl' S = extract_shorter_conflict_wl S› for S :: ‹nat twl_st_wl› define find_lit_of_max_level_wl' where ‹find_lit_of_max_level_wl' S = find_lit_of_max_level_wl S› for S :: ‹nat twl_st_wl› have extract_shorter_conflict_wl: ‹extract_shorter_conflict_wl' S ≤ ⇓ {(U, U'). U = U' ∧ equality_except_conflict_wl U S ∧ get_conflict_wl U ≠ None ∧ the (get_conflict_wl U) ⊆# the (get_conflict_wl S) ∧ -lit_of (hd (get_trail_wl S)) ∈# the (get_conflict_wl U) } (extract_shorter_conflict_wl S)› (is ‹_ ≤ ⇓ ?extract_shorter _›) unfolding extract_shorter_conflict_wl'_def extract_shorter_conflict_wl_def by (cases S) (auto 5 5 simp: extract_shorter_conflict_wl'_def extract_shorter_conflict_wl_def intro!: RES_refine) have find_decomp_wl: ‹find_decomp_wl (lit_of (hd (get_trail_wl S))) T ≤ ⇓ {(U, U'). U = U' ∧ equality_except_trail_wl U T} (find_decomp_wl (lit_of (hd (get_trail_wl S))) T')› (is ‹_ ≤ ⇓ ?find_decomp _›) if ‹(T, T') ∈ ?extract_shorter› for T T' using that unfolding find_decomp_wl_def by (cases T) (auto 5 5 intro!: RES_refine) have find_lit_of_max_level_wl: ‹find_lit_of_max_level_wl U (lit_of (hd (get_trail_wl S))) ≤ ⇓ Id (find_lit_of_max_level_wl U' (lit_of (hd (get_trail_wl S))))› if ‹(U, U') ∈ ?find_decomp T› for T U U' using that unfolding find_lit_of_max_level_wl_def by (cases T) (auto 5 5 intro!: RES_refine) have find_lit_of_max_level_wl': ‹find_lit_of_max_level_wl' U (lit_of (hd (get_trail_wl S))) ≤ ⇓{(L, L'). L = L' ∧ L ∈# remove1_mset (-lit_of (hd (get_trail_wl S))) (the (get_conflict_wl U))} (find_lit_of_max_level_wl U' (lit_of (hd (get_trail_wl S))))› (is ‹_ ≤ ⇓ ?find_lit _›) if ‹backtrack_wl_inv S› and ‹backtrack_wl_D_inv S› and ‹(U, U') ∈ ?find_decomp T› and ‹1 < size (the (get_conflict_wl U))› and ‹1 < size (the (get_conflict_wl U'))› for U U' T using that unfolding find_lit_of_max_level_wl'_def find_lit_of_max_level_wl_def by (cases U) (auto 5 5 intro!: RES_refine) have is_ℒ⇩a⇩l⇩l_add: ‹is_ℒ⇩a⇩l⇩l 𝒜 (A + B) ⟷ set_mset A ⊆ set_mset (ℒ⇩a⇩l⇩l 𝒜)› if ‹is_ℒ⇩a⇩l⇩l 𝒜 B› for A B using that unfolding is_ℒ⇩a⇩l⇩l_def by auto have propagate_bt_wl_D: ‹propagate_bt_wl_D (lit_of (hd (get_trail_wl S))) L U ≤ ⇓ {(T', T). T = T' ∧ literals_are_ℒ⇩i⇩n 𝒜 T} (propagate_bt_wl (lit_of (hd (get_trail_wl S))) L' U')› if ‹backtrack_wl_inv S› and bt: ‹backtrack_wl_D_inv S› and TT': ‹(T, T') ∈ ?extract_shorter› and UU': ‹(U, U') ∈ ?find_decomp T› and ‹1 < size (the (get_conflict_wl U))› and ‹1 < size (the (get_conflict_wl U'))› and LL': ‹(L, L') ∈ ?find_lit U› for L L' T T' U U' proof - obtain MS NS DS NES UES W Q where S: ‹S = (MS, NS, Some DS, NES, UES, Q, W)› using bt by (cases S; cases ‹get_conflict_wl S›) (auto simp: backtrack_wl_D_inv_def backtrack_wl_inv_def backtrack_l_inv_def state_wl_l_def) then obtain DT where T: ‹T = (MS, NS, Some DT, NES, UES, Q, W)› and DT: ‹DT ⊆# DS› using TT' by (cases T'; cases ‹get_conflict_wl T'›) auto then obtain MU where U: ‹U = (MU, NS, Some DT, NES, UES, Q, W)› and U': ‹U' = U› using UU' by (cases U) auto define list_of_mset where ‹list_of_mset D L L' = ?list_of_mset D L L'› for D and L L' :: ‹nat literal› have [simp]: ‹get_conflict_wl S = Some DS› using S by auto obtain T U where dist: ‹distinct_mset (the (get_conflict_wl S))› and ST: ‹(S, T) ∈ state_wl_l None› and TU: ‹(T, U) ∈ twl_st_l None› and alien: ‹cdcl⇩W_restart_mset.no_strange_atm (state⇩W_of U)› using bt unfolding backtrack_wl_D_inv_def backtrack_wl_inv_def backtrack_l_inv_def twl_struct_invs_def cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def cdcl⇩W_restart_mset.distinct_cdcl⇩W_state_def apply - apply normalize_goal+ by (auto simp: twl_st_wl twl_st_l twl_st) then have ‹distinct_mset DT› using DT unfolding S by (auto simp: distinct_mset_mono) then have [simp]: ‹L ≠ -lit_of (hd MS)› using LL' by (auto simp: U S dest: distinct_mem_diff_mset) have ‹x ∈# all_lits_of_m (the (get_conflict_wl S)) ⟹ x ∈# all_lits_of_mm ({#mset x. x ∈# ran_mf (get_clauses_wl S)#} + get_unit_clauses_wl S)› for x using alien ST TU unfolding cdcl⇩W_restart_mset.no_strange_atm_def all_clss_lf_ran_m[symmetric] set_mset_union by (auto simp: twl_st_wl twl_st_l twl_st in_all_lits_of_m_ain_atms_of_iff in_all_lits_of_mm_ain_atms_of_iff get_unit_clauses_wl_alt_def) then have ‹x ∈# all_lits_of_m DS ⟹ x ∈# all_lits_of_mm ({#mset x. x ∈# ran_mf NS#} + (NES + UES))› for x by (simp add: S) then have H: ‹x ∈# all_lits_of_m DT ⟹ x ∈# all_lits_of_mm ({#mset x. x ∈# ran_mf NS#} + (NES + UES))› for x using DT all_lits_of_m_mono by blast have propa_ref: ‹((Propagated (- lit_of (hd (get_trail_wl S))) i # MU, fmupd i (D, False) NS, None, NES, UES, unmark (hd (get_trail_wl S)), W (- lit_of (hd (get_trail_wl S)) := W (- lit_of (hd (get_trail_wl S))) @ [(i, L, length D = 2)], L := W L @ [(i, -lit_of (hd (get_trail_wl S)), length D = 2)])), Propagated (- lit_of (hd (get_trail_wl S))) i' # MU, fmupd i' ([- lit_of (hd (get_trail_wl S)), L'] @ remove1 (- lit_of (hd (get_trail_wl S))) (remove1 L' D'), False) NS, None, NES, UES, unmark (hd (get_trail_wl S)), W (- lit_of (hd (get_trail_wl S)) := W (- lit_of (hd (get_trail_wl S))) @ [(i', L', length ([- lit_of (hd (get_trail_wl S)), L'] @ remove1 (- lit_of (hd (get_trail_wl S))) (remove1 L' D')) = 2)], L' := W L' @ [(i', - lit_of (hd (get_trail_wl S)), length ([- lit_of (hd (get_trail_wl S)), L'] @ remove1 (- lit_of (hd (get_trail_wl S))) (remove1 L' D')) = 2)])) ∈ {(T', T). T = T' ∧ literals_are_ℒ⇩i⇩n 𝒜 T}› if DD': ‹(D, D') ∈ list_of_mset (the (Some DT)) (- lit_of (hd (get_trail_wl S))) L› and ii': ‹(i, i') ∈ {(i, i'). i = i' ∧ i ∉# dom_m NS}› for i i' D D' proof - have [simp]: ‹i = i'› ‹L = L'› and i'_dom: ‹i' ∉# dom_m NS› using ii' LL' by auto have D: ‹D = [- lit_of (hd (get_trail_wl S)), L] @ remove1 (- lit_of (hd (get_trail_wl S))) (remove1 L D')› and DT_D: ‹DT = mset D› using DD' unfolding list_of_mset_def by force+ have ‹L ∈ set D› using ii' LL' by (auto simp: U DT_D dest!: in_diffD) have K: ‹L ∈ set D ⟹ L ∈# all_lits_of_m (mset D)› for L unfolding in_multiset_in_set[symmetric] apply (drule multi_member_split) by (auto simp: all_lits_of_m_add_mset) have [simp]: ‹- lit_of (hd (get_trail_wl S)) # L' # remove1 (- lit_of (hd (get_trail_wl S))) (remove1 L' D') = D› using D by simp then have 1[simp]: ‹- lit_of (hd MS) # L' # remove1 (- lit_of (hd MS)) (remove1 L' D') = D› using D by (simp add: S) have ‹- lit_of (hd MS) ∈ set D› apply (subst 1[symmetric]) unfolding set_append list.sel by (rule list.set_intros) have ‹set_mset (all_lits_of_m (mset D)) ⊆ set_mset (all_lits_of_mm ({#mset (fst x). x ∈# ran_m NS#} + (NES + UES)))› by (auto dest!: H[unfolded DT_D]) then have [simp]: ‹is_ℒ⇩a⇩l⇩l 𝒜 (all_lits (fmupd i' (D, False) NS) (NES + UES)) = is_ℒ⇩a⇩l⇩l 𝒜 (all_lits NS (NES + UES))› ‹set_mset (ℒ⇩a⇩l⇩l (atm_of `# all_lits (fmupd i' (D, False) NS) (NES + UES))) = set_mset (ℒ⇩a⇩l⇩l (atm_of `# all_lits NS (NES + UES)))› using i'_dom unfolding is_ℒ⇩a⇩l⇩l_def all_lits_def by (auto 5 5 simp add: ran_m_mapsto_upd_notin all_lits_of_mm_add_mset in_ℒ⇩a⇩l⇩l_atm_of_𝒜⇩i⇩n atm_of_eq_atm_of) have ‹x ∈# all_lits_of_mm ({#mset (fst x). x ∈# ran_m NS#} + (NES + UES)) ⟹ x ∈# ℒ⇩a⇩l⇩l 𝒜› for x using i'_dom 𝒜⇩i⇩n unfolding is_ℒ⇩a⇩l⇩l_def literals_are_ℒ⇩i⇩n_def by (auto simp: S all_lits_def) then show ?thesis using i'_dom 𝒜⇩i⇩n K[OF ‹L ∈ set D›] K[OF ‹- lit_of (hd MS) ∈ set D›] unfolding literals_are_ℒ⇩i⇩n_def by (auto simp: ran_m_mapsto_upd_notin all_lits_of_mm_add_mset blits_in_ℒ⇩i⇩n_def is_ℒ⇩a⇩l⇩l_add S dest!: H[unfolded DT_D]) qed define get_fresh_index2 where ‹get_fresh_index2 N NUE W = get_fresh_index_wl (N :: nat clauses_l) (NUE :: nat clauses) (W::nat literal ⇒ (nat watcher) list)› for N NUE W have fresh: ‹get_fresh_index_wl N NUE W ≤ ⇓ {(i, i'). i = i' ∧ i ∉# dom_m N} (get_fresh_index2 N' NUE' W')› if ‹N = N'› ‹NUE = NUE'› ‹W=W'›for N N' NUE NUE' W W' using that by (auto simp: get_fresh_index_wl_def get_fresh_index2_def intro!: RES_refine) show ?thesis unfolding propagate_bt_wl_D_def propagate_bt_wl_def propagate_bt_wl_D_def U U' S T apply (subst (2) get_fresh_index2_def[symmetric]) apply clarify apply (refine_rcg list_of_mset fresh) subgoal .. subgoal using TT' T by (auto simp: U S) subgoal using LL' by (auto simp: T U S dest: in_diffD) subgoal by auto subgoal .. subgoal .. subgoal .. subgoal for D D' i i' unfolding list_of_mset_def[symmetric] U[symmetric] U'[symmetric] S[symmetric] T[symmetric] by (rule propa_ref) done qed have propagate_unit_bt_wl_D: ‹propagate_unit_bt_wl_D (lit_of (hd (get_trail_wl S))) U ≤ SPEC (λc. (c, propagate_unit_bt_wl (lit_of (hd (get_trail_wl S))) U') ∈ {(T', T). T = T' ∧ literals_are_ℒ⇩i⇩n 𝒜 T})› if ‹backtrack_wl_inv S› and bt: ‹backtrack_wl_D_inv S› and TT': ‹(T, T') ∈ ?extract_shorter› and UU': ‹(U, U') ∈ ?find_decomp T› and ‹¬1 < size (the (get_conflict_wl U))› and ‹¬1 < size (the (get_conflict_wl U'))› for L L' T T' U U' proof - obtain MS NS DS NES UES W Q where S: ‹S = (MS, NS, Some DS, NES, UES, Q, W)› using bt by (cases S; cases ‹get_conflict_wl S›) (auto simp: backtrack_wl_D_inv_def backtrack_wl_inv_def backtrack_l_inv_def state_wl_l_def) then obtain DT where T: ‹T = (MS, NS, Some DT, NES, UES, Q, W)› and DT: ‹DT ⊆# DS› using TT' by (cases T'; cases ‹get_conflict_wl T'›) auto then obtain MU where U: ‹U = (MU, NS, Some DT, NES, UES, Q, W)› and U': ‹U' = U› using UU' by (cases U) auto define list_of_mset where ‹list_of_mset D L L' = ?list_of_mset D L L'› for D and L L' :: ‹nat literal› have [simp]: ‹get_conflict_wl S = Some DS› using S by auto obtain T U where dist: ‹distinct_mset (the (get_conflict_wl S))› and ST: ‹(S, T) ∈ state_wl_l None› and TU: ‹(T, U) ∈ twl_st_l None› and alien: ‹cdcl⇩W_restart_mset.no_strange_atm (state⇩W_of U)› using bt unfolding backtrack_wl_D_inv_def backtrack_wl_inv_def backtrack_l_inv_def twl_struct_invs_def cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def cdcl⇩W_restart_mset.distinct_cdcl⇩W_state_def apply - apply normalize_goal+ by (auto simp: twl_st_wl twl_st_l twl_st) then have ‹distinct_mset DT› using DT unfolding S by (auto simp: distinct_mset_mono) have ‹x ∈# all_lits_of_m (the (get_conflict_wl S)) ⟹ x ∈# all_lits_of_mm ({#mset x. x ∈# ran_mf (get_clauses_wl S)#} + get_unit_init_clss_wl S)› for x using alien ST TU unfolding cdcl⇩W_restart_mset.no_strange_atm_def all_clss_lf_ran_m[symmetric] set_mset_union by (auto simp: twl_st_wl twl_st_l twl_st in_all_lits_of_m_ain_atms_of_iff in_all_lits_of_mm_ain_atms_of_iff) then have ‹x ∈# all_lits_of_m DS ⟹ x ∈# all_lits_of_mm ({#mset x. x ∈# ran_mf NS#} + NES)› for x by (simp add: S) then have H: ‹x ∈# all_lits_of_m DT ⟹ x ∈# all_lits_of_mm ({#mset x. x ∈# ran_mf NS#} + NES)› for x using DT all_lits_of_m_mono by blast then have 𝒜⇩i⇩n_D: ‹literals_are_in_ℒ⇩i⇩n 𝒜 DT› using DT 𝒜⇩i⇩n unfolding literals_are_in_ℒ⇩i⇩n_def S is_ℒ⇩a⇩l⇩l_def literals_are_ℒ⇩i⇩n_def by (auto simp: all_lits_of_mm_union all_lits_def) have [simp]: ‹is_ℒ⇩a⇩l⇩l 𝒜 (all_lits NS (add_mset {#x#} (NES + UES))) = is_ℒ⇩a⇩l⇩l 𝒜 (all_lits NS (NES + UES))› ‹set_mset (ℒ⇩a⇩l⇩l (atm_of `# all_lits NS (add_mset {#x#} (NES + UES)))) = set_mset (ℒ⇩a⇩l⇩l (atm_of `# all_lits NS (NES + UES)))› if ‹DT = {#x#}› for x using H[of x] H[of ‹-x›] that unfolding is_ℒ⇩a⇩l⇩l_def all_lits_def by (auto simp add: all_lits_of_mm_add_mset in_ℒ⇩a⇩l⇩l_atm_of_𝒜⇩i⇩n atm_of_eq_atm_of all_lits_of_m_add_mset insert_absorb all_lits_of_mm_union) show ?thesis unfolding propagate_unit_bt_wl_D_def propagate_unit_bt_wl_def U U' single_of_mset_def apply clarify apply refine_vcg using 𝒜⇩i⇩n_D 𝒜⇩i⇩n unfolding literals_are_ℒ⇩i⇩n_def by (auto simp: clauses_def mset_take_mset_drop_mset mset_take_mset_drop_mset' all_lits_of_mm_add_mset is_ℒ⇩a⇩l⇩l_add literals_are_in_ℒ⇩i⇩n_def S blits_in_ℒ⇩i⇩n_def) qed show ?thesis unfolding backtrack_wl_D_def backtrack_wl_def find_lit_of_max_level_wl'_def apply (subst extract_shorter_conflict_wl'_def[symmetric]) apply (subst find_lit_of_max_level_wl'_def[symmetric]) supply [[goals_limit=1]] apply (refine_vcg extract_shorter_conflict_wl find_lit_of_max_level_wl find_decomp_wl find_lit_of_max_level_wl' propagate_bt_wl_D propagate_unit_bt_wl_D) subgoal using 𝒜⇩i⇩n unfolding backtrack_wl_D_inv_def by fast subgoal by auto by assumption+ qed subsubsection ‹Decide or Skip› definition find_unassigned_lit_wl_D :: ‹nat twl_st_wl ⇒ (nat twl_st_wl × nat literal option) nres› where ‹find_unassigned_lit_wl_D S = ( SPEC(λ((M, N, D, NE, UE, WS, Q), L). S = (M, N, D, NE, UE, WS, Q) ∧ (L ≠ None ⟶ undefined_lit M (the L) ∧ the L ∈# ℒ⇩a⇩l⇩l (all_atms N NE) ∧ atm_of (the L) ∈ atms_of_mm (clause `# twl_clause_of `# init_clss_lf N + NE)) ∧ (L = None ⟶ (∄L'. undefined_lit M L' ∧ atm_of L' ∈ atms_of_mm (clause `# twl_clause_of `# init_clss_lf N + NE))))) › definition decide_wl_or_skip_D_pre :: ‹nat twl_st_wl ⇒ bool› where ‹decide_wl_or_skip_D_pre S ⟷ decide_wl_or_skip_pre S ∧ literals_are_ℒ⇩i⇩n (all_atms_st S) S› definition decide_wl_or_skip_D :: ‹nat twl_st_wl ⇒ (bool × nat twl_st_wl) nres› where ‹decide_wl_or_skip_D S = (do { ASSERT(decide_wl_or_skip_D_pre S); (S, L) ← find_unassigned_lit_wl_D S; case L of None ⇒ RETURN (True, S) | Some L ⇒ RETURN (False, decide_lit_wl L S) }) › theorem decide_wl_or_skip_D_spec: assumes ‹literals_are_ℒ⇩i⇩n 𝒜 S› shows ‹decide_wl_or_skip_D S ≤ ⇓ {((b', T'), b, T). b = b' ∧ T = T' ∧ literals_are_ℒ⇩i⇩n 𝒜 T} (decide_wl_or_skip S)› proof - have H: ‹find_unassigned_lit_wl_D S ≤ ⇓ {((S', L'), L). S' = S ∧ L = L' ∧ literals_are_ℒ⇩i⇩n 𝒜 S ∧ (L ≠ None ⟶ undefined_lit (get_trail_wl S) (the L) ∧ atm_of (the L) ∈ atms_of_mm (clause `# twl_clause_of `# init_clss_lf (get_clauses_wl S) + get_unit_init_clss_wl S)) ∧ (L = None ⟶ (∄L'. undefined_lit (get_trail_wl S) L' ∧ atm_of L' ∈ atms_of_mm (clause `# twl_clause_of `# init_clss_lf (get_clauses_wl S) + get_unit_init_clss_wl S)))} (find_unassigned_lit_wl S')› (is ‹_ ≤ ⇓ ?find _›) if ‹S = S'› and ‹literals_are_ℒ⇩i⇩n 𝒜 S› for S S' :: ‹nat twl_st_wl› using that(2) unfolding find_unassigned_lit_wl_def find_unassigned_lit_wl_D_def that(1) by (cases S') (auto intro!: RES_refine simp: mset_take_mset_drop_mset') have [refine]: ‹x = x' ⟹ (x, x') ∈ ⟨Id⟩ option_rel› for x x' by auto have decide_lit_wl: ‹((False, decide_lit_wl L T), False, decide_lit_wl L' S') ∈ {((b', T'), b, T). b = b' ∧ T = T' ∧ literals_are_ℒ⇩i⇩n 𝒜 T}› if SS': ‹(S, S') ∈ {(T', T). T = T' ∧ literals_are_ℒ⇩i⇩n 𝒜 T}› and ‹decide_wl_or_skip_pre S'› and pre: ‹decide_wl_or_skip_D_pre S› and LT_L': ‹(LT, bL') ∈ ?find S› and LT: ‹LT = (T, bL)› and ‹bL' = Some L'› and ‹bL = Some L› and LL': ‹(L, L') ∈ Id› for S S' L L' LT bL bL' T proof - have 𝒜⇩i⇩n: ‹literals_are_ℒ⇩i⇩n 𝒜 T› and [simp]: ‹T = S› using LT_L' pre unfolding LT decide_wl_or_skip_D_pre_def by fast+ have [simp]: ‹S' = S› ‹L = L'› using SS' LL' by simp_all have ‹literals_are_ℒ⇩i⇩n 𝒜 (decide_lit_wl L' S)› using 𝒜⇩i⇩n by (cases S) (auto simp: decide_lit_wl_def clauses_def blits_in_ℒ⇩i⇩n_def literals_are_ℒ⇩i⇩n_def) then show ?thesis by auto qed have ‹(decide_wl_or_skip_D, decide_wl_or_skip) ∈ {(T', T). T = T' ∧ literals_are_ℒ⇩i⇩n 𝒜 T} →⇩f ⟨{((b', T'), (b, T)). b = b' ∧ T = T' ∧ literals_are_ℒ⇩i⇩n 𝒜 T}⟩ nres_rel› unfolding decide_wl_or_skip_D_def decide_wl_or_skip_def apply (intro frefI) apply (refine_vcg H) subgoal unfolding decide_wl_or_skip_D_pre_def by blast subgoal by simp subgoal by auto subgoal by simp subgoal unfolding decide_wl_or_skip_D_pre_def by fast subgoal by (rule decide_lit_wl) assumption+ done then show ?thesis using assms by (cases S) (auto simp: fref_def nres_rel_def) qed subsubsection ‹Backtrack, Skip, Resolve or Decide› definition cdcl_twl_o_prog_wl_D_pre where ‹cdcl_twl_o_prog_wl_D_pre S ⟷ cdcl_twl_o_prog_wl_pre S ∧ literals_are_ℒ⇩i⇩n (all_atms_st S) S› definition cdcl_twl_o_prog_wl_D :: ‹nat twl_st_wl ⇒ (bool × nat twl_st_wl) nres› where ‹cdcl_twl_o_prog_wl_D S = do { ASSERT(cdcl_twl_o_prog_wl_D_pre S); if get_conflict_wl S = None then decide_wl_or_skip_D S else do { if count_decided (get_trail_wl S) > 0 then do { T ← skip_and_resolve_loop_wl_D S; ASSERT(get_conflict_wl T ≠ None ∧ get_clauses_wl S = get_clauses_wl T); U ← backtrack_wl_D T; RETURN (False, U) } else RETURN (True, S) } } › theorem cdcl_twl_o_prog_wl_D_spec: assumes ‹literals_are_ℒ⇩i⇩n 𝒜 S› shows ‹cdcl_twl_o_prog_wl_D S ≤ ⇓ {((b', T'), (b, T)). b = b' ∧ T = T' ∧ literals_are_ℒ⇩i⇩n 𝒜 T} (cdcl_twl_o_prog_wl S)› proof - have 1: ‹backtrack_wl_D S ≤ ⇓ {(T', T). T = T' ∧ literals_are_ℒ⇩i⇩n 𝒜 T} (backtrack_wl T)› if ‹literals_are_ℒ⇩i⇩n 𝒜 S› and ‹get_conflict_wl S ≠ None› and ‹S = T› for S T using backtrack_wl_D_spec[of 𝒜 S] that by fast have 2: ‹skip_and_resolve_loop_wl_D S ≤ ⇓ {(T', T). T = T' ∧ literals_are_ℒ⇩i⇩n 𝒜 T ∧ get_clauses_wl T = get_clauses_wl S} (skip_and_resolve_loop_wl T)› if 𝒜⇩i⇩n: ‹literals_are_ℒ⇩i⇩n 𝒜 S› ‹S = T› for S T using skip_and_resolve_loop_wl_D_spec[of 𝒜 S] that by fast show ?thesis using assms unfolding cdcl_twl_o_prog_wl_D_def cdcl_twl_o_prog_wl_def apply (refine_vcg decide_wl_or_skip_D_spec 1 2) subgoal unfolding cdcl_twl_o_prog_wl_D_pre_def by auto subgoal by simp subgoal by simp subgoal by simp subgoal by simp subgoal by auto subgoal by auto subgoal by auto subgoal by simp subgoal by auto subgoal by auto done qed theorem cdcl_twl_o_prog_wl_D_spec': ‹(cdcl_twl_o_prog_wl_D, cdcl_twl_o_prog_wl) ∈ {(S,S'). (S,S') ∈ Id ∧literals_are_ℒ⇩i⇩n 𝒜 S} →⇩f ⟨bool_rel ×⇩r {(T', T). T = T' ∧ literals_are_ℒ⇩i⇩n 𝒜 T}⟩ nres_rel› apply (intro frefI nres_relI) subgoal for x y apply (rule order_trans) apply (rule cdcl_twl_o_prog_wl_D_spec[of 𝒜 x]) apply (auto simp: prod_rel_def intro: conc_fun_R_mono) done done subsubsection ‹Full Strategy› definition cdcl_twl_stgy_prog_wl_D :: ‹nat twl_st_wl ⇒ nat twl_st_wl nres› where ‹cdcl_twl_stgy_prog_wl_D S⇩0 = do { do { (brk, T) ← WHILE⇩T⇗λ(brk, T). cdcl_twl_stgy_prog_wl_inv S⇩0 (brk, T) ∧ literals_are_ℒ⇩i⇩n (all_atms_st T) T⇖ (λ(brk, _). ¬brk) (λ(brk, S). do { T ← unit_propagation_outer_loop_wl_D S; cdcl_twl_o_prog_wl_D T }) (False, S⇩0); RETURN T } } › theorem cdcl_twl_stgy_prog_wl_D_spec: assumes ‹literals_are_ℒ⇩i⇩n 𝒜 S› shows ‹cdcl_twl_stgy_prog_wl_D S ≤ ⇓ {(T', T). T = T' ∧ literals_are_ℒ⇩i⇩n 𝒜 T} (cdcl_twl_stgy_prog_wl S)› proof - have 1: ‹((False, S), False, S) ∈ {((brk', T'), brk, T). brk = brk' ∧ T = T' ∧ literals_are_ℒ⇩i⇩n 𝒜 T}› using assms by fast have 2: ‹unit_propagation_outer_loop_wl_D S ≤ ⇓ {(T', T). T = T' ∧ literals_are_ℒ⇩i⇩n 𝒜 T} (unit_propagation_outer_loop_wl T)› if ‹S = T› ‹literals_are_ℒ⇩i⇩n 𝒜 S› for S T using unit_propagation_outer_loop_wl_D_spec[of 𝒜 S] that by fast have 3: ‹cdcl_twl_o_prog_wl_D S ≤ ⇓ {((b', T'), b, T). b = b' ∧ T = T' ∧ literals_are_ℒ⇩i⇩n 𝒜 T} (cdcl_twl_o_prog_wl T)› if ‹S = T› ‹literals_are_ℒ⇩i⇩n 𝒜 S› for S T using cdcl_twl_o_prog_wl_D_spec[of 𝒜 S] that by fast show ?thesis unfolding cdcl_twl_stgy_prog_wl_D_def cdcl_twl_stgy_prog_wl_def apply (refine_vcg 1 2 3) subgoal by auto subgoal by auto subgoal by fast subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto done qed lemma cdcl_twl_stgy_prog_wl_D_spec': ‹(cdcl_twl_stgy_prog_wl_D, cdcl_twl_stgy_prog_wl) ∈ {(S,S'). (S,S') ∈ Id ∧literals_are_ℒ⇩i⇩n 𝒜 S} →⇩f ⟨{(T', T). T = T' ∧ literals_are_ℒ⇩i⇩n 𝒜 T}⟩ nres_rel› by (intro frefI nres_relI) (auto intro: cdcl_twl_stgy_prog_wl_D_spec) definition cdcl_twl_stgy_prog_wl_D_pre where ‹cdcl_twl_stgy_prog_wl_D_pre S U ⟷ (cdcl_twl_stgy_prog_wl_pre S U ∧ literals_are_ℒ⇩i⇩n (all_atms_st S) S)› lemma cdcl_twl_stgy_prog_wl_D_spec_final: assumes ‹cdcl_twl_stgy_prog_wl_D_pre S S'› shows ‹cdcl_twl_stgy_prog_wl_D S ≤ ⇓ (state_wl_l None O twl_st_l None) (conclusive_TWL_run S')› proof - have T: ‹cdcl_twl_stgy_prog_wl_pre S S' ∧ literals_are_ℒ⇩i⇩n (all_atms_st S) S› using assms unfolding cdcl_twl_stgy_prog_wl_D_pre_def by blast show ?thesis apply (rule order_trans[OF cdcl_twl_stgy_prog_wl_D_spec[of ‹all_atms_st S›]]) subgoal using T by auto subgoal apply (rule order_trans) apply (rule ref_two_step') apply (rule cdcl_twl_stgy_prog_wl_spec_final[of _ S']) subgoal using T by fast subgoal unfolding conc_fun_chain by (rule conc_fun_R_mono) blast done done qed definition cdcl_twl_stgy_prog_break_wl_D :: ‹nat twl_st_wl ⇒ nat twl_st_wl nres› where ‹cdcl_twl_stgy_prog_break_wl_D S⇩0 = do { b ← SPEC (λ_. True); (b, brk, T) ← WHILE⇩T⇗λ(b, brk, T). cdcl_twl_stgy_prog_wl_inv S⇩0 (brk, T) ∧ literals_are_ℒ⇩i⇩n (all_atms_st T) T⇖ (λ(b, brk, _). b ∧ ¬brk) (λ(b, brk, S). do { ASSERT(b); T ← unit_propagation_outer_loop_wl_D S; (brk, T) ← cdcl_twl_o_prog_wl_D T; b ← SPEC (λ_. True); RETURN(b, brk, T) }) (b, False, S⇩0); if brk then RETURN T else cdcl_twl_stgy_prog_wl_D T }› theorem cdcl_twl_stgy_prog_break_wl_D_spec: assumes ‹literals_are_ℒ⇩i⇩n 𝒜 S› shows ‹cdcl_twl_stgy_prog_break_wl_D S ≤ ⇓ {(T', T). T = T' ∧ literals_are_ℒ⇩i⇩n 𝒜 T} (cdcl_twl_stgy_prog_break_wl S)› proof - define f where ‹f ≡ SPEC (λ_::bool. True)› have 1: ‹((b, False, S), b, False, S) ∈ {((b', brk', T'), b, brk, T). b = b' ∧ brk = brk' ∧ T = T' ∧ literals_are_ℒ⇩i⇩n 𝒜 T}› for b using assms by fast have 1: ‹((b, False, S), b', False, S) ∈ {((b', brk', T'), b, brk, T). b = b' ∧ brk = brk' ∧ T = T' ∧ literals_are_ℒ⇩i⇩n 𝒜 T}› if ‹(b, b') ∈ bool_rel› for b b' using assms that by fast have 2: ‹unit_propagation_outer_loop_wl_D S ≤ ⇓ {(T', T). T = T' ∧ literals_are_ℒ⇩i⇩n 𝒜 T} (unit_propagation_outer_loop_wl T)› if ‹S = T› ‹literals_are_ℒ⇩i⇩n 𝒜 S› for S T using unit_propagation_outer_loop_wl_D_spec[of 𝒜 S] that by fast have 3: ‹cdcl_twl_o_prog_wl_D S ≤ ⇓ {((b', T'), b, T). b = b' ∧ T = T' ∧ literals_are_ℒ⇩i⇩n 𝒜 T} (cdcl_twl_o_prog_wl T)› if ‹S = T› ‹literals_are_ℒ⇩i⇩n 𝒜 S› for S T using cdcl_twl_o_prog_wl_D_spec[of 𝒜 S] that by fast show ?thesis unfolding cdcl_twl_stgy_prog_break_wl_D_def cdcl_twl_stgy_prog_break_wl_def f_def[symmetric] apply (refine_vcg 1 2 3) subgoal by auto subgoal by fast subgoal by fast subgoal by fast subgoal by fast subgoal by fast subgoal by fast subgoal by fast subgoal by fast subgoal by fast subgoal by fast subgoal by (fast intro!: cdcl_twl_stgy_prog_wl_D_spec) done qed lemma cdcl_twl_stgy_prog_break_wl_D_spec_final: assumes ‹cdcl_twl_stgy_prog_wl_D_pre S S'› shows ‹cdcl_twl_stgy_prog_break_wl_D S ≤ ⇓ (state_wl_l None O twl_st_l None) (conclusive_TWL_run S')› proof - have T: ‹cdcl_twl_stgy_prog_wl_pre S S' ∧ literals_are_ℒ⇩i⇩n (all_atms_st S) S› using assms unfolding cdcl_twl_stgy_prog_wl_D_pre_def by blast show ?thesis apply (rule order_trans[OF cdcl_twl_stgy_prog_break_wl_D_spec[of ‹all_atms_st S›]]) subgoal using T by auto subgoal apply (rule order_trans) apply (rule ref_two_step') apply (rule cdcl_twl_stgy_prog_break_wl_spec_final[of _ S']) subgoal using T by fast subgoal unfolding conc_fun_chain by (rule conc_fun_R_mono) blast done done qed text ‹The definition is here to be shared later.› definition get_propagation_reason :: ‹('v, 'mark) ann_lits ⇒ 'v literal ⇒ 'mark option nres› where ‹get_propagation_reason M L = SPEC(λC. C ≠ None ⟶ Propagated L (the C) ∈ set M)› end