Theory IsaSAT_LBD

theory IsaSAT_LBD
  imports IsaSAT_Setup
begin

definition mark_lbd_from_clause_heur :: ‹trail_pol ⇒ arena ⇒ nat ⇒ lbd ⇒ lbd nres› where
  ‹mark_lbd_from_clause_heur M N C lbd = do {
  n ← mop_arena_length N C;
  nfoldli [1..<n] (λ_. True)
    (λi lbd. do {
       L ← mop_arena_lit2 N C i;
       ASSERT(get_level_pol_pre (M, L));
       let lev = get_level_pol M L;
       ASSERT(lev ≤ Suc (unat32_max div 2));
       RETURN (if lev = 0 then lbd else lbd_write lbd lev)})
    lbd}›

lemma count_decided_le_length: ‹count_decided M ≤ length M›
  unfolding count_decided_def by (rule length_filter_le)

lemma mark_lbd_from_clause_heur_correctness:
  assumes ‹(M, M') ∈ trail_pol 𝒜› and ‹valid_arena N N' vdom› ‹C ∈# dom_m N'› and
    ‹literals_are_in_ℒin 𝒜 (mset (N' ∝ C))›
  shows ‹mark_lbd_from_clause_heur M N C lbd ≤ ⇓ Id (SPEC(λ_::bool list. True))›
  using assms
  unfolding mark_lbd_from_clause_heur_def
  apply (refine_vcg mop_arena_length[THEN fref_to_Down_curry, THEN order_trans, of N' C _ _ vdom]
        nfoldli_rule[where I = ‹ λ_ _ _. True›])
  subgoal by auto
  subgoal by auto
  unfolding Down_id_eq comp_def
  apply (refine_vcg mop_arena_length[THEN fref_to_Down_curry, THEN order_trans, of N' C _ _ vdom]
        nfoldli_rule[where I = ‹ λ_ _ _. True›] mop_arena_lit[THEN order_trans])
  subgoal by auto
  apply assumption+
  subgoal by simp
  apply auto[]
  subgoal H
    by (metis append_cons_eq_upt(2) eq_upt_Cons_conv)
  subgoal for x l1 l2 σ xa using H[of l1 x l2] apply -
    by (auto intro!: get_level_pol_pre  literals_are_in_ℒin_in_ℒall)
  subgoal for x l1 l2 σ xa using H[of l1 x l2] apply -
    using count_decided_ge_get_level[of M' xa] count_decided_le_length[of M']
    by (auto simp: trail_pol_alt_def literals_are_in_ℒin_in_ℒall simp flip: get_level_get_level_pol)
  done

definition calculate_LBD_st :: ‹(nat, nat) ann_lits ⇒ nat clauses_l ⇒ nat ⇒ nat clauses_l nres› where
  ‹calculate_LBD_st = (λM N C. RETURN N)›

abbreviation TIER_TWO_MAXIMUM where
  ‹TIER_TWO_MAXIMUM ≡ 6›

abbreviation TIER_ONE_MAXIMUM where
  ‹TIER_ONE_MAXIMUM ≡ 2›

definition calculate_LBD_heur_st :: ‹_ ⇒ arena ⇒ lbd ⇒ nat ⇒ (arena × lbd) nres› where
  ‹calculate_LBD_heur_st = (λM N lbd C. do{
     old_glue ← mop_arena_lbd N C;
     st ← mop_arena_status N C;
     if st = IRRED then RETURN (N, lbd)
     else if old_glue < TIER_TWO_MAXIMUM then do {
       N ← mop_arena_mark_used2 N C;
       RETURN (N, lbd)
     }
     else do {
       lbd ← mark_lbd_from_clause_heur M N C lbd;
       glue ← get_LBD lbd;
       lbd ← lbd_empty lbd;
       N ← (if glue < old_glue then mop_arena_update_lbd C glue N else RETURN N);
       N ← (if glue < TIER_TWO_MAXIMUM ∨ old_glue < TIER_TWO_MAXIMUM then mop_arena_mark_used2 N C else mop_arena_mark_used N C);
       RETURN (N, lbd)
    }})›


lemma calculate_LBD_st_alt_def:
  ‹calculate_LBD_st = (λM N C. do {
      old_glue :: nat ← SPEC(λ_ . True);
      st :: clause_status ← SPEC(λ_ . True);
      if st = IRRED then RETURN N
      else if old_glue < 6 then  do {
         _ ← RETURN N;
         RETURN N
      }
      else do {
       lbd::bool list ← SPEC(λ_. True);
       glue::nat ← get_LBD lbd;
       _::bool list ← lbd_empty lbd;
       _ ← RETURN N;
       _ ← RETURN N;
      RETURN N
    }})› (is ‹?A = ?B›)
  unfolding calculate_LBD_st_def get_LBD_def lbd_empty_def
  by (auto intro!: ext rhs_step_bind_RES split: if_splits cong: if_cong)


(* TODO Move *)
lemma RF_COME_ON: ‹(x, y) ∈ Id ⟹ f x ≤ ⇓ Id (f y)›
  by auto

lemma mop_arena_update_lbd:
  ‹C ∈# dom_m N ⟹ valid_arena arena N vdom ⟹
     mop_arena_update_lbd C glue arena ≤ SPEC(λc. (c, N) ∈ {(c, N'). N'=N ∧ valid_arena c N vdom ∧
       length c = length arena})›
  unfolding mop_arena_update_lbd_def
  by (auto simp: update_lbd_pre_def arena_is_valid_clause_idx_def
    intro!: ASSERT_leI valid_arena_update_lbd)

lemma mop_arena_mark_used_valid:
  ‹C ∈# dom_m N ⟹ valid_arena arena N vdom ⟹
     mop_arena_mark_used arena C ≤ SPEC(λc. (c, N) ∈ {(c, N'). N'=N ∧ valid_arena c N vdom ∧
       length c = length arena})›
  unfolding mop_arena_mark_used_def
  by (auto simp: arena_act_pre_def arena_is_valid_clause_idx_def
    intro!: ASSERT_leI valid_arena_mark_used)

lemma mop_arena_mark_used2_valid:
  ‹C ∈# dom_m N ⟹ valid_arena arena N vdom ⟹
     mop_arena_mark_used2 arena C ≤ SPEC(λc. (c, N) ∈ {(c, N'). N'=N ∧ valid_arena c N vdom ∧
       length c = length arena})›
  unfolding mop_arena_mark_used2_def
  by (auto simp: arena_act_pre_def arena_is_valid_clause_idx_def
    intro!: ASSERT_leI valid_arena_mark_used2)

abbreviation twl_st_heur_conflict_ana'
  :: ‹nat ⇒ clss_size ⇒ (isasat × nat twl_st_wl) set›
where
  ‹twl_st_heur_conflict_ana' r lcount ≡ {(S, T). (S, T) ∈ twl_st_heur_conflict_ana ∧
     length (get_clauses_wl_heur S) = r ∧ get_learned_count S = lcount}›

lemma calculate_LBD_heur_st_calculate_LBD_st:
  assumes ‹valid_arena arena N vdom›
    ‹(M, M') ∈ trail_pol 𝒜›
    ‹C ∈# dom_m N›
    ‹literals_are_in_ℒin 𝒜 (mset (N ∝ C))› ‹(C, C') ∈ nat_rel›
  shows ‹calculate_LBD_heur_st M arena lbd C ≤
     ⇓{((arena', lbd), N'). valid_arena arena' N' vdom ∧ N = N' ∧ length arena = length arena'}
       (calculate_LBD_st M' N C')›
proof -
  have WTF: ‹(a, b) ∈ R ⟹  b=b' ⟹ (a, b') ∈ R› for a a' b b' R
    by auto
  show ?thesis
    using assms
    unfolding calculate_LBD_heur_st_def calculate_LBD_st_alt_def
    apply (refine_vcg mark_lbd_from_clause_heur_correctness[of _ M'
       𝒜 _ N vdom]
      mop_arena_update_lbd[of _ _ _ vdom]
      mop_arena_mark_used_valid[of _ N _ vdom]
      mop_arena_mark_used2_valid[of _ N _ vdom])
    subgoal
      unfolding twl_st_heur_conflict_ana_def
      by (auto simp: mop_arena_lbd_def get_clause_LBD_pre_def arena_is_valid_clause_idx_def
        intro!: ASSERT_leI exI[of _ N] exI[of _ vdom])
    subgoal
      unfolding twl_st_heur_conflict_ana_def
      by (auto simp: mop_arena_status_def arena_is_valid_clause_vdom_def arena_is_valid_clause_idx_def
        intro!: ASSERT_leI exI[of _ N] exI[of _ vdom])
    subgoal
      by (auto simp: twl_st_heur_conflict_ana_def RETURN_RES_refine_iff)
    subgoal
      by (auto simp: twl_st_heur_conflict_ana_def RETURN_RES_refine_iff)
    subgoal
      by (auto simp: twl_st_heur_conflict_ana_def RETURN_RES_refine_iff)
    subgoal
      by (force simp: twl_st_heur_conflict_ana_def)
    apply (rule RF_COME_ON)
    subgoal
      by auto
    apply (rule RF_COME_ON)
    subgoal
      by auto
    subgoal
      unfolding twl_st_heur_conflict_ana_def
      by (auto simp: mop_arena_lbd_def get_clause_LBD_pre_def arena_is_valid_clause_idx_def
        intro!: ASSERT_leI exI[of _ ‹get_clauses_wl (fst y)›] exI[of _ ‹set (get_vdom (fst x))›])
    subgoal
      by (force simp: twl_st_heur_conflict_ana_def)
    subgoal
      by (force simp: twl_st_heur_conflict_ana_def)
    subgoal
      by (force simp: twl_st_heur_conflict_ana_def)
   done
qed


definition mark_lbd_from_list :: ‹_› where
  ‹mark_lbd_from_list M C lbd = do {
    nfoldli (drop 1 C) (λ_. True)
      (λL lbd. RETURN (lbd_write lbd (get_level M L))) lbd
  }›

definition mark_lbd_from_list_heur :: ‹trail_pol ⇒ nat clause_l ⇒ lbd ⇒ lbd nres› where
  ‹mark_lbd_from_list_heur M C lbd = do {
  let n = length C;
  nfoldli [1..<n] (λ_. True)
    (λi lbd. do {
       ASSERT(i < length C);
       let L = C ! i;
       ASSERT(get_level_pol_pre (M, L));
       let lev = get_level_pol M L;
       ASSERT(lev ≤ Suc (unat32_max div 2));
       RETURN (if lev = 0 then lbd else lbd_write lbd lev)})
    lbd}›

definition mark_lbd_from_conflict :: ‹isasat ⇒ isasat nres› where
  ‹mark_lbd_from_conflict = (λS. do{
     lbd ← mark_lbd_from_list_heur (get_trail_wl_heur S) (get_outlearned_heur S) (get_lbd S);
     RETURN (set_lbd_wl_heur lbd S)
    })›


lemma mark_lbd_from_list_heur_correctness:
  assumes ‹(M, M') ∈ trail_pol 𝒜› and ‹literals_are_in_ℒin 𝒜 (mset (tl C))›
  shows ‹mark_lbd_from_list_heur M C lbd ≤ ⇓ Id (SPEC(λ_::bool list. True))›
  using assms
  unfolding mark_lbd_from_list_heur_def
  apply (refine_vcg nfoldli_rule[where I = ‹λ_ _ _. True›])
  subgoal by auto
  subgoal
    by (auto simp: upt_eq_lel_conv nth_tl)
  subgoal for x l1 l2 σ
    using literals_are_in_ℒin_in_ℒall[of 𝒜 ‹tl C› ‹x - 1›]
    by (auto intro!: get_level_pol_pre  simp: upt_eq_lel_conv nth_tl)
  subgoal for x l1 l2 σ
    using count_decided_ge_get_level[of M' ‹C ! x›] count_decided_le_length[of M']
    using literals_are_in_ℒin_in_ℒall[of 𝒜 ‹tl C› ‹x - 1›]
    by (auto simp: upt_eq_lel_conv nth_tl simp flip: get_level_get_level_pol)
      (auto simp: trail_pol_alt_def)
  done


definition mark_LBD_st :: ‹'v twl_st_wl ⇒ ('v twl_st_wl) nres› where
  ‹mark_LBD_st = (λS. SPEC (λ(T). S = T))›

lemma mark_LBD_st_alt_def:
   ‹mark_LBD_st S = do {n :: bool list ← SPEC (λ_. True); SPEC (λ(T). S = T)}›
  unfolding mark_LBD_st_def
  by auto

lemma mark_lbd_from_conflict_mark_LBD_st:
  ‹(mark_lbd_from_conflict, mark_LBD_st) ∈
    [λS. get_conflict_wl S ≠ None ∧ literals_are_in_ℒin (all_atms_st S) (the (get_conflict_wl S))]f
     twl_st_heur_conflict_ana → ⟨twl_st_heur_conflict_ana⟩nres_rel›
  unfolding mark_lbd_from_conflict_def mark_LBD_st_alt_def
  apply (intro frefI nres_relI)
  subgoal for x y
    apply (refine_rcg mark_lbd_from_list_heur_correctness[of _ ‹get_trail_wl y› ‹all_atms_st y›,
      THEN order_trans])
    subgoal
      by (force simp: twl_st_heur_conflict_ana_def)
    subgoal
      by (rule literals_are_in_ℒin_mono[of _ ‹(the (get_conflict_wl y))›])
        (auto simp: twl_st_heur_conflict_ana_def out_learned_def)
    subgoal by auto
    subgoal by (auto simp: twl_st_heur_conflict_ana_def RETURN_RES_refine_iff)
    done
  done

definition update_lbd_and_mark_used where
  ‹update_lbd_and_mark_used i glue N = 
    (let N = update_lbd i glue N in
    (if glue ≤ TIER_TWO_MAXIMUM then mark_used2 N i else mark_used N i))›

lemma length_update_lbd_and_mark_used[simp]: ‹length (update_lbd_and_mark_used i glue N) = length N›
  by (auto simp: update_lbd_and_mark_used_def Let_def split: if_splits)

text ‹CaDiCaL sets the used flags of clauses only as 1, not as two.›
definition update_lbd_shrunk_clause where
  ‹update_lbd_shrunk_clause C N = do {
     old_glue ← mop_arena_lbd N C;
     st ← mop_arena_status N C;
     le ← mop_arena_length N C;
     ASSERT (le ≥ 2);
     if st = IRRED then RETURN N
     else do {
       let new_glue = (if le - 1 ≥ old_glue then old_glue else le - 1);
       ASSERT (update_lbd_pre ((C, new_glue), N));
       RETURN (update_lbd_and_mark_used C new_glue N)
    }
}›


lemma update_lbd_shrunk_clause_valid:
  ‹C ∈# dom_m N ⟹ valid_arena arena N vdom ⟹
     update_lbd_shrunk_clause C arena ≤ SPEC(λc. (c, N) ∈ {(c, N'). N'=N ∧ valid_arena c N vdom ∧
       length c = length arena})›
  unfolding update_lbd_shrunk_clause_def mop_arena_lbd_def nres_monad3 mop_arena_status_def
    mop_arena_length_def update_lbd_and_mark_used_def
  apply refine_vcg
  subgoal
    unfolding get_clause_LBD_pre_def arena_is_valid_clause_idx_def
    by auto
  subgoal
    unfolding arena_is_valid_clause_vdom_def
    by auto
  subgoal
    unfolding arena_is_valid_clause_idx_def
    by auto
  subgoal
    by (rule arena_lifting(18))
  subgoal by auto
  subgoal by (auto simp: update_lbd_pre_def)
  subgoal by (auto simp: Let_def intro!: valid_arena_mark_used2 valid_arena_mark_used
    valid_arena_update_lbd)
  done

end