Theory IsaSAT_Bump_Heuristics_State

theory IsaSAT_Bump_Heuristics_State
  imports Watched_Literals_VMTF
    IsaSAT_ACIDS
  Tuple4
begin

(*TODO: share the to_remove part of Bump_Heuristics*)
type_synonym bump_heuristics = ‹((nat, nat) acids, vmtf, bool, nat list × bool list) tuple4›

abbreviation Bump_Heuristics :: ‹_ ⇒ _ ⇒ _ ⇒ _ ⇒ bump_heuristics› where
  ‹Bump_Heuristics a b c d ≡ Tuple4 a b c d›

lemmas bump_heuristics_splits = Tuple4.tuple4.splits
hide_fact tuple4.splits

abbreviation get_stable_heuristics :: ‹bump_heuristics ⇒ (nat, nat) acids› where
  ‹get_stable_heuristics ≡ Tuple4_a›

abbreviation get_focused_heuristics :: ‹bump_heuristics ⇒ vmtf› where
  ‹get_focused_heuristics ≡ Tuple4_b›

abbreviation is_focused_heuristics :: ‹bump_heuristics ⇒ bool› where
  ‹is_focused_heuristics ≡ Tuple4_c›

abbreviation is_stable_heuristics:: ‹bump_heuristics ⇒ bool› where
  ‹is_stable_heuristics x ≡ ¬is_focused_heuristics x›

abbreviation get_bumped_variables :: ‹bump_heuristics ⇒ nat list × bool list› where
  ‹get_bumped_variables ≡ Tuple4_d›

abbreviation set_stable_heuristics :: ‹(nat, nat) acids ⇒bump_heuristics ⇒ _› where
  ‹set_stable_heuristics ≡ Tuple4.set_a›

abbreviation set_focused_heuristics :: ‹vmtf ⇒bump_heuristics ⇒ _› where
  ‹set_focused_heuristics ≡ Tuple4.set_b›

abbreviation set_is_focused_heuristics :: ‹bool ⇒bump_heuristics ⇒ _› where
  ‹set_is_focused_heuristics ≡ Tuple4.set_c›

abbreviation set_bumped_variables :: ‹nat list × bool list ⇒bump_heuristics ⇒ _› where
  ‹set_bumped_variables ≡ Tuple4.set_d›

definition get_unit_trail where
  ‹get_unit_trail M = (rev (takeWhile (λx. ¬is_decided x) (rev M)))›

definition bump_heur :: ‹_ ⇒ _ ⇒ bump_heuristics set› where
  ‹bump_heur 𝒜 M = {x.
    (is_focused_heuristics x ⟶
      (get_stable_heuristics x ∈ acids 𝒜 (get_unit_trail M)  ∧
      get_focused_heuristics x ∈ vmtf 𝒜 M)) ∧
    (¬is_focused_heuristics x ⟶
      (get_stable_heuristics x ∈ acids 𝒜 M ∧
       get_focused_heuristics x ∈ vmtf 𝒜 (get_unit_trail M))) ∧
   (get_bumped_variables x, set (fst (get_bumped_variables x))) ∈ distinct_atoms_rel 𝒜
  }›

definition switch_bump_heur :: ‹bump_heuristics ⇒ bump_heuristics› where
  ‹switch_bump_heur x = do {
    (set_is_focused_heuristics (¬(is_focused_heuristics x)) x)
  }›

lemma get_unit_trail_count_decided_0[simp]: ‹count_decided M = 0 ⟹ get_unit_trail M = M›
  by (auto simp: get_unit_trail_def count_decided_0_iff)
   (metis rev_swap set_rev takeWhile_eq_all_conv)

lemma switch_bump_heur:
  assumes ‹x ∈ bump_heur 𝒜 M› and
    ‹count_decided M = 0›
  shows ‹switch_bump_heur x ∈ bump_heur 𝒜 M›
  using assms
  by (cases x)
   (auto simp: switch_bump_heur_def bump_heur_def)


subsection ‹Access Function›
definition isa_bump_unset_pre where
  ‹isa_bump_unset_pre = (λL x.
  (is_focused_heuristics x ⟶ vmtf_unset_pre L (get_focused_heuristics x)) ∧
  (is_stable_heuristics x ⟶ acids_tl_pre L (get_stable_heuristics x))
  )›
definition isa_bump_unset :: ‹nat ⇒ bump_heuristics ⇒ bump_heuristics nres› where
  ‹isa_bump_unset L vm = (case vm of Tuple4 (hstable) (focused) foc a ⇒ do {
  hstable ← (if ¬foc then acids_tl L hstable else RETURN hstable);
  let focused = (if foc then vmtf_unset L focused else focused);
  RETURN (Tuple4 hstable focused foc a)
  })›

lemma get_unit_trail_simps[simp]: ‹is_decided L ⟹ get_unit_trail (L # M) = get_unit_trail M›
  ‹¬is_decided L ⟹ count_decided M = 0 ⟹ get_unit_trail (L # M) = L # M›
  ‹¬is_decided L ⟹ count_decided M > 0 ⟹ get_unit_trail (L # M) = get_unit_trail M›
  apply (auto simp: get_unit_trail_def takeWhile_append)
  apply (metis set_rev takeWhile_eq_all_conv)
  apply (metis count_decided_0_iff nat_neq_iff)
  using bot_nat_0.not_eq_extremum count_decided_0_iff by blast

lemma get_unit_trail_cons_if:
  ‹get_unit_trail (L # M) = (if is_decided L then get_unit_trail M else if count_decided M = 0 then L # M else get_unit_trail M)›
  by (auto simp: takeWhile_append)

lemma get_unit_trail_tl[simp]: ‹count_decided M > 0 ⟹ get_unit_trail (tl M) = get_unit_trail M›
  by (cases M; cases ‹hd M›) auto

lemma isa_vmtf_consD:
  ‹x ∈ bump_heur 𝒜 M ⟹ x ∈ bump_heur 𝒜 (L # M)›
  by (auto simp add: bump_heur_def takeWhile_append get_unit_trail_cons_if
      intro!: vmtf_consD' acids_prepend)


lemma isa_bump_unset_vmtf_tl:
  fixes M
  defines [simp]: ‹L ≡ atm_of (lit_of (hd M))›
  assumes vmtf: ‹x∈ bump_heur 𝒜 M› and
    L_N: ‹L ∈ atms_of (ℒ⇩a⇩l⇩l 𝒜)› and [simp]: ‹M ≠ []› and
    nz: ‹count_decided M > 0›
  shows ‹isa_bump_unset L x ≤ SPEC (λa. a ∈ bump_heur 𝒜 (tl M))›
proof -
  obtain ns m fst_As lst_As next_search where
    ‹is_focused_heuristics x ⟹ get_focused_heuristics x = ((ns, m, fst_As, lst_As, next_search))›
   by (cases ‹get_focused_heuristics x›; cases ‹is_focused_heuristics x›) auto
  then show ?thesis
    using vmtf_unset_vmtf_tl[of ns m fst_As lst_As next_search 𝒜 M] nz
      assms unfolding isa_bump_unset_def apply (cases x, simp only: tuple4.case Let_def)
    apply (cases ‹is_focused_heuristics x›)
    subgoal
      by (refine_vcg acids_tl[of _ 𝒜 M, THEN order_trans])
       (auto simp: bump_heur_def isa_bump_unset_def split: bump_heuristics_splits)
    subgoal
      by (refine_vcg acids_tl[of _ 𝒜 M, THEN order_trans])
        (auto simp: bump_heur_def isa_bump_unset_def atms_of_ℒ⇩a⇩l⇩l_𝒜⇩i⇩n split: bump_heuristics_splits)
    done
qed


  (*TODO: this should probably be only the focused version, but for our first porting experiments, let's
  implement the switching version*)
definition bump_get_heuristics :: ‹_ ⇒ vmtf› where
  ‹bump_get_heuristics x = (get_focused_heuristics x)›

definition length_bumped_vmtf_array :: ‹bump_heuristics ⇒ nat› where
  ‹length_bumped_vmtf_array x =
  length (fst (bump_get_heuristics x))›

definition current_vmtf_array_nxt_score :: ‹bump_heuristics ⇒ nat› where
  ‹current_vmtf_array_nxt_score x = fst (snd (bump_get_heuristics x))›
definition access_focused_vmtf_array where
  ‹access_focused_vmtf_array x i = do {
  ASSERT (i < length (fst (bump_get_heuristics x)));
  RETURN (fst (bump_get_heuristics x) ! i)}›

definition bumped_vmtf_array_fst where
  ‹bumped_vmtf_array_fst x =
  fst (snd (snd (bump_get_heuristics x)))›

definition isa_bump_mark_to_rescore
  :: ‹nat ⇒ bump_heuristics ⇒ bump_heuristics nres›
where
  ‹isa_bump_mark_to_rescore L x = (case x of Bump_Heuristics a b c d ⇒ do {
    ASSERT (atms_hash_insert_pre L d);
    RETURN (Bump_Heuristics a b c (atoms_hash_insert L d))
  })›


end