Theory CDCL_W_Partial_Optimal

theory CDCL_W_Partial_Optimal_Model imports CDCL_W_Partial_Encoding begin lemma isabelle_should_do_that_automatically: ‹Suc (a - Suc 0) = a ⟷ a ≥ 1› by auto lemma (in conflict_driven_clause_learning_W_optimal_weight) conflict_opt_state_eq_compatible: ‹conflict_opt S T ⟹ S ∼ S' ⟹ T ∼ T' ⟹ conflict_opt S' T'› using state_eq_trans[of T' T ‹update_conflicting (Some (negate_ann_lits (trail S'))) S›] using state_eq_trans[of T ‹update_conflicting (Some (negate_ann_lits (trail S'))) S› ‹update_conflicting (Some (negate_ann_lits (trail S'))) S'›] update_conflicting_state_eq[of S S' ‹Some {#}›] apply (auto simp: conflict_opt.simps state_eq_sym) using reduce_trail_to_state_eq state_eq_trans update_conflicting_state_eq by blast context optimal_encoding begin definition base_atm :: ‹'v ⇒ 'v› where ‹base_atm L = (if L ∈ Σ - ΔΣ then L else if L ∈ replacement_neg ` ΔΣ then (SOME K. (K ∈ ΔΣ ∧ L = replacement_neg K)) else (SOME K. (K ∈ ΔΣ ∧ L = replacement_pos K)))› lemma normalize_lit_Some_simp[simp]: ‹(SOME K. K ∈ ΔΣ ∧ (L^↦⁰ = K^↦⁰)) = L› if ‹L ∈ ΔΣ› for K by (rule some1_equality) (use that in auto) lemma base_atm_simps1[simp]: ‹L ∈ Σ ⟹ L ∉ ΔΣ ⟹ base_atm L = L› by (auto simp: base_atm_def) lemma base_atm_simps2[simp]: ‹L ∈ (Σ - ΔΣ) ∪ replacement_neg ` ΔΣ ∪ replacement_pos ` ΔΣ ⟹ K ∈ Σ ⟹ K ∉ ΔΣ ⟹ L ∈ Σ ⟹ K = base_atm L ⟷ L = K› by (auto simp: base_atm_def) lemma base_atm_simps3[simp]: ‹L ∈ Σ - ΔΣ ⟹ base_atm L ∈ Σ› ‹L ∈ replacement_neg ` ΔΣ ∪ replacement_pos ` ΔΣ ⟹ base_atm L ∈ ΔΣ› apply (auto simp: base_atm_def) by (metis (mono_tags, lifting) tfl_some) lemma base_atm_simps4[simp]: ‹L ∈ ΔΣ ⟹ base_atm (replacement_pos L) = L› ‹L ∈ ΔΣ ⟹ base_atm (replacement_neg L) = L› by (auto simp: base_atm_def) fun normalize_lit :: ‹'v literal ⇒ 'v literal› where ‹normalize_lit (Pos L) = (if L ∈ replacement_neg ` ΔΣ then Neg (replacement_pos (SOME K. (K ∈ ΔΣ ∧ L = replacement_neg K))) else Pos L)› | ‹normalize_lit (Neg L) = (if L ∈ replacement_neg ` ΔΣ then Pos (replacement_pos (SOME K. K ∈ ΔΣ ∧ L = replacement_neg K)) else Neg L)› abbreviation normalize_clause :: ‹'v clause ⇒ 'v clause› where ‹normalize_clause C ≡ normalize_lit `# C› lemma normalize_lit[simp]: ‹L ∈ Σ - ΔΣ ⟹ normalize_lit (Pos L) = (Pos L)› ‹L ∈ Σ - ΔΣ ⟹ normalize_lit (Neg L) = (Neg L)› ‹L ∈ ΔΣ ⟹ normalize_lit (Pos (replacement_neg L)) = Neg (replacement_pos L)› ‹L ∈ ΔΣ ⟹ normalize_lit (Neg (replacement_neg L)) = Pos (replacement_pos L)› by auto definition all_clauses_literals :: ‹'v list› where ‹all_clauses_literals = (SOME xs. mset xs = mset_set ((Σ - ΔΣ) ∪ replacement_neg ` ΔΣ ∪ replacement_pos ` ΔΣ))› (in -) 'c search_depth = sd_is_zero: SD_ZERO (the_search_depth: 'c) | sd_is_one: SD_ONE (the_search_depth: 'c) | sd_is_two: SD_TWO (the_search_depth: 'c) abbreviation (in -) un_hide_sd :: ‹'a search_depth list ⇒ 'a list› where ‹un_hide_sd ≡ map the_search_depth› fun nat_of_search_deph :: ‹'c search_depth ⇒ nat› where ‹nat_of_search_deph (SD_ZERO _) = 0› | ‹nat_of_search_deph (SD_ONE _) = 1› | ‹nat_of_search_deph (SD_TWO _) = 2› definition opposite_var where ‹opposite_var L = (if L ∈ replacement_pos ` ΔΣ then replacement_neg (base_atm L) else replacement_pos (base_atm L))› lemma opposite_var_replacement_if[simp]: ‹L ∈ (replacement_neg ` ΔΣ ∪ replacement_pos ` ΔΣ) ⟹ A ∈ ΔΣ ⟹ opposite_var L = replacement_pos A ⟷ L = replacement_neg A› ‹L ∈ (replacement_neg ` ΔΣ ∪ replacement_pos ` ΔΣ) ⟹ A ∈ ΔΣ ⟹ opposite_var L = replacement_neg A ⟷ L = replacement_pos A› ‹A ∈ ΔΣ ⟹ opposite_var (replacement_pos A) = replacement_neg A› ‹A ∈ ΔΣ ⟹ opposite_var (replacement_neg A) = replacement_pos A› by (auto simp: opposite_var_def) context assumes [simp]: ‹finite Σ› begin lemma all_clauses_literals: ‹mset all_clauses_literals = mset_set ((Σ - ΔΣ) ∪ replacement_neg ` ΔΣ ∪ replacement_pos ` ΔΣ)› ‹distinct all_clauses_literals› ‹set all_clauses_literals = ((Σ - ΔΣ) ∪ replacement_neg ` ΔΣ ∪ replacement_pos ` ΔΣ)› proof - let ?A = ‹mset_set ((Σ - ΔΣ) ∪ replacement_neg ` ΔΣ ∪ replacement_pos ` ΔΣ)› show 1: ‹mset all_clauses_literals = ?A› using someI[of ‹λxs. mset xs = ?A›] finite_Σ ex_mset[of ?A] unfolding all_clauses_literals_def[symmetric] by metis show 2: ‹distinct all_clauses_literals› using someI[of ‹λxs. mset xs = ?A›] finite_Σ ex_mset[of ?A] unfolding all_clauses_literals_def[symmetric] by (metis distinct_mset_mset_set distinct_mset_mset_distinct) show 3: ‹set all_clauses_literals = ((Σ - ΔΣ) ∪ replacement_neg ` ΔΣ ∪ replacement_pos ` ΔΣ)› using arg_cong[OF 1, of set_mset] finite_Σ by simp qed definition unset_literals_in_Σ where ‹unset_literals_in_Σ M L ⟷ undefined_lit M (Pos L) ∧ L ∈ Σ - ΔΣ› definition full_unset_literals_in_ΔΣ where ‹full_unset_literals_in_ΔΣ M L ⟷ undefined_lit M (Pos L) ∧ L ∉ Σ - ΔΣ ∧ undefined_lit M (Pos (opposite_var L)) ∧ L ∈ replacement_pos ` ΔΣ› definition full_unset_literals_in_ΔΣ' where ‹full_unset_literals_in_ΔΣ' M L ⟷ undefined_lit M (Pos L) ∧ L ∉ Σ - ΔΣ ∧ undefined_lit M (Pos (opposite_var L)) ∧ L ∈ replacement_neg ` ΔΣ› definition half_unset_literals_in_ΔΣ where ‹half_unset_literals_in_ΔΣ M L ⟷ undefined_lit M (Pos L) ∧ L ∉ Σ - ΔΣ ∧ defined_lit M (Pos (opposite_var L))› definition sorted_unadded_literals :: ‹('v, 'v clause) ann_lits ⇒ 'v list› where ‹sorted_unadded_literals M = (let M0 = filter (full_unset_literals_in_ΔΣ' M) all_clauses_literals; ― ‹weight is 0› M1 = filter (unset_literals_in_Σ M) all_clauses_literals; ― ‹weight is 2› M2 = filter (full_unset_literals_in_ΔΣ M) all_clauses_literals; ― ‹weight is 2› M3 = filter (half_unset_literals_in_ΔΣ M) all_clauses_literals ― ‹weight is 1› in M0 @ M3 @ M1 @ M2)› definition complete_trail :: ‹('v, 'v clause) ann_lits ⇒ ('v, 'v clause) ann_lits› where ‹complete_trail M = (map (Decided o Pos) (sorted_unadded_literals M) @ M)› lemma in_sorted_unadded_literals_undefD: ‹atm_of (lit_of l) ∈ set (sorted_unadded_literals M) ⟹ l ∉ set M› ‹atm_of (l') ∈ set (sorted_unadded_literals M) ⟹ undefined_lit M l'› ‹xa ∈ set (sorted_unadded_literals M) ⟹ lit_of x = Neg xa ⟹ x ∉ set M› and set_sorted_unadded_literals[simp]: ‹set (sorted_unadded_literals M) = Set.filter (λL. undefined_lit M (Pos L)) (set all_clauses_literals)› by (auto simp: sorted_unadded_literals_def undefined_notin all_clauses_literals(1,2) defined_lit_Neg_Pos_iff half_unset_literals_in_ΔΣ_def full_unset_literals_in_ΔΣ_def unset_literals_in_Σ_def Let_def full_unset_literals_in_ΔΣ'_def all_clauses_literals(3)) lemma [simp]: ‹full_unset_literals_in_ΔΣ [] = (λL. L ∈ replacement_pos ` ΔΣ)› ‹full_unset_literals_in_ΔΣ' [] = (λL. L ∈ replacement_neg ` ΔΣ)› ‹half_unset_literals_in_ΔΣ [] = (λL. False)› ‹unset_literals_in_Σ [] = (λL. L ∈ Σ - ΔΣ)› by (auto simp: full_unset_literals_in_ΔΣ_def unset_literals_in_Σ_def full_unset_literals_in_ΔΣ'_def half_unset_literals_in_ΔΣ_def intro!: ext) lemma filter_disjount_union: ‹(⋀x. x ∈ set xs ⟹ P x ⟹ ¬Q x) ⟹ length (filter P xs) + length (filter Q xs) = length (filter (λx. P x ∨ Q x) xs)› by (induction xs) auto lemma length_sorted_unadded_literals_empty[simp]: ‹length (sorted_unadded_literals []) = length all_clauses_literals› apply (auto simp: sorted_unadded_literals_def sum_length_filter_compl Let_def ac_simps filter_disjount_union) apply (subst filter_disjount_union) apply auto apply (subst filter_disjount_union) apply auto by (metis (no_types, lifting) Diff_iff UnE all_clauses_literals(3) filter_True) lemma sorted_unadded_literals_Cons_notin_all_clauses_literals[simp]: assumes ‹atm_of (lit_of K) ∉ set all_clauses_literals› shows ‹sorted_unadded_literals (K # M) = sorted_unadded_literals M› proof - have [simp]: ‹filter (full_unset_literals_in_ΔΣ' (K # M)) all_clauses_literals = filter (full_unset_literals_in_ΔΣ' M) all_clauses_literals› ‹filter (full_unset_literals_in_ΔΣ (K # M)) all_clauses_literals = filter (full_unset_literals_in_ΔΣ M) all_clauses_literals› ‹filter (half_unset_literals_in_ΔΣ (K # M)) all_clauses_literals = filter (half_unset_literals_in_ΔΣ M) all_clauses_literals› ‹filter (unset_literals_in_Σ (K # M)) all_clauses_literals = filter (unset_literals_in_Σ M) all_clauses_literals› using assms unfolding full_unset_literals_in_ΔΣ'_def full_unset_literals_in_ΔΣ_def half_unset_literals_in_ΔΣ_def unset_literals_in_Σ_def by (auto simp: sorted_unadded_literals_def undefined_notin all_clauses_literals(1,2) defined_lit_Neg_Pos_iff all_clauses_literals(3) defined_lit_cons intro!: ext filter_cong) show ?thesis by (auto simp: undefined_notin all_clauses_literals(1,2) defined_lit_Neg_Pos_iff all_clauses_literals(3) sorted_unadded_literals_def) qed lemma sorted_unadded_literals_cong: assumes ‹⋀L. L ∈ set all_clauses_literals ⟹ defined_lit M (Pos L) = defined_lit M' (Pos L)› shows ‹sorted_unadded_literals M = sorted_unadded_literals M'› proof - have [simp]: ‹filter (full_unset_literals_in_ΔΣ' (M)) all_clauses_literals = filter (full_unset_literals_in_ΔΣ' M') all_clauses_literals› ‹filter (full_unset_literals_in_ΔΣ (M)) all_clauses_literals = filter (full_unset_literals_in_ΔΣ M') all_clauses_literals› ‹filter (half_unset_literals_in_ΔΣ (M)) all_clauses_literals = filter (half_unset_literals_in_ΔΣ M') all_clauses_literals› ‹filter (unset_literals_in_Σ (M)) all_clauses_literals = filter (unset_literals_in_Σ M') all_clauses_literals› using assms unfolding full_unset_literals_in_ΔΣ'_def full_unset_literals_in_ΔΣ_def half_unset_literals_in_ΔΣ_def unset_literals_in_Σ_def by (auto simp: sorted_unadded_literals_def undefined_notin all_clauses_literals(1,2) defined_lit_Neg_Pos_iff all_clauses_literals(3) defined_lit_cons intro!: ext filter_cong) show ?thesis by (auto simp: undefined_notin all_clauses_literals(1,2) defined_lit_Neg_Pos_iff all_clauses_literals(3) sorted_unadded_literals_def) qed lemma sorted_unadded_literals_Cons_already_set[simp]: assumes ‹defined_lit M (lit_of K)› shows ‹sorted_unadded_literals (K # M) = sorted_unadded_literals M› by (rule sorted_unadded_literals_cong) (use assms in ‹auto simp: defined_lit_cons›) lemma distinct_sorted_unadded_literals[simp]: ‹distinct (sorted_unadded_literals M)› unfolding half_unset_literals_in_ΔΣ_def full_unset_literals_in_ΔΣ_def unset_literals_in_Σ_def sorted_unadded_literals_def full_unset_literals_in_ΔΣ'_def by (auto simp: sorted_unadded_literals_def all_clauses_literals(1,2)) lemma Collect_req_remove1: ‹{a ∈ A. a ≠ b ∧ P a} = (if P b then Set.remove b {a ∈ A. P a} else {a ∈ A. P a})› and Collect_req_remove2: ‹{a ∈ A. b ≠ a ∧ P a} = (if P b then Set.remove b {a ∈ A. P a} else {a ∈ A. P a})› by auto lemma card_remove: ‹card (Set.remove a A) = (if a ∈ A then card A - 1 else card A)› by (auto simp: Set.remove_def) lemma sorted_unadded_literals_cons_in_undef[simp]: ‹undefined_lit M (lit_of K) ⟹ atm_of (lit_of K) ∈ set all_clauses_literals ⟹ Suc (length (sorted_unadded_literals (K # M))) = length (sorted_unadded_literals M)› by (auto simp flip: distinct_card simp: Set.filter_def Collect_req_remove2 card_remove isabelle_should_do_that_automatically card_gt_0_iff simp flip: less_eq_Suc_le) lemma no_dup_complete_trail[simp]: ‹no_dup (complete_trail M) ⟷ no_dup M› by (auto simp: complete_trail_def no_dup_def comp_def all_clauses_literals(1,2) undefined_notin) lemma tautology_complete_trail[simp]: ‹tautology (lit_of `# mset (complete_trail M)) ⟷ tautology (lit_of `# mset M)› by (auto simp: complete_trail_def tautology_decomp' comp_def all_clauses_literals undefined_notin uminus_lit_swap defined_lit_Neg_Pos_iff simp flip: defined_lit_Neg_Pos_iff) lemma atms_of_complete_trail: ‹atms_of (lit_of `# mset (complete_trail M)) = atms_of (lit_of `# mset M) ∪ (Σ - ΔΣ) ∪ replacement_neg ` ΔΣ ∪ replacement_pos ` ΔΣ› by (auto simp add: complete_trail_def all_clauses_literals image_image image_Un atms_of_def defined_lit_map) fun depth_lit_of :: ‹('v,_) ann_lit ⇒ ('v, _) ann_lit search_depth› where ‹depth_lit_of (Decided L) = SD_TWO (Decided L)› | ‹depth_lit_of (Propagated L C) = SD_ZERO (Propagated L C)› fun depth_lit_of_additional_fst :: ‹('v,_) ann_lit ⇒ ('v, _) ann_lit search_depth› where ‹depth_lit_of_additional_fst (Decided L) = SD_ONE (Decided L)› | ‹depth_lit_of_additional_fst (Propagated L C) = SD_ZERO (Propagated L C)› fun depth_lit_of_additional_snd :: ‹('v,_) ann_lit ⇒ ('v, _) ann_lit search_depth list› where ‹depth_lit_of_additional_snd (Decided L) = [SD_ONE (Decided L)]› | ‹depth_lit_of_additional_snd (Propagated L C) = []› text ‹ This function is suprisingly complicated to get right. Remember that the last set element is at the beginning of the list › fun remove_dup_information_raw :: ‹('v, _) ann_lits ⇒ ('v, _) ann_lit search_depth list› where ‹remove_dup_information_raw [] = []› | ‹remove_dup_information_raw (L # M) = (if atm_of (lit_of L) ∈ Σ - ΔΣ then depth_lit_of L # remove_dup_information_raw M else if defined_lit (M) (Pos (opposite_var (atm_of (lit_of L)))) then if Decided (Pos (opposite_var (atm_of (lit_of L)))) ∈ set (M) then remove_dup_information_raw M else depth_lit_of_additional_fst L # remove_dup_information_raw M else depth_lit_of_additional_snd L @ remove_dup_information_raw M)› definition remove_dup_information where ‹remove_dup_information xs = un_hide_sd (remove_dup_information_raw xs)› lemma [simp]: ‹the_search_depth (depth_lit_of L) = L› by (cases L) auto lemma length_complete_trail[simp]: ‹length (complete_trail []) = length all_clauses_literals› unfolding complete_trail_def by (auto simp: sum_length_filter_compl) lemma distinct_count_list_if: ‹distinct xs ⟹ count_list xs x = (if x ∈ set xs then 1 else 0)› by (induction xs) auto lemma length_complete_trail_Cons: ‹no_dup (K # M) ⟹ length (complete_trail (K # M)) = (if atm_of (lit_of K) ∈ set all_clauses_literals then 0 else 1) + length (complete_trail M)› unfolding complete_trail_def by auto lemma length_complete_trail_eq: ‹no_dup M ⟹ atm_of ` (lits_of_l M) ⊆ set all_clauses_literals ⟹ length (complete_trail M) = length all_clauses_literals› by (induction M rule: ann_lit_list_induct) (auto simp: length_complete_trail_Cons) lemma in_set_all_clauses_literals_simp[simp]: ‹atm_of L ∈ Σ - ΔΣ ⟹ atm_of L ∈ set all_clauses_literals› ‹K ∈ ΔΣ ⟹ replacement_pos K ∈ set all_clauses_literals› ‹K ∈ ΔΣ ⟹ replacement_neg K ∈ set all_clauses_literals› by (auto simp: all_clauses_literals) lemma [simp]: ‹remove_dup_information [] = []› by (auto simp: remove_dup_information_def) lemma atm_of_remove_dup_information: ‹atm_of ` (lits_of_l M) ⊆ set all_clauses_literals ⟹ atm_of ` (lits_of_l (remove_dup_information M)) ⊆ set all_clauses_literals› unfolding remove_dup_information_def apply (induction M rule: ann_lit_list_induct) apply (auto simp: Decided_Propagated_in_iff_in_lits_of_l lits_of_def image_image) done primrec remove_dup_information_raw2 :: ‹('v, _) ann_lits ⇒ ('v, _) ann_lits ⇒ ('v, _) ann_lit search_depth list› where ‹remove_dup_information_raw2 M' [] = []› | ‹remove_dup_information_raw2 M' (L # M) = (if atm_of (lit_of L) ∈ Σ - ΔΣ then depth_lit_of L # remove_dup_information_raw2 M' M else if defined_lit (M @ M') (Pos (opposite_var (atm_of (lit_of L)))) then if Decided (Pos (opposite_var (atm_of (lit_of L)))) ∈ set (M @ M') then remove_dup_information_raw2 M' M else depth_lit_of_additional_fst L # remove_dup_information_raw2 M' M else depth_lit_of_additional_snd L @ remove_dup_information_raw2 M' M)› lemma remove_dup_information_raw2_Nil[simp]: ‹remove_dup_information_raw2 [] M = remove_dup_information_raw M› by (induction M) auto text ‹This can be useful as simp, but I am not certain (yet), because the RHS does not look simpler than the LHS.› lemma remove_dup_information_raw_cons: ‹remove_dup_information_raw (L # M2) = remove_dup_information_raw2 M2 [L] @ remove_dup_information_raw M2› by (auto simp: defined_lit_append) lemma remove_dup_information_raw_append: ‹remove_dup_information_raw (M1 @ M2) = remove_dup_information_raw2 M2 M1 @ remove_dup_information_raw M2› by (induction M1) (auto simp: defined_lit_append) lemma remove_dup_information_raw_append2: ‹remove_dup_information_raw2 M (M1 @ M2) = remove_dup_information_raw2 (M @ M2) M1 @ remove_dup_information_raw2 M M2› by (induction M1) (auto simp: defined_lit_append) lemma remove_dup_information_subset: ‹mset (remove_dup_information M) ⊆# mset M› unfolding remove_dup_information_def apply (induction M rule: ann_lit_list_induct) apply auto apply (metis add_mset_remove_trivial diff_subset_eq_self subset_mset.dual_order.trans)+ done (*TODO Move*) lemma no_dup_subsetD: ‹no_dup M ⟹ mset M' ⊆# mset M ⟹ no_dup M'› unfolding no_dup_def distinct_mset_mset_distinct[symmetric] mset_map apply (drule image_mset_subseteq_mono[of _ _ ‹atm_of o lit_of›]) apply (drule distinct_mset_mono) apply auto done lemma no_dup_remove_dup_information: ‹no_dup M ⟹ no_dup (remove_dup_information M)› using no_dup_subsetD[OF _ remove_dup_information_subset] by blast lemma atm_of_complete_trail: ‹atm_of ` (lits_of_l M) ⊆ set all_clauses_literals ⟹ atm_of ` (lits_of_l (complete_trail M)) = set all_clauses_literals› unfolding complete_trail_def by (auto simp: lits_of_def image_image image_Un defined_lit_map) lemmas [simp del] = remove_dup_information_raw.simps remove_dup_information_raw2.simps lemmas [simp] = remove_dup_information_raw_append remove_dup_information_raw_cons remove_dup_information_raw_append2 definition truncate_trail :: ‹('v, _) ann_lits ⇒ _› where ‹truncate_trail M ≡ (snd (backtrack_split M))› definition ocdcl_score :: ‹('v, _) ann_lits ⇒ _› where ‹ocdcl_score M = rev (map nat_of_search_deph (remove_dup_information_raw (complete_trail (truncate_trail M))))› interpretation enc_weight_opt: conflict_driven_clause_learning_W_optimal_weight where state_eq = state_eq and state = state and trail = trail and init_clss = init_clss and learned_clss = learned_clss and conflicting = conflicting and cons_trail = cons_trail and tl_trail = tl_trail and add_learned_cls = add_learned_cls and remove_cls = remove_cls and update_conflicting = update_conflicting and init_state = init_state and ρ = ρ_e and update_additional_info = update_additional_info apply unfold_locales subgoal by (rule ρ_e_mono) subgoal using update_additional_info by fast subgoal using weight_init_state by fast done lemma ‹(a, b) ∈ lexn less_than n ⟹ (b, c) ∈ lexn less_than n ∨ b = c ⟹ (a, c) ∈ lexn less_than n› ‹(a, b) ∈ lexn less_than n ⟹ (b, c) ∈ lexn less_than n ∨ b = c ⟹ (a, c) ∈ lexn less_than n› apply (auto intro: ) apply (meson lexn_transI trans_def trans_less_than)+ done lemma truncate_trail_Prop[simp]: ‹truncate_trail (Propagated L E # S) = truncate_trail (S)› by (auto simp: truncate_trail_def) lemma ocdcl_score_Prop[simp]: ‹ocdcl_score (Propagated L E # S) = ocdcl_score (S)› by (auto simp: ocdcl_score_def truncate_trail_def) lemma remove_dup_information_raw2_undefined_Σ: ‹distinct xs ⟹ (⋀L. L ∈ set xs ⟹ undefined_lit M (Pos L) ⟹ L ∈ Σ ⟹ undefined_lit MM (Pos L)) ⟹ remove_dup_information_raw2 MM (map (Decided ∘ Pos) (filter (unset_literals_in_Σ M) xs)) = map (SD_TWO o Decided ∘ Pos) (filter (unset_literals_in_Σ M) xs)› by (induction xs) (auto simp: remove_dup_information_raw2.simps unset_literals_in_Σ_def) lemma defined_lit_map_Decided_pos: ‹defined_lit (map (Decided ∘ Pos) M) L ⟷ atm_of L ∈ set M› by (induction M) (auto simp: defined_lit_cons) lemma remove_dup_information_raw2_full_undefined_Σ: ‹distinct xs ⟹ set xs ⊆ set all_clauses_literals ⟹ (⋀L. L ∈ set xs ⟹ undefined_lit M (Pos L) ⟹ L ∉ Σ - ΔΣ ⟹ undefined_lit M (Pos (opposite_var L)) ⟹ L ∈ replacement_pos ` ΔΣ ⟹ undefined_lit MM (Pos (opposite_var L))) ⟹ remove_dup_information_raw2 MM (map (Decided ∘ Pos) (filter (full_unset_literals_in_ΔΣ M) xs)) = map (SD_ONE o Decided ∘ Pos) (filter (full_unset_literals_in_ΔΣ M) xs)› unfolding all_clauses_literals apply (induction xs) subgoal by (simp_all add: remove_dup_information_raw2.simps) subgoal premises p for L xs using p(1-3) p(4)[of L] p(4) by (clarsimp simp add: remove_dup_information_raw2.simps defined_lit_map_Decided_pos full_unset_literals_in_ΔΣ_def defined_lit_append) done lemma full_unset_literals_in_ΔΣ_notin[simp]: ‹La ∈ Σ ⟹ full_unset_literals_in_ΔΣ M La ⟷ False› ‹La ∈ Σ ⟹ full_unset_literals_in_ΔΣ' M La ⟷ False› apply (metis (mono_tags) full_unset_literals_in_ΔΣ_def image_iff new_vars_pos) by (simp add: full_unset_literals_in_ΔΣ'_def image_iff) lemma Decided_in_definedD: ‹Decided K ∈ set M ⟹ defined_lit M K› by (simp add: defined_lit_def) lemma full_unset_literals_in_ΔΣ'_full_unset_literals_in_ΔΣ: ‹L ∈ replacement_pos ` ΔΣ ∪ replacement_neg ` ΔΣ ⟹ full_unset_literals_in_ΔΣ' M (opposite_var L) ⟷ full_unset_literals_in_ΔΣ M L› by (auto simp: full_unset_literals_in_ΔΣ'_def full_unset_literals_in_ΔΣ_def opposite_var_def) lemma remove_dup_information_raw2_full_unset_literals_in_ΔΣ': ‹(⋀L. L ∈ set (filter (full_unset_literals_in_ΔΣ' M) xs) ⟹ Decided (Pos (opposite_var L)) ∈ set M') ⟹ set xs ⊆ set all_clauses_literals ⟹ (remove_dup_information_raw2 M' (map (Decided ∘ Pos) (filter (full_unset_literals_in_ΔΣ' (M)) xs))) = []› supply [[goals_limit=1]] apply (induction xs) subgoal by (auto simp: remove_dup_information_raw2.simps) subgoal premises p for L xs using p by (force simp add: remove_dup_information_raw2.simps full_unset_literals_in_ΔΣ'_full_unset_literals_in_ΔΣ all_clauses_literals defined_lit_map_Decided_pos defined_lit_append image_iff dest: Decided_in_definedD) done lemma fixes M :: ‹('v, _) ann_lits› and L :: ‹('v, _) ann_lit› defines ‹n1 ≡ map nat_of_search_deph (remove_dup_information_raw (complete_trail (L # M)))› and ‹n2 ≡ map nat_of_search_deph (remove_dup_information_raw (complete_trail M))› assumes lits: ‹atm_of ` (lits_of_l (L # M)) ⊆ set all_clauses_literals› and undef: ‹undefined_lit M (lit_of L)› shows ‹(rev n1, rev n2) ∈ lexn less_than n ∨ n1 = n2› proof - show ?thesis using lits apply (auto simp: n1_def n2_def complete_trail_def prepend_same_lexn) apply (auto simp: sorted_unadded_literals_def remove_dup_information_raw2.simps all_clauses_literals(2) defined_lit_map_Decided_pos remove_dup_information_raw2_undefined_Σ) subgoal apply (subst remove_dup_information_raw2_undefined_Σ) apply (simp_all add: all_clauses_literals(2) defined_lit_map_Decided_pos remove_dup_information_raw2_undefined_Σ) apply (subst remove_dup_information_raw2_full_undefined_Σ) apply (auto simp: all_clauses_literals(2)) apply (subst remove_dup_information_raw2_full_unset_literals_in_ΔΣ') apply (auto simp: full_unset_literals_in_ΔΣ'_full_unset_literals_in_ΔΣ)[2] oops lemma defines ‹n ≡ card Σ› assumes ‹init_clss S = penc N› and ‹enc_weight_opt.cdcl_bnb_stgy S T› and struct: ‹cdcl_W_restart_mset.cdcl_W_all_struct_inv (enc_weight_opt.abs_state S)› and smaller_propa: ‹no_smaller_propa S› and smaller_confl: ‹cdcl_bnb_stgy_inv S› shows ‹(ocdcl_score (trail T), ocdcl_score (trail S)) ∈ lexn less_than n ∨ ocdcl_score (trail T) = ocdcl_score (trail S)› using assms(3) proof (cases) case cdcl_bnb_conflict then show ?thesis by (auto elim!: rulesE) next case cdcl_bnb_propagate then show ?thesis by (auto elim!: rulesE) next case cdcl_bnb_improve then show ?thesis by (auto elim!: enc_weight_opt.improveE) next case cdcl_bnb_conflict_opt then show ?thesis by (auto elim!: enc_weight_opt.conflict_optE) next case cdcl_bnb_other' then show ?thesis proof cases case bj then show ?thesis proof cases case skip then show ?thesis by (auto elim!: rulesE) next case resolve then show ?thesis by (cases ‹trail S›) (auto elim!: rulesE) next case backtrack then obtain M1 M2 :: ‹('v, 'v clause) ann_lits› and K L :: ‹'v literal› and D D' :: ‹'v clause› where confl: ‹conflicting S = Some (add_mset L D)› and decomp: ‹(Decided K # M1, M2) ∈ set (get_all_ann_decomposition (trail S))› and ‹get_maximum_level (trail S) (add_mset L D') = local.backtrack_lvl S› and ‹get_level (trail S) L = local.backtrack_lvl S› and lev_K: ‹get_level (trail S) K = Suc (get_maximum_level (trail S) D')› and D'_D: ‹D' ⊆# D› and ‹set_mset (clauses S) ∪ set_mset (enc_weight_opt.conflicting_clss S) ⊨p add_mset L D'› and T: ‹T ∼ cons_trail (Propagated L (add_mset L D')) (reduce_trail_to M1 (add_learned_cls (add_mset L D') (update_conflicting None S)))› by (auto simp: enc_weight_opt.obacktrack.simps) have tr_D: ‹trail S ⊨as CNot (add_mset L D)› and ‹distinct_mset (add_mset L D)› and ‹cdcl_W_restart_mset.cdcl_W_M_level_inv (abs_state S)› and n_d: ‹no_dup (trail S)› using struct confl unfolding cdcl_W_restart_mset.cdcl_W_all_struct_inv_def cdcl_W_restart_mset.cdcl_W_conflicting_def cdcl_W_restart_mset.distinct_cdcl_W_state_def cdcl_W_restart_mset.cdcl_W_M_level_inv_def by auto have tr_D': ‹trail S ⊨as CNot (add_mset L D')› using D'_D tr_D by (auto simp: true_annots_true_cls_def_iff_negation_in_model) have ‹trail S ⊨as CNot D' ⟹ trail S ⊨as CNot (normalize2 D')› if ‹get_maximum_level (trail S) D' < backtrack_lvl S› for D' (*by induction on all the literals*) oops (* lemma remove_dup_information_subset: ‹mset (remove_dup_information M) ⊆# mset M› unfolding remove_dup_information_def apply (induction M rule: ann_lit_list_induct) apply auto apply (metis add_mset_remove_trivial diff_subset_eq_self subset_mset.dual_order.trans)+ done (*TODO Move*) lemma no_dup_subsetD: ‹no_dup M ⟹ mset M' ⊆# mset M ⟹ no_dup M'› unfolding no_dup_def distinct_mset_mset_distinct[symmetric] mset_map apply (drule image_mset_subseteq_mono[of _ _ ‹atm_of o lit_of›]) apply (drule distinct_mset_mono) apply auto done lemma no_dup_remove_dup_information: ‹no_dup M ⟹ no_dup (remove_dup_information M)› using no_dup_subsetD[OF _ remove_dup_information_subset] by blast lemma atm_of_complete_trail: ‹atm_of ` (lits_of_l M) ⊆ set all_clauses_literals ⟹ atm_of ` (lits_of_l (complete_trail M)) = set all_clauses_literals› unfolding complete_trail_def by (auto simp: lits_of_def image_image image_Un defined_lit_map) definition ocdcl_trail_inv where ‹ocdcl_trail_inv M ⟷ no_dup M ∧ atm_of ` (lits_of_l M) ⊆ Σ ∪ replacement_pos ` ΔΣ ∪ replacement_neg ` ΔΣ ∧ (∀P. P ∈ replacement_pos ` ΔΣ ∪ replacement_neg ` ΔΣ ⟶ Decided (Neg P) ∉ set M) ∧ (∀P. P ∈ replacement_pos ` ΔΣ ∪ replacement_neg ` ΔΣ ⟶ Decided (Pos P) ∈ set M ⟶ Decided (Pos (opposite_var P)) ∉ set M)› lemma ocdcl_trail_inv_tlD: ‹ocdcl_trail_inv (L # M) ⟹ ocdcl_trail_inv M› by (auto simp: ocdcl_trail_inv_def) lemma ocdcl_trail_inv_Cons1[simp]: ‹atm_of (lit_of L) ∈ Σ ⟹ ocdcl_trail_inv (L # M) ⟷ undefined_lit M (lit_of L) ∧ ocdcl_trail_inv M› by (auto simp: ocdcl_trail_inv_def) lemma ocdcl_trail_inv_Cons2: ‹atm_of (lit_of L) ∈ replacement_pos ` ΔΣ ∪ replacement_neg ` ΔΣ ⟹ ocdcl_trail_inv (L # M) ⟹ undefined_lit M (lit_of L) ∧ (is_decided L ⟶ is_pos (lit_of L) ∧ Decided (Pos (opposite_var (atm_of (lit_of L)))) ∉ set M) ∧ ocdcl_trail_inv M› by (cases L; cases ‹lit_of L›; auto simp: ocdcl_trail_inv_def) lemma ocdcl_trail_inv_ConsE: ‹ocdcl_trail_inv (L # M) ⟹ atm_of (lit_of L) ∈ Σ ∪ replacement_pos ` ΔΣ ∪ replacement_neg ` ΔΣ ⟹ (atm_of (lit_of L) ∈ replacement_pos ` ΔΣ ∪ replacement_neg ` ΔΣ ⟹ undefined_lit M (lit_of L) ⟹ (is_decided L ⟶ is_pos (lit_of L) ∧ Decided (Pos (opposite_var (atm_of (lit_of L)))) ∉ set M) ⟹ ocdcl_trail_inv M ⟹ P) ⟹ (atm_of (lit_of L) ∈ Σ ⟹ undefined_lit M (lit_of L) ⟹ ocdcl_trail_inv M ⟹ P) ⟹ P› using ocdcl_trail_inv_Cons2 ocdcl_trail_inv_Cons1 by blast lemma ‹P ∈ replacement_pos ` ΔΣ ∪ replacement_neg ` ΔΣ ⟹ ocdcl_trail_inv M ⟹ defined_lit (remove_dup_information M) (Pos P) ⟹ undefined_lit (remove_dup_information M) (Pos (opposite_var P))› unfolding remove_dup_information_def apply (induction M arbitrary: P rule: ann_lit_list_induct) apply (auto simp: defined_lit_cons split: dest: elim!: ) thm TrueI subgoal apply (auto elim!: ocdcl_trail_inv_ConsE) sorry lemma atm_of_complete_trail_remove_dup_information: ‹no_dup M ⟹ atm_of ` (lits_of_l M) ⊆ set all_clauses_literals ⟹ atm_of ` (lits_of_l (complete_trail (remove_dup_information M))) = set all_clauses_literals› by (simp_all add: atm_of_complete_trail atm_of_remove_dup_information) text ‹TODO: ▪ complete_trail is doing the wrong thing (or it should be done before @{term ‹remove_dup_information›}). ▪ is the measure really the simplest thing we can do? › fun ocdcl_score_rev :: ‹('v, _) ann_lits ⇒ nat list› where ‹ocdcl_score_rev [] = []› | ‹ocdcl_score_rev (Propagated K C # M) = (if defined_lit M (Pos (opposite_var (atm_of K))) then 1 else 0) # ocdcl_score_rev M› | ‹ocdcl_score_rev (Decided K # M) = (if atm_of K ∈ Σ - ΔΣ then 1 else if defined_lit M (Pos (opposite_var (atm_of K))) then 2 else 1) # ocdcl_score_rev M› definition ocdcl_mu where ‹ocdcl_mu M = rev (ocdcl_score_rev (complete_trail M))› lemma ocdcl_score_rev_in_0_3: ‹x ∈ set (ocdcl_score_rev M) ⟹ x ∈ {0..<3}› by (induction M rule: ann_lit_list_induct) auto lemma ‹no_dup M ⟹ length (ocdcl_score_rev M) ≤ length M› fun ocdcl_score_rev :: ‹('v, 'b) ann_lits ⇒ ('v, 'b) ann_lits ⇒ nat› where ‹ocdcl_score_rev _ [] = 0› | ‹ocdcl_score_rev M' (Propagated K C # M) = ocdcl_score_rev (M' @ [Propagated K C]) M› | ‹ocdcl_score_rev M' (Decided K # M) = ocdcl_score_rev (M' @ [Decided K]) M + (if atm_of K ∈ Σ - ΔΣ then 1 else if Decided (base_atm (atm_of K)) ∈ set (map (map_annotated_lit (base_atm o atm_of) id id) M') then 2 else 1) * 3^card (base_atm ` atms_of (lit_of `# mset M))› abbreviation ocdcl_score:: ‹('v, 'b) ann_lits ⇒ ('v, 'b) ann_lits ⇒ nat› where ‹ocdcl_score M M' ≡ ocdcl_score_rev M (rev M')› lemma ocdcl_score_rev_induct_internal: fixes xs ys :: ‹('v, 'b) ann_lits› assumes ‹ys @ xs = M0› ‹P M0 []› ‹⋀L C M M'. M0 = M' @ Propagated L C # M ⟹ P (M' @ [Propagated L C]) M ⟹ P M' (Propagated L C # M)› ‹⋀L M M'. M0 = M' @ Decided L # M⟹ P (M' @ [Decided L]) M ⟹ P M' (Decided L # M)› shows ‹P ys xs ∧ ys @ xs = M0› using assms(1) apply (induction ys xs rule: ocdcl_score_rev.induct) subgoal using assms(1,2) by auto subgoal for M L C M' using assms(3) by auto subgoal for M L M' using assms(4) by auto done lemma ocdcl_score_rev_induct2: fixes xs ys :: ‹('v, 'b) ann_lits› assumes ‹P (ys @ xs) []› ‹⋀L C M M'. ys @ xs = M' @ Propagated L C # M ⟹ P (M' @ [Propagated L C]) M ⟹ P M' (Propagated L C # M)› ‹⋀L M M'. ys @ xs = M' @ Decided L # M ⟹ P (M' @ [Decided L]) M ⟹ P M' (Decided L # M) › shows ‹P ys xs› using ocdcl_score_rev_induct_internal[of ys xs ‹ys @ xs› P] assms by auto lemma ocdcl_score_rev_induct: fixes xs ys :: ‹('v, 'b) ann_lits› assumes ‹P xs []› ‹⋀L C M M'. xs = M' @ Propagated L C # M ⟹ P (M' @ [Propagated L C]) M ⟹ P M' (Propagated L C # M)› ‹⋀L M M'. xs = M' @ Decided L # M ⟹ P (M' @ [Decided L]) M ⟹ P M' (Decided L # M) › shows ‹P [] xs› using ocdcl_score_rev_induct_internal[of ‹[]› xs xs P] assms by auto lemma Decided_map_annotated_lit_iff[simp]: ‹Decided L = map_annotated_lit f g h x ⟷ (∃x'. x = Decided x' ∧ L = f x')› by (cases x) auto lemma ‹atm_of ` (lits_of_l (M' @ M)) ⊆ Σ ⟹ no_dup (M' @ M) ⟹ ocdcl_score_rev M' M ≤ 3 ^ (card ((base_atm o atm_of) ` lits_of_l M))› apply (induction M' M rule: ocdcl_score_rev_induct2) subgoal by auto subgoal for L M' M by (cases ‹atm_of L ∈ Σ›) (auto simp: card_insert_if) subgoal for L Ma M'a using ΔΣ_Σ apply (auto simp: card_insert_if atm_of_eq_atm_of lits_of_def image_image atms_of_def image_Un dest!: split_list[of _ M'a]) oops *) end interpretation enc_weight_opt: conflict_driven_clause_learning_W_optimal_weight where state_eq = state_eq and state = state and trail = trail and init_clss = init_clss and learned_clss = learned_clss and conflicting = conflicting and cons_trail = cons_trail and tl_trail = tl_trail and add_learned_cls = add_learned_cls and remove_cls = remove_cls and update_conflicting = update_conflicting and init_state = init_state and ρ = ρ_e and update_additional_info = update_additional_info apply unfold_locales subgoal by (rule ρ_e_mono) subgoal using update_additional_info by fast subgoal using weight_init_state by fast done inductive simple_backtrack_conflict_opt :: ‹'st ⇒ 'st ⇒ bool› where ‹simple_backtrack_conflict_opt S T› if ‹backtrack_split (trail S) = (M2, Decided K # M1)› and ‹negate_ann_lits (trail S) ∈# enc_weight_opt.conflicting_clss S› and ‹conflicting S = None› and ‹T ∼ cons_trail (Propagated (-K) (DECO_clause (trail S))) (add_learned_cls (DECO_clause (trail S)) (reduce_trail_to M1 S))› inductive_cases simple_backtrack_conflict_optE: ‹simple_backtrack_conflict_opt S T› lemma simple_backtrack_conflict_opt_conflict_analysis: assumes ‹simple_backtrack_conflict_opt S U› and inv: ‹cdcl_W_restart_mset.cdcl_W_all_struct_inv (enc_weight_opt.abs_state S)› shows ‹∃T T'. enc_weight_opt.conflict_opt S T ∧ resolve^*^* T T' ∧ enc_weight_opt.obacktrack T' U› using assms proof (cases rule: simple_backtrack_conflict_opt.cases) case (1 M2 K M1) have tr: ‹trail S = M2 @ Decided K # M1› using 1 backtrack_split_list_eq[of ‹trail S›] by auto let ?S = ‹update_conflicting (Some (negate_ann_lits (trail S))) S› have ‹enc_weight_opt.conflict_opt S ?S› by (rule enc_weight_opt.conflict_opt.intros[OF 1(2,3)]) auto let ?T = ‹λn. update_conflicting (Some (negate_ann_lits (drop n (trail S)))) (reduce_trail_to (drop n (trail S)) S)› have proped_M2: ‹is_proped (M2 ! n)› if ‹n < length M2› for n using that 1(1) nth_length_takeWhile[of ‹Not ∘ is_decided› ‹trail S›] length_takeWhile_le[of ‹Not ∘ is_decided› ‹trail S›] unfolding backtrack_split_takeWhile_dropWhile apply auto by (metis annotated_lit.exhaust_disc comp_apply nth_mem set_takeWhileD) have is_dec_M2[simp]: ‹filter_mset is_decided (mset M2) = {#}› using 1(1) nth_length_takeWhile[of ‹Not ∘ is_decided› ‹trail S›] length_takeWhile_le[of ‹Not ∘ is_decided› ‹trail S›] unfolding backtrack_split_takeWhile_dropWhile apply (auto simp: filter_mset_empty_conv) by (metis annotated_lit.exhaust_disc comp_apply nth_mem set_takeWhileD) have n_d: ‹no_dup (trail S)› and le: ‹cdcl_W_restart_mset.cdcl_W_conflicting (enc_weight_opt.abs_state S)› and dist: ‹cdcl_W_restart_mset.distinct_cdcl_W_state (enc_weight_opt.abs_state S)› and decomp_imp: ‹all_decomposition_implies_m (clauses S + (enc_weight_opt.conflicting_clss S)) (get_all_ann_decomposition (trail S))› and learned: ‹cdcl_W_restart_mset.cdcl_W_learned_clause (enc_weight_opt.abs_state S)› using inv unfolding cdcl_W_restart_mset.cdcl_W_all_struct_inv_def cdcl_W_restart_mset.cdcl_W_M_level_inv_def by auto then have [simp]: ‹K ≠ lit_of (M2 ! n)› if ‹n < length M2› for n using that unfolding tr by (auto simp: defined_lit_nth) have n_d_n: ‹no_dup (drop n M2 @ Decided K # M1)› for n using n_d unfolding tr by (subst (asm) append_take_drop_id[symmetric, of _ n]) (auto simp del: append_take_drop_id dest: no_dup_appendD) have mark_dist: ‹distinct_mset (mark_of (M2!n))› if ‹n < length M2› for n using dist that proped_M2[OF that] nth_mem[OF that] unfolding cdcl_W_restart_mset.distinct_cdcl_W_state_def tr by (cases ‹M2!n›) (auto simp: tr) have [simp]: ‹undefined_lit (drop n M2) K› for n using n_d defined_lit_mono[of ‹drop n M2› K M2] unfolding tr by (auto simp: set_drop_subset) from this[of 0] have [simp]: ‹undefined_lit M2 K› by auto have [simp]: ‹count_decided (drop n M2) = 0› for n apply (subst count_decided_0_iff) using 1(1) nth_length_takeWhile[of ‹Not ∘ is_decided› ‹trail S›] length_takeWhile_le[of ‹Not ∘ is_decided› ‹trail S›] unfolding backtrack_split_takeWhile_dropWhile by (auto simp: dest!: in_set_dropD set_takeWhileD) from this[of 0] have [simp]: ‹count_decided M2 = 0› by simp have proped: ‹⋀L mark a b. a @ Propagated L mark # b = trail S ⟶ b ⊨as CNot (remove1_mset L mark) ∧ L ∈# mark› using le unfolding cdcl_W_restart_mset.cdcl_W_conflicting_def by auto have mark: ‹drop (Suc n) M2 @ Decided K # M1 ⊨as CNot (mark_of (M2 ! n) - unmark (M2 ! n)) ∧ lit_of (M2 ! n) ∈# mark_of (M2 ! n)› if ‹n < length M2› for n using proped_M2[OF that] that append_take_drop_id[of n M2, unfolded Cons_nth_drop_Suc[OF that, symmetric]] proped[of ‹take n M2› ‹lit_of (M2 ! n)› ‹mark_of (M2 ! n)› ‹drop (Suc n) M2 @ Decided K # M1›] unfolding tr by (cases ‹M2!n›) auto have confl: ‹enc_weight_opt.conflict_opt S ?S› by (rule enc_weight_opt.conflict_opt.intros) (use 1 in auto) have res: ‹resolve^*^* ?S (?T n)› if ‹n ≤ length M2› for n using that unfolding tr proof (induction n) case 0 then show ?case using get_all_ann_decomposition_backtrack_split[THEN iffD1, OF 1(1)] 1 by (cases ‹get_all_ann_decomposition (trail S)›) (auto simp: tr) next case (Suc n) have [simp]: ‹¬ Suc (length M2 - Suc n) < length M2 ⟷ n = 0› using Suc(2) by auto have [simp]: ‹reduce_trail_to (drop (Suc 0) M2 @ Decided K # M1) S = tl_trail S› apply (subst reduce_trail_to.simps) using Suc by (auto simp: tr ) have [simp]: ‹reduce_trail_to (M2 ! 0 # drop (Suc 0) M2 @ Decided K # M1) S = S› apply (subst reduce_trail_to.simps) using Suc by (auto simp: tr ) have [simp]: ‹(Suc (length M1) - (length M2 - n + (Suc (length M1) - (n - length M2)))) = 0› ‹(Suc (length M2 + length M1) - (length M2 - n + (Suc (length M1) - (n - length M2)))) =n› ‹length M2 - n + (Suc (length M1) - (n - length M2)) = Suc (length M2 + length M1) - n› using Suc by auto have [symmetric,simp]: ‹M2 ! n = Propagated (lit_of (M2 ! n)) (mark_of (M2 ! n))› using Suc proped_M2[of n] by (cases ‹M2 ! n›) (auto simp: tr trail_reduce_trail_to_drop hd_drop_conv_nth intro!: resolve.intros) have ‹- lit_of (M2 ! n) ∈# negate_ann_lits (drop n M2 @ Decided K # M1)› using Suc in_set_dropI[of ‹n› ‹map (uminus o lit_of) M2› n] by (simp add: negate_ann_lits_def comp_def drop_map del: nth_mem) moreover have ‹get_maximum_level (drop n M2 @ Decided K # M1) (remove1_mset (- lit_of (M2 ! n)) (negate_ann_lits (drop n M2 @ Decided K # M1))) = Suc (count_decided M1)› using Suc(2) count_decided_ge_get_maximum_level[of ‹drop n M2 @ Decided K # M1› ‹(remove1_mset (- lit_of (M2 ! n)) (negate_ann_lits (drop n M2 @ Decided K # M1)))›] by (auto simp: negate_ann_lits_def tr max_def ac_simps remove1_mset_add_mset_If get_maximum_level_add_mset split: if_splits) moreover have ‹lit_of (M2 ! n) ∈# mark_of (M2 ! n)› using mark[of n] Suc by auto moreover have ‹(remove1_mset (- lit_of (M2 ! n)) (negate_ann_lits (drop n M2 @ Decided K # M1)) ∪# (mark_of (M2 ! n) - unmark (M2 ! n))) = negate_ann_lits (drop (Suc n) (trail S))› apply (rule distinct_set_mset_eq) using n_d_n[of n] n_d_n[of ‹Suc n›] no_dup_distinct_mset[OF n_d_n[of n]] Suc mark[of n] mark_dist[of n] by (auto simp: tr Cons_nth_drop_Suc[symmetric, of n] entails_CNot_negate_ann_lits dest: in_diffD intro: distinct_mset_minus) moreover { have 1: ‹(tl_trail (reduce_trail_to (drop n M2 @ Decided K # M1) S)) ∼ (reduce_trail_to (drop (Suc n) M2 @ Decided K # M1) S)› apply (subst Cons_nth_drop_Suc[symmetric, of n M2]) subgoal using Suc by (auto simp: tl_trail_update_conflicting) subgoal apply (rule state_eq_trans) apply simp apply (cases ‹length (M2 ! n # drop (Suc n) M2 @ Decided K # M1) < length (trail S)›) apply (auto simp: tl_trail_reduce_trail_to_cons tr) done done have ‹update_conflicting (Some (negate_ann_lits (drop (Suc n) M2 @ Decided K # M1))) (reduce_trail_to (drop (Suc n) M2 @ Decided K # M1) S) ∼ update_conflicting (Some (negate_ann_lits (drop (Suc n) M2 @ Decided K # M1))) (tl_trail (update_conflicting (Some (negate_ann_lits (drop n M2 @ Decided K # M1))) (reduce_trail_to (drop n M2 @ Decided K # M1) S)))› apply (rule state_eq_trans) prefer 2 apply (rule update_conflicting_state_eq) apply (rule tl_trail_update_conflicting[THEN state_eq_sym[THEN iffD1]]) apply (subst state_eq_sym) apply (subst update_conflicting_update_conflicting) apply (rule 1) by fast } ultimately have ‹resolve (?T n) (?T (n+1))› apply - apply (rule resolve.intros[of _ ‹lit_of (M2 ! n)› ‹mark_of (M2 ! n)›]) using Suc get_all_ann_decomposition_backtrack_split[THEN iffD1, OF 1(1)] in_get_all_ann_decomposition_trail_update_trail[of ‹Decided K› M1 ‹M2› ‹S›] by (auto simp: tr trail_reduce_trail_to_drop hd_drop_conv_nth intro!: resolve.intros intro: update_conflicting_state_eq) then show ?case using Suc by (auto simp add: tr) qed have ‹get_maximum_level (Decided K # M1) (DECO_clause M1) = get_maximum_level M1 (DECO_clause M1)› by (rule get_maximum_level_cong) (use n_d in ‹auto simp: tr get_level_cons_if atm_of_eq_atm_of DECO_clause_def Decided_Propagated_in_iff_in_lits_of_l lits_of_def›) also have ‹... = count_decided M1› using n_d unfolding tr apply - apply (induction M1 rule: ann_lit_list_induct) subgoal by auto subgoal for L M1' apply (subgoal_tac ‹∀La∈#DECO_clause M1'. get_level (Decided L # M1') La = get_level M1' La›) subgoal using count_decided_ge_get_maximum_level[of ‹M1'› ‹DECO_clause M1'›] get_maximum_level_cong[of ‹DECO_clause M1'› ‹Decided L # M1'› ‹M1'›] by (auto simp: get_maximum_level_add_mset tr atm_of_eq_atm_of max_def) subgoal by (auto simp: DECO_clause_def get_level_cons_if atm_of_eq_atm_of Decided_Propagated_in_iff_in_lits_of_l lits_of_def) done subgoal for L C M1' apply (subgoal_tac ‹∀La∈#DECO_clause M1'. get_level (Propagated L C # M1') La = get_level M1' La›) subgoal using count_decided_ge_get_maximum_level[of ‹M1'› ‹DECO_clause M1'›] get_maximum_level_cong[of ‹DECO_clause M1'› ‹Propagated L C # M1'› ‹M1'›] by (auto simp: get_maximum_level_add_mset tr atm_of_eq_atm_of max_def) subgoal by (auto simp: DECO_clause_def get_level_cons_if atm_of_eq_atm_of Decided_Propagated_in_iff_in_lits_of_l lits_of_def) done done finally have max: ‹get_maximum_level (Decided K # M1) (DECO_clause M1) = count_decided M1› . have ‹trail S ⊨as CNot (negate_ann_lits (trail S))› by (auto simp: true_annots_true_cls_def_iff_negation_in_model negate_ann_lits_def lits_of_def) then have ‹clauses S + (enc_weight_opt.conflicting_clss S) ⊨pm DECO_clause (trail S)› unfolding DECO_clause_def apply - apply (rule all_decomposition_implies_conflict_DECO_clause[OF decomp_imp, of ‹negate_ann_lits (trail S)›]) using 1 by auto have neg: ‹trail S ⊨as CNot (mset (map (uminus o lit_of) (trail S)))› by (auto simp: true_annots_true_cls_def_iff_negation_in_model lits_of_def) have ent: ‹clauses S + enc_weight_opt.conflicting_clss S ⊨pm DECO_clause (trail S)› unfolding DECO_clause_def by (rule all_decomposition_implies_conflict_DECO_clause[OF decomp_imp, of ‹mset (map (uminus o lit_of) (trail S))›]) (use neg 1 in ‹auto simp: negate_ann_lits_def›) have deco: ‹DECO_clause (M2 @ Decided K # M1) = add_mset (- K) (DECO_clause M1)› by (auto simp: DECO_clause_def) have eg: ‹reduce_trail_to M1 (reduce_trail_to (Decided K # M1) S) ∼ reduce_trail_to M1 S› apply (subst reduce_trail_to_compow_tl_trail_le) apply (solves ‹auto simp: tr›) apply (subst (3)reduce_trail_to_compow_tl_trail_le) apply (solves ‹auto simp: tr›) apply (auto simp: tr) apply (cases ‹M2 = []›) apply (auto simp: reduce_trail_to_compow_tl_trail_le reduce_trail_to_compow_tl_trail_eq tr) done have U: ‹cons_trail (Propagated (- K) (DECO_clause (M2 @ Decided K # M1))) (add_learned_cls (DECO_clause (M2 @ Decided K # M1)) (reduce_trail_to M1 S)) ∼ cons_trail (Propagated (- K) (add_mset (- K) (DECO_clause M1))) (reduce_trail_to M1 (add_learned_cls (add_mset (- K) (DECO_clause M1)) (update_conflicting None (update_conflicting (Some (add_mset (- K) (negate_ann_lits M1))) (reduce_trail_to (Decided K # M1) S)))))› unfolding deco apply (rule cons_trail_state_eq) apply (rule state_eq_trans) prefer 2 apply (rule state_eq_sym[THEN iffD1]) apply (rule reduce_trail_to_add_learned_cls_state_eq) apply (solves ‹auto simp: tr›) apply (rule add_learned_cls_state_eq) apply (rule state_eq_trans) prefer 2 apply (rule state_eq_sym[THEN iffD1]) apply (rule reduce_trail_to_update_conflicting_state_eq) apply (solves ‹auto simp: tr›) apply (rule state_eq_trans) prefer 2 apply (rule state_eq_sym[THEN iffD1]) apply (rule update_conflicting_state_eq) apply (rule reduce_trail_to_update_conflicting_state_eq) apply (solves ‹auto simp: tr›) apply (rule state_eq_trans) prefer 2 apply (rule state_eq_sym[THEN iffD1]) apply (rule update_conflicting_update_conflicting) apply (rule eg) apply (rule state_eq_trans) prefer 2 apply (rule state_eq_sym[THEN iffD1]) apply (rule update_conflicting_itself) by (use 1 in auto) have bt: ‹enc_weight_opt.obacktrack (?T (length M2)) U› apply (rule enc_weight_opt.obacktrack.intros[of _ ‹-K› ‹negate_ann_lits M1› K M1 ‹[]› ‹DECO_clause M1› ‹count_decided M1›]) subgoal by (auto simp: tr) subgoal by (auto simp: tr) subgoal by (auto simp: tr) subgoal using count_decided_ge_get_maximum_level[of ‹Decided K # M1› ‹DECO_clause M1›] by (auto simp: tr get_maximum_level_add_mset max_def) subgoal using max by (auto simp: tr) subgoal by (auto simp: tr) subgoal by (auto simp: DECO_clause_def negate_ann_lits_def image_mset_subseteq_mono) subgoal using ent by (auto simp: tr DECO_clause_def) subgoal apply (rule state_eq_trans [OF 1(4)]) using 1(4) U by (auto simp: tr) done show ?thesis using confl res[of ‹length M2›, simplified] bt by blast qed inductive conflict_opt0 :: ‹'st ⇒ 'st ⇒ bool› where ‹conflict_opt0 S T› if ‹count_decided (trail S) = 0› and ‹negate_ann_lits (trail S) ∈# enc_weight_opt.conflicting_clss S› and ‹conflicting S = None› and ‹T ∼ update_conflicting (Some {#}) (reduce_trail_to ([] :: ('v, 'v clause) ann_lits) S)› inductive_cases conflict_opt0E: ‹conflict_opt0 S T› inductive cdcl_dpll_bnb_r :: ‹'st ⇒ 'st ⇒ bool› for S :: 'st where cdcl_conflict: ‹conflict S S' ⟹ cdcl_dpll_bnb_r S S'› | cdcl_propagate: ‹propagate S S' ⟹ cdcl_dpll_bnb_r S S'› | cdcl_improve: ‹enc_weight_opt.improvep S S' ⟹ cdcl_dpll_bnb_r S S'› | cdcl_conflict_opt0: ‹conflict_opt0 S S' ⟹ cdcl_dpll_bnb_r S S'› | cdcl_simple_backtrack_conflict_opt: ‹simple_backtrack_conflict_opt S S' ⟹ cdcl_dpll_bnb_r S S'› | cdcl_o': ‹ocdcl_W_o_r S S' ⟹ cdcl_dpll_bnb_r S S'› inductive cdcl_dpll_bnb_r_stgy :: ‹'st ⇒ 'st ⇒ bool› for S :: 'st where cdcl_dpll_bnb_r_conflict: ‹conflict S S' ⟹ cdcl_dpll_bnb_r_stgy S S'› | cdcl_dpll_bnb_r_propagate: ‹propagate S S' ⟹ cdcl_dpll_bnb_r_stgy S S'› | cdcl_dpll_bnb_r_improve: ‹enc_weight_opt.improvep S S' ⟹ cdcl_dpll_bnb_r_stgy S S'› | cdcl_dpll_bnb_r_conflict_opt0: ‹conflict_opt0 S S' ⟹ cdcl_dpll_bnb_r_stgy S S'› | cdcl_dpll_bnb_r_simple_backtrack_conflict_opt: ‹simple_backtrack_conflict_opt S S' ⟹ cdcl_dpll_bnb_r_stgy S S'› | cdcl_dpll_bnb_r_other': ‹ocdcl_W_o_r S S' ⟹ no_confl_prop_impr S ⟹ cdcl_dpll_bnb_r_stgy S S'› lemma no_dup_dropI: ‹no_dup M ⟹ no_dup (drop n M)› by (cases ‹n < length M›) (auto simp: no_dup_def drop_map[symmetric]) lemma tranclp_resolve_state_eq_compatible: ‹resolve⁺⁺ S T ⟹T ∼ T' ⟹ resolve⁺⁺ S T'› apply (induction arbitrary: T' rule: tranclp_induct) apply (auto dest: resolve_state_eq_compatible) by (metis resolve_state_eq_compatible state_eq_ref tranclp_into_rtranclp tranclp_unfold_end) lemma conflict_opt0_state_eq_compatible: ‹conflict_opt0 S T ⟹ S ∼ S' ⟹ T ∼ T' ⟹ conflict_opt0 S' T'› using state_eq_trans[of T' T ‹update_conflicting (Some {#}) (reduce_trail_to ([]::('v,'v clause) ann_lits) S)›] using state_eq_trans[of T ‹update_conflicting (Some {#}) (reduce_trail_to ([]::('v,'v clause) ann_lits) S)› ‹update_conflicting (Some {#}) (reduce_trail_to ([]::('v,'v clause) ann_lits) S')›] update_conflicting_state_eq[of S S' ‹Some {#}›] apply (auto simp: conflict_opt0.simps state_eq_sym) using reduce_trail_to_state_eq state_eq_trans update_conflicting_state_eq by blast lemma conflict_opt0_conflict_opt: assumes ‹conflict_opt0 S U› and inv: ‹cdcl_W_restart_mset.cdcl_W_all_struct_inv (enc_weight_opt.abs_state S)› shows ‹∃T. enc_weight_opt.conflict_opt S T ∧ resolve^*^* T U› proof - have 1: ‹count_decided (trail S) = 0› and neg: ‹negate_ann_lits (trail S) ∈# enc_weight_opt.conflicting_clss S› and confl: ‹conflicting S = None› and U: ‹U ∼ update_conflicting (Some {#}) (reduce_trail_to ([]::('v,'v clause)ann_lits) S)› using assms by (auto elim: conflict_opt0E) let ?T = ‹update_conflicting (Some (negate_ann_lits (trail S))) S› have confl: ‹enc_weight_opt.conflict_opt S ?T› using neg confl by (auto simp: enc_weight_opt.conflict_opt.simps) let ?T = ‹λn. update_conflicting (Some (negate_ann_lits (drop n (trail S)))) (reduce_trail_to (drop n (trail S)) S)› have proped_M2: ‹is_proped (trail S ! n)› if ‹n < length (trail S)› for n using 1 that by (auto simp: count_decided_0_iff is_decided_no_proped_iff) have n_d: ‹no_dup (trail S)› and le: ‹cdcl_W_restart_mset.cdcl_W_conflicting (enc_weight_opt.abs_state S)› and dist: ‹cdcl_W_restart_mset.distinct_cdcl_W_state (enc_weight_opt.abs_state S)› and decomp_imp: ‹all_decomposition_implies_m (clauses S + (enc_weight_opt.conflicting_clss S)) (get_all_ann_decomposition (trail S))› and learned: ‹cdcl_W_restart_mset.cdcl_W_learned_clause (enc_weight_opt.abs_state S)› using inv unfolding cdcl_W_restart_mset.cdcl_W_all_struct_inv_def cdcl_W_restart_mset.cdcl_W_M_level_inv_def by auto have proped: ‹⋀L mark a b. a @ Propagated L mark # b = trail S ⟶ b ⊨as CNot (remove1_mset L mark) ∧ L ∈# mark› using le unfolding cdcl_W_restart_mset.cdcl_W_conflicting_def by auto have [simp]: ‹count_decided (drop n (trail S)) = 0› for n using 1 unfolding count_decided_0_iff by (cases ‹n < length (trail S)›) (auto dest: in_set_dropD) have [simp]: ‹get_maximum_level (drop n (trail S)) C = 0› for n C using count_decided_ge_get_maximum_level[of ‹drop n (trail S)› C] by auto have mark_dist: ‹distinct_mset (mark_of (trail S!n))› if ‹n < length (trail S)› for n using dist that proped_M2[OF that] nth_mem[OF that] unfolding cdcl_W_restart_mset.distinct_cdcl_W_state_def by (cases ‹trail S!n›) auto have res: ‹resolve (?T n) (?T (Suc n))› if ‹n < length (trail S)› for n proof - define L and E where ‹L = lit_of (trail S ! n)› and ‹E = mark_of (trail S ! n)› have ‹hd (drop n (trail S)) = Propagated L E› and tr_Sn: ‹trail S ! n = Propagated L E› using proped_M2[OF that] by (cases ‹trail S ! n›; auto simp: that hd_drop_conv_nth L_def E_def; fail)+ have ‹L ∈# E› and ent_E: ‹drop (Suc n) (trail S) ⊨as CNot (remove1_mset L E)› using proped[of ‹take n (trail S)› L E ‹drop (Suc n) (trail S)›] that unfolding tr_Sn[symmetric] by (auto simp: Cons_nth_drop_Suc) have 1: ‹negate_ann_lits (drop (Suc n) (trail S)) = (remove1_mset (- L) (negate_ann_lits (drop n (trail S))) ∪# remove1_mset L E)› apply (subst distinct_set_mset_eq_iff[symmetric]) subgoal using n_d by (auto simp: no_dup_dropI) subgoal using n_d mark_dist[OF that] unfolding tr_Sn by (auto intro: distinct_mset_mono no_dup_dropI intro!: distinct_mset_minus) subgoal using ent_E unfolding tr_Sn[symmetric] by (auto simp: negate_ann_lits_def that Cons_nth_drop_Suc[symmetric] L_def lits_of_def true_annots_true_cls_def_iff_negation_in_model uminus_lit_swap dest!: multi_member_split) done have ‹update_conflicting (Some (negate_ann_lits (drop (Suc n) (trail S)))) (reduce_trail_to (drop (Suc n) (trail S)) S) ∼ update_conflicting (Some (remove1_mset (- L) (negate_ann_lits (drop n (trail S))) ∪# remove1_mset L E)) (tl_trail (update_conflicting (Some (negate_ann_lits (drop n (trail S)))) (reduce_trail_to (drop n (trail S)) S)))› unfolding 1[symmetric] apply (rule state_eq_trans) prefer 2 apply (rule state_eq_sym[THEN iffD1]) apply (rule update_conflicting_state_eq) apply (rule tl_trail_update_conflicting) apply (rule state_eq_trans) prefer 2 apply (rule state_eq_sym[THEN iffD1]) apply (rule update_conflicting_update_conflicting) apply (rule state_eq_ref) apply (rule update_conflicting_state_eq) using that by (auto simp: reduce_trail_to_compow_tl_trail funpow_swap1) moreover have ‹L ∈# E› using proped[of ‹take n (trail S)› L E ‹drop (Suc n) (trail S)›] that unfolding tr_Sn[symmetric] by (auto simp: Cons_nth_drop_Suc) moreover have ‹- L ∈# negate_ann_lits (drop n (trail S))› by (auto simp: negate_ann_lits_def L_def in_set_dropI that) term ‹get_maximum_level (drop n (trail S))› ultimately show ?thesis apply - by (rule resolve.intros[of _ L E]) (use that in ‹auto simp: trail_reduce_trail_to_drop ‹hd (drop n (trail S)) = Propagated L E››) qed have ‹resolve^*^* (?T 0) (?T n)› if ‹n ≤ length (trail S)› for n using that apply (induction n) subgoal by auto subgoal for n using res[of n] by auto done from this[of ‹length (trail S)›] have ‹resolve^*^* (?T 0) (?T (length (trail S)))› by auto moreover have ‹?T (length (trail S)) ∼ U› apply (rule state_eq_trans) prefer 2 apply (rule state_eq_sym[THEN iffD1], rule U) by auto moreover have False if ‹(?T 0) = (?T (length (trail S)))› and ‹length (trail S) > 0› using arg_cong[OF that(1), of conflicting] that(2) by (auto simp: negate_ann_lits_def) ultimately have ‹length (trail S) > 0 ⟶ resolve^*^* (?T 0) U› using tranclp_resolve_state_eq_compatible[of ‹?T 0› ‹?T (length (trail S))› U] by (subst (asm) rtranclp_unfold) auto then have ?thesis if ‹length (trail S) > 0› using confl that by auto moreover have ?thesis if ‹length (trail S) = 0› using that confl U enc_weight_opt.conflict_opt_state_eq_compatible[of S ‹(update_conflicting (Some {#}) S)› S U] by (auto simp: state_eq_sym) ultimately show ?thesis by blast qed lemma backtrack_split_some_is_decided_then_snd_has_hd2: ‹∃l∈set M. is_decided l ⟹ ∃M' L' M''. backtrack_split M = (M'', Decided L' # M')› by (metis backtrack_split_snd_hd_decided backtrack_split_some_is_decided_then_snd_has_hd is_decided_def list.distinct(1) list.sel(1) snd_conv) lemma no_step_conflict_opt0_simple_backtrack_conflict_opt: ‹no_step conflict_opt0 S ⟹ no_step simple_backtrack_conflict_opt S ⟹ no_step enc_weight_opt.conflict_opt S› using backtrack_split_some_is_decided_then_snd_has_hd2[of ‹trail S›] count_decided_0_iff[of ‹trail S›] by (fastforce simp: conflict_opt0.simps simple_backtrack_conflict_opt.simps enc_weight_opt.conflict_opt.simps annotated_lit.is_decided_def) lemma no_step_cdcl_dpll_bnb_r_cdcl_bnb_r: assumes ‹cdcl_W_restart_mset.cdcl_W_all_struct_inv (enc_weight_opt.abs_state S)› shows ‹no_step cdcl_dpll_bnb_r S ⟷ no_step cdcl_bnb_r S› (is ‹?A ⟷ ?B›) proof assume ?A show ?B using ‹?A› no_step_conflict_opt0_simple_backtrack_conflict_opt[of S] by (auto simp: cdcl_bnb_r.simps cdcl_dpll_bnb_r.simps all_conj_distrib) next assume ?B show ?A using ‹?B› simple_backtrack_conflict_opt_conflict_analysis[OF _ assms] by (auto simp: cdcl_bnb_r.simps cdcl_dpll_bnb_r.simps all_conj_distrib assms dest!: conflict_opt0_conflict_opt) qed lemma cdcl_dpll_bnb_r_cdcl_bnb_r: assumes ‹cdcl_dpll_bnb_r S T› and ‹cdcl_W_restart_mset.cdcl_W_all_struct_inv (enc_weight_opt.abs_state S)› shows ‹cdcl_bnb_r^*^* S T› using assms proof (cases rule: cdcl_dpll_bnb_r.cases) case cdcl_simple_backtrack_conflict_opt then obtain S1 S2 where ‹enc_weight_opt.conflict_opt S S1› ‹resolve^*^* S1 S2› and ‹enc_weight_opt.obacktrack S2 T› using simple_backtrack_conflict_opt_conflict_analysis[OF _ assms(2), of T] by auto then have ‹cdcl_bnb_r S S1› ‹cdcl_bnb_r^*^* S1 S2› ‹cdcl_bnb_r S2 T› using mono_rtranclp[of resolve enc_weight_opt.cdcl_bnb_bj] mono_rtranclp[of enc_weight_opt.cdcl_bnb_bj ocdcl_W_o_r] mono_rtranclp[of ocdcl_W_o_r cdcl_bnb_r] ocdcl_W_o_r.intros enc_weight_opt.cdcl_bnb_bj.resolve cdcl_bnb_r.intros enc_weight_opt.cdcl_bnb_bj.intros by (auto 5 4 dest: cdcl_bnb_r.intros conflict_opt0_conflict_opt) then show ?thesis by auto next case cdcl_conflict_opt0 then obtain S1 where ‹enc_weight_opt.conflict_opt S S1› ‹resolve^*^* S1 T› using conflict_opt0_conflict_opt[OF _ assms(2), of T] by auto then have ‹cdcl_bnb_r S S1› ‹cdcl_bnb_r^*^* S1 T› using mono_rtranclp[of resolve enc_weight_opt.cdcl_bnb_bj] mono_rtranclp[of enc_weight_opt.cdcl_bnb_bj ocdcl_W_o_r] mono_rtranclp[of ocdcl_W_o_r cdcl_bnb_r] ocdcl_W_o_r.intros enc_weight_opt.cdcl_bnb_bj.resolve cdcl_bnb_r.intros enc_weight_opt.cdcl_bnb_bj.intros by (auto 5 4 dest: cdcl_bnb_r.intros conflict_opt0_conflict_opt) then show ?thesis by auto qed (auto 5 4 dest: cdcl_bnb_r.intros conflict_opt0_conflict_opt simp: assms) lemma resolve_no_prop_confl: ‹resolve S T ⟹ no_step propagate S ∧ no_step conflict S› by (auto elim!: rulesE) lemma cdcl_bnb_r_stgy_res: ‹resolve S T ⟹ cdcl_bnb_r_stgy S T› using enc_weight_opt.cdcl_bnb_bj.resolve[of S T] ocdcl_W_o_r.intros[of S T] cdcl_bnb_r_stgy.intros[of S T] resolve_no_prop_confl[of S T] by (auto 5 4 dest: cdcl_bnb_r_stgy.intros conflict_opt0_conflict_opt) lemma rtranclp_cdcl_bnb_r_stgy_res: ‹resolve^*^* S T ⟹ cdcl_bnb_r_stgy^*^* S T› using mono_rtranclp[of resolve cdcl_bnb_r_stgy] cdcl_bnb_r_stgy_res by (auto) lemma obacktrack_no_prop_confl: ‹enc_weight_opt.obacktrack S T ⟹ no_step propagate S ∧ no_step conflict S› by (auto elim!: rulesE enc_weight_opt.obacktrackE) lemma cdcl_bnb_r_stgy_bt: ‹enc_weight_opt.obacktrack S T ⟹ cdcl_bnb_r_stgy S T› using enc_weight_opt.cdcl_bnb_bj.backtrack[of S T] ocdcl_W_o_r.intros[of S T] cdcl_bnb_r_stgy.intros[of S T] obacktrack_no_prop_confl[of S T] by (auto 5 4 dest: cdcl_bnb_r_stgy.intros conflict_opt0_conflict_opt) lemma cdcl_dpll_bnb_r_stgy_cdcl_bnb_r_stgy: assumes ‹cdcl_dpll_bnb_r_stgy S T› and ‹cdcl_W_restart_mset.cdcl_W_all_struct_inv (enc_weight_opt.abs_state S)› shows ‹cdcl_bnb_r_stgy^*^* S T› using assms proof (cases rule: cdcl_dpll_bnb_r_stgy.cases) case cdcl_dpll_bnb_r_simple_backtrack_conflict_opt then obtain S1 S2 where ‹enc_weight_opt.conflict_opt S S1› ‹resolve^*^* S1 S2› and ‹enc_weight_opt.obacktrack S2 T› using simple_backtrack_conflict_opt_conflict_analysis[OF _ assms(2), of T] by auto then have ‹cdcl_bnb_r_stgy S S1› ‹cdcl_bnb_r_stgy^*^* S1 S2› ‹cdcl_bnb_r_stgy S2 T› using enc_weight_opt.cdcl_bnb_bj.resolve by (auto dest: cdcl_bnb_r_stgy.intros conflict_opt0_conflict_opt rtranclp_cdcl_bnb_r_stgy_res cdcl_bnb_r_stgy_bt) then show ?thesis by auto next case cdcl_dpll_bnb_r_conflict_opt0 then obtain S1 where ‹enc_weight_opt.conflict_opt S S1› ‹resolve^*^* S1 T› using conflict_opt0_conflict_opt[OF _ assms(2), of T] by auto then have ‹cdcl_bnb_r_stgy S S1› ‹cdcl_bnb_r_stgy^*^* S1 T› using enc_weight_opt.cdcl_bnb_bj.resolve by (auto dest: cdcl_bnb_r_stgy.intros conflict_opt0_conflict_opt rtranclp_cdcl_bnb_r_stgy_res cdcl_bnb_r_stgy_bt) then show ?thesis by auto qed (auto 5 4 dest: cdcl_bnb_r_stgy.intros conflict_opt0_conflict_opt) lemma cdcl_bnb_r_stgy_cdcl_bnb_r: ‹cdcl_bnb_r_stgy S T ⟹ cdcl_bnb_r S T› by (auto simp: cdcl_bnb_r_stgy.simps cdcl_bnb_r.simps) lemma rtranclp_cdcl_bnb_r_stgy_cdcl_bnb_r: ‹cdcl_bnb_r_stgy^*^* S T ⟹ cdcl_bnb_r^*^* S T› by (induction rule: rtranclp_induct) (auto dest: cdcl_bnb_r_stgy_cdcl_bnb_r) context fixes S :: 'st assumes S_Σ: ‹atms_of_mm (init_clss S) = Σ - ΔΣ ∪ replacement_pos ` ΔΣ ∪ replacement_neg ` ΔΣ› begin lemma cdcl_dpll_bnb_r_stgy_all_struct_inv: ‹cdcl_dpll_bnb_r_stgy S T ⟹ cdcl_W_restart_mset.cdcl_W_all_struct_inv (enc_weight_opt.abs_state S) ⟹ cdcl_W_restart_mset.cdcl_W_all_struct_inv (enc_weight_opt.abs_state T)› using cdcl_dpll_bnb_r_stgy_cdcl_bnb_r_stgy[of S T] rtranclp_cdcl_bnb_r_all_struct_inv[OF S_Σ] rtranclp_cdcl_bnb_r_stgy_cdcl_bnb_r[of S T] by auto end lemma cdcl_bnb_r_stgy_cdcl_dpll_bnb_r_stgy: ‹cdcl_bnb_r_stgy S T ⟹ ∃T. cdcl_dpll_bnb_r_stgy S T› by (meson cdcl_bnb_r_stgy.simps cdcl_dpll_bnb_r_conflict cdcl_dpll_bnb_r_conflict_opt0 cdcl_dpll_bnb_r_other' cdcl_dpll_bnb_r_propagate cdcl_dpll_bnb_r_simple_backtrack_conflict_opt cdcl_dpll_bnb_r_stgy.intros(3) no_step_conflict_opt0_simple_backtrack_conflict_opt) context fixes S :: 'st assumes S_Σ: ‹atms_of_mm (init_clss S) = Σ - ΔΣ ∪ replacement_pos ` ΔΣ ∪ replacement_neg ` ΔΣ› begin lemma rtranclp_cdcl_dpll_bnb_r_stgy_cdcl_bnb_r: assumes ‹cdcl_dpll_bnb_r_stgy^*^* S T› and ‹cdcl_W_restart_mset.cdcl_W_all_struct_inv (enc_weight_opt.abs_state S)› shows ‹cdcl_bnb_r_stgy^*^* S T› using assms apply (induction rule: rtranclp_induct) subgoal by auto subgoal for T U using cdcl_dpll_bnb_r_stgy_cdcl_bnb_r_stgy[of T U] rtranclp_cdcl_bnb_r_all_struct_inv[OF S_Σ, of T] rtranclp_cdcl_bnb_r_stgy_cdcl_bnb_r[of S T] by auto done lemma rtranclp_cdcl_dpll_bnb_r_stgy_all_struct_inv: ‹cdcl_dpll_bnb_r_stgy^*^* S T ⟹ cdcl_W_restart_mset.cdcl_W_all_struct_inv (enc_weight_opt.abs_state S) ⟹ cdcl_W_restart_mset.cdcl_W_all_struct_inv (enc_weight_opt.abs_state T)› using rtranclp_cdcl_dpll_bnb_r_stgy_cdcl_bnb_r[of T] rtranclp_cdcl_bnb_r_all_struct_inv[OF S_Σ, of T] rtranclp_cdcl_bnb_r_stgy_cdcl_bnb_r[of S T] by auto lemma full_cdcl_dpll_bnb_r_stgy_full_cdcl_bnb_r_stgy: assumes ‹full cdcl_dpll_bnb_r_stgy S T› and ‹cdcl_W_restart_mset.cdcl_W_all_struct_inv (enc_weight_opt.abs_state S)› shows ‹full cdcl_bnb_r_stgy S T› using no_step_cdcl_dpll_bnb_r_cdcl_bnb_r[of T] rtranclp_cdcl_dpll_bnb_r_stgy_cdcl_bnb_r[of T] rtranclp_cdcl_dpll_bnb_r_stgy_all_struct_inv[of T] assms rtranclp_cdcl_bnb_r_stgy_cdcl_bnb_r[of S T] by (auto simp: full_def dest: cdcl_bnb_r_stgy_cdcl_bnb_r cdcl_bnb_r_stgy_cdcl_dpll_bnb_r_stgy) end lemma replace_pos_neg_not_both_decided_highest_lvl: assumes struct: ‹cdcl_W_restart_mset.cdcl_W_all_struct_inv (enc_weight_opt.abs_state S)› and smaller_propa: ‹no_smaller_propa S› and smaller_confl: ‹no_smaller_confl S› and dec0: ‹Pos (A^↦⁰) ∈ lits_of_l (trail S)› and dec1: ‹Pos (A^↦¹) ∈ lits_of_l (trail S)› and add: ‹additional_constraints ⊆# init_clss S› and [simp]: ‹A ∈ ΔΣ› shows ‹get_level (trail S) (Pos (A^↦⁰)) = backtrack_lvl S ∧ get_level (trail S) (Pos (A^↦¹)) = backtrack_lvl S› proof (rule ccontr) assume neg: ‹¬?thesis› let ?L0 = ‹get_level (trail S) (Pos (A^↦⁰))› let ?L1 = ‹get_level (trail S) (Pos (A^↦¹))› define KL where ‹KL = (if ?L0 > ?L1 then (Pos (A^↦¹)) else (Pos (A^↦⁰)))› define KL' where ‹KL' = (if ?L0 > ?L1 then (Pos (A^↦⁰)) else (Pos (A^↦¹)))› then have ‹get_level (trail S) KL < backtrack_lvl S› and le: ‹?L0 < backtrack_lvl S ∨ ?L1 < backtrack_lvl S› ‹?L0 ≤ backtrack_lvl S ∧ ?L1 ≤ backtrack_lvl S› using neg count_decided_ge_get_level[of ‹trail S› ‹Pos (A^↦⁰)›] count_decided_ge_get_level[of ‹trail S› ‹Pos (A^↦¹)›] unfolding KL_def by force+ have ‹KL ∈ lits_of_l (trail S)› using dec1 dec0 by (auto simp: KL_def) have add: ‹additional_constraint A ⊆# init_clss S› using add multi_member_split[of A ‹mset_set ΔΣ›] by (auto simp: additional_constraints_def subset_mset.dual_order.trans) have n_d: ‹no_dup (trail S)› using struct unfolding cdcl_W_restart_mset.cdcl_W_all_struct_inv_def cdcl_W_restart_mset.cdcl_W_M_level_inv_def by auto have H: ‹⋀M K M' D L. trail S = M' @ Decided K # M ⟹ D + {#L#} ∈# additional_constraint A ⟹ undefined_lit M L ⟹ ¬ M ⊨as CNot D› and H': ‹⋀M K M' D L. trail S = M' @ Decided K # M ⟹ D ∈# additional_constraint A ⟹ ¬ M ⊨as CNot D› using smaller_propa add smaller_confl unfolding no_smaller_propa_def no_smaller_confl_def clauses_def by auto have L1_L0: ‹?L1 = ?L0› proof (rule ccontr) assume neq: ‹?L1 ≠ ?L0› define i where ‹i ≡ min ?L1 ?L0› obtain K M1 M2 where decomp: ‹(Decided K # M1, M2) ∈ set (get_all_ann_decomposition (trail S))› and ‹get_level (trail S) K = Suc i› using backtrack_ex_decomp[OF n_d, of i] neq le by (cases ‹?L1 < ?L0›) (auto simp: min_def i_def) have ‹get_level (trail S) KL ≤ i› and ‹get_level (trail S) KL' > i› using neg neq le by (auto simp: KL_def KL'_def i_def) then have ‹undefined_lit M1 KL'› using n_d decomp ‹get_level (trail S) K = Suc i› count_decided_ge_get_level[of ‹M1› KL'] by (force dest!: get_all_ann_decomposition_exists_prepend simp: get_level_append_if get_level_cons_if atm_of_eq_atm_of dest: defined_lit_no_dupD split: if_splits) moreover have ‹{#-KL', -KL#} ∈# additional_constraint A› using neq by (auto simp: additional_constraint_def KL_def KL'_def) moreover have ‹KL ∈ lits_of_l M1› using ‹get_level (trail S) KL ≤ i› ‹get_level (trail S) K = Suc i› n_d decomp ‹KL ∈ lits_of_l (trail S)› count_decided_ge_get_level[of ‹M1› KL] by (auto dest!: get_all_ann_decomposition_exists_prepend simp: get_level_append_if get_level_cons_if atm_of_eq_atm_of dest: defined_lit_no_dupD in_lits_of_l_defined_litD split: if_splits) ultimately show False using H[of _ K M1 ‹{#-KL#}› ‹-KL'›] decomp by force qed obtain K M1 M2 where decomp: ‹(Decided K # M1, M2) ∈ set (get_all_ann_decomposition (trail S))› and lev_K: ‹get_level (trail S) K = Suc ?L1› using backtrack_ex_decomp[OF n_d, of ?L1] le by (cases ‹?L1 < ?L0›) (auto simp: min_def L1_L0) then obtain M3 where M3: ‹trail S = M3 @ Decided K # M1› by auto then have [simp]: ‹undefined_lit M3 (Pos (A^↦¹))› ‹undefined_lit M3 (Pos (A^↦⁰))› by (solves ‹use n_d L1_L0 lev_K M3 in auto›) (solves ‹use n_d L1_L0[symmetric] lev_K M3 in auto›) then have [simp]: ‹Pos (A^↦⁰) ∉ lits_of_l M3› ‹Pos (A^↦¹) ∉ lits_of_l M3› using Decided_Propagated_in_iff_in_lits_of_l by blast+ have ‹Pos (A^↦¹) ∈ lits_of_l M1› ‹Pos (A^↦⁰) ∈ lits_of_l M1› using n_d L1_L0 lev_K dec0 dec1 Decided_Propagated_in_iff_in_lits_of_l by (auto dest!: get_all_ann_decomposition_exists_prepend simp: M3 get_level_cons_if split: if_splits) then show False using H'[of M3 K M1 ‹{#Neg (A^↦⁰), Neg (A^↦¹)#}›] by (auto simp: additional_constraint_def M3) qed lemma cdcl_dpll_bnb_r_stgy_clauses_mono: ‹cdcl_dpll_bnb_r_stgy S T ⟹ clauses S ⊆# clauses T› by (cases rule: cdcl_dpll_bnb_r_stgy.cases, assumption) (auto elim!: rulesE obacktrackE enc_weight_opt.improveE conflict_opt0E simple_backtrack_conflict_optE odecideE enc_weight_opt.obacktrackE simp: ocdcl_W_o_r.simps enc_weight_opt.cdcl_bnb_bj.simps) lemma rtranclp_cdcl_dpll_bnb_r_stgy_clauses_mono: ‹cdcl_dpll_bnb_r_stgy^*^* S T ⟹ clauses S ⊆# clauses T› by (induction rule: rtranclp_induct) (auto dest!: cdcl_dpll_bnb_r_stgy_clauses_mono) lemma cdcl_dpll_bnb_r_stgy_init_clss_eq: ‹cdcl_dpll_bnb_r_stgy S T ⟹ init_clss S = init_clss T› by (cases rule: cdcl_dpll_bnb_r_stgy.cases, assumption) (auto elim!: rulesE obacktrackE enc_weight_opt.improveE conflict_opt0E simple_backtrack_conflict_optE odecideE enc_weight_opt.obacktrackE simp: ocdcl_W_o_r.simps enc_weight_opt.cdcl_bnb_bj.simps) lemma rtranclp_cdcl_dpll_bnb_r_stgy_init_clss_eq: ‹cdcl_dpll_bnb_r_stgy^*^* S T ⟹ init_clss S = init_clss T› by (induction rule: rtranclp_induct) (auto dest!: cdcl_dpll_bnb_r_stgy_init_clss_eq) context fixes S :: 'st and N :: ‹'v clauses› assumes S_Σ: ‹init_clss S = penc N› begin lemma replacement_pos_neg_defined_same_lvl: assumes struct: ‹cdcl_W_restart_mset.cdcl_W_all_struct_inv (enc_weight_opt.abs_state S)› and A: ‹A ∈ ΔΣ› and lev: ‹get_level (trail S) (Pos (replacement_pos A)) < backtrack_lvl S› and smaller_propa: ‹no_smaller_propa S› and smaller_confl: ‹cdcl_bnb_stgy_inv S› shows ‹Pos (replacement_pos A) ∈ lits_of_l (trail S) ⟹ Neg (replacement_neg A) ∈ lits_of_l (trail S)› proof - have n_d: ‹no_dup (trail S)› using struct unfolding cdcl_W_restart_mset.cdcl_W_all_struct_inv_def cdcl_W_restart_mset.cdcl_W_M_level_inv_def by auto have H: ‹⋀M K M' D L. trail S = M' @ Decided K # M ⟹ D + {#L#} ∈# additional_constraint A ⟹ undefined_lit M L ⟹ ¬ M ⊨as CNot D› and H': ‹⋀M K M' D L. trail S = M' @ Decided K # M ⟹ D ∈# additional_constraint A ⟹ ¬ M ⊨as CNot D› using smaller_propa S_Σ A smaller_confl unfolding no_smaller_propa_def clauses_def penc_def additional_constraints_def cdcl_bnb_stgy_inv_def no_smaller_confl_def by fastforce+ show ‹Neg (replacement_neg A) ∈ lits_of_l (trail S)› if Pos: ‹Pos (replacement_pos A) ∈ lits_of_l (trail S)› proof - obtain M1 M2 K where ‹trail S = M2 @ Decided K # M1› and ‹Pos (replacement_pos A) ∈ lits_of_l M1› using lev n_d Pos by (force dest!: split_list elim!: is_decided_ex_Decided simp: lits_of_def count_decided_def filter_empty_conv) then show ‹Neg (replacement_neg A) ∈ lits_of_l (trail S)› using H[of M2 K M1 ‹{#Neg (replacement_pos A)#}› ‹Neg (replacement_neg A)›] H'[of M2 K M1 ‹{#Neg (replacement_pos A), Neg (replacement_neg A)#}›] by (auto simp: additional_constraint_def Decided_Propagated_in_iff_in_lits_of_l) qed qed lemma replacement_pos_neg_defined_same_lvl': assumes struct: ‹cdcl_W_restart_mset.cdcl_W_all_struct_inv (enc_weight_opt.abs_state S)› and A: ‹A ∈ ΔΣ› and lev: ‹get_level (trail S) (Pos (replacement_neg A)) < backtrack_lvl S› and smaller_propa: ‹no_smaller_propa S› and smaller_confl: ‹cdcl_bnb_stgy_inv S› shows ‹Pos (replacement_neg A) ∈ lits_of_l (trail S) ⟹ Neg (replacement_pos A) ∈ lits_of_l (trail S)› proof - have n_d: ‹no_dup (trail S)› using struct unfolding cdcl_W_restart_mset.cdcl_W_all_struct_inv_def cdcl_W_restart_mset.cdcl_W_M_level_inv_def by auto have H: ‹⋀M K M' D L. trail S = M' @ Decided K # M ⟹ D + {#L#} ∈# additional_constraint A ⟹ undefined_lit M L ⟹ ¬ M ⊨as CNot D› and H': ‹⋀M K M' D L. trail S = M' @ Decided K # M ⟹ D ∈# additional_constraint A ⟹ ¬ M ⊨as CNot D› using smaller_propa S_Σ A smaller_confl unfolding no_smaller_propa_def clauses_def penc_def additional_constraints_def cdcl_bnb_stgy_inv_def no_smaller_confl_def by fastforce+ show ‹Neg (replacement_pos A) ∈ lits_of_l (trail S)› if Pos: ‹Pos (replacement_neg A) ∈ lits_of_l (trail S)› proof - obtain M1 M2 K where ‹trail S = M2 @ Decided K # M1› and ‹Pos (replacement_neg A) ∈ lits_of_l M1› using lev n_d Pos by (force dest!: split_list elim!: is_decided_ex_Decided simp: lits_of_def count_decided_def filter_empty_conv) then show ‹Neg (replacement_pos A) ∈ lits_of_l (trail S)› using H[of M2 K M1 ‹{#Neg (replacement_neg A)#}› ‹Neg (replacement_pos A)›] H'[of M2 K M1 ‹{#Neg (replacement_neg A), Neg (replacement_pos A)#}›] by (auto simp: additional_constraint_def Decided_Propagated_in_iff_in_lits_of_l) qed qed end definition all_new_literals :: ‹'v list› where ‹all_new_literals = (SOME xs. mset xs = mset_set (replacement_neg ` ΔΣ ∪ replacement_pos ` ΔΣ))› lemma set_all_new_literals[simp]: ‹set all_new_literals = (replacement_neg ` ΔΣ ∪ replacement_pos ` ΔΣ)› using finite_Σ apply (simp add: all_new_literals_def) apply (metis (mono_tags) ex_mset finite_Un finite_Σ finite_imageI finite_set_mset_mset_set set_mset_mset someI) done text ‹This function is basically resolving the clause with all the additional clauses term‹{#Neg (replacement_pos L), Neg (replacement_neg L)#}›.› fun resolve_with_all_new_literals :: ‹'v clause ⇒ 'v list ⇒ 'v clause› where ‹resolve_with_all_new_literals C [] = C› | ‹resolve_with_all_new_literals C (L # Ls) = remdups_mset (resolve_with_all_new_literals (if Pos L ∈# C then add_mset (Neg (opposite_var L)) (removeAll_mset (Pos L) C) else C) Ls)› abbreviation normalize2 where ‹normalize2 C ≡ resolve_with_all_new_literals C all_new_literals› lemma Neg_in_normalize2[simp]: ‹Neg L ∈# C ⟹ Neg L ∈# resolve_with_all_new_literals C xs› by (induction arbitrary: C rule: resolve_with_all_new_literals.induct) auto lemma Pos_in_normalize2D[dest]: ‹Pos L ∈# resolve_with_all_new_literals C xs ⟹ Pos L ∈# C› by (induction arbitrary: C rule: resolve_with_all_new_literals.induct) (force split: if_splits)+ lemma opposite_var_involutive[simp]: ‹L ∈ (replacement_neg ` ΔΣ ∪ replacement_pos ` ΔΣ) ⟹ opposite_var (opposite_var L) = L› by (auto simp: opposite_var_def) lemma Neg_in_resolve_with_all_new_literals_Pos_notin: ‹L ∈ (replacement_neg ` ΔΣ ∪ replacement_pos ` ΔΣ) ⟹ set xs ⊆ (replacement_neg ` ΔΣ ∪ replacement_pos ` ΔΣ) ⟹ Pos (opposite_var L) ∉# C ⟹ Neg L ∈# resolve_with_all_new_literals C xs ⟷ Neg L ∈# C› apply (induction arbitrary: C rule: resolve_with_all_new_literals.induct) apply clarsimp+ subgoal premises p using p(2-) by (auto simp del: Neg_in_normalize2 simp: eq_commute[of _ ‹opposite_var _›]) done lemma Pos_in_normalize2_Neg_notin[simp]: ‹L ∈ (replacement_neg ` ΔΣ ∪ replacement_pos ` ΔΣ) ⟹ Pos (opposite_var L) ∉# C ⟹ Neg L ∈# normalize2 C ⟷ Neg L ∈# C› by (rule Neg_in_resolve_with_all_new_literals_Pos_notin) (auto) lemma all_negation_deleted: ‹L ∈ set all_new_literals ⟹ Pos L ∉# normalize2 C› apply (induction arbitrary: C rule: resolve_with_all_new_literals.induct) subgoal by auto subgoal by (auto split: if_splits) done lemma Pos_in_resolve_with_all_new_literals_iff_already_in_or_negation_in: ‹L ∈ set all_new_literals ⟹set xs ⊆ (replacement_neg ` ΔΣ ∪ replacement_pos ` ΔΣ) ⟹ Neg L ∈# resolve_with_all_new_literals C xs⟹ Neg L ∈# C ∨ Pos (opposite_var L) ∈# C› apply (induction arbitrary: C rule: resolve_with_all_new_literals.induct) subgoal by auto subgoal premises p for C La Ls Ca using p by (auto split: if_splits dest: simp: Neg_in_resolve_with_all_new_literals_Pos_notin) done lemma Pos_in_normalize2_iff_already_in_or_negation_in: ‹L ∈ set all_new_literals ⟹ Neg L ∈# normalize2 C ⟹ Neg L ∈# C ∨ Pos (opposite_var L) ∈# C› using Pos_in_resolve_with_all_new_literals_iff_already_in_or_negation_in[of L ‹all_new_literals› C] by auto text ‹This proof makes it hard to measure progress because I currently do not see a way to distinguish between term‹add_mset (replacement_pos A) C› and term‹add_mset (replacement_pos A) (add_mset (replacement_neg A) C)›. › lemma assumes ‹enc_weight_opt.cdcl_bnb_stgy S T› and struct: ‹cdcl_W_restart_mset.cdcl_W_all_struct_inv (enc_weight_opt.abs_state S)› and dist: ‹distinct_mset (normalize_clause `# learned_clss S)› and smaller_propa: ‹no_smaller_propa S› and smaller_confl: ‹cdcl_bnb_stgy_inv S› shows ‹distinct_mset (remdups_mset (normalize2 `# learned_clss T))› using assms(1) proof (cases) case cdcl_bnb_conflict then show ?thesis using dist by (auto elim!: rulesE) next case cdcl_bnb_propagate then show ?thesis using dist by (auto elim!: rulesE) next case cdcl_bnb_improve then show ?thesis using dist by (auto elim!: enc_weight_opt.improveE) next case cdcl_bnb_conflict_opt then show ?thesis using dist by (auto elim!: enc_weight_opt.conflict_optE) next case cdcl_bnb_other' then show ?thesis proof cases case decide then show ?thesis using dist by (auto elim!: rulesE) next case bj then show ?thesis proof cases case skip then show ?thesis using dist by (auto elim!: rulesE) next case resolve then show ?thesis using dist by (auto elim!: rulesE) next case backtrack then obtain M1 M2 :: ‹('v, 'v clause) ann_lits› and K L :: ‹'v literal› and D D' :: ‹'v clause› where confl: ‹conflicting S = Some (add_mset L D)› and decomp: ‹(Decided K # M1, M2) ∈ set (get_all_ann_decomposition (trail S))› and ‹get_maximum_level (trail S) (add_mset L D') = local.backtrack_lvl S› and ‹get_level (trail S) L = local.backtrack_lvl S› and lev_K: ‹get_level (trail S) K = Suc (get_maximum_level (trail S) D')› and D'_D: ‹D' ⊆# D› and ‹set_mset (clauses S) ∪ set_mset (enc_weight_opt.conflicting_clss S) ⊨p add_mset L D'› and T: ‹T ∼ cons_trail (Propagated L (add_mset L D')) (reduce_trail_to M1 (add_learned_cls (add_mset L D') (update_conflicting None S)))› by (auto simp: enc_weight_opt.obacktrack.simps) have tr_D: ‹trail S ⊨as CNot (add_mset L D)› and ‹distinct_mset (add_mset L D)› and ‹cdcl_W_restart_mset.cdcl_W_M_level_inv (abs_state S)› and n_d: ‹no_dup (trail S)› using struct confl unfolding cdcl_W_restart_mset.cdcl_W_all_struct_inv_def cdcl_W_restart_mset.cdcl_W_conflicting_def cdcl_W_restart_mset.distinct_cdcl_W_state_def cdcl_W_restart_mset.cdcl_W_M_level_inv_def by auto have tr_D': ‹trail S ⊨as CNot (add_mset L D')› using D'_D tr_D by (auto simp: true_annots_true_cls_def_iff_negation_in_model) have ‹trail S ⊨as CNot D' ⟹ trail S ⊨as CNot (normalize2 D')› if ‹get_maximum_level (trail S) D' < backtrack_lvl S› for D' (*by induction on all the literals*) oops find_theorems get_level Pos Neg (* sorry have False if C: ‹add_mset (normalize_lit L) (normalize_clause D') = normalize_clause C› and ‹C ∈# learned_clss S› for C proof - obtain L' C' where C_L'_C'[simp]: ‹C = add_mset L' C'› and ‹normalize_clause C' = normalize_clause D'› and [simp]: ‹normalize_lit L' = normalize_lit L› using C msed_map_invR[of ‹normalize_lit› C ‹normalize_lit L› ‹normalize_clause D'›] by auto have ‹trail S ⊨as CNot C'› unfolding true_annots_true_cls_def_iff_negation_in_model proof fix A assume ‹A ∈# C'› then obtain A' where ‹A' ∈# D'› and ‹normalize_lit A' = normalize_lit A› using ‹normalize_clause C' = normalize_clause D'›[symmetric] by (force dest!: msed_map_invR multi_member_split) then have ‹- A' ∈ lits_of_l (trail S)› using tr_D' by (auto dest: multi_member_split) then have ‹-normalize_lit A' ∈ lits_of_l (trail S)› apply (cases A') apply auto sorry then show ‹- A ∈ lits_of_l (trail S)› sorry qed show False sorry qed then show ?thesis using dist T by (auto simp: enc_weight_opt.obacktrack.simps) qed qed qed *) end end

Theory CDCL_W_Partial_Optimal_Model