Theory IsaSAT_Watch_List

theory IsaSAT_Watch_List
  imports IsaSAT_Literals IsaSAT_Clauses Watched_Literals.Watched_Literals_Watch_List_Initialisation
    Pairing_Heap_LLVM.Map_Fun_Rel
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 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 ∈# ℒall 𝒜in]f ((⟨Id⟩map_fun_rel (D0 𝒜in)) ×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 ∈# ℒall 𝒜]f ⟨Id⟩map_fun_rel (D0 𝒜) ×f Id ×f Id → ⟨⟨Id⟩map_fun_rel (D0 𝒜)⟩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 ∈# ℒall 𝒜]f (⟨Id⟩map_fun_rel (D0 𝒜) ×r nat_lit_rel) ×r nat_rel →
      ⟨⟨Id⟩map_fun_rel (D0 𝒜)⟩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)


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, NEk, UEk, NS, US, N0, U0, 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 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 ∈# (ℒall 𝒜)]f ((⟨Id⟩map_fun_rel (D0 𝒜)) ×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)




section ‹Rewatch›

definition rewatch_heur where
‹rewatch_heur vdom arena W = do {
  let _ = vdom;
  nfoldli [0..<length vdom] (λ_. True)
   (λi W. do {
      ASSERT(i < length vdom);
      let C = vdom ! i;
      ASSERT(arena_is_valid_clause_vdom arena C);
      if arena_status arena C ≠ DELETED
      then do {
        L1 ← mop_arena_lit2 arena C 0;
        L2 ← mop_arena_lit2 arena C 1;
        n ← mop_arena_length arena C;
        let b = (n = 2);
        ASSERT(length (W ! (nat_of_lit L1)) < length arena);
        W ← mop_append_ll W L1 (C, L2, b);
        ASSERT(length (W ! (nat_of_lit L2)) < length arena);
        W ← mop_append_ll W L2 (C, L1, b);
        RETURN W
      }
      else RETURN W
    })
   W
  }›

lemma rewatch_heur_rewatch:
  assumes
    valid: ‹valid_arena arena N vdom› and ‹set xs ⊆ vdom› and ‹distinct xs› and ‹set_mset (dom_m N) ⊆ set xs› and
    ‹(W, W') ∈ ⟨Id⟩map_fun_rel (D0 𝒜)› and lall: ‹literals_are_in_ℒin_mm 𝒜 (mset `# ran_mf N)› and
    ‹vdom_m 𝒜 W' N ⊆ set_mset (dom_m N)›
  shows
    ‹rewatch_heur xs arena W ≤ ⇓ ({(W, W'). (W, W') ∈⟨Id⟩map_fun_rel (D0 𝒜) ∧ vdom_m 𝒜 W' N ⊆ set_mset (dom_m N)}) (rewatch N W')›
proof -
  have [refine0]: ‹(xs, xsa) ∈ Id ⟹
     ([0..<length xs], [0..<length xsa]) ∈ ⟨{(x, x'). x = x' ∧ x < length xsa ∧ xs!x ∈ vdom}⟩list_rel›
    for xsa
    using assms unfolding list_rel_def
    by (auto simp: list_all2_same)
  show ?thesis
    unfolding rewatch_heur_def rewatch_def
    apply (subst (2) nfoldli_nfoldli_list_nth)
    apply (refine_vcg mop_arena_lit[OF valid] mop_append_ll[of 𝒜, THEN fref_to_Down_curry2, unfolded comp_def]
       mop_arena_length[of vdom, THEN fref_to_Down_curry, unfolded comp_def])
    subgoal
      using assms by fast
    subgoal
      using assms by fast
    subgoal
      using assms by fast
    subgoal by fast
    subgoal by auto
    subgoal
      using assms
      unfolding arena_is_valid_clause_vdom_def
      by blast
    subgoal
      using assms
      by (auto simp: arena_dom_status_iff)
    subgoal for xsa xi x si s
      using assms
      by auto
    subgoal by simp
    subgoal by linarith
    subgoal for xsa xi x si s
      using assms
      unfolding arena_lit_pre_def
      by (auto)
    subgoal by simp
    subgoal by simp
    subgoal by simp
    subgoal for xsa xi x si s
      using assms
      unfolding arena_is_valid_clause_idx_and_access_def
        arena_is_valid_clause_idx_def
      by (auto simp: arena_is_valid_clause_idx_and_access_def
          intro!: exI[of _ N] exI[of _ vdom])
    subgoal for xsa xi x si s
      using valid_arena_size_dom_m_le_arena[OF assms(1)] assms
         literals_are_in_ℒin_mm_in_ℒall[OF lall, of  ‹xs ! xi› 0]
      by (auto simp: map_fun_rel_def arena_lifting)
    subgoal for xsa xi x si s
      using valid_arena_size_dom_m_le_arena[OF assms(1)] assms
         literals_are_in_ℒin_mm_in_ℒall[OF lall, of  ‹xs ! xi› 0]
      by (auto simp: map_fun_rel_def arena_lifting)
    subgoal using assms by (simp add: arena_lifting)
    subgoal for xsa xi x si s
      using literals_are_in_ℒin_mm_in_ℒall[OF lall, of  ‹xs ! xi› 1]
      assms valid_arena_size_dom_m_le_arena[OF assms(1)]
      by (auto simp: arena_lifting append_ll_def map_fun_rel_def)
    subgoal for xsa xi x si s
      using literals_are_in_ℒin_mm_in_ℒall[OF lall, of  ‹xs ! xi› 1]
        assms
      by (auto simp: arena_lifting append_ll_def map_fun_rel_def)
    subgoal for xsa xi x si s
      using assms
      by (auto simp: arena_lifting append_ll_def map_fun_rel_def)
    subgoal for xsa xi x si s
      using assms
      by (auto simp: arena_lifting append_ll_def map_fun_rel_def)
    done
qed

lemma rewatch_heur_alt_def:
‹rewatch_heur vdom arena W = do {
  let _ = vdom;
  nfoldli [0..<length vdom] (λ_. True)
   (λi W. do {
      ASSERT(i < length vdom);
      let C = vdom ! i;
      ASSERT(arena_is_valid_clause_vdom arena C);
      if arena_status arena C ≠ DELETED
      then do {
        L1 ← mop_arena_lit2 arena C 0;
        L2 ← mop_arena_lit2 arena C 1;
        n ← mop_arena_length arena C;
        let b = (n = 2);
        ASSERT(length (W ! (nat_of_lit L1)) < length arena);
        W ← mop_append_ll W L1 (C, L2, b);
        ASSERT(length (W ! (nat_of_lit L2)) < length arena);
        W ← mop_append_ll W L2 (C, L1, b);
        RETURN W
      }
      else RETURN W
    })
   W
  }›
  unfolding Let_def rewatch_heur_def
  by auto

definition watchlist_put_binaries_first_one :: ‹_› where
  ‹watchlist_put_binaries_first_one W0 L = do {
      ASSERT (L < length W0);
      let m = length (W0 ! L);
      (_, _, W) ← WHILET⇗(λ(i,j,W). length W = length W0 ∧ length (W ! L) = length (W0 ! L) ∧ i ≤ j ∧ (∀K. mset (W ! K) = mset (W0 ! K)))⇖ (λ(i,j,W). j < m)
       (λ(i,j,W). do {
          ASSERT (j < length (W ! L));
          let (_, _, b) = W ! L ! j;
          if b then RETURN (i+1,j+1, W[L := swap (W!L) i j])
          else RETURN (i+1, j+1, W)
       })
       (0, 0, W0);
    RETURN W
}›

definition watchlist_put_binaries_first :: ‹_› where
  ‹watchlist_put_binaries_first W0 = do {
     let m = length W0;
      (_, W) ← WHILET⇗ λ(i, W). length W = length W0 ∧ (∀K. mset (W ! K) = mset (W0 ! K))⇖  (λ(i,W). i < m)
       (λ(i,W). do {
          ASSERT (i < length (W));
          W ← watchlist_put_binaries_first_one W i;
          RETURN (i+1, W)
       })
       (0, W0);
    RETURN W
}›




definition rewatch_heur_and_reorder where
‹rewatch_heur_and_reorder vdom arena W = do {
    W ← rewatch_heur vdom arena W;
    watchlist_put_binaries_first W}›


end