Theory CDCL_W_Covering_Models

theory CDCL_W_Covering_Models
  imports CDCL_W_Optimal_Model
begin

section ‹Covering Models›

text ‹I am only interested in the extension of CDCL to find covering mdoels, not in the required
subsequent extraction of the minimal covering models.›

type_synonym 'v cov = ‹'v literal multiset multiset›

lemma true_clss_cls_in_susbsuming:
  ‹C' ⊆# C ⟹ C' ∈ N ⟹ N ⊨p C›
  by (metis subset_mset.le_iff_add true_clss_cls_in true_clss_cls_mono_r)

locale covering_models =
  fixes
    ρ :: ‹'v ⇒ bool›
begin

definition model_is_dominated :: ‹'v literal multiset ⇒ 'v literal multiset ⇒ bool› where
‹model_is_dominated M M' ⟷
  filter_mset (λL. is_pos L ∧ ρ (atm_of L)) M ⊆# filter_mset (λL. is_pos L ∧ ρ (atm_of L)) M'›

lemma model_is_dominated_refl: ‹model_is_dominated I I›
  by (auto simp: model_is_dominated_def)

lemma model_is_dominated_trans:
  ‹model_is_dominated I J ⟹ model_is_dominated J K ⟹ model_is_dominated I K›
  by (auto simp: model_is_dominated_def)

definition is_dominating :: ‹'v literal multiset multiset ⇒ 'v literal multiset ⇒ bool› where
  ‹is_dominating ℳ I ⟷ (∃M∈#ℳ. ∃J. I ⊆# J ∧ model_is_dominated J M)›

lemma
  is_dominating_in:
    ‹I ∈# ℳ ⟹ is_dominating ℳ I› and
  is_dominating_mono:
    ‹is_dominating ℳ I ⟹ set_mset ℳ ⊆ set_mset ℳ' ⟹ is_dominating ℳ' I› and
  is_dominating_mono_model:
    ‹is_dominating ℳ I ⟹ I' ⊆# I ⟹ is_dominating ℳ I'›
  using multiset_filter_mono[of I' I ‹λL.  is_pos L ∧ ρ (atm_of L)›]
  by (auto 5 5 simp: is_dominating_def model_is_dominated_def
    dest!: multi_member_split)

lemma is_dominating_add_mset:
  ‹is_dominating (add_mset x ℳ) I ⟷
   is_dominating ℳ I ∨ (∃J. I ⊆# J ∧  model_is_dominated J x)›
  by (auto simp: is_dominating_def)

definition is_improving_int
  :: ‹('v, 'v clause) ann_lits ⇒ ('v, 'v clause) ann_lits ⇒ 'v clauses ⇒ 'v cov ⇒ bool›
where
‹is_improving_int M M' N ℳ ⟷
  M = M' ∧ (∀I ∈# ℳ. ¬model_is_dominated (lit_of `# mset M) I) ∧
  total_over_m (lits_of_l M) (set_mset N) ∧
  lit_of `# mset M ∈ simple_clss (atms_of_mm N) ∧
  lit_of `# mset M ∉# ℳ ∧
  M ⊨asm N ∧
  no_dup M›


text ‹This criteria is a bit more general than Weidenbach's version.›
abbreviation conflicting_clauses_ent where
  ‹conflicting_clauses_ent N ℳ ≡
     {#pNeg {#L ∈# x. ρ (atm_of L)#}.
        x ∈# filter_mset (λx. is_dominating ℳ x ∧ atms_of x = atms_of_mm N)
            (mset_set (simple_clss (atms_of_mm N)))#}+ N›

definition conflicting_clauses
  :: ‹'v clauses ⇒ 'v cov ⇒ 'v clauses›
where
  ‹conflicting_clauses N ℳ =
    {#C ∈# mset_set (simple_clss (atms_of_mm N)).
      conflicting_clauses_ent N ℳ ⊨pm C#}›

lemma conflicting_clauses_insert:
  assumes ‹M ∈ simple_clss (atms_of_mm N)› and ‹atms_of M = atms_of_mm N›
  shows ‹pNeg M ∈# conflicting_clauses N (add_mset M w)›
  using assms true_clss_cls_in_susbsuming[of ‹pNeg {#L ∈# M. ρ (atm_of L)#}›
    ‹pNeg M› ‹set_mset (conflicting_clauses_ent N (add_mset M w))›]
    is_dominating_in
  by (auto simp: conflicting_clauses_def simple_clss_finite
    pNeg_def image_mset_subseteq_mono)

lemma is_dominating_in_conflicting_clauses:
  assumes ‹is_dominating ℳ I› and
    atm: ‹atms_of_s (set_mset I) = atms_of_mm N› and
    ‹set_mset I ⊨m N› and
    ‹consistent_interp (set_mset I)› and
    ‹¬tautology I› and
    ‹distinct_mset I›
  shows
    ‹pNeg I ∈# conflicting_clauses N ℳ›
proof -
  have simpI: ‹I ∈ simple_clss (atms_of_mm N)›
    using assms by (auto simp: simple_clss_def atms_of_s_def atms_of_def)
  obtain I' J where ‹J ∈# ℳ› and ‹model_is_dominated I' J› and ‹I ⊆# I'›
    using assms(1) unfolding is_dominating_def
    by auto
  then have ‹I ∈ {x ∈ simple_clss (atms_of_mm N).
         (is_dominating A x ∨ (∃Ja. x ⊆# Ja ∧ model_is_dominated Ja J)) ∧
         atms_of x = atms_of_mm N}›
    using assms(1) atm
    by (auto simp: conflicting_clauses_def simple_clss_finite simpI atms_of_def
        pNeg_mono true_clss_cls_in_susbsuming is_dominating_add_mset atms_of_s_def
      dest!: multi_member_split)
  then show ?thesis
    using assms(1)
    by (auto simp: conflicting_clauses_def simple_clss_finite simpI
        pNeg_mono  is_dominating_add_mset
      dest!: multi_member_split
      intro!: true_clss_cls_in_susbsuming[of ‹(λx. pNeg {#L ∈# x. ρ (atm_of L)#}) I›])
qed

end

locale conflict_driven_clause_learningW_covering_models =
  conflict_driven_clause_learningW
    state_eq
    state
    ― ‹functions for the state:›
      ― ‹access functions:›
    trail init_clss learned_clss conflicting
      ― ‹changing state:›
    cons_trail tl_trail add_learned_cls remove_cls
    update_conflicting
      ― ‹get state:›
    init_state +
  covering_models ρ
  for
    state_eq :: ‹'st ⇒ 'st ⇒ bool› (infix ‹∼› 50) and
    state :: "'st ⇒ ('v, 'v clause) ann_lits × 'v clauses × 'v clauses × 'v clause option ×
      'v cov × 'b" and
    trail :: ‹'st ⇒ ('v, 'v clause) ann_lits› and
    init_clss :: ‹'st ⇒ 'v clauses› and
    learned_clss :: ‹'st ⇒ 'v clauses› and
    conflicting :: ‹'st ⇒ 'v clause option› and

    cons_trail :: ‹('v, 'v clause) ann_lit ⇒ 'st ⇒ 'st› and
    tl_trail :: ‹'st ⇒ 'st› and
    add_learned_cls :: ‹'v clause ⇒ 'st ⇒ 'st› and
    remove_cls :: ‹'v clause ⇒ 'st ⇒ 'st› and
    update_conflicting :: ‹'v clause option ⇒ 'st ⇒ 'st› and
    init_state :: ‹'v clauses ⇒ 'st› and
    ρ :: ‹'v ⇒ bool›  +
  fixes
    update_additional_info :: ‹'v cov × 'b ⇒ 'st ⇒ 'st›
  assumes
    update_additional_info:
      ‹state S = (M, N, U, C, ℳ) ⟹ state (update_additional_info K' S) = (M, N, U, C, K')› and
    weight_init_state:
      ‹⋀N :: 'v clauses. fst (additional_info (init_state N)) = {#}›
begin

definition update_weight_information :: ‹('v, 'v clause) ann_lits ⇒ 'st ⇒ 'st› where
  ‹update_weight_information M S =
    update_additional_info (add_mset (lit_of `# mset M) (fst (additional_info S)), snd (additional_info S)) S›

lemma
  trail_update_additional_info[simp]: ‹trail (update_additional_info w S) = trail S› and
  init_clss_update_additional_info[simp]:
    ‹init_clss (update_additional_info w S) = init_clss S› and
  learned_clss_update_additional_info[simp]:
    ‹learned_clss (update_additional_info w S) = learned_clss S› and
  backtrack_lvl_update_additional_info[simp]:
    ‹backtrack_lvl (update_additional_info w S) = backtrack_lvl S› and
  conflicting_update_additional_info[simp]:
    ‹conflicting (update_additional_info w S) = conflicting S› and
  clauses_update_additional_info[simp]:
    ‹clauses (update_additional_info w S) = clauses S›
  using update_additional_info[of S] unfolding clauses_def
  by (subst (asm) state_prop; subst (asm) state_prop; auto; fail)+

lemma
  trail_update_weight_information[simp]:
    ‹trail (update_weight_information w S) = trail S› and
  init_clss_update_weight_information[simp]:
    ‹init_clss (update_weight_information w S) = init_clss S› and
  learned_clss_update_weight_information[simp]:
    ‹learned_clss (update_weight_information w S) = learned_clss S› and
  backtrack_lvl_update_weight_information[simp]:
    ‹backtrack_lvl (update_weight_information w S) = backtrack_lvl S› and
  conflicting_update_weight_information[simp]:
    ‹conflicting (update_weight_information w S) = conflicting S› and
  clauses_update_weight_information[simp]:
    ‹clauses (update_weight_information w S) = clauses S›
  using update_additional_info[of S] unfolding update_weight_information_def by auto

definition covering :: ‹'st ⇒ 'v cov› where
  ‹covering S = fst (additional_info S)›

lemma
  additional_info_update_additional_info[simp]:
  ‹additional_info (update_additional_info w S) = w›
  unfolding additional_info_def using update_additional_info[of S]
  by (cases ‹state S›; auto; fail)+

lemma
  covering_cons_trail2[simp]: ‹covering (cons_trail L S) = covering S› and
  clss_tl_trail2[simp]: ‹covering (tl_trail S) = covering S› and
  covering_add_learned_cls_unfolded:
    ‹covering (add_learned_cls U S) = covering S›
    and
  covering_update_conflicting2[simp]: ‹covering (update_conflicting D S) = covering S› and
  covering_remove_cls2[simp]:
    ‹covering (remove_cls C S) = covering S› and
  covering_add_learned_cls2[simp]:
    ‹covering (add_learned_cls C S) = covering S› and
  covering_update_covering_information2[simp]:
    ‹covering (update_weight_information M S) = add_mset (lit_of `# mset M) (covering S)›
  by (auto simp: update_weight_information_def covering_def)



sublocale conflict_driven_clause_learningW 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
  by unfold_locales

sublocale conflict_driven_clause_learning_with_adding_init_clause_bnbW_no_state
  where
    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
    weight = covering and
    update_weight_information = update_weight_information and
    is_improving_int = is_improving_int and
    conflicting_clauses = conflicting_clauses
  by unfold_locales

lemma state_additional_info2':
  ‹state S = (trail S, init_clss S, learned_clss S, conflicting S, covering S, additional_info' S)›
  unfolding additional_info'_def by (cases ‹state S›; auto simp: state_prop covering_def)

lemma state_update_weight_information:
  ‹state S = (M, N, U, C, w, other) ⟹
    ∃w'. state (update_weight_information T S) = (M, N, U, C, w', other)›
  unfolding update_weight_information_def by (cases ‹state S›; auto simp: state_prop covering_def)


lemma conflicting_clss_incl_init_clss:
  ‹atms_of_mm (conflicting_clss S) ⊆ atms_of_mm (init_clss S)›
  unfolding conflicting_clss_def conflicting_clauses_def
  apply (auto simp: simple_clss_finite)
  by (auto simp: simple_clss_def atms_of_ms_def split: if_splits)

lemma conflict_clss_update_weight_no_alien:
  ‹atms_of_mm (conflicting_clss (update_weight_information M S))
    ⊆ atms_of_mm (init_clss S)›
  by (auto simp: conflicting_clss_def conflicting_clauses_def atms_of_ms_def
      cdclW_restart_mset_state simple_clss_finite
    dest: simple_clssE)


lemma distinct_mset_mset_conflicting_clss2: ‹distinct_mset_mset (conflicting_clss S)›
  unfolding conflicting_clss_def conflicting_clauses_def distinct_mset_set_def
  apply (auto simp: simple_clss_finite)
  by (auto simp: simple_clss_def)


lemma total_over_m_atms_incl:
  assumes ‹total_over_m M (set_mset N)›
  shows
    ‹x ∈ atms_of_mm N ⟹ x ∈ atms_of_s M›
  by (meson assms contra_subsetD total_over_m_alt_def)

lemma negate_ann_lits_simple_clss_iff[iff]:
  ‹negate_ann_lits M ∈ simple_clss N ⟷ lit_of `# mset M ∈ simple_clss N›
  unfolding negate_ann_lits_def
  by (subst uminus_simple_clss_iff[symmetric]) auto

lemma conflicting_clss_update_weight_information_in2:
  assumes ‹is_improving M M' S›
  shows ‹negate_ann_lits M' ∈# conflicting_clss (update_weight_information M' S)›
proof -
  have
    [simp]: ‹M' = M› and
    ‹∀I∈#covering S. ¬ model_is_dominated (lit_of `# mset M) I› and
    tot: ‹total_over_m (lits_of_l M) (set_mset (init_clss S))› and
    simpI: ‹lit_of `# mset M ∈ simple_clss (atms_of_mm (init_clss S))› and
    ‹lit_of `# mset M ∉# covering S› and
    ‹no_dup M› and
    ‹M ⊨asm init_clss S›
    using assms unfolding is_improving_int_def by auto
  have ‹pNeg {#L ∈# lit_of `# mset M. ρ (atm_of L)#}
     ∈ (λx. pNeg {#L ∈# x. ρ (atm_of L)#}) `
       {x ∈ simple_clss (atms_of_mm (init_clss S)).
        is_dominating (add_mset (lit_of `# mset M) (covering S)) x}›
    using is_dominating_in[of ‹lit_of `# mset M› ‹add_mset (lit_of `# mset M) (covering S)›]
    by (auto simp: simple_clss_finite multiset_filter_mono2 pNeg_mono
      conflicting_clauses_def conflicting_clss_def is_improving_int_def
      simpI)
  moreover have ‹atms_of (lit_of `# mset M) = atms_of_mm (init_clss S)›
    using tot simpI
    by (auto simp: simple_clss_finite multiset_filter_mono2 pNeg_mono
      conflicting_clauses_def conflicting_clss_def is_improving_int_def
      total_over_m_alt_def atms_of_s_def lits_of_def image_image atms_of_def
      simple_clss_def)
  ultimately have ‹(∃x. x ∈ simple_clss (atms_of_mm (init_clss S)) ∧
          is_dominating (add_mset (lit_of `# mset M) (covering S)) x ∧
          atms_of x = atms_of_mm (init_clss S) ∧
          pNeg {#L ∈# lit_of `# mset M. ρ (atm_of L)#} =
          pNeg {#L ∈# x. ρ (atm_of L)#})›
    by (auto intro: exI[of _ ‹lit_of `# mset M›] simp add: simpI is_dominating_in)
  then show ?thesis
    using is_dominating_in
     true_clss_cls_in_susbsuming[of ‹pNeg {#L ∈# lit_of `# mset M. ρ (atm_of L)#}›
    ‹pNeg (lit_of `# mset M)› ‹set_mset (conflicting_clauses_ent
      (init_clss S) (covering (update_weight_information M' S)))›]
    by (auto simp: simple_clss_finite multiset_filter_mono2 simpI
      conflicting_clauses_def conflicting_clss_def pNeg_mono
        negate_ann_lits_pNeg_lit_of image_iff image_mset_subseteq_mono)
qed

lemma is_improving_conflicting_clss_update_weight_information: ‹is_improving M M' S ⟹
       conflicting_clss S ⊆# conflicting_clss (update_weight_information M' S)›
  by (auto simp: is_improving_int_def conflicting_clss_def conflicting_clauses_def
      simp: multiset_filter_mono2 le_less true_clss_cls_tautology_iff simple_clss_finite
        is_dominating_add_mset filter_disj_eq image_Un
      intro!: image_mset_subseteq_mono
      intro: true_clss_cls_subsetI
      dest: simple_clssE
      split: enat.splits)

sublocale stateW_no_state
  where
    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
  by unfold_locales

sublocale stateW_no_state 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
  by unfold_locales

sublocale conflict_driven_clause_learningW 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
  by unfold_locales

sublocale conflict_driven_clause_learning_with_adding_init_clause_bnbW_ops
  where
    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
    weight = covering and
    update_weight_information = update_weight_information and
    is_improving_int = is_improving_int and
    conflicting_clauses = conflicting_clauses
  apply unfold_locales
  subgoal by (rule state_additional_info2')
  subgoal by (rule state_update_weight_information)
  subgoal by (rule conflicting_clss_incl_init_clss)
  subgoal by (rule distinct_mset_mset_conflicting_clss2)
  subgoal by (rule is_improving_conflicting_clss_update_weight_information)
  subgoal by (rule conflicting_clss_update_weight_information_in2)
  done

definition covering_simple_clss where
  ‹covering_simple_clss N S ⟷ (set_mset (covering S) ⊆ simple_clss (atms_of_mm N)) ∧
     distinct_mset (covering S) ∧
     (∀M ∈# covering S. total_over_m (set_mset M) (set_mset N))›

lemma [simp]: ‹covering (init_state N) = {#}›
  by (simp add: covering_def weight_init_state)

lemma ‹covering_simple_clss N (init_state N)›
  by (auto simp: covering_simple_clss_def)

lemma cdcl_bnb_covering_simple_clss:
  ‹cdcl_bnb S T ⟹ init_clss S = N ⟹ covering_simple_clss N S ⟹ covering_simple_clss N T›
  by (auto simp: cdcl_bnb.simps covering_simple_clss_def is_improving_int_def
      model_is_dominated_refl ocdclW_o.simps cdcl_bnb_bj.simps
      lits_of_def
    elim!: rulesE improveE conflict_optE obacktrackE
    dest!: multi_member_split[of _ ‹covering S›])

lemma rtranclp_cdcl_bnb_covering_simple_clss:
  ‹cdcl_bnb** S T ⟹ init_clss S = N ⟹ covering_simple_clss N S ⟹ covering_simple_clss N T›
  by (induction rule: rtranclp_induct)
    (auto simp: cdcl_bnb_covering_simple_clss simp: rtranclp_cdcl_bnb_no_more_init_clss
      cdcl_bnb_no_more_init_clss)


lemma wf_cdcl_bnb_fixed:
   ‹wf {(T, S). cdclW_restart_mset.cdclW_all_struct_inv (abs_state S) ∧ cdcl_bnb S T
       ∧ covering_simple_clss N S ∧ init_clss S = N}›
  apply (rule wf_cdcl_bnb_with_additional_inv[of
     ‹covering_simple_clss N›
     N id ‹{(T, S). (T, S) ∈ {(ℳ', ℳ). ℳ ⊂# ℳ' ∧ distinct_mset ℳ'
       ∧ set_mset ℳ' ⊆ simple_clss (atms_of_mm N)}}›])
  subgoal
    by (auto simp: improvep.simps is_improving_int_def covering_simple_clss_def
         add_mset_eq_add_mset  model_is_dominated_refl
      dest!: multi_member_split)
  subgoal
    apply (rule wf_bounded_set[of _ ‹λ_. simple_clss (atms_of_mm N)› set_mset])
    apply (auto simp: distinct_mset_subset_iff_remdups[symmetric] simple_clss_finite
      simp flip: remdups_mset_def)
    by (metis distinct_mset_mono distinct_mset_set_mset_ident)
  subgoal
    by (rule cdcl_bnb_covering_simple_clss)
  done

lemma can_always_improve:
  assumes
    ent: ‹trail S ⊨asm clauses S› and
    total: ‹total_over_m (lits_of_l (trail S)) (set_mset (clauses S))› and
    n_s: ‹no_step conflict_opt S› and
    confl: ‹conflicting S = None› and
    all_struct: ‹cdclW_restart_mset.cdclW_all_struct_inv (abs_state S)›
  shows ‹Ex (improvep S)›
proof -
  have ‹cdclW_restart_mset.cdclW_M_level_inv (abs_state S)› and
    alien: ‹cdclW_restart_mset.no_strange_atm (abs_state S)›
    using all_struct
    unfolding cdclW_restart_mset.cdclW_all_struct_inv_def
    by fast+
  then have n_d: ‹no_dup (trail S)›
    unfolding cdclW_restart_mset.cdclW_M_level_inv_def
    by auto
  have [simp]:
    ‹atms_of_mm (CDCL_W_Abstract_State.init_clss (abs_state S)) = atms_of_mm (init_clss S)›
    unfolding abs_state_def init_clss.simps
    by auto
  let ?M = ‹(lit_of `# mset (trail S))›
  have trail_simple: ‹?M ∈ simple_clss (atms_of_mm (init_clss S))›
    using n_d alien
    by (auto simp: simple_clss_def cdclW_restart_mset.no_strange_atm_def
        lits_of_def image_image atms_of_def
      dest: distinct_consistent_interp no_dup_not_tautology
        no_dup_distinct)
  then have [simp]: ‹atms_of ?M = atms_of_mm (init_clss S)›
    using total
    by (auto simp: total_over_m_alt_def simple_clss_def atms_of_def image_image
      lits_of_def atms_of_s_def clauses_def)
  then have K: ‹is_dominating (covering S) ?M ⟹ pNeg {#L ∈# lit_of `# mset (trail S). ρ (atm_of L)#}
         ∈ (λx. pNeg {#L ∈# x. ρ (atm_of L)#}) `
           {x ∈ simple_clss (atms_of_mm (init_clss S)).
            is_dominating (covering S) x ∧
            atms_of x = atms_of_mm (init_clss S)}›
    by (auto simp: image_iff trail_simple
      intro!: exI[of _ ‹lit_of `# mset (trail S)›])
  have H: ‹I ∈# covering S ⟹
        model_is_dominated ?M I ⟹
	pNeg {#L ∈# ?M. ρ (atm_of L)#}
     ∈ (λx. pNeg {#L ∈# x. ρ (atm_of L)#}) `
       {x ∈ simple_clss (atms_of_mm (init_clss S)).
        is_dominating (covering S) x}› for I
    using is_dominating_in[of ‹lit_of `# mset M› ‹add_mset (lit_of `# mset M) (covering S)›]
      trail_simple
    by (auto 5 5 simp: simple_clss_finite multiset_filter_mono2 pNeg_mono
          conflicting_clauses_def conflicting_clss_def is_improving_int_def
          is_dominating_add_mset filter_disj_eq image_Un
        dest!: multi_member_split)
  have ‹I ∈# covering S ⟹
        model_is_dominated ?M I ⟹ False› for I
    using n_s confl H[of I] K
     true_clss_cls_in_susbsuming[of ‹pNeg {#L ∈# ?M. ρ (atm_of L)#}›
    ‹pNeg ?M› ‹set_mset (conflicting_clauses_ent
      (init_clss S) (covering S))›]
    by (auto simp: conflict_opt.simps simple_clss_finite
        conflicting_clss_def conflicting_clauses_def is_dominating_def
	is_dominating_add_mset filter_disj_eq image_Un pNeg_mono
	multiset_filter_mono2 negate_ann_lits_pNeg_lit_of
      intro: trail_simple)
  moreover have False if ‹lit_of `# mset (trail S) ∈# covering S›
    using n_s confl that trail_simple by (auto simp: conflict_opt.simps
      conflicting_clauses_insert conflicting_clss_def simple_clss_finite
      negate_ann_lits_pNeg_lit_of
      dest!: multi_member_split)
  ultimately have imp: ‹is_improving (trail S) (trail S) S›
    unfolding is_improving_int_def
    using assms trail_simple n_d by (auto simp: clauses_def)
  show ?thesis
    by (rule exI) (rule improvep.intros[OF imp confl state_eq_ref])
qed

lemma exists_model_with_true_lit_entails_conflicting:
  assumes
    L_I: ‹Pos L ∈ I› and
    L: ‹ρ L› and
    L_in: ‹L ∈ atms_of_mm (init_clss S)› and
    ent: ‹I ⊨m init_clss S› and
    cons: ‹consistent_interp I› and
    total: ‹total_over_m I (set_mset N)› and
    no_L: ‹¬(∃J∈# covering S. Pos L ∈# J)› and
    cov: ‹covering_simple_clss N S› and
    NS: ‹atms_of_mm N = atms_of_mm (init_clss S)›
  shows ‹I ⊨m conflicting_clss S› and
    ‹I ⊨m CDCL_W_Abstract_State.init_clss (abs_state S)›
proof -
  show ‹I ⊨m conflicting_clss S›
    unfolding conflicting_clss_def conflicting_clauses_def
      set_mset_filter true_cls_mset_def
  proof
    fix C
    assume ‹C ∈ {a. a ∈# mset_set (simple_clss (atms_of_mm (init_clss S))) ∧
                {#pNeg {#L ∈# x. ρ (atm_of L)#}.
                x ∈# {#x ∈# mset_set (simple_clss (atms_of_mm (init_clss S))).
                        is_dominating (covering S) x ∧
                        atms_of x = atms_of_mm (init_clss S)#}#} +
                init_clss S ⊨pm
                a}›
    then have simp_C: ‹C ∈ simple_clss (atms_of_mm (init_clss S))› and
      ent_C: ‹(λx. pNeg {#L ∈# x. ρ (atm_of L)#}) `
           {x ∈ simple_clss (atms_of_mm (init_clss S)). is_dominating (covering S) x ∧
	     atms_of x = atms_of_mm (init_clss S)} ∪
          set_mset (init_clss S) ⊨p C›
      by (auto simp: simple_clss_finite)
    have tot_I2: ‹total_over_m I
         ((λx. pNeg {#L ∈# x. ρ (atm_of L)#}) `
          {x ∈ simple_clss (atms_of_mm (init_clss S)).
           is_dominating (covering S) x ∧
           atms_of x = atms_of_mm (init_clss S)} ∪
          set_mset (init_clss S) ∪
          {C}) ⟷ total_over_m I (set_mset N)› for I
      using simp_C  NS[symmetric]
      by (auto simp: total_over_m_def total_over_set_def
          simple_clss_def atms_of_ms_def atms_of_def pNeg_def
	dest!: multi_member_split)
    have ‹I ⊨s (λx. pNeg {#L ∈# x. ρ (atm_of L)#}) `
           {x ∈ simple_clss (atms_of_mm (init_clss S)). is_dominating (covering S) x ∧
	     atms_of x = atms_of_mm (init_clss S)}›
      unfolding NS[symmetric]
        total_over_m_alt_def true_clss_def
    proof
      fix D
      assume ‹D ∈ (λx. pNeg {#L ∈# x. ρ (atm_of L)#}) `
            {x ∈ simple_clss (atms_of_mm N). is_dominating (covering S) x ∧
	     atms_of x = atms_of_mm N}›
      then obtain x where
        D: ‹D = pNeg {#L ∈# x. ρ (atm_of L)#}› and
        x: ‹x ∈ simple_clss (atms_of_mm N)› and
        dom: ‹is_dominating (covering S) x› and
	tot_x: ‹atms_of x = atms_of_mm N›
        by auto
      then have ‹L ∈ atms_of x›
        using cov L_in no_L
	unfolding NS[symmetric]
        by (auto simp: true_clss_def is_dominating_def model_is_dominated_def
	    covering_simple_clss_def atms_of_def pNeg_def image_image
	    total_over_m_alt_def atms_of_s_def
          dest!: multi_member_split)
      then have ‹Neg L ∈# x›
        using no_L dom L unfolding atm_iff_pos_or_neg_lit
	by (auto simp: is_dominating_def model_is_dominated_def insert_subset_eq_iff
	  dest!: multi_member_split)
      then have ‹Pos L ∈# D›
        using L
        by (auto simp: pNeg_def image_image D image_iff
          dest!: multi_member_split)
      then show ‹I ⊨ D›
        using L_I by (auto dest: multi_member_split)
    qed
    then show ‹I ⊨ C›
      using total cons ent_C ent
      unfolding true_clss_cls_def tot_I2
      by auto
  qed
  then show I_S: ‹I ⊨m CDCL_W_Abstract_State.init_clss (abs_state S)›
    using ent
    by (auto simp: abs_state_def init_clss.simps)
qed

lemma exists_model_with_true_lit_still_model:
  assumes
    L_I: ‹Pos L ∈ I› and
    L: ‹ρ L› and
    L_in: ‹L ∈ atms_of_mm (init_clss S)› and
    ent: ‹I ⊨m init_clss S› and
    cons: ‹consistent_interp I› and
    total: ‹total_over_m I (set_mset N)› and
    cdcl: ‹cdcl_bnb S T› and
    no_L_T: ‹¬(∃J∈# covering T. Pos L ∈# J)› and
    cov: ‹covering_simple_clss N S› and
    NS: ‹atms_of_mm N = atms_of_mm (init_clss S)›
  shows ‹I ⊨m CDCL_W_Abstract_State.init_clss (abs_state T)›
proof -
  have no_L: ‹¬(∃J∈# covering S. Pos L ∈# J)›
    using cdcl no_L_T
    by (cases) (auto elim!: rulesE improveE conflict_optE obacktrackE
      simp: ocdclW_o.simps cdcl_bnb_bj.simps)
  have I_S: ‹I ⊨m CDCL_W_Abstract_State.init_clss (abs_state S)›
    by (rule exists_model_with_true_lit_entails_conflicting[OF assms(1-6) no_L assms(9) NS])
  have I_T': ‹I ⊨m conflicting_clss (update_weight_information M' S)›
    if T: ‹T ∼ update_weight_information M' S› for M'
    unfolding conflicting_clss_def conflicting_clauses_def
      set_mset_filter true_cls_mset_def
  proof
    let ?T = ‹update_weight_information M' S›
    fix C
    assume ‹C ∈ {a. a ∈# mset_set (simple_clss (atms_of_mm (init_clss ?T))) ∧
                {#pNeg {#L ∈# x. ρ (atm_of L)#}.
                x ∈# {#x ∈# mset_set (simple_clss (atms_of_mm (init_clss ?T))).
                        is_dominating (covering ?T) x ∧
                        atms_of x = atms_of_mm (init_clss ?T)#}#} +
                init_clss ?T ⊨pm
                a}›
    then have simp_C: ‹C ∈ simple_clss (atms_of_mm (init_clss ?T))› and
      ent_C: ‹(λx. pNeg {#L ∈# x. ρ (atm_of L)#}) `
           {x ∈ simple_clss (atms_of_mm (init_clss ?T)). is_dominating (covering ?T) x ∧
	     atms_of x = atms_of_mm (init_clss ?T)} ∪
          set_mset (init_clss ?T) ⊨p C›
      by (auto simp: simple_clss_finite)
    have tot_I2: ‹total_over_m I
         ((λx. pNeg {#L ∈# x. ρ (atm_of L)#}) `
          {x ∈ simple_clss (atms_of_mm (init_clss ?T)).
           is_dominating (covering ?T) x ∧
           atms_of x = atms_of_mm (init_clss ?T)} ∪
          set_mset (init_clss ?T) ∪
          {C}) ⟷ total_over_m I (set_mset N)› for I
      using simp_C  NS[symmetric]
      by (auto simp: total_over_m_def total_over_set_def
          simple_clss_def atms_of_ms_def atms_of_def pNeg_def
	dest!: multi_member_split)
    have H: ‹atms_of_mm (init_clss (update_weight_information M' S)) = atms_of_mm N›
      by (auto simp: NS)
    have ‹I ⊨s (λx. pNeg {#L ∈# x. ρ (atm_of L)#}) `
           {x ∈ simple_clss (atms_of_mm (init_clss ?T)). is_dominating (covering ?T) x ∧
	     atms_of x = atms_of_mm (init_clss ?T)}›
      unfolding NS[symmetric] H
        total_over_m_alt_def true_clss_def
    proof
      fix D
      assume ‹D ∈ (λx. pNeg {#L ∈# x. ρ (atm_of L)#}) `
            {x ∈ simple_clss (atms_of_mm N). is_dominating (covering ?T) x ∧
	     atms_of x = atms_of_mm N}›
      then obtain x where
        D: ‹D = pNeg {#L ∈# x. ρ (atm_of L)#}› and
        x: ‹x ∈ simple_clss (atms_of_mm N)› and
        dom: ‹is_dominating (covering ?T) x› and
	tot_x: ‹atms_of x = atms_of_mm N›
        by auto
      then have ‹L ∈ atms_of x›
        using cov L_in no_L
	unfolding NS[symmetric]
        by (auto simp: true_clss_def is_dominating_def model_is_dominated_def
	    covering_simple_clss_def atms_of_def pNeg_def image_image
	    total_over_m_alt_def atms_of_s_def
          dest!: multi_member_split)
      then have ‹Neg L ∈# x›
        using no_L_T dom L T unfolding atm_iff_pos_or_neg_lit
	by (auto simp: is_dominating_def model_is_dominated_def insert_subset_eq_iff
	  dest!: multi_member_split)
      then have ‹Pos L ∈# D›
        using L
        by (auto simp: pNeg_def image_image D image_iff
          dest!: multi_member_split)
      then show ‹I ⊨ D›
        using L_I by (auto dest: multi_member_split)
    qed
    then show ‹I ⊨ C›
      using total cons ent_C ent
      unfolding true_clss_cls_def tot_I2
      by auto
  qed
  show ?thesis
    using cdcl
  proof (cases)
    case cdcl_conflict
    then show ?thesis using I_S by (auto elim!: conflictE)
  next
    case cdcl_propagate
    then show ?thesis using I_S by (auto elim!: rulesE)
  next
    case cdcl_improve
    show ?thesis
      using I_S cdcl_improve I_T'
      by (auto simp: abs_state_def init_clss.simps
        elim!: improveE)
  next
    case cdcl_conflict_opt
    then show ?thesis using I_S by (auto elim!: conflict_optE)
  next
    case cdcl_other'
    then show ?thesis using I_S by (auto elim!: rulesE obacktrackE simp: ocdclW_o.simps cdcl_bnb_bj.simps)
  qed
qed

lemma rtranclp_exists_model_with_true_lit_still_model:
  assumes
    L_I: ‹Pos L ∈ I› and
    L: ‹ρ L› and
    L_in: ‹L ∈ atms_of_mm (init_clss S)› and
    ent: ‹I ⊨m init_clss S› and
    cons: ‹consistent_interp I› and
    total: ‹total_over_m I (set_mset N)› and
    cdcl: ‹cdcl_bnb** S T› and
    cov: ‹covering_simple_clss N S› and
    ‹N = init_clss S›
  shows ‹I ⊨m CDCL_W_Abstract_State.init_clss (abs_state T) ∨ (∃J∈# covering T. Pos L ∈# J)›
  using cdcl assms
  apply (induction rule: rtranclp_induct)
  subgoal using exists_model_with_true_lit_entails_conflicting[of L I S N]
    by auto
  subgoal for T U
    apply (rule disjCI)
    apply (rule exists_model_with_true_lit_still_model[OF L_I L _ _ cons total, of T U])
    by (auto dest: rtranclp_cdcl_bnb_no_more_init_clss
      intro: rtranclp_cdcl_bnb_covering_simple_clss cdcl_bnb_covering_simple_clss)
  done

lemma is_dominating_nil[simp]: ‹¬is_dominating {#} x›
  by (auto simp: is_dominating_def)

lemma atms_of_conflicting_clss_init_state:
  ‹atms_of_mm (conflicting_clss (init_state N)) ⊆ atms_of_mm N›
  by (auto simp: conflicting_clss_def conflicting_clauses_def
    atms_of_ms_def simple_clss_finite
    dest!: simple_clssE)

lemma no_step_cdcl_bnb_stgy_empty_conflict2:
  assumes
    n_s: ‹no_step cdcl_bnb S› and
    all_struct: ‹cdclW_restart_mset.cdclW_all_struct_inv (abs_state S)› and
    stgy_inv: ‹cdcl_bnb_stgy_inv S›
  shows ‹conflicting S = Some {#}›
  by (rule no_step_cdcl_bnb_stgy_empty_conflict[OF can_always_improve assms])


theorem cdclcm_correctness:
  assumes
    full: ‹full cdcl_bnb_stgy (init_state N) T› and
    dist: ‹distinct_mset_mset N›
  shows
    ‹Pos L ∈ I ⟹ ρ L ⟹ L ∈ atms_of_mm N ⟹ total_over_m I (set_mset N) ⟹ consistent_interp I ⟹ I ⊨m N ⟹
      ∃J ∈# covering T. Pos L ∈# J›
proof -
  let ?S = ‹init_state N›
  have ns: ‹no_step cdcl_bnb_stgy T› and
    st: ‹cdcl_bnb_stgy** ?S T› and
    st': ‹cdcl_bnb** ?S T›
    using full unfolding full_def by (auto intro: rtranclp_cdcl_bnb_stgy_cdcl_bnb)
  have ns': ‹no_step cdcl_bnb T›
    by (meson cdcl_bnb.cases cdcl_bnb_stgy.simps no_confl_prop_impr.elims(3) ns)

  have ‹distinct_mset C› if ‹C ∈# N› for C
    using dist that by (auto simp: distinct_mset_set_def dest: multi_member_split)
  then have dist: ‹distinct_mset_mset (N)›
    by (auto simp: distinct_mset_set_def)
  then have [simp]: ‹cdclW_restart_mset.cdclW_all_struct_inv ([], N, {#}, None)›
    unfolding init_state.simps[symmetric]
    by (auto simp: cdclW_restart_mset.cdclW_all_struct_inv_def)
  have [iff]: ‹cdcl_bnb_struct_invs ?S›
    using atms_of_conflicting_clss_init_state[of N]
    by (auto simp: cdcl_bnb_struct_invs_def)
  have stgy_inv: ‹cdcl_bnb_stgy_inv ?S›
    by (auto simp: cdcl_bnb_stgy_inv_def conflict_is_false_with_level_def)
  have ent: ‹cdclW_restart_mset.cdclW_learned_clauses_entailed_by_init (abs_state ?S)›
    by (auto simp: cdclW_restart_mset.cdclW_learned_clauses_entailed_by_init_def)
  have all_struct: ‹cdclW_restart_mset.cdclW_all_struct_inv (abs_state (init_state N))›
    unfolding CDCL_W_Abstract_State.init_state.simps abs_state_def
    by (auto simp: cdclW_restart_mset.cdclW_all_struct_inv_def dist
      cdclW_restart_mset.no_strange_atm_def cdclW_restart_mset_state
      cdclW_restart_mset.cdclW_M_level_inv_def
      cdclW_restart_mset.distinct_cdclW_state_def
      cdclW_restart_mset.cdclW_conflicting_def distinct_mset_mset_conflicting_clss
      cdclW_restart_mset.cdclW_learned_clause_alt_def)
  have cdcl: ‹cdcl_bnb** ?S T›
    using st rtranclp_cdcl_bnb_stgy_cdcl_bnb unfolding full_def by blast
  have cov: ‹covering_simple_clss N ?S›
    by (auto simp: covering_simple_clss_def)

  have struct_T: ‹cdclW_restart_mset.cdclW_all_struct_inv (abs_state T)›
    using rtranclp_cdcl_bnb_stgy_all_struct_inv[OF st' all_struct] .
  have stgy_T: ‹cdcl_bnb_stgy_inv T›
    using rtranclp_cdcl_bnb_stgy_stgy_inv[OF st all_struct stgy_inv] .
  have confl: ‹conflicting T = Some {#}›
    using no_step_cdcl_bnb_stgy_empty_conflict2[OF ns' struct_T stgy_T] .
  have tot_I: ‹total_over_m I (set_mset (clauses T + conflicting_clss T)) ⟷
    total_over_m I (set_mset (init_clss T + conflicting_clss T))› for I
    using struct_T atms_of_conflicting_clss[of T]
    unfolding cdclW_restart_mset.cdclW_all_struct_inv_def
      cdclW_restart_mset.cdclW_learned_clause_alt_def satisfiable_def
      cdclW_restart_mset.no_strange_atm_def
    by (auto simp: clauses_def satisfiable_def total_over_m_alt_def
      abs_state_def cdclW_restart_mset_state
      cdclW_restart_mset.clauses_def)
  have ‹unsatisfiable (set_mset (clauses T + conflicting_clss T))›
    using full_cdcl_bnb_stgy_unsat[OF _ full all_struct _ stgy_inv]
    by (auto simp: can_always_improve)
  have ‹cdclW_restart_mset.cdclW_learned_clauses_entailed_by_init
     (abs_state T)›
    using rtranclp_cdcl_bnb_cdclW_learned_clauses_entailed_by_init[OF st' ent all_struct] .
  then have ‹init_clss T + conflicting_clss T ⊨pm {#}›
    using struct_T confl
    unfolding cdclW_restart_mset.cdclW_all_struct_inv_def
      cdclW_restart_mset.cdclW_learned_clause_alt_def
      cdclW_restart_mset.no_strange_atm_def tot_I
      cdclW_restart_mset.cdclW_learned_clauses_entailed_by_init_def
    by (auto simp: clauses_def abs_state_def cdclW_restart_mset_state
      cdclW_restart_mset.clauses_def
      satisfiable_def dest: true_clss_clss_left_right)
  then have unsat: ‹unsatisfiable (set_mset (init_clss T + conflicting_clss T))›
    by (auto simp: clauses_def true_clss_cls_def
      satisfiable_def)

  assume
    L_I: ‹Pos L ∈ I› and
    L: ‹ρ L› and
    L_N: ‹L ∈ atms_of_mm N› and
    tot_I: ‹total_over_m I (set_mset N)› and
    cons: ‹consistent_interp I› and
    I_N: ‹I ⊨m N›
  show ‹Multiset.Bex (covering T) ((∈#) (Pos L))›
    using rtranclp_exists_model_with_true_lit_still_model[OF L_I L _ _ _ _ cdcl, of N] L_N
      I_N tot_I cons cov unsat
    by (auto simp: abs_state_def cdclW_restart_mset_state)
qed

end


text ‹Now we instantiate the previous with term‹λ_. True›: This means that we aim at making
all variables that appears at least ones true.›

global_interpretation cover_all_vars: covering_models ‹λ_. True›
  .

context conflict_driven_clause_learningW_covering_models
begin

interpretation cover_all_vars: conflict_driven_clause_learningW_covering_models where
    ρ = ‹λ_::'v. True› 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
  by standard

lemma
  ‹cover_all_vars.model_is_dominated M M' ⟷
    filter_mset (λL. is_pos L) M ⊆# filter_mset (λL. is_pos L) M'›
  unfolding cover_all_vars.model_is_dominated_def
  by auto

lemma
  ‹cover_all_vars.conflicting_clauses N ℳ =
    {# C ∈# (mset_set (simple_clss (atms_of_mm N))).
        (pNeg `
        {a. a ∈# mset_set (simple_clss (atms_of_mm N)) ∧
            (∃M∈#ℳ. ∃J. a ⊆# J ∧ cover_all_vars.model_is_dominated J M) ∧
            atms_of a = atms_of_mm N} ∪
        set_mset N) ⊨p C#}›
  unfolding cover_all_vars.conflicting_clauses_def
    cover_all_vars.is_dominating_def
  by auto

theorem cdclcm_correctness_all_vars: (* \htmllink{cdclcm-correctness}*)
  assumes
    full: ‹full cover_all_vars.cdcl_bnb_stgy (init_state N) T› and
    dist: ‹distinct_mset_mset N›
  shows
    ‹Pos L ∈ I ⟹ L ∈ atms_of_mm N ⟹ total_over_m I (set_mset N) ⟹ consistent_interp I ⟹ I ⊨m N ⟹
      ∃J ∈# covering T. Pos L ∈# J›
  using cover_all_vars.cdclcm_correctness[OF assms]
  by blast

end

end