Theory IsaSAT

theory IsaSAT_Mark imports IsaSAT_Clauses IsaSAT_Watch_List IsaSAT_Trail begin chapter ‹Clauses Encoded as Positions› text ‹We use represent the conflict in two data structures close to the one used by the most SAT solvers: We keep an array that represent the clause (for efficient iteration on the clause) and a ``hash-table'' to efficiently test if a literal belongs to the clause. The first data structure is simply an array to represent the clause. This theory is only about the second data structure. We refine it from the clause (seen as a multiset) in two steps: ▸ First, we represent the clause as a ``hash-table'', where the term‹i›-th position indicates term‹Some True› (respectively term‹Some False›, term‹None›) if term‹Pos i› is present in the clause (respectively term‹Neg i›, not at all). This allows to represent every not-tautological clause whose literals fits in the underlying array. We use the first part in two different ways: once for the conflict, where we specialize it to include only information on the atoms and once in the marking structure. › text ‹This is the first level of the refinement. We tried a few different definitions (including a direct one, i.e., mapping a position to the inclusion in the set) but the inductive version turned out to the easiest one to use. › inductive mset_as_position :: ‹bool option list ⇒ nat literal multiset ⇒ bool› where empty: ‹mset_as_position (replicate n None) {#}› | add: ‹mset_as_position xs' (add_mset L P)› if ‹mset_as_position xs P› and ‹atm_of L < length xs› and ‹L ∉# P› and ‹-L ∉# P› and ‹xs' = xs[atm_of L := Some (is_pos L)]› lemma mset_as_position_distinct_mset: ‹mset_as_position xs P ⟹ distinct_mset P› by (induction rule: mset_as_position.induct) auto lemma mset_as_position_atm_le_length: ‹mset_as_position xs P ⟹ L ∈# P ⟹ atm_of L < length xs› by (induction rule: mset_as_position.induct) (auto simp: nth_list_update' atm_of_eq_atm_of) lemma mset_as_position_nth: ‹mset_as_position xs P ⟹ L ∈# P ⟹ xs ! (atm_of L) = Some (is_pos L)› by (induction rule: mset_as_position.induct) (auto simp: nth_list_update' atm_of_eq_atm_of dest: mset_as_position_atm_le_length) lemma mset_as_position_in_iff_nth: ‹mset_as_position xs P ⟹ atm_of L < length xs ⟹ L ∈# P ⟷ xs ! (atm_of L) = Some (is_pos L)› by (induction rule: mset_as_position.induct) (auto simp: nth_list_update' atm_of_eq_atm_of is_pos_neg_not_is_pos dest: mset_as_position_atm_le_length) lemma mset_as_position_tautology: ‹mset_as_position xs C ⟹ ¬tautology C› by (induction rule: mset_as_position.induct) (auto simp: tautology_add_mset) lemma mset_as_position_right_unique: assumes map: ‹mset_as_position xs D› and map': ‹mset_as_position xs D'› shows ‹D = D'› proof (rule distinct_set_mset_eq) show ‹distinct_mset D› using mset_as_position_distinct_mset[OF map] . show ‹distinct_mset D'› using mset_as_position_distinct_mset[OF map'] . show ‹set_mset D = set_mset D'› using mset_as_position_in_iff_nth[OF map] mset_as_position_in_iff_nth[OF map'] mset_as_position_atm_le_length[OF map] mset_as_position_atm_le_length[OF map'] by blast qed lemma mset_as_position_mset_union: fixes P xs defines ‹xs' ≡ fold (λL xs. xs[atm_of L := Some (is_pos L)]) P xs› assumes mset: ‹mset_as_position xs P'› and atm_P_xs: ‹∀L ∈ set P. atm_of L < length xs› and uL_P: ‹∀L ∈ set P. -L ∉# P'› and dist: ‹distinct P› and tauto: ‹¬tautology (mset P)› shows ‹mset_as_position xs' (mset P ∪# P')› using atm_P_xs uL_P dist tauto unfolding xs'_def proof (induction P) case Nil show ?case using mset by auto next case (Cons L P) note IH = this(1) and atm_P_xs = this(2) and uL_P = this(3) and dist = this(4) and tauto = this(5) then have mset: ‹mset_as_position (fold (λL xs. xs[atm_of L := Some (is_pos L)]) P xs) (mset P ∪# P')› by (auto simp: tautology_add_mset) show ?case proof (cases ‹L ∈# P'›) case True then show ?thesis using mset dist by (metis (no_types, lifting) add_mset_union assms(2) distinct.simps(2) fold_simps(2) insert_DiffM list_update_id mset.simps(2) mset_as_position_nth set_mset_mset sup_union_right1) next case False have [simp]: ‹length (fold (λL xs. xs[atm_of L := Some (is_pos L)]) P xs) = length xs› by (induction P arbitrary: xs) auto moreover have ‹- L ∉ set P› using tauto by (metis list.set_intros(1) list.set_intros(2) set_mset_mset tautology_minus) moreover have ‹fold (λL xs. xs[atm_of L := Some (is_pos L)]) P (xs[atm_of L := Some (is_pos L)]) = (fold (λL xs. xs[atm_of L := Some (is_pos L)]) P xs) [atm_of L := Some (is_pos L)]› using uL_P dist tauto apply (induction P arbitrary: xs) subgoal by auto subgoal for L' P by (cases ‹atm_of L = atm_of L'›) (auto simp: tautology_add_mset list_update_swap atm_of_eq_atm_of) done ultimately show ?thesis using mset atm_P_xs dist uL_P False by (auto intro!: mset_as_position.add) qed qed lemma mset_as_position_empty_iff: ‹mset_as_position xs {#} ⟷ (∃n. xs = replicate n None)› apply (rule iffI) subgoal by (cases rule: mset_as_position.cases, assumption) auto subgoal by (auto intro: mset_as_position.intros) done type_synonym (in -) lookup_clause_rel = ‹nat × bool option list› definition lookup_clause_rel :: ‹nat multiset ⇒ (lookup_clause_rel × nat literal multiset) set› where ‹lookup_clause_rel 𝒜 = {((n, xs), C). n = size C ∧ mset_as_position xs C ∧ (∀L∈atms_of (ℒ_a_l_l 𝒜). L < length xs)}› lemma lookup_clause_rel_empty_iff: ‹((n, xs), C) ∈ lookup_clause_rel 𝒜 ⟹ n = 0 ⟷ C = {#}› by (auto simp: lookup_clause_rel_def) lemma conflict_atm_le_length: ‹((n, xs), C) ∈ lookup_clause_rel 𝒜 ⟹ L ∈ atms_of (ℒ_a_l_l 𝒜) ⟹ L < length xs› by (auto simp: lookup_clause_rel_def) lemma conflict_le_length: assumes c_rel: ‹((n, xs), C) ∈ lookup_clause_rel 𝒜› and L_ℒ_a_l_l: ‹L ∈# ℒ_a_l_l 𝒜› shows ‹atm_of L < length xs› proof - have size: ‹n = size C› and mset_pos: ‹mset_as_position xs C› and atms_le: ‹∀L∈atms_of (ℒ_a_l_l 𝒜). L < length xs› using c_rel unfolding lookup_clause_rel_def by blast+ have ‹atm_of L ∈ atms_of (ℒ_a_l_l 𝒜)› using L_ℒ_a_l_l by (simp add: atms_of_def) then show ?thesis using atms_le by blast qed lemma lookup_clause_rel_atm_in_iff: ‹((n, xs), C) ∈ lookup_clause_rel 𝒜 ⟹ L ∈# ℒ_a_l_l 𝒜 ⟹ L ∈# C ⟷ xs!(atm_of L) = Some (is_pos L)› by (rule mset_as_position_in_iff_nth) (auto simp: lookup_clause_rel_def atms_of_def) lemma assumes c: ‹((n,xs), C) ∈ lookup_clause_rel 𝒜› shows lookup_clause_rel_not_tautolgy: ‹¬tautology C› and lookup_clause_rel_distinct_mset: ‹distinct_mset C› and lookup_clause_rel_size: ‹isasat_input_bounded 𝒜 ⟹ literals_are_in_ℒ_i_n 𝒜 C ⟹ size C ≤ 1 + unat32_max div 2› proof - have mset: ‹mset_as_position xs C› and ‹n = size C› and ‹∀L∈atms_of (ℒ_a_l_l 𝒜). L < length xs› using c unfolding lookup_clause_rel_def by fast+ show ‹¬tautology C› using mset apply (induction rule: mset_as_position.induct) subgoal by (auto simp: literals_are_in_ℒ_i_n_def) subgoal by (auto simp: tautology_add_mset) done show ‹distinct_mset C› using mset mset_as_position_distinct_mset by blast then show ‹isasat_input_bounded 𝒜 ⟹ literals_are_in_ℒ_i_n 𝒜 C ⟹ size C ≤ 1 + unat32_max div 2› using simple_clss_size_upper_div2[of 𝒜 ‹C›] ‹¬tautology C› by auto qed definition option_bool_rel :: ‹(bool × 'a option) set› where ‹option_bool_rel = {(b, x). b ⟷ ¬(is_None x)}› definition NOTIN :: ‹bool option› where [simp]: ‹NOTIN = None› definition ISIN :: ‹bool ⇒ bool option› where [simp]: ‹ISIN b = Some b› definition is_NOTIN :: ‹bool option ⇒ bool› where [simp]: ‹is_NOTIN x ⟷ x = NOTIN› lemma is_NOTIN_alt_def: ‹is_NOTIN x ⟷ is_None x› by (auto split: option.splits) lemma (in -) mset_as_position_length_not_None: ‹mset_as_position x2 C ⟹ size C = length (filter ((≠) None) x2)› proof (induction rule: mset_as_position.induct) case (empty n) then show ?case by auto next case (add xs P L xs') note m_as_p = this(1) and atm_L = this(2) have xs_L: ‹xs ! (atm_of L) = None› proof - obtain bb :: ‹bool option ⇒ bool› where f1: ‹∀z. z = None ∨ z = Some (bb z)› by (metis option.exhaust) have f2: ‹xs ! atm_of L ≠ Some (is_pos L)› using add.hyps(1) add.hyps(2) add.hyps(3) mset_as_position_in_iff_nth by blast have f3: ‹∀z b. ((Some b = z ∨ z = None) ∨ bb z) ∨ b› using f1 by blast have f4: ‹∀zs. (zs ! atm_of L ≠ Some (is_pos (- L)) ∨ ¬ atm_of L < length zs) ∨ ¬ mset_as_position zs P› by (metis add.hyps(4) atm_of_uminus mset_as_position_in_iff_nth) have ‹∀z b. ((Some b = z ∨ z = None) ∨ ¬ bb z) ∨ ¬ b› using f1 by blast then show ?thesis using f4 f3 f2 by (metis add.hyps(1) add.hyps(2) is_pos_neg_not_is_pos) qed obtain xs1 xs2 where xs_xs12: ‹xs = xs1 @ None # xs2› and xs1: ‹length xs1 = atm_of L› using atm_L upd_conv_take_nth_drop[of ‹atm_of L› xs ‹None›] apply - apply (subst(asm)(2) xs_L[symmetric]) by (force simp del: append_take_drop_id)+ then show ?case using add by (auto simp: list_update_append) qed definition (in -) is_in_lookup_conflict where ‹is_in_lookup_conflict = (λ(n, xs) L. ¬is_None (xs ! atm_of L))› lemma mset_as_position_remove: ‹mset_as_position xs D ⟹ L < length xs ⟹ mset_as_position (xs[L := None]) (remove1_mset (Pos L) (remove1_mset (Neg L) D))› proof (induction rule: mset_as_position.induct) case (empty n) then have [simp]: ‹(replicate n None)[L := None] = replicate n None› using list_update_id[of ‹replicate n None› L] by auto show ?case by (auto intro: mset_as_position.intros) next case (add xs P K xs') show ?case proof (cases ‹L = atm_of K›) case True then show ?thesis using add by (cases K) auto next case False have map: ‹mset_as_position (xs[L := None]) (remove1_mset (Pos L) (remove1_mset (Neg L) P))› using add by auto have ‹K ∉# P - {#Pos L, Neg L#}› ‹-K ∉# P - {#Pos L, Neg L#}› by (auto simp: add.hyps dest!: in_diffD) then show ?thesis using mset_as_position.add[OF map, of ‹K› ‹xs[L := None, atm_of K := Some (is_pos K)]›] add False list_update_swap[of ‹atm_of K› L xs] apply simp apply (subst diff_add_mset_swap) by auto qed qed lemma mset_as_position_remove2: ‹mset_as_position xs D ⟹ atm_of L < length xs ⟹ mset_as_position (xs[atm_of L := None]) (D - {#L, -L#})› using mset_as_position_remove[of xs D ‹atm_of (-L)›] by (smt add_mset_commute add_mset_diff_bothsides atm_of_uminus insert_DiffM literal.exhaust_sel minus_notin_trivial2 remove_1_mset_id_iff_notin uminus_not_id') lemma mset_as_position_remove3: ‹mset_as_position xs (D - {#L#}) ⟹ atm_of L < length xs ⟹ distinct_mset D ⟹ mset_as_position (xs[atm_of L := None]) (D - {#L, -L#})› using mset_as_position_remove2[of xs ‹D - {#L#}› ‹L›] mset_as_position_tautology[of xs ‹remove1_mset L D›] mset_as_position_distinct_mset[of xs ‹remove1_mset L D›] by (cases ‹L ∈# D›; cases ‹-L ∈# D›) (auto dest!: multi_member_split simp: minus_notin_trivial ac_simps add_mset_eq_add_mset tautology_add_mset) definition (in -) delete_from_lookup_conflict :: ‹nat literal ⇒ lookup_clause_rel ⇒ lookup_clause_rel nres› where ‹delete_from_lookup_conflict = (λL (n, xs). do { ASSERT(n≥1); ASSERT(atm_of L < length xs); RETURN (n - 1, xs[atm_of L := None]) })› lemma delete_from_lookup_conflict_op_mset_delete: ‹(uncurry delete_from_lookup_conflict, uncurry (RETURN oo remove1_mset)) ∈ [λ(L, D). -L ∉# D ∧ L ∈# ℒ_a_l_l 𝒜 ∧ L ∈# D]_f Id ×_f lookup_clause_rel 𝒜 → ⟨lookup_clause_rel 𝒜⟩nres_rel› apply (intro frefI nres_relI) subgoal for x y using mset_as_position_remove[of ‹snd (snd x)› ‹snd y› ‹atm_of (fst y)›] apply (cases x; cases y; cases ‹fst y›) by (auto simp: delete_from_lookup_conflict_def lookup_clause_rel_def dest!: multi_member_split intro!: ASSERT_refine_left) done definition delete_from_lookup_conflict_pre where ‹delete_from_lookup_conflict_pre 𝒜 = (λ(a, b). - a ∉# b ∧ a ∈# ℒ_a_l_l 𝒜 ∧ a ∈# b)› definition add_to_lookup_conflict :: ‹nat literal ⇒ lookup_clause_rel ⇒ lookup_clause_rel› where ‹add_to_lookup_conflict = (λL (n, xs). (if xs ! atm_of L = NOTIN then n + 1 else n, xs[atm_of L := ISIN (is_pos L)]))› lemma add_to_lookup_conflict_lookup_clause_rel: assumes confl: ‹((n, xs), C) ∈ lookup_clause_rel 𝒜› and uL_C: ‹-L ∉# C› and L_ℒ_a_l_l: ‹L ∈# ℒ_a_l_l 𝒜› shows ‹(add_to_lookup_conflict L (n, xs), {#L#} ∪# C) ∈ lookup_clause_rel 𝒜› proof - have n: ‹n = size C› and mset: ‹mset_as_position xs C› and atm: ‹∀L∈atms_of (ℒ_a_l_l 𝒜). L < length xs› using confl unfolding lookup_clause_rel_def by blast+ have ‹distinct_mset C› using mset by (blast dest: mset_as_position_distinct_mset) have atm_L_xs: ‹atm_of L < length xs› using atm L_ℒ_a_l_l by (auto simp: atms_of_def) then show ?thesis proof (cases ‹L ∈# C›) case True with mset have xs: ‹xs ! atm_of L = Some (is_pos L)› ‹xs ! atm_of L ≠ None› by (auto dest: mset_as_position_nth) moreover have ‹{#L#} ∪# C = C› using True by (metis mset_contains_eq union_mset_def) ultimately show ?thesis using n mset atm True by (auto simp: lookup_clause_rel_def add_to_lookup_conflict_def xs[symmetric]) next case False with mset have ‹xs ! atm_of L = None› using mset_as_position_in_iff_nth[of xs C L] mset_as_position_in_iff_nth[of xs C ‹-L›] atm_L_xs uL_C by (cases L; cases ‹xs ! atm_of L›) auto then show ?thesis using n mset atm False atm_L_xs uL_C by (auto simp: lookup_clause_rel_def add_to_lookup_conflict_def intro!: mset_as_position.intros) qed qed definition conflict_from_lookup where ‹conflict_from_lookup = (λ(n, xs). SPEC(λD. mset_as_position xs D ∧ n = size D))› lemma Ex_mset_as_position: ‹Ex (mset_as_position xs)› proof (induction ‹size {#x ∈# mset xs. x ≠ None#}› arbitrary: xs) case 0 then have xs: ‹xs = replicate (length xs) None› by (auto simp: filter_mset_empty_conv dest: replicate_length_same) show ?case by (subst xs) (auto simp: mset_as_position.empty intro!: exI[of _ ‹{#}›]) next case (Suc x) note IH = this(1) and xs = this(2) obtain i where [simp]: ‹i < length xs› and xs_i: ‹xs ! i ≠ None› using xs[symmetric] by (auto dest!: size_eq_Suc_imp_elem simp: in_set_conv_nth) let ?xs = ‹xs [i := None]› have ‹x = size {#x ∈# mset ?xs. x ≠ None#}› using xs[symmetric] xs_i by (auto simp: mset_update size_remove1_mset_If) from IH[OF this] obtain D where map: ‹mset_as_position ?xs D› by blast have [simp]: ‹Pos i ∉# D› ‹Neg i ∉# D› using xs_i mset_as_position_nth[OF map, of ‹Pos i›] mset_as_position_nth[OF map, of ‹Neg i›] by auto have [simp]: ‹xs ! i = a ⟹ xs[i := a] = xs› for a by auto have ‹mset_as_position xs (add_mset (if the (xs ! i) then Pos i else Neg i) D)› using mset_as_position.add[OF map, of ‹if the (xs ! i) then Pos i else Neg i› xs] xs_i[symmetric] by (cases ‹xs ! i›) auto then show ?case by blast qed lemma id_conflict_from_lookup: ‹(RETURN o id, conflict_from_lookup) ∈ [λ(n, xs). ∃D. ((n, xs), D) ∈ lookup_clause_rel 𝒜]_f Id → ⟨lookup_clause_rel 𝒜⟩nres_rel› by (intro frefI nres_relI) (auto simp: lookup_clause_rel_def conflict_from_lookup_def RETURN_RES_refine_iff) lemma lookup_clause_rel_exists_le_unat32_max: assumes ocr: ‹((n, xs), D) ∈ lookup_clause_rel 𝒜› and ‹n > 0› and le_i: ‹∀k<i. xs ! k = None› and lits: ‹literals_are_in_ℒ_i_n 𝒜 D› and bounded: ‹isasat_input_bounded 𝒜› shows ‹∃j. j ≥ i ∧ j < length xs ∧ j < unat32_max ∧ xs ! j ≠ None› proof - have n_D: ‹n = size D› and map: ‹mset_as_position xs D› and le_xs: ‹∀L∈atms_of (ℒ_a_l_l 𝒜). L < length xs› using ocr unfolding lookup_clause_rel_def by auto have map_empty: ‹mset_as_position xs {#} ⟷ (xs = [] ∨ set xs = {None})› by (subst mset_as_position.simps) (auto simp add: list_eq_replicate_iff) have ex_not_none: ‹∃j. j ≥ i ∧ j < length xs ∧ xs ! j ≠ None› proof (rule ccontr) assume ‹¬ ?thesis› then have ‹xs = [] ∨ set xs = {None}› using le_i by (fastforce simp: in_set_conv_nth) then have ‹mset_as_position xs {#}› using map_empty by auto then show False using mset_as_position_right_unique[OF map] ‹n > 0› n_D by (cases D) auto qed then obtain j where j: ‹j ≥ i›‹j < length xs›‹xs ! j ≠ None› by blast let ?L = ‹if the (xs ! j) then Pos j else Neg j› have ‹?L ∈# D› using j mset_as_position_in_iff_nth[OF map, of ?L] by auto then have ‹nat_of_lit ?L ≤ unat32_max› using lits bounded by (auto 5 5 dest!: multi_member_split[of _ D] simp: literals_are_in_ℒ_i_n_add_mset split: if_splits) then have ‹j < unat32_max› by (auto simp: unat32_max_def split: if_splits) then show ?thesis using j by blast qed definition pre_simplify_clause_inv where ‹pre_simplify_clause_inv C = (λ(i, tauto, D, D'). i ≤ length C ∧ (¬tauto ⟷ ¬tautology (mset (take i C))) ∧ (¬tauto ⟶ D = remdups_mset (mset (take i C))) ∧ set D' ⊆ set C ∧ mset D' = D ∧ ¬tautology D ∧ distinct_mset D)› definition pre_simplify_clause :: ‹'v clause_l ⇒ (bool × 'v clause_l) nres› where ‹pre_simplify_clause C = do { (_, tauto, D₀, D) ← WHILE_T⇗ pre_simplify_clause_inv C⇖ (λ(i, tauto, D, D'). i < length C ∧ ¬tauto) (λ(i, tauto, D, D'). do { ASSERT(i < length C); let L = C!i; if -L ∈# D then RETURN (i+1,True, D, D') else if L ∈# D then RETURN (i+1, tauto, D, D') else RETURN (i+1,tauto, add_mset L D, D' @ [L]) }) (0, False, {#}, []); ASSERT(D₀ = mset D ∧ set D ⊆ set C); RETURN (tauto, D) }› definition pre_simplify_clause_spec where ‹pre_simplify_clause_spec C = (λ(tauto, D). (tauto ⟷ tautology (mset C)) ∧ (¬tauto ⟶ mset D = remdups_mset (mset C)))› lemma pre_simplify_clause_spec: ‹pre_simplify_clause C ≤ ⇓ Id (SPEC(pre_simplify_clause_spec C))› proof - have [refine0]: ‹wf (measure (λ(i, _). length C - i))› by auto show ?thesis unfolding pre_simplify_clause_def apply refine_vcg subgoal by (auto simp: pre_simplify_clause_inv_def) subgoal by auto subgoal for state i b tauto ba D D' by (auto simp: pre_simplify_clause_inv_def take_Suc_conv_app_nth tautology_add_mset) subgoal by auto subgoal for state i b tauto ba D D' by (auto simp: pre_simplify_clause_inv_def take_Suc_conv_app_nth tautology_add_mset) subgoal by auto subgoal for state i b tauto ba D D' by (auto simp: pre_simplify_clause_inv_def take_Suc_conv_app_nth tautology_add_mset) subgoal by auto subgoal by (auto simp: pre_simplify_clause_inv_def) subgoal by (auto simp: pre_simplify_clause_inv_def) subgoal for state i b tauto ba D D' using not_tautology_mono[of ‹mset (take i C)› ‹mset C›] by (auto simp: pre_simplify_clause_inv_def mset_take_subseteq pre_simplify_clause_spec_def) done qed definition (in -) lit_is_in_lookup where ‹lit_is_in_lookup = (λL (n, xs). do { ASSERT(atm_of L < length xs); RETURN ((xs ! atm_of L) = Some (is_pos L))})› definition unmark_clause :: ‹_› where ‹unmark_clause C lup = do { (_, lup) ← WHILE_T (λ(i,lup). i < length C) (λ(i,lup). do { ASSERT(i < length C); lup ← delete_from_lookup_conflict (C!i) lup; RETURN (i+1, lup) }) (0, lup); RETURN lup }› lemma unmark_clause_spec: assumes ‹(lup, mset C) ∈ lookup_clause_rel 𝒜› ‹atm_of ` set C ⊆ set_mset 𝒜› shows ‹unmark_clause C lup ≤ (SPEC(λlup'. (lup', {#}) ∈ lookup_clause_rel 𝒜))› proof - have [refine]: ‹wf (measure (λ(i, _). length C - i))› by auto show ?thesis unfolding unmark_clause_def apply (refine_vcg WHILET_rule[where R = ‹measure (λ(i, _). length C - i)› and I = ‹λ(i,lup). (lup, mset (drop i C)) ∈ lookup_clause_rel 𝒜›]) subgoal using assms by auto subgoal using assms by auto subgoal for s a b using lookup_clause_rel_not_tautolgy[of ‹fst b› ‹snd b› ‹mset (drop a C)›] assms(2) apply - apply (rule delete_from_lookup_conflict_op_mset_delete[of 𝒜, THEN fref_to_Down_curry, of ‹C!a› ‹mset (drop a C)›, THEN order_trans]) by (auto simp: in_ℒ_a_l_l_atm_of_𝒜_i_n conc_fun_RES RETURN_def tautology_add_mset simp flip: Cons_nth_drop_Suc) subgoal by auto done qed lemma lit_is_in_lookup_spec: assumes ‹(lup, C) ∈ lookup_clause_rel 𝒜› ‹atm_of L ∈# 𝒜› shows ‹lit_is_in_lookup L lup = RES {L ∈# C}› using assms unfolding lit_is_in_lookup_def apply refine_rcg using mset_as_position_in_iff_nth[of ‹snd lup› C L] by (auto simp: lit_is_in_lookup_def lookup_clause_rel_def atms_of_ℒ_a_l_l_𝒜_i_n dest: multi_member_split dest: mset_as_position_nth) definition pre_simplify_clause_lookup :: ‹nat clause_l ⇒ nat clause_l ⇒ lookup_clause_rel ⇒ (bool × nat clause_l × lookup_clause_rel) nres› where ‹pre_simplify_clause_lookup C D lup = do { ASSERT(D = []); (_, tauto, lup, D) ← WHILE_T⇗ λ_. True⇖ (λ(i, tauto, D, D'). i < length C ∧ ¬tauto) (λ(i, tauto, D, D'). do { ASSERT(i < length C); ASSERT(fst D < unat32_max ∧ atm_of (C!i) < length (snd D)); ASSERT(length D' = fst D); let L = C!i; b ← lit_is_in_lookup (-L) D; if b then RETURN (i+1,True, D, D') else do { b ← lit_is_in_lookup L D; if b then RETURN (i+1, tauto, D, D') else RETURN (i+1,tauto, add_to_lookup_conflict L D, D' @ [L]) } }) (0, False, lup, D); lup ← unmark_clause D lup; RETURN (tauto, D, lup) }› lemma pre_simplify_clause_lookup_pre_simplify_clause: assumes ‹(lup, {#}) ∈ lookup_clause_rel 𝒜› ‹atm_of ` set C ⊆ set_mset 𝒜› ‹isasat_input_bounded 𝒜› and [simp]: ‹E = []› shows ‹pre_simplify_clause_lookup C E lup ≤ ⇓{((tauto, D, lup), (tauto', D')). tauto=tauto' ∧ D=D' ∧ (lup, {#}) ∈ lookup_clause_rel 𝒜} (pre_simplify_clause C)› proof - have [refine0]: ‹((0, False, lup, E), 0, False, {#}, []) ∈ nat_rel ×_r bool_rel ×_r lookup_clause_rel 𝒜 ×_r ⟨Id⟩list_rel› using assms by auto have [simp]: ‹x < length C ⟹ atm_of (- C ! x) ∈# 𝒜› ‹x < length C ⟹ atm_of (C ! x) ∈# 𝒜› for x using assms by auto show ?thesis using assms unfolding pre_simplify_clause_lookup_def pre_simplify_clause_def apply (refine_vcg lit_is_in_lookup_spec lhs_step_If) 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 using simple_clss_size_upper_div2[of 𝒜 ‹mset x2b›] assms unfolding literals_are_in_ℒ_i_n_alt_def apply - by (subgoal_tac ‹atm_of ` set (take x1 C) ⊆ atms_of (ℒ_a_l_l 𝒜)›) (auto simp: lit_is_in_lookup_spec in_ℒ_a_l_l_atm_of_𝒜_i_n pre_simplify_clause_inv_def lookup_clause_rel_def unat32_max_def atms_of_ℒ_a_l_l_𝒜_i_n dest!: in_set_takeD) subgoal for x x' x1 x2 x1a x2a x1b x2b x1c x2c x1d x2d x1e x2e using simple_clss_size_upper_div2[of 𝒜 ‹mset x2b›] assms unfolding literals_are_in_ℒ_i_n_alt_def apply - by (subgoal_tac ‹atm_of ` set (take x1 C) ⊆ atms_of (ℒ_a_l_l 𝒜)›) (auto simp: lit_is_in_lookup_spec in_ℒ_a_l_l_atm_of_𝒜_i_n pre_simplify_clause_inv_def lookup_clause_rel_def unat32_max_def atms_of_ℒ_a_l_l_𝒜_i_n dest!: in_set_takeD) subgoal by (clarsimp simp add: lookup_clause_rel_def pre_simplify_clause_inv_def simp del: size_mset simp flip: size_mset) subgoal for x x' x1 x2 x1a x2a x1b x2b x1c x2c x1d x2d x1e x2e using add_to_lookup_conflict_lookup_clause_rel[of ‹fst x1e› ‹snd x1e› x1b 𝒜 ‹C ! x1›] by (auto simp: lit_is_in_lookup_spec in_ℒ_a_l_l_atm_of_𝒜_i_n) subgoal for x x' x1 x2 x1a x2a x1b x2b x1c x2c x1d x2d x1e x2e by (rule unmark_clause_spec[of _ _ 𝒜, THEN order_trans]) auto done qed end

Theory IsaSAT_Mark