Theory IsaSAT_Simplify

theory IsaSAT_Simplify_Units imports IsaSAT_Setup IsaSAT_Simplify_Units_Defs IsaSAT_Restart (*line 691 in auto TODO: which simp rule should be moved?*) begin text ‹Makes the simplifier loop...› definition simplify_clause_with_unit2_rel_simp_wo where ‹simplify_clause_with_unit2_rel_simp_wo unc N N₀ N' ⟷ (unc ⟶ N = N₀ ∧ N' = N₀)› lemma simplify_clause_with_unit2_rel_simp_wo[iff]: ‹simplify_clause_with_unit2_rel_simp_wo True N N₀ N' ⟷ (N = N₀ ∧ N' = N₀)› ‹simplify_clause_with_unit2_rel_simp_wo False N N₀ N'› unfolding simplify_clause_with_unit2_rel_simp_wo_def by auto definition simplify_clause_with_unit2_rel where ‹simplify_clause_with_unit2_rel N₀ C= {((unc, N, L, b, i), (unc', b', N')). (C ∈# dom_m N ⟶ N' = N) ∧ (C ∉# dom_m N ⟶ fmdrop C N' = N) ∧ (¬b ⟶ length (N' ∝ C) = 1 ⟶ C ∉#dom_m N ∧ N' ∝ C = [L]) ∧ (if b ∨ i ≤ 1 then C ∉# dom_m N else C ∈#dom_m N) ∧ (b=b') ∧ (¬b ⟶ i = size (N' ∝ C)) ∧ C ∈# dom_m N' ∧ (b ∨ i ≤ 1 ⟶ size (learned_clss_lf N) = size (learned_clss_lf N₀) - (if irred N₀ C then 0 else 1))∧ (¬(b ∨ i ≤ 1) ⟶ size (learned_clss_lf N) = size (learned_clss_lf N₀)) ∧ (C ∈# dom_m N ⟶ dom_m N = dom_m N₀) ∧ (C ∈# dom_m N ⟶ irred N C = irred N₀ C ∧ irred N C = irred N' C) ∧ (C ∉# dom_m N ⟶ dom_m N = remove1_mset C (dom_m N₀)) ∧ unc=unc' ∧ simplify_clause_with_unit2_rel_simp_wo unc N N₀ N'}› lemma simplify_clause_with_unit2_simplify_clause_with_unit: fixes N N₀ :: ‹'v clauses_l› and N' :: ‹'a› assumes ‹C ∈# dom_m N› ‹no_dup M› and st: ‹(M,M') ∈ Id› ‹(C,C') ∈ Id› ‹(N,N₀)∈ Id› shows ‹simplify_clause_with_unit2 C M N ≤ ⇓ (simplify_clause_with_unit2_rel N₀ C) (simplify_clause_with_unit C' M' N₀)› proof - have simplify_clause_with_unit_alt_def: ‹simplify_clause_with_unit = (λC M N. do { (unc, b, N') ← SPEC(λ(unc, b, N'). fmdrop C N = fmdrop C N' ∧ mset (N' ∝ C) ⊆# mset (N ∝ C) ∧ C ∈# dom_m N' ∧ (¬b ⟶ (∀L ∈# mset (N' ∝ C). undefined_lit M L)) ∧ (∀L ∈# mset (N ∝ C) - mset (N' ∝ C). defined_lit M L) ∧ (irred N C = irred N' C) ∧ (b ⟷ (∃L. L ∈# mset (N ∝ C) ∧ L ∈ lits_of_l M)) ∧ (unc ⟶ N = N' ∧ ¬b)); RETURN (unc, b, N') })› (is ‹_ = (λC M N. do { (_, _, _) ← SPEC (?P C M N); RETURN _})›) unfolding simplify_clause_with_unit_def by auto have st: ‹M' = M› ‹C'=C› ‹N₀=N› using st by auto let ?R = ‹measure (λ(i, j, N', is_true). Suc (length (N ∝ C)) - j)› define I where ‹I = (λ(i::nat, j::nat, N' :: 'v clauses_l, del:: 'v clause, is_true). i ≤ j ∧ j ≤ length (N ∝ C) ∧ C ∈# dom_m N' ∧ dom_m N' = dom_m N ∧ ( (∀L∈set (take i (N' ∝ C)). undefined_lit M L) ∧ (∀L∈# del. defined_lit M L) ∧ drop j (N' ∝ C) = drop j (N ∝ C) ∧ length (N' ∝ C) = length (N ∝ C) ∧ mset (take j (N ∝ C)) = del + mset (take i (N' ∝ C))) ∧ fmdrop C N' = fmdrop C N ∧ (irred N' C = irred N C) ∧ (is_true ⟷ (∃L ∈ set (take j (N ∝ C)). L ∈ lits_of_l M)) ∧ (i = j ⟶ take i (N' ∝ C) = take j (N ∝ C)))› have I0: ‹I (0, 0, N, {#}, False)› using assms unfolding I_def by auto have H: ‹(if b then RETURN P else RETURN Q) = RETURN (if b then P else Q)› for b P Q by auto have I_Suc: ‹I (if polarity M (ab ∝ C ! aa) = Some True then (a, aa + 1, ab, add_mset (ab ∝ C ! aa) del,True) else if polarity M (ab ∝ C ! aa) = Some False then (a, aa + 1, ab, add_mset (ab ∝ C ! aa) del, False) else (a + 1, aa + 1, ab(C ↪ (ab ∝ C)[a := ab ∝ C ! aa]), del, False))› if I: ‹I s› and ‹case s of (i, j, _, _, b) ⇒ ¬ b ∧ j < length (N ∝ C)› and st: ‹s = (a, b)› ‹b = (aa, ba)› ‹ba = (ab, bdel)› ‹bdel = (del, bb)› and le: ‹a < length (ab ∝ C) ∧ aa < length (ab ∝ C) ∧ C ∈# dom_m ab ∧ a ≤ aa› for s a b aa ba ab bb el del bdel proof - have[simp]: ‹C ∉# remove1_mset C (dom_m N)› using assms distinct_mset_dom[of N] by (auto dest!: multi_member_split) have [simp]: ‹(take a (ab ∝ C) @ [ab ∝ C ! a])[a := N ∝ C ! aa] = take a (ab ∝ C) @ [N ∝ C ! aa]› using I le unfolding I_def st by (auto simp: list_update_append) consider ‹polarity M (ab ∝ C ! aa) = Some True› | ‹polarity M (ab ∝ C ! aa) = Some False› | ‹polarity M (ab ∝ C ! aa) = None› by (cases ‹polarity M (ab ∝ C ! aa)›) auto then show ?thesis using that apply cases subgoal by (auto simp: I_def take_Suc_conv_app_nth fmdrop_fmupd_same polarity_spec' assms simp flip: Cons_nth_drop_Suc dest: in_lits_of_l_defined_litD) subgoal by (auto simp: I_def take_Suc_conv_app_nth fmdrop_fmupd_same polarity_spec' assms dest: uminus_lits_of_l_definedD simp flip: Cons_nth_drop_Suc) subgoal by (simp add: I_def take_Suc_conv_app_nth polarity_spec' assms(2) fmdrop_fmupd_same nth_append list_update_append flip: Cons_nth_drop_Suc) (clarsimp simp only: Decided_Propagated_in_iff_in_lits_of_l simp_thms) done qed have [simp]: ‹C ∉# remove1_mset C (dom_m x1b)› for x1b using distinct_mset_dom[of x1b] by (cases ‹C ∈# dom_m x1b›) (auto dest!: multi_member_split) have H0: ‹C = [c] ⟷ mset C = {#c#}› for C c by auto have filt: ‹(⋀x. x ∈# C ⟹ P x) ⟹ filter_mset P C = C› ‹(⋀x. x ∈# C ⟹ ¬P x) ⟹ filter_mset P C = {#}› ‹filter P D = [] ⟷ (∀L∈#mset D. ¬P L)›for C P D by (simp_all add: filter_mset_eq_conv filter_empty_conv) have [simp]: ‹take (Suc 0) C = [C!0] ⟷ C ≠ []› for C by (cases C) auto have in_set_dropp_begin: ‹drop n xs = drop n ys ⟹ n < length xs ⟹ xs ! n ∈ set ys› for n xs ys by (metis in_set_dropD in_set_dropI le_cases) let ?Q = ‹λ(i::nat, j::nat, N', del, is_true) (unc, b, N''). (let P = (if is_true then N'(C ↪ filter (Not o defined_lit M) (N ∝ C)) else N'(C ↪ take i (N' ∝ C)))in (P, N'') ∈ Id ∧ ?P C M N (unc, b, N'') ∧ (is_true ∨ j = length (N ∝ C)) ∧ (unc ⟷ ¬is_true ∧ i = j ∧ i > 1))› have H3: ‹∀x∈#ab. defined_lit M x ⟹ undefined_lit M a ⟹ mset (N ∝ C) = add_mset a ab ⟹ filter (undefined_lit M) (N ∝ C) = [a]› for a ab by (simp add: H0 filt) have H4: ‹fmdrop C N = fmdrop C x1a ⟹ C ∈# dom_m x1a ⟹ size (learned_clss_l x1a) = size (learned_clss_l N) ⟷ (irred x1a C ⟷ irred N C)› for x1a using assms(1) apply (auto simp: ran_m_def dest!: multi_member_split split: if_splits intro!: filter_mset_cong2) apply (smt (verit, best) ‹⋀x1b. C ∉# remove1_mset C (dom_m x1b)› add_mset_remove_trivial dom_m_fmdrop fmdrop_eq_update_eq fmupd_lookup image_mset_cong2 n_not_Suc_n union_single_eq_member) apply (smt (verit, best) ‹⋀x1b. C ∉# remove1_mset C (dom_m x1b)› add_mset_remove_trivial dom_m_fmdrop fmdrop_eq_update_eq fmupd_lookup image_mset_cong2 n_not_Suc_n union_single_eq_member) apply (smt (verit, best) ‹⋀x1b. C ∉# remove1_mset C (dom_m x1b)› add_mset_remove_trivial dom_m_fmdrop fmdrop_eq_update_eq fmupd_lookup image_mset_cong2 union_single_eq_member) by (smt (verit, ccfv_SIG) ‹⋀x1b. C ∉# remove1_mset C (dom_m x1b)› add_mset_remove_trivial dom_m_fmdrop fmdrop_eq_update_eq fmupd_lookup image_mset_cong2 union_single_eq_member) have H5: ‹irred x2c C ⟹ size (learned_clss_l (fmupd C (x, True) x2c)) = size (learned_clss_l x2c)› for x x2c using distinct_mset_dom[of x2c] by (cases ‹C ∈# dom_m x2c›) (force dest!: multi_member_split simp: ran_m_def intro: filter_mset_cong2 image_mset_cong2 intro: multiset.map_cong multiset.map_cong0 intro!: arg_cong[of _ _ size])+ have H6: ‹¬irred x2c C ⟹ C ∈# dom_m x2c ⟹ size (learned_clss_l (fmupd C (x, False) x2c)) = (size (learned_clss_l x2c))› for x x2c using distinct_mset_dom[of x2c] apply (cases ‹C ∈# dom_m x2c›) by (force dest!: multi_member_split simp: ran_m_def intro: filter_mset_cong2 image_mset_cong2 intro: multiset.map_cong multiset.map_cong0 intro: arg_cong[of _ _ size])+ have H7: ‹¬irred x1a C ⟹ C ∈# dom_m x1a ⟹ size (remove1_mset (the (fmlookup x1a C)) (learned_clss_l x1a)) = size (learned_clss_l x1a) - Suc 0 › for x1a by (auto simp: ran_m_def dest!: multi_member_split) have H8: ‹fmdrop C x1a = fmdrop C N ⟹ C ∈# dom_m x1a ⟹ irred x1a C = irred N C ⟹ size (learned_clss_l x1a) - Suc 0 = size (learned_clss_l N) - Suc 0 › for x1a using assms(1) distinct_mset_dom[of x1a] apply (auto dest!: multi_member_split simp: ran_m_def) apply (smt (verit, best) ‹⋀x1b. C ∉# remove1_mset C (dom_m x1b)› add_mset_remove_trivial dom_m_fmdrop fmdrop_eq_update_eq2 fmupd_lookup image_mset_cong2 union_single_eq_member) by (metis (no_types, lifting) add_mset_remove_trivial dom_m_fmdrop fmdrop_eq_update_eq fmupd_lookup image_mset_cong2 union_single_eq_member) have H9: ‹fmdrop C N = fmdrop C x1a ⟹ remove1_mset C (dom_m x1a) = remove1_mset C (dom_m N)› for x1a by (metis dom_m_fmdrop) have eq_upd_same: ‹fmdrop C aa = fmdrop C N ⟹ b= irred N C ⟹ N = fmupd C (filter (undefined_lit M) (N ∝ C), b) aa ⟷ (∀x ∈ set (N ∝ C). undefined_lit M x)› for aa b apply (rule iffI) subgoal by (subst arg_cong[of ‹N› ‹fmupd C (filter (undefined_lit M) (N ∝ C), b) aa› ‹λN. N ∝ C›, unfolded fmupd_lookup]) simp_all subgoal apply (subst fmap.fmlookup_inject[symmetric]) apply (cases ‹the (fmlookup N C)›; cases ‹fmlookup N C›) using fmupd_same[OF assms(1)] assms(1) arg_cong[of ‹fmdrop C aa› ‹fmdrop C N› ‹λN. fmlookup N x› for x, unfolded fmlookup_drop] apply (auto intro!: ext split: if_splits) by metis done have H11: ‹¬ irred N C ⟹ C ∈# dom_m N ⟹ size (learned_clss_l (fmdrop C N)) = size (learned_clss_l N) - Suc 0› for N using distinct_mset_dom[of N] by (auto simp: learned_clss_l_l_fmdrop ran_m_def dest!: multi_member_split intro!: arg_cong[of _ _ size] image_mset_cong2 filter_mset_cong2) have fmdrop_eq_update_eq': ‹fmdrop C aa = fmdrop C N ⟹ b = irred N C ⟹ N = fmupd C (N ∝ C, b) aa› for aa b using assms(1) fmdrop_eq_update_eq by blast have [simp]: ‹fmupd C (D) aa = fmupd C (E) aa ⟷ D = E› for aa D E apply auto by (metis fmupd_lookup option.sel) have [simp]: ‹(∀a. a) ⟷ False› by blast define simp_work_around where ‹simp_work_around unc b b' ≡ unc ⟶ N = b ∧ ¬b'› for unc b b' have simp_work_around_simp[simp]: ‹simp_work_around True b b' ⟷ b = N ∧ ¬b'› for b b' unfolding simp_work_around_def by auto term ‹{(a, b). I a ∧ ?Q a (b) ∧ (fst b ⟷ ((snd o snd o snd o snd) a))}› have hd_nth_take: ‹length C > 0 ⟹ [C!0] = take (Suc 0) C› for C by (cases C; auto) show ?thesis unfolding simplify_clause_with_unit_alt_def simplify_clause_with_unit2_def Let_def H conc_fun_RES st simplify_clause_with_unit2_rel_def apply (rule ASSERT_leI) subgoal using assms by auto apply (refine_vcg WHILEIT_rule_stronger_inv_RES'[where I'=I and R = ‹?R› and H = ‹{(a, b). I a ∧ ?Q a b ∧ (fst (snd b) ⟷ ((snd o snd o snd o snd) a))}›]) subgoal by auto subgoal by (auto simp: I_def) subgoal by (rule I0) subgoal by (auto simp: I_def) subgoal by (auto simp: I_def) subgoal by (auto simp: I_def) subgoal by (auto simp: I_def) subgoal by (auto simp: I_def intro: in_set_dropp_begin) subgoal by (auto simp: I_def split: if_splits) subgoal by (rule I_Suc) subgoal by (auto simp: I_def) subgoal for s apply (cases s) apply (clarsimp intro!: RETURN_SPEC_refine) apply (intro conjI) subgoal apply (intro impI) apply (clarsimp simp add: I_def fmdrop_fmupd_same) apply (auto simp add: I_def mset_remove_filtered dest: in_set_takeD) done subgoal by (intro impI) (auto simp add: I_def fmdrop_fmupd_same intro!: fmdrop_eq_update_eq') done subgoal unfolding I_def simp_work_around_def[symmetric] by simp subgoal unfolding I_def simp_work_around_def[symmetric] by simp subgoal unfolding I_def simp_work_around_def[symmetric] by clarsimp subgoal for x x' x1 x2 x1a x2a x1b x2b x1c x2c x1d x2d x1e x2e unfolding I_def simp_work_around_def[symmetric] apply (cases ‹x2e ∨ x1b ≤ 1›) apply (simp only: if_True split: ) subgoal apply (simp add: hd_nth_take learned_clss_l_l_fmdrop_irrelev H5 H4 H9[of x2a] H11 ; (subst (asm) eq_commute[of ‹If _ (fmupd C (_, _) _) _› x2a])?) apply (intro conjI impI allI) apply (simp add: hd_nth_take) apply (clarsimp simp only:) apply (simp add: ) apply (clarsimp simp only:) apply (clarsimp simp only:) apply (simp add: ) apply (metis length_0_conv) apply (clarsimp simp only:; fail)+ apply (simp add: ) apply (clarsimp simp only: if_True if_False H11 H8[of ‹fmupd _ _ x1d›]) apply (clarsimp simp only: if_True if_False H11 H8[of ‹fmupd _ _ x1d›] refl split: if_splits) apply (metis (no_types, lifting) H8) apply (metis (no_types, lifting) H8) apply (clarsimp simp only: if_True if_False H11 H8[of x1d]) apply (metis (no_types, lifting)) apply (clarsimp simp only: if_True if_False H11 H8[of x1d]) done apply (cases ‹x1b = x1c ∧ ¬ x2e›) subgoal using fmupd_same[of C x1d] apply (cases ‹the (fmlookup x1d C)›) apply (simp only: if_True if_False simp_thms mem_Collect_eq prod.case Let_def linorder_class.not_le[symmetric] simp_work_around_simp take_all[OF order.refl] fmupd_lookup refl if_True simp_thms option.sel fst_conv simp_work_around_simp eq_commute[of ‹fmupd _ _ _› N] eq_commute [of x2a N] fst_conv snd_conv) apply (intro conjI impI allI) apply (clarsimp simp :; fail)+ done subgoal using fmupd_same[of C x1d] apply (cases ‹the (fmlookup x1d C)›) apply (cases ‹irred x2a C›) apply (simp_all only: if_True if_False simp_thms mem_Collect_eq prod.case Let_def linorder_class.not_le[symmetric] simp_work_around_simp take_all[OF order.refl] fmupd_lookup refl if_True simp_thms H4 H5 option.sel fst_conv simp_work_around_simp eq_commute[of ‹fmupd _ _ _› x2a] eq_commute [of x2a N] H4 H5 fst_conv snd_conv; intro conjI impI allI) apply (clarsimp simp :; fail)+ apply (clarsimp simp add: eq_commute[of ‹fmupd _ _ _› x2a]) apply (metis set_mset_mset union_iff) apply (clarsimp simp: H4 H5; fail)+ done done done qed lemma all_learned_all_lits_all_atms_st: ‹set_mset (all_learned_lits_of_wl T) = set_mset (all_learned_lits_of_wl S) ⟹ set_mset (all_init_lits_of_wl T) = set_mset (all_init_lits_of_wl S) ⟹ set_mset (all_atms_st T) = set_mset (all_atms_st S)› by (metis ℒ_a_l_l_all_atms all_lits_st_init_learned atms_of_ℒ_a_l_l_𝒜_i_n atms_of_cong_set_mset) lemma simplify_clause_with_unit_st2_simplify_clause_with_unit_st: fixes S :: ‹nat twl_st_wl› assumes ‹(C,C')∈Id› ‹(S,S')∈Id› shows ‹simplify_clause_with_unit_st2 C S ≤ ⇓Id (simplify_clause_with_unit_st_wl C' S')› proof - show ?thesis using assms unfolding simplify_clause_with_unit_st2_def simplify_clause_with_unit_st_wl_def if_False Let_def cons_trail_propagate_l_def nres_monad3 bind_to_let_conv supply [[goals_limit=1]] apply (refine_rcg simplify_clause_with_unit2_simplify_clause_with_unit[unfolded simplify_clause_with_unit2_rel_def]) subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal for x1 x2 x1a x2a x1b x2b x1c x2c x1d x2d x1e x2e x1f x2f x1g x2g x1h x2h x1i x2i x1j x2j x1k x2k x1l x2l x1m x2m x1n _ _ _ _ x2n x1o x2o x1p x2p x1q x2q x1r x2r x1s x2s x x' x1t x2t x1u x2u x1v x2v x1w x2w x1x x2x x1y x2y by (cases ‹C' ∉# dom_m x1y›) (simp_all add: eq_commute[of ‹remove1_mset _ _› ‹dom_m _›]) subgoal by auto subgoal by (clarsimp simp only: pair_in_Id_conv prod.inject mem_Collect_eq prod.case) subgoal by auto subgoal by auto subgoal by (clarsimp simp only: pair_in_Id_conv prod.inject mem_Collect_eq prod.case) auto subgoal by (clarsimp simp only: pair_in_Id_conv prod.inject mem_Collect_eq prod.case) auto subgoal by (rule all_learned_all_lits_all_atms_st) subgoal by (clarsimp simp add: learned_clss_l_l_fmdrop_irrelev learned_clss_l_l_fmdrop learned_clss_l_fmdrop_if) subgoal by (clarsimp simp add: ran_m_def dest!: multi_member_split) subgoal by auto subgoal by auto subgoal by auto subgoal by (simp flip: all_lits_of_all_atms_of add: all_atms_st_def all_lits_st_def) subgoal by auto subgoal by (clarsimp simp only: pair_in_Id_conv prod.inject mem_Collect_eq prod.case) auto subgoal by (clarsimp simp only: pair_in_Id_conv prod.inject mem_Collect_eq prod.case) auto subgoal by (rule all_learned_all_lits_all_atms_st) subgoal by (clarsimp simp add: learned_clss_l_l_fmdrop_irrelev learned_clss_l_l_fmdrop learned_clss_l_fmdrop_if) subgoal by (clarsimp simp add: ran_m_def dest!: multi_member_split) subgoal by auto subgoal by auto subgoal by (clarsimp simp only: pair_in_Id_conv prod.inject mem_Collect_eq prod.case) auto subgoal by (clarsimp simp only: pair_in_Id_conv prod.inject mem_Collect_eq prod.case) auto subgoal by (rule all_learned_all_lits_all_atms_st) subgoal by (clarsimp simp add: learned_clss_l_l_fmdrop_irrelev learned_clss_l_l_fmdrop learned_clss_l_fmdrop_if) subgoal by (clarsimp simp add: ran_m_def dest!: multi_member_split) subgoal by auto subgoal by (clarsimp simp only: pair_in_Id_conv prod.inject mem_Collect_eq prod.case disj.left_neutral) subgoal by (clarsimp simp only: pair_in_Id_conv prod.inject mem_Collect_eq prod.case disj.left_neutral) subgoal by (rule all_learned_all_lits_all_atms_st) subgoal by (clarsimp simp add: learned_clss_l_l_fmdrop_irrelev learned_clss_l_l_fmdrop learned_clss_l_fmdrop_if) subgoal by auto subgoal by auto done qed lemma simplify_clauses_with_unit_st2_simplify_clauses_with_unit_st: assumes ‹(S,S')∈Id› shows ‹simplify_clauses_with_unit_st2 S ≤ ⇓Id (simplify_clauses_with_unit_st_wl S')› proof - have inj: ‹inj_on id x› for x by auto show ?thesis using assms unfolding simplify_clauses_with_unit_st2_def simplify_clauses_with_unit_st_wl_def by (refine_vcg simplify_clause_with_unit_st2_simplify_clause_with_unit_st inj) auto qed lemma simplify_clause_with_unit2_alt_def: ‹simplify_clause_with_unit2 C M N₀ = do { ASSERT(C ∈# dom_m N₀); let l = length (N₀ ∝ C); (i, j, N, del, is_true) ← WHILE_T⇗λ(i, j, N, del, b). C ∈# dom_m N⇖ (λ(i, j, N, del, b). ¬b ∧ j < l) (λ(i, j, N, del, is_true). do { ASSERT(i < length (N ∝ C) ∧ j < length (N ∝ C) ∧ C ∈# dom_m N ∧ i ≤ j); let L = N ∝ C ! j; ASSERT(L ∈ set (N₀ ∝ C)); let val = polarity M L; if val = Some True then RETURN (i, j+1, N, add_mset L del, True) else if val = Some False then RETURN (i, j+1, N, add_mset L del, False) else let N = N(C ↪ ((N ∝ C)[i := L])) in RETURN (i+1, j+1, N, del, False) }) (0, 0, N₀, {#}, False); ASSERT (C ∈# dom_m N ∧ i ≤ length (N ∝ C)); ASSERT (is_true ∨ j = length (N₀ ∝ C)); let L = N ∝ C ! 0; if is_true ∨ i ≤ 1 then RETURN (False, fmdrop C N, L, is_true, i) else if i=j ∧ ¬ is_true then RETURN (True, N, L, is_true, i) else do { let N = N(C ↪ (take i (N ∝ C))) in RETURN (False, N, L, is_true, i)} }› unfolding Let_def simplify_clause_with_unit2_def by (auto intro!: bind_cong[OF refl]) (*TODO: WTF*) lemma normalize_down_return_spec: ‹⇓A ((RETURN o f) c) = SPEC (λa. (a, f c) ∈ {(a,b). (a,b) ∈ A ∧ b = f c})› by (auto simp: conc_fun_RES RETURN_def) (*TODO Move*) lemma arena_length_le_length_arena: ‹C' ∈# dom_m N ⟹ valid_arena arena N vdom ⟹ arena_length arena C' < length arena› by (smt (verit, best) Nat.le_diff_conv2 STATUS_SHIFT_def Suc_le_lessD arena_lifting(10) arena_lifting(16) arena_lifting(4) diff_self_eq_0 le_trans less_Suc_eq not_less_eq not_less_eq_eq numeral_2_eq_2) lemma simplify_clause_with_unit_st_wl_preD: assumes ‹simplify_clause_with_unit_st_wl_pre C S› shows simplify_clause_with_unit_st_wl_pre_all_init_atms_all_atms: ‹set_mset (all_init_atms_st S) = set_mset (all_atms_st S)› and ‹isasat_input_bounded (all_init_atms_st S) ⟹ length (get_clauses_wl S ∝ C) ≤ Suc (unat32_max div 2)› proof - obtain x xa where Sx: ‹(S, x) ∈ state_wl_l None› and C: ‹C ∈# dom_m (get_clauses_l x)› and ‹count_decided (get_trail_l x) = 0› and ‹get_conflict_l x = None› and ‹clauses_to_update_l x = {#}› and xxa: ‹(x, xa) ∈ twl_st_l None› and ‹twl_st_inv xa› and ‹valid_enqueued xa› and ‹cdcl_W_restart_mset.no_smaller_propa (state_W_of xa)› and alien: ‹cdcl_W_restart_mset.no_strange_atm (state_W_of xa)› and ‹entailed_clss_inv (pstate_W_of xa)› and ‹twl_st_exception_inv xa› and ‹cdcl_W_restart_mset.cdcl_W_M_level_inv (state_W_of xa)› and ‹psubsumed_invs (pstate_W_of xa)› and ‹clauses0_inv (pstate_W_of xa)› and ‹no_duplicate_queued xa› and ‹∀s∈#learned_clss (state_W_of xa). ¬ tautology s› and ‹distinct_queued xa› and dist: ‹cdcl_W_restart_mset.distinct_cdcl_W_state (state_W_of xa)› and ‹confl_cands_enqueued xa› and ‹cdcl_W_restart_mset.cdcl_W_conflicting (state_W_of xa)› and ‹propa_cands_enqueued xa› and ‹all_decomposition_implies_m (cdcl_W_restart_mset.clauses (state_W_of xa)) (get_all_ann_decomposition (trail (state_W_of xa)))› and ‹cdcl_W_restart_mset.cdcl_W_learned_clause (state_W_of xa)› and ‹get_conflict xa ≠ None ⟶ clauses_to_update xa = {#} ∧ literals_to_update xa = {#}› and ‹clauses_to_update_inv xa› and ‹past_invs xa› and list: ‹twl_list_invs x› using assms unfolding simplify_clause_with_unit_st_wl_pre_def twl_struct_invs_def simplify_clause_with_unit_st_pre_def pcdcl_all_struct_invs_def cdcl_W_restart_mset.cdcl_W_all_struct_inv_def state_W_of_def[symmetric] apply - by blast show H: ‹set_mset (all_init_atms_st S) = set_mset (all_atms_st S)› using Sx xxa alien unfolding all_init_atms_def all_init_atms_st_def all_atms_st_def all_init_lits_def all_lits_of_mm_union image_mset_union get_unit_clauses_wl_alt_def all_atms_def all_lits_def set_mset_union atm_of_all_lits_of_mm cdcl_W_restart_mset.no_strange_atm_def apply (subst (2)all_clss_l_ran_m[symmetric]) apply (subst all_clss_l_ran_m[symmetric]) unfolding image_mset_union filter_union_mset atms_of_ms_union set_mset_union by auto have ‹distinct_mset (mset (get_clauses_wl S ∝ C))› using Sx xxa dist C by (auto simp: cdcl_W_restart_mset.distinct_cdcl_W_state_def ran_m_def conj_disj_distribR image_Un Collect_disj_eq Collect_conv_if split: if_splits dest!: multi_member_split) moreover have ‹literals_are_in_ℒ_i_n (all_init_atms_st S) (mset (get_clauses_wl S ∝ C))› using C Sx xxa unfolding H literals_are_in_ℒ_i_n_def ℒ_a_l_l_cong[OF H] by (auto simp:all_atms_st_def ran_m_def in_ℒ_a_l_l_atm_of_𝒜_i_n all_lits_of_mm_add_mset all_lits_def all_atms_def all_init_lits_def dest!: multi_member_split simp del: all_atms_def[symmetric]) moreover have ‹¬tautology (mset (get_clauses_wl S ∝ C))› using list C Sx unfolding twl_list_invs_def by auto ultimately show ‹length (get_clauses_wl S ∝ C) ≤ Suc (unat32_max div 2)› if ‹isasat_input_bounded (all_init_atms_st S)› using simple_clss_size_upper_div2[OF that, of ‹mset (get_clauses_wl S ∝ C)›] by auto qed lemma isa_simplify_clause_with_unit2_isa_simplify_clause_with_unit: assumes ‹valid_arena arena N vdom› and trail: ‹(M, M') ∈ trail_pol 𝒜› and lits: ‹literals_are_in_ℒ_i_n_mm 𝒜 (mset `# ran_mf N)› and C: ‹(C,C')∈Id› and le: ‹length (N ∝ C) ≤ Suc (unat32_max div 2)› shows ‹isa_simplify_clause_with_unit2 C M arena ≤ ⇓ (bool_rel ×_r {(arena', N). valid_arena arena' N vdom ∧ length arena' = length arena} ×_r Id ×_r bool_rel ×_r nat_rel) (simplify_clause_with_unit2 C' M' N)› proof - have C: ‹C'=C› using C by auto have [refine0]: ‹C ∈# dom_m N ⟹ ((0, 0, arena, False), 0, 0, N, {#}, False) ∈ {((i, j, N, is_true), (i', j', N', del', is_true')). ((i, j, N, is_true), (i', j', N', is_true')) ∈ nat_rel ×_r nat_rel ×_r {(arena', N). valid_arena arena' N vdom ∧ length arena' = length arena ∧ C ∈# dom_m N} ×_r bool_rel}› using assms by auto show ?thesis supply [[goals_limit=1]] unfolding isa_simplify_clause_with_unit2_def simplify_clause_with_unit2_alt_def mop_polarity_pol_def nres_monad3 C apply (refine_rcg mop_arena_lit[where vdom=vdom] polarity_pol_pre[OF trail] polarity_pol_polarity[of 𝒜, unfolded option_rel_id_simp, THEN fref_to_Down_unRET_uncurry] mop_arena_shorten_spec[where vdom=vdom] mop_arena_length[THEN fref_to_Down_curry, of N C _ _ vdom, unfolded normalize_down_return_spec] ) subgoal using assms by (auto simp add: arena_lifting) subgoal using assms by (auto simp add: arena_lifting) subgoal using assms by (auto simp add: arena_lifting arena_length_le_length_arena) subgoal using le by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal using lits by (auto simp: all_lits_of_mm_def ran_m_def dest!: multi_member_split dest!: literals_are_in_ℒ_i_n_mm_add_msetD) subgoal using lits by (auto simp: all_lits_of_mm_def ran_m_def dest!: multi_member_split dest!: literals_are_in_ℒ_i_n_mm_add_msetD) subgoal using assms by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto apply (rule_tac mop_arena_update_lit_spec[where vdom=vdom]) subgoal by auto subgoal by (auto simp: arena_lifting) subgoal by (auto simp: arena_lifting) subgoal by (auto simp: arena_lifting) subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal for _ x x' x1 x2 x1a x2a x1b x2b x1c x2c x1d x2d x1e x2e x1f x2f using arena_lifting(4,19)[of x1f x1b vdom C] by auto subgoal by auto subgoal by (auto simp: mark_garbage_pre_def arena_is_valid_clause_idx_def) subgoal by (auto intro!: valid_arena_extra_information_mark_to_delete') subgoal by auto subgoal by (auto simp: arena_lifting) subgoal by auto subgoal by (auto simp: arena_lifting) subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto done qed lemma literals_are_in_mm_clauses: ‹literals_are_in_ℒ_i_n_mm (all_atms_st T) (mset `# ran_mf (get_clauses_wl T))› unfolding all_atms_st_def all_atms_def all_lits_def by (auto simp: all_lits_of_mm_union literals_are_in_ℒ_i_n_mm_def in_ℒ_a_l_l_atm_of_𝒜_i_n) (* TODO Move to IsaSAT_Arena *) lemma mop_arena_status: assumes ‹C ∈# dom_m N› and ‹(C,C')∈nat_rel› ‹valid_arena arena N vdom› shows ‹mop_arena_status arena C ≤ SPEC (λc. (c, irred N C') ∈ {(a,b). (a = IRRED ⟷ b) ∧ (a = LEARNED ⟷ ¬b) ∧ (irred N C' = b)})› using assms unfolding mop_arena_status_def by (auto intro!: ASSERT_leI simp: arena_is_valid_clause_vdom_def arena_lifting) lemma twl_st_heur_restart_alt_def[unfolded Let_def]: ‹twl_st_heur_restart = {(S, T). let M' = get_trail_wl_heur S; N' = get_clauses_wl_heur S; D' = get_conflict_wl_heur S; W' = get_watched_wl_heur S; j = literals_to_update_wl_heur S; outl = get_outlearned_heur S; cach = get_conflict_cach S; clvls = get_count_max_lvls_heur S; vm = get_vmtf_heur S; vdom = get_aivdom S; heur = get_heur S; old_arena = get_old_arena S; lcount = get_learned_count S; occs = get_occs S in let M = get_trail_wl T; N = get_clauses_wl T; D = get_conflict_wl T; Q = literals_to_update_wl T; W = get_watched_wl T; N0 = get_init_clauses0_wl T; U0 = get_learned_clauses0_wl T; NS = get_subsumed_init_clauses_wl T; US = get_subsumed_learned_clauses_wl T; NEk = get_kept_unit_init_clss_wl T; UEk = get_kept_unit_learned_clss_wl T; NE = get_unkept_unit_init_clss_wl T; UE = get_unkept_unit_learned_clss_wl T in let 𝒜 = all_init_atms_st (M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, Q, W) in (M', M) ∈ trail_pol 𝒜 ∧ valid_arena N' N (set (get_vdom_aivdom vdom)) ∧ (D', D) ∈ option_lookup_clause_rel 𝒜 ∧ (D = None ⟶ j ≤ length M) ∧ Q = uminus `# lit_of `# mset (drop j (rev M)) ∧ (W', W) ∈ ⟨Id⟩map_fun_rel (D₀ 𝒜 ) ∧ vm ∈ bump_heur 𝒜 M ∧ no_dup M ∧ clvls ∈ counts_maximum_level M D ∧ cach_refinement_empty 𝒜 cach ∧ out_learned M D outl ∧ clss_size_corr_restart N NE {#} NEk UEk NS {#} N0 {#} lcount ∧ vdom_m 𝒜 W N ⊆ set (get_vdom_aivdom vdom) ∧ aivdom_inv_dec vdom (dom_m N) ∧ isasat_input_bounded 𝒜 ∧ isasat_input_nempty 𝒜 ∧ old_arena = [] ∧ heuristic_rel 𝒜 heur ∧ (occs, empty_occs_list 𝒜) ∈ occurrence_list_ref }› unfolding twl_st_heur_restart_def all_init_atms_st_def Let_def by auto (*TODO Move*) lemma literals_are_in_ℒ_i_n_mm_cong: ‹set_mset A = set_mset B ⟹ literals_are_in_ℒ_i_n_mm A = literals_are_in_ℒ_i_n_mm B› unfolding literals_are_in_ℒ_i_n_mm_def ℒ_a_l_l_cong by force lemma aivdom_inv_mono: ‹B ⊆# A ⟹ aivdom_inv (v, x1y, x2aa, tvdom) A ⟹ aivdom_inv (v, x1y, x2aa, tvdom) B› using distinct_mset_mono[of B A] by (auto simp: aivdom_inv_alt_def) lemma aivdom_inv_dec_mono: ‹B ⊆# A ⟹ aivdom_inv_dec vdom A ⟹ aivdom_inv_dec vdom B› using aivdom_inv_mono[of B A ‹get_vdom_aivdom vdom› ‹get_avdom_aivdom vdom› ‹get_ivdom_aivdom vdom› ‹get_tvdom_aivdom vdom›] by (cases vdom) (auto simp: aivdom_inv_dec_def) lemma simplify_clause_with_unit_st2_alt_def: ‹simplify_clause_with_unit_st2 = (λC (M, N₀, D, NE, UE, NEk, UEk, NS, US, N0, U0, Q, W). do { ASSERT(simplify_clause_with_unit_st_wl_pre C (M, N₀, D, NE, UE, NEk, UEk, NS, US, N0, U0, Q, W)); ASSERT (C ∈# dom_m N₀ ∧ count_decided M = 0 ∧ D = None); let S = (M, N₀, D, NE, UE, NEk, UEk, NS, US, N0, U0, Q, W); let E = mset (N₀ ∝ C); let irr = irred N₀ C; (unc, N, L, b, i) ← simplify_clause_with_unit2 C M N₀; ASSERT(dom_m N ⊆# dom_m N₀); if unc then do { ASSERT(N = N₀); let T = (M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, Q, W); RETURN T } else if b then do { let T = (M, N, D, (if irr then add_mset E else id) NE, (if ¬irr then add_mset E else id) UE, NEk, UEk, NS, US, N0, U0, Q, W); ASSERT (set_mset (all_learned_lits_of_wl T) = set_mset (all_learned_lits_of_wl S)); ASSERT (set_mset (all_init_lits_of_wl T) = set_mset (all_init_lits_of_wl S)); ASSERT (set_mset (all_atms_st T) = set_mset (all_atms_st S)); ASSERT (size (learned_clss_lf N) = size (learned_clss_lf N₀) - (if irr then 0 else 1)); ASSERT(¬irr ⟶ size (learned_clss_lf N₀) ≥ 1); RETURN T } else if i = 1 then do { ASSERT (undefined_lit M L ∧ L ∈# ℒ_a_l_l (all_atms_st S)); M ← cons_trail_propagate_l L 0 M; let T = (M, N, D, NE, UE, (if irr then add_mset {#L#} else id) NEk, (if ¬irr then add_mset {#L#} else id)UEk, (if irr then add_mset E else id) NS, (if ¬irr then add_mset E else id)US, N0, U0, add_mset (-L) Q, W); ASSERT (set_mset (all_learned_lits_of_wl T) = set_mset (all_learned_lits_of_wl S)); ASSERT (set_mset (all_init_lits_of_wl T) = set_mset (all_init_lits_of_wl S)); ASSERT (set_mset (all_atms_st T) = set_mset (all_atms_st S)); ASSERT (size (learned_clss_lf N) = size (learned_clss_lf N₀) - (if irr then 0 else 1)); ASSERT(¬irr ⟶ size (learned_clss_lf N₀) ≥ 1); RETURN T } else if i = 0 then do { let j = length M; let T = (M, N, Some {#}, NE, UE, NEk, UEk, (if irr then add_mset E else id) NS, (if ¬irr then add_mset E else id) US, (if irr then add_mset {#} else id) N0, (if ¬irr then add_mset {#} else id)U0, {#}, W); ASSERT (set_mset (all_learned_lits_of_wl T) = set_mset (all_learned_lits_of_wl S)); ASSERT (set_mset (all_init_lits_of_wl T) = set_mset (all_init_lits_of_wl S)); ASSERT (set_mset (all_atms_st T) = set_mset (all_atms_st S)); ASSERT (size (learned_clss_lf N) = size (learned_clss_lf N₀) - (if irr then 0 else 1)); ASSERT(¬irr ⟶ size (learned_clss_lf N₀) ≥ 1); RETURN T } else do { let T = (M, N, D, NE, UE, NEk, UEk, (if irr then add_mset E else id) NS, (if ¬irr then add_mset E else id) US, N0, U0, Q, W); ASSERT (set_mset (all_learned_lits_of_wl T) = set_mset (all_learned_lits_of_wl S)); ASSERT (set_mset (all_init_lits_of_wl T) = set_mset (all_init_lits_of_wl S)); ASSERT (set_mset (all_atms_st T) = set_mset (all_atms_st S)); ASSERT (size (learned_clss_lf N) = size (learned_clss_lf N₀)); ASSERT (C ∈# dom_m N); let _ = log_clause T C; RETURN T } })› by (auto simp: simplify_clause_with_unit_st2_def log_clause_def intro!: ext Let_def cong: if_cong) lemma isa_simplify_clause_with_unit_st2_simplify_clause_with_unit_st2: assumes ‹(S, S') ∈ {(a,b). (a,b) ∈ twl_st_heur_restart ∧ get_avdom a = u∧ get_vdom a = v∧ get_ivdom a = x ∧length (get_clauses_wl_heur a) = r ∧ learned_clss_count a ≤ w ∧ get_vmtf_heur a = vm ∧ length (get_watched_wl_heur a) = lw}› ‹(C,C')∈ nat_rel› shows ‹isa_simplify_clause_with_unit_st2 C S ≤ ⇓{(a,b). (a,b) ∈ twl_st_heur_restart ∧ get_avdom a = u∧ get_vdom a = v∧ get_ivdom a = x ∧ length (get_clauses_wl_heur a) = r∧ learned_clss_count a ≤ w ∧ get_vmtf_heur a = vm ∧ learned_clss_count a ≤ learned_clss_count S ∧ length (get_watched_wl_heur a) = lw} (simplify_clause_with_unit_st2 C' S')› (is ‹_ ≤ ⇓?A _›) proof - have H: ‹A = B ⟹ x ∈ A ⟹ x ∈ B› for A B x by auto have H': ‹A = B ⟹ A x ⟹ B x› for A B x by auto have H'': ‹A = B ⟹ A ⊆ c ⟹ B ⊆ c› for A B c by auto have vdom_m_cong2: ‹set_mset 𝒜 = set_mset ℬ ⟹ vdom_m 𝒜 W N ⊆ vd ⟹ dom_m N' ⊆# dom_m N ⟹ vdom_m ℬ W N' ⊆ vd› for 𝒜 W N N' vd ℬ by (subst vdom_m_cong[of ℬ 𝒜]) (auto simp: vdom_m_def) note cong = trail_pol_cong heuristic_rel_cong option_lookup_clause_rel_cong isa_vmtf_cong vdom_m_cong[THEN H] isasat_input_nempty_cong[THEN iffD1] isasat_input_bounded_cong[THEN iffD1] cach_refinement_empty_cong[THEN H'] phase_saving_cong[THEN H'] ℒ_a_l_l_cong[THEN H] D₀_cong[THEN H] D₀_cong[OF sym] vdom_m_cong[THEN H''] vdom_m_cong2 empty_occs_list_cong have set_conflict_to_false: ‹(a, None) ∈ option_lookup_clause_rel 𝒜 ⟹ (set_conflict_to_false a, Some {#}) ∈ option_lookup_clause_rel 𝒜› for a 𝒜 by (auto simp: option_lookup_clause_rel_def set_conflict_to_false_def lookup_clause_rel_def) have outl: ‹out_learned x1 None x1s ⟹ out_learned x1 (Some {#}) (x1s)› ‹0 ∈ counts_maximum_level x1 (Some {#})› for x1 x1s by (cases x1s, auto simp: out_learned_def counts_maximum_level_def) have all_init_lits_of_wl: ‹set_mset (all_init_lits_of_wl a) = set_mset (all_init_lits_of_wl b) ⟷ set_mset (all_init_atms_st a) = set_mset (all_init_atms_st b)› for a b by (metis ℒ_a_l_l_all_init_atms(2) ℒ_a_l_l_cong atms_of_ℒ_a_l_l_𝒜_i_n atms_of_cong_set_mset) have log_clause[refine0]: ‹y' ∈# dom_m (get_clauses_wl x') ⟹ (x, x')∈ ?A ⟹ (y,y')∈ nat_rel ⟹ log_new_clause_heur x y ≤ SPEC(λc. (c, log_clause x' y') ∈ unit_rel)› for x x' y y' unfolding log_new_clause_heur_alt_def apply (rule log_clause_heur_log_clause2_ana[THEN order_trans]) apply (auto simp add: twl_st_heur_restart_ana_def) by (rule log_clause2_log_clause[THEN fref_to_Down_curry, unfolded prod.simps, THEN order_trans]) auto note accessors_def = get_trail_wl.simps get_clauses_wl.simps get_conflict_wl.simps literals_to_update_wl.simps get_watched_wl.simps get_init_clauses0_wl.simps get_learned_clauses0_wl.simps get_subsumed_init_clauses_wl.simps get_subsumed_learned_clauses_wl.simps get_kept_unit_init_clss_wl.simps get_kept_unit_learned_clss_wl.simps isasat_state_simp get_unkept_unit_init_clss_wl.simps get_unkept_unit_learned_clss_wl.simps show ?thesis supply [[goals_limit=1]] using assms unfolding isa_simplify_clause_with_unit_st2_def simplify_clause_with_unit_st2_alt_def Let_def[of "(_,_)"] Let_def[of ‹mset _›] all_init_lits_of_wl apply (rewrite at ‹let _ = set_clauses_wl_heur _ _ in _› Let_def) apply (refine_rcg isa_simplify_clause_with_unit2_isa_simplify_clause_with_unit[where vdom=‹set (get_vdom S)› and 𝒜 = ‹all_init_atms_st S'›] mop_arena_status[where vdom = ‹set (get_vdom S)›] cons_trail_Propagated_tr2[where 𝒜 = ‹all_init_atms_st S'›] mop_isa_length_trail_length_u[of ‹all_init_atms_st (S')›, THEN fref_to_Down_Id_keep, unfolded length_uint32_nat_def comp_def]) subgoal by auto subgoal by (auto simp: twl_st_heur_restart_def) subgoal by (auto simp: twl_st_heur_restart_def clss_size_corr_def ran_m_def clss_size_def dest!: multi_member_split clss_size_corr_restart_rew) subgoal by (auto simp: twl_st_heur_restart_def) subgoal by (auto simp: twl_st_heur_restart_def all_init_atms_st_def) subgoal using literals_are_in_mm_clauses[of S'] simplify_clause_with_unit_st_wl_pre_all_init_atms_all_atms[of C' S', THEN literals_are_in_ℒ_i_n_mm_cong] by (auto simp: twl_st_heur_restart_def) subgoal by (drule simplify_clause_with_unit_st_wl_preD(2)[of C']) (auto dest!: simp: twl_st_heur_restart_def all_init_atms_st_def simp del: isasat_input_bounded_def) subgoal by auto subgoal by (auto simp: twl_st_heur_restart_def learned_clss_count_def) subgoal by (auto simp: twl_st_heur_restart_def) subgoal by (auto simp: twl_st_heur_restart_def) subgoal for x1 x2 x1a x2a x1b x2b x1c x2c x1d x2d x1e x2e x1f x2f x1g x2g x1h x2h x1i x2i x1j x2j x1k x2k x1l x2l x1m x2m x1n x2n x1o x2o x1p x2p x1q x2q x1r x2r x1s x2s x1t x2t x1u by (clarsimp simp only: twl_st_heur_restart_alt_def in_pair_collect_simp prod.simps prod_rel_iff TrueI refl cong[of ‹all_init_atms_st (x1, x1a, None, x1c, x1d, x1e, x1f, x1g, x1h, x1i, x1j, uminus `# lit_of `# mset (drop (literals_to_update_wl_heur S) (rev x1)), x2k)› ‹all_init_atms_st (_, _, _, (If _ _ _) _, _)›] clss_size_corr_restart_def isasat_state_simp clss_size_def clss_size_incr_lcountUE_def learned_clss_count_def aivdom_inv_dec_mono empty_occs_list_cong[of ‹all_init_atms_st (_, _, _, (If _ _ _) _, _)›] clss_size_decr_lcount_def accessors_def) (auto split: if_splits intro: aivdom_inv_dec_mono simp: clss_size_decr_lcount_def clss_size_lcount_def clss_size_lcountUS_def clss_size_lcountU0_def clss_size_lcountUE_def clss_size_lcountUEk_def) subgoal by simp subgoal by (auto simp: twl_st_heur_restart_def all_init_atms_st_def) subgoal using simplify_clause_with_unit_st_wl_pre_all_init_atms_all_atms[of C' S', THEN ℒ_a_l_l_cong] by auto subgoal by (auto simp: DECISION_REASON_def) subgoal for x1 x2 x1a x2a x1b x2b x1c x2c x1d x2d x1e x2e x1f x2f x1g x2g x1h x2h x1i x2i x1j x2j x1k x2k x1l x2l x1m x2m x1n x2n x1o x2o x1p x2p x1q x2q x1r x2r x1s x2s x1t x2t x1u x2u x1v by (clarsimp simp only: twl_st_heur_restart_alt_def in_pair_collect_simp prod.simps prod_rel_iff TrueI refl accessors_def cong[of ‹all_init_atms_st (x1, x1a, None, x1c, x1d, x1e, x1f, x1g, x1h, x1i, x1j, uminus `# lit_of `# mset (drop (literals_to_update_wl_heur S) (rev x1)), x2k)› ‹all_init_atms_st (_, _, _, _, _, (If _ _ _) _, _)›] isa_vmtf_consD clss_size_corr_restart_def clss_size_def clss_size_incr_lcountUEk_def learned_clss_count_def aivdom_inv_dec_mono empty_occs_list_cong[of ‹all_init_atms_st (_, _, _, _, _, (If _ _ _) _, _)›] clss_size_decr_lcount_def) (auto split: if_splits intro: aivdom_inv_dec_mono simp: clss_size_decr_lcount_def clss_size_lcount_def clss_size_lcountUS_def clss_size_lcountU0_def clss_size_lcountUE_def clss_size_lcountUEk_def) subgoal by simp subgoal by simp subgoal by (auto simp add: twl_st_heur_restart_def all_init_atms_st_def) subgoal for x1 x2 x1a x2a x1b x2b x1c x2c x1d x2d x1e x2e x1f x2f x1g x2g x1h x2h x1i x2i x1j x2j x1k x2k x1l x2l x1m x2m x1n x2n x1o x2o x1p x2p x1q x2q x1r x2r x1s x2s x1t x2t x1u x2u by (clarsimp simp only: twl_st_heur_restart_alt_def in_pair_collect_simp prod.simps isasat_state_simp prod_rel_iff TrueI refl accessors_def cong[of ‹all_init_atms_st (x1, x1a, None, x1c, x1d, x1e, x1f, x1g, x1h, x1i, x1j, uminus `# lit_of `# mset (drop (literals_to_update_wl_heur S) (rev x1)), x2k)› ‹all_init_atms_st (_, _, _, _, _, _, _, (If _ _ _) _, _)›] isa_vmtf_consD clss_size_def clss_size_incr_lcountUE_def clss_size_incr_lcountUS_def clss_size_incr_lcountU0_def clss_size_decr_lcount_def clss_size_corr_restart_def empty_occs_list_cong[of ‹all_init_atms_st (_, _, _, _, _, _, _, (If _ _ _) _, _)›] option_lookup_clause_rel_cong[of ‹all_init_atms_st (x1, x1a, None, x1c, x1d, x1e, x1f, x1g, x1h, x1i, x1j, uminus `# lit_of `# mset (drop (literals_to_update_wl_heur S) (rev x1)), x2k)› ‹all_init_atms_st (_, _, _, _, _, _, _, (If _ _ _) _, _)›, OF sym] outl set_conflict_to_false aivdom_inv_dec_mono clss_size_def clss_size_incr_lcountUE_def learned_clss_count_def clss_size_decr_lcount_def) (auto split: if_splits simp: clss_size_decr_lcount_def clss_size_lcount_def clss_size_lcountUS_def clss_size_lcountU0_def clss_size_lcountUE_def clss_size_lcountUEk_def) subgoal by simp subgoal state_conv for x1 x2 x1a x2a x1b x2b x1c x2c x1d x2d x1e x2e x1f x2f x1g x2g x1h x2h x1i x2i x1j x2j x1k x2k x1l x2l x1m x2m x1n x2n x1o x2o x1p x2p x1q x2q x1r x2r x1s x2s x1t x2t x1u apply (clarsimp simp only: twl_st_heur_restart_alt_def in_pair_collect_simp prod.simps prod_rel_iff TrueI refl accessors_def isasat_state_simp empty_occs_list_cong[of ‹all_init_atms_st (_, _, _, _, _, _, _,(If _ _ _) _, _)›] cong[of ‹all_init_atms_st (x1, x1a, None, x1c, x1d, x1e, x1f, x1g, x1h, x1i, x1j, uminus `# lit_of `# mset (drop (literals_to_update_wl_heur S) (rev x1)), x2k)› ‹all_init_atms_st (_, _, _, _, _, _, _, (If _ _ _) _, _)›] isa_vmtf_consD clss_size_def clss_size_incr_lcountUE_def clss_size_incr_lcountUS_def clss_size_incr_lcountU0_def aivdom_inv_dec_mono clss_size_decr_lcount_def clss_size_corr_restart_def option_lookup_clause_rel_cong[of ‹all_init_atms_st (x1, x1a, None, x1c, x1d, x1e, x1f, x1g, x1h, x1i, x1j, uminus `# lit_of `# mset (drop (literals_to_update_wl_heur S) (rev x1)), x2k)› ‹all_init_atms_st (_, _, _, _, _, _, _, (If _ _ _) _, _)›, OF sym] outl set_conflict_to_false) apply (auto split: if_splits) done subgoal premises p by (rule state_conv[OF p(1-43)]) done qed lemma learned_clss_count_reset_units_since_last_GC_st[simp]: ‹learned_clss_count (reset_units_since_last_GC_st T) = learned_clss_count T› ‹(reset_units_since_last_GC_st T, Ta) ∈ twl_st_heur_restart ⟷ (T, Ta) ∈ twl_st_heur_restart› ‹get_clauses_wl_heur (reset_units_since_last_GC_st T) = get_clauses_wl_heur T› by (cases Ta; auto simp: reset_units_since_last_GC_st_def twl_st_heur_restart_def; fail)+ lemma isa_simplify_clauses_with_unit_st2_simplify_clauses_with_unit_st2: assumes ‹(S, S') ∈ twl_st_heur_restart_ana' r u› shows ‹isa_simplify_clauses_with_unit_st2 S ≤ ⇓(twl_st_heur_restart_ana' r u) (simplify_clauses_with_unit_st2 S')› proof - have isa_simplify_clauses_with_unit_st2_def: ‹isa_simplify_clauses_with_unit_st2 S = do { xs ← RETURN (get_avdom S @ get_ivdom S); ASSERT(length xs ≤ length (get_vdom S) ∧ length (get_vdom S) ≤ length (get_clauses_wl_heur S)); T ← do { (_, T) ← WHILE_T (λ(i, T). i < length xs ∧ get_conflict_wl_is_None_heur T) (λ(i,T). do { (T) ← do { ASSERT((i < length (get_avdom T) ⟶ access_avdom_at_pre T i) ∧ (i ≥ length (get_avdom T) ⟶ access_ivdom_at_pre T (i - length_avdom S)) ∧ length_avdom T = length_avdom S ∧ length (get_clauses_wl_heur T) = length (get_clauses_wl_heur S) ∧ learned_clss_count T ≤ learned_clss_count S); C ← RETURN (if i < length (get_avdom S) then access_avdom_at T i else access_ivdom_at T (i - length_avdom S)); E ← mop_arena_status (get_clauses_wl_heur T) C; if E ≠ DELETED then do { isa_simplify_clause_with_unit_st2 C T } else RETURN (T) }; ASSERT(i < length xs); RETURN (i+1, T)}) (0, S); RETURN T }; RETURN (reset_units_since_last_GC_st T) }› unfolding isa_simplify_clauses_with_unit_st2_def Let_def by (auto simp: intro!: bind_cong[OF refl] cong: if_cong) have simplify_clauses_with_unit_st2_def: ‹simplify_clauses_with_unit_st2 S = do { ASSERT (simplify_clauses_with_unit_st_wl_pre S); xs ← SPEC(λxs. finite xs); T ← FOREACHci(λit T. simplify_clauses_with_unit_st_wl_inv S it T) (xs) (λS. get_conflict_wl S = None) (λi S. let _ =i; b = i ∈# dom_m (get_clauses_wl S) in if b then simplify_clause_with_unit_st2 i S else RETURN S) S; ASSERT(set_mset (all_learned_lits_of_wl T) ⊆ set_mset (all_learned_lits_of_wl S)); ASSERT(set_mset (all_init_lits_of_wl T) = set_mset (all_init_lits_of_wl S)); RETURN T }› for S unfolding simplify_clauses_with_unit_st2_def by (auto simp: Let_def) have dist_vdom: ‹distinct (get_vdom S)› and valid: ‹valid_arena (get_clauses_wl_heur S) (get_clauses_wl S') (set (get_vdom S))› using assms by (auto simp: twl_st_heur_restart_def twl_st_heur_restart_ana_def aivdom_inv_dec_alt_def) have vdom_incl: ‹set (get_vdom S) ⊆ {MIN_HEADER_SIZE..< length (get_clauses_wl_heur S)}› using valid_arena_in_vdom_le_arena[OF valid] arena_dom_status_iff[OF valid] by auto have le_vdom_arena: ‹length (get_vdom S) ≤ length (get_clauses_wl_heur S)› by (subst distinct_card[OF dist_vdom, symmetric]) (use card_mono[OF _ vdom_incl] in auto) have [refine]: ‹RETURN (get_avdom S@ get_ivdom S) ≤ ⇓ {(xs, a). a = set xs ∧ distinct xs ∧ set xs ⊆ set (get_vdom S) ∧ xs = get_avdom S@ get_ivdom S} (SPEC (λxs. finite xs))› (is ‹_ ≤ ⇓?A _›) using assms distinct_mset_mono[of ‹mset (get_avdom S)› ‹mset (get_vdom S)›] distinct_mset_mono[of ‹mset (get_ivdom S)› ‹mset (get_vdom S)›] apply - by (rule RETURN_RES_refine) (auto intro!: simp: twl_st_heur_restart_def twl_st_heur_restart_ana_def aivdom_inv_dec_alt_def) let ?R = ‹{(a, b). (a, b) ∈ twl_st_heur_restart ∧ get_avdom a = get_avdom S ∧ get_vdom a = get_vdom S∧ get_ivdom a = get_ivdom S ∧ length (get_clauses_wl_heur a) = r ∧ learned_clss_count a ≤ u ∧ learned_clss_count a ≤ learned_clss_count S}› have [refine]: ‹(xs, xsa) ∈ ?A ⟹ xsa ∈ {xs:: nat set. finite xs} ⟹ ([0..<length xs], xsa) ∈ ⟨{(i, a). xs ! i =a ∧ i < length xs}⟩list_set_rel› (is ‹_ ⟹ _ ⟹ _ ∈ ⟨?B⟩list_set_rel›) for xs xsa by (auto simp: list_set_rel_def br_def intro!: relcompI[of _ xs]) (auto simp: list_rel_def intro!: list_all2_all_nthI) have H: ‹(xi, x) ∈ ?B xs ⟹ (xi, x) ∈ {(i, a). xs ! i = a}› for xi x xs by auto have H2: ‹(si, s) ∈ ?R ⟹ valid_arena (get_clauses_wl_heur si) (get_clauses_wl s) (set (get_vdom S))› for si s by (auto simp: twl_st_heur_restart_def) have H3: ‹(if xi < length (get_avdom S) then access_avdom_at si xi else access_ivdom_at si (xi - length_avdom S), x) ∈ {(C,C'). (C,C')∈ nat_rel ∧ C ∈ set (get_vdom S)}› (is ‹_ ∈ ?access›) if ‹(xs, xsa) ∈ {(xs, a). a = set xs ∧ distinct xs ∧ set xs ⊆ set (get_vdom S) ∧ xs = get_avdom S @ get_ivdom S}› and ‹(xi, x) ∈ {(i, a). xs ! i = a ∧ i < length xs}› and ‹(si, s) ∈ ?R› for xs xsa x xi s si using that by (auto simp: access_ivdom_at_def access_avdom_at_def nth_append length_avdom_def) have H5: ‹(s,si)∈ ?R ⟹ (xi, x) ∈ ?B xs ⟹ (xs, xsa) ∈ ?A ⟹ (C,C') ∈ ?access ⟹ (xa, C ∈# dom_m (get_clauses_wl si)) ∈ {(a, b). (b ⟶ (a = IRRED) = irred (get_clauses_wl si) (C) ∧ (a = LEARNED) = (¬ irred (get_clauses_wl si) C)) ∧ (a = DELETED) = (¬ b)} ⟹ (xa, C' ∈# dom_m (get_clauses_wl si)) ∈ {(a, b). (b ⟶ (a = IRRED) = irred (get_clauses_wl si) C' ∧ (a = LEARNED) = (¬ irred (get_clauses_wl si) C')) ∧ (a = DELETED) = (¬ b)}› for xi xs x s xa si xsa C C' by (auto simp: access_avdom_at_def) have H4: ‹(C,C')∈?access ⟹ (C,C')∈ nat_rel› for C C' by auto show ?thesis unfolding isa_simplify_clauses_with_unit_st2_def simplify_clauses_with_unit_st2_def nfoldli_upt_by_while[symmetric] unfolding nres_monad3 apply (refine_vcg LFOci_refine[where R= ?R] mop_arena_status2[where vdom = ‹set (get_vdom S)›]) subgoal using assms by (auto simp: twl_st_heur_restart_ana_def twl_st_heur_restart_def card_Un_Int aivdom_inv_dec_alt_def simp flip: distinct_card intro!: card_mono) subgoal using le_vdom_arena by auto subgoal by (subst get_conflict_wl_is_None_heur_get_conflict_wl_is_None_restart[THEN fref_to_Down_unRET_Id]) (auto simp: get_conflict_wl_is_None_def) subgoal by (auto simp: access_avdom_at_pre_def) subgoal by (auto simp: access_ivdom_at_pre_def length_avdom_def less_diff_conv2) subgoal by (auto simp: length_avdom_def) subgoal using assms by (auto simp: twl_st_heur_restart_ana_def) subgoal by auto apply (rule H3; assumption) apply (rule H4; assumption) subgoal by auto apply (rule H2; assumption) apply (rule H5; assumption) subgoal by auto apply (rule isa_simplify_clause_with_unit_st2_simplify_clause_with_unit_st2[where u = ‹(get_avdom S)› and v = ‹(get_vdom S)› and x = ‹(get_ivdom S)› and r=r, THEN order_trans]; assumption?) apply (auto; fail)[] apply (auto; fail)[] subgoal by (clarsimp intro!: conc_fun_R_mono) subgoal using assms by (auto simp: twl_st_heur_restart_ana_def) subgoal by (auto simp: twl_st_heur_restart_ana_def reset_units_since_last_GC_def) done qed lemma simplify_clauses_with_units_st_wl2_simplify_clauses_with_units_st_wl: ‹(S, S') ∈ Id ⟹ simplify_clauses_with_units_st_wl2 S ≤ ⇓Id (simplify_clauses_with_units_st_wl S)› unfolding simplify_clauses_with_units_st_wl2_def simplify_clauses_with_units_st_wl_def by (refine_vcg simplify_clauses_with_unit_st2_simplify_clauses_with_unit_st) auto lemma isa_simplify_clauses_with_units_st2_simplify_clauses_with_units_st2: assumes ‹(S, S') ∈ twl_st_heur_restart_ana' r u› shows ‹isa_simplify_clauses_with_units_st_wl2 S ≤ ⇓(twl_st_heur_restart_ana' r u) (simplify_clauses_with_units_st_wl2 S')› unfolding isa_simplify_clauses_with_units_st_wl2_def simplify_clauses_with_units_st_wl2_def by (refine_vcg isa_simplify_clauses_with_unit_st2_simplify_clauses_with_unit_st2) (use assms in ‹auto simp: get_conflict_wl_is_None_def get_conflict_wl_is_None_heur_get_conflict_wl_is_None_ana[THEN fref_to_Down_unRET_Id]›) end

Theory IsaSAT_Simplify_Units