Theory IsaSAT_Simplify_Binaries_Defs

theory IsaSAT_Simplify_Binaries_Defs
  imports IsaSAT_Setup
    IsaSAT_Restart_Defs
    IsaSAT_Simplify_Units_Defs
begin

type_synonym 'a ahm = ‹'a list × nat list›

definition ahm_get_marked :: ‹'a::zero ahm ⇒ nat literal ⇒ _› where
  ‹ahm_get_marked = (λ(C,stamp) L. do {
     ASSERT(nat_of_lit L < length C);
     RETURN (C!nat_of_lit L)
  })›


definition get_marked :: ‹(nat literal ⇒ 'a option) × nat ⇒ nat literal ⇒ _›   where
  ‹get_marked C L = do {
     ASSERT(nat_of_lit L < snd C ∧ fst C L ≠ None);
     RETURN (the (fst C L))
  }›


definition array_hash_map_rel :: ‹('a :: zero × 'b) set ⇒ ('a ahm × _) set› where
  ‹array_hash_map_rel R = {((xs, support), (ys, m)). m = length xs ∧
      (set support =nat_of_lit ` dom ys) ∧
      (∀i∈set support. i < m) ∧ distinct support ∧
      (∀L. nat_of_lit L < m ⟶ (ys L = None ⟷ xs ! nat_of_lit L = 0)) ∧
     (∀L. nat_of_lit L < m ⟶ (∀a. ys L = Some a ⟶ xs ! nat_of_lit L ≠ 0 ∧ (xs ! nat_of_lit L, a) ∈ R))}›


definition ahm_is_marked :: ‹'a::zero ahm ⇒ nat literal ⇒ _› where
  ‹ahm_is_marked = (λ(C,stamp) L. do {
     ASSERT(nat_of_lit L < length C);
     RETURN (C!nat_of_lit L ≠ 0)
  })›
definition is_marked :: ‹(nat literal ⇒ 'a option) × nat ⇒ nat literal ⇒ _›   where
  ‹is_marked C L =  do {
     ASSERT(nat_of_lit L < snd C);
     RETURN (fst C L ≠ None)
  }›

definition update_marked :: ‹(nat literal ⇒ _ option) × nat ⇒ nat literal ⇒ _ ⇒
  ((nat literal ⇒ _ option) × nat) nres› where
  ‹update_marked C L v = do {
     ASSERT (nat_of_lit L < snd C ∧ (fst C)L ≠ None);
     RETURN ((fst C)(L := Some v), snd C)
  }›

definition set_marked :: ‹(nat literal ⇒ _ option) × nat ⇒ nat literal ⇒ _ ⇒
  ((nat literal ⇒ _ option) × nat) nres› where
  ‹set_marked C L v = do {
     ASSERT (nat_of_lit L < snd C ∧ (fst C)L = None);
     RETURN ((fst C)(L := Some v), snd C)
  }›


(*TODO rename*)
definition empty :: ‹(nat literal ⇒ 'b option) × nat ⇒ ((nat literal ⇒ 'b option) × nat) nres›   where
  ‹empty = (λ(_, n). do {
     RETURN (λ_. None, n)
  })›

lemma ahm_is_marked_is_marked:
   ‹(uncurry ahm_is_marked, uncurry is_marked)
    ∈  (array_hash_map_rel R) ×f nat_lit_lit_rel → ⟨bool_rel⟩nres_rel›
  unfolding ahm_is_marked_def is_marked_def uncurry_def
  apply (intro frefI nres_relI fun_relI)
  apply refine_vcg
  apply (auto simp: array_hash_map_rel_def ahm_is_marked_def is_marked_def
    intro!: ASSERT_leI)[]
  apply simp
  by (auto simp: array_hash_map_rel_def ahm_is_marked_def is_marked_def
    intro!: ASSERT_leI)




lemma ahm_get_marked_get_marked:
   ‹(uncurry ahm_get_marked, uncurry get_marked)
    ∈  (array_hash_map_rel R) ×f nat_lit_lit_rel → ⟨R⟩nres_rel›
  unfolding ahm_get_marked_def get_marked_def uncurry_def
  apply (intro frefI nres_relI fun_relI)
  apply refine_vcg
  apply (auto simp: array_hash_map_rel_def ahm_is_marked_def is_marked_def
    intro!: ASSERT_leI)[]
  apply clarsimp
  apply (auto simp: array_hash_map_rel_def ahm_is_marked_def is_marked_def
    intro!: ASSERT_leI)[]
  done


definition ahm_set_marked :: ‹'a :: zero ahm ⇒ nat literal ⇒ _› where
  ‹ahm_set_marked= (λ(C,stamp) L v. do {
     ASSERT(nat_of_lit L < length C ∧ Suc (length stamp) ≤ length C);
     RETURN (C[nat_of_lit L := v], stamp @ [nat_of_lit L])
  })›


lemma ahm_set_marked_set_marked:
  assumes [simp]: ‹⋀a. (0, a) ∉ R›
  shows ‹(uncurry2 ahm_set_marked, uncurry2 set_marked)
    ∈  (array_hash_map_rel R) ×f nat_lit_lit_rel ×f R →f ⟨array_hash_map_rel R⟩nres_rel›
proof -
  have [intro!]: ‹Suc (length x2b) ≤ length x1d›
    if
      ‹nat_of_lit x2 < length x1d› and
      ‹x1d ! nat_of_lit x2 = 0› and
      ‹set x2b = nat_of_lit ` {a. ∃y. ac a = Some y}› and
      ‹∀i. (∃y. ac i = Some y) ⟶ nat_of_lit i < length x1d› and
      dist: ‹distinct x2b› and
      ‹∀L. nat_of_lit L < length x1d ⟶ (ac L = None) = (x1d ! nat_of_lit L = 0)› 
    for ac :: ‹nat literal ⇒ 'a option› and x2 :: ‹nat literal› and x2a :: 'a and x1d :: ‹'b list› and x2b :: ‹nat list› and x2d :: 'b
  proof -
    have ‹(set x2b) ⊆ nat_of_lit ` (dom ac) ∩ {0..<length x1d}›
      using that by (auto simp add: dom_def)
    moreover have ‹nat_of_lit x2 ∈  {0..<length x1d}›  and notin: ‹nat_of_lit x2 ∉ set x2b›
      using that by auto
    ultimately have H: ‹insert (nat_of_lit x2) (set x2b) ⊆ {0..<length x1d}›
      by blast
    show ?thesis
      using card_mono[OF _ H] notin dist
      by (auto simp: distinct_card)
  qed
  show ?thesis
    unfolding ahm_set_marked_def set_marked_def uncurry_def
    apply (intro frefI fun_relI nres_relI)
    apply refine_vcg
    apply (auto simp: array_hash_map_rel_def ahm_is_marked_def is_marked_def dom_def
      intro!: ASSERT_leI)
   done
qed


definition ahm_update_marked :: ‹'a :: zero ahm ⇒ nat literal ⇒ _› where
  ‹ahm_update_marked= (λ(C,stamp) L v. do {
     ASSERT(nat_of_lit L < length C);
     RETURN (C[nat_of_lit L := v], stamp)
  })›


lemma ahm_update_marked_update_marked:
  assumes [simp]: ‹⋀a. (0, a) ∉ R›
  shows ‹(uncurry2 ahm_update_marked, uncurry2 update_marked)
    ∈  (array_hash_map_rel R) ×f nat_lit_lit_rel ×f R →f ⟨array_hash_map_rel R⟩nres_rel›
  unfolding ahm_update_marked_def update_marked_def uncurry_def
  apply (intro frefI nres_relI)
  by refine_vcg
   (auto simp: array_hash_map_rel_def ahm_is_marked_def is_marked_def dom_def
    intro!: ASSERT_leI)

definition ahm_create :: ‹nat ⇒ 'a::zero ahm nres› where
  ‹ahm_create m = do {
     RETURN (replicate m 0, [])
  }›


definition create :: ‹nat ⇒ _›   where
  ‹create m = do {
     RETURN (λ_. None, m)
  }›

lemma ahm_create_create:
   ‹(ahm_create, create) ∈ nat_rel → ⟨array_hash_map_rel R⟩nres_rel›
  unfolding ahm_create_def create_def uncurry_def
  by refine_vcg
    (auto simp: array_hash_map_rel_def ahm_is_marked_def is_marked_def
    intro!: ASSERT_leI)[]


definition ahm_empty :: ‹'a::zero ahm ⇒ 'a ahm nres› where
  ‹ahm_empty = (λ(CS, support). do {
    let n = length support;
    (_, CS) ← WHILET
      (λ(i, CS). i < n)
      (λ(i, CS). do {ASSERT (i < length support ∧ support ! i < length CS); RETURN (i+1, CS[support ! i := 0])})
      (0, CS);
    RETURN (CS, take 0 support)
  })›


lemma ahm_empty_empty:
  ‹(ahm_empty, empty) ∈ (array_hash_map_rel R) → ⟨array_hash_map_rel R⟩nres_rel›
proof -
  have [simp]: ‹dom (λaa. if nat_of_lit aa ∈ xs then None else m aa) =
    dom m - {a. nat_of_lit a ∈ xs}› for xs m
    by (auto split: if_splits)
  have [simp]: ‹nat_of_lit ` dom x1 = set x2a ⟹ distinct x2a ⟹
    nat_of_lit ` (dom x1 - {aa. nat_of_lit aa ∈ set (take a x2a)}) = set (drop a x2a)› for x2a a x1
    apply (drule eq_commute[of _ "set x2a", THEN iffD1])
    apply (auto simp: dom_def)
    apply (metis (mono_tags, lifting) Reversed_Bit_Lists.atd_lem UnE image_subset_iff mem_Collect_eq set_append set_mset_mono set_mset_mset subset_mset.dual_order.refl)
    apply (frule in_set_dropD)
    apply simp
    by (smt (verit, ccfv_threshold) DiffI IntI Reversed_Bit_Lists.atd_lem distinct_append empty_iff image_iff mem_Collect_eq)

  show ?thesis
    unfolding ahm_empty_def empty_def uncurry_def fref_param1
    apply (intro ext frefI nres_relI)
    subgoal for x y
      apply (refine_vcg WHILET_rule[where I = ‹λ(i, CS).  ((CS, drop i (snd x)), (λa. if nat_of_lit a ∈ set (take i (snd x)) then None else fst y a, snd y)) ∈array_hash_map_rel R› and
        R = ‹measure (λ(i,_). length (snd x) -i)›])
      subgoal by auto
      subgoal by auto
      subgoal by (clarsimp simp: array_hash_map_rel_def)
      subgoal by (auto simp: array_hash_map_rel_def)
      subgoal premises p for x1 x2 x1a x2a s a b x1b x2b
        using p
        by (clarsimp simp: array_hash_map_rel_def less_Suc_eq  eq_commute[of _ ‹nat_of_lit ` dom _›]
          simp flip: Cons_nth_drop_Suc)
          (auto simp: take_Suc_conv_app_nth)
      subgoal by (auto simp: nth_list_update' less_Suc_eq array_hash_map_rel_def)
      subgoal for x1 x2 x1a x2a s a b
        apply (auto simp: array_hash_map_rel_def)
        apply (drule_tac x=L in spec)
        apply (auto split: if_splits)
        done
      done
    done
qed

definition isa_clause_remove_duplicate_clause_wl :: ‹nat ⇒ isasat ⇒ isasat nres› where
  ‹isa_clause_remove_duplicate_clause_wl C S = (do{
    _ ← log_del_clause_heur S C;
    let N' = get_clauses_wl_heur S;
    st ← mop_arena_status N' C;
    let st = st = IRRED;
    ASSERT (mark_garbage_pre (N', C) ∧ arena_is_valid_clause_vdom (N') C);
    let N' = extra_information_mark_to_delete (N') C;
    let lcount = get_learned_count S;
    ASSERT(¬st ⟶ clss_size_lcount lcount ≥ 1);
    let lcount = (if st then lcount else (clss_size_decr_lcount lcount));
    let stats = get_stats_heur S;
    let stats = (incr_binary_red_removed (if st then decr_irred_clss stats else stats));
    let S = set_clauses_wl_heur N' S;
    let S = set_learned_count_wl_heur lcount S;
    let S = set_stats_wl_heur stats S;
    RETURN S
   })›

definition isa_binary_clause_subres_lits_wl_pre :: ‹_› where
  ‹isa_binary_clause_subres_lits_wl_pre C L L' S ⟷
    (∃T r u. (S, T)∈ twl_st_heur_restart_ana' r u ∧  binary_clause_subres_lits_wl_pre C L L' T)›

definition isa_binary_clause_subres_wl :: ‹_› where
  ‹isa_binary_clause_subres_wl C L L' S = do {
      ASSERT (isa_binary_clause_subres_lits_wl_pre C L L' S);
      let _ = log_del_binary_clause L (-L');
      let M = get_trail_wl_heur S;
      M ← cons_trail_Propagated_tr L 0 M;
      let lcount = get_learned_count S;
      let N' = get_clauses_wl_heur S;
      st ← mop_arena_status N' C;
      let st = st = IRRED;
      ASSERT (mark_garbage_pre (N', C) ∧ arena_is_valid_clause_vdom (N') C);
      let N' = extra_information_mark_to_delete (N') C;
      ASSERT(¬st ⟶ (clss_size_lcount lcount ≥ 1 ∧ clss_size_lcountUEk (clss_size_decr_lcount lcount) < learned_clss_count S));
      let lcount = (if st then lcount else (clss_size_incr_lcountUEk (clss_size_decr_lcount lcount)));
      let stats = get_stats_heur S;
      let stats = incr_binary_unit_derived (if st then decr_irred_clss stats else stats);
      let stats = incr_units_since_last_GC (incr_uset stats);
      let S = set_trail_wl_heur M S;
      let S = set_clauses_wl_heur N' S;
      let S = set_learned_count_wl_heur lcount S;
      let S = set_stats_wl_heur stats S;
      RETURN S
  }›

definition isa_deduplicate_binary_clauses_wl :: ‹nat literal ⇒ _ ⇒ isasat ⇒ (_ × isasat) nres› where
‹isa_deduplicate_binary_clauses_wl L CS S0 = do {
    let CS = CS;
    l ← mop_length_watched_by_int S0 L;
    ASSERT (l ≤ length (get_clauses_wl_heur S0) - 2);
    val ← mop_polarity_pol (get_trail_wl_heur S0) L;
    (_, _, CS, S) ← WHILET(λ(abort, i, CS, S). ¬abort ∧ i < l ∧ get_conflict_wl_is_None_heur S)
      (λ(abort, i, CS, S).
      do {
         ASSERT (i < l);
         ASSERT (length (get_clauses_wl_heur S) = length (get_clauses_wl_heur S0));
         ASSERT (learned_clss_count S ≤ learned_clss_count S0);
         (C,L', b) ← mop_watched_by_app_heur S L i;
         ASSERT (C > 0 ∧ C < length (get_clauses_wl_heur S));
         st ← mop_arena_status (get_clauses_wl_heur S) C;
         if st = DELETED ∨ ¬b then
           RETURN (abort, i+1, CS, S)
         else do {
           val ← mop_polarity_pol (get_trail_wl_heur S) L';
           if val ≠ UNSET then do {
             S ← isa_simplify_clause_with_unit_st2 C S;
             val ← mop_polarity_pol (get_trail_wl_heur S) L;
             RETURN (val ≠ UNSET, i+1, CS, S)
           }
           else do {
             m ← is_marked CS (L');
             n ← (if m then get_marked CS L' else RETURN (1, True));
             if m then do {
               let C' = (if ¬snd n ⟶ st = LEARNED then C else fst n);
               CS ← (if ¬snd n ⟶ st = LEARNED then RETURN CS else update_marked CS (L') (C, st = IRRED));
               S ← isa_clause_remove_duplicate_clause_wl C' S;
               RETURN (abort, i+1, CS, S)
             } else do {
               m ← is_marked CS (-L') ;
               if m then do {
                 S ← isa_binary_clause_subres_wl C L (-L') S;
                 RETURN (True, i+1, CS, S)
               }
               else do {
                 CS ← set_marked CS (L') (C, st = IRRED);
                 RETURN (abort, i+1, CS, S)
             }
            }
          }
        }
      })
      (val ≠ UNSET, 0, CS, S0);
   CS ← empty CS;
   RETURN (CS, S)
}›

definition mark_duplicated_binary_clauses_as_garbage_pre_wl_heur :: ‹isasat ⇒ bool› where
  ‹mark_duplicated_binary_clauses_as_garbage_pre_wl_heur S ⟷
  (∃S' r u. (S, S') ∈ twl_st_heur_restart_ana' r u ∧
    mark_duplicated_binary_clauses_as_garbage_pre_wl S')›

definition isa_mark_duplicated_binary_clauses_as_garbage_wl :: ‹isasat ⇒ _ nres› where
  ‹isa_mark_duplicated_binary_clauses_as_garbage_wl S0 = (do {
     let ns = (get_vmtf_heur_array S0);
     ASSERT (mark_duplicated_binary_clauses_as_garbage_pre_wl_heur S0);
     skip ← RETURN (should_eliminate_pure_st S0);
     CS ← create (length (get_watched_wl_heur S0));
     (_, CS, S) ← WHILET⇗ λ(n,CS,S). ns = (get_vmtf_heur_array S)⇖(λ(n, CS,S). n ≠ None ∧ get_conflict_wl_is_None_heur S)
      (λ(n, CS, S). do {
        ASSERT (n ≠ None);
        let A = the n;
        ASSERT (A < length ns);
        ASSERT (A ≤ unat32_max div 2);
        S ← do {ASSERT (ns = (get_vmtf_heur_array S));
        _ ← mop_is_marked_added_heur_st S A;
        if ¬skip then RETURN (CS, S)
        else do {
          ASSERT (length (get_clauses_wl_heur S) ≤ length (get_clauses_wl_heur S0) ∧ learned_clss_count S ≤ learned_clss_count S0);
          (CS, S) ← isa_deduplicate_binary_clauses_wl (Pos A) CS S;
          ASSERT (length (get_clauses_wl_heur S) ≤ length (get_clauses_wl_heur S0) ∧ learned_clss_count S ≤ learned_clss_count S0);
          (CS, S) ← isa_deduplicate_binary_clauses_wl (Neg A) CS S;
          ASSERT (ns = (get_vmtf_heur_array S));
          RETURN (CS, S)
        }};
        RETURN (get_next (ns ! A), S)
     })
     (Some (get_vmtf_heur_fst S0), CS, S0);
    RETURN S
  })›


definition isa_mark_duplicated_binary_clauses_as_garbage_wl2 :: ‹isasat ⇒ _ nres› where
  ‹isa_mark_duplicated_binary_clauses_as_garbage_wl2 S0 = (do {
    let ns = get_vmtf_heur_array S0;
    ASSERT (mark_duplicated_binary_clauses_as_garbage_pre_wl_heur S0);
    dedup ← RETURN (should_eliminate_pure_st S0);
    CS ← create (length (get_watched_wl_heur S0));
    (_, CS, S) ← WHILET⇗ λ(n,CS, S). get_vmtf_heur_array S0 = (get_vmtf_heur_array S)⇖(λ(n, CS, S). n ≠ None ∧ get_conflict_wl_is_None_heur S)
      (λ(n, CS, S). do {
        ASSERT (n ≠ None);
        let A = the n;
        ASSERT (A < length (get_vmtf_heur_array S));
        ASSERT (A ≤ unat32_max div 2);
        (CS, S) ← do {
        _ ← mop_is_marked_added_heur_st S A;
        if ¬dedup then RETURN (CS, S)
        else do {
          ASSERT (length (get_clauses_wl_heur S) ≤ length (get_clauses_wl_heur S0) ∧ learned_clss_count S ≤ learned_clss_count S0);
          (CS, S) ← isa_deduplicate_binary_clauses_wl (Pos A) CS S;
          ASSERT (length (get_clauses_wl_heur S) ≤ length (get_clauses_wl_heur S0) ∧ learned_clss_count S ≤ learned_clss_count S0);
          (CS, S) ← isa_deduplicate_binary_clauses_wl (Neg A) CS S;
          ASSERT (ns = get_vmtf_heur_array S);
          RETURN (CS, S)
        }};
        RETURN (get_next (get_vmtf_heur_array S ! A), CS, S)
     })
     (Some (get_vmtf_heur_fst S0), CS, S0);
    RETURN S
 })›

end