Theory IsaSAT

theory IsaSAT_Trail imports IsaSAT_Literals begin chapter ‹Efficient Trail› text ‹Our trail contains several additional information compared to the simple trail: ▪ the (reversed) trail in an array (i.e., the trail in the same order as presented in ``Automated Reasoning''); ▪ the mapping from any ∗‹literal› (and not an atom) to its polarity; ▪ the mapping from a ∗‹atom› to its level or reason (in two different arrays); ▪ the current level of the state; ▪ the control stack. We copied the idea from the mapping from a literals to it polarity instead of an atom to its polarity from a comment by Armin Biere in CaDiCal. We only observed a (at best) faint performance increase, but as it seemed slightly faster and does not increase the length of the formalisation, we kept it. The control stack is the latest addition: it contains the positions of the decisions in the trail. It is mostly to enable fast restarts (since it allows to directly iterate over all decision of the trail), but might also slightly speed up backjumping (since we know how far we are going back in the trail). Remark that the control stack contains is not updated during the backjumping, but only ∗‹after› doing it (as we keep only the the beginning of it). › section ‹Types› type_synonym trail_pol = ‹nat literal list × tri_bool list × nat list × nat list × nat × nat list × nat› definition get_level_atm where ‹get_level_atm M L = get_level M (Pos L)› definition polarity_atm where ‹polarity_atm M L = (if Pos L ∈ lits_of_l M then SET_TRUE else if Neg L ∈ lits_of_l M then SET_FALSE else None)› definition defined_atm :: ‹('v, nat) ann_lits ⇒ 'v ⇒ bool› where ‹defined_atm M L = defined_lit M (Pos L)› abbreviation undefined_atm where ‹undefined_atm M L ≡ ¬defined_atm M L› section ‹Control Stack› inductive control_stack where empty: ‹control_stack [] []› | cons_prop: ‹control_stack cs M ⟹ control_stack cs (Propagated L C # M)› | cons_dec: ‹control_stack cs M ⟹ n = length M ⟹ control_stack (cs @ [n]) (Decided L # M)› inductive_cases control_stackE: ‹control_stack cs M› lemma control_stack_length_count_dec: ‹control_stack cs M ⟹ length cs = count_decided M› by (induction rule: control_stack.induct) auto lemma control_stack_le_length_M: ‹control_stack cs M ⟹ c∈set cs ⟹ c < length M› by (induction rule: control_stack.induct) auto lemma control_stack_propa[simp]: ‹control_stack cs (Propagated x21 x22 # list) ⟷ control_stack cs list› by (auto simp: control_stack.intros elim: control_stackE) lemma control_stack_filter_map_nth: ‹control_stack cs M ⟹ filter is_decided (rev M) = map (nth (rev M)) cs› apply (induction rule: control_stack.induct) subgoal by auto subgoal for cs M L C using control_stack_le_length_M[of cs M] by (auto simp: nth_append) subgoal for cs M L using control_stack_le_length_M[of cs M] by (auto simp: nth_append) done lemma control_stack_empty_cs[simp]: ‹control_stack [] M ⟷ count_decided M = 0› by (induction M rule:ann_lit_list_induct) (auto simp: control_stack.empty control_stack.cons_prop elim: control_stackE) text ‹This is an other possible definition. It is not inductive, which makes it easier to reason about appending (or removing) some literals from the trail. It is however much less clear if the definition is correct.› definition control_stack' where ‹control_stack' cs M ⟷ (length cs = count_decided M ∧ (∀L∈set M. is_decided L ⟶ (cs ! (get_level M (lit_of L) - 1) < length M ∧ rev M!(cs ! (get_level M (lit_of L) - 1)) = L)))› lemma control_stack_rev_get_lev: ‹control_stack cs M ⟹ no_dup M ⟹ L∈set M ⟹ is_decided L ⟹ rev M!(cs ! (get_level M (lit_of L) - 1)) = L› apply (induction arbitrary: L rule: control_stack.induct) subgoal by auto subgoal for cs M L C La using control_stack_le_length_M[of cs M] control_stack_length_count_dec[of cs M] count_decided_ge_get_level[of M ‹lit_of La›] apply (auto simp: get_level_cons_if nth_append atm_of_eq_atm_of undefined_notin) by (metis Suc_count_decided_gt_get_level Suc_less_eq Suc_pred count_decided_0_iff diff_is_0_eq le_SucI le_refl neq0_conv nth_mem) subgoal for cs M L using control_stack_le_length_M[of cs M] control_stack_length_count_dec[of cs M] apply (auto simp: nth_append get_level_cons_if atm_of_eq_atm_of undefined_notin) by (metis Suc_count_decided_gt_get_level Suc_less_eq Suc_pred count_decided_0_iff diff_is_0_eq le_SucI le_refl neq0_conv)+ done lemma control_stack_alt_def_imp: ‹no_dup M ⟹ (⋀L. L ∈set M ⟹ is_decided L ⟹ cs ! (get_level M (lit_of L) - 1) < length M ∧ rev M!(cs ! (get_level M (lit_of L) - 1)) = L) ⟹ length cs = count_decided M ⟹ control_stack cs M› proof (induction M arbitrary: cs rule:ann_lit_list_induct) case Nil then show ?case by auto next case (Decided L M) note IH = this(1) and n_d = this(2) and dec = this(3) and length = this(4) from length obtain cs' n where cs[simp]: ‹cs = cs' @ [n]› using length by (cases cs rule: rev_cases) auto have [simp]: ‹rev M ! n ∈ set M ⟹ is_decided (rev M ! n) ⟹ count_decided M ≠ 0› by (auto simp: count_decided_0_iff) have dec': ‹L'∈set M ⟹ is_decided L' ⟹ cs' ! (get_level M (lit_of L') - 1) < length M ∧ rev M ! (cs' ! (get_level M (lit_of L') - 1)) = L'› for L' using dec[of L'] n_d length count_decided_ge_get_level[of M ‹lit_of L'›] apply (auto simp: get_level_cons_if atm_of_eq_atm_of undefined_notin split: if_splits) apply (auto simp: nth_append split: if_splits) done have le: ‹length cs' = count_decided M› using length by auto have [simp]: ‹n = length M› using n_d dec[of ‹Decided L›] le undefined_notin[of M ‹rev M ! n›] nth_mem[of n ‹rev M›] by (auto simp: nth_append split: if_splits) show ?case unfolding cs apply (rule control_stack.cons_dec) subgoal apply (rule IH) using n_d dec' le by auto subgoal by auto done next case (Propagated L m M) note IH = this(1) and n_d = this(2) and dec = this(3) and length = this(4) have [simp]: ‹rev M ! n ∈ set M ⟹ is_decided (rev M ! n) ⟹ count_decided M ≠ 0› for n by (auto simp: count_decided_0_iff) have dec': ‹L'∈set M ⟹ is_decided L' ⟹ cs ! (get_level M (lit_of L') - 1) < length M ∧ rev M ! (cs ! (get_level M (lit_of L') - 1)) = L'› for L' using dec[of L'] n_d length count_decided_ge_get_level[of M ‹lit_of L'›] apply (cases L') apply (auto simp: get_level_cons_if atm_of_eq_atm_of undefined_notin split: if_splits) apply (auto simp: nth_append split: if_splits) done show ?case apply (rule control_stack.cons_prop) apply (rule IH) subgoal using n_d by auto subgoal using dec' by auto subgoal using length by auto done qed lemma control_stack_alt_def: ‹no_dup M ⟹ control_stack' cs M ⟷ control_stack cs M› using control_stack_alt_def_imp[of M cs] control_stack_rev_get_lev[of cs M] control_stack_length_count_dec[of cs M] control_stack_le_length_M[of cs M] unfolding control_stack'_def apply - apply (rule iffI) subgoal by blast subgoal using count_decided_ge_get_level[of M] by (metis One_nat_def Suc_count_decided_gt_get_level Suc_less_eq Suc_pred count_decided_0_iff less_imp_diff_less neq0_conv nth_mem) done lemma control_stack_decomp: assumes decomp: ‹(Decided L # M1, M2) ∈ set (get_all_ann_decomposition M)› and cs: ‹control_stack cs M› and n_d: ‹no_dup M› shows ‹control_stack (take (count_decided M1) cs) M1› proof - obtain M3 where M: ‹M = M3 @ M2 @ Decided L # M1› using decomp by auto define M2' where ‹M2' = M3 @ M2› have M: ‹M = M2' @ Decided L # M1› unfolding M M2'_def by auto have n_d1: ‹no_dup M1› using n_d no_dup_appendD unfolding M by auto have ‹control_stack' cs M› using cs apply (subst (asm) control_stack_alt_def[symmetric]) apply (rule n_d) apply assumption done then have cs_M: ‹length cs = count_decided M› and L: ‹⋀L. L∈set M ⟹ is_decided L ⟹ cs ! (get_level M (lit_of L) - 1) < length M ∧ rev M ! (cs ! (get_level M (lit_of L) - 1)) = L› unfolding control_stack'_def by auto have H: ‹L' ∈ set M1 ⟹ undefined_lit M2' (lit_of L') ∧ atm_of (lit_of L') ≠ atm_of L› for L' using n_d unfolding M by (metis atm_of_eq_atm_of defined_lit_no_dupD(1) defined_lit_uminus lit_of.simps(1) no_dup_appendD no_dup_append_cons no_dup_cons undefined_notin) have ‹distinct M› using no_dup_imp_distinct[OF n_d] . then have K: ‹L' ∈ set M1 ⟹ x < length M ⟹ rev M ! x = L' ⟹ x < length M1› for x L' unfolding M apply (auto simp: nth_append nth_Cons split: if_splits nat.splits) by (metis length_rev less_diff_conv local.H not_less_eq nth_mem set_rev undefined_notin) have I: ‹L ∈ set M1 ⟹ is_decided L ⟹ get_level M1 (lit_of L) > 0› for L using n_d unfolding M by (auto dest!: split_list) have cs': ‹control_stack' (take (count_decided M1) cs) M1› unfolding control_stack'_def apply (intro conjI ballI impI) subgoal using cs_M unfolding M by auto subgoal for L using n_d L[of L] H[of L] K[of L ‹cs ! (get_level M1 (lit_of L) - Suc 0)›] count_decided_ge_get_level[of ‹M1› ‹lit_of L›] I[of L] unfolding M by auto subgoal for L using n_d L[of L] H[of L] K[of L ‹cs ! (get_level M1 (lit_of L) - Suc 0)›] count_decided_ge_get_level[of ‹M1› ‹lit_of L›] I[of L] unfolding M by auto done show ?thesis apply (subst control_stack_alt_def[symmetric]) apply (rule n_d1) apply (rule cs') done qed section ‹Encoding of the reasons› definition DECISION_REASON :: nat where ‹DECISION_REASON = 1› definition ann_lits_split_reasons where ‹ann_lits_split_reasons 𝒜 = {((M, reasons), M'). M = map lit_of (rev M') ∧ (∀L ∈ set M'. is_proped L ⟶ reasons ! (atm_of (lit_of L)) = mark_of L ∧ mark_of L ≠ DECISION_REASON) ∧ (∀L ∈ set M'. is_decided L ⟶ reasons ! (atm_of (lit_of L)) = DECISION_REASON) ∧ (∀L ∈# ℒ_a_l_l 𝒜. atm_of L < length reasons) }› definition zeroed_trail :: ‹('v, nat) ann_lits ⇒ _› where ‹zeroed_trail M zeroed ⟷ zeroed ≤ length M ∧ (∀z < zeroed. is_proped (rev M ! z) ∧ mark_of (rev M ! z) = 0)› lemma zeored_trail_cons[simp]: ‹zeroed_trail M zeroed ⟹ zeroed_trail (L # M) zeroed› by (auto simp: zeroed_trail_def nth_append split: if_splits) lemma zeroed_trail_consD: assumes ‹zeroed_trail (L # M) zeroed› ‹count_decided (L # M) > 0› ‹no_dup (L # M)› shows ‹zeroed_trail M zeroed› proof - obtain M1 M2 K where ‹L # M = M2 @ Decided K # M1› and ‹get_level (L # M) K = 1› by (metis One_nat_def assms(2) assms(3) le_count_decided_decomp) then have ‹zeroed ≤ length M› using assms(1) unfolding zeroed_trail_def apply (cases ‹zeroed = Suc (length M)›) apply (auto elim!: list_Cons_eq_append_cases simp: nth_append split: if_splits) by (metis (no_types, lifting) add.right_neutral add_Suc add_diff_cancel_left' annotated_lit.disc(3) less_add_Suc2 nth_Cons_0 order_less_irrefl) then show ‹?thesis› using assms(1) unfolding zeroed_trail_def by auto qed definition trail_pol :: ‹nat multiset ⇒ (trail_pol × (nat, nat) ann_lits) set› where ‹trail_pol 𝒜 = {((M', xs, lvls, reasons, k, cs, zeroed), M). ((M', reasons), M) ∈ ann_lits_split_reasons 𝒜 ∧ no_dup M ∧ (∀L ∈# ℒ_a_l_l 𝒜. nat_of_lit L < length xs ∧ xs ! (nat_of_lit L) = polarity M L) ∧ (∀L ∈# ℒ_a_l_l 𝒜. atm_of L < length lvls ∧ lvls ! (atm_of L) = get_level M L) ∧ k = count_decided M ∧ (∀L∈set M. lit_of L ∈# ℒ_a_l_l 𝒜) ∧ control_stack cs M ∧ zeroed_trail M zeroed ∧ isasat_input_bounded 𝒜}› section ‹Definition of the full trail› lemma trail_pol_alt_def: ‹trail_pol 𝒜 = {((M', xs, lvls, reasons, k, cs, zeroed), M). ((M', reasons), M) ∈ ann_lits_split_reasons 𝒜 ∧ no_dup M ∧ (∀L ∈# ℒ_a_l_l 𝒜. nat_of_lit L < length xs ∧ xs ! (nat_of_lit L) = polarity M L) ∧ (∀L ∈# ℒ_a_l_l 𝒜. atm_of L < length lvls ∧ lvls ! (atm_of L) = get_level M L) ∧ k = count_decided M ∧ (∀L∈set M. lit_of L ∈# ℒ_a_l_l 𝒜) ∧ control_stack cs M ∧ literals_are_in_ℒ_i_n_trail 𝒜 M ∧ length M < unat32_max ∧ length M ≤ unat32_max div 2 + 1 ∧ count_decided M < unat32_max ∧ length M' = length M ∧ M' = map lit_of (rev M) ∧ zeroed_trail M zeroed ∧ isasat_input_bounded 𝒜 }› proof - have [intro!]: ‹length M < n ⟹ count_decided M < n› for M n using length_filter_le[of is_decided M] by (auto simp: literals_are_in_ℒ_i_n_trail_def unat32_max_def count_decided_def simp del: length_filter_le dest: length_trail_unat32_max_div2) show ?thesis unfolding trail_pol_def by (auto simp: literals_are_in_ℒ_i_n_trail_def unat32_max_def ann_lits_split_reasons_def dest: length_trail_unat32_max_div2 simp del: isasat_input_bounded_def) qed section ‹Code generation› subsection ‹Conversion between incomplete and complete mode› definition trail_fast_of_slow :: ‹(nat, nat) ann_lits ⇒ (nat, nat) ann_lits› where ‹trail_fast_of_slow = id› definition trail_pol_slow_of_fast :: ‹trail_pol ⇒ trail_pol› where ‹trail_pol_slow_of_fast = (λ(M, val, lvls, reason, k, cs). (M, val, lvls, reason, k, cs))› definition trail_slow_of_fast :: ‹(nat, nat) ann_lits ⇒ (nat, nat) ann_lits› where ‹trail_slow_of_fast = id› definition trail_pol_fast_of_slow :: ‹trail_pol ⇒ trail_pol› where ‹trail_pol_fast_of_slow = (λ(M, val, lvls, reason, k, cs). (M, val, lvls, reason, k, cs))› lemma trail_pol_slow_of_fast_alt_def: ‹trail_pol_slow_of_fast M = M› by (cases M) (auto simp: trail_pol_slow_of_fast_def) lemma trail_pol_fast_of_slow_trail_fast_of_slow: ‹(RETURN o trail_pol_fast_of_slow, RETURN o trail_fast_of_slow) ∈ [λM. (∀C L. Propagated L C ∈ set M ⟶ C < unat64_max)]_f trail_pol 𝒜 → ⟨trail_pol 𝒜⟩ nres_rel› by (intro frefI nres_relI) (auto simp: trail_pol_def trail_pol_fast_of_slow_def trail_fast_of_slow_def) lemma trail_pol_slow_of_fast_trail_slow_of_fast: ‹(RETURN o trail_pol_slow_of_fast, RETURN o trail_slow_of_fast) ∈ trail_pol 𝒜 →_f ⟨trail_pol 𝒜⟩ nres_rel› by (intro frefI nres_relI) (auto simp: trail_pol_def trail_pol_fast_of_slow_def trail_fast_of_slow_def trail_slow_of_fast_def trail_pol_slow_of_fast_def) lemma trail_pol_same_length[simp]: ‹(M', M) ∈ trail_pol 𝒜 ⟹ length (fst M') = length M› by (auto simp: trail_pol_alt_def) definition counts_maximum_level where ‹counts_maximum_level M C = {i. C ≠ None ⟶ i = card_max_lvl M (the C)}› lemma counts_maximum_level_None[simp]: ‹counts_maximum_level M None = Collect (λ_. True)› by (auto simp: counts_maximum_level_def) subsection ‹Level of a literal› definition get_level_atm_pol_pre where ‹get_level_atm_pol_pre = (λ((M, xs, lvls, k), L). L < length lvls)› definition get_level_atm_pol :: ‹trail_pol ⇒ nat ⇒ nat› where ‹get_level_atm_pol = (λ(M, xs, lvls, k) L. lvls ! L)› lemma get_level_atm_pol_pre: assumes ‹Pos L ∈# ℒ_a_l_l 𝒜› and ‹(M', M) ∈ trail_pol 𝒜› shows ‹get_level_atm_pol_pre (M', L)› using assms by (auto 5 5 simp: trail_pol_def nat_lit_rel_def br_def get_level_atm_pol_pre_def intro!: ext) lemma (in -) get_level_get_level_atm: ‹get_level M L = get_level_atm M (atm_of L)› unfolding get_level_atm_def by (cases L) (auto simp: get_level_Neg_Pos) definition get_level_pol where ‹get_level_pol M L = get_level_atm_pol M (atm_of L)› definition get_level_pol_pre where ‹get_level_pol_pre = (λ((M, xs, lvls, k), L). atm_of L < length lvls)› lemma get_level_pol_pre: assumes ‹L ∈# ℒ_a_l_l 𝒜› and ‹(M', M) ∈ trail_pol 𝒜› shows ‹get_level_pol_pre (M', L)› using assms by (auto 5 5 simp: trail_pol_def nat_lit_rel_def br_def get_level_pol_pre_def intro!: ext) lemma get_level_get_level_pol: assumes ‹(M', M) ∈ trail_pol 𝒜› and ‹L ∈# ℒ_a_l_l 𝒜› shows ‹get_level M L = get_level_pol M' L› using assms by (auto simp: get_level_pol_def get_level_atm_pol_def trail_pol_def) subsection ‹Current level› definition (in -) count_decided_pol where ‹count_decided_pol = (λ(_, _, _, _, k, _). k)› lemma count_decided_trail_ref: ‹(RETURN o count_decided_pol, RETURN o count_decided) ∈ trail_pol 𝒜 →_f ⟨nat_rel⟩nres_rel› by (intro frefI nres_relI) (auto simp: trail_pol_def count_decided_pol_def) subsection ‹Polarity› definition (in -) polarity_pol :: ‹trail_pol ⇒ nat literal ⇒ bool option› where ‹polarity_pol = (λ(M, xs, lvls, k) L. do { xs ! (nat_of_lit L) })› definition polarity_pol_pre where ‹polarity_pol_pre = (λ(M, xs, lvls, k) L. nat_of_lit L < length xs)› lemma polarity_pol_polarity: ‹(uncurry (RETURN oo polarity_pol), uncurry (RETURN oo polarity)) ∈ [λ(M, L). L ∈# ℒ_a_l_l 𝒜]_f trail_pol 𝒜 ×_f Id → ⟨⟨bool_rel⟩option_rel⟩nres_rel› by (intro nres_relI frefI) (auto simp: trail_pol_def polarity_def polarity_pol_def dest!: multi_member_split) lemma polarity_pol_pre: ‹(M', M) ∈ trail_pol 𝒜 ⟹ L ∈# ℒ_a_l_l 𝒜 ⟹ polarity_pol_pre M' L› by (auto simp: trail_pol_def polarity_def polarity_pol_def polarity_pol_pre_def dest!: multi_member_split) definition mop_polarity_pol :: ‹trail_pol ⇒ nat literal ⇒ bool option nres› where ‹mop_polarity_pol = (λM L. do { ASSERT(polarity_pol_pre M L); RETURN (polarity_pol M L) })› subsection ‹Length of the trail› definition (in -) isa_length_trail_pre where ‹isa_length_trail_pre = (λ (M', xs, lvls, reasons, k, cs). length M' ≤ unat32_max)› definition (in -) isa_length_trail where ‹isa_length_trail = (λ (M', xs, lvls, reasons, k, cs). length_uint32_nat M')› lemma isa_length_trail_pre: ‹(M, M') ∈ trail_pol 𝒜 ⟹ isa_length_trail_pre M› by (auto simp: isa_length_trail_def trail_pol_alt_def isa_length_trail_pre_def) lemma isa_length_trail_length_u: ‹(RETURN o isa_length_trail, RETURN o length_uint32_nat) ∈ trail_pol 𝒜 →_f ⟨nat_rel⟩nres_rel› by (intro frefI nres_relI) (auto simp: isa_length_trail_def trail_pol_alt_def intro!: ASSERT_leI) definition mop_isa_length_trail where ‹mop_isa_length_trail = (λ(M). do { ASSERT(isa_length_trail_pre M); RETURN (isa_length_trail M) })› lemma mop_isa_length_trail_length_u: ‹(mop_isa_length_trail, RETURN o length_uint32_nat) ∈ trail_pol 𝒜 →_f ⟨nat_rel⟩nres_rel› by (intro frefI nres_relI) (auto simp: mop_isa_length_trail_def isa_length_trail_def dest: isa_length_trail_pre intro!: ASSERT_leI, auto simp: trail_pol_alt_def) subsection ‹Consing elements› definition cons_trail_Propagated_tr_pre where ‹cons_trail_Propagated_tr_pre = (λ((L, C), (M, xs, lvls, reasons, k)). nat_of_lit L < length xs ∧ nat_of_lit (-L) < length xs ∧ atm_of L < length lvls ∧ atm_of L < length reasons ∧ length M < unat32_max)› definition cons_trail_Propagated_tr :: ‹nat literal ⇒ nat ⇒ trail_pol ⇒ trail_pol nres› where ‹cons_trail_Propagated_tr = (λL C (M', xs, lvls, reasons, k, cs, zeroed). do { ASSERT(cons_trail_Propagated_tr_pre ((L, C), (M', xs, lvls, reasons, k, cs, zeroed))); RETURN (M' @ [L], let xs = xs[nat_of_lit L := SET_TRUE] in xs[nat_of_lit (-L) := SET_FALSE], lvls[atm_of L := k], reasons[atm_of L:= C], k, cs, zeroed)})› lemma in_list_pos_neg_notD: ‹Pos (atm_of (lit_of La)) ∉ lits_of_l bc ⟹ Neg (atm_of (lit_of La)) ∉ lits_of_l bc ⟹ La ∈ set bc ⟹ False› by (metis Neg_atm_of_iff Pos_atm_of_iff lits_of_def rev_image_eqI) lemma cons_trail_Propagated_tr_pre: assumes ‹(M', M) ∈ trail_pol 𝒜› and ‹undefined_lit M L› and ‹L ∈# ℒ_a_l_l 𝒜› and ‹C ≠ DECISION_REASON› shows ‹cons_trail_Propagated_tr_pre ((L, C), M')› using assms by (auto simp: trail_pol_alt_def ann_lits_split_reasons_def uminus_𝒜_i_n_iff cons_trail_Propagated_tr_pre_def intro!: ext) lemma cons_trail_Propagated_tr: ‹(uncurry2 (cons_trail_Propagated_tr), uncurry2 (cons_trail_propagate_l)) ∈ [λ((L, C), M). L ∈# ℒ_a_l_l 𝒜 ∧ C ≠ DECISION_REASON]_f Id ×_f nat_rel ×_f trail_pol 𝒜 → ⟨trail_pol 𝒜⟩nres_rel› unfolding cons_trail_Propagated_tr_def cons_trail_propagate_l_def apply (intro frefI nres_relI) subgoal for x y using cons_trail_Propagated_tr_pre[of ‹snd (x)› ‹snd (y)› 𝒜 ‹fst (fst y)› ‹snd (fst y)›] unfolding uncurry_def apply refine_vcg subgoal by auto subgoal by (cases ‹fst (fst y)›) (auto simp add: trail_pol_def polarity_def uminus_lit_swap cons_trail_Propagated_tr_def Decided_Propagated_in_iff_in_lits_of_l nth_list_update' ann_lits_split_reasons_def atms_of_ℒ_a_l_l_𝒜_i_n uminus_𝒜_i_n_iff atm_of_eq_atm_of intro!: ASSERT_refine_right dest!: in_list_pos_neg_notD dest: pos_lit_in_atms_of neg_lit_in_atms_of dest!: multi_member_split simp del: nat_of_lit.simps) done done lemma cons_trail_Propagated_tr2: ‹(((L, C), M), ((L', C'), M')) ∈ Id ×_f Id ×_f trail_pol 𝒜 ⟹ L ∈# ℒ_a_l_l 𝒜 ⟹ C ≠ DECISION_REASON ⟹ cons_trail_Propagated_tr L C M ≤ ⇓ ({(M'', M'''). (M'', M''') ∈ trail_pol 𝒜 ∧ M''' = Propagated L C # M' ∧ no_dup M'''}) (cons_trail_propagate_l L' C' M')› using cons_trail_Propagated_tr[THEN fref_to_Down_curry2, of 𝒜 L' C' M' L C M] unfolding cons_trail_Propagated_tr_def cons_trail_propagate_l_def using cons_trail_Propagated_tr_pre[of M M' 𝒜 L C] unfolding uncurry_def apply refine_vcg subgoal by auto subgoal by (auto simp: trail_pol_def) done lemma undefined_lit_count_decided_unat32_max: assumes M_ℒ_a_l_l: ‹∀L∈set M. lit_of L ∈# ℒ_a_l_l 𝒜› and n_d: ‹no_dup M› and ‹L ∈# ℒ_a_l_l 𝒜› and ‹undefined_lit M L› and bounded: ‹isasat_input_bounded 𝒜› shows ‹Suc (count_decided M) ≤ unat32_max› proof - have dist_atm_M: ‹distinct_mset {#atm_of (lit_of x). x ∈# mset M#}› using n_d by (metis distinct_mset_mset_distinct mset_map no_dup_def) have incl: ‹atm_of `# lit_of `# mset (Decided L # M) ⊆# remdups_mset (atm_of `# ℒ_a_l_l 𝒜)› apply (subst distinct_subseteq_iff[THEN iffD1]) using assms dist_atm_M by (auto simp: Decided_Propagated_in_iff_in_lits_of_l lits_of_def no_dup_distinct atm_of_eq_atm_of) from size_mset_mono[OF this] have 1: ‹count_decided M + 1 ≤ size (remdups_mset (atm_of `# ℒ_a_l_l 𝒜))› using length_filter_le[of is_decided M] unfolding unat32_max_def count_decided_def by (auto simp del: length_filter_le) have inj_on: ‹inj_on nat_of_lit (set_mset (remdups_mset (ℒ_a_l_l 𝒜)))› by (auto simp: inj_on_def) have H: ‹xa ∈# ℒ_a_l_l 𝒜 ⟹ atm_of xa ≤ unat32_max div 2› for xa using bounded by (cases xa) (auto simp: unat32_max_def) have ‹remdups_mset (atm_of `# ℒ_a_l_l 𝒜) ⊆# mset [0..< 1 + (unat32_max div 2)]› apply (subst distinct_subseteq_iff[THEN iffD1]) using H distinct_image_mset_inj[OF inj_on] by (force simp del: literal_of_nat.simps simp: distinct_mset_mset_set dest: le_neq_implies_less)+ note _ = size_mset_mono[OF this] moreover have ‹size (nat_of_lit `# remdups_mset (ℒ_a_l_l 𝒜)) = size (remdups_mset (ℒ_a_l_l 𝒜))› by simp ultimately have 2: ‹size (remdups_mset (atm_of `# (ℒ_a_l_l 𝒜))) ≤ 1 + unat32_max div 2› by auto show ?thesis using 1 2 by (auto simp: unat32_max_def) from size_mset_mono[OF incl] have 1: ‹length M + 1 ≤ size (remdups_mset (atm_of `# ℒ_a_l_l 𝒜))› unfolding unat32_max_def count_decided_def by (auto simp del: length_filter_le) with 2 have ‹length M ≤ unat32_max› by auto qed lemma length_trail_unat32_max: assumes M_ℒ_a_l_l: ‹∀L∈set M. lit_of L ∈# ℒ_a_l_l 𝒜› and n_d: ‹no_dup M› and bounded: ‹isasat_input_bounded 𝒜› shows ‹length M ≤ unat32_max› proof - have dist_atm_M: ‹distinct_mset {#atm_of (lit_of x). x ∈# mset M#}› using n_d by (metis distinct_mset_mset_distinct mset_map no_dup_def) have incl: ‹atm_of `# lit_of `# mset M ⊆# remdups_mset (atm_of `# ℒ_a_l_l 𝒜)› apply (subst distinct_subseteq_iff[THEN iffD1]) using assms dist_atm_M by (auto simp: Decided_Propagated_in_iff_in_lits_of_l lits_of_def no_dup_distinct atm_of_eq_atm_of) have inj_on: ‹inj_on nat_of_lit (set_mset (remdups_mset (ℒ_a_l_l 𝒜)))› by (auto simp: inj_on_def) have H: ‹xa ∈# ℒ_a_l_l 𝒜 ⟹ atm_of xa ≤ unat32_max div 2› for xa using bounded by (cases xa) (auto simp: unat32_max_def) have ‹remdups_mset (atm_of `# ℒ_a_l_l 𝒜) ⊆# mset [0..< 1 + (unat32_max div 2)]› apply (subst distinct_subseteq_iff[THEN iffD1]) using H distinct_image_mset_inj[OF inj_on] by (force simp del: literal_of_nat.simps simp: distinct_mset_mset_set dest: le_neq_implies_less)+ note _ = size_mset_mono[OF this] moreover have ‹size (nat_of_lit `# remdups_mset (ℒ_a_l_l 𝒜)) = size (remdups_mset (ℒ_a_l_l 𝒜))› by simp ultimately have 2: ‹size (remdups_mset (atm_of `# ℒ_a_l_l 𝒜)) ≤ 1 + unat32_max div 2› by auto from size_mset_mono[OF incl] have 1: ‹length M ≤ size (remdups_mset (atm_of `# ℒ_a_l_l 𝒜))› unfolding unat32_max_def count_decided_def by (auto simp del: length_filter_le) with 2 show ?thesis by (auto simp: unat32_max_def) qed definition last_trail_pol_pre where ‹last_trail_pol_pre = (λ(M, xs, lvls, reasons, k). atm_of (last M) < length reasons ∧ M ≠ [])› definition (in -) last_trail_pol :: ‹trail_pol ⇒ (nat literal × nat option)› where ‹last_trail_pol = (λ(M, xs, lvls, reasons, k). let r = reasons ! (atm_of (last M)) in (last M, if r = DECISION_REASON then None else Some r))› definition tl_trailt_tr :: ‹trail_pol ⇒ trail_pol› where ‹tl_trailt_tr = (λ(M', xs, lvls, reasons, k, cs, zeroed). let L = last M' in (butlast M', let xs = xs[nat_of_lit L := None] in xs[nat_of_lit (-L) := None], lvls[atm_of L := 0], reasons, if reasons ! atm_of L = DECISION_REASON then k-1 else k, if reasons ! atm_of L = DECISION_REASON then butlast cs else cs, zeroed))› definition tl_trailt_tr_pre where ‹tl_trailt_tr_pre = (λ(M, xs, lvls, reason, k, cs, zeroed). M ≠ [] ∧ nat_of_lit(last M) < length xs ∧ nat_of_lit(-last M) < length xs ∧ atm_of (last M) < length lvls ∧ atm_of (last M) < length reason ∧ (reason ! atm_of (last M) = DECISION_REASON ⟶ k ≥ 1 ∧ cs ≠ []))› lemma ann_lits_split_reasons_map_lit_of: ‹((M, reasons), M') ∈ ann_lits_split_reasons 𝒜 ⟹ M = map lit_of (rev M')› by (auto simp: ann_lits_split_reasons_def) lemma control_stack_dec_butlast: ‹control_stack b (Decided x1 # M's) ⟹ control_stack (butlast b) M's› by (cases b rule: rev_cases) (auto dest: control_stackE) lemma tl_trail_tr: ‹((RETURN o tl_trailt_tr), (RETURN o tl)) ∈ [λM. M ≠ [] ∧ count_decided M > 0]_f trail_pol 𝒜 → ⟨trail_pol 𝒜⟩nres_rel› proof - show ?thesis apply (intro frefI nres_relI, rename_tac x y, case_tac ‹y›) subgoal by fast subgoal for M M' L M's unfolding trail_pol_def comp_def RETURN_refine_iff trail_pol_def Let_def apply clarify apply (intro conjI; clarify?; (intro conjI)?) subgoal by (auto simp: trail_pol_def polarity_atm_def tl_trailt_tr_def ann_lits_split_reasons_def Let_def) subgoal by (auto simp: trail_pol_def polarity_atm_def tl_trailt_tr_def) subgoal by (auto simp: polarity_atm_def tl_trailt_tr_def Let_def) subgoal by (cases ‹lit_of L›) (auto simp: polarity_def tl_trailt_tr_def Decided_Propagated_in_iff_in_lits_of_l uminus_lit_swap Let_def dest: ann_lits_split_reasons_map_lit_of) subgoal by (auto simp: polarity_atm_def tl_trailt_tr_def Let_def atm_of_eq_atm_of get_level_cons_if) subgoal by (auto simp: polarity_atm_def tl_trailt_tr_def atm_of_eq_atm_of get_level_cons_if Let_def dest!: ann_lits_split_reasons_map_lit_of) subgoal by (cases ‹L›) (auto simp: tl_trailt_tr_def in_ℒ_a_l_l_atm_of_in_atms_of_iff ann_lits_split_reasons_def dest: no_dup_consistentD) subgoal by (auto simp: tl_trailt_tr_def) subgoal by (cases ‹L›) (auto simp: tl_trailt_tr_def in_ℒ_a_l_l_atm_of_in_atms_of_iff ann_lits_split_reasons_def control_stack_dec_butlast dest: no_dup_consistentD) subgoal by (cases ‹L›) (auto simp: tl_trailt_tr_def in_ℒ_a_l_l_atm_of_in_atms_of_iff ann_lits_split_reasons_def control_stack_dec_butlast dest: no_dup_consistentD zeroed_trail_consD) done done qed lemma tl_trailt_tr_pre: assumes ‹M ≠ []› ‹(M', M) ∈ trail_pol 𝒜› shows ‹tl_trailt_tr_pre M'› proof - have [simp]: ‹x ≠ [] ⟹ is_decided (last x) ⟹ Suc 0 ≤ count_decided x› for x by (cases x rule: rev_cases) auto show ?thesis using assms by (cases M; cases ‹hd M›) (auto simp: trail_pol_def ann_lits_split_reasons_def uminus_𝒜_i_n_iff rev_map[symmetric] hd_append hd_map tl_trailt_tr_pre_def simp del: rev_map intro!: ext) qed definition tl_trail_propedt_tr :: ‹trail_pol ⇒ trail_pol› where ‹tl_trail_propedt_tr = (λ(M', xs, lvls, reasons, k, cs). let L = last M' in (butlast M', let xs = xs[nat_of_lit L := None] in xs[nat_of_lit (-L) := None], lvls[atm_of L := 0], reasons, k, cs))› definition tl_trail_propedt_tr_pre where ‹tl_trail_propedt_tr_pre = (λ(M, xs, lvls, reason, k, cs). M ≠ [] ∧ nat_of_lit(last M) < length xs ∧ nat_of_lit(-last M) < length xs ∧ atm_of (last M) < length lvls ∧ atm_of (last M) < length reason)› lemma tl_trail_propedt_tr_pre: assumes ‹(M', M) ∈ trail_pol 𝒜› and ‹M ≠ []› shows ‹tl_trail_propedt_tr_pre M'› using assms unfolding trail_pol_def comp_def RETURN_refine_iff trail_pol_def Let_def tl_trail_propedt_tr_def tl_trail_propedt_tr_pre_def apply clarify apply (cases M; intro conjI; clarify?; (intro conjI)?) subgoal by (auto simp: trail_pol_def polarity_atm_def tl_trailt_tr_def ann_lits_split_reasons_def Let_def) subgoal by (auto simp: polarity_atm_def tl_trailt_tr_def atm_of_eq_atm_of get_level_cons_if Let_def dest!: ann_lits_split_reasons_map_lit_of) subgoal by (cases ‹hd M›) (auto simp: tl_trailt_tr_def in_ℒ_a_l_l_atm_of_in_atms_of_iff ann_lits_split_reasons_def dest: no_dup_consistentD) subgoal by (cases ‹hd M›) (auto simp: tl_trailt_tr_def in_ℒ_a_l_l_atm_of_in_atms_of_iff ann_lits_split_reasons_def control_stack_dec_butlast dest: no_dup_consistentD) subgoal by (cases ‹hd M›) (auto simp: tl_trailt_tr_def in_ℒ_a_l_l_atm_of_in_atms_of_iff ann_lits_split_reasons_def control_stack_dec_butlast dest: no_dup_consistentD) done definition (in -) lit_of_hd_trail where ‹lit_of_hd_trail M = lit_of (hd M)› definition (in -) lit_of_last_trail_pol where ‹lit_of_last_trail_pol = (λ(M, _). last M)› lemma lit_of_last_trail_pol_lit_of_last_trail: ‹(RETURN o lit_of_last_trail_pol, RETURN o lit_of_hd_trail) ∈ [λS. S ≠ []]_f trail_pol 𝒜 → ⟨Id⟩nres_rel› by (auto simp: lit_of_hd_trail_def trail_pol_def lit_of_last_trail_pol_def ann_lits_split_reasons_def hd_map rev_map[symmetric] last_rev intro!: frefI nres_relI) subsection ‹Setting a new literal› definition cons_trail_Decided :: ‹nat literal ⇒ (nat, nat) ann_lits ⇒ (nat, nat) ann_lits› where ‹cons_trail_Decided L M' = Decided L # M'› definition cons_trail_Decided_tr :: ‹nat literal ⇒ trail_pol ⇒ trail_pol› where ‹cons_trail_Decided_tr = (λL (M', xs, lvls, reasons, k, cs, zeroed). do{ let n = length M' in (M' @ [L], let xs = xs[nat_of_lit L := SET_TRUE] in xs[nat_of_lit (-L) := SET_FALSE], lvls[atm_of L := k+1], reasons[atm_of L := DECISION_REASON], k+1, cs @ [n], zeroed)})› definition cons_trail_Decided_tr_pre where ‹cons_trail_Decided_tr_pre = (λ(L, (M, xs, lvls, reason, k, cs, zeroed)). nat_of_lit L < length xs ∧ nat_of_lit (-L) < length xs ∧ atm_of L < length lvls ∧ atm_of L < length reason ∧ length cs < unat32_max ∧ Suc k ≤ unat32_max ∧ length M < unat32_max)› lemma length_cons_trail_Decided[simp]: ‹length (cons_trail_Decided L M) = Suc (length M)› by (auto simp: cons_trail_Decided_def) lemma cons_trail_Decided_tr: ‹(uncurry (RETURN oo cons_trail_Decided_tr), uncurry (RETURN oo cons_trail_Decided)) ∈ [λ(L, M). undefined_lit M L ∧ L ∈# ℒ_a_l_l 𝒜]_f Id ×_f trail_pol 𝒜 → ⟨trail_pol 𝒜⟩nres_rel› by (intro frefI nres_relI, rename_tac x y, case_tac ‹fst x›) (auto simp: trail_pol_def polarity_def cons_trail_Decided_def uminus_lit_swap Decided_Propagated_in_iff_in_lits_of_l cons_trail_Decided_tr_def nth_list_update' ann_lits_split_reasons_def dest!: in_list_pos_neg_notD multi_member_split intro: control_stack.cons_dec simp del: nat_of_lit.simps) lemma cons_trail_Decided_tr_pre: assumes ‹(M', M) ∈ trail_pol 𝒜› and ‹L ∈# ℒ_a_l_l 𝒜› and ‹undefined_lit M L› shows ‹cons_trail_Decided_tr_pre (L, M')› using assms by (auto simp: trail_pol_alt_def image_image ann_lits_split_reasons_def uminus_𝒜_i_n_iff cons_trail_Decided_tr_pre_def control_stack_length_count_dec intro!: ext undefined_lit_count_decided_unat32_max length_trail_unat32_max) subsection ‹Polarity: Defined or Undefined› definition (in -) defined_atm_pol_pre where ‹defined_atm_pol_pre = (λ(M, xs, lvls, k) L. 2*L < length xs ∧ 2*L ≤ unat32_max)› definition (in -) defined_atm_pol where ‹defined_atm_pol = (λ(M, xs, lvls, k) L. ¬((xs!(2*L)) = None))› lemma undefined_atm_code: ‹(uncurry (RETURN oo defined_atm_pol), uncurry (RETURN oo defined_atm)) ∈ [λ(M, L). Pos L ∈# ℒ_a_l_l 𝒜]_f trail_pol 𝒜 ×_r Id → ⟨bool_rel⟩ nres_rel› (is ?A) and defined_atm_pol_pre: ‹(M', M) ∈ trail_pol 𝒜 ⟹ L ∈# 𝒜 ⟹ defined_atm_pol_pre M' L› proof - have H: ‹2*L < length xs› (is ‹?length›) and none: ‹defined_atm M L ⟷ xs ! (2*L) ≠ None› (is ?undef) and le: ‹2*L ≤ unat32_max› (is ?le) if L_N: ‹Pos L ∈# ℒ_a_l_l 𝒜› and tr: ‹((M', xs, lvls, k), M) ∈ trail_pol 𝒜› for M xs lvls k M' L proof - have ‹M' = map lit_of (rev M)› and ‹∀L∈#ℒ_a_l_l 𝒜. nat_of_lit L < length xs ∧ xs ! nat_of_lit L = polarity M L› using tr unfolding trail_pol_def ann_lits_split_reasons_def by fast+ then have L: ‹nat_of_lit (Pos L) < length xs› and xsL: ‹xs ! (nat_of_lit (Pos L)) = polarity M (Pos L)› using L_N by (auto dest!: multi_member_split) show ?length using L by simp show ?undef using xsL by (auto simp: polarity_def defined_atm_def Decided_Propagated_in_iff_in_lits_of_l split: if_splits) show ‹2*L ≤ unat32_max› using tr L_N unfolding trail_pol_def by auto qed show ?A unfolding defined_atm_pol_def by (intro frefI nres_relI) (auto 5 5 simp: none H le intro!: ASSERT_leI) show ‹(M', M) ∈ trail_pol 𝒜 ⟹ L ∈# 𝒜 ⟹ defined_atm_pol_pre M' L› using H le by (auto simp: defined_atm_pol_pre_def in_ℒ_a_l_l_atm_of_𝒜_i_n) qed subsection ‹Reasons› definition get_propagation_reason_pol :: ‹trail_pol ⇒ nat literal ⇒ nat option nres› where ‹get_propagation_reason_pol = (λ(_, _, _, reasons, _) L. do { ASSERT(atm_of L < length reasons); let r = reasons ! atm_of L; RETURN (if r = DECISION_REASON then None else Some r)})› lemma get_propagation_reason_pol: ‹(uncurry get_propagation_reason_pol, uncurry get_propagation_reason) ∈ [λ(M, L). L ∈ lits_of_l M]_f trail_pol 𝒜 ×_r Id → ⟨⟨nat_rel⟩option_rel⟩ nres_rel› apply (intro frefI nres_relI) unfolding lits_of_def apply clarify apply (rename_tac a aa ab ac b ba ad bb x, case_tac x) by (auto simp: get_propagation_reason_def get_propagation_reason_pol_def trail_pol_def ann_lits_split_reasons_def lits_of_def assert_bind_spec_conv) definition get_propagation_reason_raw_pol :: ‹trail_pol ⇒ nat literal ⇒ nat nres› where ‹get_propagation_reason_raw_pol = (λ(_, _, _, reasons, _) L. do { ASSERT(atm_of L < length reasons); let r = reasons ! atm_of L; RETURN r})› text ‹The version term‹get_propagation_reason› can return the reason, but does not have to: it can be more suitable for specification (like for the conflict minimisation, where finding the reason is not mandatory). The following version ∗‹always› returns the reasons if there is one. Remark that both functions are linked to the same code (but term‹get_propagation_reason› can be called first with some additional filtering later). › definition (in -) get_the_propagation_reason :: ‹('v, 'mark) ann_lits ⇒ 'v literal ⇒ 'mark option nres› where ‹get_the_propagation_reason M L = SPEC(λC. (C ≠ None ⟷ Propagated L (the C) ∈ set M) ∧ (C = None ⟷ Decided L ∈ set M ∨ L ∉ lits_of_l M))› lemma no_dup_Decided_PropedD: ‹no_dup ad ⟹ Decided L ∈ set ad ⟹ Propagated L C ∈ set ad ⟹ False› by (metis annotated_lit.distinct(1) in_set_conv_decomp lit_of.simps(1) lit_of.simps(2) no_dup_appendD no_dup_cons undefined_notin xy_in_set_cases) definition get_the_propagation_reason_pol :: ‹trail_pol ⇒ nat literal ⇒ nat option nres› where ‹get_the_propagation_reason_pol = (λ(_, xs, _, reasons, _, _) L. do { ASSERT(atm_of L < length reasons); ASSERT(nat_of_lit L < length xs); let r = reasons ! atm_of L; RETURN (if xs ! nat_of_lit L = SET_TRUE ∧ r ≠ DECISION_REASON then Some r else None)})› lemma get_the_propagation_reason_pol: ‹(uncurry get_the_propagation_reason_pol, uncurry get_the_propagation_reason) ∈ [λ(M, L). L ∈# ℒ_a_l_l 𝒜]_f trail_pol 𝒜 ×_r Id → ⟨⟨nat_rel⟩option_rel⟩ nres_rel› proof - have [dest]: ‹no_dup bb ⟹ SET_TRUE = polarity bb (Pos x1) ⟹ Pos x1 ∈ lits_of_l bb ∧ Neg x1 ∉ lits_of_l bb› for bb x1 by (auto simp: polarity_def split: if_splits dest: no_dup_consistentD) show ?thesis apply (intro frefI nres_relI) unfolding lits_of_def get_the_propagation_reason_def uncurry_def get_the_propagation_reason_pol_def apply clarify apply (refine_vcg) subgoal by (auto simp: get_the_propagation_reason_def get_the_propagation_reason_pol_def Let_def trail_pol_def ann_lits_split_reasons_def assert_bind_spec_conv dest!: multi_member_split[of _ ‹ℒ_a_l_l 𝒜›])[] subgoal by (auto simp: get_the_propagation_reason_def get_the_propagation_reason_pol_def Let_def trail_pol_def ann_lits_split_reasons_def assert_bind_spec_conv dest!: multi_member_split[of _ ‹ℒ_a_l_l 𝒜›])[] subgoal for a aa ab ac ad zeroed b ba ae bb apply (cases ‹aa ! nat_of_lit ba ≠ SET_TRUE›) apply (subgoal_tac ‹ba ∉ lits_of_l ae›) prefer 2 subgoal by (auto simp: get_the_propagation_reason_def get_the_propagation_reason_pol_def Let_def trail_pol_def ann_lits_split_reasons_def assert_bind_spec_conv polarity_spec'(2) dest: multi_member_split[of _ ‹ℒ_a_l_l 𝒜›])[] subgoal by (auto simp: lits_of_def dest: imageI[of _ _ lit_of]) apply (subgoal_tac ‹ba ∈ lits_of_l ae›) prefer 2 subgoal by (auto simp: get_the_propagation_reason_def get_the_propagation_reason_pol_def Let_def trail_pol_def ann_lits_split_reasons_def assert_bind_spec_conv polarity_spec'(2) dest: multi_member_split[of _ ‹ℒ_a_l_l 𝒜›])[] subgoal apply (auto simp: get_the_propagation_reason_def get_the_propagation_reason_pol_def Let_def trail_pol_def ann_lits_split_reasons_def assert_bind_spec_conv lits_of_def dest!: multi_member_split[of _ ‹ℒ_a_l_l 𝒜›])[] apply (case_tac x; auto) apply (case_tac x; auto) done done done qed section ‹Direct access to elements in the trail› definition (in -) rev_trail_nth where ‹rev_trail_nth M i = lit_of (rev M ! i)› definition (in -) isa_trail_nth :: ‹trail_pol ⇒ nat ⇒ nat literal nres› where ‹isa_trail_nth = (λ(M, _) i. do { ASSERT(i < length M); RETURN (M ! i) })› lemma isa_trail_nth_rev_trail_nth: ‹(uncurry isa_trail_nth, uncurry (RETURN oo rev_trail_nth)) ∈ [λ(M, i). i < length M]_f trail_pol 𝒜 ×_r nat_rel → ⟨Id⟩nres_rel› by (intro frefI nres_relI) (auto simp: isa_trail_nth_def rev_trail_nth_def trail_pol_def ann_lits_split_reasons_def intro!: ASSERT_leI) text ‹We here define a variant of the trail representation, where the the control stack is out of sync of the trail (i.e., there are some leftovers at the end). This might make backtracking a little faster. › definition trail_pol_no_CS :: ‹nat multiset ⇒ (trail_pol × (nat, nat) ann_lits) set› where ‹trail_pol_no_CS 𝒜 = {((M', xs, lvls, reasons, k, cs, zeroed), M). ((M', reasons), M) ∈ ann_lits_split_reasons 𝒜 ∧ no_dup M ∧ (∀L ∈# ℒ_a_l_l 𝒜. nat_of_lit L < length xs ∧ xs ! (nat_of_lit L) = polarity M L) ∧ (∀L ∈# ℒ_a_l_l 𝒜. atm_of L < length lvls ∧ lvls ! (atm_of L) = get_level M L) ∧ (∀L∈set M. lit_of L ∈# ℒ_a_l_l 𝒜) ∧ isasat_input_bounded 𝒜 ∧ zeroed_trail M zeroed ∧ control_stack (take (count_decided M) cs) M }› definition tl_trailt_tr_no_CS :: ‹trail_pol ⇒ trail_pol› where ‹tl_trailt_tr_no_CS = (λ(M', xs, lvls, reasons, k, cs, zeroed). let L = last M' in (butlast M', let xs = xs[nat_of_lit L := None] in xs[nat_of_lit (-L) := None], lvls[atm_of L := 0], reasons, k, cs, zeroed))› definition tl_trailt_tr_no_CS_pre where ‹tl_trailt_tr_no_CS_pre = (λ(M, xs, lvls, reason, k, cs). M ≠ [] ∧ nat_of_lit(last M) < length xs ∧ nat_of_lit(-last M) < length xs ∧ atm_of (last M) < length lvls ∧ atm_of (last M) < length reason)› lemma control_stack_take_Suc_count_dec_unstack: ‹control_stack (take (Suc (count_decided M's)) cs) (Decided x1 # M's) ⟹ control_stack (take (count_decided M's) cs) M's› using control_stack_length_count_dec[of ‹take (Suc (count_decided M's)) cs› ‹Decided x1 # M's›] by (auto simp: min_def take_Suc_conv_app_nth split: if_splits elim: control_stackE) lemma tl_trailt_tr_no_CS_pre: assumes ‹(M', M) ∈ trail_pol_no_CS 𝒜› and ‹M ≠ []› shows ‹tl_trailt_tr_no_CS_pre M'› proof - have [simp]: ‹x ≠ [] ⟹ is_decided (last x) ⟹ Suc 0 ≤ count_decided x› for x by (cases x rule: rev_cases) auto show ?thesis using assms unfolding trail_pol_def comp_def RETURN_refine_iff trail_pol_no_CS_def Let_def tl_trailt_tr_no_CS_def tl_trailt_tr_no_CS_pre_def by (cases M; cases ‹hd M›) (auto simp: trail_pol_no_CS_def ann_lits_split_reasons_def uminus_𝒜_i_n_iff rev_map[symmetric] hd_append hd_map simp del: rev_map intro!: ext) qed lemma tl_trail_tr_no_CS: ‹((RETURN o tl_trailt_tr_no_CS), (RETURN o tl)) ∈ [λM. M ≠ [] ∧ count_decided M > 0]_f trail_pol_no_CS 𝒜 → ⟨trail_pol_no_CS 𝒜⟩nres_rel› apply (intro frefI nres_relI, rename_tac x y, case_tac ‹y›) subgoal by fast subgoal for M M' L M's unfolding trail_pol_def comp_def RETURN_refine_iff trail_pol_no_CS_def Let_def tl_trailt_tr_no_CS_def apply clarify apply (intro conjI; clarify?; (intro conjI)?) subgoal by (auto simp: trail_pol_def polarity_atm_def tl_trailt_tr_def ann_lits_split_reasons_def Let_def) subgoal by (auto simp: trail_pol_def polarity_atm_def tl_trailt_tr_def) subgoal by (auto simp: polarity_atm_def tl_trailt_tr_def Let_def) subgoal by (cases ‹lit_of L›) (auto simp: polarity_def tl_trailt_tr_def Decided_Propagated_in_iff_in_lits_of_l uminus_lit_swap Let_def dest: ann_lits_split_reasons_map_lit_of) subgoal by (auto simp: polarity_atm_def tl_trailt_tr_def Let_def atm_of_eq_atm_of get_level_cons_if) subgoal by (auto simp: polarity_atm_def tl_trailt_tr_def atm_of_eq_atm_of get_level_cons_if Let_def dest!: ann_lits_split_reasons_map_lit_of) subgoal by (cases ‹L›) (auto simp: tl_trailt_tr_def in_ℒ_a_l_l_atm_of_in_atms_of_iff ann_lits_split_reasons_def control_stack_dec_butlast dest: no_dup_consistentD ann_lits_split_reasons_map_lit_of) subgoal by (cases ‹L›) (auto simp: tl_trailt_tr_def in_ℒ_a_l_l_atm_of_in_atms_of_iff ann_lits_split_reasons_def control_stack_dec_butlast control_stack_take_Suc_count_dec_unstack dest: no_dup_consistentD ann_lits_split_reasons_map_lit_of zeroed_trail_consD) subgoal by (cases ‹L›) (auto simp: tl_trailt_tr_def in_ℒ_a_l_l_atm_of_in_atms_of_iff ann_lits_split_reasons_def control_stack_dec_butlast control_stack_take_Suc_count_dec_unstack dest: no_dup_consistentD ann_lits_split_reasons_map_lit_of) done done definition trail_conv_to_no_CS :: ‹(nat, nat) ann_lits ⇒ (nat, nat) ann_lits› where ‹trail_conv_to_no_CS M = M› definition trail_pol_conv_to_no_CS :: ‹trail_pol ⇒ trail_pol› where ‹trail_pol_conv_to_no_CS M = M› lemma id_trail_conv_to_no_CS: ‹(RETURN o trail_pol_conv_to_no_CS, RETURN o trail_conv_to_no_CS) ∈ trail_pol 𝒜 →_f ⟨trail_pol_no_CS 𝒜⟩nres_rel› by (intro frefI nres_relI) (auto simp: trail_pol_no_CS_def trail_conv_to_no_CS_def trail_pol_def control_stack_length_count_dec trail_pol_conv_to_no_CS_def intro: ext) definition trail_conv_back :: ‹nat ⇒ (nat, nat) ann_lits ⇒ (nat, nat) ann_lits› where ‹trail_conv_back j M = M› definition (in -) trail_conv_back_imp :: ‹nat ⇒ trail_pol ⇒ trail_pol nres› where ‹trail_conv_back_imp j = (λ(M, xs, lvls, reason, _, cs, zeroed). do { ASSERT(j ≤ length cs); RETURN (M, xs, lvls, reason, j, take (j) cs, zeroed)})› lemma trail_conv_back: ‹(uncurry trail_conv_back_imp, uncurry (RETURN oo trail_conv_back)) ∈ [λ(k, M). k = count_decided M]_f nat_rel ×_f trail_pol_no_CS 𝒜 → ⟨trail_pol 𝒜⟩nres_rel› by (intro frefI nres_relI) (force simp: trail_pol_no_CS_def trail_conv_to_no_CS_def trail_pol_def control_stack_length_count_dec trail_conv_back_def trail_conv_back_imp_def intro: ext intro!: ASSERT_refine_left dest: control_stack_length_count_dec multi_member_split) definition (in -)take_arl where ‹take_arl = (λi (xs, j). (xs, i))› lemma isa_trail_nth_rev_trail_nth_no_CS: ‹(uncurry isa_trail_nth, uncurry (RETURN oo rev_trail_nth)) ∈ [λ(M, i). i < length M]_f trail_pol_no_CS 𝒜 ×_r nat_rel → ⟨Id⟩nres_rel› by (intro frefI nres_relI) (auto simp: isa_trail_nth_def rev_trail_nth_def trail_pol_def ann_lits_split_reasons_def trail_pol_no_CS_def intro!: ASSERT_leI) lemma trail_pol_no_CS_alt_def: ‹trail_pol_no_CS 𝒜 = {((M', xs, lvls, reasons, k, cs, zeroed), M). ((M', reasons), M) ∈ ann_lits_split_reasons 𝒜 ∧ no_dup M ∧ (∀L ∈# ℒ_a_l_l 𝒜. nat_of_lit L < length xs ∧ xs ! (nat_of_lit L) = polarity M L) ∧ (∀L ∈# ℒ_a_l_l 𝒜. atm_of L < length lvls ∧ lvls ! (atm_of L) = get_level M L) ∧ (∀L∈set M. lit_of L ∈# ℒ_a_l_l 𝒜) ∧ control_stack (take (count_decided M) cs) M ∧ literals_are_in_ℒ_i_n_trail 𝒜 M ∧ length M < unat32_max ∧ length M ≤ unat32_max div 2 + 1 ∧ count_decided M < unat32_max ∧ length M' = length M ∧ zeroed_trail M zeroed ∧ isasat_input_bounded 𝒜 ∧ M' = map lit_of (rev M) }› proof - have [intro!]: ‹length M < n ⟹ count_decided M < n› for M n using length_filter_le[of is_decided M] by (auto simp: literals_are_in_ℒ_i_n_trail_def unat32_max_def count_decided_def simp del: length_filter_le dest: length_trail_unat32_max_div2) show ?thesis unfolding trail_pol_no_CS_def by (auto simp: literals_are_in_ℒ_i_n_trail_def unat32_max_def ann_lits_split_reasons_def dest: length_trail_unat32_max_div2 simp del: isasat_input_bounded_def) qed (* TODO: Kill the other definition *) lemma isa_length_trail_length_u_no_CS: ‹(RETURN o isa_length_trail, RETURN o length_uint32_nat) ∈ trail_pol_no_CS 𝒜 →_f ⟨nat_rel⟩nres_rel› by (intro frefI nres_relI) (auto simp: isa_length_trail_def trail_pol_no_CS_alt_def ann_lits_split_reasons_def intro!: ASSERT_leI) lemma control_stack_is_decided: ‹control_stack cs M ⟹ c∈set cs ⟹ is_decided ((rev M)!c)› by (induction arbitrary: c rule: control_stack.induct) (auto simp: nth_append dest: control_stack_le_length_M) lemma control_stack_distinct: ‹control_stack cs M ⟹ distinct cs› by (induction rule: control_stack.induct) (auto simp: nth_append dest: control_stack_le_length_M) lemma control_stack_level_control_stack: assumes cs: ‹control_stack cs M› and n_d: ‹no_dup M› and i: ‹i < length cs› shows ‹get_level M (lit_of (rev M ! (cs ! i))) = Suc i› proof - define L where ‹L = rev M ! (cs ! i)› have csi: ‹cs ! i < length M› using cs i by (auto intro: control_stack_le_length_M) then have L_M: ‹L ∈ set M› using nth_mem[of ‹cs !i› ‹rev M›] unfolding L_def by (auto simp del: nth_mem) have dec_L: ‹is_decided L› using control_stack_is_decided[OF cs] i unfolding L_def by auto then have ‹rev M!(cs ! (get_level M (lit_of L) - 1)) = L› using control_stack_rev_get_lev[OF cs n_d L_M] by auto moreover have ‹distinct M› using no_dup_distinct[OF n_d] unfolding mset_map[symmetric] distinct_mset_mset_distinct by (rule distinct_mapI) moreover have lev0: ‹get_level M (lit_of L) ≥ 1› using split_list[OF L_M] n_d dec_L by (auto simp: get_level_append_if) moreover have ‹cs ! (get_level M (lit_of (rev M ! (cs ! i))) - Suc 0) < length M› using control_stack_le_length_M[OF cs, of ‹cs ! (get_level M (lit_of (rev M ! (cs ! i))) - Suc 0)›, OF nth_mem] control_stack_length_count_dec[OF cs] count_decided_ge_get_level[of M ‹lit_of (rev M ! (cs ! i))›] lev0 by (auto simp: L_def) ultimately have ‹cs ! (get_level M (lit_of L) - 1) = cs ! i› using nth_eq_iff_index_eq[of ‹rev M›] csi unfolding L_def by auto then have ‹i = get_level M (lit_of L) - 1› using nth_eq_iff_index_eq[OF control_stack_distinct[OF cs], of i ‹get_level M (lit_of L) - 1›] i lev0 count_decided_ge_get_level[of M ‹lit_of (rev M ! (cs ! i))›] control_stack_length_count_dec[OF cs] by (auto simp: L_def) then show ?thesis using lev0 unfolding L_def[symmetric] by auto qed definition get_pos_of_level_in_trail where ‹get_pos_of_level_in_trail M₀ lev = SPEC(λi. i < length M₀ ∧ is_decided (rev M₀!i) ∧ get_level M₀ (lit_of (rev M₀!i)) = lev+1)› definition (in -) get_pos_of_level_in_trail_imp :: ‹trail_pol ⇒ nat ⇒ _› where ‹get_pos_of_level_in_trail_imp = (λ(M', xs, lvls, reasons, k, cs, zeroed) lev. do { ASSERT(lev < length cs); RETURN (cs ! lev) })› definition get_pos_of_level_in_trail_pre where ‹get_pos_of_level_in_trail_pre = (λ(M, lev). lev < count_decided M)› lemma get_pos_of_level_in_trail_imp_get_pos_of_level_in_trail: ‹(uncurry get_pos_of_level_in_trail_imp, uncurry get_pos_of_level_in_trail) ∈ [get_pos_of_level_in_trail_pre]_f trail_pol_no_CS 𝒜 ×_f nat_rel → ⟨nat_rel⟩nres_rel› apply (intro nres_relI frefI) unfolding get_pos_of_level_in_trail_imp_def uncurry_def get_pos_of_level_in_trail_def get_pos_of_level_in_trail_pre_def apply clarify apply (rule ASSERT_leI) subgoal by (auto simp: trail_pol_no_CS_alt_def dest!: control_stack_length_count_dec) subgoal for a aa ab ac ad b ba ae bb by (auto simp: trail_pol_no_CS_def control_stack_length_count_dec in_set_take_conv_nth intro!: control_stack_le_length_M control_stack_is_decided dest: control_stack_level_control_stack) done lemma get_pos_of_level_in_trail_imp_get_pos_of_level_in_trail_CS: ‹(uncurry get_pos_of_level_in_trail_imp, uncurry get_pos_of_level_in_trail) ∈ [get_pos_of_level_in_trail_pre]_f trail_pol 𝒜 ×_f nat_rel → ⟨nat_rel⟩nres_rel› apply (intro nres_relI frefI) unfolding get_pos_of_level_in_trail_imp_def uncurry_def get_pos_of_level_in_trail_def get_pos_of_level_in_trail_pre_def apply clarify apply (rule ASSERT_leI) subgoal by (auto simp: trail_pol_def dest!: control_stack_length_count_dec) subgoal for a aa ab ac ad b ba ae bb by (auto simp: trail_pol_def control_stack_length_count_dec in_set_take_conv_nth intro!: control_stack_le_length_M control_stack_is_decided dest: control_stack_level_control_stack) done lemma lit_of_last_trail_pol_lit_of_last_trail_no_CS: ‹(RETURN o lit_of_last_trail_pol, RETURN o lit_of_hd_trail) ∈ [λS. S ≠ []]_f trail_pol_no_CS 𝒜 → ⟨Id⟩nres_rel› by (auto simp: lit_of_hd_trail_def trail_pol_no_CS_def lit_of_last_trail_pol_def ann_lits_split_reasons_def hd_map rev_map[symmetric] last_rev intro!: frefI nres_relI) definition trail_height_before_conflict :: ‹trail_pol ⇒ nat nres› where ‹trail_height_before_conflict = (λ(M', xs, lvls, reasons, k, cs, zeroed). do{ if k = 0 then RETURN 0 else do { let k' = k-1; ASSERT (k' < length cs); RETURN (cs ! k') } })› definition trail_height_before_conflict_spec where ‹trail_height_before_conflict_spec _ = RES (UNIV :: nat set)› lemma trail_height_before_conflict: ‹(trail_height_before_conflict, trail_height_before_conflict_spec) ∈ trail_pol 𝒜 →_f⟨nat_rel⟩nres_rel› unfolding trail_height_before_conflict_def trail_height_before_conflict_spec_def Let_def by (intro frefI, refine_vcg) (auto simp: trail_pol_def control_stack_length_count_dec intro!: frefI ASSERT_leI) definition trail_zeroed_until :: ‹trail_pol ⇒ nat› where ‹trail_zeroed_until = (λ(M', xs, lvls, reasons, k, cs, zeroed). zeroed)› definition trail_set_zeroed_until :: ‹nat ⇒ trail_pol ⇒ trail_pol› where ‹trail_set_zeroed_until = (λzeroed (M', xs, lvls, reasons, k, cs, _). (M', xs, lvls, reasons, k, cs, zeroed))› lemma trail_set_zeroed_until_rel: ‹(M,M') ∈ trail_pol 𝒜 ⟹zeroed_trail M' z ⟹ (trail_set_zeroed_until z M, M') ∈ (trail_pol 𝒜)› by (auto simp: trail_pol_def trail_set_zeroed_until_def) end

Theory IsaSAT_Trail