theory Watched_Literals_Watch_List_Restart imports Watched_Literals_List_Restart Watched_Literals_Watch_List begin text ‹To ease the proof, we introduce the following ``alternative'' definitions, that only considers variables that are present in the initial clauses (which are never deleted from the set of clauses, but only moved to another component). › fun correct_watching' :: ‹'v twl_st_wl ⇒ bool› where ‹correct_watching' (M, N, D, NE, UE, Q, W) ⟷ (∀L ∈# all_lits_of_mm (mset `# init_clss_lf N + NE). 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)) ∧ (∀(i, K, b)∈#mset (W L). b ⟶ i ∈# dom_m N) ∧ filter_mset (λi. i ∈# dom_m N) (fst `# mset (W L)) = clause_to_update L (M, N, D, NE, UE, {#}, {#}))› fun correct_watching'' :: ‹'v twl_st_wl ⇒ bool› where ‹correct_watching'' (M, N, D, NE, UE, Q, W) ⟷ (∀L ∈# all_lits_of_mm (mset `# init_clss_lf N + NE). distinct_watched (W L) ∧ (∀(i, K, b)∈#mset (W L). i ∈# dom_m N ⟶ K ∈ set (N ∝ i) ∧ K ≠ L) ∧ filter_mset (λi. i ∈# dom_m N) (fst `# mset (W L)) = clause_to_update L (M, N, D, NE, UE, {#}, {#}))› lemma correct_watching'_correct_watching'': ‹correct_watching' S ⟹ correct_watching'' S› by (cases S) auto declare correct_watching'.simps[simp del] correct_watching''.simps[simp del] definition remove_all_annot_true_clause_imp_wl_inv :: ‹'v twl_st_wl ⇒ _ ⇒ nat × 'v twl_st_wl ⇒ bool› where ‹remove_all_annot_true_clause_imp_wl_inv S xs = (λ(i, T). correct_watching'' S ∧ correct_watching'' T ∧ (∃S' T'. (S, S') ∈ state_wl_l None ∧ (T, T') ∈ state_wl_l None ∧ remove_all_annot_true_clause_imp_inv S' xs (i, T')))› definition remove_all_annot_true_clause_one_imp_wl where ‹remove_all_annot_true_clause_one_imp_wl = (λ(C, S). do { if C ∈# dom_m (get_clauses_wl S) then if irred (get_clauses_wl S) C then RETURN (drop_clause_add_move_init S C) else RETURN (drop_clause S C) else do { RETURN S } })› definition remove_all_annot_true_clause_imp_wl :: ‹'v literal ⇒ 'v twl_st_wl ⇒ ('v twl_st_wl) nres› where ‹remove_all_annot_true_clause_imp_wl = (λL S. do { let xs = get_watched_wl S L; (_, T) ← WHILE⇩T⇗λ(i, T). remove_all_annot_true_clause_imp_wl_inv S xs (i, T)⇖ (λ(i, T). i < length xs) (λ(i, T). do { ASSERT(i < length xs); let (C, _, _) = xs!i; if C ∈# dom_m (get_clauses_wl T) ∧ length ((get_clauses_wl T) ∝ C) ≠ 2 then do { T ← remove_all_annot_true_clause_one_imp_wl (C, T); RETURN (i+1, T) } else RETURN (i+1, T) }) (0, S); RETURN T })› lemma reduce_dom_clauses_fmdrop: ‹reduce_dom_clauses N0 N ⟹ reduce_dom_clauses N0 (fmdrop C N)› using distinct_mset_dom[of N] by (auto simp: reduce_dom_clauses_def distinct_mset_remove1_All) lemma correct_watching_fmdrop: assumes irred: ‹¬ irred N C› and C: ‹C ∈# dom_m N› and ‹correct_watching' (M', N, D, NE, UE, Q, W)› and C2: ‹length (N ∝ C) ≠ 2› shows ‹correct_watching' (M, fmdrop C N, D, NE, UE, Q, W)› proof - have Hdist: ‹⋀L i K b. L∈#all_lits_of_mm (mset `# init_clss_lf N + NE) ⟹ distinct_watched (W L)› and H1: ‹⋀L i K b. L∈#all_lits_of_mm (mset `# init_clss_lf N + NE) ⟹ (i, K, b)∈#mset (W L) ⟹ i ∈# dom_m N ⟹ K ∈ set (N ∝ i) ∧ K ≠ L ∧ correctly_marked_as_binary N (i, K, b)› and H1': ‹⋀L i K b. L∈#all_lits_of_mm (mset `# init_clss_lf N + NE) ⟹ (i, K, b)∈#mset (W L) ⟹ b ⟹ i ∈# dom_m N› and H2: ‹⋀L. L∈#all_lits_of_mm (mset `# init_clss_lf N + NE) ⟹ {#i ∈# fst `# mset (W L). i ∈# dom_m N#} = {#C ∈# dom_m (get_clauses_l (M', N, D, NE, UE, {#}, {#})). L ∈ set (watched_l (get_clauses_l (M', N, D, NE, UE, {#}, {#}) ∝ C))#}› using assms unfolding correct_watching'.simps clause_to_update_def by fast+ have 1: ‹{#Ca ∈# dom_m (fmdrop C N). L ∈ set (watched_l (fmdrop C N ∝ Ca))#} = {#Ca ∈# dom_m (fmdrop C N). L ∈ set (watched_l (N ∝ Ca))#}› for L apply (rule filter_mset_cong2) using distinct_mset_dom[of N] C irred by (auto simp: image_mset_remove1_mset_if clause_to_update_def image_filter_replicate_mset distinct_mset_remove1_All filter_mset_neq_cond dest: all_lits_of_mm_diffD dest: multi_member_split) have 2: ‹remove1_mset C {#Ca ∈# dom_m N. L ∈ set (watched_l (N ∝ Ca))#} = removeAll_mset C {#Ca ∈# dom_m N. L ∈ set (watched_l (N ∝ Ca))#}› for L apply (rule distinct_mset_remove1_All) using distinct_mset_dom[of N] by (auto intro: distinct_mset_filter) have [simp]: ‹filter_mset (λi. i ∈# remove1_mset C (dom_m N)) A = removeAll_mset C (filter_mset (λi. i ∈# dom_m N) A)› for A by (induction A) (auto simp: distinct_mset_remove1_All distinct_mset_dom) show ?thesis unfolding correct_watching'.simps clause_to_update_def apply (intro conjI impI ballI) subgoal for L using Hdist[of L] distinct_mset_dom[of N] H1[of L ‹fst iK› ‹fst (snd iK)› ‹snd (snd iK)›] C irred H1'[of L ‹fst iK› ‹fst (snd iK)› ‹snd (snd iK)›] apply (auto simp: image_mset_remove1_mset_if clause_to_update_def image_filter_replicate_mset distinct_mset_remove1_All filter_mset_neq_cond correctly_marked_as_binary.simps dest: all_lits_of_mm_diffD dest: multi_member_split) done subgoal for L iK using distinct_mset_dom[of N] H1[of L ‹fst iK› ‹fst (snd iK)› ‹snd (snd iK)›] C irred H1'[of L ‹fst iK› ‹fst (snd iK)› ‹snd (snd iK)›] apply (auto simp: image_mset_remove1_mset_if clause_to_update_def image_filter_replicate_mset distinct_mset_remove1_All filter_mset_neq_cond correctly_marked_as_binary.simps dest: all_lits_of_mm_diffD dest: multi_member_split) done subgoal for L iK using distinct_mset_dom[of N] H1[of L ‹fst iK› ‹fst (snd iK)› ‹snd (snd iK)›] C irred H1'[of L ‹fst iK› ‹fst (snd iK)› ‹snd (snd iK)›] C2 apply (auto simp: image_mset_remove1_mset_if clause_to_update_def image_filter_replicate_mset distinct_mset_remove1_All filter_mset_neq_cond correctly_marked_as_binary.simps dest: all_lits_of_mm_diffD dest: multi_member_split) done subgoal for L using C irred apply - unfolding get_clauses_l.simps apply (subst 1) apply (subst (asm) init_clss_lf_fmdrop_irrelev, assumption) by (auto 5 1 simp: image_mset_remove1_mset_if clause_to_update_def image_filter_replicate_mset distinct_mset_remove1_All filter_mset_neq_cond 2 H2 dest: all_lits_of_mm_diffD dest: multi_member_split) done qed lemma correct_watching''_fmdrop: assumes irred: ‹¬ irred N C› and C: ‹C ∈# dom_m N› and ‹correct_watching'' (M', N, D, NE, UE, Q, W)› shows ‹correct_watching'' (M, fmdrop C N, D, NE, UE, Q, W)› proof - have Hdist: ‹⋀L i K b. L∈#all_lits_of_mm (mset `# init_clss_lf N + NE) ⟹ distinct_watched (W L)› and H1: ‹⋀L i K b. L∈#all_lits_of_mm (mset `# init_clss_lf N + NE) ⟹ (i, K, b)∈#mset (W L) ⟹ i ∈# dom_m N ⟹ K ∈ set (N ∝ i) ∧ K ≠ L› and H2: ‹⋀L. L∈#all_lits_of_mm (mset `# init_clss_lf N + NE) ⟹ {#i ∈# fst `# mset (W L). i ∈# dom_m N#} = {#C ∈# dom_m (get_clauses_l (M', N, D, NE, UE, {#}, {#})). L ∈ set (watched_l (get_clauses_l (M', N, D, NE, UE, {#}, {#}) ∝ C))#}› using assms unfolding correct_watching''.simps clause_to_update_def by fast+ have 1: ‹{#Ca ∈# dom_m (fmdrop C N). L ∈ set (watched_l (fmdrop C N ∝ Ca))#} = {#Ca ∈# dom_m (fmdrop C N). L ∈ set (watched_l (N ∝ Ca))#}› for L apply (rule filter_mset_cong2) using distinct_mset_dom[of N] C irred by (auto simp: image_mset_remove1_mset_if clause_to_update_def image_filter_replicate_mset distinct_mset_remove1_All filter_mset_neq_cond dest: all_lits_of_mm_diffD dest: multi_member_split) have 2: ‹remove1_mset C {#Ca ∈# dom_m N. L ∈ set (watched_l (N ∝ Ca))#} = removeAll_mset C {#Ca ∈# dom_m N. L ∈ set (watched_l (N ∝ Ca))#}› for L apply (rule distinct_mset_remove1_All) using distinct_mset_dom[of N] by (auto intro: distinct_mset_filter) have [simp]: ‹filter_mset (λi. i ∈# remove1_mset C (dom_m N)) A = removeAll_mset C (filter_mset (λi. i ∈# dom_m N) A)› for A by (induction A) (auto simp: distinct_mset_remove1_All distinct_mset_dom) show ?thesis unfolding correct_watching''.simps clause_to_update_def apply (intro conjI impI ballI) subgoal for L using Hdist[of L] distinct_mset_dom[of N] H1[of L ‹fst iK› ‹fst (snd iK)› ‹snd (snd iK)›] C irred apply (auto simp: image_mset_remove1_mset_if clause_to_update_def image_filter_replicate_mset distinct_mset_remove1_All filter_mset_neq_cond correctly_marked_as_binary.simps dest: all_lits_of_mm_diffD dest: multi_member_split) done subgoal for L iK using distinct_mset_dom[of N] H1[of L ‹fst iK› ‹fst (snd iK)› ‹snd (snd iK)›] C irred apply (auto simp: image_mset_remove1_mset_if clause_to_update_def image_filter_replicate_mset distinct_mset_remove1_All filter_mset_neq_cond correctly_marked_as_binary.simps dest: all_lits_of_mm_diffD dest: multi_member_split) done subgoal for L using C irred apply - unfolding get_clauses_l.simps apply (subst 1) apply (subst (asm) init_clss_lf_fmdrop_irrelev, assumption) by (auto 5 1 simp: image_mset_remove1_mset_if clause_to_update_def image_filter_replicate_mset distinct_mset_remove1_All filter_mset_neq_cond 2 H2 dest: all_lits_of_mm_diffD dest: multi_member_split) done qed lemma correct_watching''_fmdrop': assumes irred: ‹irred N C› and C: ‹C ∈# dom_m N› and ‹correct_watching'' (M', N, D, NE, UE, Q, W)› shows ‹correct_watching'' (M, fmdrop C N, D, add_mset (mset (N ∝ C)) NE, UE, Q, W)› proof - have Hdist: ‹⋀L. L∈#all_lits_of_mm (mset `# init_clss_lf N + NE) ⟹ distinct_watched (W L)› and H1: ‹⋀L i K b. L∈#all_lits_of_mm (mset `# init_clss_lf N + NE) ⟹ (i, K, b)∈#mset (W L) ⟹ i ∈# dom_m N ⟹ K ∈ set (N ∝ i) ∧ K ≠ L› and H2: ‹⋀L. L∈#all_lits_of_mm (mset `# init_clss_lf N + NE) ⟹ {#i ∈# fst `# mset (W L). i ∈# dom_m N#} = {#C ∈# dom_m (get_clauses_l (M', N, D, NE, UE, {#}, {#})). L ∈ set (watched_l (get_clauses_l (M', N, D, NE, UE, {#}, {#}) ∝ C))#}› using assms unfolding correct_watching''.simps clause_to_update_def by blast+ have 1: ‹{#Ca ∈# dom_m (fmdrop C N). L ∈ set (watched_l (fmdrop C N ∝ Ca))#} = {#Ca ∈# dom_m (fmdrop C N). L ∈ set (watched_l (N ∝ Ca))#}› for L apply (rule filter_mset_cong2) using distinct_mset_dom[of N] H1[of L ‹fst iK› ‹snd iK›] C irred by (auto simp: image_mset_remove1_mset_if clause_to_update_def image_filter_replicate_mset distinct_mset_remove1_All filter_mset_neq_cond dest: all_lits_of_mm_diffD dest: multi_member_split) have 2: ‹remove1_mset C {#Ca ∈# dom_m N. L ∈ set (watched_l (N ∝ Ca))#} = removeAll_mset C {#Ca ∈# dom_m N. L ∈ set (watched_l (N ∝ Ca))#}› for L apply (rule distinct_mset_remove1_All) using distinct_mset_dom[of N] by (auto intro: distinct_mset_filter) have [simp]: ‹filter_mset (λi. i ∈# remove1_mset C (dom_m N)) A = removeAll_mset C (filter_mset (λi. i ∈# dom_m N) A)› for A by (induction A) (auto simp: distinct_mset_remove1_All distinct_mset_dom) show ?thesis unfolding correct_watching''.simps clause_to_update_def apply (intro conjI impI ballI) subgoal for L using distinct_mset_dom[of N] H1[of L ‹fst iK› ‹fst (snd iK)› ‹snd (snd iK)›] C irred Hdist[of L] apply (auto simp: image_mset_remove1_mset_if clause_to_update_def image_filter_replicate_mset distinct_mset_remove1_All filter_mset_neq_cond correctly_marked_as_binary.simps dest: all_lits_of_mm_diffD dest: multi_member_split) done subgoal for L iK using distinct_mset_dom[of N] H1[of L ‹fst iK› ‹fst (snd iK)› ‹snd (snd iK)›] C irred apply (auto simp: image_mset_remove1_mset_if clause_to_update_def image_filter_replicate_mset distinct_mset_remove1_All filter_mset_neq_cond correctly_marked_as_binary.simps dest: all_lits_of_mm_diffD dest: multi_member_split) done subgoal for L using C irred apply - unfolding get_clauses_l.simps apply (subst 1) by (auto 5 1 simp: image_mset_remove1_mset_if clause_to_update_def image_filter_replicate_mset distinct_mset_remove1_All filter_mset_neq_cond 2 H2 dest: all_lits_of_mm_diffD dest: multi_member_split) done qed lemma correct_watching''_fmdrop'': assumes irred: ‹¬irred N C› and C: ‹C ∈# dom_m N› and ‹correct_watching'' (M', N, D, NE, UE, Q, W)› shows ‹correct_watching'' (M, fmdrop C N, D, NE, add_mset (mset (N ∝ C)) UE, Q, W)› proof - have Hdist: ‹⋀L. L∈#all_lits_of_mm (mset `# init_clss_lf N + NE) ⟹ distinct_watched (W L)› and H1: ‹⋀L i K b. L∈#all_lits_of_mm (mset `# init_clss_lf N + NE) ⟹ (i, K, b)∈#mset (W L) ⟹ i ∈# dom_m N ⟹ K ∈ set (N ∝ i) ∧ K ≠ L› and H2: ‹⋀L. L∈#all_lits_of_mm (mset `# init_clss_lf N + NE) ⟹ {#i ∈# fst `# mset (W L). i ∈# dom_m N#} = {#C ∈# dom_m (get_clauses_l (M', N, D, NE, UE, {#}, {#})). L ∈ set (watched_l (get_clauses_l (M', N, D, NE, UE, {#}, {#}) ∝ C))#}› using assms unfolding correct_watching''.simps clause_to_update_def by blast+ have 1: ‹{#Ca ∈# dom_m (fmdrop C N). L ∈ set (watched_l (fmdrop C N ∝ Ca))#} = {#Ca ∈# dom_m (fmdrop C N). L ∈ set (watched_l (N ∝ Ca))#}› for L apply (rule filter_mset_cong2) using distinct_mset_dom[of N] H1[of L ‹fst iK› ‹snd iK›] C irred by (auto simp: image_mset_remove1_mset_if clause_to_update_def image_filter_replicate_mset distinct_mset_remove1_All filter_mset_neq_cond dest: all_lits_of_mm_diffD dest: multi_member_split) have 2: ‹remove1_mset C {#Ca ∈# dom_m N. L ∈ set (watched_l (N ∝ Ca))#} = removeAll_mset C {#Ca ∈# dom_m N. L ∈ set (watched_l (N ∝ Ca))#}› for L apply (rule distinct_mset_remove1_All) using distinct_mset_dom[of N] by (auto intro: distinct_mset_filter) have [simp]: ‹filter_mset (λi. i ∈# remove1_mset C (dom_m N)) A = removeAll_mset C (filter_mset (λi. i ∈# dom_m N) A)› for A by (induction A) (auto simp: distinct_mset_remove1_All distinct_mset_dom) show ?thesis unfolding correct_watching''.simps clause_to_update_def apply (intro conjI impI ballI) subgoal for L using distinct_mset_dom[of N] H1[of L ‹fst iK› ‹fst (snd iK)› ‹snd (snd iK)›] C irred Hdist[of L] apply (auto simp: image_mset_remove1_mset_if clause_to_update_def image_filter_replicate_mset distinct_mset_remove1_All filter_mset_neq_cond correctly_marked_as_binary.simps dest: all_lits_of_mm_diffD dest: multi_member_split) done subgoal for L iK using distinct_mset_dom[of N] H1[of L ‹fst iK› ‹fst (snd iK)› ‹snd (snd iK)›] C irred apply (auto simp: image_mset_remove1_mset_if clause_to_update_def image_filter_replicate_mset distinct_mset_remove1_All filter_mset_neq_cond correctly_marked_as_binary.simps dest: all_lits_of_mm_diffD dest: multi_member_split) done subgoal for L using C irred apply - unfolding get_clauses_l.simps apply (subst 1) by (auto 5 1 simp: image_mset_remove1_mset_if clause_to_update_def image_filter_replicate_mset distinct_mset_remove1_All filter_mset_neq_cond 2 H2 dest: all_lits_of_mm_diffD dest: multi_member_split) done qed definition remove_one_annot_true_clause_one_imp_wl_pre where ‹remove_one_annot_true_clause_one_imp_wl_pre i T ⟷ (∃T'. (T, T') ∈ state_wl_l None ∧ remove_one_annot_true_clause_one_imp_pre i T' ∧ correct_watching'' T)› definition remove_one_annot_true_clause_one_imp_wl :: ‹nat ⇒ 'v twl_st_wl ⇒ (nat × 'v twl_st_wl) nres› where ‹remove_one_annot_true_clause_one_imp_wl = (λi S. do { ASSERT(remove_one_annot_true_clause_one_imp_wl_pre i S); ASSERT(is_proped (rev (get_trail_wl S) ! i)); (L, C) ← SPEC(λ(L, C). (rev (get_trail_wl S))!i = Propagated L C); ASSERT(Propagated L C ∈ set (get_trail_wl S)); if C = 0 then RETURN (i+1, S) else do { ASSERT(C ∈# dom_m (get_clauses_wl S)); S ← replace_annot_l L C S; S ← remove_and_add_cls_l C S; ― ‹\<^text>‹S ← remove_all_annot_true_clause_imp_wl L S;›› RETURN (i+1, S) } })› lemma remove_one_annot_true_clause_one_imp_wl_remove_one_annot_true_clause_one_imp: ‹(uncurry remove_one_annot_true_clause_one_imp_wl, uncurry remove_one_annot_true_clause_one_imp) ∈ nat_rel ×⇩f {(S, T). (S, T) ∈ state_wl_l None ∧ correct_watching'' S} →⇩f ⟨nat_rel ×⇩f {(S, T). (S, T) ∈ state_wl_l None ∧ correct_watching'' S}⟩nres_rel› (is ‹_ ∈ _ ×⇩f ?A →⇩f _›) proof - have [refine0]: ‹replace_annot_l L C S ≤ ⇓ {(S', T'). (S', T') ∈ ?A ∧ get_clauses_wl S' = get_clauses_wl S} (replace_annot_l L' C' T')› if ‹(L, L') ∈ Id› and ‹(S, T') ∈ ?A› and ‹(C, C') ∈ Id› for L L' S T' C C' using that by (cases S; cases T') (fastforce simp: replace_annot_l_def state_wl_l_def correct_watching''.simps clause_to_update_def intro: RES_refine) have [refine0]: ‹remove_and_add_cls_l C S ≤⇓ ?A (remove_and_add_cls_l C' S')› if ‹(C, C') ∈ Id› and ‹(S, S') ∈ ?A› and ‹C ∈# dom_m (get_clauses_wl S)› for C C' S S' using that unfolding remove_and_add_cls_l_def by refine_rcg (auto intro!: RES_refine simp: state_wl_l_def intro: correct_watching''_fmdrop correct_watching''_fmdrop'' correct_watching''_fmdrop') show ?thesis unfolding remove_one_annot_true_clause_one_imp_wl_def remove_one_annot_true_clause_one_imp_def uncurry_def apply (intro frefI nres_relI) apply (refine_vcg) subgoal for x y unfolding remove_one_annot_true_clause_one_imp_wl_pre_def by (rule exI[of _ ‹snd y›]) auto subgoal by (simp add: state_wl_l_def) subgoal by (simp add: state_wl_l_def) subgoal by (simp add: state_wl_l_def) subgoal by simp subgoal by (simp add: state_wl_l_def) subgoal by (simp add: state_wl_l_def) subgoal by (simp add: state_wl_l_def) subgoal by simp subgoal by (simp add: state_wl_l_def) subgoal by (simp add: state_wl_l_def) subgoal by (simp add: state_wl_l_def) subgoal by (auto 5 5 simp add: state_wl_l_def) subgoal by (auto simp add: state_wl_l_def) done qed definition remove_one_annot_true_clause_imp_wl_inv where ‹remove_one_annot_true_clause_imp_wl_inv S = (λ(i, T). (∃S' T'. (S, S') ∈ state_wl_l None ∧ (T, T') ∈ state_wl_l None ∧ correct_watching'' S ∧ correct_watching'' T ∧ remove_one_annot_true_clause_imp_inv S' (i, T')))› definition remove_one_annot_true_clause_imp_wl :: ‹'v twl_st_wl ⇒ ('v twl_st_wl) nres› where ‹remove_one_annot_true_clause_imp_wl = (λS. do { k ← SPEC(λk. (∃M1 M2 K. (Decided K # M1, M2) ∈ set (get_all_ann_decomposition (get_trail_wl S)) ∧ count_decided M1 = 0 ∧ k = length M1) ∨ (count_decided (get_trail_wl S) = 0 ∧ k = length (get_trail_wl S))); (_, S) ← WHILE⇩T⇗remove_one_annot_true_clause_imp_wl_inv S⇖ (λ(i, S). i < k) (λ(i, S). remove_one_annot_true_clause_one_imp_wl i S) (0, S); RETURN S })› lemma remove_one_annot_true_clause_imp_wl_remove_one_annot_true_clause_imp: ‹(remove_one_annot_true_clause_imp_wl, remove_one_annot_true_clause_imp) ∈ {(S, T). (S, T) ∈ state_wl_l None ∧ correct_watching'' S} →⇩f ⟨{(S, T). (S, T) ∈ state_wl_l None ∧ correct_watching'' S}⟩nres_rel› proof - show ?thesis unfolding remove_one_annot_true_clause_imp_wl_def remove_one_annot_true_clause_imp_def uncurry_def apply (intro frefI nres_relI) apply (refine_vcg WHILEIT_refine[where R = ‹nat_rel ×⇩f {(S, T). (S, T) ∈ state_wl_l None ∧ correct_watching'' S}›] remove_one_annot_true_clause_one_imp_wl_remove_one_annot_true_clause_one_imp[THEN fref_to_Down_curry]) subgoal by force subgoal by auto subgoal for x y k ka xa x' unfolding remove_one_annot_true_clause_imp_wl_inv_def apply (subst case_prod_beta) apply (rule_tac x=‹y› in exI) apply (rule_tac x=‹snd x'› in exI) apply (subst (asm)(17) surjective_pairing) apply (subst (asm)(22) surjective_pairing) unfolding prod_rel_iff by auto subgoal by auto subgoal by auto subgoal by auto done qed definition collect_valid_indices_wl :: ‹'v twl_st_wl ⇒ nat list nres› where ‹collect_valid_indices_wl S = SPEC (λN. True)› definition mark_to_delete_clauses_wl_inv :: ‹'v twl_st_wl ⇒ nat list ⇒ nat × 'v twl_st_wl× nat list ⇒ bool› where ‹mark_to_delete_clauses_wl_inv = (λS xs0 (i, T, xs). ∃S' T'. (S, S') ∈ state_wl_l None ∧ (T, T') ∈ state_wl_l None ∧ mark_to_delete_clauses_l_inv S' xs0 (i, T', xs) ∧ correct_watching' S)› definition mark_to_delete_clauses_wl_pre :: ‹'v twl_st_wl ⇒ bool› where ‹mark_to_delete_clauses_wl_pre S ⟷ (∃T. (S, T) ∈ state_wl_l None ∧ mark_to_delete_clauses_l_pre T)› definition mark_garbage_wl:: ‹nat ⇒ 'v twl_st_wl ⇒ 'v twl_st_wl› where ‹mark_garbage_wl = (λC (M, N0, D, NE, UE, WS, Q). (M, fmdrop C N0, D, NE, UE, WS, Q))› definition mark_to_delete_clauses_wl :: ‹'v twl_st_wl ⇒ 'v twl_st_wl nres› where ‹mark_to_delete_clauses_wl = (λS. do { ASSERT(mark_to_delete_clauses_wl_pre S); xs ← collect_valid_indices_wl S; l ← SPEC(λ_:: nat. True); (_, S, _) ← WHILE⇩T⇗mark_to_delete_clauses_wl_inv S xs⇖ (λ(i, S, xs). i < length xs) (λ(i, T, xs). do { if(xs!i ∉# dom_m (get_clauses_wl T)) then RETURN (i, T, delete_index_and_swap xs i) else do { ASSERT(0 < length (get_clauses_wl T∝(xs!i))); can_del ← SPEC(λb. b ⟶ (Propagated (get_clauses_wl T∝(xs!i)!0) (xs!i) ∉ set (get_trail_wl T)) ∧ ¬irred (get_clauses_wl T) (xs!i) ∧ length (get_clauses_wl T ∝ (xs!i)) ≠ 2); ASSERT(i < length xs); if can_del then RETURN (i, mark_garbage_wl (xs!i) T, delete_index_and_swap xs i) else RETURN (i+1, T, xs) } }) (l, S, xs); RETURN S })› lemma mark_to_delete_clauses_wl_mark_to_delete_clauses_l: ‹(mark_to_delete_clauses_wl, mark_to_delete_clauses_l) ∈ {(S, T). (S, T) ∈ state_wl_l None ∧ correct_watching' S} →⇩f ⟨{(S, T). (S, T) ∈ state_wl_l None ∧ correct_watching' S}⟩nres_rel› proof - have [refine0]: ‹collect_valid_indices_wl S ≤ ⇓ Id (collect_valid_indices S')› if ‹(S, S') ∈ {(S, T). (S, T) ∈ state_wl_l None ∧ correct_watching' S ∧ mark_to_delete_clauses_wl_pre S}› for S S' using that by (auto simp: collect_valid_indices_wl_def collect_valid_indices_def) have if_inv: ‹(if A then RETURN P else RETURN Q) = RETURN (if A then P else Q)› for A P Q by auto have Ball_range[simp]: ‹(∀x∈range f ∪ range g. P x)⟷(∀x. P (f x) ∧ P (g x))› for P f g by auto show ?thesis unfolding mark_to_delete_clauses_wl_def mark_to_delete_clauses_l_def uncurry_def apply (intro frefI nres_relI) apply (refine_vcg WHILEIT_refine[where R = ‹{((i, S, xs), (j, T, ys)). i = j ∧ (S, T) ∈ state_wl_l None ∧ correct_watching' S ∧ xs = ys}›] remove_one_annot_true_clause_one_imp_wl_remove_one_annot_true_clause_one_imp[THEN fref_to_Down_curry]) subgoal unfolding mark_to_delete_clauses_wl_pre_def by blast subgoal by auto subgoal by (auto simp: state_wl_l_def) subgoal unfolding mark_to_delete_clauses_wl_inv_def by fast subgoal by auto subgoal by (force simp: state_wl_l_def) subgoal by auto subgoal by (force simp: state_wl_l_def) subgoal by (auto simp: state_wl_l_def can_delete_def) subgoal by auto subgoal by (force simp: state_wl_l_def) subgoal by (auto simp: state_wl_l_def correct_watching_fmdrop mark_garbage_wl_def mark_garbage_l_def split: prod.splits) subgoal by (auto simp: state_wl_l_def) subgoal by auto done qed text ‹ This is only a specification and must be implemented. There are two ways to do so: ▸ clean the watch lists and then iterate over all clauses to rebuild them. ▸ iterate over the watch list and check whether the clause index is in the domain or not. It is not clear which is faster (but option 1 requires only 1 memory access per clause instead of two). The first option is implemented in SPASS-SAT. The latter version (partly) in cadical. › definition rewatch_clauses :: ‹'v twl_st_wl ⇒ 'v twl_st_wl nres› where ‹rewatch_clauses = (λ(M, N, D, NE, UE, Q, W). SPEC(λ(M', N', D', NE', UE', Q', W'). (M, N, D, NE, UE, Q) = (M', N', D', NE', UE', Q') ∧ correct_watching (M, N', D, NE, UE, Q, W')))› definition mark_to_delete_clauses_wl_post where ‹mark_to_delete_clauses_wl_post S T ⟷ (∃S' T'. (S, S') ∈ state_wl_l None ∧ (T, T') ∈ state_wl_l None ∧ mark_to_delete_clauses_l_post S' T' ∧ correct_watching S ∧ correct_watching T)› definition cdcl_twl_full_restart_wl_prog :: ‹'v twl_st_wl ⇒ 'v twl_st_wl nres› where ‹cdcl_twl_full_restart_wl_prog S = do { ― ‹ \<^term>‹remove_one_annot_true_clause_imp_wl S›› ASSERT(mark_to_delete_clauses_wl_pre S); T ← mark_to_delete_clauses_wl S; ASSERT(mark_to_delete_clauses_wl_post S T); RETURN T }› lemma correct_watching_correct_watching: ‹correct_watching S ⟹ correct_watching' S› apply (cases S, simp only: correct_watching.simps correct_watching'.simps) apply (subst (asm) all_clss_lf_ran_m[symmetric]) unfolding image_mset_union all_lits_of_mm_union by auto lemma (in -) [twl_st_l, simp]: ‹(Sa, x) ∈ twl_st_l None ⟹ get_all_learned_clss x = mset `# (get_learned_clss_l Sa) + get_unit_learned_clauses_l Sa› by (cases Sa; cases x) (auto simp: twl_st_l_def get_learned_clss_l_def mset_take_mset_drop_mset') lemma cdcl_twl_full_restart_wl_prog_final_rel: assumes S_Sa: ‹(S, Sa) ∈ {(S, T). (S, T) ∈ state_wl_l None ∧ correct_watching' S}› and pre_Sa: ‹mark_to_delete_clauses_l_pre Sa› and pre_S: ‹mark_to_delete_clauses_wl_pre S› and T_Ta: ‹(T, Ta) ∈ {(S, T). (S, T) ∈ state_wl_l None ∧ correct_watching' S}› and pre_l: ‹mark_to_delete_clauses_l_post Sa Ta› shows ‹mark_to_delete_clauses_wl_post S T› proof - obtain x where Sa_x: ‹(Sa, x) ∈ twl_st_l None› and st: ‹remove_one_annot_true_clause⇧*⇧* Sa Ta› and list_invs: ‹twl_list_invs Sa› and struct: ‹twl_struct_invs x› and confl: ‹get_conflict_l Sa = None› and upd: ‹clauses_to_update_l Sa = {#}› using pre_l unfolding mark_to_delete_clauses_l_post_def by blast have corr_S: ‹correct_watching' S› and corr_T: ‹correct_watching' T› and S_Sa: ‹(S, Sa) ∈ state_wl_l None› and T_Ta: ‹(T, Ta) ∈ state_wl_l None› using S_Sa T_Ta by auto have ‹cdcl⇩W_restart_mset.no_strange_atm (state⇩W_of x)› using struct unfolding twl_struct_invs_def cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def by auto then have ‹set_mset (all_lits_of_mm (mset `# init_clss_lf (get_clauses_wl S) + get_unit_init_clss_wl S)) = set_mset (all_lits_of_mm (mset `# ran_mf (get_clauses_wl S) + get_unit_clauses_wl S))› apply (subst all_clss_lf_ran_m[symmetric]) using Sa_x S_Sa unfolding image_mset_union cdcl⇩W_restart_mset.no_strange_atm_def all_lits_of_mm_union by (auto simp: in_all_lits_of_mm_ain_atms_of_iff get_learned_clss_l_def twl_st get_unit_clauses_wl_alt_def) then have corr_S': ‹correct_watching S› using corr_S by (cases S; simp only: correct_watching'.simps correct_watching.simps) simp obtain y where ‹cdcl_twl_restart_l⇧*⇧* Sa Ta› and Ta_y: ‹(Ta, y) ∈ twl_st_l None› and ‹cdcl_twl_restart⇧*⇧* x y› and struct: ‹twl_struct_invs y› using rtranclp_remove_one_annot_true_clause_cdcl_twl_restart_l2[OF st list_invs confl upd Sa_x struct] by blast have ‹cdcl⇩W_restart_mset.no_strange_atm (state⇩W_of y)› using struct unfolding twl_struct_invs_def cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def by auto then have ‹set_mset (all_lits_of_mm (mset `# init_clss_lf (get_clauses_wl T) + get_unit_init_clss_wl T)) = set_mset (all_lits_of_mm (mset `# ran_mf (get_clauses_wl T) + get_unit_clauses_wl T))› apply (subst all_clss_lf_ran_m[symmetric]) using T_Ta Ta_y unfolding image_mset_union cdcl⇩W_restart_mset.no_strange_atm_def all_lits_of_mm_union by (auto simp: in_all_lits_of_mm_ain_atms_of_iff get_learned_clss_l_def twl_st get_unit_clauses_wl_alt_def) then have corr_T': ‹correct_watching T› using corr_T by (cases T; simp only: correct_watching'.simps correct_watching.simps) simp show ?thesis using S_Sa T_Ta corr_T' corr_S' pre_l unfolding mark_to_delete_clauses_wl_post_def by blast qed lemma cdcl_twl_full_restart_wl_prog_final_rel': assumes S_Sa: ‹(S, Sa) ∈ {(S, T). (S, T) ∈ state_wl_l None ∧ correct_watching S}› and pre_Sa: ‹mark_to_delete_clauses_l_pre Sa› and pre_S: ‹mark_to_delete_clauses_wl_pre S› and T_Ta: ‹(T, Ta) ∈ {(S, T). (S, T) ∈ state_wl_l None ∧ correct_watching' S}› and pre_l: ‹mark_to_delete_clauses_l_post Sa Ta› shows ‹mark_to_delete_clauses_wl_post S T› proof - obtain x where Sa_x: ‹(Sa, x) ∈ twl_st_l None› and st: ‹remove_one_annot_true_clause⇧*⇧* Sa Ta› and list_invs: ‹twl_list_invs Sa› and struct: ‹twl_struct_invs x› and confl: ‹get_conflict_l Sa = None› and upd: ‹clauses_to_update_l Sa = {#}› using pre_l unfolding mark_to_delete_clauses_l_post_def by blast have corr_S: ‹correct_watching S› and corr_T: ‹correct_watching' T› and S_Sa: ‹(S, Sa) ∈ state_wl_l None› and T_Ta: ‹(T, Ta) ∈ state_wl_l None› using S_Sa T_Ta by auto have corr_S: ‹correct_watching' S› using correct_watching_correct_watching[OF corr_S] . have ‹cdcl⇩W_restart_mset.no_strange_atm (state⇩W_of x)› using struct unfolding twl_struct_invs_def cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def by auto then have ‹set_mset (all_lits_of_mm (mset `# init_clss_lf (get_clauses_wl S) + get_unit_init_clss_wl S)) = set_mset (all_lits_of_mm (mset `# ran_mf (get_clauses_wl S) + get_unit_clauses_wl S))› apply (subst all_clss_lf_ran_m[symmetric]) using Sa_x S_Sa unfolding image_mset_union cdcl⇩W_restart_mset.no_strange_atm_def all_lits_of_mm_union by (auto simp: in_all_lits_of_mm_ain_atms_of_iff get_learned_clss_l_def twl_st get_unit_clauses_wl_alt_def) then have corr_S': ‹correct_watching S› using corr_S by (cases S; simp only: correct_watching'.simps correct_watching.simps) simp obtain y where ‹cdcl_twl_restart_l⇧*⇧* Sa Ta› and Ta_y: ‹(Ta, y) ∈ twl_st_l None› and ‹cdcl_twl_restart⇧*⇧* x y› and struct: ‹twl_struct_invs y› using rtranclp_remove_one_annot_true_clause_cdcl_twl_restart_l2[OF st list_invs confl upd Sa_x struct] by blast have ‹cdcl⇩W_restart_mset.no_strange_atm (state⇩W_of y)› using struct unfolding twl_struct_invs_def cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def by auto then have ‹set_mset (all_lits_of_mm (mset `# init_clss_lf (get_clauses_wl T) + get_unit_init_clss_wl T)) = set_mset (all_lits_of_mm (mset `# ran_mf (get_clauses_wl T) + get_unit_clauses_wl T))› apply (subst all_clss_lf_ran_m[symmetric]) using T_Ta Ta_y unfolding image_mset_union cdcl⇩W_restart_mset.no_strange_atm_def all_lits_of_mm_union by (auto simp: in_all_lits_of_mm_ain_atms_of_iff get_learned_clss_l_def twl_st get_unit_clauses_wl_alt_def) then have corr_T': ‹correct_watching T› using corr_T by (cases T; simp only: correct_watching'.simps correct_watching.simps) simp show ?thesis using S_Sa T_Ta corr_T' corr_S' pre_l unfolding mark_to_delete_clauses_wl_post_def by blast qed lemma cdcl_twl_full_restart_wl_prog_cdcl_full_twl_restart_l_prog: ‹(cdcl_twl_full_restart_wl_prog, cdcl_twl_full_restart_l_prog) ∈ {(S, T). (S, T) ∈ state_wl_l None ∧ correct_watching S} →⇩f ⟨{(S, T). (S, T) ∈ state_wl_l None ∧ correct_watching S}⟩nres_rel› unfolding cdcl_twl_full_restart_wl_prog_def cdcl_twl_full_restart_l_prog_def rewatch_clauses_def apply (intro frefI nres_relI) apply (refine_vcg mark_to_delete_clauses_wl_mark_to_delete_clauses_l[THEN fref_to_Down] remove_one_annot_true_clause_imp_wl_remove_one_annot_true_clause_imp[THEN fref_to_Down]) subgoal unfolding mark_to_delete_clauses_wl_pre_def by (blast intro: correct_watching_correct_watching) subgoal unfolding mark_to_delete_clauses_wl_pre_def by (blast intro: correct_watching_correct_watching) subgoal by (rule cdcl_twl_full_restart_wl_prog_final_rel') subgoal by (auto simp: state_wl_l_def mark_to_delete_clauses_wl_post_def) done definition (in -) cdcl_twl_local_restart_wl_spec :: ‹'v twl_st_wl ⇒ 'v twl_st_wl nres› where ‹cdcl_twl_local_restart_wl_spec = (λ(M, N, D, NE, UE, Q, W). do { (M, Q) ← SPEC(λ(M', Q'). (∃K M2. (Decided K # M', M2) ∈ set (get_all_ann_decomposition M) ∧ Q' = {#}) ∨ (M' = M ∧ Q' = Q)); RETURN (M, N, D, NE, UE, Q, W) })› lemma cdcl_twl_local_restart_wl_spec_cdcl_twl_local_restart_l_spec: ‹(cdcl_twl_local_restart_wl_spec, cdcl_twl_local_restart_l_spec) ∈ {(S, T). (S, T) ∈ state_wl_l None ∧ correct_watching S} →⇩f ⟨{(S, T). (S, T) ∈ state_wl_l None ∧ correct_watching S}⟩nres_rel› proof - have [refine0]: ‹⋀x y x1 x2 x1a x2a x1b x2b x1c x2c x1d x2d x1e x2e x1f x2f x1g x2g x1h x2h x1i x2i x1j x2j x1k x2k. (x, y) ∈ {(S, T). (S, T) ∈ state_wl_l None ∧ correct_watching S} ⟹ x2d = (x1e, x2e) ⟹ x2c = (x1d, x2d) ⟹ x2b = (x1c, x2c) ⟹ x2a = (x1b, x2b) ⟹ x2 = (x1a, x2a) ⟹ y = (x1, x2) ⟹ x2j = (x1k, x2k) ⟹ x2i = (x1j, x2j) ⟹ x2h = (x1i, x2i) ⟹ x2g = (x1h, x2h) ⟹ x2f = (x1g, x2g) ⟹ x = (x1f, x2f) ⟹ SPEC (λ(M', Q'). (∃K M2. (Decided K # M', M2) ∈ set (get_all_ann_decomposition x1f) ∧ Q' = {#}) ∨ M' = x1f ∧ Q' = x1k) ≤ ⇓Id (SPEC (λ(M', Q') .(∃K M2. (Decided K # M', M2) ∈ set (get_all_ann_decomposition x1) ∧ Q' = {#}) ∨ M' = x1 ∧ Q' = x2e))› by (auto simp: state_wl_l_def) show ?thesis unfolding cdcl_twl_local_restart_wl_spec_def cdcl_twl_local_restart_l_spec_def rewatch_clauses_def apply (intro frefI nres_relI) apply (refine_vcg) apply assumption+ subgoal by (auto simp: state_wl_l_def correct_watching.simps clause_to_update_def) done qed definition cdcl_twl_restart_wl_prog where ‹cdcl_twl_restart_wl_prog S = do { b ← SPEC(λ_. True); if b then cdcl_twl_local_restart_wl_spec S else cdcl_twl_full_restart_wl_prog S }› lemma cdcl_twl_restart_wl_prog_cdcl_twl_restart_l_prog: ‹(cdcl_twl_restart_wl_prog, cdcl_twl_restart_l_prog) ∈ {(S, T). (S, T) ∈ state_wl_l None ∧ correct_watching S} →⇩f ⟨{(S, T). (S, T) ∈ state_wl_l None ∧ correct_watching S}⟩nres_rel› unfolding cdcl_twl_restart_wl_prog_def cdcl_twl_restart_l_prog_def rewatch_clauses_def apply (intro frefI nres_relI) apply (refine_vcg cdcl_twl_local_restart_wl_spec_cdcl_twl_local_restart_l_spec[THEN fref_to_Down] cdcl_twl_full_restart_wl_prog_cdcl_full_twl_restart_l_prog[THEN fref_to_Down]) subgoal by auto done definition (in -) restart_abs_wl_pre :: ‹'v twl_st_wl ⇒ bool ⇒ bool› where ‹restart_abs_wl_pre S brk ⟷ (∃S'. (S, S') ∈ state_wl_l None ∧ restart_abs_l_pre S' brk ∧ correct_watching S)› context twl_restart_ops begin definition (in twl_restart_ops) restart_required_wl :: ‹'v twl_st_wl ⇒ nat ⇒ bool nres› where ‹restart_required_wl S n = SPEC (λb. b ⟶ f n < size (get_learned_clss_wl S))› definition (in twl_restart_ops) cdcl_twl_stgy_restart_abs_wl_inv :: ‹'v twl_st_wl ⇒ bool ⇒ 'v twl_st_wl ⇒ nat ⇒ bool› where ‹cdcl_twl_stgy_restart_abs_wl_inv S⇩0 brk T n ≡ (∃S⇩0' T'. (S⇩0, S⇩0') ∈ state_wl_l None ∧ (T, T') ∈ state_wl_l None ∧ cdcl_twl_stgy_restart_abs_l_inv S⇩0' brk T' n ∧ correct_watching T)› end context twl_restart_ops begin definition cdcl_GC_clauses_pre_wl :: ‹'v twl_st_wl ⇒ bool› where ‹cdcl_GC_clauses_pre_wl S ⟷ ( ∃T. (S, T) ∈ state_wl_l None ∧ correct_watching'' S ∧ cdcl_GC_clauses_pre T )› definition cdcl_GC_clauses_wl :: ‹'v twl_st_wl ⇒ 'v twl_st_wl nres› where ‹cdcl_GC_clauses_wl = (λ(M, N, D, NE, UE, WS, Q). do { ASSERT(cdcl_GC_clauses_pre_wl (M, N, D, NE, UE, WS, Q)); let b = True; if b then do { (N', _) ← SPEC (λ(N'', m). GC_remap⇧*⇧* (N, Map.empty, fmempty) (fmempty, m, N'') ∧ 0 ∉# dom_m N''); Q ← SPEC(λQ. correct_watching' (M, N', D, NE, UE, WS, Q)); RETURN (M, N', D, NE, UE, WS, Q) } else RETURN (M, N, D, NE, UE, WS, Q)})› lemma cdcl_GC_clauses_wl_cdcl_GC_clauses: ‹(cdcl_GC_clauses_wl, cdcl_GC_clauses) ∈ {(S::'v twl_st_wl, S'). (S, S') ∈ state_wl_l None ∧ correct_watching'' S} →⇩f ⟨{(S::'v twl_st_wl, S'). (S, S') ∈ state_wl_l None ∧ correct_watching' S}⟩nres_rel› unfolding cdcl_GC_clauses_wl_def cdcl_GC_clauses_def apply (intro frefI nres_relI) apply refine_vcg subgoal unfolding cdcl_GC_clauses_pre_wl_def by blast subgoal by (auto simp: state_wl_l_def) subgoal by (auto simp: state_wl_l_def) subgoal by auto subgoal by (auto simp: state_wl_l_def) subgoal by auto done definition cdcl_twl_full_restart_wl_GC_prog_post :: ‹'v twl_st_wl ⇒ 'v twl_st_wl ⇒ bool› where ‹cdcl_twl_full_restart_wl_GC_prog_post S T ⟷ (∃S' T'. (S, S') ∈ state_wl_l None ∧ (T, T') ∈ state_wl_l None ∧ cdcl_twl_full_restart_l_GC_prog_pre S' ∧ cdcl_twl_restart_l S' T' ∧ correct_watching' T ∧ set_mset (all_lits_of_mm (mset `# init_clss_lf (get_clauses_wl T)+ get_unit_init_clss_wl T)) = set_mset (all_lits_of_mm (mset `# ran_mf (get_clauses_wl T)+ get_unit_clauses_wl T)))› definition (in -) cdcl_twl_local_restart_wl_spec0 :: ‹'v twl_st_wl ⇒ 'v twl_st_wl nres› where ‹cdcl_twl_local_restart_wl_spec0 = (λ(M, N, D, NE, UE, Q, W). do { (M, Q) ← SPEC(λ(M', Q'). (∃K M2. (Decided K # M', M2) ∈ set (get_all_ann_decomposition M) ∧ Q' = {#} ∧ count_decided M' = 0) ∨ (M' = M ∧ Q' = Q ∧ count_decided M' = 0)); RETURN (M, N, D, NE, UE, Q, W) })› definition mark_to_delete_clauses_wl2_inv :: ‹'v twl_st_wl ⇒ nat list ⇒ nat × 'v twl_st_wl× nat list ⇒ bool› where ‹mark_to_delete_clauses_wl2_inv = (λS xs0 (i, T, xs). ∃S' T'. (S, S') ∈ state_wl_l None ∧ (T, T') ∈ state_wl_l None ∧ mark_to_delete_clauses_l_inv S' xs0 (i, T', xs) ∧ correct_watching'' S)› definition mark_to_delete_clauses_wl2 :: ‹'v twl_st_wl ⇒ 'v twl_st_wl nres› where ‹mark_to_delete_clauses_wl2 = (λS. do { ASSERT(mark_to_delete_clauses_wl_pre S); xs ← collect_valid_indices_wl S; l ← SPEC(λ_:: nat. True); (_, S, _) ← WHILE⇩T⇗mark_to_delete_clauses_wl2_inv S xs⇖ (λ(i, S, xs). i < length xs) (λ(i, T, xs). do { if(xs!i ∉# dom_m (get_clauses_wl T)) then RETURN (i, T, delete_index_and_swap xs i) else do { ASSERT(0 < length (get_clauses_wl T∝(xs!i))); can_del ← SPEC(λb. b ⟶ (Propagated (get_clauses_wl T∝(xs!i)!0) (xs!i) ∉ set (get_trail_wl T)) ∧ ¬irred (get_clauses_wl T) (xs!i) ∧ length (get_clauses_wl T ∝ (xs!i)) ≠ 2); ASSERT(i < length xs); if can_del then RETURN (i, mark_garbage_wl (xs!i) T, delete_index_and_swap xs i) else RETURN (i+1, T, xs) } }) (l, S, xs); RETURN S })› lemma mark_to_delete_clauses_wl_mark_to_delete_clauses_l2: ‹(mark_to_delete_clauses_wl2, mark_to_delete_clauses_l) ∈ {(S, T). (S, T) ∈ state_wl_l None ∧ correct_watching'' S} →⇩f ⟨{(S, T). (S, T) ∈ state_wl_l None ∧ correct_watching'' S}⟩nres_rel› proof - have [refine0]: ‹collect_valid_indices_wl S ≤ ⇓ Id (collect_valid_indices S')› if ‹(S, S') ∈ {(S, T). (S, T) ∈ state_wl_l None ∧ correct_watching'' S ∧ mark_to_delete_clauses_wl_pre S}› for S S' using that by (auto simp: collect_valid_indices_wl_def collect_valid_indices_def) have if_inv: ‹(if A then RETURN P else RETURN Q) = RETURN (if A then P else Q)› for A P Q by auto have Ball_range[simp]: ‹(∀x∈range f ∪ range g. P x)⟷(∀x. P (f x) ∧ P (g x))› for P f g by auto show ?thesis unfolding mark_to_delete_clauses_wl2_def mark_to_delete_clauses_l_def uncurry_def apply (intro frefI nres_relI) apply (refine_vcg WHILEIT_refine[where R = ‹{((i, S, xs), (j, T, ys)). i = j ∧ (S, T) ∈ state_wl_l None ∧ correct_watching'' S ∧ xs = ys}›] remove_one_annot_true_clause_one_imp_wl_remove_one_annot_true_clause_one_imp[THEN fref_to_Down_curry]) subgoal unfolding mark_to_delete_clauses_wl_pre_def by blast subgoal by auto subgoal by (auto simp: state_wl_l_def) subgoal unfolding mark_to_delete_clauses_wl2_inv_def by fast subgoal by auto subgoal by (force simp: state_wl_l_def) subgoal by auto subgoal by (force simp: state_wl_l_def) subgoal by (auto simp: state_wl_l_def can_delete_def) subgoal by auto subgoal by (force simp: state_wl_l_def) subgoal by (auto simp: state_wl_l_def correct_watching_fmdrop mark_garbage_wl_def mark_garbage_l_def correct_watching''_fmdrop split: prod.splits) subgoal by (auto simp: state_wl_l_def) subgoal by auto done qed definition cdcl_twl_full_restart_wl_GC_prog_pre :: ‹'v twl_st_wl ⇒ bool› where ‹cdcl_twl_full_restart_wl_GC_prog_pre S ⟷ (∃T. (S, T) ∈ state_wl_l None ∧ correct_watching' S ∧ cdcl_twl_full_restart_l_GC_prog_pre T)› definition cdcl_twl_full_restart_wl_GC_prog where ‹cdcl_twl_full_restart_wl_GC_prog S = do { ASSERT(cdcl_twl_full_restart_wl_GC_prog_pre S); S' ← cdcl_twl_local_restart_wl_spec0 S; T ← remove_one_annot_true_clause_imp_wl S'; ASSERT(mark_to_delete_clauses_wl_pre T); U ← mark_to_delete_clauses_wl2 T; V ← cdcl_GC_clauses_wl U; ASSERT(cdcl_twl_full_restart_wl_GC_prog_post S V); RETURN V }› lemma cdcl_twl_local_restart_wl_spec0_cdcl_twl_local_restart_l_spec0: ‹(x, y) ∈ {(S, S'). (S, S') ∈ state_wl_l None ∧ correct_watching'' S} ⟹ cdcl_twl_local_restart_wl_spec0 x ≤ ⇓ {(S, S'). (S, S') ∈ state_wl_l None ∧ correct_watching'' S} (cdcl_twl_local_restart_l_spec0 y)› by (cases x; cases y) (auto simp: cdcl_twl_local_restart_wl_spec0_def cdcl_twl_local_restart_l_spec0_def state_wl_l_def image_iff correct_watching''.simps clause_to_update_def conc_fun_RES RES_RETURN_RES2) lemma cdcl_twl_full_restart_wl_GC_prog_post_correct_watching: assumes pre: ‹cdcl_twl_full_restart_l_GC_prog_pre y› and y_Va: ‹cdcl_twl_restart_l y Va› ‹(V, Va) ∈ {(S, S'). (S, S') ∈ state_wl_l None ∧ correct_watching' S}› shows ‹(V, Va) ∈ {(S, S'). (S, S') ∈ state_wl_l None ∧ correct_watching S}› and ‹set_mset (all_lits_of_mm (mset `# init_clss_lf (get_clauses_wl V)+ get_unit_init_clss_wl V)) = set_mset (all_lits_of_mm (mset `# ran_mf (get_clauses_wl V)+ get_unit_clauses_wl V))› proof - obtain x where y_x: ‹(y, x) ∈ twl_st_l None› and struct_invs: ‹twl_struct_invs x› and list_invs: ‹twl_list_invs y› using pre unfolding cdcl_twl_full_restart_l_GC_prog_pre_def by blast obtain V' where ‹cdcl_twl_restart x V'› and Va_V': ‹(Va, V') ∈ twl_st_l None› using cdcl_twl_restart_l_cdcl_twl_restart[OF y_x list_invs struct_invs] y_Va unfolding conc_fun_RES by auto then have ‹twl_struct_invs V'› using struct_invs by (blast dest: cdcl_twl_restart_twl_struct_invs) then have ‹cdcl⇩W_restart_mset.no_strange_atm (state⇩W_of V')› unfolding twl_struct_invs_def cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def by blast then show ‹set_mset (all_lits_of_mm (mset `# init_clss_lf (get_clauses_wl V)+ get_unit_init_clss_wl V)) = set_mset (all_lits_of_mm (mset `# ran_mf (get_clauses_wl V)+ get_unit_clauses_wl V))› using assms(3) Va_V' apply (cases V; cases V') apply (auto simp: state_wl_l_def cdcl⇩W_restart_mset.no_strange_atm_def twl_st_l_def cdcl⇩W_restart_mset_state image_image mset_take_mset_drop_mset' in_all_lits_of_mm_ain_atms_of_iff atms_of_ms_def atms_of_def atm_of_eq_atm_of conj_disj_distribR Collect_disj_eq ex_disj_distrib split: if_splits dest!: multi_member_split[of _ ‹ran_m _›]) apply (auto dest!: split_list dest!: multi_member_split) done then have ‹correct_watching' V ⟹ correct_watching V› by (cases V) (auto simp: correct_watching.simps correct_watching'.simps) then show‹(V, Va) ∈ {(S, S'). (S, S') ∈ state_wl_l None ∧ correct_watching S}› using assms by (auto simp: cdcl_twl_full_restart_wl_GC_prog_post_def) qed lemma cdcl_twl_full_restart_wl_GC_prog: ‹(cdcl_twl_full_restart_wl_GC_prog, cdcl_twl_full_restart_l_GC_prog) ∈ {(S::'v twl_st_wl, S'). (S, S') ∈ state_wl_l None ∧ correct_watching' S} →⇩f ⟨{(S::'v twl_st_wl, S'). (S, S') ∈ state_wl_l None ∧ correct_watching S}⟩nres_rel› unfolding cdcl_twl_full_restart_wl_GC_prog_def cdcl_twl_full_restart_l_GC_prog_def apply (intro frefI nres_relI) apply (refine_vcg remove_one_annot_true_clause_imp_wl_remove_one_annot_true_clause_imp[THEN fref_to_Down] mark_to_delete_clauses_wl_mark_to_delete_clauses_l2[THEN fref_to_Down] cdcl_GC_clauses_wl_cdcl_GC_clauses[THEN fref_to_Down] cdcl_twl_local_restart_wl_spec0_cdcl_twl_local_restart_l_spec0) subgoal unfolding cdcl_twl_full_restart_wl_GC_prog_pre_def by blast subgoal by (auto dest: correct_watching'_correct_watching'') subgoal unfolding mark_to_delete_clauses_wl_pre_def by fast subgoal for x y S S' T Ta U Ua V Va using cdcl_twl_full_restart_wl_GC_prog_post_correct_watching[of y Va V] unfolding cdcl_twl_full_restart_wl_GC_prog_post_def by fast subgoal for x y S' S'a T Ta U Ua V Va by (rule cdcl_twl_full_restart_wl_GC_prog_post_correct_watching) done definition (in twl_restart_ops) restart_prog_wl :: "'v twl_st_wl ⇒ nat ⇒ bool ⇒ ('v twl_st_wl × nat) nres" where ‹restart_prog_wl S n brk = do { ASSERT(restart_abs_wl_pre S brk); b ← restart_required_wl S n; b2 ← SPEC(λ_. True); if b2 ∧ b ∧ ¬brk then do { T ← cdcl_twl_full_restart_wl_GC_prog S; RETURN (T, n + 1) } else if b ∧ ¬brk then do { T ← cdcl_twl_restart_wl_prog S; RETURN (T, n + 1) } else RETURN (S, n) }› lemma cdcl_twl_full_restart_wl_prog_cdcl_twl_restart_l_prog: ‹(uncurry2 restart_prog_wl, uncurry2 restart_prog_l) ∈ {(S, T). (S, T) ∈ state_wl_l None ∧ correct_watching S} ×⇩f nat_rel ×⇩f bool_rel →⇩f ⟨{(S, T). (S, T) ∈ state_wl_l None ∧ correct_watching S} ×⇩f nat_rel⟩nres_rel› (is ‹_ ∈ ?R ×⇩f _ ×⇩f _ →⇩f ⟨?R'⟩nres_rel›) proof - have [refine0]: ‹restart_required_wl a b ≤ ⇓ Id (restart_required_l a' b')› if ‹(a, a') ∈ ?R› and ‹(b, b') ∈ nat_rel› for a a' b b' using that unfolding restart_required_wl_def restart_required_l_def by (auto simp: twl_st_l) show ?thesis unfolding uncurry_def restart_prog_wl_def restart_prog_l_def rewatch_clauses_def apply (intro frefI nres_relI) apply (refine_rcg cdcl_twl_restart_wl_prog_cdcl_twl_restart_l_prog[THEN fref_to_Down] cdcl_twl_full_restart_wl_GC_prog[THEN fref_to_Down]) subgoal unfolding restart_abs_wl_pre_def by (fastforce simp: correct_watching_correct_watching) subgoal by auto subgoal by auto subgoal by auto subgoal by (auto simp: correct_watching_correct_watching) subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto done qed definition (in twl_restart_ops) cdcl_twl_stgy_restart_prog_wl :: ‹'v twl_st_wl ⇒ 'v twl_st_wl nres› where ‹cdcl_twl_stgy_restart_prog_wl (S⇩0::'v twl_st_wl) = do { (brk, T, _) ← WHILE⇩T⇗λ(brk, T, n). cdcl_twl_stgy_restart_abs_wl_inv S⇩0 brk T n⇖ (λ(brk, _). ¬brk) (λ(brk, S, n). do { T ← unit_propagation_outer_loop_wl S; (brk, T) ← cdcl_twl_o_prog_wl T; (T, n) ← restart_prog_wl T n brk; RETURN (brk, T, n) }) (False, S⇩0::'v twl_st_wl, 0); RETURN T }› lemma cdcl_twl_stgy_restart_prog_wl_cdcl_twl_stgy_restart_prog_l: ‹(cdcl_twl_stgy_restart_prog_wl, cdcl_twl_stgy_restart_prog_l) ∈ {(S, T). (S, T) ∈ state_wl_l None ∧ correct_watching S} →⇩f ⟨{(S, T). (S, T) ∈ state_wl_l None ∧ correct_watching S}⟩nres_rel› (is ‹_ ∈ ?R →⇩f ⟨?S⟩nres_rel›) proof - have [refine0]: ‹(x, y) ∈ ?R ⟹ ((False, x, 0), False, y, 0) ∈ bool_rel ×⇩r ?R ×⇩r nat_rel› for x y by auto show ?thesis unfolding cdcl_twl_stgy_restart_prog_wl_def cdcl_twl_stgy_restart_prog_l_def apply (intro frefI nres_relI) apply (refine_rcg WHILEIT_refine[where R=‹{(S, T). (S, T) ∈ state_wl_l None ∧ correct_watching S}›] unit_propagation_outer_loop_wl_spec[THEN fref_to_Down] cdcl_twl_full_restart_wl_prog_cdcl_twl_restart_l_prog[THEN fref_to_Down_curry2] cdcl_twl_o_prog_wl_spec[THEN fref_to_Down]) subgoal unfolding cdcl_twl_stgy_restart_abs_wl_inv_def by fastforce subgoal by auto subgoal by auto subgoal by (auto simp: correct_watching_correct_watching) subgoal by auto subgoal by auto done qed definition (in twl_restart_ops) cdcl_twl_stgy_restart_prog_early_wl :: ‹'v twl_st_wl ⇒ 'v twl_st_wl nres› where ‹cdcl_twl_stgy_restart_prog_early_wl (S⇩0::'v twl_st_wl) = do { ebrk ← RES UNIV; (_, brk, T, n) ← WHILE⇩T⇗λ(_, brk, T, n). cdcl_twl_stgy_restart_abs_wl_inv S⇩0 brk T n⇖ (λ(ebrk, brk, _). ¬brk ∧ ¬ebrk) (λ(_, brk, S, n). do { T ← unit_propagation_outer_loop_wl S; (brk, T) ← cdcl_twl_o_prog_wl T; (T, n) ← restart_prog_wl T n brk; ebrk ← RES UNIV; RETURN (ebrk, brk, T, n) }) (ebrk, False, S⇩0::'v twl_st_wl, 0); if ¬ brk then do { (brk, T, _) ← WHILE⇩T⇗λ(brk, T, n). cdcl_twl_stgy_restart_abs_wl_inv S⇩0 brk T n⇖ (λ(brk, _). ¬brk) (λ(brk, S, n). do { T ← unit_propagation_outer_loop_wl S; (brk, T) ← cdcl_twl_o_prog_wl T; (T, n) ← restart_prog_wl T n brk; RETURN (brk, T, n) }) (False, T::'v twl_st_wl, n); RETURN T } else RETURN T }› lemma cdcl_twl_stgy_restart_prog_early_wl_cdcl_twl_stgy_restart_prog_early_l: ‹(cdcl_twl_stgy_restart_prog_early_wl, cdcl_twl_stgy_restart_prog_early_l) ∈ {(S, T). (S, T) ∈ state_wl_l None ∧ correct_watching S} →⇩f ⟨{(S, T). (S, T) ∈ state_wl_l None ∧ correct_watching S}⟩nres_rel› (is ‹_ ∈ ?R →⇩f ⟨?S⟩nres_rel›) proof - show ?thesis unfolding cdcl_twl_stgy_restart_prog_early_wl_def cdcl_twl_stgy_restart_prog_early_l_def apply (intro frefI nres_relI) apply (refine_rcg WHILEIT_refine[where R=‹bool_rel ×⇩r ?R ×⇩r nat_rel›] WHILEIT_refine[where R=‹bool_rel ×⇩r bool_rel ×⇩r ?R ×⇩r nat_rel›] unit_propagation_outer_loop_wl_spec[THEN fref_to_Down] cdcl_twl_full_restart_wl_prog_cdcl_twl_restart_l_prog[THEN fref_to_Down_curry2] cdcl_twl_o_prog_wl_spec[THEN fref_to_Down]) subgoal by auto subgoal unfolding cdcl_twl_stgy_restart_abs_wl_inv_def by fastforce subgoal by auto subgoal by (auto simp: correct_watching_correct_watching) subgoal by auto subgoal by auto subgoal by auto subgoal by (auto simp: correct_watching_correct_watching) subgoal unfolding cdcl_twl_stgy_restart_abs_wl_inv_def by fastforce subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto done qed theorem cdcl_twl_stgy_restart_prog_wl_spec: ‹(cdcl_twl_stgy_restart_prog_wl, cdcl_twl_stgy_restart_prog_l) ∈ {(S::'v twl_st_wl, S'). (S, S') ∈ state_wl_l None ∧ correct_watching S} → ⟨state_wl_l None⟩nres_rel› (is ‹?o ∈ ?A → ⟨?B⟩ nres_rel›) using cdcl_twl_stgy_restart_prog_wl_cdcl_twl_stgy_restart_prog_l[where 'a='v] unfolding fref_param1 apply - apply (match_spec; match_fun_rel+; (fast intro: nres_rel_mono)?) by (metis (no_types, lifting) in_pair_collect_simp nres_rel_mono subrelI) theorem cdcl_twl_stgy_restart_prog_early_wl_spec: ‹(cdcl_twl_stgy_restart_prog_early_wl, cdcl_twl_stgy_restart_prog_early_l) ∈ {(S::'v twl_st_wl, S'). (S, S') ∈ state_wl_l None ∧ correct_watching S} → ⟨state_wl_l None⟩nres_rel› (is ‹?o ∈ ?A → ⟨?B⟩ nres_rel›) using cdcl_twl_stgy_restart_prog_early_wl_cdcl_twl_stgy_restart_prog_early_l[where 'a='v] unfolding fref_param1 apply - by (match_spec; match_fun_rel+; (fast intro: nres_rel_mono)?; match_fun_rel?) auto definition (in twl_restart_ops) cdcl_twl_stgy_restart_prog_bounded_wl :: ‹'v twl_st_wl ⇒ (bool × 'v twl_st_wl) nres› where ‹cdcl_twl_stgy_restart_prog_bounded_wl (S⇩0::'v twl_st_wl) = do { ebrk ← RES UNIV; (_, brk, T, n) ← WHILE⇩T⇗λ(_, brk, T, n). cdcl_twl_stgy_restart_abs_wl_inv S⇩0 brk T n⇖ (λ(ebrk, brk, _). ¬brk ∧ ¬ebrk) (λ(_, brk, S, n). do { T ← unit_propagation_outer_loop_wl S; (brk, T) ← cdcl_twl_o_prog_wl T; (T, n) ← restart_prog_wl T n brk; ebrk ← RES UNIV; RETURN (ebrk, brk, T, n) }) (ebrk, False, S⇩0::'v twl_st_wl, 0); RETURN (brk, T) }› lemma cdcl_twl_stgy_restart_prog_bounded_wl_cdcl_twl_stgy_restart_prog_bounded_l: ‹(cdcl_twl_stgy_restart_prog_bounded_wl, cdcl_twl_stgy_restart_prog_bounded_l) ∈ {(S, T). (S, T) ∈ state_wl_l None ∧ correct_watching S} →⇩f ⟨bool_rel ×⇩r {(S, T). (S, T) ∈ state_wl_l None ∧ correct_watching S}⟩nres_rel› (is ‹_ ∈ ?R →⇩f ⟨?S⟩nres_rel›) proof - show ?thesis unfolding cdcl_twl_stgy_restart_prog_bounded_wl_def cdcl_twl_stgy_restart_prog_bounded_l_def apply (intro frefI nres_relI) apply (refine_rcg WHILEIT_refine[where R=‹bool_rel ×⇩r bool_rel ×⇩r ?R ×⇩r nat_rel›] unit_propagation_outer_loop_wl_spec[THEN fref_to_Down] cdcl_twl_full_restart_wl_prog_cdcl_twl_restart_l_prog[THEN fref_to_Down_curry2] cdcl_twl_o_prog_wl_spec[THEN fref_to_Down]) subgoal by auto subgoal unfolding cdcl_twl_stgy_restart_abs_wl_inv_def by fastforce subgoal by auto subgoal by (auto simp: correct_watching_correct_watching) subgoal by auto subgoal by auto subgoal by auto done qed theorem cdcl_twl_stgy_restart_prog_bounded_wl_spec: ‹(cdcl_twl_stgy_restart_prog_bounded_wl, cdcl_twl_stgy_restart_prog_bounded_l) ∈ {(S::'v twl_st_wl, S'). (S, S') ∈ state_wl_l None ∧ correct_watching S} → ⟨bool_rel ×⇩r state_wl_l None⟩nres_rel› (is ‹?o ∈ ?A → ⟨?B⟩ nres_rel›) using cdcl_twl_stgy_restart_prog_bounded_wl_cdcl_twl_stgy_restart_prog_bounded_l[where 'a='v] unfolding fref_param1 apply - by (match_spec; match_fun_rel+; (fast intro: nres_rel_mono)?; match_fun_rel?) auto end end