Theory IsaSAT_Watch_List

theory IsaSAT_Watch_List
  imports IsaSAT_Literals
begin

chapter ‹Refinement of the Watched Function›

text ‹There is not much to say about watch lists since they are arrays of resizeable arrays,
  which are defined in a separate theory.

  However, when replacing the elements in our watch lists from ‹(nat × uint32)›
  to ‹(nat × uint32 × bool)› to enable special handling of binary clauses, we got a huge and
  unexpected slowdown, due to a much higher
  number of cache misses (roughly 3.5 times as many on a eq.atree.braun.8.unsat.cnf which also took
  66s instead of 50s). While toying with the generated ML code, we found out that our version of
  the tuples with booleans were using 40 bytes instead of 24 previously. Just merging the
  ‹uint32› and the \<^typ>‹bool› to a single ‹uint64› was sufficient to get the
  performance back.

  Remark that however, the evaluation of terms like ‹(2::uint64) ^ 32› was not done automatically
  and even worse, was redone each time, leading to a complete performance blow-up (75s on my macbook
  for eq.atree.braun.7.unsat.cnf instead of 7s).

  None of the problems appears in the LLVM code.
›

section ‹Definition›

definition map_fun_rel :: ‹(nat × 'key) set ⇒ ('b × 'a) set ⇒ ('b list × ('key ⇒ 'a)) set› where
  map_fun_rel_def_internal:
    ‹map_fun_rel D R = {(m, f). ∀(i, j)∈D. i < length m ∧ (m ! i, f j) ∈ R}›

lemma map_fun_rel_def:
  ‹⟨R⟩map_fun_rel D = {(m, f). ∀(i, j)∈D. i < length m ∧ (m ! i, f j) ∈ R}›
  unfolding relAPP_def map_fun_rel_def_internal by auto

definition mop_append_ll :: "'a list list ⇒ nat literal ⇒ 'a ⇒ 'a list list nres" where
  ‹mop_append_ll xs i x = do {
     ASSERT(nat_of_lit i < length xs);
     RETURN (append_ll xs (nat_of_lit i) x)
  }›

section ‹Operations›
lemma length_ll_length_ll_f:
  ‹(uncurry (RETURN oo length_ll), uncurry (RETURN oo length_ll_f)) ∈
     [λ(W, L). L ∈# ℒ⇩a⇩l⇩l 𝒜⇩i⇩n]⇩f ((⟨Id⟩map_fun_rel (D⇩0 𝒜⇩i⇩n)) ×⇩r nat_lit_rel) →
       ⟨nat_rel⟩ nres_rel›
  unfolding length_ll_def length_ll_f_def
  by (fastforce simp: fref_def map_fun_rel_def prod_rel_def nres_rel_def p2rel_def br_def
      nat_lit_rel_def)

lemma mop_append_ll:
   ‹(uncurry2 mop_append_ll, uncurry2 (RETURN ooo (λW i x. W(i := W i @ [x])))) ∈
    [λ((W, i), x). i ∈# ℒ⇩a⇩l⇩l 𝒜]⇩f ⟨Id⟩map_fun_rel (D⇩0 𝒜) ×⇩f Id ×⇩f Id → ⟨⟨Id⟩map_fun_rel (D⇩0 𝒜)⟩nres_rel›
  unfolding uncurry_def mop_append_ll_def
  by (intro frefI nres_relI)
    (auto intro!: ASSERT_leI simp: map_fun_rel_def append_ll_def)


definition delete_index_and_swap_update :: ‹('a ⇒ 'b list) ⇒ 'a ⇒ nat ⇒ 'a ⇒ 'b list› where
  ‹delete_index_and_swap_update W K w = W(K := delete_index_and_swap (W K) w)›

text ‹The precondition is not necessary.›
lemma delete_index_and_swap_ll_delete_index_and_swap_update:
  ‹(uncurry2 (RETURN ooo delete_index_and_swap_ll), uncurry2 (RETURN ooo delete_index_and_swap_update))
  ∈[λ((W, L), i). L ∈# ℒ⇩a⇩l⇩l 𝒜]⇩f (⟨Id⟩map_fun_rel (D⇩0 𝒜) ×⇩r nat_lit_rel) ×⇩r nat_rel →
      ⟨⟨Id⟩map_fun_rel (D⇩0 𝒜)⟩nres_rel›
  by (auto simp: delete_index_and_swap_ll_def uncurry_def fref_def nres_rel_def
      delete_index_and_swap_update_def map_fun_rel_def p2rel_def nat_lit_rel_def br_def
      nth_list_update' nat_lit_rel_def
      simp del: literal_of_nat.simps)

definition append_update :: ‹('a ⇒ 'b list) ⇒ 'a ⇒ 'b ⇒ 'a ⇒ 'b list› where
  ‹append_update W L a = W(L:= W (L) @ [a])›

type_synonym nat_clauses_l = ‹nat list list›

subsubsection ‹Refinement of the Watched Function›

definition watched_by_nth :: ‹nat twl_st_wl ⇒ nat literal ⇒ nat ⇒ nat watcher› where
  ‹watched_by_nth = (λ(M, N, D, NE, UE, NS, US, Q, W) L i. W L ! i)›

definition watched_app
  :: ‹(nat literal ⇒ (nat watcher) list) ⇒ nat literal ⇒ nat ⇒ nat watcher› where
  ‹watched_app M L i ≡ M L ! i›

lemma watched_by_nth_watched_app:
  ‹watched_by S K ! w = watched_app ((snd o snd o snd o snd o snd o snd o snd o snd) S) K w›
  by (cases S) (auto simp: watched_app_def)


lemma nth_ll_watched_app:
  ‹(uncurry2 (RETURN ooo nth_rll), uncurry2 (RETURN ooo watched_app)) ∈
     [λ((W, L), i). L ∈# (ℒ⇩a⇩l⇩l 𝒜)]⇩f ((⟨Id⟩map_fun_rel (D⇩0 𝒜)) ×⇩r nat_lit_rel) ×⇩r nat_rel →
       ⟨nat_rel ×⇩r Id⟩ nres_rel›
  unfolding watched_app_def nth_rll_def
  by (fastforce simp: fref_def map_fun_rel_def prod_rel_def nres_rel_def p2rel_def br_def
      nat_lit_rel_def)


end