Theory OCDCL

theory OCDCL
  imports CDCL_W_Optimal_Model
begin

subsubsection ‹Alternative versions›

text ‹We instantiate our more general rules with exactly the rule from Christoph's OCDCL with either
versions of improve.›


subsubsection ‹Weights›

text ‹This one is the version of the weight functions used by Christoph Weidenbach.
  However, we have decided to not instantiate tho calculus with this weight function,
  because it only a slight restriction.
›
locale ocdcl_weight_WB =
  fixes
    ν :: ‹'v literal ⇒ nat›
begin

definition ρ :: ‹'v clause ⇒ nat› where
  ‹ρ M = (∑A ∈# M. ν A)›

sublocale ocdcl_weight ρ
  by (unfold_locales)
    (auto simp: ρ_def sum_image_mset_mono)

end


subsubsection ‹Calculus with simple Improve rule›

context conflict_driven_clause_learning⇩W_optimal_weight
begin
text ‹To make sure that the paper version of the correct, we restrict the previous calculus to exactly
  the rules that are on paper.›
inductive pruning :: ‹'st ⇒ 'st ⇒ bool› where
pruning_rule:
  ‹pruning S T›
  if
    ‹⋀M'. total_over_m (set_mset (mset (map lit_of (trail S) @ M'))) (set_mset (init_clss S)) ⟹
       distinct_mset (atm_of `# mset (map lit_of (trail S) @ M')) ⟹
       consistent_interp (set_mset (mset (map lit_of (trail S) @ M'))) ⟹
       ρ' (weight S) ≤ Found (ρ (mset (map lit_of (trail S) @ M')))›
    ‹conflicting S = None›
    ‹T ∼ update_conflicting (Some (negate_ann_lits (trail S))) S›

inductive oconflict_opt :: ‹'st ⇒ 'st ⇒ bool› for S T :: 'st where
oconflict_opt_rule:
  ‹oconflict_opt S T›
  if
    ‹Found (ρ (lit_of `# mset (trail S))) ≥ ρ' (weight S)›
    ‹conflicting S = None›
    ‹T ∼ update_conflicting (Some (negate_ann_lits (trail S))) S›

inductive improve :: ‹'st ⇒ 'st ⇒ bool› for S T :: 'st where
improve_rule:
  ‹improve S T›
  if
    ‹total_over_m (lits_of_l (trail S)) (set_mset (init_clss S))›
    ‹Found (ρ (lit_of `# mset (trail S))) < ρ' (weight S)›
    ‹trail S ⊨asm init_clss S›
    ‹conflicting S = None›
    ‹T ∼ update_weight_information (trail S) S›

text ‹This is the basic version of the calculus:›
inductive ocdcl⇩w :: ‹'st ⇒ 'st ⇒ bool› for S :: 'st where (* \htmllink{ocdcl-def} *)
ocdcl_conflict: ‹conflict S S' ⟹ ocdcl⇩w S S'› |
ocdcl_propagate: ‹propagate S S' ⟹ ocdcl⇩w S S'› |
ocdcl_improve: ‹improve S S' ⟹ ocdcl⇩w S S'› |
ocdcl_conflict_opt: ‹oconflict_opt S S' ⟹ ocdcl⇩w S S'› |
ocdcl_other': ‹ocdcl⇩W_o S S' ⟹ ocdcl⇩w S S'› |
ocdcl_pruning: ‹pruning S S' ⟹ ocdcl⇩w S S'›

inductive ocdcl⇩w_stgy :: ‹'st ⇒ 'st ⇒ bool› for S :: 'st where (* \htmllink{ocdcl-strategy-def} *)
ocdcl⇩w_conflict: ‹conflict S S' ⟹ ocdcl⇩w_stgy S S'› |
ocdcl⇩w_propagate: ‹propagate S S' ⟹ ocdcl⇩w_stgy S S'› |
ocdcl⇩w_improve: ‹improve S S' ⟹ ocdcl⇩w_stgy S S'› |
ocdcl⇩w_conflict_opt: ‹conflict_opt S S' ⟹ ocdcl⇩w_stgy S S'› |
ocdcl⇩w_other': ‹ocdcl⇩W_o S S' ⟹ no_confl_prop_impr S ⟹ ocdcl⇩w_stgy S S'›

lemma pruning_conflict_opt:
  assumes ocdcl_pruning: ‹pruning S T› and
    inv: ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (abs_state S)›
  shows ‹conflict_opt S T›
proof -
  have le:
    ‹⋀M'. total_over_m (set_mset (mset (map lit_of (trail S) @ M')))
          (set_mset (init_clss S)) ⟹
         distinct_mset (atm_of `# mset (map lit_of (trail S) @ M')) ⟹
         consistent_interp (set_mset (mset (map lit_of (trail S) @ M'))) ⟹
         ρ' (weight S) ≤ Found (ρ (mset (map lit_of (trail S) @ M')))›
    using ocdcl_pruning by (auto simp: pruning.simps)
  have alien: ‹cdcl⇩W_restart_mset.no_strange_atm (abs_state S)› and
    lev: ‹cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv (abs_state S)›
    using inv unfolding cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def
    by fast+
  have incl: ‹atms_of (mset (map lit_of (trail S))) ⊆ atms_of_mm (init_clss S)›
    using alien unfolding cdcl⇩W_restart_mset.no_strange_atm_def
    by (auto simp: abs_state_def cdcl⇩W_restart_mset_state lits_of_def image_image atms_of_def)
  have dist: ‹distinct (map lit_of (trail S))› and
    cons: ‹consistent_interp (set (map lit_of (trail S)))›
    using lev unfolding cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv_def
    by (auto simp: abs_state_def cdcl⇩W_restart_mset_state lits_of_def image_image atms_of_def
      dest: no_dup_map_lit_of)
  have ‹negate_ann_lits (trail S) ∈# conflicting_clss S›
    unfolding negate_ann_lits_pNeg_lit_of comp_def mset_map[symmetric]
    by (rule pruned_clause_in_conflicting_clss[OF le incl dist cons]) fast+
  then show ‹conflict_opt S T›
    by (rule conflict_opt.intros) (use ocdcl_pruning in ‹auto simp: pruning.simps›)
qed

lemma ocdcl_conflict_opt_conflict_opt:
  assumes ocdcl_pruning: ‹oconflict_opt S T› and
    inv: ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (abs_state S)›
  shows ‹conflict_opt S T›
proof -
  have alien: ‹cdcl⇩W_restart_mset.no_strange_atm (abs_state S)› and
    lev: ‹cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv (abs_state S)›
    using inv unfolding cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def
    by fast+
  have incl: ‹atms_of (lit_of `# mset (trail S)) ⊆ atms_of_mm (init_clss S)›
    using alien unfolding cdcl⇩W_restart_mset.no_strange_atm_def
    by (auto simp: abs_state_def cdcl⇩W_restart_mset_state lits_of_def image_image atms_of_def)
  have dist: ‹distinct_mset (lit_of `# mset (trail S))› and
    cons: ‹consistent_interp (set (map lit_of (trail S)))› and
    tauto: ‹¬tautology (lit_of `# mset (trail S))›
    using lev unfolding cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv_def
    by (auto simp: abs_state_def cdcl⇩W_restart_mset_state lits_of_def image_image atms_of_def
      dest: no_dup_map_lit_of no_dup_distinct no_dup_not_tautology)
  have ‹lit_of `# mset (trail S) ∈ simple_clss (atms_of_mm (init_clss S))›
    using dist incl tauto by (auto simp: simple_clss_def)
  then have simple: ‹(lit_of `# mset (trail S))
    ∈ {a. a ∈# mset_set (simple_clss (atms_of_mm (init_clss S))) ∧
          ρ' (weight S) ≤ Found (ρ a)}›
    using ocdcl_pruning by (auto simp: simple_clss_finite oconflict_opt.simps)
  have ‹negate_ann_lits (trail S) ∈# conflicting_clss S›
    unfolding negate_ann_lits_pNeg_lit_of comp_def conflicting_clss_def
    by (rule too_heavy_clauses_conflicting_clauses)
      (use simple in ‹auto simp: too_heavy_clauses_def oconflict_opt.simps›)
  then show ‹conflict_opt S T›
    apply (rule conflict_opt.intros)
    subgoal using ocdcl_pruning by (auto simp: oconflict_opt.simps)
    subgoal using ocdcl_pruning by (auto simp: oconflict_opt.simps)
    done
qed


lemma improve_improvep:
  assumes imp: ‹improve S T› and
    inv: ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (abs_state S)›
  shows ‹improvep S T›
proof -
  have alien: ‹cdcl⇩W_restart_mset.no_strange_atm (abs_state S)› and
    lev: ‹cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv (abs_state S)›
    using inv unfolding cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def
    by fast+
  have incl: ‹atms_of (lit_of `# mset (trail S)) ⊆ atms_of_mm (init_clss S)›
    using alien unfolding cdcl⇩W_restart_mset.no_strange_atm_def
    by (auto simp: abs_state_def cdcl⇩W_restart_mset_state lits_of_def image_image atms_of_def)
  have dist: ‹distinct_mset (lit_of `# mset (trail S))› and
    cons: ‹consistent_interp (set (map lit_of (trail S)))› and
    tauto: ‹¬tautology (lit_of `# mset (trail S))› and
    nd: ‹no_dup (trail S)›
    using lev unfolding cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv_def
    by (auto simp: abs_state_def cdcl⇩W_restart_mset_state lits_of_def image_image atms_of_def
      dest: no_dup_map_lit_of no_dup_distinct no_dup_not_tautology)
  have ‹lit_of `# mset (trail S) ∈ simple_clss (atms_of_mm (init_clss S))›
    using dist incl tauto by (auto simp: simple_clss_def)
  have tot': ‹total_over_m (lits_of_l (trail S)) (set_mset (init_clss S))› and
    confl: ‹conflicting S = None› and
    T: ‹T ∼ update_weight_information (trail S) S›
    using imp nd by (auto simp: is_improving_int_def improve.simps)
  have M': ‹ρ (lit_of `# mset M') = ρ (lit_of `# mset (trail S))›
    if ‹total_over_m (lits_of_l M') (set_mset (init_clss S))› and
      incl: ‹mset (trail S) ⊆# mset M'› and
      ‹lit_of `# mset M' ∈ simple_clss (atms_of_mm (init_clss S))›
      for M'
    proof -
      have [simp]: ‹lits_of_l M' = set_mset (lit_of `# mset M')›
        by (auto simp: lits_of_def)
      obtain A where A: ‹mset M' = A + mset (trail S)›
        using incl by (auto simp: mset_subset_eq_exists_conv)
      have M': ‹lits_of_l M' = lit_of ` set_mset A ∪ lits_of_l (trail S)›
        unfolding lits_of_def
        by (metis A image_Un set_mset_mset set_mset_union)
      have ‹mset M' = mset (trail S)›
        using that tot' unfolding A total_over_m_alt_def
          apply (case_tac A)
        apply (auto simp: A simple_clss_def distinct_mset_add M' image_Un
            tautology_union mset_inter_empty_set_mset atms_of_def atms_of_s_def
            atm_of_in_atm_of_set_iff_in_set_or_uminus_in_set image_image
            tautology_add_mset)
          by (metis (no_types, lifting) atm_of_in_atm_of_set_iff_in_set_or_uminus_in_set
          lits_of_def subsetCE)
      then show ?thesis
        by auto
    qed

  have ‹lit_of `# mset (trail S) ∈ simple_clss (atms_of_mm (init_clss S))›
    using tauto dist incl by (auto simp: simple_clss_def)
  then have improving: ‹is_improving (trail S) (trail S) S› and
    ‹total_over_m (lits_of_l (trail S)) (set_mset (init_clss S))›
    using imp nd by (auto simp: is_improving_int_def improve.simps intro: M')

  show ‹improvep S T›
    by (rule improvep.intros[OF improving confl T])
qed

lemma ocdcl⇩w_cdcl_bnb:
  assumes ‹ocdcl⇩w S T› and
    inv: ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (abs_state S)›
  shows ‹cdcl_bnb S T›
  using assms by (cases) (auto intro: cdcl_bnb.intros dest: pruning_conflict_opt
    ocdcl_conflict_opt_conflict_opt improve_improvep)


lemma ocdcl⇩w_stgy_cdcl_bnb_stgy:
  assumes ‹ocdcl⇩w_stgy S T› and
    inv: ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (abs_state S)›
  shows ‹cdcl_bnb_stgy S T›
  using assms by (cases)
    (auto intro: cdcl_bnb_stgy.intros dest: pruning_conflict_opt improve_improvep)

lemma rtranclp_ocdcl⇩w_stgy_rtranclp_cdcl_bnb_stgy:
  assumes ‹ocdcl⇩w_stgy⇧*⇧* S T› and
    inv: ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (abs_state S)›
  shows ‹cdcl_bnb_stgy⇧*⇧* S T›
  using assms
  by (induction rule: rtranclp_induct)
    (auto dest: rtranclp_cdcl_bnb_stgy_all_struct_inv[OF rtranclp_cdcl_bnb_stgy_cdcl_bnb]
      ocdcl⇩w_stgy_cdcl_bnb_stgy)

lemma no_step_ocdcl⇩w_no_step_cdcl_bnb:
  assumes ‹no_step ocdcl⇩w S› and
    inv: ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (abs_state S)›
  shows ‹no_step cdcl_bnb S›
proof -
  have
    nsc: ‹no_step conflict S› and
    nsp: ‹no_step propagate S› and
    nsi: ‹no_step improve S› and
    nsco: ‹no_step oconflict_opt S› and
    nso: ‹no_step ocdcl⇩W_o S›and
    nspr: ‹no_step pruning S›
    using assms(1) by (auto simp: cdcl_bnb.simps ocdcl⇩w.simps)
  have alien: ‹cdcl⇩W_restart_mset.no_strange_atm (abs_state S)› and
    lev: ‹cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv (abs_state S)›
    using inv unfolding cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def
    by fast+
  have incl: ‹atms_of (lit_of `# mset (trail S)) ⊆ atms_of_mm (init_clss S)›
    using alien unfolding cdcl⇩W_restart_mset.no_strange_atm_def
    by (auto simp: abs_state_def cdcl⇩W_restart_mset_state lits_of_def image_image atms_of_def)
  have dist: ‹distinct_mset (lit_of `# mset (trail S))› and
    cons: ‹consistent_interp (set (map lit_of (trail S)))› and
    tauto: ‹¬tautology (lit_of `# mset (trail S))› and
    n_d: ‹no_dup (trail S)›
    using lev unfolding cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv_def
    by (auto simp: abs_state_def cdcl⇩W_restart_mset_state lits_of_def image_image atms_of_def
      dest: no_dup_map_lit_of no_dup_distinct no_dup_not_tautology)

  have nsip: False if imp: ‹improvep S S'› for S'
  proof -
    obtain M' where
      [simp]: ‹conflicting S = None› and
      is_improving:
        ‹⋀M'. total_over_m (lits_of_l M') (set_mset (init_clss S)) ⟶
              mset (trail S) ⊆# mset M' ⟶
              lit_of `# mset M' ∈ simple_clss (atms_of_mm (init_clss S)) ⟶
              ρ (lit_of `# mset M') = ρ (lit_of `# mset (trail S))› and
      S': ‹S' ∼ update_weight_information M' S›
      using imp by (auto simp: improvep.simps is_improving_int_def)
    have 1: ‹¬ ρ' (weight S) ≤ Found (ρ (lit_of `# mset (trail S)))›
      using nsco
      by (auto simp: is_improving_int_def oconflict_opt.simps)
    have 2: ‹total_over_m (lits_of_l (trail S)) (set_mset (init_clss S))›
    proof (rule ccontr)
      assume ‹¬ ?thesis›
      then obtain A where
        ‹A ∈ atms_of_mm (init_clss S)› and
        ‹A ∉ atms_of_s (lits_of_l (trail S))›
        by (auto simp: total_over_m_def total_over_set_def)
      then show ‹False›
        using decide_rule[of S ‹Pos A›, OF _ _ _ state_eq_ref] nso
        by (auto simp: Decided_Propagated_in_iff_in_lits_of_l ocdcl⇩W_o.simps)
    qed
    have 3: ‹trail S ⊨asm init_clss S›
      unfolding true_annots_def
    proof clarify
      fix C
      assume C: ‹C ∈# init_clss S›
      have ‹total_over_m (lits_of_l (trail S)) {C}›
        using 2 C by (auto dest!: multi_member_split)
      moreover have ‹¬ trail S ⊨as CNot C›
        using C nsc conflict_rule[of S C, OF _ _ _ state_eq_ref]
        by (auto simp: clauses_def dest!: multi_member_split)
      ultimately show ‹trail S ⊨a C›
        using total_not_CNot[of ‹lits_of_l (trail S)› C] unfolding true_annots_true_cls true_annot_def
        by auto
    qed
    have 4: ‹lit_of `# mset (trail S) ∈ simple_clss (atms_of_mm (init_clss S))›
      using tauto cons incl dist by (auto simp: simple_clss_def)
    have ‹improve S (update_weight_information (trail S) S)›
      by (rule improve.intros[OF 2 _ 3]) (use 1 2 in auto)
    then show False
      using nsi by auto
  qed
  moreover have False if ‹conflict_opt S S'› for S'
  proof -
    have [simp]: ‹conflicting S = None›
      using that by (auto simp: conflict_opt.simps)
    have 1: ‹¬ ρ' (weight S) ≤ Found (ρ (lit_of `# mset (trail S)))›
      using nsco
      by (auto simp: is_improving_int_def oconflict_opt.simps)
    have 2: ‹total_over_m (lits_of_l (trail S)) (set_mset (init_clss S))›
    proof (rule ccontr)
      assume ‹¬ ?thesis›
      then obtain A where
        ‹A ∈ atms_of_mm (init_clss S)› and
        ‹A ∉ atms_of_s (lits_of_l (trail S))›
        by (auto simp: total_over_m_def total_over_set_def)
      then show ‹False›
        using decide_rule[of S ‹Pos A›, OF _ _ _ state_eq_ref] nso
        by (auto simp: Decided_Propagated_in_iff_in_lits_of_l ocdcl⇩W_o.simps)
      qed
    have 3: ‹trail S ⊨asm init_clss S›
      unfolding true_annots_def
    proof clarify
      fix C
      assume C: ‹C ∈# init_clss S›
      have ‹total_over_m (lits_of_l (trail S)) {C}›
        using 2 C by (auto dest!: multi_member_split)
      moreover have ‹¬ trail S ⊨as CNot C›
        using C nsc conflict_rule[of S C, OF _ _ _ state_eq_ref]
        by (auto simp: clauses_def dest!: multi_member_split)
      ultimately show ‹trail S ⊨a C›
        using total_not_CNot[of ‹lits_of_l (trail S)› C] unfolding true_annots_true_cls true_annot_def
        by auto
    qed
    have 4: ‹lit_of `# mset (trail S) ∈ simple_clss (atms_of_mm (init_clss S))›
      using tauto cons incl dist by (auto simp: simple_clss_def)

    have [intro]: ‹ρ (lit_of `# mset M') = ρ (lit_of `# mset (trail S))›
      if
        ‹lit_of `# mset (trail S) ∈ simple_clss (atms_of_mm (init_clss S))› and
        ‹atms_of (lit_of `# mset (trail S)) ⊆ atms_of_mm (init_clss S)› and
        ‹no_dup (trail S)› and
        ‹total_over_m (lits_of_l M') (set_mset (init_clss S))› and
        incl: ‹mset (trail S) ⊆# mset M'› and
        ‹lit_of `# mset M' ∈ simple_clss (atms_of_mm (init_clss S))›
      for M' :: ‹('v literal, 'v literal, 'v literal multiset) annotated_lit list›
    proof -
      have [simp]: ‹lits_of_l M' = set_mset (lit_of `# mset M')›
        by (auto simp: lits_of_def)
      obtain A where A: ‹mset M' = A + mset (trail S)›
        using incl by (auto simp: mset_subset_eq_exists_conv)
      have M': ‹lits_of_l M' = lit_of ` set_mset A ∪ lits_of_l (trail S)›
        unfolding lits_of_def
        by (metis A image_Un set_mset_mset set_mset_union)
      have ‹mset M' = mset (trail S)›
        using that 2 unfolding A total_over_m_alt_def
        apply (case_tac A)
        apply (auto simp: A simple_clss_def distinct_mset_add M' image_Un
            tautology_union mset_inter_empty_set_mset atms_of_def atms_of_s_def
            atm_of_in_atm_of_set_iff_in_set_or_uminus_in_set image_image
            tautology_add_mset)
        by (metis (no_types, lifting) atm_of_in_atm_of_set_iff_in_set_or_uminus_in_set
            lits_of_def subsetCE)
      then show ?thesis
        using 2 by auto
    qed
    have imp: ‹is_improving (trail S) (trail S) S›
      using 1 2 3 4 incl n_d unfolding is_improving_int_def
      by (auto simp:  oconflict_opt.simps)

    show ‹False›
      using trail_is_improving_Ex_improve[of S, OF _ imp] nsip
      by auto
  qed
  ultimately show ?thesis
    using nsc nsp nsi nsco nso nsp nspr
    by (auto simp: cdcl_bnb.simps)
qed

lemma all_struct_init_state_distinct_iff:
  ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (abs_state (init_state N)) ⟷
  distinct_mset_mset N›
  unfolding init_state.simps[symmetric]
  by (auto simp: cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def
      cdcl⇩W_restart_mset.distinct_cdcl⇩W_state_def
      cdcl⇩W_restart_mset.no_strange_atm_def
      cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv_def
      cdcl⇩W_restart_mset.cdcl⇩W_conflicting_def
      cdcl⇩W_restart_mset.cdcl⇩W_learned_clause_alt_def
      abs_state_def cdcl⇩W_restart_mset_state)

lemma no_step_ocdcl⇩w_stgy_no_step_cdcl_bnb_stgy:
  assumes ‹no_step ocdcl⇩w_stgy S› and
    inv: ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (abs_state S)›
  shows ‹no_step cdcl_bnb_stgy S›
  using assms no_step_ocdcl⇩w_no_step_cdcl_bnb[of S]
  by (auto simp: ocdcl⇩w_stgy.simps ocdcl⇩w.simps cdcl_bnb.simps cdcl_bnb_stgy.simps
    dest: ocdcl_conflict_opt_conflict_opt pruning_conflict_opt)

lemma full_ocdcl⇩w_stgy_full_cdcl_bnb_stgy:
  assumes ‹full ocdcl⇩w_stgy S T› and
    inv: ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (abs_state S)›
  shows ‹full cdcl_bnb_stgy S T›
  using assms rtranclp_ocdcl⇩w_stgy_rtranclp_cdcl_bnb_stgy[of S T]
    no_step_ocdcl⇩w_stgy_no_step_cdcl_bnb_stgy[of T]
  unfolding full_def
  by (auto dest: rtranclp_cdcl_bnb_stgy_all_struct_inv[OF rtranclp_cdcl_bnb_stgy_cdcl_bnb])

corollary full_ocdcl⇩w_stgy_no_conflicting_clause_from_init_state: (* \htmllink{ocdcl-correctness} *)
  assumes
    st: ‹full ocdcl⇩w_stgy (init_state N) T› and
    dist: ‹distinct_mset_mset N›
  shows
    ‹weight T = None ⟹ unsatisfiable (set_mset N)› and
    ‹weight T ≠ None ⟹ model_on (set_mset (the (weight T))) N ∧ set_mset (the (weight T)) ⊨sm N ∧
       distinct_mset (the (weight T))› and
    ‹distinct_mset I ⟹ consistent_interp (set_mset I) ⟹ atms_of I = atms_of_mm N ⟹
      set_mset I ⊨sm N ⟹ Found (ρ I) ≥ ρ' (weight T)›
  using full_cdcl_bnb_stgy_no_conflicting_clause_from_init_state[of N T,
    OF full_ocdcl⇩w_stgy_full_cdcl_bnb_stgy[OF st] dist] dist
  by (auto simp: all_struct_init_state_distinct_iff model_on_def
    dest: multi_member_split)


lemma wf_ocdcl⇩w:  (* \htmllink{ocdcl-improve-termination} *)
  ‹wf {(T, S). cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (abs_state S)
     ∧ ocdcl⇩w S T}›
  by (rule wf_subset[OF wf_cdcl_bnb2]) (auto dest: ocdcl⇩w_cdcl_bnb)


subsubsection ‹Calculus with generalised Improve rule›

text ‹Now a version with the more general improve rule:›
inductive ocdcl⇩w_p :: ‹'st ⇒ 'st ⇒ bool› for S :: 'st where
ocdcl_conflict: ‹conflict S S' ⟹ ocdcl⇩w_p S S'› |
ocdcl_propagate: ‹propagate S S' ⟹ ocdcl⇩w_p S S'› |
ocdcl_improve: ‹improvep S S' ⟹ ocdcl⇩w_p S S'› |
ocdcl_conflict_opt: ‹oconflict_opt S S' ⟹ ocdcl⇩w_p S S'› |
ocdcl_other': ‹ocdcl⇩W_o S S' ⟹ ocdcl⇩w_p S S'› |
ocdcl_pruning: ‹pruning S S' ⟹ ocdcl⇩w_p S S'›

inductive ocdcl⇩w_p_stgy :: ‹'st ⇒ 'st ⇒ bool› for S :: 'st where
ocdcl⇩w_p_conflict: ‹conflict S S' ⟹ ocdcl⇩w_p_stgy S S'› |
ocdcl⇩w_p_propagate: ‹propagate S S' ⟹ ocdcl⇩w_p_stgy S S'› |
ocdcl⇩w_p_improve: ‹improvep S S' ⟹ ocdcl⇩w_p_stgy S S'› |
ocdcl⇩w_p_conflict_opt: ‹conflict_opt S S' ⟹ ocdcl⇩w_p_stgy S S'›|
ocdcl⇩w_p_pruning: ‹pruning S S' ⟹ ocdcl⇩w_p_stgy S S'› |
ocdcl⇩w_p_other': ‹ocdcl⇩W_o S S' ⟹ no_confl_prop_impr S ⟹ ocdcl⇩w_p_stgy S S'›

lemma ocdcl⇩w_p_cdcl_bnb:
  assumes ‹ocdcl⇩w_p S T› and
    inv: ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (abs_state S)›
  shows ‹cdcl_bnb S T›
  using assms by (cases) (auto intro: cdcl_bnb.intros dest: pruning_conflict_opt
    ocdcl_conflict_opt_conflict_opt)


lemma ocdcl⇩w_p_stgy_cdcl_bnb_stgy:
  assumes ‹ocdcl⇩w_p_stgy S T› and
    inv: ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (abs_state S)›
  shows ‹cdcl_bnb_stgy S T›
  using assms by (cases) (auto intro: cdcl_bnb_stgy.intros dest: pruning_conflict_opt)

lemma rtranclp_ocdcl⇩w_p_stgy_rtranclp_cdcl_bnb_stgy:
  assumes ‹ocdcl⇩w_p_stgy⇧*⇧* S T› and
    inv: ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (abs_state S)›
  shows ‹cdcl_bnb_stgy⇧*⇧* S T›
  using assms
  by (induction rule: rtranclp_induct)
    (auto dest: rtranclp_cdcl_bnb_stgy_all_struct_inv[OF rtranclp_cdcl_bnb_stgy_cdcl_bnb]
      ocdcl⇩w_p_stgy_cdcl_bnb_stgy)

lemma no_step_ocdcl⇩w_p_no_step_cdcl_bnb:
  assumes ‹no_step ocdcl⇩w_p S› and
    inv: ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (abs_state S)›
  shows ‹no_step cdcl_bnb S›
proof -
  have
    nsc: ‹no_step conflict S› and
    nsp: ‹no_step propagate S› and
    nsi: ‹no_step improvep S› and
    nsco: ‹no_step oconflict_opt S› and
    nso: ‹no_step ocdcl⇩W_o S›and
    nspr: ‹no_step pruning S›
    using assms(1) by (auto simp: cdcl_bnb.simps ocdcl⇩w_p.simps)
  have alien: ‹cdcl⇩W_restart_mset.no_strange_atm (abs_state S)› and
    lev: ‹cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv (abs_state S)›
    using inv unfolding cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def
    by fast+
  have incl: ‹atms_of (lit_of `# mset (trail S)) ⊆ atms_of_mm (init_clss S)›
    using alien unfolding cdcl⇩W_restart_mset.no_strange_atm_def
    by (auto simp: abs_state_def cdcl⇩W_restart_mset_state lits_of_def image_image atms_of_def)
  have dist: ‹distinct_mset (lit_of `# mset (trail S))› and
    cons: ‹consistent_interp (set (map lit_of (trail S)))› and
    tauto: ‹¬tautology (lit_of `# mset (trail S))› and
    n_d: ‹no_dup (trail S)›
    using lev unfolding cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv_def
    by (auto simp: abs_state_def cdcl⇩W_restart_mset_state lits_of_def image_image atms_of_def
      dest: no_dup_map_lit_of no_dup_distinct no_dup_not_tautology)

  have False if ‹conflict_opt S S'› for S'
  proof -
    have [simp]: ‹conflicting S = None›
      using that by (auto simp: conflict_opt.simps)
    have 1: ‹¬ ρ' (weight S) ≤ Found (ρ (lit_of `# mset (trail S)))›
      using nsco
      by (auto simp: is_improving_int_def oconflict_opt.simps)
    have 2: ‹total_over_m (lits_of_l (trail S)) (set_mset (init_clss S))›
    proof (rule ccontr)
      assume ‹¬ ?thesis›
      then obtain A where
        ‹A ∈ atms_of_mm (init_clss S)› and
        ‹A ∉ atms_of_s (lits_of_l (trail S))›
        by (auto simp: total_over_m_def total_over_set_def)
      then show ‹False›
        using decide_rule[of S ‹Pos A›, OF _ _ _ state_eq_ref] nso
        by (auto simp: Decided_Propagated_in_iff_in_lits_of_l ocdcl⇩W_o.simps)
      qed
    have 3: ‹trail S ⊨asm init_clss S›
      unfolding true_annots_def
    proof clarify
      fix C
      assume C: ‹C ∈# init_clss S›
      have ‹total_over_m (lits_of_l (trail S)) {C}›
        using 2 C by (auto dest!: multi_member_split)
      moreover have ‹¬ trail S ⊨as CNot C›
        using C nsc conflict_rule[of S C, OF _ _ _ state_eq_ref]
        by (auto simp: clauses_def dest!: multi_member_split)
      ultimately show ‹trail S ⊨a C›
        using total_not_CNot[of ‹lits_of_l (trail S)› C] unfolding true_annots_true_cls true_annot_def
        by auto
    qed
    have 4: ‹lit_of `# mset (trail S) ∈ simple_clss (atms_of_mm (init_clss S))›
      using tauto cons incl dist by (auto simp: simple_clss_def)

    have [intro]: ‹ρ (lit_of `# mset M') = ρ (lit_of `# mset (trail S))›
      if
        ‹lit_of `# mset (trail S) ∈ simple_clss (atms_of_mm (init_clss S))› and
        ‹atms_of (lit_of `# mset (trail S)) ⊆ atms_of_mm (init_clss S)› and
        ‹no_dup (trail S)› and
        ‹total_over_m (lits_of_l M') (set_mset (init_clss S))› and
        incl: ‹mset (trail S) ⊆# mset M'› and
        ‹lit_of `# mset M' ∈ simple_clss (atms_of_mm (init_clss S))›
      for M' :: ‹('v literal, 'v literal, 'v literal multiset) annotated_lit list›
    proof -
      have [simp]: ‹lits_of_l M' = set_mset (lit_of `# mset M')›
        by (auto simp: lits_of_def)
      obtain A where A: ‹mset M' = A + mset (trail S)›
        using incl by (auto simp: mset_subset_eq_exists_conv)
      have M': ‹lits_of_l M' = lit_of ` set_mset A ∪ lits_of_l (trail S)›
        unfolding lits_of_def
        by (metis A image_Un set_mset_mset set_mset_union)
      have ‹mset M' = mset (trail S)›
        using that 2 unfolding A total_over_m_alt_def
          apply (case_tac A)
        apply (auto simp: A simple_clss_def distinct_mset_add M' image_Un
            tautology_union mset_inter_empty_set_mset atms_of_def atms_of_s_def
            atm_of_in_atm_of_set_iff_in_set_or_uminus_in_set image_image
            tautology_add_mset)
          by (metis (no_types, lifting) atm_of_in_atm_of_set_iff_in_set_or_uminus_in_set
          lits_of_def subsetCE)
      then show ?thesis
        using 2 by auto
    qed
    have imp: ‹is_improving (trail S) (trail S) S›
      using 1 2 3 4 incl n_d unfolding is_improving_int_def
      by (auto simp:  oconflict_opt.simps)

    show ‹False›
      using trail_is_improving_Ex_improve[of S, OF _ imp] nsi by auto
  qed
  then show ?thesis
    using nsc nsp nsi nsco nso nsp nspr
    by (auto simp: cdcl_bnb.simps)
qed

lemma no_step_ocdcl⇩w_p_stgy_no_step_cdcl_bnb_stgy:
  assumes ‹no_step ocdcl⇩w_p_stgy S› and
    inv: ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (abs_state S)›
  shows ‹no_step cdcl_bnb_stgy S›
  using assms no_step_ocdcl⇩w_p_no_step_cdcl_bnb[of S]
  by (auto simp: ocdcl⇩w_p_stgy.simps ocdcl⇩w_p.simps
    cdcl_bnb.simps cdcl_bnb_stgy.simps)

lemma full_ocdcl⇩w_p_stgy_full_cdcl_bnb_stgy:
  assumes ‹full ocdcl⇩w_p_stgy S T› and
    inv: ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (abs_state S)›
  shows ‹full cdcl_bnb_stgy S T›
  using assms rtranclp_ocdcl⇩w_p_stgy_rtranclp_cdcl_bnb_stgy[of S T]
    no_step_ocdcl⇩w_p_stgy_no_step_cdcl_bnb_stgy[of T]
  unfolding full_def
  by (auto dest: rtranclp_cdcl_bnb_stgy_all_struct_inv[OF rtranclp_cdcl_bnb_stgy_cdcl_bnb])

corollary full_ocdcl⇩w_p_stgy_no_conflicting_clause_from_init_state: (* \htmllink{ocdcl-improvep-correctness} *)
  assumes
    st: ‹full ocdcl⇩w_p_stgy (init_state N) T› and
    dist: ‹distinct_mset_mset N›
  shows
    ‹weight T = None ⟹ unsatisfiable (set_mset N)› and
    ‹weight T ≠ None ⟹ model_on (set_mset (the (weight T))) N ∧ set_mset (the (weight T)) ⊨sm N ∧
       distinct_mset (the (weight T))› and
    ‹distinct_mset I ⟹ consistent_interp (set_mset I) ⟹ atms_of I = atms_of_mm N ⟹
      set_mset I ⊨sm N ⟹ Found (ρ I) ≥ ρ' (weight T)›
  using full_cdcl_bnb_stgy_no_conflicting_clause_from_init_state[of N T,
    OF full_ocdcl⇩w_p_stgy_full_cdcl_bnb_stgy[OF st] dist] dist
  by (auto simp: all_struct_init_state_distinct_iff model_on_def
    dest: multi_member_split)


lemma cdcl_bnb_stgy_no_smaller_propa:
  ‹cdcl_bnb_stgy S T ⟹ cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (abs_state S) ⟹
    no_smaller_propa S ⟹ no_smaller_propa T›
  apply (induction rule: cdcl_bnb_stgy.induct)
  subgoal
    by (auto simp: no_smaller_propa_def propagated_cons_eq_append_decide_cons conflict.simps)
  subgoal
    by (auto simp: no_smaller_propa_def propagated_cons_eq_append_decide_cons
        propagate.simps no_smaller_propa_tl elim!: rulesE)
  subgoal
    by (auto simp: no_smaller_propa_def propagated_cons_eq_append_decide_cons
          improvep.simps elim!: rulesE)
  subgoal
    by (auto simp: no_smaller_propa_def propagated_cons_eq_append_decide_cons
           conflict_opt.simps no_smaller_propa_tl elim!: rulesE)
  subgoal for T
    apply (cases rule: ocdcl⇩W_o.cases, assumption; thin_tac ‹ocdcl⇩W_o S T›)
    subgoal
      using decide_no_smaller_step[of S T] unfolding no_confl_prop_impr.simps by auto
    subgoal
      apply (cases rule: cdcl_bnb_bj.cases, assumption; thin_tac ‹cdcl_bnb_bj S T›)
      subgoal
        by (use no_smaller_propa_tl[of S T] in ‹auto elim: rulesE›)
      subgoal
        by (use no_smaller_propa_tl[of S T] in ‹auto elim: rulesE›)
      subgoal
        using backtrackg_no_smaller_propa[OF obacktrack_backtrackg, of S T]
        unfolding cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def
          cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv_def cdcl⇩W_restart_mset.cdcl⇩W_conflicting_def
        by (auto elim: obacktrackE)
      done
    done
  done

lemma rtranclp_cdcl_bnb_stgy_no_smaller_propa:
  ‹cdcl_bnb_stgy⇧*⇧* S T ⟹ cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (abs_state S) ⟹
    no_smaller_propa S ⟹ no_smaller_propa T›
  by (induction rule: rtranclp_induct)
    (use rtranclp_cdcl_bnb_stgy_all_struct_inv
        rtranclp_cdcl_bnb_stgy_cdcl_bnb in ‹force intro: cdcl_bnb_stgy_no_smaller_propa›)+

lemma wf_ocdcl⇩w_p:  (* \htmllink{ocdcl-improvep-termination} *)
  ‹wf {(T, S). cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (abs_state S)
     ∧ ocdcl⇩w_p S T}›
  by (rule wf_subset[OF wf_cdcl_bnb2]) (auto dest: ocdcl⇩w_p_cdcl_bnb)

end

end